public-inflate-mark.lean

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

1import ZlibF.Proof.«public-inflate-small-queries»
2
3namespace ZlibF.Spec.Public.InflateMarkProof
4open C Zlib.Inflate Zlib.Inflate.Spec Zlib.Inflate.Proofs ZlibF.Spec.Public.InflateQueryProof
5
6def markValue (st : InflateState) : Int :=
7  st.back.toInt * 65536 + (if st.mode = COPY then st.length.toNat else if st.mode = MATCH then (st.was - st.length).toNat else 0)
8
9
10theorem mark_hi (b : Int32) :
11    ((b.toInt64.toUInt64 <<< (16 : UInt64)).toInt64).toInt = b.toInt * 65536 := by
12  have hb1 := b.le_toInt
13  have hb2 := b.toInt_lt
14  have : (b.toInt64.toUInt64 <<< (16 : UInt64)).toInt64 = b.toInt64 * 65536 := by
15    apply Int64.toBitVec_inj.mp
16    rw [UInt64.toBitVec_toInt64, UInt64.toBitVec_shiftLeft, Int64.toBitVec_mul, BitVec.shiftLeft_eq',
17      BitVec.shiftLeft_eq_mul_twoPow]
18    have e1 : ((16 : UInt64).toBitVec % 64).toNat = 16 := rfl
19    rw [e1]
20    have e2 : BitVec.twoPow 64 16 = (65536 : Int64).toBitVec := by decide
21    rw [e2]
22    rfl
23  rw [this, Int64.toInt_mul]
24  simp only [Int32.toInt_toInt64]
25  rw [Int.bmod_eq_iff (by decide)]
26  have e3 : (65536 : Int64).toInt = 65536 := by decide
27  have e4 : ((2 ^ 64 : Nat) : Int) = 18446744073709551616 := rfl
28  rw [e3, e4]
29  refine ⟨by omega, by omega, by simp⟩
30
31theorem inflateMark_spec {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState}
32    (hL : Live h r zs z st) :
33    ∃ v, C.run (inflateMark (some r)) h = .ok (v, h) ∧ v.toInt = markValue st := by
34  have hb1 := st.back.le_toInt
35  have hb2 := st.back.toInt_lt
36  have hl := st.length.toNat_lt
37  have hw := (st.was - st.length).toNat_lt
38  have key : ∀ lo : UInt32, ∃ v, (do
39      let hi : Int64 := ((st.back.toInt64.toUInt64) <<< 16).toInt64
40      chkI64 (hi.toInt + lo.toNat) : M Int64) h = .ok (v, h) ∧ v.toInt = st.back.toInt * 65536 + lo.toNat := by
41    intro lo
42    have hlo := lo.toNat_lt
43    have hm := mark_hi st.back
44    have hr : -9223372036854775808 ≤ st.back.toInt * 65536 + (lo.toNat : Int) ∧
45        st.back.toInt * 65536 + (lo.toNat : Int) < 9223372036854775808 := by omega
46    refine ⟨Int64.ofInt (st.back.toInt * 65536 + lo.toNat), ?_, ?_⟩
47    · simp only [bind_app, pure_app]
48      have : (((st.back.toInt64.toUInt64) <<< 16).toInt64).toInt = st.back.toInt * 65536 := mark_hi st.back
49      simp [chkI64, this, hr.1, hr.2]
50    · rw [Int64.toInt_ofInt_of_le (by omega) (by omega)]
51  have hrun : inflateMark (some r) h = (do
52      let hi : Int64 := ((st.back.toInt64.toUInt64) <<< 16).toInt64
53      let lo : UInt32 := if st.mode = COPY then st.length else if st.mode = MATCH then st.was - st.length else 0
54      chkI64 (hi.toInt + lo.toNat) : M Int64) h := by
55    unfold inflateMark
56    isimp [stateCheck_live hL, hL.zst, hL.hz, hL.hs]
57  rw [C.run, hrun]
58  obtain ⟨v, hv, hv2⟩ := key (if st.mode = COPY then st.length else if st.mode = MATCH then st.was - st.length else 0)
59  refine ⟨v, ?_, ?_⟩
60  · simpa using hv
61  · rw [hv2]; unfold markValue
62    by_cases c1 : st.mode = COPY
63    · simp [c1]
64    · have hne : (MATCH : UInt32) ≠ COPY := by decide
65      by_cases c2 : st.mode = MATCH
66      · simp [c1, c2, hne]
67      · simp [c1, c2]
68
69
70/-- `long inflateMark(z_streamp strm)` returns the exact copy or match position. -/
71theorem mark_public : Goal.inflateMark := by
72  constructor
73  · intro h p hr
74    show inflateMark p h = _
75    unfold inflateMark
76    simp [bind_app, notInit_check (refused_dom hr) (refused_not_initialised hr), pure_app]
77    decide
78  · intro h r i z s hv
79    rcases hv with ⟨hz, hstate, hi, hb, ha, hf, hlo, hhi⟩
80    have hl : Live h r i z s := ⟨hz, hi, hstate, hb, ⟨hlo, hhi⟩, ha, hf⟩
81    obtain ⟨v, hv, he⟩ := inflateMark_spec hl
82    simp only [markValue] at he
83    rw [← he, Int64.ofInt_toInt]
84    exact hv
85
86#print axioms mark_public
87end ZlibF.Spec.Public.InflateMarkProof