public-inflate-header.lean

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

1import ZlibF.Spec.Public.Lifecycle
2import ZlibF.Proof.«inflate.c.base»
3
4namespace ZlibF.Spec.Public.InflateHeaderProof
5open C Zlib.Inflate Zlib.Inflate.Spec Zlib.Inflate.Proofs
6
7theorem inflateGetHeader_nogzip {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState}
8    (hL : Live h r zs z st) (head : GzHeaderPtr) (hw : st.wrap &&& 2 = 0) :
9    C.run (inflateGetHeader (some r) head) h = .ok (Z_STREAM_ERROR, h) := by
10  show inflateGetHeader (some r) head h = _
11  unfold inflateGetHeader
12  isimp [stateCheck_live hL, hL.zst, hL.hz, hL.hs, hw]
13
14/-- The state record after a successful `inflateGetHeader`: only `head` changes. -/
15def getHeaderState (head : GzHeaderPtr) (st : InflateState) : InflateState := { st with head := head }
16
17
18theorem inflateGetHeader_record {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState}
19    (hl : Live h r zs z st) {g : GzHeaderRef} {gh : GzHeader}
20    (hg : g.get h = some gh) (hw : st.wrap &&& 2 ≠ 0) :
21    C.run (inflateGetHeader (some r) (some g)) h =
22      .ok (Z_OK, g.put (setI h zs (getHeaderState (some g) st)) { gh with done := 0 }) := by
23  have hg1 : g.get (setI h zs (getHeaderState (some g) st)) = some gh := by
24    cases g with | tab i => simp [GzHeaderRef.get, setI] at hg ⊢; exact hg
25  show inflateGetHeader (some r) (some g) h = _
26  unfold inflateGetHeader
27  have hro : g.isRo = false := by cases g; rfl
28  have hg' : GzHeaderRef.get (setI h zs { st with head := some g }) g = some gh := hg1
29  isimp [stateCheck_live hl, hl.zst, hl.hz, hl.hs, hw, getHeaderState, ldGzHeader_ok hg', stGzHeader_ok hg' hro]
30
31
32/-- `int inflateGetHeader(z_streamp strm, gz_headerp head)`
33The exact public result, state, frame and ownership contract. -/
34theorem getheader_public : Goal.inflateGetHeader := by
35  intro h r i z s head hv hheader
36  rcases hv with ⟨hz,hstate,hi,hback,ha,hf,hlo,hhi⟩
37  have hl : Live h r i z s := ⟨hz,hi,hstate,hback,⟨hlo,hhi⟩,ha,hf⟩
38  by_cases hw : s.wrap &&& 2 = 0
39  · exact ⟨Z_STREAM_ERROR, h, inflateGetHeader_nogzip hl head hw, by simp [hw]⟩
40  · obtain ⟨g, gh, hptr, hgh⟩ := hheader hw
41    subst head
42    refine ⟨Z_OK, (GzHeaderRef.tab g).put (setI h i (getHeaderState (some (.tab g)) s)) { gh with done := 0 }, ?_, ?_⟩
43    · simpa [GzHeaderRef.get, GzHeaderRef.put, getHeaderState, setI, putInflate] using
44        inflateGetHeader_record hl (g := .tab g) (gh := gh) hgh hw
45    · simp [hw, hgh, GzHeaderRef.put, getHeaderState, setI, putInflate]
46
47
48#print axioms getheader_public
49end ZlibF.Spec.Public.InflateHeaderProof