deflate.c.engine.readbuf.lean

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

1import ZlibF.Zlib.«deflate_base.c»
2import ZlibF.Proof.«deflate.c.engine.macros»
3import ZlibF.Proof.«deflate.c.engine.loops»
4import ZlibF.Proof.«adler32.c»
5import ZlibF.Proof.«crc32.c»
6
7/-!
8# deflate.c, engine: `read_buf`
9
10`read_buf(strm, buf, size)` copies `L = min(avail_in, size)` bytes from `next_in` to `buf`, advances `next_in`,
11`total_in`, lowers `avail_in`, and updates `adler` with the Adler-32 (`wrap = 1`) or CRC-32 (`wrap = 2`) of the bytes
12copied. Nothing else changes. The checksum theorems of `adler32.c` and `crc32.c` are used as proved.
13-/
14
15namespace Zlib.Deflate.Engine.Proofs
16open C Zlib.Deflate
17
18/-- `len = strm->avail_in; if (len > size) len = size;` -/
19def rbLen (avail size : UInt32) : UInt32 := if avail > size then size else avail
20
21theorem seg_eq_take_drop (a : Array UInt8) (p n : Nat) (h : p + n ≤ a.size) :
22    Zlib.Adler32.Proofs.seg a p n = (a.toList.drop p).take n := by
23  apply List.ext_getElem
24  · simp [Zlib.Adler32.Proofs.seg]; omega
25  · intro i h1 h2
26    simp [Zlib.Adler32.Proofs.seg] at h1 ⊢
27    simp [getElem!_def, Array.getElem?_eq_getElem (show p + i < a.size by omega)]
28
29theorem seg_copyRange (ba ia : Array UInt8) (bo io L : Nat) (hfit : bo + L ≤ ba.size) :
30    Zlib.Adler32.Proofs.seg (copyRange ba ia bo io L) bo L = Zlib.Adler32.Proofs.seg ia io L := by
31  unfold Zlib.Adler32.Proofs.seg
32  apply List.map_congr_left
33  intro i hi
34  have hi' : i < L := List.mem_range.mp hi
35  have := getElem?_copyRange ba ia bo io L (bo + i) hfit
36  simp only [getElem!_def, this, show bo ≤ bo + i ∧ bo + i < bo + L by omega, and_self, ite_true,
37    Nat.add_sub_cancel_left]
38
39/-- `strm->avail_in -= len` -/
40def rbDec (L : UInt32) : ZStream → ZStream := fun z => { z with avail_in := z.avail_in - L }
41/-- `strm->adler = a` -/
42def rbSetAd (a : UInt64) : ZStream → ZStream := fun z => { z with adler := a }
43/-- `strm->next_in += len; strm->total_in += len` (the new `next_in` is `ni`) -/
44def rbAdvF (ni : BPtr) (L : UInt32) : ZStream → ZStream := fun z => { z with next_in := ni, total_in := z.total_in + L.toUInt64 }
45
46/-- `read_buf` with the length already computed (`len` is `min(avail_in, size)`). -/
47def rbCore (strm : ZStreamPtr) (buf : BPtr) (len : UInt32) : M UInt32 := do
48  if len == 0 then return 0
49  zwr strm (rbDec len)
50  memcpyB buf (← zrd strm (·.next_in)) len.toNat
51  let sp ← castDeflateState (← zrd strm (·.state))
52  let wrap ← rd sp (·.wrap)
53  if wrap == 1 then
54    let a ← zrd strm (·.adler)
55    let r ← Zlib.Adler32.adler32 a buf len
56    zwr strm (rbSetAd r)
57  else if wrap == 2 then
58    let a ← zrd strm (·.adler)
59    let r ← Zlib.Crc32.crc32 a buf len
60    zwr strm (rbSetAd r)
61  let ni ← padd (← zrd strm (·.next_in)) len.toNat
62  zwr strm (rbAdvF ni len)
63  return len
64
65theorem read_buf_eq {h : Heap} {zr : Nat} {z : ZStream} (buf : BPtr) (size : UInt32) (hz : h.streams zr = some z) :
66    read_buf (some (.tab zr)) buf size h = rbCore (some (.tab zr)) buf (rbLen z.avail_in size) h := by
67  have e1 : ldZStream (some (.tab zr)) h = .ok (z, h) := ldZStream_tab hz
68  unfold read_buf rbCore rbLen
69  simp only [zrd, bind_app, e1, pure_app]
70  by_cases hg : z.avail_in > size
71  · simp only [ite_eq_left hg]; rfl
72  · simp only [ite_eq_right hg]; rfl
73
74/-- No byte to copy (`min(avail_in, size) = 0`): `read_buf` returns 0 and changes nothing. -/
75theorem read_buf_zero {h : Heap} {zr : Nat} {z : ZStream} (buf : BPtr) (size : UInt32)
76    (hz : h.streams zr = some z) (h0 : rbLen z.avail_in size = 0) :
77    read_buf (some (.tab zr)) buf size h = .ok (0, h) := by
78  rw [read_buf_eq buf size hz, h0]
79  simp [rbCore]
80
81/-- The stream record after `read_buf` copied `L` bytes from `next_in` (block `ib`, offset `io`) and the checksum became `a`. -/
82def rbStream (z : ZStream) (L : UInt32) (ib io : Nat) (a : UInt64) : ZStream :=
83  { z with avail_in := z.avail_in - L, next_in := .ref (.blk ib) (io + L.toNat), total_in := z.total_in + L.toUInt64,
84           adler := a }
85
86/-- The last step of `read_buf`: `next_in += L`, `total_in += L`. -/
87def rbAdv (z : ZStream) (L : UInt32) (ib io : Nat) : ZStream :=
88  { z with next_in := .ref (.blk ib) (io + L.toNat), total_in := z.total_in + L.toUInt64 }
89
90theorem u32_toUInt64_eq (len : UInt32) : len.toUInt64 = len.toNat.toUInt64 := by
91  apply UInt64.toNat_inj.mp; simp
92
93/-- **read_buf, the copy.** When `L = min(avail_in, size)` is not zero, the source `next_in[0 .. L)` and the
94destination `buf[0 .. L)` lie in their blocks and do not overlap, and the destination block is writable, the call does
95not fault, returns `L`, copies the bytes, lowers `avail_in` by `L`, advances `next_in` and `total_in` by `L`, and
96changes `adler` to the checksum of the bytes copied: the Adler-32 for `wrap = 1`, the CRC-32 for `wrap = 2`, no change
97otherwise. (For `wrap = 1` and `L = 1`, the value is the Adler-32 only if the old high sum is canonical, which
98every stored value is; without it the value is still computed without fault.) -/
99theorem read_buf_ok {h : Heap} {zr dsid ib bb io bo : Nat} {z : ZStream} {d : DeflateState} {ia ba : Array UInt8}
100    (buf : BPtr) (size : UInt32)
101    (hz : h.streams zr = some z) (hs : z.state = some (.deflate dsid)) (hd : h.dstates dsid = some d)
102    (hL : rbLen z.avail_in size ≠ 0)
103    (hin : z.next_in = .ref (.blk ib) io) (hib : h.bytes ib = some ia)
104    (hbuf : buf = .ref (.blk bb) bo) (hbb : h.bytes bb = some ba) (hro : h.ro bb = false)
105    (hfin : io + (rbLen z.avail_in size).toNat ≤ ia.size) (hfbuf : bo + (rbLen z.avail_in size).toNat ≤ ba.size)
106    (hdis : bb ≠ ib ∨ io + (rbLen z.avail_in size).toNat ≤ bo ∨ bo + (rbLen z.avail_in size).toNat ≤ io)
107    (hstat : d.wrap = 2 → Zlib.Crc32.Proofs.StaticsOK h) :
108    ∃ adler' : UInt64, read_buf (some (.tab zr)) buf size h = .ok (rbLen z.avail_in size, { h with
109        bytes := upd h.bytes bb (some (copyRange ba ia bo io (rbLen z.avail_in size).toNat)),
110        streams := upd h.streams zr (some (rbStream z (rbLen z.avail_in size) ib io adler')) }) ∧
111      (d.wrap = 1 → ((rbLen z.avail_in size).toNat ≠ 1 ∨ (z.adler >>> 16 &&& 65535).toNat < 65521) →
112        adler'.toNat = Zlib.Adler32.Spec.adler32 z.adler.toNat (Zlib.Adler32.Proofs.seg ia io (rbLen z.avail_in size).toNat)) ∧
113      (d.wrap = 2 → adler' = (ZlibF.Spec.crc32Update z.adler.toUInt32
114        ((ia.toList.drop io).take (rbLen z.avail_in size).toNat)).toUInt64) ∧
115      (d.wrap ≠ 1 → d.wrap ≠ 2 → adler' = z.adler) := by
116  obtain ⟨L, hLd⟩ : ∃ L, L = rbLen z.avail_in size := ⟨_, rfl⟩
117  rw [← hLd] at hL hfin hfbuf hdis ⊢
118  have hL0 : L.toNat ≠ 0 := fun h0 => hL (UInt32.toNat_inj.mp (by simpa using h0))
119  have hLle : L.toNat ≤ z.avail_in.toNat := by
120    rw [hLd]; unfold rbLen; split
121    · rename_i hg; rw [GT.gt, UInt32.lt_iff_toNat_lt] at hg; omega
122    · rename_i hg; rw [GT.gt, UInt32.lt_iff_toNat_lt] at hg; omega
123  have e1 : ldZStream (some (.tab zr)) h = .ok (z, h) := ldZStream_tab hz
124  obtain ⟨z1, hz1⟩ : ∃ z1 : ZStream, z1 = { z with avail_in := z.avail_in - L } := ⟨_, rfl⟩
125  obtain ⟨H1, hH1⟩ : ∃ H1 : Heap, H1 = { h with streams := upd h.streams zr (some z1) } := ⟨_, rfl⟩
126  have hs1 : H1.streams zr = some z1 := by rw [hH1]; simp
127  have e2 : zwr (some (.tab zr)) (rbDec L) h = .ok ((), H1) := by
128    unfold zwr; simp only [bind_app, e1]; rw [stZStream_tab hz, hH1, hz1]; try rfl
129  have hL0b : (L == 0) = false := by
130    simp only [beq_eq_false_iff_ne, ne_eq]; intro h0; exact hL0 (by rw [h0]; rfl)
131  subst hbuf
132  have hdis' : bb ≠ ib ∨ bo + L.toNat ≤ io ∨ io + L.toNat ≤ bo := by
133    rcases hdis with h1 | h1 | h1
134    · exact Or.inl h1
135    · exact Or.inr (Or.inr h1)
136    · exact Or.inr (Or.inl h1)
137  -- the copy
138  have e3 : zrd (some (.tab zr)) (·.next_in) H1 = .ok (Ptr.ref (BRef.blk ib) io, H1) := by
139    simp [zrd, ldZStream_tab hs1, hz1, hin]
140  obtain ⟨H2, hH2⟩ : ∃ H2 : Heap, H2 = { H1 with bytes := upd H1.bytes bb (some (copyRange ba ia bo io L.toNat)) } :=
141    ⟨_, rfl⟩
142  have e4 : memcpyB (Ptr.ref (BRef.blk bb) bo) (Ptr.ref (BRef.blk ib) io) L.toNat H1 = .ok ((), H2) := by
143    have := Ptr.memcpy_ok (h := H1) (rd := BRef.blk bb) (rs := BRef.blk ib) (od := bo) (os := io) (n := L.toNat)
144      (da := ba) (sa := ia) (by simpa [hH1] using hbb) (by simpa [hH1] using hib) (by simpa [hH1] using hro)
145      hfbuf hfin (by simpa using hdis')
146    simpa [hH2] using this
147  have hs2 : H2.streams zr = some z1 := by rw [hH2]; exact hs1
148  have hd2 : H2.dstates dsid = some d := by rw [hH2, hH1]; exact hd
149  have e5 : zrd (some (.tab zr)) (·.state) H2 = .ok (some (StateRef.deflate dsid), H2) := by
150    simp [zrd, ldZStream_tab hs2, hz1, hs]
151  have e6 : rd (some (.tab dsid)) (·.wrap) H2 = .ok (d.wrap, H2) := by
152    simp [rd, ldDeflateState_tab hd2]
153  have hbib : ∃ X, H2.bytes ib = some X ∧ X.size = ia.size := by
154    by_cases hib2 : ib = bb
155    · subst hib2
156      have : ba = ia := by rw [hib] at hbb; exact (Option.some.inj hbb).symm
157      subst this
158      exact ⟨copyRange ba ba bo io L.toNat, by rw [hH2]; simp, size_copyRange _ _ _ _ _⟩
159    · exact ⟨ia, by rw [hH2, hH1]; simp [upd_ne _ _ _ _ hib2, hib], rfl⟩
160  obtain ⟨X, hX, hXs⟩ := hbib
161  have hbb2 : H2.bytes bb = some (copyRange ba ia bo io L.toNat) := by rw [hH2]; simp
162  have hsz2 : (copyRange ba ia bo io L.toNat).size = ba.size := size_copyRange _ _ _ _ _
163  -- the tail after the checksum
164  have tailA : ∀ (H3 : Heap) (z2 : ZStream), H3.streams zr = some z2 → z2.next_in = Ptr.ref (BRef.blk ib) io →
165      H3.bytes ib = some X →
166      zrd (some (.tab zr)) (·.next_in) H3 = .ok (Ptr.ref (BRef.blk ib) io, H3) ∧
167      padd (Ptr.ref (BRef.blk ib) io) L.toNat H3 = .ok (Ptr.ref (BRef.blk ib) (io + L.toNat), H3) ∧
168      zwr (some (.tab zr)) (rbAdvF (Ptr.ref (BRef.blk ib) (io + L.toNat)) L) H3 =
169        .ok ((), { H3 with streams := upd H3.streams zr (some (rbAdv z2 L ib io)) }) := by
170    intro H3 z2 hs3 hn3 hX3
171    refine ⟨by simp [zrd, ldZStream_tab hs3, hn3], padd_ok' (by simpa using hX3) (by omega), ?_⟩
172    unfold zwr
173    simp only [bind_app, ldZStream_tab hs3]
174    rw [stZStream_tab hs3]
175    simp [rbAdv, rbAdvF, hn3]
176  have f0 : zrd (some (.tab zr)) (·.avail_in) h = .ok (z.avail_in, h) := by simp [zrd, e1]
177  have f7 : zrd (some (.tab zr)) (·.adler) H2 = .ok (z.adler, H2) := by simp [zrd, ldZStream_tab hs2, hz1]
178  have hLle32 : L.toNat < 2 ^ 32 := L.toNat_lt
179  have hcheck : ∀ (adler' : UInt64) (H3 : Heap), H3 = { H2 with streams := upd H2.streams zr (some { z1 with adler := adler' }) } →
180      zwr (some (.tab zr)) (rbSetAd adler') H2 = .ok ((), H3) := by
181    intro adler' H3 hH3
182    unfold zwr
183    simp only [bind_app, ldZStream_tab hs2]
184    rw [stZStream_tab hs2, hH3]
185    try rfl
186  have hend : ∀ (adler' : UInt64) (H3 : Heap), H3 = { H2 with streams := upd H2.streams zr (some { z1 with adler := adler' }) } →
187      ({ H3 with streams := upd H3.streams zr (some (rbAdv { z1 with adler := adler' } L ib io)) } : Heap) = { h with
188        bytes := upd h.bytes bb (some (copyRange ba ia bo io L.toNat)),
189        streams := upd h.streams zr (some (rbStream z L ib io adler')) } := by
190    intro adler' H3 hH3
191    simp [hH3, hH2, hH1, hz1, upd_upd, rbStream, rbAdv, rbDec, rbSetAd]
192  have htail : ∀ (adler' : UInt64) (H3 : Heap), H3 = { H2 with streams := upd H2.streams zr (some { z1 with adler := adler' }) } →
193      zrd (some (.tab zr)) (·.next_in) H3 = .ok (Ptr.ref (BRef.blk ib) io, H3) ∧
194      padd (Ptr.ref (BRef.blk ib) io) L.toNat H3 = .ok (Ptr.ref (BRef.blk ib) (io + L.toNat), H3) ∧
195      zwr (some (.tab zr)) (rbAdvF (Ptr.ref (BRef.blk ib) (io + L.toNat)) L) H3 = .ok ((), { h with
196        bytes := upd h.bytes bb (some (copyRange ba ia bo io L.toNat)),
197        streams := upd h.streams zr (some (rbStream z L ib io adler')) }) := by
198    intro adler' H3 hH3
199    have hs3 : H3.streams zr = some { z1 with adler := adler' } := by rw [hH3]; simp
200    obtain ⟨t1, t2, t3⟩ := tailA H3 _ hs3 (by rw [hz1]; exact hin) (by rw [hH3]; exact hX)
201    exact ⟨t1, t2, by rw [t3, hend adler' H3 hH3]⟩
202  have hhead : ∀ (m : M Unit), (m H2 = m H2) → True := fun _ _ => trivial
203  by_cases hw1 : d.wrap = 1
204  · obtain ⟨r, hr⟩ := Zlib.Adler32.Proofs.adler32_z_safe H2 bb _ hbb2 z.adler bo L.toNat (by omega) (by omega)
205    have e7 : Zlib.Adler32.adler32 z.adler (Ptr.ref (BRef.blk bb) bo) L H2 = .ok (r, H2) := by
206      unfold Zlib.Adler32.adler32; rw [u32_toUInt64_eq]; exact hr
207    obtain ⟨H3, hH3⟩ : ∃ H3 : Heap, H3 = { H2 with streams := upd H2.streams zr (some { z1 with adler := r }) } := ⟨_, rfl⟩
208    refine ⟨r, ?_, ?_, ?_, ?_⟩
209    · rw [read_buf_eq (Ptr.ref (BRef.blk bb) bo) size hz, ← hLd]; unfold rbCore
210      have hb1t : (d.wrap == 1) = true := by simpa using hw1
211      simp only [bind_app, pure_app, hL0b, M_ite_app, Bool.false_eq_true, ↓reduceIte, e2, e3, e4, e5,
212        castDeflateState_ok, e6, hb1t, f7, e7, hcheck r H3 hH3, (htail r H3 hH3).1, (htail r H3 hH3).2.1, (htail r H3 hH3).2.2]
213    · intro _ hc
214      have hv : Zlib.Adler32.Proofs.seg (copyRange ba ia bo io L.toNat) bo L.toNat = Zlib.Adler32.Proofs.seg ia io L.toNat :=
215        seg_copyRange ba ia bo io L.toNat hfbuf
216      have hcor : ∃ r', C.run (Zlib.Adler32.adler32_z z.adler (Ptr.ref (BRef.blk bb) bo) L.toNat.toUInt64) H2 = .ok (r', H2) ∧
217          r'.toNat = Zlib.Adler32.Spec.adler32 z.adler.toNat (Zlib.Adler32.Proofs.seg (copyRange ba ia bo io L.toNat) bo L.toNat) := by
218        by_cases h1 : L.toNat = 1
219        · have hv' : (z.adler >>> 16 &&& 65535).toNat < 65521 := hc.resolve_left (by simpa using h1)
220          exact Zlib.Adler32.Proofs.adler32_z_correct H2 bb _ hbb2 z.adler bo L.toNat (by omega) (by omega) hv'
221        · exact Zlib.Adler32.Proofs.adler32_z_correct_ne_one H2 bb _ hbb2 z.adler bo L.toNat (by omega) (by omega) h1
222      obtain ⟨r', hr', hspec⟩ := hcor
223      have : r' = r := by
224        have := hr'.symm.trans hr
225        simpa using this
226      rw [← this, hspec, hv]
227    · intro h2; rw [hw1] at h2; exact absurd h2 (by decide)
228    · intro h1; exact absurd hw1 h1
229  · by_cases hw2 : d.wrap = 2
230    · have hS := hstat hw2
231      have hS2 : Zlib.Crc32.Proofs.StaticsOK H2 := by rw [hH2, hH1]; exact hS
232      have hc := Zlib.Crc32.Proofs.crc32_z_correct H2 hS2 z.adler bb bo _ hbb2 L.toUInt64 (by rw [UInt32.toNat_toUInt64]; omega)
233      obtain ⟨r, hrd⟩ : ∃ r, r = (ZlibF.Spec.crc32Update z.adler.toUInt32 (((copyRange ba ia bo io L.toNat).toList.drop bo).take L.toNat)).toUInt64 := ⟨_, rfl⟩
234      have e7 : Zlib.Crc32.crc32 z.adler (Ptr.ref (BRef.blk bb) bo) L H2 = .ok (r, H2) := by
235        unfold Zlib.Crc32.crc32
236        have := hc
237        rw [UInt32.toNat_toUInt64] at this
238        unfold C.run at this
239        rw [hrd]; exact this
240      have hseg : ((copyRange ba ia bo io L.toNat).toList.drop bo).take L.toNat = (ia.toList.drop io).take L.toNat := by
241        rw [← seg_eq_take_drop _ _ _ (by omega), ← seg_eq_take_drop _ _ _ hfin, seg_copyRange ba ia bo io L.toNat hfbuf]
242      obtain ⟨H3, hH3⟩ : ∃ H3 : Heap, H3 = { H2 with streams := upd H2.streams zr (some { z1 with adler := r }) } := ⟨_, rfl⟩
243      refine ⟨r, ?_, ?_, ?_, ?_⟩
244      · rw [read_buf_eq (Ptr.ref (BRef.blk bb) bo) size hz, ← hLd]; unfold rbCore
245        have hb1 : (d.wrap == 1) = false := by simpa using hw1
246        have hb2t : (d.wrap == 2) = true := by simpa using hw2
247        simp only [bind_app, pure_app, hL0b, M_ite_app, Bool.false_eq_true, ↓reduceIte, e2, e3, e4, e5,
248          castDeflateState_ok, e6, hb1, hb2t, f7, e7, hcheck r H3 hH3, (htail r H3 hH3).1, (htail r H3 hH3).2.1, (htail r H3 hH3).2.2]
249      · intro h1; exact absurd h1 hw1
250      · intro _; rw [hrd, hseg]
251      · intro _ h2; exact absurd hw2 h2
252    · refine ⟨z.adler, ?_, ?_, ?_, ?_⟩
253      · rw [read_buf_eq (Ptr.ref (BRef.blk bb) bo) size hz, ← hLd]; unfold rbCore
254        have hb1 : (d.wrap == 1) = false := by simpa using hw1
255        have hb2 : (d.wrap == 2) = false := by simpa using hw2
256        have hH3 : H2 = { H2 with streams := upd H2.streams zr (some { z1 with adler := z.adler }) } := by
257          have : ({ z1 with adler := z.adler } : ZStream) = z1 := by rw [hz1]
258          rw [this, upd_self _ _ _ hs2]
259        simp only [bind_app, pure_app, hL0b, M_ite_app, Bool.false_eq_true, ↓reduceIte, e2, e3, e4, e5,
260          castDeflateState_ok, e6, hb1, hb2]
261        have ht := htail z.adler H2 hH3
262        simp only [ht.1, ht.2.1, ht.2.2]
263      · intro h1; exact absurd h1 hw1
264      · intro h1; exact absurd h1 hw2
265      · intro _ _; rfl
266
267end Zlib.Deflate.Engine.Proofs