InflateDecodeTableShort.lean

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

1import ZlibF.Spec.InflateDecodeTableSoundness
2
3/-!
4# A successful table lookup on a short bit prefix
5
6BITS observes zero in unavailable high positions of a normalized hold value.
7A lookup may return only when the selected code length fits the available
8bits. The padding below supplies a full-width mathematical table query; it
9does not permit consuming bits from the padding. Actual refill execution is
10a separate bridge.
11-/
12
13namespace Zlib.Inftrees.Spec.DecodeShort
14open C Zlib.Inftrees Zlib.Inftrees.Proofs
15open Zlib.Inftrees.Spec.DecodeSemantics Zlib.Inftrees.Spec.DecodeSoundness
16
17/-- Complete a short query to fifteen bits with zeros. Longer queries are
18unchanged. The selected consumed length must fit the original prefix. -/
19def padded (inp : List Bool) : List Bool :=
20  inp ++ List.replicate (15 - inp.length) false
21
22/-- An accepted leaf selected by a zero-padded query is justified by the
23available prefix when its consumed length fits. Appending future input does
24not change the selected independent symbol. Constructor acceptance supplies
25the prefix-free alphabet; it is not assumed as a callee contract. -/
26def Goal.short_decode_table_leaf_sound : Prop :=
27  ∀ (h : Heap) (type : UInt32) (rl : WRef) (ol : Nat) (codes : UInt32)
28    (rc : CodeRef) (oc : Nat) (bits : UInt32) (rw : WRef) (ow : Nat)
29    (pre : CallPre h type rl ol codes rc oc bits rw ow),
30    (type = LENS ∨ type = DISTS) →
31    ∃ (r : Int32 × CodePtr × UInt32) (after : Heap),
32      C.run (inflate_table type (.ref rl ol) codes (.ref rc oc) bits (.ref rw ow)) h =
33        .ok (r, after) ∧
34      (r.1 = 0 → ∀ (inp : List Bool) (ca : Array Code) (entry : Code) (used : Nat),
35        Space.get after rc = some ca →
36        tableRead type ca oc r.2.2.toNat (padded inp) = some (entry, used) →
37        used ≤ inp.length → LeafAccepted type entry →
38        ∃ symbol,
39          ValidSymbol type symbol ∧ SymbolEntry type symbol entry ∧
40          used = (lensOf pre.f codes.toNat).getD symbol 0 ∧
41          ZlibF.Spec.decodeSym (lensOf pre.f codes.toNat) inp =
42            some (symbol, inp.drop used) ∧
43          ∀ more : List Bool,
44            ZlibF.Spec.decodeSym (lensOf pre.f codes.toNat) (inp ++ more) =
45              some (symbol, inp.drop used ++ more))
46
47end Zlib.Inftrees.Spec.DecodeShort