InflateTableExtent.lean

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

1import ZlibF.Spec.InflateTableSafety
2
3/-!
4# The returned extent of a decoding table
5
6The constructor returns a pointer just past the storage it used. A later table may be
7built in the same array at that pointer. Decoder safety must therefore depend only on
8cells before the returned pointer, rather than on the size of the backing array.
9-/
10
11namespace Zlib.Inftrees.Spec
12open C Zlib.Inftrees Zlib.Inftrees.Proofs
13
14/-- All root cells and every second-level cell that the decoder may read lie before the
15returned end. This is a property of a successful constructor result, not an input
16assumption. -/
17def TableReadExtent (type : UInt32) (ca : Array Code) (offset root used : Nat) : Prop :=
18  1 ≤ root ∧ root ≤ 15 ∧ offset + 2 ^ root ≤ offset + used ∧
19    ∀ i, i < 2 ^ root →
20      let entry := ca.getD (offset + i) default
21      ((type = LENS ∧ Zlib.Inffast.Spec.LenLink entry) ∨
22       (type = DISTS ∧ Zlib.Inffast.Spec.DistLink entry)) →
23      offset + entry.val.toNat + 2 ^ entry.op.toNat ≤ offset + used
24
25/-- The actual builder bounds its returned extent and establishes both the decoder
26predicate and the extent needed when a following table reuses the same array. Accepted
27empty and single-symbol codes are included. -/
28def Goal.inflate_table_read_extent : 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) (used : Nat),
37        Space.get after rc = some ca ∧
38        r.2.1 = .ref rc (oc + used) ∧ used ≤ capOf type ∧
39        TableReadExtent type ca oc r.2.2.toNat used ∧
40        (type = CODES → CodeLengthTableSafe ca oc r.2.2.toNat) ∧
41        (type = LENS → Zlib.Inffast.Spec.LenTableSafe ca oc r.2.2.toNat) ∧
42        (type = DISTS → Zlib.Inffast.Spec.DistTableSafe ca oc r.2.2.toNat))
43
44end Zlib.Inftrees.Spec