add slot locked disperser

.gitmodules

@@ -0,0 +1,9 @@
+[submodule "contracts/lib/forge-std"]
+	path = contracts/lib/forge-std
+	url = https://github.com/foundry-rs/forge-std
+[submodule "contracts/lib/foundry-huff"]
+	path = contracts/lib/foundry-huff
+	url = https://github.com/huff-language/foundry-huff
+[submodule "contracts/lib/halmos-cheatcodes"]
+	path = contracts/lib/halmos-cheatcodes
+	url = https://github.com/a16z/halmos-cheatcodes

contracts/.gitignore

@@ -1,3 +1,4 @@
 out/
 cache/
 broadcast/
+.venv-halmos/

contracts/README.md

@@ -1,88 +1,42 @@
-# PaymentForwarder
+# contracts
 
-```
-0xFEEEEEE44046c3f61a8CC081E0918eF0de0a7ffC
-```
-
-Same address on every chain: deployed with the canonical deterministic-deployment
-proxy (`0x4e59b44847b379578588920cA78FbF26c0B4956C`) under a mined salt.
-
-## Why
-
-A proposer payment sent as a plain transfer is valid in any block. If the block
-it was built for is reorged out, or the slot is missed once the payload is
-public, the signed transfer can be replayed in a later slot and the payer pays
-the previous slot's fee recipient a second time.
-
-Paying through this contract binds the payment to one slot. The recipient and the
-expected timestamp travel in the calldata, and the call reverts unless
-`block.timestamp` matches.
+Slot-locked payment contracts: bind a payment to the one block/slot it was
+built for, so a payment exposed by a reorg or a missed slot can't be
+replayed into a later slot.
 
-## The contract
+- **[PaymentForwarder](docs/PaymentForwarder.md)** — forwards the contract's
+  entire balance to a single recipient. 20 bytes of runtime, deployed at the
+  same address on every chain, the canonical payment contract relays
+  validate against.
+- **[SlotLockedDisperser](docs/SlotLockedDisperser.md)** — pays N recipients
+  and refunds the caller's leftover in one atomic call, for splitting a Merged block's added value between several contributors instead of forwarding to one.
 
-20 bytes of runtime, in full:
+## Development
 
-```
-5f358060e01c4218600f5760401cff5b5f5ffd00
+Requires [forge](https://getfoundry.sh). `SlotLockedDisperser` additionally
+needs [`huffc`](https://docs.huff.sh/get-started/installing/) (`PaymentForwarder`
+tests run against a committed runtime and don't need it).
 
-PUSH0 CALLDATALOAD    // calldata word: [uint32 timestamp][20-byte recipient]
-DUP1 PUSH1 0xe0 SHR   // timestamp
-TIMESTAMP XOR         // zero if it matches
-PUSH1 0x0f JUMPI      // otherwise revert
-PUSH1 0x40 SHR        // recipient
-SELFDESTRUCT          // send balance to recipient
-JUMPDEST PUSH0 PUSH0 REVERT
+```bash
+forge test
+forge snapshot    # refresh .gas-snapshot
 ```
 
-Since EIP-6780 `SELFDESTRUCT` just sends the balance to the recipient. A payment
-costs at most 29,022 gas, or 54,022 when the recipient account does not exist
-yet, and does not depend on the recipient's code; zero bytes in the calldata come
-in a few gas under. That figure is also the minimum viable gas limit, since
-nothing is held in flight. The recipient is not executed, so nothing can be left
-in the contract and a recipient that would reject a transfer is still paid.
-
-Calldata is not forwarded and there is no length check: a payment that omits the
-recipient sends the balance to the zero address, so callers must encode all 24
-bytes.
+### Formal verification (Halmos)
 
-## Payment verification
+`SlotLockedDisperser` can't use the SELFDESTRUCT that PaymentForwarder uses so extra steps have been taken to ensure it's safe to use. It's properties are proven, not sampled, with
+[Halmos](https://github.com/a16z/halmos) — see
+[docs/SlotLockedDisperser.md](docs/SlotLockedDisperser.md#formal-verification)
+for what's proven. Install:
 
-This is the canonical payment contract for builders, so a relay validating a
-submission has to accept it alongside a direct transfer.
-
-`ensure_payment` prefers the fee recipient's balance delta, which is unaffected
-by the forwarder. When that check does not cover the bid, the fallback inspects
-the last transaction, and a forwarded payment does not look like a transfer: `to`
-is the forwarder and the calldata is not empty. The fallback therefore accepts
-either shape:
-
-- `to` is the fee recipient with empty calldata, or
-- `to` is `PAYMENT_FORWARDER` and the recipient in its calldata is the fee
-  recipient
-
-with the value equal to the bid in both cases. A successful receipt for the
-second shape means the balance reached the recipient, since the contract has no
-other path to success.
-
-## Bid adjustments
-
-An adjustment rewrites the payment from the relay's own fee payer. The contract
-does not authenticate the sender, so it can keep every field of the original
-payment except the nonce and the value.
-
-Keeping `to` and the calldata is what an implementation must do: the substituted
-transaction then costs exactly the gas the builder reported, so the header
-`gas_used`, the payment receipt's `cumulative_gas_used` and the fee payer's
-balance all stay consistent without re-estimating anything. Replacing a forwarded
-payment with a direct transfer changes its gas and invalidates the block.
-
-## Development
+```bash
+python3 -m venv .venv-halmos && .venv-halmos/bin/pip install halmos
+```
 
-Foundry project, not wired into the Rust build. Requires
-[forge](https://getfoundry.sh). The tests run against the committed runtime, so
-no Huff compiler is needed to verify behaviour.
+Run (`--ffi` lets `HuffDeployer` shell out to `huffc`, off by default in
+Halmos; `--loop` raises the loop-unrolling bound past its default of 2,
+enough to cover the largest recipient count checked):
 
 ```bash
-forge test
-forge snapshot    # refresh .gas-snapshot
+.venv-halmos/bin/halmos --contract SlotLockedDisperserSymbolicTest --ffi --loop 27
 ```

contracts/docs/PaymentForwarder.md

@@ -0,0 +1,84 @@
+# PaymentForwarder
+
+```
+0xFEEEEEE44046c3f61a8CC081E0918eF0de0a7ffC
+```
+
+Same address on every chain: deployed with the canonical deterministic-deployment
+proxy (`0x4e59b44847b379578588920cA78FbF26c0B4956C`) under a mined salt.
+
+## Why
+
+A proposer payment sent as a plain transfer is valid in any block. If the block
+it was built for is reorged out, or the slot is missed once the payload is
+public, the signed transfer can be replayed in a later slot and the payer pays
+the previous slot's fee recipient a second time.
+
+Paying through this contract binds the payment to one slot. The recipient and the
+expected timestamp travel in the calldata, and the call reverts unless
+`block.timestamp` matches.
+
+## The contract
+
+20 bytes of runtime, in full:
+
+```
+5f358060e01c4218600f5760401cff5b5f5ffd00
+
+PUSH0 CALLDATALOAD    // calldata word: [uint32 timestamp][20-byte recipient]
+DUP1 PUSH1 0xe0 SHR   // timestamp
+TIMESTAMP XOR         // zero if it matches
+PUSH1 0x0f JUMPI      // otherwise revert
+PUSH1 0x40 SHR        // recipient
+SELFDESTRUCT          // send balance to recipient
+JUMPDEST PUSH0 PUSH0 REVERT
+```
+
+Since EIP-6780 `SELFDESTRUCT` just sends the balance to the recipient. A payment
+costs at most 29,022 gas, or 54,022 when the recipient account does not exist
+yet, and does not depend on the recipient's code; zero bytes in the calldata come
+in a few gas under. That figure is also the minimum viable gas limit, since
+nothing is held in flight. The recipient is not executed, so nothing can be left
+in the contract and a recipient that would reject a transfer is still paid.
+
+Calldata is not forwarded and there is no length check: a payment that omits the
+recipient sends the balance to the zero address, so callers must encode all 24
+bytes.
+
+## Payment verification
+
+This is the canonical payment contract for builders, so a relay validating a
+submission has to accept it alongside a direct transfer.
+
+`ensure_payment` prefers the fee recipient's balance delta, which is unaffected
+by the forwarder. When that check does not cover the bid, the fallback inspects
+the last transaction, and a forwarded payment does not look like a transfer: `to`
+is the forwarder and the calldata is not empty. The fallback therefore accepts
+either shape:
+
+- `to` is the fee recipient with empty calldata, or
+- `to` is `PAYMENT_FORWARDER` and the recipient in its calldata is the fee
+  recipient
+
+with the value equal to the bid in both cases. A successful receipt for the
+second shape means the balance reached the recipient, since the contract has no
+other path to success.
+
+## Bid adjustments
+
+An adjustment rewrites the payment from the relay's own fee payer. The contract
+does not authenticate the sender, so it can keep every field of the original
+payment except the nonce and the value.
+
+Keeping `to` and the calldata is what an implementation must do: the substituted
+transaction then costs exactly the gas the builder reported, so the header
+`gas_used`, the payment receipt's `cumulative_gas_used` and the fee payer's
+balance all stay consistent without re-estimating anything. Replacing a forwarded
+payment with a direct transfer changes its gas and invalidates the block.
+
+## Development
+
+Unlike `SlotLockedDisperser`, tests run against the committed runtime
+(`hex"..."`, hardcoded in `test/PaymentForwarder.t.sol`), so no Huff compiler
+is needed to verify behaviour — see the top-level README for the general
+`forge test` / `forge snapshot` workflow.

contracts/docs/SlotLockedDisperser.md

@@ -0,0 +1,102 @@
+# SlotLockedDisperser
+
+Multi-recipient generalization of [`PaymentForwarder`](PaymentForwarder.md):
+pays N recipients in one call instead of one, for the case where a single
+block's extra value needs splitting between several parties (a relay's own
+fee, several contributing builders, the proposer) rather than forwarded to
+one. Same slot-lock idea, same underlying threat (a payment exposed by a
+reorg or a missed slot must not be replayable in a later slot), but `CALL`
+in a loop instead of a single `SELFDESTRUCT`, since more than one recipient
+needs paying. Not yet deployed.
+
+## Why not just N `PaymentForwarder` calls
+
+Sending N separate slot-locked payments doesn't get you atomicity: if
+recipient 3 of 5 can't be paid, 1 and 2 already were, and the tx that would
+have reverted the whole batch doesn't exist. `SlotLockedDisperser` pays all
+recipients and refunds the caller's leftover in one call, atomically — all
+of it happens or none of it does.
+
+## Calldata
+
+```
+Offset 0..3:    uint32 timestamp   (must equal block.timestamp)
+Offset 4..23:   recipient 1        (20 bytes)
+Offset 24..55:  amount 1           (32 bytes)
+Offset 56..75:  recipient 2        (20 bytes)
+Offset 76..107: amount 2           (32 bytes)
+... repeating [20-byte address][32-byte amount] ...
+```
+
+No function selector, no length check on the trailing entry — same
+calldata-is-caller-constructed assumption as `PaymentForwarder`. Any leftover
+balance after all recipients are paid is refunded to `msg.sender`.
+
+## Guarantees
+
+- **Atomic.** Either every recipient is paid and the caller gets the exact
+  leftover refund, or the entire call reverts and the contract's balance is
+  untouched.
+- **Block-locked**, same mechanism as `PaymentForwarder`: reverts with
+  `TimestampMismatch()` unless the first 4 bytes of calldata equal
+  `block.timestamp`.
+- **Reentrancy-guarded.** Unlike `PaymentForwarder`, this contract pays via
+  `CALL` (a loop needs to keep going after paying each recipient, which
+  `SELFDESTRUCT` doesn't allow), so a malicious recipient's `receive()` could
+  otherwise reenter mid-loop — `CALL` forwards all remaining gas — and
+  redirect funds meant for other recipients or the refund. A storage-backed
+  lock blocks any nested call while one is in flight. Costs ~2.3k gas per
+  call (the lock is set then cleared within the same tx, so the EIP-3529
+  refund cancels out most of the base `SSTORE` cost).
+- **No access control**, same reasoning as `PaymentForwarder`'s "anyone may
+  pay": nothing checks `msg.sender`, recipients/amounts are fully
+  caller-controlled. Safe only because the contract is never expected to
+  hold a balance at rest.
+
+Revert reasons decode as custom errors, not a bare `revert(0,0)`:
+
+```solidity
+error AlreadyEntered();                    // reentrancy guard tripped
+error TimestampMismatch();                 // calldata timestamp != block.timestamp
+error TransferFailed(address recipient);   // named recipient's CALL failed,
+                                            // including the final refund-to-caller CALL
+```
+
+`TransferFailed` names whichever `CALL` failed first — useful for identifying
+a misbehaving recipient after a failed pre-inclusion simulation without a
+tracer. Survives most gas-griefing attempts too: EIP-150 only forwards
+63/64ths of remaining gas to a `CALL`, so the outer contract keeps a 1/64th
+sliver — usually enough to still name the culprit before reverting.
+
+## Known accepted trade-offs
+
+- **Gas griefing.** `CALL` forwards all remaining gas uncapped, so one
+  adversarial or merely gas-hungry recipient can force the whole batch to
+  revert, blocking payment to every other recipient in the same call.
+  Alternatives (capped gas, pull-based claims) trade away either legitimate
+  contract-wallet recipients or atomicity; accepted as-is since the caller
+  controls calldata construction and can react out-of-band.
+- **Misaligned calldata** (trailing entry not an exact 20+32-byte multiple)
+  burns gas via an unbounded loop rather than failing fast, since `offset`
+  never exactly equals `calldatasize`. Not reachable if the caller
+  constructs calldata correctly.
+
+## Formal verification
+
+`test/SlotLockedDisperser.symbolic.t.sol` proves properties with
+[Halmos](https://github.com/a16z/halmos) across the full input space rather
+than sampling concrete cases: value conservation (exact accounting between
+recipients and the caller's refund, for any address/amount/starting balance,
+at recipient counts up to the real usage bound), the reentrancy lock
+rejecting any nested call regardless of content, a timestamp mismatch never
+mutating state, and conservation holding even against a recipient that
+always tries to reenter with arbitrary calldata/value. See the test file's
+comments for what's proven at which bound and why (mutually-distinct
+*symbolic* addresses hit a solver wall around N=5-6; fixing concrete
+addresses and leaving amounts symbolic scales the same property to N=25).
+
+## Development
+
+Needs [`huffc`](https://docs.huff.sh/get-started/installing/) — tests deploy
+via `HuffDeployer`, which shells out to it (`ffi = true` in `foundry.toml`).
+See the top-level README for the Halmos setup/invocation.

contracts/foundry.lock

@@ -0,0 +1,11 @@
+{
+  "lib/forge-std": {
+    "tag": {
+      "name": "v1.16.2",
+      "rev": "bf647bd6046f2f7da30d0c2bf435e5c76a780c1b"
+    }
+  },
+  "lib/foundry-huff": {
+    "rev": "7d1ce15ccf92bd68458c7e28e0ae847b64b4fc74"
+  }
+}

contracts/foundry.toml

@@ -5,13 +5,23 @@ test = "test"
 script = "script"
 libs = ["lib"]
 solc_version = "0.8.30"
-evm_version = "prague"
+evm_version = "osaka"
 optimizer = true
 optimizer_runs = 1000000
 # Strip metadata so the runtime bytecode is reproducible byte-for-byte and the
 # CREATE2 address is stable.
 bytecode_hash = "none"
 cbor_metadata = false
+# SlotLockedDisperser.huff needs both: HuffDeployer (foundry-huff) shells out to
+# huffc, and Halmos needs the AST in build artifacts (not included by default).
+ffi = true
+ast = true
+
+remappings = [
+    "forge-std/=lib/forge-std/src/",
+    "foundry-huff/=lib/foundry-huff/src/",
+    "halmos-cheatcodes/=lib/halmos-cheatcodes/src/",
+]
 
 [profile.default.fuzz]
 runs = 1024