deflate.c.public-getdict.lean

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

1import ZlibF.Proof.«deflate.c.life.getdict»
2
3/-! Dictionary copy into any represented writable byte object. -/
4
5namespace Zlib.Deflate.Proofs
6open C Zlib.Deflate Zlib.Deflate.Spec Zlib.Deflate.Engine.Proofs
7
8/-- `int deflateGetDictionary(z_streamp strm, Bytef *dictionary, uInt *dictLength)`
9copies into any represented writable byte object when its source and destination
10ranges are disjoint. The exact result describes the updated object. -/
11theorem deflateGetDictionary_run_copy_general {h : Heap} {r : ZStreamRef} {ds : Nat} {z : ZStream} {d : DeflateState}
12    {w p q b : Nat} (hL : DLive h r ds z d) (hB : DBlocks h d w p q b)
13    (hfill : d.strstart.toNat + d.lookahead.toNat ≤ d.window_size.toNat)
14    (dictionary : BPtr) (hasDictLength : Bool) {ref : BRef} {off : Nat} {da wa : Array UInt8}
15    (hd : dictionary = .ref ref off) (hda : Space.get h ref = some da) (hro : Space.ro h ref = false)
16    (hroom : off + (dictLen d).toNat ≤ da.size) (hwa : h.bytes w = some wa)
17    (hlen : (dictLen d).toNat = min (d.strstart.toNat + d.lookahead.toNat) d.w_size.toNat)
18    (hne : (dictLen d) ≠ 0)
19    (hdis : ref ≠ .blk w ∨ off + (dictLen d).toNat ≤ d.strstart.toNat + d.lookahead.toNat - (dictLen d).toNat ∨
20      d.strstart.toNat + d.lookahead.toNat - (dictLen d).toNat + (dictLen d).toNat ≤ off)
21    (hwsz : wa.size = d.window_size.toNat) :
22    deflateGetDictionary (some r) dictionary hasDictLength h =
23      .ok ((Z_OK, if hasDictLength then some (dictLen d) else none),
24        Space.put h ref (copyRange da wa off
25          (d.strstart.toNat + d.lookahead.toNat - (dictLen d).toNat) (dictLen d).toNat)) := by
26  rw [getdict_unfold hL]
27  have hc : (dictionary != .null && dictLen d != 0) = true := by simp [hd, hne]
28  simp only [hc, ite_true]
29  have hwa' : Space.get h (BRef.blk w) = some wa := hwa
30  have e1 : padd d.window d.strstart.toNat h = .ok (.ref (.blk w) d.strstart.toNat, h) := by
31    have := padd_ok' (r := BRef.blk w) (T := UInt8) (off := 0) (n := d.strstart.toNat) hwa' (by omega)
32    rw [hB.win]; simpa using this
33  have e2 : padd (.ref (.blk w) d.strstart.toNat : BPtr) d.lookahead.toNat h =
34      .ok (.ref (.blk w) (d.strstart.toNat + d.lookahead.toNat), h) :=
35    padd_ok' (r := BRef.blk w) (T := UInt8) (off := d.strstart.toNat) (n := d.lookahead.toNat) hwa' (by omega)
36  have e3 : psub (.ref (.blk w) (d.strstart.toNat + d.lookahead.toNat) : BPtr) (dictLen d).toNat h =
37      .ok (.ref (.blk w) (d.strstart.toNat + d.lookahead.toNat - (dictLen d).toNat), h) :=
38    psub_ok' (r := BRef.blk w) (T := UInt8) (off := d.strstart.toNat + d.lookahead.toNat) (n := (dictLen d).toNat)
39      hwa' (by omega) (by omega)
40  have e4 : memcpyB dictionary (.ref (.blk w) (d.strstart.toNat + d.lookahead.toNat - (dictLen d).toNat))
41      (dictLen d).toNat h = .ok ((), Space.put h ref (copyRange da wa off
42          (d.strstart.toNat + d.lookahead.toNat - (dictLen d).toNat) (dictLen d).toNat)) := by
43    subst hd
44    have := Ptr.memcpy_ok (rd := ref) (rs := BRef.blk w) (od := off)
45      (os := d.strstart.toNat + d.lookahead.toNat - (dictLen d).toNat) (n := (dictLen d).toNat) (da := da) (sa := wa)
46      (by simpa using hda) (by simpa using hwa) (by simpa using hro) hroom (by omega)
47      hdis
48    simpa using this
49  simp only [bind_app, e1, e2, e3, e4, pure_app]
50
51
52theorem copyRange_extract (da wa : Array UInt8) (off src n : Nat)
53    (hd : off + n ≤ da.size) (hs : src + n ≤ wa.size) :
54    copyRange da wa off src n = da.extract 0 off ++ wa.extract src (src+n) ++ da.extract (off+n) da.size := by
55  apply Array.ext_getElem?
56  intro i
57  rw [getElem?_copyRange _ _ _ _ _ _ hd]
58  have hs1 : min off da.size = off := Nat.min_eq_left (by omega)
59  have hs2 : min (src+n) wa.size = src+n := Nat.min_eq_left hs
60  by_cases h0 : i < off
61  · simp [Array.getElem?_append, Array.getElem?_extract, Array.size_extract, hs1, hs2, h0, show ¬ off ≤ i by omega, show i < da.size by omega]
62  · by_cases h1 : i < off + n
63    · have hsrc : src + (i - off) < wa.size := by omega
64      simp [Array.getElem?_append, Array.getElem?_extract, Array.size_extract, hs1, hs2, h0, h1,
65        show off ≤ i by omega, show i - off < n by omega, getElem!_pos wa (src + (i - off)) hsrc]
66    · have hshift : off + n + (i - off - n) = i := by omega
67      by_cases h2 : i < da.size
68      · simp [Array.getElem?_append, Array.getElem?_extract, Array.size_extract, hs1, hs2, h0, h1, h2,
69          show ¬ i - off < n by omega, show i - off - n < da.size - (off+n) by omega, hshift]
70      · have hout : da[i]? = none := Array.getElem?_eq_none (by omega)
71        simp [Array.getElem?_append, Array.getElem?_extract, Array.size_extract, hs1, hs2, h0, h1, h2,
72          show ¬ i - off < n by omega, show ¬ i - off - n < da.size - (off+n) by omega, hout]
73
74end Zlib.Deflate.Proofs