deflate.c.engine.lmbody.lean

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

1import ZlibF.Proof.«deflate.c.engine.lminner»
2import ZlibF.Proof.«deflate.c.engine.chains»
3import ZlibF.Proof.«deflate.c.engine.window»
4
5/-!
6# deflate.c, engine: one candidate of `longest_match`
7
8The loop of `longest_match` visits the candidates on the hash chain. This module defines the environment (the
9window block, the `prev` block, the size and position facts), the loop invariant `LMInv`, and proves that one
10execution of the body `lm_body` does not fault and keeps the invariant.
11
12**Environment.** The window block holds at least `2 * w_size` bytes and `strstart <= window_size - 262`; `prev` holds
13`w_size` words; the first candidate `c` satisfies `1 <= c < strstart` and `strstart - c <= MAX_DIST`; every position
14on the chain from `c` (while above `limit`) is in `[1, strstart)`, its `prev` entry is smaller, and it agrees with
15`strstart` in the third byte whenever it agrees in the first two (this is what H gives after `INSERT_STRING`).
16
17**Invariant.** `best_len` is `b` with `prev_length <= b <= 258`; `scan_end1` and `scan_end` are the window bytes
18`strstart + b - 1` and `strstart + b`; `cur_match` lies on the chain; and either nothing has been found
19(`b = prev_length`, `match_start` unchanged) or `match_start` names a good match of length `b`.
20-/
21
22namespace Zlib.Deflate.Engine.Proofs
23open C Zlib.Deflate
24
25/-- A good match: before `ss`, within `MAX_DIST`, of length at most 258, and the bytes agree. -/
26def GoodMatch (wa : Array UInt8) (ss ws m len : Nat) : Prop :=
27  m < ss ∧ ss - m ≤ ws - 262 ∧ len ≤ 258 ∧ ∀ j, j < len → bfn wa (m + j) = bfn wa (ss + j)
28
29/-- The heap once `match_start` of the state record `sr` was set to `ms`. -/
30def hAt (h0 : Heap) (sr : Nat) (d : DeflateState) (ms : UInt32) : Heap :=
31  { h0 with dstates := upd h0.dstates sr (some { d with match_start := ms }) }
32
33structure LMEnv (h0 : Heap) (sr : Nat) (d : DeflateState) (wb pb : Nat) (wa : Array UInt8) (pa : Array UInt16)
34    (c : UInt32) : Prop where
35  hd : h0.dstates sr = some d
36  win : d.window = .ref (.blk wb) 0
37  wbytes : h0.bytes wb = some wa
38  prevp : d.prev = .ref (.blk pb) 0
39  pwords : h0.words pb = some pa
40  wsb : ∃ b, d.w_size.toNat = 2 ^ b ∧ 9 ≤ b ∧ b ≤ 15
41  wmask : d.w_mask = d.w_size - 1
42  psize : d.w_size.toNat ≤ pa.size
43  asize : 2 * d.w_size.toNat ≤ wa.size
44  room : d.strstart.toNat + 262 ≤ 2 * d.w_size.toNat
45  lale : d.lookahead.toNat ≤ 2 * d.w_size.toNat
46  plle : d.prev_length.toNat ≤ 258
47  c1 : 1 ≤ c.toNat
48  clt : c.toNat < d.strstart.toNat
49  cdist : d.strstart.toNat - c.toNat ≤ d.w_size.toNat - 262
50  chain : ∀ p, Chain (wfn pa) (d.w_size.toNat - 1) (lmLimit d.strstart.toNat (d.w_size.toNat - 262)) c.toNat p →
51    1 ≤ p ∧ p < d.strstart.toNat ∧ (wfn pa (p &&& (d.w_size.toNat - 1))).toNat < p ∧
52    (bfn wa p = bfn wa d.strstart.toNat → bfn wa (p + 1) = bfn wa (d.strstart.toNat + 1) →
53      bfn wa (p + 2) = bfn wa (d.strstart.toNat + 2))
54
55def LMInv (h0 : Heap) (sr : Nat) (d : DeflateState) (wb pb : Nat) (wa : Array UInt8) (pa : Array UInt16)
56    (c : UInt32) (st : LMState) (h : Heap) : Prop :=
57  ∃ (ms : UInt32) (b : Nat), h = hAt h0 sr d ms ∧
58    st.scan = .ref (.blk wb) d.strstart.toNat ∧ st.best_len.toInt = (b : Int) ∧ d.prev_length.toNat ≤ b ∧ b ≤ 258 ∧
59    (st.brk = false → st.scan_end1 = bfn wa (d.strstart.toNat + b - 1) ∧ st.scan_end = bfn wa (d.strstart.toNat + b)) ∧
60    Chain (wfn pa) (d.w_size.toNat - 1) (lmLimit d.strstart.toNat (d.w_size.toNat - 262)) c.toNat st.cur_match.toNat ∧
61    ((b = d.prev_length.toNat ∧ ms = d.match_start) ∨
62     (d.prev_length.toNat < b ∧ GoodMatch wa d.strstart.toNat d.w_size.toNat ms.toNat b))
63
64/-! ## Integer helpers -/
65
66theorem isub_ok (a b : Int32) (hr : -2147483648 ≤ a.toInt - b.toInt ∧ a.toInt - b.toInt ≤ 2147483647) :
67    ∀ h, isub a b h = .ok (Int32.ofInt (a.toInt - b.toInt), h) := by
68  intro h
69  simp [isub, chk32, hr]
70
71theorem getElem_bfn (a : Array UInt8) (j : Nat) (hj : j < a.size) : a[j] = bfn a j := by
72  simp [bfn, Array.getD_eq_getD_getElem?, hj]
73
74theorem load8_bfn {h : Heap} {wb : Nat} {wa : Array UInt8} (hb : h.bytes wb = some wa) {i : Nat}
75    (hi : i < wa.size) : load8 (.ref (.blk wb) i) h = .ok (bfn wa i, h) := by
76  have g : Space.get h (BRef.blk wb) = some wa := by simpa using hb
77  have := Ptr.load_ok (h := h) (r := BRef.blk wb) (a := wa) (off := i) g hi
78  unfold OkOn at this
79  show (Ptr.ref (BRef.blk wb) i).load h = _
80  rw [this, getElem_bfn _ _ hi]
81
82theorem index8_bfn {h : Heap} {wb : Nat} {wa : Array UInt8} (hb : h.bytes wb = some wa) {off : Nat} {k : Int} {i : Nat}
83    (hk : (off : Int) + k = i) (hi : i < wa.size) : index8 (.ref (.blk wb) off) k h = .ok (bfn wa i, h) := by
84  have g : Space.get h (BRef.blk wb) = some wa := by simpa using hb
85  have a1 := Ptr.add_ok (h := h) (r := BRef.blk wb) (a := wa) (off := off) (k := k) g (by omega) (by omega)
86  have e : ((off : Int) + k).toNat = i := by omega
87  rw [e] at a1
88  have a2 : OkOn h (Ptr.load (Ptr.ref (BRef.blk wb) i)) (bfn wa i) := load8_bfn hb hi
89  exact OkOn.bind (f := fun p => Ptr.load p) a1 a2
90
91theorem LMEnv.dist {h0 : Heap} {sr : Nat} {d : DeflateState} {wb pb : Nat} {wa : Array UInt8} {pa : Array UInt16} {c : UInt32}
92    (E : LMEnv h0 sr d wb pb wa pa c) :
93    ∀ p, Chain (wfn pa) (d.w_size.toNat - 1) (lmLimit d.strstart.toNat (d.w_size.toNat - 262)) c.toNat p →
94      p ≤ d.strstart.toNat → d.strstart.toNat - p ≤ d.w_size.toNat - 262 := by
95  intro p hp hps
96  induction hp with
97  | start => exact E.cdist
98  | step _ hq hlim _ => unfold lmLimit at hlim; split at hlim <;> omega
99
100/-- **One candidate.** The body of the `longest_match` loop does not fault when the loop invariant holds and
101`brk` is false, and the invariant holds afterwards; `cur_match`, `chain_length` and `nice_match` are not changed. -/
102theorem lm_body_ok {h0 : Heap} {sr wb pb : Nat} {d : DeflateState} {wa : Array UInt8} {pa : Array UInt16} {c : UInt32}
103    (E : LMEnv h0 sr d wb pb wa pa c) (st : LMState) {h : Heap} (hbrk : st.brk = false)
104    (hI : LMInv h0 sr d wb pb wa pa c st h) :
105    ∃ st' h', lm_body (some (.tab sr)) st h = .ok (st', h') ∧ LMInv h0 sr d wb pb wa pa c st' h' ∧
106      st'.cur_match = st.cur_match ∧ st'.chain_length = st.chain_length ∧ st'.nice_match = st.nice_match := by
107  have hI0 := hI
108  obtain ⟨ms, b, rfl, hscan, hb, hpl, hb258, hse, hch, hgood⟩ := hI
109  obtain ⟨hse1, hse⟩ := hse hbrk
110  obtain ⟨k, hk, hk9, hk15⟩ := E.wsb
111  have hws9 : 512 ≤ d.w_size.toNat := by
112    rw [hk]; calc 512 = 2 ^ 9 := by decide
113      _ ≤ 2 ^ k := Nat.pow_le_pow_right (by decide) hk9
114  have hws15 : d.w_size.toNat ≤ 32768 := by
115    rw [hk]; calc 2 ^ k ≤ 2 ^ 15 := Nat.pow_le_pow_right (by decide) hk15
116      _ = 32768 := by decide
117  have hroom := E.room
118  have hasz := E.asize
119  obtain ⟨hcm1, hcmlt, hcmprev, hcm3⟩ := E.chain _ hch
120  have hdist := E.dist _ hch (by omega)
121  have hss : d.strstart.toNat + 258 < wa.size := by omega
122  -- the heap
123  have hdd : (hAt h0 sr d ms).dstates sr = some { d with match_start := ms } := by simp [hAt]
124  have e_ld : ldDeflateState (some (.tab sr)) (hAt h0 sr d ms) = .ok ({ d with match_start := ms }, hAt h0 sr d ms) :=
125    ldDeflateState_tab hdd
126  have hbytes : (hAt h0 sr d ms).bytes wb = some wa := E.wbytes
127  have hmm : MAX_MATCH_u.toNat = 258 := rfl
128  have h258 : (258 : Int32).toInt = 258 := by decide
129  have h1i : (1 : Int32).toInt = 1 := by decide
130  -- the monadic steps
131  have f2 : padd (Ptr.ref (BRef.blk wb) 0) st.cur_match.toNat (hAt h0 sr d ms) = .ok (Ptr.ref (BRef.blk wb) st.cur_match.toNat, hAt h0 sr d ms) := by
132    simpa using padd_ok' (h := hAt h0 sr d ms) (r := BRef.blk wb) (a := wa) (off := 0) (n := st.cur_match.toNat)
133      (by simpa using hbytes) (by omega)
134  have f3 : index8 (Ptr.ref (BRef.blk wb) st.cur_match.toNat) (b : Int) (hAt h0 sr d ms) = .ok (bfn wa (st.cur_match.toNat + b), hAt h0 sr d ms) :=
135    index8_bfn hbytes (by omega) (by omega)
136  have f4 : isub st.best_len 1 (hAt h0 sr d ms) = .ok (Int32.ofInt ((b : Int) - 1), hAt h0 sr d ms) := by
137    rw [isub_ok st.best_len 1 (by rw [hb, h1i]; omega)]
138    rw [hb, h1i]
139  have f5 : (Int32.ofInt ((b : Int) - 1)).toInt = (b : Int) - 1 := Int32.toInt_ofInt_of_le (by omega) (by omega)
140  have f6 : index8 (Ptr.ref (BRef.blk wb) st.cur_match.toNat) ((b : Int) - 1) (hAt h0 sr d ms) = .ok (bfn wa (st.cur_match.toNat + b - 1), hAt h0 sr d ms) :=
141    index8_bfn hbytes (by omega) (by omega)
142  have f7 : load8 (Ptr.ref (BRef.blk wb) st.cur_match.toNat) (hAt h0 sr d ms) = .ok (bfn wa st.cur_match.toNat, hAt h0 sr d ms) :=
143    load8_bfn hbytes (by omega)
144  have f8 : load8 (Ptr.ref (BRef.blk wb) d.strstart.toNat) (hAt h0 sr d ms) = .ok (bfn wa d.strstart.toNat, hAt h0 sr d ms) :=
145    load8_bfn hbytes (by omega)
146  have f9 : padd (Ptr.ref (BRef.blk wb) st.cur_match.toNat) 1 (hAt h0 sr d ms) = .ok (Ptr.ref (BRef.blk wb) (st.cur_match.toNat + 1), hAt h0 sr d ms) :=
147    padd_ok' (by simpa using hbytes) (by omega)
148  have f10 : load8 (Ptr.ref (BRef.blk wb) (st.cur_match.toNat + 1)) (hAt h0 sr d ms) = .ok (bfn wa (st.cur_match.toNat + 1), hAt h0 sr d ms) :=
149    load8_bfn hbytes (by omega)
150  have f11 : index8 (Ptr.ref (BRef.blk wb) d.strstart.toNat) 1 (hAt h0 sr d ms) = .ok (bfn wa (d.strstart.toNat + 1), hAt h0 sr d ms) :=
151    index8_bfn hbytes (by omega) (by omega)
152  have f12 : padd (Ptr.ref (BRef.blk wb) d.strstart.toNat) 2 (hAt h0 sr d ms) = .ok (Ptr.ref (BRef.blk wb) (d.strstart.toNat + 2), hAt h0 sr d ms) :=
153    padd_ok' (by simpa using hbytes) (by omega)
154  have f13 : padd (Ptr.ref (BRef.blk wb) (st.cur_match.toNat + 1)) 1 (hAt h0 sr d ms) = .ok (Ptr.ref (BRef.blk wb) (st.cur_match.toNat + 2), hAt h0 sr d ms) :=
155    padd_ok' (by simpa using hbytes) (by omega)
156  have f14 : padd (Ptr.ref (BRef.blk wb) 0) d.strstart.toNat (hAt h0 sr d ms) = .ok (Ptr.ref (BRef.blk wb) d.strstart.toNat, hAt h0 sr d ms) := by
157    simpa using padd_ok' (h := hAt h0 sr d ms) (r := BRef.blk wb) (a := wa) (off := 0) (n := d.strstart.toNat)
158      (by simpa using hbytes) (by omega)
159  have f15 : padd (Ptr.ref (BRef.blk wb) d.strstart.toNat) 258 (hAt h0 sr d ms) = .ok (Ptr.ref (BRef.blk wb) (d.strstart.toNat + 258), hAt h0 sr d ms) :=
160    padd_ok' (by simpa using hbytes) (by omega)
161  have f16 : psub (Ptr.ref (BRef.blk wb) (d.strstart.toNat + 258)) 258 (hAt h0 sr d ms) = .ok (Ptr.ref (BRef.blk wb) d.strstart.toNat, hAt h0 sr d ms) := by
162    simpa using psub_ok' (h := hAt h0 sr d ms) (r := BRef.blk wb) (a := wa) (off := d.strstart.toNat + 258) (n := 258)
163      (by simpa using hbytes) (by omega) (by omega)
164  -- the early returns
165  by_cases T1 : bfn wa (st.cur_match.toNat + b) = bfn wa (d.strstart.toNat + b)
166  rotate_left
167  · refine ⟨st, hAt h0 sr d ms, ?_, hI0, rfl, rfl, rfl⟩
168    simp only [lm_body, bind_app, pure_app, M_ite_app, ↓reduceIte, e_ld, E.win, f2, hb, f3, hse, T1]
169    simp [T1]
170  by_cases T2 : bfn wa (st.cur_match.toNat + b - 1) = bfn wa (d.strstart.toNat + b - 1)
171  rotate_left
172  · refine ⟨st, hAt h0 sr d ms, ?_, hI0, rfl, rfl, rfl⟩
173    simp only [lm_body, bind_app, pure_app, M_ite_app, ↓reduceIte, e_ld, E.win, f2, hb, f3, hse, T1, f4, f5, f6, hse1]
174    simp [T2]
175  by_cases T3 : bfn wa st.cur_match.toNat = bfn wa d.strstart.toNat
176  rotate_left
177  · refine ⟨st, hAt h0 sr d ms, ?_, hI0, rfl, rfl, rfl⟩
178    simp only [lm_body, bind_app, pure_app, M_ite_app, ↓reduceIte, e_ld, E.win, f2, hb, f3, hse, T1, f4, f5, f6, hse1, T2, f7,
179      hscan, f8]
180    simp [T3]
181  by_cases T4 : bfn wa (st.cur_match.toNat + 1) = bfn wa (d.strstart.toNat + 1)
182  rotate_left
183  · refine ⟨st, hAt h0 sr d ms, ?_, hI0, rfl, rfl, rfl⟩
184    simp only [lm_body, bind_app, pure_app, M_ite_app, ↓reduceIte, e_ld, E.win, f2, hb, f3, hse, T1, f4, f5, f6, hse1, T2, f7,
185      hscan, f8, T3, f9, f10, f11]
186    simp [T4]
187  -- the candidate agrees on three bytes
188  have T5 : bfn wa (st.cur_match.toNat + 2) = bfn wa (d.strstart.toNat + 2) := hcm3 T3 T4
189  obtain ⟨r, hr⟩ : ∃ r, r = matchLen (bfn wa) d.strstart.toNat st.cur_match.toNat := ⟨_, rfl⟩
190  obtain ⟨hr3, hr258⟩ := matchLen_bounds (bfn wa) d.strstart.toNat st.cur_match.toNat
191  rw [← hr] at hr3 hr258
192  have hcmss : st.cur_match.toNat ≤ d.strstart.toNat := by omega
193  have hloop := lm_inner_loop (h := hAt h0 sr d ms) hbytes d.strstart.toNat st.cur_match.toNat hss hcmss T3.symm T4.symm T5.symm
194  rw [← hr] at hloop
195  have hagree : ∀ j, j < r → bfn wa (st.cur_match.toNat + j) = bfn wa (d.strstart.toNat + j) := by
196    intro j hj
197    rw [hr] at hj
198    exact (matchLen_agree (bfn wa) d.strstart.toNat st.cur_match.toNat T3.symm T4.symm T5.symm j hj).symm
199  have fd : Ptr.diff (Ptr.ref (BRef.blk wb) (d.strstart.toNat + 258)) (Ptr.ref (BRef.blk wb) (d.strstart.toNat + r)) (hAt h0 sr d ms) =
200      .ok (Int64.ofInt (258 - (r : Int)), hAt h0 sr d ms) := by
201    have := Ptr.diff_ok (h := hAt h0 sr d ms) (r := BRef.blk wb) (a := wa) (o1 := d.strstart.toNat + 258) (o2 := d.strstart.toNat + r)
202      (by simpa using hbytes) (by omega) (by omega) (by omega)
203    unfold OkOn at this
204    rw [this]
205    congr 3
206    omega
207  have fl : isub 258 (Int64.ofInt (258 - (r : Int))).toInt32 (hAt h0 sr d ms) = .ok (Int32.ofInt (r : Int), hAt h0 sr d ms) := by
208    rw [Int64.toInt32_ofInt]
209    have e1 : (Int32.ofInt (258 - (r : Int))).toInt = 258 - (r : Int) := Int32.toInt_ofInt_of_le (by omega) (by omega)
210    rw [isub_ok 258 _ (by rw [e1, h258]; omega), e1, h258]
211    congr 3
212    omega
213  have hlen : (Int32.ofInt (r : Int)).toInt = (r : Int) := Int32.toInt_ofInt_of_le (by omega) (by omega)
214  by_cases hgt : b < r
215  rotate_left
216  · -- no improvement
217    have hngt : ¬ (Int32.ofInt (r : Int) > st.best_len) := by
218      rw [GT.gt, Int32.lt_iff_toInt_lt, hb, hlen]; omega
219    refine ⟨{ st with scan := Ptr.ref (BRef.blk wb) d.strstart.toNat }, hAt h0 sr d ms, ?_, ?_, rfl, rfl, rfl⟩
220    · simp only [lm_body, bind_app, pure_app, M_ite_app, ↓reduceIte, e_ld, E.win, f2, hb, f3, hse, T1, f4, f5, f6, hse1, T2,
221        f7, hscan, f8, T3, f9, f10, f11, T4, f12, f13, f14, f15, hmm, hloop, fd, fl, f16, hngt]
222      simp [T1, T2, T3, T4, hngt]
223    · exact ⟨ms, b, rfl, rfl, hb, hpl, hb258, fun _ => ⟨hse1, hse⟩, hch, hgood⟩
224  -- an improvement
225  have hgt' : Int32.ofInt (r : Int) > st.best_len := by
226    rw [GT.gt, Int32.lt_iff_toInt_lt, hb, hlen]; omega
227  have hgm : GoodMatch wa d.strstart.toNat d.w_size.toNat st.cur_match.toNat r :=
228    ⟨hcmlt, hdist, hr258, hagree⟩
229  have hdd1 : (hAt h0 sr d ms).dstates sr = some { d with match_start := ms } := hdd
230  have f17 : wr (some (.tab sr)) (fun d => { d with match_start := st.cur_match }) (hAt h0 sr d ms) =
231      .ok ((), hAt h0 sr d st.cur_match) := by
232    unfold wr
233    simp only [bind_app, e_ld]
234    rw [stDeflateState_tab hdd1]
235    simp [hAt, upd_upd]
236  have hbytes1 : (hAt h0 sr d st.cur_match).bytes wb = some wa := E.wbytes
237  have g1 : isub (Int32.ofInt (r : Int)) 1 (hAt h0 sr d st.cur_match) =
238      .ok (Int32.ofInt ((r : Int) - 1), hAt h0 sr d st.cur_match) := by
239    rw [isub_ok _ 1 (by rw [hlen, h1i]; omega)]
240    rw [hlen, h1i]
241  have g1' : (Int32.ofInt ((r : Int) - 1)).toInt = (r : Int) - 1 := Int32.toInt_ofInt_of_le (by omega) (by omega)
242  have g2 : index8 (Ptr.ref (BRef.blk wb) d.strstart.toNat) ((r : Int) - 1) (hAt h0 sr d st.cur_match) =
243      .ok (bfn wa (d.strstart.toNat + r - 1), hAt h0 sr d st.cur_match) := index8_bfn hbytes1 (by omega) (by omega)
244  have g3 : index8 (Ptr.ref (BRef.blk wb) d.strstart.toNat) (r : Int) (hAt h0 sr d st.cur_match) =
245      .ok (bfn wa (d.strstart.toNat + r), hAt h0 sr d st.cur_match) := index8_bfn hbytes1 (by omega) (by omega)
246  have hgm' : GoodMatch wa d.strstart.toNat d.w_size.toNat st.cur_match.toNat r := hgm
247  by_cases hnice : st.nice_match ≤ Int32.ofInt (r : Int)
248  · refine ⟨{ st with scan := Ptr.ref (BRef.blk wb) d.strstart.toNat, best_len := Int32.ofInt (r : Int), brk := true },
249      hAt h0 sr d st.cur_match, ?_, ?_, rfl, rfl, rfl⟩
250    · simp only [lm_body, bind_app, pure_app, M_ite_app, ↓reduceIte, e_ld, E.win, f2, hb, f3, hse, T1, f4, f5, f6, hse1, T2,
251        f7, hscan, f8, T3, f9, f10, f11, T4, f12, f13, f14, f15, hmm, hloop, fd, fl, f16, hgt', f17]
252      simp [T1, T2, T3, T4, hgt', hnice]
253    · exact ⟨st.cur_match, r, rfl, rfl, hlen, by omega, hr258, fun h => by simp at h, hch, Or.inr ⟨by omega, hgm'⟩⟩
254  · refine ⟨{ st with scan := Ptr.ref (BRef.blk wb) d.strstart.toNat, best_len := Int32.ofInt (r : Int), scan_end1 := bfn wa (d.strstart.toNat + r - 1), scan_end := bfn wa (d.strstart.toNat + r) }, hAt h0 sr d st.cur_match, ?_, ?_, rfl, rfl, rfl⟩
255    · simp only [lm_body, bind_app, pure_app, M_ite_app, ↓reduceIte, e_ld, E.win, f2, hb, f3, hse, T1, f4, f5, f6, hse1, T2,
256        f7, hscan, f8, T3, f9, f10, f11, T4, f12, f13, f14, f15, hmm, hloop, fd, fl, f16, hgt', f17, g1, g1', g2, hlen, g3]
257      simp [T1, T2, T3, T4, hgt', hnice]
258    · exact ⟨st.cur_match, r, rfl, rfl, hlen, by omega, hr258, fun _ => ⟨rfl, rfl⟩, hch, Or.inr ⟨by omega, hgm'⟩⟩
259
260end Zlib.Deflate.Engine.Proofs