trees.c.codes.lean

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

1import ZlibF.Math.DeflateCodes
2import ZlibF.Proof.«trees.c.monad»
3import ZlibF.Proof.«trees.c.heap.gbp1»
4import ZlibF.Proof.«trees.c.reverse»
5
6/-!
7# trees.c: canonical code assignment
8
9The two loop invariants follow the reference `zlib-formal` `GenCodes` proof.
10The executions below use this repository's actual accessors and checked
11arithmetic. No tree-construction contract is assumed.
12-/
13
14namespace Zlib.Trees.Proofs
15open C Zlib.Trees
16
17/-- The first loop of `gen_codes`, verbatim. -/
18def gcStart (bl_count : WPtr) : M (Int32 × UInt32 × Array UInt16) :=
19  cfor (σ := Int32 × UInt32 × Array UInt16)
20    (fun (bits, _, _) => pure (decide (bits.toInt ≤ MAX_BITS.toInt)))
21    (fun (bits, code, nc) => do pure (← iadd bits 1, code, nc))
22    (fun (bits, code, nc) => do
23      let b ← Ptr.index bl_count (← isub bits 1).toInt
24      let code := (code + b.toUInt32) <<< 1
25      if bits.toInt < 0 ∨ nc.size ≤ bits.toInt.toNat then ub "next_code index outside its array"
26      pure (bits, code, nc.set! bits.toInt.toNat code.toUInt16))
27    (1, 0, Array.replicate 16 0)
28
29/-- The symbol loop of `gen_codes`, verbatim. -/
30def gcAssign (tree : CtDataPtr) (max_code : Int32) (next_code : Array UInt16) :
31    M (Int32 × Array UInt16) :=
32  cfor (σ := Int32 × Array UInt16)
33    (fun (n, _) => pure (decide (n.toInt ≤ max_code.toInt)))
34    (fun (n, nc) => do pure (← iadd n 1, nc))
35    (fun (n, nc) => do
36      let len := u16i (← getDl tree n.toInt)
37      if len == 0 then return (n, nc)
38      let li := len.toInt.toNat
39      if nc.size ≤ li then ub "next_code index outside its array"
40      let old := nc[li]!
41      let nc := nc.set! li (old + 1)
42      let r ← bi_reverse old.toUInt32 len
43      setFc tree n.toInt r.toUInt16
44      pure (n, nc))
45    (0, next_code)
46
47theorem gen_codes_eq (tree : CtDataPtr) (max_code : Int32) (bl_count : WPtr) :
48    gen_codes tree max_code bl_count = (do
49      let (_, _, nc) ← gcStart bl_count
50      let _ ← gcAssign tree max_code nc
51      pure ()) := rfl
52
53/-- All fifteen canonical starting codes are computed without changing the
54heap. Counts are arbitrary unsigned 16-bit values; wrapping is accounted for. -/
55theorem gcStart_run {h0 : Heap} {id : Nat} (d : DeflateState)
56    (hsz : 15 ≤ d.bl_count.size) :
57    WS h0 id (gcStart (.ref (.dstate_bl_count id) 0)) d (fun r e =>
58      e = d ∧ r.2.2.size = 16 ∧ ∀ b, 1 ≤ b → b < 16 →
59        r.2.2[b]! = UInt16.ofNat (Math.nextCode (fun i => d.bl_count[i]!.toNat) b)) := by
60  let bl : Nat → Nat := fun i => d.bl_count[i]!.toNat
61  let Inv : Int32 × UInt32 × Array UInt16 → DeflateState → Prop := fun r e =>
62    ∃ k : Nat, k ≤ 15 ∧ e = d ∧ r.1.toInt = k + 1 ∧
63      r.2.1.toNat = Math.nextCode bl k % 4294967296 ∧ r.2.2.size = 16 ∧
64      ∀ b, 1 ≤ b → b ≤ k → r.2.2[b]! = UInt16.ofNat (Math.nextCode bl b)
65  unfold gcStart
66  refine WS.cfor2 Inv (fun r _ => 15 - (r.1.toInt - 1).toNat) _ ?_
67    ⟨0, by omega, rfl, rfl, rfl, by simp, fun b h1 h2 => by omega⟩ (by simp [fuel])
68  rintro ⟨bits, code, nc⟩ e ⟨k, hk, rfl, hb, hc, hs, hv⟩
69  change bits.toInt = (k : Int) + 1 at hb
70  change code.toNat = Math.nextCode bl k % 4294967296 at hc
71  change nc.size = 16 at hs
72  change ∀ b, 1 ≤ b → b ≤ k → nc[b]! = UInt16.ofNat (Math.nextCode bl b) at hv
73  refine WS.pure' ?_
74  by_cases hlt : k < 15
75  · refine Or.inr ⟨by simp only [decide_eq_true_eq]; change bits.toInt ≤ 15; omega, ?_⟩
76    have h1 : (1 : Int32).toInt = 1 := rfl
77    dsimp only
78    simp only [M_bind_assoc]
79    refine WS.bind' (ws_isub bits 1 (by omega) (by omega)) fun ix e1 ⟨hi, he1⟩ => ?_
80    subst e1
81    have hik : ix.toInt = k := by omega
82    refine WS.bind' (ws_index_blc ix.toInt (by omega) (by omega)) fun v e1 ⟨hv0, he1⟩ => ?_
83    subst e1; subst v
84    have hiN : ix.toInt.toNat = k := by omega
85    have hbN : bits.toInt.toNat = k + 1 := by omega
86    have hbad : ¬ (bits.toInt < 0 ∨ nc.size ≤ bits.toInt.toNat) := by omega
87    simp only [hbad, ite_false, M_pure_bind]
88    refine WS.bind' (ws_iadd bits 1 (by omega) (by omega)) fun bits' e1 ⟨hb', he1⟩ => ?_
89    subst e1
90    refine WS.pure' ⟨⟨k + 1, by omega, rfl, by dsimp; omega, ?_, ?_, ?_⟩, ?_⟩
91    · dsimp only
92      rw [UInt32.toNat_shiftLeft, UInt32.toNat_add, hc, hiN]
93      simp only [UInt16.toNat_toUInt32, Math.nextCode]
94      rw [show (1 : UInt32).toNat % 32 = 1 from rfl, Nat.shiftLeft_eq]
95      dsimp only [bl]
96      omega
97    · simpa only [size_set!] using hs
98    · intro b h1 h2
99      dsimp only
100      rw [getD_set nc bits.toInt.toNat b _ (by omega), hbN]
101      by_cases heq : b = k + 1
102      · rw [ite_eq_left heq]
103        subst b
104        apply UInt16.toNat_inj.mp
105        simp only [UInt32.toNat_toUInt16, UInt16.toNat_ofNat', UInt32.toNat_shiftLeft,
106          UInt32.toNat_add, hc, UInt16.toNat_toUInt32, hiN, Math.nextCode]
107        rw [show (1 : UInt32).toNat % 32 = 1 from rfl, Nat.shiftLeft_eq]
108        dsimp only [bl]
109        omega
110      · rw [ite_eq_right heq]; exact hv b h1 (by omega)
111    · dsimp only; omega
112  · refine Or.inl ⟨by simp only [decide_eq_false_iff_not]; change ¬ bits.toInt ≤ 15; omega,
113      rfl, hs, fun b h1 h2 => hv b h1 (by omega)⟩
114
115private theorem gc_reverse_eq (c k : Nat) : Out.revBits c k = Math.reverseLowBits c k := by
116  induction k with
117  | zero => rfl
118  | succ k ih => simp only [Out.revBits, Math.reverseLowBits, ih]
119
120private theorem gc_setArr_twice (tk : TK) (d : DeflateState) (a b : Array CtData) :
121    tk.setArr (tk.setArr d a) b = tk.setArr d b := by cases tk <;> rfl
122
123/-- The actual symbol loop writes each positive-length symbol's canonical,
124bit-reversed code. Zero-length symbols and every other field are preserved.
125The internal domain includes empty ranges and arbitrary length/count arrays;
126only the array bounds and the fifteen-bit length limit are required. -/
127theorem gcAssign_run {h0 : Heap} {id : Nat} (d : DeflateState) (tk : TK)
128    (max_code : Int32) (nc : Array UInt16)
129    (hm0 : -1 ≤ max_code.toInt) (hm1 : max_code.toInt < 573)
130    (hfit : (max_code.toInt + 1).toNat ≤ (tk.arr d).size)
131    (hlen : ∀ j < (max_code.toInt + 1).toNat, ((tk.arr d)[j]!).dl.toNat ≤ 15)
132    (hnc : nc.size = 16)
133    (hstart : ∀ b, 1 ≤ b → b < 16 →
134      nc[b]! = UInt16.ofNat (Math.nextCode (fun i => d.bl_count[i]!.toNat) b)) :
135    WS h0 id (gcAssign (.ref (tk.ref id) 0) max_code nc) d (fun _ e =>
136      ∃ a : Array CtData, e = tk.setArr d a ∧ a.size = (tk.arr d).size ∧
137        ∀ j < a.size, a[j]! =
138          if j < (max_code.toInt + 1).toNat ∧ ((tk.arr d)[j]!).dl ≠ 0 then
139            { (tk.arr d)[j]! with fc := UInt16.ofNat (Math.storedCode
140              (fun i => d.bl_count[i]!.toNat) (fun i => ((tk.arr d)[i]!).dl.toNat) j) }
141          else (tk.arr d)[j]!) := by
142  let M := (max_code.toInt + 1).toNat
143  let orig := tk.arr d
144  let len : Nat → Nat := fun j => orig[j]!.dl.toNat
145  let bl : Nat → Nat := fun j => d.bl_count[j]!.toNat
146  let entry : Nat → Nat → CtData := fun m j =>
147    if j < m ∧ orig[j]!.dl ≠ 0 then
148      { orig[j]! with fc := UInt16.ofNat (Math.storedCode bl len j) }
149    else orig[j]!
150  let Inv : Int32 × Array UInt16 → DeflateState → Prop := fun r e =>
151    ∃ (m : Nat) (a : Array CtData), m ≤ M ∧ r.1.toInt = m ∧
152      e = tk.setArr d a ∧ a.size = orig.size ∧ r.2.size = 16 ∧
153      (∀ b, 1 ≤ b → b < 16 →
154        r.2[b]! = UInt16.ofNat (Math.nextCode bl b + Math.countBefore len b m)) ∧
155      ∀ j < a.size, a[j]! = entry m j
156  have hi1 : (1 : Int32).toInt = 1 := rfl
157  have hMv : max_code.toInt + 1 = M := by dsimp [M]; omega
158  have hself : tk.setArr d orig = d := by cases tk <;> rfl
159  unfold gcAssign
160  refine WS.cfor2 Inv (fun r _ => M - r.1.toInt.toNat) _ ?_
161    ⟨0, orig, by omega, rfl, hself.symm, rfl, hnc, ?_, ?_⟩ (by simp only [fuel]; omega)
162  · rintro ⟨n, nc⟩ e ⟨m, a, hm, hn, he, hsz, hnc, hv, ha⟩
163    subst e
164    change n.toInt = (m : Int) at hn
165    change nc.size = 16 at hnc
166    change ∀ b, 1 ≤ b → b < 16 →
167      nc[b]! = UInt16.ofNat (Math.nextCode bl b + Math.countBefore len b m) at hv
168    refine WS.pure' ?_
169    by_cases hlt : m < M
170    · refine Or.inr ⟨by simp only [decide_eq_true_eq]; omega, ?_⟩
171      have hnN : n.toInt.toNat = m := by omega
172      have hmA : m < a.size := by dsimp [orig] at hsz; dsimp [M] at hlt; omega
173      have hmOrig : m < orig.size := by omega
174      have hdl : a[m]!.dl = orig[m]!.dl := by
175        rw [ha m hmA]; dsimp only [entry]; split <;> rfl
176      have hlen15 : len m ≤ 15 := hlen m hlt
177      dsimp only
178      simp only [M_bind_assoc]
179      refine WS.bind' (ws_getDl tk n.toInt (by omega) (by simp only [tk_arr_setArr]; omega))
180        fun v e1 ⟨hv0, he1⟩ => ?_
181      subst e1
182      have hv' : v = orig[m]!.dl := by simpa only [tk_arr_setArr, hnN, hdl] using hv0
183      subst v
184      simp only [tk_arr_setArr, hnN, hdl]
185      have hlenInt : (u16i orig[m]!.dl).toInt = len m := u16i_toInt _
186      by_cases hz : orig[m]!.dl = 0
187      · have hzero : (u16i orig[m]!.dl == 0) = true := by simp [hz, u16i]
188        simp only [hzero, Bool.true_eq, ite_true, M_pure_bind]
189        refine WS.bind' (ws_iadd n 1 (by have : (1 : Int32).toInt = 1 := rfl; omega)
190          (by have : (1 : Int32).toInt = 1 := rfl; omega)) fun n' e1 ⟨hn', he1⟩ => ?_
191        subst e1
192        refine WS.pure' ⟨⟨m + 1, a, by omega, by dsimp; have : (1 : Int32).toInt = 1 := rfl; omega,
193          rfl, hsz, hnc, ?_, ?_⟩, by dsimp; have : (1 : Int32).toInt = 1 := rfl; omega⟩
194        · intro b hb1 hb2
195          have hlzero : len m = 0 := by dsimp [len]; rw [hz]; rfl
196          rw [Math.countBefore_succ, ite_eq_right (by omega), Nat.add_zero]
197          exact hv b hb1 hb2
198        · intro j hj
199          rw [ha j hj]
200          dsimp only [entry]
201          by_cases heq : j = m
202          · subst j; simp [hz]
203          · have hcut : (j < m) ↔ (j < m + 1) := by omega
204            simp only [hcut]
205      · have hlenPos : 1 ≤ len m := by
206          have h0 : orig[m]!.dl.toNat ≠ 0 := fun h => hz (UInt16.toNat_inj.mp h)
207          dsimp only [len]; omega
208        have hnonzero : (u16i orig[m]!.dl == 0) = false := by
209          simp only [beq_eq_false_iff_ne]
210          intro h; have hh := congrArg Int32.toInt h
211          rw [hlenInt] at hh; have : (0 : Int32).toInt = 0 := rfl; omega
212        have hbad : ¬ nc.size ≤ (u16i orig[m]!.dl).toInt.toNat := by omega
213        simp only [hnonzero, Bool.false_eq_true, ite_false, hbad]
214        have hli : (u16i orig[m]!.dl).toInt.toNat = len m := by omega
215        rw [hli]
216        let X := Math.nextCode bl (len m) + Math.countBefore len (len m) m
217        have hncval : nc[len m]! = UInt16.ofNat X := hv (len m) hlenPos (by omega)
218        obtain ⟨r, hr, hrv⟩ := Out.bi_reverse_correct (setD h0 id (tk.setArr d a))
219          nc[len m]!.toUInt32 (u16i orig[m]!.dl) (by omega) (by omega)
220        have hcode : r.toNat = Math.storedCode bl len m := by
221          rw [hrv, hli, hncval, UInt16.toNat_toUInt32, UInt16.toNat_ofNat', gc_reverse_eq]
222          change Math.reverseLowBits (X % 2 ^ 16) (len m) = Math.reverseLowBits X (len m)
223          exact Math.reverseLowBits_mod_of_le X (len m) 16 (by omega)
224        simp only [M_bind_assoc, M_pure_bind]
225        have hrev : WS h0 id (bi_reverse nc[len m]!.toUInt32 (u16i orig[m]!.dl))
226            (tk.setArr d a) (fun v e => v = r ∧ e = tk.setArr d a) := WS.of_eq hr ⟨rfl, rfl⟩
227        refine WS.bind' hrev
228          fun r' e1 ⟨hr', he1⟩ => ?_
229        subst e1; subst r'
230        refine WS.bind' (ws_setFc tk n.toInt r.toUInt16 (by omega)
231          (by simp only [tk_arr_setArr]; omega)) fun _ e1 he1 => ?_
232        subst e1
233        simp only [tk_arr_setArr, hnN, gc_setArr_twice]
234        refine WS.bind' (ws_iadd n 1 (by have : (1 : Int32).toInt = 1 := rfl; omega)
235          (by have : (1 : Int32).toInt = 1 := rfl; omega)) fun n' e1 ⟨hn', he1⟩ => ?_
236        subst e1
237        refine WS.pure' ⟨⟨m + 1, a.set! m { a[m]! with fc := r.toUInt16 }, by omega,
238          by dsimp; have : (1 : Int32).toInt = 1 := rfl; omega,
239          rfl, by simpa only [size_set!] using hsz,
240          by simpa only [size_set!] using hnc, ?_, ?_⟩,
241          by dsimp; have : (1 : Int32).toInt = 1 := rfl; omega⟩
242        · intro b hb1 hb2
243          dsimp only
244          rw [getD_set nc (len m) b _ (by omega), Math.countBefore_succ]
245          by_cases heq : len m = b
246          · rw [ite_eq_left heq, ite_eq_left heq.symm]
247            subst b
248            rw [hncval]
249            apply UInt16.toNat_inj.mp
250            simp only [UInt16.toNat_add, UInt16.toNat_ofNat']
251            change (X % 65536 + 1) % 65536 = (X + 1) % 65536
252            omega
253          · rw [ite_eq_right heq, ite_eq_right (Ne.symm heq), Nat.add_zero]
254            exact hv b hb1 hb2
255        · intro j hj
256          have hjA : j < a.size := by simpa only [size_set!] using hj
257          rw [getD_set a m j _ hmA]
258          by_cases heq : j = m
259          · rw [ite_eq_left heq]
260            subst j
261            have hsame : a[m]! = orig[m]! := by
262              rw [ha m hmA]; dsimp only [entry]; simp
263            have hcv : r.toUInt16 = UInt16.ofNat (Math.storedCode bl len m) := by
264              apply UInt16.toNat_inj.mp
265              simp only [UInt32.toNat_toUInt16, UInt16.toNat_ofNat', hcode]
266            dsimp only [entry]
267            simp only [Nat.lt_succ_self, hz, ne_eq, not_false_eq_true, and_self, ite_true]
268            rw [hsame, hcv]
269          · rw [ite_eq_right heq, ha j hjA]
270            dsimp only [entry]
271            have hcut : (j < m) ↔ (j < m + 1) := by omega
272            simp only [hcut]
273    · refine Or.inl ⟨by simp only [decide_eq_false_iff_not]; omega,
274        a, rfl, hsz, ?_⟩
275      intro j hj
276      have hmM : m = M := by omega
277      simpa only [hmM] using ha j hj
278  · intro b h1 h2
279    simpa only [Math.countBefore_zero, Nat.add_zero] using hstart b h1 h2
280  · intro j hj
281    dsimp only [entry]
282    simp
283
284/-- `gen_codes` composes its two actual loops on one state. All lengths and
285all fields outside the selected tree's code cells are preserved. -/
286theorem ws_gen_codes {h0 : Heap} {id : Nat} (d : DeflateState) (tk : TK)
287    (max_code : Int32) (hbc : 15 ≤ d.bl_count.size)
288    (hm0 : -1 ≤ max_code.toInt) (hm1 : max_code.toInt < 573)
289    (hfit : (max_code.toInt + 1).toNat ≤ (tk.arr d).size)
290    (hlen : ∀ j < (max_code.toInt + 1).toNat, ((tk.arr d)[j]!).dl.toNat ≤ 15) :
291    WS h0 id (gen_codes (.ref (tk.ref id) 0) max_code (.ref (.dstate_bl_count id) 0)) d
292      (fun _ e => ∃ a : Array CtData, e = tk.setArr d a ∧ a.size = (tk.arr d).size ∧
293        ∀ j < a.size, a[j]! =
294          if j < (max_code.toInt + 1).toNat ∧ ((tk.arr d)[j]!).dl ≠ 0 then
295            { (tk.arr d)[j]! with fc := UInt16.ofNat (Math.storedCode
296              (fun i => d.bl_count[i]!.toNat) (fun i => ((tk.arr d)[i]!).dl.toNat) j) }
297          else (tk.arr d)[j]!) := by
298  rw [gen_codes_eq]
299  refine WS.bind' (gcStart_run d hbc) fun r e ⟨he, hsz, hv⟩ => ?_
300  subst e
301  rcases r with ⟨bits, code, nc⟩
302  dsimp only at hsz hv ⊢
303  refine WS.bind' (gcAssign_run d tk max_code nc hm0 hm1 hfit hlen hsz hv) fun _ e he => ?_
304  exact WS.pure' he
305
306/-- `local void gen_codes(ct_data *tree, int max_code, ushf *bl_count)`.
307For any of the three live dynamic tree arrays, an internal symbol range
308`-1 ≤ max_code < 573` fitting that array, at least fifteen readable counts,
309and code lengths at most fifteen, the actual translated function terminates
310without a fault. Every positive-length symbol receives its canonical code
311in reversed bit order. Only those code cells change. No consistency or Kraft
312condition on the counts and lengths is assumed. This is an internal callee
313result; its preconditions still have to be established by `build_tree`. -/
314theorem gen_codes_correct {h : Heap} {id : Nat} {d : DeflateState}
315    (hd : h.dstates id = some d) (tk : TK) (max_code : Int32)
316    (hbc : 15 ≤ d.bl_count.size) (hm0 : -1 ≤ max_code.toInt) (hm1 : max_code.toInt < 573)
317    (hfit : (max_code.toInt + 1).toNat ≤ (tk.arr d).size)
318    (hlen : ∀ j < (max_code.toInt + 1).toNat, ((tk.arr d)[j]!).dl.toNat ≤ 15) :
319    ∃ a : Array CtData,
320      gen_codes (.ref (tk.ref id) 0) max_code (.ref (.dstate_bl_count id) 0) h =
321        .ok ((), setD h id (tk.setArr d a)) ∧
322      a.size = (tk.arr d).size ∧ ∀ j < a.size, a[j]! =
323        if j < (max_code.toInt + 1).toNat ∧ ((tk.arr d)[j]!).dl ≠ 0 then
324          { (tk.arr d)[j]! with fc := UInt16.ofNat (Math.storedCode
325            (fun i => d.bl_count[i]!.toNat) (fun i => ((tk.arr d)[i]!).dl.toNat) j) }
326        else (tk.arr d)[j]! := by
327  obtain ⟨u, e, hr, a, rfl, hsz, hv⟩ := ws_gen_codes (h0 := h) (id := id) d tk max_code hbc hm0 hm1 hfit hlen
328  cases u
329  rw [setD_self hd] at hr
330  exact ⟨a, hr, hsz, hv⟩
331
332end Zlib.Trees.Proofs