trees.c.build.emit.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.build.support»
2import ZlibF.Proof.«trees.c.emit»
3import ZlibF.Spec.Format.Bits
4
5/-! # trees.c: transmitting the canonical values established by tree building -/
6
7namespace Zlib.Trees.Proofs
8open C Zlib.Trees
9
10/-- Stored reversed canonical words are sent in the format's most-significant
11bit order. This statement concerns exact bit order; prefix freedom requires
12the separate length/count consistency bridge. -/
13theorem canonical_code_wire (tk : TK) (d : DeflateState) (v : Nat)
14    (hc : (tk.arr d)[v]!.fc.toNat = Math.storedCode
15      (fun b => d.bl_count[b]!.toNat) (fun n => (tk.arr d)[n]!.dl.toNat) v) :
16    Out.natBits (tk.arr d)[v]!.fc.toNat (tk.arr d)[v]!.dl.toNat =
17      ZlibF.Spec.natToBitsMSB (tk.arr d)[v]!.dl.toNat
18        (Math.canonicalCode (fun b => d.bl_count[b]!.toNat) (fun n => (tk.arr d)[n]!.dl.toNat) v) := by
19  rw [hc]
20  unfold Out.natBits ZlibF.Spec.natToBitsMSB Math.storedCode
21  exact Math.reverseLowBits_wire _ _
22
23/-- The actual send_code reads the represented dynamic-tree entry and
24emits its exact canonical bits. Length and code-value facts are the data
25results of build_tree; its two reads are proved here. Output capacity and
26the current live output invariant remain explicit caller obligations. -/
27theorem send_canonical_code_emit {h : Heap} {id b : Nat} {d : DeflateState} {buf : Array UInt8}
28    (hI : Out.TreesInvAt h id d b buf) (tk : TK) (v : Nat) (hv : v < (tk.arr d).size)
29    (hl : (tk.arr d)[v]!.dl.toNat ≤ 15)
30    (hc : (tk.arr d)[v]!.fc.toNat = Math.storedCode
31      (fun b => d.bl_count[b]!.toNat) (fun n => (tk.arr d)[n]!.dl.toNat) v)
32    (hroom : 8 * d.pending.toNat + d.bi_valid.toInt.toNat + (tk.arr d)[v]!.dl.toNat ≤ 8 * buf.size) :
33    Out.Emit id b (send_code (Sp id) (v : Int) (.ref (tk.ref id) 0)) h d buf
34      (ZlibF.Spec.natToBitsMSB (tk.arr d)[v]!.dl.toNat
35        (Math.canonicalCode (fun b => d.bl_count[b]!.toNat) (fun n => (tk.arr d)[n]!.dl.toNat) v)) 2 := by
36  have hg := tk_get (h0 := h) (id := id) (d := d) tk
37  rw [setD_self hI.base.dstate] at hg
38  have hdl : getDl (.ref (tk.ref id) 0) (v : Int) h = .ok ((tk.arr d)[v]!.dl, h) := by
39    simpa only [getElem!_pos, hv] using Out.getDl_gen hg hv
40  have hfc : getFc (.ref (tk.ref id) 0) (v : Int) h = .ok ((tk.arr d)[v]!.fc, h) := by
41    simpa only [getElem!_pos, hv] using Out.getFc_gen hg hv
42  have hfit : (tk.arr d)[v]!.fc.toNat < 2 ^ (tk.arr d)[v]!.dl.toNat := by
43    rw [hc]
44    exact Math.storedCode_lt _ _ _
45  have hemit := Out.send_code_emit hI (v : Int) (.ref (tk.ref id) 0) _ _ hdl hfc hl hfit hroom
46  rw [canonical_code_wire tk d v hc] at hemit
47  exact hemit
48
49end Zlib.Trees.Proofs