inflate.c.main.stored.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.type»
2
3/-!
4# inflate.c: `COPY_`, `COPY` and `STORED` (stored blocks)
5-/
6
7namespace Zlib.Inflate.Proofs
8open C Zlib.Inflate Zlib.Inflate.Spec
9
10/-- The number of bytes `case COPY:` moves: `state->length` capped by `have` and then by `left`. -/
11def copyAmt (len have_ left : UInt32) : UInt32 :=
12  let c := if len > have_ then have_ else len
13  if c > left then left else c
14
15theorem copyAmt_le (len have_ left : UInt32) : (copyAmt len have_ left).toNat ≤ len.toNat ∧
16    (copyAmt len have_ left).toNat ≤ have_.toNat ∧ (copyAmt len have_ left).toNat ≤ left.toNat := by
17  unfold copyAmt
18  simp only [gt_iff_lt, UInt32.lt_iff_toNat_lt]
19  split <;> split <;> omega
20
21/-- `case COPY:` with nothing left to copy: back to `TYPE`; `copy` is recorded as 0. -/
22theorem inflate_COPY_done {c : Ctx} {h : Heap} {r zs z s} (E : Env c h r zs z s) (l : IL) (hz : s.length = 0) :
23    runX (inflate_COPY c) l h = .ok ((.ok (), { l with copy := 0 }), setI h zs { s with mode := TYPE }) := by
24  unfold inflate_COPY
25  have hb : (s.length != 0) = false := by simp [hz]
26  rw [runX_bind, runX_ldS E]
27  simp only [hb, Bool.false_eq_true, ↓reduceIte]
28  rw [runX_bind, runX_modify]
29  simp only []
30  rw [runX_setMode E]
31  simp [hz]
32
33/-- What `case COPY:` does once the amount `n` to copy is known. -/
34def copyTail (c : Ctx) (n : UInt32) : X Unit := do
35  let l ← get
36  if n == 0 then
37    set { l with copy := n }
38    throw Ex.leave
39  memcpyB l.put l.next n.toNat
40  let nx ← l.next.add (n.toNat : Int)
41  let pt ← l.put.add (n.toNat : Int)
42  set { l with copy := n, have_ := l.have_ - n, next := nx, left := l.left - n, put := pt }
43  wrS c.st fun s => { s with length := s.length - n }
44  return
45
46theorem inflate_COPY_split {c : Ctx} {h : Heap} {r zs z s} (E : Env c h r zs z s) (l : IL) (hnz : s.length ≠ 0) :
47    runX (inflate_COPY c) l h = runX (copyTail c (copyAmt s.length l.have_ l.left)) l h := by
48  have hb : (s.length != 0) = true := by simpa using hnz
49  unfold inflate_COPY
50  rw [runX_bind, runX_ldS E]
51  simp only [hb, ↓reduceIte]
52  rw [runX_bind, runX_get]
53  simp only []
54  unfold copyAmt
55  by_cases c1 : s.length > l.have_ <;> by_cases c2 : l.have_ > l.left <;> by_cases c3 : s.length > l.left <;>
56    simp [c1, c2, c3, copyTail]
57  all_goals (split <;> simp_all [runX_bind, runX_set, runX_throw, runX_get, copyTail])
58
59theorem copyTail_stall (c : Ctx) (l : IL) (h : Heap) :
60    runX (copyTail c 0) l h = .ok ((.error Ex.leave, { l with copy := 0 }), h) := by
61  unfold copyTail
62  rw [runX_bind, runX_get]
63  simp only [beq_self_eq_true, ↓reduceIte]
64  rw [runX_bind, runX_set]
65  simp only []
66  rw [runX_bind, runX_throw]
67
68/-- After writing the byte block `db`, every array keeps its size. -/
69theorem get_after_put {h : Heap} {db : Nat} {da a' : Array UInt8} (hd : h.bytes db = some da) (hs : a'.size = da.size)
70    {r : BRef} {a : Array UInt8} (hg : (Space.get h r : Option (Array UInt8)) = some a) :
71    ∃ a2, (Space.get { h with bytes := upd h.bytes db (some a') } r : Option (Array UInt8)) = some a2 ∧ a2.size = a.size := by
72  cases r with
73  | blk b =>
74    by_cases hb : b = db
75    · subst hb
76      refine ⟨a', ?_, ?_⟩
77      · show (upd h.bytes b (some a')) b = _
78        simp
79      · have : a = da := by
80          have : h.bytes b = some a := hg
81          rw [hd] at this; exact (Option.some.inj this).symm
82        subst this; exact hs
83    · refine ⟨a, ?_, rfl⟩
84      show (upd h.bytes db (some a')) b = _
85      rw [upd_ne _ _ _ _ hb]; exact hg
86  | str i => exact ⟨a, hg, rfl⟩
87  | dstate_depth i => exact ⟨a, hg, rfl⟩
88  | st_dist_code => exact ⟨a, hg, rfl⟩
89  | st_length_code => exact ⟨a, hg, rfl⟩
90
91end Zlib.Inflate.Proofs