public-inflate-reset.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.Lifecycle
2import ZlibF.Proof.«inflate.c.reset»
3
4open C Zlib.Inflate Zlib.Inflate.Spec Zlib.Inflate.Proofs ZlibF.Spec.Public ZlibF.Spec
5
6namespace ZlibF.Spec.Public.InflateResetProof
7
8theorem drop_matches_freewin (h : Heap) (p : BPtr) : dropWindow h p = freeWin h p := by
9  cases p with
10  | null => rfl
11  | ref r off =>
12    cases r <;> cases off <;> rfl
13
14/-- `int inflateReset(z_streamp strm)`
15The exact public result, state, frame and ownership contract. -/
16theorem reset_public : Goal.inflateReset := by
17  intro h r i z s hv hf hwin
18  rcases hv with ⟨hz,hstate,hi,hback,ha,hfree,hlo,hhi⟩
19  have hl : Live h r i z s := ⟨hz,hi,hstate,hback,⟨hlo,hhi⟩,ha,hfree⟩
20  have hw : WindowOk h s.window := hwin
21  have hr := inflateReset_run hl hf (Or.inr hw)
22  by_cases hbits : s.wbits = s.reqbits
23  · simpa [C.run, hbits, resetHeap, resetPre, inflateResetPre, resetKeepState,
24      inflateResetState, resetKeepStream, inflateResetStream, setI, putInflate, i2ul] using hr
25  · by_cases hwrap : s.reqwrap = 0
26    · simpa [C.run, hbits, hwrap, drop_matches_freewin, resetHeap, resetPre, inflateResetPre, resetKeepState,
27        inflateResetState, resetKeepStream, inflateResetStream, setI, putInflate, i2ul] using hr
28    · simpa [C.run, hbits, hwrap, drop_matches_freewin, resetHeap, resetPre, inflateResetPre, resetKeepState,
29        inflateResetState, resetKeepStream, inflateResetStream, setI, putInflate, i2ul] using hr
30
31#print axioms reset_public
32
33end ZlibF.Spec.Public.InflateResetProof