deflate.c.init.construct.lean

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

1import ZlibF.Proof.«deflate.c.init.default»
2
3/-! # deflate.c: establishing the invariant from default initialization writes
4
5The construction state is not assumed to satisfy DGood. In particular its
6window_size is still zero and its pending_out is still null before reset.
7-/
8
9namespace Zlib.Deflate.Proofs.DefaultInit
10open C Zlib.Deflate Zlib.Deflate.Spec
11open Zlib.Trees.Proofs.Out (TreesBase TreesInvAt ibRec trInitRec)
12set_option autoImplicit false
13
14def allocatedState (r : ZStreamRef) (w p q b : Nat) : DeflateState :=
15  { baseState r with
16    window := .ref (.blk w) 0, prev := .ref (.blk p) 0, head := .ref (.blk q) 0,
17    high_water := 0, lit_bufsize := 16384, pending_buf := .ref (.blk b) 0,
18    pending_buf_size := 65536 }
19
20def readyState (r : ZStreamRef) (level : Int32) (w p q b : Nat) : DeflateState :=
21  { allocatedState r w p q b with
22    sym_buf := .ref (.blk b) 16384, sym_end := 49149,
23    level, strategy := 0, «method» := 8 }
24
25def resetState (ds : Nat) (r : ZStreamRef) (level : Int32) (w p q b : Nat)
26    (a1 a2 a3 : Array CtData) : DeflateState :=
27  rkPost ds (rkMid (readyState r level w p q b)) a1 a2 a3
28
29def finalState (ds : Nat) (r : ZStreamRef) (level : Int32) (w p q b : Nat)
30    (a1 a2 a3 : Array CtData) : DeflateState :=
31  lmD (resetState ds r level w p q b a1 a2 a3)
32
33@[simp] theorem get_setW (h : Heap) (q : Nat) (a : Array UInt16) (r : ZStreamRef) :
34    r.get (setW h q a) = r.get h := by cases r <;> rfl
35
36/-- The match initializer does not change any storage pointer or extent. -/
37theorem blocks_lm {h : Heap} {d : DeflateState} {w p q b : Nat}
38    (hb : DBlocks h d w p q b) : DBlocks h (lmD d) w p q b := by
39  exact ⟨hb.win, hb.prev, hb.head, hb.pbuf, hb.wa, hb.wro, hb.pa, hb.qa, hb.ba,
40    hb.bro, hb.psize, hb.wb, hb.pq, hb.pout⟩
41
42/-- Reset sets pending_out before the normal initialized-state storage
43predicate is required. The premise describes the four allocated buffers;
44it does not claim that the unwritten pending_out field already has a value. -/
45theorem blocks_reset {h : Heap} {ds : Nat} {d : DeflateState} {w p q b : Nat}
46    (hb : DBlocks h { d with pending_out := d.pending_buf } w p q b)
47    (a1 a2 a3 : Array CtData) :
48    DBlocks h (rkPost ds (rkMid d) a1 a2 a3) w p q b := by
49  refine ⟨hb.win, hb.prev, hb.head, hb.pbuf, hb.wa, hb.wro, hb.pa, hb.qa, hb.ba,
50    hb.bro, hb.psize, hb.wb, hb.pq, 0, ?_, ?_⟩
51  · simpa [rkPost, rkPost3, rkMid, ibRec, trInitRec] using hb.pbuf
52  · simp [rkPost, rkPost3, rkMid, ibRec, trInitRec]
53
54/-- All representation fields after the actual reset and match initializer.
55Only the arbitrary legal compression level and the actual constructor's
56array extents remain symbolic. -/
57theorem final_inv {h : Heap} (ds : Nat) (r : ZStreamRef) (level : Int32) (w p q b : Nat)
58    (a1 a2 a3 : Array CtData) (s1 : a1.size = 573) (s2 : a2.size = 61) (s3 : a3.size = 39)
59    (hl0 : 0 ≤ level.toInt) (hl9 : level.toInt ≤ 9)
60    (hb : DBlocks h (finalState ds r level w p q b a1 a2 a3) w p q b) :
61    DStInv h ds (finalState ds r level w p q b a1 a2 a3) := by
62  constructor
63  all_goals first
64    | exact ⟨w, p, q, b, hb⟩
65    | simpa [finalState, resetState, lmD, rkPost, rkPost3, rkMid, ibRec, trInitRec,
66        readyState, allocatedState, baseState] using hl0
67    | simpa [finalState, resetState, lmD, rkPost, rkPost3, rkMid, ibRec, trInitRec,
68        readyState, allocatedState, baseState] using hl9
69    | simp [finalState, resetState, lmD, rkPost, rkPost3, rkMid, absWrap, ibRec, trInitRec,
70        readyState, allocatedState, baseState, DeflateState.WellFormed, DeflateState.zeroed,
71        DeflateState.garbage, s1, s2, s3, GzOk]
72
73/-- The actual reset establishes DGood from the construction storage.
74Neither DGood nor any reset execution contract is a premise. The caller
75has not yet written pending_out or window_size; the reset writes both. -/
76theorem reset_construct {h : Heap} {r : ZStreamRef} {z : ZStream} {ds w p q b : Nat}
77    (level : Int32) (hl : DLive h r ds z (readyState r level w p q b))
78    (ht : TreesBase h ds (readyState r level w p q b) b
79      ((h.bytes b).getD #[]))
80    (hb : DBlocks h { readyState r level w p q b with
81      pending_out := (readyState r level w p q b).pending_buf } w p q b)
82    (hu : Uniq h) (hf : Fresh h) (hl0 : 0 ≤ level.toInt) (hl9 : level.toInt ≤ 9) :
83    ∃ (a1 a2 a3 : Array CtData) (qa : Array UInt16),
84      a1.size = 573 ∧ a2.size = 61 ∧ a3.size = 39 ∧ h.words q = some qa ∧
85      let dr := resetState ds r level w p q b a1 a2 a3
86      let hr := setD (r.put h (rkZ z (readyState r level w p q b))) ds dr
87      let after := setD (setW hr q (clearHead qa 32768)) ds (lmD dr)
88      deflateReset (some r) h = .ok (Z_OK, after) ∧
89      DGood after r ds (rkZ z (readyState r level w p q b)) (lmD dr) ∧
90      (∀ x, after.live x ↔ h.live x) := by
91  obtain ⟨a1, a2, a3, hreset, s1, s2, s3⟩ := resetKeep_run' hl ht
92    (by change (-2 : Int) ≤ (1 : Int32).toInt; decide +kernel)
93    (by change (1 : Int32).toInt ≤ (2 : Int); decide +kernel)
94  let dr := resetState ds r level w p q b a1 a2 a3
95  let zr := rkZ z (readyState r level w p q b)
96  let hr := setD (r.put h zr) ds dr
97  have hsR : hr.dstates ds = some dr := by simp [hr]
98  have hzR : r.get hr = some zr := by simp [hr, ZStreamRef.get_put_same hl.hz]
99  have hbR : DBlocks hr dr w p q b := DBlocks.congr (by simp [hr]) (by simp [hr])
100    (by simp [hr]) (blocks_reset hb a1 a2 a3)
101  obtain ⟨qa, hqa, sizeQ⟩ := hbR.qa
102  have qsize : qa.size = 32768 := by simpa [dr, resetState, rkPost, rkPost3, rkMid,
103    ibRec, trInitRec, readyState, allocatedState, baseState] using sizeQ
104  have level0 : 0 ≤ dr.level.toInt := by simpa [dr, resetState, rkPost, rkPost3, rkMid,
105    ibRec, trInitRec, readyState] using hl0
106  have level9 : dr.level.toInt ≤ 9 := by simpa [dr, resetState, rkPost, rkPost3, rkMid,
107    ibRec, trInitRec, readyState] using hl9
108  have hash : dr.hash_size.toNat = 32768 := by
109    simp [dr, resetState, rkPost, rkPost3, rkMid, ibRec, trInitRec, readyState, allocatedState, baseState]
110  have hlm := lm_init_run hsR hbR hqa level0 level9 (by omega) (by omega)
111  rw [hash] at hlm
112  let after := setD (setW hr q (clearHead qa 32768)) ds (lmD dr)
113  have hbW := hbR.words_set q (clearHead qa 32768) qa hqa (size_clearHead _ _)
114  have hbF : DBlocks after (lmD dr) w p q b :=
115    blocks_lm (DBlocks.congr (by simp [after, setW]) (by simp [after, setW])
116      (by simp [after, setW]) hbW)
117  have hI : DStInv after ds (lmD dr) := final_inv ds r level w p q b a1 a2 a3
118    s1 s2 s3 hl0 hl9 hbF
119  have shapeR : Shape h hr := (shape_put hl.hz zr).trans (shape_setD (by simpa using hl.hs) dr)
120  have shapeF : Shape hr after := (shape_setW hqa _).trans (shape_setD (by simpa using hsR) _)
121  have shape := shapeR.trans shapeF
122  refine ⟨a1, a2, a3, qa, s1, s2, s3, by simpa [hr] using hqa, ?_, ?_, fun x => shape.live x⟩
123  · unfold deflateReset
124    rw [bind_app, hreset]
125    simp only [bind_app, beq_self_eq_true, ite_true]
126    change (do lm_init (← castDeflateState (← zrd (some r) (·.state))); pure Z_OK) hr = _
127    simp only [bind_app, zrd_eq, hzR, zr, rkZ, hl.zst, castD]
128    rw [hlm]
129    simp only [pure_app]
130    simp [after, hr, zr, rkZ, hl.zst, dr]
131  · refine ⟨⟨?_, by simp [after], ?_, ?_, ?_, ?_, ?_⟩, hI,
132      shape.uniq hu, shape.fresh (by simp [after, hr, setW]) hf, ?_⟩
133    · simp only [after, ZStreamRef.get_setD, get_setW, hr, zr,
134        ZStreamRef.get_put_same hl.hz]
135    · simpa [zr, rkZ] using hl.zst
136    · simp [dr, lmD, resetState, rkPost, rkPost3, rkMid, ibRec, trInitRec,
137        readyState, allocatedState, baseState]
138    · left
139      simp [dr, lmD, resetState, rkPost, rkPost3, rkMid, absWrap, ibRec, trInitRec,
140        readyState, allocatedState, baseState]
141    · simpa [zr, rkZ] using hl.zalloc
142    · simpa [zr, rkZ] using hl.zfree
143    · refine ⟨lmD dr, b, (h.bytes b).getD #[], ?_, ?_⟩
144      · refine ⟨by simp only [after, setD_dstates_same]; rfl, hI.wf, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
145        · simpa [after, hr, setW] using ht.static
146        · simpa [dr, lmD, resetState, rkPost, rkPost3, rkMid, ibRec, trInitRec] using ht.pbuf
147        · simpa [after, hr, setW] using ht.bytes
148        · simpa [after, hr, setW] using ht.rw
149        · simpa [dr, lmD, resetState, rkPost, rkPost3, rkMid, ibRec, trInitRec] using ht.size
150        · simpa [dr, lmD, resetState, rkPost, rkPost3, rkMid, ibRec, trInitRec] using ht.psize
151        · simpa [dr, lmD, resetState, rkPost, rkPost3, rkMid, ibRec, trInitRec] using ht.sym
152        · simpa [dr, lmD, resetState, rkPost, rkPost3, rkMid, ibRec, trInitRec] using ht.lit_lo
153        · simpa [dr, lmD, resetState, rkPost, rkPost3, rkMid, ibRec, trInitRec] using ht.lit_hi
154        · simpa [dr, lmD, resetState, rkPost, rkPost3, rkMid, ibRec, trInitRec] using ht.sym_end
155        · simp [dr, lmD, resetState, rkPost, rkPost3, rkMid, ibRec, trInitRec]
156      · refine ⟨rfl, rfl, rfl, rfl, rfl, rfl, ?_, ?_, ?_, ?_, ?_⟩ <;>
157          simp [dr, lmD, resetState, rkPost, rkPost3, rkMid, ibRec, trInitRec]
158
159end Zlib.Deflate.Proofs.DefaultInit