public-inflate-reset-keep.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.base»
3
4namespace ZlibF.Spec.Public.InflateResetKeepProof
5open C Zlib.Inflate Zlib.Inflate.Spec Zlib.Inflate.Proofs
6
7/-- `int inflateResetKeep(z_streamp strm)` resets decode progress while retaining the window. -/
8theorem resetkeep_public : Goal.inflateResetKeep := by
9  intro h r i z s hv
10  rcases hv with ⟨hz, hstate, hi, hback, ha, hf, hlo, hhi⟩
11  have hl : Live h r i z s := ⟨hz, hi, hstate, hback, ⟨hlo, hhi⟩, ha, hf⟩
12  by_cases hw : s.wrap = 0
13  · simpa [C.run, setI, putInflate, resetKeepState, resetKeepStream, inflateResetState,
14      inflateResetStream, hw] using resetKeep_run hl
15  · simpa [C.run, setI, putInflate, resetKeepState, resetKeepStream, inflateResetState,
16      inflateResetStream, hw, i2ul] using resetKeep_run hl
17
18#print axioms resetkeep_public
19end ZlibF.Spec.Public.InflateResetKeepProof