inflate.c.lookup-loop.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.input-cursor»
2import ZlibF.Proof.«inflate.c.xloop-rank»
3
4namespace Zlib.Inflate.Proofs
5open C Zlib.Inflate
6set_option autoImplicit false
7
8def codeLookupValue (ca : Array Code) (offset root : Nat) (l : IL) : Code :=
9  ca.getD (offset + l.hold.toNat % 2 ^ root) default
10
11/-- Root lookup changes input and bit registers and the selected entry only. -/
12def LookupRegShape (before after : IL) : Prop :=
13  after = { before with next := after.next, have_ := after.have_, hold := after.hold, bits := after.bits, here := after.here }
14
15theorem LookupRegShape.refl (l : IL) : LookupRegShape l l := rfl
16
17theorem LookupRegShape.trans {a b c : IL} (first : LookupRegShape a b) (second : LookupRegShape b c) :
18    LookupRegShape a c := by
19  unfold LookupRegShape at *
20  rw [second, first]
21
22/-- A checked table-lookup body either stops on sufficient bits or refills.
23This loop rule retains exact input consumption, the selected entry and the
24bit stream. Actual lookup bodies must establish the execution equality. -/
25theorem lookupLoop_run_cursor {body : X Bool} {h : Heap} {l : IL} {bs : List UInt8}
26    (query : IL → Code) (need : Code → UInt32)
27    (stable : ∀ current, query { current with here := query current } = query current)
28    (bound : ∀ current, (need (query current)).toNat ≤ 15)
29    (bodyRun : ∀ current, LookupRegShape l current →
30      runX body current h =
31        if need (query current) ≤ current.bits then
32          .ok ((.ok true, { current with here := query current }), h)
33        else runX (do PULLBYTE; pure false : X Bool) { current with here := query current } h)
34    (B : BitInv h l bs) :
35    ∃ result regs used,
36      runX (xloopBrk body) l h = .ok ((result, regs), h) ∧
37      used ≤ 2 ∧ used ≤ bs.length ∧ BitInv h regs (bs.drop used) ∧
38      stream regs (bs.drop used) = stream l bs ∧ LookupRegShape l regs ∧
39      regs.bits.toNat = l.bits.toNat + 8 * used ∧
40      regs.bits.toNat ≤ max l.bits.toNat 22 ∧
41      regs.here = query regs ∧ (need regs.here).toNat ≤ 15 ∧
42      (result = .ok () ∨ result = .error Ex.leave) ∧
43      (result = .ok () → (need regs.here).toNat ≤ regs.bits.toNat) ∧
44      (result = .error Ex.leave → regs.have_ = 0) ∧ regs.next = inputAdvance l.next used := by
45  let P : IL → Heap → Prop := fun regs heap =>
46    heap = h ∧ ∃ used, used ≤ bs.length ∧ BitInv h regs (bs.drop used) ∧
47      stream regs (bs.drop used) = stream l bs ∧ LookupRegShape l regs ∧
48      regs.bits.toNat = l.bits.toNat + 8 * used ∧ regs.bits.toNat ≤ max l.bits.toNat 22 ∧
49      regs.next = inputAdvance l.next used
50  let Q : Except Ex Unit → IL → Heap → Prop := fun result regs heap =>
51    P regs heap ∧ regs.here = query regs ∧
52      (need regs.here).toNat ≤ 15 ∧ (result = .ok () ∨ result = .error Ex.leave) ∧
53      (result = .ok () → (need regs.here).toNat ≤ regs.bits.toNat) ∧
54      (result = .error Ex.leave → regs.have_ = 0)
55  have step : ∀ current heap, P current heap → ∃ test regs heap1,
56      runX (pure true : X Bool) current heap = .ok ((test, regs), heap1) ∧
57      (match test with
58       | .error fault => Q (.error fault) regs heap1
59       | .ok false => Q (.ok ()) regs heap1
60       | .ok true => ∃ result final heap2,
61           runX body regs heap1 = .ok ((result, final), heap2) ∧
62           (match result with
63            | .error fault => Q (.error fault) final heap2
64            | .ok true => Q (.ok ()) final heap2
65            | .ok false => P final heap2 ∧ 15 - final.bits.toNat < 15 - current.bits.toNat)) := by
66    rintro current heap ⟨heapEq, used, usedBound, inv, sameStream, shape, count, bitBound, cursor⟩
67    subst heap
68    refine ⟨.ok true, current, h, rfl, ?_⟩
69    let entry := query current
70    let read := { current with here := entry }
71    have entryBound : (need entry).toNat ≤ 15 := bound current
72    have readInv : BitInv h read (bs.drop used) := ⟨inv.have_eq, inv.next, inv.hold_lt⟩
73    have readShape : LookupRegShape l read := shape.trans (by rfl)
74    have actual := bodyRun current shape
75    change runX body current h =
76      if need entry ≤ current.bits then .ok ((.ok true, read), h)
77      else runX (do PULLBYTE; pure false : X Bool) read h at actual
78    by_cases fits : need entry ≤ current.bits
79    · rw [ite_eq_left fits] at actual
80      refine ⟨.ok true, read, h, actual, ⟨rfl, used, usedBound, readInv, sameStream, readShape, count, bitBound, cursor⟩,
81        (stable current).symm, entryBound, Or.inl rfl, ?_, ?_⟩
82      · intro _
83        have bound := UInt32.le_iff_toNat_le.mp fits
84        exact bound
85      · intro impossible
86        cases impossible
87    · rw [ite_eq_right fits] at actual
88      have short : current.bits.toNat < (need entry).toNat := by
89        have := (not_congr UInt32.le_iff_toNat_le).mp fits
90        omega
91      cases remaining : bs.drop used with
92      | nil =>
93        have empty : read.have_ = 0 := by
94          apply UInt32.toNat_inj.mp
95          have len := inv.have_eq
96          rw [remaining] at len
97          exact len
98        rw [runX_bind, PULLBYTE_zero empty] at actual
99        refine ⟨.error Ex.leave, read, h, actual,
100          ⟨rfl, used, usedBound, readInv, sameStream, readShape, count, bitBound, cursor⟩,
101          (stable current).symm, entryBound, Or.inr rfl, ?_, fun _ => empty⟩
102        intro impossible
103        cases impossible
104      | cons byte rest =>
105        have readCons : BitInv h read (byte :: rest) := by rwa [remaining] at readInv
106        obtain ⟨next, pull, nextInv, nextStream, nextBits, nextCursor⟩ := PULLBYTE_succ_cursor readCons
107          (by change current.bits.toNat ≤ 56; omega)
108        let final := pulled read byte next
109        have restEq : bs.drop (used + 1) = rest := by
110          have eq : (bs.drop used).drop 1 = rest := by rw [remaining]; rfl
111          simpa only [List.drop_drop, Nat.add_comm] using eq
112        have usedNext : used + 1 ≤ bs.length := by
113          have len := congrArg List.length remaining
114          simp only [List.length_drop, List.length_cons] at len
115          omega
116        have finalInv : BitInv h final (bs.drop (used + 1)) := by rwa [restEq]
117        have finalStream : stream final (bs.drop (used + 1)) = stream l bs := by
118          rw [restEq, nextStream, ← remaining]
119          exact sameStream
120        have finalCount : final.bits.toNat = l.bits.toNat + 8 * (used + 1) := by
121          rw [nextBits]
122          change current.bits.toNat + 8 = _
123          rw [count, Nat.mul_add]
124          omega
125        have finalBound : final.bits.toNat ≤ max l.bits.toNat 22 := by
126          rw [nextBits]
127          change current.bits.toNat + 8 ≤ _
128          omega
129        rw [runX_bind, pull] at actual
130        simp only [runX_pure] at actual
131        refine ⟨.ok false, final, h, actual,
132          ⟨rfl, used + 1, usedNext, finalInv, finalStream, readShape.trans (by rfl), finalCount, finalBound, ?_⟩, ?_⟩
133        · change next = inputAdvance l.next (used + 1)
134          rw [nextCursor]
135          change inputAdvance current.next 1 = _
136          rw [cursor, inputAdvance_add]
137        · rw [nextBits]
138          change 15 - (current.bits.toNat + 8) < 15 - current.bits.toNat
139          omega
140  have initial : P l h := ⟨rfl, 0, by omega, by simpa using B, rfl, LookupRegShape.refl l, by simp, by omega, (inputAdvance_zero l.next).symm⟩
141  have fuelBound : 17 < fuel := by decide
142  obtain ⟨result, regs, after, run, post, selected, entryBits, kinds, enough, empty⟩ :=
143    xwhileBrk_rank P (fun regs _ => 15 - regs.bits.toNat) Q step initial (by change 15 - l.bits.toNat + 2 < fuel; omega)
144  obtain ⟨heapEq, used, usedBound, inv, sameStream, shape, count, bitBound, cursor⟩ := post
145  subst after
146  have atMostTwo : used ≤ 2 := by omega
147  exact ⟨result, regs, used, run, atMostTwo, usedBound, inv, sameStream, shape, count, bitBound,
148    selected, entryBits, kinds, enough, empty, cursor⟩
149
150/-- Projection retaining the original checked lookup-loop contract. -/
151theorem lookupLoop_run {body : X Bool} {h : Heap} {l : IL} {bs : List UInt8}
152    (query : IL → Code) (need : Code → UInt32)
153    (stable : ∀ current, query { current with here := query current } = query current)
154    (bound : ∀ current, (need (query current)).toNat ≤ 15)
155    (bodyRun : ∀ current, LookupRegShape l current →
156      runX body current h =
157        if need (query current) ≤ current.bits then
158          .ok ((.ok true, { current with here := query current }), h)
159        else runX (do PULLBYTE; pure false : X Bool) { current with here := query current } h)
160    (B : BitInv h l bs) :
161    ∃ result regs used,
162      runX (xloopBrk body) l h = .ok ((result, regs), h) ∧
163      used ≤ 2 ∧ used ≤ bs.length ∧ BitInv h regs (bs.drop used) ∧
164      stream regs (bs.drop used) = stream l bs ∧ LookupRegShape l regs ∧
165      regs.bits.toNat = l.bits.toNat + 8 * used ∧
166      regs.bits.toNat ≤ max l.bits.toNat 22 ∧
167      regs.here = query regs ∧ (need regs.here).toNat ≤ 15 ∧
168      (result = .ok () ∨ result = .error Ex.leave) ∧
169      (result = .ok () → (need regs.here).toNat ≤ regs.bits.toNat) ∧
170      (result = .error Ex.leave → regs.have_ = 0) := by
171  obtain ⟨result, regs, used, run, two, usedBound, inv, bits, shape, count, bitBound,
172    selected, width, kinds, enough, empty, _⟩ := lookupLoop_run_cursor query need stable bound bodyRun B
173  exact ⟨result, regs, used, run, two, usedBound, inv, bits, shape, count, bitBound,
174    selected, width, kinds, enough, empty⟩
175
176end Zlib.Inflate.Proofs