trees.c.bits.lean

Lean source with line numbers. Follow a line number to locate a statement, or an import to read its dependency.

1import ZlibF.Proof.«trees.c.inv»
2
3/-!
4# trees.c: the bit writers (`put_byte`, `put_short`, `send_bits`, `bi_reverse`, `bi_flush`, `bi_windup`)
5-/
6
7namespace Zlib.Trees.Proofs.Out
8open C Zlib.Trees
9
10theorem put_byte_run {h : Heap} {id : Nat} {d : DeflateState} {b : Nat} {buf : Array UInt8}
11    (hb : TreesBase h id d b buf) (hroom : d.pending.toNat < buf.size) (c : UInt8) :
12    put_byte (some (.tab id)) c h =
13      .ok ((), setD (setB h b (buf.set! d.pending.toNat c)) id { d with pending := d.pending + 1 }) := by
14  have hg : Space.get h (BRef.blk b) = some buf := hb.bytes
15  have e1 := Ptr.add_nat_ok (off := 0) (n := d.pending.toNat) hg (by omega)
16  have e2 := Ptr.store_ok (v := c) (off := 0 + d.pending.toNat) hg hb.rw (by omega)
17  unfold OkOn at e1
18  unfold put_byte
19  rw [bind_app, rd_run hb.dstate]
20  simp only [hb.pbuf]
21  rw [bind_app, e1]
22  simp only []
23  rw [bind_app]
24  unfold store8
25  rw [e2]
26  simp only []
27  have hd : (Space.put h (BRef.blk b) (buf.set! (0 + d.pending.toNat) c)).dstates id = some d := hb.dstate
28  rw [md_run hd]
29  simp [setD, Space.put, setB]
30  rw [hb.pbuf]
31
32
33@[simp] theorem setB_setB (h : Heap) (b : Nat) (a a' : Array UInt8) : setB (setB h b a) b a' = setB h b a' := by
34  simp [setB, upd_upd]
35
36theorem TreesBase.step {h : Heap} {id : Nat} {d : DeflateState} {b : Nat} {buf : Array UInt8}
37    (hb : TreesBase h id d b buf) (buf' : Array UInt8) (hsz : buf'.size = buf.size) (d' : DeflateState)
38    (hw : d'.WellFormed) (h1 : d'.pending_buf = d.pending_buf) (h2 : d'.pending_buf_size = d.pending_buf_size)
39    (h3 : d'.sym_buf = d.sym_buf) (h4 : d'.lit_bufsize = d.lit_bufsize) (h5 : d'.sym_end = d.sym_end)
40    (h6 : d'.pending.toNat ≤ d'.pending_buf_size.toNat) :
41    TreesBase (setD (setB h b buf') id d') id d' b buf' where
42  dstate := by simp
43  wf := hw
44  static := by simpa using hb.static
45  pbuf := by rw [h1]; exact hb.pbuf
46  bytes := by simp
47  rw := by simpa using hb.rw
48  size := by rw [hsz, h4]; exact hb.size
49  psize := by rw [hsz, h2]; exact hb.psize
50  sym := by rw [h3, h4]; exact hb.sym
51  lit_lo := by rw [h4]; exact hb.lit_lo
52  lit_hi := by rw [h4]; exact hb.lit_hi
53  sym_end := by rw [h5, h4]; exact hb.sym_end
54  pending_le := h6
55
56theorem toNat_add_one_u64 {x : UInt64} (hx : x.toNat < 2 ^ 20) : (x + 1).toNat = x.toNat + 1 := by
57  rw [UInt64.toNat_add]; simp; omega
58
59theorem toNat_add_two_u64 {x : UInt64} (hx : x.toNat < 2 ^ 20) : (x + 2).toNat = x.toNat + 2 := by
60  rw [UInt64.toNat_add]; simp; omega
61
62theorem TreesBase.pending_small {h : Heap} {id : Nat} {d : DeflateState} {b : Nat} {buf : Array UInt8}
63    (hb : TreesBase h id d b buf) : d.pending.toNat < 2 ^ 20 := by
64  have := hb.pending_le; have := hb.psize; have := hb.size; have := hb.lit_hi; omega
65
66theorem put_short_run {h : Heap} {id : Nat} {d : DeflateState} {b : Nat} {buf : Array UInt8}
67    (hb : TreesBase h id d b buf) (hroom : d.pending.toNat + 2 ≤ buf.size) (w : UInt16) :
68    put_short (some (.tab id)) w h =
69      .ok ((), setD (setB h b ((buf.set! d.pending.toNat (w &&& 0xff).toUInt8).set! (d.pending.toNat + 1)
70          (w >>> 8).toUInt8)) id { d with pending := d.pending + 2 }) := by
71  have hp := hb.pending_small
72  have hp1 := toNat_add_one_u64 hp
73  have hs1 := hb.size
74  have hs2 := hb.lit_hi
75  unfold put_short
76  rw [bind_app, put_byte_run hb (by omega)]
77  simp only []
78  have hb1 := hb.step (buf.set! d.pending.toNat (w &&& 0xff).toUInt8) (by simp) { d with pending := d.pending + 1 }
79    hb.wf rfl rfl rfl rfl rfl (by simp only []; rw [hp1]; have := hb.psize; omega)
80  rw [put_byte_run hb1 (by simp only []; rw [hp1]; simp; omega)]
81  simp only [setD_setB, setD_setD, setB_setB]
82  have e2 : d.pending + 1 + 1 = d.pending + 2 := by
83    apply UInt64.toNat_inj.mp
84    rw [toNat_add_one_u64 (by rw [hp1]; omega), hp1, toNat_add_two_u64 hp]
85  simp only [e2, hp1]
86
87
88theorem Buf_size_toInt : Buf_size.toInt = 16 := by decide
89
90/-- `(ush)value` as a natural number. -/
91def v16 (value : Int32) : Nat := (i2us value).toNat
92
93theorem v16_lt (value : Int32) : v16 value < 65536 := by
94  unfold v16; exact UInt16.toNat_lt _
95
96theorem shlUs_eq (value c : Int32) (h0 : 0 ≤ c.toInt) (h1 : c.toInt ≤ 31)
97    (h2 : v16 value * 2 ^ c.toInt.toNat < 2147483648) : shlUs value c = pure (v16 value * 2 ^ c.toInt.toNat) := by
98  funext h
99  have : ¬ (c.toInt < 0 ∨ 31 < c.toInt) := by omega
100  have h3 : ¬ ((i2us value).toNat * 2 ^ c.toInt.toNat ≥ 2147483648) := by unfold v16 at h2; omega
101  simp only [shlUs, this, h3, ite_false]
102  rfl
103
104theorem shrUs_eq (value c : Int32) (h0 : 0 ≤ c.toInt) (h1 : c.toInt ≤ 31) :
105    shrUs value c = pure (UInt16.ofNat (v16 value >>> c.toInt.toNat)) := by
106  funext h
107  have : ¬ (c.toInt < 0 ∨ 31 < c.toInt) := by omega
108  simp only [shrUs, this, ite_false]
109  rfl
110
111theorem i32_lt_iff {a b : Int32} : a < b ↔ a.toInt < b.toInt := Int32.lt_iff_toInt_lt
112
113
114theorem pow_mul_lt (v n m : Nat) (hv : v < 2 ^ n) : v * 2 ^ m < 2 ^ (n + m) := by
115  rw [Nat.pow_add]; exact Nat.mul_lt_mul_of_pos_right hv (Nat.pow_pos (by omega))
116
117theorem send_bits_B {h : Heap} {id : Nat} {d : DeflateState} {b : Nat} {buf : Array UInt8}
118    (hb : TreesBase h id d b buf) (hr : TreesRun id d) (value len : Int32)
119    (hl0 : 0 ≤ len.toInt) (hl1 : len.toInt ≤ 15) (hv : v16 value < 2 ^ len.toInt.toNat)
120    (hcase : d.bi_valid.toInt + len.toInt ≤ 16) :
121    send_bits (some (.tab id)) value len h =
122      .ok ((), setD h id { d with
123        bi_buf := UInt16.ofNat (d.bi_buf.toNat ||| v16 value * 2 ^ d.bi_valid.toInt.toNat),
124        bi_valid := Int32.ofInt (d.bi_valid.toInt + len.toInt) }) := by
125  have hbl := hr.bi_lo
126  have hbh := hr.bi_hi
127  have hlt := pow_mul_lt _ _ d.bi_valid.toInt.toNat hv
128  have hpow : 2 ^ (len.toInt.toNat + d.bi_valid.toInt.toNat) ≤ 2 ^ 16 :=
129    Nat.pow_le_pow_right (by omega) (by omega)
130  have hsh := shlUs_eq value d.bi_valid hr.bi_lo (by have := hr.bi_hi; omega) (by omega)
131  have hsub := isub_eq (a := Buf_size) (b := len) (by rw [Buf_size_toInt]; omega) (by rw [Buf_size_toInt]; omega)
132  have hnc : ¬ (d.bi_valid > Int32.ofInt (Buf_size.toInt - len.toInt)) := by
133    rw [gt_iff_lt, i32_lt_iff, i32_ofInt_toInt (by rw [Buf_size_toInt]; omega) (by rw [Buf_size_toInt]; omega),
134      Buf_size_toInt]
135    omega
136  unfold send_bits
137  rw [bind_app, rd_run hb.dstate]
138  simp only []
139  rw [bind_app, hsub]
140  simp only [pure_app, hnc, ite_false]
141  rw [bind_app, hsh]
142  simp only [pure_app]
143  rw [bind_app, md_run hb.dstate]
144  simp only []
145  have hd1 : (setD h id { d with bi_buf := UInt16.ofNat (d.bi_buf.toNat ||| v16 value * 2 ^ d.bi_valid.toInt.toNat) }).dstates id
146      = some _ := setD_dstates_same _ _ _
147  rw [bind_app, rd_run hd1]
148  simp only []
149  have hadd := iadd_eq (a := d.bi_valid) (b := len) (by omega) (by omega)
150  rw [bind_app, hadd]
151  simp only [pure_app]
152  rw [md_run hd1]
153  simp
154
155
156theorem TreesBase.stepD {h : Heap} {id : Nat} {d : DeflateState} {b : Nat} {buf : Array UInt8}
157    (hb : TreesBase h id d b buf) (d' : DeflateState)
158    (hw : d'.WellFormed) (h1 : d'.pending_buf = d.pending_buf) (h2 : d'.pending_buf_size = d.pending_buf_size)
159    (h3 : d'.sym_buf = d.sym_buf) (h4 : d'.lit_bufsize = d.lit_bufsize) (h5 : d'.sym_end = d.sym_end)
160    (h6 : d'.pending.toNat ≤ d'.pending_buf_size.toNat) :
161    TreesBase (setD h id d') id d' b buf where
162  dstate := by simp
163  wf := hw
164  static := by simpa using hb.static
165  pbuf := by rw [h1]; exact hb.pbuf
166  bytes := by simpa using hb.bytes
167  rw := by simpa using hb.rw
168  size := by rw [h4]; exact hb.size
169  psize := by rw [h2]; exact hb.psize
170  sym := by rw [h3, h4]; exact hb.sym
171  lit_lo := by rw [h4]; exact hb.lit_lo
172  lit_hi := by rw [h4]; exact hb.lit_hi
173  sym_end := by rw [h5, h4]; exact hb.sym_end
174  pending_le := h6
175
176theorem send_bits_A {h : Heap} {id : Nat} {d : DeflateState} {b : Nat} {buf : Array UInt8}
177    (hb : TreesBase h id d b buf) (hr : TreesRun id d) (value len : Int32)
178    (hl0 : 0 ≤ len.toInt) (hl1 : len.toInt ≤ 15) (hv : v16 value < 2 ^ len.toInt.toNat)
179    (hcase : 16 < d.bi_valid.toInt + len.toInt) (hroom : d.pending.toNat + 2 ≤ buf.size) :
180    send_bits (some (.tab id)) value len h =
181      .ok ((), setD (setB h b ((buf.set! d.pending.toNat
182            (UInt16.ofNat (d.bi_buf.toNat ||| v16 value * 2 ^ d.bi_valid.toInt.toNat) &&& 0xff).toUInt8).set!
183            (d.pending.toNat + 1) (UInt16.ofNat (d.bi_buf.toNat ||| v16 value * 2 ^ d.bi_valid.toInt.toNat) >>> 8).toUInt8))
184        id { d with
185          pending := d.pending + 2,
186          bi_buf := UInt16.ofNat (v16 value >>> (16 - d.bi_valid.toInt).toNat),
187          bi_valid := Int32.ofInt (d.bi_valid.toInt + len.toInt - 16) }) := by
188  have hbl := hr.bi_lo
189  have hbh := hr.bi_hi
190  have hlt := pow_mul_lt _ _ d.bi_valid.toInt.toNat hv
191  have hpow : 2 ^ (len.toInt.toNat + d.bi_valid.toInt.toNat) ≤ 2 ^ 31 :=
192    Nat.pow_le_pow_right (by omega) (by omega)
193  have hsh := shlUs_eq value d.bi_valid hr.bi_lo (by omega) (by omega)
194  have hsub := isub_eq (a := Buf_size) (b := len) (by rw [Buf_size_toInt]; omega) (by rw [Buf_size_toInt]; omega)
195  have hc : d.bi_valid > Int32.ofInt (Buf_size.toInt - len.toInt) := by
196    rw [gt_iff_lt, i32_lt_iff, i32_ofInt_toInt (by rw [Buf_size_toInt]; omega) (by rw [Buf_size_toInt]; omega),
197      Buf_size_toInt]
198    omega
199  have hb1 : TreesBase (setD h id { d with bi_buf := (UInt16.ofNat (d.bi_buf.toNat ||| v16 value * 2 ^ d.bi_valid.toInt.toNat)) }) id { d with bi_buf := (UInt16.ofNat (d.bi_buf.toNat ||| v16 value * 2 ^ d.bi_valid.toInt.toNat)) } b buf := hb.stepD _ hb.wf rfl rfl rfl rfl rfl hb.pending_le
200  have hd1 : (setD h id { d with bi_buf := (UInt16.ofNat (d.bi_buf.toNat ||| v16 value * 2 ^ d.bi_valid.toInt.toNat)) }).dstates id = some { d with bi_buf := (UInt16.ofNat (d.bi_buf.toNat ||| v16 value * 2 ^ d.bi_valid.toInt.toNat)) } := setD_dstates_same _ _ _
201  have hsr : isub Buf_size d.bi_valid = pure (Int32.ofInt (16 - d.bi_valid.toInt)) :=
202    isub_eq (by rw [Buf_size_toInt]; omega) (by rw [Buf_size_toInt]; omega) |>.trans (by rw [Buf_size_toInt])
203  have hrr := shrUs_eq value (Int32.ofInt (16 - d.bi_valid.toInt)) (by rw [i32_ofInt_toInt (by omega) (by omega)]; omega)
204    (by rw [i32_ofInt_toInt (by omega) (by omega)]; omega)
205  rw [i32_ofInt_toInt (by omega) (by omega)] at hrr
206  have hsl : isub len Buf_size = pure (Int32.ofInt (len.toInt - 16)) :=
207    isub_eq (by rw [Buf_size_toInt]; omega) (by rw [Buf_size_toInt]; omega) |>.trans (by rw [Buf_size_toInt])
208  unfold send_bits
209  rw [bind_app, rd_run hb.dstate]
210  simp only []
211  rw [bind_app, hsub]
212  simp only [pure_app, hc, ite_true]
213  rw [bind_app, hsh]
214  simp only [pure_app]
215  rw [bind_app, md_run hb.dstate]
216  simp only []
217  -- put_short s (← rd s).bi_buf
218  rw [bind_app, rd_run hd1]
219  simp only []
220  rw [bind_app, put_short_run hb1 (by simpa using hroom)]
221  simp only [setD_setB, setD_setD]
222  have hadd : iadd d.bi_valid (Int32.ofInt (len.toInt - 16)) =
223      pure (Int32.ofInt (d.bi_valid.toInt + len.toInt - 16)) := by
224    rw [iadd_eq (by rw [i32_ofInt_toInt (by omega) (by omega)]; omega)
225      (by rw [i32_ofInt_toInt (by omega) (by omega)]; omega), i32_ofInt_toInt (by omega) (by omega)]
226    simp only [Int.add_sub_assoc]
227  simp (disch := simp [hb.dstate]) only [bind_app, rd_run', md_run', hsr, hrr, hsl, hadd, pure_app, rdD_setD_same,
228    rdD_setB, setD_setD, setD_setB]
229  done
230
231
232theorem setB_self {h : Heap} {b : Nat} {buf : Array UInt8} (e : h.bytes b = some buf) : setB h b buf = h := by
233  have := upd_self h.bytes b buf e
234  cases h; simp only [setB] at *; simp_all
235
236theorem natBits_or_shift (old w n m : Nat) (ho : old < 2 ^ n) :
237    natBits (old ||| w * 2 ^ n) (n + m) = natBits old n ++ natBits w m := by
238  have hor : old ||| w * 2 ^ n = old + w * 2 ^ n := by
239    rw [Nat.or_comm, ← Nat.shiftLeft_eq, ← Nat.shiftLeft_add_eq_or_of_lt ho, Nat.add_comm]
240  rw [hor, natBits_add]
241  congr 1
242  · apply natBits_congr
243    rw [Nat.add_mul_mod_self_right]
244  · rw [Nat.shiftRight_eq_div_pow, Nat.add_mul_div_right _ _ (Nat.pow_pos (by omega)),
245      Nat.div_eq_of_lt ho, Nat.zero_add]
246
247theorem natBits_shr_lt (v n k : Nat) (hv : v < 2 ^ n) (hk : k ≤ n) : v >>> k < 2 ^ (n - k) := by
248  rw [Nat.shiftRight_eq_div_pow, Nat.div_lt_iff_lt_mul (Nat.pow_pos (by omega)), ← Nat.pow_add]
249  have : n - k + k = n := by omega
250  rw [this]; exact hv
251
252theorem toNat_lo (bb : UInt16) : ((bb &&& 0xff).toUInt8).toNat = bb.toNat % 256 := by
253  simp only [UInt16.toNat_toUInt8, UInt16.toNat_and]
254  rw [show (0xff : UInt16).toNat = 2 ^ 8 - 1 from rfl, Nat.and_two_pow_sub_one_eq_mod]; omega
255
256theorem natBits_word (W : UInt16) :
257    natBits (((W &&& 0xff).toUInt8).toNat) 8 ++ natBits (((W >>> 8).toUInt8).toNat) 8 = natBits W.toNat 16 := by
258  rw [show (16 : Nat) = 8 + 8 from rfl, natBits_add]
259  congr 1
260  · apply natBits_congr
261    rw [toNat_lo]; show W.toNat % 256 % 2 ^ 8 = W.toNat % 2 ^ 8; simp
262  · apply natBits_congr
263    simp [UInt16.toNat_toUInt8, UInt16.toNat_shiftRight]
264
265
266theorem u16_toNat_ofNat_mod (x : Nat) : (UInt16.ofNat x).toNat = x % 65536 := by
267  first | exact UInt16.toNat_ofNat x | simp | (simp [UInt16.toNat, UInt16.ofNat, BitVec.toNat_ofNat])
268
269theorem u16_toNat_ofNat_lt {x : Nat} (hx : x < 65536) : (UInt16.ofNat x).toNat = x := by
270  first | exact UInt16.toNat_ofNat_of_lt' hx | exact UInt16.toNat_ofNat_of_lt hx | (simp [UInt16.toNat_ofNat]; omega) | (simp; omega)
271
272theorem send_bits_spec_B {h : Heap} {id : Nat} {d : DeflateState} {b : Nat} {buf : Array UInt8}
273    (hI : TreesInvAt h id d b buf) (value len : Int32)
274    (hl0 : 0 ≤ len.toInt) (hl1 : len.toInt ≤ 15) (hv : v16 value < 2 ^ len.toInt.toNat)
275    (hcase : d.bi_valid.toInt + len.toInt ≤ 16) :
276    ∃ d', send_bits (some (.tab id)) value len h = .ok ((), setD h id d') ∧
277      TreesInvAt (setD h id d') id d' b buf ∧
278      outBits buf d' = outBits buf d ++ natBits (v16 value) len.toInt.toNat ∧
279      d'.pending = d.pending ∧ (∃ a v, d' = { d with bi_buf := a, bi_valid := v }) := by
280  obtain ⟨hb, hr⟩ := hI
281  have hbl := hr.bi_lo
282  have hbh := hr.bi_hi
283  have hbb := hr.bi_buf
284  have hlt := pow_mul_lt _ _ d.bi_valid.toInt.toNat hv
285  have hpow : 2 ^ (len.toInt.toNat + d.bi_valid.toInt.toNat) ≤ 2 ^ 16 :=
286    Nat.pow_le_pow_right (by omega) (by omega)
287  have hor : d.bi_buf.toNat ||| v16 value * 2 ^ d.bi_valid.toInt.toNat < 2 ^ (d.bi_valid.toInt.toNat + len.toInt.toNat) := by
288    apply Nat.or_lt_two_pow
289    · exact Nat.lt_of_lt_of_le hbb (Nat.pow_le_pow_right (by omega) (by omega))
290    · rw [Nat.add_comm]; exact hlt
291  have hx : d.bi_buf.toNat ||| v16 value * 2 ^ d.bi_valid.toInt.toNat < 65536 := by
292    have : 2 ^ (d.bi_valid.toInt.toNat + len.toInt.toNat) ≤ 2 ^ 16 := by rw [Nat.add_comm]; exact hpow
293    omega
294  have hnv : (Int32.ofInt (d.bi_valid.toInt + len.toInt)).toInt = d.bi_valid.toInt + len.toInt :=
295    i32_ofInt_toInt (by omega) (by omega)
296  refine ⟨_, send_bits_B hb hr value len hl0 hl1 hv hcase, ?_, ?_, rfl, _, _, rfl⟩
297  · refine ⟨hb.stepD _ hb.wf rfl rfl rfl rfl rfl hb.pending_le, ?_⟩
298    refine ⟨hr.ldyn, hr.lstat, hr.ddyn, hr.dstat, hr.bldyn, hr.blstat, ?_, ?_, ?_, hr.sym_next_le, hr.sym_next_mod⟩
299    · show 0 ≤ (Int32.ofInt _).toInt; rw [hnv]; omega
300    · show (Int32.ofInt _).toInt ≤ 16; rw [hnv]; omega
301    · show (UInt16.ofNat _).toNat < 2 ^ (Int32.ofInt _).toInt.toNat
302      rw [hnv, u16_toNat_ofNat_lt hx]
303      have : (d.bi_valid.toInt + len.toInt).toNat = d.bi_valid.toInt.toNat + len.toInt.toNat := by omega
304      rw [this]; exact hor
305  · unfold outBits
306    show bytesBits buf d.pending.toNat ++ natBits (UInt16.ofNat _).toNat (Int32.ofInt _).toInt.toNat = _
307    rw [hnv, u16_toNat_ofNat_lt hx]
308    have : (d.bi_valid.toInt + len.toInt).toNat = d.bi_valid.toInt.toNat + len.toInt.toNat := by omega
309    rw [this, natBits_or_shift _ _ _ _ hbb, List.append_assoc]
310
311
312theorem getD_set_u8 (a : Array UInt8) (i j : Nat) (v : UInt8) :
313    (a.set! i v).getD j 0 = if i = j ∧ i < a.size then v else a.getD j 0 := by
314  rw [Array.set!_eq_setIfInBounds, Array.getD_eq_getD_getElem?, Array.getD_eq_getD_getElem?,
315    Array.getElem?_setIfInBounds]
316  by_cases h1 : i = j
317  · subst h1; by_cases h2 : i < a.size <;> simp [h2]
318  · simp [h1]
319
320/-- Two bytes appended at `p`: the bits of the pending bytes grow by those of the two bytes. -/
321theorem bytesBits_two {buf : Array UInt8} {p : Nat} (v0 v1 : UInt8) (hp : p + 2 ≤ buf.size) :
322    bytesBits ((buf.set! p v0).set! (p + 1) v1) (p + 2) = bytesBits buf p ++ natBits v0.toNat 8 ++ natBits v1.toNat 8 := by
323  have e1 : ((buf.set! p v0).set! (p + 1) v1).getD (p + 1) 0 = v1 := by
324    rw [getD_set_u8]; simp; omega
325  have e0 : ((buf.set! p v0).set! (p + 1) v1).getD p 0 = v0 := by
326    rw [getD_set_u8, getD_set_u8]; simp
327    intro h; omega
328  rw [show p + 2 = (p + 1) + 1 from rfl, bytesBits_succ, bytesBits_succ, bytesBits_set _ (by omega),
329    bytesBits_set _ (by omega), e1, e0]
330
331
332theorem send_bits_spec_A {h : Heap} {id : Nat} {d : DeflateState} {b : Nat} {buf : Array UInt8}
333    (hI : TreesInvAt h id d b buf) (value len : Int32)
334    (hl0 : 0 ≤ len.toInt) (hl1 : len.toInt ≤ 15) (hv : v16 value < 2 ^ len.toInt.toNat)
335    (hcase : 16 < d.bi_valid.toInt + len.toInt) (hroom : d.pending.toNat + 2 ≤ buf.size) :
336    ∃ buf' d', send_bits (some (.tab id)) value len h = .ok ((), setD (setB h b buf') id d') ∧
337      TreesInvAt (setD (setB h b buf') id d') id d' b buf' ∧
338      outBits buf' d' = outBits buf d ++ natBits (v16 value) len.toInt.toNat ∧
339      buf'.size = buf.size ∧
340      (∀ i, (i < d.pending.toNat ∨ d.pending.toNat + 2 ≤ i) → buf'.getD i 0 = buf.getD i 0) ∧
341      d'.pending = d.pending + 2 ∧ (∃ a v, d' = { d with pending := d.pending + 2, bi_buf := a, bi_valid := v }) := by
342  obtain ⟨hb, hr⟩ := hI
343  have hbl := hr.bi_lo
344  have hbh := hr.bi_hi
345  have hbb := hr.bi_buf
346  have hp := hb.pending_small
347  have hp2 := toNat_add_two_u64 hp
348  have hs1 := hb.size
349  have hs2 := hb.lit_hi
350  have hpsz := hb.psize
351  have hvl := v16_lt value
352  obtain ⟨W, hW⟩ : ∃ W, W = UInt16.ofNat (d.bi_buf.toNat ||| v16 value * 2 ^ d.bi_valid.toInt.toNat) := ⟨_, rfl⟩
353  have hA := send_bits_A hb hr value len hl0 hl1 hv hcase hroom
354  rw [← hW] at hA
355  have hnv : (Int32.ofInt (d.bi_valid.toInt + len.toInt - 16)).toInt = d.bi_valid.toInt + len.toInt - 16 :=
356    i32_ofInt_toInt (by omega) (by omega)
357  have hshr : v16 value >>> (16 - d.bi_valid.toInt).toNat < 2 ^ (d.bi_valid.toInt + len.toInt - 16).toNat := by
358    have := natBits_shr_lt (v16 value) len.toInt.toNat (16 - d.bi_valid.toInt).toNat hv (by omega)
359    have e : len.toInt.toNat - (16 - d.bi_valid.toInt).toNat = (d.bi_valid.toInt + len.toInt - 16).toNat := by omega
360    rwa [e] at this
361  have hsr : v16 value >>> (16 - d.bi_valid.toInt).toNat ≤ v16 value := by
362    rw [Nat.shiftRight_eq_div_pow]; exact Nat.div_le_self _ _
363  have hbuf2 : ((buf.set! d.pending.toNat (W &&& 0xff).toUInt8).set! (d.pending.toNat + 1) (W >>> 8).toUInt8).size
364      = buf.size := by simp
365  refine ⟨_, _, hA, ?_, ?_, hbuf2, ?_, ?_, _, _, rfl⟩
366  · refine ⟨hb.step _ hbuf2 _ hb.wf rfl rfl rfl rfl rfl (by simp only []; rw [hp2]; omega), ?_⟩
367    refine ⟨hr.ldyn, hr.lstat, hr.ddyn, hr.dstat, hr.bldyn, hr.blstat, ?_, ?_, ?_, hr.sym_next_le, hr.sym_next_mod⟩
368    · show 0 ≤ (Int32.ofInt _).toInt; rw [hnv]; omega
369    · show (Int32.ofInt _).toInt ≤ 16; rw [hnv]; omega
370    · show (UInt16.ofNat _).toNat < 2 ^ (Int32.ofInt _).toInt.toNat
371      rw [hnv, u16_toNat_ofNat_lt (by omega)]
372      exact hshr
373  · unfold outBits
374    show bytesBits _ (d.pending + 2).toNat ++ natBits (UInt16.ofNat _).toNat (Int32.ofInt _).toInt.toNat = _
375    rw [hp2, bytesBits_two _ _ (by omega), hnv, u16_toNat_ofNat_lt (by omega)]
376    have hw16 : natBits (((W &&& 0xff).toUInt8).toNat) 8 ++ natBits (((W >>> 8).toUInt8).toNat) 8
377        = natBits d.bi_buf.toNat d.bi_valid.toInt.toNat ++ natBits (v16 value) (16 - d.bi_valid.toInt).toNat := by
378      rw [natBits_word]
379      have : natBits W.toNat 16
380          = natBits (d.bi_buf.toNat ||| v16 value * 2 ^ d.bi_valid.toInt.toNat) 16 := by
381        apply natBits_congr
382        rw [hW, u16_toNat_ofNat_mod]; simp
383      rw [this, show (16 : Nat) = d.bi_valid.toInt.toNat + (16 - d.bi_valid.toInt).toNat by omega,
384        natBits_or_shift _ _ _ _ hbb]
385    have hsplit : natBits (v16 value) len.toInt.toNat =
386        natBits (v16 value) (16 - d.bi_valid.toInt).toNat ++
387          natBits (v16 value >>> (16 - d.bi_valid.toInt).toNat) (d.bi_valid.toInt + len.toInt - 16).toNat := by
388      rw [← natBits_add]; congr 1; omega
389    rw [hsplit]
390    have := congrArg (· ++ natBits (v16 value >>> (16 - d.bi_valid.toInt).toNat)
391      (d.bi_valid.toInt + len.toInt - 16).toNat) hw16
392    simp only [List.append_assoc] at this ⊢
393    rw [this]
394  · intro i hi
395    have h1 : ¬ (d.pending.toNat + 1 = i) := by omega
396    have h2 : ¬ (d.pending.toNat = i) := by omega
397    rw [getD_set_u8, getD_set_u8]
398    simp [h1, h2]
399  · rfl
400
401
402/-- **`send_bits`, safety and specification.** `send_bits(s, value, length)` appends the `length` low bits of `value`
403(least significant first) to the output bit stream `outBits`: the bits of the pending bytes followed by those of
404`bi_buf`. Preconditions: `TreesInvAt` (so `bi_valid <= 16`, no stray bits in `bi_buf`); `0 <= length <= 15` (every
405caller in `trees.c` sends at most 15 bits: codes have length at most 15, extra bits at most 13);
406`(ush)value < 2^length` (the value has no bits above its length: true for the codes of `gen_codes`, for the extra
407bits, and for the block header); and room: the bits already written plus `length` fit in `pending_buf`
408(`8 * pending + bi_valid + length <= 8 * pending_buf_size`; `deflate.c` establishes this by the overlay lemma F9).
409Afterwards: no fault, `TreesInvAt` again for the same byte block `b`, the stream grew by exactly the bits, at most
410two bytes were written at `pending_buf[pending]` and the bytes outside `[pending, pending')` are unchanged. -/
411theorem send_bits_spec {h : Heap} {id : Nat} {d : DeflateState} {b : Nat} {buf : Array UInt8}
412    (hI : TreesInvAt h id d b buf) (value len : Int32)
413    (hl0 : 0 ≤ len.toInt) (hl1 : len.toInt ≤ 15) (hv : v16 value < 2 ^ len.toInt.toNat)
414    (hroom : 8 * d.pending.toNat + d.bi_valid.toInt.toNat + len.toInt.toNat ≤ 8 * buf.size) :
415    ∃ buf' d', send_bits (some (.tab id)) value len h = .ok ((), setD (setB h b buf') id d') ∧
416      TreesInvAt (setD (setB h b buf') id d') id d' b buf' ∧
417      outBits buf' d' = outBits buf d ++ natBits (v16 value) len.toInt.toNat ∧
418      buf'.size = buf.size ∧
419      (∀ i, (i < d.pending.toNat ∨ d'.pending.toNat ≤ i) → buf'.getD i 0 = buf.getD i 0) ∧
420      d.pending.toNat ≤ d'.pending.toNat ∧ d'.pending.toNat ≤ d.pending.toNat + 2 ∧
421      (∃ p a v, d' = { d with pending := p, bi_buf := a, bi_valid := v }) := by
422  have hbl := hI.run.bi_lo
423  have hbh := hI.run.bi_hi
424  by_cases hcase : d.bi_valid.toInt + len.toInt ≤ 16
425  · obtain ⟨d', e, hinv, hbits, hpend, a, v, hd'⟩ := send_bits_spec_B hI value len hl0 hl1 hv hcase
426    refine ⟨buf, d', ?_, ?_, hbits, rfl, fun _ _ => rfl, by rw [hpend]; exact Nat.le_refl _,
427      by rw [hpend]; omega, ?_⟩
428    · rw [setB_self hI.base.bytes]; exact e
429    · rw [setB_self hI.base.bytes]; exact hinv
430    · exact ⟨d.pending, a, v, by rw [hd']⟩
431  · have hcase' : 16 < d.bi_valid.toInt + len.toInt := by omega
432    have hpe := hI.base.pending_small
433    obtain ⟨buf', d', e, hinv, hbits, hsz, hfr, hpend, a, v, hd'⟩ :=
434      send_bits_spec_A hI value len hl0 hl1 hv hcase' (by omega)
435    have hp2 := toNat_add_two_u64 hpe
436    refine ⟨buf', d', e, hinv, hbits, hsz, ?_, by rw [hpend, hp2]; omega, by rw [hpend, hp2]; omega,
437      ⟨_, a, v, hd'⟩⟩
438    intro i hi
439    apply hfr
440    rw [hpend, hp2] at hi
441    omega
442
443
444theorem i32_beq_toInt (a b : Int32) : (a == b) = decide (a.toInt = b.toInt) := by
445  by_cases h : a = b
446  · subst h; simp
447  · have : a.toInt ≠ b.toInt := fun e => h (Int32.toInt_inj.mp e)
448    simp [h, this]
449
450theorem i32_le_toInt {a b : Int32} : a ≤ b ↔ a.toInt ≤ b.toInt := Int32.le_iff_toInt_le
451
452theorem i32_16 : (16 : Int32).toInt = 16 := by decide
453theorem i32_8 : (8 : Int32).toInt = 8 := by decide
454theorem i32_0 : (0 : Int32).toInt = 0 := by decide
455
456theorem u16_shr8_toNat (w : UInt16) : (w >>> 8).toNat = w.toNat / 256 := by
457  simp [Nat.shiftRight_eq_div_pow]
458
459theorem bi_flush_16 {h : Heap} {id : Nat} {d : DeflateState} {b : Nat} {buf : Array UInt8}
460    (hb : TreesBase h id d b buf) (hv : d.bi_valid.toInt = 16) (hroom : d.pending.toNat + 2 ≤ buf.size) :
461    bi_flush (some (.tab id)) h =
462      .ok ((), setD (setB h b ((buf.set! d.pending.toNat (d.bi_buf &&& 0xff).toUInt8).set! (d.pending.toNat + 1)
463          (d.bi_buf >>> 8).toUInt8)) id { d with pending := d.pending + 2, bi_buf := 0, bi_valid := 0 }) := by
464  have hc : (d.bi_valid == 16) = true := by rw [i32_beq_toInt, i32_16]; simp [hv]
465  unfold bi_flush
466  rw [bind_app, rd_run hb.dstate]
467  simp only [hc, ite_true]
468  rw [bind_app, rd_run hb.dstate]
469  simp only []
470  rw [bind_app, put_short_run hb hroom]
471  simp (disch := simp [hb.dstate]) only [setD_setB, setD_setD, bind_app, rd_run', md_run', rdD_setD_same, rdD_setB,
472    setD_setB]
473
474
475theorem bi_flush_mid {h : Heap} {id : Nat} {d : DeflateState} {b : Nat} {buf : Array UInt8}
476    (hb : TreesBase h id d b buf) (hv8 : 8 ≤ d.bi_valid.toInt) (hv16 : d.bi_valid.toInt < 16)
477    (hroom : d.pending.toNat + 1 ≤ buf.size) :
478    bi_flush (some (.tab id)) h =
479      .ok ((), setD (setB h b (buf.set! d.pending.toNat d.bi_buf.toUInt8)) id
480        { d with pending := d.pending + 1, bi_buf := d.bi_buf >>> 8,
481                 bi_valid := Int32.ofInt (d.bi_valid.toInt - 8) }) := by
482  have hc : (d.bi_valid == 16) = false := by rw [i32_beq_toInt, i32_16]; simp; omega
483  have hge : d.bi_valid ≥ 8 := by
484    show 8 ≤ d.bi_valid
485    rw [i32_le_toInt, i32_8]; exact hv8
486  have hsub : isub d.bi_valid 8 = pure (Int32.ofInt (d.bi_valid.toInt - 8)) :=
487    (isub_eq (a := d.bi_valid) (b := 8) (by rw [i32_8]; omega) (by rw [i32_8]; omega)).trans (by rw [i32_8])
488  have hp := hb.pending_small
489  have hs1 := hb.size
490  have hs2 := hb.lit_hi
491  have hp1 := toNat_add_one_u64 hp
492  unfold bi_flush
493  rw [bind_app, rd_run hb.dstate]
494  simp only [hc, hge, ite_true, ite_false, Bool.false_eq_true]
495  rw [bind_app, rd_run hb.dstate]
496  simp only []
497  rw [bind_app, put_byte_run hb hroom]
498  simp (disch := simp [hb.dstate]) only [setD_setB, setD_setD, bind_app, rd_run', md_run', rdD_setD_same, rdD_setB,
499    hsub, pure_app]
500
501theorem bi_flush_low {h : Heap} {id : Nat} {d : DeflateState} (hd : h.dstates id = some d)
502    (hv8 : d.bi_valid.toInt < 8) : bi_flush (some (.tab id)) h = .ok ((), h) := by
503  have hc : (d.bi_valid == 16) = false := by rw [i32_beq_toInt, i32_16]; simp; omega
504  have hge : ¬ d.bi_valid ≥ 8 := by
505    show ¬ 8 ≤ d.bi_valid
506    rw [i32_le_toInt, i32_8]; omega
507  unfold bi_flush
508  rw [bind_app, rd_run hd]
509  simp only [hc, hge, ite_true, ite_false, Bool.false_eq_true]
510  rfl
511
512
513theorem setD_self {h : Heap} {id : Nat} {d : DeflateState} (e : h.dstates id = some d) : setD h id d = h := by
514  have := upd_self h.dstates id d e
515  cases h; simp only [setD] at *; simp_all
516
517theorem bytesBits_one {buf : Array UInt8} {p : Nat} (v : UInt8) (hp : p < buf.size) :
518    bytesBits (buf.set! p v) (p + 1) = bytesBits buf p ++ natBits v.toNat 8 := by
519  rw [bytesBits_succ, bytesBits_set _ (Nat.le_refl _)]
520  rw [show (buf.set! p v).getD p 0 = v by rw [getD_set_u8]; simp; omega]
521
522theorem natBits_byte (w : UInt16) : natBits (w.toUInt8).toNat 8 = natBits w.toNat 8 := by
523  apply natBits_congr
524  rw [UInt16.toNat_toUInt8]; simp
525
526theorem TreesRun.with_bi {id : Nat} {d : DeflateState} (hr : TreesRun id d) (d' : DeflateState)
527    (h1 : d'.l_desc = d.l_desc) (h2 : d'.d_desc = d.d_desc) (h3 : d'.bl_desc = d.bl_desc)
528    (h4 : 0 ≤ d'.bi_valid.toInt) (h5 : d'.bi_valid.toInt ≤ 16)
529    (h6 : d'.bi_buf.toNat < 2 ^ d'.bi_valid.toInt.toNat) (h7 : d'.sym_next = d.sym_next)
530    (h8 : d'.sym_end = d.sym_end) : TreesRun id d' where
531  ldyn := by rw [h1]; exact hr.ldyn
532  lstat := by rw [h1]; exact hr.lstat
533  ddyn := by rw [h2]; exact hr.ddyn
534  dstat := by rw [h2]; exact hr.dstat
535  bldyn := by rw [h3]; exact hr.bldyn
536  blstat := by rw [h3]; exact hr.blstat
537  bi_lo := h4
538  bi_hi := h5
539  bi_buf := h6
540  sym_next_le := by rw [h7, h8]; exact hr.sym_next_le
541  sym_next_mod := by rw [h7]; exact hr.sym_next_mod
542
543/-- **`bi_flush`, safety and specification.** Writes the complete bytes of `bi_buf` to the pending output: the
544output bit stream `outBits` is unchanged and `bi_valid < 8` afterwards. Precondition: `TreesInvAt` and the bits
545already written fit in `pending_buf` (`8 * pending + bi_valid <= 8 * pending_buf_size`, from the overlay
546lemma F9; `bi_valid = 16` needs 2 bytes, `bi_valid >= 8` needs 1). Called by `_tr_flush_bits` (from
547`flush_pending`) and `_tr_align`. -/
548theorem bi_flush_spec {h : Heap} {id : Nat} {d : DeflateState} {b : Nat} {buf : Array UInt8}
549    (hI : TreesInvAt h id d b buf)
550    (hroom : 8 * d.pending.toNat + d.bi_valid.toInt.toNat ≤ 8 * buf.size) :
551    ∃ buf' d', bi_flush (some (.tab id)) h = .ok ((), setD (setB h b buf') id d') ∧
552      TreesInvAt (setD (setB h b buf') id d') id d' b buf' ∧
553      outBits buf' d' = outBits buf d ∧ d'.bi_valid.toInt < 8 ∧
554      buf'.size = buf.size ∧
555      (∀ i, (i < d.pending.toNat ∨ d'.pending.toNat ≤ i) → buf'.getD i 0 = buf.getD i 0) ∧
556      d.pending.toNat ≤ d'.pending.toNat ∧ d'.pending.toNat ≤ d.pending.toNat + 2 ∧
557      (∃ p a v, d' = { d with pending := p, bi_buf := a, bi_valid := v }) := by
558  obtain ⟨hb, hr⟩ := hI
559  have hbl := hr.bi_lo
560  have hbh := hr.bi_hi
561  have hbb := hr.bi_buf
562  have hp := hb.pending_small
563  have hs1 := hb.size
564  have hs2 := hb.lit_hi
565  have hp1 := toNat_add_one_u64 hp
566  have hpsz := hb.psize
567  by_cases h16 : d.bi_valid.toInt = 16
568  · have hroom2 : d.pending.toNat + 2 ≤ buf.size := by
569      have : d.bi_valid.toInt.toNat = 16 := by omega
570      omega
571    have hp2 := toNat_add_two_u64 hp
572    have hbuf2 : ((buf.set! d.pending.toNat (d.bi_buf &&& 0xff).toUInt8).set! (d.pending.toNat + 1)
573        (d.bi_buf >>> 8).toUInt8).size = buf.size := by simp
574    refine ⟨_, _, bi_flush_16 hb h16 hroom2, ?_, ?_, ?_, hbuf2, ?_, ?_, ?_, ⟨_, _, _, rfl⟩⟩
575    · refine ⟨hb.step _ hbuf2 _ hb.wf rfl rfl rfl rfl rfl (by simp only []; rw [hp2]; omega), ?_⟩
576      refine hr.with_bi _ rfl rfl rfl ?_ ?_ ?_ rfl rfl
577      · show 0 ≤ (0 : Int32).toInt; rw [i32_0]; omega
578      · show (0 : Int32).toInt ≤ 16; rw [i32_0]; omega
579      · show (0 : UInt16).toNat < 2 ^ (0 : Int32).toInt.toNat; rw [i32_0]; simp
580    · unfold outBits
581      show bytesBits _ (d.pending + 2).toNat ++ natBits (0 : UInt16).toNat (0 : Int32).toInt.toNat = _
582      rw [hp2, bytesBits_two _ _ (by omega), i32_0, List.append_assoc (bytesBits _ _), natBits_word, h16]
583      simp [natBits]
584    · show (0 : Int32).toInt < 8; rw [i32_0]; omega
585    · intro i hi
586      have h1 : ¬ (d.pending.toNat + 1 = i) := by simp only [] at hi; rw [hp2] at hi; omega
587      have h2 : ¬ (d.pending.toNat = i) := by simp only [] at hi; rw [hp2] at hi; omega
588      rw [getD_set_u8, getD_set_u8]
589      simp [h1, h2]
590    · show d.pending.toNat ≤ (d.pending + 2).toNat; rw [hp2]; omega
591    · show (d.pending + 2).toNat ≤ _; rw [hp2]; exact Nat.le_refl _
592  · by_cases h8 : 8 ≤ d.bi_valid.toInt
593    · have hlt16 : d.bi_valid.toInt < 16 := by omega
594      have hroom1 : d.pending.toNat + 1 ≤ buf.size := by
595        have : 8 ≤ d.bi_valid.toInt.toNat := by omega
596        omega
597      have hbuf1 : (buf.set! d.pending.toNat d.bi_buf.toUInt8).size = buf.size := by simp
598      have hnv : (Int32.ofInt (d.bi_valid.toInt - 8)).toInt = d.bi_valid.toInt - 8 :=
599        i32_ofInt_toInt (by omega) (by omega)
600      refine ⟨_, _, bi_flush_mid hb h8 hlt16 hroom1, ?_, ?_, ?_, hbuf1, ?_, ?_, ?_, ⟨_, _, _, rfl⟩⟩
601      · refine ⟨hb.step _ hbuf1 _ hb.wf rfl rfl rfl rfl rfl (by simp only []; rw [hp1]; omega), ?_⟩
602        refine hr.with_bi _ rfl rfl rfl ?_ ?_ ?_ rfl rfl
603        · show 0 ≤ (Int32.ofInt _).toInt; rw [hnv]; omega
604        · show (Int32.ofInt _).toInt ≤ 16; rw [hnv]; omega
605        · show (d.bi_buf >>> 8).toNat < 2 ^ (Int32.ofInt _).toInt.toNat
606          rw [hnv, u16_shr8_toNat]
607          have := natBits_shr_lt d.bi_buf.toNat d.bi_valid.toInt.toNat 8 hbb (by omega)
608          rw [Nat.shiftRight_eq_div_pow] at this
609          have e : (d.bi_valid.toInt - 8).toNat = d.bi_valid.toInt.toNat - 8 := by omega
610          rw [e]; simpa using this
611      · unfold outBits
612        show bytesBits _ (d.pending + 1).toNat ++ natBits (d.bi_buf >>> 8).toNat (Int32.ofInt _).toInt.toNat = _
613        rw [hp1, bytesBits_one _ (by omega), hnv, natBits_byte, u16_shr8_toNat, List.append_assoc]
614        congr 1
615        have e : d.bi_valid.toInt.toNat = 8 + (d.bi_valid.toInt - 8).toNat := by omega
616        conv => rhs; rw [e, natBits_add]
617        rw [Nat.shiftRight_eq_div_pow]
618      · show (Int32.ofInt _).toInt < 8; rw [hnv]; omega
619      · intro i hi
620        have h2 : ¬ (d.pending.toNat = i) := by simp only [] at hi; rw [hp1] at hi; omega
621        rw [getD_set_u8]
622        simp [h2]
623      · show d.pending.toNat ≤ (d.pending + 1).toNat; rw [hp1]; omega
624      · show (d.pending + 1).toNat ≤ _; rw [hp1]; omega
625    · have hlt8 : d.bi_valid.toInt < 8 := by omega
626      refine ⟨buf, d, ?_, ?_, rfl, hlt8, rfl, fun _ _ => rfl, Nat.le_refl _, by omega, ⟨_, _, _, rfl⟩⟩
627      · rw [setB_self hb.bytes, setD_self hb.dstate]; exact bi_flush_low hb.dstate hlt8
628      · rw [setB_self hb.bytes, setD_self hb.dstate]; exact ⟨hb, hr⟩
629
630
631/-- The last part of `bi_windup`: `bi_used = ((bi_valid - 1) & 7) + 1`, then clear the bit buffer. -/
632def windupTail (s : DeflateStatePtr) : M Unit := do
633  let t ← isub (← rd s).bi_valid 1
634  let u ← iadd (t &&& 7) 1
635  md s fun d => { d with bi_used := u }
636  md s fun d => { d with bi_buf := 0 }
637  md s fun d => { d with bi_valid := 0 }
638
639/-- `bi_used` as `bi_windup` computes it, for `0 <= bi_valid <= 16`. -/
640def usedOf (bv : Int) : Int := if bv = 0 then 8 else (bv - 1) % 8 + 1
641
642theorem usedOf_key : ∀ k : Fin 17, ((Int32.ofInt ((k : Int) - 1)) &&& 7).toInt + 1 = usedOf (k : Int) := by decide
643
644theorem i32_1 : (1 : Int32).toInt = 1 := by decide
645
646theorem windupTail_run {h : Heap} {id : Nat} {d : DeflateState} (hd : h.dstates id = some d)
647    (hl : 0 ≤ d.bi_valid.toInt) (hh : d.bi_valid.toInt ≤ 16) :
648    windupTail (some (.tab id)) h =
649      .ok ((), setD h id { d with bi_used := Int32.ofInt (usedOf d.bi_valid.toInt), bi_buf := 0, bi_valid := 0 }) := by
650  have hne : h.dstates id ≠ none := by simp [hd]
651  have hsub : isub d.bi_valid 1 = pure (Int32.ofInt (d.bi_valid.toInt - 1)) :=
652    (isub_eq (a := d.bi_valid) (b := 1) (by rw [i32_1]; omega) (by rw [i32_1]; omega)).trans (by rw [i32_1])
653  obtain ⟨n, hn⟩ : ∃ n : Nat, (n : Int) = d.bi_valid.toInt := ⟨d.bi_valid.toInt.toNat, Int.toNat_of_nonneg hl⟩
654  have hkey := usedOf_key ⟨n, by omega⟩
655  simp only [] at hkey
656  rw [hn] at hkey
657  have h1 : usedOf d.bi_valid.toInt ≤ 8 := by unfold usedOf; split <;> omega
658  have h2 : 1 ≤ usedOf d.bi_valid.toInt := by unfold usedOf; split <;> omega
659  have hadd : iadd (Int32.ofInt (d.bi_valid.toInt - 1) &&& 7) 1 = pure (Int32.ofInt (usedOf d.bi_valid.toInt)) := by
660    rw [iadd_eq (a := Int32.ofInt (d.bi_valid.toInt - 1) &&& 7) (b := 1) (by rw [i32_1]; omega)
661      (by rw [i32_1]; omega), i32_1, hkey]
662  have hrd : rdD h id = d := by simp [rdD, hd]
663  unfold windupTail
664  simp (disch := simp [hd]) only [bind_app, rd_run', md_run', rdD_setD_same, hrd, hsub, hadd, pure_app, setD_setD]
665  done
666
667
668theorem i32_gt_toInt {a b : Int32} : a > b ↔ a.toInt > b.toInt := by
669  rw [gt_iff_lt, Int32.lt_iff_toInt_lt]
670
671theorem bi_windup_big {h : Heap} {id : Nat} {d : DeflateState} {b : Nat} {buf : Array UInt8}
672    (hb : TreesBase h id d b buf) (hl : 0 ≤ d.bi_valid.toInt) (hh : d.bi_valid.toInt ≤ 16)
673    (h8 : 8 < d.bi_valid.toInt) (hroom : d.pending.toNat + 2 ≤ buf.size) :
674    bi_windup (some (.tab id)) h =
675      .ok ((), setD (setB h b ((buf.set! d.pending.toNat (d.bi_buf &&& 0xff).toUInt8).set! (d.pending.toNat + 1)
676          (d.bi_buf >>> 8).toUInt8)) id
677        { d with pending := d.pending + 2, bi_used := Int32.ofInt (usedOf d.bi_valid.toInt), bi_buf := 0,
678                 bi_valid := 0 }) := by
679  have hc : d.bi_valid > 8 := by rw [i32_gt_toInt, i32_8]; exact h8
680  unfold bi_windup
681  rw [bind_app, rd_run hb.dstate]
682  simp only [hc, ite_true]
683  rw [bind_app, rd_run hb.dstate]
684  simp only []
685  rw [bind_app, put_short_run hb hroom]
686  simp only []
687  have hd' : (setD (setB h b ((buf.set! d.pending.toNat (d.bi_buf &&& 0xff).toUInt8).set! (d.pending.toNat + 1)
688          (d.bi_buf >>> 8).toUInt8)) id { d with pending := d.pending + 2 }).dstates id
689        = some { d with pending := d.pending + 2 } := by simp
690  exact (windupTail_run hd' hl hh).trans (by simp only [setD_setD])
691
692theorem bi_windup_small {h : Heap} {id : Nat} {d : DeflateState} {b : Nat} {buf : Array UInt8}
693    (hb : TreesBase h id d b buf) (hl : 0 ≤ d.bi_valid.toInt) (hh : d.bi_valid.toInt ≤ 16)
694    (h8 : d.bi_valid.toInt ≤ 8) (h0 : 0 < d.bi_valid.toInt) (hroom : d.pending.toNat + 1 ≤ buf.size) :
695    bi_windup (some (.tab id)) h =
696      .ok ((), setD (setB h b (buf.set! d.pending.toNat d.bi_buf.toUInt8)) id
697        { d with pending := d.pending + 1, bi_used := Int32.ofInt (usedOf d.bi_valid.toInt), bi_buf := 0,
698                 bi_valid := 0 }) := by
699  have hc : ¬ d.bi_valid > 8 := by rw [i32_gt_toInt, i32_8]; omega
700  have hc2 : d.bi_valid > 0 := by rw [i32_gt_toInt, i32_0]; exact h0
701  unfold bi_windup
702  rw [bind_app, rd_run hb.dstate]
703  simp only [hc, hc2, ite_true, ite_false]
704  rw [bind_app, rd_run hb.dstate]
705  simp only []
706  rw [bind_app, put_byte_run hb hroom]
707  simp only []
708  have hd' : (setD (setB h b (buf.set! d.pending.toNat d.bi_buf.toUInt8)) id { d with pending := d.pending + 1 }).dstates id
709        = some { d with pending := d.pending + 1 } := by simp
710  exact (windupTail_run hd' hl hh).trans (by simp only [setD_setD])
711
712theorem bi_windup_zero {h : Heap} {id : Nat} {d : DeflateState} (hd : h.dstates id = some d)
713    (hl : d.bi_valid.toInt = 0) :
714    bi_windup (some (.tab id)) h =
715      .ok ((), setD h id { d with bi_used := Int32.ofInt (usedOf d.bi_valid.toInt), bi_buf := 0, bi_valid := 0 }) := by
716  have hc : ¬ d.bi_valid > 8 := by rw [i32_gt_toInt, i32_8]; omega
717  have hc2 : ¬ d.bi_valid > 0 := by rw [i32_gt_toInt, i32_0]; omega
718  unfold bi_windup
719  rw [bind_app, rd_run hd]
720  simp only [hc, hc2, ite_false]
721  exact windupTail_run hd (by omega) (by omega)
722
723
724theorem natBits_pad (w bv k : Nat) (hw : w < 2 ^ bv) : natBits w (bv + k) = natBits w bv ++ List.replicate k false := by
725  rw [natBits_add, Nat.shiftRight_eq_div_pow, Nat.div_eq_of_lt hw, natBits_zero]
726
727/-- **`bi_windup`, safety and specification.** Flushes the bit buffer to a byte boundary: the output bit stream
728gets `(8 - bi_valid % 8) % 8` zero bits appended (the padding), `bi_buf = bi_valid = 0` and
729`bi_used = ((bi_valid - 1) & 7) + 1` (`usedOf`). Precondition: `TreesInvAt` and room for the pending bits
730(`8 * pending + bi_valid <= 8 * pending_buf_size`, F9). Called by `_tr_stored_block` and `_tr_flush_block`. -/
731theorem bi_windup_spec {h : Heap} {id : Nat} {d : DeflateState} {b : Nat} {buf : Array UInt8}
732    (hI : TreesInvAt h id d b buf)
733    (hroom : 8 * d.pending.toNat + d.bi_valid.toInt.toNat ≤ 8 * buf.size) :
734    ∃ buf' d', bi_windup (some (.tab id)) h = .ok ((), setD (setB h b buf') id d') ∧
735      TreesInvAt (setD (setB h b buf') id d') id d' b buf' ∧
736      outBits buf' d' = outBits buf d ++ List.replicate ((8 - d.bi_valid.toInt.toNat % 8) % 8) false ∧
737      d'.bi_valid.toInt = 0 ∧ d'.bi_buf = 0 ∧ d'.bi_used.toInt = usedOf d.bi_valid.toInt ∧
738      buf'.size = buf.size ∧
739      (∀ i, (i < d.pending.toNat ∨ d'.pending.toNat ≤ i) → buf'.getD i 0 = buf.getD i 0) ∧
740      d.pending.toNat ≤ d'.pending.toNat ∧ d'.pending.toNat ≤ d.pending.toNat + 2 ∧
741      (∃ p u, d' = { d with pending := p, bi_used := u, bi_buf := 0, bi_valid := 0 }) := by
742  obtain ⟨hb, hr⟩ := hI
743  have hbl := hr.bi_lo
744  have hbh := hr.bi_hi
745  have hbb := hr.bi_buf
746  have hp := hb.pending_small
747  have hs1 := hb.size
748  have hs2 := hb.lit_hi
749  have hp1 := toNat_add_one_u64 hp
750  have hpsz := hb.psize
751  have hu : (Int32.ofInt (usedOf d.bi_valid.toInt)).toInt = usedOf d.bi_valid.toInt := by
752    have h1 : usedOf d.bi_valid.toInt ≤ 8 := by unfold usedOf; split <;> omega
753    have h2 : 1 ≤ usedOf d.bi_valid.toInt := by unfold usedOf; split <;> omega
754    exact i32_ofInt_toInt (by omega) (by omega)
755  have hrun : ∀ (d' : DeflateState), d'.l_desc = d.l_desc → d'.d_desc = d.d_desc → d'.bl_desc = d.bl_desc →
756      d'.bi_valid = 0 → d'.bi_buf = 0 → d'.sym_next = d.sym_next → d'.sym_end = d.sym_end → TreesRun id d' := by
757    intro d' h1 h2 h3 h4 h5 h7 h8
758    refine hr.with_bi d' h1 h2 h3 ?_ ?_ ?_ h7 h8
759    · rw [h4, i32_0]; omega
760    · rw [h4, i32_0]; omega
761    · rw [h4, h5, i32_0]; simp
762  by_cases h8 : 8 < d.bi_valid.toInt
763  · have hroom2 : d.pending.toNat + 2 ≤ buf.size := by
764      have : 8 < d.bi_valid.toInt.toNat := by omega
765      omega
766    have hp2 := toNat_add_two_u64 hp
767    have hbuf2 : ((buf.set! d.pending.toNat (d.bi_buf &&& 0xff).toUInt8).set! (d.pending.toNat + 1)
768        (d.bi_buf >>> 8).toUInt8).size = buf.size := by simp
769    refine ⟨_, _, bi_windup_big hb hbl hbh h8 hroom2, ?_, ?_, ?_, ?_, ?_, hbuf2, ?_, ?_, ?_, ⟨_, _, rfl⟩⟩
770    · exact ⟨hb.step _ hbuf2 _ hb.wf rfl rfl rfl rfl rfl (by simp only []; rw [hp2]; omega), hrun _ rfl rfl rfl rfl rfl rfl rfl⟩
771    · unfold outBits
772      show bytesBits _ (d.pending + 2).toNat ++ natBits (0 : UInt16).toNat (0 : Int32).toInt.toNat = _
773      rw [hp2, bytesBits_two _ _ (by omega), i32_0, List.append_assoc (bytesBits _ _), natBits_word]
774      have e : (16 : Nat) = d.bi_valid.toInt.toNat + (16 - d.bi_valid.toInt.toNat) := by omega
775      rw [e, natBits_pad _ _ _ hbb]
776      have e2 : 16 - d.bi_valid.toInt.toNat = (8 - d.bi_valid.toInt.toNat % 8) % 8 := by omega
777      rw [e2]; simp [natBits]
778    · exact i32_0
779    · rfl
780    · show Int32.toInt (Int32.ofInt _) = _; exact hu
781    · intro i hi
782      have h1 : ¬ (d.pending.toNat + 1 = i) := by simp only [] at hi; rw [hp2] at hi; omega
783      have h2 : ¬ (d.pending.toNat = i) := by simp only [] at hi; rw [hp2] at hi; omega
784      rw [getD_set_u8, getD_set_u8]
785      simp [h1, h2]
786    · show d.pending.toNat ≤ (d.pending + 2).toNat; rw [hp2]; omega
787    · show (d.pending + 2).toNat ≤ _; rw [hp2]; omega
788  · by_cases h0 : 0 < d.bi_valid.toInt
789    · have hroom1 : d.pending.toNat + 1 ≤ buf.size := by
790        have : 0 < d.bi_valid.toInt.toNat := by omega
791        omega
792      have hbuf1 : (buf.set! d.pending.toNat d.bi_buf.toUInt8).size = buf.size := by simp
793      refine ⟨_, _, bi_windup_small hb hbl hbh (by omega) h0 hroom1, ?_, ?_, ?_, ?_, ?_, hbuf1, ?_, ?_, ?_, ⟨_, _, rfl⟩⟩
794      · exact ⟨hb.step _ hbuf1 _ hb.wf rfl rfl rfl rfl rfl (by simp only []; rw [hp1]; omega), hrun _ rfl rfl rfl rfl rfl rfl rfl⟩
795      · unfold outBits
796        show bytesBits _ (d.pending + 1).toNat ++ natBits (0 : UInt16).toNat (0 : Int32).toInt.toNat = _
797        rw [hp1, bytesBits_one _ (by omega), i32_0, natBits_byte]
798        have hpad := natBits_pad d.bi_buf.toNat d.bi_valid.toInt.toNat (8 - d.bi_valid.toInt.toNat) hbb
799        rw [show d.bi_valid.toInt.toNat + (8 - d.bi_valid.toInt.toNat) = 8 by omega] at hpad
800        have e2 : 8 - d.bi_valid.toInt.toNat = (8 - d.bi_valid.toInt.toNat % 8) % 8 := by omega
801        rw [hpad, e2]; simp [natBits]
802      · exact i32_0
803      · rfl
804      · show Int32.toInt (Int32.ofInt _) = _; exact hu
805      · intro i hi
806        have h2 : ¬ (d.pending.toNat = i) := by simp only [] at hi; rw [hp1] at hi; omega
807        rw [getD_set_u8]
808        simp [h2]
809      · show d.pending.toNat ≤ (d.pending + 1).toNat; rw [hp1]; omega
810      · show (d.pending + 1).toNat ≤ _; rw [hp1]; omega
811    · have hz : d.bi_valid.toInt = 0 := by omega
812      refine ⟨buf, { d with bi_used := Int32.ofInt (usedOf d.bi_valid.toInt), bi_buf := 0, bi_valid := 0 }, ?_, ?_, ?_, i32_0, rfl, ?_, rfl, fun _ _ => rfl, Nat.le_refl _, (by show d.pending.toNat ≤ d.pending.toNat + 2; omega), ⟨_, _, rfl⟩⟩
813      · rw [setB_self hb.bytes]; exact bi_windup_zero hb.dstate hz
814      · rw [setB_self hb.bytes]
815        exact ⟨hb.stepD _ hb.wf rfl rfl rfl rfl rfl hb.pending_le, hrun _ rfl rfl rfl rfl rfl rfl rfl⟩
816      · unfold outBits
817        show bytesBits buf d.pending.toNat ++ natBits (0 : UInt16).toNat (0 : Int32).toInt.toNat = _
818        rw [i32_0, hz]; simp [natBits]
819      · show Int32.toInt (Int32.ofInt _) = _; exact hu
820
821end Zlib.Trees.Proofs.Out