InflateSubtable.lean

本页保留 Lean 源码及行号。点击行号可定位语句，点击 import 中的模块名可查看依赖。

1import ZlibF.Spec.InflateRootTable
2
3/-!
4# Bounds of a root link and its second-level entries
5
6These facts are outputs of actual table construction. The slow decoder uses
7bits+op to index the subtable and bits+leaf.bits for its fit test.
8-/
9namespace Zlib.Inftrees.Spec.Subtable
10open C Zlib.Inftrees Zlib.Inftrees.Proofs
11
12def IsLink (type : UInt32) (entry : Code) : Bool :=
13  if type = LENS then entry.op != 0 && (entry.op &&& 0xf0) == 0
14  else (entry.op &&& 0xf0) == 0
15
16def Safe (ca : Array Code) (offset : Nat) (link : Code) : Prop :=
17  1 ≤ link.bits.toNat ∧ 1 ≤ link.op.toNat ∧
18    link.bits.toNat + link.op.toNat ≤ 15 ∧
19    offset + link.val.toNat + 2 ^ link.op.toNat ≤ ca.size ∧
20    ∀ j, j < 2 ^ link.op.toNat →
21      ∃ entry, ca[offset + link.val.toNat + j]? = some entry ∧
22        1 ≤ entry.bits.toNat ∧ entry.bits.toNat ≤ link.op.toNat
23
24/-- Each actual root link has a bounded subtable of positive-length leaves.
25Empty and singleton tables are included and must not invent links. -/
26def Goal.constructor_subtable_bits : 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 after,
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 → ∃ ca : Array Code,
35        Space.get after rc = some ca ∧ RootTable.Safe ca oc r.2.2.toNat ∧
36        ∀ i entry, i < 2 ^ r.2.2.toNat → ca[oc + i]? = some entry →
37          IsLink type entry = true → entry.bits.toNat = r.2.2.toNat ∧ Safe ca oc entry)
38
39end Zlib.Inftrees.Spec.Subtable