deflate.c.engine.macros.lean

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

1import ZlibF.Zlib.«deflate_base.c»
2import ZlibF.Proof.«deflate.c.engine.hash»
3
4/-!
5# deflate.c, engine: `put_byte`, `putShortMSB`, `UPDATE_HASH`, `INSERT_STRING`, `CLEAR_HASH`
6
7Memory-dependent statements on the translation of `deflate_base.c.lean`. A byte block is `h.bytes b`, a block of
8words is `h.words b`; `head` and `prev` are pointers to word blocks, `pending_buf` and `window` to byte blocks.
9Each theorem says that the call does not fault and gives the exact new heap. The frame is then read off the
10equation: the heap changes only in the tables that the equation names, and in each of them only at the index it
11names.
12-/
13
14namespace Zlib.Deflate.Engine.Proofs
15open C Zlib.Deflate
16
17/-- The byte function of a block (the content, `0` beyond its end). -/
18def bfn (a : Array UInt8) : Nat → UInt8 := fun i => a.getD i 0
19/-- The word function of a block (the content, `0` beyond its end). -/
20def wfn (a : Array UInt16) : Nat → UInt16 := fun i => a.getD i 0
21
22theorem bfn_set (a : Array UInt8) (k : Nat) (v : UInt8) (hk : k < a.size) (i : Nat) :
23    bfn (a.set! k v) i = if i = k then v else bfn a i := by
24  unfold bfn
25  by_cases h : i = k
26  · subst h; simp [Array.getD_eq_getD_getElem?, hk]
27  · simp [Array.getD_eq_getD_getElem?, Array.set!_eq_setIfInBounds, h, Ne.symm h]
28
29theorem wfn_set (a : Array UInt16) (k : Nat) (v : UInt16) (hk : k < a.size) (i : Nat) :
30    wfn (a.set! k v) i = if i = k then v else wfn a i := by
31  unfold wfn
32  by_cases h : i = k
33  · subst h; simp [Array.getD_eq_getD_getElem?, hk]
34  · simp [Array.getD_eq_getD_getElem?, Array.set!_eq_setIfInBounds, h, Ne.symm h]
35
36theorem padd_ok' {R T : Type} [Space Heap R T] {h : Heap} {r : R} {a : Array T} {off n : Nat}
37    (hg : Space.get h r = some a) (hn : off + n ≤ a.size) : padd (Ptr.ref r off) n h = .ok (Ptr.ref r (off + n), h) :=
38  Ptr.add_nat_ok hg hn
39
40theorem psub_ok' {R T : Type} [Space Heap R T] {h : Heap} {r : R} {a : Array T} {off n : Nat}
41    (hg : Space.get h r = some a) (h1 : n ≤ off) (h2 : off ≤ a.size) :
42    psub (Ptr.ref r off) n h = .ok (Ptr.ref r (off - n), h) :=
43  Ptr.sub_nat_ok hg h1 h2
44
45theorem wfn_getElem (a : Array UInt16) (i : Nat) (hi : i < a.size) : wfn a i = a[i] := by
46  simp [wfn, Array.getD_eq_getD_getElem?, hi]
47
48/-! ## Pointwise views of `fillRange` and `copyRange` -/
49
50theorem fillRange_succ {T : Type} (d : Array T) (off n : Nat) (v : T) :
51    fillRange d off (n + 1) v = (fillRange d off n v).set! (off + n) v := by
52  unfold fillRange; rw [List.range_succ, List.foldl_append]; rfl
53
54theorem copyRange_succ {T : Type} [Inhabited T] (d s : Array T) (doff soff n : Nat) :
55    copyRange d s doff soff (n + 1) = (copyRange d s doff soff n).set! (doff + n) s[soff + n]! := by
56  unfold copyRange; rw [List.range_succ, List.foldl_append]; rfl
57
58/-- `fillRange`, pointwise: positions in `[off, off + n)` get `v`, the others keep their value. -/
59theorem getElem?_fillRange {T : Type} (d : Array T) (off n : Nat) (v : T) (i : Nat) (hfit : off + n ≤ d.size) :
60    (fillRange d off n v)[i]? = if off ≤ i ∧ i < off + n then some v else d[i]? := by
61  induction n generalizing i with
62  | zero => simp [fillRange]; intro h1 h2; omega
63  | succ n ih =>
64    rw [fillRange_succ, Array.set!_eq_setIfInBounds, Array.getElem?_setIfInBounds, ih i (by omega)]
65    have hs : (fillRange d off n v).size = d.size := size_fillRange _ _ _ _
66    by_cases hi : off + n = i
67    · subst hi
68      simp [hs, show off + n < d.size by omega]
69    · simp [hi]
70      by_cases h1 : off ≤ i ∧ i < off + n
71      · simp [h1]; omega
72      · simp [h1]; intro _ ; omega
73
74/-- `copyRange`, pointwise: positions in `[doff, doff + n)` get the source bytes, the others keep their value. -/
75theorem getElem?_copyRange {T : Type} [Inhabited T] (d s : Array T) (doff soff n : Nat) (i : Nat)
76    (hfit : doff + n ≤ d.size) :
77    (copyRange d s doff soff n)[i]? = if doff ≤ i ∧ i < doff + n then some s[soff + (i - doff)]! else d[i]? := by
78  induction n generalizing i with
79  | zero => simp [copyRange]; intro h1 h2; omega
80  | succ n ih =>
81    rw [copyRange_succ, Array.set!_eq_setIfInBounds, Array.getElem?_setIfInBounds, ih i (by omega)]
82    have hs : (copyRange d s doff soff n).size = d.size := size_copyRange _ _ _ _ _
83    by_cases hi : doff + n = i
84    · subst hi
85      simp [hs, show doff + n < d.size by omega]
86    · simp [hi]
87      by_cases h1 : doff ≤ i ∧ i < doff + n
88      · simp [h1]; omega
89      · simp [h1]; intro _ ; omega
90
91/-! ## `put_byte` and `putShortMSB` -/
92
93/-- **put_byte.** With `pending_buf` pointing into a writable byte block and room for the byte, `put_byte(s, c)`
94does not fault: it stores `c` at `pending_buf[pending]` and increments `pending`. The room is
95`pending_buf_size`-bounded in C (the callers keep `pending < pending_buf_size`); here the room is the block bound. -/
96theorem put_byte_ok {h : Heap} {sr b off : Nat} {d : DeflateState} {a : Array UInt8} (c : UInt8)
97    (hd : h.dstates sr = some d) (hp : d.pending_buf = .ref (.blk b) off) (ha : h.bytes b = some a)
98    (hro : h.ro b = false) (hlt : off + d.pending.toNat < a.size) :
99    put_byte (some (.tab sr)) c h = .ok ((), { h with
100      bytes := upd h.bytes b (some (a.set! (off + d.pending.toNat) c)),
101      dstates := upd h.dstates sr (some { d with pending := d.pending + 1 }) }) := by
102  have e1 : ldDeflateState (some (.tab sr)) h = .ok (d, h) := ldDeflateState_tab hd
103  have e2 : padd d.pending_buf d.pending.toNat h = .ok (.ref (.blk b) (off + d.pending.toNat), h) := by
104    rw [hp]; exact padd_ok' (by simpa using ha) (by omega)
105  have e3 : store8 (.ref (.blk b) (off + d.pending.toNat)) c h =
106      .ok ((), { h with bytes := upd h.bytes b (some (a.set! (off + d.pending.toNat) c)) }) := by
107    have := Ptr.store_ok (r := BRef.blk b) (T := UInt8) (a := a) (off := off + d.pending.toNat) (v := c)
108      (by simpa using ha) (by simpa using hro) hlt
109    simpa using this
110  simp only [put_byte, store_at, bind_app, e1, e2, e3]
111  rw [stDeflateState_tab (by simpa using hd)]
112
113theorem u64_succ_toNat (p : UInt64) (h : p.toNat + 1 < 2 ^ 64) : (p + 1).toNat = p.toNat + 1 := by
114  rw [UInt64.toNat_add]; simp; omega
115
116/-- **putShortMSB.** With room for two bytes, `putShortMSB(s, b)` does not fault: it stores the high byte of the
117low 16 bits of `b`, then the low byte, at `pending_buf[pending]` and `pending_buf[pending + 1]`, and adds 2 to
118`pending`. The hypothesis `pending + 2 < 2^64` holds whenever `pending <= pending_buf_size`. -/
119theorem putShortMSB_ok {h : Heap} {sr b off : Nat} {d : DeflateState} {a : Array UInt8} (v : UInt32)
120    (hd : h.dstates sr = some d) (hp : d.pending_buf = .ref (.blk b) off) (ha : h.bytes b = some a)
121    (hro : h.ro b = false) (hlt : off + d.pending.toNat + 1 < a.size) (hw : d.pending.toNat + 2 < 2 ^ 64) :
122    putShortMSB (some (.tab sr)) v h = .ok ((), { h with
123      bytes := upd h.bytes b (some ((a.set! (off + d.pending.toNat) (v >>> 8).toUInt8).set!
124        (off + d.pending.toNat + 1) (v &&& 0xff).toUInt8)),
125      dstates := upd h.dstates sr (some { d with pending := d.pending + 2 }) }) := by
126  have s1 := put_byte_ok (h := h) (sr := sr) (b := b) (off := off) (d := d) (a := a) (v >>> 8).toUInt8 hd hp ha hro
127    (by omega)
128  have hn1 : (d.pending + 1).toNat = d.pending.toNat + 1 := u64_succ_toNat _ (by omega)
129  have s2 := put_byte_ok (h := { h with
130      bytes := upd h.bytes b (some (a.set! (off + d.pending.toNat) (v >>> 8).toUInt8)),
131      dstates := upd h.dstates sr (some { d with pending := d.pending + 1 }) })
132    (sr := sr) (b := b) (off := off) (d := { d with pending := d.pending + 1 })
133    (a := a.set! (off + d.pending.toNat) (v >>> 8).toUInt8) (v &&& 0xff).toUInt8
134    (by simp) (by simpa using hp) (by simp) (by simpa using hro) (by simp [hn1]; omega)
135  unfold putShortMSB
136  rw [bind_app, s1]
137  simp only [hn1] at s2
138  simp only [s2]
139  have e2 : d.pending + 1 + 1 = d.pending + 2 := by
140    apply UInt64.toNat_inj.mp; rw [UInt64.toNat_add, UInt64.toNat_add]; simp
141  simp [e2, upd_upd, Nat.add_assoc]
142
143/-! ## The hash macros -/
144
145/-- **UPDATE_HASH.** With `hash_shift < 32`, `UPDATE_HASH(s, s->ins_h, c)` does not fault and sets `ins_h` to
146`((ins_h << hash_shift) ^ c) & hash_mask`. -/
147theorem UPDATE_HASH_ok {h : Heap} {sr : Nat} {d : DeflateState} (c : UInt8)
148    (hd : h.dstates sr = some d) (hs : d.hash_shift < 32) :
149    UPDATE_HASH (some (.tab sr)) c h = .ok ((), { h with
150      dstates := upd h.dstates sr (some { d with ins_h := updHash d.hash_shift d.hash_mask d.ins_h c }) }) := by
151  have e1 : ldDeflateState (some (.tab sr)) h = .ok (d, h) := ldDeflateState_tab hd
152  have e2 : ushl d.ins_h d.hash_shift h = .ok (d.ins_h <<< d.hash_shift, h) := by
153    simp [ushl, hs]
154  simp only [UPDATE_HASH, bind_app, e1, e2]
155  rw [stDeflateState_tab (by simpa using hd)]
156  rfl
157
158/-- The environment of `INSERT_STRING` and `fill_window`'s insertion loop: the window block, the `head` block of
159`hash_size` entries and the `prev` block of `w_size` entries, two different word blocks, and the hash parameters. -/
160structure HashEnv (h : Heap) (d : DeflateState) (wb hb pb : Nat) (wa : Array UInt8) (ha pa : Array UInt16) : Prop where
161  win : d.window = .ref (.blk wb) 0
162  wbytes : h.bytes wb = some wa
163  wro : h.ro wb = false
164  headp : d.head = .ref (.blk hb) 0
165  hwords : h.words hb = some ha
166  prevp : d.prev = .ref (.blk pb) 0
167  pwords : h.words pb = some pa
168  hne : hb ≠ pb
169  hsize : d.hash_size.toNat ≤ ha.size
170  wsize : d.w_size.toNat ≤ pa.size
171  wmask : d.w_mask.toNat < d.w_size.toNat
172  params : HashParams d.hash_size d.hash_shift d.hash_mask
173
174/-- **INSERT_STRING.** With the window holding the three bytes at `str` (`str + 2` in the block), `INSERT_STRING`
175does not fault. It updates `ins_h` with `window[str + 2]`, stores the old `head[ins_h]` into `prev[str & wmask]`,
176stores `str` into `head[ins_h]`, and returns the old `head[ins_h]`. -/
177theorem INSERT_STRING_ok {h : Heap} {sr wb hb pb : Nat} {d : DeflateState} {wa : Array UInt8} {ha pa : Array UInt16}
178    (hd : h.dstates sr = some d) (E : HashEnv h d wb hb pb wa ha pa) (str : UInt32)
179    (hstr : str.toNat + 2 < wa.size) (h32 : str.toNat + 2 < 2 ^ 32) :
180    ∃ x' : UInt32, x' = updHash d.hash_shift d.hash_mask d.ins_h wa[str.toNat + 2]! ∧ x'.toNat < d.hash_size.toNat ∧
181    INSERT_STRING (some (.tab sr)) str h = .ok ((wfn ha x'.toNat).toUInt32, { h with
182      dstates := upd h.dstates sr (some { d with ins_h := x' }),
183      words := upd (upd h.words pb (some (pa.set! (str &&& d.w_mask).toNat (wfn ha x'.toNat))))
184        hb (some (ha.set! x'.toNat str.toUInt16)) }) := by
185  obtain ⟨hwin, hwb, hwro, hhp, hhw, hpp, hpw, hne, hhs, hws, hwm, hprm⟩ := E
186  have h2 : (str + (MIN_MATCH_u - 1)).toNat = str.toNat + 2 := by
187    have : (MIN_MATCH_u - 1) = 2 := rfl
188    rw [this, UInt32.toNat_add]; simp; omega
189  have hsh : d.hash_shift < 32 := by
190    have := hprm.hsh_lt; rw [UInt32.lt_iff_toNat_lt]; simpa using this
191  have e1 : ldDeflateState (some (.tab sr)) h = .ok (d, h) := ldDeflateState_tab hd
192  have e2 : index8 d.window (str + (MIN_MATCH_u - 1)).toNat h = .ok (wa[str.toNat + 2], h) := by
193    rw [hwin, h2]
194    have := index8_ok (off := 0) (i := str.toNat + 2) hwb (by omega)
195    simpa [OkOn] using this
196  have hget : wa[str.toNat + 2]! = wa[str.toNat + 2] := by simp [hstr]
197  obtain ⟨x', hx'⟩ : ∃ x', x' = updHash d.hash_shift d.hash_mask d.ins_h wa[str.toNat + 2]! := ⟨_, rfl⟩
198  have hxlt : x'.toNat < d.hash_size.toNat := by rw [hx']; exact updHash_lt hprm _ _
199  refine ⟨x', hx', hxlt, ?_⟩
200  have e3 := UPDATE_HASH_ok (h := h) (sr := sr) (d := d) wa[str.toNat + 2] hd hsh
201  have hx2 : x' = updHash d.hash_shift d.hash_mask d.ins_h wa[str.toNat + 2] := by rw [hx', hget]
202  rw [← hx2] at e3
203  obtain ⟨h1, hh1⟩ : ∃ h1 : Heap, h1 = { h with dstates := upd h.dstates sr (some { d with ins_h := x' }) } := ⟨_, rfl⟩
204  rw [← hh1] at e3
205  have hd1 : h1.dstates sr = some { d with ins_h := x' } := by simp [hh1]
206  have e4 : ldDeflateState (some (.tab sr)) h1 = .ok ({ d with ins_h := x' }, h1) := ldDeflateState_tab hd1
207  have e5 : Ptr.index d.head x'.toNat h1 = .ok (ha[x'.toNat], h1) := by
208    rw [hhp]
209    have := Ptr.index_ok (h := h1) (r := WRef.blk hb) (T := UInt16) (a := ha) (off := 0) (i := x'.toNat)
210      (by simpa [hh1] using hhw) (by omega)
211    simpa [OkOn] using this
212  have hslot : (str &&& d.w_mask).toNat < pa.size := by
213    rw [UInt32.toNat_and]; have := Nat.and_le_right (n := str.toNat) (m := d.w_mask.toNat); omega
214  have e6 : padd d.prev (str &&& d.w_mask).toNat h1 = .ok (.ref (.blk pb) (str &&& d.w_mask).toNat, h1) := by
215    rw [hpp]
216    have := padd_ok' (h := h1) (r := WRef.blk pb) (a := pa) (off := 0) (n := (str &&& d.w_mask).toNat)
217      (by simpa [hh1] using hpw) (by omega)
218    simpa using this
219  obtain ⟨h2, hh2⟩ : ∃ h2 : Heap, h2 = { h1 with words := upd h1.words pb (some (pa.set! (str &&& d.w_mask).toNat ha[x'.toNat])) } := ⟨_, rfl⟩
220  have e7 : Ptr.store (Ptr.ref (WRef.blk pb) (str &&& d.w_mask).toNat) ha[x'.toNat] h1 = .ok ((), h2) := by
221    have := Ptr.store_ok (h := h1) (r := WRef.blk pb) (T := UInt16) (a := pa) (off := (str &&& d.w_mask).toNat)
222      (v := ha[x'.toNat]) (by simpa [hh1] using hpw) rfl hslot
223    rw [this, hh2]; simp
224  have hh2w : h2.words hb = some ha := by
225    simp only [hh2, hh1]; rw [upd_ne _ _ _ _ hne]; exact hhw
226  have e8 : padd d.head x'.toNat h2 = .ok (.ref (.blk hb) x'.toNat, h2) := by
227    rw [hhp]
228    have := padd_ok' (h := h2) (r := WRef.blk hb) (a := ha) (off := 0) (n := x'.toNat) hh2w (by omega)
229    simpa using this
230  have e9 : Ptr.store (Ptr.ref (WRef.blk hb) x'.toNat) str.toUInt16 h2 =
231      .ok ((), { h2 with words := upd h2.words hb (some (ha.set! x'.toNat str.toUInt16)) }) := by
232    have := Ptr.store_ok (r := WRef.blk hb) (T := UInt16) (a := ha) (off := x'.toNat) (v := str.toUInt16)
233      hh2w rfl (by omega)
234    simpa using this
235  have hv : wfn ha x'.toNat = ha[x'.toNat] := wfn_getElem _ _ (by omega)
236  simp only [INSERT_STRING, bind_app, e1, e2, e3, e4, e5, e6, e7, e8, e9]
237  rw [hv]
238  simp [hh2, hh1]
239
240end Zlib.Deflate.Engine.Proofs