inftrees.c.decoder-safe.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.data»
2import ZlibF.Proof.«inftrees.c.content.result»
3
4namespace Zlib.Inftrees.Proofs
5open C Zlib.Inftrees Zlib.Inftrees.Spec Zlib.Inftrees.Canon Zlib.Inffast.Spec
6set_option autoImplicit false
7
8theorem lenLeaf_not_link {drop : Nat} {entry : Code} (leaf : LenLeaf drop entry) :
9    ¬ LenLink entry := by
10  rintro ⟨nonzero, bit16, bit64⟩
11  rcases leaf.2 with literal | length | invalid
12  · exact nonzero literal
13  · exact length.1 bit16
14  · exact invalid.2 bit64
15
16theorem distLeaf_not_link {drop : Nat} {entry : Code} (leaf : DistLeaf drop entry) :
17    ¬ DistLink entry := by
18  rintro ⟨bit16, bit64⟩
19  rcases leaf.2 with distance | invalid
20  · exact distance.1 bit16
21  · exact invalid.2 bit64
22
23private theorem two_cell_table {P : Nat → Code → Prop} {L : Code → Prop}
24    [DecidablePred L] {ca : Array Code} {offset : Nat} {first second : Code}
25    (one : ca[offset]? = some first) (two : ca[offset + 1]? = some second)
26    (firstLeaf : P 0 first) (firstNotLink : ¬ L first)
27    (secondLeaf : P 0 second) (secondNotLink : ¬ L second) :
28    TableSafe P L ca offset 1 := by
29  have bound : offset + 1 < ca.size := by
30    by_cases inside : offset + 1 < ca.size
31    · exact inside
32    · rw [Array.getElem?_eq_none (by omega)] at two
33      contradiction
34  refine ⟨by decide, by change offset + 2 ≤ ca.size; omega, ?_⟩
35  intro cell inside
36  have cases : cell = 0 ∨ cell = 1 := by change cell < 2 at inside; omega
37  rcases cases with rfl | rfl
38  · simp only [Nat.add_zero, Array.getD_eq_getD_getElem?, one, Option.getD_some,
39      firstNotLink, ite_false]
40    exact firstLeaf
41  · simp only [Array.getD_eq_getD_getElem?, two, Option.getD_some, secondNotLink, ite_false]
42    exact secondLeaf
43
44theorem invalid_two_cells {ca : Array Code} {offset : Nat}
45    (one : ca[offset]? = some ⟨64, 1, 0⟩) (two : ca[offset + 1]? = some ⟨64, 1, 0⟩) :
46    LenTableSafe ca offset 1 ∧ DistTableSafe ca offset 1 := by
47  have leaves := Cover.invalid_leaf 0 1 (by decide)
48  exact ⟨two_cell_table one two leaves.1 (lenLeaf_not_link leaves.1)
49      leaves.1 (lenLeaf_not_link leaves.1),
50    two_cell_table one two leaves.2 (distLeaf_not_link leaves.2)
51      leaves.2 (distLeaf_not_link leaves.2)⟩
52
53theorem singleton_data_tables {e : Env} {ca : Array Code}
54    (single : e.m = 1) (one : e.mx = 1) (written : Written e e.m ca)
55    (invalid : ca[e.oc + 1]? = some ⟨64, 1, 0⟩) :
56    (e.c.type = LENS → LenTableSafe ca e.oc e.R) ∧
57    (e.c.type = DISTS → DistTableSafe ca e.oc e.R) := by
58  have root : e.R = 1 := by
59    have := e.h_R1
60    have := e.h_Rmx
61    have one' : mxl e.f e.n = 1 := one
62    omega
63  have len : Canon.L e.ls 0 = 1 := by
64    rw [show Canon.L e.ls 0 = lenAt e.f e.n 0 from L_eq e.f e.n e.h_pos]
65    have last : e.mx = lenAt e.f e.n 0 := by
66      change lenAt e.f e.n (e.m - 1) = lenAt e.f e.n 0
67      rw [single]
68    exact last.symm.trans one
69  have drop : (e.D 0).drop = 0 := rfl
70  have replicas : 0 < gReps e.ls e.R e.mx 0 := Nat.two_pow_pos _
71  have first := written 0 (by omega) 0 replicas
72  rw [gaddr0 e single root replicas, Nat.add_zero] at first
73  have leaf := here_data_leaf_of_drop (e := e) (j := 0) (by omega)
74    (by rw [drop]; omega) (by omega)
75  have invalidLeaf := Cover.invalid_leaf 0 1 (by decide)
76  constructor
77  · intro type
78    have firstLeaf : LenLeaf 0 (e.here 0) := by simpa only [drop] using leaf.1 type
79    rw [root]
80    exact two_cell_table first invalid firstLeaf (lenLeaf_not_link firstLeaf)
81      invalidLeaf.1 (lenLeaf_not_link invalidLeaf.1)
82  · intro type
83    have firstLeaf : DistLeaf 0 (e.here 0) := by simpa only [drop] using leaf.2 type
84    rw [root]
85    exact two_cell_table first invalid firstLeaf (distLeaf_not_link firstLeaf)
86      invalidLeaf.2 (distLeaf_not_link invalidLeaf.2)
87
88/-- `int inflate_table(codetype type, unsigned short *lens, unsigned codes,
89code **table, unsigned *bits, unsigned short *work)`.
90The existing decoder-safety goal, including rejected alphabets, capacity
91errors, empty tables and incomplete single-symbol tables. Every table
92property comes from actual writes on the same execution. -/
93theorem inflate_table_decoder_safe : Goal.inflate_table_decoder_safe := by
94  intro h type rl ol codes rc oc bits rw ow pre
95  by_cases codeLength : type = CODES
96  · subst type
97    obtain ⟨result, after, run, frame, safe⟩ := inflate_table_codes_decoder_safe pre
98    refine ⟨result, after, run, frame, ?_⟩
99    intro success
100    obtain ⟨ca, get, table⟩ := safe success
101    refine ⟨ca, get, table.1, by have := table.2.1; omega, fun _ => table, ?_, ?_⟩
102    · intro impossible; cases impossible
103    · intro impossible; cases impossible
104  · obtain ⟨result, after, run, frame, _, construction⟩ :=
105      inflate_table_construction h type rl ol codes rc oc bits rw ow pre
106    refine ⟨result, after, run, frame, ?_⟩
107    intro success
108    rcases construction success with ⟨_, root, _, ca, get, first, second⟩ |
109      ⟨_, e, ca, function, count, width, reference, offset, kind, get, written, links, details⟩
110    · have tables := invalid_two_cells first second
111      refine ⟨ca, get, ?_, ?_, ?_, ?_, ?_⟩
112      · rw [root]; decide
113      · rw [root]; decide
114      · intro impossible; exact False.elim (codeLength impossible)
115      · intro _; rw [root]; exact tables.1
116      · intro _; rw [root]; exact tables.2
117    · have rootLo : 1 ≤ result.2.2.toNat := by rw [← width]; exact e.h_R1
118      have rootHi : result.2.2.toNat ≤ 15 := by
119        rw [← width]
120        have bound := lenAt_bounds (f := e.f) (n := e.n)
121          (show Tc e.f e.n 15 - 1 < Tc e.f e.n 15 by have := e.h_pos; omega)
122        have := e.h_Rmx
123        exact Nat.le_trans this bound.2
124      refine ⟨ca, get, rootLo, rootHi, ?_, ?_, ?_⟩
125      · intro impossible; exact False.elim (codeLength impossible)
126      all_goals
127        intro typeEq
128        rw [← offset, ← width]
129        rcases e.h_end with complete | ⟨one, single, _⟩
130        · first
131          | exact complete_len_table_of_content (kind.trans typeEq) complete written links
132          | exact complete_dist_table_of_content (kind.trans typeEq) complete written links
133        · obtain ⟨_, _, _, invalid⟩ := details success
134          have tables := singleton_data_tables single one written (invalid single one)
135          first
136          | exact tables.1 (kind.trans typeEq)
137          | exact tables.2 (kind.trans typeEq)
138
139end Zlib.Inftrees.Proofs