public-infback-end.lean

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

1import ZlibF.Spec.Public.Back
2import ZlibF.Proof.«infback.c.end»
3
4namespace ZlibF.Spec.Public.InflateBackEndProof
5open C Zlib.Inflate Zlib.Inflate.Spec Zlib.Inflate.Proofs Zlib.Infback Zlib.Infback.Spec Zlib.Infback.Proofs
6
7theorem inflateBackEnd_record {h : Heap} {r : ZStreamRef} {i : Nat} {z : ZStream} {s : InflateState}
8    (hz : r.get h = some z) (hs : h.istates i = some s)
9    (hstate : z.state = some (.inflate i)) (hfree : z.zfree = .fn "zcfree") :
10    C.run (inflateBackEnd (some r)) h = .ok (Z_OK, backEndHeap h r z i) := by
11  show inflateBackEnd (some r) h = _
12  unfold inflateBackEnd
13  have hz0 : z.zfree ≠ .null := by rw [hfree]; intro c; cases c
14  have hs0 : z.state ≠ none := by rw [hstate]; intro c; cases c
15  isimp [hz, hs0, hz0, hstate, hfree, zfrees_run hz hfree hs, backEndHeap]
16
17
18/-- `int inflateBackEnd(z_streamp strm)`
19The exact public result, state, frame and ownership contract. -/
20theorem back_end_public : Goal.inflateBackEnd := by
21  refine ⟨fun h => inflateBackEnd_nullstream h, ?_, ?_⟩
22  · intro h r z hz hn
23    exact inflateBackEnd_refused hz hn
24  · intro h r i z s hv
25    rcases hv with ⟨hz, hs, hstate, halloc, hfree, hwf, hwlo, hwhi, hwsize, hwne, hwrite, hfresh, huniq, hglobal⟩
26    let after := backEndHeap h r z i
27    refine ⟨after, inflateBackEnd_record hz hs hstate hfree, ?_, ?_, ?_, ?_, ?_⟩
28    · simp [after, backEndHeap, hz]
29    · have ho : h.Owns (fun b => h.live b) := fun _ => Iff.rfl
30      have hfreeown := owns_freeIst huniq hs ho
31      have hz' : r.get (freeIst h i) = some z := by simpa using hz
32      have hafter := (shape_put hz' { z with state := none }).owns hfreeown
33      intro b
34      simpa [LiveChange, after, backEndHeap] using hafter b
35    · cases r with
36      | tab j =>
37        have hjz : h.streams j = some z := hz
38        simp only [Frame, after, backEndHeap, freeIst, ZStreamRef.put, hjz]
39        simp only [true_and]
40        refine ⟨Nat.le_refl _, Nat.le_refl _, ?_⟩
41
42        intro b hl hb
43        have hi : b ≠ i := fun e => hb (Or.inr e)
44        have hj : b ≠ j := fun e => hb (Or.inl (by simpa [StreamRoot] using e))
45        simp [upd_ne, hi, hj]
46      | in_gzstate_strm j =>
47        cases he : h.gzstates j with
48        | none => simp [ZStreamRef.get, he] at hz
49        | some g =>
50          simp only [Frame, after, backEndHeap, freeIst, ZStreamRef.put, he]
51          simp only [true_and]
52          refine ⟨Nat.le_refl _, Nat.le_refl _, ?_⟩
53
54          intro b hl hb
55          have hi : b ≠ i := fun e => hb (Or.inr e)
56          have hj : b ≠ j := fun e => hb (Or.inl (by simpa [StreamRoot] using e))
57          simp [upd_ne, hi, hj]
58    · cases r with
59      | tab j =>
60        have hjz : h.streams j = some z := hz
61        simp [after, backEndHeap, ZStreamRef.put, freeIst, hjz]
62      | in_gzstate_strm j =>
63        cases he : h.gzstates j <;> simp [after, backEndHeap, ZStreamRef.put, freeIst, he]
64    · cases r with
65      | tab j =>
66        have hjz : h.streams j = some z := hz
67        simp [after, backEndHeap, ZStreamRef.put, freeIst, hjz]
68      | in_gzstate_strm j =>
69        cases he : h.gzstates j <;> simp [after, backEndHeap, ZStreamRef.put, freeIst, he]
70
71
72#print axioms back_end_public
73end ZlibF.Spec.Public.InflateBackEndProof