r-gen — CoEngineers / Ingenesist

r-gen is the first reasonably complete suite of Rholang contracts, paired with a Lean 4 model, for Dan Robles’ CoEngineers and Ingenesist Project vision. The papers start from a plain problem: “the value of engineering is invisible” (@robles2017stewardship p.3). The suite makes the work and its validation first-class, durable records.

The handshake is the paper’s claim → validation → approval sequence (@zhong2019bridge p.4); the claim is the quantity and the validation the quality (@robles2020innovation p.5):

Claim (quantity, work element, selection criteria, clock, comments, value proposition ref)
  -> Validation (quality, qualified validator, evidence)
  -> Approval (acceptable completion, liability)
  -> K-Asset (the claim+validation pair, with approval)

A K-Asset is the paper’s pairing: “Each pairing forms a single node with two branches constituting a knowledge asset – ‘K-asset’” (@robles2020innovation p.4). A ValueProposition is a separate cell, composable with a claim or K-Asset by reference (@mathews2017bim p.7). An Oracle case resolves a dispute through one credential-proved adjudicator (@robles2016nspe p.25). A Provenance cell keeps the asset’s documents and comments with the asset (@robles2016nspe p.29).

The repo is the contracts, the Lean model, and the paper-linked documentation. The core deliberately does not mint, price, transfer, score risk, run panels, or administer a governance layer. Those are extensions. The Pareto ledger states why each primitive is present and what was removed; it is a design test, not the repo’s purpose. The paper-to-code matrix links each core idea to the contract, the Lean theorem, and the tests.

The design test is: remove the primitive; can the remaining set still express a claim, a validation, a value proposition and a K-Asset? If yes, it was not core.

Claim, validation, K-Asset

The handshake is the paper’s claim → validation → approval sequence (@zhong2019bridge p.4); the claim is the quantity and the validation the quality (@robles2020innovation p.5). A Claim is one linear cell. It carries:

• the claimant and the work element (titleHash, discipline, jurisdiction, projectRef);
• the selection criteria (the paper’s Talent Pool → Selection Criteria step, @zhong2019bridge p.4);
• the statement/definition hashes and the quantity {unit, value};
• the agreed clock (deadlineHeight, commentUntilHeight) and comment hashes (@zhong2019bridge p.5);
• an optional value-proposition reference.

A Validation consumes the open Claim. If the validator holds a credential issued by the genesis issuer and matching the claim’s selection criteria, the claim creates a K-Asset and transitions to validated (or rejected for an invalid verdict). A second validation cannot succeed: the Claim cell is no longer open.

The K-Asset is the pair: “Each pairing forms a single node with two branches constituting a knowledge asset – ‘K-asset’” (@robles2020innovation p.4). It carries the claim+validation pair, the validator’s credential, the verdict and quality, and the approval state. Approval is “an acceptable completion” (@zhong2019bridge p.4). Approval records the approver, conditions, liability and an approvalVersion. A dispute opens an Oracle case with the K-Asset’s private applyDecision capability; the case stores that capability, so a decision on one K-Asset cannot be applied to another.

A ValueProposition is a separate cell: a proposer states a value statement, terms and beneficiaries; a qualified validator validates it; a K-Asset may reference a validated value proposition. The papers name “the new value proposition” (@mathews2017bim p.7) but define no state machine; the separate primitive is a user decision recorded in the Pareto ledger. See the primitive pages.

Bridge inspection walkthrough

1. Alice registers an identity under her REV address (@robles2016nspe p.40).
2. The genesis issuer issues Bob a Validator credential and Carol an Approver credential.
3. Alice proposes a value proposition for the inspection and Bob validates it (@mathews2017bim p.7).
4. Alice creates a claim: twelve deck inspections, a statement hash, a definition hash, a selection criterion for Validator/structural/US-TX, a clock and a comment window (@robles2020innovation p.5; @zhong2019bridge p.4-5).
5. Bob validates. The Claim cell creates the K-Asset and becomes validated (@robles2020innovation p.4-5).
6. Carol approves. The K-Asset becomes approved; the approval records liability and an approval version (@zhong2019bridge p.4). No token is minted.
7. If a party disputes, the K-Asset opens an Oracle case with its private apply capability. Dave, the named adjudicator with an Oracle credential, decides (@robles2016nspe p.25). Execution calls the K-Asset’s private apply; the K-Asset becomes upheld or revoked.
8. Alice creates a provenance cell for the K-Asset and anchors the inspection report (@robles2016nspe p.29; @zhong2019bridge p.3). The anchor is immutable; verify recomputes the anchor’s presence.

The harness runs this path in harness/unit_core.py; the same-deploy race suite is harness/concurrency_core.py.

Quickstart

make venv
make build-check
make parse-check
make check-core-boundary
make check-concurrency
make check-citations

export RHOLO_DIR=../RNodeRust
DEVNET_PREFIX=rgen make devnet-up keys install
make unit-core
make concurrency

The installer deploys seven terms in dependency order and wires factory URIs at install time:

00_root -> 10_identity -> 11_credentials -> 30_oracle -> 40_provenance
        -> 22_value -> 20_claim

There is no r-cash dependency in the core. KAT, payments, risk, panels, admin, handles and metrics are extensions and are not installed by make install.

If the default devnet-bootstrap volume already exists, use DEVNET_PREFIX=rgen as shown; it starts an isolated rgen-bootstrap on 40403/40405.

Identity

Paper anchor

“Records” (identity/credential context). — @robles2016nspe p.40

“‘Claim’ and ‘Validation’ represent a key mechanism i.e. the ‘handshake’.” — @zhong2019bridge p.4

The papers assume identified practitioners and participants. r-gen turns that assumption into a first-class, per-address identity cell and a first-writer-wins directory.

What the paper means

The NSPE record/identity passage treats records as attributable to a person or firm; the Bridge handshake assumes the talent pool and selection criteria identify who may act. The core does not invent a global reputation system; it records the address that owns an identity and the address that authored each fact.

How the Rholang expresses it

• contracts/src/deploy/10_identity.rho — IdentityFactory@"create" consumes directoryState, rejects a duplicate address, creates a per-address Identity cell, and appends the address-to-URI entry.
• IdentityDirectory@"lookup" / "count" are peeks of directoryState; they never write.
• Identity@"get" peeks identityState; Identity@"update" consumes it and requires the caller to be the current owner.

What the Lean proves

• RGen.Directory.create_unique — a successful create makes a second create at the same address fail.
• RGen.update_owner_requires_owner — only the current owner can transfer the identity.
• RGen.update_owner_preserves_address — the address is never rewritten.
• RGen.core_arm_authority — the create/update decisions factor through their consumed cell.

Deliberately excluded

Handles, global uniqueness of human-readable names, and reputation scores are extensions. The core uses the REV address as the identity.

See also

• Core arm reference
• Paper-to-code matrix
• Pareto ledger
• Suite: harness/unit_identity.py

Issuer, credential, and proof

Paper anchors

“A ‘Permissioned by Qualifications Blockchain’, facilitated by an Oracle…” — @mathews2017bim p.7

“permissioned by qualifications” and the validator must be qualified — @zhong2019bridge p.6

“the adjudicator is deemed the most appropriate person” — @robles2016nspe p.25

“An Oracle contract is an adjudicated contract…” — @robles2016naic p.9

What the paper means

The papers put qualification before action: a validator, approver, or adjudicator must hold a credential that a recognized issuer covers. The core therefore makes the credential a linear cell and the proof a one-shot capability, not a caller-supplied boolean.

How the Rholang expresses it

• contracts/src/deploy/11_credentials.rho — the genesis Issuer is immutable and has no revoke arm. Issuer@"authorize" and "covers" are monotone reads of issuerState.
• CredentialFactory@"issue" rejects self-issue and appends the credential to factoryState; CredentialFactory@"verify" reads that append-only registry.
• Credential@"prove" consumes credState, checks subject/active/scope/issuer, creates a one-shot Proof cell, re-posts the credential, and returns the proof URI.
• Credential@"revoke", "renew", and "attest" consume the same cell.

What the Lean proves

• RGen.C1_prove_requires_active — a proof requires an active credential at the stated height.
• RGen.C2_revoke_blocks_prove — a revoked credential cannot prove.
• RGen.C3_issuer_immutable — the issuer transition relation has no constructor.
• RGen.CredentialState.prove_snapshot — the proof payload is a pre-revoke snapshot.
• RGen.core_arm_authority and RGen.proof_take_once_versioned — the decision is authority from the consumed credential plus the one-shot proof payload.
• Pair matrix: credential_prove_revoke_never_after, credential_prove_revoke_snapshot, credential_attest_same_never_after.

Deliberately excluded

Issuer rotation/revocation is a governance extension. Reputation and issuer chains are extensions. The core issuer is one genesis cell.

See also

• Paper-to-code matrix
• Pareto ledger
• Race-freedom proof
• Suites: harness/unit_credentials.py, harness/integration_core.py

Claim

Paper anchors

“The claim serves as the quantity (definition) and the validation serves as the quality (characteristics).” — @robles2020innovation p.5

“‘Claim’ and ‘Validation’ represent a key mechanism i.e. the ‘handshake’.” — @zhong2019bridge p.4

“pre-defined and agreed upon ‘clock’ … and all participants can see the specific actions to be taken and their status” — @zhong2019bridge p.5

What the paper means

A claim states the work element, its quantity, its definition, and the agreed clock. It is the quantity half of the handshake; validation is the quality half. The claim is a durable record, not a transient message.

How the Rholang expresses it

• contracts/src/deploy/20_claim.rho — ClaimFactory@"create" checks the required fields and appends the claim URI to claimRegistryState.
• The Claim cell stores work, selectionCriteria, statementHash, definitionHash, quantity, evidence, valuePropositionRef, deadlineHeight, commentUntilHeight, and comments.
• Claim@"comment" appends inside the comment window; Claim@"withdraw" and @"expire" are terminal; Claim@"validate" consumes the cell and creates the K-Asset.

What the Lean proves

• RGen.ClaimState.validate_once — a claim validates once.
• RGen.ClaimState.validate_requires_open, validate_requires_non_claimant, validate_within_deadline, validate_requires_subject, validate_requires_no_kasset.
• RGen.ClaimState.validate_creates_exactly_one_kasset — a validated claim has exactly one K-Asset reference.
• RGen.claim_validate_blocks_comment, claim_validate_expire_two_way, claim_validate_withdraw_two_way, claim_comment_comment_appends.

Deliberately excluded

Global claim registries for search, human-readable identifiers, and cross-claim aggregation are extensions. The core registry is append-only creation only.

See also

• Validation
• K-Asset
• Paper-to-code matrix
• Suites: harness/unit_claim.py, harness/unit_core.py

Validation

Paper anchors

“The claim serves as the quantity (definition) and the validation serves as the quality (characteristics).” — @robles2020innovation p.5

“‘Claim’ and ‘Validation’ represent a key mechanism i.e. the ‘handshake’.” — @zhong2019bridge p.4

“validation of credentials should be in place before validation of events” — @zhong2019bridge p.6

What the paper means

Validation is the quality half of the handshake. It requires a qualified validator who is not the claimant, a credential proof, a verdict, and evidence/quality records. It is the moment the claim and validation pair becomes a K-Asset.

How the Rholang expresses it

• Claim@"validate" consumes claimState, rejects self-validation and late validation, verifies the credential URI in ClaimFactory/CredentialFactory, resolves the credential, calls Credential@"prove", takes and checks the proof (subject, credential URI, height), then calls finalizeValidation.
• finalizeValidation maps the verdict to the claim status and K-Asset status, calls makeKAsset, and commits the claim with validationRef and kassetRef.

What the Lean proves

• RGen.ClaimState.validate_once and validate_requires_non_claimant.
• RGen.ClaimState.validate_within_deadline and validate_expired_after_deadline.
• RGen.ClaimState.validate_requires_subject and validate_sets_kasset.
• RGen.C1_prove_requires_active / C2_revoke_blocks_prove — the credential proof is the authority, not a peek.
• RGen.claim_validation_exactly_one_kasset — composition with the K-Asset.

Deliberately excluded

Validator panels, weighted votes, reputation weighting, and off-chain quality scoring are extensions. The core records the verdict and quality hashes.

See also

• Claim
• K-Asset
• Race-freedom proof
• Suite: harness/unit_claim.py

K-Asset

Paper anchors

“Each pairing forms a single node with two branches constituting a knowledge asset – ‘K-asset’ – which is memorialized by the creation of an electronic token awarded to each participant in a pair.” — @robles2020innovation p.4

“The claim serves as the quantity (definition) and the validation serves as the quality (characteristics).” — @robles2020innovation p.5

“‘Approval’ represents an acceptable completion.” — @zhong2019bridge p.4

“‘Blocks’ on a blockchain are nested in this manner as well.” — @zhong2019bridge p.6

What the paper means

The claim+validation pair is the K-Asset. Approval is a separate, qualified act after validation. K-Assets can be nested; the core records the nesting order and the approval data without minting a token.

How the Rholang expresses it

• contracts/src/deploy/20_claim.rho calls makeKAsset from finalizeValidation; the K-Asset library is in contracts/src/lib/KAsset.rho.
• KAsset@"approve" requires validated/conditional, a non-claimant, non-validator approver, a credential proof, and (when a VP is referenced) a validated VP proof.
• KAsset@"reject" requires the same qualification and records the rejection.
• KAsset@"proveApproved" creates a one-shot approval proof.
• KAsset@"nest" is two-phase: a read-only pre-pass, child proveApproved proofs, then a consume of the parent and a final duplicate/scope/order check.
• KAsset@"openDispute" passes the private Apply capability to an oracle case.

What the Lean proves

• RGen.K1_approve_credential — the credential proof subject is the approver.
• RGen.K2_approve_status — approval is only from validated or conditional.
• RGen.K3_nest_acyclic — strict order and no nesting cycle.
• RGen.KAssetState.approve_requires_vp_proof, approve_by_claimant_refused, reject_requires_credential_proof, nest_child_below_parent, nest_child_scope.
• Pair matrix: kasset_approve_reject_two_way, kasset_openDispute_proveApproved_never_after, kasset_nest_same_never_after_arm.

Deliberately excluded

KAT/receipt minting, pricing, liability accounting, and token transfer are extensions. The core records approval and nesting facts; an extension can mint when it chooses validation or approval as its receipt timing.

See also

• Claim, Validation, Oracle
• Paper-to-code matrix
• Suites: harness/unit_kasset.py, harness/integration_core.py

Value proposition

Paper anchors

“This is in essence ‘the new value proposition’.” — @mathews2017bim p.7

“develop a ‘new value proposition’ to extract reward … also the intrinsic intangible value” — @mathews2017bim p.9

What the paper means

The papers name a “new value proposition” and connect it to intrinsic intangible value and reward. They do not define a value-proposition state machine. r-gen makes it a separate, user-requested primitive: a proposition cell that a qualified validator can validate, that can be disputed, and whose validated state can be proved to an approver.

How the Rholang expresses it

• contracts/src/deploy/22_value.rho — ValuePropositionFactory@"propose" creates a per-proposition cell and appends it to vpRegistryState.
• ValueProposition@"validate" consumes the cell, resolves the credential by URI, calls Credential@"prove", takes/checks the proof, and commits the validation.
• ValueProposition@"proveValidated" creates a one-shot validated proof for an approver.
• ValueProposition@"withdraw" is proposed-only; @"openDispute" accepts proposed/validated and refuses a second dispute; Apply@"applyDecision" resolves upheld/revoked/partial.

What the Lean proves

• RGen.V1_validate_once — validation is once.
• RGen.V2_dispute_blocks_prove — a disputed proposition cannot prove validated.
• RGen.VPState.validate_requires_non_proposer, proveValidated_requires_validated, openDispute_requires_status, terminal_no_transition.
• Pair matrix: vp_validate_withdraw_two_way, vp_proveValidated_openDispute_ordered, vp_decision_decision_never_after.

Deliberately excluded

The papers do not define the state machine, so the states and guards are a user decision. The core does not price, reward, mint, or score the proposition; those are extensions.

See also

• K-Asset
• Pareto ledger (marks this as a user decision)
• Suite: harness/unit_value.py

Oracle

Paper anchors

“the adjudicator is deemed the most appropriate person to be performing the adjudication.” — @robles2016nspe p.25

“An Oracle contract is an adjudicated contract…” — @robles2016naic p.9

“An Oracle contract is an adjudicated contract with the added requirement the adjudicator … is deemed the most appropriate person” — @mathews2017bim p.8

What the paper means

An oracle case has one named adjudicator, chosen because they are the most appropriate person, not a weighted panel. The adjudicator must prove a credential at decision time. The decision is applied to the subject through the subject’s own capability.

How the Rholang expresses it

• contracts/src/deploy/30_oracle.rho — OracleFactory@"open" checks the adjudicator credential by registry URI and requires its subject to match the named adjudicator.
• OracleCase@"decide" consumes caseState, uses the stored adjudicatorCredentialUri, calls Credential@"prove", takes/checks the proof, and records the decision.
• OracleCase@"execute" is two-phase (decided → executing → executed), re-posts before calling the subject’s private applyDecision, and is one-shot.
• OracleCase@"expire" and @"close" guard the terminal paths.

What the Lean proves

• RGen.O1_execute_bound_once — execution is subject-bound and one-shot.
• RGen.O2_close_finished — closing requires executed/expired.
• RGen.OracleState.decide_once, decide_requires_proof, execute_subject_bound, execute_once, close_open_refused.
• Pair matrix: oracle_decide_expire_two_way, oracle_execute_execute_never_after, oracle_decide_evidence_never_after.

Deliberately excluded

Panels, voting, tallying, random selection, and fund/payment execution are extensions. The core has one adjudicator and no payment arm.

See also

• K-Asset, Value proposition
• Race-freedom proof
• Suite: harness/unit_oracle.py

Provenance

Paper anchors

“The asset becomes the keeper of its own information.” — @robles2016nspe p.29

“their provenance and ownership” — @zhong2019bridge p.3

“Tokens issuance marks points where risk is transferred from one party to another.” — @zhong2019bridge p.6

What the paper means

Provenance belongs to the asset, not to a global book. Documents and comments are anchored to the asset; a parent hash gives the minimal document graph. The core records anchors and comments; token issuance and risk transfer are extensions.

How the Rholang expresses it

• contracts/src/deploy/40_provenance.rho — ProvenanceFactory@"create" creates a per-asset cell with an assetRef and a writer list.
• Provenance@"anchor" requires a writer, a non-empty hash, and a non-duplicate anchor; it appends {id, kind, hash, parentHash, by, at}.
• Provenance@"comment" requires a writer and appends a comment.
• Provenance@"verify" is a monotone read of the anchor list.

What the Lean proves

• RGen.P1_anchors_append_only — anchors are append-only.
• RGen.ProvenanceState.anchor_unique, verify_monotone, addComment_requires_writer, addAnchor_nonempty_hash.
• Pair matrix: provenance_anchor_anchor_same_never_after, provenance_comment_comment_appends.

Deliberately excluded

Global provenance registries, IPFS pinning policy, and risk-transfer/token issuance are extensions. The core anchors hashes and comments to the asset.

See also

• Paper-to-code matrix
• Suite: harness/unit_provenance.py

Creation registries

The core has append-only creation registries for credentials (factoryState), claims (claimRegistryState), value propositions (vpRegistryState), and identities (directoryState). They are engineering infrastructure, not a paper primitive.

What they do

• Serialize creation so a forged URI cannot be resolved as genuine.
• Make verify(uri) monotone: once true, it stays true.
• Keep the hot path per-entity; validation, approval, decision, nesting, and provenance do not write a registry.

How the Rholang expresses it

• CredentialFactory@"issue" writes factoryState; @"verify" peeks it.
• ClaimFactory@"create" writes claimRegistryState; @"verify" peeks it.
• ValuePropositionFactory@"propose" writes vpRegistryState; @"verify" peeks it.
• IdentityFactory@"create" writes directoryState; IdentityDirectory@"lookup" peeks it.

What the Lean proves

• RGen.Registry.verify_monotone — registration never un-verifies an entry.
• RGen.Registry.register_twice / register_unique — a duplicate registration is refused.
• RGen.Directory.create_unique — first-writer-wins identity creation.
• RGen.core_arm_authority — the create/issue decisions factor through their consumed cells.

Deliberately excluded

There is no global nonce, no admin registry, and no off-chain indexer. Registries are creation-only serialization points.

See also

• Core arm reference
• Formal model

Pareto ledger

The Pareto test: remove a primitive and ask whether the remaining set can still express the papers’ claim → validation → approval handshake, the K-Asset, and a value proposition. If it can, the removed thing was not core.

Labels: paper-derived (a passage requires it), paper-adjacent (a passage names the idea but does not define its mechanism), user decision (the user asked for it), or engineering infrastructure (needed to run, not a value primitive).

Core (default install and verification)

Each core primitive has a page with paper quotes, the Rholang arm/field references, and the Lean theorem names under docs/src/primitives/; the row-by-row linkage is paper-to-code.

Extensions (excluded from the default build)

What was removed or narrowed

• Four-axis quality rubric (completeness/correctness/traceability/fitness): no paper defines these dimensions. The core carries an opaque quality map and a qualityNotesHash; the validator supplies the characteristics.
• Fixed reputation tiers and 50/50 split: the papers say “in proportion to reputation”, not these numbers. Reputation is an extension.
• Risk class ladder and validator/approver levels: an extension policy, not core.
• Weighted oracle panels / tally: the core has one adjudicator; panels are an extension.
• ERTP KAT, transfer, slashing: the core does not mint or transfer; a receipt extension owns those races.
• Admin multisig / pause / freeze / setParams: the core has no admin arms.
• Handles: the identity directory is keyed by REV address.
• WorkBook / global books: the core uses per-claim cells and the claim carries work metadata.
• Dead configs/rgen.json and GenAdmin.params: removed; core constants live where they are used.

Paper facts the docs must not overclaim

• “Pareto” does not appear in the seven papers. “Primitive” appears once, rhetorically. The Pareto framing is the user’s.
• “Value proposition” is a phrase in BIM, not a defined state machine. The separate ValueProposition cell is a user decision.
• IMECE mints at validation; Bridge supports risk-transfer at approval. The core avoids the choice by not minting.

Paper-to-code matrix

One row per core idea: paper key and page, the quoted claim, the Rholang expression, the Lean theorem, and the behavioural/corpus tie. This is the extensive linkage between the Robles papers and the Pareto core. The core rows are anchored in @robles2020innovation p.4, @robles2020innovation p.5, @zhong2019bridge p.4, @zhong2019bridge p.6, @robles2016nspe p.29, and @mathews2017bim p.7.

Not mapped to a core primitive

• @robles2017stewardship p.3 — reputation/Quant and the invisibility thesis. Background for why claim and validation are first-class; tokenisation and reputation are extensions.
• @robles2020innovation p.3 — Risk = S×P×E. Deferred risk extension.
• @robles2020innovation p.6-7 — WIKiD tools. Deferred metrics extension.
• @robles2016naic p.4, @robles2016nspe p.14 — insurability questions. Deferred risk extension.
• @caase2018agenda — included but uncited; not a source for a core primitive.

Reading the columns

• Rholang names the deploy term/arm or the private library arm. The // Paper: header in each term carries the same page cites.
• Lean names the essential theorem from spec/lean/RGen/Pareto.lean and the per-primitive model. The proof is model-level; see Race-freedom proof.
• Tie is a behavioural suite or corpus row. It is finite evidence, not refinement.

Code-header citation index

@mathews2017bim p.7, @mathews2017bim p.8, @robles2016naic p.9, @robles2016nspe p.25, @robles2016nspe p.29, @robles2016nspe p.40, @robles2020innovation p.4, @robles2020innovation p.5, @zhong2019bridge p.3, @zhong2019bridge p.6

Design rationale

Why the Rholang is written the way it is. Rows marked r-gen are engineering decisions with no paper basis; they must not be presented as paper-derived.

Concurrency

The declared serialization points are rootState, directoryState, issuerState, and factoryState.

Consume-first liveness. Holding a consumed cell across a cross-contract call is safe only if the call graph is acyclic. The only cross-entity acquisitions are: Claim.validate creates a K-Asset (new cell); K-Asset.openDispute creates an Oracle case (new cell); Oracle.execute calls the subject’s private apply (case → subject). There is no reverse edge: openDispute creates a case and never consumes one, and the subject never calls the case. The concurrency lint and the same-deploy tests enforce this.

Paper-derived process choices

User decisions (not paper-derived)

Explicit non-goals

• The core does not mint, price, or transfer anything.
• The core does not call an extension. Extensions read core facts by URI/capability.
• The core does not claim “maximal concurrency” absolutely. It claims: no shared mutable cell across independent entities; one writer per entity; independent-entity transitions do not serialize. Within one entity, serialization is inherent and intentional.

Formal model

The Lean model is in spec/lean/. It is built with Lean v4.12.0, no Mathlib, no external require. make lean-check builds it, rejects sorry/admit/native_decide and declared axioms, audits the public theorems, and checks the emitted corpus.

What is proved

Lean proves properties of the model, not of the deployed Rholang. There is no mechanized Rholang semantics and no refinement theorem. The flow manifest and the conformance corpus are traceability, not refinement. This is the same boundary r-cash and r-share draw around proved-model.

Module map

Cell semantics

Store α maps a CellId to a list. run interprets peek, take, put, call, and commit. take requires a singleton and records the cell as held; put requires the cell empty and held, then erases one occurrence from the held list; call is refused on a held cell; commit is one atomic read-modify-write and never exposes an empty cell.

The held list records a take by consing without deduplicating. Held agreement is therefore stated as per-cell occurrence counts (occ), which take/put preserve; plain membership is not preserved by put when the initial held list has duplicates.

World α maps a cell to Option α and is the application-level concurrency model: commit_commute, commit_same_cell, and commit_preserves_other are the three commit lemmas used by the entity proofs.

Per-primitive guarantees

Representative public names (the full list is RGen/Audit.lean):

• Credential: prove_requires_subject, prove_requires_active, prove_requires_scope, prove_snapshot, prove_after_revoke, prove_wrong_subject, credReach_preserves_identity.
• Value proposition: validate_once, proveValidated_requires_validated, prove_after_dispute, dispute_once, terminal_no_transition.
• Claim: validate_requires_open, validate_requires_non_claimant, validate_within_deadline, validate_once, validate_sets_kasset, validate_creates_exactly_one_kasset, terminal_no_transition.
• K-Asset: approve_only_from_validated_or_conditional, approve_requires_credential_proof, approve_requires_vp_proof, approve_by_claimant_refused, nest_requires_order, nest_refused_unsorted, nest_acyclic, proveApproved_requires_approved, approvedAt_stable.
• Oracle: decide_requires_adjudicator, decide_requires_proof, decide_once, execute_subject_bound, execute_once, close_requires_finished, close_open_refused.
• Provenance: anchors_append_only, anchor_unique, verify_monotone, addComment_requires_writer.

One-shot proofs

ProofState α is { data : α, used : Bool }. take returns the payload and marks the cell used; take_second and take_take show a second take fails; take_data shows the payload is a snapshot. The used flag is observability and testability, not the security boundary: the capability is private and unforgeable in the deployed model.

Credential, value-proposition, and K-Asset proofs use the same cell. Revocation and dispute after a proof are non-retroactive by construction: the proof carries a snapshot of the pre-state.

Axiom audit

tools/check_lean.py --audit elaborates RGen/Audit.lean. On 2026-11-04 the listed 131 theorems reported only propext and Quot.sound (Classical.choice is permitted but unused). The list is hand-maintained; the proof audit records that gap as RGA-006.

Manifest and corpus

spec/flows/core.yaml maps every deployed arm to a Lean declaration and one of four statuses: proved-model, proved-conformance, owed, open. At this checkpoint 34 of the 65 deployed arms are proved-model, 0 are proved-conformance, and 31 are owed (read-only arms, creation registries, and extensions). Identity.update is owed because the deployed profile patch has no model transition. tools/check_flows.py enforces coverage, deployment, and declaration existence.

spec/vectors/core.tsv is emitted by lake exe emit from RGen/Emit.lean. tools/gen_vectors.py --write refreshes it; tools/check_core_vectors.py rejects drift. proved-conformance is claimed only for a row that is both emitted and asserted by a suite; no row is claimed yet.

Honest limits

• The deployed contracts use the proof-URI design and the reconciled guards; the race proof is core_races_not_representable. The arm-to-model map is hand-transcribed, not a refinement.
• deadlock_free_of_rank is a lock-order theorem under finite cells and no dynamic locks. It is not global scheduler liveness or starvation freedom.
• Race freedom is structural: proof issuance is the linearization point. The model does not enumerate interleavings.
• The nest pre-pass in the contract is a hint; the child proof is the authority. The model has no KAsset → KAsset acquisition edge.

Race-freedom proof

The core claim is a Lean model theorem, not a behavioural test. This page states the theorem, the model, and the boundary.

Headline theorem

RGen.core_races_not_representable (spec/lean/RGen/RaceFreedom.lean):

For every Run over a versioned cell world, and every cell c, NoTwoSameExpected c es: no two events on c in the run share an expected generation.

Run is the inductive execution semantics in spec/lean/RGen/Linear/Exec.lean. NoTwoSameExpected is occurrence-level: for every pair of same-cell events in the run, their expected generations differ. Accepted commits are a subset of events, so no two accepted commits share a generation. The quantified statement ranges over all runs, not a chosen schedule.

The proof is runExec_no_same_expected, via per-cell projection (runCell) and the AppliedExpecteds invariant: a successful run can only apply a same-cell event when its expected generation equals the cell’s current generation, then advances the generation. The executable fold and the proof semantics are tied by runExec_sound and runExec_complete.

Consume/post is atomic commit

RGen.VWorld.take_take_blocks: after a take, a second take on the same cell fails without a post. RGen.VWorld.take_post_commit_equiv: the deployed for (@s <- cell) { ...; cell!(s') } pattern equals the atomic VWorld.commit step. RGen.VWorld.commit and RGen.Event.apply advance the generation on both acceptance and refusal, matching a consume/re-post on every path.

Decision authority

RGen.Arm.decision_factors and RGen.core_arm_authority: every arm built with Arm reaches its decision through its consumed cell and nothing else. Arm.decision reads only w.cell a.cell. This is functional dependence, not permission: the theorem does not say who may invoke the arm. Arm.proofCells is metadata and is not read by the decision; the one-shot proof cell is proved separately. The proof audit records both gaps (RGA-002, RGA-012).

RGen.cross_cell_read_not_authority: if a decision varies with a cell d while every other cell is held equal, it does not factor through the consumed cell c, and every authority set for it must contain d. This is the formal “a peek is not a linearization point” rule. A peek of d can be a linearization point at d; then d must be consumed/authority, not an ambient read. RGen.peek_not_authority is the two-cell form.

RGen.proof_take_once_versioned / RGen.core_proof_payloads_consumed: after an accepted proof take, the next take rejects; the payload is a snapshot and is not reachable twice.

Pair matrix

spec/flows/races.yaml records every proved arm pair, its class, and the Lean theorem. tools/check_race_matrix.py verifies the class vocabulary, uniqueness, and theorem existence. There are 31 pairs: 19 exclusive, 11 ordered, and 1 independent.

• exclusive: whichever arm runs first, the second arm’s guard refuses on the post-state.
• ordered: one direction is refused; the other is the serialized/non-retroactive order (for example prove then revoke is admitted and the proof remains a snapshot, while revoke then prove refuses).

Representative theorems:

Guard reconciliation

The model was partially reconciled with the deployed arms before these proofs: VP withdraw is proposed-only; VP openDispute accepts proposed/validated with no prior dispute; K-Asset approve rejects the validator; K-Asset openDispute parties are claimant/validator; nest checks existing children, scope, and child.approvedAt < parent.approvedAt; claim validation expires late; claim comment has its window; credential renew is issuer-only and active-only; provenance has a writer list; oracle execute has a rollback/retry path.

The audit found residual divergences that this list does not close: credential revoke idempotence, expiry boundaries, the missing approver-qualification requirement, nest status admission and tie handling, caller-chosen claim K-Asset ids, oracle evidence gating, and the Identity.update mapping. The direction of each is in the proof audit and spec/proofs/rigor.yaml.

tools/check_arm_guards.py ties each mutating .rho arm to its manifest cell and checks that any declared transition/authority/guard_eq names exist. This is a coarse hand-encoding check, not a refinement.

What is not claimed

• No mechanized Rholang semantics and no refinement theorem. The arm-to-model map is hand-transcribed; proved-conformance remains reserved and unclaimed.
• The model cites the node’s single-use COMM / one-message cell / unforgeable names; it does not prove them.
• Run is a trace semantics over all runs, not an interleaving enumerator.
• The lock-order deadlock theorem remains a lock-order theorem, not scheduler liveness.
• The Python race suite is behavioural regression evidence only. It is not the proof and must not be cited as non-representability.

Reproduce

cd spec/lean && lake build
cd ../.. && .venv/bin/python tools/check_lean.py --audit
.venv/bin/python tools/check_race_matrix.py
.venv/bin/python tools/check_arm_guards.py
.venv/bin/python tools/check_flows.py

Concurrency and proofs

This page states the model’s concurrency argument and the rholo principles it mirrors.

Linear cells

Every entity is a cell with one message. The trace model (RGen.Linear.Cell) enforces:

• D1 — a peek followed by a put is not a committed update; a put with no take is refused.
• D2 — a take with no put is not well formed (it leaves the cell held).
• D3 — a nested call on a held cell is blocked.

peek_then_put_rejected, put_without_take_rejected, take_without_put_not_wf, and nested_call_rejected are the model’s names; D1–D3 are the stable aliases.

Framing and independence

run_frame says a successful trace leaves every cell outside its footprint unchanged, both its value and its occurrence count in the held list. run_agree says two runs whose states agree on the footprint and on a protected set produce results that agree on the same set; it is the induction used to compose traces.

disjoint_cells_commute states that traces with disjoint footprints commute on the store. The held list is deliberately byte-level (a take conses without deduplicating), so two disjoint traces can produce the same store with the held cells in a different order. disjoint_cells_commute_wf therefore states the exact result equality for two well-formed traces started from an empty held set: both end with the empty held set, and the stores agree everywhere.

disjoint_cells_commute_wf does not depend on the scheduler picking a winner. It is a property of the trace semantics: independent entities do not interact, and shared cells serialize.

Commits

The application model uses World/commit:

• commit_commute — commits on different cells commute.
• commit_same_cell — a second commit on the same cell composes with the first; the second sees the first’s post-state, so two operations cannot both decide from the same pre-state.
• commit_preserves_other — a commit on one cell leaves every other cell alone.

independent_commute and shared_serializes are the stable L1/L2 names.

Acquisition order

RGen.Concurrency assigns ranks:

MayAcquire has no KAsset → KAsset edge. Nesting takes child proofs in a phase that holds no business cell, so the model does not claim a recursive lock. mayAcquire_rank_strict shows every edge strictly decreases rank, mayAcquire_acyclic shows the acquisition relation has no cycle, and deadlock_free_of_rank is the general rank argument.

This is a lock-order theorem under the finite-cell/no-dynamic-locks hypothesis, not global scheduler liveness. Rholo’s Law 20 global deadlock-freedom was deleted as unprovable without a finiteness hypothesis; the same caution applies.

Non-representability theorem

RGen.core_races_not_representable (spec/lean/RGen/RaceFreedom.lean) quantifies over all Runs of the versioned-cell semantics: for every cell c, no two events on c share an expected generation. Accepted commits are a subset of events. The proof is runExec_no_same_expected, via per-cell projection and the AppliedExpecteds invariant.

RGen.core_arm_authority says every Arm decision factors through its consumed cell. This is functional dependence, not permission: who may invoke the arm is a guard concern. Proof payloads live in a separate one-shot cell; the arm’s proofCells metadata is not wired to that consumption, so cross-arm proof reuse is not proved (RGA-002). RGen.cross_cell_read_not_authority is the formal rule that a decision varying with a non-consumed cell does not factor through the consumed cell; any authority set must contain the other cell. A peek can be a linearization point at that other cell, but then it must be authority, not a peek.

The pair matrix spec/flows/races.yaml records 31 rows (19 exclusive, 11 ordered, 1 independent) and is checked by tools/check_race_matrix.py. It is not the complete cross-product over the six modeled cells; the proof audit records the gap (RGA-007). The model’s arm encoding is hand-written; tools/check_arm_guards.py ties each mutating .rho arm to its consumed cell. There is no mechanized Rholang refinement.

Linearization points

Proof issuance is the linearization point for every credential-gated arm:

• Credential.prove requires an active credential at the stated height and returns a one-shot proof; it does not change the credential.
• A revoke or dispute consumes the same cell, so a second operation cannot both read the pre-state and commit against it. prove_after_revoke and prove_after_dispute show the refusal from the post-state.
• The proof is a snapshot; a later revoke or dispute is non-retroactive. This is by design, not a gap.

Registries (factoryState, claimRegistryState, vpRegistryState, directoryState) serialize creation only. Validation, approval, decision, nesting, and provenance remain per-entity.

rholo principles mirrored

The model cites the node’s formal layer rather than re-proving it: single-use COMM (Reduce.comm), unforgeable names (reduce_freeVars_subset), matcher linearity, append-only registry reasoning, and closure-disjointness commutation (effect_commute_of_disjoint_closure). The application invariants are stated here; the node supplies the ingredients.

What is not claimed

• No mechanized Rholang semantics and no refinement theorem. The arm-to-model map is hand-transcribed; proved-conformance is reserved and unclaimed. The full claim and divergence ledger is in the proof audit.
• The theorem is over the model’s Run semantics, not an enumeration of the deployed scheduler’s interleavings. The behavioural race suite is regression evidence only.
• No claim that the deployed nest pre-pass is authoritative: the child proof is.
• No global fairness or starvation-freedom claim.

Adversarial review

Reviewed against the legacy-2026-11-04 tag: the 12-term prototype that passed 12/12 behavioural suites. Passing tests did not make it race-free or Pareto-minimal.

P0 — representable races or fund loss

P1 — stale reads and lifecycle corruption

• Mint-after-revoke / missed slash (legacy/deploy/21_kasset.rho:623-682, legacy/deploy/12_token.rho:242-428): removed from core; a receipt extension must make mint a one-shot transition against the K-Asset’s approval version.
• Permissionless WorkBook.close with an arbitrary status (legacy/deploy/20_work.rho:219-257): removed; the Claim cell’s own transitions set status.
• reject overwrites approved (legacy/deploy/21_kasset.rho:448-506): the core K-Asset consumes first and only rejects from validated/conditional.
• nest double-links a child (legacy/deploy/21_kasset.rho:508-621): the core parent consumes first, checks the fresh child list, and appends under the same consume.
• tally drops a concurrent vote (legacy/deploy/50_oracle.rho:386-455): panels removed; the core has one adjudicator.
• Duplicate attestation (legacy/deploy/30_risk.rho:179-242): risk removed; a risk extension must consume the assessment first and re-check the attester.

P2 — serialization and dead configuration

• One global state cell per book serialized independent entities. The core uses per-entity cells; the only serialization points are identity creation and credential issuance.
• 1/0 after a pending flag relied on whole-deploy rollback. The core uses refusal paths and re-posts; it does not use 1/0 for state.
• Stale panel overwrite: panels removed.
• Dead configs/rgen.json, orphan GenAdmin.params, dead IdentityBook.nonce, holds ignoring caseId, negative last share, undocumented 6666 bps threshold: removed with the legacy terms.
• “12/12 pass” was not a committed artifact. The core records its verification in docs/src/reference/verification.md.

What the legacy did well and the core keeps

• No cell was held across a cross-contract call in the legacy code; the core deliberately changes this to consume-first with a documented acyclic call graph.
• Every legacy arm re-posted exactly once; the core keeps this and adds a lint.
• Helpers were not published; the core’s Apply and KAsset library are private.
• Bundles were used correctly; the core keeps bundle+{*C} publication.

Audit charter

This page records the method and the boundary of the current-core audit. The machine-readable record is in spec/audit/findings.yaml, spec/hazop/worksheet.yaml, spec/proofs/rigor.yaml, and spec/improvements/rholang.yaml. The checker is tools/check_audit.py.

Status: Phase 1 complete. Phase 2 authorized by the owner; independent technical review has not been performed. The review record is approved by the owner with that limitation stated. Phase 2 items remain traceable to accepted findings; an external review is still required for any S1.

Scope

Audited: the seven deploy terms and all 65 deployed arms under contracts/src, the Lean model that claims to describe them, the flow/race manifests, and the current documentation claims.

Not audited: legacy/ (the tagged pre-Pareto prototype), crates/ (client tooling), the node’s Rholang implementation, and the economics of the extension primitives (KATs, payments, risk, panels, governance). The legacy adversarial review is not a current-core review and is labelled as such.

Baseline evidence

The audit is fixed at 527ed95. Phase 1 changes manifests, tools, and documentation only. The --phase1 checker mode rejects a diff under contracts/ or spec/lean/.

The priority counts follow the severity/likelihood rubric below. They are not a claim that twelve critical exploits exist; they mean twelve findings cross the rubric’s P0 line and need a review decision before Phase 2.

Method

1. Normalize the claim. Extract a public claim from a README, docs page, contract header, or manifest and write it as “for all … if … then …”.
2. Compare with the theorem. Read the actual Lean statement, its quantifiers, its premises, and its dependencies. Use the verdict vocabulary below.
3. Compare with the contract. Read the deployed guard and state write. Record whether the model is permissive, stricter, effect-omitting, shape-different, or mixed.
4. Apply guide words. For each HAZOP node and parameter, ask what happens under No/Not, More, Less, As well as, Part of, Reverse, Other than, Late, Early, Before, After, Duplicate/Replay, Stale, Substitute/confused-deputy, and Partial commit.
5. Disposition. A holding safeguard becomes a negative row with evidence. A partial or missing safeguard becomes a finding and must name a Lean item, a Rholang item, or an explicit risk acceptance.

Claim verdicts

“Proved” always means “proved about the Lean model”. It never means “proved about the deployed Rholang” in this repository.

Severity, likelihood, and risk

Likelihood A is an ordinary reachable call; B is crafted input or interleaving; C is a privileged or unlikely configuration; D is theoretical. Risk is severity × likelihood with S1=4 … S4=1 and A=4 … D=1. P0 when S1 or risk ≥ 9; P1 when 4–8; P2 when ≤ 3. Scores are judgements, not probabilities.

Independence and review

The Phase 1 record is not self-approving. The review must name its reviewers, re-derive at least 20% of the findings (including every S1 and every finding that changes a guard or a public claim), and mark each finding accepted, rejected, or accept-risk. An auditor must not approve code or proofs they authored. With one maintainer, the record must state the role separation and the independence limitation; external review is recommended for any S1.

What is not claimed

• No mechanized Rholang semantics and no refinement theorem.
• No proof of name/capability unforgeability, chain-height authenticity, JSON schema validity, phlo exhaustion, scheduler fairness, or liveness.
• No penetration test. Dynamic evidence is limited to the documented harness suites.
• A negative HAZOP row means the considered deviation had a holding safeguard; it does not mean the node is hazard-free.
• Phase 1 is read-only against contracts/ and spec/lean/; it does not fix what it finds.

HAZOP of the core primitives

This is the current-core HAZOP. It treats the seven deploy terms as ten nodes and applies fifteen guide words to each node’s parameters. The worksheet is spec/hazop/worksheet.yaml; the method is in the audit charter.

Design intent

Coverage

The worksheet has 150 coverage cells (10 nodes × 15 guide words): 145 are covered by a full row and five are marked not applicable with a reason. There are 146 rows. Seventy-seven rows are negative results: the considered deviation has a holding safeguard. Sixty-nine rows have a partial or no safeguard and therefore name a Lean item (LR-###), a Rholang item (RR-###), or accept-risk.

A negative row is evidence that a specific deviation was considered, not a claim that the node is safe. The most useful negative results are:

Deviations that feed the backlog

The rows below are representative, not the full register. Each has a finding and an action in the worksheet; the action is either a Lean item in the rigor roadmap or a Rholang item in the improvement plan.

How to read a row

A row is a deviation from design intent, not a bug report by itself. safeguard_status: holds means the arm or platform check was found and is cited. partial means the safeguard narrows but does not close the deviation. none means no safeguard was found for the considered case. The action field is the disposition: a Lean item, a Rholang item, accept-risk, or none for a closing safeguard.

Limits

The HAZOP is qualitative. It does not cover the node’s Rholang semantics, phlo accounting, or the extension primitives. It is not exhaustive over all parameter values; it covers the fifteen guide words per node and the parameters listed above. A clean coverage cell is a considered not-applicable, not proof of safety.

Proof audit

This page audits what the Lean theorems actually state and where the model diverges from the deployed Rholang. The machine-readable record is spec/proofs/rigor.yaml and spec/audit/findings.yaml.

Claim versus theorem

All 39 Pareto theorems have a claim entry. The verdict vocabulary is in the audit charter. The table below is representative; the full ledger carries the exact quantifiers, premises, and missing coverage.

The headline theorem is true and useful. It is not a general race-freedom result. It does not cover cross-cell races, proof reuse across arms, deployed guard equivalence, scheduler/interleaving semantics, or Rholang capability semantics. The public pages now state that boundary; the theorem name is retained for compatibility.

core_arm_authority means functional dependence, not permission. Arm.decision reads only w.cell a.cell. Who may invoke the arm, and which proof it must consume, are guard and operational concerns. The arm’s proofCells field is not read by decision or event; see RGA-002.

Model-versus-code divergences

Sixteen divergences are recorded with a direction. model-permissive means the model admits more than the contract, so a model invariant may still be conservative but the arm’s real guard is unproved. model-stricter and effect-omitting mean a model proof may not cover the deployed arm.

Assumption ledger

The model assumes, but does not prove: Run is a finite trace and not a scheduler; Event.apply is deterministic and pure; names and proof capabilities are unforgeable; heights are authentic; arm steps are hand-transcribed; proofs are data plus a one-shot cell; phlo, depth, serialization size, and JSON shape are deployment concerns; model state records only the fields the invariants need. These assumptions are mirrored in the formal model and the race-freedom proof.

Gate audit

The devnet and behavioural suites run nightly or manually, not on every pull request (RGA-011). They are regression evidence, not the proof.

Findings that need a proof decision

The twelve P0-scored findings are not all proof defects. They are the items that crossed the rubric’s P0 line at the audit baseline and needed an explicit review decision. The proof-side items were:

• RGA-002: proof-cell metadata is inert; no cross-arm proof-reuse theorem.
• RGA-003: versioned independence is missing; the L1 alias is a plain-Store theorem.
• RGA-004: no guard equivalence; several model guards differ from the deployed guards.
• RGA-005: proved-conformance is zero; vectors are not asserted end-to-end.
• RGA-013: Identity.update is mapped to a different operation.

The remaining P0 items are contract-state and atomicity findings: RGA-020 (verdict mapping), RGA-022 (provenance creation), RGA-023 (oracle open), RGA-024 (oracle execute retry), RGA-031 (identity create), RGA-032 (claim mint), and RGA-033 (nest proof consumption). The complete ranked list is in the HAZOP and the improvement plan.

Phase 2 progress

The owner authorized Phase 2 with the independence limitation recorded. Since the audit:

• ProfileState.updateProfile and an IdentityPatch model replace the wrong Identity.update mapping, and Identity.update, IdentityFactory.create, and ValueProposition.comment have Arm values (LR-00, RGA-013, RGA-008).
• 21 core arms have a guard_eq theorem and a manifest entry, including identity, credential, claim, K-Asset approval/rejection, oracle, and provenance write guards (LR-01).
• VWorld.set_commute, VWorld.commit_commute, Event.apply_commute_distinct, and core_independent_arms_commute connect the versioned layer to independence (LR-02, LR-04).
• check_lean.py --audit-coverage requires every Pareto #check in Audit.lean; 64 Pareto checks and 173 axiom checks pass (LR-07).
• The model-only finish/execute race row is removed; the matrix is 31 rows (LR-05 partial).
• Claim and K-Asset verdict mappings now agree for valid, partial, invalid, and unknown verdicts; claim deadline presence and comment-window ordering are checked at creation (RR-04, RR-07 partial).

Still open: proofCells trace consumption (LR-03), runExec commute, 14 proved-model arms without guard equivalence, conformance vectors (LR-06), and the remaining model/code divergences (LR-08).

What would change the verdict

The proof-side verdicts become proved for the model only when the corresponding LR item closes. Even then the result is a model result, not a refinement. The rigor roadmap states the ladder and the remaining unprovable boundary.

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-model arms.

Work items

Phase 2 progress

The guard count is 21 of 35 proved-model arms. The rest are recorded as unverified or divergence in spec/audit/findings.yaml; no arm is silently treated as aligned.

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.

Rholang improvement plan

This is the ranked Rholang backlog from the audit and HAZOP. The machine-readable record is spec/improvements/rholang.yaml. Every item cites a finding and at least one HAZOP row; Phase 2 may not start until the review accepts the finding.

Staged policy

Phase 1 changes no contract. Phase 2 implements accepted items with the listed tests and a compatibility note. A breaking change requires a migration note and an updated suite. A P0 is not “fix immediately”; it is “requires an explicit review decision before Phase 2”. The review may accept, reject, or accept the risk.

Ranked items

The HAZOP rows for each item are in the manifest. Representative links:

• RR-01: HZ-ORACLE-004, HZ-ORACLE-005.
• RR-02: HZ-PROV-002, HZ-PROV-003, HZ-PROV-012.
• RR-03: HZ-VP-005, HZ-VP-013.
• RR-04: HZ-CLAIM-004, HZ-CLAIM-005, HZ-CLAIM-007.
• RR-05: HZ-DEPLOY-002, HZ-KASSET-016.
• RR-07: HZ-CLAIM-016, HZ-VP-016, HZ-ORACLE-016.
• RR-08: HZ-ORACLE-013, HZ-ORACLE-015.
• RR-11: HZ-ID-011, HZ-CRED-015, HZ-CLAIM-015, HZ-KASSET-015.

Phase 2 progress

• RR-04 is fixed: claimStatus and kassetStatus both map valid to validated, partial to conditional/validated, and invalid or unknown to rejected. An unknown verdict no longer produces a validated claim beside a rejected K-Asset. Pre-write rejection remains a follow-up.
• RR-01 is partial: OracleFactory.open now authenticates the opener and requires it to match caseReq.openedBy. Parties and subjectRef remain caller-supplied; registry binding is open.
• RR-02 is partial: ProvenanceFactory.create now authenticates the creator and rejects an empty writer list. assetRef is still a free string; asset-registry binding is an extension.
• RR-03 is fixed: ValueProposition.proveValidated reads nowHeight and rejects a supplied atHeight that differs from chain height.
• RR-05 is fixed: KAsset.nest caps a batch at 32 children and the parent list at 64, rejecting larger batches before proof consumption.
• RR-07 is partial: claim creation now requires a deadline and rejects a comment window after the deadline. Future-ness relative to chain height is still not checked for claim or oracle creation.
• The other items remain proposed. The devnet suites were not re-run after the contract changes in this environment because the isolated node failed to start (exit 137); parse-check passes and the changes are static. Re-run make install unit-all before promotion.

Why these orderings

• State integrity first. RR-04 and RR-11 prevent a claim and its K-Asset, or a parent and its child proofs, from disagreeing. They are the highest-value contract changes.
• Authority next. RR-01 and RR-02 close unauthenticated record creation. Neither is a direct authority bypass today, because the private Apply and the advisory nature of provenance limit the impact; both are record-integrity hazards.
• Time and resources after that. RR-03, RR-05, and RR-07 remove caller-controlled height, unbounded nest work, and impossible schedules. They are availability and API hazards.
• Documentation and policy last. RR-06, RR-09, and RR-10 make advisory and design choices explicit. They may close with no code change.

What is not in this plan

No KATs, payments, risk scoring, panels, governance, handles, or metrics primitives. They remain extensions. No change to the five paper-derived primitives’ core purpose. No new token or minting arm. No attempt to make the contracts a refined implementation of the Lean model; that requires a Rholang semantics, which this repository does not have.

Test plan

Each item names the harness suite that must gain a negative case before the fix and a passing case after it:

The devnet suites are nightly/manual (RGA-011). A Phase 2 change that cannot be covered statically adds its negative test to the nightly job and documents that it did not run on the pull request.

Open decisions for the review

1. Keep proved-conformance and define it as an evidence bundle, or rename it model-vector-conformance? Recommendation: keep the name, publish the definition.
2. Oracle execution: keep a permissionless crank with an idempotent receipt, or require subject authorization? Recommendation: keep the crank, make it outcome-blind and receipt-backed.
3. Identity participation: enforce an Identity record, or document permissionless participation as intentional? Recommendation: document it, test it, and revisit if Sybil resistance is a goal.
4. Provenance creation: require an asset registry binding, or state that provenance is advisory? Recommendation: require a creator capability and non-empty writers now; treat registry binding as an extension.

Rholang model used by the core

The papers define the engineering domain, not Rholang semantics. The concurrency argument rests on the pinned rholo runtime:

• Linear channels. A name with one message is a cell. for (@s <- state) removes the message; a second consumer blocks until the first re-posts. This is the single-writer linear cell used for every entity. Source: RNodeRust/rholang/src/reduce.rs, the interpreter’s receive/send rules, and RNodeRust/docs/src/formal/.
• Peek <<-. A read that leaves the message in place; used by read-only arms (get, comments, verify, authorize, covers).
• Bundle bundle+{*Contract}. The published capability; only the named contract is in the bundle. Private helpers (Apply, KAsset in the Claim term) are not in the bundle.
• Deploy atomicity. A deploy’s state changes are rolled back on failure; the core avoids relying on 1/0 for a pending flag. Refusals re-post the consumed state and reply (false, reason).
• No names in state. State maps hold data (String, Int, Bool, List, Map, Nil). Capabilities live in process closures. This avoids serialization and equality ambiguity for names.
• Registry URIs. rho:registry:insertArbitrary returns a URI value. The credential registry canonicalizes it with uri.toString() so a caller’s string URI matches the stored key.

The core does not use rho:rchain:makeMint, ERTP, r-cash, or any extension system process. The native rho:block:data and rho:crypto:blake2b256Hash are the only system processes used for time and hashing.

Core arm reference

Replies are (true, payload…) or (false, reason). Mutating arms consume the entity cell first and re-post exactly once. Proofs are one-shot capabilities returned as a registry URI; the caller resolves the URI, calls Proof("take"), and checks the payload.

Each section links the primitive page with the paper anchors and the Lean theorem names.

Root and identity

• GenRoot("resolve"|"get"|"keys"|"register", ...) — installer-gated directory.
• IdentityFactory("create", dId, profile, ret) -> (true, identityUri)
• IdentityDirectory("lookup"|"count", ...)
• Identity("get"|"update", ...)

Paper: @robles2016nspe p.40 (records/identity); @zhong2019bridge p.4 (participants). Lean: Directory.create_unique, update_owner_requires_owner. See Identity.

Credentials

• Issuer("get"|"authorize"|"covers", ...) — immutable genesis issuer; no revoke arm.
• CredentialFactory("issue"|"verify"|"count", ...) -> (true, credentialUri)
• Credential("get"|"check"|"prove"|"revoke"|"renew"|"attest", ...)
• Proof("take", ret) -> (true, proofData) once, then (false, "used")

Paper: @mathews2017bim p.7, @zhong2019bridge p.6, @robles2016nspe p.25, @robles2016naic p.9. Lean: C1_prove_requires_active, C2_revoke_blocks_prove, C3_issuer_immutable, prove_snapshot, proof_take_once_versioned. See Issuer, credential, proof.

Claims and K-Assets

• ClaimFactory("create"|"verify", ...)
• Claim("get"|"comments"|"comment"|"withdraw"|"expire"|"validate", ...)
• K-Asset arms (created by the Claim): get, approve, reject, proveApproved, nest, openDispute, children, revocation, and the private applyDecision.

Paper: @robles2020innovation p.4-5, @zhong2019bridge p.4-6. Lean: ClaimState.validate_once, claim_validation_exactly_one_kasset, K1_approve_credential, K2_approve_status, K3_nest_acyclic. See Claim, Validation, K-Asset.

Value proposition

• ValuePropositionFactory("propose"|"verify", ...)
• ValueProposition("get"|"comments"|"comment"|"withdraw"|"validate"|"proveValidated"|"openDispute"|"revocation", ...)
• Private applyDecision.

Paper: @mathews2017bim p.7,p.9 (paper-adjacent; no state machine defined). Lean: V1_validate_once, V2_dispute_blocks_prove, proveValidated_requires_validated. See Value proposition.

Oracle

• OracleFactory("open", subjectRef, caseReq, subjectApply, ret) -> (true, {id, uri})
• OracleCase("get"|"evidence"|"decide"|"execute"|"expire"|"close", ...)

Paper: @robles2016nspe p.25, @robles2016naic p.9, @mathews2017bim p.8. Lean: O1_execute_bound_once, O2_close_finished, decide_once, execute_once. See Oracle.

Provenance

• ProvenanceFactory("create", assetRef, writers, ret) -> (true, {id, uri})
• Provenance("get"|"anchors"|"anchor"|"comment"|"verify", ...)

Paper: @robles2016nspe p.29, @zhong2019bridge p.3,p.6. Lean: P1_anchors_append_only, anchor_unique, verify_monotone. See Provenance.

Creation registries

CredentialFactory, ClaimFactory, ValuePropositionFactory, and IdentityFactory write append-only creation registries. See Creation registries.

Citations

Citation keys live in docs/papers/manifest.json. Convention: p.N is PDF page N (1-based), not the printed page.

The core contract headers use the form:

// Why: ...
// Paper: @key p.N; @key2 p.N
// r-gen decision: ...

@caase2018agenda is included but uncited; do not cite it. A term with no paper basis uses // Paper: none (engineering infrastructure).

tools/check_citations.py verifies:

1. Every @key in a // Paper: header exists in the manifest.
2. Every p.N is within the paper’s page count.
3. Every cited key has docs/papers/extract/<key>.md with a ## p.N heading.
4. Every core deploy term has // Why: and // Paper: lines.
5. @caase2018agenda is never cited.

Paper map

This page has moved to the Pareto ledger, which states for every primitive:

• the paper claim and page citation;
• the necessity argument;
• whether it is paper-derived, paper-adjacent, a user decision, or engineering infrastructure;
• what was removed or moved to an extension.

The papers themselves are indexed at docs/papers/README.md; citation keys and the checker rules are in citations.md.

Papers

The paper archive lives in docs/papers/. It contains all seven PDFs, short page-cited extracts, and a manifest with authors, venues and SHA-256. The papers are already public on Arweave and the authors’ websites.

NOTICE. The papers are third-party copyrighted works. They are not covered by r-gen’s AGPL license; they are included as cited reference material. See docs/papers/manifest.json.

Citation keys

Convention: p.N is PDF page N (1-based). The extracts are short quotations, not full text.

@robles2020innovation — The Innovation Bank (IMECE2020-23015)

p.3 — risk = S × P × E

“Risk = f(S, P, E). Specifically, Risk = S × P × E where specific values for SPE are ranked on an integer scale, with 1 representing slight … to 100.”

Why it matters. The risk model is paper-derived, but it is an application extension in r-gen, not part of the core claim/validation primitive.

p.4 — K-Asset pairing and receipt

“Each pairing forms a single node with two branches constituting a knowledge asset – ‘K-asset’ – which is memorialized by the creation of an electronic token awarded to each participant in a pair.”

Why it matters. This is the definition of the K-Asset and the reason the Claim cell creates a K-Asset on validation. The receipt is tokenisation; the core does not mint.

p.5 — claim is quantity, validation is quality

“The claim serves as the quantity (definition) and the validation serves as the quality (characteristics).”

Why it matters. The Claim cell carries quantity, statementHash, and definitionHash; the Validation carries quality and the evidence hash. It also shows the paper’s mint timing: the receipt is produced when the pair forms, at validation. r-gen’s core does not mint; the receipt extension must choose validation (this paper) or approval (the Bridge paper).

p.6-7 — WIKiD

“6. THE WIKiD TOOLS ALGORITHM”

Why it matters. WIKiD is a valuation/measurement model, not a claim/validation state machine. It is deferred as a metric extension and is not a core primitive.

@zhong2019bridge — A New Perspective of Accelerated Bridge Construction

p.3 — provenance and ownership

“their provenance and ownership”

Why it matters. The provenance cell anchors document hashes to the asset; the asset is the keeper of its own information.

p.4 — the handshake and Figure 1

“‘Claim’ and ‘Validation’ represent a key mechanism i.e. the ‘handshake’.”

“‘Approval’ represents an acceptable completion.”

Why it matters. The core is claim → validation → approval. The Claim cell carries the work element and selection criteria from Figure 1; the K-Asset carries the validation and approval.

p.5 — clock and stakeholder comments

“pre-defined and agreed upon ‘clock’ embedded in the blockchain and all participants can see the specific actions to be taken and their status”

Why it matters. The core carries deadlineHeight and commentUntilHeight on the Claim cell, and records comment hashes on the claim, not in a detached global book.

p.6 — nesting and risk transfer

“‘Blocks’ on a blockchain are nested in this manner as well.”

“Tokens issuance marks points where risk is transferred from one party to another.”

Why it matters. K-Asset nesting is parent-owned and ordered; the core records approval and liability data without minting. A receipt extension may read the approval event if it chooses the Bridge mint timing.

@mathews2017bim — BIM+Blockchain: A Solution to the Trust Problem in Collaboration?

p.7 — permissioned by qualifications; value proposition

“A ‘Permissioned by Qualifications Blockchain’, facilitated by an Oracle…”

“This is in essence ‘the new value proposition’.”

Why it matters. Qualification gates are primary: a validator must hold a credential that the genesis issuer recognizes. The “value proposition” phrase is the paper-adjacent anchor for the user-requested ValueProposition primitive; the papers do not define its state machine.

p.8 — oracle adjudication

“An Oracle contract is an adjudicated contract with the added requirement the adjudicator … is deemed the most appropriate person to be performing the adjudication.”

Why it matters. The core Oracle has one adjudicator proved by a credential, not a weighted voting panel.

p.9 — reputation and intrinsic value

“Reputation now is a currency.”

“develop a ‘new value proposition’ to extract reward … also the intrinsic intangible value”

Why it matters. Reputation is an extension concern; the core records validation and approval facts. The value proposition is a separate cell in the user’s Pareto core.

@robles2016naic — Insurance: The Highest and Best Use Case for Blockchain Technology

p.4 — the three insurability questions

“1. Can we identify the risk exposure? 2. What is the [mathematical] probability that such risk exposure will manifest? 3. If failure occurs, what are the consequences [cost] of that failure?”

Why it matters. The three questions are the source of the insurability gate. r-gen keeps risk as an extension so it does not conflate this consequence question with the IMECE exposure factor.

p.9 — the oracle as the most appropriate person

“An Oracle contract is an adjudicated contract with the added requirement the adjudicator … is deemed the most appropriate person to be performing the adjudication.”

Why it matters. The core Oracle names a single adjudicator and checks a credential at decision time.

@robles2016nspe — Blockchain Technology: Implications and Opportunities For Professional Engineers

p.14 — insurability

“Can we identify the risk exposure? What is the probability that such risk exposure will manifest? If failure occurs, what are the consequences of that failure?”

Why it matters. The insurability questions are an extension gate in r-gen, not a core claim/validation state.

p.25 — the most appropriate adjudicator

“An Oracle contract is an adjudicated contract with the added requirement the adjudicator is deemed the most appropriate person to be performing the adjudication.”

Why it matters. The core Oracle implements a singular adjudicator; panels are an extension.

p.29 — the asset keeps its information

“The asset becomes the keeper of its own information.”

Why it matters. Provenance is a per-asset cell that anchors the asset’s documents and comments, not a global registry.

p.40 — records and identity

“Records” (identity/credential context)

Why it matters. The core uses the REV address as identity and keeps per-address profiles; handles are an extension.

@robles2017stewardship — The Revolutionary Blockchain

p.3 — reputation and the invisible value of engineering

“award Quant to author and verifier in proportion to the reputation of each. Reputation is determined by total number of lifetime Quant awarded.”

“The fundamental problem is that the value of engineering is invisible.”

Why it matters. r-gen’s core records validation and approval; reputation and Quant-style tokenisation are extension concerns. The invisibility thesis is the reason the claim and validation are first-class records.

Verification record

Date: 2026-11-04 Node: rholo e2d073dcd02f1e560ccb84749937138a1e184b0b Devnet: isolated rgen-bootstrap on 40403/40405/40402 (8 GB), existing networks untouched Core: 7 deploy terms, 16 catalogue components, 10 state cells

Passed

• tools/build_contracts.py --check: 7 terms, no drift.
• tools/parse_check.sh on all rendered core terms: 7/7 OK.
• tools/check_arch.py: 16 components, 10 state cells, acyclic.
• tools/check_captures.py, check_placeholders.py, check_money.py: pass.
• harness/unit_core.py: pass — identity → credential → value proposition → claim → validation → K-Asset → approval → dispute → oracle → provenance.
• harness/concurrency_core.py: pass — one of two validations wins; one of two approvals wins; exactly one oracle apply; cross-subject isolation; two comments both stored; eight independent claims validate in one deploy; a revoked credential refuses.

Lean model (2026-11-04)

• cd spec/lean && lake build: 36 Lean files build on Lean v4.12.0, no Mathlib.
• tools/check_lean.py: 37 files, no sorry, admit, native_decide, or declared axioms.
• tools/check_lean.py --audit: the 180 theorems listed in RGen/Audit.lean, only propext and Quot.sound; no Classical.choice use in the audited set. The list is hand-maintained (RGA-006).
• tools/check_core_vectors.py: 21 emitted rows match spec/vectors/core.tsv.
• tools/check_flows.py: 65 deployed arms mapped — 35 proved-model, 0 proved-conformance, 30 owed (read-only arms, creation registries, and extensions). The former phantom Issuer.revoke entry is removed. Identity.update, IdentityFactory.create, and ValueProposition.comment now have Arm values.
• tools/check_race_matrix.py: 31 pairs (19 exclusive, 11 ordered, 1 independent).
• tools/check_arm_guards.py: the mutating arms are tied to a consumed cell.
• tools/check_audit.py --strict: 65 arms dispositioned, 10 HAZOP nodes, 150 coverage cells, 146 rows, 39 claims, 27 findings, 11 Rholang items. Review status is approved by the owner; independent technical review has not been performed. The reviewed pages start at the audit charter; the findings are in spec/audit/findings.yaml.

The model proves run_frame, run_agree, disjoint_cells_commute, disjoint_cells_commute_wf, the three commit lemmas, D1–D3, the versioned no-same- generation theorem core_races_not_representable, the arm authority theorem core_arm_authority, and the 31-pair race matrix in spec/flows/races.yaml. The behavioural race suite is regression evidence only; it is not the proof. It is a model proof: no mechanized Rholang semantics and no refinement theorem.

Baseline

The pre-Pareto 12-term prototype is on tag legacy-2026-11-04; its 12/12 suite result is the baseline, not the target. The core does not install KAT, payments, risk, panels, admin, handles, or metrics; those are extensions.

Reproduce

make venv
make lean-check
make build-check parse-check
make check-core-boundary check-concurrency check-citations check-flows check-audit
make install
make unit-core
make unit-race

Honest limit: the core has two behavioural suites (vertical slice and race suite). The extension suites (receipt, payments, risk, panels) are not implemented in this tree.

Status and limits

Devnet-only, no real value. Phase 1 audit recorded; Phase 2 in progress; independent review pending.

Verified on 2026-11-04

• 7 core deploy terms, 16 catalogue components, 10 state cells, acyclic.
• All 7 rendered terms parse with the pinned rholo parser.
• harness/unit_core.py: pass — identity → credential → value proposition → claim → validation → K-Asset → approval → dispute → oracle → provenance.
• Ten behavioural suites pass: identity, credentials, claim, K-asset, value, oracle, provenance, integration, vertical slice, and behavioural race regression.
• Lean proof gates: 37 files, no sorry/axiom; the 180 theorems listed in Audit.lean are axiom-clean (propext, Quot.sound only); core_races_not_representable; 31-pair race matrix; no proved-conformance claim. The list is hand-maintained (RGA-006).
• Static gates: build, parse, arch, captures, placeholders, money, core boundary, concurrency, citations, flows, race matrix, arm guards, audit.
• Phase 1 audit: 65 deployed arms dispositioned; 10 HAZOP nodes, 150 coverage cells, 146 rows; 27 findings (12 P0, 13 P1, 2 P2; no S1); 39 Pareto claim entries; 11 Rholang items and 9 Lean items. The record is in spec/audit, spec/hazop, spec/proofs, and spec/improvements.

Core boundaries

The core installs only: Root, Identity, Issuer/Credential, Claim/K-Asset, ValueProposition, Oracle, Provenance. It does not install KAT, payments, risk scoring, panels, admin, handles, metrics, or a web client.

Owed

• Extension suites: receipt/KAT, payments/r-cash, risk/SPE, panels, governance, metrics.
• A mechanized Rholang refinement; the current proof is model-level with a hand-encoded arm map.

Honest limits

• “Maximal concurrency” means no shared mutable cell across independent entities and one writer per entity. It is not an absolute optimality theorem.
• Identity creation and credential issuance are deliberate serialization points; neither is on the claim/validation hot path.
• Oracle selection is deterministic and named by the parties, not a random beacon.
• Nesting uses a strict (approvedAt, id) order; a later-approved child cannot be nested into an older parent.
• Race freedom is proved for the Lean model (core_races_not_representable), not for a mechanized Rholang semantics. The behavioural suites are regression evidence. The theorem is per-cell and per-valid-trace; see the proof audit.
• The Phase 1 audit found no S1, but it did find material P0-scored state-integrity and proof-coverage gaps. They are not fixed yet: Phase 2 requires an approved review. See the HAZOP and the Rholang plan.
• The papers are third-party copyrighted works and are not AGPL; see docs/papers/README.md.