InflateRootTable.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
2
3/-!
4# Positive code lengths in a constructed root table
5
6Array bounds alone do not ensure that a lookup consumes a positive number
7of bits. This local predicate is established by the actual constructor,
8including empty and singleton-invalid entries.
9-/
10namespace Zlib.Inftrees.Spec.RootTable
11open C Zlib.Inftrees Zlib.Inftrees.Proofs
12
13def Safe (ca : Array Code) (offset root : Nat) : Prop :=
14  1 ≤ root ∧ root ≤ 15 ∧ offset + 2 ^ root ≤ ca.size ∧
15    ∀ i, i < 2 ^ root →
16      ∃ entry, ca[offset + i]? = some entry ∧
17        1 ≤ entry.bits.toNat ∧ entry.bits.toNat ≤ root
18
19/-- Every successful actual table construction gives the root-entry bounds
20needed by lookup1. No validity of the compressed input is assumed. -/
21def Goal.constructor_root_bits : Prop :=
22  ∀ (h : Heap) (type : UInt32) (rl : WRef) (ol : Nat) (codes : UInt32)
23    (rc : CodeRef) (oc : Nat) (bits : UInt32) (rw : WRef) (ow : Nat)
24    (pre : CallPre h type rl ol codes rc oc bits rw ow),
25    ∃ r after,
26      C.run (inflate_table type (.ref rl ol) codes (.ref rc oc) bits (.ref rw ow)) h =
27        .ok (r, after) ∧
28      (r.1 = 0 → ∃ ca : Array Code,
29        Space.get after rc = some ca ∧ Safe ca oc r.2.2.toNat)
30
31end Zlib.Inftrees.Spec.RootTable