inflate.c.main.macros.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.xloop»
2
3/-!
4# inflate.c: the bit-buffer macros
5
6`PULLBYTE`, `NEEDBITS`, `BITS`, `DROPBITS`, `BYTEBITS` and `INITBITS` of `inflate()` against the bit-stream invariant
7`BitInv`: the registers `next`, `have`, `hold`, `bits` describe the unconsumed DEFLATE bit stream
8`natBits bits hold ++ bytesBits bs`, where `bs` are the input bytes not yet pulled. Migrated from the earlier attempt's
9`InflateBits`; the byte-block pointer facts are now facts about `Space.get h r`. None of these macros writes the heap.
10-/
11
12namespace Zlib.Inflate.Proofs
13open C Zlib.Inflate
14
15theorem runX_get (l : IL) (h : Heap) : runX (get : X IL) l h = .ok ((.ok l, l), h) := rfl
16theorem runX_set (l l' : IL) (h : Heap) : runX (set l' : X PUnit) l h = .ok ((.ok (), l'), h) := rfl
17theorem runX_throw {α : Type} (e : Ex) (l : IL) (h : Heap) : runX (throw e : X α) l h = .ok ((.error e, l), h) := rfl
18theorem runX_modify (f : IL → IL) (l : IL) (h : Heap) : runX (modify f : X PUnit) l h = .ok ((.ok (), f l), h) := rfl
19theorem runX_lift {α : Type} (m : M α) (l : IL) (h : Heap) :
20    runX (monadLift m : X α) l h = match m h with
21      | .ok (a, h') => .ok ((.ok a, l), h')
22      | .error e => .error e := by
23  unfold runX
24  rcases hm : m h with e | ⟨a, h'⟩ <;>
25    simp [hm, monadLift, MonadLift.monadLift, ExceptT.lift, ExceptT.run, ExceptT.mk, StateT.lift, StateT.run,
26      Functor.map, StateT.map, ExceptT.map, bind_app]
27
28/-- The registers describe the bit stream `natBits bits hold` followed by the bytes `bs` at `next`. -/
29structure BitInv (h : Heap) (l : IL) (bs : List UInt8) : Prop where
30  have_eq : l.have_.toNat = bs.length
31  next : bs = [] ∨ ∃ (r : BRef) (a : Array UInt8) (off : Nat), l.next = .ref r off ∧
32    (Space.get h r : Option (Array UInt8)) = some a ∧ off + bs.length ≤ a.size ∧
33    bs = (a.toList.drop off).take bs.length
34  hold_lt : l.hold.toNat < 2 ^ l.bits.toNat
35
36/-- The unconsumed bit stream. -/
37def stream (l : IL) (bs : List UInt8) : List Bool := natBits l.bits.toNat l.hold.toNat ++ bytesBits bs
38
39/-- The registers after one successful `PULLBYTE` of the byte `b`, the pointer now `nx`. -/
40def pulled (l : IL) (b : UInt8) (nx : BPtr) : IL :=
41  { l with have_ := l.have_ - 1, next := nx, hold := l.hold + (b.toUInt64 <<< l.bits.toUInt64), bits := l.bits + 8 }
42
43/-- `PULLBYTE` with no input left (`have = 0`): `goto inf_leave` with the registers and the heap unchanged. -/
44theorem PULLBYTE_zero {l : IL} {h : Heap} (h0 : l.have_ = 0) :
45    runX PULLBYTE l h = .ok ((.error Ex.leave, l), h) := by
46  unfold PULLBYTE
47  simp [runX_bind, runX_get, h0, runX_throw]
48
49theorem runX_lift_ok {α : Type} {m : M α} {a : α} {h h' : Heap} (e : m h = .ok (a, h')) (l : IL) :
50    runX (monadLift m : X α) l h = .ok ((.ok a, l), h') := by
51  rw [runX_lift, e]
52
53theorem take_succ_drop (a : Array UInt8) (off n : Nat) (h : off + n + 1 ≤ a.size) :
54    (a.toList.drop off).take (n + 1) = a[off] :: (a.toList.drop (off + 1)).take n := by
55  have : off < a.toList.length := by simp; omega
56  rw [List.drop_eq_getElem_cons this]
57  simp
58
59theorem hold_add_lt (hold b P : Nat) (hh : hold < P) (hb : b < 256) : hold + b * P < 256 * P := by
60  have : (b + 1) * P ≤ 256 * P := Nat.mul_le_mul_right _ hb
61  rw [Nat.add_mul, Nat.one_mul] at this
62  omega
63
64theorem u32_add8 (x : UInt32) (hx : x.toNat ≤ 56) : (x + 8).toNat = x.toNat + 8 := by
65  rw [UInt32.toNat_add]; simp; omega
66
67/-- The hold word after pulling the byte `b` below `bits ≤ 56` held bits. -/
68theorem pull_hold (hold : UInt64) (b : UInt8) (bits : UInt32) (hb : bits.toNat ≤ 56) (hh : hold.toNat < 2 ^ bits.toNat) :
69    (hold + (b.toUInt64 <<< bits.toUInt64)).toNat = hold.toNat + b.toNat * 2 ^ bits.toNat ∧
70    hold.toNat + b.toNat * 2 ^ bits.toNat < 2 ^ (bits.toNat + 8) := by
71  have hK : (256 : Nat) * 2 ^ 56 = 2 ^ 64 := by decide
72  have hpow : 2 ^ bits.toNat ≤ 2 ^ 56 := Nat.pow_le_pow_right (by decide) hb
73  have hlt := hold_add_lt hold.toNat b.toNat _ hh (UInt8.toNat_lt b)
74  have h256 : 256 * 2 ^ bits.toNat ≤ 2 ^ 64 := by
75    have := Nat.mul_le_mul_left 256 hpow
76    omega
77  have hm : b.toNat * 2 ^ bits.toNat < 2 ^ 64 := by omega
78  have hsh : (b.toUInt64 <<< bits.toUInt64).toNat = b.toNat * 2 ^ bits.toNat := by
79    have := shl64_toNat b.toUInt64 bits (by omega) (by simpa using hm)
80    simpa using this
81  have hsum : (hold + (b.toUInt64 <<< bits.toUInt64)).toNat = hold.toNat + b.toNat * 2 ^ bits.toNat := by
82    rw [UInt64.toNat_add, hsh]
83    exact Nat.mod_eq_of_lt (by omega)
84  refine ⟨hsum, ?_⟩
85  rw [Nat.pow_add]
86  omega
87
88/-- `PULLBYTE` with the next input byte `b` at `next` (a readable byte array; `bits <= 56` so the shift does not overflow): no fault, the byte is appended to the bit buffer, `next` moves one byte, `have` drops by one, and the bit stream is the same as before. -/
89theorem PULLBYTE_succ {h : Heap} {l : IL} {b : UInt8} {bs : List UInt8} (B : BitInv h l (b :: bs))
90    (hb : l.bits.toNat ≤ 56) :
91    ∃ nx, runX PULLBYTE l h = .ok ((.ok (), pulled l b nx), h) ∧ BitInv h (pulled l b nx) bs ∧
92      stream (pulled l b nx) bs = stream l (b :: bs) ∧ (pulled l b nx).bits.toNat = l.bits.toNat + 8 := by
93  have hne0 : l.have_ ≠ 0 := fun e => by have := B.have_eq; rw [e] at this; simp at this
94  have hne : (l.have_ == 0) = false := by simpa using hne0
95  obtain ⟨r, a, off, hnext, hg, hsz, hbs⟩ := B.next.resolve_left (by simp)
96  have hsz' : off + bs.length + 1 ≤ a.size := by simp at hsz; omega
97  have hlt : off < a.size := by omega
98  have hbs' : b :: bs = a[off] :: (a.toList.drop (off + 1)).take bs.length := by
99    have := take_succ_drop a off bs.length hsz'
100    simp only [List.length_cons] at hbs
101    rw [← this]; exact hbs
102  have hbb : a[off] = b := by injection hbs' with h1; exact h1.symm
103  have hbs2 : bs = (a.toList.drop (off + 1)).take bs.length := by injection hbs' with _ h2
104  have hlb : l.bits.toNat < 64 := by omega
105  obtain ⟨hsum, hlt2⟩ := pull_hold l.hold b l.bits hb B.hold_lt
106  have hadd : OkOn h (l.next.add 1) (.ref r (off + 1)) := by
107    rw [hnext]; exact Ptr.add_nat_ok (n := 1) hg (by omega)
108  have hld : OkOn h (load8 l.next) b := by
109    rw [hnext]
110    have := Ptr.load_ok (h := h) (r := r) (off := off) hg hlt
111    rw [hbb] at this; exact this
112  have hshl : shl64 b.toUInt64 l.bits h = .ok (b.toUInt64 <<< l.bits.toUInt64, h) := by
113    rw [shl64_run _ _ hlb]; rfl
114  have hbn := u32_add8 l.bits hb
115  refine ⟨.ref r (off + 1), ?_, ?_, ?_, by simp [pulled, hbn]⟩
116  · unfold PULLBYTE
117    rw [runX_bind, runX_get]
118    simp only [hne, Bool.false_eq_true, ↓reduceIte]
119    simp only [runX_bind, runX_set, runX_lift_ok hld, runX_lift_ok hadd, runX_lift_ok hshl]
120    rfl
121  · refine ⟨?_, Or.inr ⟨r, a, off + 1, rfl, hg, by omega, hbs2⟩, ?_⟩
122    · have := B.have_eq
123      simp only [pulled, List.length_cons] at this ⊢
124      rw [UInt32.toNat_sub_of_le _ _ (by rw [UInt32.le_iff_toNat_le]; simp; omega)]
125      simp; omega
126    · simp only [pulled, hbn, hsum]; exact hlt2
127  · unfold stream
128    simp only [pulled, hbn, hsum]
129    rw [natBits_pull _ _ _ B.hold_lt (UInt8.toNat_lt _), List.append_assoc, bytesBits_cons]
130
131/-! ## NEEDBITS -/
132
133theorem runX_cond_lt (n : UInt32) (l : IL) (h : Heap) :
134    runX (do return (← get).bits < n : X Bool) l h = .ok ((.ok (decide (l.bits < n)), l), h) := rfl
135
136/-- What every state of the `NEEDBITS` loop satisfies: `j` input bytes of `bs` were pulled from the start registers `l0`. -/
137def NBase (h : Heap) (l0 : IL) (bs : List UInt8) (n : UInt32) (l1 : IL) (j : Nat) : Prop :=
138  j ≤ bs.length ∧ BitInv h l1 (bs.drop j) ∧ stream l1 (bs.drop j) = stream l0 bs ∧
139    l1.bits.toNat = l0.bits.toNat + 8 * j ∧
140    l1 = { l0 with next := l1.next, have_ := l1.have_, hold := l1.hold, bits := l1.bits } ∧
141    l1.bits.toNat ≤ max l0.bits.toNat (n.toNat + 7) ∧ (j = 0 → l1 = l0)
142
143/-- `NEEDBITS` loop invariant: `k` iterations remain. -/
144def NInv (h : Heap) (l0 : IL) (bs : List UInt8) (n : UInt32) (k : Nat) (l1 : IL) (h1 : Heap) : Prop :=
145  h1 = h ∧ ∃ j, NBase h l0 bs n l1 j ∧ k = (if l1.bits.toNat < n.toNat then min ((n.toNat - l1.bits.toNat + 7) / 8) (bs.length - j + 1) else 0)
146
147/-- `NEEDBITS(n)` for `n ≤ 49`: either enough bits are held afterwards (`ok`), or the input ran out (`goto inf_leave`, all
148input pulled, still fewer than `n` bits). Only `next`, `have`, `hold`, `bits` change, the stream is preserved, and nothing is
149pulled when `n` bits are already held. -/
150theorem NEEDBITS_run {h : Heap} {l : IL} {bs : List UInt8} (B : BitInv h l bs) (n : UInt32) (hn : n.toNat ≤ 49) :
151    ∃ r l' j, runX (NEEDBITS n) l h = .ok ((r, l'), h) ∧ j ≤ bs.length ∧ BitInv h l' (bs.drop j) ∧
152      stream l' (bs.drop j) = stream l bs ∧ l'.bits.toNat = l.bits.toNat + 8 * j ∧
153      l' = { l with next := l'.next, have_ := l'.have_, hold := l'.hold, bits := l'.bits } ∧
154      l'.bits.toNat ≤ max l.bits.toNat (n.toNat + 7) ∧ (n.toNat ≤ l.bits.toNat → l' = l) ∧
155      (r = .ok () → n.toNat ≤ l'.bits.toNat) ∧
156      (r = .error Ex.leave → j = bs.length ∧ l'.have_ = 0 ∧ l'.bits.toNat < n.toNat) := by
157  have hlen : bs.length < 2 ^ 32 := by
158    have := B.have_eq; have := UInt32.toNat_lt l.have_; simp at *; omega
159  have key := xwhileBrk_run (cond := (do return (← get).bits < n : X Bool)) (body := (do PULLBYTE; pure false : X Bool))
160    (NInv h l bs n)
161    (fun r l1 h1 => h1 = h ∧ ∃ j, NBase h l bs n l1 j ∧ (r = .ok () → n.toNat ≤ l1.bits.toNat) ∧
162      (r = .error Ex.leave → j = bs.length ∧ l1.have_ = 0 ∧ l1.bits.toNat < n.toNat))
163    (fun k l1 h1 hP => by
164      obtain ⟨hh, j, hb, hk⟩ := hP
165      subst hh
166      have hnl : l1.bits.toNat < n.toNat := by
167        by_cases hc : l1.bits.toNat < n.toNat
168        · exact hc
169        · rw [ite_eq_right hc] at hk; omega
170      have hnl' : l1.bits < n := UInt32.lt_iff_toNat_lt.mpr hnl
171      obtain ⟨hj, hB, hS, hbits, hshape, hmax, hz⟩ := hb
172      have hcond : runX (do return (← get).bits < n : X Bool) l1 h1 = .ok ((.ok true, l1), h1) := by
173        rw [runX_cond_lt]; simp [hnl']
174      refine ⟨l1, h1, hcond, ?_⟩
175      by_cases h0 : l1.have_ = 0
176      · refine ⟨.error Ex.leave, l1, h1, ?_, ?_⟩
177        · rw [runX_bind, PULLBYTE_zero h0]
178        · have := hB.have_eq
179          have h00 : l1.have_.toNat = 0 := by rw [h0]; rfl
180          simp only [List.length_drop] at this
181          refine ⟨rfl, j, ⟨hj, hB, hS, hbits, hshape, hmax, hz⟩, (fun e => nomatch e), fun _ => ⟨by omega, h0, hnl⟩⟩
182      · have hlenj : j < bs.length := by
183          have := hB.have_eq
184          simp only [List.length_drop] at this
185          apply Decidable.byContradiction
186          intro hc
187          apply h0
188          have : l1.have_.toNat = 0 := by omega
189          exact UInt32.toNat_inj.mp (by simpa using this)
190        have hdrop : bs.drop j = bs[j] :: bs.drop (j + 1) := List.drop_eq_getElem_cons hlenj
191        rw [hdrop] at hB hS
192        obtain ⟨nx, hrun, hB2, hS2, hb2⟩ := PULLBYTE_succ hB (by omega)
193        refine ⟨.ok false, pulled l1 bs[j] nx, h1, ?_, ?_⟩
194        · rw [runX_bind, hrun]; rfl
195        · refine ⟨rfl, j + 1, ⟨by omega, hB2, ?_, by omega, ?_, by omega, by omega⟩, ?_⟩
196          · rw [hS2, hS]
197          · rw [hshape]; simp [pulled]
198          · rw [ite_eq_left hnl] at hk
199            rw [hb2]
200            split <;> omega)
201
202    (fun l1 h1 hP => by
203      obtain ⟨hh, j, hb, hk⟩ := hP
204      subst hh
205      have hnl : ¬ l1.bits.toNat < n.toNat := by intro hl; rw [ite_eq_left hl] at hk; omega
206      refine ⟨l1, h1, by rw [runX_cond_lt]; simp [UInt32.lt_iff_toNat_lt, hnl], rfl, j, hb, ?_, ?_⟩
207      · intro _
208        omega
209      · intro e; cases e)
210    (k := (if l.bits.toNat < n.toNat then min ((n.toNat - l.bits.toNat + 7) / 8) (bs.length + 1) else 0)) (l := l) (h := h)
211    ⟨rfl, 0, ⟨by omega, by simpa using B, by simp [stream], by simp, by simp, by omega, fun _ => rfl⟩, by simp⟩
212    (by unfold fuel; split <;> omega)
213  obtain ⟨r, l', h', hr, rfl, j, hb, hq1, hq2⟩ := key
214  obtain ⟨hj, hB, hS, hbits, hshape, hmax, hz⟩ := hb
215  refine ⟨r, l', j, by unfold NEEDBITS xwhile; exact hr, hj, hB, hS, hbits, hshape, hmax, ?_, hq1, hq2⟩
216  intro hge
217  by_cases hj0 : j = 0
218  · exact hz hj0
219  · exfalso; omega
220
221/-! ## BITS, DROPBITS, BYTEBITS, INITBITS -/
222
223/-- `BITS(n)` for `n < 32`: no fault, the low `n` bits of `hold`; nothing else changes. -/
224theorem BITS_run (l : IL) (h : Heap) (n : UInt32) (hn : n.toNat < 32) :
225    runX (BITS n) l h = .ok ((.ok (l.hold.toUInt32 &&& ((1 : UInt32) <<< n - 1)), l), h) := by
226  have hs : shl32 1 n h = .ok (1 <<< n, h) := by rw [shl32_run _ _ hn]; rfl
227  unfold BITS
228  rw [runX_bind, runX_get]
229  simp only []
230  rw [runX_bind, runX_lift_ok hs]
231  rfl
232
233/-- The value of `BITS(n)` is `hold % 2^n`. -/
234theorem BITS_toNat (l : IL) (n : UInt32) (hn : n.toNat < 32) :
235    (l.hold.toUInt32 &&& ((1 : UInt32) <<< n - 1)).toNat = l.hold.toNat % 2 ^ n.toNat := by
236  rw [land_mask32 _ n.toNat _ (mask_toNat n hn)]
237  simp only [UInt64.toNat_toUInt32]
238  rw [Nat.mod_mod_of_dvd _ (Nat.pow_dvd_pow 2 (by omega))]
239
240/-- `DROPBITS(n)` for `n < 64`: no fault, `hold` shifts right and `bits` drops by `n`. -/
241theorem DROPBITS_run (l : IL) (h : Heap) (n : UInt32) (hn : n.toNat < 64) :
242    runX (DROPBITS n) l h = .ok ((.ok (), { l with hold := l.hold >>> n.toUInt64, bits := l.bits - n }), h) := by
243  have hs : shr64 l.hold n h = .ok (l.hold >>> n.toUInt64, h) := by rw [shr64_run _ _ hn]; rfl
244  unfold DROPBITS
245  rw [runX_bind, runX_get]
246  simp only []
247  rw [runX_bind, runX_lift_ok hs]
248  rfl
249
250/-- `DROPBITS(n)` consumes the first `n` stream bits. -/
251theorem DROPBITS_inv {h : Heap} {l : IL} {bs : List UInt8} (B : BitInv h l bs) (n : UInt32)
252    (hn : n.toNat ≤ l.bits.toNat) (hn64 : n.toNat < 64) :
253    BitInv h { l with hold := l.hold >>> n.toUInt64, bits := l.bits - n } bs ∧
254    stream { l with hold := l.hold >>> n.toUInt64, bits := l.bits - n } bs = (stream l bs).drop n.toNat ∧
255    (l.bits - n).toNat = l.bits.toNat - n.toNat := by
256  have hlt := B.hold_lt
257  have hsub : (l.bits - n).toNat = l.bits.toNat - n.toNat :=
258    UInt32.toNat_sub_of_le _ _ (UInt32.le_iff_toNat_le.mpr hn)
259  have hsh := shr64_toNat l.hold n hn64
260  refine ⟨⟨B.have_eq, B.next, ?_⟩, ?_, hsub⟩
261  · simp only [hsub, hsh]
262    rw [Nat.div_lt_iff_lt_mul (Nat.two_pow_pos _), ← Nat.pow_add, Nat.sub_add_cancel hn]
263    exact hlt
264  · unfold stream
265    simp only [hsub, hsh]
266    rw [List.drop_append_of_le_length (by simp [natBits_length]; exact hn), natBits_drop _ _ _ hn]
267
268/-- The registers after `BYTEBITS()`. -/
269def bytebits (l : IL) : IL :=
270  { l with hold := l.hold >>> (l.bits &&& 7).toUInt64, bits := l.bits - (l.bits &&& 7) }
271
272theorem and7_le (l : IL) : (l.bits &&& 7).toNat ≤ l.bits.toNat := by
273  rw [UInt32.toNat_and]; exact Nat.and_le_left
274
275theorem and7_toNat (l : IL) : (l.bits &&& 7).toNat = l.bits.toNat % 8 := by
276  rw [UInt32.toNat_and]
277  exact Nat.and_two_pow_sub_one_eq_mod _ 3
278
279theorem and7_lt (l : IL) : (l.bits &&& 7).toNat < 64 := by
280  rw [and7_toNat]; omega
281
282/-- `BYTEBITS()`: no fault, the registers become `bytebits`. -/
283theorem BYTEBITS_run (l : IL) (h : Heap) : runX BYTEBITS l h = .ok ((.ok (), bytebits l), h) := by
284  have hs : shr64 l.hold (l.bits &&& 7) h = .ok (l.hold >>> (l.bits &&& 7).toUInt64, h) := by
285    rw [shr64_run _ _ (and7_lt l)]; rfl
286  unfold BYTEBITS
287  rw [runX_bind, runX_get]
288  simp only []
289  rw [runX_bind, runX_lift_ok hs]
290  rfl
291
292/-- `BYTEBITS()` discards the `bits % 8` stream bits up to the next byte boundary. -/
293theorem BYTEBITS_inv {h : Heap} {l : IL} {bs : List UInt8} (B : BitInv h l bs) :
294    BitInv h (bytebits l) bs ∧ stream (bytebits l) bs = (stream l bs).drop (l.bits.toNat % 8) ∧
295    (bytebits l).bits.toNat % 8 = 0 := by
296  obtain ⟨B', hs, hsub⟩ := DROPBITS_inv B (l.bits &&& 7) (and7_le l) (and7_lt l)
297  rw [and7_toNat] at hs hsub
298  refine ⟨B', hs, ?_⟩
299  show (l.bits - (l.bits &&& 7)).toNat % 8 = 0
300  rw [hsub]
301  omega
302
303/-- `INITBITS()` empties the bit buffer. -/
304theorem INITBITS_inv {h : Heap} {l : IL} {bs : List UInt8} (B : BitInv h l bs) :
305    BitInv h { l with hold := 0, bits := 0 } bs ∧
306    stream { l with hold := 0, bits := 0 } bs = bytesBits bs := by
307  refine ⟨⟨B.have_eq, B.next, by simp⟩, ?_⟩
308  simp [stream, natBits]
309
310theorem runX_INITBITS (l : IL) (h : Heap) : runX INITBITS l h = .ok ((.ok (), { l with hold := 0, bits := 0 }), h) := rfl
311
312end Zlib.Inflate.Proofs