This document covers the B1–B3 work area of the fixed completion contract. A1–A4 are merged in #1237. B1 is merged in #1238. B2 is merged in #1239. B3 is complete at the signed-bridge boundary in this change. C1–C3 are implemented in the final theorem work, including the approved clock, chain-context and richer-receipt corrections.
Both Gatekeepers own historical controller selection in event authorization (controllerForEvent in TypeScript, controller_for_event in Rust). The low-level proof verifier receives the resulting document. Import, confirmation replacement, branch reorganization and verified replay share this path. Mediators supply chain receipts; they do not choose controller versions.
Selection first tries the receipt’s authoritative chain context when registration metadata is present. Same-registry updates are bounded strictly by ordinal; other-registry updates are bounded inclusively by event time. Genesis is admitted independently of these cutoffs. Every successor must remain in the confirmed prefix, and traversal stops at the first excluded event; it never sorts or filters the history by proof time.
The candidate chain-bounded document supplies the registry used by isAnchored. Anchoring scans the whole confirmed prefix, not just that time-bounded prefix. A matching chain receipt without registration metadata defeats anchoring; a wrong-registry suffix cannot establish it. Local/Hyperswarm/pin registries cannot establish chain anchoring. If that test fails, selection is recomputed using the dependent operation’s proof time. Hyperswarm/pin controller times have already been normalized at import/recovery.
Agent genesis and component tables come from A’s validated signed graph. Missing controller evidence produces no document. Deletion produces an explicit deleted component state, which asset authorization must reject. The current implementations admit controller genesis even when the requested cutoff predates genesis; the model preserves that behavior.
Runtime recovery keeps rejected/deferred candidates in the journal and reconstructs agent histories before assets. Self-controlled agents have no external authority dependency; assets have only agent owners, including prospective owners after transfers. B2 must exploit that dependency ordering rather than assume asset verdicts are fixed initially.
ControllerSelection.lean implements the prefix, component execution, anchoring scan and proof-time fallback. controller_selection_same_sources composes these functions with A3’s source-derived confirmed receipt-view equality. Its premises are the existing signed graph, source/clock projection contracts, ancestry bounds and equal source evidence; equal final controller documents and equal signature verdicts are not premises.
The receipt abstraction inherits A3’s source contract: chain clocks/positions are authoritative shared chain facts, while unanchored clocks are derived from operation content. A ControllerRequest.chain denotes such a chain receipt, not arbitrary peer metadata claiming chain authority. Direct and unanchored requests use proof time. The model is a protocol proof, not general verification of JSON decoding or malicious admin-supplied source facts.
ControllerSelectionExamples.lean contains kernel-checked synthetic examples for strict same-chain ordinal and inclusive cross-chain time boundaries, nonmonotone times, confirmation gaps, missing metadata, migrations, deletion and missing evidence. These are rule examples, not the signed runtime bridge required by B3.
AssetAuthorization.lean derives authority for each retained receipt using B1. Asset structure is reconstructed from signed predecessor links, whole-document replacement and deletion; no signature verdict is hidden in that structural evaluation. The predecessor document supplies the signing owner. A transfer separately requires the proposed owner to resolve to an active agent at the same cutoff; it does not require that owner to co-sign. Creation checks the signer/controller identity and the local-controller/non-local-asset restriction. Proposed documents and registration shape are checked even on deletion, before deletion discards their payloads.
AssetControllerInputs.table filters specifications by an explicit immutable genesis-kind projection before replay or owner lookup; nonagent DIDs have no entry. The integrated endpoint requires this decoded kind table and returns the domain exclusion theorem. DocumentGraph implements self-controlled predecessor-key authorization and has no external-controller edge. Missing agents and asset DIDs provide no entry, so an asset cannot recursively authorize another asset. ControllerHistories is the converged confirmed receipt view proved by A3; it is not a supplied table of dependent-operation verdicts. asset_authorization_from_histories derives equality of every contextual asset verdict from equality of those agent histories. C1 will compose the finite family of agent and asset executions; B2 establishes the asset phase once the independent agent phase has completed.
The asset tables encode operation shape/identity/registration validity, canonical predecessor references, complete operation proof times, document proposals, component patches, normalized method names, signer identity and operation/key signature validity. Shape checks are context-free parser primitives; controller availability, controller version and signature-key selection are derived here. Opaque payload indices name shared whole-component values. Registry-name projections are explicit functions of those full registration values, so changing metadata without changing the registry neither loses payload nor changes chain priority. An AssetDocument contains the owner field and the remaining document fields together; the same document table supplies ownership and the returned document. The B3 bridge must derive both from the signed document and check the decoding.
AssetComponents.lean proves structural component execution agrees with document ancestry and is independent of sufficient evaluation fuel. asset_predecessor_components connects the actual executed prefix to the ancestry state used for registry/owner selection. Deletion clears document/data and retains registration; an operation after deletion cannot execute, but a preferred sibling at an earlier live predecessor may still replace the deleted branch.
AssetReplay.lean reevaluates every retained source in its own receipt context before normalizing priority. This matters because asset authorization can differ between proof-time and chain-position cutoffs: a rejected chain receipt must not manufacture an accepted gossip hint. Source identity carries the operation, registry and authoritative anchor class; arbitrary first-observation bookkeeping does not enter the authorization predicate. asset_selected_authorized proves every selected representation came from an authorized retained receipt, and asset_reconsidered proves a previously rejected/deferred source contributes when new controller history makes it valid.
asset_reconciliation_converges proves both nodes actually stop on full-record equality, at the same operation history and decoded document/data/registration/deactivation result, from equal source sets and converged controller histories. It starts from an empty projection, so previously published state and prior rejection verdicts are not premises. asset_source_execution additionally proves a retained creation authorized by B1 yields a nonempty history and successful complete component execution; equality of failed folds does not suffice.
AssetPriority.lean derives predecessor-registry agreement for siblings and checks anchored ordinal/CID priority under AssetCidRanks. Priority ranks are registry-local ordinal/CID classes; equivalent classes share a rank. Provisional representations remain canonical-CID ranks after all chain ranks. This is the same explicit source ordering/identity contract as A, not a proof of canonicalization or mediator correctness. Per-receipt chain facts and registry classification must agree with those classes; B3 will check the translation using signed source records.
AssetExamples.lean supplies kernel-checked synthetic examples for transfers, missing/nonagent owners, old/new keys, deletion, the local creation rule, reverse predecessor delivery, and revocation of all old-key evidence. These do not discharge B3. All new general theorems are included in the transitive axiom allowlist audit.
IntegratedAssetConvergence.lean now supplies the source-level endpoint integrated_asset_convergence. It reconstructs every controller view from shared agent source evidence via A3, proves those controller reconstructions terminate, then passes the derived views through B1 into asset authorization and replay. Equal controller histories are an intermediate lemma, not an endpoint premise. The endpoint also requires AssetCidRanks and proves the same-registry ordinal/CID sibling-order interpretation alongside stopping and result equality. This closes the two integration gaps identified in review; global finite-family execution remains C1.
AssetGraph.rootNotDeleted and AssetGraph.rootNoProposal together encode that the root is a creation. The B3 bridge must identify it from the actual create operation and instantiate both invariants, rather than accepting an arbitrary root/action combination. Wrong-registry sources remain eligible provisional evidence when their contextual authorization succeeds; only matching predecessor-registry chain anchors receive chain priority. Rejecting all registry mismatches would contradict ordinary gossip/import behavior.
The integrated endpoint also returns AssetSourceGuarantees for both reconstructed worlds: every newly authorized retained receipt contributes to replay, every selected record has an authorized retained source, and an authorized retained creation implies nonempty history and successful full-component execution. These are instantiated over the reconstructed controllers, not supplied controller histories. Parent bounds and root bounds are explicit graph premises.
Creation alone requires the proof method’s DID prefix to equal the controller DID (g.signer). Updates/deletions use normalized named-method lookup in the selected predecessor owner’s document, exactly as TypeScript verifyUpdateOperation/operationKey and Rust operation verification do; they do not impose a separate prefix-equality rule. Method identity and public-key identity remain distinct, and the signature oracle cannot bypass named-method lookup.
tests/convergence/generate-asset-vectors.mjs creates public synthetic signatures in both proof formats. Ten vectors cover Hyperswarm, pin, same-chain ordinal selection, cross-chain time selection, and the local-controller registration restriction. Each has seven evidence stages and three delivery orders (forward, reversed, and late genesis with duplicates). Ten additional staged recovery cases reuse one database while importing controller rotations. The TypeScript and Rust suites repeat imports and reopen JSON storage from disk at every stage, checking accepted canonical operation IDs, all document/data/registration components, deactivation separately, and retention of rejected/deferred asset evidence.
Coverage includes owner transfers, prospective owners that are missing or are assets, whole-component replacement/omission, named secondary keys including relative references, unknown methods, controller deletion, terminal asset deletion, competing canonical-CID successors, tied ordinals, registry migration, an earlier controller anchor arriving after a later copy, an invalid early asset receipt alongside a valid later receipt, and gossip-only assets with chain-anchored controllers. The staged cases explicitly revoke accepted old-key operations and recover previously rejected new-key operations.
generate-asset-fixtures.mjs derives controller graphs, asset predecessor graphs, owners, named methods, component tokens, registry projections, signature predicates and receipt classes from the signed tables. AssetControllerFixtures.lean supplies A3 graphs and component/method projections; AssetFixtures.lean reconstructs controllers from each source set, checks every retained asset receipt’s derived verdict and the complete replay result with the kernel, and instantiates integrated_asset_convergence for each delivery order. It does not supply equal accepted histories or verdicts to that theorem. Registry names share one numeric projection across controllers and assets; complete registration objects remain distinct tokens. Root creation invariants are checked explicitly.
Generator rejection tests cover malformed roots, missing predecessors, detached receipts, bad signature-table dimensions, invalid agent genesis signatures, missing asset owners, incorrect expected payload/deletion metadata and unequal evidence. Reordering paired operation/ID/signature tables or event tables with remapped deliveries preserves successful generation. CI regenerates source signatures before checking both generated Lean modules, runs both runtime bridges, and builds proofs under the existing axiom allowlist.
This is finite correspondence coverage for the B1/B2 source model. It does not prove universal TypeScript/Rust refinement, signature primitives, arbitrary JSON decoding, storage/concurrency correctness or global family scheduling. C1–C3 compose and audit that boundary in the final theorem.