inflate.c.main.table3.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.table2»
2
3/-!
4# inflate.c: `case LENLENS:` -- the loops
5
6The two loops of `LENLENS` as local definitions (checked equal to the translation by `rfl`), their bodies and the run lemmas.
7-/
8
9namespace Zlib.Inflate.Proofs
10open C Zlib.Inflate Zlib.Inflate.Spec
11open Zlib.Inftrees (inflate_table)
12
13/-! ## Accesses to the arrays of the state record -/
14
15theorem BitInv.tc_of_heap {h h' : Heap} {l : IL} {bs : List UInt8} (B : BitInv h l bs) (hb : h'.bytes = h.bytes)
16    (hd : h'.dstates = h.dstates) (hs : h'.static = h.static) : BitInv h' l bs := by
17  refine ⟨B.have_eq, ?_, B.hold_lt⟩
18  rcases B.next with e | ⟨r, a, off, hn, hg, hsz, hbs⟩
19  · exact Or.inl e
20  · refine Or.inr ⟨r, a, off, hn, ?_, hsz, hbs⟩
21    cases r <;> simpa [Space.get, hb, hd, hs] using hg
22
23theorem BitInv.tc_setI {h : Heap} {l : IL} {bs : List UInt8} (B : BitInv h l bs) (zs : Nat) (s : InflateState) :
24    BitInv (setI h zs s) l bs := B.tc_of_heap rfl rfl rfl
25
26theorem tcStore_lens {h : Heap} {zs : Nat} {t : InflateState} {k : Nat} (v : UInt16) (ht : h.istates zs = some t)
27    (hk : k < t.lens.size) :
28    Ptr.store (Ptr.ref (WRef.istate_lens zs) k) v h = .ok ((), setI h zs { t with lens := t.lens.set! k v }) := by
29  rw [Ptr.store_ok (WRef.get_istate_lens ht) (WRef.ro_istate_lens h zs) hk, WRef.put_istate_lens ht]
30  rfl
31
32theorem tcAdd_lens {h : Heap} {zs : Nat} {t : InflateState} {k : Nat} (ht : h.istates zs = some t)
33    (hk : k ≤ t.lens.size) :
34    Ptr.add (Ptr.ref (WRef.istate_lens zs) 0) (k : Int) h = .ok (Ptr.ref (WRef.istate_lens zs) k, h) := by
35  have := Ptr.add_nat_ok (n := k) (off := 0) (WRef.get_istate_lens ht) (by omega)
36  simpa [OkOn] using this
37
38/-! ## The loops of `case LENLENS:` -/
39
40/-- `while (state->have < state->ncode)` -/
41def llCond (c : Ctx) : X Bool := do let s ← ldInflateState c.st; return s.«have» < s.ncode
42
43/-- `{ NEEDBITS(3); state->lens[order[state->have++]] = (unsigned short)BITS(3); DROPBITS(3); }` -/
44def llBody (c : Ctx) : X Unit := do
45  NEEDBITS 3
46  let s ← ldInflateState c.st
47  wrS c.st fun s => { s with «have» := s.«have» + 1 }
48  let o ← orderAt s.«have»
49  let b ← BITS 3
50  Ptr.store (← (lensP c.st).add (o.toNat : Int)) b.toUInt16
51  DROPBITS 3
52
53/-- `while (state->have < 19)` -/
54def lzCond (c : Ctx) : X Bool := do let s ← ldInflateState c.st; return s.«have» < 19
55
56/-- `state->lens[order[state->have++]] = 0;` -/
57def lzBody (c : Ctx) : X Unit := do
58  let s ← ldInflateState c.st
59  wrS c.st fun s => { s with «have» := s.«have» + 1 }
60  let o ← orderAt s.«have»
61  Ptr.store (← (lensP c.st).add (o.toNat : Int)) (0 : UInt16)
62
63/-- From `state->next = state->codes ...` to the end of the mode. -/
64def llTail (c : Ctx) : X Unit := do
65  wrS c.st fun s => { s with next := codesP c.st, distcode := codesP c.st, lencode := codesP c.st, lenbits := 7 }
66  let s ← ldInflateState c.st
67  let (r, nx, lb) ← inflate_table CODES (lensP c.st) 19 s.next s.lenbits (workP c.st)
68  wrS c.st fun s => { s with next := nx, lenbits := lb }
69  modify fun l => { l with ret := r }
70  if r != 0 then
71    badMode c "invalid code lengths set"
72    return
73  wrS c.st fun s => { s with «have» := 0, mode := CODELENS }
74  inflate_CODELENS c
75
76/-- The translation of `case LENLENS:` is the two loops and the tail. -/
77theorem inflate_LENLENS_eq (c : Ctx) :
78    inflate_LENLENS c = (do xwhile (llCond c) (llBody c); xwhile (lzCond c) (lzBody c); llTail c) := rfl
79
80theorem tcBITS3_run (l : IL) (h : Heap) : runX (BITS 3) l h = .ok ((.ok (l.hold.toUInt32 &&& 7), l), h) := by
81  rw [BITS_run l h 3 (by decide)]; rfl
82
83theorem tcDROP3_run (l : IL) (h : Heap) :
84    runX (DROPBITS 3) l h = .ok ((.ok (), { l with hold := l.hold >>> 3, bits := l.bits - 3 }), h) := by
85  rw [DROPBITS_run l h 3 (by decide)]; rfl
86
87/-- One iteration of the first loop of `LENLENS`, in a state with `have < 19` and `lens` of its declared size:
88`NEEDBITS(3)`, and then either `goto inf_leave` (input ran out: nothing was written) or the next code length is stored in
89`lens[order[have]]`, `have` grows by one, three bits are dropped. -/
90theorem llBody_run {c : Ctx} {l : IL} {h : Heap} {zs : Nat} {t : InflateState} {bs : List UInt8}
91    (hc : c.st = some (.tab zs)) (ht : h.istates zs = some t) (hsz : t.lens.size = 320) (hH : t.«have».toNat < 19)
92    (B : BitInv h l bs) :
93    ∃ rr l' j, runX (NEEDBITS 3) l h = .ok ((rr, l'), h) ∧ j ≤ bs.length ∧ BitInv h l' (bs.drop j) ∧
94      stream l' (bs.drop j) = stream l bs ∧
95      l' = { l with next := l'.next, have_ := l'.have_, hold := l'.hold, bits := l'.bits } ∧
96      (rr = .error Ex.leave → l'.have_ = 0 ∧ j = bs.length ∧ l'.bits.toNat < 3 ∧
97        runX (llBody c) l h = .ok ((.error Ex.leave, l'), h)) ∧
98      (rr = .ok () → 3 ≤ l'.bits.toNat ∧
99        runX (llBody c) l h = .ok ((.ok (), { l' with hold := l'.hold >>> 3, bits := l'.bits - 3 }),
100          setI h zs { t with «have» := t.«have» + 1, lens := t.lens.set! (orderNat t.«have».toNat) (l'.hold.toUInt32 &&& 7).toUInt16 })) := by
101  obtain ⟨rr, l', j, hrun, hj, B', hS', hbits, hshape, hmax, hid, hok, hleave⟩ := NEEDBITS_run B 3 (by decide)
102  refine ⟨rr, l', j, hrun, hj, B', hS', hshape, ?_, ?_⟩
103  · intro e
104    obtain ⟨h1, h2, h3⟩ := hleave e
105    refine ⟨h2, h1, h3, ?_⟩
106    unfold llBody
107    simp [runX_bind, hrun, e]
108  · intro e
109    refine ⟨hok e, ?_⟩
110    have ho : orderNat t.«have».toNat < 19 := order_lt _ hH
111    have hhave1 : (t.«have» + 1).toNat = t.«have».toNat + 1 := by
112      rw [UInt32.toNat_add]; simp; omega
113    have hoa := orderAt_run (setI h zs { t with «have» := t.«have» + 1 }) t.«have» hH
114    have hadd := tcAdd_lens (h := setI h zs { t with «have» := t.«have» + 1 }) (zs := zs)
115      (t := { t with «have» := t.«have» + 1 }) (k := (order[t.«have».toNat]!).toNat) (by simp)
116      (by have := ho; unfold orderNat at this; simp [hsz]; omega)
117    have hst := tcStore_lens (h := setI h zs { t with «have» := t.«have» + 1 }) (zs := zs)
118      (t := { t with «have» := t.«have» + 1 }) (k := (order[t.«have».toNat]!).toNat) (l'.hold.toUInt32 &&& 7).toUInt16
119      (by simp) (by have := ho; unfold orderNat at this; simp [hsz]; omega)
120    unfold llBody
121    rw [hc]
122    simp at hst
123    simp [runX_bind, runX_lift, ldI_eq, ht, hrun, e, wrI_eq, hoa, hadd, hst, tcBITS3_run, tcDROP3_run, lensP, orderNat]
124
125end Zlib.Inflate.Proofs