inflate.c.public-setdict.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.«adler32.c.public-any»
3
4namespace Zlib.Inflate.Proofs
5open C Zlib.Inflate Zlib.Inflate.Spec Zlib.Adler32.Proofs ZlibF.Spec
6
7theorem adler32_dict_any {h : Heap} {ref : BRef} {off : Nat} {a : Array UInt8}
8    (ha : Space.get h ref = some a) (len : UInt32) (hf : off + len.toNat ≤ a.size) :
9    Zlib.Adler32.adler32 1 (.ref ref off) len h =
10      .ok ((ZlibF.Spec.adler32 (seg a off len.toNat)).toUInt64, h) := by
11  by_cases h1 : len.toNat = 1
12  · have he : len = 1 := UInt32.toNat_inj.mp (by simpa using h1)
13    subst len
14    have hr := adler32_z_one_public (h := h) (r := ref) (off := off) (bytes := a) ha (by simpa using hf) 1
15    change Zlib.Adler32.adler32 1 (.ref ref off) 1 h = .ok ((ZlibF.Spec.adler32 (seg a off 1)).toUInt64, h)
16    rw [seg_one]
17    unfold Zlib.Adler32.adler32
18    change C.run (Zlib.Adler32.adler32_z 1 (.ref ref off) 1) h = _
19    rw [hr]
20    congr 2
21    apply UInt64.toNat_inj.mp
22    have hb := UInt8.toNat_lt a[off]!
23    have hsmall : (1 + a[off]!.toNat) % 65521 = 1 + a[off]!.toNat := Nat.mod_eq_of_lt (by omega)
24    have h32 : (1 + a[off]!.toNat) * 65536 + (1 + a[off]!.toNat) < 2 ^ 32 := by omega
25    have h64 : (1 + a[off]!.toNat) + 65536 * (1 + a[off]!.toNat) < 2 ^ 64 := by omega
26    simp [ZlibF.Spec.adler32, ZlibF.Spec.adler32Update, ZlibF.Spec.adlerStep,
27      hsmall,
28      Nat.mod_eq_of_lt h32, Nat.mod_eq_of_lt h64, show ¬ 65521 ≤ 1 + a[off]!.toNat by omega]
29    omega
30  · have hr := adler32_any_format ha 1 off len hf h1
31    simpa [C.run, canonicalStart, ZlibF.Spec.adler32] using hr
32
33#print axioms adler32_dict_any
34end Zlib.Inflate.Proofs
35
36namespace Zlib.Inflate.Proofs
37open C Zlib.Inflate Zlib.Inflate.Spec Zlib.Adler32.Proofs ZlibF.Spec
38
39/-- `int inflateSetDictionary(z_streamp strm, const Bytef *dictionary, uInt dictLength)`
40rejects an incorrect dictionary without modifying the heap, for every represented
41readable byte object. The stream must be in DICT mode. -/
42theorem inflateSetDictionary_dataerr_any {H : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState}
43    {ref : BRef} {off : Nat} {data : Array UInt8} {len : UInt32}
44    (hl : Live H r zs z st) (hd : Space.get H ref = some data)
45    (hf : off + len.toNat ≤ data.size) (hm : st.mode = DICT)
46    (hbad : (ZlibF.Spec.adler32 (seg data off len.toNat)).toUInt64 ≠ st.check) :
47    C.run (inflateSetDictionary (some r) (.ref ref off) len) H = .ok (Z_DATA_ERROR, H) := by
48  have hnn : (Ptr.ref ref off == (Ptr.null : BPtr)) = false := by simp
49  have hra := adler32_dict_any hd len hf
50  have hne : ((ZlibF.Spec.adler32 (seg data off len.toNat)).toUInt64 != st.check) = true := by simpa using hbad
51  show inflateSetDictionary (some r) (.ref ref off) len H = _
52  unfold inflateSetDictionary
53  simp only [bind_app, stateCheck_live hl, ldZ_eq, ldI_eq, hl.hz, hl.zst, castI, hl.hs, hnn, bne_self_eq_false,
54    Bool.or_self, Bool.false_eq_true, ite_false, hm, beq_self_eq_true, Bool.and_false, ite_true]
55  simp only [adler32_init, hra, hne, ite_true]
56  rfl
57
58/-- `int inflateSetDictionary(z_streamp strm, const Bytef *dictionary, uInt dictLength)`
59rejects a null source or a wrapped stream outside DICT mode before reading the source. -/
60theorem inflateSetDictionary_refused_any {H : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState}
61    (hl : Live H r zs z st) (source : BPtr) (len : UInt32)
62    (hn : source = .null ∨ (st.wrap ≠ 0 ∧ st.mode ≠ DICT)) :
63    C.run (inflateSetDictionary (some r) source len) H = .ok (Z_STREAM_ERROR, H) := by
64  show inflateSetDictionary (some r) source len H = _
65  unfold inflateSetDictionary
66  rcases hn with hn | ⟨hw, hm⟩
67  · simp [bind_app, stateCheck_live hl, hn, pure_app]
68  · by_cases he : source = .null
69    · simp [bind_app, stateCheck_live hl, he, pure_app]
70    · simp [bind_app, stateCheck_live hl, ldZ_eq, ldI_eq, hl.hz, hl.zst, castI, hl.hs, he, hw, hm, pure_app]
71
72#print axioms inflateSetDictionary_dataerr_any
73#print axioms inflateSetDictionary_refused_any
74end Zlib.Inflate.Proofs
75
76namespace Zlib.Inflate.Proofs
77open C Zlib.Inflate Zlib.Inflate.Spec Zlib.Adler32.Proofs ZlibF.Spec
78
79/-- `int inflateSetDictionary(z_streamp strm, const Bytef *dictionary, uInt dictLength)`
80returns a memory error and sets MEM when allocating the missing window fails.
81The readable source can be any represented byte object. -/
82theorem inflateSetDictionary_alloc_fail_any {H : Heap} {r : ZStreamRef} {zs : Nat}
83    {z : ZStream} {st : InflateState} {ref : BRef} {off : Nat} {data : Array UInt8}
84    {len : UInt32} (hG : Good H r zs z st) (hza : z.zalloc = .fn "zcalloc")
85    (hd : Space.get H ref = some data) (hf : off + len.toNat ≤ data.size)
86    (hwrap : st.wrap = 0 ∨ st.mode = DICT)
87    (hcheck : st.mode = DICT → (ZlibF.Spec.adler32 (seg data off len.toNat)).toUInt64 = st.check)
88    (hw : st.window = .null) (hok : ¬ H.allocOk H.nalloc = true) :
89    C.run (inflateSetDictionary (some r) (.ref ref off) len) H =
90      .ok (Z_MEM_ERROR, setI (setI { H with nalloc := H.nalloc + 1 } zs st) zs { st with mode := MEM }) := by
91  have hl := hG.live
92  have hadd : Ptr.add (Ptr.ref ref off) (len.toNat : Int) H =
93      .ok (Ptr.ref ref (off + len.toNat), H) := Ptr.add_nat_ok hd hf
94  have hrun := uw_alloc_fail hl hza hG.inv.win.wbits hw hok (.ref ref (off + len.toNat)) len
95  have hs : (setI { H with nalloc := H.nalloc + 1 } zs st).istates zs = some st := by simp
96  have hnn : (Ptr.ref ref off == (Ptr.null : BPtr)) = false := by simp
97  show inflateSetDictionary (some r) (.ref ref off) len H = _
98  unfold inflateSetDictionary
99  simp only [bind_app, stateCheck_live hl, ldZ_eq, ldI_eq, hl.hz, hl.zst, castI, hl.hs, hnn,
100    bne_self_eq_false, Bool.or_self, Bool.false_eq_true, ite_false]
101  by_cases hm : st.mode = DICT
102  · have hra := adler32_dict_any hd len hf
103    have hck := hcheck hm
104    simp only [hm, beq_self_eq_true, Bool.and_false, ite_true, adler32_init, hra, hck,
105      bne_self_eq_false, Bool.false_eq_true, ite_false, hadd, hrun, bind_app, setMode, wrI_eq, hs, pure_app]
106    simp only [show ((1 : Int32) != 0) = true by decide, ite_true, bind_app, wrI_eq, hs, pure_app]
107  · have hw0 : st.wrap = 0 := hwrap.resolve_right hm
108    have hmb : (st.mode == DICT) = false := by simpa using hm
109    simp only [hmb, hw0, bne_self_eq_false, Bool.false_and, Bool.false_eq_true, ite_false,
110      Bool.and_false, hadd, hrun, bind_app, setMode, wrI_eq, hs, pure_app]
111    simp only [show ((1 : Int32) != 0) = true by decide, ite_true, bind_app, wrI_eq, hs, pure_app]
112    simp only [hw0]
113
114#print axioms inflateSetDictionary_alloc_fail_any
115
116/-- A failed window allocation leaves a valid stream in MEM mode. -/
117theorem inflateSetDictionary_alloc_fail_good {H : Heap} {r : ZStreamRef} {zs : Nat}
118    {z : ZStream} {st : InflateState} (hG : Good H r zs z st) :
119    Good (setI (setI { H with nalloc := H.nalloc + 1 } zs st) zs { st with mode := MEM })
120      r zs z { st with mode := MEM } := by
121  have hL := hG.live
122  have hI := hG.inv
123  have hz' : r.get { H with nalloc := H.nalloc + 1 } = some z := by
124    cases r <;> simpa [ZStreamRef.get] using hL.hz
125  have hg : Good (setI { H with nalloc := H.nalloc + 1 } zs st) r zs z st := by
126    have hs := good_set (h0 := { H with nalloc := H.nalloc + 1 }) (z0 := z) (z' := z)
127      (s0 := st) (st' := st) hL.hz hL.hs hG.uniq hG.fresh hL.zst hL.zalloc hL.zfree
128      hL.back hL.mode (StInv.congr (h := H) rfl rfl hI)
129    rwa [ZStreamRef.put_self hz'] at hs
130  exact good_state hg rfl mode_mem
131    (hg.inv.of_fields rfl rfl rfl rfl rfl rfl rfl rfl rfl hg.inv.bits rfl rfl rfl)
132
133#print axioms inflateSetDictionary_alloc_fail_good
134end Zlib.Inflate.Proofs