inftrees.c.decode.stability-rejection.lean

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

1import ZlibF.Spec.InflateDecodeTableStability
2import ZlibF.Proof.«inftrees.c.decode.frame»
3import ZlibF.Proof.Format.Huffman
4
5/-!
6# Stable queries and early invalid-code rejection
7
8The prefix frame transports the exact query, rather than only its bounds.
9A hypothetical valid decode after a rejected fitted query is extended to
10full width, where classification contradicts stability of the rejection.
11-/
12
13namespace Zlib.Inftrees.Proofs
14open C Zlib.Inftrees.Spec
15open Zlib.Inftrees.Spec.DecodeSemantics Zlib.Inftrees.Spec.DecodeSoundness
16open Zlib.Inftrees.Spec.DecodeTableStability
17
18/-- Preserving every potentially read cell preserves stability under all
19future input suffixes, including the rejected leaves. -/
20theorem query_stability_of_prefix : Goal.query_stability_of_prefix := by
21  intro type before after offset root used ht hext stable cells
22  intro inp entry consumed query fit more
23  have frame := decode_table_read_preserved type before after offset root used ht hext cells
24  rw [frame] at query
25  rw [frame]
26  exact stable inp entry consumed query fit more
27
28/-- A fitted rejected entry cannot become a valid independent symbol by
29adding input. The hypothetical decode extends to a full-width query, where
30the invariant's classification and the unchanged entry contradict it. -/
31theorem short_rejected_leaf_stays_invalid : Goal.short_rejected_leaf_stays_invalid := by
32  intro type ca offset root used lens inv stable inp entry consumed query fit rejected more
33  rintro ⟨symbol, rest, decoded, valid⟩
34  let padding : List Bool := List.replicate (15 - (inp ++ more).length) false
35  let full : List Bool := (inp ++ more) ++ padding
36  have long : 15 ≤ full.length := by simp [full, padding]; omega
37  have fullPadded : DecodeShort.padded full = full := by
38    simp [DecodeShort.padded, Nat.sub_eq_zero_of_le long]
39  have extended := ZlibF.Spec.Proofs.ext_acceptable inv.acceptable
40    (inp ++ more) symbol rest padding decoded
41  have fullQuery : tableRead type ca offset root full = some (entry, consumed) := by
42    have stableQuery := stable inp entry consumed query fit (more ++ padding)
43    have reassoc : inp ++ (more ++ padding) = full := by
44      simp only [full, List.append_assoc]
45    rw [reassoc, fullPadded] at stableQuery
46    exact stableQuery
47  obtain ⟨entry', consumed', classifiedQuery, classification⟩ := inv.classify full long
48  rw [fullQuery] at classifiedQuery
49  have same := Option.some.inj classifiedQuery
50  obtain ⟨sameEntry, sameConsumed⟩ := Prod.mk.inj same
51  subst entry' consumed'
52  apply rejected
53  exact classification.mpr ⟨symbol, rest ++ padding, extended, valid⟩
54
55end Zlib.Inftrees.Proofs