Repository navigation
refactor(evm): drive EVM send and receive from state-machine tables - #344
Conversation
EvmSendMachine and EvmReceiveMachine (solver-core/core/evmSwapState.ts) replace the hand-written state unions and NON_TERMINAL/EXPOSED lists. They stay in solver-core because the planners type against them. EVM_*_NON_TERMINAL and EVM_*_EXPOSED are now aliases of the machine's lists, so importers are untouched. Behaviour change: EvmSwapStore.transition() now rejects an edge the machine lacks, before its CAS. Until now it had no edge check at all. The edges are exactly the `Edges` tables in spec/tla/EvmSend.tla and EvmReceive.tla, and test/core/evmMachines.test.ts pins them. Every production transition (both orchestrators, plus operator park from any live state to stuck) is an edge. Test fixtures relied on shortcuts production never takes (quoted->funded, quoted->awaiting_lock, quoted->refunding_evm, funding_arkade->refunding_arkade). Chains that only passed through a dead state now take the legal edge. Tests that need a row resting in `funded`/`awaiting_lock`/`locked` (planner states no transition enters) seed it via test/evm/fixtures/seedState.ts. Adding inbound edges to the machine was rejected: it would admit edges production never takes and diverge from the TLA+ models.
planEvmSend returned lock_evm from `funded` unconditionally, with no valid_until or refund-locktime check. An audit flagged this: a row that stalled in `funded` would lock the ERC20 late, possibly after the client's Arkade refund opened, letting the client take both legs. Not reachable today: no EVM code path writes `funded`, and the machine now has no edge into it. The fix is defence in depth. `funded` gets the same RULE 5 gate as quoted's funded branch. Quoting already enforces valid_until < refund_locktime, so the gate also keeps a late lock out of the refund race. Past the deadline the row is refused, which routes the lockup to the covenant refund. The machine and spec/tla/EvmSend.tla gain funded -> refused. RefuseQuoted now also fires from `funded`, and SubmitEvmLock from `funded` requires ~QuoteStale. TLC was not re-run: `funded` is unreachable in the model too, so the green cfg's state space is unchanged.
|
Important
This repository does not receive automatic reviews because it has fewer than 10 stars.
|
EvmSendSwapService.quote() reserved house-wide headroom before the uncached
fetchPrice and held it across the feed's round trip, contradicting its own
comment ("Taken HERE rather than before the price fetch, deliberately").
Every in-flight quote therefore pinned headroom on every corridor for the
feed's latency. That is part of an audit finding: unfunded quotes from free
Nostr identities can saturate maxExposedSats.
The reservation now comes after pricing and the token-unit range check, and
before payoutFunding.prepareQuote. Moving it right before the insert was
rejected: a quote the cap refuses would then reserve provider liquidity only
to abandon it. Atomicity is unchanged: reserve() still claims in one
serialised step and is held until the row lands.
This only shrinks the in-flight window. The main part of the finding, quoted
rows holding the cap for quoteValiditySeconds, is house-wide and not fixed here.
The test merged from main walked quoted -> funded -> locking_evm. The EVM send machine has no edge into funded, so it now goes straight to locking_evm.
arkana-ai-bot
left a comment
There was a problem hiding this comment.
Review: refactor(evm) drive EVM send/receive from state-machine tables
Reviewed at 277a7a5. Diff read in full; full files for evmSwapState.ts, stateMachine.ts, evmSwapStore.ts, evmSendPlan.ts, evmReceivePlan.ts, evmOrchestrator.ts and the TLA+ spec fetched from the head SHA. No consumers of the renamed symbols were found in the other SDK repos under /srv/arkana/repos.
✅ What is correct
Reservation ordering fix (evmOrchestrator.ts ~line 612–653):
The old code held admission.reserve() across the fetchPrice round-trip, serialising every concurrent quote behind feed latency and contradicting its own comment. The new order—fetchPrice → limits checks → reserve → prepareQuote—is correct. Early-return paths (price_unavailable, payout_below_dust, amount_out_of_range) now fire before the reservation is taken, so no headroom is claimed for quotes that would be refused anyway on price grounds. The new test 'holds no headroom while the price feed is answering' in test/send/evmQuote.test.ts pins exactly this property. Good.
funded → refused edge (evmSendPlan.ts case 'funded' + evmSwapState.ts + EvmSend.tla):
Applying RULE 5 to the funded state is the correct money-path addition: funding observed after valid_until now refuses rather than locking at a stale rate. The TLA+ RefuseQuoted and SubmitEvmLock actions are updated consistently—RefuseQuoted gains the Saw(w, s, "funded") ∧ QuoteStale branch, and SubmitEvmLock's funded branch gains ~QuoteStale. Both are symmetric with the existing quoted/funded handling. The planner tests cover the boundary at NOW + 60 and REFUND_LOCKTIME.
Machine-enforced edges (evmSwapStore.ts):
Rejecting illegal edges at call time rather than silently no-oping is a strict improvement. The edge check fires before the SQL UPDATE, so a caller bug is loud before any state change.
Test migration (seedState.ts, updated orchestrator/db tests):
Using direct SQL to seed dead states (funded, awaiting_lock, locked) rather than routing through the machine is the right choice—these states are now unreachable via transition() but must still be handled for in-flight rows on upgrade. The comment in seedState.ts is clear.
EVM_*_NON_TERMINAL / EVM_*_EXPOSED as machine aliases: backward-compatible; external consumers see the same exported symbol names.
🔴 Gate item (should block merge)
TLC not re-run (spec/tla/EvmSend.tla):
The PR adds funded → refused to Edges and a new Saw(w, s, "funded") ∧ QuoteStale branch to RefuseQuoted. The PR argues funded is unreachable in the model, so the state space is unchanged—that reasoning is likely sound, but it has not been verified. This change is to the normative spec that the machine test (test/core/evmMachines.test.ts line 455) explicitly cross-references. The spec and the implementation are now tightly coupled, which is exactly the right design; the consequence is that a spec change without a TLC run leaves the coupling unverified. Run EvmSend.cfg before merging.
🟡 Issues worth fixing
legalEdges[from] can produce a confusing TypeError (evmSwapStore.ts line ~264):
if (!this.shape.legalEdges[from].includes(to)) {legalEdges is typed Readonly<Record<State, readonly State[]>>. TypeScript won't prevent a row in the DB carrying a state string that predates or postdates the machine (migration gap, hand-edit, forward-compat). If from is not a key, legalEdges[from] is undefined and .includes() throws a TypeError, not the descriptive illegal transition error. A one-liner fix:
if (!(this.shape.legalEdges[from] ?? []).includes(to)) {or assert the lookup before using it. The machine-derived legalEdges will always cover the full state union for well-formed rows, but a row with a stale/unknown state should emit the named error.
locked state in receive planner has no valid_until guard (evmReceivePlan.ts line ~159):
case 'locked':
return { do: 'fund_arkade' }locked is a dead state on the receive side (symmetric with funded on send), so this cannot trigger today. But the machine now explicitly permits locked → refused, and the send side's funded case was updated. If locked ever becomes reachable again, the planner will fund Arkade at a stale rate. Consider adding the symmetric guard:
case 'locked':
if (seen.nowSeconds >= row.validUntil) {
return { do: 'refuse', reason: 'ERC20 lock observed after the quote expired' }
}
return { do: 'fund_arkade' }Not blocking, but it closes the gap the PR opens on the send side while leaving it open on the receive side.
🔵 Observations / nits
-
seedState.tsaccessesdriverandshapeviastore as unknown as { ... }.driverisprotected,shapeisprivate; both are cast away. Acceptable for a test-only helper—the comment makes the intent clear. Ifshapeis ever renamed, this silently breaks. A single integration test onseedStateitself (round-trips a seeded state and reads it back) would catch that. -
The test fixture at
test/core/evmMachines.test.tsline 471 asserts terminal order:expect(EvmSendMachine.terminal).toEqual(['claimed', 'refunded', 'refused', 'stuck'])
defineMachinebuildsterminalfromObject.keys(table)order. This assertion is fragile to key reordering in theEvmSendMachinedefinition. Usingexpect.arrayContainingor sorting would be more robust. -
The PR description calls
funded,awaiting_lock, andlockeddead states and flags their removal as a follow-up. Tracking that work (the dead states still appear inEVM_SEND_NON_TERMINAL/EVM_RECEIVE_NON_TERMINALand therefore count against the cap) would be helpful.
Summary
The reservation-ordering fix and funded → refused guard are both correct and well-tested. The machine-enforced edge table is an improvement. TLC must be run on EvmSend.cfg before this merges. The legalEdges[from] defensive fix is small and worth doing. Everything else is non-blocking.
arkana-ai-bot
left a comment
There was a problem hiding this comment.
6 commits merged since 277a7a5 (4 from main via merge commit, 2 branch-specific); 0 of 5 prior open issues fixed; 1 prior gate item still blocking.
Prior-finding closure
1. TLC not re-run on EvmSend.tla (gate item) — Still open.
spec/tla/EvmSend.tla did not change between 277a7a5 and 8c8c04b3db. The green-run comment still records the pre-funded→refused figures (22,039,291 generated / 2,841,354 distinct / depth 48). No new TLC run has been recorded. The PR description still says "TLC was not re-run." This remains a merge blocker.
2. legalEdges[from] can produce TypeError (evmSwapStore.ts:253) — Still open. Code unchanged:
if (!this.shape.legalEdges[from].includes(to)) {If a row carries an unknown or stale state string, legalEdges[from] is undefined and .includes() throws a TypeError rather than the named illegal transition error.
3. locked state has no valid_until guard in receive planner (evmReceivePlan.ts:160–161) — Still open. Code unchanged.
4. seedState.ts fragile driver/shape cast — Still open. Code unchanged.
5. Terminal-order assertion fragility (test/core/evmMachines.test.ts:62) — Still open.
expect(EvmSendMachine.terminal).toEqual(['claimed', 'refunded', 'refused', 'stuck'])Still a brittle key-order assertion rather than expect.arrayContaining.
Incremental-diff findings
What actually changed on the branch
Two branch-specific commits since 277a7a5:
3512288454— fix(evm-send): take the exposure reservation after the price fetch8c8c04b3db— test(evm-send): seed #318's claim-scan test through a legal edge
Plus a merge of four main-branch commits (3e2cb0f5, e6959b65, 68538941, via merge commit 362ee130). I have not re-reviewed those main-branch changes; they are outside this PR's scope.
capture/unwrap utility — correct
packages/solver-core/src/util/capture.ts is a clean observable-rejection pattern. It attaches .then/.catch immediately so the promise is never "unobserved" for the duration of a concurrent await. The two new unhandled-rejection tests pin this:
test/receive/evmOrchestrator.test.ts—'a failing preimage read beside the depth probe'test/send/evmOrchestrator.test.ts—'a failing claim scan beside the depth probe'
Both correctly use a raw async () => { throw ... } rather than vi.fn().mockRejectedValue, so the rejection is genuinely unobserved if the fix is absent. Good.
One subtlety to verify: in the send tick() IIFE, EvmClaimVerificationError is explicitly re-thrown before capture sees the settled state — meaning capture will catch it as { ok: false } and unwrap will rethrow it. The test (proofError is an EvmClaimVerificationError) confirms this round-trips cleanly. ✓
Reservation ordering — correct and now tested
send/evmOrchestrator.ts now sequences: fetchPrice → evmAmount checks → reserve → prepareQuote. The new test 'holds no headroom while the price feed is answering' in test/send/evmQuote.test.ts verifies the reservation is not held across the feed round-trip. This is the fix I described as correct in the prior review. ✓
🟡 Nit: traceP starts before the duplicate check (send/evmOrchestrator.ts:585–586)
const tipP = this.deps.timelockHeight()
const traceP = capture(this.deps.assertClaimTraceSupport(hex.decode(token.address.slice(2))))
// ...
const spokenFor = await Promise.all([store.findLiveByPaymentHash(...), ...])
if (spokenFor.some(Boolean)) return { accepted: false, reason: 'duplicate_swap' }
const trace = await tracePassertClaimTraceSupport fires before the duplicate check. A retry storm against a known payment hash launches a chain call per attempt. Not a correctness issue, but inverting the order (duplicate check → start traceP) would be cheap and would make the guard more defensive. Non-blocking.
watch() parallelisation — correct
Promise.allSettled([presentP, claimedP]) with explicit status checks correctly propagates rejections from either branch without leaving a dangling rejection. The chained .then on claimScanFloor correctly defers findClaimPreimage until the floor is known while still running in parallel with isLocked. ✓
Summary
The two branch-specific commits are correct: the unhandled-rejection fix using capture/unwrap is sound, the new tests are well-targeted, and the reservation-ordering fix is now implemented and pinned. No new protocol or money-path issues introduced.
The gate item from the prior review — running TLC on EvmSend.cfg to verify the funded→refused spec change — is still open and still blocks merge. The other four findings are non-blocking.
|
Following up on the open items from the last review:
Nit, |
|
TLC on |
arkana-ai-bot
left a comment
There was a problem hiding this comment.
2 commits since last pass (126ff8c, d38d305); 1 of 5 prior issues fixed; gate item still blocking; no new findings.
Prior-finding closure
1. TLC not re-run on EvmSend.tla (gate item) — Still open.
Neither spec/tla/EvmSend.tla nor any recorded TLC output changed. The funded → refused branch added to RefuseQuoted and the ~QuoteStale guard on SubmitEvmLock remain unverified by the model checker. Must be run before merge.
2. legalEdges[from] can produce TypeError (evmSwapStore.ts:253) — Fixed in d38d305.
if (!this.shape.legalEdges[from]?.includes(to)) {Optional chaining is the right one-liner: legalEdges[unknown] → undefined; undefined?.includes(to) → undefined; !undefined → true; named error thrown. The companion test in 126ff8c ('names a state the machine does not know rather than crashing on it') uses 'legacy' as never as the from-state and asserts /illegal transition legacy -> refused/ — it correctly covers exactly the class the fix is protecting against. ✓
3. locked state has no valid_until guard in receive planner (evmReceivePlan.ts:~160) — Still open. Code unchanged. If locked ever becomes reachable again the planner will fund Arkade at a stale rate. Non-blocking but the gap is now asymmetric with the send side's funded case.
4. seedState.ts fragile driver/shape cast — Still open. Non-blocking.
5. Terminal-order assertion fragility (test/core/evmMachines.test.ts) — Still open. toEqual(['claimed', 'refunded', 'refused', 'stuck']) is brittle to key-reorder. Non-blocking.
Incremental findings
None. The two new commits are surgical: one adds a regression test, one applies the ?. fix. No new paths, no logic change outside the guard.
TLC must run on EvmSend.cfg before this merges. Items 3–5 remain non-blocking.
Moves the two EVM legs onto
defineMachine, the pattern LN send, LN receive and onchain send already use (#326). After this PR, asset RFQ and offer fills are the only lifecycles still using hand-written edge tables.Breaking / behaviour change
EvmSwapStore.transition()used to have no edge check at all, only the CAS onfrom. It now throwsillegal transition X -> Yfor any edge the machine lacks, the same wayBaseSwapStoredoes. The edges are exactly theEdgestables inspec/tla/EvmSend.tlaandEvmReceive.tla, andtest/core/evmMachines.test.tspins them to the spec. I checked every production transition by hand: both orchestrators, plus operator park from any live state tostuck. All of them are edges.Money-path correction
planEvmSendlocked the ERC20 fromfundedwithout checkingvalid_until(raised in an audit). It is not reachable today, because nothing writesfunded, and after this PR the machine also rejects any edge into it.fundednow gets the same RULE 5 gate as quoted's funded branch: past the deadline it refuses, which routes the lockup to the covenant refund. The machine and spec gainfunded -> refused.Reservation held across the price fetch.
EvmSendSwapService.quote()reserved house-wide headroom before the uncachedfetchPrice, which contradicted its own comment. It now reserves after pricing and beforepayoutFunding.prepareQuote, so a quote refused by the cap never reserves provider liquidity. Atomicity is unchanged.Changes
EvmSendMachineandEvmReceiveMachinelive insolver-core/core/evmSwapState.ts, because the planners type against them.EVM_*_NON_TERMINALandEVM_*_EXPOSEDbecome aliases of the machine's lists, so importers don't change.TERMINALlists now come from the machine.quoted->funded,quoted->awaiting_lock,quoted->refunding_evm,funding_arkade->refunding_arkade). Chains through a dead state now take the legal edge. Rows that must rest infunded,awaiting_lockorlockedare seeded viatest/evm/fixtures/seedState.ts.Known gaps
EvmSend.tlachange.fundedis unreachable in the model too, so the green cfg's state space should be unchanged, but someone should runEvmSend.cfgbefore merge.funded,awaiting_lockandlockedare dead states. Removing them is a follow-up.Gates
pnpm -r build,pnpm typecheck,pnpm test(6494 passed),pnpm format:check: all green locally.