public-inflate-reset2.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.«inflate.c.init»
3
4open C Zlib.Inflate Zlib.Inflate.Spec Zlib.Inflate.Proofs ZlibF.Spec.Public ZlibF.Spec
5
6namespace ZlibF.Spec.Public.InflateReset2Proof
7
8theorem params_equiv (w : Int32) :
9    reset2Params w = (Api.inflWbits w.toInt).map (fun (wr, n) =>
10      ((match wr with | .raw => 0 | .zlib => 5 | .gzip => 6 | .auto => 7 : Int32), Int32.ofInt n)) := by
11  by_cases hlo : w.toInt < -15
12  · have hn : w < 0 := Int32.lt_iff_toInt_lt.mpr (by simpa using (show w.toInt < 0 by omega))
13    have h15 : w < -15 := Int32.lt_iff_toInt_lt.mpr (by simpa using hlo)
14    simp [reset2Params, hn, h15, Api.inflWbits, hlo, show w.toInt < 0 by omega]
15  · by_cases hhi : 48 ≤ w.toInt
16    · have hn : ¬ w < 0 := fun x => by have := Int32.lt_iff_toInt_lt.mp x; simp at this; omega
17      have h48 : ¬ w < 48 := fun x => by have := Int32.lt_iff_toInt_lt.mp x; simp at this; omega
18      have h16 : 15 < w := Int32.lt_iff_toInt_lt.mpr (by simpa using (show 15 < w.toInt by omega))
19      have hb : badBits w = true := by simp [badBits, h16, show w ≠ 0 by intro h; subst w; simp at hhi]
20      have hdiv0 : w.toInt / 16 ≠ 0 := by omega
21      have hdiv1 : w.toInt / 16 ≠ 1 := by omega
22      have hdiv2 : w.toInt / 16 ≠ 2 := by omega
23      simp [reset2Params, hn, h48, hb, Api.inflWbits, show ¬ w.toInt < 0 by omega, hdiv0, hdiv1, hdiv2]
24    · have hc : w.toInt = -15 ∨ w.toInt = -14 ∨ w.toInt = -13 ∨ w.toInt = -12 ∨
25        w.toInt = -11 ∨ w.toInt = -10 ∨ w.toInt = -9 ∨ w.toInt = -8 ∨
26        w.toInt = -7 ∨ w.toInt = -6 ∨ w.toInt = -5 ∨ w.toInt = -4 ∨
27        w.toInt = -3 ∨ w.toInt = -2 ∨ w.toInt = -1 ∨ w.toInt = 0 ∨
28        w.toInt = 1 ∨ w.toInt = 2 ∨ w.toInt = 3 ∨ w.toInt = 4 ∨
29        w.toInt = 5 ∨ w.toInt = 6 ∨ w.toInt = 7 ∨ w.toInt = 8 ∨
30        w.toInt = 9 ∨ w.toInt = 10 ∨ w.toInt = 11 ∨ w.toInt = 12 ∨
31        w.toInt = 13 ∨ w.toInt = 14 ∨ w.toInt = 15 ∨ w.toInt = 16 ∨
32        w.toInt = 17 ∨ w.toInt = 18 ∨ w.toInt = 19 ∨ w.toInt = 20 ∨
33        w.toInt = 21 ∨ w.toInt = 22 ∨ w.toInt = 23 ∨ w.toInt = 24 ∨
34        w.toInt = 25 ∨ w.toInt = 26 ∨ w.toInt = 27 ∨ w.toInt = 28 ∨
35        w.toInt = 29 ∨ w.toInt = 30 ∨ w.toInt = 31 ∨ w.toInt = 32 ∨
36        w.toInt = 33 ∨ w.toInt = 34 ∨ w.toInt = 35 ∨ w.toInt = 36 ∨
37        w.toInt = 37 ∨ w.toInt = 38 ∨ w.toInt = 39 ∨ w.toInt = 40 ∨
38        w.toInt = 41 ∨ w.toInt = 42 ∨ w.toInt = 43 ∨ w.toInt = 44 ∨
39        w.toInt = 45 ∨ w.toInt = 46 ∨ w.toInt = 47 := by omega
40      have hw : w = Int32.ofInt w.toInt := (Int32.ofInt_toInt w).symm
41      rcases hc with hcase | hcase | hcase | hcase | hcase | hcase | hcase | hcase |
42        hcase | hcase | hcase | hcase | hcase | hcase | hcase | hcase |
43        hcase | hcase | hcase | hcase | hcase | hcase | hcase | hcase |
44        hcase | hcase | hcase | hcase | hcase | hcase | hcase | hcase |
45        hcase | hcase | hcase | hcase | hcase | hcase | hcase | hcase |
46        hcase | hcase | hcase | hcase | hcase | hcase | hcase | hcase |
47        hcase | hcase | hcase | hcase | hcase | hcase | hcase | hcase |
48        hcase | hcase | hcase | hcase | hcase | hcase | hcase
49      all_goals rw [hcase] at hw; subst w; decide
50
51#print axioms params_equiv
52
53theorem api_bits_bound (w : Int) (wr : Api.Wrap) (n : Nat)
54    (h : Api.inflWbits w = some (wr, n)) : n ≤ 15 := by
55  unfold Api.inflWbits at h
56  repeat' split at h
57  all_goals simp_all <;> omega
58
59/-- `int inflateReset2(z_streamp strm, int windowBits)`
60The exact public result, state, frame and ownership contract. -/
61theorem reset2_public : Goal.inflateReset2 := by
62  intro h r i z s wb hv hf hwin
63  rcases hv with ⟨hz,hstate,hi,hback,ha,hfree,hlo,hhi⟩
64  have hl : Live h r i z s := ⟨hz,hi,hstate,hback,⟨hlo,hhi⟩,ha,hfree⟩
65  have hw : WindowOk h s.window := hwin
66  have hr := inflateReset2_run hl hf hw wb
67  have hp := params_equiv wb
68  cases hap : Api.inflWbits wb.toInt with
69  | none =>
70    rw [hap] at hp
71    simp only [Option.map_none] at hp
72    rw [hp] at hr
73    simpa [hap, C.run] using hr
74  | some pair =>
75    obtain ⟨wr,n⟩ := pair
76    have hn : n ≤ 15 := api_bits_bound wb.toInt wr n hap
77    have hcast : (Int32.ofInt n).toUInt32 = UInt32.ofNat n := by rfl
78    have hnat : (UInt32.ofNat n).toNat = n := by change n % 2 ^ 32 = n; exact Nat.mod_eq_of_lt (by omega)
79    have hn32 : n < 4294967296 := by omega
80    have hbiteq : (s.wbits = (Int32.ofInt n).toUInt32) ↔ s.wbits.toNat = n := by
81      rw [hcast, ← UInt32.toNat_inj, hnat]
82    rw [hap] at hp
83    simp only [Option.map_some] at hp
84    rw [hp] at hr
85    cases wr <;>
86      simp only at hr ⊢
87    all_goals
88      have hrun := hr.2
89      by_cases hb : s.wbits.toNat = n
90      · have he : s.wbits = (Int32.ofInt n).toUInt32 := hbiteq.mpr hb
91        simpa [hap, C.run, hb, he, reset2Heap, reset2Pre, resetPre, resetKeepState, resetKeepStream,
92          inflateResetState, inflateResetStream, setI, putInflate, i2u, i2ul, hcast, hn32, hnat] using hrun
93      · have he : s.wbits ≠ (Int32.ofInt n).toUInt32 := fun x => hb (hbiteq.mp x)
94        have he' : s.wbits ≠ UInt32.ofNat n := by simpa [hcast] using he
95        rcases hwin with hnull | ⟨b, a, hptr, _, _⟩
96        · simpa [hap, C.run, hb, he, hnull, reset2Heap, reset2Pre, resetPre, resetKeepState, resetKeepStream,
97            inflateResetState, inflateResetStream, setI, putInflate, i2u, i2ul, hcast, hn32, hnat, he', dropWindow, freeWin] using hrun
98        · simpa [hap, C.run, hb, he, hptr, reset2Heap, reset2Pre, resetPre, resetKeepState, resetKeepStream,
99            inflateResetState, inflateResetStream, setI, putInflate, i2u, i2ul, hcast, hn32, hnat, he', dropWindow, freeWin] using hrun
100
101#print axioms reset2_public
102
103end ZlibF.Spec.Public.InflateReset2Proof