inffast.c.tableok.lean

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

1import ZlibF.Runtime.Schema
2import ZlibF.Zlib.«inffixed.h»
3
4/-!
5# inffast.c: the shape of the decoding tables (`TableOK` for `inflate_fast`)
6
7`inflate_fast` reads the literal/length table `lencode` and the distance table `distcode` without checking them. What
8it needs is the shape that `inflate_table` gives (`proof/inftrees.md`, theorem T2) and that the static tables `lenfix`
9and `distfix` have. `LenTableSafe` and `DistTableSafe` state it for a table `ca[o ..]` with root width `R`:
10
11* the root has `2^R` entries inside the array and `R ≤ 15`;
12* a root entry is a leaf (literal, base value, end of block, invalid code) or a link to a second level that lies inside
13  the array, with `1 ≤ op ≤ 15` bits, and whose entries are leaves;
14* the bits of a root entry plus those of the second-level entry reached from it are at most 15;
15* a length base has at most 5 extra bits and a base value of at least 3 whose largest value, with the extra bits, is
16  258; a distance base has at most 13 extra bits and a base value of at least 1.
17
18`inflate_table` must establish `LenTableSafe` for the table it builds for `LENS` and `DistTableSafe` for `DISTS`
19(the table pointer and `*bits` it returns being `o` and `R`). The static tables are proved below.
20-/
21
22namespace Zlib.Inffast.Spec
23open C
24
25/-- A leaf of the literal/length table that is read after `d` bits of the same code were dropped (`d = 0` in the root,
26`d = ` the root width in a second-level table): `bits + d ≤ 15`; a literal (`op = 0`); a length base (`op & 16`)
27with at most 5 extra bits and a base value in `3 .. 258` with the extra bits included; or an end of block or an
28invalid code (`op & 16 = 0`, `op & 64`). -/
29abbrev LenLeaf (d : Nat) (e : Code) : Prop :=
30  e.bits.toNat + d ≤ 15 ∧
31  (e.op = 0 ∨
32   (e.op &&& 16 ≠ 0 ∧ (e.op &&& 15).toNat ≤ 5 ∧ 3 ≤ e.val.toNat ∧ e.val.toNat + 2 ^ (e.op &&& 15).toNat ≤ 259) ∨
33   (e.op &&& 16 = 0 ∧ e.op &&& 64 ≠ 0))
34
35/-- A leaf of the distance table: `bits + d ≤ 15`; a distance base (`op & 16`) with at most 13 extra bits and a base
36value of at least 1; or an invalid code (`op & 16 = 0`, `op & 64`). -/
37abbrev DistLeaf (d : Nat) (e : Code) : Prop :=
38  e.bits.toNat + d ≤ 15 ∧
39  ((e.op &&& 16 ≠ 0 ∧ (e.op &&& 15).toNat ≤ 13 ∧ 1 ≤ e.val.toNat) ∨
40   (e.op &&& 16 = 0 ∧ e.op &&& 64 ≠ 0))
41
42/-- The entry is a link to a second-level table in `inflate_fast` for the literal/length table (the tests of the C:
43`op != 0`, `op & 16 == 0`, `op & 64 == 0`). -/
44abbrev LenLink (e : Code) : Prop := e.op ≠ 0 ∧ e.op &&& 16 = 0 ∧ e.op &&& 64 = 0
45
46/-- The same for the distance table (`op` may be 0 there). -/
47abbrev DistLink (e : Code) : Prop := e.op &&& 16 = 0 ∧ e.op &&& 64 = 0
48
49/-- The second level that a link entry `e` of a table `ca[o ..]` describes: it has between 2 and `2^15` entries, lies
50inside the array, and its entries are leaves that are read after `e.bits` bits were dropped. -/
51abbrev LinkOK (P : Nat → Code → Prop) (ca : Array Code) (o : Nat) (e : Code) : Prop :=
52  e.bits.toNat ≤ 15 ∧ 1 ≤ e.op.toNat ∧ e.op.toNat ≤ 15 ∧ o + e.val.toNat + 2 ^ e.op.toNat ≤ ca.size ∧
53  ∀ j, j < 2 ^ e.op.toNat → P e.bits.toNat (ca.getD (o + e.val.toNat + j) default)
54
55/-- The shape of a table `ca[o ..]` with root width `R`, leaves described by `P`, links by `L`: every root entry is
56either a link with `LinkOK`, or a leaf (`P 0`). -/
57def TableSafe (P : Nat → Code → Prop) (L : Code → Prop) [DecidablePred L] (ca : Array Code) (o R : Nat) : Prop :=
58  R ≤ 15 ∧ o + 2 ^ R ≤ ca.size ∧
59  ∀ i, i < 2 ^ R →
60    (if L (ca.getD (o + i) default) then LinkOK P ca o (ca.getD (o + i) default) else P 0 (ca.getD (o + i) default))
61
62/-- `TableSafe` of the literal/length table. -/
63abbrev LenTableSafe (ca : Array Code) (o R : Nat) : Prop := TableSafe LenLeaf LenLink ca o R
64/-- `TableSafe` of the distance table. -/
65abbrev DistTableSafe (ca : Array Code) (o R : Nat) : Prop := TableSafe DistLeaf DistLink ca o R
66
67end Zlib.Inffast.Spec
68
69namespace Zlib.Inffast.Proofs
70open C Zlib.Inffast.Spec
71
72set_option maxRecDepth 100000 in
73/-- The static literal/length table `lenfix` (inffixed.h), root width 9, has the shape `LenTableSafe` (kernel
74evaluation of all 512 entries). -/
75theorem lenfix_tableSafe : LenTableSafe Zlib.InffixedH.lenfix 0 9 := by
76  unfold LenTableSafe TableSafe
77  refine ⟨by decide, by decide +kernel, ?_⟩
78  decide +kernel
79
80set_option maxRecDepth 100000 in
81/-- The static distance table `distfix`, root width 5, has the shape `DistTableSafe`. -/
82theorem distfix_tableSafe : DistTableSafe Zlib.InffixedH.distfix 0 5 := by
83  unfold DistTableSafe TableSafe
84  refine ⟨by decide, by decide +kernel, ?_⟩
85  decide +kernel
86
87end Zlib.Inffast.Proofs