inflate.c.misc.lean

本页保留 Lean 源码及行号。点击行号可定位语句，点击 import 中的模块名可查看依赖。

1import ZlibF.Proof.«inflate.c.start»
2
3/-!
4# inflate.c: `inflatePrime`, `inflateValidate`, `inflateUndermine`, `inflateMark`, `inflateCodesUsed`,
5`inflateSyncPoint`, `inflateGetHeader`, `inflateInit_`
6
7The integer lemmas (`mark_hi`, `u32_i64`) come from the earlier development, restated for these definitions.
8-/
9
10namespace Zlib.Inflate.Spec
11open C
12
13/-- `inflateValidate`: the wrapper bit 4 (check) is set or cleared in `wrap` and `reqwrap`. -/
14def validateState (check : Int32) (st : InflateState) : InflateState :=
15  { st with
16    wrap := if check != 0 && st.wrap != 0 then st.wrap ||| 4 else st.wrap &&& ~~~4,
17    reqwrap := if check != 0 && st.reqwrap != 0 then st.reqwrap ||| 4 else st.reqwrap &&& ~~~4 }
18
19/-- `inflatePrime`: the `bits` low bits of `value`, as `(unsigned long)(value & ((1L << bits) - 1))`. -/
20def primeBits (bits value : Int32) : UInt64 :=
21  Zlib.Inflate.i2ul ((value.toInt64 &&& (((1 : Int64) <<< bits.toInt64) - 1)).toInt32)
22
23/-- The state after `inflatePrime` inserted `bits` bits (`1 ≤ bits ≤ 16`, they fit): `hold += value << bits_in_hold`. -/
24def primeState (bits value : Int32) (st : InflateState) : InflateState :=
25  { st with hold := st.hold + (primeBits bits value <<< st.bits.toUInt64), bits := st.bits + Zlib.Inflate.i2u bits }
26
27/-- The value `inflateMark` returns: `back << 16` plus the number of bytes of the current copy or match so far. -/
28def markValue (st : InflateState) : Int :=
29  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)
30
31end Zlib.Inflate.Spec
32
33namespace Zlib.Inflate.Proofs
34open C Zlib.Inflate Zlib.Inflate.Spec
35
36theorem mark_hi (b : Int32) :
37    ((b.toInt64.toUInt64 <<< (16 : UInt64)).toInt64).toInt = b.toInt * 65536 := by
38  have hb1 := b.le_toInt
39  have hb2 := b.toInt_lt
40  have : (b.toInt64.toUInt64 <<< (16 : UInt64)).toInt64 = b.toInt64 * 65536 := by
41    apply Int64.toBitVec_inj.mp
42    rw [UInt64.toBitVec_toInt64, UInt64.toBitVec_shiftLeft, Int64.toBitVec_mul, BitVec.shiftLeft_eq',
43      BitVec.shiftLeft_eq_mul_twoPow]
44    have e1 : ((16 : UInt64).toBitVec % 64).toNat = 16 := rfl
45    rw [e1]
46    have e2 : BitVec.twoPow 64 16 = (65536 : Int64).toBitVec := by decide
47    rw [e2]
48    rfl
49  rw [this, Int64.toInt_mul]
50  simp only [Int32.toInt_toInt64]
51  rw [Int.bmod_eq_iff (by decide)]
52  have e3 : (65536 : Int64).toInt = 65536 := by decide
53  have e4 : ((2 ^ 64 : Nat) : Int) = 18446744073709551616 := rfl
54  rw [e3, e4]
55  refine ⟨by omega, by omega, by simp⟩
56
57theorem u32_i64 (x : UInt32) : (x.toUInt64.toInt64).toInt = x.toNat := by
58  have := x.toNat_lt
59  rw [Int64.toInt, UInt64.toBitVec_toInt64, BitVec.toInt_eq_toNat_of_lt]
60  · simp
61  · simp; omega
62
63theorem ZStreamRef.put_self {h : Heap} {r : ZStreamRef} {z : ZStream} (e : r.get h = some z) : r.put h z = h := by
64  cases r with
65  | tab i =>
66    simp only [ZStreamRef.get] at e
67    simp [ZStreamRef.put, e, upd_self _ _ _ e]
68  | in_gzstate_strm i =>
69    simp only [ZStreamRef.get] at e
70    obtain ⟨g, hg, hgz⟩ := Option.map_eq_some_iff.mp e
71    subst hgz
72    simp [ZStreamRef.put, hg, upd_self _ _ _ hg]
73
74theorem _root_.Zlib.Inflate.Spec.StInv.of_fields {h : Heap} {zs : Nat} {st st' : InflateState} (hI : StInv h zs st)
75    (l : st'.lens = st.lens) (w : st'.work = st.work) (c : st'.codes = st.codes)
76    (a : st'.wbits = st.wbits) (b : st'.window = st.window) (c1 : st'.wsize = st.wsize) (d : st'.whave = st.whave)
77    (e : st'.wnext = st.wnext) (f : st'.reqbits = st.reqbits) (g : st'.bits.toNat ≤ 39) (n : st'.next = st.next)
78    (lc : st'.lencode = st.lencode) (dc : st'.distcode = st.distcode) : StInv h zs st' := by
79  obtain ⟨⟨w1, w2, w3⟩, hw, hq, hb, ⟨hn, hp⟩⟩ := hI
80  refine ⟨⟨by rw [l]; exact w1, by rw [w]; exact w2, by rw [c]; exact w3⟩,
81    ⟨by rw [a]; exact hw.wbits, by rw [a, b]; exact hw.block, by rw [b, c1]; exact hw.nullws,
82      by rw [a, c1]; exact hw.ws, by rw [c1, d]; exact hw.hv, by rw [c1, e]; exact hw.wn, by rw [c1, d, e]; exact hw.eq⟩,
83    by rw [f]; exact hq, g, by unfold PtrInv; rw [n, lc, dc]; exact ⟨hn, hp⟩⟩
84
85theorem good_state {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState}
86    (hG : Good h r zs z st) {st' : InflateState} (hs : st'.strm = st.strm)
87    (hm : HEAD ≤ st'.mode ∧ st'.mode ≤ SYNC) (hI : StInv h zs st') : Good (setI h zs st') r zs z st' := by
88  have := hG.setZI (z' := z) rfl hG.live.zalloc hG.live.zfree hs hm hI
89  rwa [ZStreamRef.put_self hG.live.hz] at this
90
91/-! ### inflateValidate, inflateUndermine, inflateSyncPoint -/
92
93/-- **inflateValidate, safety.** On an initialised stream the call returns `Z_OK`, changes only `wrap` and `reqwrap`
94(`validateState`) and keeps the invariants. -/
95theorem inflateValidate_safe {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState}
96    (hG : Good h r zs z st) (check : Int32) :
97    ∃ h', C.run (inflateValidate (some r) check) h = .ok (Z_OK, h') ∧ h' = setI h zs (validateState check st) ∧
98      Good h' r zs z (validateState check st) ∧ (∀ b, h'.live b ↔ h.live b) := by
99  have hL := hG.live
100  have hrun : inflateValidate (some r) check h = .ok (Z_OK, setI h zs (validateState check st)) := by
101    unfold inflateValidate
102    isimp [stateCheck_live hL, hL.zst, hL.hz, hL.hs, validateState]
103  refine ⟨_, hrun, rfl, good_state hG (by simp [validateState]) (by simpa [validateState] using hL.mode)
104    (hG.inv.of_fields rfl rfl rfl rfl rfl rfl rfl rfl rfl hG.inv.bits rfl rfl rfl), ?_⟩
105  exact fun b => (shape_setI hL.hs _).live b
106
107/-- **inflateUndermine, safety.** The call (without `INFLATE_ALLOW_INVALID_DISTANCE_TOOFAR_ARRR`) sets `sane` to 1 and
108returns `Z_DATA_ERROR`. -/
109theorem inflateUndermine_safe {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState}
110    (hG : Good h r zs z st) (subvert : Int32) :
111    ∃ h', C.run (inflateUndermine (some r) subvert) h = .ok (Z_DATA_ERROR, h') ∧
112      h' = setI h zs { st with sane := 1 } ∧ Good h' r zs z { st with sane := 1 } := by
113  have hL := hG.live
114  refine ⟨_, ?_, rfl, good_state hG rfl hL.mode (hG.inv.of_fields rfl rfl rfl rfl rfl rfl rfl rfl rfl hG.inv.bits rfl rfl rfl)⟩
115  show inflateUndermine (some r) subvert h = _
116  unfold inflateUndermine
117  isimp [stateCheck_live hL, hL.zst, hL.hz, hL.hs]
118
119/-- **inflateSyncPoint, specification.** Returns 1 exactly when the mode is `STORED` and the bit buffer is empty;
120nothing changes. -/
121theorem inflateSyncPoint_spec {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState}
122    (hL : Live h r zs z st) :
123    C.run (inflateSyncPoint (some r)) h = .ok ((if st.mode = STORED ∧ st.bits = 0 then 1 else 0), h) := by
124  show inflateSyncPoint (some r) h = _
125  unfold inflateSyncPoint
126  by_cases hc : st.mode = STORED ∧ st.bits = 0
127  · isimp [stateCheck_live hL, hL.zst, hL.hz, hL.hs, hc.1, hc.2]
128  · have : ¬ (st.mode = STORED ∧ st.bits = 0) := hc
129    isimp [stateCheck_live hL, hL.zst, hL.hz, hL.hs]
130
131theorem ofInt_toUInt64 (i : Nat) : (Int64.ofInt (i : Int)).toUInt64 = UInt64.ofNat i := by
132  apply UInt64.toBitVec_inj.mp
133  simp [Int64.toBitVec_ofInt]
134  rfl
135
136/-! ### inflateMark, inflateCodesUsed -/
137
138/-- **inflateMark, specification.** The call returns `markValue st` (`back << 16` plus the length so far of a copy
139or match) without a fault: no `long` overflow is possible. The heap is unchanged. -/
140theorem inflateMark_spec {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState}
141    (hL : Live h r zs z st) :
142    ∃ v, C.run (inflateMark (some r)) h = .ok (v, h) ∧ v.toInt = markValue st := by
143  have hb1 := st.back.le_toInt
144  have hb2 := st.back.toInt_lt
145  have hl := st.length.toNat_lt
146  have hw := (st.was - st.length).toNat_lt
147  have key : ∀ lo : UInt32, ∃ v, (do
148      let hi : Int64 := ((st.back.toInt64.toUInt64) <<< 16).toInt64
149      chkI64 (hi.toInt + lo.toNat) : M Int64) h = .ok (v, h) ∧ v.toInt = st.back.toInt * 65536 + lo.toNat := by
150    intro lo
151    have hlo := lo.toNat_lt
152    have hm := mark_hi st.back
153    have hr : -9223372036854775808 ≤ st.back.toInt * 65536 + (lo.toNat : Int) ∧
154        st.back.toInt * 65536 + (lo.toNat : Int) < 9223372036854775808 := by omega
155    refine ⟨Int64.ofInt (st.back.toInt * 65536 + lo.toNat), ?_, ?_⟩
156    · simp only [bind_app, pure_app]
157      have : (((st.back.toInt64.toUInt64) <<< 16).toInt64).toInt = st.back.toInt * 65536 := mark_hi st.back
158      simp [chkI64, this, hr.1, hr.2]
159    · rw [Int64.toInt_ofInt_of_le (by omega) (by omega)]
160  have hrun : inflateMark (some r) h = (do
161      let hi : Int64 := ((st.back.toInt64.toUInt64) <<< 16).toInt64
162      let lo : UInt32 := if st.mode = COPY then st.length else if st.mode = MATCH then st.was - st.length else 0
163      chkI64 (hi.toInt + lo.toNat) : M Int64) h := by
164    unfold inflateMark
165    isimp [stateCheck_live hL, hL.zst, hL.hz, hL.hs]
166  rw [C.run, hrun]
167  obtain ⟨v, hv, hv2⟩ := key (if st.mode = COPY then st.length else if st.mode = MATCH then st.was - st.length else 0)
168  refine ⟨v, ?_, ?_⟩
169  · simpa using hv
170  · rw [hv2]; unfold markValue
171    by_cases c1 : st.mode = COPY
172    · simp [c1]
173    · have hne : (MATCH : UInt32) ≠ COPY := by decide
174      by_cases c2 : st.mode = MATCH
175      · simp [c1, c2, hne]
176      · simp [c1, c2]
177
178/-- **inflateCodesUsed, specification.** For an initialised stream the call returns the offset of `next` in `codes`
179(at most 1444) without a fault; nothing changes. -/
180theorem inflateCodesUsed_spec {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState}
181    (hG : Good h r zs z st) :
182    ∃ i, i ≤ 1444 ∧ st.next = .ref (.istate_codes zs) i ∧
183      C.run (inflateCodesUsed (some r)) h = .ok (UInt64.ofNat i, h) := by
184  have hL := hG.live
185  obtain ⟨i, hi, hi2⟩ := hG.inv.ptr.1
186  refine ⟨i, hi2, hi, ?_⟩
187  have hc : Space.get h (CodeRef.istate_codes zs) = some st.codes := by simp [Space.get, hL.hs]
188  have hsz : st.codes.size = 1444 := hG.inv.wf.2.2
189  have hd : OkOn h (Ptr.diff (Ptr.ref (CodeRef.istate_codes zs) i) (Ptr.ref (CodeRef.istate_codes zs) 0))
190      (Int64.ofInt ((i : Int) - (0 : Nat))) :=
191    Ptr.diff_ok hc (by omega) (by omega) (by omega)
192  have hd' : Ptr.diff (Ptr.ref (CodeRef.istate_codes zs) i) (Ptr.ref (CodeRef.istate_codes zs) 0) h =
193      .ok (Int64.ofInt ((i : Int) - (0 : Nat)), h) := hd
194  rw [C.run]
195  unfold inflateCodesUsed
196  isimp [stateCheck_live hL, hL.zst, hL.hz, hL.hs, hi, codesP, hd']
197  simp [ofInt_toUInt64]
198
199end Zlib.Inflate.Proofs