inflate.c.misc2.lean

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

1import ZlibF.Proof.«inflate.c.misc»
2
3/-!
4# inflate.c: `inflatePrime`, `inflateGetHeader`, `inflateInit_`
5-/
6
7namespace Zlib.Inflate.Proofs
8open C Zlib.Inflate Zlib.Inflate.Spec
9
10theorem i2u_toNat {b : Int32} (h0 : 0 ≤ b.toInt) : (i2u b).toNat = b.toInt.toNat := by
11  unfold i2u
12  rw [Int32.toNat_toUInt32_of_le (by rw [Int32.le_iff_toInt_le]; simpa using h0)]
13  rfl
14
15theorem int32_pos {b : Int32} (h : 0 < b) : 0 < b.toInt := by
16  have := Int32.lt_iff_toInt_lt.mp h; simpa using this
17
18theorem int32_neg_lt {b : Int32} (h : b < 0) : b.toInt < 0 := by
19  have := Int32.lt_iff_toInt_lt.mp h; simpa using this
20
21theorem int32_gt16 {b : Int32} : 16 < b ↔ 16 < b.toInt := by
22  rw [show (16 : Int32) = Int32.ofInt 16 from rfl, Int32.lt_iff_toInt_lt, int32_ofInt_toInt 16 (by omega) (by omega)]
23
24/-- **inflatePrime, specification and safety.** On an initialised stream the call never faults and the invariants hold
25afterwards. `bits = 0`: `Z_OK`, nothing changes. `bits < 0`: `Z_OK`, the bit buffer is emptied. `bits > 16`, or more than
2632 bits in the buffer afterwards: `Z_STREAM_ERROR`, nothing changes. Otherwise `Z_OK` and the low `bits` bits of `value`
27are put above the bits already held (`primeState`). -/
28theorem inflatePrime_spec {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState}
29    (hG : Good h r zs z st) (bits value : Int32) :
30    (bits = 0 → C.run (inflatePrime (some r) bits value) h = .ok (Z_OK, h)) ∧
31    (bits < 0 → C.run (inflatePrime (some r) bits value) h = .ok (Z_OK, setI h zs { st with hold := 0, bits := 0 }) ∧
32      Good (setI h zs { st with hold := 0, bits := 0 }) r zs z { st with hold := 0, bits := 0 }) ∧
33    (0 < bits → (16 < bits.toInt ∨ 32 < st.bits.toNat + bits.toInt.toNat) →
34      C.run (inflatePrime (some r) bits value) h = .ok (Z_STREAM_ERROR, h)) ∧
35    (0 < bits → bits.toInt ≤ 16 → st.bits.toNat + bits.toInt.toNat ≤ 32 →
36      C.run (inflatePrime (some r) bits value) h = .ok (Z_OK, setI h zs (primeState bits value st)) ∧
37      Good (setI h zs (primeState bits value st)) r zs z (primeState bits value st)) := by
38  have hL := hG.live
39  have hb39 := hG.inv.bits
40  refine ⟨fun h0 => ?_, fun hn => ?_, fun hp hbad => ?_, fun hp h16 hfit => ?_⟩
41  · subst h0
42    show inflatePrime (some r) 0 value h = _
43    unfold inflatePrime; isimp [stateCheck_live hL]
44  · have h0 : bits ≠ 0 := by intro e; subst e; have := int32_neg_lt hn; simp at this
45    refine ⟨?_, good_state hG rfl hL.mode (hG.inv.of_fields rfl rfl rfl rfl rfl rfl rfl rfl rfl (by simp) rfl rfl rfl)⟩
46    show inflatePrime (some r) bits value h = _
47    unfold inflatePrime; isimp [stateCheck_live hL, hL.zst, hL.hz, hL.hs, h0, hn]
48  · have hpi := int32_pos hp
49    have h0 : bits ≠ 0 := by intro e; subst e; simp at hpi
50    have hn : ¬ bits < 0 := fun hn => by have := int32_neg_lt hn; omega
51    show inflatePrime (some r) bits value h = _
52    unfold inflatePrime
53    by_cases h16 : 16 < bits
54    · isimp [stateCheck_live hL, hL.zst, hL.hz, hL.hs, h0, hn, h16]
55    · have h16'' : ¬ 16 < bits.toInt := fun hh => h16 (int32_gt16.mpr hh)
56      have h16' : bits.toInt ≤ 16 := by omega
57      have hgt : 32 < st.bits + i2u bits := by
58        rw [UInt32.lt_iff_toNat_lt, UInt32.toNat_add, i2u_toNat (by omega), Nat.mod_eq_of_lt (by omega)]
59        have : (32 : UInt32).toNat = 32 := rfl
60        omega
61      isimp [stateCheck_live hL, hL.zst, hL.hz, hL.hs, h0, hn, h16, hgt]
62  · have hpi := int32_pos hp
63    have h0 : bits ≠ 0 := by intro e; subst e; simp at hpi
64    have hn : ¬ bits < 0 := fun hn => by have := int32_neg_lt hn; omega
65    have h16 : ¬ 16 < bits := fun hh => by have := int32_gt16.mp hh; omega
66    have hu := i2u_toNat (b := bits) (by omega)
67    have hgt : ¬ 32 < st.bits + i2u bits := by
68      rw [UInt32.lt_iff_toNat_lt, UInt32.toNat_add, hu, Nat.mod_eq_of_lt (by omega)]
69      have : (32 : UInt32).toNat = 32 := rfl
70      omega
71    have hlt : st.bits < 64 := by rw [UInt32.lt_iff_toNat_lt]; have : (64 : UInt32).toNat = 64 := rfl; omega
72    have hrun : inflatePrime (some r) bits value h = .ok (Z_OK, setI h zs (primeState bits value st)) := by
73      unfold inflatePrime
74      isimp [stateCheck_live hL, hL.zst, hL.hz, hL.hs, h0, hn, h16, hgt, shl64, hlt, primeState, primeBits]
75    refine ⟨hrun, good_state hG rfl hL.mode ?_⟩
76    have hsum : (st.bits + i2u bits).toNat = st.bits.toNat + bits.toInt.toNat := by
77      rw [UInt32.toNat_add, hu, Nat.mod_eq_of_lt (by omega)]
78    exact hG.inv.of_fields rfl rfl rfl rfl rfl rfl rfl rfl rfl (by show (st.bits + i2u bits).toNat ≤ 39; omega) rfl rfl rfl
79
80end Zlib.Inflate.Proofs