trees.c.tally-support.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.bl-support»
2import ZlibF.Proof.«trees.c.tally»
3
4/-! # trees.c: retaining dynamic-header entry facts through actual tallies -/
5
6namespace Zlib.Trees.Proofs
7open C Zlib.Trees
8
9/-- Neither a literal nor a match tally writes the END_BLOCK frequency. -/
10theorem tallyRec_end_block (d : DeflateState) (dist lc : UInt32)
11    (hlit : dist = 0 → lc.toNat < 256) :
12    (Out.tallyRec d dist lc).dyn_ltree[256]!.fc = d.dyn_ltree[256]!.fc := by
13  unfold Out.tallyRec Out.tallyMatchRec Out.bumpFc
14  split
15  · rename_i hz
16    have hne : ¬ (lc.toNat = 256 ∧ lc.toNat < d.dyn_ltree.size) := by
17      have := hlit hz
18      omega
19    rw [Out.getElem!_set!, ite_eq_right hne]
20  · rw [Out.getElem!_set!]
21    rw [ite_eq_right (by omega)]
22
23/-- Tallies leave the bit-length tree unchanged. -/
24theorem tallyRec_bl_tree (d : DeflateState) (dist lc : UInt32) :
25    (Out.tallyRec d dist lc).bl_tree = d.bl_tree := by
26  unfold Out.tallyRec Out.tallyMatchRec
27  split <;> rfl
28
29/-- The three symbol stores advance sym_next by three. -/
30theorem tallyRec_sym_next (d : DeflateState) (dist lc : UInt32) :
31    (Out.tallyRec d dist lc).sym_next = d.sym_next + 1 + 1 + 1 := by
32  unfold Out.tallyRec Out.tallyMatchRec
33  split <;> rfl
34
35/-- A finite composition of actual tally calls. This is a proof harness for
36one block, not a replacement for a translated strategy loop. -/
37def tallyCalls (s : DeflateStatePtr) : List (UInt32 × UInt32) → M Unit
38  | [] => pure ()
39  | (dist, lc) :: rest => do
40      let _ ← «_tr_tally» s dist lc
41      tallyCalls s rest
42
43/-- Any capacity-bounded sequence of actual valid tallies retains the
44END_BLOCK frequency and all bit-length frequencies on its actual heap.
45No claim about the strategy's input history or emitted output is made here. -/
46theorem tallyCalls_preserves {h : Heap} {id b : Nat} {d : DeflateState} {buf : Array UInt8}
47    (hI : Out.TreesInvAt h id d b buf) (symbols : List (UInt32 × UInt32))
48    (hlegal : ∀ t ∈ symbols, t.2.toNat < 256 ∧ t.1.toNat ≤ 32768)
49    (hroom : d.sym_next.toNat + 3 * symbols.length ≤ d.sym_end.toNat) :
50    ∃ (e : DeflateState) (buf' : Array UInt8),
51      tallyCalls (Sp id) symbols h = .ok ((), Out.setD (Out.setB h b buf') id e) ∧
52      Out.TreesInvAt (Out.setD (Out.setB h b buf') id e) id e b buf' ∧
53      e.dyn_ltree[256]!.fc = d.dyn_ltree[256]!.fc ∧ e.bl_tree = d.bl_tree ∧
54      e.sym_next.toNat = d.sym_next.toNat + 3 * symbols.length ∧ e.sym_end = d.sym_end := by
55  induction symbols generalizing h d buf with
56  | nil =>
57    refine ⟨d, buf, ?_, ?_, rfl, rfl, by simp, rfl⟩
58    · simp only [tallyCalls, pure_app, Out.setB_self hI.base.bytes, Out.setD_self hI.base.dstate]
59    · simpa only [Out.setB_self hI.base.bytes, Out.setD_self hI.base.dstate] using hI
60  | cons t rest ih =>
61    obtain ⟨dist, lc⟩ := t
62    have hvalid := hlegal (dist, lc) (by simp)
63    have hstepRoom : d.sym_next.toNat + 3 ≤ d.sym_end.toNat := by
64      simp only [List.length_cons] at hroom
65      omega
66    obtain ⟨buf1, r, hstep, hI1, hflag, hsize, hbytes⟩ :=
67      Out.tr_tally_spec hI dist lc hstepRoom (fun _ => hvalid.1) (fun _ => hvalid)
68    let mid := Out.tallyRec d dist lc
69    have hnext : mid.sym_next.toNat = d.sym_next.toNat + 3 := by
70      have hbound : d.sym_next.toNat + 3 < 2 ^ 32 := by
71        have := hI.base.sym_end
72        have := hI.base.lit_hi
73        omega
74      rw [tallyRec_sym_next]
75      have h1 := Out.toNat_add_one_u32 (x := d.sym_next) (by omega)
76      have h2 := Out.toNat_add_one_u32 (x := d.sym_next + 1) (by rw [h1]; omega)
77      have h3 := Out.toNat_add_one_u32 (x := d.sym_next + 1 + 1) (by rw [h2, h1]; omega)
78      rw [h3, h2, h1]
79    have hend : mid.sym_end = d.sym_end := (Out.tallyRec_fields d dist lc).2.2.2.2.1
80    have hrestRoom : mid.sym_next.toNat + 3 * rest.length ≤ mid.sym_end.toNat := by
81      rw [hnext, hend]
82      simp only [List.length_cons] at hroom
83      omega
84    obtain ⟨e, buf', hrest, hIe, hEOB, hBL, hcount, hEnd⟩ :=
85      ih hI1 (fun t ht => hlegal t (by simp [ht])) hrestRoom
86    refine ⟨e, buf', ?_, ?_, ?_, ?_, ?_, hEnd.trans hend⟩
87    · simp only [tallyCalls, bind_app, hstep]
88      simpa only [Out.setB_setD, Out.setB_setB, Out.setD_setD] using hrest
89    · simpa only [Out.setB_setD, Out.setB_setB, Out.setD_setD] using hIe
90    · exact hEOB.trans (tallyRec_end_block d dist lc (fun _ => hvalid.1))
91    · exact hBL.trans (tallyRec_bl_tree d dist lc)
92    · rw [hcount, hnext, List.length_cons]
93      omega
94
95/-- Valid tallies within one block establish the actual dynamic-header
96construction premises. The result is on the same heap after all calls. -/
97theorem tallyCalls_prepare_bl_fields {h : Heap} {id b : Nat} {d : DeflateState} {buf : Array UInt8}
98    (hI : Out.TreesInvAt h id d b buf) (symbols : List (UInt32 × UInt32))
99    (hlegal : ∀ t ∈ symbols, t.2.toNat < 256 ∧ t.1.toNat ≤ 32768)
100    (hroom : d.sym_next.toNat + 3 * symbols.length ≤ d.sym_end.toNat)
101    (hEOB : d.dyn_ltree[256]!.fc ≠ 0) (hzero : ∀ k < 19, d.bl_tree[k]!.fc = 0) :
102    ∃ (mb : Int32) (e : DeflateState) (buf' : Array UInt8),
103      (do tallyCalls (Sp id) symbols; blPrepare (Sp id); build_bl_tree (Sp id)) h =
104        .ok (mb, Out.setD (Out.setB h b buf') id e) ∧
105      3 ≤ mb.toInt ∧ mb.toInt ≤ 18 ∧
106      257 ≤ e.l_desc.max_code.toInt + 1 ∧ e.l_desc.max_code.toInt + 1 ≤ 286 ∧
107      1 ≤ e.d_desc.max_code.toInt + 1 ∧ e.d_desc.max_code.toInt + 1 ≤ 30 ∧
108      (∀ v < 19, e.bl_tree[v]!.dl.toNat ≤ 7) ∧
109      (∀ v < 19, e.bl_desc.max_code.toInt.toNat < v → e.bl_tree[v]!.dl = 0) ∧
110      Out.TreesInvAt (Out.setD (Out.setB h b buf') id e) id e b buf' := by
111  obtain ⟨counted, buf', htally, hIC, hEC, hBC, hcount, hEnd⟩ :=
112    tallyCalls_preserves hI symbols hlegal hroom
113  have hEC' : counted.dyn_ltree[256]!.fc ≠ 0 := by rwa [hEC]
114  have hBC' : ∀ k < 19, counted.bl_tree[k]!.fc = 0 := by rwa [hBC]
115  obtain ⟨mb, e, hbuild, hlo, hhi, hlL, hlH, hdL, hdH, hlen, hupper, hIe, hout⟩ :=
116    prepare_build_bl_fields hIC hEC' hBC'
117  refine ⟨mb, e, buf', ?_, hlo, hhi, hlL, hlH, hdL, hdH, hlen, hupper, ?_⟩
118  · change (do blPrepare (Sp id); build_bl_tree (Sp id))
119        (Out.setD (Out.setB h b buf') id counted) =
120        .ok (mb, Out.setD (Out.setD (Out.setB h b buf') id counted) id e) at hbuild
121    rw [bind_app, htally]
122    simpa only [Out.setD_setD] using hbuild
123  · change Out.TreesInvAt (Out.setD (Out.setD (Out.setB h b buf') id counted) id e) id e b buf' at hIe
124    simpa only [Out.setD_setD] using hIe
125
126/-- Actual init_block, any capacity-bounded list of valid actual tallies,
127and actual literal/distance/bit-length construction supply all dynamic-header
128field ranges. This proves the call composition, not the strategy loop that
129produces the tallies, header emission, or the output/symbol overlay bound. -/
130theorem init_tallies_prepare_bl_fields {h : Heap} {id b : Nat} {d : DeflateState} {buf : Array UInt8}
131    (hI : Out.TreesInvAt h id d b buf) (symbols : List (UInt32 × UInt32))
132    (hlegal : ∀ t ∈ symbols, t.2.toNat < 256 ∧ t.1.toNat ≤ 32768)
133    (hroom : 3 * symbols.length ≤ d.sym_end.toNat) :
134    ∃ (mb : Int32) (e : DeflateState) (buf' : Array UInt8),
135      (do init_block (Sp id); tallyCalls (Sp id) symbols
136          blPrepare (Sp id); build_bl_tree (Sp id)) h =
137        .ok (mb, Out.setD (Out.setB h b buf') id e) ∧
138      3 ≤ mb.toInt ∧ mb.toInt ≤ 18 ∧
139      257 ≤ e.l_desc.max_code.toInt + 1 ∧ e.l_desc.max_code.toInt + 1 ≤ 286 ∧
140      1 ≤ e.d_desc.max_code.toInt + 1 ∧ e.d_desc.max_code.toInt + 1 ≤ 30 ∧
141      (∀ v < 19, e.bl_tree[v]!.dl.toNat ≤ 7) ∧
142      (∀ v < 19, e.bl_desc.max_code.toInt.toNat < v → e.bl_tree[v]!.dl = 0) ∧
143      Out.TreesInvAt (Out.setD (Out.setB h b buf') id e) id e b buf' := by
144  obtain ⟨aL, aD, aB, initialized, hinit, hII, heI, hLs, hDs, hBs,
145    hLzero, hEOB, hDzero, hBzero, hLdl, hDdl, hBdl⟩ := Out.init_block_spec0 hI.base hI.run.to0
146  have hEI : initialized.dyn_ltree[256]!.fc ≠ 0 := by
147    rw [heI]
148    change aL[256]!.fc ≠ 0
149    rw [hEOB]
150    decide +kernel
151  have hzI : ∀ k < 19, initialized.bl_tree[k]!.fc = 0 := by
152    intro k hk
153    rw [heI]
154    exact hBzero k hk
155  have hroomI : initialized.sym_next.toNat + 3 * symbols.length ≤ initialized.sym_end.toNat := by
156    rw [heI]
157    change (0 : UInt32).toNat + 3 * symbols.length ≤ d.sym_end.toNat
158    simpa using hroom
159  obtain ⟨mb, e, buf', hbuild, hlo, hhi, hlL, hlH, hdL, hdH, hlen, hupper, hIe⟩ :=
160    tallyCalls_prepare_bl_fields hII symbols hlegal hroomI hEI hzI
161  refine ⟨mb, e, buf', ?_, hlo, hhi, hlL, hlH, hdL, hdH, hlen, hupper, ?_⟩
162  · rw [bind_app, hinit]
163    simpa only [Out.setB_setD, Out.setD_setD] using hbuild
164  · simpa only [Out.setB_setD, Out.setD_setD] using hIe
165
166end Zlib.Trees.Proofs