trees.c.send-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.send-tree»
2import ZlibF.Proof.«trees.c.tally-support»
3
4/-! # trees.c: deriving send_tree's data premises from actual construction -/
5
6namespace Zlib.Trees.Proofs
7open C Zlib.Trees Out
8
9/-- Length values actually read by the tree-description writer. -/
10def sendLengths (d : DeflateState) (tk : TK) (i : Nat) : Nat := (tk.arr d)[i]!.dl.toNat
11
12/-- Source storage and code data for the actual writer. No callee contract
13or output-capacity assumption is a field. -/
14structure SendTreeData (d : DeflateState) (tk : TK) : Prop where
15  nonneg : 0 ≤ (tk.getDesc d).max_code.toInt
16  max285 : (tk.getDesc d).max_code.toInt ≤ 285
17  capacity : (tk.getDesc d).max_code.toInt.toNat + 1 < (tk.arr d).size
18  lengths : ∀ i ≤ (tk.getDesc d).max_code.toInt.toNat, sendLengths d tk i ≤ 15
19  codes : ∀ k < 19, 0 < scanFreqUpTo (sendLengths d tk) ((tk.getDesc d).max_code.toInt.toNat + 1) k →
20    CodeFits (blWords d) k ∧ ∀ suffix : List Bool,
21      ZlibF.Spec.decodeSym (Zlib.Inftrees.Proofs.lensOf (fun n => d.bl_tree[n]!.dl.toNat)
22        (d.bl_desc.max_code.toInt.toNat + 1))
23        (codeBits (blWords d) k ++ suffix) = some (k, suffix)
24
25/-- Derived data and exact bit room suffice for the actual writer. -/
26theorem SendTreeData.emit {h : Heap} {id b : Nat} {d : DeflateState} {buf : Array UInt8}
27    (hI : TreesInvAt h id d b buf) (tk : TK) (hd : SendTreeData d tk)
28    (hr : 8 * d.pending.toNat + d.bi_valid.toInt.toNat +
29      (sendTreeBits (blWords d) (sendLengths d tk) (tk.getDesc d).max_code.toInt.toNat).length ≤ 8 * buf.size) :
30    Emit id b (send_tree (Sp id) (.ref (tk.ref id) 0) (tk.getDesc d).max_code) h d buf
31      (sendTreeBits (blWords d) (sendLengths d tk) (tk.getDesc d).max_code.toInt.toNat)
32      (d.bi_valid.toInt.toNat + (sendTreeBits (blWords d) (sendLengths d tk) (tk.getDesc d).max_code.toInt.toNat).length) := by
33  exact send_tree_emit hI tk (sendLengths d tk) _ _ (by have := hd.nonneg; omega)
34    (by have := hd.max285; omega) hd.capacity (fun _ _ => rfl) (fun _ => UInt16.toNat_lt _)
35    hd.lengths (fun k hk hpos => (hd.codes k hk hpos).1) hr
36
37/-- Complete actual BL construction establishes the source and code data
38for both real send_tree calls. Initial zero BL frequencies prevent wrapping
39from erasing a positively used source symbol. Output room is not assumed. -/
40theorem build_bl_tree_ready_to_send {h : Heap} {id b : Nat} {d : DeflateState} {buf : Array UInt8}
41    (hI : TreesInvAt h id d b buf) (hin : BLInput d)
42    (hzero : ∀ k < 19, d.bl_tree[k]!.fc = 0) :
43    ∃ (mb : Int32) (e : DeflateState), build_bl_tree (Sp id) h = .ok (mb, setD h id e) ∧
44      TreesInvAt (setD h id e) id e b buf ∧
45      (∀ tk : TK, tk ≠ .bl → SendTreeData e tk) := by
46  obtain ⟨mb, scanned, built, e, B, hr, hs, hfreq, hframe, he, hmb, hlo, hhi, htail, hIe, hout, hcodes⟩ :=
47    build_bl_tree_checked hI hin
48  have hLT := hframe.other_tree .lit (by decide +kernel)
49  have hDT := hframe.other_tree .dist (by decide +kernel)
50  have hLD := hframe.other_desc .lit (by decide +kernel)
51  have hDD := hframe.other_desc .dist (by decide +kernel)
52  simp only [TK.arr] at hLT hDT
53  simp only [TK.getDesc] at hLD hDD
54  have hEL : e.dyn_ltree = scGuard d.dyn_ltree d.l_desc.max_code.toInt.toNat := by
55    rw [he]
56    change built.dyn_ltree = _
57    rw [hLT, hs]
58    rfl
59  have hED : e.dyn_dtree = scGuard d.dyn_dtree d.d_desc.max_code.toInt.toNat := by
60    rw [he]
61    change built.dyn_dtree = _
62    rw [hDT, hs]
63    rfl
64  have hELD : e.l_desc = d.l_desc := by
65    rw [he]
66    change built.l_desc = _
67    rw [hLD, hs]
68    rfl
69  have hEDD : e.d_desc = d.d_desc := by
70    rw [he]
71    change built.d_desc = _
72    rw [hDD, hs]
73    rfl
74  have hLsize := hI.base.wf.1
75  have hDsize := hI.base.wf.2.1
76  have hLM := hin.l286
77  have hDM := hin.d30
78  have hL0 := hin.l0
79  have hD0 := hin.d0
80  have hLCap : d.l_desc.max_code.toInt.toNat + 1 < d.dyn_ltree.size := by omega
81  have hDCap : d.d_desc.max_code.toInt.toNat + 1 < d.dyn_dtree.size := by omega
82  have hLfun : sendLengths e .lit = guarded (fun i => d.dyn_ltree[i]!.dl.toNat) d.l_desc.max_code.toInt.toNat := by
83    funext i
84    change e.dyn_ltree[i]!.dl.toNat = _
85    rw [hEL]
86    exact scGuard_lengths _ _ hLCap i
87  have hDfun : sendLengths e .dist = guarded (fun i => d.dyn_dtree[i]!.dl.toNat) d.d_desc.max_code.toInt.toNat := by
88    funext i
89    change e.dyn_dtree[i]!.dl.toNat = _
90    rw [hED]
91    exact scGuard_lengths _ _ hDCap i
92  have hfits : ∀ k < 19, 0 < blScanCount d k → CodeFits (blWords e) k ∧ ∀ suffix : List Bool,
93      ZlibF.Spec.decodeSym (Zlib.Inftrees.Proofs.lensOf (fun n => e.bl_tree[n]!.dl.toNat)
94        (e.bl_desc.max_code.toInt.toNat + 1))
95        (codeBits (blWords e) k ++ suffix) = some (k, suffix) := by
96    intro k hk hpos
97    have hbound := blScanCount_le d hin k
98    have hnat : B[k]!.fc.toNat = blScanCount d k := by
99      rw [hfreq k, hzero k hk, UInt16.zero_add, UInt16.toNat_ofNat']
100      exact Nat.mod_eq_of_lt (by omega)
101    have hnz : scanned.bl_tree[k]!.fc ≠ 0 := by
102      rw [hs]
103      change B[k]!.fc ≠ 0
104      intro hz
105      rw [hz] at hnat
106      change 0 = blScanCount d k at hnat
107      omega
108    obtain ⟨maxc, hmax, hdesc, hacc, hword⟩ := hcodes
109    have hdata := (hword k hk hnz).1
110    refine ⟨?_, ?_⟩
111    · change e.bl_tree[k]!.dl.toNat ≤ 15 ∧ e.bl_tree[k]!.fc.toNat < 2 ^ e.bl_tree[k]!.dl.toNat
112      exact ⟨by have := hdata.2.1; omega, hdata.2.2.2⟩
113    · rw [hdesc]
114      simpa only [Int.toNat_natCast, codeBits, blWords] using (hword k hk hnz).2
115  refine ⟨mb, e, hr, hIe, ?_⟩
116  intro tk hne
117  cases tk
118  · refine ⟨?_, ?_, ?_, ?_, ?_⟩
119    · change 0 ≤ e.l_desc.max_code.toInt
120      rw [hELD]
121      exact hL0
122    · change e.l_desc.max_code.toInt ≤ 285
123      rw [hELD]
124      omega
125    · change e.l_desc.max_code.toInt.toNat + 1 < e.dyn_ltree.size
126      rw [hELD, hEL]
127      simpa only [scGuard, Array.size_set!] using hLCap
128    · intro i hi
129      change i ≤ e.l_desc.max_code.toInt.toNat at hi
130      rw [hELD] at hi
131      rw [hLfun]
132      rw [guarded, ite_eq_right (by omega)]
133      exact hin.llen i hi
134    · intro k hk hpos
135      rw [hLfun] at hpos
136      change 0 < scanFreqUpTo _ (e.l_desc.max_code.toInt.toNat + 1) k at hpos
137      rw [hELD] at hpos
138      exact hfits k hk (by unfold blScanCount; omega)
139  · refine ⟨?_, ?_, ?_, ?_, ?_⟩
140    · change 0 ≤ e.d_desc.max_code.toInt
141      rw [hEDD]
142      exact hD0
143    · change e.d_desc.max_code.toInt ≤ 285
144      rw [hEDD]
145      omega
146    · change e.d_desc.max_code.toInt.toNat + 1 < e.dyn_dtree.size
147      rw [hEDD, hED]
148      simpa only [scGuard, Array.size_set!] using hDCap
149    · intro i hi
150      change i ≤ e.d_desc.max_code.toInt.toNat at hi
151      rw [hEDD] at hi
152      rw [hDfun]
153      rw [guarded, ite_eq_right (by omega)]
154      exact hin.dlen i hi
155    · intro k hk hpos
156      rw [hDfun] at hpos
157      change 0 < scanFreqUpTo _ (e.d_desc.max_code.toInt.toNat + 1) k at hpos
158      rw [hEDD] at hpos
159      exact hfits k hk (by unfold blScanCount; omega)
160  · exact False.elim (hne rfl)
161
162/-- Actual block initialization, any capacity-bounded list of legal actual
163tallies, and all three actual tree constructors establish both senders'
164data and independent symbol meaning. This is a call-composition result;
165strategy input history, full header emission and overlay room remain separate. -/
166theorem init_tallies_ready_to_send {h : Heap} {id b : Nat} {d : DeflateState} {buf : Array UInt8}
167    (hI : TreesInvAt h id d b buf) (symbols : List (UInt32 × UInt32))
168    (hlegal : ∀ t ∈ symbols, t.2.toNat < 256 ∧ t.1.toNat ≤ 32768)
169    (hroom : 3 * symbols.length ≤ d.sym_end.toNat) :
170    ∃ (mb : Int32) (e : DeflateState) (buf' : Array UInt8),
171      (do init_block (Sp id); tallyCalls (Sp id) symbols
172          blPrepare (Sp id); build_bl_tree (Sp id)) h =
173        .ok (mb, Out.setD (Out.setB h b buf') id e) ∧
174      TreesInvAt (Out.setD (Out.setB h b buf') id e) id e b buf' ∧
175      (∀ tk : TK, tk ≠ .bl → SendTreeData e tk) := by
176  obtain ⟨aL, aD, aB, initialized, hinit, hII, heI, hLs, hDs, hBs,
177    hLzero, hEOB, hDzero, hBzero, hLdl, hDdl, hBdl⟩ := init_block_spec0 hI.base hI.run.to0
178  have hroomI : initialized.sym_next.toNat + 3 * symbols.length ≤ initialized.sym_end.toNat := by
179    rw [heI]
180    change (0 : UInt32).toNat + 3 * symbols.length ≤ d.sym_end.toNat
181    simpa using hroom
182  obtain ⟨counted, buf', htally, hIC, hEC, hBC, hcount, hEnd⟩ :=
183    tallyCalls_preserves hII symbols hlegal hroomI
184  obtain ⟨ready, hprepare, hin, hIR, hBready, hout⟩ := bl_prepare hIC
185  have hzeroR : ∀ k < 19, ready.bl_tree[k]!.fc = 0 := by
186    intro k hk
187    rw [hBready, hBC, heI]
188    exact hBzero k hk
189  obtain ⟨mb, e, hbuild, hIe, hdata⟩ := build_bl_tree_ready_to_send hIR hin hzeroR
190  have hDsame : Zlib.Trees.Proofs.setD = Out.setD := rfl
191  simp only [hDsame, Out.setB_setD, Out.setD_setD] at htally hprepare hbuild hIe
192  refine ⟨mb, e, buf', ?_, hIe, hdata⟩
193  simp only [bind_app, hinit, htally, hprepare]
194  exact hbuild
195
196end Zlib.Trees.Proofs