InflateFastBodyToken.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.Token
2import ZlibF.Spec.InflateFastLengthTrace
3import ZlibF.Spec.InflateFastDistanceResult
4
5/-!
6# Actual fast-body output refines an independent token
7
8This local result covers every input, including invalid symbols and
9too-far matches. It consumes only the current token. No valid completion
10of all pulled lookahead is assumed.
11-/
12
13namespace Zlib.Inffast.Spec.BodyToken
14open C Zlib.Inffast Zlib.Inffast.Proofs ZlibF.Spec
15open Zlib.Inftrees Zlib.Inftrees.Spec
16open ZlibF.Math.LZ77Copy
17
18/-- Data facts about the same actual arrays used by the fast decoder.
19Actual construction and installation must establish these fields; no
20translated function contract is stored here. -/
21structure Tables (e : Env) (L D : List Nat) : Prop where
22  lengthTable : ∃ used,
23    DecodeTableInvariant.Inv LENS e.LCA e.ol e.s0.lenbits.toNat used L
24  distanceTable : ∃ used,
25    DecodeTableInvariant.Inv DISTS e.DCA e.od e.s0.distbits.toNat used D
26  lengthStable : DecodeTableStability.StableQuery LENS e.LCA e.ol e.s0.lenbits.toNat
27  distanceStable : DecodeTableStability.StableQuery DISTS e.DCA e.od e.s0.distbits.toNat
28  lengthFlags : FastTableFlags.QueryCompatible LENS e.LCA e.ol e.s0.lenbits.toNat
29  distanceFlags : FastTableFlags.QueryCompatible DISTS e.DCA e.od e.s0.distbits.toNat
30
31/-- The actual distance call reached after length extras and refill.
32Its physical entry state is retained so that the proved distance result
33can be applied. The run equation is a conclusion, never a hypothesis
34standing in for a callee's correctness theorem. -/
35def DistanceEntry (e : Env) (c : Ctx) (bytes : Array UInt8) (msg : BPtr) (mode : UInt32)
36    (source : List Bool) (beforeRefill output len : Nat)
37    (l' : Zlib.Inffast.L) (after : Heap) : Prop :=
38  ∃ (entry : Zlib.Inffast.L) (input : Nat),
39    beforeRefill ≤ input ∧ input ≤ beforeRefill + 2 ∧
40    LS e entry input output ∧ entry.broke = false ∧ entry.len.toNat = len ∧
41    15 ≤ entry.bits.toNat ∧
42    (input + 2 ≤ e.i0 + e.sm0.avail_in.toNat ∨
43      (input + 1 ≤ e.i0 + e.sm0.avail_in.toNat ∧ 20 ≤ entry.bits.toNat)) ∧
44    Sg e entry.hold.toNat entry.bits.toNat input = source ∧
45    C.run (dolenDist c entry) (e.heap bytes msg mode) = .ok (l', after)
46
47/-- The source length tail retains its extra-bit read and the actual
48distance-entry cut point. The old `RefillPost` alone loses that cut point
49on errors and cannot justify applying a distance execution theorem. -/
50def LengthTail (e : Env) (c : Ctx) (bytes : Array UInt8) (msg : BPtr) (mode : UInt32)
51    (source : List Bool) (input output : Nat) (entry : Code)
52    (l' : Zlib.Inffast.L) (after : Heap) : Prop :=
53  ∃ input' extra rest,
54    input ≤ input' ∧ input' ≤ input + 1 ∧
55    readBits (entry.op &&& 15).toNat source = some (extra, rest) ∧
56    DistanceEntry e c bytes msg mode rest input' output (entry.val.toNat + extra) l' after
57
58/-- Strengthen the source result without changing the already proved
59length trace or the public target. Only a length-base branch needs the
60additional actual distance-entry equation. -/
61def EndWithDistanceEntry (e : Env) (c : Ctx) (bytes : Array UInt8) (msg : BPtr) (mode : UInt32)
62    (source : List Bool) (input output : Nat) (entry : Code)
63    (l' : Zlib.Inffast.L) (after : Heap) : Prop :=
64  LengthTrace.End e bytes msg mode source input output entry l' after ∧
65  (entry.op ≠ 0 ∧ entry.op &&& 16 ≠ 0 →
66    LengthTail e c bytes msg mode source input output entry l' after)
67
68/-- The actual body emits exactly one independently decoded token, ends
69the block, or rejects that token without output. The full old safety
70postcondition and actual heap result are retained. Source-origin and the
71across-call history invariant connect these local inputs to public runs.
72This is the existing internal physical domain, not the public API goal. -/
73def Goal.actual_body_refines_token : Prop :=
74  ∀ (e : Env) (c : Ctx) (bytes : Array UInt8) (msg : BPtr) (mode : UInt32)
75    (l : Zlib.Inffast.L) (input output : Nat) (L D : List Nat),
76    StepPre e c bytes l input output → Tables e L D →
77    ∃ (l' : Zlib.Inffast.L) (after : Heap) (input' output' : Nat)
78      (result : Array UInt8) (resultMsg : BPtr) (resultMode : UInt32),
79      C.run (inflate_fast_body c l) (e.heap bytes msg mode) = .ok (l', after) ∧
80      StepPost e bytes msg mode input output l' after ∧
81      LS e l' input' output' ∧ result.size = bytes.size ∧
82      after = e.heap result resultMsg resultMode ∧
83      let history := MatchHistory.saved e.W e.s0.wsize.toNat e.s0.wnext.toNat
84        e.s0.whave.toNat e.woff
85      let current := writtenBytes bytes output (output - e.bg)
86      let produced := writtenBytes result output' (output' - e.bg)
87      let source := Sg e l.hold.toNat l.bits.toNat input
88      let rest := Sg e l'.hold.toNat l'.bits.toNat input'
89      ((l'.broke = false ∧ Token.Step L D history current source rest produced false) ∨
90       (l'.broke = true ∧ resultMode = TYPE ∧
91         Token.Step L D history current source rest produced true) ∨
92       (l'.broke = true ∧ resultMode = BAD ∧ produced = current ∧
93         Token.Rejected L D history current source))
94
95end Zlib.Inffast.Spec.BodyToken