public-deflate-init.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.init.failure»
2
3/-! # The default deflate initialization entry
4
5The default entry expands the translated fixed-parameter call directly.
6The universal deflateInit2_ theorem is not a proof dependency.
7-/
8
9namespace ZlibF.Spec.Public.Proofs.DeflateInit
10open C Zlib.Deflate Zlib.Deflate.Spec Zlib.Deflate.Proofs
11open Zlib.Deflate.Proofs.DefaultInit
12open Zlib.Trees.Proofs.Out (TreesStatic)
13set_option autoImplicit false
14
15def settings (level : Int32) : Api.DeflParams := ⟨level.toInt.toNat, .zlib, 15, 8, 0⟩
16
17theorem parameters_equiv (level : Int32) :
18    Api.deflInit? level.toInt 8 15 8 0 =
19      if levelValue level < 0 || levelValue level > 9 then none else some (settings (levelValue level)) := by
20  by_cases hd : level = Z_DEFAULT_COMPRESSION
21  · subst level
22    decide +kernel
23  · have hi : level.toInt ≠ -1 := by
24      intro hi
25      apply hd
26      apply Int32.toInt_inj.mp
27      simpa only [show Z_DEFAULT_COMPRESSION.toInt = -1 from rfl] using hi
28    simp [Api.deflInit?, settings, levelValue, hd, hi,
29      Int32.lt_iff_toInt_lt]
30
31def resultState (h : Heap) (r : ZStreamRef) (level : Int32) (a1 a2 a3 : Array CtData) : DeflateState :=
32  finalState h.nextBlk r level (h.nextBlk + 1) (h.nextBlk + 2) (h.nextBlk + 3) (h.nextBlk + 4) a1 a2 a3
33
34/-- All five successful requests establish DGood by actual execution,
35including hash clearing. No callee or initialized-state invariant is assumed. -/
36theorem allocate_success {h : Heap} {r : ZStreamRef} {z : ZStream}
37    (hf : Fresh h) (hu : Uniq h) (hz : r.get h = some z) (hd : DefAlloc z)
38    (hs : TreesStatic h.static) (ha : ∀ j, j < 5 → h.allocOk (h.nalloc + j) = true)
39    (level : Int32) (hl0 : 0 ≤ level.toInt) (hl9 : level.toInt ≤ 9) :
40    ∃ (a1 a2 a3 : Array CtData) (qa : Array UInt16),
41      allocate (some r) level h = .ok (Z_OK, successHeap h r z level a1 a2 a3 qa) ∧
42      DGood (successHeap h r z level a1 a2 a3 qa) r h.nextBlk (resultStream h r z level)
43        (resultState h r level a1 a2 a3) ∧
44      (∀ x, (successHeap h r z level a1 a2 a3 qa).live x ↔
45        h.live x ∨ h.nextBlk ≤ x ∧ x < h.nextBlk + 5) := by
46  let ph := publishedHeap h r z
47  have ha0 : h.allocOk h.nalloc = true := by simpa using ha 0 (by decide)
48  have ha4 : ∀ j, j < 4 → ph.allocOk (ph.nalloc + j) = true := by
49    intro j hj
50    simpa [ph, publishedHeap, stateHeap, Nat.add_assoc, Nat.add_comm, Nat.add_left_comm] using ha (j + 1) (by omega)
51  have hfp := (shape_put hz (stateStream z h.nextBlk)).fresh (by simp) hf
52  have hup := (shape_put hz (stateStream z h.nextBlk)).uniq hu
53  have hfP : Fresh ph := fresh_stateHeap hfp _
54  have huP : Uniq ph := uniq_stateHeap hup hfp _
55  have hzP : r.get ph = some (stateStream z h.nextBlk) := by
56    simp [ph, publishedHeap, ZStreamRef.get_put_same hz]
57  have hdP : DefAlloc (stateStream z h.nextBlk) := hd
58  have hsP : ph.dstates h.nextBlk = some (baseState r) := by simp [ph, publishedHeap, stateHeap]
59  have hst : TreesStatic ph.static := by simpa [ph, publishedHeap, stateHeap] using hs
60  obtain ⟨hlR, htR, hbR, huR, hfR⟩ := ready_storage level hfP huP hzP hsP
61    (by simp [ph, publishedHeap, stateHeap]) hdP rfl hst ha4
62  obtain ⟨a1, a2, a3, qa, s1, s2, s3, hqa, hreset, hG, hLive⟩ :=
63    reset_construct level hlR htR hbR huR hfR hl0 hl9
64  refine ⟨a1, a2, a3, qa, ?_, ?_, ?_⟩
65  · rw [allocate_to_finish hf hz hd.1 ha0, finish_to_reset _ _ _ _ ha4, hreset]
66    rfl
67  · simpa only [successHeap, resultStream, resultState, finalState,
68      ph, publishedHeap, stateHeap, ZStreamRef.put_nextBlk, Nat.add_assoc] using hG
69  · intro x
70    have hc := ready_live hz level ha4 x
71    have hr := hLive x
72    simpa only [successHeap, resultStream] using hr.trans hc
73
74theorem globals_trees {h : Heap} (hg : LibraryGlobals h) : TreesStatic h.static := by
75  rw [hg]
76  rfl
77
78theorem result_owned (h : Heap) (r : ZStreamRef) (level : Int32)
79    (a1 a2 a3 : Array CtData) (x : Nat) :
80    DeflateOwned h.nextBlk (resultState h r level a1 a2 a3) x ↔
81      h.nextBlk ≤ x ∧ x < h.nextBlk + 5 := by
82  simp only [DeflateOwned, resultState, finalState, lmD, resetState, rkPost, rkPost3, rkMid,
83    Zlib.Trees.Proofs.Out.ibRec, Zlib.Trees.Proofs.Out.trInitRec, readyState, allocatedState,
84    baseState]
85  simp only [Ptr.ref.injEq, BRef.blk.injEq, WRef.blk.injEq, and_true]
86  omega
87
88/-- Actual successful default allocation establishes the exact public
89initial relation, with old-object frame and the five-object ledger. -/
90theorem success_initial {h : Heap} {r : ZStreamRef} {z : ZStream}
91    (hf : Fresh h) (hu : Uniq h) (hg : LibraryGlobals h) (hz : r.get h = some z)
92    (ha : DefaultOrNull z) (allok : ∀ j, j < 5 → h.allocOk (h.nalloc + j) = true)
93    (level : Int32) (hl0 : 0 ≤ level.toInt) (hl9 : level.toInt ≤ 9) :
94    ∃ after, allocate (some r) level (r.put h (preparedStream z)) = .ok (Z_OK, after) ∧
95      DeflateInitial h after r (settings level) := by
96  let zp := preparedStream z
97  let hp := r.put h zp
98  have shape := shape_put hz zp
99  have hfP : Fresh hp := shape.fresh (by simp [hp]) hf
100  have huP : Uniq hp := shape.uniq hu
101  have hzP : r.get hp = some zp := ZStreamRef.get_put_same hz _
102  have haP : DefAlloc zp := prepared_allocators ha
103  have globalsP : TreesStatic hp.static := by simpa [hp] using globals_trees hg
104  have allP : ∀ j, j < 5 → hp.allocOk (hp.nalloc + j) = true := by
105    intro j hj
106    simpa [hp] using allok j hj
107  obtain ⟨a1, a2, a3, qa, hrun, hG, hLive⟩ := allocate_success hfP huP hzP haP globalsP allP level hl0 hl9
108  let after := successHeap hp r zp level a1 a2 a3 qa
109  let zf := resultStream hp r zp level
110  let sf := resultState hp r level a1 a2 a3
111  have nb : hp.nextBlk = h.nextBlk := by simp [hp]
112  have hGood : DGood after r h.nextBlk zf sf := by simpa only [nb] using hG
113  have owned : ∀ x, DeflateOwned h.nextBlk sf x ↔ h.nextBlk ≤ x ∧ x < h.nextBlk + 5 := by
114    intro x
115    simpa only [nb] using result_owned hp r level a1 a2 a3 x
116  have hFrame : Frame h after (StreamRoot r) := frame_trans r (frame_put r zp hf)
117    (success_frame r zp level a1 a2 a3 qa hfP)
118  refine ⟨after, hrun, zf, sf, hGood, ?_, ?_, ?_, ?_, ?_, ?_, ?_,
119    rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, hFrame, ?_, owned⟩
120  · simpa [zf, resultStream, rkZ, stateStream] using haP.1
121  · simpa [zf, resultStream, rkZ, stateStream] using haP.2
122  · simp only [sf, resultState, finalState, lmD, resetState, rkPost, rkPost3, rkMid,
123      Zlib.Trees.Proofs.Out.ibRec, Zlib.Trees.Proofs.Out.trInitRec, readyState, settings]
124    omega
125  · simp [sf, resultState, finalState, lmD, resetState, rkPost, rkPost3, rkMid,
126      Zlib.Trees.Proofs.Out.ibRec, Zlib.Trees.Proofs.Out.trInitRec, readyState, settings]
127  · simp [sf, resultState, finalState, lmD, resetState, rkPost, rkPost3, rkMid,
128      Zlib.Trees.Proofs.Out.ibRec, Zlib.Trees.Proofs.Out.trInitRec, readyState, allocatedState, baseState, settings]
129  · simp [sf, resultState, finalState, lmD, resetState, rkPost, rkPost3, rkMid,
130      Zlib.Trees.Proofs.Out.ibRec, Zlib.Trees.Proofs.Out.trInitRec, readyState, allocatedState, baseState, settings]
131  · simp [sf, resultState, finalState, lmD, resetState, rkPost, rkPost3, rkMid, absWrap,
132      Zlib.Trees.Proofs.Out.ibRec, Zlib.Trees.Proofs.Out.trInitRec, readyState, allocatedState, baseState, settings]
133  · intro x
134    simp only [LiveChange, not_false_eq_true, and_true] at *
135    change after.live x ↔ h.live x ∨ DeflateOwned h.nextBlk sf x
136    rw [owned]
137    have live := hLive x
138    rw [shape.live] at live
139    simpa only [nb] using live
140
141theorem allocate_success_count {h after : Heap} {r : ZStreamRef} {z : ZStream}
142    (hf : Fresh h) (hu : Uniq h) (hz : r.get h = some z) (hd : DefAlloc z)
143    (hs : TreesStatic h.static) (ha : ∀ j, j < 5 → h.allocOk (h.nalloc + j) = true)
144    (level : Int32) (hl0 : 0 ≤ level.toInt) (hl9 : level.toInt ≤ 9)
145    (hrun : allocate (some r) level h = .ok (Z_OK, after)) :
146    after.nalloc = h.nalloc + 5 := by
147  obtain ⟨a1, a2, a3, qa, hr, _, _⟩ := allocate_success hf hu hz hd hs ha level hl0 hl9
148  rw [hr] at hrun
149  cases hrun
150  simp only [successHeap, setD_nalloc, setW, readyHeap, successfulBuffers,
151    publishedHeap, stateHeap, ZStreamRef.put_nalloc, Nat.add_assoc]
152
153theorem same_objects_refl (h : Heap) : SameObjects h h := by
154  exact ⟨rfl, rfl, fun _ _ => rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl,
155    Nat.le_refl _, Nat.le_refl _⟩
156
157/-- The exact public default-entry goal, including arbitrary levels, every
158allocation outcome, cleanup, ownership and the initialized invariant.
159The translated fixed-parameter call is expanded; the general Init2 goal
160is not assumed. -/
161theorem deflateInit_proof : Goal.deflateInit_ := by
162  intro level
163  refine ⟨version_refusal level, null_stream level, ?_⟩
164  intro h r z version hf hu hg hz ha hv
165  let zp := preparedStream z
166  let hp := r.put h zp
167  let lev := levelValue level
168  have hshape := shape_put hz zp
169  have hfP : Fresh hp := hshape.fresh (by simp [hp]) hf
170  have huP : Uniq hp := hshape.uniq hu
171  have hzP : r.get hp = some zp := ZStreamRef.get_put_same hz _
172  have haP : DefAlloc zp := prepared_allocators ha
173  have entry := entry_run hz hv level
174  simp only [show (8 : Int32).toInt = (8 : Int) from rfl,
175    show (15 : Int32).toInt = (15 : Int) from rfl,
176    show (0 : Int32).toInt = (0 : Int) from rfl]
177  rw [parameters_equiv]
178  by_cases bad : (levelValue level < 0 || levelValue level > 9) = true
179  · refine ⟨Z_STREAM_ERROR, hp, ?_, ?_⟩
180    · simpa only [C.run, ite_eq_left bad] using entry
181    · simp only [ite_eq_left bad]
182      exact ⟨True.intro, same_objects_refl hp, by simp [hp]⟩
183  · have bounds : 0 ≤ lev.toInt ∧ lev.toInt ≤ 9 := by
184      have bn := bad
185      simp only [Bool.or_eq_true, decide_eq_true_eq, Int32.lt_iff_toInt_lt] at bn
186      change ¬ (lev.toInt < 0 ∨ 9 < lev.toInt) at bn
187      omega
188    have entry' : deflateInit_ (some r) level version 112 h = allocate (some r) lev hp := by
189      simpa only [ite_eq_right bad] using entry
190    simp only [ite_eq_right bad]
191    by_cases first : h.allocOk h.nalloc = false
192    · refine ⟨Z_MEM_ERROR, { hp with nalloc := hp.nalloc + 1 }, ?_, ?_⟩
193      · change deflateInit_ (some r) level version 112 h = _
194        rw [entry']
195        exact allocate_state_fail hzP haP.1 (by simpa [hp] using first) lev
196      · simp only [ite_eq_left first]
197        refine ⟨True.intro, by simp [hp], ?_⟩
198        dsimp [SameObjects]
199        exact ⟨rfl, rfl, fun _ _ => rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl,
200          Nat.le_refl _, by simp [hp]⟩
201    · have firstT : h.allocOk h.nalloc = true := by cases he : h.allocOk h.nalloc <;> simp_all
202      simp only [ite_eq_right first]
203      by_cases all : (List.range 5).all (fun j => h.allocOk (h.nalloc + j)) = true
204      · have allok : ∀ j, j < 5 → h.allocOk (h.nalloc + j) = true := by
205          simpa only [List.all_eq_true, List.mem_range] using all
206        obtain ⟨after, hr, hi⟩ := success_initial hf hu hg hz ha allok lev bounds.1 bounds.2
207        refine ⟨Z_OK, after, ?_, ?_⟩
208        · change deflateInit_ (some r) level version 112 h = _
209          rw [entry']
210          exact hr
211        · refine ⟨?_, ?_⟩
212          · have count := allocate_success_count hfP huP hzP haP
213              (by simpa [hp] using globals_trees hg)
214              (by simpa [hp] using allok) lev bounds.1 bounds.2 hr
215            simpa [hp] using count
216          · simpa only [ite_eq_left all] using (show Z_OK = Z_OK ∧ DeflateInitial h after r (settings lev) from ⟨rfl, hi⟩)
217      · let ph := publishedHeap hp r zp
218        have failed : ((bufferPointers ph).1 == .null || (bufferPointers ph).2.1 == .null ||
219            (bufferPointers ph).2.2.1 == .null || (bufferPointers ph).2.2.2 == .null) = true := by
220          apply Classical.byContradiction
221          intro hn
222          have hb : ((bufferPointers ph).1 == .null || (bufferPointers ph).2.1 == .null ||
223              (bufferPointers ph).2.2.1 == .null || (bufferPointers ph).2.2.2 == .null) = false := by
224            cases he : ((bufferPointers ph).1 == .null || (bufferPointers ph).2.1 == .null ||
225              (bufferPointers ph).2.2.1 == .null || (bufferPointers ph).2.2.2 == .null) <;> simp_all
226          obtain ⟨h0, h1, h2, h3⟩ := (buffers_failed_iff ph).mp hb
227          apply all
228          rw [List.all_eq_true]
229          intro j hj
230          have hj5 := List.mem_range.mp hj
231          have hn : ph.nalloc = h.nalloc + 1 := by simp [ph, publishedHeap, stateHeap, hp]
232          have ao : ph.allocOk = h.allocOk := by simp [ph, publishedHeap, stateHeap, hp]
233          rw [ao, hn] at h0 h1 h2 h3
234          have cases5 : j = 0 ∨ j = 1 ∨ j = 2 ∨ j = 3 ∨ j = 4 := by omega
235          rcases cases5 with h | h | h | h | h <;> subst j <;>
236            simpa only [Nat.add_assoc, Nat.add_zero] using (by assumption)
237        obtain ⟨m, hm⟩ := finish_failure hzP haP lev failed
238        let after := failureHeap hp r zp m
239        refine ⟨Z_MEM_ERROR, after, ?_, ?_⟩
240        · change deflateInit_ (some r) level version 112 h = _
241          rw [entry', allocate_to_finish hfP hzP haP.1 (by simpa [hp] using firstT)]
242          exact hm
243        · refine ⟨by simpa [after, hp] using failure_count hp r zp m, ?_⟩
244          simp only [ite_eq_right all]
245          refine ⟨True.intro, ⟨_, failure_stream_cleared hzP m, rfl⟩, ?_, ?_⟩
246          · intro x
247            simpa only [not_false_eq_true, and_true, or_false] using
248              ((failure_shape hzP hfP m).live x).trans (hshape.live x)
249          · exact frame_trans r (frame_put r zp hf) (failure_frame r zp m hfP)
250
251/-- A concrete caller heap. The version and stream are distinct live
252objects, and every default allocation request succeeds. -/
253def witnessHeap : Heap :=
254  { Heap.empty with
255    streams := upd Heap.empty.streams 0 (some default)
256    bytes := upd Heap.empty.bytes 1 (some #[49, 0])
257    nextBlk := 2
258    static := Zlib.Crc32.initStatics
259      (Zlib.Inftrees.initStatics (Zlib.Trees.trees_statics Heap.empty.static)) }
260
261theorem witness_fresh : Fresh witnessHeap := by
262  intro b hb hl
263  have h0 : b ≠ 0 := by change 2 ≤ b at hb; omega
264  have h1 : b ≠ 1 := by change 2 ≤ b at hb; omega
265  simp [Heap.live, witnessHeap, Heap.empty, upd_ne _ _ _ _ h0, upd_ne _ _ _ _ h1] at hl
266
267theorem witness_uniq : Uniq witnessHeap := by
268  intro b
269  by_cases h0 : b = 0
270  · subst b; simp [witnessHeap, Heap.empty, cnt]
271  by_cases h1 : b = 1
272  · subst b; simp [witnessHeap, Heap.empty, cnt]
273  simp [witnessHeap, Heap.empty, cnt, upd_ne _ _ _ _ h0, upd_ne _ _ _ _ h1]
274
275theorem witness_version : VersionValue witnessHeap (.ref (.blk 1) 0) (some 49) := by
276  right
277  refine ⟨49, rfl, Or.inr ⟨.blk 1, 0, #[49, 0], rfl, ?_, ?_, ?_⟩⟩ <;>
278    simp [Space.get, witnessHeap, Heap.empty]
279
280/-- Non-vacuity: a concrete default caller actually returns an initialized
281stream whose representation invariant was established by the entry. -/
282theorem default_init_witness :
283    ∃ after, C.run (deflateInit_ (some (.tab 0)) Z_DEFAULT_COMPRESSION (.ref (.blk 1) 0) 112)
284      witnessHeap = .ok (Z_OK, after) ∧
285      DeflateInitial witnessHeap after (.tab 0) (settings 6) := by
286  obtain ⟨rc, after, hr, hp⟩ := (deflateInit_proof Z_DEFAULT_COMPRESSION).2.2
287    witnessHeap (.tab 0) default (.ref (.blk 1) 0) witness_fresh witness_uniq rfl
288    (by simp [ZStreamRef.get, witnessHeap]) ⟨Or.inl rfl, Or.inl rfl⟩ witness_version
289  change after.nalloc = 5 ∧ rc = Z_OK ∧ DeflateInitial witnessHeap after (.tab 0) (settings 6) at hp
290  rw [hp.2.1] at hr
291  exact ⟨after, hr, hp.2.2⟩
292
293end ZlibF.Spec.Public.Proofs.DeflateInit