inftrees.c.read-extent.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.decoder-safe»
2import ZlibF.Spec.InflateTableExtent
3
4namespace Zlib.Inftrees.Proofs
5open C Zlib.Inftrees Zlib.Inftrees.Spec Zlib.Inftrees.Canon Zlib.Inffast.Spec
6set_option autoImplicit false
7
8private theorem prefix_cell (ca : Array Code) {stop i : Nat} (bound : i < stop) :
9    (ca.extract 0 stop)[i]? = ca[i]? := by
10  rw [Array.getElem?_extract]
11  simp only [Nat.sub_zero, Nat.zero_add]
12  by_cases inside : i < ca.size
13  · rw [ite_eq_left (by omega)]
14  · rw [ite_eq_right (by omega), Array.getElem?_eq_none (by omega)]
15
16private theorem prefix_getD (ca : Array Code) {stop i : Nat} (bound : i < stop) :
17    (ca.extract 0 stop).getD i default = ca.getD i default := by
18  simp only [Array.getD_eq_getD_getElem?]
19  rw [prefix_cell ca bound]
20
21private theorem prefix_link_bound {P : Nat → Code → Prop} {L : Code → Prop}
22    [DecidablePred L] {ca : Array Code} {offset root used : Nat}
23    (safe : TableSafe P L (ca.extract 0 (offset + used)) offset root)
24    (rootEnd : 2 ^ root ≤ used) {i : Nat} (index : i < 2 ^ root)
25    (link : L (ca.getD (offset + i) default)) :
26    offset + (ca.getD (offset + i) default).val.toNat +
27      2 ^ (ca.getD (offset + i) default).op.toNat ≤ offset + used := by
28  have entry := safe.2.2 i index
29  rw [prefix_getD ca (by omega), ite_eq_left link] at entry
30  have bound := Array.size_extract_le (as := ca) (i := 0) (j := offset + used)
31  simp only [Nat.sub_zero] at bound
32  exact Nat.le_trans entry.2.2.2.1 bound
33
34/-- Every retained write and root link remains present after discarding
35the array suffix past the actual final descriptor. -/
36theorem complete_content_prefix {e : Env} {ca : Array Code}
37    (code : CompleteCode e.ls e.R e.mx)
38    (written : Written e e.m ca) (links : Links e e.m ca) :
39    Written e e.m (ca.extract 0 (e.oc + (e.D (e.m - 1)).used)) ∧
40      Links e e.m (ca.extract 0 (e.oc + (e.D (e.m - 1)).used)) := by
41  have lastIndex : e.m - 1 < Canon.nz e.ls := by rw [e.nz_eq]; have := e.h_pos; change 0 < e.m at this; omega
42  have rootBound : 2 ^ e.R ≤ (e.D (e.m - 1)).used := by
43    exact desc_used_mono e.ls e.R e.mx (Nat.zero_le (e.m - 1))
44  constructor
45  · intro j index replica bound
46    have listIndex : j < Canon.nz e.ls := by rw [e.nz_eq]; exact index
47    have region := (gAddr_in_region code listIndex bound).2
48    have order := desc_used_mono e.ls e.R e.mx (by omega : j ≤ e.m - 1)
49    have total : gAddr e.ls e.R e.mx j replica < (e.D (e.m - 1)).used :=
50      Nat.lt_of_lt_of_le region order
51    rw [prefix_cell ca (by omega)]
52    exact written j index replica bound
53  · intro a positive le index start
54    have slot : gSlot e.ls e.R a < 2 ^ e.R := Canon.rev_lt _ _
55    rw [prefix_cell ca (by omega)]
56    exact links a positive le index start
57
58theorem complete_table_read_extent {e : Env} {ca : Array Code}
59    (complete : Kc e.f e.n 15 = 2 ^ 15)
60    (written : Written e e.m ca) (links : Links e e.m ca) :
61    TableReadExtent e.c.type ca e.oc e.R (e.D (e.m - 1)).used := by
62  have code := e.completeCode complete
63  obtain ⟨writtenPrefix, linksPrefix⟩ := complete_content_prefix code written links
64  have rootBound : 2 ^ e.R ≤ (e.D (e.m - 1)).used :=
65    desc_used_mono e.ls e.R e.mx (Nat.zero_le (e.m - 1))
66  refine ⟨e.h_R1, Nat.le_trans code.root_le code.mx_le, by omega, ?_⟩
67  intro i index
68  dsimp only
69  intro link
70  rcases link with ⟨type, link⟩ | ⟨type, link⟩
71  · exact prefix_link_bound (complete_len_table_of_content type complete writtenPrefix linksPrefix)
72      rootBound index link
73  · exact prefix_link_bound (complete_dist_table_of_content type complete writtenPrefix linksPrefix)
74      rootBound index link
75
76private theorem two_cells_read_extent {type : UInt32} {ca : Array Code} {offset : Nat}
77    {first second : Code} (one : ca[offset]? = some first) (two : ca[offset + 1]? = some second)
78    (firstLen : type = LENS → ¬ LenLink first) (firstDist : type = DISTS → ¬ DistLink first)
79    (secondLen : ¬ LenLink second) (secondDist : ¬ DistLink second) :
80    TableReadExtent type ca offset 1 2 := by
81  refine ⟨by decide, by decide, by omega, ?_⟩
82  intro i index
83  dsimp only
84  intro link
85  have cases : i = 0 ∨ i = 1 := by change i < 2 at index; omega
86  rcases cases with rfl | rfl
87  · simp only [Nat.add_zero, Array.getD_eq_getD_getElem?, one, Option.getD_some] at link
88    rcases link with ⟨kind, link⟩ | ⟨kind, link⟩
89    · exact False.elim (firstLen kind link)
90    · exact False.elim (firstDist kind link)
91  · simp only [Array.getD_eq_getD_getElem?, two, Option.getD_some] at link
92    rcases link with ⟨kind, link⟩ | ⟨kind, link⟩
93    · exact False.elim (secondLen link)
94    · exact False.elim (secondDist link)
95
96theorem singleton_table_read_extent {e : Env} {ca : Array Code}
97    (single : e.m = 1) (one : e.mx = 1) (written : Written e e.m ca)
98    (invalid : ca[e.oc + 1]? = some ⟨64, 1, 0⟩) :
99    TableReadExtent e.c.type ca e.oc e.R (e.D (e.m - 1)).used := by
100  have root : e.R = 1 := by
101    have := e.h_R1
102    have := e.h_Rmx
103    have one' : mxl e.f e.n = 1 := one
104    omega
105  have len : Canon.L e.ls 0 = 1 := by
106    rw [show Canon.L e.ls 0 = lenAt e.f e.n 0 from L_eq e.f e.n e.h_pos]
107    have last : e.mx = lenAt e.f e.n 0 := by
108      change lenAt e.f e.n (e.m - 1) = lenAt e.f e.n 0
109      rw [single]
110    exact last.symm.trans one
111  have replicas : 0 < gReps e.ls e.R e.mx 0 := Nat.two_pow_pos _
112  have first := written 0 (by omega) 0 replicas
113  rw [gaddr0 e single root replicas, Nat.add_zero] at first
114  have drop : (e.D 0).drop = 0 := rfl
115  have leaf := here_data_leaf_of_drop (e := e) (j := 0) (by omega)
116    (by rw [drop]; omega) (by omega)
117  have invalidLeaf := Cover.invalid_leaf 0 1 (by decide)
118  have firstLen : e.c.type = LENS → ¬ LenLink (e.here 0) := by
119    intro type
120    have firstLeaf : LenLeaf 0 (e.here 0) := by simpa only [drop] using leaf.1 type
121    exact lenLeaf_not_link firstLeaf
122  have firstDist : e.c.type = DISTS → ¬ DistLink (e.here 0) := by
123    intro type
124    have firstLeaf : DistLeaf 0 (e.here 0) := by simpa only [drop] using leaf.2 type
125    exact distLeaf_not_link firstLeaf
126  have extent : (e.D (e.m - 1)).used = 2 := by
127    rw [single]
128    change 2 ^ e.R = 2
129    rw [root]
130  rw [extent, root]
131  exact two_cells_read_extent first invalid firstLen firstDist
132    (lenLeaf_not_link invalidLeaf.1) (distLeaf_not_link invalidLeaf.2)
133
134/-- `int inflate_table(codetype type, unsigned short *lens, unsigned codes,
135code **table, unsigned *bits, unsigned short *work)`.
136The existing returned-extent goal. Decoder safety and every read bound
137are established on the same actual returned heap, including empty and
138accepted single-symbol tables and every constructor error return. -/
139theorem inflate_table_read_extent : Goal.inflate_table_read_extent := by
140  intro h type rl ol codes rc oc bits rw ow pre
141  obtain ⟨result, after, run, frame, _, construction⟩ :=
142    inflate_table_construction h type rl ol codes rc oc bits rw ow pre
143  obtain ⟨safeResult, safeAfter, safeRun, _, decoder⟩ :=
144    inflate_table_decoder_safe h type rl ol codes rc oc bits rw ow pre
145  have same := run.symm.trans safeRun
146  cases same
147  refine ⟨result, after, run, frame, ?_⟩
148  intro success
149  have returned : ∃ used, used ≤ capOf type ∧ result.2.1 = .ref rc (oc + used) := by
150    obtain ⟨_, _, _, _, _, _, _, classify⟩ := frame
151    rcases classify with ⟨_, used, bound, pointer⟩ | ⟨bad, _⟩
152    · exact ⟨used, bound, pointer⟩
153    · rcases bad with bad | bad <;> rw [success] at bad <;> cases bad
154  obtain ⟨safeArray, safeGet, _, _, codeSafe, lenSafe, distSafe⟩ := decoder success
155  rcases construction success with ⟨_, root, endPointer, ca, get, first, second⟩ |
156    ⟨_, e, ca, function, count, width, reference, offset, kind, get, written, links, details⟩
157  · have sameArray := Option.some.inj (safeGet.symm.trans get)
158    subst safeArray
159    obtain ⟨used, bound, pointer⟩ := returned
160    have two : used = 2 := by
161      have equality := Ptr.ref.inj (pointer.symm.trans endPointer)
162      omega
163    have invalidLeaf := Cover.invalid_leaf 0 1 (by decide)
164    have extent : TableReadExtent type ca oc 1 2 :=
165      two_cells_read_extent first second
166        (fun _ => lenLeaf_not_link invalidLeaf.1) (fun _ => distLeaf_not_link invalidLeaf.2)
167        (lenLeaf_not_link invalidLeaf.1) (distLeaf_not_link invalidLeaf.2)
168    exact ⟨ca, 2, get, endPointer, by omega, by rw [root]; exact extent,
169      codeSafe, lenSafe, distSafe⟩
170  · have sameArray := Option.some.inj (safeGet.symm.trans get)
171    subst safeArray
172    obtain ⟨used, pointer, usedValue, invalid⟩ := details success
173    rw [reference, offset] at pointer
174    obtain ⟨otherUsed, bound, otherPointer⟩ := returned
175    have usedEq : used = otherUsed := by
176      have equality := Ptr.ref.inj (pointer.symm.trans otherPointer)
177      omega
178    have extent : TableReadExtent e.c.type ca e.oc e.R (e.D (e.m - 1)).used := by
179      rcases e.h_end with complete | ⟨one, single, _⟩
180      · exact complete_table_read_extent complete written links
181      · exact singleton_table_read_extent single one written (invalid single one)
182    rw [kind, offset, width, ← usedValue] at extent
183    exact ⟨ca, used, get, pointer, by omega, extent, codeSafe, lenSafe, distSafe⟩
184
185/-- Constructor refusals retain the input pointer and root width. Thus
186the successful-extent facts also bound every returned pointer and width
187at a mode call whose requested root width is already bounded. -/
188theorem result_pointer_width_bounds {h after : Heap} {rw : WRef} {rc : CodeRef}
189    {ow oc cap count : Nat} {work : Array UInt16} {codes : Array Code} {bits : UInt32}
190    {result : Int32 × CodePtr × UInt32}
191    (frame : Result h rw rc ow oc cap count work codes (.ref rc oc) bits result after)
192    (root : bits.toNat ≤ 15) (successRoot : result.1 = 0 → result.2.2.toNat ≤ 15) :
193    (∃ used, used ≤ cap ∧ result.2.1 = .ref rc (oc + used)) ∧ result.2.2.toNat ≤ 15 := by
194  obtain ⟨_, _, _, _, _, _, _, classify⟩ := frame
195  rcases classify with ⟨success, used, bound, pointer⟩ | ⟨_, pointer, width⟩
196  · exact ⟨⟨used, bound, pointer⟩, successRoot success⟩
197  · exact ⟨⟨0, Nat.zero_le _, by simpa only [Nat.add_zero] using pointer⟩, by rw [width]; exact root⟩
198
199end Zlib.Inftrees.Proofs