Two invariants from the R0.4.3 review:
A descendant capability must never reveal material sufficient to reconstruct an ancestor capability.
Evidence may be Copy. Authority-bearing transition tokens may not be Copy, Clone, repeatably derivable, or reproducible from immutable inputs. A value being non-copyable is not enough; authority must have a non-forking derivation.
Every provenance-bearing type carried the root mark and derived Debug; derived Debug prints private fields, so any holder of an honest event could recover the world-global mark and, bootstrap being public, reconstruct root authority — descendant→ancestor amplification. Closure:
Manual Debug for every mark-bearing type; the mark renders as
<redacted>. No Display/Hash/serialization impls exist.
PartialEq/Eq removed from all mark-bearing types: equality over a
secret is a guess-oracle, and nothing in replay needs record equality.
A DOWNSTREAM test (cd-node, not in-crate) formats every public
diagnostic surface with a distinctive mark and proves the bytes are absent.
Documented authority-amplification boundary: the same raw bytes that
tag descendants are what bootstrap accepts. Without cryptographic one-way derivation (out of scope for no_std R0, and faking one with an invertible permutation would be worse than honesty), redaction plus the absence of any read-back API is the containment. A deployment must replace marks with derived/attested material; stated on the skepticism list.
Not "unforgeable within a process" — type privacy is not hostile-process isolation. The enforceable claim: safe-Rust API-level unforgeability for callers that do not possess ancestor capabilities or bootstrap material. cd-core itself remains #![forbid(unsafe_code)].
LocusRoot ──begin()──────────────► Vacant(L,0) + FinalityWarden + Admission(0)
Vacant(L,N) + Admission ──attach(c)──► Attached(L,c,N) + AttachRecord(N) + Admission' [no recovery value exists]
Attached ──detach()──────────────► Vacant(L,N+1) + DetachReceipt(N)
Attached ──suspend()─────────────► CarrierCustody(N) [CONSUMES live: Live XOR Recoverable]
CarrierCustody(N) + &Admission ──recover──► Attached(L,c,N) [CONSUMES custody; judged vs CURRENT admission]
Warden + Admission ──finalize_loss► LossFinalization + Vacant(L,N+1) + Admission' [atomic; R0.4.7]
(every transition above also consumes and returns the Admission — docs/admission-model.md)R0.4.5 invariant: **a recovery representation of possession must be
mutually exclusive with live possession, unless an external fencing primitive proves only one can become active.** The R0.4.4 shape (custody minted at attach beside the live value) violated this by aliasing; the former custody() accessor is gone for the same reason. Now custody exists only by consuming the live attachment, and recovery consumes the custody. Two operational attachments for one locus/carrier/generation cannot be derived via any safe-Rust API.
Reopen was removed in R0.4.7: finality now materializes the successor
vacancy atomically with the admission advance, so an accepted closure yields exactly one vacancy within one lineage by construction. A trusted root can still mint parallel lineages via repeated create_locus; global Locus-birth uniqueness is a future World-level invariant.
The root's create_locus(same id) repeatability remains an explicitly
trusted-root act, stated, outside the linearity claim.
The R0 property is linear checkpointed restart/reconstitution in safe Rust: a planned suspend() then recover. An unplanned crash cannot call a consuming transition first, so unplanned crash recovery is NOT modeled or claimed. Durable persistence inherently copies bytes (RAM/disk/backup/journal), so !Clone is not evidence of durable single-use semantics. Durable recovery will need an explicitly modeled primitive (incarnation counters over monotonic/CAS storage, secure-element monotonicity, or supervisor fencing) — deliberately NOT designed in R0.4.4; claimed nowhere.
Consequently the possession claim in STATUS is corrected to: single-log replay accepts at most one Carrier per generation, with capability-graph forking limits (trusted-root duplicate genesis; durable copies of custody bytes) stated explicitly.
Debug of every public diagnostic surface contains no mark bytes
(downstream test).
attachment.custody() no longer exists (compile gate).
A consumed custody cannot be used twice (compile gate); recovery
yields exactly one successor.
A consumed admission cannot be reused (compile gate); one accepted
closure yields exactly one successor vacancy (finality is atomic).
All R0.4.1–R0.4.3 falsifiers still pass unchanged in meaning.