public-deflate-reset.lean

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

1import ZlibF.Spec.Public.Lifecycle
2import ZlibF.Proof.«deflate.c.life.reset»
3
4open C Zlib.Deflate Zlib.Deflate.Spec Zlib.Deflate.Proofs ZlibF.Spec.Public
5
6namespace ZlibF.Spec.Public.DeflateResetProof
7
8private theorem abswrap_properties (d : DeflateState) (hlo : -2 ≤ d.wrap.toInt) (hhi : d.wrap.toInt ≤ 2) :
9    (absWrap d.wrap).toInt = d.wrap.toInt.natAbs ∧
10    (if absWrap d.wrap == 2 then (0 : UInt64) else 1) =
11      if d.wrap = 2 ∨ d.wrap = -2 then 0 else 1 := by
12  have hc : d.wrap.toInt = -2 ∨ d.wrap.toInt = -1 ∨ d.wrap.toInt = 0 ∨ d.wrap.toInt = 1 ∨ d.wrap.toInt = 2 := by omega
13  have he : d.wrap = Int32.ofInt d.wrap.toInt := (Int32.ofInt_toInt d.wrap).symm
14  rcases hc with hh | hh | hh | hh | hh <;> rw [hh] at he <;>
15    simp [absWrap, he]
16
17private theorem local_fillRange_succ {T : Type} (d : Array T) (off n : Nat) (v : T) :
18    fillRange d off (n + 1) v = (fillRange d off n v).set! (off + n) v := by
19  unfold fillRange; rw [List.range_succ, List.foldl_append]; rfl
20
21
22private theorem local_getElem_fillRange {T : Type} (d : Array T) (off n : Nat) (v : T) (i : Nat) (hfit : off + n ≤ d.size) :
23    (fillRange d off n v)[i]? = if off ≤ i ∧ i < off + n then some v else d[i]? := by
24  induction n generalizing i with
25  | zero => simp [fillRange]; intro h1 h2; omega
26  | succ n ih =>
27    rw [local_fillRange_succ, Array.set!_eq_setIfInBounds, Array.getElem?_setIfInBounds, ih i (by omega)]
28    have hs : (fillRange d off n v).size = d.size := size_fillRange _ _ _ _
29    by_cases hi : off + n = i
30    · subst hi
31      simp [hs, show off + n < d.size by omega]
32    · simp [hi]
33      by_cases h1 : off ≤ i ∧ i < off + n
34      · simp [h1]; omega
35      · simp [h1]; intro _ ; omega
36
37
38private theorem clear_head_get (qa : Array UInt16) (n : Nat) (hn : 1 ≤ n) (hs : n ≤ qa.size)
39    (j : Nat) (hj : j < n) : (clearHead qa n)[j]? = some 0 := by
40  have hf : 0 + (n - 1) ≤ (qa.set! (n - 1) 0).size := by simp; omega
41  have he := local_getElem_fillRange (qa.set! (n - 1) 0) 0 (n - 1) (0 : UInt16) j hf
42  unfold clearHead
43  rw [he]
44  by_cases hp : j < n - 1
45  · simp [hp]
46  · have hx : j = n - 1 := by omega
47    subst j
48    simp [Array.set!_eq_setIfInBounds, show n - 1 < qa.size by omega]
49
50/-- `int deflateReset(z_streamp strm)`; reset progress and clear the dictionary hash.
51The exact public result, state, frame and ownership contract. -/
52theorem deflate_reset_public : Goal.deflateReset := by
53  intro h r i z s hG
54  obtain ⟨a1,a2,a3,q,qa,after,hr,ha1,ha2,ha3,hq,hqa,he,hgood,hlive⟩ := deflateReset_safe hG
55  let z' := rkZ z s
56  let s' := lmD (rkPost i (rkMid s) a1 a2 a3)
57  refine ⟨after,z',s',hr,hgood,?_⟩
58  have hw := abswrap_properties s hG.inv.wrap_lo hG.inv.wrap_hi
59  have hadler : (if absWrap s.wrap = 2 then (0 : UInt64) else 1) =
60      if s.wrap = 2 ∨ s.wrap = -2 then 0 else 1 := by simpa using hw.2
61  have hbytes : after.bytes = h.bytes := by rw [he]; simp [setW]
62  have hnalloc : after.nalloc = h.nalloc := by rw [he]; simp [setW]
63  have hhashpos : 1 ≤ s.hash_size.toNat := by
64    rw [hG.inv.hsize]
65    exact Nat.one_le_pow _ _ (by decide)
66  obtain ⟨w,p,q',b,hB⟩ := hG.inv.blocks
67  have hqq : q = q' := by
68    have hh := hB.head
69    rw [hq] at hh
70    cases hh
71    rfl
72  subst q'
73  obtain ⟨qa',hqa',hsize⟩ := hB.qa
74  have haeq : qa = qa' := Option.some.inj (hqa.symm.trans hqa')
75  have hbound : s.hash_size.toNat ≤ qa.size := by rw [haeq, hsize]; exact Nat.le_refl _
76  have hzero : ∀ ref off a, s.head = .ref ref off → Space.get after ref = some a →
77      ∀ j, j < s.hash_size.toNat → a[off+j]? = some 0 := by
78    intro ref off a hptr hget j hj
79    rw [hq] at hptr
80    cases hptr
81    have hget' : after.words q = some a := by simpa [Space.get] using hget
82    have hz : after.words q = some (clearHead qa s.hash_size.toNat) := by
83      rw [he]
84      simp [setW]
85    have : a = clearHead qa s.hash_size.toNat := Option.some.inj (hget'.symm.trans hz)
86    subst a
87    simpa using clear_head_get qa s.hash_size.toNat hhashpos hbound j hj
88  have hframe : Frame h after (fun b => StreamRoot r b ∨ DeflateOwned i s b) := by
89    rw [he]
90    cases r with
91    | tab k =>
92      have hk : h.streams k = some z := hG.live.hz
93      simp only [Frame, setD, setW, ZStreamRef.put, hk, true_and]
94      refine ⟨Nat.le_refl _, Nat.le_refl _, ?_⟩
95      intro x hx hn
96      have hi : x ≠ i := fun e => hn (Or.inr (Or.inl e))
97      have hk : x ≠ k := fun e => hn (Or.inl (by simpa [StreamRoot] using e))
98      have hq' : x ≠ q := fun e => hn (Or.inr (Or.inr (Or.inr (Or.inr (Or.inl (by simpa [hq] using e.symm))))))
99      simp [upd_ne, hi, hk, hq']
100    | in_gzstate_strm k =>
101      cases hk : h.gzstates k with
102      | none =>
103        have hz := hG.live.hz
104        simp [ZStreamRef.get, hk] at hz
105      | some g =>
106        simp only [Frame, setD, setW, ZStreamRef.put, hk, true_and]
107        refine ⟨Nat.le_refl _, Nat.le_refl _, ?_⟩
108        intro x hx hn
109        have hi : x ≠ i := fun e => hn (Or.inr (Or.inl e))
110        have hk : x ≠ k := fun e => hn (Or.inl (by simpa [StreamRoot] using e))
111        have hq' : x ≠ q := fun e => hn (Or.inr (Or.inr (Or.inr (Or.inr (Or.inl (by simpa [hq] using e.symm))))))
112        simp [upd_ne, hi, hk, hq']
113  simp [z', s', rkZ, lmD, rkPost, rkPost3, rkMid,
114    Zlib.Trees.Proofs.Out.ibRec, Zlib.Trees.Proofs.Out.trInitRec,
115    hw.1, hadler, hbytes, hnalloc, hframe, LiveChange, hlive]
116  exact hzero
117
118#print axioms deflate_reset_public
119
120end ZlibF.Spec.Public.DeflateResetProof