inftrees.c.content.codes.lean

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

1import ZlibF.Proof.«inftrees.c.content»
2import ZlibF.Spec.InflateTableSafety
3
4/-!
5# inftrees.c: the constructed code-length table is safe to decode
6
7The code-length alphabet uses only a root table. Complete root coverage and
8the actual retained writes establish the lookup facts. The accepted empty
9alphabet has the two explicit invalid cells written by the real constructor.
10-/
11
12namespace Zlib.Inftrees.Proofs
13open C Zlib.Inftrees Zlib.Inftrees.Spec Zlib.Inftrees.Canon
14set_option autoImplicit false
15
16private theorem codes_here {e : Env} (type : e.c.type = CODES) {j : Nat}
17    (index : j < e.m) :
18    1 ≤ (e.here j).bits.toNat ∧ (e.here j).bits.toNat ≤ e.R ∧
19      (e.here j).op = 0 ∧ (e.here j).val.toNat < 19 := by
20  obtain ⟨maxBound, root, countBound, matchValue⟩ := e.h_codes type
21  have symbol := ws_getD_lt index
22  have count : e.n ≤ 19 := countBound
23  let w := (wsAux e.f e.n 15).getD j 0
24  have word : (UInt16.ofNat w).toNat = w := by
25    rw [UInt16.toNat_ofNat']
26    exact Nat.mod_eq_of_lt (by change w < e.n at symbol; omega)
27  have widened : (UInt16.ofNat w).toUInt32.toNat = w := by
28    rw [UInt16.toNat_toUInt32, word]
29  have test : (UInt16.ofNat w).toUInt32 + 1 < e.c.match_ := by
30    rw [matchValue]
31    apply UInt32.lt_iff_toNat_lt.mpr
32    rw [u32_succ (by rw [widened]; change w < e.n at symbol; omega), widened]
33    change w + 1 < 20
34    change w < e.n at symbol
35    omega
36  have jList : j < Canon.nz e.ls := by
37    change j < Canon.nz (lensOf e.f e.n)
38    rw [Zlib.Inftrees.Proofs.nz_eq]
39    exact index
40  have lengthBounds := Canon.L_interval e.ls jList
41  have lengthMax : Canon.L e.ls j ≤ e.R := by
42    change Canon.L (lensOf e.f e.n) j ≤ e.R
43    rw [L_eq e.f e.n index, root]
44    have actualIndex : j < Tc e.f e.n 15 := index
45    exact lenAt_mono (f := e.f) (n := e.n) (by omega)
46      (by have := e.h_pos; omega)
47  have drop : (e.D j).drop = 0 := by
48    change (Canon.desc e.ls e.R e.mx j).drop = 0
49    rw [Canon.desc_short e.ls jList lengthMax]
50    rfl
51  have bits : ((Canon.L e.ls j).toUInt8).toNat = Canon.L e.ls j := by
52    rw [UInt8.toNat_ofNat']
53    exact Nat.mod_eq_of_lt (by omega)
54  have here : e.here j = ⟨0, (Canon.L e.ls j).toUInt8, UInt16.ofNat w⟩ := by
55    unfold Env.here
56    change hereC e.c (UInt16.ofNat w) (Canon.L e.ls j - (e.D j).drop).toUInt8 = _
57    rw [drop, Nat.sub_zero]
58    unfold hereC
59    rw [ite_eq_left test]
60  rw [here]
61  change 1 ≤ ((Canon.L e.ls j).toUInt8).toNat ∧
62    ((Canon.L e.ls j).toUInt8).toNat ≤ e.R ∧ (0 : UInt8) = 0 ∧ (UInt16.ofNat w).toNat < 19
63  rw [bits, word]
64  change w < e.n at symbol
65  exact ⟨lengthBounds.1, lengthMax, rfl, by omega⟩
66
67theorem codes_table_of_written {e : Env} {ca : Array Code}
68    (type : e.c.type = CODES) (written : Written e e.m ca) :
69    CodeLengthTableSafe ca e.oc e.R := by
70  obtain ⟨maxBound, root, _, _⟩ := e.h_codes type
71  have complete : Kc e.f e.n 15 = 2 ^ 15 := by
72    rcases e.h_end with full | ⟨_, _, notCodes⟩
73    · exact full
74    · exact False.elim (notCodes type)
75  have entry : ∀ cell, cell < 2 ^ e.R →
76      ∃ j, j < e.m ∧ ca[e.oc + cell]? = some (e.here j) := by
77    intro cell inside
78    have cover := Cover.root_cover_complete_fn e.h_fits complete
79      (by rw [root]; exact Nat.le_trans maxBound (by decide)) inside
80    rcases cover with ⟨j, short, _, _⟩ | ⟨⟨j, long⟩, _⟩
81    · have shortList := (Cover.shortAt_iff e.f e.n e.R cell j).mpr short
82      obtain ⟨replica, bounded, address⟩ := short_root_replica (mx := e.mx)
83        shortList.1 shortList.2.1 inside shortList.2.2
84      refine ⟨j, short.1, ?_⟩
85      have cellValue := written j short.1 replica bounded
86      change gAddr e.ls e.R e.mx j replica = cell at address
87      rwa [address] at cellValue
88    · have upper : lenAt e.f e.n j ≤ e.R := by
89        rw [root]
90        have index := long.1
91        exact lenAt_mono (f := e.f) (n := e.n) (by omega)
92          (by have := e.h_pos; omega)
93      exact False.elim (by have := long.2.1; omega)
94  have limit : e.oc + 2 ^ e.R ≤ ca.size := by
95    have positive := Nat.two_pow_pos e.R
96    obtain ⟨j, _, last⟩ := entry (2 ^ e.R - 1) (by omega)
97    have inArray : e.oc + (2 ^ e.R - 1) < ca.size := by
98      by_cases bound : e.oc + (2 ^ e.R - 1) < ca.size
99      · exact bound
100      · rw [Array.getElem?_eq_none (by omega)] at last
101        contradiction
102    omega
103  refine ⟨e.h_R1, by omega, limit, ?_⟩
104  intro cell inside
105  obtain ⟨j, index, get⟩ := entry cell inside
106  have here := codes_here type index
107  have value : ca.getD (e.oc + cell) default = e.here j := by
108    simp only [Array.getD_eq_getD_getElem?, get, Option.getD_some]
109  dsimp only
110  rw [value]
111  exact ⟨here.1, here.2.1, Or.inl here.2.2⟩
112
113/-- `int inflate_table(codetype type, unsigned short *lens, unsigned codes,
114code **table, unsigned *bits, unsigned short *work)` for CODES.
115On every existing constructor precondition, the actual call returns with its
116original safety frame. A successful return establishes the code-length table
117predicate used at CODELENS. No table predicate or callee contract is assumed. -/
118theorem inflate_table_codes_decoder_safe
119    {h : Heap} {rl rw : WRef} {ol ow oc : Nat} {codes bits : UInt32} {rc : CodeRef}
120    (pre : CallPre h CODES rl ol codes rc oc bits rw ow) :
121    ∃ result after,
122      C.run (inflate_table CODES (.ref rl ol) codes (.ref rc oc) bits (.ref rw ow)) h =
123        .ok (result, after) ∧
124      Result h rw rc ow oc (capOf CODES) codes.toNat pre.wa pre.ca (.ref rc oc) bits result after ∧
125      (result.1 = 0 → ∃ ca : Array Code, Space.get after rc = some ca ∧
126        CodeLengthTableSafe ca oc result.2.2.toNat) := by
127  obtain ⟨result, after, run, frame, _, content⟩ :=
128    inflate_table_content h CODES rl ol codes rc oc bits rw ow pre
129  refine ⟨result, after, run, frame, ?_⟩
130  intro success
131  rcases content success with ⟨_, root, _, ca, get, first, second⟩ |
132    ⟨_, e, ca, _, _, width, reference, offset, type, get, written, _⟩
133  · refine ⟨ca, get, ?_⟩
134    rw [root]
135    have bound : oc + 1 < ca.size := by
136      by_cases inside : oc + 1 < ca.size
137      · exact inside
138      · rw [Array.getElem?_eq_none (by omega)] at second
139        contradiction
140    refine ⟨by decide, by decide, by change oc + 2 ≤ ca.size; omega, ?_⟩
141    intro cell inside
142    have value : ca.getD (oc + cell) default = ⟨64, 1, 0⟩ := by
143      have cases : cell = 0 ∨ cell = 1 := by change cell < 2 at inside; omega
144      rcases cases with rfl | rfl
145      · simpa only [Nat.add_zero, Array.getD_eq_getD_getElem?, first, Option.getD_some]
146      · simp only [Array.getD_eq_getD_getElem?, second, Option.getD_some]
147    dsimp only
148    rw [value]
149    exact ⟨by decide, by decide, Or.inr rfl⟩
150  · refine ⟨ca, get, ?_⟩
151    rw [← offset, ← width]
152    exact codes_table_of_written type written
153
154end Zlib.Inftrees.Proofs