infback.c.init.lean

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

1import ZlibF.Proof.«inflate.c.start»
2import ZlibF.Zlib.«infback.c»
3
4/-!
5# infback.c: `inflateBackInit_`
6
7The caller supplies the window (`zlib.h`: a buffer of `1 << windowBits` bytes that stays valid and is not touched by the
8caller until `inflateBack` returns). `inflateBackInit_` only stores the pointer. It allocates the state record and
9leaves all fields except seven unwritten: the heap record is the allocator's arbitrary content with those seven fields
10set (`backState`).
11
12The state of a stream set up by `inflateBackInit_` is not an `inflate` state: nothing points back to the stream
13(`strm` is not written) and `inflateStateCheck` is not run by `inflateBack` or `inflateBackEnd`. The invariant is
14therefore its own (`BackInv`, `BackGood`).
15-/
16
17namespace Zlib.Infback.Spec
18open C Zlib.Inflate Zlib.Inflate.Spec
19
20/-- The state record after `inflateBackInit_` has written its fields: the allocator's arbitrary content `g`, with
21`dmax`, `wbits`, `wsize`, `window`, `wnext`, `whave` and `sane` set. -/
22def backState (g : Nat → UInt64) (window : BPtr) (wb : Int32) : InflateState :=
23  { InflateState.garbage g with
24    dmax := 32768, wbits := i2u wb, wsize := (1 : UInt32) <<< (i2u wb), window := window, wnext := 0, whave := 0,
25    sane := 1 }
26
27/-- The heap after a successful `inflateBackInit_`: the state is the block `h.nextBlk`, holding `backState`; the stream
28record has the default allocator functions, no message, and points to the state. -/
29def backOkHeap (h : Heap) (r : ZStreamRef) (z : ZStream) (window : BPtr) (wb : Int32) : Heap :=
30  r.put (allocIstHeap (r.put h (initStream z)) (backState (h.garbage h.nalloc) window wb)) (initStream2 z h.nextBlk)
31
32/-- The caller's window: `n` writable bytes of a byte block, starting at the pointer. -/
33def WindowOk (h : Heap) (window : BPtr) (n : Nat) : Prop :=
34  ∃ w off a, window = .ref (.blk w) off ∧ h.bytes w = some a ∧ h.ro w = false ∧ off + n ≤ a.size
35
36/-- The representation invariant of a state that `inflateBackInit_` made: the arrays have the declared lengths,
37`windowBits` is 8 to 15, `wsize` is `2^wbits`, and the window is the caller's writable buffer of `wsize` bytes. -/
38structure BackInv (h : Heap) (st : InflateState) : Prop where
39  wf : st.WellFormed
40  wbits : 8 ≤ st.wbits.toNat ∧ st.wbits.toNat ≤ 15
41  wsize : st.wsize.toNat = 2 ^ st.wbits.toNat
42  win : WindowOk h st.window st.wsize.toNat
43
44/-- A stream set up by `inflateBackInit_`: the stream record `z` is the stream `r`, its state is the record `st` at
45block `zs`, the allocator functions are the default ones, and the heap is well formed. -/
46structure BackGood (h : Heap) (r : ZStreamRef) (zs : Nat) (z : ZStream) (st : InflateState) : Prop where
47  hz : r.get h = some z
48  hs : h.istates zs = some st
49  zst : z.state = some (.inflate zs)
50  zalloc : z.zalloc = .fn "zcalloc"
51  zfree : z.zfree = .fn "zcfree"
52  inv : BackInv h st
53  uniq : Uniq h
54  fresh : Fresh h
55
56end Zlib.Infback.Spec
57
58namespace Zlib.Infback.Proofs
59open C Zlib.Inflate Zlib.Inflate.Spec Zlib.Inflate.Proofs Zlib.Infback Zlib.Infback.Spec
60
61theorem inflateBackInit__version_null (strm : ZStreamPtr) (wb : Int32) (window : BPtr) (sz : Int32) (h : Heap) :
62    inflateBackInit_ strm wb window .null sz h = .ok (Z_VERSION_ERROR, h) := by
63  simp [inflateBackInit_]
64
65theorem inflateBackInit__version_char (strm : ZStreamPtr) (wb : Int32) (window version : BPtr) (sz : Int32) (h : Heap)
66    (c : UInt8) (hv : version ≠ .null) (hc : index8 version 0 h = .ok (c, h)) (hne : c ≠ 49) :
67    inflateBackInit_ strm wb window version sz h = .ok (Z_VERSION_ERROR, h) := by
68  simp [inflateBackInit_, hv, hc, hne]
69
70theorem inflateBackInit__version_size (strm : ZStreamPtr) (wb : Int32) (window version : BPtr) (sz : Int32) (h : Heap)
71    (hv : version ≠ .null) (hc : index8 version 0 h = .ok (49, h)) (hne : sz ≠ 112) :
72    inflateBackInit_ strm wb window version sz h = .ok (Z_VERSION_ERROR, h) := by
73  simp [inflateBackInit_, hv, hc, hne]
74
75/-- The parameter check: no stream, no window, or `windowBits` outside 8 to 15 returns `Z_STREAM_ERROR` and changes
76nothing. -/
77theorem inflateBackInit__stream_error (strm : ZStreamPtr) (wb : Int32) (window version : BPtr) (h : Heap)
78    (hv : version ≠ .null) (hc : index8 version 0 h = .ok (49, h))
79    (hbad : strm = none ∨ window = .null ∨ wb < 8 ∨ wb > 15) :
80    inflateBackInit_ strm wb window version 112 h = .ok (Z_STREAM_ERROR, h) := by
81  have c : ((strm = none ∨ window = Ptr.null) ∨ wb < 8) ∨ 15 < wb := by
82    rcases hbad with e | e | e | e
83    · exact Or.inl (Or.inl (Or.inl e))
84    · exact Or.inl (Or.inl (Or.inr e))
85    · exact Or.inl (Or.inr e)
86    · exact Or.inr e
87  simp [inflateBackInit_, hv, hc, c]
88
89theorem inflateBackInit__memfail {h : Heap} {r : ZStreamRef} {z : ZStream} {wb : Int32} {window version : BPtr}
90    (hz : r.get h = some z) (_hF : Fresh h) (hok : ¬ h.allocOk h.nalloc = true)
91    (hza : z.zalloc = .null ∨ z.zalloc = .fn "zcalloc") (hzf : z.zfree = .null ∨ z.zfree = .fn "zcfree")
92    (hv : version ≠ .null) (hv0 : OkOn h (index8 version 0) 49) (hw : window ≠ .null) (h8 : ¬ wb < 8) (h15 : ¬ wb > 15) :
93    inflateBackInit_ (some r) wb window version 112 h = .ok (Z_MEM_ERROR, initMemHeap h r z) := by
94  have hv0' : index8 version 0 h = .ok (49, h) := hv0
95  unfold inflateBackInit_
96  rcases hza with hza | hza <;> rcases hzf with hzf | hzf <;>
97  isimp [hz, hv, hv0', hw, h8, h15, initStream, hza, hzf, zallocs_run, allocIst_fail_put (r := r) hok, initMemHeap]
98
99theorem i2u_range {wb : Int32} (h8 : ¬ wb < 8) (h15 : ¬ wb > 15) : 8 ≤ (i2u wb).toNat ∧ (i2u wb).toNat ≤ 15 := by
100  have h1' : ¬ wb < Int32.ofInt 8 := h8
101  have h2' : ¬ Int32.ofInt 15 < wb := h15
102  rw [int32_lt_c wb 8 (by omega) (by omega)] at h1'
103  rw [Int32.lt_iff_toInt_lt, int32_ofInt_toInt 15 (by omega) (by omega)] at h2'
104  have hlo := wb.le_toInt
105  have hhi := wb.toInt_lt
106  obtain ⟨k, hk⟩ : ∃ k, k = wb.toInt := ⟨_, rfl⟩
107  have hw : wb = Int32.ofInt k := by rw [hk]; exact (Int32.ofInt_toInt wb).symm
108  have hk1 : 8 ≤ k := by omega
109  have hk2 : k ≤ 15 := by omega
110  rw [hw]
111  have hc : k = 8 ∨ k = 9 ∨ k = 10 ∨ k = 11 ∨ k = 12 ∨ k = 13 ∨ k = 14 ∨ k = 15 := by omega
112  rcases hc with rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl <;> decide
113
114theorem shl32_one {n : UInt32} (hn : n.toNat ≤ 15) : ((1 : UInt32) <<< n).toNat = 2 ^ n.toNat := by
115  rw [UInt32.toNat_shiftLeft]
116  have : n.toNat % 32 = n.toNat := Nat.mod_eq_of_lt (by omega)
117  rw [this]
118  have h2 : 2 ^ n.toNat < 2 ^ 32 := Nat.pow_lt_pow_right (by omega) (by omega)
119  simp [Nat.shiftLeft_eq, Nat.mod_eq_of_lt h2]
120
121theorem shl32_one_run (wb : Int32) (h8 : ¬ wb < 8) (h15 : ¬ wb > 15) (h : Heap) :
122    shl32 1 (i2u wb) h = .ok ((1 : UInt32) <<< (i2u wb), h) := by
123  have := (i2u_range h8 h15).2
124  have hl : i2u wb < 32 := by rw [UInt32.lt_iff_toNat_lt]; simpa using (by omega : (i2u wb).toNat < 32)
125  simp [shl32, hl]
126
127theorem inflateBackInit__success {h : Heap} {r : ZStreamRef} {z : ZStream} {wb : Int32} {window version : BPtr}
128    (hz : r.get h = some z) (hF : Fresh h) (hok : h.allocOk h.nalloc = true)
129    (hza : z.zalloc = .null ∨ z.zalloc = .fn "zcalloc") (hzf : z.zfree = .null ∨ z.zfree = .fn "zcfree")
130    (hv : version ≠ .null) (hv0 : OkOn h (index8 version 0) 49) (hw : window ≠ .null) (h8 : ¬ wb < 8) (h15 : ¬ wb > 15) :
131    inflateBackInit_ (some r) wb window version 112 h = .ok (Z_OK, backOkHeap h r z window wb) := by
132  have hv0' : index8 version 0 h = .ok (49, h) := hv0
133  unfold inflateBackInit_
134  rcases hza with hza | hza <;> rcases hzf with hzf | hzf <;>
135  isimp [hz, hv, hv0', hw, h8, h15, initStream, hza, hzf, zallocs_run, allocIst_put hz hok hF, shl32_one_run wb h8 h15,
136    backOkHeap, backState, initStream2, StateRef.ofInflateState]
137
138theorem wf_backState (g : Nat → UInt64) (window : BPtr) (wb : Int32) : (backState g window wb).WellFormed := by
139  simp [backState, InflateState.WellFormed, InflateState.garbage]
140
141/-- **inflateBackInit_, success.** With a correct release string and `stream_size`, a non-null window, `windowBits` 8 to
14215 and a successful allocation, the call returns `Z_OK` without a fault. The new state is the block `h.nextBlk`
143(nothing else is allocated); the stream record has the default allocator functions, a null message and points to the
144state; the representation invariant holds when the window is the caller's writable buffer of `2^windowBits` bytes
145(`zlib.h`); the stream owns exactly one more block, the state (the window stays the caller's). The allocator functions of
146the caller's record are `NULL` or the default ones (the model has no others). -/
147theorem inflateBackInit__ok {h : Heap} {r : ZStreamRef} {z : ZStream} {wb : Int32} {window version : BPtr}
148    (hU : Uniq h) (hF : Fresh h) (hz : r.get h = some z) (hok : h.allocOk h.nalloc = true)
149    (hza : z.zalloc = .null ∨ z.zalloc = .fn "zcalloc") (hzf : z.zfree = .null ∨ z.zfree = .fn "zcfree")
150    (hv : version ≠ .null) (hv0 : OkOn h (index8 version 0) 49) (h8 : ¬ wb < 8) (h15 : ¬ wb > 15)
151    (hwin : WindowOk h window (2 ^ (i2u wb).toNat)) :
152    ∃ h', C.run (inflateBackInit_ (some r) wb window version 112) h = .ok (Z_OK, h') ∧ h' = backOkHeap h r z window wb ∧
153      BackGood h' r h.nextBlk (initStream2 z h.nextBlk) (backState (h.garbage h.nalloc) window wb) ∧
154      (∀ S, h.Owns S → h'.Owns (fun b => S b ∨ b = h.nextBlk)) := by
155  have hw : window ≠ .null := by
156    obtain ⟨w, off, a, e, -⟩ := hwin; rw [e]; intro c; cases c
157  have hrun := inflateBackInit__success hz hF hok hza hzf hv hv0 hw h8 h15
158  have hr := i2u_range h8 h15
159  have hza' : (initStream z).zalloc = .fn "zcalloc" := by rcases hza with e | e <;> simp [initStream, e]
160  have hzf' : (initStream z).zfree = .fn "zcfree" := by rcases hzf with e | e <;> simp [initStream, e]
161  have hzp : r.get (r.put h (initStream z)) = some (initStream z) := by simp [hz]
162  have hFp : Fresh (r.put h (initStream z)) := (shape_put hz _).fresh (by simp) hF
163  have hUp : Uniq (r.put h (initStream z)) := (shape_put hz _).uniq hU
164  have hz0 : r.get (allocIstHeap (r.put h (initStream z)) (backState (h.garbage h.nalloc) window wb)) = some (initStream z) := by simp [hz]
165  have hFA : Fresh (allocIstHeap (r.put h (initStream z)) (backState (h.garbage h.nalloc) window wb)) := fresh_allocIst hFp _
166  have hUA : Uniq (allocIstHeap (r.put h (initStream z)) (backState (h.garbage h.nalloc) window wb)) := uniq_allocIst hUp hFp _
167  refine ⟨_, by rw [C.run]; exact hrun, rfl, ?_, ?_⟩
168  · have hS := shape_put hz0 (initStream2 z h.nextBlk)
169    have hUp2 : Uniq (backOkHeap h r z window wb) := hS.uniq hUA
170    have hFp2 : Fresh (backOkHeap h r z window wb) := hS.fresh (by simp) hFA
171    refine ⟨?_, ?_, ?_, ?_, ?_, ⟨wf_backState _ _ _, ?_, ?_, ?_⟩, hUp2, hFp2⟩
172    · simp [backOkHeap, hz]
173    · simp [backOkHeap]
174    · simp [initStream2, StateRef.ofInflateState]
175    · simpa [initStream2] using hza'
176    · simpa [initStream2] using hzf'
177    · simp [backState, i2u]; exact ⟨by simpa [i2u] using hr.1, by simpa [i2u] using hr.2⟩
178    · simp only [backState]; rw [shl32_one hr.2]
179    · obtain ⟨w, off, a, e, hb, hro, hle⟩ := hwin
180      refine ⟨w, off, a, by simp [backState, e], by simpa [backOkHeap] using hb, by simpa [backOkHeap] using hro, ?_⟩
181      simp only [backState]; rw [shl32_one hr.2]; exact hle
182  · intro S hO
183    have h1 := owns_allocIst hFp (backState (h.garbage h.nalloc) window wb) ((shape_put hz _).owns hO)
184    simp only [ZStreamRef.put_nextBlk] at h1
185    exact (shape_put hz0 _).owns h1
186
187theorem backOk_shape {h : Heap} {r : ZStreamRef} {z : ZStream} (hz : r.get h = some z) (hF : Fresh h) (window : BPtr)
188    (wb : Int32) : Uniq h → Uniq (backOkHeap h r z window wb) ∧ Fresh (backOkHeap h r z window wb) := by
189  intro hU
190  have hFp : Fresh (r.put h (initStream z)) := (shape_put hz _).fresh (by simp) hF
191  have hUp : Uniq (r.put h (initStream z)) := (shape_put hz _).uniq hU
192  have hz0 : r.get (allocIstHeap (r.put h (initStream z)) (backState (h.garbage h.nalloc) window wb)) =
193      some (initStream z) := by simp [hz]
194  have hS := shape_put hz0 (initStream2 z h.nextBlk)
195  exact ⟨hS.uniq (uniq_allocIst hUp hFp _), hS.fresh (by simp) (fresh_allocIst hFp _)⟩
196
197/-- **inflateBackInit_, safety (every outcome).** For a stream record `z` whose allocator functions are `NULL` or the
198default ones (`zlib.h`: the caller sets them before the call; the model has only the defaults), a release string that is
199`NULL` or points to a readable byte, any `stream_size`, any `windowBits` and any `window` pointer (it is only stored),
200the call never faults and keeps `Uniq` and `Fresh`. The outcome is exactly one of: `Z_VERSION_ERROR` (nothing changes);
201`Z_STREAM_ERROR` (`window` is `NULL` or `windowBits` is outside 8 to 15: nothing changes); `Z_MEM_ERROR` (the allocation
202oracle says no: no block is allocated, none leaks); `Z_OK` (the state is the new block; see `inflateBackInit__ok`). -/
203theorem inflateBackInit__safe {h : Heap} {r : ZStreamRef} {z : ZStream} {wb : Int32} {window version : BPtr} {sz : Int32}
204    (hU : Uniq h) (hF : Fresh h) (hz : r.get h = some z)
205    (hza : z.zalloc = .null ∨ z.zalloc = .fn "zcalloc") (hzf : z.zfree = .null ∨ z.zfree = .fn "zcfree")
206    (hv : version = .null ∨ ∃ c, OkOn h (index8 version 0) c) :
207    ∃ v h', C.run (inflateBackInit_ (some r) wb window version sz) h = .ok (v, h') ∧ Uniq h' ∧ Fresh h' ∧
208      ((v = Z_VERSION_ERROR ∧ h' = h ∧ (version = .null ∨ (∃ c, OkOn h (index8 version 0) c ∧ c ≠ 49) ∨ sz ≠ 112)) ∨
209       (v = Z_STREAM_ERROR ∧ h' = h ∧ (window = .null ∨ wb < 8 ∨ wb > 15)) ∨
210       (v = Z_MEM_ERROR ∧ ¬ h.allocOk h.nalloc = true ∧ h' = initMemHeap h r z ∧ (∀ b, h'.live b ↔ h.live b)) ∨
211       (v = Z_OK ∧ sz = 112 ∧ h.allocOk h.nalloc = true ∧ window ≠ .null ∧ ¬ wb < 8 ∧ ¬ wb > 15 ∧
212          h' = backOkHeap h r z window wb)) := by
213  by_cases hvn : version = .null
214  · subst hvn
215    exact ⟨_, _, by rw [C.run]; exact inflateBackInit__version_null _ _ _ _ _, hU, hF, Or.inl ⟨rfl, rfl, Or.inl rfl⟩⟩
216  obtain ⟨c, hc⟩ := hv.resolve_left hvn
217  by_cases hc49 : c = 49
218  · subst hc49
219    by_cases hsz : sz = 112
220    · subst hsz
221      by_cases hbad : window = .null ∨ wb < 8 ∨ wb > 15
222      · exact ⟨_, _, (by rw [C.run]; exact inflateBackInit__stream_error (some r) wb window version h hvn hc (Or.inr hbad)), hU, hF, Or.inr (Or.inl ⟨rfl, rfl, hbad⟩)⟩
223      · have hw : window ≠ .null := fun e => hbad (Or.inl e)
224        have h8 : ¬ wb < 8 := fun e => hbad (Or.inr (Or.inl e))
225        have h15 : ¬ wb > 15 := fun e => hbad (Or.inr (Or.inr e))
226        by_cases hok : h.allocOk h.nalloc = true
227        · obtain ⟨u, f⟩ := backOk_shape hz hF window wb hU
228          exact ⟨_, _, by rw [C.run]; exact inflateBackInit__success hz hF hok hza hzf hvn hc hw h8 h15, u, f,
229            Or.inr (Or.inr (Or.inr ⟨rfl, rfl, hok, hw, h8, h15, rfl⟩))⟩
230        · obtain ⟨u1, f1, l1⟩ := initMem_good hz hU hF
231          exact ⟨_, _, by rw [C.run]; exact inflateBackInit__memfail hz hF hok hza hzf hvn hc hw h8 h15, u1, f1,
232            Or.inr (Or.inr (Or.inl ⟨rfl, hok, rfl, l1⟩))⟩
233    · exact ⟨_, _, by rw [C.run]; exact inflateBackInit__version_size _ _ _ _ _ _ hvn hc hsz, hU, hF,
234        Or.inl ⟨rfl, rfl, Or.inr (Or.inr hsz)⟩⟩
235  · exact ⟨_, _, by rw [C.run]; exact inflateBackInit__version_char _ _ _ _ _ _ c hvn hc hc49, hU, hF,
236      Or.inl ⟨rfl, rfl, Or.inr (Or.inl ⟨c, hc, hc49⟩)⟩⟩
237
238/-- `inflateBackInit_` with a null stream returns `Z_STREAM_ERROR` and changes nothing (given a correct release string). -/
239theorem inflateBackInit__nullstream {h : Heap} {wb : Int32} {window version : BPtr}
240    (hv : version ≠ .null) (hv0 : OkOn h (index8 version 0) 49) :
241    inflateBackInit_ none wb window version 112 h = .ok (Z_STREAM_ERROR, h) :=
242  inflateBackInit__stream_error none wb window version h hv hv0 (Or.inl rfl)
243
244end Zlib.Infback.Proofs