InflateFastBodyOrigin.lean

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

1import ZlibF.Spec.InflateFast
2import ZlibF.Spec.InflateFastOrigin
3
4/-!
5# One actual fast body preserves the source-bit origin
6
7The safety postcondition retains scalar bounds but does not identify the
8buffer's value. This obligation threads the source suffix through actual
9refills, code drops, extra-bit drops, copying and error/end exits.
10-/
11
12namespace Zlib.Inffast.Spec.BodyOrigin
13open C Zlib.Inffast Zlib.Inffast.Proofs
14
15/-- Actual bit movement consumes a nonnegative exact prefix of the
16original fast-call input and retains the complete existing body result.
17This property alone does not assign DEFLATE meanings to the consumed bits. -/
18def Goal.actual_body_preserves_origin : Prop :=
19  ∀ (e : Env) (c : Ctx) (bytes : Array UInt8) (msg : BPtr) (mode : UInt32)
20    (l : L) (i o used : Nat),
21    StepPre e c bytes l i o → Origin.Inv e l.hold.toNat l.bits.toNat i used →
22    ∃ (l' : L) (after : Heap),
23      C.run (inflate_fast_body c l) (e.heap bytes msg mode) = .ok (l', after) ∧
24      StepPost e bytes msg mode i o l' after ∧
25      ∃ i' o' used',
26        LS e l' i' o' ∧ Origin.Inv e l'.hold.toNat l'.bits.toNat i' used' ∧ used ≤ used'
27
28end Zlib.Inffast.Spec.BodyOrigin