inflate.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.«inflate.c.dict»
2import ZlibF.Proof.«deflate.c.engine.macros»
3
4/-! General byte-object support for the dictionary query. -/
5
6namespace Zlib.Inflate.Proofs
7open C Zlib.Inflate Zlib.Inflate.Spec Zlib.Deflate.Engine.Proofs
8
9/-- Updating a writable byte object preserves a distinct byte-block source.
10The two writes to the destination compose to the final replacement. -/
11theorem getdict_put_properties {h : Heap} {rd : BRef} {old src : Array UInt8} {w : Nat}
12    (hd : Space.get h rd = some old) (hro : Space.ro h rd = false)
13    (hw : h.bytes w = some src) (hne : rd ≠ BRef.blk w) (a b : Array UInt8) :
14    Space.get (Space.put h rd a) rd = some a ∧
15    Space.get (Space.put h rd a) (BRef.blk w) = some src ∧
16    Space.ro (Space.put h rd a) rd = false ∧
17    Space.put (Space.put h rd a) rd b = Space.put h rd b := by
18  cases rd with
19  | blk x =>
20    change h.ro x = false at hro
21    have hx : x ≠ w := fun e => hne (by cases e; rfl)
22    simp [Space.get, Space.put, Space.ro, upd_ne _ _ _ _ hx.symm, hw, hro, upd_upd]
23  | str x => simp [Space.ro] at hro
24  | st_dist_code => simp [Space.ro] at hro
25  | st_length_code => simp [Space.ro] at hro
26  | dstate_depth x =>
27    cases he : h.dstates x with
28    | none => simp [Space.get, he] at hd
29    | some d =>
30      simp [Space.get, Space.put, Space.ro, he, hw, upd_upd]
31
32/-- `int inflateGetDictionary(z_streamp strm, Bytef *dictionary, uInt *dictLength)`
33copies both chronological window segments into any distinct writable byte object.
34The source remains intact and the final object is described exactly. -/
35theorem inflateGetDictionary_copy_general {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState}
36    {w off : Nat} {rd : BRef} {a D : Array UInt8} {dl : Option UInt32}
37    (hL : Live h r zs z st) (hw : st.window = .ref (.blk w) 0) (ha : h.bytes w = some a)
38    (hd : Space.get h rd = some D) (hro : Space.ro h rd = false) (hne : rd ≠ .blk w)
39    (hpos : st.whave ≠ 0) (hv : st.wnext.toNat ≤ st.whave.toNat)
40    (hwh : st.whave.toNat ≤ a.size) (hfit : off + st.whave.toNat ≤ D.size) :
41    inflateGetDictionary (some r) (.ref rd off) dl h =
42      .ok ((Z_OK, dl.map (fun _ => st.whave)),
43        Space.put h rd (getDictBytes D a off st.wnext.toNat st.whave.toNat)) := by
44  have hsub : (st.whave - st.wnext).toNat = st.whave.toNat - st.wnext.toNat :=
45    UInt32.toNat_sub_of_le _ _ (by rw [UInt32.le_iff_toNat_le]; exact hv)
46  have hfirst : Ptr.add (Ptr.ref (BRef.blk w) 0) (st.wnext.toNat : Int) h =
47      .ok (Ptr.ref (BRef.blk w) st.wnext.toNat, h) := by
48    have hh := Ptr.add_nat_ok (a := a) (r := BRef.blk w) (off := 0) (n := st.wnext.toNat) (by simpa using ha) (by omega)
49    unfold OkOn at hh
50    simpa using hh
51  let first := copyRange D a off st.wnext.toNat (st.whave - st.wnext).toNat
52  let mid := Space.put h rd first
53  have hmem1 : memcpyB (.ref rd off) (.ref (.blk w) st.wnext.toNat) (st.whave - st.wnext).toNat h =
54      .ok ((), mid) := by
55    exact Ptr.memcpy_ok (rd := rd) (rs := .blk w) hd (by simpa using ha) hro (by omega) (by omega) (Or.inl hne)
56  obtain ⟨hdmid, hamid, hromid, hput⟩ := getdict_put_properties hd hro ha hne first
57    (getDictBytes D a off st.wnext.toNat st.whave.toNat)
58  have hsize : first.size = D.size := size_copyRange ..
59  have hadd := Ptr.add_nat_ok (h := mid) (r := rd) (a := first) (off := off) (n := st.whave.toNat) hdmid (by omega)
60  have hsub' := Ptr.sub_nat_ok (h := mid) (r := rd) (a := first) (off := off + st.whave.toNat) (n := st.wnext.toNat)
61    hdmid (by omega) (by omega)
62  have hmem2 : memcpyB (.ref rd (off + st.whave.toNat - st.wnext.toNat)) (.ref (.blk w) 0) st.wnext.toNat mid =
63      .ok ((), Space.put mid rd (getDictBytes D a off st.wnext.toNat st.whave.toNat)) := by
64    have h := Ptr.memcpy_ok (rd := rd) (rs := .blk w) (od := off + st.whave.toNat - st.wnext.toNat)
65      (os := 0) (n := st.wnext.toNat) (da := first) (sa := a) hdmid hamid hromid (by omega) (by omega) (Or.inl hne)
66    simpa [getDictBytes, first, mid, hsub] using h
67  have hc : (st.whave != 0 && (Ptr.ref rd off : BPtr) != .null) = true := by simp [hpos]
68  unfold OkOn at hadd hsub'
69  unfold inflateGetDictionary
70  simp only [bind_app, pure_app, ldI_eq, ldZ_eq, hL.hz, hL.zst, castI, hL.hs, stateCheck_live hL,
71    bne_iff_ne, ne_eq, hpos, not_false_eq_true, not_true_eq_false, ite_false, hc, hw, hfirst, hmem1, Ptr.noConfusion, true_and,
72    ite_true, hadd, hsub', hmem2, hput]
73  cases dl <;> simp [hsub] <;> exact (show _ from hput)
74
75theorem ring_copy_extract (D a : Array UInt8) (off wn wh : Nat)
76    (hwn : wn ≤ wh) (ha : wh ≤ a.size) (hd : off + wh ≤ D.size) :
77    getDictBytes D a off wn wh =
78      D.extract 0 off ++ (a.extract wn wh ++ a.extract 0 wn) ++ D.extract (off + wh) D.size := by
79  apply Array.ext_getElem?
80  intro i
81  have hfit1 : off + (wh - wn) ≤ D.size := by omega
82  have hs1 : (copyRange D a off wn (wh - wn)).size = D.size := size_copyRange ..
83  have hfit2 : off + wh - wn + wn ≤ (copyRange D a off wn (wh - wn)).size := by rw [hs1]; omega
84  unfold getDictBytes
85  rw [getElem?_copyRange _ _ _ _ _ _ hfit2, getElem?_copyRange _ _ _ _ _ _ hfit1]
86  have hs0 : min off D.size = off := Nat.min_eq_left (by omega)
87  have hs2 : min wh a.size = wh := Nat.min_eq_left ha
88  have hs3 : min wn a.size = wn := Nat.min_eq_left (by omega)
89  by_cases h0 : i < off
90  · simp [Array.getElem?_append, Array.getElem?_extract, Array.size_extract, hs0, hs2, hs3,
91      h0, show ¬ off + wh - wn ≤ i by omega, show ¬ off ≤ i by omega, show i < D.size by omega]
92  · by_cases h1 : i < off + (wh - wn)
93    · have hx : wn + (i-off) < a.size := by omega
94      simp [Array.getElem?_append, Array.getElem?_extract, Array.size_extract, hs0, hs2, hs3,
95        h0, h1, show off ≤ i by omega, show ¬ off + wh - wn ≤ i by omega,
96        show i - off < wh - wn by omega, getElem!_pos a (wn + (i-off)) hx]
97    · by_cases h2 : i < off + wh
98      · have hx : i - (off + (wh - wn)) < a.size := by omega
99        simp [Array.getElem?_append, Array.getElem?_extract, Array.size_extract, hs0, hs2, hs3,
100          h0, h1, h2, show off ≤ i by omega, show off + wh - wn ≤ i by omega,
101          show i < off + wh - wn + wn by omega, show ¬ i - off < wh - wn by omega,
102          show i - off - (wh - wn) < wn by omega,
103          show i - (off + wh - wn) = i - off - (wh - wn) by omega,
104          getElem!_pos a (i - off - (wh - wn)) (by omega)]
105      · by_cases h3 : i < D.size
106        · simp [Array.getElem?_append, Array.getElem?_extract, Array.size_extract, hs0, hs2, hs3,
107            h0, h1, h2, h3, show ¬ i < off + wh - wn + wn by omega,
108            show ¬ i - off < wh - wn by omega,
109            show ¬ i - off - (wh - wn) < wn by omega,
110            show i - off - (wh - wn) - wn < D.size - (off + wh) by omega,
111            show off + wh + (i - off - (wh - wn) - wn) = i by omega]
112        · have hout : D[i]? = none := Array.getElem?_eq_none (by omega)
113          simp [Array.getElem?_append, Array.getElem?_extract, Array.size_extract, hs0, hs2, hs3,
114            h0, h1, h2, h3, show ¬ i < off + wh - wn + wn by omega,
115            show ¬ i - off < wh - wn by omega,
116            show ¬ i - off - (wh - wn) < wn by omega,
117            show ¬ i - off - (wh - wn) - wn < D.size - (off + wh) by omega, hout]
118
119end Zlib.Inflate.Proofs