public-deflate-reset-keep.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.DeflateResetKeepProof
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
17/-- `int deflateResetKeep(z_streamp strm)`; reset progress while retaining the match history.
18The exact public result, state, frame and ownership contract. -/
19theorem deflate_resetkeep_public : Goal.deflateResetKeep := by
20  intro h r i z s hG
21  obtain ⟨a1,a2,a3,after,hr,he,ha1,ha2,ha3,hgood,hlive⟩ := deflateResetKeep_safe hG
22  let z' := rkZ z s
23  let s' := rkPost i (rkMid s) a1 a2 a3
24  refine ⟨after,z',s',hr,hgood,?_⟩
25  have hw := abswrap_properties s hG.inv.wrap_lo hG.inv.wrap_hi
26  have hadler : (if absWrap s.wrap = 2 then (0 : UInt64) else 1) =
27      if s.wrap = 2 ∨ s.wrap = -2 then 0 else 1 := by simpa using hw.2
28  have hbytes : after.bytes = h.bytes := by rw [he]; simp
29  have hwords : after.words = h.words := by rw [he]; simp
30  have hnalloc : after.nalloc = h.nalloc := by rw [he]; simp
31  have hframe : Frame h after (fun b => StreamRoot r b ∨ DeflateOwned i s b) := by
32    rw [he]
33    cases r with
34    | tab j =>
35      have hj : h.streams j = some z := hG.live.hz
36      simp only [Frame, setD, ZStreamRef.put, hj, true_and]
37      refine ⟨Nat.le_refl _, Nat.le_refl _, ?_⟩
38      intro b hb hn
39      have hi : b ≠ i := fun e => hn (Or.inr (Or.inl e))
40      have hj : b ≠ j := fun e => hn (Or.inl (by simpa [StreamRoot] using e))
41      simp [upd_ne, hi, hj]
42    | in_gzstate_strm j =>
43      cases hj : h.gzstates j with
44      | none =>
45        have hz := hG.live.hz
46        simp [ZStreamRef.get, hj] at hz
47      | some g =>
48        simp only [Frame, setD, ZStreamRef.put, hj, true_and]
49        refine ⟨Nat.le_refl _, Nat.le_refl _, ?_⟩
50        intro b hb hn
51        have hi : b ≠ i := fun e => hn (Or.inr (Or.inl e))
52        have hj : b ≠ j := fun e => hn (Or.inl (by simpa [StreamRoot] using e))
53        simp [upd_ne, hi, hj]
54  simp [z', s', rkZ, rkPost, rkPost3, rkMid,
55    Zlib.Trees.Proofs.Out.ibRec, Zlib.Trees.Proofs.Out.trInitRec,
56    hw.1, hadler, hbytes, hwords, hnalloc, hframe, LiveChange, hlive]
57
58#print axioms deflate_resetkeep_public
59
60end ZlibF.Spec.Public.DeflateResetKeepProof