InflateDecodeTableSoundness.lean

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

1import ZlibF.Spec.InflateDecodeTableSemantics
2
3/-!
4# Soundness of accepted decoding-table leaves
5
6The literal/length decoder tests the end-of-block flag before the invalid
7flag. EOB therefore remains accepted even though its op is 96. Reserved
8symbols and incomplete-table padding are rejected. This internal goal still
9uses fifteen available bits; it does not restrict public input splits.
10-/
11
12namespace Zlib.Inftrees.Spec.DecodeSoundness
13open C Zlib.Inftrees Zlib.Inftrees.Proofs
14open Zlib.Inftrees.Spec.DecodeSemantics
15
16/-- The branch condition by which the actual slow decoder accepts a final
17leaf. LENS tests bit 32 before bit 64; DISTS rejects bit 64 directly. -/
18def LeafAccepted (type : UInt32) (entry : Code) : Prop :=
19  if type = LENS then (entry.op &&& 32) != 0 ∨ (entry.op &&& 64) = 0
20  else (entry.op &&& 64) = 0
21
22/-- Valid format symbols, excluding the reserved literal/length and distance
23symbols that can have canonical codes in fixed or generic accepted tables. -/
24def ValidSymbol (type : UInt32) (symbol : Nat) : Prop :=
25  if type = LENS then symbol ≤ 285 else symbol ≤ 29
26
27/-- Every full-width read of an actual successful LENS/DISTS constructor
28result exists. Its leaf is accepted exactly when it is the independent
29decoder's valid symbol, with the same code length and leaf meaning. Empty
30alphabets, singleton padding and reserved symbols remain in the domain. -/
31def Goal.decode_table_leaf_sound : Prop :=
32  ∀ (h : Heap) (type : UInt32) (rl : WRef) (ol : Nat) (codes : UInt32)
33    (rc : CodeRef) (oc : Nat) (bits : UInt32) (rw : WRef) (ow : Nat)
34    (pre : CallPre h type rl ol codes rc oc bits rw ow),
35    (type = LENS ∨ type = DISTS) →
36    ∃ (r : Int32 × CodePtr × UInt32) (after : Heap),
37      C.run (inflate_table type (.ref rl ol) codes (.ref rc oc) bits (.ref rw ow)) h =
38        .ok (r, after) ∧
39      (r.1 = 0 → ∀ (inp : List Bool), 15 ≤ inp.length →
40        ∃ (ca : Array Code) (entry : Code) (used : Nat),
41          Space.get after rc = some ca ∧
42          tableRead type ca oc r.2.2.toNat inp = some (entry, used) ∧
43          (LeafAccepted type entry ↔
44            ∃ (symbol : Nat) (rest : List Bool),
45              ZlibF.Spec.decodeSym (lensOf pre.f codes.toNat) inp = some (symbol, rest) ∧
46              ValidSymbol type symbol ∧
47              used = (lensOf pre.f codes.toNat).getD symbol 0 ∧
48              rest = inp.drop used ∧ SymbolEntry type symbol entry))
49
50end Zlib.Inftrees.Spec.DecodeSoundness