Permanent registration and termination: candidate evidence¶
As a participant, I create a new registry, register a key and terminate it permanently. The fixed contract refuses every other registry edge. The ordinary CLI selects the known new scripts and refuses unknown supplied code. Old registries are abandoned, with no migration or compatibility recognition.
Active source-removal candidate¶
The operator subsequently authorized removing obsolete active success paths.
Singular.Model now owns the two supported transitions, with compatibility
aliases in Singular.M1; canonical validators and builders implement that law.
The retired scope table records
exact archived identities and changed signatures without consumer coverage credit.
The single registry law is lean/Singular/Model.lean, source SHA-256
af220eec1be2733a7930c7fc047da63737ae26667049386eaee7af8a6559907b.
Its driver, exported corpora, simulator, validators and builders share that law.
The application model stamp carried by the archive is separately
de34300540223ccedf1ca85216b131fd09a148b4; it is not the registry source identity.
| Boundary | Fresh source-removal evidence | Limit |
|---|---|---|
| Model and application | Native Lean builds; 57 generic/naming/lifecycle/wire declarations and 10 M1 admission declarations; application 35/35 proved with executable and independent axiom-bridge controls | Abstract model; terminal hypotheses are proof-only |
| Compiled admission | 39 evaluated contexts against exported code, including both allowed effects, all five excluded encodings, mixed batches and malformed contexts; an always-unit state mutant is detected | CEK evaluation, not ledger budget or reachable Absent history |
| Validators and identities | Canonical Aiken 2,562 reported checks and naming 307 checks, zero errors; identity, size and complete deployment identity checks including disposable-devnet controls | Property iterations are included in reported counts |
| Haskell consumers | 1,077 examples, zero failures, 11 existing pending; supported components compile | Component compilation is separate from execution |
| Conformance reader and controls | 608 appendix examples, zero failures; original broader requirement texts retained; separate current retirement evidence cannot cover them; archived receipts remain readable with structural and replay checks | Appendix checks do not establish a live product claim |
| Extracted ordinary CLI | One complete fresh packaged check passes on eae076fb8847c419bc5d7577551e5339e1ca1b3a: registration, payload update without registry movement, permanent termination, rejection, owner reclaim, recovery, capabilities/events and deliberate receipt/readback faults; retained insert-active/update-terminal commands also pass |
Owner execution on disposable local ledgers; retained-command negative probes are builder/evaluator refusals |
| Presentation and scope | Simulator browser assertions, 32 inspected diagram views and missing-render controls; inventory/coverage ratchet and extra-active-deletion fault; regenerated evidence page and all five page tampering controls | Historical diagrams and receipts retain their recorded revision; no consumer credit from theorem retirement |
The connected command summary binds the extracted candidate, 69 exact source hashes, fixed script identities and individual receipt hashes. Registration reads Active. The payload update leaves the registry root unchanged and the 2,000,000-lovelace application deposit held. Termination reads Terminal with no live holding. Rejection and owner reclaim are checked against signed transaction outputs and independent readback; both leave the registry root unchanged and allow a later registration. All eight commands have actual capability evidence, and 178 prepared submissions in twelve journals name their acquisition. Archive integrity and these connected results are distinct checks. Subsequent conformance reader/control and evidence-documentation changes leave the bound production, model, validator and CLI sources byte-identical.
The public inventory has 48 requirements, 47 owned. The consumer scope receipt lists the exact four original broader requirements and their computed current uncovered state, with historical passing receipt identities. No successful Absent setup, deletion refund or reincarnation is claimed by the supported current retirement story. The generated conformance evidence page remains an explicitly historical snapshot; its counts are computed from that snapshot's receipts. Current conformance and exact-head hosted outcomes are recorded separately in PR523.
Canonical state is 68df9c42ebd4468be130e9cd5538a7af39cc31c146cda45f274cccc5,
11,557 bytes under the unchanged 15,878-byte limit. Naming custody
f154ff8488a83ed77e4cf3e4b2702d781f86d783ee291ef32e82dee5 and application
6f778eccda6306d930c6443a5d7670a02b2df79ac71437488d38a559 now carry
pins sourced from the canonical compiled identities.
Earlier aggregate failures at application proof inversion, naming cross-pins and
the historical evidence-page reader are preserved as failures; their targeted
repairs pass. Reproduce the complete repository gate with nix develop -c just ci
and the connected check with nix run .#demo1-cli-check; consult PR523 for the
final frozen-head gate outcomes. Existing processing-window and protected-rejection
holds, KERI integration and unreachable Absent cases are not counted as passing.
Protected rejection #498/#495 follows this carve; this delivery does not close M1.
Archived evidence before source removal¶
Everything in this section is historical evidence for preserved revision
a098408e58c150b9ebf83c3fd1dff1704599c01f, available on
preserve/m2/pre-m1-source-removal. Its source identities and receipts do not
certify the active source-removal candidate.
The broader model remains bound to base 464ed8674de626470396cc871f3af85a1d489477.
The new law is Singular.M1, source SHA-256
e94c1bbc502514a7be7083f56a52b595bd435050cbc868b61fe44a1fe7301a93. Its audited statement manifest
and driver corpus carry all source and declaration digests; the broader generic
corpus and driver remain byte-identical. Naming and lifecycle corpus envelopes
are refreshed for the wider source inventory; their behavior is unchanged.
| Boundary | Actual evidence | Limit |
|---|---|---|
| Bounded model | 10 audited declarations using standard axioms; 10 executed scenarios and 4 batches, 30 independently derived observations | Abstract model, not Cardano execution |
| Conformance transport | 10 scenario and 4 batch outputs match the bounded driver; broader-law and unknown-contract controls fire | No live consumer comparison receipt |
| Exported state/request/witness code | 57 component evaluations: 2 allowed edges, all 5 excluded edges, mixed batch, 6 malformed or alternate contexts, joined component contexts for every edge and four application booking/update/release contexts against both fixed and broader code | Fixture roots and witness policies; absent starting states are unreachable from genesis |
| Boundary checker fault | Replace the bounded exported state with the broader program; the same checker exits1 and names accepted terminal witnessing as a mismatch | Controlled artifact mutation, not a chain transaction |
| Script identity and size | Nix identity and publication-size checks passed, including their controls; state15,231 bytes under15,878 limit | Unapplied identities; application and witness instance pins are derived from the boot seed |
| Ordinary CLI handlers | 13 examples passed including lifecycle receipts and unknown-code refusal with final fixed script pins | Synthetic provider fixture |
| Extracted ordinary CLI journey | The complete existing package check passed: archive integrity, model stamp, script identity, connected registration, payload update with root unchanged, permanent termination, rejection, owner reclaim, capability/event and fault controls, and both retained archive commands | Owner execution on a disposable local devnet; no public-network acceptance or live bounded consumer comparison receipt |
| Ledger refusal controls | Two fresh keys on one fixed registry each satisfy 29 of 29 take clauses: duplicate Active insertion, stranger-signed update, release outside a fold and Terminal reinsertion are submitted without local evaluation and refused by the ledger, beside accepting controls and readbacks | Owner execution; the selected run covers 5 of 32 approved application cases, with 27 uncovered in that run |
| Repository boundaries | One aggregate invocation failed on a stale generated simulator identity; targeted repair passed. Separately canceled model and release checks passed; repaired documentation check passed, including computed evidence, source links and fault controls | Exact-head hosted outcomes are recorded separately in the PR and immutable handoff |
| Public conformance inventory | 47 rows, 46 owned; new bounded story remains uncovered; original broader rows retained | A component result never assigns an executed product status |
New state: 807d91e4dc360ab722ad2b3b47d6b3d000237992048f3333ae799aaa. New unapplied witness: 4c87b7aa4c2f509c8de536243f98da7a44b48cfc5bb541e19c38f5a1.
New unapplied application: eeb82738115c80dc63d606513387b85bb93e35657744a34e318d3f03. Its booking, payload-update and release guards are unchanged; its fixed state pin matches the new registry.
All four fixed scripts, compiler identity, parameter counts and byte digests are
recorded in onchain/permanent-contract.json. Every original broader compiled identity is unchanged. The simulator preserves those broader profiles and explicitly discloses that it has no playable bounded profile. The theorem inventory retains all prior declarations and adds the ten audited bounded statements: 136 obligations, 77 manifest-bound and 59 unclassified; integration coverage debt stays visible.
Reproduce the component boundary from a clean checkout:
nix build --no-link ./onchain#checks.x86_64-linux.permanent-boundary
nix build --no-link ./onchain#script-identity ./onchain#checks.x86_64-linux.reference-publication-size
nix run .#model-check
nix develop -c just model
nix run ./offchain#cage-tests -- --match Singular.CLI.CommandRun
nix run .#demo1-cli-check
nix run .#demo1-cli-attach-takes
The first check retains raw evaluated programs, context arguments, exits, output
and controlled-fault replay. The committed component and transport reports are
under evidence/. The connected command receipt summary
binds the extracted candidate 2a243ef03d556bd6c725e097d67d3d3e6ffdb442, all four compiled script digests,
the bounded law source and individual command receipt hashes. The archive's
application model stamp is de34300540223ccedf1ca85216b131fd09a148b4, distinct from
the bounded registry law source digest above. Later reference-index and independent
CLI-control runner repairs leave these production CLI, model and script sources unchanged.
The connected receipts show an active registered leaf, an application update with the same registry root and a 2,000,000-lovelace deposit still held, then a terminal leaf without a live holding. Rejection returned 2,000,000 lovelace from the request's 3,000,000 with the original 1,000,000 tip; owner reclaim returned the whole locked value. The existing journey checks these amounts against signed transaction outputs and node readback, with deliberate receipt and readback edits. It also checks later registrations after both exits. Its 178 prepared submissions across 12 journals name their actual observation capability; all eight commands have execution receipts. This product execution does not assign an executed status to the uncovered bounded public conformance story.
The first connected attempt exposed the old application's state pin at approval minting. The separate fixed application now passes 66 controls and the complete connected journey. The independent CLI refusal runner was also corrected to load the same fixed scripts before exercising its ledger controls. No old deployed recognition path was added.
The hosted a0fc7fe5 cross-wallet recovery case stopped before signing because
the built fold was inside the existing 30-second deadline guard. Its requested
hold was never reached, so that recovery evidence is missing. Hosted served-preview
verification also failed temporary DNS. Both results remain retained and affected
acceptance held; the guard, processing window and expected recovery behavior are
unchanged. Performance work belongs to the separate owner. The final exact-head
hosted outcomes remain distinct from these local results.
These results establish their named boundary only. Existing timing and protected-rejection discrepancies are not counted as passing behavior; folding an update outside its processing window remains affected acceptance held where the model and validator differ. KERI integration and broader uncovered requirements remain visible. Protected rejection follows this carve through