Token.lean

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

1import ZlibF.Spec.Format.Deflate
2
3/-!
4# One independent Huffman-block token
5
6These relations use only the format decoder, extra-bit tables and bytewise
7history copying. They do not mention a heap or a decoding-table entry.
8A token may be justified even when later, unread tokens are invalid.
9-/
10
11namespace ZlibF.Spec.Token
12
13/-- One literal, complete match, or end-of-block symbol. The final Boolean
14is true only for end of block. The remaining bits are not required to have
15a valid completion; no future input is chosen to justify earlier output. -/
16inductive Step (L D : List Nat) (dict : List UInt8) :
17    List UInt8 → List Bool → List Bool → List UInt8 → Bool → Prop
18  | literal {history : List UInt8} {input rest : List Bool} {symbol : Nat} :
19      decodeSym L input = some (symbol, rest) → symbol < 256 →
20      Step L D dict history input rest (history ++ [symbol.toUInt8]) false
21  | copy {history : List UInt8} {input r1 r2 r3 rest : List Bool}
22      {symbol distanceSymbol lengthExtra distanceExtra : Nat} :
23      decodeSym L input = some (symbol, r1) → 257 ≤ symbol → symbol ≤ 285 →
24      readBits (lengthExtras.getD (symbol - 257) 0) r1 = some (lengthExtra, r2) →
25      decodeSym D r2 = some (distanceSymbol, r3) → distanceSymbol ≤ 29 →
26      readBits (distExtras.getD distanceSymbol 0) r3 = some (distanceExtra, rest) →
27      distBases.getD distanceSymbol 0 + distanceExtra ≤ (dict ++ history).length →
28      Step L D dict history input rest
29        (copyBack dict (distBases.getD distanceSymbol 0 + distanceExtra)
30          (lengthBases.getD (symbol - 257) 0 + lengthExtra) history) false
31  | eob {history : List UInt8} {input rest : List Bool} :
32      decodeSym L input = some (256, rest) →
33      Step L D dict history input rest history true
34
35/-- Independent reasons for rejecting the current token. Invalid-code
36rejection rules out every future extension. A too-far match uses the same
37dictionary-plus-output bound as `Symbols.copy`. -/
38inductive Rejected (L D : List Nat) (dict history : List UInt8) : List Bool → Prop
39  | length {input : List Bool} :
40      (∀ more : List Bool,
41        ¬ ∃ (symbol : Nat) (rest : List Bool),
42          decodeSym L (input ++ more) = some (symbol, rest) ∧ symbol ≤ 285) →
43      Rejected L D dict history input
44  | distance {input r1 r2 : List Bool} {symbol lengthExtra : Nat} :
45      decodeSym L input = some (symbol, r1) → 257 ≤ symbol → symbol ≤ 285 →
46      readBits (lengthExtras.getD (symbol - 257) 0) r1 = some (lengthExtra, r2) →
47      (∀ more : List Bool,
48        ¬ ∃ (distanceSymbol : Nat) (rest : List Bool),
49          decodeSym D (r2 ++ more) = some (distanceSymbol, rest) ∧ distanceSymbol ≤ 29) →
50      Rejected L D dict history input
51  | tooFar {input r1 r2 r3 rest : List Bool}
52      {symbol distanceSymbol lengthExtra distanceExtra : Nat} :
53      decodeSym L input = some (symbol, r1) → 257 ≤ symbol → symbol ≤ 285 →
54      readBits (lengthExtras.getD (symbol - 257) 0) r1 = some (lengthExtra, r2) →
55      decodeSym D r2 = some (distanceSymbol, r3) → distanceSymbol ≤ 29 →
56      readBits (distExtras.getD distanceSymbol 0) r3 = some (distanceExtra, rest) →
57      (dict ++ history).length < distBases.getD distanceSymbol 0 + distanceExtra →
58      Rejected L D dict history input
59
60/-- A successful local token composes with the original format relation.
61An end token itself supplies the original end-of-block constructor. -/
62def Goal.step_composes_symbols : Prop :=
63  ∀ (L D : List Nat) (dict history : List UInt8) (input rest : List Bool)
64    (next : List UInt8) (finished : Bool),
65    Step L D dict history input rest next finished →
66    (finished = true → next = history ∧ Symbols L D dict history input rest next) ∧
67    (finished = false → ∀ (tail : List Bool) (output : List UInt8),
68      Symbols L D dict next rest tail output → Symbols L D dict history input tail output)
69
70/-- Every original Huffman-block derivation exposes one such token.
71Together with composition, this prevents weakening the format by using
72the local token relation as the implementation's postcondition. -/
73def Goal.symbols_exposes_step : Prop :=
74  ∀ (L D : List Nat) (dict history : List UInt8) (input tail : List Bool)
75    (output : List UInt8),
76    Symbols L D dict history input tail output →
77    ∃ (rest : List Bool) (next : List UInt8) (finished : Bool),
78      Step L D dict history input rest next finished ∧
79      ((finished = true ∧ rest = tail ∧ next = output) ∨
80       (finished = false ∧ Symbols L D dict next rest tail output))
81
82/-- Every stated rejection contradicts the original format relation.
83No table predicate, heap condition or valid-input assumption is needed. -/
84def Goal.rejected_has_no_symbols : Prop :=
85  ∀ (L D : List Nat) (dict history : List UInt8) (input : List Bool),
86    Rejected L D dict history input →
87    ∀ (rest : List Bool) (output : List UInt8),
88      ¬ Symbols L D dict history input rest output
89
90end ZlibF.Spec.Token