PRT Contracts Review by GCdePaula · Pull Request #273 · cartesi/dave

GCdePaula · 2026-07-20T14:56:50Z

Summary

This PR completes a security, correctness, documentation, test-coverage, and readability review of the PRT dispute game.

The campaign began as a review of the contracts under prt/contracts/, explicitly excluding the implementation semantics of the state-transition function. It produced:

fixes for terminal bond accounting, clock conservation, timeout classification, callback isolation, Match existence, and configuration validation;
a redesign from front-loaded match effort to a back-loaded response discount;
substantial Clock and Match library refactors around explicit phases and centralized invariants;
recalibrated gas allocations and bonds derived automatically from the work reserve;
geometry-independent unit, fuzz, stateful, recursive, gas, and compatibility tests;
a code-aligned dispute-game specification and a permanent audit/review record.

The deployed Tournament ABI and semantic storage layout are preserved. Production bytecode changes intentionally, so deployment artifacts and CREATE2-derived addresses must be regenerated before release.

The off-chain clients ride along only where the contract changes demand it: the Rust node and the Lua client now mirror the contracts' shared timeout classification, and the node adopts the contracts' outputsMerkleRoot naming in its settlement types and schema. No other node behavior changes.

Main security and correctness changes

Terminal bond settlement

Terminal recovery is now bounded, retryable, and idempotent:

The winning claimer receives at most one configured bond.
Any residual tournament balance is burned after a successful payment.
Repeated recovery calls become successful no-ops.
If the recipient rejects or exhausts the payment callback, the full balance and claimer remain available for permissionless retry.
Zero-value payments do not call the recipient.

This closes two related findings:

Successful recovery previously deleted the winning claimer but left the function non-idempotent. In the historical atomic settlement flow, an attacker could recover immediately before application settlement and make the subsequent recovery attempt revert, bricking settlement.
The first claimer of the correct deterministic root could add incorrect Sybil claims and later recover the entire residual losing pool, recycling most of the capital intended to fund the dispute.

The feature/sling-node target already uses staged consensus and catches recovery failure during staging. This PR does not introduce that staged design; it fixes the underlying Tournament behavior and adapts the regression coverage to the target's stageTournamentResult / acceptStagedTournamentResult lifecycle.

Bounded recipient callbacks

Both refund and terminal-payment callbacks are now bounded:

nonzero ETH payments expose at most 50,000 gas to recipient code;
no recipient return data is copied;
PartialBondRefund.ret remains ABI-compatible but is always empty;
failed action refunds do not revert successful tournament progress;
terminal payment failures preserve state for retry;
parent-tournament progress no longer performs unrelated child bond recovery.

This keeps arbitrary recipient behavior outside the critical progress path while preserving the existing per-tournament reentrancy protection.

Clock conservation and timeout partition

The sealed-leaf timeout path previously charged the prospective winner from its stored allowance rather than its live remaining time. Because both clocks run after leaf sealing, this could restore time already consumed during the leaf race.

It also created a window in which both timeout victory and double elimination were valid. Transaction ordering could therefore decide between incompatible outcomes.

The fix:

charges from live remaining time;
centralizes timeout classification into NONE, ONE_WINS, TWO_WINS, and ELIMINATE_BOTH;
uses that classification in the capability view, both timeout mutation paths, and objective leaf-proof resolution;
assigns equality, winnerRemaining == loserOverdue, to ELIMINATE_BOTH;
prevents a proof from overriding an opposite timeout winner or double elimination.

MatchClocks is now the pair-level policy boundary. Clock remains responsible for one-clock arithmetic at an explicit observation instant.

The off-chain clients are aligned with the same classification. The Rust node's garbage collector previously compared the expired side's overdue time against the opponent's static allowance and could wait up to a full allowance longer than the contract to sweep a doubly dead match; it now eliminates exactly on ELIMINATE_BOTH, equality included. Its Hero previously claimed a timeout win on opponent expiry alone, which inside the eliminate-both zone submits a winMatchByTimeout the contract rejects; it now acts only when the classification names its side the winner. The Lua client's gc and honest strategy carried the same two gates and received the identical fix.

Back-loaded response effort

The former design granted matchEffort when commitments were paired. A fresh or late commitment could therefore receive bankable time before doing any useful work.

Pairing and survivor re-entry now grant no time. Instead, every successful bisection response, including final leaf or inner sealing, receives a non-bankable response discount:

newBalance = startingBalance - max(elapsed - responseBudget, 0)

The response must still arrive before the starting balance expires. The discount can reduce the time charged for the successful response, but it can never increase the clock above its previous balance.

The public configuration shape is preserved. On Ethereum, matchEffort is now the scalar five-minute response budget, currently 25 blocks, rather than a front-loaded sum over commitment heights.

Match existence and phases

Match existence previously relied in part on checking whether a keccak-derived Match ID hash was zero. That check was dead code: a valid keccak output is not a meaningful storage-existence sentinel.

Existence now comes from mapped Match state. Nonexistent and deleted matches are rejected consistently before phase-specific interpretation.

The Match library now derives explicit phases from the existing representation:

UNINITIALIZED
BISECTING
READY_TO_SEAL
SEALED

The refactor centralizes:

existence-before-phase precedence;
branch selection;
revealer rotation;
divergence encoding;
final-seal parity;
agree-proof ownership;
final-state attribution;
paused allowance and duration calculations;
zero-height rejection.

No new Match storage is introduced. The raw tuple, sealed encoding, Tournament ABI, storage layout, selectors, and event signatures remain compatibility surfaces.

Factory and configuration validation

Factories now reject zero or no-code implementation, provider, and state-transition dependencies. The canonical provider rejects a zero maximum allowance.

Test-owned validation covers:

positive level counts and heights;
stride ordering;
span tiling;
root extent;
supported timing assumptions.

Canonical geometry validation remains a test/deployment responsibility rather than a recurring runtime cost.

Refund, gas, and bond policy

Refunds are bounded, best-effort subsidies for altruistic validators. They are not:

an endogenous validator incentive;
a safety mechanism;
receipt-exact transaction reimbursement;
a guarantee to cover every valid proof class;
a guarantee to cover L2 data or security fees.

The selected action allocations are:

Action	Gas allocation
`ADVANCE_MATCH`	125,000
`WIN_MATCH_BY_TIMEOUT`	260,000
`ELIMINATE_MATCH_BY_TIMEOUT`	135,000
`SEAL_INNER_MATCH_AND_CREATE_INNER_TOURNAMENT`	363,000
`WIN_INNER_TOURNAMENT`	336,000
`ELIMINATE_INNER_TOURNAMENT`	172,000
`SEAL_LEAF_MATCH`	105,000
`WIN_LEAF_MATCH`	843,000

WIN_LEAF_MATCH is a provisional subsidy for the exercised ordinary-proof path, not a universal upper bound across input and proof classes.

The join bond is now derived automatically from the work it may need to fund:

bondValue(height) =
    ((height - 1) * ADVANCE_MATCH + maximumLegalTerminalPath)
    * WORK_PRICE_CAP

The current maximum terminal allocation is the 948,000-gas leaf seal plus leaf win path. WORK_PRICE_CAP remains 50 gwei and the priority-fee cap remains 10 gwei.

There is no separately maintained or additional Sybil-principal constant. Losing reserves may fund successful bounded progress refunds; the residual present at successful terminal recovery is burned after paying at most one bond. This does not claim a fixed positive burn for every losing commitment.

The calibration procedure is deliberately manual but reproducible and fail-closed. It checks the exact Foundry release, configuration, clean-tree state, environment overrides, and all retained witnesses before recommending a table change.

See GAS-CALIBRATION.md and REFUND-DESIGN.md.

Test architecture

The dispute gate grew from 42 to 231 tests.

Behavior tests are no longer coupled to the canonical Top/Middle/Bottom constants. Tests inject the geometry required by the property being exercised, including one-, two-, and four-level shapes.

The historical three-level suites remain as frozen characterization coverage rather than defining all PRT semantics.

New coverage includes:

single-clock arithmetic and fuzz properties;
pair-clock phase, transition, symmetry, and timeout-partition tests;
Match identity, existence, phase, parity, and rejection matrices;
an independent sparse-Merkle/parity oracle;
public Tournament composition tests;
refund, callback, reserve, and bond-formula properties;
recursive two- and four-level factory/clone traces;
real child-tournament population and propagation;
18 retained gas witnesses;
ABI, storage, selector, event, and bytecode compatibility snapshots;
32,768 positive stateful lifecycle handler invocations;
16,384 mixed legal/rejection stateful handler invocations;
bounded exhaustive one-level delay models.

The bounded delay models are executable finite checks, not a proof of general multi-level liveness.

See TEST-REPORT.md.

Documentation

The PR adds a code-aligned description of the current protocol in dispute-game.md and expands dimensioning.md, the glossary, READMEs, AGENTS guidance, and Solidity documentation.

The permanent review corpus includes:

REVIEW.md: confirmed findings, decisions, evidence, and disposition;
MAP.md: source map and lead inventory;
CLOCK-DESIGN.md;
MATCH-DESIGN.md;
REFUND-DESIGN.md;
GAS-CALIBRATION.md;
TEST-REPORT.md.

The documentation distinguishes current behavior, historical checkpoints, accepted policy, deferred work, and non-claims.

Findings disposition

Finding	Severity	Disposition
PRT-001: Arbitrum time calibration	Medium	Deferred; Ethereum is the supported target and other base chains remain experimental
PRT-002: sealed-leaf time restoration	Medium	Resolved
PRT-003: stale/unbounded gas assumptions	Low	Resolved with a bounded heuristic subsidy policy
PRT-004: timeout view/mutation mismatch	Low	Resolved through shared classification
PRT-005: root-only `arbitrationResult` documentation	Low	Clarified as a generic view
PRT-006: Match hash zero existence sentinel	Low	Resolved with state-backed existence
PRT-007: non-idempotent bond recovery	High	Resolved
PRT-008: residual losing-pool recycling	Medium	Resolved with one-bond payout cap and residual burn
PRT-009: bankable pairing effort	Low	Resolved with back-loaded response discounts
PRT-010: proof/timeout overlap	Low	Resolved through shared outcome classification
PRT-011: parent propagation coupled to recovery	Low	Resolved
PRT-012: unjustified additional Sybil principal	Medium	Removed; bonds derive from work reserve
PRT-013: unbounded payment callbacks	Medium	Resolved
CFG-001: selected two-level layout	Planned	Requires coordinated node/client integration
CFG-002: dependency and timing validation	Resolved	Added fail-early validation
STF-TODO-001: halt/exception status semantics	Deferred	Owned by the separate state-transition workstream

Compatibility and deployment

Preserved:

deployed Tournament ABI;
semantic Tournament storage layout;
raw Match.State tuple;
existing event signatures and selectors;
staged sling consensus behavior.

Intentionally changed:

Tournament creation and runtime bytecode;
timeout and proof resolution at previously overlapping boundaries;
response-effort accounting;
terminal bond settlement;
invalid-edge behavior for nonexistent and zero-height matches;
PartialBondRefund.ret, which is now always empty;
source-level internal Clock, Match, and Time helper APIs.

Compatibility witnesses:

Tournament ABI:
67e34ced79c75e19935e3cfc67305ac22f634a0a90f9477e10062ac0bc8feb8a

Semantic Tournament storage layout:
952af2f68c5d04f9bf27a720e04c12492453d2edd76b7516bcdb1cf2e873a329

Metadata-free Tournament creation bytecode:
a638837b16a7cb21139706ff3aaecbb79a2f3b663d1b1dbb50f1e0243735ed4c

Metadata-free Tournament runtime bytecode:
631eb0908dfce360f6b6d85fb827ff4c5fe201b9e48e6af74b99f0cd35d2d5d3

Before deployment, regenerate and review all deployment artifacts and CREATE2-derived addresses.

The checked-in canonical contracts still use the historical three-level table:

log2step = [44, 27, 0]
height   = [48, 17, 27]

The selected two-level deployment table remains an integration gate:

log2step = [37, 0]
height   = [55, 37]

This PR does not switch canonical geometry and does not claim node or Lua-client agreement with the selected table.

Validation

The final tree was validated with official Forge 1.5.1-v1.5.1, Solc 0.8.30, optimized IR, 200 optimizer runs, and Prague EVM.

cd prt/contracts
forge fmt --check

just prt-contracts::test-disputes
just prt-contracts::coverage
just prt-contracts::measure-gas
just rollups-contracts::test

just check
just rollups-tests::test echo gc_match
just rollups-tests::test echo multi_sybil

Results:

formatting passed;
PRT dispute tests: 52 suites, 231/231 passed;
gas witnesses: 18/18 passed;
downstream rollups-contract tests: 4/4 passed;
each downstream fuzz property ran 256 cases;
coverage tests: 30 suites, 204/204 passed;
line coverage: 693/705, 98.30%;
statement coverage: 715/727, 98.35%;
function coverage: 145/145, 100%;
reported branch mapping: 65/138, 47.10%;
the full workspace gate (formatting, luacheck, clippy, unit tests) passed with the client alignment, including new unit tests pinning the contract's bisection and leaf-race timeout boundary matrices;
the gc_match and multi_sybil e2e scenarios (timeout elimination and timeout win against live sybils) passed against a freshly rebuilt devnet.

The post-rebase Forge 1.5.1 rerun required no further Gas or Bond changes. The retained advance and full-proof inner-seal witnesses reproduced the selected 125,000 and 363,000 allocations.

Branch mappings remain investigative because optimized-IR source maps and the deliberate coverage exclusions do not provide a complete semantic branch metric.

Explicit non-claims and deferred work

This PR does not claim:

a proof of complete PRT security;
a general multi-level liveness theorem;
a proof that at least half of all clocks tick in every recursive state;
a stateful recursive adversarial-arrival scheduler;
activation of the selected two-level production geometry;
node, Lua-client, or end-to-end commitment conformance;
corrected non-Ethereum time semantics;
an audit or definition of state-transition halt, overflow, exception, or reset semantics;
universal leaf-proof gas coverage;
receipt-exact reimbursement or endogenous validator incentives;
complete semantic branch coverage.

Ethereum is the supported timing target. Non-Ethereum registrations remain experimental. In particular, the current Arbitrum calibration is not valid for its parent-chain NUMBER semantics.

State-transition halt and exception semantics remain documented as a deferred lead for the separate workstream already addressing them.

Review guide

The commits are intentionally sequenced and are best reviewed chronologically. The highest-risk production changes are:

5f3a071 - bounded and idempotent terminal bond settlement;
f7d74a9 - Clock behavior, timeout partition, and back-loaded effort;
b5eca6a - callback isolation and recovery/propagation separation;
d61d3c2 - Match phase and bisection refactor;
301e438 - final refund calibration and bond derivation;
ac3bea0 - final Clock and Match invariant centralization;
185098e - the off-chain companion: node and Lua-client timeout-classification alignment, plus the outputsMerkleRoot naming adoption.

The geometry, lifecycle, recursive, callback, and compatibility test commits around these changes form the evidence fence. The final documentation and Forge 1.5.1 commits record the release-verification provenance.

Document the on-chain tournament lifecycle, commitment geometry, clock model, trust boundary, and review scope with the contracts as the source of truth. Add the audit map, review ledger, Clock design record, and documentation corrections that motivate the subsequent implementation and test campaign. Mark unverified leads and deferred decisions explicitly instead of presenting them as established guarantees.

Pay the winning claimer at most one bond, burn the residual tournament balance, and make repeated successful recovery a permissionless no-op. Preserve both the claimer and the full balance when recipient payment fails so settlement remains retryable. Cover zero-balance, failed-payment, repeated-recovery, payout-cap, and downstream Dave settlement behavior. This closes the path where terminal recovery could brick application settlement or recycle losing reserves into a Sybil budget.

Charge timeout winners from live remaining time, introduce MatchClocks as the two-clock policy boundary, and derive proof and timeout settlement from one outcome classifier. Preserve the inclusive equality boundary as double elimination. Replace front-loaded match effort with a non-bankable response discount applied after each eligible response. Cover legal clock shapes, deadline boundaries, time conservation, both winner orientations, sealed-leaf settlement, and the absence of pairing or re-entry grants.

Keep the two-level deployment migration explicitly gated and leave canonical production geometry unchanged. Freeze the historical three-level parameters, bind legacy suites to that provider, and quarantine role-oriented history under characterization tests. Separate behavior fixtures from canonical conformance so tests inject the shape they need and future parameter updates do not rewrite unrelated expectations. The temporary two-level production switch and its exact revert are omitted from the cleaned history.

Require the stored Match state to exist before sealing an inner match and creating its child tournament. Preserve existence-before-phase error ordering and pin the missing-match regression at the public entry point.

Remove the unused duration subtraction helper and a duplicate deployment import. Document that block-number calibration outside Ethereum is experimental and can be invalidated by changes in the underlying chain timing model. This cleanup changes no supported dispute-game behavior and leaves alternate base-layer timing as an explicit deployment gate.

Remove test-only topology counters from production, separate child balance recovery from parent winner propagation, and make the work reserve and price caps explicit in Bond. Characterize pooled reserves without relying on mutable instrumentation. Bound recipient callback gas, skip zero-value calls, avoid copying return data, and retain retry semantics for failed terminal payments. Prove that rejecting, reverting, data-amplifying, and gas-exhausting recipients cannot reenter or block unrelated tournament progress.

Measure the successful advance, leaf and inner seal, timeout, child propagation, and child elimination branches with storage-aware fixtures. Replace stale refund allocations with the first complete reviewed action table and pin its derived reserve arithmetic. Retain both winner orientations and first-write paths so later implementation changes fail the witnesses when they cross a reviewed margin.

Remove the ineffective zero check on a hashed Match identifier and derive existence from the mapped Match state instead. Apply the same stored-state guard to child-resolution paths and getMatchCycle so absent and deleted matches cannot look valid through a nonzero keccak slot. Pin default-ID hashing, unlinked child tournaments, and nonexistent and deleted cycle queries.

Add a release-pinned gas runner, scoped coverage recipe, independent bisection parity model, configurable full Merkle trees, and inspectable single-level tournament fixtures. Build stateful positive and rejection campaigns plus coherent two-level claim and tournament fixtures. Exercise recursive winner propagation, double elimination, late entry, clock carryover, sequential children, strict response deadlines, and proof-timeout convergence without importing canonical geometry.

Pin raw state encoding, validation order, events, errors, and compatibility witnesses before changing the implementation. Derive explicit phases and sealed views from the existing representation without adding storage. Centralize branch selection, revealer rotation, divergence encoding, sealing parity, and winner attribution behind phase-oriented verbs. Retire legacy helpers after all callers migrate, preserve the deployed ABI and semantic storage layout, and compare both gas-sensitive branch orientations.

Extend coherent claim fixtures and trace concurrent child populations without assuming root identity determines the selected parent side. Add sealed-state existence checks and harden the retained gas witnesses. Characterize callback isolation and reproduce the production refund cap with an independent formula over base fee, priority fee, balance, and recipient behavior. Record the exact supported refund boundary and the remaining proof-gas limits.

Reject zero or no-code implementation, parameter-provider, and state-transition dependencies, and reject a zero canonical maximum allowance. Validate geometry tables, row tiling, level counts, height and stride bounds, and root extent in test-owned fixtures. Exercise strict four-level recursion, sequential dangling populations, and an exhaustive bounded one-level delay model. Document these as configuration and finite-model evidence rather than a multi-level liveness theorem.

Raise the intentionally provisional leaf-proof allocation and derive every bond from positive-height match work plus the maximum terminal path. Remove the additional Sybil principal so reserves follow the reviewed gas table and work price cap automatically. Pin the terminal maximum, per-height work reserve, join deposits, refund cap, and automatic propagation from Gas into Bond policy values.

Finish the authoritative Match phase API and sealed decoder, then separate single-clock arithmetic tests from pair-policy tests. Centralize the response discount, existence-before-phase precedence, paused allowance boundary, and duration maximum; reject zero-height Match creation and remove dead duration helpers. Recalibrate advance and inner-seal refunds to 125,000 and 363,000 gas while the terminal maximum remains unchanged. Complete role-guard, phase, parity, final-state child-selection, raw-state preservation, and compatibility coverage.

Consolidate the Clock and Match design outcomes, confirmed findings, test assessment, compatibility witnesses, coverage qualifications, and refund calibration procedure after the implementation campaign. Separate historical checkpoints from the current contract and test candidate. Record exact pre-rebase gas provenance and make the planned Foundry-version bump an explicit recalibration and release gate.

Use the release version pinned by the rebased CI and container as the authoritative refund-calibration runner. Keep the recipe fail-closed so unpinned or dirty measurements remain diagnostic only.

Distinguish the final Solidity and test tree from the clean calibration candidate, and close the Foundry-version rebase trigger with an exact official 1.5.1 record. Document the unchanged 18-witness recommendations, compatibility hashes, 231-test dispute gate, 204-test coverage map, and four downstream integration tests.

Move the completed internal dispute-game review out of the contract workspace into a dated, explicitly historical archive. Extract the durable refund-accounting proof, Foundry test architecture, and gas calibration procedure into maintained documents. Move the storage-layout normalizer into contract tooling and add a compatibility-hash recipe. Rework root and nested agent guidance into cumulative, scoped routers, add the nested Claude import shim, and remove stale pre-sling repository orientation.

…tion The GC's elimination gate compared the expired side's overdue time against the opponent's static allowance where the reviewed contracts compare live remaining time, equality eliminating both: two 100-block clocks racing from one instant die together on-chain around block 100, but the node waited past block 200 to sweep (node-audit.md finding 8, inherited from the pre-rewrite reference). The Hero's win gate had the mirror defect - opponent-timed-out alone - so inside the eliminate-both zone it submitted winMatchByTimeout transactions the contract rejects (NeitherClockHasTimedOut). Mirror MatchClocks.classifyTimeoutAt once as tournament::classify_timeout and decide both paths with it: the GC eliminates exactly on EliminateBoth and the Hero fires only when its own side wins. The Lua client carried both gates verbatim; align its gc and honest strategy the same way (its clock gains remaining()). Unit tests pin the contract's bisection and leaf-race boundary matrices, both hero-side zones, and the shared-deadline sweep. Folded in, opportunistically: - adopt the contracts' outputsMerkleRoot naming across the Rust side: Settlement.outputs_merkle_root(_proof), the settlement_info columns (fresh stores are born v4; migrate_to_latest refuses a pre-rename store loudly with the wipe-and-rebuild message), and machine.outputs_merkle_root_with_proof(). - the STF-upgrade campaign plan (docs/plans/stf-upgrade.md), staging the next node campaign's TODOs.

GCdePaula force-pushed the feature/sling-node branch from e7b0efd to d8cc329 Compare July 21, 2026 13:55

GCdePaula added 18 commits July 21, 2026 10:56

fix(prt): reject nonexistent inner matches

74cd17e

Require the stored Match state to exist before sealing an inner match and creating its child tournament. Preserve existence-before-phase error ordering and pin the missing-match regression at the public entry point.

chore(prt): align gas calibration with Foundry 1.5.1

7565ec2

Use the release version pinned by the rebased CI and container as the authoritative refund-calibration runner. Keep the recipe fail-closed so unpinned or dirty measurements remain diagnostic only.

GCdePaula force-pushed the feature/contracts-review branch from bbb0280 to ac058eb Compare July 21, 2026 14:57

GCdePaula requested review from guidanoli and stephenctw and removed request for guidanoli July 21, 2026 17:07

GCdePaula self-assigned this Jul 21, 2026

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

PRT Contracts Review#273

PRT Contracts Review#273
GCdePaula wants to merge 20 commits into
feature/sling-nodefrom
feature/contracts-review

GCdePaula commented Jul 20, 2026 •

edited

Loading

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Uh oh!

Conversation

GCdePaula commented Jul 20, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Main security and correctness changes

Terminal bond settlement

Bounded recipient callbacks

Clock conservation and timeout partition

Back-loaded response effort

Match existence and phases

Factory and configuration validation

Refund, gas, and bond policy

Test architecture

Documentation

Findings disposition

Compatibility and deployment

Validation

Explicit non-claims and deferred work

Review guide

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

GCdePaula commented Jul 20, 2026 •

edited

Loading