deflate.c.init.default.lean

Lean source with line numbers. Follow a line number to locate a statement, or an import to read its dependency.

1import ZlibF.Proof.«deflate.c.life.reset»
2import ZlibF.Proof.«deflate.c.life.end»
3import ZlibF.Proof.«deflate.c.init.memory»
4import ZlibF.Proof.«trees.c.monad»
5import ZlibF.Spec.Public.Initialisation
6
7/-! # deflate.c: direct proof of the default initialization entry
8
9The public default entry is proved by expanding its fixed-parameter call.
10No universal deflateInit2_ execution theorem is used or assumed.
11-/
12
13namespace Zlib.Deflate.Proofs.DefaultInit
14open C Zlib.Deflate Zlib.Deflate.Spec
15open ZlibF.Spec.Public
16set_option autoImplicit false
17
18/-- The default entry normalizes only its caller-supplied compression level. -/
19def levelValue (level : Int32) : Int32 := if level == Z_DEFAULT_COMPRESSION then 6 else level
20
21/-- The actual allocation suffix at the default method, window, memory and
22strategy. Constant arithmetic is discharged by the whole-source equality.
23All allocations, stores and cleanup calls retain their source order. -/
24def allocate (strm : ZStreamPtr) (level : Int32) : M Int32 := do
25  zalloc_default strm
26  let s ← allocDeflateState
27  if s == none then return Z_MEM_ERROR
28  stDeflateState s DeflateState.zeroed
29  zwr strm (fun z => { z with state := StateRef.ofDeflateState s })
30  wr s (fun d => { d with
31    strm := strm, status := INIT_STATE, wrap := 1,
32    w_bits := 15, w_size := 32768, w_mask := 32767,
33    hash_bits := 15, hash_size := 32768, hash_mask := 32767, hash_shift := 5 })
34  let window ← ZALLOC_bytes strm 32768 2
35  wr s (fun d => { d with window })
36  let prev ← ZALLOC_words strm 32768
37  wr s (fun d => { d with prev })
38  let head ← ZALLOC_words strm 32768
39  wr s (fun d => { d with head })
40  wr s (fun d => { d with high_water := 0, lit_bufsize := 16384 })
41  let pending_buf ← ZALLOC_bytes strm 16384 4
42  wr s (fun d => { d with pending_buf, pending_buf_size := 65536 })
43  if window == .null || prev == .null || head == .null || pending_buf == .null then
44    wr s (fun d => { d with status := FINISH_STATE })
45    let m ← ERR_MSG Z_MEM_ERROR
46    zwr strm (fun z => { z with msg := m })
47    let _ ← deflateEnd strm
48    return Z_MEM_ERROR
49  let sym_buf ← padd pending_buf 16384
50  wr s (fun d => { d with sym_buf, sym_end := 49149 })
51  wr s (fun d => { d with level, strategy := 0, «method» := 8 })
52  deflateReset strm
53
54/-- `int deflateInit_(z_streamp strm, int level, const char *version, int stream_size)`.
55Source equality specializes the translated call, without requiring the
56universal deflateInit2_ theorem. The arbitrary level and refusal order remain. -/
57theorem source_eq (strm : ZStreamPtr) (level : Int32) (version : BPtr) (size : Int32) :
58    deflateInit_ strm level version size = (do
59      if version == .null then return Z_VERSION_ERROR
60      if (← load8 version) != 49 || size != sizeof_z_stream then return Z_VERSION_ERROR
61      if strm == none then return Z_STREAM_ERROR
62      zwr strm (fun z => { z with msg := .null })
63      if (← zrd strm (·.zalloc)) == FnPtr.null then
64        zwr strm (fun z => { z with zalloc := FnPtr.fn "zcalloc", «opaque» := .null })
65      if (← zrd strm (·.zfree)) == FnPtr.null then
66        zwr strm (fun z => { z with zfree := FnPtr.fn "zcfree" })
67      if levelValue level < 0 || levelValue level > 9 then return Z_STREAM_ERROR
68      allocate strm (levelValue level)) := by
69  by_cases hd : level = Z_DEFAULT_COMPRESSION
70  all_goals unfold deflateInit_ deflateInit2_ allocate levelValue
71  all_goals simp [hd, Z_DEFLATED, MAX_WBITS, DEF_MEM_LEVEL, Z_DEFAULT_STRATEGY, MAX_MEM_LEVEL,
72    Z_FIXED, MIN_MATCH_u, iadd, ishl, chk32, M_bind_assoc, M_pure_bind]
73  all_goals rfl
74
75/-- The default allocator check reads the actual stream record. -/
76theorem allocator_run {h : Heap} {r : ZStreamRef} {z : ZStream}
77    (hz : r.get h = some z) (ha : z.zalloc = .fn "zcalloc") :
78    zalloc_default (some r) h = .ok ((), h) := by
79  simp [zalloc_default, bind_app, ldZ_eq, hz, ha]
80
81/-- Both nullable allocator fields are prepared exactly as specified. -/
82theorem prepared_allocators {z : ZStream} (ha : DefaultOrNull z) :
83    (preparedStream z).zalloc = .fn "zcalloc" ∧ (preparedStream z).zfree = .fn "zcfree" := by
84  obtain ⟨hza, hzf⟩ := ha
85  rcases hza with hza | hza <;> rcases hzf with hzf | hzf <;>
86    simp [preparedStream, hza, hzf]
87
88/-- The deflate version check dereferences the actual version pointer. -/
89theorem version_load {h : Heap} {v : BPtr} {byte : UInt8}
90    (hv : VersionValue h v (some byte)) : v ≠ .null ∧ load8 v h = .ok (byte, h) := by
91  rcases hv with ⟨_, hn⟩ | ⟨b, hb, hbytes⟩
92  · cases hn
93  · cases hb
94    rcases hbytes with ⟨_, hn, _⟩ | ⟨ref, off, a, rfl, hg, hfit, hlist⟩
95    · cases hn
96    · have hi : off < a.size := by omega
97      have he : a[off]? = some byte := by
98        have hh := congrArg (fun l : List UInt8 => l[0]?) hlist
99        simpa [List.getElem?_take, List.getElem?_drop] using hh.symm
100      have hbyte : a[off] = byte := by
101        rw [Array.getElem?_eq_getElem hi] at he
102        exact Option.some.inj he
103      refine ⟨by simp, ?_⟩
104      have hr := Ptr.load_ok hg hi
105      simpa only [OkOn, load8, hbyte] using hr
106
107/-- Version and size refusal occurs before any stream access or allocation. -/
108theorem version_refusal (level : Int32) :
109    ∀ h p version head size, VersionValue h version head →
110      (head ≠ some 49 ∨ size ≠ 112) →
111      C.run (deflateInit_ p level version size) h = .ok (Z_VERSION_ERROR, h) := by
112  intro h p version head size hv hbad
113  rw [C.run, source_eq]
114  cases head with
115  | none =>
116    rcases hv with ⟨rfl, _⟩ | ⟨b, hb, _⟩
117    · simp
118    · cases hb
119  | some byte =>
120    obtain ⟨hn, read⟩ := version_load hv
121    by_cases hb : byte = 49
122    · subst byte
123      have hs : size ≠ 112 := by simpa using hbad
124      simp [hn, bind_app, read, sizeof_z_stream, hs]
125    · simp [hn, bind_app, read, hb]
126
127/-- The null stream is rejected after the successful version read. -/
128theorem null_stream (level : Int32) :
129    ∀ h version, VersionValue h version (some 49) →
130      C.run (deflateInit_ none level version 112) h = .ok (Z_STREAM_ERROR, h) := by
131  intro h version hv
132  obtain ⟨hn, read⟩ := version_load hv
133  rw [C.run, source_eq]
134  simp [hn, bind_app, read, sizeof_z_stream]
135
136/-- After the successful version read, the actual prefix prepares the
137stream and checks the arbitrary level before entering allocation. -/
138theorem entry_run {h : Heap} {r : ZStreamRef} {z : ZStream} {version : BPtr}
139    (hz : r.get h = some z) (hv : VersionValue h version (some 49)) (level : Int32) :
140    deflateInit_ (some r) level version 112 h =
141      (if levelValue level < 0 || levelValue level > 9 then
142        .ok (Z_STREAM_ERROR, r.put h (preparedStream z))
143      else allocate (some r) (levelValue level) (r.put h (preparedStream z))) := by
144  obtain ⟨hn, read⟩ := version_load hv
145  rw [source_eq]
146  by_cases hza : z.zalloc = .null <;> by_cases hzf : z.zfree = .null <;>
147    by_cases bad : levelValue level < 0 ∨ 9 < levelValue level
148  all_goals simp [hn, bind_app, pure_app, read, sizeof_z_stream, zwr_eq, zrd_eq, hz,
149    ZStreamRef.get_put_same hz, ZStreamRef.put_put, preparedStream, hza, hzf, bad]
150
151/-- Failure of the first allocation returns before any state is published. -/
152theorem allocate_state_fail {h : Heap} {r : ZStreamRef} {z : ZStream}
153    (hz : r.get h = some z) (ha : z.zalloc = .fn "zcalloc")
154    (hf : h.allocOk h.nalloc = false) (level : Int32) :
155    allocate (some r) level h = .ok (Z_MEM_ERROR, { h with nalloc := h.nalloc + 1 }) := by
156  unfold allocate
157  rw [bind_app, allocator_run hz ha]
158  simp only []
159  rw [bind_app, allocDeflateState_none (by rw [hf]; decide)]
160  rfl
161
162/-- The actual byte-buffer allocator, including arbitrary allocation failure. -/
163theorem bytes_run {h : Heap} {r : ZStreamRef} {z : ZStream}
164    (hf : Fresh h) (hz : r.get h = some z) (ha : z.zalloc = .fn "zcalloc")
165    (items size : UInt32) :
166    ZALLOC_bytes (some r) items size h = .ok (bytePtr h, byteResult h (items * size).toNat) := by
167  unfold ZALLOC_bytes
168  rw [bind_app, allocator_run hz ha]
169  simp only []
170  simp only [bind_app, ldZ_eq, hz]
171  exact byte_alloc_run hf _
172
173/-- The actual word-buffer allocator retains its unsigned byte product. -/
174theorem words_run {h : Heap} {r : ZStreamRef} {z : ZStream}
175    (hf : Fresh h) (hz : r.get h = some z) (ha : z.zalloc = .fn "zcalloc") (items : UInt32) :
176    ZALLOC_words (some r) items h = .ok (wordPtr h, wordResult h ((items * 2).toNat / 2)) := by
177  unfold ZALLOC_words
178  rw [bind_app, allocator_run hz ha]
179  exact word_alloc_run hf _
180
181/-- The four actual buffer allocations and their intervening stores. -/
182def buffers (strm : ZStreamPtr) (s : DeflateStatePtr) : M (BPtr × WPtr × WPtr × BPtr) := do
183  let window ← ZALLOC_bytes strm 32768 2
184  wr s (fun d => { d with window })
185  let prev ← ZALLOC_words strm 32768
186  wr s (fun d => { d with prev })
187  let head ← ZALLOC_words strm 32768
188  wr s (fun d => { d with head })
189  wr s (fun d => { d with high_water := 0, lit_bufsize := 16384 })
190  let pending_buf ← ZALLOC_bytes strm 16384 4
191  wr s (fun d => { d with pending_buf, pending_buf_size := 65536 })
192  pure (window, prev, head, pending_buf)
193
194def windowHeap (h : Heap) : Heap := byteResult h 65536
195def prevHeap (h : Heap) : Heap := wordResult (windowHeap h) 32768
196def headHeap (h : Heap) : Heap := wordResult (prevHeap h) 32768
197def buffersHeap (h : Heap) : Heap := byteResult (headHeap h) 65536
198
199def bufferPointers (h : Heap) : BPtr × WPtr × WPtr × BPtr :=
200  (bytePtr h, wordPtr (windowHeap h), wordPtr (prevHeap h), bytePtr (headHeap h))
201
202def bufferState (h : Heap) (d : DeflateState) : DeflateState :=
203  { d with
204    window := bytePtr h, prev := wordPtr (windowHeap h), head := wordPtr (prevHeap h),
205    high_water := 0, lit_bufsize := 16384,
206    pending_buf := bytePtr (headHeap h), pending_buf_size := 65536 }
207
208/-- Each of the four buffer requests executes even if an earlier one fails.
209The theorem retains the exact oracle-dependent pointers and heap, before
210the cleanup decision. No initialized-state invariant is assumed. -/
211theorem buffers_run {h : Heap} {r : ZStreamRef} {z : ZStream} {ds : Nat} {d : DeflateState}
212    (hf : Fresh h) (hz : r.get h = some z) (ha : z.zalloc = .fn "zcalloc")
213    (hs : h.dstates ds = some d) (hds : ds < h.nextBlk) :
214    buffers (some r) (some (.tab ds)) h =
215      .ok (bufferPointers h, setD (buffersHeap h) ds (bufferState h d)) := by
216  let d1 := { d with window := bytePtr h }
217  let H1 := setD (windowHeap h) ds d1
218  let d2 := { d1 with prev := wordPtr (windowHeap h) }
219  let H2 := setD (prevHeap h) ds d2
220  let d3 := { d2 with head := wordPtr (prevHeap h) }
221  let d4 := { d3 with high_water := 0, lit_bufsize := 16384 }
222  let H4 := setD (headHeap h) ds d4
223  have fW := fresh_byteResult hf 65536
224  have fP := fresh_wordResult fW 32768
225  have fH := fresh_wordResult fP 32768
226  have pW := byteResult_next h 65536
227  have pP := wordResult_next (windowHeap h) 32768
228  have pH := wordResult_next (prevHeap h) 32768
229  have hf1 : Fresh H1 := fresh_setD_below fW ds (by dsimp only [windowHeap] at *; omega) d1
230  have hf2 : Fresh H2 := fresh_setD_below fP ds (by dsimp only [prevHeap, windowHeap] at *; omega) d2
231  have hf4 : Fresh H4 := fresh_setD_below fH ds
232    (by dsimp only [headHeap, prevHeap, windowHeap] at *; omega) d4
233  have runW := bytes_run hf hz ha 32768 2
234  have runP := words_run hf1 (r := r) (z := z) (by simpa [H1, windowHeap] using hz) ha 32768
235  have runH := words_run hf2 (r := r) (z := z) (by simpa [H2, prevHeap, windowHeap] using hz) ha 32768
236  have runB := bytes_run hf4 (r := r) (z := z) (by simpa [H4, headHeap, prevHeap, windowHeap] using hz) ha 16384 4
237  change ZALLOC_bytes (some r) 32768 2 h = .ok (bytePtr h, windowHeap h) at runW
238  simp only [show ((32768 : UInt32) * 2).toNat / 2 = 32768 from by decide +kernel] at runP runH
239  simp only [show ((16384 : UInt32) * 4).toNat = 65536 from by decide +kernel] at runB
240  simp only [H1, H2, H4, prevHeap, headHeap, buffersHeap, windowHeap, wordPtr_setD,
241    bytePtr_setD, wordResult_setD, byteResult_setD] at runP runH runB
242  dsimp only [d1, d2, d3, d4, prevHeap, headHeap, windowHeap] at runP runH runB
243  unfold buffers
244  rw [bind_app, runW]
245  simp only [bind_app, wrD_eq, windowHeap, byteResult_dstates, hs, d1, d2, d3, d4]
246  rw [runP]
247  simp only [bind_app, wrD_eq, setD_dstates_same, setD_setD, d1, d2, d3, d4]
248  rw [runH]
249  simp only [bind_app, wrD_eq, setD_dstates_same, setD_setD, d1, d2, d3, d4]
250  rw [runB]
251  simp only [bind_app, wrD_eq, setD_dstates_same, setD_setD, pure_app]
252  rfl
253
254/-- The exact state fields written before the four buffer allocations. -/
255def baseState (r : ZStreamRef) : DeflateState :=
256  { DeflateState.zeroed with
257    strm := some r, status := INIT_STATE, wrap := 1,
258    w_bits := 15, w_size := 32768, w_mask := 32767,
259    hash_bits := 15, hash_size := 32768, hash_mask := 32767, hash_shift := 5 }
260
261def stateStream (z : ZStream) (ds : Nat) : ZStream := { z with state := some (.deflate ds) }
262
263def publishedHeap (h : Heap) (r : ZStreamRef) (z : ZStream) : Heap :=
264  stateHeap (r.put h (stateStream z h.nextBlk)) (baseState r)
265
266/-- The actual final decision after all four buffer requests. -/
267def finish (strm : ZStreamPtr) (s : DeflateStatePtr) (level : Int32)
268    (ps : BPtr × WPtr × WPtr × BPtr) : M Int32 := do
269  let (window, prev, head, pending_buf) := ps
270  if window == .null || prev == .null || head == .null || pending_buf == .null then
271    wr s (fun d => { d with status := FINISH_STATE })
272    let m ← ERR_MSG Z_MEM_ERROR
273    zwr strm (fun z => { z with msg := m })
274    let _ ← deflateEnd strm
275    return Z_MEM_ERROR
276  let sym_buf ← padd pending_buf 16384
277  wr s (fun d => { d with sym_buf, sym_end := 49149 })
278  wr s (fun d => { d with level, strategy := 0, «method» := 8 })
279  deflateReset strm
280
281/-- Naming allocation and cleanup cut points preserves the actual suffix. -/
282theorem allocate_eq (strm : ZStreamPtr) (level : Int32) : allocate strm level = (do
283    zalloc_default strm
284    let s ← allocDeflateState
285    if s == none then return Z_MEM_ERROR
286    stDeflateState s DeflateState.zeroed
287    zwr strm (fun z => { z with state := StateRef.ofDeflateState s })
288    wr s (fun d => { d with
289      strm := strm, status := INIT_STATE, wrap := 1,
290      w_bits := 15, w_size := 32768, w_mask := 32767,
291      hash_bits := 15, hash_size := 32768, hash_mask := 32767, hash_shift := 5 })
292    let ps ← buffers strm s
293    finish strm s level ps) := by
294  unfold allocate buffers finish
295  simp only [M_bind_assoc, M_pure_bind]
296
297/-- Actual state allocation, zeroing and publication, followed by all four
298buffer requests. Its result is the real cleanup/success cut point for
299every four-buffer allocation oracle. -/
300theorem allocate_to_finish {h : Heap} {r : ZStreamRef} {z : ZStream}
301    (hf : Fresh h) (hz : r.get h = some z) (ha : z.zalloc = .fn "zcalloc")
302    (ho : h.allocOk h.nalloc = true) (level : Int32) :
303    allocate (some r) level h =
304      finish (some r) (some (.tab h.nextBlk)) level (bufferPointers (publishedHeap h r z))
305        (setD (buffersHeap (publishedHeap h r z)) h.nextBlk
306          (bufferState (publishedHeap h r z) (baseState r))) := by
307  have hfP : Fresh (publishedHeap h r z) :=
308    fresh_stateHeap ((shape_put hz _).fresh (by simp) hf) _
309  have hsP : (publishedHeap h r z).dstates h.nextBlk = some (baseState r) := by
310    simp [publishedHeap, stateHeap]
311  have hzP : r.get (publishedHeap h r z) = some (stateStream z h.nextBlk) := by
312    simp [publishedHeap, ZStreamRef.get_put_same hz]
313  have hbuffer := buffers_run hfP hzP (by simpa [stateStream] using ha) hsP
314    (by simp [publishedHeap, stateHeap])
315  rw [allocate_eq]
316  rw [bind_app, allocator_run hz ha]
317  simp only []
318  have runS : allocDeflateState h = .ok (some (.tab h.nextBlk),
319      stateHeap h (DeflateState.garbage (h.garbage h.nalloc))) := allocDeflateState_some ho
320  rw [bind_app, runS]
321  simp [bind_app, stD_eq, pure_app, ZStreamRef.put_dstates, stateHeap_dstates_same,
322    zwr_eq, get_stateHeap, ZStreamRef.get_put_same hz, wrD_eq, upd_upd,
323    put_stateHeap, stateHeap_setD, hz, StateRef.ofDeflateState]
324  change (do let ps ← buffers (some r) (some (.tab h.nextBlk))
325             finish (some r) (some (.tab h.nextBlk)) level ps) (publishedHeap h r z) = _
326  rw [bind_app, hbuffer]
327
328end Zlib.Deflate.Proofs.DefaultInit