Specification

The state machine, the parameters and the tables they imply, as the code has them.

This file is generated. cargo run -p truth-sim --release -- --spec > docs/SPEC.md rebuilds it, and a test fails if the committed copy has drifted. The transition table is not transcribed from anywhere: it is produced by driving the real state machine, attempting every action from every reachable state and recording what came back. A spec that claimed the machine refuses something it allows could not survive being written this way, which is the reason it is.

Account layouts are deliberately not copied here. They are the IDLs in packages/sdk/src/idl/, generated from the programs by anchor build and committed, so they are already the machine-readable, non-drifting description of every account, instruction and error code. Restating them in prose would be the drift this file exists to avoid.

Outcomes

An answer is one of four things. TooEarly re-opens the request; the other three end it. TooEarly and Unresolvable are abstentions: a juror is never slashed for either.

Ballots are counted into 34 slots.

The request lifecycle

Every row below was produced by attempting the action and recording the result. at says when the clock had to be for the attempt to be anything but early.

A TooEarly answer returns the request to Requested and pushes earliest_proposal_at forward by one tier window, at most 3 times. With no proposal by max_open_at — 14.0 days after the request becomes proposable — it resolves Unresolvable and the market refunds at par. A finalized answer may be corrected once, inside 7.0 days of becoming final.

The dispute ladder

Round 1 is a sampled panel of the tier's size. When governance has opened the agent bench and it can seat at least 3 model families with no operator holding more than 2 seats, Round 1 is drawn from bonded agents on the court's agent clock; otherwise, and on every round above the first, it is drawn from humans. An agent panel's decision binds on T0–T2 and is advice on T3–T4, where it escalates free to the grand panel with its verdict on the record. A round that cannot decide escalates free; a round that decides opens a 24.0 h appeal window. There are 2 panel rounds before the assembly, and a grand panel is 2n+1 capped at 15. When governance has opened assembly appeals, a grand panel's ruling can be appealed to the assembly and a grand panel that cannot decide escalates there free; with them closed, the grand panel is the last rung and one that cannot decide answers Unresolvable.

For a long-tail request with 60.00 USDC of bonds that works out at 120.00 USDC to the grand panel and 600.00 USDC to the assembly.

Seats and thresholds, by panel size

Both numbers are ceilings, which is why they are lumpy in the seat count: nine seats demand a tighter turnout than either seven or eleven.

Tiers

The scorer produces a total in 0..=1000, and the total picks the tier.

Time and jurors, by tier

An undisputed answer is final when its window closes. Each attestation, up to 3, cuts 25% of what remains, never below 25% of the window nor below 30 min, and one that would cut nothing because the window is already at that floor is refused; the fully attested column has all of them signed at once. A grand panel's jurors must not have sat on Round 1, so hearing both rungs in full takes the distinct jurors shown. A draw is offered at most 24 pool members, cut from the pool less the round below, so a pool of that many eligible jurors seats every grand panel in full; a thinner one seats short, decides on 2/3 of the seats it has, and is not drawn below 3.

Slashing

A misaligned juror never loses more than 3x what the round pays an aligned one, so the accuracy a juror needs before serving is worth it does not move with the tier. Reputation decays 1000 bps (10.00%) a quarter and floors at zero.

Settlement

Four verdicts. The caller picks one by comparing the proposal with the final answer, and the split follows. Rounding remainders go to the insurance fund, and the transfers always sum to the pot — proved by property test and checked against the chain by the oracle's differential test.

A request offers 3 attester seats, fixed when it opens. When the proposal stands, the proposer is paid the reward less the 5% treasury fee and the whole 20% attesters' pool, however many seats were filled, which is the figure shown before signing; each filled seat is paid an even share of the pool, and an empty seat's share goes to the insurance fund. The tag subsidy's attester bonus is split by seat the same way.

Worked on a pot of 1000.00 USDC proposer bond, 1000.00 USDC disputer bond, 100.00 USDC attester stake (one attester, 3 seats) and a 100.00 USDC reward.

Parameters

Every one of these is governance-tunable without a redeploy. The values are v0.

CourtParams

RiskParams

StakeParams

SettlementParams

InsuranceParams

ReputationParams

What is checked, and how

• Machine-checked under kani (crates/truth-core/src/proofs.rs): the lifecycle never reaches an illegal state from any state under any action; the scorer's terms stay inside the tier it picks; a round is carried only by a bloc that could carry a full panel; the proven-stake discount can only lower the bar.
• Property-tested in truth-core: value conservation at settlement, monotonicity of bond and window in the score, the weight cap, manifest validation over every field combination.
• Differentially tested against the deployed programs in programs/truth_oracle/tests and programs/truth_court/tests: the same inputs give the same scores, bonds, settlements and tallies on chain as in the crate.
• Simulated in truth-sim, with the results and their caveats in Economics.

Source: docs/SPEC.md in the axmc repo. Edit the file; the next deploy rebuilds this page.