Skip to content

refactor(evm): drive EVM send and receive from state-machine tables - #344

Merged
d4rp4t merged 7 commits into
mainfrom
refactor/evm-state-machine
Nov 13, 2026
Merged

d4rp4t merged 7 commits into
mainfrom
refactor/evm-state-machine

Conversation

@d4rp4t

@d4rp4t d4rp4t commented Nov 9, 2026 •

Copy link
Copy Markdown
Contributor

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 on from. It now throws illegal transition X -> Y for any edge the machine lacks, the same way BaseSwapStore does. The edges are exactly the Edges tables in spec/tla/EvmSend.tla and EvmReceive.tla, and test/core/evmMachines.test.ts pins them to the spec. I checked every production transition by hand: both orchestrators, plus operator park from any live state to stuck. All of them are edges.

Money-path correction

planEvmSend locked the ERC20 from funded without checking valid_until (raised in an audit). It is not reachable today, because nothing writes funded, and after this PR the machine also rejects any edge into it. funded now 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 gain funded -> refused.

Reservation held across the price fetch. EvmSendSwapService.quote() reserved house-wide headroom before the uncached fetchPrice, which contradicted its own comment. It now reserves after pricing and before payoutFunding.prepareQuote, so a quote refused by the cap never reserves provider liquidity. Atomicity is unchanged.

Changes

  • EvmSendMachine and EvmReceiveMachine live in solver-core/core/evmSwapState.ts, because the planners type against them. EVM_*_NON_TERMINAL and EVM_*_EXPOSED become aliases of the machine's lists, so importers don't change.
  • The planners' TERMINAL lists now come from the machine.
  • 66 tests used edges production never takes (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 in funded, awaiting_lock or locked are seeded via test/evm/fixtures/seedState.ts.

Known gaps

  • TLC was not re-run for the EvmSend.tla change. funded is unreachable in the model too, so the green cfg's state space should be unchanged, but someone should run EvmSend.cfg before merge.
  • funded, awaiting_lock and locked are dead states. Removing them is a follow-up.

Gates

pnpm -r build, pnpm typecheck, pnpm test (6494 passed), pnpm format:check: all green locally.

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.
@coderabbitai

coderabbitai Bot commented Nov 9, 2026 •

Copy link
Copy Markdown
Contributor

Important

  • Trigger review

This repository does not receive automatic reviews because it has fewer than 10 stars.

Run configuration

  • Source mode: Auto
  • Repository: Unavailable
  • Branch: Unavailable
  • File: No configuration file from this repository applied
  • Commit: Unavailable
  • Layers: Organization UI
  • Review profile: CHILL
  • Plan: Advanced
  • Run ID: 6fb3eec5-a5eb-4a4b-921c-76bd4d77d749
  • Autofix · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

Share

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 arkana-ai-bot left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.ts accesses driver and shape via store as unknown as { ... }. driver is protected, shape is private; both are cast away. Acceptable for a test-only helper—the comment makes the intent clear. If shape is ever renamed, this silently breaks. A single integration test on seedState itself (round-trips a seeded state and reads it back) would catch that.

  • The test fixture at test/core/evmMachines.test.ts line 471 asserts terminal order:

    expect(EvmSendMachine.terminal).toEqual(['claimed', 'refunded', 'refused', 'stuck'])

    defineMachine builds terminal from Object.keys(table) order. This assertion is fragile to key reordering in the EvmSendMachine definition. Using expect.arrayContaining or sorting would be more robust.

  • The PR description calls funded, awaiting_lock, and locked dead states and flags their removal as a follow-up. Tracking that work (the dead states still appear in EVM_SEND_NON_TERMINAL / EVM_RECEIVE_NON_TERMINAL and 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 arkana-ai-bot left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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 fetch
  • 8c8c04b3db — 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 traceP

assertClaimTraceSupport 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.

@d4rp4t

d4rp4t commented Nov 13, 2026

Copy link
Copy Markdown
Contributor Author

Following up on the open items from the last review:

  1. TLC on EvmSend.cfg: running now. I will post the counts here when it finishes.
  2. legalEdges[from] can throw a TypeError: fixed. 126ff8c0 adds a test that a state outside the machine is refused with illegal transition legacy -> refused. That test fails on the previous head. d38d305f makes the lookup legalEdges[from]?.includes(to).
  3. locked has no valid_until guard: not reachable. No transition writes locked; evmSwapState.ts lists it as a planner state that no edge enters. Even if it were reached, fund_arkade re-checks the fund window on a fresh height read before its CAS. That code is unchanged by this PR.
  4. seedState.ts cast: this is a test fixture. If driver or shape were renamed, every test that seeds would fail immediately, so the failure would not be silent. Leaving it as is.
  5. Terminal-order assertion: the order is intentional. A machine's lists are in declaration order, and sqlList writes that order into schema text, so the test pins it on purpose. arrayContaining would stop it from catching a reordering.

Nit, traceP before the duplicate check: the overlap is deliberate (#318 overlaps independent reads to shorten the quote path), and quoteLimiter already bounds a retry storm.

@d4rp4t

d4rp4t commented Nov 13, 2026

Copy link
Copy Markdown
Contributor Author

TLC on EvmSend.cfg at head d38d305f, TLC2 2026.11.06 (rev d8fb231), -workers 8: green. 22,039,291 states generated, 2,841,354 distinct, depth 48, no error, 7min 27s. That is exactly the figure in EvmSend.tla's green-run block, so the funded -> refused edge leaves the state space unchanged, as expected with funded unreachable in the model.

@d4rp4t
d4rp4t merged commit 4874f17 into main Nov 13, 2026
19 checks passed

@arkana-ai-bot arkana-ai-bot left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants