Authenticated Actor

Composition grounded on Final Critique 10 — 2026-11-06 at 368ce1f 4 invariants TLA+ model buggy twin ×4 regulated composes 2 atoms
Derived card — generated from the corpus (status line, invariant headers, sibling formal-model files, Composes edges). The specification below is canonical. composition graph →
Table of contents
  1. Authenticated Actor
    1. Summary
    2. Intent
    3. Composes
    4. Composition logic
      1. Composition state
      2. Capability requirement
      3. Primitive policy
      4. Action wiring
        1. Closure table
      5. Wiring decision
      6. Housekeeping
    5. Composition-level invariants
    6. Examples
      1. Walkthrough — register, attest, then revoke-and-fail, end to end
      2. Domain example — rotation keeps the surface open
      3. Rejection path — namespace conflict and unbound attest
      4. Regulated adversarial scenarios
    7. Generation acceptance
      1. Conformance checks
      2. External checks
    8. Non-goals
    9. Edge cases
      1. Concurrency
    10. Composition notes
    11. Terms
      1. Vocabulary
        1. Register Authenticated Actor
        2. Attest As Actor
        3. Verify Actor Attestation
        4. Namespace Conflict
        5. Invalid Credential
        6. Not Bound
        7. Credential Not Active
        8. Invalid Attest Credential
        9. Attest Failed
        10. Outcome
        11. Observed Status
    12. Standards references
    13. Status
    14. Ledger

Summary

Authenticated Actor is a composition — a specification that wires together two freestanding patterns, each complete on its own and depending on neither the other — that ties a principal’s login to their signature. One pattern, Credential, checks that a presented secret belongs to a principal (the login). The other, Actor Identity, produces an attestation: a permanent, checkable record that a specific actor authorized a specific action (the signature). On their own, neither pattern knows about the other, which leaves three questions unanswered when the same person has both — and this composition answers all three.

First: if you revoke someone’s login, can they still produce new signatures through this composition? The answer is no. The composition checks, every time an actor goes to sign, that their login credential is still active, and the check and the recording of the signature commit as one transaction that no revocation can split, so a revocation either comes first and the check turns the signature away, or comes after the signature is recorded. The attest log entry of every signature names the credential the check saw. Crucially, signatures made before the revocation were properly authorized at the time, and erasing them would be wrong, so the cascade only closes the door going forward; it never rewrites the past. Whether a past signature still checks out afterwards depends on the credential mechanism the deployment uses.

Second: the login secret and the signing key are kept as two separate things; the composition never uses one as the other (a password hash is not a signing key). Third: the login identity and the signing identity are locked together as one principal, so any signature can always be traced back to the person who logged in.

The composition’s defining emergent guarantee — a property that appears only when the two patterns are combined, belonging to neither alone — is that revocation cascade: a revoked login closes the signing surface. Its most common uses are regulated systems where the same person both logs in and signs actions of consequence: a clinician authenticating and then electronically signing a controlled-substance prescription, a bank officer logging in and attesting a wire approval, a developer authenticating and signing a release commit at a regulated software vendor. Any system where revoking someone’s access must also stop them from producing new signed authorizations — and where an auditor must be able to trace each signature to the authenticated identity behind it — is a candidate for this composition.


Intent

Two freestanding atoms answer two adjacent but distinct questions about a principal. Credential answers “did the right material arrive — does this presented secret match what was registered for this principal?” and produces a momentary verified signal. Actor Identity answers “can a future verifier confirm this actor authorized this specific action?” and produces a durable, non-repudiable attestation. Each is correctly specified without depending on the other (Credential’s specification names no other atom; Actor Identity’s verify validates a proof against the actor registry’s public material, not against any credential record). Yet the moment both exist for the same principal, three concepts arise that belong to neither atom alone — concepts that were surfaced not by a thought experiment but by a real implementation. The Attributed Permissions Admin demo conflated a single secret to serve as both the login credential and the attestation signing key (the section titled Cross-atom identity surface aliasing in demos/attributed-permissions-admin/CORNERS.md), and in doing so exposed three questions the library could not answer: does revoking a login revoke the ability to sign? must the two secret surfaces be distinct? and are the principal reference and actor reference namespaces bound to one principal or free to diverge? This composition is the structure that answers them.

The first and load-bearing concept is the revocation cascade, and it is the outbound-authority counterpart to Login’s session cascade. Login makes a revoked credential’s sessions die: revoking a credential and calling revoke_sessions_for_credential walks the derived-session set and terminates each. Authenticated Actor makes a revoked credential’s attestation surface die: once the principal’s authentication credential is revoked, the composition produces no new attestation for the bound actor. The asymmetry between the two cascades is itself load-bearing. A session is mutable, live state with an active set to walk; the cascade is an enumeration-and-revoke. An attestation is an immutable, point-in-time record — there is no active-attestation set to retract, and retracting one would be wrong: a validly-authorized attestation made before revocation remains a record of an authorization that was valid at its instant (Actor Identity’s non-repudiation contract is conditional on credential integrity at attestation time, not perpetually); whether it still verifies after revocation depends on the credential mechanism (Actor Identity Term proof check). The cascade that fits an immutable record surface is forward closure: the composition stops producing new attestations from the first gate read that finds the gating credential not effective-active. That forward closure is the emergent guarantee this composition owns.

The second concept is secret-surface separation. The authentication credential’s stored form is a verifier — a one-way artifact (a salted password hash, an encoded public key) from which the original secret cannot be recovered (Credential Invariant 8) and which Credential never exposes in any output (Credential’s Outputs and Feedback sections — the stored verifier is not an output field). An attestation key is a signing surface — material that produces a verifiable proof of authorship. A password hash is not a signing key; the surfaces are structurally different, and conflating them (as the demo did, for demo simplicity) is an architectural error, not a conforming shortcut. The composition forecloses the cross-routing half of this structurally — Attest As Actor takes a distinct attestation credential and never reads or re-purposes the Credential verifier (which is, by Credential Invariant 8, not even available to read) — and names the distinct-provisioning half as a deployment obligation, because no records check can prove that two opaque secrets are cryptographically distinct.

The third concept is namespace binding. Attestations are attributed to actor reference; sessions and credentials are keyed on principal reference. If the two namespaces are allowed to diverge, an audit record attributed to one identity surface cannot be reconciled to the session or credential record on the other — a forensic reconstruction problem. The composition binds the two namespaces bijectively: each authenticated actor is one (principal_ref, actor_ref) pair, recorded at registration and immutable thereafter, so an attestation’s actor reference always resolves to exactly one authenticated principal reference and vice versa.

This is a composition, not a new primitive. Credential and Actor Identity are unchanged; Authenticated Actor is the wiring that makes them coherent for a single principal. It introduces emergent actions — Register Authenticated Actor, Attest As Actor, and the read-only Verify Actor Attestation — that belong to no single constituent and exist only because the two atoms are wired together. What it is not: it is not the credential-revocation surface (the identity-management surface calls Credential.revoke; this composition provides the downstream gate, exactly as Login provides the downstream session cascade without initiating the revocation); it is not the actor registry that provisions the attestation key’s public material (an Actor Registry / Identity Provisioning concept Actor Identity already defers to); it is not an authorization surface deciding what the authenticated actor may do (Permissions); and it is not a session manager (Login). Each is named in Edge cases.


Composes

  • Credential — the authentication surface, and the constituent the gate reads.
  • Actor Identity — the attestation surface.
Composes 1: EXACTLY ONE Credential instance MUST serve the composition.
Composes 2: EXACTLY ONE Actor Identity instance MUST serve the composition.
Composes 3: The composition MUST NOT change a constituent's spec.
Composes 4: The composition MUST inherit a constituent's invariants PER Execution Contract Conformance 8.
Composes 5: The composition MUST NOT call Credential's verify at the gate.
Composes 6: The composition MUST NOT call Credential's rotate.
Composes 7: The composition MUST NOT call Credential's revoke.
Composes 8: The composition MUST NOT register an actor reference in the actor registry.
Composes 9: The composition MUST key the gate on the principal reference AND the credential type.
Composes 10: The composition MUST NOT key the gate on a credential id.

Term composition: this pattern’s wiring of Credential and Actor Identity — the namespace binding, the cascade gate and the three actions below.

Term constituents: Credential, Actor Identity.


Composition logic

Composition state

Composition state 1: The composition MUST store a principal binding map.
Composition state 2: The composition MUST store the strict inverse of the principal binding map.
Deleted: Composition state 3. Execution Contract Database 1 owns it.
Composition state 4: The composition MUST hold the principal binding map's key unique.
Composition state 5: The composition MUST hold the inverse map's key unique.
Composition state 6: The composition MUST NOT change a binding.
Composition state 7: The composition MUST store an attest log.
Deleted: Composition state 8. Action wiring 45 owns it.
Composition state 9: The composition MUST NOT change an attest log entry.
Composition state 10: EXACTLY ONE writer MUST write an attest log entry.
Composition state 11: The composition MUST NOT store a constituent's record.
Composition state 12: EVERY attest log entry MUST carry the principal reference AND the action reference the call supplied.
Composition state 13: EVERY attest log entry MUST carry the outcome of the call the entry records.

Term principal binding: the composition’s own map from a principal reference to the bound actor reference, the bound credential type, the credential id current when the binding was written (Action wiring 7) and the bound instant — a principal binding; one half of the bijection.

Term attest log: the composition’s own append-only record of every Attest As Actor call answering an attest answer — an attest log.

Term attest answer: attestation id not-bound credential-not-active registry-unavailable mechanism-unavailable invalid-attest-credential — what Attest As Actor answers, every arm of its answers line, its refusals being none of them — an attest answer.

Term success entry: an attest log entry whose outcome is success — a success entry.

Term bijection: the principal binding and the inverse together, unique on both keys — what neither constituent provides.

Contract classification: extraction-pending, two elements (the section titled Composition state in execution-contract.md). The extraction rule is unconditional — composition state that carries truth not reconstructible from constituent records is a not-yet-extracted atom — and it reaches both, because Credential keys on principal reference, Actor Identity keys on actor reference, and neither relates the two.

  • The bijection is one element, not two — two directions of one truth, with a uniqueness constraint per side. Proposed atom: a Namespace Binding — immutable, bijective, unique on both keys, no lifecycle beyond bound. Any pattern joining constituents that key on different opaque namespaces needs it.
  • The attest log is the second. Proposed atom: an Attempt Log — an append-only record of every attempt at an action past its input checks, and of what each answered. The case against it is the corpus’s split: Login holds a sibling login_event_log, and Notification Fanout routes the identical concept out to Event Log — three compositions, two answers — so if the attest log proves to be Event Log wired with a composition-supplied entry schema, the extraction goes to Event Log and no new atom is owed.

Capability requirement

Capability requirement 1: A deployment MUST declare the attest surface separation.
Capability requirement 2: A deployment MUST set the gating credential type default.
Deleted: Capability requirement 3. Execution Contract Database 2 owns it.
Deleted: Capability requirement 4. Execution Contract Database 2 owns it: an action's guard reads and the writes they decide are one transaction, and the composition names no critical section to release.
Deleted: Capability requirement 5. Execution Contract Database 2 owns it: an action's guard reads and the writes they decide are one transaction, and the composition names no critical section to release.
Deleted: Capability requirement 6. Execution Contract Database 2 owns it: an action's guard reads and the writes they decide are one transaction, and the composition names no critical section to lease.
Deleted: Capability requirement 7. Execution Contract Database 1 and Execution Contract Database 2 own it.
Deleted: Capability requirement 8. Execution Contract Database 1 and Execution Contract Database 2 own it.
Deleted: Capability requirement 9. Execution Contract Database 1 owns it.
Capability requirement 10: The deployment MUST declare the clock offset allowance.
Deleted: Capability requirement 11. Execution Contract Database 1 and Execution Contract Database 2 own it: the composition names no completion bound or cadence for a deployment to leave unset.
Capability requirement 12: The deployment MUST supply the database PER Execution Contract Database 1 through 5.
Capability requirement 13: A deployment MUST authenticate the caller of [Register Authenticated Actor] as Credential's authorized caller (Credential Composition note 12).
Capability requirement 14: A deployment MUST provision the attest credential distinct from the credential material.
Deleted: Capability requirement 15. Execution Contract Conformance 9 owns it.

Term attest surface separation: the deployment’s declaration that the attestation key material is provisioned distinct from the authentication credential material — an attest surface separation; the declaring source for Capability requirement 14’s distinct provisioning.

Term gating credential type default: the credential type the deployment sets, which a registration carrying no credential type passes to Credential’s register (Capability requirement 2, Action wiring 30) — a gating credential type default.

Term clock offset allowance: the declared bound on disagreement between this composition’s clock reading, Credential’s and Actor Identity’s, which an auditor’s comparison of a credential’s stamp with an attestation’s narrows under and no rule decides on (the regulated adversarial scenarios) — a clock offset allowance.

Primitive policy

Primitive policy 1: The composition MUST answer invalid-request for a blank principal reference.
Primitive policy 2: The composition MUST answer invalid-request for a blank actor reference.
Primitive policy 3: The composition MUST answer invalid-request for a blank credential material.
Primitive policy 4: The composition MUST answer invalid-request for a blank credential type the caller supplies.
Primitive policy 5: The composition MUST answer invalid-request for a blank action reference.
Primitive policy 6: The composition MUST answer invalid-request for a blank attest credential.
Primitive policy 7: The composition MUST answer invalid-request for an expiry instant the clock reading DOES NOT PRECEDE.
Primitive policy 8: The composition MUST compare an opaque input byte-exact AFTER the seam canonicalizes a reference (Execution Contract Logic confinement 13).
Primitive policy 9: The composition MUST NOT normalize an opaque input.
Primitive policy 10: The composition MUST NOT case-fold an opaque input.
Primitive policy 11: The composition MUST NOT interpret an action reference.
Primitive policy 12: The composition MUST NOT confirm an actor reference in the actor registry.
Term opaque input: principal reference actor reference credential type action reference attestation id.

Term reference: principal reference, actor reference, action reference, attestation id — every opaque reference this composition records or compares; the deployment canonicalizes each at the seam (Execution Contract Logic confinement 13).

Term boundary predicate: the composition’s own validation of an action’s inputs, judged before any constituent call (Primitive policy 1 through 7).

Action wiring

register_authenticated_actor(principal_ref, actor_ref, credential_material, optional credential_type, optional expires_at)
  answers registration result
  refuses invalid-request | invalid-credential(credential position) | namespace-conflict(conflict position) | storage-failure(storage position)

attest_as_actor(principal_ref, action_ref, attest_credential)
  answers attestation_id | not-bound | credential-not-active | registry-unavailable | mechanism-unavailable | invalid-attest-credential
  refuses invalid-request | attest-failed(attest position)

verify_actor_attestation(attestation_id)
  answers attestation verification result

Term registration result: credential id, actor reference and bound_at, the binding’s bound instant — what register_authenticated_actor answers.

Term attestation verification result: Actor Identity’s verify answer, passed through, with a known attestation’s actor reference and the principal reference the inverse map carries for it — what verify_actor_attestation answers; not-known carries neither, and a known attestation whose actor reference the inverse map does not carry carries the actor reference and no principal reference (Non-goal 13).

Term conflict position: guard — where a namespace conflict is found: at the guard.

Term credential position: existing — which credential a re-entry’s verification ran against: the pair’s current credential, named by its position and never by its credential id.

Term storage position: credential binding — the write that failed: the credential or the binding; nothing the registration wrote commits (Execution Contract Database 1).
Term attest position: attestation log — where an attest failed: at the attestation or at the log write.
Deleted: Action wiring 1. Execution Contract Database 2 owns it.
Action wiring 2: An admitted registration MUST answer namespace-conflict naming the guard for a principal reference the principal binding carries.
Action wiring 3: An admitted registration MUST answer namespace-conflict naming the guard for an actor reference the inverse map carries.
Action wiring 4: An admitted registration MUST call Credential's register ONLY AFTER the guard clears.
Action wiring 5: IF Credential's register answers duplicate-active-credential THEN an admitted registration MUST call Credential's verify with the supplied credential material.
Action wiring 6: IF Credential's verify answers failed-verification THEN an admitted registration MUST answer invalid-credential naming existing.
Action wiring 7: IF Credential's verify answers verified THEN an admitted registration MUST write the principal binding carrying the current credential's credential id AND the inverse map entry.
Action wiring 8: The composition MUST NOT answer duplicate-active-credential.
Action wiring 9: IF Credential's register answers a credential id THEN an admitted registration MUST write the principal binding AND the inverse map entry ONLY AFTER Credential's register answers, in the one transaction of Execution Contract Database 1.
Action wiring 41: An admitted registration MUST record the registration's own clock reading as the bound instant (Execution Contract Logic confinement 3).
Deleted: Action wiring 10. Execution Contract Database 2 owns it.
Action wiring 11: IF the binding write fails THEN an admitted registration MUST answer storage-failure naming the binding.
Deleted: Action wiring 12. Execution Contract Database 2 owns it: an action's guard reads and the writes they decide are one transaction, and the composition names no critical section to lapse.
Deleted: Action wiring 13. Execution Contract Database 2 owns it: an action's guard reads and the writes they decide are one transaction, so no guard runs again over a committed credential.
Action wiring 14: An admitted attestation MUST resolve the actor reference from the principal binding.
Action wiring 15: IF no principal binding EXISTS for the principal reference THEN an admitted attestation MUST answer not-bound.
Deleted: Action wiring 16. Execution Contract Database 2 owns it.
Action wiring 17: An admitted attestation MUST read Credential's effective status, of each credential, for the principal reference AND the bound credential type; the gate read answers effective-active where an effective-active credential EXISTS for the principal reference AND the bound credential type (Action wiring 18; Credential Operation 52).
Action wiring 18: IF no effective-active credential EXISTS THEN an admitted attestation MUST answer credential-not-active.
Action wiring 19: An admitted attestation MUST call Actor Identity's attest ONLY AFTER the gate read answers effective-active.
Action wiring 20: An admitted attestation MUST call Actor Identity's attest with the caller's action reference AND the bound actor reference.
Action wiring 21: An admitted attestation MUST NOT call Actor Identity's attest with a caller-supplied actor reference.
Action wiring 22: An admitted attestation MUST call Actor Identity's attest with the caller's attest credential.
Action wiring 23: An admitted attestation MUST NOT call Actor Identity's attest with the credential material.
Deleted: Action wiring 38. Action wiring 47 owns it.
Action wiring 47: IF Actor Identity's attest answers registry-unavailable THEN an admitted attestation MUST answer registry-unavailable (Execution Contract Constituent failure 2).
Action wiring 49: IF Actor Identity's attest answers mechanism-unavailable THEN an admitted attestation MUST answer mechanism-unavailable.
Action wiring 39: IF Actor Identity's attest answers invalid-credential THEN an admitted attestation MUST answer invalid-attest-credential.
Action wiring 40: IF Actor Identity's attest answers storage-failure THEN an admitted attestation MUST answer attest-failed naming the attestation (Execution Contract Constituent failure 1).
Action wiring 42: IF Actor Identity's attest answers invalid-request THEN an admitted attestation MUST answer invalid-request.
Action wiring 44: IF Actor Identity's attest answers state-unavailable THEN an admitted attestation MUST answer attest-failed naming the attestation (Execution Contract Constituent failure 3).
Action wiring 45: EVERY [Attest As Actor] call answering an attest answer MUST append EXACTLY ONE attest log entry.
Action wiring 24: IF the gate read answers effective-active THEN the attest log entry MUST carry the current credential's credential id.
Action wiring 48: IF Actor Identity's attest answers an attestation id THEN the attest log entry MUST carry the attestation id.
Action wiring 25: IF an attest log entry's append fails THEN an admitted attestation MUST answer attest-failed naming the log.
Action wiring 26: [Verify Actor Attestation] MUST call Actor Identity's verify with the attestation id.
Action wiring 50: IF Actor Identity's verify answers verified OR failed-verification THEN [Verify Actor Attestation] MUST read the attestation's actor reference through Actor Identity's read, selecting the attestation by the attestation id.
Action wiring 27: IF the inverse map carries a known attestation's actor reference THEN [Verify Actor Attestation] MUST resolve the actor reference through the inverse map.
Action wiring 28: [Verify Actor Attestation] MUST NOT write.
Action wiring 29: The composition MUST take a principal reference, an actor reference AND a credential material on register_authenticated_actor.
Action wiring 30: An admitted registration MUST pass the gating credential type default for an absent credential type.
Action wiring 31: IF Credential's register answers invalid-request THEN an admitted registration MUST answer invalid-request.
Action wiring 32: IF Credential's register answers storage-failure THEN an admitted registration MUST answer storage-failure naming the credential (Execution Contract Constituent failure 1).
Action wiring 43: IF Credential's register answers state-unavailable THEN an admitted registration MUST answer storage-failure naming the credential (Execution Contract Constituent failure 3).
Deleted: Action wiring 33. Execution Contract Database 2 owns it: an action's guard reads and the writes they decide are one transaction, so no guard runs again over a committed credential.
Action wiring 34: IF the gate read answers a credential AND no effective-active credential EXISTS THEN the attest log entry MUST carry the observed status AND the credential id of the credential Credential's read answers last for the principal reference AND the bound credential type (Execution Contract Read 5).
Action wiring 46: IF the gate read answers no credential THEN the attest log entry MUST carry the observed status none.
Deleted: Action wiring 35. Action wiring 25 owns it.
Deleted: Action wiring 36. Execution Contract Database 2 owns it: an action's guard reads and the writes they decide are one transaction, and the composition names no critical section to lapse.
Deleted: Action wiring 37. Execution Contract Database 2 owns it: an action's guard reads and the writes they decide are one transaction, and the composition names no critical section to lapse.

NOTE: watch the constituent’s failed read (Action wiring 43, Action wiring 44).

Term admitted registration: a Register Authenticated Actor call whose inputs cleared the boundary predicate; the composition’s own sense, in which a rule conditioned on it holds for a call whose write then fails and answers its failure, and which Execution Contract Read 4’s reading of admission on the committed writes does not govern here.

Term admitted attestation: an Attest As Actor call whose inputs cleared the boundary predicate; the composition’s own sense, in which a rule conditioned on it holds for a call whose write then fails and answers attest-failed, and which Execution Contract Read 4’s reading of admission on the committed writes does not govern here.

Term effective-active: Credential’s derived status projection reading active — stored active AND the credential’s expiry instant not reached, evaluated by Credential against the clock reading at Credential’s own seam.

Term current credential: of the effective-active credentials Credential’s read answers for a principal reference AND a credential type, the one it answers last, the latest by registration instant and, of equal instants, the greatest by credential id, the order Credential’s read answers in (Execution Contract Read 5, Credential Operation 69, Credential Operation 70).

NOTE: watch cardinality (Term current credential, Action wiring 17).

Closure table

Every input an action takes, and every answer a call of the three actions can meet — Credential’s register, verify and read, and Actor Identity’s attest, verify and read — with where the call lands it and the rule that owns the landing. A constituent call meets the answers its signature declares and the state-unavailable a failed read of the database gives every action (Execution Contract Read 1); a call that never answers is the lost answer of Execution Contract Error model 1, written no answer here. Each action is one transaction (Execution Contract Database 1), the state its guards decide on read inside it (Execution Contract Database 2). An Attest As Actor row landing not-bound, credential-not-active, registry-unavailable, mechanism-unavailable or invalid-attest-credential lands an answer, not a refusal, so the call is admitted and its attest log entry commits with it (Action wiring 45); a refusal writes nothing (Execution Contract Read 4). A constituent’s state-unavailable lands where the composition lands that constituent’s storage-failure for the same call (Execution Contract Constituent failure 3): Credential’s register’s as storage-failure naming the credential (Action wiring 43) and Actor Identity’s attest’s as attest-failed naming the attestation (Action wiring 44), each a code the signature already carries; a read the composition itself makes, Credential’s read and verify and Actor Identity’s verify and read answer it passed through unchanged (Execution Contract Read 1).

Inputs.

Action Input Lands Owner
Register Authenticated Actor a blank principal reference, actor reference or credential material invalid-request, nothing written Primitive policy 1, 2, 3
Register Authenticated Actor a blank credential type the call carries invalid-request, nothing written Primitive policy 4
Register Authenticated Actor no credential type the gating credential type default, passed to Credential’s register Action wiring 30
Register Authenticated Actor an expiry instant the clock reading does not precede invalid-request, nothing written: the registration’s own clock reading judges the instant before Credential’s register judges it on Credential’s, and a refusal at either seam lands invalid-request Primitive policy 7, Action wiring 31
Attest As Actor a blank principal reference, action reference or attest credential invalid-request, nothing written Primitive policy 1, 5, 6
Verify Actor Attestation an attestation id passed to Actor Identity’s verify unchanged Action wiring 26
every action an opaque input compared byte-exact, a reference after the seam canonicalizes it, never normalized, case-folded or interpreted by the composition Primitive policy 8 through 11

The composition’s own reads, each inside its action’s transaction. A read of the principal binding or the inverse map that fails answers state-unavailable and writes nothing (Execution Contract Read 1 through 3).

Read Finds Lands Owner
the guard, at Register Authenticated Actor a principal reference the principal binding carries, or an actor reference the inverse map carries namespace-conflict naming the guard, nothing written Action wiring 2, 3
the guard neither Credential’s register Action wiring 4
the principal binding, at Attest As Actor no binding for the principal reference not-bound, and its attest log entry Action wiring 15, 45
the principal binding the bound actor reference and the bound credential type the gate read Action wiring 14, 17
the inverse map, at Verify Actor Attestation the principal reference bound to the attestation’s actor reference, or none the attestation verification result Action wiring 27, Non-goal 13

Credential’s register, at Register Authenticated Actor once the guard clears (Action wiring 4).

Answer Lands Owner
a credential id the principal binding and the inverse map entry written, then the registration result answered Action wiring 9, 41, Term registration result
duplicate-active-credential Credential’s verify, with the supplied credential material; never answered Action wiring 5, 8
invalid-request invalid-request Action wiring 31
storage-failure storage-failure naming the credential, nothing committed Action wiring 32
state-unavailable storage-failure naming the credential, nothing committed Action wiring 43
no answer no answer to give Execution Contract Error model 1

Credential’s verify, at the re-entry arm (Action wiring 5).

Answer Lands Owner
verified the principal binding, carrying the current credential’s credential id, and the inverse map entry written, then the registration result answered Action wiring 7, 41, Term current credential
failed-verification invalid-credential naming existing, nothing written Action wiring 6
state-unavailable passed through unchanged, nothing written Execution Contract Read 1 through 3
no answer no answer to give Execution Contract Error model 1

Credential’s read: the gate read at Attest As Actor (Action wiring 17), and at the re-entry arm the read that finds the current credential (Term current credential).

Answer Lands Owner
at the gate, an effective-active credential for the principal reference and the bound credential type Actor Identity’s attest Action wiring 19
at the gate, credentials of the pair, none of them effective-active credential-not-active, and its attest log entry carrying the observed status and the credential id of the credential the read answers last Action wiring 18, 34, 45
at the gate, no credential of the pair credential-not-active, and its attest log entry carrying the observed status none Action wiring 18, 46, 45
at the re-entry arm, the pair’s credentials the current credential, whose credential id the principal binding carries Action wiring 7, Term current credential
state-unavailable passed through unchanged, nothing written Execution Contract Read 1 through 3
no answer no answer to give Execution Contract Error model 1

Actor Identity’s attest, at Attest As Actor once the gate read answers effective-active, with the caller’s action reference, the bound actor reference and the caller’s attest credential (Action wiring 19 through 23).

Answer Lands Owner
an attestation id the success entry appended, carrying the attestation id and the current credential’s credential id, then the attestation id answered Action wiring 45, 24, 48, Invariant 4.3
invalid-request invalid-request, nothing written Action wiring 42
registry-unavailable registry-unavailable, and its attest log entry carrying the current credential’s credential id Action wiring 47, 45, 24
mechanism-unavailable mechanism-unavailable, and its attest log entry carrying the current credential’s credential id Action wiring 49, 45, 24
invalid-credential invalid-attest-credential, and its attest log entry carrying the current credential’s credential id Action wiring 39, 45, 24
storage-failure attest-failed naming the attestation, nothing committed Action wiring 40, Invariant 4.2
state-unavailable attest-failed naming the attestation, nothing committed Action wiring 44, Invariant 4.2
no answer no answer to give Execution Contract Error model 1

Actor Identity’s verify, at Verify Actor Attestation (Action wiring 26), which writes nothing (Action wiring 28).

Answer Lands Owner
verified or failed-verification passed through, with the attestation’s actor reference, which Actor Identity’s read answers (the next table), and the principal reference the inverse map carries for it, or no principal reference where it carries none Action wiring 50, 27, Non-goal 13, Term attestation verification result
not-known passed through, carrying neither Term attestation verification result
state-unavailable passed through unchanged Execution Contract Read 1 through 3
no answer no answer to give Execution Contract Error model 1

Actor Identity’s read, at Verify Actor Attestation once Actor Identity’s verify answers verified or failed-verification (Action wiring 50), which writes nothing (Action wiring 28).

Answer Lands Owner
every attestation the attestation carrying the attestation id selected, and its actor reference taken for the attestation verification result Action wiring 50, 27
state-unavailable passed through unchanged Execution Contract Read 1 through 3
no answer no answer to give Execution Contract Error model 1

The composition’s own writes. A binding write that fails answers storage-failure naming the binding (Action wiring 11); an attest log entry’s append that fails answers attest-failed naming the log (Action wiring 25). In each, nothing the action wrote commits (Execution Contract Database 1), and an attest-failed call appends no entry (Invariant 4.2).

Wiring decision

Wiring decision 1: The composition MUST gate an attestation on the gating credential's effective-active status.
Deleted: Wiring decision 2. Execution Contract Database 2 owns it.
Deleted: Wiring decision 3. Execution Contract Database 2 owns it.
Wiring decision 4: The composition MUST NOT close an attestation Actor Identity already recorded.
Wiring decision 5: The composition MUST NOT ask Actor Identity to refuse a revoked principal's attestation.
WHY

Principle. No attestation is produced through this composition for a principal whose gating credential does not read effective-active at the gate read, and no attestation Actor Identity has recorded is closed.

Likely objection. Why not have Actor Identity refuse a revoked principal, or walk a revocation to the principal’s attestations, as Login walks a revoked credential’s sessions?

Mechanism that resolves it. Actor Identity verifies against the actor registry, not a credential record, and an attestation is an immutable, point-in-time record with no active set to walk: retracting one would undo an authorization that was valid when made (Actor Identity Invariant 8). Only the composition holds both the binding and the call order, so it reads Credential’s effective status for the bound pair inside the attesting transaction, and Execution Contract Database 2 commits no write of that transaction against a state the gate read did not see: a revoke commits before the gate read, which then answers credential-not-active, or after the attestation commits.

Result. Forward closure: a revoked login opens no new signature, and every signature recorded before the revoke stays a record of an authorization that was valid when made (Actor Identity Invariant 8).

Housekeeping

Deleted: Housekeeping 1. Execution Contract Database 1 and Execution Contract Database 3 own it.
Deleted: Housekeeping 2. Execution Contract Database 1 owns it.
Deleted: Housekeeping 3. Execution Contract Database 1 owns it.
Deleted: Housekeeping 4. Execution Contract Database 1 owns it.
Deleted: Housekeeping 5. Execution Contract Database 1 owns it.
Deleted: Housekeeping 6. Execution Contract Database 1 owns it.
Deleted: Housekeeping 7. Execution Contract Database 1 owns it.

Composition-level invariants

Each emerges from the composition; none belongs to one constituent.

  • Invariant 1 — Revocation cascade, attest-surface closure.
    Invariant 1.1: The composition MUST NOT produce an attestation for a principal reference carrying no effective-active gating credential at the gate read.
    Deleted: Invariant 1.2. Action wiring 19 and Execution Contract Database 2 own it.
    Deleted: Invariant 1.3. Invariant 1.1 owns it: a revoked credential never reads effective-active again (Credential Invariant 5.1), and a new credential for the principal reference AND the credential type opens the gate (Composes 9).
    
  • Invariant 2 — Secret-surface separation.
    Invariant 2.1: The composition MUST NOT pass the credential material to Actor Identity's attest.
    Invariant 2.2: The composition MUST NOT pass Credential's verifier to Actor Identity's attest.
    Deleted: Invariant 2.3. Capability requirement 14 owns it.
    
  • Invariant 3 — Namespace binding.
    Invariant 3.1: EVERY bound principal reference MUST carry EXACTLY ONE actor reference.
    Invariant 3.2: EVERY bound actor reference MUST carry EXACTLY ONE principal reference.
    Invariant 3.3: The principal binding AND the inverse map MUST agree.
    
  • Invariant 4 — Attestation traceability.
    Deleted: Invariant 4.1. Action wiring 45 owns it.
    Invariant 4.2: An [Attest As Actor] call answering attest-failed MUST NOT append an attest log entry.
    Invariant 4.3: EVERY success entry MUST carry the attestation id AND the current credential's credential id.
    Deleted: Invariant 5. Composes 4 owns it.
    

Examples

Walkthrough — register, attest, then revoke-and-fail, end to end

A regulated software vendor authenticates developers and requires every release commit to be signed. It deploys Authenticated Actor with gating_credential_type_default = "fido2" and attest_surface_separation = enforced.

  1. Registration. The identity-management surface registers developer dev_smith: register_authenticated_actor(principal_ref = "dev_smith", actor_ref = "actor_smith", credential_material = <fido2-attestation-object>, credential_type = "fido2"). The namespace-conflict guard passes (neither namespace is bound); Credential.register returns credential_id = "cred_s01"; principal_to_actor["dev_smith"] = {actor_ref: "actor_smith", credential_type: "fido2", credential_id: "cred_s01", bound_at} and actor_to_principal["actor_smith"] = "dev_smith" are written. Returns {credential_id: "cred_s01", actor_ref: "actor_smith", bound_at}.

  2. Attestation while Active. The developer signs a release commit with their separate hardware signing key: attest_as_actor(principal_ref = "dev_smith", action_ref = "commit_c44a", attest_credential = <hardware-signing-key>). Step 2 resolves actor_smith. Step 3 reads Credential’s read(filter) surface: an effective-Active fido2 credential, cred_s01, exists for ("dev_smith", "fido2") → gate open. Step 4 calls Actor Identity.attest("commit_c44a", "actor_smith", <hardware-signing-key>) → attestation_id = "att_a17". Step 5 logs success with credential_id: "cred_s01". Returns att_a17. The continuous-integration system later calls verify_actor_attestation("att_a17") → {result: verified, actor_ref: "actor_smith", principal_ref: "dev_smith"} before merging — the signature verifies and resolves to the authenticated developer.

  3. Revocation closes the surface. Security determines cred_s01 was compromised. The identity-management surface calls Credential.revoke("cred_s01", revoked_by_ref = "security_team", reason = "key-compromise") — cred_s01 is now Revoked (Credential Invariant 4). No call into Authenticated Actor is required to “cascade”: the next attestation attempt is turned away structurally. attest_as_actor("dev_smith", "commit_c45b", <hardware-signing-key>) → step 3 reads the credential records, finds no effective-Active credential for ("dev_smith", "fido2") → appends attest_log {outcome: credential-not-active, observed_status: Revoked, credential_id: "cred_s01"}; returns credential-not-active. The revoked login can no longer sign (Invariant 1). The earlier att_a17 was validly authorized before revocation (Actor Identity Invariant 8). Under a mechanism that carries the revocation status inside the proof (Actor Identity Revocation status 1) it still verifies; under a live revocation mechanism (Revocation status 3) its verify answers failed-verification with the reason proof-invalid once that service names the signing key revoked, which the revoke of the login does not itself do (Capability requirement 14 keeps the signing key distinct from the login).

Domain example — rotation keeps the surface open

The same developer’s hardware authenticator is replaced under the 12-month rotation policy. The identity-management surface calls Credential.rotate("cred_s01", <new-fido2-object>) → "cred_s02" (cred_s01 → Rotated, cred_s02 → Active, same ("dev_smith", "fido2") pair — Credential Invariants 2 and 6). No rebinding is needed: attest_as_actor("dev_smith", "commit_c46c", <hardware-signing-key>) → step 3 finds an Active credential for the pair (the rotation successor) → gate open → attestation produced. The gate keys on the (principal_ref, credential_type) pair, not the fixed credential id, precisely so that a rotation (the actor is still legitimate) keeps the surface open while a revocation (the actor’s authority is withdrawn) closes it. This is the load-bearing distinction between Credential Invariant 6 (rotation non-mutation, new Active successor) and Invariant 4 (revocation absorbing, no Active successor).

Rejection path — namespace conflict and unbound attest

  • Namespace conflict. A second registration reuses an already-bound actor: register_authenticated_actor("dev_jones", "actor_smith", <material>, "fido2") → step 2 finds actor_smith already in actor_to_principal → namespace-conflict(guard); no credential is registered, no binding written. Had two registrations for actor_smith under two different principals run concurrently, the later would read the maps again once the earlier committed, find actor_smith bound and answer namespace-conflict(guard), registering no credential. The bijection (Invariant 3) is preserved: actor_smith stays bound to exactly dev_smith.
  • Attest for an unbound principal. attest_as_actor("dev_unknown", "action_x", <key>) for a principal never registered through the composition → step 2 finds no binding → attest_log {outcome: not-bound}; not-bound. This is distinct from credential-not-active: the principal was never an authenticated actor at all.
  • Invalid attestation credential. attest_as_actor("dev_smith", "commit_c47d", <wrong-signing-key>) while the credential is Active → gate open, but Actor Identity.attest returns invalid-credential (the signing material does not validate against the registry’s public material for actor_smith) → attest_log {outcome: invalid-attest-credential}; invalid-attest-credential. The gate (authentication still valid) and the attest check (signing key valid) are independent surfaces — secret-surface separation in action (Invariant 2).

Regulated adversarial scenarios

Three scenarios the composition must survive in regulated contexts.

Regulator audit — “prove this signed action was authorized by a principal whose login was valid at signing time, and trace the signature to that login.” An auditor examines attestation att_a17. verify_actor_attestation("att_a17") returns {verified, actor_ref: "actor_smith", principal_ref: "dev_smith"} where the mechanism carries the revocation status inside the proof (Actor Identity Revocation status 1; under a live revocation mechanism, Revocation status 3, a verify made after that service names the signing key revoked answers failed-verification with the reason proof-invalid, and the audit rests on the credential records below) — the proof verifies (Actor Identity Invariants 2 and 3) and resolves to the authenticated principal via the namespace binding (Invariant 3). The auditor reads the credential records for ("dev_smith", "fido2") — cred_s01, the record the success entry’s credential id names — and confirms it was effective-Active at att_a17.attested_at: its revoked_at lies later than that by more than clock offset allowance (Credential’s clock and Actor Identity’s are two seams, so the comparison narrows under the allowance rather than deciding on its own). The attest-log entry for att_a17 corroborates the timeline (Invariant 4). Every claim is provable from the composition’s records plus the two constituent records. The structural guarantee that a revoked login could not have produced a new signature after revocation is Invariant 1.

Disputed signature — the principal claims they did not authorize an action. dev_smith disputes commit_c44a. The investigator calls verify_actor_attestation("att_a17"): verified binds actor_smith to commit_c44a at attested_at (Actor Identity Invariant 8). The namespace binding resolves actor_smith to dev_smith (Invariant 3). The dispute cannot be sustained without claiming credential compromise — which is exactly the boundary Actor Identity Invariant 8 names (non-repudiation conditional on credential integrity), routed to a Compromise Disclosure composing pattern. The investigator additionally confirms, from the credential records and by the entry’s credential id, that cred_s01 was effective-Active at signing time within clock offset allowance, so the signature was produced through a valid login surface — Invariant 1’s gate was satisfied at the time.

Breach investigation — “during the compromise window, was any new signature produced after we revoked the credential?” A security team revoked cred_s01 and asks whether the attacker produced signatures afterward. The revoke’s commit is the boundary, not its stamp: T_revoke (cred_s01.revoked_at) is Credential’s clock reading when the revoke ran, an attestation’s attested_at is Actor Identity’s reading inside the attesting transaction, and a revoke can take its reading while an attestation’s transaction is open and still commit after it (Execution Contract Database 2), so an attested_at later than T_revoke, by any margin, the clock offset allowance included, proves nothing alone. For each success entry naming cred_s01, they read cred_s01 as it stood at the entry’s commit (Execution Contract Database 5): an entry whose credential stood Revoked there would be the smoking gun, the conformance failure Check 2.2 reads, and Invariant 1 forecloses it: Execution Contract Database 2 commits no write against a state its guards did not see, so an attestation whose gate read found cred_s01 effective-Active commits before the revoke does or not at all, reading again and deciding again, and a gate read made after the revoke committed finds no effective-Active record. Every call whose gate read came after the revoke’s commit appended outcome: credential-not-active, observed_status: Revoked, credential_id: "cred_s01" and no attestation id — the gate closed on it. The forward-closure boundary is the revocation’s commit, and the attest_log makes every post-revocation attempt provable.


Generation acceptance

An implementation is acceptable when the checks below are provable to an external auditor given the credential records with their earlier versions (Execution Contract Database 5), the attestation records, the binding maps and the attest log.

Conformance checks

Check 1.1: An auditor MUST find EVERY bound principal reference carrying one actor reference (Invariant 3.1).
Check 1.2: An auditor MUST find EVERY bound actor reference carrying one principal reference (Invariant 3.2).
Check 1.3: An auditor MUST find the principal binding AND the inverse map agreeing (Invariant 3.3).
Check 2.1: An auditor MUST find EVERY success entry carrying the attestation id AND the current credential's credential id (Invariant 4.3).
Check 2.2: An auditor MUST read a success entry whose credential id names a credential standing in revoked at the entry's commit as an Invariant 1.1 violation (Execution Contract Database 5).
Deleted: Check 2.3. Execution Contract Database 2 owns it.
Check 3.1: An auditor MUST find EVERY [Attest As Actor] call answering an attest answer carrying one attest log entry (Action wiring 45).
Check 3.2: An auditor MUST find EVERY credential-not-active entry carrying the observed status (Action wiring 34, Action wiring 46).
Deleted: Check 4.1. Execution Contract Database 1 owns it.
Check 5.1: An auditor MUST find no attest log entry changed (Composition state 9).
Deleted: Check 6.1. Execution Contract Database 1 owns it.

NOTE: EVERY check names the rule the check tests.

External checks

External check 1: An auditor needing the two secret surfaces confirmed distinct MUST read the deployment's own provisioning (Capability requirement 14).
Deleted: External check 2. Execution Contract Database 2 owns it.
External check 3: An auditor needing an actor reference confirmed in the actor registry MUST read the actor registry (Composes 8).
External check 4: An auditor needing a verification read recorded MUST read a composed access log (Non-goal 12).
External check 5: An auditor needing a constituent's own guarantee confirmed MUST read the constituent's own acceptance (Composes 4).

Non-goals

Non-goal 1: The composition MUST NOT confirm the two secret surfaces cryptographically distinct.
Non-goal 2: The composition MUST NOT confirm an actor reference provisioned in the actor registry.
Non-goal 3: The composition MUST NOT invalidate an attestation for a credential later found compromised.
Non-goal 4: The composition MUST NOT compose Audit Trail.
Non-goal 5: The composition MUST NOT revoke a credential.
Non-goal 6: The composition MUST NOT rotate a credential.
Non-goal 7: The composition MUST NOT close an attestation already recorded.
Non-goal 8: The composition MUST NOT register an actor reference.
Non-goal 9: The composition MUST NOT authorize an action.
Non-goal 10: A deployment needing an authorized action MUST compose Permissions.
Non-goal 11: The composition MUST NOT rebind a bound principal reference.
Non-goal 12: The composition MUST NOT record a verification read.
Non-goal 13: The composition MUST NOT resolve an attestation carrying an actor reference the inverse map does not carry.
Deleted: Non-goal 14. Execution Contract Database 1 owns it.
Non-goal 15: The composition MUST NOT set a retention policy.
NOTE: watch the adopter's policy note (Non-goal 15).
NOTE: open 2026-11-04-a (Non-goal 15).

NOTE: the owners — the attestation records themselves, as the tamper-evident external-auditor surface (Non-goal 4); a composed Retention Window, which a deployment needing a retention bound on an attestation composes (Non-goal 15; Actor Identity Composition note 4, Actor Identity Non-goal 16).


Edge cases

Concurrency

Deleted: Concurrency 1. Execution Contract Database 2 owns it.
Deleted: Concurrency 2. Execution Contract Database 2 owns it: an action's guard reads and the writes they decide are one transaction, so a revoke of the credential a gate read commits before the read or after the attestation.
Deleted: Concurrency 3. Execution Contract Database 2 owns it.
Deleted: Concurrency 4. Execution Contract Database 2 owns it: an action's guard reads and the writes they decide are one transaction, so the composition declares no residue to bound.
Deleted: Concurrency 5. Execution Contract Database 2 owns it.
Deleted: Concurrency 6. Execution Contract Database 2 owns it: an action's guard reads and the writes they decide are one transaction, so the composition declares no residue for a deployment to close.

Composition notes

Deleted: Composition note 1. Execution Contract Conformance 9 owns it.
Deleted: Composition note 2. Capability requirement 14 owns it.
Composition note 3: A deployment MUST own an actor reference's provisioning in the actor registry.
Composition note 4: A deployment MUST own a credential's revocation AND rotation.
Composition note 7: A deployment MUST own Credential's register of a new credential for a bound principal reference.
Deleted: Composition note 5. Execution Contract Database 2 owns it: an action's guard reads and the writes they decide are one transaction, so the composition declares no residue for a deployment to close.
Deleted: Composition note 6. Execution Contract Database 1 owns it: a registration's credential and binding commit together, so the composition reports no orphaned credential.

Terms

The canonical concepts this spec refers to. Each term marker in the prose above links to its term entry here. A term entry states what the concept is, in plain English, plus its Kind — one of five: Type (a thing or category), Operation (a behavior), Member (a value of an enumerated Type), or, for a named datum, Field (a datum a Type carries — what does it carry?) or Parameter (a value an Operation needs — what does it need?). A term entry also names the Type it is a Member of / Field of, the Operation it is a Parameter of, and its Role where the domain assigns one. A term entry carries one Projection line — the concept’s single canonical lowering token, the one place the concrete name stays visible on the page — for every Field, Parameter, and pinned/wire Member. Everything else about casing (each target’s snake / camel / pascal / const / wire form) is derived from that one token by tools/harness/term-adapter.mjs, never hand-written. This is a composition, so its own concepts are the three emergent actions it exposes (Register Authenticated Actor, Attest As Actor, Verify Actor Attestation) — none belonging to a single constituent — the attest-log fields those actions record (Outcome, Observed Status), the outcomes Attest As Actor answers without producing an attestation (Not Bound, Credential Not Active, Invalid Attest Credential), and its own rejections (Namespace Conflict, Invalid Credential, Attest Failed). Its emergent state — the namespace-binding maps (principal_to_actor, actor_to_principal) and the attest_log — is a composition-introduced surface no constituent provides, left as backticked record tokens rather than carded. References to the constituent atoms and their operations — Credential’s register / rotate / revoke, Actor Identity’s attest / verify — the relayed tokens (principal reference, actor reference, action reference, credential material, attest credential, credential type, credential id, attestation id), the credential states (Active / Revoked / Expired / Rotated), and the inherited codes (invalid-request; registry-unavailable and mechanism-unavailable, Actor Identity’s attest’s, which Attest As Actor answers as outcomes (Action wiring 47, Action wiring 49); storage-failure — exported at this boundary with its position, storage-failure(credential | binding); duplicate-active-credential is consumed by step 3’s re-entry arm and not exported) remain qualified/backticked, not carded here. (annotation.md Terms registry; representational only — it changes no guarantee, invariant, or behavior of the composition above.)

Vocabulary

Term qualifiers: migrated — rewritten in GRACE lang v0.40 (2026-09-14).

Term terms: composition, constituents, reference, principal binding, attest log, attest answer, success entry, bijection, attest surface separation, gating credential type default, clock offset allowance, blank, opaque input, boundary predicate, admitted registration, admitted attestation, effective-active, current credential, conflict position, credential position, storage position, attest position, registration result, attestation verification result.

Term record verbs: call, answer, read, write, append, store, key, hold, take, resolve, bind, register, revoke, rotate, gate, precede, close, produce, provision, pass, agree, carry, change, refuse, set, declare, own, compose, inherit, confirm, interpret, normalize, case-fold, compare, authorize, authenticate, invalidate, rebind, find, serve, supply, ask, record.

Term actors: the composition; the constituents; a deployment; an auditor; a caller; a principal; an actor; an invocation; an attestation; a credential.

Term cited: Execution Contract Conformance 8 — recursive conformance and the inherited guarantee. The section titled Composition state in execution-contract.md — the extraction-pending classification. The section titled Capability provenance in pressure-testing.md — the declared-source discipline.

Term attest credential: attest_credential — the signing material the caller presents for Actor Identity’s attest; never the credential material.

Register Authenticated Actor

The composition’s intake action: it binds an actor reference to a principal reference (behind the namespace-conflict guard) and registers the principal’s authentication credential through Credential.register — two ordered writes, credential then binding, the strict-inverse binding maps written as the second. Returns {credential_id, actor_ref, bound_at}, or Namespace Conflict, Invalid Credential, or an inherited Credential rejection (invalid-request, storage-failure(credential | binding)); Credential’s duplicate-active-credential is the re-entry arm that binds an existing effective-Active credential once Credential.verify proves the presenter holds it.

Kind: Operation

Attest As Actor

The composition’s load-bearing emergent action: it produces a non-repudiable attestation for the bound actor only if the principal’s gating credential is currently Active — the revocation cascade, enforced as a forward gate read immediately before the attestation write (Invariant 1). Answers the attestation id, or one of five outcomes that produce no attestation: Not Bound (principal never bound), Credential Not Active (the gate is closed), registry-unavailable (Actor Identity could not read the actor registry), mechanism-unavailable (the deployment’s credential mechanism supplied no credential check) and Invalid Attest Credential (signing key invalid). Each is the call’s answer, not a refusal, and the call’s attest log entry commits with it (Action wiring 45). Refuses invalid-request and Attest Failed — positioned attestation or log — and a refused call writes nothing (Execution Contract Read 4).

Kind: Operation

Verify Actor Attestation

The composition’s read-only query: a pass-through to Actor Identity.verify that additionally reads the attestation’s actor reference through Actor Identity.read and resolves it back to its bound principal reference. Returns an attestation verification result; changes no state.

Kind: Operation

Namespace Conflict

The composition’s own rejection from Register Authenticated Actor — returned when the principal reference or the actor reference is already bound, enforcing the principal ⇔ actor bijection at the boundary (Invariant 3). Positioned: guard (step 2 — nothing is written).

Kind: Member Member of: the register rejection Role: Rejection Projection: namespace-conflict

Invalid Credential

The composition’s own rejection from Register Authenticated Actor’s re-entry arm — returned when the pair already holds an effective-Active credential and Credential.verify does not return verified for the presented credential material: the presenter has not proved possession of the existing credential, so nothing is adopted and nothing is written. Carries existing, its credential position: the verification ran against the pair’s current credential, and the answer carries no credential id.

Kind: Member Member of: the register rejection Role: Rejection Projection: invalid-credential

Not Bound

The composition’s own outcome of Attest As Actor, answered and not refused — returned when the principal reference was never bound through the composition, with the call’s attest log entry (Action wiring 15, Action wiring 45). Structurally distinct from Credential Not Active: never an authenticated actor, versus bound but no longer authenticated.

Kind: Member Member of: the attest outcome Role: Outcome Projection: not-bound

Credential Not Active

The composition’s load-bearing outcome of Attest As Actor, answered and not refused — the revocation cascade’s observable form: returned when no Active credential exists for the bound (principal_ref, credential_type) pair (revoked, expired, rotated without a current successor, or none at all). The answer carries no payload; the call’s attest log entry carries the Observed Status (Action wiring 34, Action wiring 46).

Kind: Member Member of: the attest outcome Role: Outcome Projection: credential-not-active

Invalid Attest Credential

The composition’s own outcome of Attest As Actor, answered and not refused — the mapping of Actor Identity.attest’s invalid-credential: the presented signing material did not validate against the actor registry’s public material for the bound actor reference. Independent of the authentication gate (secret-surface separation, Invariant 2).

Kind: Member Member of: the attest outcome Role: Outcome Projection: invalid-attest-credential

Attest Failed

The composition’s own rejection from Attest As Actor, positioned. attestation: the mapping of Actor Identity.attest’s storage-failure and state-unavailable (Action wiring 40, Action wiring 44) — nothing was recorded, the whole action may be retried. log: the attest_log append failed, so nothing the call wrote commits, an attestation Actor Identity’s attest wrote in the same transaction included (Execution Contract Database 1) — nothing was recorded, the whole action may be retried.

Kind: Member Member of: the attest rejection Role: Rejection Projection: attest-failed

Outcome

The attest-log entry’s classification of the Attest As Actor call it records, by the call’s answer: success for an attestation id, or the outcome answered — Not Bound, Credential Not Active, registry-unavailable, mechanism-unavailable or Invalid Attest Credential (Composition state 13). A refused call, invalid-request or Attest Failed, appends no entry (Execution Contract Read 4); the log is the composition’s provable audit surface.

Kind: Field Field of: the attest-log entry Role: the attempt classification Projection: outcome

Observed Status

The credential status the attest gate observed when it closed — the effective status (Credential Operation 52) of the credential Credential’s read answers last for the (principal_ref, credential_type) pair (Revoked Expired Rotated), or none where the read answers no credential for the pair (Action wiring 34, Action wiring 46), the absence of any effective-active credential being what closed the gate. Carried inside the Credential Not Active outcome for post-hoc forensics.

Kind: Field Field of: the attest-log entry Role: the gate-closing credential status Projection: observed_status


Standards references

Authenticated Actor is the structural form of the requirement that authentication and non-repudiable attestation be bound under one principal, with revocation of the former closing the latter. Its primary anchors:

  • NIST (National Institute of Standards and Technology — US federal standards body) SP 800-63B section 5.2 (Authenticator Lifecycle — Binding, Revocation, and Reauthentication) — the requirement that a revoked authenticator can no longer be used to establish authority. The revocation cascade (Invariant 1) is the structural form: a revoked authentication credential closes the actor’s attestation surface, so authority to sign flows from a currently-valid authenticator.
  • NIST SP 800-57 Part 1 (Recommendation for Key Management — General) — key-usage separation: a key used for one purpose (authentication) should not serve another (signing/attestation). Secret-surface separation (Invariant 2) is the composition-level expression of the key-separation principle.
  • PCI DSS (Payment Card Industry Data Security Standard — the card networks’ mandatory security rules for cardholder data) Requirement 8.6 (management of authentication factors and their binding to individual accounts) — authentication factors must be bound to a specific identity and managed through their lifecycle; the namespace binding (Invariant 3) and the revocation cascade (Invariant 1) are the structural mechanisms for the bind-and-revoke lifecycle of a payment-system actor.
  • FIPS 140-3 (Federal Information Processing Standard — Security Requirements for Cryptographic Modules) — the standard for the cryptographic modules that hold and operate signing keys; the distinct-key-surface obligation (Capability requirement 14, externally-clearable) is where a deployment’s FIPS 140-3-validated module provisioning is the cleared evidence that the attestation key is genuinely separate material.

Authenticated Actor inherits the broader standards compliance of its constituents:

  • Through Credential: NIST SP 800-63B (authenticator and verifier requirements — stored verifiers, not raw secrets), FIDO2 / WebAuthn (phishing-resistant authenticator binding), PCI DSS Requirement 8, ISO/IEC 27001 clause A.9.4 (system and application access control), GDPR (EU General Data Protection Regulation) Article 32 (security of processing — the verifier-not-material discipline). The revocation-absorbing and terminal-absorbing invariants the cascade rests on are Credential’s.
  • Through Actor Identity: NIST SP 800-63-3 (identity and authenticator assurance), eIDAS Regulation (EU 910/2014 — qualified electronic signatures), FIPS 186-5 (Digital Signature Standard), 21 CFR (US Code of Federal Regulations) Part 11 (FDA electronic records and signatures — uniquely attributable, repudiation-resistant signatures), DEA EPCS (US Drug Enforcement Administration — Electronic Prescriptions for Controlled Substances; 21 CFR section 1311 — two-factor cryptographic attestation for controlled-substance prescriptions), HIPAA (US Health Insurance Portability and Accountability Act) section 164.312(d) (person or entity authentication), SOX (Sarbanes-Oxley Act) section 302/section 404 (officer certifications and internal-control evidence). The non-repudiation contract the cascade preserves forward is Actor Identity’s.

Status

grounded on Final Critique 10 — 2026-11-06 at 368ce1f — see the Ledger.

Ledger

status: grounded on Final Critique 10 — 2026-11-06 at 368ce1f
formal: verified — authenticated-actor.tla + 4 twins + 6 probes, 2026-10-27
last gate: 2026-11-06 — Final Critique 10, a delta round, frozen at 368ce1f — foundational count 0, clean, one sample; 2026-11-05 — Final Critique 9, a delta round, frozen at ec26ba5 — foundational count 1, cured, not clean, no sample; 2026-11-04 — Final Critique 8 — foundational count 4, not clean, no sample

open:
- 2026-11-04-a · refining · Non-goal 15 · a purge a composed Retention Window makes of an attest log entry, a binding or an earlier version of a credential is described by no rule here, so the bijection, Check 3.1 and Check 2.2's version history have no stated answer for what a purge leaves → state what a purge of each record does to the checks, once a Retention Window composed with this pattern is read

Decisions

Directional changes only — the turns a future reader must know the pattern took, and why. Everything smaller lives in the commit that made it: git log -- compositions/authenticated-actor.md; the migration, the council read’s collapse, the family placement and the regeneration that got it here are in its history.

  • 2026-08-30 — The gate runs under the composition’s own critical section and names its residue; the orphan re-enters instead of dying; every exported code carries its position. Chose: principal_section declared as an instance capability requirement with lease semantics, under which the status read and the attestation write run, with an externally-issued Credential.revoke stated as not serialized and the one-attestation residue it can produce declared, bounded by attest_completion_bound, and made findable by a credential id on every attest_log entry; a composition-introduced storage-level uniqueness constraint on both binding maps re-checked at step 4; a re-entry arm on duplicate-active-credential that binds the existing effective-Active credential only after Credential.verify proves the presenter holds it (invalid-credential(existing) otherwise), so a re-invocation after a binding-position failure reaches the step that failed without becoming a way to claim another principal’s credential; orphan-credential(credential_id) for the post-commit guard re-run; the lease measured from the critical section take as one interval with each completion bound; check 2 sizing the residue on the attestation’s attested_at against revoked_at within clock_offset_allowance + attest_completion_bound; a report-only orphaned-credential leg on reconciliation_cadence and at restart, filtered by unbound credential id and gating pair, bounded below by registration_completion_bound, declared horizon-less, promising no closure window, and carried as check 6; storage-failure(credential | binding), namespace-conflict(guard | binding), and attest-failed(attestation | log(attestation_id)) on the signatures; clock offset allowance on every cross-seam comparison, with check 2 reporting candidates inside the window. Over: a “record lock Credential.revoke must acquire” attributed to Credential Invariant 2, which declares a uniqueness constraint and no lock; a re-entry arm that adopted an existing credential on the presenter’s say-so; a namespace guard offered as a serialization; an orphan “surfaced as a finding” by no leg and repaired by no action; a bare token on both sides of the credential commit and no arm at all after the attestation commit; a breach example that ordered two seams’ stamps as if they were one clock. Because: an invariant is only as sound as the capability it rests on, and a lock nobody declared is ambient authority; a re-invocation that dies at duplicate-active-credential cannot repair the failure it was retried for; a caller who cannot tell credential from binding registers twice; a binding nobody proved possession for is an authority-bearing transition resting on an unauthenticated principal; and a stamp from another seam narrows a decision, never makes one (the frozen rules of 2026-08-30 — Capability provenance, A composition’s own rejection arm carries the retry bit, A stamp from another seam never decides a write alone, A compensator is exclusive — with A reconciliation is bounded at both ends and Recovery commits under a declared service identity, frozen 2026-08-29, and the section titled Authentication precedence in pressure-testing.md, frozen 2026-08-27).

  • 2026-10-20 — The store’s guarantees cited, not restated, the per-principal critical section and its declared residue among them. Chose: the store supplied under Execution Contract Store 1 through 4 (Capability requirement 12), and the forty rules that restated it, or existed only for a store that could lose or split a write, tombstoned to their owner — to Store 1, under which a registration’s credential and binding commit together and an attestation commits with its attest log entry: the maps’ one transaction and the bar on wrapping the credential write and the binding write in one (Composition state 3, Non-goal 14), the report-only orphaned-credential leg with its cadence, its check and the note obliging a deployment to act on its report (Housekeeping 1 through 7, the first with Store 3; Capability requirement 9, Check 6.1, Composition note 6), and the check finding every attestation older than the attest completion bound carrying its entry (Check 4.1); to Store 1 and Store 2, the two completion bounds and the refusal to start without them (Capability requirement 7, 8, 11); and to Store 2, under which an action’s guard reads and the writes they decide are one transaction: the host’s critical section keyed by principal reference, with its supply, release, lease and holding rules and its external check (Capability requirement 3 through 6, Action wiring 1, 16, Wiring decision 2, 3, Concurrency 1, External check 2), the binding write’s uniqueness refusal and the lapsed section’s re-take with its re-run guard’s landings (Action wiring 10, 12, 13, 33, 36, 37), the gate read preceding the attestation write inside the held section (Invariant 1.2, with Action wiring 19), and the declared revoke residue with its bound, its check, the routes a deployment had to close it and the gate read after a revoke (Concurrency 2 through 6, Check 2.3, Composition note 5); with them Register Authenticated Actor’s signature loses orphan-credential and the conflict position its binding value, a failed success entry answers attest-failed naming the log without a committed attestation’s id (Action wiring 25), and Check 2.2 reads a violation beyond the clock offset allowance alone; rules 146 to 107. Over: a host-supplied critical section with lease semantics under which the gate read and the attestation write ran, a declared one-attestation residue for a revoke landing inside it, and a credential committed apart from its binding, with positioned arms and a report-only leg for the orphan — the turn of 2026-08-30, above. Because: the maintainer ruled 2026-10-12 that the corpus takes a store’s specification, never the store, and 2026-10-20 that Store 1 binds every store write of one composition action, its constituents’ included: Credential’s records, the binding maps, Actor Identity’s attestations and the attest log are one store, so a registration’s credential and binding commit together or not at all, and an attestation commits with its entry. Store 2 reads the state an action’s guards decide on inside the transaction that writes the action’s effects, so the gate’s read of the gating credential is in the attesting transaction and a revoke of that credential commits before the read or after the attestation, as the maintainer ruled 2026-10-20 for a guard decided across a lease check whose grant lives in the one store; the composition still never calls Credential’s revoke (Composes 7). The other calls a rule decided: the rewrite’s rule that machinery existing only because a store could lose, split, edit or forget a write goes takes the orphaned-credential leg, which the page gave the split’s orphan alone (Non-goal 14), though its pair filter would also have reported a credential registered for the pair outside the composition, the kind Action wiring 5 through 7 adopt; the same rule keeps Action wiring 11, a storage failure’s only landing and no machinery, now with nothing committed; Action wiring 9 stays as the only rule obliging the binding write, the register’s commit being its nested Step 3 inside the registration’s one transaction (pipelines nest whole: the section titled Substrate composition invocation in execution-contract.md); and Check 5.1 rests on the auditor’s own reads rather than on an entry’s earlier versions, so Store 5 is not cited. What the composition does for its domain is otherwise unchanged.

  • 2026-10-31 — An attempt the gate turns away is answered, not refused, so the attest log keeps it. Chose: Attest As Actor answering not-bound, credential-not-active, registry-unavailable and invalid-attest-credential beside the attestation id, and refusing only invalid-request and attest-failed, so each of those four calls is admitted and its attest log entry is its own committed write: the append moved out of the Invariant family into Action wiring 45 (Invariant 4.1 deleted to it), Actor Identity’s registry-unavailable landed as the composition’s answer by Action wiring 47 under Execution Contract Constituent failure 2, a pair Credential’s read answers no credential for recorded as the observed status none (Action wiring 46), and a refused call, the boundary predicate’s or Actor Identity’s invalid-request, writing nothing. Over: the four as refusals whose attest log entries the page obliged while Execution Contract Read 4 has a refused call write nothing (open line 2026-10-27-a, opened by Final Critique 5’s settle and re-found by every reader of Final Critiques 6 and 7), and retire, which would have dropped the refused attempts’ entries and the breach investigation’s claim. Because: the ruling of 2026-10-31 16:48Z, recorded under the maintainer’s standing ruling of 2026-10-20 that a refused attempt a page keeps as evidence stays, written in the same transaction as the refusal, answered the 2026-10-26 11:43Z escalation’s (b) for this page: keep, in the form Final Critique 6’s Linus pass wrote. The record of every post-revocation attempt is what the breach investigation reads, and Read 4 holds as written, as Credential’s verify answers failed-verification as an outcome.

NOTE: End of Authenticated Actor.


↑