Harden PRT dispute-game contracts by GCdePaula · Pull Request #273 · cartesi/dave

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

Summary

This PR contains the smart-contract side of the PRT review. The corresponding node-reader adaptation is isolated in feature/node-reader-update and will follow separately, keeping this review focused on contract behavior and evidence.

Fixes

Terminal bond recovery now pays at most one bond and is idempotent. A failed recipient payment preserves the claimer and full balance so settlement remains permissionlessly retryable. This fixes an exploit where an attacker could brick the tournament.
Refund and payment callbacks can no longer block tournament progress: calls have bounded gas, copy no return data, skip zero-value transfers, and preserve state where retry is required. This fixes an exploit where a claim made by a malicious smart contract could brick the tournament.
After a successful recovery, any balance remaining after the one-bond payment is burned. Pooled reserves behind eliminated commitments therefore cannot be recycled into another Sybil campaign, preserving a real marginal cost for each attack. This fixes a bug that made recurrent Sybil attacks cheap, where losing Sybil bonds could be recycled into later disputes.
A sealed-leaf timeout could restore time already spent by the survivor, while proof and timeout paths could overlap. Settlement now uses live clock balances and one four-way classifier shared by timeout views, mutations, and leaf-proof eligibility. This fixes a bug that degraded tournament liveness.
Refund allocations and bonds previously rested on incomplete gas measurements. The new harness covers storage-sensitive branches, both orientations, and full-stack leaf proofs, then rounds allocations conservatively. Bonds derive from the maximum legal work reserve, so gas-table changes propagate into the required deposit. This fixes a bug where bond value was underestimated.

Security and correctness testing

Testing is the largest part of this PR, accounting for more than 60% of its changed lines. The campaign replaces geometry-coupled coverage and implementation-shaped helpers with injectable fixtures, independent models, focused regressions, stateful positive and rejection campaigns, recursive lifecycle and accounting scenarios, adversarial callback recipients, and full-stack proof witnesses.

The resulting suite passes 235 PRT dispute tests across 52 suites, 4 downstream Rollups contract tests, 3 deterministic STF tests, both STF fuzz properties at 256 cases each, and 30 release-pinned gas witnesses. Scoped coverage is 98.43% lines, 98.47% statements, 49.31% branches, and 100% functions.

Simplifications

The front-loaded clock design is gone, substituted by a back-loading clock design. Pairing previously granted matchEffort to both participants before either responded, introducing bankable, capped balance changes. A successful response now receives a non-bankable discount after the fact: clock balances never increase, unused grants cannot be banked, timeout calibration is more direct and easier to reason about (major win), the tournament's worst-case delay bound is tighter, and pairing performs less storage work.
Clock owns single-clock arithmetic and distinguishes checked from saturating subtraction; MatchClocks owns pair-level transitions and timeout policy.
Match now expresses its phases directly, branches once during bisection and sealing, and stores sealed final states in commitment order.
Match IDs now only locate mapping slots; existence is checked from the stored isInit flag. The old nonzero-hash check accepted arbitrary IDs, allowing nonexistent or deleted matches to produce plausible view results. Views and phase-specific transitions now reject uninitialized slots consistently.
Internal library interfaces now receive the dimensions they operate on explicitly instead of depending on canonical configuration objects. Tests can now inject small or adversarial geometries while production geometry remains separately pinned.

Review map

The PR changes 102 files and +25,495/-1,864 lines, but tests and documentation account for 93.1% of the changed lines.

Area	Files	Changed lines	Share
Tests and fixtures	50	16,836	61.54%
Documentation and guidance	30	8,634	31.56%
Production Solidity	13	1,539	5.63%
Tooling and witness support	9	350	1.28%

Frozen review and calibration records contribute 6,107 added lines. The seven core logic files are 1,245 changed lines, or 4.55% of the PR.

A focused review can start with Time.sol, Clock.sol, and MatchClocks.sol; continue through Match.sol and Tournament.sol; and finish with Bond.sol, Gas.sol, and the corresponding focused and recursive suites.

Reproduce

Run from the repository root:

just doctor
just check
just test-smart-contracts
just prt-contracts::test-stf
just prt-contracts::test-stf-fuzzy
just test-prt-gas
just prt-contracts::coverage
just prt-contracts::compatibility-hashes

The authoritative gas calibration requires a clean worktree and Forge 1.5.1:

just measure-prt-gas

Refund allocations are bounded subsidies, not receipt-exact reimbursement or safety bounds. The final post-refactor measurement required no further production-constant changes: ADVANCE_MATCH matches its rounded recommendation, inner sealing retains 1,000 gas of headroom, and WIN_LEAF_MATCH is calibrated to the largest retained canonical InputBox witness.

Compatibility details

The Solidity ABI schema, storage layout, selectors, and events remain unchanged and are guarded by the compatibility tests and hash recipe.

getMatch has one intentional semantic change: after sealing, leftNode always contains commitment one's final state and rightNode always contains commitment two's final state. The previous height-parity-dependent interpretation no longer applies.

Raw readers must determine the Match phase before interpreting the overloaded tuple. Their corresponding update is handled in feature/node-reader-update.

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.

Account timeout debt according to the clock phase. Paused bisection survivors still pay an expired responder overdue interval, while running sealed-leaf survivors preserve their live remainder instead of paying the same censorship interval twice. Make leaf proofs exclusive to the pre-timeout state, keep timeout victory available from the shorter deadline until the longer leaf clock expires, and retain double elimination at that inclusive deadline. Adopt the cumulative, non-rechargeable censorship budget as protocol provenance. Document the phase-aware timeout table and retain pair-clock, public lifecycle, recursive, stateful, bounded-model, and three-claim regressions. Keep Rust, Lua, gas, and end-to-end alignment as explicit release gates.

Branch once when advancing or sealing a divergence, keep each left/right body self-contained, and decode the legacy sealed representation through the same explicit shape. Document how alternating responders open two adjacent edges while the shared frontier descends one level in both commitment trees. Require braces and make the clock responder branch explicit. Preserve the external ABI and semantic storage layout. Defer the complete gas remeasurement to the tracked calibration gate.

Update the retained sealed-leaf gas scenarios for cumulative-censorship clock semantics: preserve the running winner remainder, move double elimination to the longer clock deadline, and treat expired leaf proofs as rejection cases. Keep the existing advance and timeout-elimination allocations after release-pinned measurements moved down by one rounding bucket. Assert the exact 1,000-unit retained headroom so later drift cannot hide behind a generic upper bound. Archive the 18-witness measurement matrix, environment, compatibility hashes, reserve checkpoints, and validation results. Mark contract calibration complete while leaving Rust, Lua, and end-to-end alignment open.

Compute the shared terminal work reserve from three protocol-shaped families: direct timeouts, sealed leaves, and sealed inner tournaments. This is algebraically identical to the flattened seven-path maximum while making shared prefixes and Gas-table propagation explicit. Keep the independent accounting oracle flattened across all legal paths. Preserve ABI, storage, allocations, reserves, and bonds while reducing optimized Tournament bytecode and bond-computation cost. Advance the accepted calibration record through the refactor with a clean lockfile-restored reproduction, updated bytecode hashes, and the measured artifact reduction.

Exercise the asymmetric parent-child seam where the selected parent side has less time than its opponent at inner sealing. The child receives the pair maximum and may return it to the smaller side while remaining bounded by the sealed pair envelope and total clock mass. Pin the complementary parent phase rule: both parent clocks stay paused while the linked child owns resolution, so neither timeout verb becomes valid merely because wall time exceeds their stored allowances.

Exercise the supported 12-second block-number conversion for Ethereum mainnet and Sepolia, including both the five-minute response budget and each chain kind's maximum allowance. Keep the local devnet conversion covered alongside them while leaving experimental L2 entries unendorsed.

Replace stale descriptions of midpoint leaf elimination and proof-after-timeout with the implemented phase-aware partition. Document block-number time, strict progress boundaries, back-loaded response discounts, prompt-cleanup and capacity assumptions, and the cumulative censorship ledger. Define recursive conservation over the sealed pair post-discount live envelope rather than per-side storage. Distinguish the exact single-level population invariant from the open recursive theorem, and record the balanced multi-level attack construction without presenting it as an upper bound. Align repository guidance, glossary terms, lifecycle and harness documentation, source-level invariants, and the Foundry evidence map so future work starts from current behavior and explicit non-claims.

Hash the raw checkpoint leaf before reconstructing its memory root. The previous helper attempted to call the Hash digest field as a method and, after that typo alone was corrected, supplied the raw checkpoint twice instead of the leaf hash expected by EmulatorCompat.getRevertRootHash.

Retain twelve full Tournament leaf-win witnesses through the real Cartesi state transition, DaveConsensus provider, and InputBox. Cover ordinary steps, resets, rejected-input reverts, in-range inputs through the maximum reachable encoding, the out-of-range fixpoint, both winner orientations, nonzero divergence, and dangling re-pairing. Select the maximum canonical InputBox witness as the bounded subsidy: 3,907,553 measured units, 4,295,809 after review margin, rounded to 4,296,000. Let the existing Bond formula propagate the new 4,401,000 terminal maximum into every height-dependent reserve and join bond. Wire the serialized full-stack FFI matrix into combined test and calibration recipes, pin reserve consequences, and document exact tool and proof provenance. Keep arbitrary trailing proof bytes, unenumerated transitions, unresolved halt or exception semantics, and whole-receipt reimbursement outside the claim. Record that the 5,359,940-unit maximum canonical transaction diagnostic is 31.95% of Ethereum current 16,777,216-unit transaction cap and require future calibrations to recheck network admission limits.

Canonicalize sealed match state by commitment order, simplify bisection and sealing, and express the timeout partition directly. Distinguish saturating from checked clock subtraction and clarify refund fee and payment-call policy without changing gas allocations or the external tuple shape.

Move the retained leaf-gas shell workflows out of the justfile while preserving the public recipes and pinned provenance checks. Hash only stable dependency source and configuration inputs so equivalent locked restores reproduce the accepted digest.

Pin ADVANCE_MATCH to its exact rounded recommendation and retain the existing 1,000-unit inner-seal headroom without changing any production gas or accounting constant.

Archive the clean 30-witness release-pinned rerun, unchanged allocation decision, derived accounting, compatibility hashes, coverage, and reproducible dependency provenance.

stephenctw

LGTM!

Leaving the node/Lua timeout alignment and getMatch sealed-tuple reader update for the follow-up branch (feature/node-reader-update / timeout plan).

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

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

GCdePaula force-pushed the feature/contracts-review branch 2 times, most recently from 15db309 to eff3fb3 Compare July 26, 2026 10:27

GCdePaula changed the title ~~PRT Contracts Review~~ Harden PRT dispute-game contracts Jul 26, 2026

GCdePaula force-pushed the feature/contracts-review branch from 3b5cf3d to ef683c2 Compare July 26, 2026 22:00

GCdePaula marked this pull request as ready for review July 26, 2026 23:06

Base automatically changed from feature/sling-node to next/3.0 July 27, 2026 12:39

GCdePaula added 17 commits July 27, 2026 09:41

fix(prt): reject nonexistent inner matches

b0ce597

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

45d7eaa

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 added 15 commits July 27, 2026 09:41

test(prt): pin post-refactor gas headroom

9adca25

Pin ADVANCE_MATCH to its exact rounded recommendation and retain the existing 1,000-unit inner-seal headroom without changing any production gas or accounting constant.

docs(prt): record post-refactor gas calibration

49eefed

Archive the clean 30-witness release-pinned rerun, unchanged allocation decision, derived accounting, compatibility hashes, coverage, and reproducible dependency provenance.

GCdePaula force-pushed the feature/contracts-review branch from ef683c2 to 49eefed Compare July 27, 2026 12:42

stephenctw approved these changes Jul 27, 2026

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Harden PRT dispute-game contracts - #273

Harden PRT dispute-game contracts#273
GCdePaula wants to merge 32 commits into
next/3.0from
feature/contracts-review

GCdePaula commented Jul 20, 2026 •

edited

Loading

Uh oh!

stephenctw left a comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

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

Fixes

Security and correctness testing

Simplifications

Review map

Reproduce

Compatibility details

Uh oh!

stephenctw left a comment

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

GCdePaula commented Jul 20, 2026 •

edited

Loading