public-inflate-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.«inflate.c.base»
3
4namespace ZlibF.Spec.Public.InflateQueryProof
5open C Zlib.Inflate Zlib.Inflate.Spec Zlib.Inflate.Proofs
6
7theorem refused_dom {h : Heap} {p : ZStreamPtr} (hr : RefusedInflate 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_not_initialised {h : Heap} {p : ZStreamPtr} (hr : RefusedInflate h p) : ¬ Initialised 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 | hlo | hhi
39      · exact hback hL.back
40      · exact (UInt32.not_lt.mpr hL.mode.1) hlo
41      · exact (UInt32.not_lt.mpr hL.mode.2) hhi
42
43/-- `int inflateSyncPoint(z_streamp strm)` tests the stored-block boundary. -/
44theorem syncpoint_public : Goal.inflateSyncPoint := by
45  constructor
46  · intro h p hr
47    show inflateSyncPoint p h = _
48    unfold inflateSyncPoint
49    simp [bind_app, notInit_check (refused_dom hr) (refused_not_initialised hr), pure_app, Z_STREAM_ERROR]
50  · intro h r i z s hv
51    rcases hv with ⟨hz, hstate, hi, hb, ha, hf, hlo, hhi⟩
52    have hl : Live h r i z s := ⟨hz, hi, hstate, hb, ⟨hlo, hhi⟩, ha, hf⟩
53    show inflateSyncPoint (some r) h = _
54    unfold inflateSyncPoint
55    by_cases hc : s.mode = STORED ∧ s.bits = 0
56    · isimp [stateCheck_live hl, hl.zst, hl.hz, hl.hs, hc.1, hc.2]
57    · isimp [stateCheck_live hl, hl.zst, hl.hz, hl.hs, hc]
58
59/-- `int inflateUndermine(z_streamp strm, int subvert)` keeps strict distance checks. -/
60theorem undermine_public : Goal.inflateUndermine := by
61  intro subvert
62  constructor
63  · intro h p hr
64    show inflateUndermine p subvert h = _
65    unfold inflateUndermine
66    simp [bind_app, notInit_check (refused_dom hr) (refused_not_initialised hr), pure_app, Z_STREAM_ERROR]
67  · intro h r i z s hv
68    rcases hv with ⟨hz, hstate, hi, hb, ha, hf, hlo, hhi⟩
69    have hl : Live h r i z s := ⟨hz, hi, hstate, hb, ⟨hlo, hhi⟩, ha, hf⟩
70    show inflateUndermine (some r) subvert h = _
71    unfold inflateUndermine
72    isimp [stateCheck_live hl, hl.zst, hl.hz, hl.hs, putInflate, setI]
73
74/-- `int inflateValidate(z_streamp strm, int check)` changes both validation flags. -/
75theorem validate_public : Goal.inflateValidate := by
76  intro check
77  constructor
78  · intro h p hr
79    show inflateValidate p check h = _
80    unfold inflateValidate
81    simp [bind_app, notInit_check (refused_dom hr) (refused_not_initialised hr), pure_app, Z_STREAM_ERROR]
82  · intro h r i z s hv
83    rcases hv with ⟨hz, hstate, hi, hb, ha, hf, hlo, hhi⟩
84    have hl : Live h r i z s := ⟨hz, hi, hstate, hb, ⟨hlo, hhi⟩, ha, hf⟩
85    show inflateValidate (some r) check h = _
86    unfold inflateValidate
87    isimp [stateCheck_live hl, hl.zst, hl.hz, hl.hs, putInflate, setI]
88
89#print axioms syncpoint_public
90#print axioms undermine_public
91#print axioms validate_public
92end ZlibF.Spec.Public.InflateQueryProof