prt-contract-testing.md

PRT contract testing

This document describes how the Foundry dispute-game tests divide responsibility and how new tests should be designed. It covers prt/contracts; test-harness.md separately owns the Lua and real-node end-to-end harness.

Exact campaign counts, hashes, mutation experiments, and release results are historical evidence in the TEST-REPORT.md archive.

Commands

Run from the repository root:

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

The state-transition suites require the machine/step submodule, FFI, and the yield machine image (just programs::build-programs):

just prt-contracts::test-stf
just prt-contracts::test-stf-fuzzy

just prt-contracts::test-all combines the dispute and state-transition gates. just test-prt-gas runs both the Tournament-only witnesses and the serialized full-stack FFI leaf-proof matrix, and CI runs it in the prt-contracts job. The witnesses are one-sided: a pass means every allocation still covers its witnesses. Moving a constant has stricter toolchain and clean-tree requirements; follow prt-refund-gas-calibration.md. Ordinary Rollups contract tests and coverage exclude the *FfiTest contracts deliberately.

Directory ownership

Location	Responsibility
test/*.t.sol	Focused library tests and public Tournament composition
test/accounting/	Reserve algebra, exact refund formula, and callback behavior
test/characterization/	Frozen historical three-level behavior
test/config/	Canonical and generic parameter-table validation
test/devnet/	The devnet-only deployment of the three-level test table CI and local tests run (the default DEVNET_GEOMETRY) and its test
test/fixtures/	Injected geometry, small trees, independent models, and test-only transitions
test/gas/	Retained production refund witnesses
test/properties/	Match parity, lifecycle, recursion, population, and delay properties
test/step/ and FFI suites	Solidity-step and external state-transition oracles

The full-stack leaf-proof gas fixture lives under cartesi-rollups/contracts/test/gas/, where it can compose the production InputBox, DaveConsensus provider, Cartesi state transition, and PRT Tournament. Its height-one, position-one commitments are coordinate coherent and inject only the geometry needed by the measured entry point.

Characterization is a historical behavior fossil, not the preferred semantic oracle. New behavior tests should use the smallest injected geometry that exposes the property under review.

Test layers

Each layer has one job:

Layer	What it establishes	What it does not establish
Deterministic regressions	Exact boundaries, selectors, rollback, precedence, and lifecycle traces	Exhaustive arrival schedules
Fuzz properties	Arithmetic partitions, symmetry, geometry, caps, and bounded input domains	Completeness outside the generator
Stateful invariants	Legal and rejected operation sequences against an independent ghost model	Recursive adversarial scheduling unless modeled explicitly
Finite exhaustive models	Every state in a stated small domain	An unbounded theorem
Characterization	Historical observable behavior	The desired semantics of new code
Compatibility and impact checks	Wire ABI and clone encoding; storage and bytecode drift	Correctness, or a promise that internal layout and deployment identity remain unchanged
Gas witnesses	Production refund-seam work for a declared execution envelope	Receipt gas or unbounded proof classes
Downstream integration	Rollups factory and staged-consensus composition	Real validator or Lua conformance
Coverage mapping	Production locations that deserve investigation	Semantic assurance or branch completeness

Do not use a higher test count as a substitute for independent oracles and failure-sensitive assertions.

Clock ownership

The tests mirror the production abstraction:

• Clock owns one-clock representation, arithmetic, and storage transitions.
• MatchClocks owns policy involving two clocks.
• Match owns commitment existence and structural phase.
• Tournament proves that those local responsibilities compose correctly.

One-clock properties should cover elapsed time, remaining time, overdue time, strict deadlines, charging, replacement, and zero-sentinel rejection at an explicit observation instant.

Pair-clock tests should cover every supported local shape: uninitialized, two paused, exactly one running, and two running. Each transition needs both orientations and a rejection matrix. The shared timeout classifier must remain exhaustive and disjoint, with equality assigned explicitly. Its independent oracle must distinguish a paused winner's deferred overdue charge from a running winner's zero deferred charge. Winner tests must show that survival is decided on the full cost while the stored clock forgives at most one response budget of it (min(cost, G)). Tournament tests own the strict verb partition: a leaf proof is valid only under NONE, single-winner statuses select timeout victory, and ELIMINATE_BOTH selects elimination. Response-budget tests must prove that a successful response discounts elapsed time once without increasing the prior balance; pairing must not grant time, and same-tournament survivor re-entry must not raise the stored balance or forgive more than one response budget. Recursive integration separately owns the shared pair envelope: a child return may exceed the selected side's snapshotted remainder, but not max(r1, r2) or the post-discount live pair mass, and it owns the refill property: a commitment joining each child within T + G and propagating within G returns with its pre-seal clock, delegation after delegation, from either side of the pair envelope. Before every successful child return, the recursive suites also assert that the carried allowance already lies within the envelope: the return clamps to it, which would otherwise mask a child that added time.

Tournament integration owns the structural distinctions that pair clocks alone cannot infer, including ready-to-bisect versus sealed-inner states when both clocks are paused.

The living clock evidence map is:

Concern	Primary evidence
One-clock arithmetic, strict deadlines, and zero sentinel	test/Clock.t.sol
Legal pair shapes, timeout partition, equality, and orientation symmetry	test/MatchClocks.t.sol
Public proof, timeout, pairing, and rollback composition	test/Tournament.t.sol
Independent one-level topology and clock ghost state	test/properties/TournamentLifecycleInvariant.t.sol
Reachable lower bounds and exhaustive small one-level schedules	test/properties/LeafPopulationDelay.t.sol and test/properties/BoundedOneLevelDelay.t.sol
Shared child envelopes, propagation, concurrent children, and generic depth	test/properties/RecursiveTournamentLifecycle.t.sol, ConcurrentRecursivePopulation.t.sol, and FourLevelRecursiveLifecycle.t.sol
Ethereum and local-devnet block conversion for response and allowance budgets	test/Deployment.t.sol

Within RecursiveTournamentLifecycle.t.sol, testChildWinnerSelectsParentSideByFinalStateNotByRoot pins final-state classification, while testChildReturnUsesSharedParentPairEnvelope pins the asymmetric clock return. Together they establish the mechanics behind the simplification; they do not identify an optimal attacker schedule or prove a general recursive delay bound.

The one-level invariant establishes the exact parity-aware relation runningClocks >= floor(K / 2) for leaf tournaments. It is not a recursive clock theorem: sealed inner parents pause both clocks and delegate the obligation to a linked child. No current model combines an identified correct commitment, an eager correct strategy, an adversarial scheduler, and one shared censorship ledger C; that general recursive result remains open.

Match ownership

Match tests deliberately triangulate four independent concerns:

1. raw characterization records the historical tuple and sealed encoding while pinning the externally observable events and errors;
2. an independent sparse-Merkle model owns divergence, parity, agree-proof ownership, and fixed-side winner attribution;
3. focused validation tests own malformed children, proof failures, and phase guards; and
4. Tournament integration owns clocks, deletion, re-pairing, recursion, and terminal outcomes.

The sparse-tree oracle must derive turn ownership independently. Copying the production parity table into the test would create correlated evidence rather than an oracle. Exercise both commitment orders, valid zero-valued payloads, leftmost divergence, every small-tree position, and the supported large-height boundaries.

Configuration independence

Behavioral tests inject the geometry they require. Imports of production ArbitrationConstants belong in canonical conformance tests, not in generic Clock, Match, Tournament, or accounting properties.

The suite uses one-, two-, and four-level fixtures to exercise generic structure. Historical Top/Middle/Bottom suites use a frozen test-owned provider under test/characterization/. None of these fixtures proves that an off-chain client uses a selected deployment table; that requires coordinated node and Lua conformance.

Oracle independence

Prefer evidence that does not replay production storage or branch tables:

• the Match oracle constructs its own sparse trees and tracks the revealer by alternation;
• the lifecycle ghost model tracks population, topology, coordinates, clocks, claimers, and counters independently;
• finite schedulers use their own packed state and enumerate a declared domain; and
• refund and reserve properties derive the algebra from joins, matches, caps, and balances instead of comparing two production getters.

Settlement stubs select a claimed leaf outcome. They are not oracles for the real machine transition. Coordinate-coherent fixtures prove that tournament spans and contested states line up, not that either computation is correct.

State-transition boundary

The state-transition suites separate cheap routing evidence from semantic oracles. Solidity-only tests exercise input and ordinary-step dispatch across the full 24-bit input, 48-bit mcycle, and 20-bit ucycle fields. Structured FFI fuzzing adds canonical closing proofs and all four transition shapes, generated with the v0.21 emulator and replayed through CartesiStateTransition.

The deterministic FFI matrix pins boundary-adjacent counters at the first and last uarch spans, input-window transitions, and the epoch tail. A tiny RV64 guest reaches zero and nonzero halt, TX exception, unexpected manual yield, and mcycle overflow. Opening vectors cover both halt values and every terminal class; representative closing vectors establish reset without rejected-input substitution. Separate vectors own rejected-input restoration and uarch-cycle overflow. Pending-yield vectors, logged from a bare emulator so client terminal classification cannot shape them, own a manual yield that outranks halt and the input budget: an RX_ACCEPTED opening on the budget's last cycle (also at the maximum mcycle) or on a preset halted machine takes the input, unlike the idle opening, and an RX_REJECTED closing on the budget's last cycle still restores the revert root. Combined witness mutations cover exact DA header and payload boundaries, the CMIO-step and step-reset seams, before-root and provider-root binding, one representative byte in each composed primitive, and replay across adjacent transition shapes.

Those vectors come from the Lua client and bare emulators. The Rust node's own witness bytes are pinned on its side by node_witness_vectors_hold (cartesi-rollups/node/tests/engine_machine.rs): window openings with and without an input, a second input's opening, a maximum-size input's opening, a plain ustep, a closing slot, and a rejected-input closing slot. seam_witness_vectors_hold (engine/machine_stf.rs) adds the node's bytes at the input budget's seams, where the v0.21 CLI departs from the step: accepted openings on the budget's last cycle and on a halted machine, and a rejected closing on the budget's last cycle. NodeWitnessesTest (cartesi-rollups/contracts) replays each through CartesiStateTransition, with inputs rooted the way DaveConsensus roots them, and requires the node's post-state. Likewise node_proof_vectors_hold pins the node's commitment proofs (root joins under both tables, and a leaf agree-state opening and a leaf join at each table's leaf height) and an epoch's settlement validity proof; NodeProofsTest opens the former with the tournament's Commitment library and validates the latter as DaveConsensus stages it, requiring the reference CLI's outputs Merkle root. A nonempty DA payload paired with the provider's zero out-of-range root is rejected (StateTransition.t.sol): a position with no input carries no input bytes, which fixes the proof's length for the leaf refund. One PRT-side composition test carries a canonical input-opening vector through the real leaf Tournament and CartesiStateTransition with a standalone IDataProvider. This pins the generic dispute seam without depending on DaveConsensus or creating another expected-root implementation.

This is bounded cross-implementation evidence for the v0.21 adapter. It is not an exhaustive enumeration of every RV64 instruction, access-log shape, proof byte, or gas envelope; those lower-level instruction and log semantics remain owned by machine/step and the emulator.

Fuzz and stateful reproducibility

The ordinary Foundry fuzz budget is pinned in foundry.toml. A deeper campaign must record its run count, depth where applicable, and seed. Do not describe a fuzz campaign as exhaustive unless its generator enumerates the entire stated domain.

Stateful handlers must account for reverts and discarded inputs. A green invariant with most operations rejected is weak evidence; retain counters or companion traces that prove the intended operations executed.

Coverage discipline

Coverage instrumentation changes gas and cannot run the retained gas witnesses or exact refund-formula measurements faithfully. FFI and state-transition tests have separate execution requirements, and the slow stateful executors are owned by the ordinary dispute gate. Deterministic companion traces map their principal production paths.

The coverage recipe uses IR-minimum mappings as a stack-depth workaround. Reported branch totals are directional and can disagree with demonstrably executing tests. Use uncovered lines and functions as investigation leads, not as a correctness score.

Compatibility and impact checks

Within one deployment generation, the supported wire surface includes the Tournament function, event, and error ABI plus the immutable clone-argument encoding. An intentional wire-format break starts a new generation: deploy a fresh Tournament implementation, factory, and dependent Dave bundle; ship matching bindings, clients, and artifacts; and do not carry a live dispute or persisted event stream across the boundary.

Storage layout and raw Match and Clock encoding are internal in the current non-upgradeable design. There is no supported state migration or raw-storage client. Solidity tests reach raw Match, Clock, and topology state through the white-box probe in test/fixtures/TournamentInspector.sol. Its slot constants must follow intentional layout changes; they do not turn the current layout into a compatibility promise. Clone-argument decoding and the independently derived closure and finish predicates remain useful oracles rather than echoes of the observer views.

Run:

just prt-contracts::compatibility-hashes

The report separates wire compatibility from implementation and deployment impact. An ABI difference changes the supported wire surface. A storage-layout difference means white-box probes must be reviewed. A bytecode difference changes deployment identity and may change CREATE2-derived addresses. Inspect every unexpected difference rather than updating a recorded value mechanically, but do not require internal hashes to remain equal. Metadata-free hashes also do not enforce the EIP-170 runtime-size ceiling; every release-facing contract change must still pass the full forge build --sizes gate.

When to add tests

Add a test when it:

• protects a production change;
• reproduces a concrete finding;
• validates a new supported geometry, proof, or fee envelope; or
• attacks an explicitly scoped open question.

Do not add fixed lifecycle traces or fuzz volume solely to improve headline counts. Current non-claims include a general recursive adversarial-arrival proof, node and Lua agreement with a future geometry, exhaustive state-transition instruction and access-log coverage, a universal leaf-proof gas ceiling, and semantic meaning for IR branch percentages.