gzlib.c.public-clearerr.lean

本页保留 Lean 源码及行号。点击行号可定位语句，点击 import 中的模块名可查看依赖。

1import ZlibF.Spec.Public.GzControl
2import ZlibF.Proof.«gzlib.c.simple»
3
4namespace ZlibF.Spec.Public.Proofs
5open C Zlib.GzFs Zlib.Gzguts Zlib.Gzlib Zlib.Gzlib.Spec Zlib.Gzlib.Proofs
6
7private theorem gzclearerr_record {h : Heap} {i : Nat} {s : GzState}
8    (hs : h.gzstates i = some s) (hm : s.mode = GZ_READ ∨ s.mode = GZ_WRITE)
9    (hmsg : s.msg = .null ∨ ∃ b a, s.msg = .ref (.blk b) 0 ∧
10      h.bytes b = some a ∧ h.ro b = false)
11    (hmem : s.err = Z_MEM_ERROR → s.msg = .null) :
12    C.run (gzclearerr (hnd i)) h =
13      .ok ((), setS (freeStr h s.msg) i (errNull (clearRec s) Z_OK)) := by
14  unfold C.run gzclearerr
15  rcases hmsg with hn | ⟨mb, a, hp, ha, hro⟩
16  · rcases hm with hmode | hmode <;>
17      gsimp [hs, hn, hmode, gz_error, clearRec, errNull, GZ_READ, GZ_WRITE]
18  · have hne : s.err ≠ Z_MEM_ERROR := fun he => by
19      have hnull := hmem he
20      rw [hp] at hnull
21      cases hnull
22    rcases hm with hmode | hmode <;>
23      gsimp [hs, hp, hne, hmode, freeB_blk_setS ha hro, freeB_blk_run ha hro,
24        gz_error, clearRec, errNull, GZ_READ, GZ_WRITE]
25
26/-- `void gzclearerr(gzFile file)` clears the error, frees the message, and
27rearms end-of-file reporting for a reader, under the public handle contract. -/
28theorem gzclearerr : Goal.gzclearerr := by
29  constructor
30  · intro h
31    exact gzclearerr_null h
32  · intro h i s hv
33    rcases hv with ⟨hs, hm, _, _, _, _, hmsg, hmem, _⟩
34    have hm' : s.msg = .null ∨ ∃ b a, s.msg = .ref (.blk b) 0 ∧
35        h.bytes b = some a ∧ h.ro b = false := by
36      rcases hmsg with hnull | ⟨_, _, b, a, hp, ha, hro, _⟩
37      · exact Or.inl hnull
38      · exact Or.inr ⟨b, a, hp, ha, hro⟩
39    have heq : freeStr h s.msg = dropWindow h s.msg := by
40      rcases hm' with hnull | ⟨b, a, hp, ha, hro⟩
41      · simp [hnull, freeStr, dropWindow]
42      · simp [hp, freeStr, dropWindow]
43    have hr := gzclearerr_record hs hm hm' hmem
44    rw [heq] at hr
45    rcases hm with hread | hwrite
46    · simpa [hnd, putGz, setS, clearRec, errNull, hread] using hr
47    · simpa [hnd, putGz, setS, clearRec, errNull, hwrite, GZ_READ, GZ_WRITE] using hr
48
49end ZlibF.Spec.Public.Proofs