InflateFastLengthSemantics.lean

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

1import ZlibF.Spec.InflateDecodeTableStability
2import ZlibF.Spec.InflateFastTableFlags
3import ZlibF.Spec.InflateFast
4
5/-!
6# Fast literal/length selection and independent symbols
7
8The selected leaf must be connected to the independent Huffman decoder.
9Source-bit origin and range-safe tables alone do not establish this fact.
10The table predicates below are internal data obligations for construction.
11-/
12
13namespace Zlib.Inffast.Spec.LengthSemantics
14open C Zlib.Inffast Zlib.Inffast.Proofs
15open Zlib.Inftrees Zlib.Inftrees.Spec
16
17/-- The final entry selected by the actual fast root/link branch order.
18The second index uses the hold value after dropping the root code bits. -/
19def Look (e : Env) (hold index : Nat) (entry : Code) (consumed : Nat) : Prop :=
20  (e.LCA.getD (e.ol + index) default = entry ∧
21    consumed = entry.bits.toNat ∧ ¬ LenLink entry) ∨
22  (∃ first next,
23    e.LCA.getD (e.ol + index) default = first ∧ LenLink first ∧
24    next < 2 ^ first.op.toNat ∧
25    next = (hold / 2 ^ first.bits.toNat) % 2 ^ first.op.toNat ∧
26    e.LCA.getD (e.ol + first.val.toNat + next) default = entry ∧
27    consumed = first.bits.toNat + entry.bits.toNat ∧
28    first.bits.toNat + entry.bits.toNat ≤ 15 ∧ ¬ LenLink entry)
29
30/-- A selected fast leaf has the independent symbol meaning and exact
31code length, or rejects every future extension. This includes reserved
32symbols and incomplete-table padding. It does not assume valid input or
33assert that the main decoder has established the table predicates. -/
34def Goal.length_lookup_matches_format : Prop :=
35  ∀ (e : Env) (hold bits input tableUsed : Nat) (lens : List Nat)
36    (entry : Code) (consumed : Nat),
37    DecodeTableInvariant.Inv LENS e.LCA e.ol e.s0.lenbits.toNat tableUsed lens →
38    DecodeTableStability.StableQuery LENS e.LCA e.ol e.s0.lenbits.toNat →
39    FastTableFlags.QueryCompatible LENS e.LCA e.ol e.s0.lenbits.toNat →
40    hold < 2 ^ bits → 15 ≤ bits →
41    Look e hold (hold % 2 ^ e.s0.lenbits.toNat) entry consumed →
42    let stream := Sg e hold bits input
43    DecodeSemantics.tableRead LENS e.LCA e.ol e.s0.lenbits.toNat stream =
44      some (entry, consumed) ∧
45    1 ≤ consumed ∧ consumed ≤ 15 ∧ LenLeaf 0 entry ∧
46    ((¬ FastTableFlags.FastLeafAccepted LENS entry ∧
47      ∀ more : List Bool,
48        ¬ ∃ (symbol : Nat) (rest : List Bool),
49          ZlibF.Spec.decodeSym lens (stream ++ more) = some (symbol, rest) ∧ symbol ≤ 285) ∨
50     (FastTableFlags.FastLeafAccepted LENS entry ∧
51      ∃ symbol, symbol ≤ 285 ∧ DecodeSemantics.SymbolEntry LENS symbol entry ∧
52        consumed = lens.getD symbol 0 ∧
53        ZlibF.Spec.decodeSym lens stream = some (symbol, stream.drop consumed) ∧
54        ∀ more : List Bool,
55          ZlibF.Spec.decodeSym lens (stream ++ more) =
56            some (symbol, stream.drop consumed ++ more)))
57
58end Zlib.Inffast.Spec.LengthSemantics