InflateDecodeTableInvariant.lean

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

1import ZlibF.Spec.InflateSubtable
2import ZlibF.Spec.InflateDecodeTableShort
3import ZlibF.Spec.InflateDecodeTableRejection
4import ZlibF.Spec.InflateDecodeTableFrame
5
6/-!
7# The shape and meaning of an installed decoding table
8
9The logical alphabet remains fixed when a later constructor writes another
10table in the same array. Every field below is a property of the current
11array. The constructor goal establishes these properties by executing the
12translated function; it does not assume a callee contract.
13-/
14
15namespace Zlib.Inftrees.Spec.DecodeTableInvariant
16open C Zlib.Inftrees Zlib.Inftrees.Proofs
17open Zlib.Inftrees.Spec.DecodeSemantics Zlib.Inftrees.Spec.DecodeSoundness
18
19/-- Shape, actual read extent and independent symbol semantics at one
20installed table. Empty and singleton alphabets are retained. No assumption
21is made about whether the future compressed input will be valid. -/
22structure Inv (type : UInt32) (ca : Array Code) (offset root used : Nat)
23    (lens : List Nat) : Prop where
24  tableType : type = LENS ∨ type = DISTS
25  rootTable : RootTable.Safe ca offset root
26  subtables : ∀ i entry, i < 2 ^ root → ca[offset + i]? = some entry →
27    Subtable.IsLink type entry = true →
28    entry.bits.toNat = root ∧ Subtable.Safe ca offset entry
29  readExtent : TableReadExtent type ca offset root used
30  acceptable : ZlibF.Spec.Acceptable (kindOf type) lens
31  short : ∀ (inp : List Bool) (entry : Code) (consumed : Nat),
32    tableRead type ca offset root (DecodeShort.padded inp) = some (entry, consumed) →
33    consumed ≤ inp.length → LeafAccepted type entry →
34    ∃ symbol,
35      ValidSymbol type symbol ∧ SymbolEntry type symbol entry ∧
36      consumed = lens.getD symbol 0 ∧
37      ZlibF.Spec.decodeSym lens inp = some (symbol, inp.drop consumed) ∧
38      ∀ more : List Bool,
39        ZlibF.Spec.decodeSym lens (inp ++ more) =
40          some (symbol, inp.drop consumed ++ more)
41  classify : ∀ inp : List Bool, 15 ≤ inp.length →
42    ∃ (entry : Code) (consumed : Nat),
43      tableRead type ca offset root inp = some (entry, consumed) ∧
44      (LeafAccepted type entry ↔ ∃ (symbol : Nat) (rest : List Bool),
45        ZlibF.Spec.decodeSym lens inp = some (symbol, rest) ∧ ValidSymbol type symbol)
46
47/-- Actual construction establishes the invariant with its original
48alphabet and its returned extent. The existing heap frame and all rejected
49results are retained. This is a local constructor result, not a public
50decoder theorem or a claim about fixed static tables. -/
51def Goal.constructor_establishes_decode_table_invariant : Prop :=
52  ∀ (h : Heap) (type : UInt32) (rl : WRef) (ol : Nat) (codes : UInt32)
53    (rc : CodeRef) (oc : Nat) (bits : UInt32) (rw : WRef) (ow : Nat)
54    (pre : CallPre h type rl ol codes rc oc bits rw ow),
55    (type = LENS ∨ type = DISTS) →
56    ∃ (r : Int32 × CodePtr × UInt32) (after : Heap),
57      C.run (inflate_table type (.ref rl ol) codes (.ref rc oc) bits (.ref rw ow)) h =
58        .ok (r, after) ∧
59      Result h rw rc ow oc (capOf type) codes.toNat pre.wa pre.ca (.ref rc oc) bits r after ∧
60      (r.1 = 0 → ∃ (ca : Array Code) (used : Nat),
61        Space.get after rc = some ca ∧ r.2.1 = .ref rc (oc + used) ∧
62        used ≤ capOf type ∧
63        Inv type ca oc r.2.2.toNat used (lensOf pre.f codes.toNat))
64
65/-- A later builder preserves the whole invariant when its actual frame
66preserves this table's returned extent. Array growth is harmless. A mere
67capacity bound does not supply the required pointwise frame. -/
68def Goal.decode_table_invariant_of_prefix : Prop :=
69  ∀ (type : UInt32) (before after : Array Code) (offset root used : Nat)
70    (lens : List Nat),
71    Inv type before offset root used lens →
72    before.size ≤ after.size →
73    (∀ i, offset ≤ i → i < offset + used → after[i]? = before[i]?) →
74    Inv type after offset root used lens
75
76end Zlib.Inftrees.Spec.DecodeTableInvariant