InflateDecodeTableFrame.lean

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

1import ZlibF.Spec.InflateDecodeTableSemantics
2import ZlibF.Spec.InflateTableExtent
3
4/-!
5# Transporting table meaning across a later constructor
6
7LENS and DISTS share one code array. A semantic result about the first
8constructor's array cannot be applied to the second constructor's array
9without a frame argument. The returned extent bounds both table reads.
10This obligation transports the query itself, including failed queries.
11It does not assume or establish a constructor's frame.
12-/
13
14namespace Zlib.Inftrees.Spec.DecodeTableFrame
15open C Zlib.Inftrees.Spec.DecodeSemantics
16
17/-- Preserving every cell of the first table's returned extent preserves
18every two-level query, for inputs of any length. The actual second builder
19must supply the cell equality. A capacity bound alone cannot replace it. -/
20def Goal.decode_table_read_preserved : Prop :=
21  ∀ (type : UInt32) (before after : Array Code) (offset root used : Nat),
22    (type = LENS ∨ type = DISTS) →
23    TableReadExtent type before offset root used →
24    (∀ i, offset ≤ i → i < offset + used → after[i]? = before[i]?) →
25    ∀ inp : List Bool,
26      tableRead type after offset root inp = tableRead type before offset root inp
27
28end Zlib.Inftrees.Spec.DecodeTableFrame