deflate.c.life.reset.lean

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

1import ZlibF.Proof.«deflate.c.base»
2import ZlibF.Proof.«trees.c.block»
3
4/-!
5# deflate.c: `lm_init`, `deflateResetKeep`, `deflateReset`
6-/
7
8namespace Zlib.Deflate.Spec
9open C
10
11/-- The head array after `CLEAR_HASH`: the first `hash_size` entries are 0 (`head[hash_size - 1] = NIL` and the
12`memset` of the entries before it); the array has the same size. -/
13def clearHead (qa : Array UInt16) (hs : Nat) : Array UInt16 := fillRange (qa.set! (hs - 1) 0) 0 (hs - 1) 0
14
15/-- The state record after `lm_init`: `window_size = 2 * w_size`, the hash is cleared (`slid = 0`), `matches = 0`, the
16tuning fields come from the table row of the level, and the position and match fields are reset. -/
17def lmD (d : DeflateState) : DeflateState :=
18  let c := Zlib.Deflate.configuration_table[d.level.toInt.toNat]!
19  { d with window_size := 2 * d.w_size.toUInt64, slid := 0, «matches» := 0, max_lazy_match := c.max_lazy.toUInt32,
20           good_match := c.good_length.toUInt32, nice_match := c.nice_length.toUInt32.toInt32,
21           max_chain_length := c.max_chain.toUInt32, strstart := 0, block_start := 0, lookahead := 0, insert := 0,
22           match_length := Zlib.Deflate.MIN_MATCH_u - 1, prev_length := Zlib.Deflate.MIN_MATCH_u - 1,
23           match_available := 0, ins_h := 0 }
24
25
26/-- `abs (wrap)`: `deflateResetKeep` makes the wrapper positive again (`wrap` is negative once the trailer was written). -/
27def absWrap (w : Int32) : Int32 := if w < 0 then -w else w
28
29/-- The state record after the first statements of `deflateResetKeep` (up to the wrapper): the pending output is dropped and
30the wrapper is positive. -/
31def rkMid (d : DeflateState) : DeflateState :=
32  { d with pending := 0, pending_out := d.pending_buf, wrap := absWrap d.wrap }
33
34/-- The state record after the statements of `deflateResetKeep` that follow the update of `status`, from the record `d3` that
35has the new `status`: `last_flush = -2`, `gzhead = NULL`, then `_tr_init` (given the three code arrays that `init_block`
36produced: their size is the C size, `Freq` is 0 except `dyn_ltree[END_BLOCK]`, which is 1): the descriptors point to the
37arrays of the record, the bit buffer is empty; `matches` is kept at level 0 and cleared otherwise, `block_start = strstart`,
38and the match state is reset. -/
39def rkPost3 (id : Nat) (d3 : DeflateState) (a1 a2 a3 : Array CtData) : DeflateState :=
40  let d4 : DeflateState := { d3 with last_flush := -2, gzhead := none }
41  let dT := Zlib.Trees.Proofs.Out.ibRec (Zlib.Trees.Proofs.Out.trInitRec id d4) a1 a2 a3
42  { dT with «matches» := if d3.level == 0 then d3.«matches» else 0, block_start := dT.strstart.toUInt64.toInt64,
43            lookahead := 0, match_length := Zlib.Deflate.MIN_MATCH_u - 1, prev_length := Zlib.Deflate.MIN_MATCH_u - 1,
44            match_available := 0 }
45
46/-- The state record after the rest of `deflateResetKeep`, from the record `d2` after the wrapper: `status` is the gzip or
47zlib header state, then `rkPost3`. -/
48def rkPost (id : Nat) (d2 : DeflateState) (a1 a2 a3 : Array CtData) : DeflateState :=
49  rkPost3 id { d2 with status := if d2.wrap == 2 then GZIP_STATE else INIT_STATE } a1 a2 a3
50
51/-- The stream record after `deflateResetKeep`: the counters and `msg` are cleared, `data_type = Z_UNKNOWN`, and `adler` is the
52checksum of nothing (1, or 0 for a gzip stream). -/
53def rkZ (z : ZStream) (d : DeflateState) : ZStream :=
54  { z with total_in := 0, total_out := 0, msg := .null, data_type := Z_UNKNOWN,
55           adler := if absWrap d.wrap == 2 then 0 else 1 }
56
57end Zlib.Deflate.Spec
58
59namespace Zlib.Deflate.Proofs
60open C Zlib.Deflate Zlib.Deflate.Spec
61
62theorem u32_sub_one {x : UInt32} (hx : 1 ≤ x.toNat) : (x - 1).toNat = x.toNat - 1 := by
63  rw [UInt32.toNat_sub_of_le x 1 (by rw [UInt32.le_iff_toNat_le]; simp; omega)]
64  simp
65
66/-- The heap with the block of words `q` replaced. -/
67def setW (h : Heap) (q : Nat) (a : Array UInt16) : Heap := { h with words := upd h.words q (some a) }
68
69@[simp] theorem setW_dstates (h : Heap) (q : Nat) (a : Array UInt16) : (setW h q a).dstates = h.dstates := rfl
70@[simp] theorem setW_words_same (h : Heap) (q : Nat) (a : Array UInt16) : (setW h q a).words q = some a := by
71  simp [setW]
72@[simp] theorem setW_bytes (h : Heap) (q : Nat) (a : Array UInt16) : (setW h q a).bytes = h.bytes := rfl
73@[simp] theorem setW_ro (h : Heap) (q : Nat) (a : Array UInt16) : (setW h q a).ro = h.ro := rfl
74theorem Space_put_words (h : Heap) (q : Nat) (a : Array UInt16) : Space.put h (WRef.blk q) a = setW h q a := rfl
75
76/-- `CLEAR_HASH(s)` on a state whose `head` is a block of at least `hash_size` words (and `hash_size` is not 0). -/
77theorem clearHash_run {h : Heap} {ds : Nat} {d : DeflateState} {q : Nat} {qa : Array UInt16}
78    (hs : h.dstates ds = some d) (hq : d.head = .ref (.blk q) 0) (hqa : h.words q = some qa)
79    (h1 : 1 ≤ d.hash_size.toNat) (h2 : d.hash_size.toNat ≤ qa.size) :
80    CLEAR_HASH (some (.tab ds)) h =
81      .ok ((), setD (setW h q (clearHead qa d.hash_size.toNat)) ds { d with slid := 0 }) := by
82  have hn : (d.hash_size - 1).toNat = d.hash_size.toNat - 1 := u32_sub_one h1
83  have e1 : padd (Ptr.ref (WRef.blk q) 0) (d.hash_size.toNat - 1) h = .ok (Ptr.ref (WRef.blk q) (0 + (d.hash_size.toNat - 1)), h) :=
84    Ptr.add_nat_ok (h := h) (r := WRef.blk q) (a := qa) (off := 0) (n := d.hash_size.toNat - 1) hqa (by omega)
85  have e2 := Ptr.store_ok (h := h) (r := WRef.blk q) (a := qa) (off := 0 + (d.hash_size.toNat - 1)) (v := (0 : UInt16))
86    hqa rfl (by omega)
87  have e3 := Ptr.fill_ok (h := setW h q (qa.set! (0 + (d.hash_size.toNat - 1)) 0))
88    (r := WRef.blk q) (a := qa.set! (0 + (d.hash_size.toNat - 1)) 0) (off := 0) (n := d.hash_size.toNat - 1) (v := (0 : UInt16))
89    (by simp [Space.get, setW]) rfl (by simp; omega)
90  rw [Space_put_words] at e2 e3
91  unfold CLEAR_HASH
92  simp only [bind_app, ldD_eq, hs]
93  rw [hq, hn, e1]
94  simp only []
95  rw [e2]
96  simp only []
97  rw [e3]
98  simp only []
99  rw [wrD_eq]
100  simp only [setW_dstates, hs]
101  simp [setW, clearHead, setD, upd_upd, hq]
102
103theorem config_at_run (h : Heap) {level : Int32} (h0 : 0 ≤ level.toInt) (h1 : level.toInt ≤ 9) :
104    config_at level h = .ok (Zlib.Deflate.configuration_table[level.toInt.toNat]!, h) := by
105  unfold config_at
106  simp [show 0 ≤ level.toInt ∧ level.toInt < 10 from ⟨h0, by omega⟩]
107
108theorem lm_init_run {h : Heap} {ds : Nat} {d : DeflateState} {w p q b : Nat} {qa : Array UInt16}
109    (hs : h.dstates ds = some d) (hB : DBlocks h d w p q b) (hqa : h.words q = some qa)
110    (hl0 : 0 ≤ d.level.toInt) (hl1 : d.level.toInt ≤ 9)
111    (h1 : 1 ≤ d.hash_size.toNat) (h2 : d.hash_size.toNat ≤ qa.size) :
112    lm_init (some (.tab ds)) h = .ok ((), setD (setW h q (clearHead qa d.hash_size.toNat)) ds (lmD d)) := by
113  have hs1 : (setD h ds { d with window_size := 2 * d.w_size.toUInt64 }).dstates ds = some { d with window_size := 2 * d.w_size.toUInt64 } :=
114    setD_dstates_same _ _ _
115  have hc := clearHash_run (h := setD h ds { d with window_size := 2 * d.w_size.toUInt64 }) (ds := ds)
116    (d := { d with window_size := 2 * d.w_size.toUInt64 }) (q := q) (qa := qa) hs1 hB.head (by simpa using hqa) h1 h2
117  unfold lm_init
118  simp only [wrD_eq, bind_app, hs]
119  rw [hc]
120  simp only [wrD_eq, rdD_eq, bind_app, setD_dstates_same, setW_dstates, setD_setD]
121  rw [config_at_run _ hl0 hl1]
122  simp only [wrD_eq, rdD_eq, bind_app, setD_dstates_same, setW_dstates, setD_setD]
123  simp [lmD, setD, setW, clearHead, hs, upd_upd]
124
125theorem toNat_two_mul_toUInt64 (x : UInt32) : (2 * x.toUInt64).toNat = 2 * x.toNat := by
126  rw [UInt64.toNat_mul]
127  have := UInt32.toNat_lt x
128  simp
129  omega
130
131theorem size_clearHead (qa : Array UInt16) (hs : Nat) : (clearHead qa hs).size = qa.size := by
132  unfold clearHead
133  rw [size_fillRange]
134  simp
135
136theorem _root_.Zlib.Deflate.Spec.DStInv.lm {h : Heap} {ds : Nat} {d : DeflateState} (hI : DStInv h ds d) :
137    DStInv h ds (lmD d) := by
138  have e : (lmD d).window_size.toNat = 2 * d.w_size.toNat := toNat_two_mul_toUInt64 d.w_size
139  exact { hI with
140    wsz := e
141    hw := by rw [e]; rw [← hI.wsz]; exact hI.hw
142    blocks := hI.blocks_keys rfl rfl rfl rfl rfl rfl rfl rfl rfl rfl }
143
144/-- **lm_init, safety and specification.** On a state of a stream with the invariant the call never faults. It clears
145the hash heads (the first `hash_size` entries of the `head` block become 0, the block keeps its size), sets
146`window_size = 2 * w_size`, `matches = 0`, loads `max_lazy_match`, `good_match`, `nice_match` and `max_chain_length` from the
147configuration table row of `level`, and sets `strstart`, `block_start`, `lookahead` and `insert` to 0, `match_length` and
148`prev_length` to `MIN_MATCH - 1`, `match_available` and `ins_h` to 0. The record is `lmD d`; the heap is the old one with
149the `head` block replaced (`clearHead`) and the state record replaced. The stream is initialised again with the
150invariants intact; the live blocks are the same. -/
151theorem lm_init_safe {h : Heap} {r : ZStreamRef} {ds : Nat} {z : ZStream} {d : DeflateState}
152    (hG : DGood h r ds z d) :
153    ∃ q qa h', C.run (lm_init (some (.tab ds))) h = .ok ((), h') ∧ d.head = .ref (.blk q) 0 ∧ h.words q = some qa ∧
154      h' = setD (setW h q (clearHead qa d.hash_size.toNat)) ds (lmD d) ∧
155      DGood h' r ds z (lmD d) ∧ (∀ b, h'.live b ↔ h.live b) := by
156  have hI := hG.inv
157  obtain ⟨w, p, q, b, hB⟩ := hI.blocks
158  obtain ⟨qa, hqa, hqz⟩ := hB.qa
159  have h1 : 1 ≤ d.hash_size.toNat := by
160    have := hI.hsize; have : 2 ^ d.hash_bits.toNat > 0 := Nat.two_pow_pos _; omega
161  refine ⟨q, qa, _, lm_init_run hG.live.hs hB hqa hI.level_lo hI.level_hi h1 (Nat.le_of_eq hqz.symm), hB.head, hqa, rfl, ?_, ?_⟩
162  · have hG1 := hG.words_set q (clearHead qa d.hash_size.toNat) qa hqa (size_clearHead _ _)
163    have := hG1.setD' (d' := lmD d) rfl hG.live.status (hI.lm.words_set q _ qa hqa (size_clearHead _ _)) (by trkeep)
164    simpa [setD, setW] using this
165  · intro x
166    exact ((shape_setW hqa _).trans (shape_setD (d0 := d) (by simpa using hG.live.hs) _)).live x
167
168open Zlib.Trees (_tr_init)
169
170/-- The part of `deflateResetKeep` from the store of `adler` on. -/
171def rkTail2 (strm : ZStreamPtr) (s : DeflateStatePtr) (adler : UInt64) : M Int32 := do
172  zwr strm (fun z => { z with adler })
173  wr s (fun d => { d with last_flush := -2, gzhead := none })
174  let d ← ldDeflateState s
175  let «matches» : UInt32 := if d.level == 0 then d.«matches» else 0
176  _tr_init s
177  wr s (fun d => { d with «matches» := «matches» })
178  wr s (fun d => { d with block_start := d.strstart.toUInt64.toInt64, lookahead := 0,
179                          match_length := MIN_MATCH_u - 1, prev_length := MIN_MATCH_u - 1, match_available := 0 })
180  return Z_OK
181
182/-- The part of `deflateResetKeep` from the status on. -/
183def rkTail (strm : ZStreamPtr) (s : DeflateStatePtr) : M Int32 := do
184  wr s (fun d => { d with status := if d.wrap == 2 then GZIP_STATE else INIT_STATE })
185  let adler ← if (← rd s (·.wrap)) == 2 then Zlib.Crc32.crc32 0 (Ptr.null : BPtr) 0
186    else Zlib.Adler32.adler32 0 (Ptr.null : BPtr) 0
187  rkTail2 strm s adler
188
189theorem deflateResetKeep_eq (strm : ZStreamPtr) : deflateResetKeep strm = (do
190    if (← deflateStateCheck strm) != 0 then return Z_STREAM_ERROR
191    zwr strm (fun z => { z with total_in := 0, total_out := 0, msg := .null, data_type := Z_UNKNOWN })
192    let s ← castDeflateState (← zrd strm (·.state))
193    wr s (fun d => { d with pending := 0, pending_out := d.pending_buf })
194    let d ← ldDeflateState s
195    if d.wrap < 0 then
196      let w ← ineg d.wrap
197      wr s (fun d => { d with wrap := w })
198    rkTail strm s) := by
199  rfl
200
201theorem crc32_null : Zlib.Crc32.crc32 0 (Ptr.null : BPtr) 0 = (pure 0 : M UInt64) := by
202  unfold Zlib.Crc32.crc32 Zlib.Crc32.crc32_z
203  simp
204
205theorem adler32_null : Zlib.Adler32.adler32 0 (Ptr.null : BPtr) 0 = (pure 1 : M UInt64) := by
206  unfold Zlib.Adler32.adler32 Zlib.Adler32.adler32_z
207  simp
208
209
210theorem trSetD_eq (h : Heap) (id : Nat) (d : DeflateState) : Zlib.Trees.Proofs.Out.setD h id d = setD h id d := rfl
211
212theorem rkTail2_run {H : Heap} {r : ZStreamRef} {ds : Nat} {z' : ZStream} {d3 : DeflateState} {b : Nat} {buf : Array UInt8}
213    (hz : r.get H = some z') (hb : Zlib.Trees.Proofs.Out.TreesBase H ds d3 b buf) (v : UInt64) :
214    ∃ a1 a2 a3, rkTail2 (some r) (some (.tab ds)) v H =
215      .ok (Z_OK, setD (r.put H { z' with adler := v }) ds (rkPost3 ds d3 a1 a2 a3)) ∧
216      a1.size = 573 ∧ a2.size = 61 ∧ a3.size = 39 := by
217  have hd := hb.dstate
218  have hb2 : Zlib.Trees.Proofs.Out.TreesBase (setD (r.put H { z' with adler := v }) ds { d3 with last_flush := -2, gzhead := none })
219      ds { d3 with last_flush := -2, gzhead := none } b buf :=
220    ⟨by simp [setD], hb.wf, by simpa using hb.static, hb.pbuf, by simpa using hb.bytes, by simpa using hb.rw, hb.size,
221      hb.psize, hb.sym, hb.lit_lo, hb.lit_hi, hb.sym_end, hb.pending_le⟩
222  obtain ⟨a1, a2, a3, d', e, -, hd', s1, s2, s3⟩ := Zlib.Trees.Proofs.Out.tr_init_spec hb2
223  refine ⟨a1, a2, a3, ?_, s1, s2, s3⟩
224  rw [trSetD_eq] at e
225  unfold rkTail2
226  simp only [bind_app, zwr_eq, hz, wrD_eq, rdD_eq, ldD_eq, ZStreamRef.put_dstates, hd, setD_dstates_same, ZStreamRef.get_setD, e, pure_app, setD_setD]
227  subst hd'
228  simp [rkPost3, setD_setD]
229
230theorem rkTail_run {H : Heap} {r : ZStreamRef} {ds : Nat} {z' : ZStream} {d2 : DeflateState} {b : Nat} {buf : Array UInt8}
231    (hz : r.get H = some z') (hb : Zlib.Trees.Proofs.Out.TreesBase H ds d2 b buf) :
232    ∃ a1 a2 a3, rkTail (some r) (some (.tab ds)) H =
233      .ok (Z_OK, setD (r.put H { z' with adler := if d2.wrap == 2 then 0 else 1 }) ds (rkPost ds d2 a1 a2 a3)) ∧
234      a1.size = 573 ∧ a2.size = 61 ∧ a3.size = 39 := by
235  have hd := hb.dstate
236  have hb3 : Zlib.Trees.Proofs.Out.TreesBase (setD H ds { d2 with status := if d2.wrap == 2 then GZIP_STATE else INIT_STATE })
237      ds { d2 with status := if d2.wrap == 2 then GZIP_STATE else INIT_STATE } b buf :=
238    ⟨by simp [setD], hb.wf, by simpa using hb.static, hb.pbuf, by simpa using hb.bytes, by simpa using hb.rw, hb.size,
239      hb.psize, hb.sym, hb.lit_lo, hb.lit_hi, hb.sym_end, hb.pending_le⟩
240  have hz3 : r.get (setD H ds { d2 with status := if d2.wrap == 2 then GZIP_STATE else INIT_STATE }) = some z' := by
241    simpa using hz
242  obtain ⟨a1, a2, a3, e, s1, s2, s3⟩ := rkTail2_run hz3 hb3 (if d2.wrap == 2 then 0 else 1)
243  refine ⟨a1, a2, a3, ?_, s1, s2, s3⟩
244  unfold rkTail
245  by_cases hc : (d2.wrap == 2) = true
246  · simp only [hc, ↓reduceIte] at e
247    simp only [bind_app, wrD_eq, rdD_eq, hd, setD_dstates_same, hc, ↓reduceIte, crc32_null, pure_app]
248    rw [e]
249    simp [ZStreamRef.put_setD, setD_setD, rkPost, hc]
250  · have hc' : (d2.wrap == 2) = false := by simpa using hc
251    simp only [hc', Bool.false_eq_true, ↓reduceIte] at e
252    simp only [bind_app, wrD_eq, rdD_eq, hd, setD_dstates_same, hc', Bool.false_eq_true, ↓reduceIte, adler32_null, pure_app]
253    rw [e]
254    simp [ZStreamRef.put_setD, setD_setD, rkPost, hc]
255
256theorem ineg_neg {w : Int32} (h1 : -2 ≤ w.toInt) (h2 : w.toInt < 0) : ineg w = (pure (-w) : M Int32) := by
257  unfold ineg chk32
258  have e : (-w).toInt = - w.toInt := by
259    rw [Int32.toInt_neg]
260    have := w.toInt_lt
261    have := w.le_toInt
262    rw [Int.bmod_eq_of_le (by omega) (by omega)]
263  have : -2147483648 ≤ -w.toInt ∧ -w.toInt ≤ 2147483647 := by omega
264  simp only [this, and_self, ↓reduceIte]
265  congr 1
266  apply Int32.toInt_inj.mp
267  rw [e, Int32.toInt_ofInt]
268  rw [Int.bmod_eq_of_le (by simp only [Int32.size]; omega) (by simp only [Int32.size]; omega)]
269
270theorem resetKeep_run' {h : Heap} {r : ZStreamRef} {ds : Nat} {z : ZStream} {d : DeflateState} {b : Nat}
271    {buf : Array UInt8} (hL : DLive h r ds z d) (hB : Zlib.Trees.Proofs.Out.TreesBase h ds d b buf)
272    (hw1 : -2 ≤ d.wrap.toInt) (hw2 : d.wrap.toInt ≤ 2) :
273    ∃ a1 a2 a3, deflateResetKeep (some r) h =
274      .ok (Z_OK, setD (r.put h (rkZ z d)) ds (rkPost ds (rkMid d) a1 a2 a3)) ∧
275      a1.size = 573 ∧ a2.size = 61 ∧ a3.size = 39 := by
276  have hbm : Zlib.Trees.Proofs.Out.TreesBase (setD (r.put h { z with total_in := 0, total_out := 0, msg := .null, data_type := Z_UNKNOWN }) ds (rkMid d))
277      ds (rkMid d) b buf :=
278    ⟨by simp [setD], hB.wf, by simpa using hB.static, hB.pbuf, by simpa using hB.bytes, by simpa using hB.rw, hB.size,
279      hB.psize, hB.sym, hB.lit_lo, hB.lit_hi, hB.sym_end, by simp [rkMid]⟩
280  have hzm : r.get (setD (r.put h { z with total_in := 0, total_out := 0, msg := .null, data_type := Z_UNKNOWN }) ds (rkMid d)) =
281      some { z with total_in := 0, total_out := 0, msg := .null, data_type := Z_UNKNOWN } := by
282    simp [ZStreamRef.get_put, hL.hz]
283  obtain ⟨a1, a2, a3, e, s1, s2, s3⟩ := rkTail_run hzm hbm
284  refine ⟨a1, a2, a3, ?_, s1, s2, s3⟩
285  rw [deflateResetKeep_eq]
286  by_cases hw : d.wrap < 0
287  · have hw' : -2 ≤ d.wrap.toInt ∧ d.wrap.toInt < 0 := ⟨hw1, (Int32.lt_iff_toInt_lt.mp hw)⟩
288    simp only [bind_app, stateCheck_live hL, bne_self_eq_false, Bool.false_eq_true, ↓reduceIte, zwr_eq, hL.hz, zrd_eq,
289      ZStreamRef.get_put_same hL.hz, hL.zst, castD, wrD_eq, ZStreamRef.put_dstates, hL.hs, setD_dstates_same, ldD_eq, hw,
290      ineg_neg hw'.1 hw'.2, pure_app, setD_setD]
291    simp only [rkMid, absWrap, hw, ↓reduceIte, hL.zst] at e
292    rw [e]
293    simp [rkZ, rkMid, absWrap, hw, ZStreamRef.put_setD, ZStreamRef.put_put, hL.zst]
294  · simp only [bind_app, stateCheck_live hL, bne_self_eq_false, Bool.false_eq_true, ↓reduceIte, zwr_eq, hL.hz, zrd_eq,
295      ZStreamRef.get_put_same hL.hz, hL.zst, castD, wrD_eq, ZStreamRef.put_dstates, hL.hs, setD_dstates_same, ldD_eq, hw,
296      pure_app, setD_setD]
297    simp only [rkMid, absWrap, hw, ↓reduceIte, hL.zst] at e
298    rw [e]
299    simp [rkZ, rkMid, absWrap, hw, ZStreamRef.put_setD, ZStreamRef.put_put, hL.zst]
300
301theorem resetKeep_run {h : Heap} {r : ZStreamRef} {ds : Nat} {z : ZStream} {d : DeflateState}
302    (hG : DGood h r ds z d) :
303    ∃ a1 a2 a3, deflateResetKeep (some r) h =
304      .ok (Z_OK, setD (r.put h (rkZ z d)) ds (rkPost ds (rkMid d) a1 a2 a3)) ∧
305      a1.size = 573 ∧ a2.size = 61 ∧ a3.size = 39 := by
306  obtain ⟨d0, b, buf, hB, hR⟩ := hG.trees
307  have e0 : d0 = d := Option.some.inj (hB.dstate.symm.trans hG.live.hs)
308  rw [e0] at hB
309  exact resetKeep_run' hG.live hB hG.inv.wrap_lo hG.inv.wrap_hi
310
311theorem absWrap_range {w : Int32} (h1 : -2 ≤ w.toInt) (h2 : w.toInt ≤ 2) :
312    0 ≤ (absWrap w).toInt ∧ (absWrap w).toInt ≤ 2 := by
313  unfold absWrap
314  by_cases hw : w < 0
315  · have hw' := Int32.lt_iff_toInt_lt.mp hw
316    simp at hw'
317    have : (-w).toInt = - w.toInt := by
318      rw [Int32.toInt_neg]
319      have := w.toInt_lt
320      have := w.le_toInt
321      rw [Int.bmod_eq_of_le (by omega) (by omega)]
322    rw [ite_eq_left hw, this]; omega
323  · have hw' : ¬ w.toInt < 0 := fun h => hw (Int32.lt_iff_toInt_lt.mpr (by simpa using h))
324    rw [ite_eq_right hw]; omega
325
326theorem _root_.Zlib.Deflate.Spec.DStInv.resetKeep {h : Heap} {ds : Nat} {d : DeflateState} (hI : DStInv h ds d) (a1 a2 a3 : Array CtData)
327    (s1 : a1.size = 573) (s2 : a2.size = 61) (s3 : a3.size = 39) :
328    DStInv h ds (rkPost ds (rkMid d) a1 a2 a3) := by
329  obtain ⟨w, p, q, b, hB⟩ := hI.blocks
330  obtain ⟨wf1, wf2, wf3, wf4, wf5, wf6⟩ := hI.wf
331  have hr := absWrap_range hI.wrap_lo hI.wrap_hi
332  obtain ⟨_, hsb, hsl⟩ := hI.sym
333  refine ⟨⟨s1, s2, s3, wf4, wf5, wf6⟩, hI.wbits_lo, hI.wbits_hi, hI.wsize, hI.wmask, hI.wsz, hI.hbits_lo, hI.hbits_hi,
334    hI.hsize, hI.hmask, hI.hshift, hI.lit, hI.level_lo, hI.level_hi, hI.strat_lo, hI.strat_hi, hI.method, ?_, ?_, hI.hw,
335    ⟨w, p, q, b, ?_⟩, ?_, ?_, ?_⟩
336  · simp [rkPost, rkPost3, rkMid, Zlib.Trees.Proofs.Out.ibRec, Zlib.Trees.Proofs.Out.trInitRec]; have := hr.1; omega
337  · simp [rkPost, rkPost3, rkMid, Zlib.Trees.Proofs.Out.ibRec, Zlib.Trees.Proofs.Out.trInitRec]; exact hr.2
338  · obtain ⟨a1', a2', a3', a4', wa, r1, pa, qa, ba, r4, ps, wb, pq, ⟨off, po, pl⟩⟩ := hB
339    refine ⟨a1', a2', a3', a4', wa, r1, pa, qa, ba, r4, ps, wb, pq, ⟨0, ?_, ?_⟩⟩
340    · simp [rkPost, rkPost3, rkMid, Zlib.Trees.Proofs.Out.ibRec, Zlib.Trees.Proofs.Out.trInitRec, a4']
341    · simp [rkPost, rkPost3, rkMid, Zlib.Trees.Proofs.Out.ibRec, Zlib.Trees.Proofs.Out.trInitRec]
342  · refine ⟨?_, ?_, ?_, ?_⟩
343    · obtain ⟨b', hb1, hb2⟩ := hI.sym.1
344      exact ⟨b', by simpa [rkPost, rkPost3, rkMid, Zlib.Trees.Proofs.Out.ibRec, Zlib.Trees.Proofs.Out.trInitRec] using hb1,
345        by simpa [rkPost, rkPost3, rkMid, Zlib.Trees.Proofs.Out.ibRec, Zlib.Trees.Proofs.Out.trInitRec] using hb2⟩
346    · simpa [rkPost, rkPost3, rkMid, Zlib.Trees.Proofs.Out.ibRec, Zlib.Trees.Proofs.Out.trInitRec] using hsb
347    · simp [rkPost, rkPost3, rkMid, Zlib.Trees.Proofs.Out.ibRec, Zlib.Trees.Proofs.Out.trInitRec]
348    · simp [rkPost, rkPost3, rkMid, Zlib.Trees.Proofs.Out.ibRec, Zlib.Trees.Proofs.Out.trInitRec]
349  · simp [rkPost, rkPost3, rkMid, Zlib.Trees.Proofs.Out.ibRec, Zlib.Trees.Proofs.Out.trInitRec]
350  · simp [rkPost, rkPost3, rkMid, Zlib.Trees.Proofs.Out.ibRec, Zlib.Trees.Proofs.Out.trInitRec, GzOk]
351
352theorem mod_absWrap_status (d : DeflateState) : GoodStatus (if (absWrap d.wrap == 2) = true then GZIP_STATE else INIT_STATE) := by
353  unfold GoodStatus
354  split
355  · exact Or.inr (Or.inl rfl)
356  · exact Or.inl rfl
357
358/-- **deflateResetKeep, safety and specification.** On an initialised stream with the invariant the call never faults and
359returns `Z_OK`. The stream record gets `total_in = total_out = 0`, `msg = NULL`, `data_type = Z_UNKNOWN` and `adler` 1 (0 for
360a gzip wrapper): `rkZ`. The state record is `rkPost`: the pending output is dropped (`pending = 0`, `pending_out =
361pending_buf`), a negative wrapper becomes positive, `status` is the zlib or gzip header state, `last_flush = -2`, `gzhead =
362NULL`, the trees are reset (`_tr_init`: empty bit buffer, no symbols, the code frequencies of the three arrays are 0 except
363the end-of-block code, `opt_len = static_len = 0`), `matches` is kept at level 0 and cleared otherwise, `block_start =
364strstart`, `lookahead = 0`, `match_length = prev_length = MIN_MATCH - 1`, `match_available = 0`. The window, the hash and
365the other settings are kept. The stream is initialised again with the invariants intact, and the live blocks are the same
366(no allocation, no free). -/
367theorem deflateResetKeep_safe {h : Heap} {r : ZStreamRef} {ds : Nat} {z : ZStream} {d : DeflateState}
368    (hG : DGood h r ds z d) :
369    ∃ a1 a2 a3 h', C.run (deflateResetKeep (some r)) h = .ok (Z_OK, h') ∧
370      h' = setD (r.put h (rkZ z d)) ds (rkPost ds (rkMid d) a1 a2 a3) ∧ a1.size = 573 ∧ a2.size = 61 ∧ a3.size = 39 ∧
371      DGood h' r ds (rkZ z d) (rkPost ds (rkMid d) a1 a2 a3) ∧ (∀ b, h'.live b ↔ h.live b) := by
372  obtain ⟨a1, a2, a3, e, s1, s2, s3⟩ := resetKeep_run hG
373  refine ⟨a1, a2, a3, _, e, rfl, s1, s2, s3, ?_, ?_⟩
374  · have hI := hG.inv.resetKeep a1 a2 a3 s1 s2 s3
375    obtain ⟨d0, b, buf, hB, hR⟩ := hG.trees
376    have e0 : d0 = d := Option.some.inj (hB.dstate.symm.trans hG.live.hs)
377    rw [e0] at hB hR
378    have hS : Shape h (setD (r.put h (rkZ z d)) ds (rkPost ds (rkMid d) a1 a2 a3)) :=
379      (shape_put hG.live.hz _).trans (shape_setD (by simpa using hG.live.hs) _)
380    refine ⟨⟨?_, by simp, ?_, ?_, ?_, ?_, ?_⟩,
381      DStInv.congr (h := h) (h' := setD (r.put h (rkZ z d)) ds (rkPost ds (rkMid d) a1 a2 a3)) (by simp) (by simp) (by simp) (by simp) hI,
382      hS.uniq hG.uniq, hS.fresh (by simp) hG.fresh, ?_⟩
383    · simp [ZStreamRef.get_put, hG.live.hz]
384    · simpa [rkZ] using hG.live.zst
385    · simpa [rkPost, rkPost3, rkMid, Zlib.Trees.Proofs.Out.ibRec, Zlib.Trees.Proofs.Out.trInitRec] using hG.live.back
386    · exact mod_absWrap_status d
387    · simpa [rkZ] using hG.live.zalloc
388    · simpa [rkZ] using hG.live.zfree
389    · refine ⟨_, b, buf, ⟨by simp, hI.wf, by simpa using hB.static, hB.pbuf, by simpa using hB.bytes, by simpa using hB.rw,
390        hB.size, hB.psize, hB.sym, hB.lit_lo, hB.lit_hi, hB.sym_end,
391        by simp [rkPost, rkPost3, rkMid, Zlib.Trees.Proofs.Out.ibRec, Zlib.Trees.Proofs.Out.trInitRec]⟩, ?_⟩
392      refine ⟨rfl, rfl, rfl, rfl, rfl, rfl, ?_, ?_, ?_, ?_, ?_⟩ <;>
393        simp [rkPost, rkPost3, rkMid, Zlib.Trees.Proofs.Out.ibRec, Zlib.Trees.Proofs.Out.trInitRec]
394  · intro x
395    exact ((shape_put hG.live.hz _).trans (shape_setD (by simpa using hG.live.hs) _)).live x
396
397/-- **deflateReset, safety and specification.** On an initialised stream with the invariant the call never faults and returns
398`Z_OK`: it is `deflateResetKeep` (`rkZ`, `rkPost`) followed by `lm_init` (`lmD`: the hash heads are cleared, `window_size =
3992 * w_size`, the tuning fields are reloaded from the table row of `level`, the position and the match state are reset). The
400stream is initialised again with the invariants intact, and the live blocks are the same (no allocation, no free). -/
401theorem deflateReset_safe {h : Heap} {r : ZStreamRef} {ds : Nat} {z : ZStream} {d : DeflateState}
402    (hG : DGood h r ds z d) :
403    ∃ a1 a2 a3 q qa h', C.run (deflateReset (some r)) h = .ok (Z_OK, h') ∧
404      a1.size = 573 ∧ a2.size = 61 ∧ a3.size = 39 ∧ d.head = .ref (.blk q) 0 ∧ h.words q = some qa ∧
405      h' = setD (setW (setD (r.put h (rkZ z d)) ds (rkPost ds (rkMid d) a1 a2 a3)) q
406        (clearHead qa d.hash_size.toNat)) ds (lmD (rkPost ds (rkMid d) a1 a2 a3)) ∧
407      DGood h' r ds (rkZ z d) (lmD (rkPost ds (rkMid d) a1 a2 a3)) ∧ (∀ b, h'.live b ↔ h.live b) := by
408  obtain ⟨a1, a2, a3, h1, e1, rfl, s1, s2, s3, hG1, hl1⟩ := deflateResetKeep_safe hG
409  obtain ⟨q, qa, h2, e2, hq, hqa, rfl, hG2, hl2⟩ := lm_init_safe hG1
410  have hq0 : d.head = .ref (.blk q) 0 := by
411    simpa [rkPost, rkPost3, rkMid, Zlib.Trees.Proofs.Out.ibRec, Zlib.Trees.Proofs.Out.trInitRec] using hq
412  have hqa0 : h.words q = some qa := by simpa using hqa
413  have hhs : (rkPost ds (rkMid d) a1 a2 a3).hash_size = d.hash_size := by
414    simp [rkPost, rkPost3, rkMid, Zlib.Trees.Proofs.Out.ibRec, Zlib.Trees.Proofs.Out.trInitRec]
415  refine ⟨a1, a2, a3, q, qa, _, ?_, s1, s2, s3, hq0, hqa0, by rw [hhs], by simpa [hhs] using hG2, fun b => (hl2 b).trans (hl1 b)⟩
416  have hz1 := hG1.live
417  unfold deflateReset
418  rw [C.run] at e1 ⊢
419  simp only [bind_app, e1, beq_self_eq_true, ↓reduceIte, zrd_eq, hz1.hz, hz1.zst, castD, pure_app]
420  rw [C.run] at e2
421  rw [e2]
422
423/-- **deflateResetKeep, refusal.** On a stream the check refuses: `Z_STREAM_ERROR`, nothing changes. -/
424theorem deflateResetKeep_reject {h : Heap} {strm : ZStreamPtr} (hD : StreamDom h strm) (hN : ¬ DInitialised h strm) :
425    C.run (deflateResetKeep strm) h = .ok (Z_STREAM_ERROR, h) := by
426  rw [C.run, deflateResetKeep_eq]
427  exact check_refuse hD hN _ _
428
429/-- **deflateReset, refusal.** On a stream the check refuses: `Z_STREAM_ERROR`, nothing changes. -/
430theorem deflateReset_reject {h : Heap} {strm : ZStreamPtr} (hD : StreamDom h strm) (hN : ¬ DInitialised h strm) :
431    C.run (deflateReset strm) h = .ok (Z_STREAM_ERROR, h) := by
432  have e := deflateResetKeep_reject hD hN
433  unfold deflateReset
434  rw [C.run] at e ⊢
435  have hne : ¬ (Z_STREAM_ERROR = Z_OK) := by decide
436  simp [bind_app, e, hne]
437
438end Zlib.Deflate.Proofs