InflateFastTableFlags.lean

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

1import ZlibF.Spec.InflateDecodeTableFrame
2import ZlibF.Spec.InflateDecodeTableSoundness
3
4/-!
5# Leaf flags shared by slow and fast decoding
6
7The fast decoder tests bit 16 before bit 64. The slow decoder tests the
8invalid flag before interpreting a length or distance. Their existing
9safety predicates alone do not rule out both bits being set. This extra
10data property must follow from actual construction, not a public caller
11restriction or an assumed callee contract.
12-/
13
14namespace Zlib.Inftrees.Spec.FastTableFlags
15open C Zlib.Inftrees Zlib.Inftrees.Proofs
16open Zlib.Inftrees.Spec.DecodeSemantics
17
18/-- A length or distance marker is never also an invalid marker. EOB 96
19and the actual reserved markers remain allowed. -/
20def Compatible (entry : Code) : Prop :=
21  entry.op &&& 16 ≠ 0 → entry.op &&& 64 = 0
22
23/-- Every full-width table query returns compatible flags. The fifteen
24bits describe an internal table query, not a public input-buffer minimum.
25Actual fast decoding must establish the available-bit bound separately. -/
26def QueryCompatible (type : UInt32) (ca : Array Code) (offset root : Nat) : Prop :=
27  ∀ (inp : List Bool) (entry : Code) (consumed : Nat),
28    15 ≤ inp.length →
29    tableRead type ca offset root inp = some (entry, consumed) → Compatible entry
30
31/-- The fast branch order after a final leaf is selected. Links are not
32final leaves; the shape premise in the next goal excludes them. -/
33def FastLeafAccepted (type : UInt32) (entry : Code) : Prop :=
34  if type = LENS then
35    entry.op = 0 ∨ entry.op &&& 16 ≠ 0 ∨
36      (entry.op &&& 64 ≠ 0 ∧ entry.op &&& 32 ≠ 0)
37  else entry.op &&& 16 ≠ 0
38
39/-- Compatible flags and the existing leaf shape reconcile the two branch
40orders. This is a data lemma; actual table selection and independent symbol
41meaning remain separate obligations. -/
42def Goal.leaf_classification_agrees : Prop :=
43  ∀ (type : UInt32) (entry : Code),
44    (type = LENS ∨ type = DISTS) → Compatible entry →
45    ((type = LENS → Zlib.Inffast.Spec.LenLeaf 0 entry) ∧
46     (type = DISTS → Zlib.Inffast.Spec.DistLeaf 0 entry)) →
47    (FastLeafAccepted type entry ↔ DecodeSoundness.LeafAccepted type entry)
48
49/-- Actual table construction establishes flag compatibility, retaining
50the existing execution and result. Rejected constructions are retained.
51This does not assert independent decoding correctness of inflate_fast. -/
52def Goal.constructor_establishes_fast_leaf_flags : Prop :=
53  ∀ (h : Heap) (type : UInt32) (rl : WRef) (ol : Nat) (codes : UInt32)
54    (rc : CodeRef) (oc : Nat) (bits : UInt32) (rw : WRef) (ow : Nat)
55    (pre : CallPre h type rl ol codes rc oc bits rw ow),
56    (type = LENS ∨ type = DISTS) →
57    ∃ (r : Int32 × CodePtr × UInt32) (after : Heap),
58      C.run (inflate_table type (.ref rl ol) codes (.ref rc oc) bits (.ref rw ow)) h =
59        .ok (r, after) ∧
60      Result h rw rc ow oc (capOf type) codes.toNat pre.wa pre.ca (.ref rc oc) bits r after ∧
61      (r.1 = 0 → ∀ ca : Array Code, Space.get after rc = some ca →
62        QueryCompatible type ca oc r.2.2.toNat)
63
64/-- A later builder preserves the property through the actual extent and
65cell frame. Equal capacities alone do not establish the frame. -/
66def Goal.fast_leaf_flags_of_prefix : Prop :=
67  ∀ (type : UInt32) (before after : Array Code) (offset root used : Nat),
68    (type = LENS ∨ type = DISTS) →
69    TableReadExtent type before offset root used →
70    QueryCompatible type before offset root →
71    (∀ i, offset ≤ i → i < offset + used → after[i]? = before[i]?) →
72    QueryCompatible type after offset root
73
74/-- The actual default static tables provide the same property. Their
75reserved markers are checked as stored, without replacing their values. -/
76def Goal.fixed_tables_have_fast_leaf_flags : Prop :=
77  QueryCompatible LENS Zlib.InffixedH.lenfix 0 9 ∧
78  QueryCompatible DISTS Zlib.InffixedH.distfix 0 5
79
80end Zlib.Inftrees.Spec.FastTableFlags