InflateDecodeTableSemantics.lean

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

1import ZlibF.Spec.InflateTableContent
2import ZlibF.Spec.Format.Huffman
3
4/-!
5# Canonical symbols in the constructed LENS and DISTS tables
6
7This internal bridge starts with a successful independent Huffman decode.
8It requires fifteen available bits so both levels can be indexed without
9padding. Actual early-returning lookup with less input needs a later bridge.
10The relation includes reserved symbols and identifies their invalid flag.
11-/
12
13namespace Zlib.Inftrees.Spec.DecodeSemantics
14open C Zlib.Inftrees Zlib.Inftrees.Proofs
15
16/-- The two-level table access used by the slow decoder. Link values are
17offsets from the table start; the second entry's bit count excludes the root.
18Only this finite access is modeled here, not input refill or bit dropping. -/
19def tableRead (type : UInt32) (ca : Array Code) (offset root : Nat)
20    (inp : List Bool) : Option (Code × Nat) := do
21  let (i, _) ← ZlibF.Spec.readBits root inp
22  let first ← ca[offset + i]?
23  let link := if type = LENS then first.op != 0 && (first.op &&& 0xf0) == 0
24    else (first.op &&& 0xf0) == 0
25  if link then
26    let (j, _) ← ZlibF.Spec.readBits first.op.toNat (inp.drop first.bits.toNat)
27    let second ← ca[offset + first.val.toNat + j]?
28    return (second, first.bits.toNat + second.bits.toNat)
29  else return (first, first.bits.toNat)
30
31/-- Independent DEFLATE meanings of leaf operations. Reserved symbols are
32invalid, even though they have canonical codes in some accepted tables. -/
33def SymbolEntry (type : UInt32) (symbol : Nat) (entry : Code) : Prop :=
34  if type = LENS then
35    if symbol < 256 then entry.op = 0 ∧ entry.val.toNat = symbol
36    else if symbol = 256 then entry.op = 96 ∧ entry.val = 0
37    else if symbol ≤ 285 then
38      entry.op.toNat = 16 + ZlibF.Spec.lengthExtras.getD (symbol - 257) 0 ∧
39      entry.val.toNat = ZlibF.Spec.lengthBases.getD (symbol - 257) 0
40    else (entry.op &&& 64) != 0
41  else
42    if symbol ≤ 29 then
43      entry.op.toNat = 16 + ZlibF.Spec.distExtras.getD symbol 0 ∧
44      entry.val.toNat = ZlibF.Spec.distBases.getD symbol 0
45    else (entry.op &&& 64) != 0
46
47/-- The actual constructor's table selects the independent decoder's symbol,
48with the exact consumed code length and the DEFLATE leaf meaning. This is
49the forward direction for full-width input. It does not yet assert that
50every table result is a valid independent symbol. -/
51def Goal.decode_table_matches_format : 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      (r.1 = 0 → ∀ (inp : List Bool) (symbol : Nat) (rest : List Bool),
60        15 ≤ inp.length →
61        ZlibF.Spec.decodeSym (lensOf pre.f codes.toNat) inp = some (symbol, rest) →
62        ∃ (ca : Array Code) (entry : Code) (used : Nat),
63          Space.get after rc = some ca ∧
64          tableRead type ca oc r.2.2.toNat inp = some (entry, used) ∧
65          used = (lensOf pre.f codes.toNat).getD symbol 0 ∧
66          rest = inp.drop used ∧ SymbolEntry type symbol entry)
67
68end Zlib.Inftrees.Spec.DecodeSemantics