infback.c.room.lean

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

1import ZlibF.Proof.«infback.c.macros»
2import ZlibF.Proof.«inflate.c.main.simple»
3
4/-!
5# infback.c: `ROOM()` and the mode setters
6
7`ROOM()` hands the full window to `out` and starts again at its beginning. The call-back sees the window as `len` readable
8bytes; it may not change them (`CbContract`).
9-/
10
11namespace Zlib.Infback.Proofs
12open C Zlib.Inflate Zlib.Inflate.Spec Zlib.Inflate.Proofs Zlib.Infback Zlib.Infback.Spec
13
14/-- `ROOM()` while there is room: nothing happens. -/
15theorem ROOM_have (c : BCtx) {l : IL} {h : Heap} (hl : l.left ≠ 0) :
16    runX (ROOM c) l h = .ok ((.ok (), l), h) := by
17  have hb : (l.left == 0) = false := by simpa using hl
18  unfold ROOM
19  simp [runX_bind, runX_get, hb, hl, runX_pure]
20
21/-- The heap `ROOM()` sets before it calls `out`: `state->whave = state->wsize`. -/
22def roomHeap (h : Heap) (zs : Nat) (s : InflateState) : Heap := setI h zs { s with whave := s.wsize }
23
24/-- **`ROOM()` with a full window.** The state is the record `s` at block `zs`, its window is `wsize` readable bytes. `out` is
25called once on the window; it changes only its own blocks. If it returns 0 the fill restarts at the window, otherwise the call
26ends with `Z_BUF_ERROR`. -/
27theorem ROOM_run (c : BCtx) {win : Nat} {ownI ownO : Nat → Prop} {R : Heap → Prop}
28    (hK : CbContract c.inCb c.inDesc c.outCb c.outDesc win ownI ownO R) {l : IL} {h : Heap} {zs : Nat}
29    {s : InflateState} (hc : c.st = some (.tab zs)) (hs : h.istates zs = some s) (hl : l.left = 0) (hR : R h)
30    (hW : ReadableAt h s.window s.wsize.toNat) :
31    ∃ r l' h', runX (ROOM c) l h = .ok ((r, l'), h') ∧ CbFrame ownO (roomHeap h zs s) h' ∧ R h' ∧
32      ((r = .ok () ∧ l' = { l with put := s.window, left := s.wsize }) ∨
33       (r = .error Ex.leave ∧ l' = { l with put := s.window, left := s.wsize, ret := Z_BUF_ERROR })) := by
34  have hR1 : R (roomHeap h zs s) := (hK.local_ h (roomHeap h zs s) (fun b _ => rfl)).1 hR
35  have hW1 : ReadableAt (roomHeap h zs s) s.window s.wsize.toNat := by
36    obtain ⟨b, off, a, e, hb, hle⟩ := hW
37    exact ⟨b, off, a, e, hb, hle⟩
38  obtain ⟨r, h', he, fr, hR'⟩ := hK.outOk _ s.window s.wsize hR1 hW1
39  have hld : ldInflateState c.st h = .ok (s, h) := by rw [hc]; exact ldInflateState_tab hs
40  have hwr : wrS c.st (fun s => { s with whave := s.wsize }) h = .ok ((), roomHeap h zs s) := by
41    rw [hc]; exact wrS_tab hs _
42  have hb : (l.left == 0) = true := by simpa using hl
43  have hcall : ∀ l1 : IL, runX (monadLift (c.outCb c.outDesc s.window s.wsize) : X Int32) l1 (roomHeap h zs s) =
44      .ok ((.ok r, l1), h') := fun l1 => runX_lift_ok he l1
45  by_cases hr0 : r = 0
46  · refine ⟨.ok (), { l with put := s.window, left := s.wsize }, h', ?_, fr, hR', Or.inl ⟨rfl, rfl⟩⟩
47    unfold ROOM
48    simp [runX_bind, runX_get, hb, hl, runX_lift_ok hld, runX_set, runX_lift_ok hwr, hcall, hr0, runX_pure]
49  · refine ⟨.error Ex.leave, { l with put := s.window, left := s.wsize, ret := Z_BUF_ERROR }, h', ?_, fr, hR',
50      Or.inr ⟨rfl, rfl⟩⟩
51    unfold ROOM
52    simp [runX_bind, runX_get, hb, hl, runX_lift_ok hld, runX_set, runX_lift_ok hwr, hcall, hr0, runX_modify, runX_throw]
53
54end Zlib.Infback.Proofs