Initialisation.lean

本页保留 Lean 源码及行号。点击行号可定位语句，点击 import 中的模块名可查看依赖。

1import ZlibF.Spec.Api.Basic
2import ZlibF.Spec.Public.StreamQueries
3import ZlibF.Proof.«inflate.c.base»
4import ZlibF.Proof.«deflate.c.base»
5
6namespace ZlibF.Spec.Public
7open C
8
9/-- A frame over existing allocations. New allocations are governed separately by `LiveChange`. -/
10def Frame (before after : Heap) (changed : Nat → Prop) : Prop :=
11  before.static = after.static ∧ before.allocOk = after.allocOk ∧ before.garbage = after.garbage ∧
12  before.nextBlk ≤ after.nextBlk ∧ before.nalloc ≤ after.nalloc ∧
13  ∀ b, before.live b → ¬ changed b →
14    after.bytes b = before.bytes b ∧ after.words b = before.words b ∧
15    after.streams b = before.streams b ∧ after.gzheaders b = before.gzheaders b ∧
16    after.dstates b = before.dstates b ∧ after.istates b = before.istates b ∧
17    after.gzstates b = before.gzstates b ∧ after.ro b = before.ro b
18
19/-- An exact allocation ledger. A live allocation cannot disappear or remain unaccounted for. -/
20def LiveChange (before after : Heap) (created removed : Nat → Prop) : Prop :=
21  ∀ b, after.live b ↔ (before.live b ∧ ¬ removed b) ∨ created b
22
23def StreamRoot (r : ZStreamRef) (b : Nat) : Prop :=
24  match r with | .tab i | .in_gzstate_strm i => b = i
25
26def InflateOwned (i : Nat) (s : InflateState) (b : Nat) : Prop :=
27  b = i ∨ s.window = .ref (.blk b) 0
28
29def DeflateOwned (i : Nat) (s : DeflateState) (b : Nat) : Prop :=
30  b = i ∨ s.window = .ref (.blk b) 0 ∨ s.prev = .ref (.blk b) 0 ∨
31  s.head = .ref (.blk b) 0 ∨ s.pending_buf = .ref (.blk b) 0
32
33def DefaultOrNull (z : ZStream) : Prop :=
34  (z.zalloc = .null ∨ z.zalloc = .fn "zcalloc") ∧
35  (z.zfree = .null ∨ z.zfree = .fn "zcfree")
36
37def preparedStream (z : ZStream) : ZStream :=
38  { z with
39    msg := .null
40    zalloc := if z.zalloc == .null then .fn "zcalloc" else z.zalloc
41    «opaque» := if z.zalloc == .null then .null else z.opaque
42    zfree := if z.zfree == .null then .fn "zcfree" else z.zfree }
43
44/-- The version check reads only the first byte; the null version is a clean error. -/
45def VersionValue (h : Heap) (p : BPtr) (head : Option UInt8) : Prop :=
46  (p = .null ∧ head = none) ∨ ∃ b, head = some b ∧ Bytes h p 1 [b]
47
48def WindowAllocation (h : Heap) (p : BPtr) : Prop :=
49  p = .null ∨ ∃ b a, p = .ref (.blk b) 0 ∧ h.bytes b = some a ∧ h.ro b = false
50
51/-- Remove a writable byte allocation. Read-only metadata, including its table shape, is
52unchanged. Callers establish WindowAllocation or the corresponding owned-message condition. -/
53def dropWindow (h : Heap) : BPtr → Heap
54  | .ref (.blk b) 0 => { h with bytes := upd h.bytes b none }
55  | _ => h
56
57/-- Init's successful representation includes the complete established invariant, not an
58invariant supplied by the caller. The single allocation is the new state record. -/
59def InflateInitial (before after : Heap) (r : ZStreamRef) (wrap : Api.Wrap) (bits : Nat) : Prop :=
60  ∃ z s, Zlib.Inflate.Spec.Good after r before.nextBlk z s ∧
61    z.zalloc = .fn "zcalloc" ∧ z.zfree = .fn "zcfree" ∧
62    s.mode = HEAD ∧ s.window = .null ∧ s.wbits.toNat = bits ∧ s.reqbits.toNat = bits ∧
63    s.wrap = (match wrap with | .raw => 0 | .zlib => 5 | .gzip => 6 | .auto => 7) ∧
64    s.reqwrap = s.wrap ∧ s.wsize = 0 ∧ s.whave = 0 ∧ s.wnext = 0 ∧
65    s.hold = 0 ∧ s.bits = 0 ∧ s.havedict = 0 ∧ s.head = none ∧
66    z.total_in = 0 ∧ z.total_out = 0 ∧ z.msg = .null ∧
67    Frame before after (StreamRoot r) ∧
68    LiveChange before after (fun b => b = before.nextBlk) (fun _ => False)
69
70/-- Allocation precedes the window-bit check in inflate init. In particular, an invalid
71window configuration can return `Z_MEM_ERROR` before it returns `Z_STREAM_ERROR`. -/
72def InflateInitContract (program : ZStreamPtr → BPtr → Int32 → M Int32) (wb : Int32) : Prop :=
73  (∀ h p version head size, VersionValue h version head →
74    (head ≠ some 49 ∨ size ≠ 112) → C.run (program p version size) h = .ok (Z_VERSION_ERROR, h)) ∧
75  (∀ h version, VersionValue h version (some 49) →
76    C.run (program none version 112) h = .ok (Z_STREAM_ERROR, h)) ∧
77  (∀ h r z version, Fresh h → Zlib.Inflate.Spec.Uniq h → LibraryGlobals h →
78    r.get h = some z → DefaultOrNull z → VersionValue h version (some 49) →
79    ∃ rc after, C.run (program (some r) version 112) h = .ok (rc, after) ∧
80      after.nalloc = h.nalloc + 1 ∧
81      (if h.allocOk h.nalloc = false then
82        rc = Z_MEM_ERROR ∧ SameObjects (r.put h (preparedStream z)) after
83      else match Api.inflWbits wb.toInt with
84      | none => rc = Z_STREAM_ERROR ∧
85          SameObjects (r.put h { preparedStream z with state := none }) after
86      | some (wrap, bits) => rc = Z_OK ∧ InflateInitial h after r wrap bits))
87
88/-- `int inflateInit2_(z_streamp strm, int windowBits, const char *version, int stream_size)`.
89All signed window arguments and every allocation oracle are included, in source error order. -/
90def Goal.inflateInit2_ : Prop :=
91  ∀ wb, InflateInitContract (fun p v size => Zlib.Inflate.inflateInit2_ p wb v size) wb
92
93/-- `int inflateInit_(z_streamp strm, const char *version, int stream_size)`.
94The same version, stream, allocation, cleanup and invariant contract at window bits 15. -/
95def Goal.inflateInit_ : Prop := InflateInitContract Zlib.Inflate.inflateInit_ 15
96
97def DeflateInitial (before after : Heap) (r : ZStreamRef) (p : Api.DeflParams) : Prop :=
98  ∃ z s, Zlib.Deflate.Spec.DGood after r before.nextBlk z s ∧
99    z.zalloc = .fn "zcalloc" ∧ z.zfree = .fn "zcfree" ∧
100    s.level.toInt = p.level ∧ s.strategy.toInt = p.strategy ∧ s.w_bits.toNat = p.wbits ∧
101    s.hash_bits.toNat = p.memLevel + 7 ∧
102    s.wrap = (match p.wrap with | .raw => 0 | .zlib => 1 | .gzip => 2) ∧
103    s.strstart = 0 ∧ s.lookahead = 0 ∧ s.pending = 0 ∧ s.bi_valid = 0 ∧ s.gzhead = none ∧
104    z.total_in = 0 ∧ z.total_out = 0 ∧ z.msg = .null ∧
105    Frame before after (StreamRoot r) ∧
106    LiveChange before after (DeflateOwned before.nextBlk s) (fun _ => False) ∧
107    (∀ b, DeflateOwned before.nextBlk s b ↔ before.nextBlk ≤ b ∧ b < before.nextBlk + 5)
108
109/-- Deflate validates parameters before allocating. Once the state allocation succeeds it
110attempts all four buffer allocations, even when an earlier buffer allocation failed. -/
111def DeflateInitContract (program : ZStreamPtr → BPtr → Int32 → M Int32)
112    (level method wb mem strategy : Int32) : Prop :=
113  (∀ h p version head size, VersionValue h version head →
114    (head ≠ some 49 ∨ size ≠ 112) → C.run (program p version size) h = .ok (Z_VERSION_ERROR, h)) ∧
115  (∀ h version, VersionValue h version (some 49) →
116    C.run (program none version 112) h = .ok (Z_STREAM_ERROR, h)) ∧
117  (∀ h r z version, Fresh h → Zlib.Deflate.Spec.Uniq h → LibraryGlobals h →
118    r.get h = some z → DefaultOrNull z → VersionValue h version (some 49) →
119    ∃ rc after, C.run (program (some r) version 112) h = .ok (rc, after) ∧
120      (match Api.deflInit? level.toInt method.toInt wb.toInt mem.toInt strategy.toInt with
121      | none => rc = Z_STREAM_ERROR ∧ SameObjects (r.put h (preparedStream z)) after ∧
122          after.nalloc = h.nalloc
123      | some p =>
124        if h.allocOk h.nalloc = false then
125          rc = Z_MEM_ERROR ∧ after.nalloc = h.nalloc + 1 ∧
126          SameObjects (r.put h (preparedStream z)) after
127        else after.nalloc = h.nalloc + 5 ∧
128          if (List.range 5).all (fun j => h.allocOk (h.nalloc + j)) then
129            rc = Z_OK ∧ DeflateInitial h after r p
130          else rc = Z_MEM_ERROR ∧
131            (∃ z', r.get after = some z' ∧ z'.state = none) ∧
132            LiveChange h after (fun _ => False) (fun _ => False) ∧
133            Frame h after (StreamRoot r)))
134
135/-- `int deflateInit2_(z_streamp strm, int level, int method, int windowBits, int memLevel,
136int strategy, const char *version, int stream_size)`.
137Every signed argument, source-ordered refusal, five allocations, failure cleanup and success invariant. -/
138def Goal.deflateInit2_ : Prop :=
139  ∀ level method wb mem strategy,
140    DeflateInitContract (fun p v size => Zlib.Deflate.deflateInit2_ p level method wb mem strategy v size)
141      level method wb mem strategy
142
143/-- `int deflateInit_(z_streamp strm, int level, const char *version, int stream_size)`.
144The default method, window, memory level and strategy; the level remains arbitrary. -/
145def Goal.deflateInit_ : Prop :=
146  ∀ level, DeflateInitContract (fun p v size => Zlib.Deflate.deflateInit_ p level v size)
147    level 8 15 8 0
148
149end ZlibF.Spec.Public