InflateFastDistanceOrigin.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# Source-bit origin through the actual fast distance sub-block
6
7The source split dolenDist includes lookup, extra bits and copying. Its
8old error postcondition does not retain the bit stream. Origin must hold
9on error as well as on a successful copy.
10-/
11
12namespace Zlib.Inffast.Spec.DistanceOrigin
13open C Zlib.Inffast Zlib.Inffast.Proofs
14
15/-- The complete actual distance sub-block retains its existing result
16and the exact source suffix on every exit. These are internal data
17preconditions, not an assumed distance-callee contract. -/
18def Goal.actual_distance_block_preserves_origin : Prop :=
19  ∀ (e : Env) (c : Ctx) (bytes : Array UInt8) (msg : BPtr) (mode : UInt32)
20    (l : L) (i o used : Nat),
21    CtxOK e c → LS e l i o →
22    e.o0 + e.sm0.avail_out.toNat ≤ bytes.size →
23    o + 258 ≤ e.o0 + e.sm0.avail_out.toNat → bytes.size < 2 ^ 63 →
24    l.broke = false → (3 ≤ l.len.toNat ∧ l.len.toNat ≤ 258) →
25    15 ≤ l.bits.toNat →
26    (i + 2 ≤ e.i0 + e.sm0.avail_in.toNat ∨
27      (i + 1 ≤ e.i0 + e.sm0.avail_in.toNat ∧ 20 ≤ l.bits.toNat)) →
28    Origin.Inv e l.hold.toNat l.bits.toNat i used →
29    ∃ (l' : L) (after : Heap),
30      C.run (dolenDist c l) (e.heap bytes msg mode) = .ok (l', after) ∧
31      (∃ entry consumed,
32        consumed ≤ 15 ∧
33        DistLook e l.hold.toNat (l.hold.toNat % 2 ^ e.s0.distbits.toNat) entry consumed ∧
34        DistEnd e bytes msg mode ((Sg e l.hold.toNat l.bits.toNat i).drop consumed)
35          i o l.len.toNat entry l' after) ∧
36      ∃ i' o' used',
37        LS e l' i' o' ∧ Origin.Inv e l'.hold.toNat l'.bits.toNat i' used' ∧ used ≤ used'
38
39end Zlib.Inffast.Spec.DistanceOrigin