InflateFastCallOrigin.lean

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

1import ZlibF.Spec.InflateFastBodyOrigin
2
3/-!
4# Exact remaining source input after a whole fast call
5
6Body origin must survive the actual loop and epilogue. This property
7identifies the final heap registers with the original input suffix. It
8does not assign a DEFLATE token meaning to the bits consumed.
9-/
10
11namespace Zlib.Inffast.Spec.CallOrigin
12open C Zlib.Inffast Zlib.Inffast.Proofs
13
14def HasOrigin (e : Env) (after : Heap) : Prop :=
15  ∃ (state : InflateState) (stream : ZStream) (input used : Nat),
16    after.istates e.stid = some state ∧ e.r.get after = some stream ∧
17    stream.next_in = .ref (.blk e.ib) input ∧
18    input + stream.avail_in.toNat = e.i0 + e.sm0.avail_in.toNat ∧
19    Origin.Inv e state.hold.toNat state.bits.toNat input used
20
21/-- The actual whole call preserves the source suffix through every
22body and rollback, retaining its full existing safety/frame result.
23The actual body-origin theorem must be proved, not taken as a premise. -/
24def Goal.actual_fast_preserves_origin : Prop :=
25  ∀ e : Env, ∃ after,
26    C.run (inflate_fast e.strm e.start) e.h0 = .ok ((), after) ∧
27    FastPost e after ∧ HasOrigin e after
28
29end Zlib.Inffast.Spec.CallOrigin