inflate.c.main.simple.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.macros»
2
3/-!
4# inflate.c: the modes that touch only the registers and the state record
5
6`DONE` and `LIT`. A mode theorem is stated for a mode function run by `runX` from registers `l` on heap `h`; the
7state record is `s` at table entry `zs` (`c.st = some (.tab zs)`). The heap after a write is `setI` of the base module.
8-/
9
10namespace Zlib.Inflate.Proofs
11open C Zlib.Inflate Zlib.Inflate.Spec
12
13theorem wrS_tab {h : Heap} {zs : Nat} {s : InflateState} (e : h.istates zs = some s) (f : InflateState → InflateState) :
14    wrS (some (.tab zs)) f h = .ok ((), setI h zs (f s)) := by
15  unfold wrS
16  rw [bind_app, ldInflateState_tab e]
17  simp only []
18  rw [stInflateState_tab e]
19  rfl
20
21theorem setMode_tab {h : Heap} {zs : Nat} {s : InflateState} (e : h.istates zs = some s) (m : UInt32) :
22    setMode (some (.tab zs)) m h = .ok ((), setI h zs { s with mode := m }) := wrS_tab e _
23
24/-- `case DONE:` -- `ret = Z_STREAM_END; goto inf_leave`. -/
25theorem inflate_DONE_run (c : Ctx) (l : IL) (h : Heap) :
26    runX (inflate_DONE c) l h = .ok ((.error Ex.leave, { l with ret := Z_STREAM_END }), h) := rfl
27
28/-- `case LIT:` with no room (`left = 0`): `goto inf_leave`, nothing changes. -/
29theorem inflate_LIT_full (c : Ctx) (l : IL) (h : Heap) (h0 : l.left = 0) :
30    runX (inflate_LIT c) l h = .ok ((.error Ex.leave, l), h) := by
31  unfold inflate_LIT
32  rw [runX_bind, runX_get]
33  simp [h0, runX_throw, runX_bind]
34
35/-- `case LIT:` with room: the byte `state->length` is stored at `put` (a writable caller byte block), `put` and `left`
36move, and the mode becomes `LEN`. The only heap changes are that byte block and the state record. -/
37theorem inflate_LIT_run {c : Ctx} {l : IL} {h : Heap} {zs : Nat} {s : InflateState} {b off : Nat} {a : Array UInt8}
38    (hc : c.st = some (.tab zs)) (hs : h.istates zs = some s) (hl : l.left ≠ 0) (hp : l.put = .ref (.blk b) off)
39    (ha : h.bytes b = some a) (hro : Space.ro h (BRef.blk b) = false) (hoff : off < a.size) :
40    runX (inflate_LIT c) l h = .ok ((.ok (), { l with put := .ref (.blk b) (off + 1), left := l.left - 1 }),
41      setI { h with bytes := upd h.bytes b (some (a.set! off s.length.toUInt8)) } zs { s with mode := LEN }) := by
42  have hg : (Space.get h (BRef.blk b) : Option (Array UInt8)) = some a := ha
43  have hst : store8 l.put s.length.toUInt8 h = .ok ((), { h with bytes := upd h.bytes b (some (a.set! off s.length.toUInt8)) }) := by
44    rw [hp]; exact Ptr.store_ok hg hro hoff
45  have hadd : OkOn { h with bytes := upd h.bytes b (some (a.set! off s.length.toUInt8)) } (l.put.add 1) (.ref (.blk b) (off + 1)) := by
46    rw [hp]
47    have hg' : (Space.get { h with bytes := upd h.bytes b (some (a.set! off s.length.toUInt8)) } (BRef.blk b) : Option (Array UInt8))
48        = some (a.set! off s.length.toUInt8) := by
49      show (upd h.bytes b (some (a.set! off s.length.toUInt8))) b = _
50      simp
51    exact Ptr.add_nat_ok (n := 1) hg' (by simp; omega)
52  have hs' : ({ h with bytes := upd h.bytes b (some (a.set! off s.length.toUInt8)) } : Heap).istates zs = some s := hs
53  have hld : ldInflateState c.st h = .ok (s, h) := by rw [hc]; exact ldInflateState_tab hs
54  have hne : (l.left == 0) = false := by simpa using hl
55  unfold inflate_LIT
56  rw [runX_bind, runX_get]
57  simp only [hne, Bool.false_eq_true, ↓reduceIte]
58  rw [runX_bind, runX_lift_ok hld]
59  simp only []
60  rw [runX_bind, runX_lift_ok hst]
61  simp only []
62  rw [runX_bind, runX_lift_ok hadd]
63  simp only []
64  rw [runX_bind, runX_set]
65  simp only []
66  rw [hc]
67  have := runX_lift_ok (m := setMode (some (.tab zs)) LEN) (setMode_tab hs' LEN) { l with put := .ref (.blk b) (off + 1), left := l.left - 1 }
68  exact this
69
70end Zlib.Inflate.Proofs