InflateFast.lean

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

1import ZlibF.Proof.«inffast.c.len»
2
3/-!
4# Concrete obligations for one fast-decoder iteration
5
6These are internal safety and frame obligations for the actual translated body. The caller must
7establish the table and buffer facts from the decoder invariant. They are not callee contracts
8assumed by an enclosing theorem, and do not assert format correctness for arbitrary safe tables.
9-/
10
11namespace Zlib.Inffast.Spec
12open C Zlib.Inffast
13
14/-- The loop's six-byte and 258-byte margins, and the existing concrete heap/table context.
15`A` is the current output array, with its original allocation size. No function contract occurs
16in this precondition. -/
17structure StepPre (e : Proofs.Env) (c : Ctx) (A : Array UInt8) (l : L) (i o : Nat) : Prop where
18  context : Proofs.CtxOK e c
19  locals : Proofs.LS e l i o
20  outputSize : A.size = e.A0.size
21  inputRoom : i + 6 ≤ e.i0 + e.sm0.avail_in.toNat
22  outputRoom : o + 258 ≤ e.o0 + e.sm0.avail_out.toNat
23  notStopped : l.broke = false
24
25/-- One actual body execution reads at most six bytes and writes at most 258 bytes. A continuing
26iteration writes at least one byte. Only the newly written output interval and the stream's
27message/state mode may change; table storage, input and other allocations are framed by `heap`.
28This is a safety/progress contract, not the still-required Huffman-format refinement. -/
29def StepPost (e : Proofs.Env) (A : Array UInt8) (msg : BPtr) (mode : UInt32)
30    (i o : Nat) (l' : L) (h' : Heap) : Prop :=
31  ∃ i' o' A' msg' mode',
32    Proofs.LS e l' i' o' ∧
33    i ≤ i' ∧ i' ≤ i + 6 ∧ o ≤ o' ∧ o' ≤ o + 258 ∧
34    A'.size = A.size ∧ h' = e.heap A' msg' mode' ∧ l'.againL = false ∧
35    (∀ j, (j < o ∨ o' ≤ j) → A'[j]? = A[j]?) ∧
36    (l'.broke = false → o < o' ∧ msg' = msg ∧ mode' = mode) ∧
37    (l'.broke = true → mode' = TYPE ∨ mode' = BAD)
38
39/-- Safety and progress of the actual fast body on every concrete permitted state. -/
40def Goal.step_safe : Prop :=
41  ∀ (e : Proofs.Env) (c : Ctx) (A : Array UInt8) (msg : BPtr) (mode : UInt32)
42      (l : L) (i o : Nat),
43    StepPre e c A l i o →
44    ∃ l' h', C.run (inflate_fast_body c l) (e.heap A msg mode) = .ok (l', h') ∧
45      StepPost e A msg mode i o l' h'
46
47/-- The complete fast call restores normalized bits and exact remaining input/output counts.
48Only the produced output interval, stream buffer fields/message, and state bits/mode change.
49The internal `Env` table predicates must be established by the main decoder; they do not
50assert RFC decoding for arbitrary safe tables. -/
51def FastPost (e : Proofs.Env) (after : Heap) : Prop :=
52  ∃ (inputUsed outputUsed bufferedBytes : Nat) (bytes : Array UInt8) (msg : BPtr)
53    (mode bits : UInt32) (hold : UInt64),
54    inputUsed + bufferedBytes ≤ e.sm0.avail_in.toNat ∧ bufferedBytes ≤ 3 ∧
55    outputUsed ≤ e.sm0.avail_out.toNat ∧
56    bytes.size = e.A0.size ∧ bits.toNat < 8 ∧ hold.toNat < 2 ^ bits.toNat ∧
57    after = e.r.put
58      { e.h0 with bytes := upd e.h0.bytes e.ob (some bytes), istates := upd e.h0.istates e.stid (some { e.s0 with mode, bits, hold }) }
59      { e.sm0 with next_in := .ref (.blk e.ib) (e.i0 + inputUsed), next_out := .ref (.blk e.ob) (e.o0 + outputUsed), avail_in := UInt32.ofNat (e.sm0.avail_in.toNat - inputUsed), avail_out := UInt32.ofNat (e.sm0.avail_out.toNat - outputUsed), msg } ∧
60    (∀ index, (index < e.o0 ∨ e.o0 + outputUsed ≤ index) → bytes[index]? = e.A0[index]?) ∧
61    ((mode = e.s0.mode ∧ msg = e.sm0.msg) ∨ (mode = TYPE ∧ msg = e.sm0.msg) ∨ mode = BAD) ∧
62    (mode ≠ TYPE → mode ≠ BAD →
63      e.sm0.avail_in.toNat - inputUsed < 6 + bufferedBytes ∨
64      e.sm0.avail_out.toNat - outputUsed < 258)
65
66/-- Safety, termination, frame and exact register writeback of the actual whole fast decoder.
67No body/callee contract is a hypothesis. The complete format-refinement goal is separate. -/
68def Goal.fast_safe : Prop :=
69  ∀ e : Proofs.Env, ∃ after,
70    C.run (inflate_fast e.strm e.start) e.h0 = .ok ((), after) ∧ FastPost e after
71
72end Zlib.Inffast.Spec