InflateDecodeTableStability.lean

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

1import ZlibF.Spec.InflateDecodeTableInvariant
2
3/-!
4# A fitted query is independent of unread input
5
6Both accepted and rejected entries must be stable under later input. The
7fit check alone is not enough for an arbitrary range-safe table: its cells
8must have the replication pattern established by the actual constructor.
9This obligation is separate from accepted-symbol soundness.
10-/
11
12namespace Zlib.Inftrees.Spec.DecodeTableStability
13open C Zlib.Inftrees Zlib.Inftrees.Proofs
14open Zlib.Inftrees.Spec.DecodeSemantics Zlib.Inftrees.Spec.DecodeSoundness
15
16/-- Once the returned code length fits the available prefix, every future
17suffix selects the very same entry and consumed length. Zero padding is
18only a mathematical query convention, never input that may be consumed. -/
19def StableQuery (type : UInt32) (ca : Array Code) (offset root : Nat) : Prop :=
20  ∀ (inp : List Bool) (entry : Code) (consumed : Nat),
21    tableRead type ca offset root (DecodeShort.padded inp) = some (entry, consumed) →
22    consumed ≤ inp.length →
23    ∀ more : List Bool,
24      tableRead type ca offset root (DecodeShort.padded (inp ++ more)) =
25        some (entry, consumed)
26
27/-- The actual accepted constructor supplies suffix stability, including
28invalid singleton padding, empty tables and reserved symbols. This says
29nothing about the validity of the compressed input. -/
30def Goal.constructor_establishes_query_stability : Prop :=
31  ∀ (h : Heap) (type : UInt32) (rl : WRef) (ol : Nat) (codes : UInt32)
32    (rc : CodeRef) (oc : Nat) (bits : UInt32) (rw : WRef) (ow : Nat)
33    (pre : CallPre h type rl ol codes rc oc bits rw ow),
34    (type = LENS ∨ type = DISTS) →
35    ∃ (r : Int32 × CodePtr × UInt32) (after : Heap),
36      C.run (inflate_table type (.ref rl ol) codes (.ref rc oc) bits (.ref rw ow)) h =
37        .ok (r, after) ∧
38      (r.1 = 0 → ∀ ca : Array Code, Space.get after rc = some ca →
39        StableQuery type ca oc r.2.2.toNat)
40
41/-- An actual cell frame also transports suffix stability. The extent is
42supplied by the first constructor, and the equality by the following one. -/
43def Goal.query_stability_of_prefix : Prop :=
44  ∀ (type : UInt32) (before after : Array Code) (offset root used : Nat),
45    (type = LENS ∨ type = DISTS) →
46    TableReadExtent type before offset root used →
47    StableQuery type before offset root →
48    (∀ i, offset ≤ i → i < offset + used → after[i]? = before[i]?) →
49    StableQuery type after offset root
50
51/-- A fitted rejected entry rules out a valid independent symbol on every
52future extension. Full-width classification alone does not justify this
53early error path; the constructor's suffix stability is used explicitly. -/
54def Goal.short_rejected_leaf_stays_invalid : Prop :=
55  ∀ (type : UInt32) (ca : Array Code) (offset root used : Nat) (lens : List Nat),
56    DecodeTableInvariant.Inv type ca offset root used lens →
57    StableQuery type ca offset root →
58    ∀ (inp : List Bool) (entry : Code) (consumed : Nat),
59      tableRead type ca offset root (DecodeShort.padded inp) = some (entry, consumed) →
60      consumed ≤ inp.length → ¬ LeafAccepted type entry →
61      ∀ more : List Bool,
62        ¬ ∃ (symbol : Nat) (rest : List Bool),
63          ZlibF.Spec.decodeSym lens (inp ++ more) = some (symbol, rest) ∧
64          ValidSymbol type symbol
65
66end Zlib.Inftrees.Spec.DecodeTableStability