Claude session 1ae28c85-fa7f-4acc-94e7-3a085e27eda4

I'll read the relevant section of ~/main.tex.

Let me read the base reserve balance section to understand the original mechanism and the soundness argument.

I read Algorithm alg:inclusion-delayed (lines 709–746) along with the base spec (§sec:reservebalance), the precompile (Listing lst:precompile-delayed), and the realtime version for comparison. Here is my assessment.

Verdict: it is not sound. Reserve‑balance increases break it.

The bug is that the inclusion check evaluates the reserve once, as user_reserve = delayed_urb(t.sender, n), and applies that single value to the whole intermediate set 𝓘 — but 𝓘 spans blocks n-k+1 … n, and each of those blocks was actually protected (by its own dip‑detection in Alg. alg:dipdection-delayed) using delayed_urb(·, b) for its block b, not n. When the delayed URB changes across that window, the two diverge.

Why the direction matters

The verified base proof (fixed reserve R) works because **the same R** appears in the inclusion check and in every intermediate dip‑detection: the pool min(R,B) is protected against external draining and against non‑emptying value spends, so it survives to pay the cumulative gas of 𝓘.

With delayed URB:

• delayed_urb(a, m) returns the latest update with pending_block ≤ m-k. As m grows the threshold grows, so a newer (possibly higher) value appears at the later block. So within the window delayed_urb can step up at the transition block.
• Decrease (U_n < U_b for earlier blocks): inclusion uses the smaller U_n ⇒ stricter than what was actually enforced ⇒ conservative ⇒ sound.
• Increase (U_n > U_b): inclusion optimistically uses the new, larger U_n and permits cumulative gas up to min(U_n, B), but during the in‑flight blocks only the old, smaller U_b was protected — so the balance could have been legally spent below what the inclusion check assumed. Unsound.

Concrete counterexample (k = 2)

• Account a, balance B = 130 in state^{n-2} (what consensus sees; x = n-2).
• Block n-2: a updates reserve 100 → 1000 (pending_block = n-2).
• delayed_urb(a, n) (threshold n-2) ⇒ 1000.
• delayed_urb(a, n-1) (threshold n-3) ⇒ 100.
• Block n-1: tx₀ from a, gas 50, transfers value out. Its dip floor is min(100,130)-50 = 50, so it legally drains a to 50. (tx₀'s own inclusion at block n-1 passes: reserve min(100,·)=100 ≥ 50.)
• Block n: t from a, gas 80. 𝓘 = [tx₀, t], tx₀ non‑emptying.
• Inclusion (last branch): reserve = min(1000, 130) = 130 ≥ gas(tx₀)+gas(t) = 50+80 = 130 ✓ → included.
• Execution of t at block n: balance is 50, solvency_condition: 50 ≥ 80 is false → AssertionFailure.

Consensus committed to t, execution cannot charge its gas — the exact unsoundness the spec is supposed to prevent. The drain at n-1 is invisible to consensus (it's after n-2), and it was permitted because block n-1 only protected the old reserve of 100.

This matches why the realtime version is safe

The verified realtime algorithm (alg:inclusion-reconfig-new) processes 𝓘 transaction‑by‑transaction and, on a reconfig, sets min(prev - gasᵢ, urbᵢ). A reconfig can therefore only lower the effective remaining reserve, never retroactively raise the protected pool. The delayed version drops that per‑step capping and substitutes a single end‑of‑window value — which is exactly where it loses soundness on increases.

Fix options

1. Use the minimum over the window in inclusion: user_reserve = min_{b ∈ [n-k+1, n]} delayed_urb(t.sender, b). Increases then take effect for inclusion only once they've been in force across the whole in‑flight window; decreases stay conservative. Both directions become sound.
2. **Equivalently, defer increases by an extra k** — require the value used at block n to have been settled by n-2k+1 so it's stable across all of [n-k+1, n]. (Decreases can stay at the current k delay.)
3. Keep the realtime version's per‑transaction min capping, just sourcing each urbᵢ from delayed_urb.

Option 1 is the smallest change and the one I'd recommend.

One caveat: this is a manual proof‑sketch‑level analysis, and unlike the realtime spec (which links to a Coq proof), the delayed spec doesn't appear to be machine‑checked. Given a soundness counterexample exists, I'd treat formalizing the fixed version in Coq as the bar before relying on it.

Want me to draft the corrected algorithm text (option 1) as an edit to main.tex?