public-gzeof.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.GzControl
2import ZlibF.Proof.«gzlib.c.base»
3
4namespace ZlibF.Spec.Public.Proofs
5open C Zlib.GzFs Zlib.Gzguts Zlib.Gzlib Zlib.Gzlib.Spec Zlib.Gzlib.Proofs
6
7/-- `int gzeof(gzFile file)` reads an existing state record and leaves the heap unchanged. -/
8theorem gzeof_record {h : Heap} {i : Nat} {s : GzState} (hs : h.gzstates i = some s) :
9    C.run (gzeof (hnd i)) h = .ok ((if s.mode = GZ_READ then s.past else 0), h) := by
10  unfold C.run gzeof
11  by_cases hr : s.mode = GZ_READ
12  · gsimp [hs, hr]
13  · by_cases hw : s.mode = GZ_WRITE
14    · gsimp [hs, hr, hw]
15    · gsimp [hs, hr, hw]
16
17/-- `int gzeof(gzFile file)` satisfies the complete public goal. -/
18theorem gzeof_public : Goal.gzeof := by
19  constructor
20  · intro h
21    rfl
22  · intro h i s hs
23    exact gzeof_record hs
24
25#print axioms gzeof_record
26#print axioms gzeof_public
27
28end ZlibF.Spec.Public.Proofs