InflateFastDistanceSemantics.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.Proof.«inffast.c.lp»
4
5/-!
6# The fast distance lookup selects an independent Huffman symbol
7
8DistLook is already produced by the actual distance lookup proof. Its
9fast link tests must agree with the two-level format query. Final leaves
10need the actual constructor's flags as well as the old safety shape.
11-/
12
13namespace Zlib.Inffast.Spec.DistanceSemantics
14open C Zlib.Inffast Zlib.Inffast.Proofs
15open Zlib.Inftrees Zlib.Inftrees.Spec
16
17/-- A selected fast leaf has the exact query, consumed code length and
18independent symbol meaning, or rejects every future extension. This is
19a lookup-data bridge, not complete extra-bit or copy execution. -/
20def Goal.distance_lookup_matches_format : Prop :=
21  ∀ (e : Env) (hold bits input tableUsed : Nat) (lens : List Nat)
22    (entry : Code) (consumed : Nat),
23    DecodeTableInvariant.Inv DISTS e.DCA e.od e.s0.distbits.toNat tableUsed lens →
24    DecodeTableStability.StableQuery DISTS e.DCA e.od e.s0.distbits.toNat →
25    FastTableFlags.QueryCompatible DISTS e.DCA e.od e.s0.distbits.toNat →
26    hold < 2 ^ bits → 15 ≤ bits →
27    DistLook e hold (hold % 2 ^ e.s0.distbits.toNat) entry consumed →
28    let stream := Sg e hold bits input
29    DecodeSemantics.tableRead DISTS e.DCA e.od e.s0.distbits.toNat stream = some (entry, consumed) ∧
30    1 ≤ consumed ∧ consumed ≤ 15 ∧ DistLeaf 0 entry ∧
31    ((entry.op &&& 16 = 0 ∧
32      ∀ more : List Bool,
33        ¬ ∃ (symbol : Nat) (rest : List Bool),
34          ZlibF.Spec.decodeSym lens (stream ++ more) = some (symbol, rest) ∧ symbol ≤ 29) ∨
35     (entry.op &&& 16 ≠ 0 ∧
36      ∃ symbol, symbol ≤ 29 ∧ DecodeSemantics.SymbolEntry DISTS symbol entry ∧
37        consumed = lens.getD symbol 0 ∧
38        ZlibF.Spec.decodeSym lens stream = some (symbol, stream.drop consumed) ∧
39        ∀ more : List Bool,
40          ZlibF.Spec.decodeSym lens (stream ++ more) =
41            some (symbol, stream.drop consumed ++ more)))
42
43end Zlib.Inffast.Spec.DistanceSemantics