public-deflate-small-queries.lean

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

1import ZlibF.Spec.Public.StreamQueries
2import ZlibF.Proof.«deflate.c.base»
3
4namespace ZlibF.Spec.Public.DeflateQueryProof
5open C Zlib.Deflate Zlib.Deflate.Spec Zlib.Deflate.Proofs
6
7theorem refused_deflate_dom {h : Heap} {p : ZStreamPtr} (hr : RefusedDeflate h p) : StreamDom h p := by
8  rcases hr with hnull | ⟨r,z,rfl,hz,hbad⟩
9  · exact Or.inl hnull
10  · refine Or.inr ⟨r,z,rfl,hz,?_⟩
11    rcases hbad with hza | hzf | hs | ⟨i,s,hstate,hsi,_⟩
12    · exact Or.inl hza
13    · exact Or.inr (Or.inl hzf)
14    · exact Or.inr (Or.inr (Or.inl hs))
15    · exact Or.inr (Or.inr (Or.inr ⟨i,s,hstate,hsi⟩))
16
17theorem refused_deflate_not_init {h : Heap} {p : ZStreamPtr} (hr : RefusedDeflate h p) : ¬ DInitialised h p := by
18  intro ⟨r',i',z',s',hp,hL⟩
19  rcases hr with hn | ⟨r,z,hp',hz,hbad⟩
20  · rw [hn] at hp; cases hp
21  · rw [hp'] at hp
22    cases hp
23    have heq : z = z' := Option.some.inj (hz.symm.trans hL.hz)
24    subst z'
25    rcases hbad with ha | hf | hstate | ⟨i,s,hi,hs,hfail⟩
26    · exact hL.zalloc ha
27    · exact hL.zfree hf
28    · have hh := hL.zst
29      rw [hstate] at hh; cases hh
30    · have hieq : i = i' := by
31        have hh := hL.zst
32        rw [hi] at hh
33        cases hh
34        rfl
35      subst i'
36      have hseq : s = s' := Option.some.inj (hs.symm.trans hL.hs)
37      subst s'
38      rcases hfail with hback | hstatus
39      · exact hback hL.back
40      · exact hstatus hL.status
41
42theorem view_dlive {h : Heap} {r : ZStreamRef} {i : Nat} {z : ZStream} {s : DeflateState}
43    (hv : DeflateView h r i z s) : DLive h r i z s := by
44  rcases hv with ⟨hz,hstate,hi,hback,ha,hf,hstatus⟩
45  exact ⟨hz,hi,hstate,hback,hstatus,ha,hf⟩
46
47/-- `int deflateUsed(z_streamp strm, int *bits)` reads the optional bit count. -/
48theorem used_public : Goal.deflateUsed := by
49  intro bits
50  constructor
51  · intro h p hr
52    unfold deflateUsed
53    exact check_refuse (refused_deflate_dom hr) (refused_deflate_not_init hr) _ _
54  · intro h r i z s hv
55    have hl := view_dlive hv
56    show deflateUsed (some r) bits h = _
57    unfold deflateUsed
58    dsimp' [stateCheck_live hl, hl.zst, hl.hz, hl.hs]
59
60/-- `int deflateTune(z_streamp strm, int good_length, int max_lazy, int nice_length, int max_chain)` updates four tuning fields. -/
61theorem tune_public : Goal.deflateTune := by
62  intro good lazy nice chain
63  constructor
64  · intro h p hr
65    unfold deflateTune
66    exact check_refuse (refused_deflate_dom hr) (refused_deflate_not_init hr) _ _
67  · intro h r i z s hv
68    have hl := view_dlive hv
69    show deflateTune (some r) good lazy nice chain h = _
70    unfold deflateTune
71    dsimp' [stateCheck_live hl, hl.zst, hl.hz, hl.hs, putDeflate, setD]
72
73/-- `int deflateSetHeader(z_streamp strm, gz_headerp head)` stores the header only for gzip streams. -/
74theorem header_public : Goal.deflateSetHeader := by
75  intro head
76  constructor
77  · intro h p hr
78    unfold deflateSetHeader
79    exact check_refuse (refused_deflate_dom hr) (refused_deflate_not_init hr) _ _
80  · intro h r i z s hv
81    have hl := view_dlive hv
82    show deflateSetHeader (some r) head h = _
83    unfold deflateSetHeader
84    by_cases hw : s.wrap = 2
85    · dsimp' [stateCheck_live hl, hl.zst, hl.hz, hl.hs, putDeflate, setD, hw]
86    · dsimp' [stateCheck_live hl, hl.zst, hl.hz, hl.hs, hw]
87
88def pendingResult (d : DeflateState) (hasPending hasBits : Bool) : Int32 × Option UInt32 × Option Int32 :=
89  let bits := if hasBits then some d.bi_valid else none
90  if hasPending then
91    if d.pending.toUInt32.toUInt64 != d.pending then (Z_BUF_ERROR, some 0xffffffff, bits)
92    else (Z_OK, some d.pending.toUInt32, bits)
93  else (Z_OK, none, bits)
94
95theorem deflatePending_run {h : Heap} {r : ZStreamRef} {ds : Nat} {z : ZStream} {d : DeflateState}
96    (hL : DLive h r ds z d) (hasPending hasBits : Bool) :
97    deflatePending (some r) hasPending hasBits h = .ok (pendingResult d hasPending hasBits, h) := by
98  unfold deflatePending
99  cases hasPending <;> cases hasBits <;> dsimp' [stateCheck_live hL, hL.zst, hL.hz, hL.hs, pendingResult] <;>
100    split <;> simp_all
101
102
103theorem pending_cast_iff (x : UInt64) :
104    x.toUInt32.toUInt64 = x ↔ x.toNat < 2 ^ 32 := by
105  constructor
106  · intro he
107    have hn := congrArg UInt64.toNat he
108    rw [UInt32.toNat_toUInt64, UInt64.toNat_toUInt32] at hn
109    have hm := Nat.mod_lt x.toNat (by decide : 0 < 2 ^ 32)
110    rw [hn] at hm
111    exact hm
112  · intro hn
113    apply UInt64.toNat_inj.mp
114    rw [UInt32.toNat_toUInt64, UInt64.toNat_toUInt32, Nat.mod_eq_of_lt hn]
115
116/-- `int deflatePending(z_streamp strm, unsigned *pending, int *bits)` returns
117the exact public result for an accepted state, including oversized pending
118counts and both optional outputs. It does not modify the heap. -/
119theorem deflatePending_public {h : Heap} {r : ZStreamRef} {i : Nat} {z : ZStream} {s : DeflateState}
120    (hl : DLive h r i z s) (pending bits : Bool) :
121    C.run (deflatePending (some r) pending bits) h =
122      .ok (((if pending ∧ 2 ^ 32 ≤ s.pending.toNat then Z_BUF_ERROR else Z_OK),
123        if pending then some (if 2 ^ 32 ≤ s.pending.toNat then 0xffffffff else s.pending.toUInt32) else none,
124        if bits then some s.bi_valid else none), h) := by
125  have hr := deflatePending_run hl pending bits
126  have hc := pending_cast_iff s.pending
127  by_cases hp : pending = true
128  · subst pending
129    by_cases ho : 2 ^ 32 ≤ s.pending.toNat
130    · have hne : s.pending.toUInt32.toUInt64 ≠ s.pending := fun he => by have := hc.mp he; omega
131      have hr' := hr
132      simp only [pendingResult, ite_true, bne_iff_ne] at hr'
133      split at hr'
134      · simpa [C.run, ho] using hr'
135      · rename_i hc2
136        exact (hc2 hne).elim
137    · have he : s.pending.toUInt32.toUInt64 = s.pending := hc.mpr (by omega)
138      simpa [C.run, pendingResult, he, ho] using hr
139  · have hp' : pending = false := by cases pending <;> simp_all
140    subst pending
141    simpa [C.run, pendingResult] using hr
142
143
144/-- `int deflatePending(z_streamp strm, unsigned *pending, int *bits)` returns both optional values and detects a 32-bit overflow. -/
145theorem pending_public : Goal.deflatePending := by
146  intro pending bits
147  constructor
148  · intro h p hr
149    unfold deflatePending
150    exact check_refuse (refused_deflate_dom hr) (refused_deflate_not_init hr) _ _
151  · intro h r i z state hv
152    exact deflatePending_public (view_dlive hv) pending bits
153
154#print axioms pending_public
155#print axioms used_public
156#print axioms tune_public
157#print axioms header_public
158end ZlibF.Spec.Public.DeflateQueryProof