Repository navigation
Conversation
Record the 2026-11-10 whole-boundary audit: one full read of the PRT contracts by the orchestrating session and three independent reviewers in fresh contexts (clocks, structure, value flows), each working blind from the code before the documents. No fleet ran. No defect was found. The record keeps nine leads (N-01 to N-09), the evidence the reviewers produced and the orchestrator re-ran, a first read of the rollups consensus contracts, and the two decisions already taken: the leaf handover stays, and orphan clones are documented, not bounded in code. The settlement phase is still open. The reviewed state is identified by its tree hash; the evidence stays out of tree until it is promoted into the owning suites.
The second contracts audit executed the documented proof-to-timeout handover at the deployed two-level formula: with no censorship budget, two occurrences defeat a correct commitment whose every action lands inside its own response budget. It also showed that occurrences repeat after closure by parking late-joined Sybils, and priced them. Keep the disjoint leaf verbs and write the reasoning beside the accepted limitation, for whoever revisits it: the correct side loses only its joint lateness beyond one G, the adversary pays at least a leaf bond for every such block (about 1,100 to 3,400 ETH for a week of C at the maximum overrun), and each of the three guards considered changes the trust boundary for a loss the reference price rule already calls a door. State what would reopen the judgment, so it is re-run rather than inherited, and route agents to it from the contract guidance. Correct the per-occurrence price, which is a leaf bond or more, not one bond.
The factory's instantiateInner is permissionless and checks no argument, so an orphan can be a level-zero, root-kind clone with a nonzero nested dispute and no TournamentCreated, or a clone whose allowance never elapses and whose bonds are never recovered. The interface comments said a level-zero tournament has a zero nested dispute and presented the event as the record of a root's creation. Say so where a client would read it, with the rule that keeps a client clear of orphans: follow tournaments from the consensus's EpochSealed through each parent's NewInnerTournament, and join only what was read after finality. The node does both and never reads factory events. Bounding the level and the allowance in the factory was weighed and left out as machinery for a case the consumers do not have; the spec records that and when to look again (second contracts audit, N-03). Comments only: the ABI, storage layout and metadata-free bytecode fingerprints are unchanged, and only the metadata-included ones move.
solc 0.8.30 is inside the range (0.8.19 to 0.8.37) of a Yul optimizer bug announced on 2026-10-22 and fixed in 0.8.38: stale knowledge-base bookkeeping could replace a load with an outdated value or remove a needed store. It applies to any optimized via-IR code, which is how both contract projects compile, and its trigger cannot be checked from the source. Nothing is deployed for production, so pin the fixed compiler instead of analyzing the old bytecode. The bug list names nothing for 0.8.38 today; the readiness plan keeps the re-check for the freeze. No source changes. Every contract's bytecode moves, and with it every deterministic address; the ABI and storage-layout fingerprints of Tournament and the factory are unchanged. On the new pin: disputes 447, rollups contracts 19, gas witnesses 22 and 13, state-transition FFI 42, all passing. The one-sided gas witnesses still fit, so no allocation moves here; the dated recalibration is deferred to the end of the cycle and tracked in the to-do list.
Four things the code and tests already rely on, said where a reader would look for them: - One-transaction provability is a safety assumption. A sealed leaf nobody proves is decided by the clocks, which favor whoever joined the child first, so an inadmissible proof loses the dispute. The only proof an adversary can size embeds an input, bounded by the InputBox's 64 KiB cap, which the leaf gas fixture pins. - Latency bounds are strict. A one-level table has no slack under an inclusive reading; two levels keep a margin of G. - No clock can run out before its tournament stops accepting joins, so no timeout is enabled while joins are open and a child never closes before its parent. - A child cannot see that its parent consumed its result and keeps reporting a winner, then an expired one. Also said in the interface. Complete the refund slack list with the storage-clearing credits the meter does not net (17,500 to 35,700 units above receipt cost on a match-deleting action, for any caller), and give the measured unrefunded cost of the correct side's advances, seals and joins.
fineLeaves built a leaf as (family << 8) | (0x100 + i), so the low bit of the family was always set and families 2n and 2n + 1 gave the same table. The existing tests happened to avoid adjacent families; nothing said they had to (second contracts audit, N-09). fineLeaf(family, i) puts the family above bit 16 and bounds the index, and fineLeaves and the honest-survival handler build their leaves through it. No existing test depended on the collision: the dispute suite passes unchanged.
RefundReserve.t.sol owns the algebra and height-one traces at the work price, where no cap binds. These put the same identities on real clones, from the second contracts audit's value-flow review: - ReserveAtRefundCaps: three priced traces with the fee far above the cap, so every refund equals its action cap, over a root and its leaf children. The tightest one has one match fewer than joins and every match consuming its whole reserve; the root still ends with exactly one bond. - ProductionReserveSingleLevel and ProductionReserveTwoLevel: random schedules of joins, advances, seals, proofs, timeouts, propagations and child eliminations at random fee regimes. After every step, per clone: the balance is joins times bond minus refunds, each refund is within its cap, each match's refunds are within one bond, and one bond is held for every join not yet matched. At the end every bond is accounted for. Each fuzz has a sample test asserting that every action kind executed, that caps bound, and that clones ended both with and without a winner. The leaf proof is a stub, so none of this prices a real proof.
Three deterministic pins beside the callback behavior RefundCallbacks owns: - tryRecoveringBond releases its transient lock on every return path: a rejected payment, the full path, and the already-recovered path are called back to back in one transaction. - Refuted: a low gas limit lets an action complete while the 63/64 rule starves its refund callback. Over a sweep of the gas given to one advance, the call either reverts and pays nothing, or completes with the refund paid and the recipient seeing at least 45,000 of its 50,000 gas ceiling. - A clone takes value only through a join.
The factory's instantiateInner is permissionless and checks no argument. The second contracts audit (N-03) decided to document that rather than bound it; these traces are the executable half of the documentation. - A level-zero orphan is a root-kind clone with a caller-chosen window, base cycle and provider, a nonzero nested dispute, and no TournamentCreated. It reports ROOT_WINNER on its own. - An orphan with an allowance no parent would pass never closes, so a bond joined there stays locked: once as a level-zero look-alike of the genuine root, once as the reorg twin of FactoryNonceReorg with only the allowance changed. - Refuted: a parent calls, consumes or refunds a child it did not record, whether a byte-identical orphan or an address that is no clone. - The canonical provider fails with an array panic outside its table, and the factory forwards the level unchecked. On chain an orphan has no authority. The traces price a client that joins an address it did not reach from its parent after finality.
Three sets of deterministic schedules from the second contracts audit, in small injected geometry: - LeafHandover (N-01): at the deployed two-level formula with C = 0, two late Sybils, one of them parked under a full-clock holder and released after closure, make the honest proof revert twice. With every honest action inside its own G the second handover eliminates the honest commitment and the root reports a wrong winner, for two root bonds and four leaf bonds. The control lands proof and claim within one G of the seal together, the documented joint bound, and survives both. This is the trace behind "Why the handover stays" in dispute-game.md. - InclusiveLatencyBoundary (N-07): every expiry is inclusive, so at one level a join at G and a response at G lose by one block under exactly C of censorship; two levels keep a margin of G, and one unopposed delegation needs the whole formula for latencies of exactly G. - LeafRaceFastForward (N-04): a third party can play both sides down to the leaf seal in one block. Refuted as an attack on a party that joined nothing, since equal leaf clocks leave room for the build and one inclusion. Joined one block late, the correct commitment holds the shorter clock and an unproven race goes to the Sybil: safety needs the proof, or the claim, to land.
HonestSurvivalInvariant searches two levels. This generalizes its handler to any level count and any small heights: the same eager honest strategy derived from production state, the same adversary moves, one censorship ledger, plus a build model (one commitment at a time, T per level), a move that drives the deepest honest dispute down within one block, clock and topology invariants over every commitment ever joined, and a termination probe once no Sybil acts any more. One fuzz run is one schedule, so the search passes under forge's default gas limit: eight tables at one to four levels, G = 3, T = 6, C of 0, 2 or 5, both orientations, with the root allowance at the deployed formula or a stated number of inclusions below it. A schedule fails if the honest commitment is eliminated, if a pending honest action would land after the clock it draws on, if an invariant breaks, or if the root does not finish with the honest commitment as its winner. The least slack on a running honest clock is predicted as (L - 1)(G + 1) + 2 blocks, less G per inclusion below the formula. Four controls replay recorded schedules that survive at the last allowance keeping it positive and lose one inclusion further down, and four sample tests assert that the honest side reaches the leaf level and returns. A seeded search in a small box, from the second contracts audit's clock review; not a proof for any level count. It resolves a sealed leaf in one landing that picks the verb, the documented joint bound.
AdversarialWalk: any of four callers performs any verb, legal or not, on a root and on every descendant it creates, with time moving in small steps or to one block before, at, or after a boundary. The walk folds a ghost of the live matches from events, predicts from raw clocks and topology whether each call must succeed and what it must leave behind, and after every step compares legality, the timeout view, clock charges and refills, the sealed divergence against an independent scan of the claim tables, child arguments and linkage, the standing and inner-result views field by field, root finality, and per-clone balances. Eight claim tables include same-root impostors at the leaf and middle levels. DefendedWalk: the same adversary with one defended claim. The test contract is the state transition, so only the correct computation is provable, and an honest party follows the latency model of the security statement, read inclusively, under one censorship ledger at the deployed formula. It fails if an honest action reverts, the honest commitment is eliminated or locked out, or a root is decided for anything else. A control replays a recorded walk that the formula survives and one inclusion less loses. The model reads raw clocks and topology from production storage, so the walk is a consistency oracle rather than an independent specification. The second contracts audit made its agreement informative with 21 single-line mutants of src, 20 of which fail the walk; the last only drops an assert. Each walk has a sample test asserting that every transition class, and every kind of honest action, is reached.
The promoted tests change what the living documents can say. - dimensioning.md: the honest-survival evidence is no longer two levels only. The search now covers one to four levels, and the least slack it observed on a running correct clock is (L - 1)(G + 1) + 2 blocks, less G per inclusion below the formula, which is the unspent propagation inclusion of the balance argument. The defended walk adds a second adversary with inclusive latencies. Still seeded searches in small boxes, and the argument still awaits a reviewer other than its author. - dispute-game.md: the remaining liveness work is an argument for every level count, not a model beyond two levels. - prt-refund-accounting.md: the reserve identities are also checked on the production Tournament, at the caps and under random schedules. - prt-contract-testing.md: the evidence map gains the latency boundary, the handover, the walks and the multi-level search; the walk's model is described as a consistency oracle whose sensitivity rests on a mutation run; testSample and testControl join the naming conventions; test/config is named as the home of factory wiring and clone identity. - todo.md and plans/audit-readiness.md: the review of the argument by someone other than its author stays open, and says why the audit's re-derivation does not close it.
The record said the evidence was kept out of tree with promotion pending. It now lists each promoted test file against what it establishes, how the set was curated, the campaigns run during the review, and the seeded campaigns re-run on the promoted tests after the compiler pin moved. The follow-ups separate what has landed on the audit branch from what is open: the gas recalibration at the end of the cycle, the one devnet transaction N-08 needs, and the settlement phase. The reproduction note drops the raised gas limit the search no longer needs.
DaveConsensus had scenario tests and no stateful one, and two of its errors were never exercised by selector (second contracts audit). The handler composes the production InputBox, Application, DaveAppFactory, DaveConsensus and a real root tournament on an injected one-level table, and keeps its own ghost of the epoch bounds, the input list, sentry slots and claims, the staged snapshot, the settled values and each root's clocks. Before every call it asks the model: an allowed call must succeed and a forbidden one must revert with the exact error. After every step each consensus view is compared with the model: epoch bookkeeping and the 2^24 capacity, input finality, settled values, sentry slots and claim counts, the two readiness views, input binding and padding, tournament balances, and that the stored views stop moving once the application is foreclosed. Acceptance also runs while the retiring tournament's standing is replaced by another winner, a failed root or a revert: the staged snapshot settles regardless. The model runs under forge's invariant engine with three sentries and with none, as seeded walks at three sentry configurations that must reach every settlement operation, every root outcome and every refusal the model names outside the dispute moves, as a fuzz test whose run is one walk, and as fifteen directed schedules. DaveConsensusErrorPaths pins TournamentResultNotStaged in every state with nothing staged, and InputHashMismatch for every way the bytes can differ. Of 55 single-statement mutants of DaveConsensus.sol, 52 fail these suites and the other three fail the older ones; eight pass the suites that existed before, among them input bytes not checked against the InputBox hash and acceptance without a staged result. The model does not own the dispute itself, which is driven only as far as a root result needs; machine validity proofs come from the upstream emulator model, not from a machine; and a backlog's inputs have no bytes. Rollups suite 19 to 61 tests.
canStageTournamentResult and canAcceptStagedTournamentResult tell validators when to call stage and accept. Both read the live tournament and the block number whether or not the application is foreclosed, so after foreclosure isClaimStagingPeriodOver still turns true while the call it advertises reverts with ApplicationForeclosed (second contracts audit, S-01). Comments only. epoch-lifecycle.md already documents the freeze and the node reads foreclosure separately; this puts the caveat where a validator author reads the calling condition. The ABI is unchanged. The metadata hash, and with it the consensus bytecode, moves, as it already has in this cycle with the compiler pin.
The honest coverage statement predates the stateful model. It now says what the lifecycle handler composes and checks, what the error-path tests pin, where the model stops, and what its mutation run recorded, and it asks for the model to change with any change to staging, sentry or settlement logic. The padding rule gains its one exception: an index whose position overflows uint256 reverts with an arithmetic panic instead of padding. The state transition's 24-bit index cannot reach it, and the sum must stay checked, since a wrapped position would bind a settled input (second contracts audit, S-02).
The settlement section said "first read only". It now records the stateful model of DaveConsensus added on the audit branch: what it composes and checks, what it does not own, the mutation run (55 mutants, 52 failing the new suites, three failing the older ones, eight passing the suites that existed before), and the campaigns. Two leads came out of the model, neither a defect: the readiness views do not reflect foreclosure (S-01, now said in the interface comments), and an input index whose position overflows uint256 panics instead of padding (S-02, unreachable from a tournament; the sum must stay checked). What stays open for the settlement phase is the factory's reserved CREATE2 after the alpha.11 adoption and a re-read of the upstream diff.
The index line still described the rollups consensus contracts as read once. They now also have a stateful model; the phase stays open until the alpha.11 adoption.
The arm64 release build failed at `just bind` with "version not found in artifacts for this platform: 0.8.38". Foundry 1.5.1 embeds svm-rs 0.5.22, which takes Linux arm64 compilers from a community list at a pinned commit, and that list stops at solc 0.8.30. Solidity has published official Linux arm64 builds since 0.8.31; newer svm reads them, but the Foundry pin stays on 1.5.x. Foundry does not ask svm to download a pinned compiler it finds installed, so script/solc-linux-arm64.sh fetches the official build from binaries.soliditylang.org, by the SHA-256 that list and the GitHub release both give, into the directory svm resolves. On every other platform it does nothing. On every platform it fails when the projects' solc_version and its own pin disagree, so a compiler bump cannot leave the arm64 release build as the only place to notice. `just install-solc` runs it: CI's tool setup calls the recipe after installing Foundry, `just setup` includes it, and `just doctor` reports a miss with that fix. The script's test fakes the platform and the download and covers each directory svm can resolve, a compiler that reports another version, a file that does not match the checksum, and pin drift. Checked on macOS with the pinned Foundry: a compiler placed at ~/.svm/0.8.38/solc-0.8.38 in an empty home builds offline, and the same build without it fails. The Linux arm64 path itself runs first in CI.
This branch has not been deployed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The second whole-boundary audit of the contracts (2026-11-10) found no defect in
prt/contracts: no call sequence by which a wrong commitment beats a correct one that acts within the documented bounds, by which a foreign, stale or repeated child result is applied, by which a reported root winner changes, or by which more value leaves a tournament than entered it. This PR carries the record and everything the audit led to. The settlement boundary (cartesi-rollups/contracts) has a first read and a new stateful model; its phase stays open until the rollups-contracts alpha.11 adoption.Production source changes are the compiler pin and comments in four interface files. Nothing else under
src/moves.What is in it
docs/reviews/2026-11-10-contracts-audit/REVIEW.md: scope, method (four independent reads of the PRT boundary, three of them blind to the earlier review record), nine PRT leads (N-01 to N-09), two settlement leads (S-01, S-02), the evidence, and what stays open.C = 0and every honest action inside its ownG, and priced it: the correct side loses only its joint lateness beyond oneG, and draining a week of censorship budget costs the adversary on the order of thousands of leaf bonds.docs/dispute-game.md, "Why the handover stays", gives the argument, the three guards considered, and what would reopen it.instantiateInnerchecks neither level nor allowance. Documented rather than bounded: the node reaches tournaments only from the consensus through each parent'sNewInnerTournament, so an orphan is invisible to it. The interface comments anddispute-game.mdnow say what an orphan can look like.build!: solc 0.8.38 in both projects and in the gas script (N-02). 0.8.30 sits inside the range of the Yul optimizer bug fixed in 0.8.38 (announced 2026-10-22, 0.8.19 to 0.8.37), whose trigger cannot be checked from source. Every production bytecode moves; the ABI and storage-layout fingerprints ofTournamentand the factory do not.Tournamentis 17,058 bytes of runtime code.IDaveConsensus.solcomments), and the one exception to the input padding rule.test/accounting: the work reserve on the production Tournament with every refund at its cap and under random schedules at one and two levels; the boundaries of the two payment paths.test/config: what an orphan clone can look like, including the two shapes that lock a bond.test/properties: the leaf handover trace with its control, the inclusive-latency boundary, the leaf-race fast-forward, honest survival searched at one to four levels, and a model-based adversarial walk over two- and three-level clone trees with a defended variant.test/fixtures:fineLeafkeeps claim family and leaf index apart (N-09).DaveConsensus(rollups gate 19 to 61 tests). The handler composes the production InputBox, Application, factory, consensus and a real one-level root tournament and keeps its own ghost model: a call the model allows must succeed, a call it forbids must revert with the exact error, and every view is compared after each step. Focused tests pinTournamentResultNotStagedandInputHashMismatch, which nothing exercised by selector.dimensioning.md,dispute-game.md, the refund accounting doc, the rollups agent guidance,todo.mdand the audit-readiness plan.just install-solc, called by CI's tool setup and byjust setup, places Solidity's official build there by its pinned SHA-256. It does nothing on other platforms, and fails on every platform if the compiler pin and the script's disagree.just doctorreports a miss.Validation
Run locally on the final tree, through the repository's recipes:
prt-contracts::check-fmt,test-disputes(490),test-stf(42),test-stf-fuzzy,test-prt-gas(22 + 13).rollups-contracts::check-fmt,test(61).test-build-tooling,test-lua-client,lint-lua, andforge build --sizesin both projects.prt-contracts::compatibility-hashes: ABI and storage-layout fingerprints equal main's; every bytecode fingerprint differs, as a compiler move must.Deeper campaigns, all passing under
FOUNDRY_FUZZ_SEED=0x2026111001: 3,000 runs of each of the eight survival fuzz tests, 4,000 runs of each walk and each reserve fuzz, and 4,000 seeded walks of the settlement model at each of three sentry configurations. The settlement model also ran under forge's invariant engine at 1,500 runs of depth 256 with two seeds.Can the new tests fail?
DaveConsensus.sol, 52 fail the new suites and the other three fail the older ones. Eight pass the suites that existed before, among them input bytes not checked against the InputBox hash and acceptance without a staged result.Not run locally: the Rust workspace jobs (clippy, unit tests, node harness, KMS) and the e2e smoke, which exercise the node against contracts built with the new compiler. They passed in this PR's first CI run. The Linux arm64 install has a test that fakes the platform and the download; the real path runs only in CI's arm64 release build.
For the reviewer
docs/todo.md), with the devnet bundle and deployment addresses regenerated then.