InflateTableSafety.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.Proof.«inffast.c.tableok»
3
4/-!
5# Table predicates established by the actual constructor
6
7This obligation connects construction to the predicates used by the decoder. Every root
8entry must be covered, including invalid entries in empty or single-symbol codes. A result
9about the leaves and links that were written is insufficient by itself.
10-/
11
12namespace Zlib.Inftrees.Spec
13open C Zlib.Inftrees Zlib.Inftrees.Proofs
14
15/-- The code-length table has no second level. Every lookup reads a nonzero number of bits
16and yields a code-length alphabet symbol or an invalid marker. -/
17def CodeLengthTableSafe (ca : Array Code) (offset root : Nat) : Prop :=
18  1 ≤ root ∧ root ≤ 7 ∧ offset + 2 ^ root ≤ ca.size ∧
19    ∀ i, i < 2 ^ root →
20      let entry := ca.getD (offset + i) default
21      1 ≤ entry.bits.toNat ∧ entry.bits.toNat ≤ root ∧
22        ((entry.op = 0 ∧ entry.val.toNat < 19) ∨ entry.op = 64)
23
24/-- Successful construction establishes every table predicate that the slow and fast
25decoders use. The real call and existing safety frame remain explicit. The input lengths
26may be empty, incomplete, oversubscribed or too large for the capacity; error returns are
27allowed. No table property or callee contract is an input hypothesis. -/
28def Goal.inflate_table_decoder_safe : Prop :=
29  ∀ (h : Heap) (type : UInt32) (rl : WRef) (ol : Nat) (codes : UInt32)
30    (rc : CodeRef) (oc : Nat) (bits : UInt32) (rw : WRef) (ow : Nat)
31    (pre : CallPre h type rl ol codes rc oc bits rw ow),
32    ∃ r after,
33      C.run (inflate_table type (.ref rl ol) codes (.ref rc oc) bits (.ref rw ow)) h =
34        .ok (r, after) ∧
35      Result h rw rc ow oc (capOf type) codes.toNat pre.wa pre.ca (.ref rc oc) bits r after ∧
36      (r.1 = 0 → ∃ ca : Array Code, Space.get after rc = some ca ∧
37        1 ≤ r.2.2.toNat ∧ r.2.2.toNat ≤ 15 ∧
38        (type = CODES → CodeLengthTableSafe ca oc r.2.2.toNat) ∧
39        (type = LENS → Zlib.Inffast.Spec.LenTableSafe ca oc r.2.2.toNat) ∧
40        (type = DISTS → Zlib.Inffast.Spec.DistTableSafe ca oc r.2.2.toNat))
41
42end Zlib.Inftrees.Spec