InflateFastLengthTrace.lean

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

1import ZlibF.Spec.InflateFastLengthSemantics
2
3/-!
4# Actual fast-body result tied to its selected length-table leaf
5
6The old body postcondition does not identify which literal/length entry
7was selected. This obligation retains that selection and its actual
8effects, including the length extras and the existing distance result.
9-/
10
11namespace Zlib.Inffast.Spec.LengthTrace
12open C Zlib.Inffast Zlib.Inffast.Proofs ZlibF.Spec
13
14/-- The two actual pre-lookup pulls, when needed, expressed with the
15existing register-update function. No output or table storage changes. -/
16def ready (e : Env) (l : L) (input : Nat) : L × Nat :=
17  if l.bits < 15 then
18    let first := pullL l (e.IN.getD input 0) (.ref (.blk e.ib) (input + 1))
19    (pullL first (e.IN.getD (input + 1) 0) (.ref (.blk e.ib) (input + 2)), input + 2)
20  else (l, input)
21
22/-- The source branches after dropping the selected literal/length code.
23The length branch retains actual extra-bit reading, refill and distance
24lookup/copy results. Symbol meaning is supplied by the separate format
25bridge, and saved-window provenance remains an enclosing invariant. -/
26def End (e : Env) (bytes : Array UInt8) (msg : BPtr) (mode : UInt32)
27    (remaining : List Bool) (input output : Nat) (entry : Code)
28    (l' : L) (after : Heap) : Prop :=
29  ¬ LenLink entry ∧ l'.againL = false ∧
30  ((entry.op = 0 ∧ l'.broke = false ∧ LS e l' input (output + 1) ∧
31      Sg e l'.hold.toNat l'.bits.toNat input = remaining ∧
32      after = e.heap (bytes.set! output entry.val.toUInt8) msg mode) ∨
33   (entry.op ≠ 0 ∧ entry.op &&& 16 ≠ 0 ∧
34      ∃ input' extra rest,
35        input ≤ input' ∧ input' ≤ input + 1 ∧
36        readBits (entry.op &&& 15).toNat remaining = some (extra, rest) ∧
37        RefillPost e bytes msg mode rest input' output (entry.val.toNat + extra) l' after) ∨
38   (entry.op ≠ 0 ∧ entry.op &&& 16 = 0 ∧ entry.op &&& 64 ≠ 0 ∧
39      entry.op &&& 32 ≠ 0 ∧ l'.broke = true ∧ LS e l' input output ∧
40      Sg e l'.hold.toNat l'.bits.toNat input = remaining ∧
41      after = e.heap bytes msg TYPE) ∨
42   (entry.op ≠ 0 ∧ entry.op &&& 16 = 0 ∧ entry.op &&& 64 ≠ 0 ∧
43      entry.op &&& 32 = 0 ∧ l'.broke = true ∧ LS e l' input output ∧
44      Sg e l'.hold.toNat l'.bits.toNat input = remaining ∧
45      ∃ errorMsg, after = e.heap bytes errorMsg BAD))
46
47/-- The actual whole body returns its original safety result and the
48selected leaf's exact effects. All source exits are retained. No body or
49callee contract is a hypothesis, and no format-validity assumption hides
50an invalid-code exit. These are the existing internal fast-body bounds. -/
51def Goal.actual_body_retains_selected_length : Prop :=
52  ∀ (e : Env) (c : Ctx) (bytes : Array UInt8) (msg : BPtr) (mode : UInt32)
53    (l : L) (input output : Nat),
54    StepPre e c bytes l input output →
55    let prepared := ready e l input
56    ∃ (l' : L) (after : Heap),
57      C.run (inflate_fast_body c l) (e.heap bytes msg mode) = .ok (l', after) ∧
58      StepPost e bytes msg mode input output l' after ∧
59      Sg e prepared.1.hold.toNat prepared.1.bits.toNat prepared.2 =
60        Sg e l.hold.toNat l.bits.toNat input ∧
61      ∃ entry consumed,
62        consumed ≤ 15 ∧
63        LengthSemantics.Look e prepared.1.hold.toNat
64          (prepared.1.hold.toNat % 2 ^ e.s0.lenbits.toNat) entry consumed ∧
65        End e bytes msg mode
66          ((Sg e prepared.1.hold.toNat prepared.1.bits.toNat prepared.2).drop consumed)
67          prepared.2 output entry l' after
68
69end Zlib.Inffast.Spec.LengthTrace