trees.c.tally.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.align»
2
3/-!
4# trees.c: `_tr_tally`
5-/
6
7namespace Zlib.Trees.Proofs.Out
8open C Zlib.Trees
9
10/-- One `s->sym_buf[s->sym_next++] = v` of `_tr_tally`. -/
11theorem sym_put_run {h : Heap} {id : Nat} {d : DeflateState} {b : Nat} {buf : Array UInt8}
12    (hb : TreesBase h id d b buf) (hlt : d.lit_bufsize.toNat + d.sym_next.toNat < buf.size) (v : UInt8)
13    (hsn : d.sym_next.toNat < 2 ^ 31) :
14    (do let d ← rd (some (.tab id))
15        setAt d.sym_buf d.sym_next.toNat v
16        md (some (.tab id)) fun d => { d with sym_next := d.sym_next + 1 } : M Unit) h =
17      .ok ((), setD (setB h b (buf.set! (d.lit_bufsize.toNat + d.sym_next.toNat) v)) id
18        { d with sym_next := d.sym_next + 1 }) := by
19  have hg : Space.get h (BRef.blk b) = some buf := hb.bytes
20  have e1 := Ptr.add_nat_ok (off := d.lit_bufsize.toNat) (n := d.sym_next.toNat) hg (by omega)
21  have e2 := Ptr.store_ok (v := v) (off := d.lit_bufsize.toNat + d.sym_next.toNat) hg hb.rw hlt
22  unfold OkOn at e1
23  unfold setAt
24  rw [bind_app, rd_run hb.dstate]
25  simp only [hb.sym]
26  rw [bind_app, bind_app, e1]
27  simp only []
28  rw [e2]
29  simp only []
30  have hd : (Space.put h (BRef.blk b) (buf.set! (d.lit_bufsize.toNat + d.sym_next.toNat) v)).dstates id = some d :=
31    hb.dstate
32  rw [md_run hd]
33  simp [setD, Space.put, setB]
34  rw [hb.sym]
35
36
37theorem length_code_le (i : Nat) (hi : i < 256) : (length_code_tab[i]'(by rw [length_code_tab_size]; exact hi)).toNat ≤ 28 := by
38  have : ∀ j : Fin 256, (length_code_tab[j.val]'(by rw [length_code_tab_size]; exact j.isLt)).toNat ≤ 28 := by
39    decide +kernel
40  exact this ⟨i, hi⟩
41
42theorem dist_code_le (i : Nat) (hi : i < 512) : (dist_code_tab[i]'(by rw [dist_code_tab_size]; exact hi)).toNat ≤ 29 := by
43  have : ∀ j : Fin 512, (dist_code_tab[j.val]'(by rw [dist_code_tab_size]; exact j.isLt)).toNat ≤ 29 := by
44    decide +kernel
45  exact this ⟨i, hi⟩
46
47theorem arr_get_bang (a : Array UInt8) (i : Nat) (hi : i < a.size) : a[i]! = a[i] := getElem!_pos a i hi
48
49/-- `d_code(dist)` as a number (`dist` here is `dist - 1` of the symbol). -/
50def dcodeN (d : Nat) : Nat := if d < 256 then (dist_code_tab[d]!).toNat else (dist_code_tab[256 + d / 128]!).toNat
51
52/-- `d_code` reads `_dist_code` inside its bounds for `dist < 32768`; the code is at most 29. -/
53theorem d_code_run {h : Heap} (hs : TreesStatic h.static) (dist : UInt32) (hd : dist.toNat < 32768) :
54    ∃ c : UInt8, d_code dist h = .ok (c, h) ∧ c.toNat = dcodeN dist.toNat ∧ c.toNat ≤ 29 := by
55  have hg : Space.get h BRef.st_dist_code = some dist_code_tab := by simp [Space.get, hs.dist_code]
56  unfold d_code
57  by_cases h1 : dist < 256
58  · have h2 : dist.toNat < 256 := by simpa [UInt32.lt_iff_toNat_lt] using h1
59    have hi : dist.toNat < dist_code_tab.size := by rw [dist_code_tab_size]; omega
60    have e := Ptr.index_ok (off := 0) (i := dist.toNat) hg (by omega)
61    unfold OkOn at e
62    simp only [h1, ite_true]
63    refine ⟨_, e, ?_, ?_⟩
64    · have := arr_get_bang dist_code_tab dist.toNat hi
65      simp only [dcodeN, h2, ite_true, Nat.zero_add]
66      exact congrArg UInt8.toNat this.symm
67    · exact dist_code_le _ (by omega)
68  · have h2 : ¬ dist.toNat < 256 := by simpa [UInt32.lt_iff_toNat_lt] using h1
69    have hsh : (dist >>> 7).toNat = dist.toNat / 128 := by
70      rw [UInt32.toNat_shiftRight]; simp [Nat.shiftRight_eq_div_pow]
71    have hidx : ((256 : UInt32) + (dist >>> 7)).toNat = 256 + dist.toNat / 128 := by
72      rw [UInt32.toNat_add, hsh]; simp; omega
73    have hi : 256 + dist.toNat / 128 < dist_code_tab.size := by rw [dist_code_tab_size]; omega
74    have e := Ptr.index_ok (off := 0) (i := 256 + dist.toNat / 128) hg (by omega)
75    unfold OkOn at e
76    simp only [h1, ite_false]
77    refine ⟨_, by rw [hidx, e], ?_, ?_⟩
78    · have := arr_get_bang dist_code_tab (256 + dist.toNat / 128) hi
79      simp only [dcodeN, h2, ite_false, Nat.zero_add]
80      exact congrArg UInt8.toNat this.symm
81    · exact dist_code_le _ (by omega)
82
83
84theorem toNat_add_one_u32 {x : UInt32} (hx : x.toNat + 1 < 2 ^ 32) : (x + 1).toNat = x.toNat + 1 := by
85  rw [UInt32.toNat_add]; have : (1 : UInt32).toNat = 1 := by decide
86  rw [this]; omega
87
88/-- The three stores of `_tr_tally` into the symbol buffer. -/
89theorem tally_puts {h : Heap} {id : Nat} {d : DeflateState} {b : Nat} {buf : Array UInt8}
90    (hb : TreesBase h id d b buf) (hroom : d.sym_next.toNat + 3 ≤ d.sym_end.toNat) (dist lc : UInt32)
91    (rest : Unit → M Int32) :
92    ((do
93          let d ← rd (some (DeflateStateRef.tab id))
94          setAt d.sym_buf (↑d.sym_next.toNat) dist.toUInt8
95          md (some (DeflateStateRef.tab id)) fun d => { d with sym_next := d.sym_next + 1 } : M Unit) >>= fun _ =>
96      ((do
97          let d ← rd (some (DeflateStateRef.tab id))
98          setAt d.sym_buf (↑d.sym_next.toNat) (dist >>> 8).toUInt8
99          md (some (DeflateStateRef.tab id)) fun d => { d with sym_next := d.sym_next + 1 } : M Unit) >>= fun _ =>
100      ((do
101          let d ← rd (some (DeflateStateRef.tab id))
102          setAt d.sym_buf (↑d.sym_next.toNat) lc.toUInt8
103          md (some (DeflateStateRef.tab id)) fun d => { d with sym_next := d.sym_next + 1 } : M Unit) >>= rest))) h =
104    rest () (setD (setB h b (((buf.set! (d.lit_bufsize.toNat + d.sym_next.toNat) dist.toUInt8).set!
105        (d.lit_bufsize.toNat + (d.sym_next.toNat + 1)) (dist >>> 8).toUInt8).set!
106        (d.lit_bufsize.toNat + (d.sym_next.toNat + 2)) lc.toUInt8)) id { d with sym_next := d.sym_next + 1 + 1 + 1 }) := by
107  have hl := hb.lit_hi
108  have hse := hb.sym_end
109  have hs1 := hb.size
110  have hsn1 : (d.sym_next + 1).toNat = d.sym_next.toNat + 1 := toNat_add_one_u32 (by omega)
111  have hb1 := hb.step (buf.set! (d.lit_bufsize.toNat + d.sym_next.toNat) dist.toUInt8) (by simp)
112    { d with sym_next := d.sym_next + 1 } hb.wf rfl rfl rfl rfl rfl hb.pending_le
113  have hsn2 : (d.sym_next + 1 + 1).toNat = d.sym_next.toNat + 2 := by rw [toNat_add_one_u32 (by omega), hsn1]
114  have hb2 : TreesBase (setD (setB h b ((buf.set! (d.lit_bufsize.toNat + d.sym_next.toNat) dist.toUInt8).set!
115      (d.lit_bufsize.toNat + (d.sym_next.toNat + 1)) (dist >>> 8).toUInt8)) id { d with sym_next := d.sym_next + 1 + 1 })
116      id { d with sym_next := d.sym_next + 1 + 1 } b ((buf.set! (d.lit_bufsize.toNat + d.sym_next.toNat) dist.toUInt8).set!
117      (d.lit_bufsize.toNat + (d.sym_next.toNat + 1)) (dist >>> 8).toUInt8) := by
118    simpa only [setB_setD, setD_setD, setB_setB] using hb1.step ((buf.set! (d.lit_bufsize.toNat + d.sym_next.toNat) dist.toUInt8).set!
119      (d.lit_bufsize.toNat + (d.sym_next.toNat + 1)) (dist >>> 8).toUInt8) (by simp)
120      { d with sym_next := d.sym_next + 1 + 1 } hb.wf rfl rfl rfl rfl rfl hb.pending_le
121  rw [bind_app, sym_put_run hb (by omega) _ (by omega)]
122  simp only []
123  rw [bind_app, sym_put_run hb1 (by simp only [Array.size_set!]; rw [hsn1]; omega) _ (by simp only []; rw [hsn1]; omega)]
124  simp only [hsn1, Nat.add_assoc, setB_setD, setD_setD, setB_setB]
125  rw [bind_app, sym_put_run hb2 (by simp only [Array.size_set!]; rw [hsn2]; omega) _ (by simp only []; rw [hsn2]; omega)]
126  simp only [hsn2, Nat.add_assoc, setB_setD, setD_setD, setB_setB]
127
128
129/-- The array with `Freq` of entry `i` incremented (`tree[i].Freq++`, modulo 2^16). -/
130def bumpFc (a : Array CtData) (i : Nat) : Array CtData := a.set! i { (a[i]!) with fc := (a[i]!).fc + 1 }
131
132/-- The part of `_tr_tally` after the three stores into the symbol buffer. -/
133def tallyTail (s : DeflateStatePtr) (dist lc : UInt32) : M Int32 := do
134  if dist == 0 then
135    let lt ← pLtree s
136    setFc lt lc.toNat ((← getFc lt lc.toNat) + 1)
137  else
138    md s fun d => { d with «matches» := d.«matches» + 1 }
139    let dist := dist - 1
140    let lcode ← Ptr.index (.ref .st_length_code 0 : BPtr) lc.toNat
141    let idx := (u8i lcode).toInt + LITERALS.toInt + 1
142    let lt ← pLtree s
143    setFc lt idx ((← getFc lt idx) + 1)
144    let dc ← d_code dist
145    let dt ← pDtree s
146    setFc dt dc.toNat ((← getFc dt dc.toNat) + 1)
147  let d ← rd s
148  return (if d.sym_next == d.sym_end then 1 else 0)
149
150theorem tally_split (s : DeflateStatePtr) (dist lc : UInt32) :
151    «_tr_tally» s dist lc = ((do
152          let d ← rd s
153          setAt d.sym_buf (↑d.sym_next.toNat) dist.toUInt8
154          md s fun d => { d with sym_next := d.sym_next + 1 } : M Unit) >>= fun _ =>
155      ((do
156          let d ← rd s
157          setAt d.sym_buf (↑d.sym_next.toNat) (dist >>> 8).toUInt8
158          md s fun d => { d with sym_next := d.sym_next + 1 } : M Unit) >>= fun _ =>
159      ((do
160          let d ← rd s
161          setAt d.sym_buf (↑d.sym_next.toNat) lc.toUInt8
162          md s fun d => { d with sym_next := d.sym_next + 1 } : M Unit) >>= fun _ => tallyTail s dist lc))) := rfl
163
164theorem tallyTail_lit {H : Heap} {id : Nat} {D : DeflateState} (hd : H.dstates id = some D) (dist lc : UInt32)
165    (hdist : dist = 0) (hlc : lc.toNat < D.dyn_ltree.size) :
166    tallyTail (some (.tab id)) dist lc H =
167      .ok ((if D.sym_next == D.sym_end then 1 else 0),
168        setD H id { D with dyn_ltree := bumpFc D.dyn_ltree lc.toNat }) := by
169  subst hdist
170  have hg : getFc (.ref (Sel.l.ref id) 0) ((lc.toNat : Nat) : Int) H = .ok ((D.dyn_ltree[lc.toNat]!).fc, H) :=
171    getFc_sel hd .l hlc
172  have hs := setFc_sel hd .l (i := lc.toNat) hlc ((D.dyn_ltree[lc.toNat]!).fc + 1)
173  unfold tallyTail
174  simp only [beq_self_eq_true, ite_true]
175  rw [bind_app, pLtree_run hd]
176  simp only []
177  rw [bind_app]
178  have hg' : getFc (.ref (CtDataRef.dstate_dyn_ltree id) 0) ((lc.toNat : Nat) : Int) H = _ := hg
179  rw [hg']
180  simp only []
181  have hs' : setFc (.ref (CtDataRef.dstate_dyn_ltree id) 0) ((lc.toNat : Nat) : Int) ((D.dyn_ltree[lc.toNat]!).fc + 1) H = _ := hs
182  rw [bind_app, hs']
183  simp only []
184  simp (disch := simp [hd]) only [bind_app, rd_run', rdD_setD_same, pure_app]
185  simp only [Sel.upd, Sel.arr, bumpFc]
186  rfl
187
188
189theorem LITERALS_toInt : LITERALS.toInt = 256 := by decide
190
191theorem u8i_toInt (x : UInt8) : (u8i x).toInt = x.toNat := by
192  unfold u8i
193  have := x.toNat_lt
194  exact i32_ofInt_toInt (by omega) (by omega)
195
196/-- The record after the counting part of a match symbol. -/
197def tallyMatchRec (D : DeflateState) (dist lc : UInt32) : DeflateState :=
198  { D with «matches» := D.«matches» + 1, dyn_ltree := bumpFc D.dyn_ltree ((length_code_tab[lc.toNat]!).toNat + 257), dyn_dtree := bumpFc D.dyn_dtree (dcodeN (dist.toNat - 1)) }
199
200theorem idx_cast (x : UInt8) : (u8i x).toInt + LITERALS.toInt + 1 = (((x.toNat + 257 : Nat)) : Int) := by
201  rw [u8i_toInt, LITERALS_toInt]; omega
202
203theorem tallyTail_match {H : Heap} {id : Nat} {D : DeflateState} (hd : H.dstates id = some D)
204    (hs : TreesStatic H.static) (hwf : D.WellFormed) (dist lc : UInt32)
205    (hdist : (dist == 0) = false) (hlc : lc.toNat < 256) (hd32 : dist.toNat ≤ 32768) :
206    tallyTail (some (.tab id)) dist lc H =
207      .ok ((if D.sym_next == D.sym_end then 1 else 0), setD H id (tallyMatchRec D dist lc)) := by
208  obtain ⟨w1, w2, w3, w4, w5, w6⟩ := hwf
209  have hd0 : dist ≠ 0 := by
210    intro h0; subst h0; simp at hdist
211  have hd1 : (dist - 1).toNat = dist.toNat - 1 := by
212    have : 1 ≤ dist.toNat := by
213      rcases Nat.eq_zero_or_pos dist.toNat with h0 | h0
214      · exact absurd (UInt32.toNat_inj.mp (by simpa using h0)) hd0
215      · exact h0
216    rw [UInt32.toNat_sub_of_le _ _ (by simp [UInt32.le_iff_toNat_le]; omega)]
217    simp
218  have hsL : (setD H id { D with «matches» := D.«matches» + 1 }).dstates id = some { D with «matches» := D.«matches» + 1 } :=
219    setD_dstates_same _ _ _
220  have hsS : TreesStatic (setD H id { D with «matches» := D.«matches» + 1 }).static := by simpa using hs
221  have hlg : Space.get (setD H id { D with «matches» := D.«matches» + 1 }) BRef.st_length_code = some length_code_tab := by
222    simp [Space.get, hs.length_code]
223  have hil : lc.toNat < length_code_tab.size := by rw [length_code_tab_size]; omega
224  have eL := Ptr.index_ok (off := 0) (i := lc.toNat) hlg (by omega)
225  unfold OkOn at eL
226  have eL' : Ptr.index (.ref .st_length_code 0 : BPtr) (lc.toNat : Int) (setD H id { D with «matches» := D.«matches» + 1 })
227      = .ok (length_code_tab[lc.toNat]!, setD H id { D with «matches» := D.«matches» + 1 }) := by
228    rw [eL]; simp only [Nat.zero_add]; rw [arr_get_bang length_code_tab lc.toNat hil]
229  have hlc28 : (length_code_tab[lc.toNat]!).toNat ≤ 28 := by
230    rw [arr_get_bang length_code_tab lc.toNat hil]; exact length_code_le _ hlc
231  unfold tallyTail
232  simp only [hdist, Bool.false_eq_true, ite_false]
233  rw [bind_app, md_run hd]
234  simp only []
235  rw [bind_app, eL']
236  simp only []
237  have hD1w : ({ D with «matches» := D.«matches» + 1 } : DeflateState).dyn_ltree.size = 573 := w1
238  have hD1w2 : ({ D with «matches» := D.«matches» + 1 } : DeflateState).dyn_dtree.size = 61 := w2
239  generalize hD1 : ({ D with «matches» := D.«matches» + 1 } : DeflateState) = D1 at *
240  rw [bind_app, pLtree_run hsL]
241  simp only [idx_cast]
242  have hi1 : (length_code_tab[lc.toNat]!).toNat + 257 < (Sel.l.arr D1).size := by
243    show _ < D1.dyn_ltree.size; omega
244  rw [bind_app]
245  have g1 : getFc (.ref (CtDataRef.dstate_dyn_ltree id) 0) ((((length_code_tab[lc.toNat]!).toNat + 257 : Nat)) : Int)
246      (setD H id D1) = _ := getFc_sel hsL .l hi1
247  rw [g1]
248  simp only []
249  have s1 : setFc (.ref (CtDataRef.dstate_dyn_ltree id) 0) ((((length_code_tab[lc.toNat]!).toNat + 257 : Nat)) : Int)
250      ((Sel.l.arr D1)[(length_code_tab[lc.toNat]!).toNat + 257]!.fc + 1) (setD H id D1) = _ :=
251    setFc_sel hsL .l hi1 _
252  rw [bind_app, s1]
253  simp only [setD_setD]
254  have hsz2 : (Sel.l.upd D1 ((Sel.l.arr D1).set! ((length_code_tab[lc.toNat]!).toNat + 257)
255      { (Sel.l.arr D1)[(length_code_tab[lc.toNat]!).toNat + 257]! with fc := (Sel.l.arr D1)[(length_code_tab[lc.toNat]!).toNat + 257]!.fc + 1 })).dyn_dtree.size = 61 := hD1w2
256  generalize hD2 : Sel.l.upd D1 ((Sel.l.arr D1).set! ((length_code_tab[lc.toNat]!).toNat + 257)
257      { (Sel.l.arr D1)[(length_code_tab[lc.toNat]!).toNat + 257]! with fc := (Sel.l.arr D1)[(length_code_tab[lc.toNat]!).toNat + 257]!.fc + 1 }) = D2 at *
258  have hsD : (setD H id D2).dstates id = some D2 := setD_dstates_same _ _ _
259  obtain ⟨c, hcr, hcn, hc29⟩ := d_code_run (h := setD H id D2) (by simpa using hs) (dist - 1) (by omega)
260  rw [bind_app, hcr]
261  simp only []
262  rw [bind_app, pDtree_run hsD]
263  simp only []
264  have hi2 : c.toNat < (Sel.d.arr D2).size := by show _ < D2.dyn_dtree.size; omega
265  have g2 : getFc (.ref (CtDataRef.dstate_dyn_dtree id) 0) ((c.toNat : Nat) : Int) (setD H id D2) = _ := getFc_sel hsD .d hi2
266  rw [bind_app, g2]
267  simp only []
268  have s2 : setFc (.ref (CtDataRef.dstate_dyn_dtree id) 0) ((c.toNat : Nat) : Int)
269      ((Sel.d.arr D2)[c.toNat]!.fc + 1) (setD H id D2) = _ := setFc_sel hsD .d hi2 _
270  rw [bind_app, s2]
271  simp only [setD_setD]
272  simp (disch := simp) only [bind_app, rd_run', rdD_setD_same, pure_app]
273  rw [hcn, hd1]
274  subst hD2
275  subst hD1
276  unfold tallyMatchRec bumpFc
277  simp only [Sel.upd, Sel.arr]
278  rfl
279
280
281@[simp] theorem bumpFc_size (a : Array CtData) (i : Nat) : (bumpFc a i).size = a.size := by
282  simp [bumpFc]
283
284/-- The record after `_tr_tally`. -/
285def tallyRec (d : DeflateState) (dist lc : UInt32) : DeflateState :=
286  if dist = 0 then { d with sym_next := d.sym_next + 1 + 1 + 1, dyn_ltree := bumpFc d.dyn_ltree lc.toNat }
287  else tallyMatchRec { d with sym_next := d.sym_next + 1 + 1 + 1 } dist lc
288
289theorem tallyRec_wf {d : DeflateState} (hw : d.WellFormed) (dist lc : UInt32) : (tallyRec d dist lc).WellFormed := by
290  obtain ⟨w1, w2, w3, w4, w5, w6⟩ := hw
291  unfold tallyRec tallyMatchRec
292  split <;> exact ⟨by simpa using w1, by simpa using w2, w3, w4, w5, w6⟩
293
294theorem tallyRec_fields (d : DeflateState) (dist lc : UInt32) :
295    (tallyRec d dist lc).pending_buf = d.pending_buf ∧ (tallyRec d dist lc).pending_buf_size = d.pending_buf_size ∧
296    (tallyRec d dist lc).sym_buf = d.sym_buf ∧ (tallyRec d dist lc).lit_bufsize = d.lit_bufsize ∧
297    (tallyRec d dist lc).sym_end = d.sym_end ∧ (tallyRec d dist lc).pending = d.pending := by
298  unfold tallyRec tallyMatchRec
299  split <;> exact ⟨rfl, rfl, rfl, rfl, rfl, rfl⟩
300
301theorem tallyRec_run {id : Nat} {d : DeflateState} (hr : TreesRun id d) (hroom : d.sym_next.toNat + 3 ≤ d.sym_end.toNat)
302    (hm : d.sym_next.toNat % 3 = 0) (hsn : d.sym_next.toNat + 3 < 2 ^ 32) (dist lc : UInt32) :
303    TreesRun id (tallyRec d dist lc) := by
304  have e : (d.sym_next + 1 + 1 + 1).toNat = d.sym_next.toNat + 3 := by
305    have e1 : (d.sym_next + 1).toNat = d.sym_next.toNat + 1 := toNat_add_one_u32 (by omega)
306    have e2 : (d.sym_next + 1 + 1).toNat = d.sym_next.toNat + 2 := by
307      rw [toNat_add_one_u32 (by rw [e1]; omega), e1]
308    rw [toNat_add_one_u32 (by rw [e2]; omega), e2]
309  unfold tallyRec tallyMatchRec
310  split
311  · exact ⟨hr.ldyn, hr.lstat, hr.ddyn, hr.dstat, hr.bldyn, hr.blstat, hr.bi_lo, hr.bi_hi, hr.bi_buf,
312      by show (d.sym_next + 1 + 1 + 1).toNat ≤ d.sym_end.toNat; omega,
313      by show (d.sym_next + 1 + 1 + 1).toNat % 3 = 0; omega⟩
314  · exact ⟨hr.ldyn, hr.lstat, hr.ddyn, hr.dstat, hr.bldyn, hr.blstat, hr.bi_lo, hr.bi_hi, hr.bi_buf,
315      by show (d.sym_next + 1 + 1 + 1).toNat ≤ d.sym_end.toNat; omega,
316      by show (d.sym_next + 1 + 1 + 1).toNat % 3 = 0; omega⟩
317
318
319/-- **`_tr_tally`, safety and specification.** `_tr_tally(s, dist, lc)` stores the symbol `(dist, lc)` as 3 bytes at
320`sym_buf[sym_next ..]` (`dist` little-endian, then `lc`), counts it in `dyn_ltree` (a literal: `dyn_ltree[lc].Freq++`;
321a match: `matches++`, `dyn_ltree[_length_code[lc] + 257].Freq++`, `dyn_dtree[d_code(dist - 1)].Freq++`) and returns
322whether the symbol buffer is now full (`sym_next == sym_end`), which is when `deflate.c` flushes the block.
323Preconditions: `TreesInvAt`; `sym_next + 3 <= sym_end` (deflate.c flushes the block as soon as `sym_next == sym_end`,
324so a tally always starts below it); a literal has `lc < 256` (`lc` is a byte); a match has `lc < 256` (length minus
325`MIN_MATCH`, at most 255) and `1 <= dist <= 32768` (`MAX_DIST` is at most 32506). Nothing else of the record changes;
326the byte block changes only at the three symbol bytes. -/
327theorem tr_tally_spec {h : Heap} {id : Nat} {d : DeflateState} {b : Nat} {buf : Array UInt8}
328    (hI : TreesInvAt h id d b buf) (dist lc : UInt32)
329    (hroom : d.sym_next.toNat + 3 ≤ d.sym_end.toNat)
330    (hlit : dist = 0 → lc.toNat < 256) (hmatch : dist ≠ 0 → lc.toNat < 256 ∧ dist.toNat ≤ 32768) :
331    ∃ buf' r, «_tr_tally» (some (.tab id)) dist lc h = .ok (r, setD (setB h b buf') id (tallyRec d dist lc)) ∧
332      TreesInvAt (setD (setB h b buf') id (tallyRec d dist lc)) id (tallyRec d dist lc) b buf' ∧
333      r = (if d.sym_next + 1 + 1 + 1 == d.sym_end then 1 else 0) ∧
334      buf'.size = buf.size ∧
335      buf'.getD (d.lit_bufsize.toNat + d.sym_next.toNat) 0 = dist.toUInt8 ∧
336      buf'.getD (d.lit_bufsize.toNat + d.sym_next.toNat + 1) 0 = (dist >>> 8).toUInt8 ∧
337      buf'.getD (d.lit_bufsize.toNat + d.sym_next.toNat + 2) 0 = lc.toUInt8 ∧
338      (∀ i, (i < d.lit_bufsize.toNat + d.sym_next.toNat ∨ d.lit_bufsize.toNat + d.sym_next.toNat + 3 ≤ i) →
339        buf'.getD i 0 = buf.getD i 0) := by
340  obtain ⟨hb, hr⟩ := hI
341  have hl := hb.lit_hi
342  have hse := hb.sym_end
343  have hs1 := hb.size
344  have hm := hr.sym_next_mod
345  have hsn : d.sym_next.toNat + 3 < 2 ^ 32 := by omega
346  have e1 : (d.sym_next + 1).toNat = d.sym_next.toNat + 1 := toNat_add_one_u32 (by omega)
347  have e2 : (d.sym_next + 1 + 1).toNat = d.sym_next.toNat + 2 := by
348    rw [toNat_add_one_u32 (by rw [e1]; omega), e1]
349  have e3 : (d.sym_next + 1 + 1 + 1).toNat = d.sym_next.toNat + 3 := by
350    rw [toNat_add_one_u32 (by rw [e2]; omega), e2]
351  set_option maxRecDepth 4000 in
352  have hbuf3 : ((((buf.set! (d.lit_bufsize.toNat + d.sym_next.toNat) dist.toUInt8).set!
353        (d.lit_bufsize.toNat + (d.sym_next.toNat + 1)) (dist >>> 8).toUInt8).set!
354        (d.lit_bufsize.toNat + (d.sym_next.toNat + 2)) lc.toUInt8)).size = buf.size := by simp
355  have hb3 : TreesBase (setD (setB h b ((((buf.set! (d.lit_bufsize.toNat + d.sym_next.toNat) dist.toUInt8).set!
356        (d.lit_bufsize.toNat + (d.sym_next.toNat + 1)) (dist >>> 8).toUInt8).set!
357        (d.lit_bufsize.toNat + (d.sym_next.toNat + 2)) lc.toUInt8))) id { d with sym_next := d.sym_next + 1 + 1 + 1 })
358      id { d with sym_next := d.sym_next + 1 + 1 + 1 } b ((((buf.set! (d.lit_bufsize.toNat + d.sym_next.toNat) dist.toUInt8).set!
359        (d.lit_bufsize.toNat + (d.sym_next.toNat + 1)) (dist >>> 8).toUInt8).set!
360        (d.lit_bufsize.toNat + (d.sym_next.toNat + 2)) lc.toUInt8)) :=
361    hb.step _ hbuf3 _ hb.wf rfl rfl rfl rfl rfl hb.pending_le
362  have hd3 := setD_dstates_same (setB h b ((((buf.set! (d.lit_bufsize.toNat + d.sym_next.toNat) dist.toUInt8).set!
363        (d.lit_bufsize.toNat + (d.sym_next.toNat + 1)) (dist >>> 8).toUInt8).set!
364        (d.lit_bufsize.toNat + (d.sym_next.toNat + 2)) lc.toUInt8))) id { d with sym_next := d.sym_next + 1 + 1 + 1 }
365  have hrun : «_tr_tally» (some (.tab id)) dist lc h =
366      .ok ((if d.sym_next + 1 + 1 + 1 == d.sym_end then 1 else 0),
367        setD (setB h b ((((buf.set! (d.lit_bufsize.toNat + d.sym_next.toNat) dist.toUInt8).set!
368        (d.lit_bufsize.toNat + (d.sym_next.toNat + 1)) (dist >>> 8).toUInt8).set!
369        (d.lit_bufsize.toNat + (d.sym_next.toNat + 2)) lc.toUInt8))) id (tallyRec d dist lc)) := by
370    rw [tally_split, tally_puts hb hroom dist lc (fun _ => tallyTail (some (.tab id)) dist lc)]
371    by_cases hz : dist = 0
372    · have hlc := hlit hz
373      have hlt : lc.toNat < ({ d with sym_next := d.sym_next + 1 + 1 + 1 } : DeflateState).dyn_ltree.size := by
374        show lc.toNat < d.dyn_ltree.size
375        have := hb.wf.1; omega
376      rw [tallyTail_lit hd3 dist lc hz hlt]
377      simp only [tallyRec, hz, ite_true, setD_setD]
378    · obtain ⟨hlc, hdd⟩ := hmatch hz
379      have hdz : (dist == 0) = false := by simpa using hz
380      rw [tallyTail_match hd3 (by simpa using hb.static) hb.wf dist lc hdz hlc hdd]
381      simp only [tallyRec, hz, ite_false, setD_setD]
382  refine ⟨_, _, hrun, ?_, rfl, hbuf3, ?_, ?_, ?_, ?_⟩
383  · obtain ⟨f1, f2, f3, f4, f5, f6⟩ := tallyRec_fields d dist lc
384    exact ⟨hb.step _ hbuf3 _ (tallyRec_wf hb.wf dist lc) f1 f2 f3 f4 f5 (by rw [f6, f2]; exact hb.pending_le),
385      tallyRec_run hr hroom hm hsn dist lc⟩
386  · rw [getD_set_u8, getD_set_u8, getD_set_u8]
387    have n1 : ¬ (d.lit_bufsize.toNat + (d.sym_next.toNat + 2) = d.lit_bufsize.toNat + d.sym_next.toNat) := by omega
388    have n2 : ¬ (d.lit_bufsize.toNat + (d.sym_next.toNat + 1) = d.lit_bufsize.toNat + d.sym_next.toNat) := by omega
389    have n3 : d.lit_bufsize.toNat + d.sym_next.toNat < buf.size := by omega
390    simp [n1, n2, n3]
391  · rw [getD_set_u8, getD_set_u8, getD_set_u8]
392    have n1 : ¬ (d.lit_bufsize.toNat + (d.sym_next.toNat + 2) = d.lit_bufsize.toNat + d.sym_next.toNat + 1) := by omega
393    have n3 : d.lit_bufsize.toNat + (d.sym_next.toNat + 1) < buf.size := by omega
394    simp [n1, n3, Nat.add_assoc]
395  · rw [getD_set_u8, getD_set_u8, getD_set_u8]
396    have n3 : d.lit_bufsize.toNat + (d.sym_next.toNat + 2) < buf.size := by omega
397    simp [n3, Nat.add_assoc]
398  · intro i hi
399    have n1 : ¬ (d.lit_bufsize.toNat + (d.sym_next.toNat + 2) = i) := by omega
400    have n2 : ¬ (d.lit_bufsize.toNat + (d.sym_next.toNat + 1) = i) := by omega
401    have n3 : ¬ (d.lit_bufsize.toNat + d.sym_next.toNat = i) := by omega
402    rw [getD_set_u8, getD_set_u8, getD_set_u8]
403    simp [n1, n2, n3]
404
405end Zlib.Trees.Proofs.Out