InflateDecodeTableRejection.lean

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

1import ZlibF.Spec.InflateDecodeTableSoundness
2
3/-!
4# Classifying valid and rejected full-width input
5
6This combines the independent-to-table and table-to-independent directions.
7The existence of a valid independent decode below does not depend on the
8returned table entry's meaning. Thus a rejected entry rules out a valid
9independent symbol, including empty and singleton-padding cases.
10-/
11
12namespace Zlib.Inftrees.Spec.DecodeRejection
13open C Zlib.Inftrees Zlib.Inftrees.Proofs
14open Zlib.Inftrees.Spec.DecodeSemantics Zlib.Inftrees.Spec.DecodeSoundness
15
16/-- Actual full-width table lookup accepts exactly the inputs with a valid
17independent Huffman symbol. This local classification still needs a bridge
18to actual input refill and early lookup on shorter prefixes. -/
19def Goal.decode_table_classifies_input : Prop :=
20  ∀ (h : Heap) (type : UInt32) (rl : WRef) (ol : Nat) (codes : UInt32)
21    (rc : CodeRef) (oc : Nat) (bits : UInt32) (rw : WRef) (ow : Nat)
22    (pre : CallPre h type rl ol codes rc oc bits rw ow),
23    (type = LENS ∨ type = DISTS) →
24    ∃ (r : Int32 × CodePtr × UInt32) (after : Heap),
25      C.run (inflate_table type (.ref rl ol) codes (.ref rc oc) bits (.ref rw ow)) h =
26        .ok (r, after) ∧
27      (r.1 = 0 → ∀ (inp : List Bool), 15 ≤ inp.length →
28        ∃ (ca : Array Code) (entry : Code) (used : Nat),
29          Space.get after rc = some ca ∧
30          tableRead type ca oc r.2.2.toNat inp = some (entry, used) ∧
31          (LeafAccepted type entry ↔ ∃ (symbol : Nat) (rest : List Bool),
32            ZlibF.Spec.decodeSym (lensOf pre.f codes.toNat) inp = some (symbol, rest) ∧
33            ValidSymbol type symbol))
34
35end Zlib.Inftrees.Spec.DecodeRejection