inflate.c.lookup-codes.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.lookup-loop»
2import ZlibF.Proof.«inflate.c.input-cursor»
3import ZlibF.Proof.«inftrees.c.decoder-safe»
4
5namespace Zlib.Inflate.Proofs
6open C Zlib.Inflate Zlib.Inflate.Spec
7set_option autoImplicit false
8
9def codesLookupBody (c : Ctx) : X Bool := do
10  let s ← ldInflateState c.st
11  let b ← BITS s.lenbits
12  let here ← Ptr.index s.lencode (b.toNat : Int)
13  modify fun l => { l with here := here }
14  if here.bits.toUInt32 <= (← get).bits then return true
15  PULLBYTE
16  return false
17
18theorem lookup1_codes_eq (c : Ctx) : lookup1 c false = xloopBrk (codesLookupBody c) := rfl
19
20/-- The root lookup executes on the actual table and actual bit mask,
21even when fewer than root bits are currently held. -/
22theorem codesLookupBody_run {c : Ctx} {h : Heap} {zs : Nat} {s : InflateState}
23    {ref : CodeRef} {offset : Nat} {ca : Array Code} (l : IL)
24    (hc : c.st = some (.tab zs)) (hs : h.istates zs = some s)
25    (pointer : s.lencode = .ref ref offset) (get : Space.get h ref = some ca)
26    (safe : Zlib.Inftrees.Spec.CodeLengthTableSafe ca offset s.lenbits.toNat) :
27    let entry := codeLookupValue ca offset s.lenbits.toNat l
28    runX (codesLookupBody c) l h =
29      if entry.bits.toUInt32 ≤ l.bits then .ok ((.ok true, { l with here := entry }), h)
30      else runX (do PULLBYTE; pure false : X Bool) { l with here := entry } h := by
31  dsimp only
32  have root : s.lenbits.toNat < 32 := by have := safe.2.1; omega
33  let mask := l.hold.toUInt32 &&& ((1 : UInt32) <<< s.lenbits - 1)
34  have value : mask.toNat = l.hold.toNat % 2 ^ s.lenbits.toNat := BITS_toNat l s.lenbits root
35  have inside : offset + mask.toNat < ca.size := by
36    have := Nat.mod_lt l.hold.toNat (Nat.two_pow_pos s.lenbits.toNat)
37    have := safe.2.2.1
38    omega
39  have read := Ptr.index_ok (off := offset) (i := mask.toNat) get inside
40  have actual : ca[offset + mask.toNat] = codeLookupValue ca offset s.lenbits.toNat l := by
41    unfold codeLookupValue
42    rw [← value, Array.getD_eq_getD_getElem?, Array.getElem?_eq_getElem inside, Option.getD_some]
43  dsimp only [mask] at read actual
44  unfold codesLookupBody
45  rw [hc]
46  have load : ldInflateState (some (.tab zs)) h = .ok (s, h) := by simp [ldI_eq, hs]
47  simp only [runX_bind, runX_lift_ok load, BITS_run l h s.lenbits root,
48    runX_modify, runX_get, pointer, runX_lift_ok read, actual]
49  by_cases fit : (codeLookupValue ca offset s.lenbits.toNat l).bits.toUInt32 ≤ l.bits
50  all_goals simp only [fit, ite_true, ite_false, runX_bind, runX_pure]
51
52private theorem xloopBrk_stop {body : X Bool} {l l' : IL} {h : Heap}
53    (run : runX body l h = .ok ((.ok true, l'), h)) :
54    runX (xloopBrk body) l h = .ok ((.ok (), l'), h) := by
55  have rule := xwhileBrk_run (cond := pure true) (body := body)
56    (fun k current heap => k = 1 ∧ current = l ∧ heap = h)
57    (fun result current heap => result = .ok () ∧ current = l' ∧ heap = h)
58    (by
59      intro k current heap inv
60      obtain ⟨count, currentEq, heapEq⟩ := inv
61      subst current heap
62      exact ⟨l, h, rfl, .ok true, l', h, run, rfl, rfl, rfl⟩)
63    (by intro current heap inv; have := inv.1; omega)
64    (k := 1) ⟨rfl, rfl, rfl⟩ (by decide)
65  obtain ⟨result, current, heap, actual, rfl, rfl, rfl⟩ := rule
66  exact actual
67
68private theorem xloopBrk_leave {body : X Bool} {l l' : IL} {h : Heap}
69    (run : runX body l h = .ok ((.error Ex.leave, l'), h)) :
70    runX (xloopBrk body) l h = .ok ((.error Ex.leave, l'), h) := by
71  have rule := xwhileBrk_run (cond := pure true) (body := body)
72    (fun k current heap => k = 1 ∧ current = l ∧ heap = h)
73    (fun result current heap => result = .error Ex.leave ∧ current = l' ∧ heap = h)
74    (by
75      intro k current heap inv
76      obtain ⟨count, currentEq, heapEq⟩ := inv
77      subst current heap
78      exact ⟨l, h, rfl, .error Ex.leave, l', h, run, rfl, rfl, rfl⟩)
79    (by intro current heap inv; have := inv.1; omega)
80    (k := 1) ⟨rfl, rfl, rfl⟩ (by decide)
81  obtain ⟨result, current, heap, actual, rfl, rfl, rfl⟩ := rule
82  exact actual
83
84private theorem xloopBrk_pull_stop {body : X Bool} {l middle final : IL} {h : Heap}
85    (first : runX body l h = .ok ((.ok false, middle), h))
86    (second : runX body middle h = .ok ((.ok true, final), h)) :
87    runX (xloopBrk body) l h = .ok ((.ok (), final), h) := by
88  have rule := xwhileBrk_run (cond := pure true) (body := body)
89    (fun k current heap => heap = h ∧ ((k = 2 ∧ current = l) ∨ (k = 1 ∧ current = middle)))
90    (fun result current heap => result = .ok () ∧ current = final ∧ heap = h)
91    (by
92      intro k current heap inv
93      obtain ⟨heapEq, two | one⟩ := inv
94      · subst heap
95        obtain ⟨count, currentEq⟩ := two
96        subst current
97        have zero : k = 1 := by omega
98        subst k
99        exact ⟨l, h, rfl, .ok false, middle, h, first, rfl, Or.inr ⟨rfl, rfl⟩⟩
100      · subst heap
101        obtain ⟨count, currentEq⟩ := one
102        subst current
103        exact ⟨middle, h, rfl, .ok true, final, h, second, rfl, rfl, rfl⟩)
104    (by intro current heap inv; rcases inv.2 with inv | inv <;> have := inv.1 <;> omega)
105    (k := 2) ⟨rfl, Or.inl ⟨rfl, rfl⟩⟩ (by decide)
106  obtain ⟨result, current, heap, actual, rfl, rfl, rfl⟩ := rule
107  exact actual
108
109private theorem codeLookupValue_bits {ca : Array Code} {offset root : Nat} (l : IL)
110    (safe : Zlib.Inftrees.Spec.CodeLengthTableSafe ca offset root) :
111    1 ≤ (codeLookupValue ca offset root l).bits.toNat ∧
112      (codeLookupValue ca offset root l).bits.toNat ≤ root := by
113  have entry := safe.2.2.2 (l.hold.toNat % 2 ^ root)
114    (Nat.mod_lt _ (Nat.two_pow_pos _))
115  exact ⟨entry.1, entry.2.1⟩
116
117/-- `for (;;) { here = lencode[BITS(lenbits)]; ... PULLBYTE(); }` in CODELENS.
118The constructed code-length table makes the actual lookup terminate after
119at most one input byte is pulled. Input exhaustion leaves safely. The held
120bit stream is unchanged and the selected entry has a positive bounded width. -/
121theorem lookup1_codes_run_cursor {c : Ctx} {h : Heap} {zs : Nat} {s : InflateState}
122    {ref : CodeRef} {offset : Nat} {ca : Array Code} {l : IL} {bs : List UInt8}
123    (hc : c.st = some (.tab zs)) (hs : h.istates zs = some s)
124    (pointer : s.lencode = .ref ref offset) (get : Space.get h ref = some ca)
125    (safe : Zlib.Inftrees.Spec.CodeLengthTableSafe ca offset s.lenbits.toNat)
126    (B : BitInv h l bs) :
127    ∃ result l' used,
128      runX (lookup1 c false) l h = .ok ((result, l'), h) ∧
129      used ≤ 1 ∧ used ≤ bs.length ∧ BitInv h l' (bs.drop used) ∧
130      stream l' (bs.drop used) = stream l bs ∧
131      l' = { l with next := l'.next, have_ := l'.have_, hold := l'.hold, bits := l'.bits, here := l'.here } ∧
132      l'.bits.toNat ≤ max l.bits.toNat 14 ∧
133      1 ≤ l'.here.bits.toNat ∧ l'.here.bits.toNat ≤ s.lenbits.toNat ∧
134      (result = .ok () ∨ result = .error Ex.leave) ∧
135      (result = .ok () → l'.here.bits.toNat ≤ l'.bits.toNat) ∧
136      (result = .error Ex.leave → l'.have_ = 0) ∧
137      l'.next = inputAdvance l.next used ∧ l'.bits.toNat = l.bits.toNat + 8 * used := by
138  let entry := codeLookupValue ca offset s.lenbits.toNat l
139  let read := { l with here := entry }
140  have bits := codeLookupValue_bits l safe
141  have readB : BitInv h read bs := ⟨B.have_eq, B.next, B.hold_lt⟩
142  have entryBound : entry.bits.toNat ≤ s.lenbits.toNat := bits.2
143  have body := codesLookupBody_run l hc hs pointer get safe
144  change runX (codesLookupBody c) l h =
145    if entry.bits.toUInt32 ≤ l.bits then .ok ((.ok true, read), h)
146    else runX (do PULLBYTE; pure false : X Bool) read h at body
147  rw [lookup1_codes_eq]
148  by_cases fit : entry.bits.toUInt32 ≤ l.bits
149  · rw [ite_eq_left fit] at body
150    have enough : entry.bits.toNat ≤ l.bits.toNat := by
151      have := UInt32.le_iff_toNat_le.mp fit
152      simpa only [UInt8.toNat_toUInt32] using this
153    refine ⟨.ok (), read, 0, xloopBrk_stop body, by omega, by omega, ?_, rfl,
154      rfl, by dsimp only [read]; omega, bits.1, bits.2, Or.inl rfl,
155      fun _ => enough, ?_, (inputAdvance_zero l.next).symm, by simp only [Nat.mul_zero, Nat.add_zero]; rfl⟩
156    · simpa only [List.drop_zero] using readB
157    · intro impossible
158      cases impossible
159  · rw [ite_eq_right fit] at body
160    have short : l.bits.toNat < entry.bits.toNat := by
161      have := (not_congr UInt32.le_iff_toNat_le).mp fit
162      simp only [UInt8.toNat_toUInt32] at this
163      omega
164    have root : s.lenbits.toNat ≤ 7 := safe.2.1
165    cases bs with
166    | nil =>
167      have empty : read.have_ = 0 := by
168        apply UInt32.toNat_inj.mp
169        change l.have_.toNat = 0
170        simpa only [List.length_nil] using B.have_eq
171      rw [runX_bind, PULLBYTE_zero empty] at body
172      refine ⟨.error Ex.leave, read, 0, xloopBrk_leave body, by omega, by omega, ?_, rfl,
173        rfl, by dsimp only [read]; omega, bits.1, bits.2, Or.inr rfl, ?_, fun _ => empty, (inputAdvance_zero l.next).symm, by simp only [Nat.mul_zero, Nat.add_zero]; rfl⟩
174      · simpa only [List.drop_zero] using readB
175      · intro impossible
176        cases impossible
177    | cons b bs =>
178      obtain ⟨next, pull, B', sameStream, bitCount, cursor⟩ := PULLBYTE_succ_cursor readB
179        (by change l.bits.toNat ≤ 56; omega)
180      let middle := pulled read b next
181      let finalEntry := codeLookupValue ca offset s.lenbits.toNat middle
182      let final := { middle with here := finalEntry }
183      have finalBits := codeLookupValue_bits middle safe
184      have fits : finalEntry.bits.toUInt32 ≤ middle.bits := by
185        apply UInt32.le_iff_toNat_le.mpr
186        rw [UInt8.toNat_toUInt32]
187        change finalEntry.bits.toNat ≤ (pulled read b next).bits.toNat
188        rw [bitCount]
189        have bound : finalEntry.bits.toNat ≤ s.lenbits.toNat := finalBits.2
190        omega
191      have second := codesLookupBody_run middle hc hs pointer get safe
192      change runX (codesLookupBody c) middle h =
193        if finalEntry.bits.toUInt32 ≤ middle.bits then .ok ((.ok true, final), h)
194        else runX (do PULLBYTE; pure false : X Bool) final h at second
195      rw [ite_eq_left fits] at second
196      rw [runX_bind, pull] at body
197      simp only [runX_pure] at body
198      have execution := xloopBrk_pull_stop body second
199      have streamFinal : stream final bs = stream l (b :: bs) := sameStream
200      have bound : final.bits.toNat ≤ max l.bits.toNat 14 := by
201        change (pulled read b next).bits.toNat ≤ _
202        rw [bitCount]
203        change l.bits.toNat + 8 ≤ max l.bits.toNat 14
204        have entryBound : entry.bits.toNat ≤ s.lenbits.toNat := bits.2
205        omega
206      refine ⟨.ok (), final, 1, execution, by omega, by simp, ?_, streamFinal, ?_, bound,
207        finalBits.1, finalBits.2, Or.inl rfl, ?_, ?_, cursor, by simpa only [Nat.mul_one] using bitCount⟩
208      · exact ⟨B'.have_eq, B'.next, B'.hold_lt⟩
209      · rfl
210      · intro _
211        have enough := UInt32.le_iff_toNat_le.mp fits
212        simpa only [UInt8.toNat_toUInt32] using enough
213      · intro impossible
214        cases impossible
215
216/-- Projection retaining the original lookup interface. -/
217theorem lookup1_codes_run {c : Ctx} {h : Heap} {zs : Nat} {s : InflateState}
218    {ref : CodeRef} {offset : Nat} {ca : Array Code} {l : IL} {bs : List UInt8}
219    (hc : c.st = some (.tab zs)) (hs : h.istates zs = some s)
220    (pointer : s.lencode = .ref ref offset) (get : Space.get h ref = some ca)
221    (safe : Zlib.Inftrees.Spec.CodeLengthTableSafe ca offset s.lenbits.toNat)
222    (B : BitInv h l bs) :
223    ∃ result l' used,
224      runX (lookup1 c false) l h = .ok ((result, l'), h) ∧
225      used ≤ 1 ∧ used ≤ bs.length ∧ BitInv h l' (bs.drop used) ∧
226      stream l' (bs.drop used) = stream l bs ∧
227      l' = { l with next := l'.next, have_ := l'.have_, hold := l'.hold, bits := l'.bits, here := l'.here } ∧
228      l'.bits.toNat ≤ max l.bits.toNat 14 ∧
229      1 ≤ l'.here.bits.toNat ∧ l'.here.bits.toNat ≤ s.lenbits.toNat ∧
230      (result = .ok () ∨ result = .error Ex.leave) ∧
231      (result = .ok () → l'.here.bits.toNat ≤ l'.bits.toNat) ∧
232      (result = .error Ex.leave → l'.have_ = 0) := by
233  obtain ⟨result, regs, used, run, one, bound, inv, stream, shape, bits, lower, upper,
234    kinds, full, empty, _, _⟩ := lookup1_codes_run_cursor hc hs pointer get safe B
235  exact ⟨result, regs, used, run, one, bound, inv, stream, shape, bits, lower, upper, kinds, full, empty⟩
236
237end Zlib.Inflate.Proofs