inflate.c.main.common.lean

Lean source with line numbers. Follow a line number to locate a statement, or an import to read its dependency.

1import ZlibF.Proof.«inflate.c.main.simple»
2import ZlibF.Proof.«zutil.c»
3
4/-!
5# inflate.c: access to the state and the stream from a mode
6
7The access functions of a mode (`rdS`, `wrS`, `rdZ`, `wrZ`, `setMsg`, `setMode`, `inflate_fixed`) as `runX` rules. The
8context of a mode is `Env`: the state record `s` at table entry `zs`, and the stream record `z` at `r`. The heap after
9`badMode` is `badHeap`.
10-/
11
12namespace Zlib.Inflate.Proofs
13open C Zlib.Inflate Zlib.Inflate.Spec
14
15/-- The mode context: `c` names the stream `r` and the state entry `zs`, which hold `z` and `s` in `h`. -/
16structure Env (c : Ctx) (h : Heap) (r : ZStreamRef) (zs : Nat) (z : ZStream) (s : InflateState) : Prop where
17  strm : c.strm = some r
18  st : c.st = some (.tab zs)
19  hz : r.get h = some z
20  hs : h.istates zs = some s
21
22theorem runX_rdS {c : Ctx} {h : Heap} {r zs z s} {α : Type} (E : Env c h r zs z s) (f : InflateState → α) (l : IL) :
23    runX (monadLift (rdS c.st f) : X α) l h = .ok ((.ok (f s), l), h) := by
24  apply runX_lift_ok
25  rw [E.st, rdI_eq, E.hs]
26
27theorem runX_ldS {c : Ctx} {h : Heap} {r zs z s} (E : Env c h r zs z s) (l : IL) :
28    runX (monadLift (ldInflateState c.st) : X InflateState) l h = .ok ((.ok s, l), h) := by
29  apply runX_lift_ok
30  rw [E.st]; exact ldInflateState_tab E.hs
31
32theorem runX_wrS {c : Ctx} {h : Heap} {r zs z s} (E : Env c h r zs z s) (f : InflateState → InflateState) (l : IL) :
33    runX (monadLift (wrS c.st f) : X Unit) l h = .ok ((.ok (), l), setI h zs (f s)) := by
34  apply runX_lift_ok
35  rw [E.st, wrI_eq, E.hs]
36
37theorem runX_setMode {c : Ctx} {h : Heap} {r zs z s} (E : Env c h r zs z s) (m : UInt32) (l : IL) :
38    runX (monadLift (setMode c.st m) : X Unit) l h = .ok ((.ok (), l), setI h zs { s with mode := m }) := by
39  apply runX_lift_ok
40  rw [E.st]; exact setMode_tab E.hs m
41
42/-- The heap after `strm->msg = "..."; state->mode = BAD;` for the literal at string index `i`. -/
43def badHeap (h : Heap) (r : ZStreamRef) (zs : Nat) (z : ZStream) (s : InflateState) (i : Nat) : Heap :=
44  setI (r.put h { z with msg := .ref (.str i) 0 }) zs { s with mode := BAD }
45
46theorem Env.put {c : Ctx} {h : Heap} {r zs z s} (E : Env c h r zs z s) (v : ZStream) :
47    Env c (r.put h v) r zs v s :=
48  ⟨E.strm, E.st, ZStreamRef.get_put_same E.hz v, by simpa using E.hs⟩
49
50/-- `badMode c msg` for a literal of the sources. -/
51theorem badMode_run {c : Ctx} {h : Heap} {r zs z s} (E : Env c h r zs z s) {msg : String} (hm : msg ∈ strTable) :
52    ∃ i, strTable[i]? = some msg ∧ badMode c msg h = .ok ((), badHeap h r zs z s i) := by
53  obtain ⟨i, hi, hi'⟩ := Zlib.Zutil.Proofs.strLit_run h msg hm
54  refine ⟨i, hi', ?_⟩
55  have hz : ldZStream c.strm h = .ok (z, h) := by rw [E.strm, ldZ_eq, E.hz]
56  have hst : stZStream c.strm { z with msg := .ref (.str i) 0 } h = .ok ((), r.put h { z with msg := .ref (.str i) 0 }) := by
57    rw [E.strm]; exact stZStream_ok E.hz (by cases r <;> rfl)
58  have hE := E.put { z with msg := .ref (.str i) 0 }
59  unfold badMode setMsg
60  rw [bind_app]
61  simp only [Zlib.Zutil.Proofs.litHeap] at hi
62  simp only [bind_app, hi, hz, hst]
63  have := setMode_tab (m := BAD) hE.hs
64  rw [E.st]
65  simpa [badHeap] using this
66
67theorem runX_badMode {c : Ctx} {h : Heap} {r zs z s} (E : Env c h r zs z s) {msg : String} (hm : msg ∈ strTable) (l : IL) :
68    ∃ i, strTable[i]? = some msg ∧ runX (monadLift (badMode c msg) : X Unit) l h = .ok ((.ok (), l), badHeap h r zs z s i) := by
69  obtain ⟨i, hi, he⟩ := badMode_run E hm
70  exact ⟨i, hi, runX_lift_ok he l⟩
71
72/-- The state after `inflate_fixed`. -/
73def fixedState (s : InflateState) : InflateState :=
74  { s with
75    lencode := Ptr.ref CodeRef.st_lenfix 0
76    lenbits := 9
77    distcode := Ptr.ref CodeRef.st_distfix 0
78    distbits := 5 }
79
80/-- `inflate_fixed(state)`: the static tables become the current ones. -/
81theorem inflate_fixed_tab {h : Heap} {zs : Nat} {s : InflateState} (e : h.istates zs = some s) :
82    Zlib.Inftrees.inflate_fixed (some (.tab zs)) h = .ok ((), setI h zs (fixedState s)) := by
83  unfold Zlib.Inftrees.inflate_fixed
84  simp only [bind_app, ldInflateState_tab e, stInflateState_tab e]
85  simp [setI, ldInflateState_tab, stInflateState_tab, upd_upd]
86  rfl
87
88theorem runX_fixed {c : Ctx} {h : Heap} {r zs z s} (E : Env c h r zs z s) (l : IL) :
89    runX (monadLift (Zlib.Inftrees.inflate_fixed c.st) : X Unit) l h = .ok ((.ok (), l), setI h zs (fixedState s)) := by
90  apply runX_lift_ok
91  rw [E.st]; exact inflate_fixed_tab E.hs
92
93end Zlib.Inflate.Proofs