Proof-rigor roadmap

This page is the plan for making the primitives more rigorously proved, given the audit. It is deliberately a ladder: each rung is a stronger claim with a different evidence standard. Most of the current suite is R1. The roadmap targets R2 for the core arms and leaves R3/R4 out of scope.

The rigor ladder

R2 is not refinement. It says the model’s accept/refuse decision matches an explicit table for the tested parameter domains, and that the deployed contract agrees with the same table. It does not say the table is complete over unbounded inputs. The target set is the 35 proved arms; all 35 are promoted.

Work items

Phase 2 progress

The guard count is 32 of 35 proved-model arms; the remaining three are read-only verification arms with no committed transition. Divergences are still tracked separately; a guard_eq proves the model guard, not the deployed guard.

Phase 3 candidates

• Give proofCells a trace-consumption relation and prove no cross-arm proof reuse (LR-03).
• Prove a full runExec commute theorem and retire the Store compatibility alias (LR-02).
• Promote the remaining 32 proved arms to proved-conformance (LR-06).
• Redesign the model for the remaining divergences: Claim K-Asset minting, Oracle evidence parties, VP proof caller, IdentityFactory effects, and nest tie handling (LR-08).

Guard extraction in practice

For an arm, define a pure guard g : σ → π → Bool and an effect f : σ → π → σ. Prove:

1. step s p = some (f s p) when g s p, and step s p = none otherwise.
2. A decision table transcribed from the contract’s guard, with columns for each status, role, proof, and height boundary, agrees with g on every row.
3. The deployed suite asserts the same table against the contract, and a vector file records the row.

The table is finite and the domains are chosen. The proof must not claim completeness beyond the table. native_decide is forbidden; the tables are small enough for cases/decide or explicit rewrites. This is the honest form of “the model matches the code” available without a Rholang semantics.

Versioned independence in practice

The current Store/World layer already has framing and commute theorems. The versioned layer adds generations and the accepted/rejected/stale outcome. The target is:

• set_commute and commit_commute for distinct cells;
• a frame theorem that a run on cell c leaves every other cell unchanged;
• runExec_append and runExec_commute_distinct for disjoint footprints;
• a projection theorem that a multi-cell run restricts to each cell’s serialized run.

The last theorem is the bridge to core_races_not_representable: the headline result is the per-cell projection of the versioned run, while independence is a separate property of disjoint footprints. The roadmap does not claim that independence implies global race freedom.

Proof-cell linearity in practice

Arm.proofCells must become a relation, not metadata. The plan:

1. A proof event is an Event (ProofState α) on a proof cell, as in ProofVersioned.
2. An arm event is related to a proof event by a Consumes predicate carrying the proof cell, the arm, and the payload.
3. A well-formed arm run requires every declared proof cell to be consumed before the arm’s commit, exactly once, and no two arms to consume the same proof generation.
4. core_no_proof_reuse_across_arms is a trace theorem over the combined event list, not a statement about one proof cell in isolation.

This still does not prove that the deployed private capability is unforgeable. It proves the consumption discipline of the model.

Invariant coverage after the roadmap

What remains unprovable here

No mechanized Rholang semantics, no refinement of the deployed contracts, no proof of name unforgeability, chain-height authenticity, JSON schema validity, phlo exhaustion, scheduler fairness, or liveness. A model theorem is never cited as deployed refinement. proved-conformance is finite evidence, not a proof over all inputs.

Acceptance

• Every deployed mutating arm has an Arm value and, when proved-model, a guard_eq entry or an explicit owed reason.
• VWorld has the commute/frame theorems and the independence alias is no longer a Store alias.
• proofCells is read by a consumption theorem.
• The pair matrix is complete or every unmodeled pair has a reason.
• check_lean --audit-coverage, check_flows, check_race_matrix, and check_arm_guards enforce the above; check_audit --phase2 requires an approved review and no open P0/P1 disposition.
• No sorry, admit, native_decide, or new axiom.