InflateFastOrigin.lean

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

1import ZlibF.Proof.«inffast.c.dist»
2
3/-!
4# Provenance of the fast decoder's bit buffer
5
6Scalar bounds do not relate the buffer's value to input already read.
7The origin invariant records both consumed-bit accounting and the actual
8remaining stream. Whole-byte rollback must preserve that exact stream.
9-/
10
11namespace Zlib.Inffast.Spec.Origin
12open C Zlib.Inffast Zlib.Inffast.Proofs
13
14/-- The complete logical input remaining at entry to this fast call. -/
15def initial (e : Env) : List Bool := Sg e e.s0.hold.toNat e.s0.bits.toNat e.i0
16
17/-- Current buffered bits followed by unread bytes are the exact suffix
18after consuming `used` entry bits. The accounting prevents an unrelated
19suffix or guessed buffered value from satisfying the invariant. -/
20structure Inv (e : Env) (hold bits input used : Nat) : Prop where
21  inputLower : e.i0 ≤ input
22  inputUpper : input ≤ e.i0 + e.sm0.avail_in.toNat
23  normalized : hold < 2 ^ bits
24  accounting : used + bits = e.s0.bits.toNat + 8 * (input - e.i0)
25  stream : Sg e hold bits input = (initial e).drop used
26
27def Goal.initial_origin : Prop :=
28  ∀ e : Env, Inv e e.s0.hold.toNat e.s0.bits.toNat e.i0 0
29
30/-- Reading the actual next byte preserves the source suffix without
31consuming any logical bit. This is the data equation used by actual pull. -/
32def Goal.pull_preserves_origin : Prop :=
33  ∀ (e : Env) (hold bits input used : Nat),
34    Inv e hold bits input used → input < e.i0 + e.sm0.avail_in.toNat →
35    Inv e (hold + (e.IN.getD input 0).toNat * 2 ^ bits) (bits + 8) (input + 1) used
36
37/-- Dropping available low bits consumes exactly that entry-stream prefix. -/
38def Goal.drop_preserves_origin : Prop :=
39  ∀ (e : Env) (hold bits input used count : Nat),
40    Inv e hold bits input used → count ≤ bits →
41    Inv e (hold / 2 ^ count) (bits - count) input (used + count)
42
43/-- Returning unused whole bytes restores the exact same remaining input,
44not merely its length. The retained low bits are the actual mask result.
45The byte rollback bound follows from origin accounting and entry bits < 8. -/
46def Goal.rollback_preserves_origin : Prop :=
47  ∀ (e : Env) (hold bits input used : Nat),
48    Inv e hold bits input used →
49    let returned := bits / 8
50    let residual := bits % 8
51    returned ≤ input - e.i0 ∧
52    Sg e (hold % 2 ^ residual) residual (input - returned) = Sg e hold bits input ∧
53    Inv e (hold % 2 ^ residual) residual (input - returned) used
54
55/-- The actual input-byte load and register updates establish the same
56origin relation. The bound is the source pull helper's internal bound. -/
57def Goal.actual_pull_preserves_origin : Prop :=
58  ∀ (e : Env) (bytes : Array UInt8) (msg : BPtr) (mode : UInt32)
59    (l : L) (i o used : Nat),
60    LS e l i o → Inv e l.hold.toNat l.bits.toNat i used →
61    l.bits.toNat ≤ 22 → i < e.i0 + e.sm0.avail_in.toNat →
62    ∃ l',
63      C.run (pull l) (e.heap bytes msg mode) = .ok (l', e.heap bytes msg mode) ∧
64      LS e l' (i + 1) o ∧ Inv e l'.hold.toNat l'.bits.toNat (i + 1) used
65
66/-- The source shift and unsigned count subtraction consume exactly the
67available low bits, with no heap effect or unchecked shift. -/
68def Goal.actual_drop_preserves_origin : Prop :=
69  ∀ (e : Env) (h : Heap) (l : L) (i o used : Nat) (count : UInt32),
70    LS e l i o → Inv e l.hold.toNat l.bits.toNat i used →
71    count.toNat ≤ l.bits.toNat →
72    C.run (do
73      let hold ← shr64 l.hold count.toUInt64
74      pure { l with hold, bits := l.bits - count }) h = .ok (dropL l count, h) ∧
75    LS e (dropL l count) i o ∧
76    Inv e (dropL l count).hold.toNat (dropL l count).bits.toNat i (used + count.toNat)
77
78/-- Actual epilogue pointer rollback and masking preserve the same exact
79stream. This source prefix is checked separately from counter writeback;
80the loop still has to establish origin at its exit. -/
81def Goal.actual_rollback_preserves_origin : Prop :=
82  ∀ (e : Env) (bytes : Array UInt8) (msg : BPtr) (mode : UInt32)
83    (l : L) (i o used : Nat),
84    LS e l i o → Inv e l.hold.toNat l.bits.toNat i used →
85    let returned := l.bits >>> 3
86    let bits := l.bits - (returned <<< 3)
87    let hold := l.hold &&& (((1 : UInt32) <<< bits) - 1).toUInt64
88    C.run (do
89      let input ← subn l.in_ returned
90      let mask ← shl32 1 bits
91      pure (input, l.hold &&& (mask - 1).toUInt64, bits)) (e.heap bytes msg mode) =
92        .ok ((.ref (.blk e.ib) (i - l.bits.toNat / 8), hold, bits), e.heap bytes msg mode) ∧
93    bits.toNat < 8 ∧
94    Inv e hold.toNat bits.toNat (i - l.bits.toNat / 8) used ∧
95    Sg e hold.toNat bits.toNat (i - l.bits.toNat / 8) = Sg e l.hold.toNat l.bits.toNat i
96
97end Zlib.Inffast.Spec.Origin