InflateCausality.lean

本页保留 Lean 源码及行号。点击行号可定位语句，点击 import 中的模块名可查看依赖。

1import ZlibF.Spec.Api.Inflate
2import ZlibF.Proof.Format.Api
3import ZlibF.Math.InflatePrefixes
4
5/-!
6# Causal output evidence
7
8These proofs concern the heap-free API model. They establish the relationship between
9bit-prefix evidence and byte-prefix determinacy, and a concrete delayed-error regression.
10They do not assert refinement of the translated implementation.
11-/
12
13namespace ZlibF.Spec.Api.Proofs
14open ZlibF.Spec
15
16set_option maxRecDepth 100000
17
18/-- The universal part of causal evidence entails the original byte-based determinacy. -/
19theorem output_evidence_determined {w : Wrap} {b : Nat} {allowed : List UInt8 → Prop}
20    {input output : List UInt8} (h : Layer.OutputEvidence w b allowed input output) :
21    ∀ d, allowed d → Layer.Determined w b d input output := by
22  obtain ⟨pfx, hp, _, hu⟩ := h
23  intro d ha stream decoded hc hd
24  exact hu d stream decoded ha (bit_compatible_of_byte_compatible hp hc) hd
25
26/-- An empty output has causal evidence when an allowed valid stream exists. -/
27theorem output_evidence_nil {w : Wrap} {b : Nat} {allowed : List UInt8 → Prop}
28    {dictionary stream decoded : List UInt8} (ha : allowed dictionary)
29    (hd : Layer.Decodes w b dictionary stream decoded) (input : List UInt8) :
30    Layer.OutputEvidence w b allowed input [] := by
31  refine ⟨[], List.nil_prefix, ⟨dictionary, stream, decoded, ha, Or.inl List.nil_prefix, hd⟩, ?_⟩
32  intro _ _ _ _ _ _
33  exact List.nil_prefix
34
35/-- A complete stream provides causal evidence when the dictionary is fixed. -/
36theorem output_evidence_of_decodes {w : Wrap} {b : Nat} {allowed : List UInt8 → Prop}
37    {dictionary input output : List UInt8} (ha : allowed dictionary)
38    (hfixed : ∀ d, allowed d → d = dictionary)
39    (hd : Layer.Decodes w b dictionary input output) :
40    Layer.OutputEvidence w b allowed input output := by
41  refine ⟨bytesToBits input, List.prefix_refl _,
42    ⟨dictionary, input, output, ha, Or.inl (List.prefix_refl _), hd⟩, ?_⟩
43  intro d stream decoded had hc hs
44  obtain rfl := hfixed d had
45  rcases hc with hc | hc
46  · obtain ⟨tail, heq⟩ := bytesToBits_prefix_reflect hc
47    have hx := Layer.ext hd (by simpa only [← heq] using hs)
48    simpa only [← hx.2] using List.prefix_refl output
49  · obtain ⟨tail, heq⟩ := bytesToBits_prefix_reflect hc
50    have hx := Layer.ext hs (by simpa only [← heq] using hd)
51    simpa only [hx.2] using List.prefix_refl output
52
53private theorem copyBack_prefix (dict : List UInt8) (dist n : Nat) (h : List UInt8) :
54    h <+: copyBack dict dist n h := by
55  induction n generalizing h with
56  | zero => exact List.prefix_refl _
57  | succ n ih => exact (List.prefix_append _ _).trans (ih _)
58
59private theorem symbols_output_prefix {L D : List Nat} {dict h : List UInt8}
60    {inp rest : List Bool} {out : List UInt8} (hs : Symbols L D dict h inp rest out) :
61    h <+: out := by
62  induction hs with
63  | eob => exact List.prefix_refl _
64  | lit _ _ _ ih => exact (List.prefix_append _ _).trans ih
65  | copy _ _ _ _ _ _ _ _ _ ih => exact (copyBack_prefix _ _ _ _).trans ih
66
67private theorem literal65 (tail : List Bool) :
68    decodeSym fixedLitLens
69      ([false, true, true, true, false, false, false, true] ++ tail) = some (65, tail) := by
70  simpa only [List.nil_append] using
71    ZlibF.Spec.Proofs.ext_fixedLit _ _ _ tail
72      (by decide +kernel : decodeSym fixedLitLens
73        [false, true, true, true, false, false, false, true] = some (65, []))
74
75private theorem deferred_valid_completion :
76    Layer.Decodes .raw 15 [] [115, 4, 0] [65] :=
77  ⟨_, .last rfl rfl (.fixed (.lit (s := 65) rfl (by decide) (.eob rfl))), by decide⟩
78
79private theorem deferred_bits_force_output {stream decoded : List UInt8}
80    (hp : [true, true, false, false, true, true, true, false, false, false, true] <+:
81      bytesToBits stream) (hd : Deflate.Decodes [] stream decoded) : [65] <+: decoded := by
82  obtain ⟨tail, heq⟩ := hp
83  obtain ⟨rest, hb, _⟩ := hd
84  rw [← heq] at hb
85  cases hb with
86  | more h1 =>
87    change some (1, _) = some (0, _) at h1
88    simp only [Option.some.injEq, Prod.mk.injEq] at h1
89    omega
90  | last h1 h2 hbody =>
91    change some (1, _) = some (1, _) at h1
92    simp only [Option.some.injEq, Prod.mk.injEq] at h1
93    obtain ⟨_, rfl⟩ := h1
94    change some (1, _) = some (_, _) at h2
95    simp only [Option.some.injEq, Prod.mk.injEq] at h2
96    obtain ⟨rfl, rfl⟩ := h2
97    cases hbody with
98    | fixed hs =>
99      change Symbols fixedLitLens fixedDistLens [] []
100        ([false, true, true, true, false, false, false, true] ++ tail) rest decoded at hs
101      cases hs with
102      | eob h => rw [literal65] at h; simp at h
103      | copy h hlow =>
104        rw [literal65] at h
105        simp only [Option.some.injEq, Prod.mk.injEq] at h
106        obtain ⟨rfl, _⟩ := h
107        omega
108      | lit h _ hs =>
109        rw [literal65] at h
110        simp only [Option.some.injEq, Prod.mk.injEq] at h
111        obtain ⟨rfl, rfl⟩ := h
112        exact symbols_output_prefix hs
113
114/-- The eleven checked bits end after literal 65; the invalid distance is still lookahead. -/
115theorem deferred_distance_output_evidence :
116    (InflState.fresh .raw 15).Consistent [115, 4, 66] [65] := by
117  refine ⟨[true, true, false, false, true, true, true, false, false, false, true],
118    by decide +kernel, ⟨[], [115, 4, 0], [65], Or.inr rfl, Or.inl (by decide +kernel),
119      deferred_valid_completion⟩, ?_⟩
120  intro dictionary stream decoded hdictionary hcompatible hdecode
121  have hdict : dictionary = [] := by simpa [InflState.PermitsDictionary, InflState.fresh] using hdictionary
122  subst dictionary
123  change Layer.Decodes .raw 15 [] stream decoded at hdecode
124  rcases hcompatible with hcompatible | hcompatible
125  · exact deferred_bits_force_output hcompatible hdecode
126  · have hp : bytesToBits stream <+: bytesToBits [115, 4, 0] :=
127      hcompatible.trans (by decide +kernel)
128    obtain ⟨tail, heq⟩ := bytesToBits_prefix_reflect hp
129    have hx := Layer.ext hdecode (by simpa only [← heq] using deferred_valid_completion)
130    simpa only [hx.2] using List.prefix_refl [65]
131
132private theorem length257 (tail : List Bool) :
133    decodeSym fixedLitLens
134      ([false, false, false, false, false, false, true] ++ tail) = some (257, tail) := by
135  simpa only [List.nil_append] using
136    ZlibF.Spec.Proofs.ext_fixedLit _ _ _ tail
137      (by decide +kernel : decodeSym fixedLitLens
138        [false, false, false, false, false, false, true] = some (257, []))
139
140private theorem distance1 (tail : List Bool) :
141    decodeSym fixedDistLens ([false, false, false, false, true] ++ tail) = some (1, tail) := by
142  simpa only [List.nil_append] using
143    ZlibF.Spec.Proofs.ext_fixedDist _ _ _ tail
144      (by decide +kernel : decodeSym fixedDistLens [false, false, false, false, true] = some (1, []))
145
146private theorem deferred_invalid_prefix (tail out : List UInt8) :
147    ¬ Deflate.Decodes [] ([115, 4, 66] ++ tail) out := by
148  rintro ⟨rest, hb, _⟩
149  cases hb with
150  | more h1 =>
151    change some (1, _) = some (0, _) at h1
152    simp only [Option.some.injEq, Prod.mk.injEq] at h1
153    omega
154  | last h1 h2 hbody =>
155    change some (1, _) = some (1, _) at h1
156    simp only [Option.some.injEq, Prod.mk.injEq] at h1
157    obtain ⟨_, rfl⟩ := h1
158    change some (1, _) = some (_, _) at h2
159    simp only [Option.some.injEq, Prod.mk.injEq] at h2
160    obtain ⟨rfl, rfl⟩ := h2
161    cases hbody with
162    | fixed hs =>
163      change Symbols fixedLitLens fixedDistLens [] []
164        ([false, true, true, true, false, false, false, true] ++
165          [false, false, false, false, false, false, true,
166           false, false, false, false, true, false] ++ bytesToBits tail) rest out at hs
167      cases hs with
168      | eob h => rw [List.append_assoc, literal65] at h; simp at h
169      | copy h hlow =>
170        rw [List.append_assoc, literal65] at h
171        simp only [Option.some.injEq, Prod.mk.injEq] at h
172        obtain ⟨rfl, _⟩ := h
173        omega
174      | lit h _ hs =>
175        rw [List.append_assoc, literal65] at h
176        simp only [Option.some.injEq, Prod.mk.injEq] at h
177        obtain ⟨rfl, rfl⟩ := h
178        change Symbols fixedLitLens fixedDistLens [] [65]
179          ([false, false, false, false, false, false, true] ++
180            [false, false, false, false, true, false] ++ bytesToBits tail) rest out at hs
181        cases hs with
182        | eob h => rw [List.append_assoc, length257] at h; simp at h
183        | lit h hlt =>
184          rw [List.append_assoc, length257] at h
185          simp only [Option.some.injEq, Prod.mk.injEq] at h
186          obtain ⟨rfl, _⟩ := h
187          omega
188        | copy h _ _ hl hd _ hx hbound =>
189          rw [List.append_assoc, length257] at h
190          simp only [Option.some.injEq, Prod.mk.injEq] at h
191          obtain ⟨rfl, rfl⟩ := h
192          change some (0, _) = some (_, _) at hl
193          simp only [Option.some.injEq, Prod.mk.injEq] at hl
194          obtain ⟨rfl, rfl⟩ := hl
195          change decodeSym fixedDistLens
196            ([false, false, false, false, true] ++ (false :: bytesToBits tail)) = some (_, _) at hd
197          rw [distance1] at hd
198          simp only [Option.some.injEq, Prod.mk.injEq] at hd
199          obtain ⟨rfl, rfl⟩ := hd
200          change some (0, _) = some (_, _) at hx
201          simp only [Option.some.injEq, Prod.mk.injEq] at hx
202          obtain ⟨rfl, _⟩ := hx
203          exact absurd hbound (by decide)
204
205
206private theorem deferred_no_complete_prefix (n : Nat) (output : List UInt8) :
207    ¬ Layer.Decodes .raw 15 [] ([115, 4, 66, 0].take n) output := by
208  intro hd
209  by_cases hn : 3 ≤ n
210  · have heq : ([115, 4, 66, 0] : List UInt8).take n = [115, 4, 66] ++ [0].take (n - 3) := by
211      change (([115, 4, 66] : List UInt8) ++ [0]).take n = _
212      rw [List.take_append, List.take_of_length_le hn]
213      rfl
214    rw [heq] at hd
215    exact deferred_invalid_prefix _ _ hd
216  · have hp : ([115, 4, 66, 0] : List UInt8).take n <+: [115, 4, 0] := by
217      have hc : n = 0 ∨ n = 1 ∨ n = 2 := by omega
218      rcases hc with rfl | rfl | rfl <;> decide
219    obtain ⟨tail, heq⟩ := hp
220    have hx := Layer.ext hd (by simpa only [← heq] using deferred_valid_completion)
221    have hlen := congrArg List.length heq
222    rw [hx.1] at hlen
223    simp only [List.length_append, List.length_nil, Nat.add_zero, List.length_take,
224      List.length_cons] at hlen
225    omega
226
227/-- The former whole-lookahead condition rejects the actual first call. This proof uses
228the old predicate, which remains available separately from the corrected causal relation. -/
229theorem inflate_deferred_distance_rejects_legacy_consistency :
230    ¬ Layer.Consistent .raw 15 [] [115, 4, 66] [65] := by
231  intro h
232  rcases h with h | ⟨tail, output, n, hn, hd, _⟩
233  · have bad := h.1
234    simp [hdrLag] at bad
235  · have heq : (([115, 4, 66] : List UInt8) ++ tail).take n =
236        [115, 4, 66] ++ tail.take (n - 3) := by
237      rw [List.take_append, List.take_of_length_le hn]
238      rfl
239    change Deflate.Decodes [] ((([115, 4, 66] : List UInt8) ++ tail).take n) output at hd
240    rw [heq] at hd
241    exact deferred_invalid_prefix _ _ hd
242
243/-- The model admits the real first call before the invalid distance is checked. -/
244theorem inflate_deferred_distance : Goal.inflate_deferred_distance := by
245  refine ⟨{ (InflState.fresh .raw 15) with
246    seen := [115, 4, 66]
247    out := [65]
248    totalIn := 3
249    totalOut := 1 }, ?_⟩
250  unfold InflRunOk
251  and_intros
252  all_goals first
253    | rfl
254    | decide
255    | (intro h; exact absurd h (by decide))
256    | (intro _ h; exact absurd h (by decide))
257    | (intro _; exact ⟨Or.inl (by decide), by decide, rfl⟩)
258    | (intro _ _; exact deferred_distance_output_evidence)
259    | (intro _; exact Or.inl rfl)
260    | (intro _ _ _ _ ⟨n, output, _, _, hd, _, _⟩;
261       exact False.elim (deferred_no_complete_prefix n output hd))
262    | (intro _ _ _ _ h; exact absurd h (by decide))
263    | (intro _ _ h; exact absurd h (by decide))
264    | (intro _ h; exact absurd h (by decide))
265    | (intro _ _; exact output_evidence_determined deferred_distance_output_evidence)
266    | (intro req h; cases h)
267
268end ZlibF.Spec.Api.Proofs