Project Overview

Aura is a fully peer-to-peer, private communication system that operates without dedicated servers. It uses a web-of-trust architecture to provide discovery, data availability, account recovery, and graceful async protocol evolution.

Threshold signatures are used to abstract keys from devices. The network topology between logical users reflects social relationships, forming encrypted mesh that provides discovery, availability, and recovery. State converges through CRDT journals without central coordination, while session-typed choreographic protocols ensure safe multi-party execution.

How Aura Works

In Aura, all actors are authorities. An authority is an opaque cryptographic actor that may represent a person, a device group, or a shared context. External observers see only public keys and signed operations. This enables unlinkable participation across contexts.

State is append-only facts in journals. Each authority maintains its own journal. Shared contexts have journals written by multiple participants. Facts accumulate through CRDT merge and views are derived by reduction.

Side effects flow through explicit traits. Cryptography, storage, networking, and time are accessed only through effect handlers. This enables deterministic simulation and cross-platform portability.

Multi-party coordination uses session-typed choreographies. A global protocol specifies message flow. Each party's local behavior is projected from the global view.

Authorization passes through a layered guard chain. Before any message leaves, capabilities are verified, flow budgets are charged, and facts are committed atomically.

Aura separates key generation from agreement. Fast paths provide immediate usability while durable shared state is always consensus-finalized.

For the complete architecture, see System Architecture.

Documentation Index

The documents below cover theory, technical components, implementation guidance, and project organization.

1. Foundation

Theoretical Model establishes the formal calculus, algebraic types, and semilattice semantics underlying the system.

System Architecture describes the 8-layer architecture, effect patterns, and choreographic protocol structure.

Privacy and Information Flow Contract specifies consent-based privacy with trust boundaries, flow budgets, and leakage tracking.

Distributed Systems Contract defines safety and liveness guarantees, synchrony assumptions, and adversarial tolerance.

2. Core Systems

Cryptography documents primitives, key derivation, threshold signatures, and VSS schemes.

Identifiers and Boundaries defines the identifier types and their privacy-preserving properties.

Authority and Identity describes opaque authorities, commitment trees, and relational context structure.

Journal specifies fact-based journals, validation rules, and deterministic reduction flows.

Authorization covers capability semantics, Biscuit token integration, and guard chain authorization.

Effect System documents effect traits, handler design, and context propagation.

Runtime describes lifecycle management, guard chain execution, and service composition.

User Flow Harness defines the shared UX contract, authoritative observation rules, and browser freshness model for parity-critical harness flows.

Ownership Model defines the four ownership categories, capability-gated authority, terminality rules, and the workspace crate inventory.

Consensus specifies single-shot agreement for non-monotone operations with witness attestation.

Operation Categories defines A/B/C operation tiers, K1/K2/K3 key generation, and agreement levels.

MPST and Choreography covers multi-party session types and choreographic protocol projection.

Transport and Information Flow specifies guard chain enforcement, secure channels, and flow receipts.

Aura Messaging Protocol (AMP) documents reliable async messaging with acknowledgment and ordering patterns.

Network Anonymity documents anonymous path routing, bootstrap re-entry records, and reply-block semantics.

Rendezvous Architecture covers context-scoped peer discovery and encrypted envelope exchange.

Relational Contexts specifies guardian bindings, recovery grants, and cross-authority journals.

Database Architecture defines the query layer using journals, Biscuit predicates, and CRDT views.

Social Architecture describes the three-tier model of messages, homes, and neighborhoods.

Distributed Maintenance Architecture covers snapshots, garbage collection, and system evolution.

CLI and Terminal User Interface specifies command-line and TUI interfaces for Aura operations.

Test Infrastructure Reference documents test fixtures, mock handlers, and scenario builders.

Simulation Infrastructure Reference covers deterministic simulation with virtual time and fault injection.

Formal Verification Reference describes Quint model checking and Lean theorem proving integration.

3. Developer Guides

Getting Started Guide provides a starting point for developers new to the codebase.

Effects and Handlers Guide covers the algebraic effect system, handler implementation, and platform support.

Choreography Development Guide explains choreographic protocol design, CRDTs, and distributed coordination.

Testing Guide covers test patterns, fixtures, conformance testing, and runtime harness.

User Flow Harness explains the determinism model for shared-flow harness execution, revisioned observation, and trace conformance.

Simulation Guide explains deterministic simulation for debugging and property verification.

Verification Guide documents Quint model checking and Lean proof workflows.

System Internals Guide covers guard chain internals, service patterns, and reactive scheduling.

Distributed Maintenance Guide covers operational concerns including snapshots and system upgrades.

Capability Vocabulary Inventory inventories authorization capability strings and their migration targets.

4. Project Meta

UX Flow Coverage Report tracks harness and scenario coverage for user-visible flows.

Verification Coverage Report tracks formal verification status across Quint specs and Lean proofs.

Project Structure documents the 8-layer crate architecture and dependency relationships.

System Architecture

This document gives an intuitive overview of Aura's architecture, covering core abstractions, information flow and component interactions. Formal definitions live in Theoretical Model. Crate organization are documented in Project Structure.

Overview

Aura distributes identity and trust across devices and social relationships to enable private peer-to-peer communication.

The system is designed to operate without dedicated servers. Discovery, availability, and recovery are provided by the web of trust. Peers relay messages for one another based on social proximity. Without centralized routing, no single party can observe all traffic or deny service.

flowchart TB
    subgraph Authorities
        A1[Authority A]
        A2[Authority B]
    end

    subgraph State
        J1[Journal A]
        J2[Journal B]
        JC[Context Journal]
    end

    subgraph Enforcement
        GC[Guard Chain]
        FB[Flow Budget]
    end

    subgraph Effects
        EF[Effect System]
        TR[Transport]
    end

    A1 --> J1
    A2 --> J2
    A1 & A2 --> JC
    J1 & J2 & JC --> GC
    GC --> FB
    FB --> EF
    EF --> TR

This diagram shows the primary data flow. Authorities own journals that store facts. The guard chain enforces authorization before any transport effect. The effect system provides the abstraction layer for all operations.

Every operation flows through the effect system. Every state change is replicated through journals. Every external action is authorized through guards. These three invariants define the architectural contract.

1. State Model

1.1 Dual semilattice

Aura state consists of two complementary semilattices. Facts form a join-semilattice where information accumulates through the join operation. Capabilities form a meet-semilattice where authority restricts through the meet operation.

#![allow(unused)]
fn main() {
struct Journal {
    facts: FactSet,        // join-semilattice (⊔)
    frontier: CapFrontier, // meet-semilattice (⊓)
}
}

The Journal type keeps these dimensions separate. Facts can only grow. Capabilities can only shrink. This dual monotonicity provides convergence guarantees for replicated state.

Facts represent evidence that accumulates over time. Examples include signed operations, attestations, flow budget charges, and consensus commits. Once a fact is added, it cannot be removed. Garbage collection uses tombstones and reduction rather than deletion.

Capabilities represent authority that restricts over time. First-party capability vocabulary is declared in typed families owned by the crates that define the behavior. The system evaluates Biscuit tokens against policy to derive the current capability frontier. Delegation can only attenuate. No operation can widen capability scope. Token issuance is explicit, and guard snapshots carry evaluated frontiers rather than declared capability families. See Theoretical Model for formal definitions of these lattices.

1.2 Journals and namespaces

The journal is the canonical state mechanism. All durable state is represented as facts in journals. Views are derived by reducing accumulated facts.

Journals are partitioned into namespaces. Authority namespaces store facts owned by a single authority. Context namespaces store facts shared across authorities participating in a relational context. Facts in one namespace cannot reference or affect facts in another namespace. Cross-namespace coordination requires explicit protocols.

Facts are content-addressed immutable records. Each fact includes a type identifier, payload, attestation, and metadata. Facts accumulate through CRDT merge. Duplicate facts are deduplicated by content hash. Conflicting facts are resolved by type-specific merge rules.

Attestations prove that an authority endorsed the fact. Threshold signatures require multiple devices to attest. Single-device signatures are used for local facts. See Journal for the complete specification.

1.3 State reduction

State reduction computes views from accumulated facts. Reducers are pure functions that transform fact sets into derived state. Reduction is deterministic and reproducible.

Reduction runs on demand or is cached for performance. Cached views are invalidated when new facts arrive. The reduction pipeline supports incremental updates for large fact sets. See Journal for the reduction architecture.

1.4 Content addressing

All Aura artifacts are identified by the hash of their DAG-CBOR canonical encoding. Published digests are immutable. Journal merges and payload downloads verify digests before accepting data. See Theoretical Model for the content addressing contract.

2. Identity and Trust

2.1 Authorities

An authority is an opaque cryptographic actor. External parties see only public keys and signed facts. Internal device structure is hidden. This abstraction provides unlinkability across contexts.

flowchart LR
    subgraph External View
        PK[Threshold Public Key]
    end

    subgraph Authority [Internal Structure]
        direction TB
        CT[Commitment Tree]
        subgraph Devices
            direction LR
            D1[Device 1<br/>Share 1]
            D2[Device 2<br/>Share 2]
            D3[Device 3<br/>Share 3]
        end
        CT --> Devices
    end

    Devices -.->|2-of-3 signing| PK

    style Authority fill:transparent,stroke:#888,stroke-dasharray: 5 5

Account authorities maintain device membership using commitment trees. The journal stores signed tree operations as facts. Reduction reconstructs the canonical tree state from accumulated facts. FROST provides the threshold signature scheme. DKG distributes key shares without a trusted dealer. Key rotation and resharing maintain security as devices join or leave. See Cryptography for threshold details.

2.2 Relational contexts

Relational contexts are shared journals for cross-authority state. Each context has its own namespace and does not reveal participants to external observers. Participation is expressed by writing relational facts. Profile data, nicknames, and relationship state live in context journals. See Authority and Identity for commitment tree details and Relational Contexts for context patterns.

2.3 Contextual identity

Identity is scoped to contexts. A device can participate in many contexts without linking them. Each context derives independent keys through deterministic key derivation. This prevents cross-context correlation by external observers. See Identifiers and Boundaries for identifier semantics.

2.4 Social topology

Aura organizes social structure into three tiers. Messages are communication contexts for direct and group conversations. Homes are semi-public communities capped by storage constraints. Neighborhoods are collections of homes connected via 1-hop links.

The social topology shapes routing, relay selection, and governance. Authorities prefer relays operated by trusted peers within their home or neighborhood. Storage allocation is bounded per home, producing natural scarcity that scales with social investment. Local governance is encoded as capability-gated policy facts within each home's journal.

Access levels to a home follow the topology. Full access applies within the home. Partial access applies across 1-hop neighborhood links. Limited access applies at greater distances. See Social Architecture for the complete model.

3. Effects and Time

3.1 Effect system

Effect traits define async capabilities with explicit context. Handlers implement these traits for specific environments. The effect system provides the abstraction layer between application logic and runtime behavior.

flowchart TB
    subgraph L3["Composite"]
        direction LR
        TRE[TreeEffects] ~~~ CHE[ChoreographyExt]
    end

    subgraph L2["Application"]
        direction LR
        JE[JournalEffects] ~~~ AE[AuthorizationEffects] ~~~ FE[FlowBudgetEffects] ~~~ LE[LeakageEffects]
    end

    subgraph L1["Infrastructure"]
        direction LR
        CE[CryptoEffects] ~~~ NE[NetworkEffects] ~~~ SE[StorageEffects] ~~~ TE[TimeEffects] ~~~ RE[RandomEffects]
    end

    L1 --> L2 --> L3

Infrastructure effects wrap OS primitives including cryptography, networking, storage, time, and randomness. Application effects encode domain logic including journal operations, authorization, flow budgets, and leakage tracking. Composite effects combine lower layers for commitment tree operations and choreography execution.

Application code must not call system time, randomness, or IO directly. These operations must flow through effect traits. This constraint enables deterministic testing and simulation. See Effect System for the full specification.

3.2 Time domains

The time system provides four domains for different use cases. PhysicalClock uses wall-clock time for cooldowns, receipts, and liveness. LogicalClock uses vector and Lamport clocks for causal ordering. OrderClock uses opaque tokens for deterministic ordering without temporal leakage. Range uses earliest and latest bounds for validity windows.

Time access happens exclusively through effect traits. Application code does not call system time directly. Cross-domain comparisons require explicit policy. See Effect System for time domain details.

3.3 Context propagation

Every async call chain carries an EffectContext that identifies the authority, context, session, and execution mode. Guards access context to make authorization decisions. Handlers access context to route operations to the correct namespace. See Effect System for the context model.

4. Authorization and Enforcement

4.1 Guard chain

All transport sends pass through a guard chain before any network effect. The chain enforces authorization, budget accounting, journal coupling, and leakage tracking in a fixed sequence:

CapabilityGuard → FlowBudgetGuard → JournalCouplingGuard → LeakageTrackingGuard → TransportEffects

Each guard must succeed before the next executes. Failure at any guard blocks the send. This order enforces the charge-before-send invariant. See Authorization for the full guard chain specification.

4.2 Capability model

Authorization uses Biscuit tokens with cryptographic attenuation. Capabilities can only be restricted, never expanded. Delegation chains are verifiable without contacting the issuer.

CapabilityGuard evaluates Biscuit tokens against required capabilities. It verifies that the sender has authority to perform the requested operation. Biscuit caveats can restrict scope, time, or target. See Authorization for token structure and evaluation.

4.3 Flow budgets and receipts

Flow budgets track message emission per context and peer. Only spent and epoch values are stored as facts. The limit is computed at runtime from capability evaluation through the meet-semilattice. This keeps replicated state minimal while enabling runtime limit computation.

FlowBudgetGuard charges budgets and emits receipts before each send. Budget charges are atomic with receipt generation. If spent + cost > limit, the send is blocked locally with no observable behavior. Epoch rotation resets counters through new epoch facts.

Receipts include context, sender, receiver, epoch, cost, and a hash chain link. The chain provides accountability for multi-hop message forwarding. Relays validate upstream receipts before forwarding and charge their own budgets before emitting. See Transport and Information Flow for receipt verification.

4.4 Context isolation and leakage tracking

Contexts provide information flow boundaries. Keys are derived per-context. Facts are scoped to namespaces. Cross-context flow requires explicit bridge protocols.

LeakageTrackingGuard records privacy budget usage per observer class. Observer classes include relationship, group, neighbor, and external. Operations that exceed leakage budgets are blocked. See Privacy and Information Flow Contract for the leakage model.

5. Protocols

5.1 Choreographic protocols

Choreographies define global protocols using multi-party session types. A global type describes the entire protocol from an overview perspective. Each message specifies sender, receiver, payload type, and guard annotations.

Annotations compile into guard chain requirements: guard_capability is the canonical namespaced capability string admitted at the DSL boundary, flow_cost specifies budget charges, journal_facts specifies facts to commit, and leak specifies leakage budget allocation.

Projection extracts each role's local view from the global type. The local view specifies what messages the role sends and receives. Execution interprets the local view against the effect system. See MPST and Choreography for projection rules and the global type grammar.

5.2 Telltale Protocol Machine

Production choreography execution uses the Telltale protocol machine with a host bridge. Startup is manifest-driven and admitted by construction. Execution is bounded by deterministic step budgets derived from weighted measures of the local session type. The budget removes wall-clock coupling from safety enforcement and keeps bound checks replay-deterministic across native and WASM conformance lanes.

The protocol machine supports canonical, hardening, and parity profiles. The canonical profile runs at concurrency 1 as the reference behavior. Hardening profiles test edge cases. Parity profiles compare native and WASM execution. See MPST and Choreography for runtime details.

5.3 Consensus and agreement

Aura Consensus provides single-shot agreement for non-monotone operations. Monotone operations use CRDT merge without consensus. Non-monotone operations such as key rotation, membership changes, and authoritative state transitions require consensus.

Operations are classified into categories A, B, and C. Category A uses CRDTs with immediate local effect. Category B shows pending state until agreement. Category C blocks until the consensus ceremony completes. See Operation Categories for classification rules.

The fast path completes in one round trip when witnesses agree on prestate. The fallback path activates when witnesses disagree or the initiator stalls. Bounded gossip propagates evidence until a quorum forms. Both paths yield the same CommitFact format.

CommitFact represents a consensus decision. It binds prestate hash, operation hash, participant set, threshold signature, and timestamp. CommitFacts are inserted into the relevant journal namespace. The prestate binding prevents reusing signatures across unrelated operations. Consensus failures fall back to gossip. Network partitions delay but do not corrupt state. See Consensus for protocol details.

5.4 Invitation lifecycle

Invitations establish new relationships. Contact invitations create direct messaging contexts. Channel invitations grant access to home channels. Guardian invitations bind recovery relationships.

Invitation creation is authorization-gated. Only the sender can cancel. Only the receiver can accept or decline. No invitation is resolved twice. Terminal states (accepted, declined, cancelled, expired) are immutable. Accepted invitations are backed by journal facts. Ceremony initiation is gated on acceptance. See Relational Contexts for invitation patterns.

5.5 Recovery

Device recovery uses guardian protocols. Guardians hold encrypted recovery shares established through relational contexts. A threshold of guardians can restore account access by contributing their shares.

Recovery operates through the same consensus and session-type infrastructure as other protocols. The recovered authority retains its identity while rotating to new key material. See Relational Contexts for recovery architecture.

6. Communication

6.1 Secure channels

SecureChannel provides encrypted, authenticated communication between two authorities. Channels use context-scoped keys derived through deterministic key derivation. Channel state is not stored in journals. Channels are established through rendezvous or direct connection. See Rendezvous Architecture for channel establishment.

6.2 Rendezvous

Rendezvous enables authorities to find each other without centralized directories. Rendezvous servers are untrusted relays that cannot read message content. Authorities publish encrypted envelopes that peers can retrieve. The social topology provides routing hints based on home and neighborhood membership. See Rendezvous Architecture for the full protocol.

6.3 Asynchronous messaging

AMP provides patterns for reliable asynchronous messaging. Messages may arrive out of order. Delivery may be delayed by offline peers. AMP handles acknowledgment, retry, and ordering. Channels support both synchronous request-response and asynchronous fire-and-forget patterns. See Aura Messaging Protocol for details.

6.4 Anti-entropy

Journal state converges through anti-entropy after network partitions. Each peer periodically exchanges fact digests with its neighbors, identifies gaps, and selectively transfers missing facts. Because journals are CRDTs, merging facts from any peer is safe regardless of ordering. This process runs continuously in the background without coordination or agreement and ensures that connected peers eventually share the same fact set.

7. Runtime and Ownership

7.1 Ownership model

Aura uses four ownership categories to prevent multiple layers from co-owning the same semantic truth: Pure for reducers and validators, MoveOwned for handle and session transfer, ActorOwned for long-lived mutable runtime state, and Observed for projections and UI reads. Parity-critical mutation must be capability-gated. Parity-critical operations must terminate explicitly with typed success, failure, or cancellation. Errors are classified by recoverability and propagated through Result types. See Ownership Model for the full contract.

7.2 Structured concurrency

Actor-owned state is managed through a hierarchical task supervisor. Each service owns a rooted task group. Child tasks inherit cancellation from parents. Shutdown is hierarchical and parent-driven. All mutation of actor-owned state flows through bounded typed ingress rather than shared mutable access.

Session and endpoint transfer uses move-owned capabilities with monotone generation counters that reject stale access. Delegation atomically transfers the owner record and capability. This separation keeps supervision (who manages the lifecycle) distinct from session ownership (who may act on the state). See Runtime for the structured concurrency model.

7.3 Reactive state

The system uses reactive signals for state propagation. Journal fact changes flow through reducers to signals. Signals expose derived state to UI observers. The flow is unidirectional: facts are the source of truth, views are derived, and subscribers receive the latest state when they poll.

Subscription to an unregistered signal is a typed failure. Lagging subscribers may miss intermediate updates and resume from a newer snapshot. Reactive delivery is a transport for authoritative snapshots, not an alternate owner of semantic truth.

7.4 Workflow ownership

User-facing operations such as sending a message, accepting an invitation, or rotating a key are executed as workflows that progress through typed lifecycle phases to a terminal outcome. Each workflow has one authoritative lifecycle owner. Frontend and harness layers may submit commands and observe results, but they do not publish terminal truth. Ownership transfers through explicit handoff before the workflow begins awaited work. See Ownership Model for the semantic owner protocol.

8. Maintenance and Evolution

8.1 Snapshots and garbage collection

Snapshots bound storage size. A snapshot proposal announces a target epoch and a digest of the journal prefix. Devices verify the digest and contribute threshold signatures to complete the snapshot. Devices then prune facts and blobs whose epochs fall below the snapshot epoch. This pruning does not affect correctness because the snapshot represents a complete prefix.

8.2 OTA upgrades

OTA separates release distribution from activation. Release propagation is multi-directional and eventual. Activation is scope-bound and uses explicit epoch fences. Soft forks preserve compatibility. Hard forks require threshold-signed activation ceremonies scoped to the affected authority or context. See Distributed Maintenance Architecture for the full upgrade model.

8.3 Epoch fencing

Epochs gate budget resets, receipt validity, and upgrade activation. Epoch rotation inserts a new epoch fact into the journal. All replicas treat an epoch change as effective once they observe it in the journal. This avoids hard clock synchronization requirements. Receipts are valid only within their epoch. Old epoch receipts cannot be replayed.

References

• Theoretical Model: formal calculus and semilattice semantics
• Privacy and Information Flow Contract: leakage budgets and privacy layers
• Distributed Systems Contract: safety, liveness, and consistency guarantees
• Cryptography: threshold signatures and key management
• Identifiers and Boundaries: identifier semantics
• Authority and Identity: commitment trees and relational contexts
• Effect System: effect traits and time domains
• Runtime: lifecycle management and service composition
• Journal: fact storage and reduction
• Authorization: guard chain and Biscuit integration
• Consensus: single-shot agreement protocol
• Operation Categories: A/B/C classification
• MPST and Choreography: session types and projection
• Transport and Information Flow: transport semantics
• Aura Messaging Protocol: reliable async messaging
• Rendezvous Architecture: peer discovery and channel establishment
• Relational Contexts: cross-authority state and recovery
• Social Architecture: homes, neighborhoods, and governance
• Distributed Maintenance Architecture: snapshots, GC, and OTA
• Ownership Model: ownership categories and semantic owner protocol
• Project Structure: crate organization and dependency graph

Theoretical Model

This document establishes the complete mathematical foundation for Aura's distributed system architecture. It presents the formal calculus, algebraic/session types, and semilattice semantics that underlie all system components.

Overview

Aura's theoretical foundation rests on four mathematical pillars:

1. Aura Calculus ($\mathcal{A}$) provides the core computational model for communication, state, and trust.
2. Algebraic Types structure state as semilattices with monotonic properties.
3. Multi-Party Session Types specify choreographic protocols with safety guarantees.
4. CRDT Semantics enable conflict-free replication with convergence proofs.

The combination forms a privacy-preserving, spam-resistant, capability-checked distributed λ-calculus that enforces information flow budget across all operations.

Shared Terms and Notation

This section defines shared terminology and notation for core contracts. Use this section when writing Theoretical Model, Privacy and Information Flow Contract, and Distributed Systems Contract.

Core Entities

Access and Topology

Flow Budget and Receipts

Use $‘B[\kappa ,a]‘$ for a flow budget for context $‘\kappa ‘$ and peer authority $‘a‘$.

Observers, Time, and Delay

Leakage tuple order: $‘({\ell }_{\text{rel}},{\ell }_{\text{grp}},{\ell }_{\text{ngh}},{\ell }_{\text{ext}})‘$

Invariant Naming

Use InvariantXxx names for implementation and proof references. If a prose alias exists, include it once, then reference the invariant name.

Guard Chain Order

This order defines ChargeBeforeSend.

1. Aura Calculus ($‘\mathcal{A}‘$)

1.1 Syntax

We define programs as effectful, session-typed processes operating over semilattice-structured state.

Terms:

$$e::=v\mid e_1{e}_2\mid \text{handle}e\text{with}H\mid \text{send}\kappa m\mid \text{recv}\kappa \mid \text{merge}\delta \mid \text{refine}\gamma$$

Facts (Join-Semilattice):

$$(F,\bigsqcup ,\perp )\text{where}x\bigsqcup y=y\bigsqcup x,x\bigsqcup (y\bigsqcup z)=(x\bigsqcup y)\bigsqcup z,x\bigsqcup x=x$$

Capabilities (Meet-Semilattice):

$$(C,\sqcap ,\top )\text{where}x\sqcap y=y\sqcap x,x\sqcap (y\sqcap z)=(x\sqcap y)\sqcap z,x\sqcap x=x$$

Contexts:

$$\kappa \in \text{Ctx}=\{\text{ContextId}\}$$

Contexts are opaque UUIDs representing authority journals or relational contexts. Keys for transport sessions and DKD outputs are scoped to these identifiers. The identifier itself never leaks participants. See Identifiers and Boundaries for canonical definitions.

Messages:

$$m::=⟨\kappa ,T,\sigma ,\beta ⟩\text{// context, typed payload, signature/auth tag, optional Biscuit token}$$

Message extraction functions (used by operational rules):

$$\text{facts}(m):\text{Fact}\text{// join-contribution carried by message payload}$$

$$\text{token}(m):\text{Biscuit}\text{// attenuated capability presented alongside the message}$$

A process configuration:

$$⟨P,F,C,\kappa ⟩$$

This represents a running session with fact-state $‘F‘$, capability frontier $‘C‘$ derived from verified Biscuit tokens and local policy, and privacy context $‘\kappa ‘$.

1.2 Judgments

$$\Gamma ⊢e:T\mid ϵ$$

Under typing context $‘\Gamma ‘$, expression $‘e‘$ has type $‘T‘$ and may perform effects $‘ϵ‘$.

Effect set:

$$ϵ::=\varnothing \mid ϵ\cup \{\text{Merge}\Delta F\}\mid ϵ\cup \{\text{Refine}\Delta C\}\mid ϵ\cup \{\text{Send}\kappa m\}\mid ϵ\cup \{\text{Recv}\kappa \}$$

1.3 Operational Semantics

State evolution:

$$(Merge)⟨\text{merge}\delta ,F,C,\kappa ⟩\to ⟨\text{unit},F\bigsqcup \delta ,C,\kappa ⟩$$

$$(Refine)⟨\text{refine}\gamma ,F,C,\kappa ⟩\to ⟨\text{unit},F,C\sqcap \gamma ,\kappa ⟩$$

Capability-guarded actions:

Each side effect or message action $‘a‘$ carries a required capability predicate $‘\text{need}(a)‘$.

$$(Send)\text{if}\text{need}(m)\le C\wedge \text{headroom}(\kappa ,\text{cost},F,C)\text{then}⟨\text{send}\kappa m,F,C,\kappa ⟩\to ⟨\text{unit},F,C,\kappa ⟩$$

$$\text{else block}$$

$$(Recv)⟨\text{recv}\kappa ,F,C,\kappa ⟩\to ⟨m,F\bigsqcup \text{facts}(m),C\sqcap \text{attn}(\text{token}(m)),\kappa ⟩$$

The function attn applies the Biscuit token's caveats to the local frontier. Biscuit attenuation never widens authority. The operation remains meet-monotone even though the token data lives outside the journal.

Context isolation:

No reduction may combine messages of distinct contexts:

$$\text{if}{\kappa }_1\ne {\kappa }_2\text{then}\text{send}{\kappa }_{1}m\parallel \text{recv}{\kappa }_2\equiv \text{blocked}$$

Here $‘\text{headroom}(\kappa ,\text{cost},F,C)‘$ is shorthand for the budget predicate derived from journal facts and Biscuit-imposed limits for context $‘\kappa ‘$:

$$\text{headroom}(\kappa ,\text{cost},F,C)\triangleq {\text{spent}}_{\kappa }(F)+\text{cost}\le {\text{limit}}_{\kappa }(\text{policy}\sqcap C)$$

Implementations realize this by merging a FlowBudget charge fact before send (see §2.3 and §5.3) while evaluating Biscuit caveats inside the guard chain. The side condition is enforced by the same monotone laws as other effects even though capability data itself is not stored in the CRDT.

1.4 Algebraic Laws (Invariants)

1. Monotonic Growth: $‘F_{t+1}=F_t\bigsqcup \delta ⟹F_t\le F_{t+1}‘$
2. Monotonic Restriction: $‘C_{t+1}=C_t\sqcap \gamma ⟹C_{t+1}\le C_t‘$
3. Safety: Every side effect $‘\sigma ‘$ requires $‘\text{need}(\sigma )\le C‘$.
4. Context Separation: For any two contexts $‘{\kappa }_1,{\kappa }_2‘$, no observable trace relates their internal state unless a bridge protocol is typed for $‘({\kappa }_1,{\kappa }_2)‘$.
5. Compositional Confluence: $‘(\text{merge}{\delta }_1;\text{merge}{\delta }_2)\equiv \text{merge}({\delta }_1\bigsqcup {\delta }_2)‘$ and $‘(\text{refine}{\gamma }_1;\text{refine}{\gamma }_2)\equiv \text{refine}({\gamma }_1\sqcap {\gamma }_2)‘$

2. Core Algebraic Types

2.1 Foundation Objects

#![allow(unused)]
fn main() {
// Capabilities describe Biscuit caveats. They form a meet-semilattice but are evaluated outside the CRDT.
type Cap        // partially ordered set (≤), with meet ⊓ and top ⊤
type Policy     // same carrier as Cap, representing sovereign policy

// Facts are join-semilattice elements (accumulation only grows them).
type Fact       // partially ordered set (≤), with join ⊔ and bottom ⊥

// Journal state is only a Cv/Δ/CmRDT over facts.
struct Journal {
  facts: Fact,            // Cv/Δ/CmRDT carrier with ⊔
}

// Context identifiers are opaque (authority namespace or relational context).
struct ContextId(Uuid);
struct Epoch(u64);  // monotone, context-scoped
struct FlowBudget { limit: u64, spent: u64, epoch: Epoch };
struct Receipt { ctx: ContextId, src: AuthorityId, dst: AuthorityId, epoch: Epoch, cost: u32, nonce: u64, prev_hash: Hash32, sig: Signature };

// Typed messages carry effects and proofs under a context.
struct Msg<Ctx, Payload, Version> {
  ctx: Ctx,                 // ContextId chosen by relationship
  payload: Payload,         // typed by protocol role/state
  ver: Version,             // semantic version nego
  auth: AuthTag,            // signatures/MACs/AEAD tags
  biscuit: Option<Biscuit>, // optional attenuated capability
}
}

These type definitions establish the foundation for Aura's formal model. The Cap and Policy types form meet-semilattices for capability evaluation. The Fact type forms a join-semilattice for accumulating evidence. The Journal contains only facts and inherits join-semilattice properties. Messages are typed and scoped to contexts to ensure isolation.

The type Cap represents the evaluation lattice used by Biscuit. Refinement operations (caveats, delegation) can only reduce authority through the meet operation.

The type Fact represents facts as join-semilattice elements. Accumulation operations can only add information through the join operation.

Journals replicate only facts. Capability evaluations run locally by interpreting Biscuit tokens plus policy. This keeps authorization independent of the replicated CRDT while preserving the same meet monotonicity at runtime.

Contexts (ContextId) define privacy partitions. Messages never cross partition boundaries without explicit protocol support. See Identifiers and Boundaries for precise identifier semantics and Relational Contexts for implementation patterns.

2.2 Content Addressing Contract

All Aura artifacts are identified by the hash of their canonical encoding. This includes facts, snapshot blobs, cache metadata, and upgrade manifests.

Structures are serialized using canonical CBOR with sorted maps and deterministic integer width. The helper function hash_canonical(bytes) computes digests when needed.

Once a digest is published, the bytes for that artifact cannot change. New content requires a new digest and a new fact in the journal.

Snapshots and upgrade bundles stored outside the journal are referenced solely by their digest. Downloaders verify the digest before accepting the payload. Journal merges compare digests and reject mismatches before updating state. See Distributed Maintenance Architecture for the complete fact-to-state pipeline.

2.3 Effect Signatures

Core effect families provide the runtime contract:

-- Read/append mergeable state
class JournalEffects (m : Type → Type) where
  read_facts  : m Fact
  merge_facts : Fact → m Unit

-- Biscuit verification + guard evaluation
class AuthorizationEffects (m : Type → Type) where
  evaluate_guard : Biscuit → CapabilityPredicate → m Cap
  derive_cap     : ContextId → m Cap  -- cached policy frontier

-- Cryptography and key mgmt (abstracted to swap FROST, AEAD, DR, etc.)
class CryptoEffects (m : Type → Type) where
  sign_threshold  : Bytes → m SigWitness
  aead_seal       : K_box → Plain → m Cipher
  aead_open       : K_box → Cipher → m (Option Plain)
  commitment_step : ContextId → m ContextId

-- Transport (unified)
class TransportEffects (m : Type → Type) where
  send    : PeerId → Msg Ctx P V → m Unit
  recv    : m (Msg Ctx Any V)
  connect : PeerId → m Channel

These effect signatures define the interface between protocols and the runtime. The JournalEffects family handles state operations. The AuthorizationEffects family verifies Biscuit tokens and fuses them with local policy. The CryptoEffects family handles cryptographic operations. The TransportEffects family handles network communication.

2.4 Guards and Observability Invariants

Every observable side effect is mediated by a guard chain fully described in Authorization:

1. CapGuard: $‘\text{need}(\sigma )\le \text{Caps}(\text{ctx})‘$
2. FlowGuard: headroom(ctx, cost) where charge(ctx, peer, cost, epoch) succeeds and yields a Receipt
3. JournalCoupler: commit of attested facts is atomic with the send

Named invariants used across documents:

• Charge-Before-Send: FlowGuard must succeed before any transport send.
• No-Observable-Without-Charge: there is no $‘\text{send}(\text{ctx},\text{peer},\dots )‘$ event without a preceding successful $‘\text{charge}(\text{ctx},\text{peer},\text{cost},\text{epoch})‘$.
• Deterministic-Replenishment: limit(ctx) is computed deterministically from capability evaluation. The value spent (stored as journal facts) is join-monotone. Epochs gate resets.

-- Time & randomness for simulation/proofs
class TimeEffects (m : Type → Type) where
  now   : m Instant
  sleep : Duration → m Unit

class RandEffects (m : Type → Type) where
  sample : Dist → m Val

-- Privacy budgets (relationship, group, neighbor, external observers)
class LeakageEffects (m : Type → Type) where
  record_leakage   : ObserverClass → Number → m Unit
  remaining_budget : ObserverClass → m Number

The TimeEffects and RandEffects families support simulation and testing. The LeakageEffects family enforces privacy budget constraints.

The LeakageEffects implementation is the runtime hook that enforces the $‘[\text{leak}:({\ell }_{\text{rel}},{\ell }_{\text{grp}},{\ell }_{\text{ngh}},{\ell }_{\text{ext}})]‘$ annotations introduced in the session grammar. The system wires it through the effect system so choreographies cannot exceed configured budgets.

Information Flow Budgets (Spam + Privacy)

Each context and peer authority pair $‘(\kappa ,a)‘$ carries a flow budget to couple spam resistance with privacy guarantees. This pair is written as $‘B[\kappa ,a]‘$. Keys and receipts are authority-scoped. Devices are internal to an authority and never appear in flow-budget state.

#![allow(unused)]
fn main() {
struct FlowBudget {
    spent: u64,   // monotone counter (join = max)
    limit: u64,   // capability-style guard (meet = min)
}

// Logical key: (ContextId, AuthorityId) -> FlowBudget
// Receipts: (ctx, src_authority, dst_authority, epoch, cost, nonce)
}

The FlowBudget struct tracks message emission through two components:

• The spent field is stored in the journal as facts and increases through join operations
• The limit field is derived from capability evaluation (Biscuit tokens + local policy) and decreases through meet operations

Only spent counters live in the journal as facts, inheriting join-semilattice properties. The limit is computed at runtime by evaluating Biscuit tokens and local policy through the capability meet-semilattice, consistent with the principle that capabilities are evaluated outside the CRDT.

Sending a message deducts a fixed flow_cost from the local budget before the effect executes. If $‘\text{spent}+\text{flow\_cost}>\text{limit}‘$, the effect runtime blocks the send.

Budget charge facts (incrementing spent) are emitted to the journal during send operations. The limit value is deterministically computed from the current capability frontier, ensuring all replicas with the same tokens and policy derive the same limit. Receipts bind to AuthorityId for both src/dst and use nonce chains per (ctx, src, epoch) to maintain charge-before-send proofs without leaking device structure.

Multi-hop forwarding charges budgets hop-by-hop. Relays attach a signed Receipt that proves the previous hop still had headroom. Receipts are scoped to the same context so they never leak to unrelated observers.

2.5 Semantic Laws

Join laws apply to facts. These operations are associative, commutative, and idempotent. If $‘F_0=\text{read\_facts}()‘$ and after $‘\text{merge\_facts}(f)‘$ we have $‘F_1‘$, then $‘F_0\le F_1‘$ with respect to the facts partial order.

Meet laws apply to capabilities. These operations are associative, commutative, and idempotent. Applying Biscuit caveats corresponds to multiplying by $‘c‘$ under $‘\sqcap ‘$ and never increases authority.

Cap-guarded effects enforce non-interference. For any effect $‘e‘$ guarded by capability predicate $‘\Gamma ⊢e:\text{allowed}‘$, executing $‘e‘$ from $‘\text{caps}=C‘$ is only permitted if $‘C\sqcap \text{need}(e)=\text{need}(e)‘$.

Context isolation prevents cross-context flow. If two contexts $‘{\text{Ctx}}_1\ne {\text{Ctx}}_2‘$ are not explicitly bridged by a typed protocol, no $‘\text{Msg}⟨{\text{Ctx}}_1,\dots ⟩‘$ flows into $‘{\text{Ctx}}_2‘$.

3. Multi-Party Session Type Algebra

3.1 Global Type Grammar (G)

The global choreography type describes the entire protocol from a bird's-eye view. Aura extends vanilla MPST with capability guards, journal coupling, and leakage budgets:

$$G::=r_1\to r_2:T[\text{guard}:\Gamma ,▹\Delta ,\text{leak}:L].G\text{(Point-to-point send)}$$

$$\mid r\to \ast :T[\text{guard}:\Gamma ,▹\Delta ,\text{leak}:L].G\text{(Broadcast)}$$

$$\mid G\parallel G\text{(Parallel composition)}$$

$$\mid r▹\{{\ell }_i:G_i{\}}_{i\in I}\text{(Choice)}$$

$$\mid \mu X.G\text{(Recursion)}$$

$$\mid X\text{(Recursion variable)}$$

$$\mid \text{end}\text{(Termination)}$$

$$T::=\text{Unit}\mid \text{Bool}\mid \text{Int}\mid \text{String}\mid \dots \text{(Message types)}$$

$$r::=\text{Role identifiers (Alice, Bob, }\dots \text{)}$$

$$\ell ::=\text{Label identifiers (accept, reject, }\dots \text{)}$$

$$\Gamma ::=\text{meet-closed predicate}\text{need}(m)\le {\text{caps}}_r(\text{ctx})$$

$$\Delta ::=\text{journal delta (facts) merged around the message}$$

$$L::=\text{leakage tuple}({\ell }_{\text{rel}},{\ell }_{\text{grp}},{\ell }_{\text{ngh}},{\ell }_{\text{ext}})$$

Conventions:

• $‘r_1\to r_2:T[\text{guard}:\Gamma ,▹\Delta ,\text{leak}:L].G‘$ means "role $‘r_1‘$ checks $‘\Gamma ‘$, applies $‘\Delta ‘$, records leakage $‘L‘$, sends $‘T‘$ to $‘r_2‘$, then continues with $‘G‘$."
• $‘r\to \ast :\dots ‘$ performs the same sequence for broadcasts.
• $‘G_1\parallel G_2‘$ means "execute $‘G_1‘$ and $‘G_2‘$ concurrently."
• $‘r▹\{{\ell }_i:G_i\}‘$ means "role $‘r‘$ decides which branch $‘{\ell }_i‘$ to take, affecting all participants."
• $‘\mu X.G‘$ binds recursion variable $‘X‘$ in $‘G‘$.

Note on $‘\Delta ‘$: the journal delta may include budget-charge updates (incrementing spent for the active epoch) and receipt acknowledgments. Projection ensures these updates occur before any transport effect so "no observable without charge" holds operationally.

Note on $‘\Gamma ‘$: check_caps and refine_caps are implemented via AuthorizationEffects. Sends verify Biscuit chains (with optional cached evaluations) before touching transport. Receives cache new tokens by refining the local capability frontier. Neither operation mutates the journal. All capability semantics stay outside the CRDT.

3.2 Local Type Grammar (L)

After projection, each role executes a local session type (binary protocol) augmented with effect sequencing:

$$L::=\text{do}E.L\text{(Perform effect)}$$

$$\mid !T.L\text{(Send)}$$

$$\mid ?T.L\text{(Receive)}$$

$$\mid \oplus \{{\ell }_i:L_i{\}}_{i\in I}\text{(Internal choice)}$$

$$\mid \&\{{\ell }_i:L_i{\}}_{i\in I}\text{(External choice)}$$

$$\mid \mu X.L\text{(Recursion)}$$

$$\mid X\text{(Recursion variable)}$$

$$\mid \text{end}\text{(Termination)}$$

$$E::=\text{merge}(\Delta )\mid \text{check\_caps}(\Gamma )\mid \text{refine\_caps}(\Gamma )\mid \text{record\_leak}(L)\mid \text{noop}$$

3.3 Projection Function ($‘\pi ‘$)

The projection function $‘{\pi }_r(G)‘$ extracts role $‘r‘$'s local view from global choreography $‘G‘$:

By convention, an annotation $‘▹\Delta ‘$ at a global step induces per-side deltas $‘{\Delta }_{\text{send}}‘$ and $‘{\Delta }_{\text{recv}}‘$. Unless otherwise specified by a protocol, we take $‘{\Delta }_{\text{send}}={\Delta }_{\text{recv}}=\Delta ‘$ (symmetric journal updates applied at both endpoints).

Point-to-point projection:

• If $‘r=r_1‘$ (sender): $‘{\pi }_r(r_1\to r_2:T[\dots ])=\text{do merge}({\Delta }_{\text{send}});\text{do check\_caps}(\Gamma );\text{do record\_leak}(L);!T.{\pi }_r(G)‘$
• If $‘r=r_2‘$ (receiver): $‘{\pi }_r(r_1\to r_2:T[\dots ])=\text{do merge}({\Delta }_{\text{recv}});\text{do refine\_caps}(\Gamma );\text{do record\_leak}(L);?T.{\pi }_r(G)‘$
• Otherwise: $‘{\pi }_r(r_1\to r_2:T[\dots ])={\pi }_r(G)‘$

Broadcast projection:

• If $‘r=s‘$ (sender): $‘{\pi }_r(s\to \ast :T[\dots ])=\text{do merge}({\Delta }_{\text{send}});\text{do check\_caps}(\Gamma );\text{do record\_leak}(L);!T.{\pi }_r(G)‘$
• Otherwise (receiver): $‘{\pi }_r(s\to \ast :T[\dots ])=\text{do merge}({\Delta }_{\text{recv}});\text{do refine\_caps}(\Gamma );\text{do record\_leak}(L);?T.{\pi }_r(G)‘$

Parallel composition:

$${\pi }_r(G_1\parallel G_2)={\pi }_r(G_1)\odot {\pi }_r(G_2)$$

where $‘\odot ‘$ is the merge operator (sequential interleaving if no conflicts)

Choice projection:

• If $‘r=r^{\prime }‘$ (decider): $‘{\pi }_r(r^{\prime }▹\{{\ell }_i:G_i\})=\oplus \{{\ell }_i:{\pi }_r(G_i)\}‘$
• If $‘r\ne r^{\prime }‘$ (observer): $‘{\pi }_r(r^{\prime }▹\{{\ell }_i:G_i\})=\&\{{\ell }_i:{\pi }_r(G_i)\}‘$

Recursion projection:

• If $‘{\pi }_r(G)\ne \text{end}‘$: $‘{\pi }_r(\mu X.G)=\mu X.{\pi }_r(G)‘$
• If $‘{\pi }_r(G)=\text{end}‘$: $‘{\pi }_r(\mu X.G)=\text{end}‘$

Base cases:

$${\pi }_r(X)=X$$

$${\pi }_r(\text{end})=\text{end}$$

3.4 Duality and Safety

For binary session types, duality ensures complementary behavior:

$$\text{dual}(!T.L)=?T.\text{dual}(L)$$

$$\text{dual}(?T.L)=!T.\text{dual}(L)$$

$$\text{dual}(\oplus \{{\ell }_i:L_i\})=\&\{{\ell }_i:\text{dual}(L_i)\}$$

$$\text{dual}(\&\{{\ell }_i:L_i\})=\oplus \{{\ell }_i:\text{dual}(L_i)\}$$

$$\text{dual}(\mu X.L)=\mu X.\text{dual}(L)$$

$$\text{dual}(X)=X$$

$$\text{dual}(\text{end})=\text{end}$$

Property: If Alice's local type is $‘L‘$, then Bob's local type is $‘\text{dual}(L)‘$ for their communication to be type-safe.

3.5 Session Type Safety Guarantees

The projection process ensures:

1. Deadlock Freedom: No circular dependencies in communication
2. Type Safety: Messages have correct types at send/receive
3. Communication Safety: Every send matches a receive
4. Progress: Protocols always advance (no livelocks)
5. Agreement: All participants agree on the chosen branch and protocol state (modulo permitted interleavings of independent actions)

3.6 Turing Completeness vs Safety Restrictions

The MPST algebra is Turing complete when recursion ($\text{Rec}/\text{Var}$) is unrestricted. However, well-typed programs intentionally restrict expressivity to ensure critical safety properties:

• Termination: Protocols that always complete (no infinite loops)
• Deadlock Freedom: No circular waiting on communication
• Progress: Protocols always advance to next state

Telltale-backed session runtimes balance expressivity and safety through guarded recursion constructs.

3.7 Free Algebra View (Choreography as Initial Object)

You can think of the choreography language as a small set of protocol-building moves:

Generators:

• $\text{Send}(r_1,r_2,T,[\text{guard}:\Gamma ,▹\Delta ,\text{leak}:L])$
• $\text{Broadcast}(r,R^{\ast },T,[\text{guard}:\Gamma ,▹\Delta ,\text{leak}:L])$
• $\text{Parallel}(G_1,\dots ,G_n)$
• $\text{Choice}(r,\{{\ell }_i\mapsto G_i{\}}_{i\in I})$
• $\text{Rec}(X,G)$ and $\text{Var}(X)$
• $\text{End}$

Taken together, these moves form a free algebra: the language carries just enough structure to compose protocols, but no extra operational behavior. The effect runtime is the target algebra that gives these moves concrete meaning.

Projection (from a global protocol to each role) followed by interpretation (running it against the effect runtime) yields one canonical way to execute any choreography.

The "free" (initial) property is what keeps this modular. Because the choreographic layer only expresses structure, any effect runtime that respects those composition laws admits exactly one interpretation of a given protocol. This allows swapping or layering handlers without changing choreographies.

The system treats computation and communication symmetrically. A step is the same transform whether it happens locally or across the network. If the sender and receiver are the same role, the projection collapses the step into a local effect call. If they differ, it becomes a message exchange with the same surrounding journal/guard/leak actions. Protocol authors write global transforms, the interpreter decides local versus remote at time of projection.

3.8 Algebraic Effects and the Interpreter

Aura treats protocol execution as interpretation over an algebraic effect interface. After projecting a global choreography to each role, a polymorphic interpreter walks the role's AST and dispatches each operation to AuraEffectSystem via explicit effect handlers. The core actions are exactly the ones defined by the calculus and effect signatures in this document: merge (facts grow by $‘\bigsqcup ‘$), refine (caps shrink by $‘\sqcap ‘$), send/recv (context-scoped communication), and leakage/budget metering. The interpreter enforces the lattice laws and guard predicates while executing these actions in the order dictated by the session type.

Because the interface is algebraic, there is a single semantics regardless of execution strategy. This enables two interchangeable modes:

• Static compilation: choreographies lower to direct effect calls with zero runtime overhead.
• Dynamic interpretation: choreographies execute through the runtime interpreter for flexibility and tooling.

Both preserve the same program structure and checks. The choice becomes an implementation detail. This also captures the computation/communication symmetry. A choreographic step describes a typed transform. If the sender and receiver are the same role, projection collapses the step to a local effect invocation. If they differ, the interpreter performs a network send/receive with the same surrounding merge/check_caps/refine/record_leak sequence. Protocol authors reason about transforms. The interpreter decides locality at projection time.

4. CRDT Semantic Foundations

4.1 CRDT Type System

Aura implements four CRDT variants to handle different consistency requirements.

#![allow(unused)]
fn main() {
// State-based (CvRDT) - Full state synchronization
pub trait JoinSemilattice: Clone { fn join(&self, other: &Self) -> Self; }
pub trait Bottom { fn bottom() -> Self; }
pub trait CvState: JoinSemilattice + Bottom {}

// Delta CRDTs - Incremental state synchronization
pub trait Delta: Clone { fn join_delta(&self, other: &Self) -> Self; }
pub trait DeltaProduce<S> { fn delta_from(old: &S, new: &S) -> Self; }

// Operation-based (CmRDT) - Causal operation broadcast
pub trait CausalOp { type Id: Clone; type Ctx: Clone; fn id(&self) -> Self::Id; fn ctx(&self) -> &Self::Ctx; }
pub trait CmApply<Op> { fn apply(&mut self, op: Op); }
pub trait Dedup<I> { fn seen(&self, id: &I) -> bool; fn mark_seen(&mut self, id: I); }

// Meet-based CRDTs - Constraint propagation
pub trait MeetSemilattice: Clone { fn meet(&self, other: &Self) -> Self; }
pub trait Top { fn top() -> Self; }
pub trait MvState: MeetSemilattice + Top {}
}

The type system enforces mathematical properties. CvState types must satisfy associativity, commutativity, and idempotency for join operations. MvState types satisfy the same laws for meet operations.

4.2 Convergence Proofs

Each CRDT type provides specific convergence guarantees:

CvRDT Convergence: Under eventual message delivery, all replicas converge to the least upper bound of their updates.

Proof sketch: Let states $‘S_1,S_2,\dots ,S_n‘$ be replica states after all updates. The final state is $‘S_1\bigsqcup S_2\bigsqcup \cdots \bigsqcup S_n‘$. By associativity and commutativity of join, this value is unique regardless of message ordering.

Delta-CRDT Convergence: Equivalent to CvRDT but with bandwidth optimization through incremental updates.

CmRDT Convergence: Under causal message delivery and deduplication, all replicas apply the same set of operations.

Proof sketch: Causal delivery ensures operations are applied in a consistent order respecting dependencies. Deduplication prevents double-application. Commutativity ensures that concurrent operations can be applied in any order with the same result.

Meet-CRDT Convergence: All replicas converge to the greatest lower bound of their constraints.

4.3 Authority-Specific Applications

Authority journals use join-semilattice facts for evidence accumulation. Facts include AttestedOp records proving commitment tree operations occurred. Multiple attestations of the same operation join to the same fact.

Relational context journals use both join operations for shared facts and meet operations for consensus constraints. The prestate model ensures all authorities agree on initial conditions before applying operations.

Biscuit capability evaluation uses meet operations outside the CRDT. Token caveats restrict authority through intersection without affecting replicated state.

4.4 Message Schemas for Authority Synchronization

#![allow(unused)]
fn main() {
// Tagged message types for different synchronization patterns
#[derive(Clone)] pub enum SyncMsgKind { FullState, Delta, Op, Constraint }

pub type AuthorityStateMsg = (AuthorityFacts, SyncMsgKind);
pub type ContextStateMsg = (ContextFacts, SyncMsgKind);
pub type FactDelta = (Vec<Fact>, SyncMsgKind);

#[derive(Clone)] pub struct AuthenticatedOp { 
    pub op: TreeOp, 
    pub attestation: ThresholdSig, 
    pub ctx: ContextId 
}

// Anti-entropy protocol support
pub type FactDigest = Vec<Hash32>;
pub type MissingFacts = Vec<Fact>;
}

These message types support different synchronization strategies. Authority namespaces primarily use delta synchronization for efficiency. Relational context namespaces use operation-based synchronization to preserve consensus ordering.

4.5 Authority Synchronization Protocols

Authority Fact Synchronization: Authorities exchange facts using delta-based gossip for efficiency.

$$\text{AuthoritySync}:=\mu X.(A\to B:\text{FactDelta}⟨\Delta ⟩.X)\parallel (B\to A:\text{FactDelta}⟨\Delta ⟩.X)$$

Relational context consensus: Contexts use operation-based synchronization to preserve consensus ordering.

$$\text{ContextSync}:=\mu X.(r\to \ast :\text{AuthenticatedOp}⟨\text{Op},\text{Ctx}⟩.X)$$

Anti-Entropy Recovery: Peers detect missing facts through digest comparison and request specific items.

$$\text{AntiEntropy}:=\text{Alice}\to \text{Bob}:\text{FactDigest}.\text{Bob}\to \text{Alice}:\text{MissingFacts}.\text{end}$$

These protocols ensure eventual consistency across authority boundaries while maintaining context isolation. Facts are scoped to their originating authority or relational context.

4.6 Implementation Verification

Aura provides property verification for CRDT implementations through several mechanisms.

Property-Based Testing: Implementations include QuickCheck properties verifying semilattice laws. Tests generate random sequences of operations and verify associativity, commutativity, and idempotency.

Convergence Testing: Integration tests simulate network partitions and verify that replicas converge after partition healing. Tests measure convergence time and verify final state consistency.

Formal Verification: Critical CRDT implementations include formal proofs using the Quint specification language. Proofs verify that implementation behavior matches mathematical specifications.

Safety Guarantees: Session type projection ensures communication safety and deadlock freedom. Semilattice laws guarantee convergence under eventual message delivery. Meet operations ensure that capability restrictions are monotonic and cannot be bypassed.

5. Information Flow Contract (Privacy + Spam)

5.1 Privacy Layers

For any trace $‘\tau ‘$ of observable messages:

1. Unlinkability: $‘\forall {\kappa }_1\ne {\kappa }_2,\tau [{\kappa }_1\leftrightarrow {\kappa }_2]{\approx }_{\text{ext}}\tau ‘$
2. Non-amplification: Information visible to observer class $‘o‘$ is monotone in authorized capabilities:

$$I_o({\tau }_1)\le I_o({\tau }_2)⟺C_o({\tau }_1)\le C_o({\tau }_2)$$

3. Leakage Bound: For each observer $‘o‘$, $‘L(\tau ,o)\le \text{Budget}(o)‘$.
4. Flow Budget Soundness (Named):
   • Charge-Before-Send
   • No-Observable-Without-Charge
   • Deterministic-Replenishment
   • Convergence: Within a fixed epoch and after convergence, $‘{\text{spent}}_{\kappa }\le {\min }_r{\text{limit}}_{\kappa }^r‘$ across replicas $‘r‘$.

5.2 Web-of-Trust Model

Let $‘W=(V,E)‘$ where vertices are accounts. Edges carry relationship contexts and delegation fragments.

• Each edge $‘(A,B)‘$ defines a pairwise context $‘{\text{Ctx}}_{AB}‘$ with derived keys
• Delegations are meet-closed elements $‘d\in \text{Cap}‘$, scoped to contexts
• The effective capability at $‘A‘$ is:

$${\text{Caps}}_A=({\text{LocalGrants}}_A\sqcap \bigcap _{(A,x)\in E}{\text{Delegation}}_{x\to A})\sqcap {\text{Policy}}_A$$

WoT invariants:

• Compositionality: Combining multiple delegations uses $‘\sqcap ‘$ (never widens)
• Local sovereignty: $‘{\text{Policy}}_A‘$ is always in the meet. $‘A‘$ can only reduce authority further
• Projection: For any protocol projection to $‘A‘$, guard checks refer to $‘{\text{Caps}}_A(\text{ctx})‘$

5.3 Flow Budget Contract

The unified information-flow budget regulates emission rate/volume and observable leakage. The budget system combines join-semilattice facts (for spent counters) with meet-semilattice capability evaluation (for limit computation). For any context $‘\kappa ‘$ and peer $‘p‘$:

1. Charge-Before-Send: A send or forward is permitted only if a budget charge succeeds first. If charging fails, the step blocks locally and emits no network observable.
2. No-Observable-Without-Charge: For any trace $‘\tau ‘$, there is no event labeled $‘\text{send}(\kappa ,p,\dots )‘$ without a preceding successful charge for $‘(\kappa ,p)‘$ in the same epoch.
3. Receipt soundness: A relay accepts a packet only with a valid per-hop Receipt (context-scoped, epoch-bound, signed) and sufficient local headroom. Otherwise it drops locally.
4. Deterministic limit computation: $‘{\text{limit}}_{\kappa }‘$ is computed deterministically from Biscuit tokens and local policy via meet operations. $‘{\text{spent}}_{\kappa }‘$ is stored as journal facts and is join-monotone. Upon epoch rotation, $‘{\text{spent}}_{\kappa }‘$ resets through new epoch facts.
5. Context scope: Budget facts and receipts are scoped to $‘\kappa ‘$. They neither leak nor apply across distinct contexts (non-interference).
6. Composition with caps: A transport effect requires both $‘\text{need}(m)\le C‘$ and $‘\text{headroom}(\kappa ,\text{cost},F,C)‘$ (see §1.3). Either guard failing blocks the effect.
7. Convergence bound: Within a fixed epoch and after convergence, $‘{\text{spent}}_{\kappa }\le {\min }_r{\text{limit}}_{\kappa }^r‘$ across replicas $‘r‘$, where each replica's limit is computed from its local capability evaluation.

6. Application Model

Every distributed protocol $‘G‘$ is defined as a multi-party session type with role projections:

$$G::=\mu X.A\to B:m⟨T⟩[\text{guard}\text{need}(m)\le C_A,\text{update}{F}_A\bigsqcup =\Delta F,\text{refine}{C}_B\sqcap =\Delta C],X$$

When executed, each role $‘\rho ‘$ instantiates a handler:

$$\text{handle protocol}(G,\rho )\text{with}\{\text{on\_send},\text{on\_recv},\text{on\_merge},\text{on\_refine}\}$$

Handlers compose algebraically over $‘(F,C)‘$ by distributing operations over semilattice state transitions. This yields an effect runtime capable of:

• key-ceremony coordination (threshold signatures)
• gossip and rendezvous (context-isolated send/recv)
• distributed indexing (merge facts, meet constraints)
• garbage collection (join-preserving retractions)

7. Interpretation

Under this calculus, we can make the following interpretation:

The Semilattice Layer

The join-semilattice (Facts) captures evidence and observations (trust and information flow). Examples: delegations/attestations, quorum proofs, ceremony transcripts, flow receipts, and monotone spent counters.

The meet-semilattice (Capabilities) captures enforcement limits and constraints (trust and information flow). Examples: the sovereign policy lattice, Biscuit token caveats, leak bounds, and consent gates. See Authorization for implementation details. Flow budget limits are derived from capability evaluation, not stored as facts. This lattice is evaluated locally rather than stored in the journal, but it obeys the same algebra.

Effective authority and headroom are computed from both lattices:

$$C_{\text{eff}}(\text{tokens},\text{Policy})=\left(\underset{t\in \text{tokens}}{\bigwedge }\text{attn}(t)\right)\sqcap \text{Policy}$$

$$\text{headroom}(F,C)\text{ uses }\text{limit}(C_{\text{eff}})\text{ and }\text{spent}\in F,\text{ permitting sends iff }\text{spent}+\text{cost}\le \text{limit}$$

The Session-Typed Process Layer

This layer guarantees communication safety and progress. It projects global types with annotations $‘[\text{guard}:\Gamma ,▹\Delta ,\text{leak}:L]‘$ into local programs, ensuring deadlock freedom, communication safety, branch agreement, and aligning capability checks, journal updates, and leakage accounting with each send/recv.

The Effect Handler Layer

The Effect Handler system provides operational semantics and composability. It realizes merge/refine/send/recv as algebraic effects, enforces lattice monotonicity ($‘\bigsqcup ‘$ facts, $‘\sqcap ‘$ caps), guard predicates, and budget/leakage metering, and composes via explicit dependency injection across crypto, storage, and transport layers.

The Privacy Contract

The privacy contract defines which transitions are observationally equivalent. Under context isolation and budgeted leakage, traces that differ only by in-context reorderings or by merges/refinements preserving observer-class budgets and effective capabilities are indistinguishable. No cross-context flow occurs without a typed bridge.

Together, these form a privacy-preserving, capability-checked distributed λ-calculus.

System Contracts

• Privacy and Information Flow Contract - Unified information-flow budgets, privacy layers, leakage tracking, and adversary analysis
• Distributed Systems Contract - Safety, liveness, consistency guarantees, synchrony assumptions, and failure handling

See Also

• Aura System Architecture - Implementation patterns and runtime layering
• Journal - Fact storage and CRDT semantics
• Authorization - Biscuit evaluation and guard chaining
• Identifiers and Boundaries - Canonical identifier definitions
• Distributed Maintenance Architecture - Reducer pipelines for authorities and contexts

Privacy and Information Flow Contract

This contract specifies Aura's privacy and information-flow model. It defines privacy boundaries, leakage budgets, and required privacy properties. Privacy boundaries align with social relationships rather than technical perimeters.

Violations occur when information crosses trust boundaries without consent. Acceptable flows consume explicitly budgeted headroom.

This document complements Distributed Systems Contract, which covers safety, liveness, and consistency. Together these contracts define the full set of invariants protocol authors must respect.

Verification of these properties uses Quint model checking (verification/quint/) and Lean 4 theorem proofs (verification/lean/). See Verification Coverage Report for current status.

1. Scope

The contract applies to information flows across privacy boundaries:

• Flow budgets: Per-context per-peer spending limits enforced before transport
• Leakage tracking: Metadata exposure accounting by observer class
• Context isolation: Separation of identities and journals across contexts
• Receipt chains: Multi-hop forwarding accountability
• Epoch boundaries: Isolation of budget and receipt state between logical budget epochs (AMP-style generations and windows)
• Service families: Establish, Move, and Hold as the privacy-relevant service surfaces
• Selector retrieval: Capability-derived retrieval without identity-addressed mailbox polling
• Hold custody: Neighborhood-scoped opaque retention with bounded retrieval authority

Related specifications: Authorization, Transport and Information Flow, and Theoretical Model. Shared notation appears in Theoretical Model.

1.1 Terminology Alignment

This contract uses shared terminology from Theoretical Model.

• Home role terms: Member, Participant, Moderator (only members can be moderators)
• Access-level terms: Full, Partial, Limited
• Storage terms: Shared Storage and allocation
• Pinning term: pinned as a fact attribute

1.2 Contract Vocabulary

• observer: any party that can learn information from traffic, custody, or local state exposure
• authoritative: part of replicated truth rather than local runtime interpretation
• retrieval: recovery of an object through bounded authority rather than identity-addressed delivery
• custody: opaque best-effort retention of a non-authoritative object
• accountability evidence: bounded evidence used to verify that a service action occurred

1.3 Assumptions

• Cryptographic primitives are secure at configured key sizes.
• Local runtimes enforce guard-chain ordering before transport sends.
• Epoch updates and budget facts eventually propagate through anti-entropy.
• The service-family model is part of the active privacy contract.
• Privacy-mode deployments use encrypted envelopes and the fixed adaptive policy.
• Debug and simulation modes are excluded from production privacy claims.

1.4 Non-goals

• This contract does not guarantee traffic-analysis resistance against global passive adversaries without encrypted envelopes and sufficiently regular cover behavior.
• This contract does not define social policy decisions such as who should trust whom.
• This contract does not treat Hold custody as authoritative durable storage.
• This contract does not guarantee durable delivery from custody services.
• This contract does not guarantee that debug or simulation modes preserve production privacy properties.

2. Privacy Philosophy

Traditional privacy systems offer only complete isolation or complete exposure. Aura treats privacy as relational. Sharing information with trusted parties is a consented disclosure, not a privacy violation.

2.1 Core Principles

• Consensual disclosure: Joining a group or establishing a relationship implies consent to share coordination information
• Contextual identity: Deterministic Key Derivation presents different identities in different contexts, and only relationship parties can link them
• Neighborhood visibility: Gossip neighbors observe encrypted envelope metadata, bounded by flow budgets and context isolation
• Service trust is social: social planes may admit or weight providers, but provider trust must not become visible service shape
• Communication privacy is envelope-level: descriptors, routes, retrieval, and retention behavior must remain socially neutral at the network boundary

2.2 Privacy Layers

2.3 Service-Family Boundary

Establish, Move, and Hold are the privacy-relevant service families. They describe service behavior, not social role. A provider may be admitted because of neighborhood membership, direct friendship, bounded introduction evidence, or descriptor fallback, but the service interface must not reveal which reason dominated.

Trust evidence may affect Permit and runtime-local weighting. It must not appear as route shape, descriptor kind, retrieval shape, retention tier, or wire-visible policy class. Coarse selection tiers are local runtime derivations and are not canonical shared state.

3. Budgeted Send Invariant

Transport observables require prior local authorization, accounting, and fact-coupling.

Budget state is monotone within its active epoch. Over-budget sends must remain local. Receipt validity is epoch-scoped and old receipts must not be replayable in new epochs. Budget epochs are logical and follow the AMP ratchet model: receipt generations must fall inside the receiver-anchored window, the receiver advances the epoch by the spacing rule, and the window (allowance) resolves from per-peer override, context policy, then default (see Transport and Information Flow §3.1).

Forwarding is hop-local. Each hop must validate the required upstream accountability state before emitting downstream transport.

4. Leakage Tracking

4.1 Observer Classes

Information leakage is tracked per observer class:

4.2 Leakage Budget

Each observer class has a leakage budget separate from flow budgets.

Leakage is charged before any operation that exposes information to the observer class.

Custody observers are special. They may see that an opaque object is deposited, retained, expired, or retrieved. They must not learn mailbox identity or depositor identity from that flow.

4.3 Policy Modes

5. Privacy Boundaries

5.1 Relationship Boundary

Within a direct relationship, both parties have consented to share coordination information:

• Visible: Context-specific identity, online status, message content
• Hidden: Activity in other contexts, identity linkage across contexts
• Violation: cross-context identity reuse or disclosure of undisclosed contexts

5.2 Neighborhood Boundary

Gossip neighbors forward encrypted traffic:

• Visible: Envelope size (fixed), rotating rtags, timing patterns
• Hidden: Content, ultimate sender/receiver, rtag-to-identity mapping
• Violation: disclosure of plaintext content or protected endpoint identity

5.3 Group Boundary

Group participants share group-scoped information:

• Visible: Member identities (within group), group content, threshold operations
• Hidden: Member identities outside group, other group memberships
• Violation: disclosure of unrelated group membership through group participation

5.4 External Boundary

External observers have no relationship with you:

• In privacy mode: protected Aura traffic patterns and timing are visible
• In passthrough mode: direct Aura connectivity is visible
• Violation: treating basic availability deployment as a stronger privacy claim

5.5 Retrieval Boundary

Retrieval is not identity-addressed at the network boundary.

• Visible to intermediaries: selector traffic shape and reply-path usage
• Hidden from intermediaries: mailbox identity, semantic object meaning, and direct reverse identity
• Violation: identity-addressed retrieval on parity-critical paths

5.6 Custody Boundary

Hold providers operate on opaque custody objects rather than authoritative truth.

• Visible to the holder: bounded retention requests, opaque held objects, selector usage, and storage pressure
• Hidden from the holder under onion routing: specific depositor identity and mailbox identity
• Violation: treating custody state as authoritative truth or varying retention by social distance

6. Time Domain Semantics

Time handling affects privacy through leakage:

• Cross-domain time comparison must be explicit.
• Privacy-preserving flows must not expose physical time unless that exposure is part of the contract.

7. Adversarial Model

7.1 Direct Relationship

A party in a direct relationship may observe the full contents of that relationship context by consent.

• Must not: learn undisclosed contexts or link identity across contexts
• Contract boundary: relationship consent does not widen to other contexts

7.2 Group Insider

A group member may observe group-scoped activity by consent.

• Must not: learn other group memberships or unrelated identities
• Contract boundary: group visibility remains group-scoped

7.3 Gossip Neighbor

Devices forwarding traffic may observe protected metadata.

• Must not: decrypt content, identify protected endpoints, or map routing tags to identity
• Contract boundary: neighbor visibility remains budgeted metadata only

7.4 Network Observer

A network observer may observe connectivity and timing patterns.

• Must not: gain stronger privacy guarantees than the active deployment mode provides
• Contract boundary: privacy claims vary with the active protection mode

7.5 Compromised Device

A compromised device may reveal its local share and replicated state.

• Must not: unilaterally satisfy threshold requirements or derive protected root material
• Contract boundary: single-device compromise does not imply full authority compromise

8. External Observer Limits

Stronger privacy claims against external observers require sufficiently regular protected network behavior.

Basic availability deployments do not claim those stronger bounds. Routing and budgeting must also limit metadata concentration at any single relay or hub.

9. Required Properties

9.1 Identity and Key Separation

• Contexts must not share reusable identity material.
• Key derivation must remain domain-separated.
• Keys must not be reused across contexts.

9.2 Transport Privacy

• Protected transport must use authenticated encrypted envelopes.
• Transport observables must remain budgeted by observer class.
• Accountability return paths must not require direct reverse identity.

9.3 Send Authorization

• No transport observable may occur without prior local authorization and accounting.
• Failed authorization or charging must remain local.
• Forwarding must validate the required receipt or accountability state before onward transport.

9.4 Retrieval and Custody

• Parity-critical retrieval must use bounded retrieval authority.
• Parity-critical retrieval must not use identity-addressed mailbox polling.
• Hold custody must remain opaque and non-authoritative.
• Uniform retention policy must not vary by social distance.
• Applications that require guaranteed durability must use authoritative replicated state rather than Hold.

9.5 Accountability and Local Consequences

• Accountability evidence must be verified by the relevant local verifier before any local consequence is applied.
• Local scoring, reciprocal budget, and admission effects apply only after successful verification.
• Accountability traffic must not become a new global visibility layer.

9.6 Secret Material and Error Channels

• Secret material must not be stored in plaintext.
• Guard failures must return bounded, typed errors only.
• Error payloads must not include raw context payload, peer identity material, or decrypted content.
• Remote peers must not infer internal failure causes beyond allowed protocol-level status codes.

10. References

Distributed Systems Contract covers safety, liveness, and consistency.

Theoretical Model covers the formal calculus and semilattice laws.

System Architecture describes runtime layering and the guard chain.

Authorization covers authorization, budgeting, and Biscuit integration.

Transport and Information Flow documents transport semantics and receipts.

Relational Contexts documents cross-authority state and context isolation.

Verification Coverage Report tracks formal verification status.

Distributed Systems Contract

This contract specifies Aura's distributed systems model. It defines the safety, liveness, and consistency guarantees provided by the architecture. It also documents the synchrony assumptions and adversarial capabilities the system tolerates.

This contract complements Privacy and Information Flow Contract, which focuses on metadata and privacy budgets. Together these contracts define the full set of invariants protocol authors must respect.

Formal verification of these properties uses Quint model checking (verification/quint/) and Lean 4 theorem proofs (verification/lean/). See Verification Coverage Report for current status.

1. Scope

The contract applies to the following aspects of the system.

Effect handlers and protocols operate within the 8-layer architecture described in System Architecture. Journals and reducers are covered by this contract. The journal specification appears in Authority and Identity and Journal. Aura Consensus is documented in Consensus.

Relational contexts and rendezvous flows fall under this contract. Relational contexts are specified in Relational Contexts. Transport semantics appear in Transport and Information Flow. Rendezvous flows are detailed in Rendezvous Architecture. Shared notation appears in Theoretical Model.

1.1 Terminology Alignment

This contract uses shared terminology from Theoretical Model.

• Consensus role terms: witness for consensus attestation, signer for FROST share holders
• Social-role terms: Member, Participant, Moderator
• Access terms: AccessLevel (Full, Partial, Limited)
• Topology terms: 1-hop and n-hop paths

1.2 Contract Vocabulary

• authoritative: part of replicated truth and subject to convergence requirements
• protocol object: an execution object that supports transport or coordination without becoming replicated truth
• runtime-local: state owned by a local runtime and not treated as authoritative
• accountability witness: bounded evidence that a service action occurred
• custody failure: loss, eviction, or retrieval miss for a non-authoritative held object

1.3 Assumptions

• Cryptographic primitives remain secure at configured parameters.
• Partial synchrony eventually holds after GST, with bounded Δ_net.
• Honest participants execute the guard chain in the required order.
• Anti-entropy exchange eventually delivers missing facts to connected peers.

1.4 Non-goals

• This contract does not provide global linearizability across all operations.
• This contract does not guarantee progress during permanent partitions.
• This contract does not guarantee metadata secrecy without privacy controls defined in Privacy and Information Flow Contract.
• This contract does not guarantee that runtime-local caches reflect authoritative truth at all times.
• This contract does not guarantee durable custody from Hold services.

1.5 Service Object Classes

Distributed behavior depends on three object classes with different contracts:

• authoritative shared objects
• transport and protocol objects
• runtime-derived local state

Only authoritative shared objects participate in replicated truth. Transport and protocol objects support execution. Runtime-derived local state remains non-authoritative and local to the runtime that owns it.

2. Safety Guarantees

2.1 Journal CRDT Properties

Facts merge via set union and never retract. Journals satisfy the semilattice laws:

• Commutativity: merge(j1, j2) ≡ merge(j2, j1)
• Associativity: merge(merge(j1, j2), j3) ≡ merge(j1, merge(j2, j3))
• Idempotence: merge(j, j) ≡ j

Reduction is deterministic. Identical fact sets produce identical states. No two facts share the same nonce within a namespace (InvariantNonceUnique).

2.2 Charge-Before-Send

Every transport observable is preceded by local authorization, accounting, and fact-coupling checks. No packet is emitted without a successful local decision.

Flow budgets satisfy monotonicity: charging never increases available budget (monotonic_decrease). Charging the exact remaining amount results in zero budget (exact_charge).

2.3 Consensus Agreement

For any pair (cid, prestate_hash) there is at most one commit fact (InvariantUniqueCommitPerInstance). Fallback gossip plus FROST signatures prevent divergent commits. Byzantine witnesses cannot force multiple commits for the same instance.

Commits require threshold participation (InvariantCommitRequiresThreshold). Equivocating witnesses are excluded from threshold calculations (InvariantEquivocatorsExcluded).

2.3.1 Fault Assumptions

Consensus safety depends on declared threshold and fault bounds.

Threshold signatures require the configured threshold of distinct valid shares. Safety requires fault assumptions that remain within the bound declared for the active ceremony. Different ceremonies may declare different admissible fault bounds.

2.4 Evidence CRDT

The evidence system tracks votes and equivocations as a grow-only CRDT:

• Monotonicity: Votes and equivocator sets only grow under merge
• Commit preservation: merge preserves existing commit facts
• Semilattice laws: Evidence merge is commutative, associative, and idempotent

2.5 Equivocation Detection

The system detects witnesses who vote for conflicting results:

• Soundness: Detection only reports actual equivocation (no false positives)
• Completeness: All equivocations are detectable given sufficient evidence
• Honest safety: Honest witnesses are never falsely accused

Types like HasEquivocated and HasEquivocatedInSet exclude conflicting shares from consensus. See Consensus.

2.6 FROST Threshold Signatures

Threshold signatures satisfy binding and consistency properties:

• Share binding: Shares are cryptographically bound to (consensus_id, result_id, prestate_hash)
• Threshold requirement: Aggregation requires at least k shares from distinct signers
• Session consistency: All shares in an aggregation have the same session
• Determinism: Same shares always produce the same signature

2.7 Context Isolation

Messages scoped to ContextId never leak into other contexts. Contexts may be explicitly bridged through typed protocols only. See Theoretical Model. Each authority maintains separate journals per context to enforce this isolation.

2.8 Transport Layer

Beyond context isolation, transport satisfies:

• Flow budget non-negativity: Spent never exceeds limit (InvariantFlowBudgetNonNegative)
• Sequence monotonicity: Message sequence numbers strictly increase (InvariantSequenceMonotonic)
• Fact backing: Every sent message has a corresponding journal fact (InvariantSentMessagesHaveFacts)

2.9 Deterministic Reduction Order

Commitment tree operations resolve conflicts using the stable ordering described in Authority and Identity. This ordering is derived from the cryptographic identifiers and facts stored in the journal. Conflicts are always resolved in the same way across all replicas.

2.10 Receipt Chain

Multi-hop forwarding requires signed receipts. Downstream peers reject messages lacking a chain rooted in their relational context. See Transport and Information Flow. This prevents unauthorized message propagation.

2.11 Onion Accountability Verification

Onion-routed accountability must preserve anonymous reverse delivery of bounded witnesses.

Verifier roles are explicit and local. Local runtime consequences such as scoring, reciprocal budget, and admission preference apply only after verification succeeds.

Accountability return paths use typed single-use reply blocks. MoveReceiptReplyBlock, HoldDepositReplyBlock, HoldRetrievalReplyBlock, and HoldAuditReplyBlock are scoped proof-return capabilities. They are not generic reverse channels.

Witness traffic must return through the shared movement substrate when onion routing is active. Direct callback assumptions are not part of the privacy-mode contract.

2.12 Hold Service Profiles

Hold is a shared custody service surface. Profile-specific retrieval or retention semantics are allowed.

All Hold services must preserve the common custody invariants. Custody remains opaque, non-authoritative, selector-driven, and best-effort.

DeferredDeliveryHold and CacheReplicaHold are named profiles over one custody substrate. DeferredDeliveryHold uses retrieve-once semantics and re-deposit on miss. CacheReplicaHold uses retention-window-governed replica semantics.

Applications that need durable truth must use journals, consensus, or another authoritative replicated state path. Hold does not provide durable custody.

3. Protocol-Specific Guarantees

3.1 DKG and Resharing

Distributed key generation and resharing satisfy:

• Threshold bounds: 1 ≤ t ≤ n where t is threshold and n is participant count
• Phase consistency: Commitment counts match protocol phase
• Share timing: Shares distributed only after commitment verification

3.2 Invitation Flows

Invitation lifecycle satisfies authorization invariants:

• Sender authority: Only sender can cancel an invitation
• Receiver authority: Only receiver can accept or decline
• Single resolution: No invitation resolved twice
• Terminal immutability: Terminal status (accepted/declined/cancelled/expired) is permanent
• Fact backing: Accepted invitations have corresponding journal facts
• Ceremony gating: Ceremonies only initiated for accepted invitations

3.3 Epoch Validity

Epochs enforce temporal boundaries:

• Receipt validity window: Receipts only valid within their epoch
• Replay prevention: Old epoch receipts cannot be replayed in new epochs

3.4 Cross-Protocol Safety

Concurrent protocol execution (e.g., Recovery∥Consensus) satisfies:

• No deadlock: Interleaved execution always makes progress
• Revocation enforcement: Revoked devices excluded from all protocols

4. Liveness Guarantees

4.1 Fast-Path Consensus

Fast-path consensus completes within bounded delay when the fast-path witness and network assumptions hold.

4.2 Fallback Consensus

Fallback consensus eventually completes under partial synchrony when the fallback quorum and delivery assumptions hold.

4.3 Anti-Entropy

Journals converge under eventual delivery. CRDT merges reconcile fact sets even after partitions.

4.4 Rendezvous

Offer and answer envelopes flood gossip neighborhoods. Secure channels can be established as long as at least one bidirectional path remains between parties. See Rendezvous Architecture.

4.5 Flow Budgets

Flow-budget progress is conditional. If future epoch state restores positive headroom and epoch updates converge, local budget enforcement eventually grants headroom. Budget exhaustion remains temporary only under these assumptions.

Liveness requires that each authority eventually receives messages from its immediate neighbors. This is the eventual delivery assumption. Liveness also requires that clocks do not drift unboundedly. This is necessary for epoch rotation and receipt expiry.

4.6 Hold Availability

Hold availability is neighborhood-scoped and selector-driven. It is not a guarantee that any specific holder remains available.

Liveness for Hold requires that the runtime can find some admissible holder within the neighborhood-scoped provider set. Retrieval miss and re-deposit are expected recovery behaviors. They are not contract violations by themselves.

The runtime may choose a bounded rotating subset of holders inside the wider neighborhood-scoped provider set. This bounded operational set does not narrow the interface scope. Retention treatment must remain uniform across neighborhood deposits.

5. Time System

Aura uses a unified TimeStamp with domain-specific comparison:

• Reflexivity: compare(policy, t, t) = eq
• Transitivity: compare(policy, a, b) = lt ∧ compare(policy, b, c) = lt → compare(policy, a, c) = lt
• Privacy: Physical time hidden when ignorePhysical = true

Time variants include PhysicalClock (wall time), LogicalClock (vector/Lamport), OrderClock (opaque ordering tokens), and Range (validity windows).

6. Synchrony and Timing Model

Aura assumes partial synchrony. There exists a bound Δ_net on message delay and processing time once the network stabilizes. This bound may be unknown before stabilization occurs.

Before stabilization, progress may stall. After stabilization, protocols that depend on eventual delivery and bounded delay may resume progress.

Flow budget epochs are logical, using AMP-style generations, windows and spacing (see Transport and Information Flow §3.1); no clock decides which budget epoch is in force. Where other epochs use time-based rotation, it relies on loosely synchronized clocks. The journal remains the source of truth for observed epoch state.

7. Adversarial Model

7.1 Network Adversary

A network adversary may delay or drop traffic and may control a subset of links.

• Must not: break cryptography or forge valid accountability material without the required local authorization and signatures
• Contract boundary: safety holds only within the declared fault bounds for the active ceremony

7.2 Byzantine Witness

A Byzantine witness may equivocate or refuse to participate.

• Must not: cause multiple commits for the same consensus instance while the declared fault assumptions hold
• Contract boundary: equivocation is detectable and excluded from valid threshold outcomes

7.3 Malicious Relay

A malicious relay may drop, delay, or refuse to forward envelopes.

• Must not: read protected payload content or forge valid forwarding accountability
• Contract boundary: relay failure may reduce liveness but must not violate transport safety or accountability rules

7.4 Malicious Hold Provider

A malicious hold provider may evict, refuse retrieval, or under-serve after accepting custody.

• Must not: turn custody objects into authoritative state or obtain legitimate service credit without successful witness verification
• Contract boundary: custody failure affects availability, not authoritative truth

7.5 Device Compromise

A compromised device may reveal its local share and journal copy.

• Must not: satisfy threshold requirements on its own or rewrite authoritative history unilaterally
• Contract boundary: device compromise is recoverable if the remaining threshold and recovery assumptions still hold

8. Consistency Model

9. Failure Handling

Failure classes are distinct:

• authoritative state failure
• custody failure
• runtime-local cache or selection failure

Allowed failure:

• temporary loss of progress during partition or instability
• custody miss, eviction, or re-deposit
• runtime-local cache invalidation or reselection

Forbidden failure:

• divergent authoritative truth for the same committed operation
• treating custody state as authoritative replicated truth
• exposing internal failure causes through remote error detail

Local-only failure:

• authorization failure
• budget exhaustion
• runtime-local cache or selection failure

9.1 Error-Channel Privacy Requirements

• Runtime errors must use bounded enums and redacted payloads.
• Error paths must not include plaintext message content, raw capability tokens, or cross-context identifiers.
• Remote peers may observe protocol-level status outcomes only, not internal guard-stage diagnostics.

10. References

System Architecture describes runtime layering.

Authorization describes authorization and budgeting ordering.

Theoretical Model covers the formal calculus and semilattice laws.

Authority and Identity documents reduction ordering.

Journal and Distributed Maintenance Architecture cover fact storage and convergence.

Relational Contexts documents cross-authority state.

Consensus describes fast path and fallback consensus.

Transport and Information Flow documents transport semantics.

Authorization covers authorization and budgeting sequencing.

Verification Coverage Report tracks formal verification status.

Cryptography

This document describes the cryptographic architecture in Aura. It defines layer responsibilities, code organization patterns, security invariants, and compliance requirements for cryptographic operations.

Distributed FROST package construction exchanges public signing commitments, never private nonce bundles. A participant signs only after matching the native and outer signing messages to its independently admitted intent, and matching the public package, complete selected participant inventory, local share and threshold to its admitted policy. The native public key package does not encode the threshold; its presence alone cannot establish quorum policy. Runtime ownership must additionally enforce durable one-use nonce consumption and the original admitted execution window. Public commitment data does not grant that ownership.

FROST aggregation requires exactly one supplied signature share per selected participant. Extra shares cannot be ignored. The native commitment inventory and message must match the outer package; malformed shares and audited-library aggregation failures retain their concrete causes.

1. Overview

Aura's cryptographic architecture follows the 8-layer system design with strict separation of concerns.

• Layer 1 (aura-core): Type wrappers, trait definitions, pure functions
• Layer 3 (aura-effects): Production implementations with real crypto libraries
• Layer 8 (aura-testkit): Mock implementations for deterministic testing

This separation ensures that cryptographic operations are auditable, testable, and maintainable. Security review focuses on a small number of files rather than scattered usage throughout the codebase.

2. Layer Responsibilities

2.1 Layer 1: aura-core

The aura-core crate provides cryptographic foundations without direct side effects.

Type Wrappers

Type wrappers live in crates/aura-core/src/crypto/ed25519.rs.

#![allow(unused)]
fn main() {
pub struct Ed25519SigningKey(pub [u8; 32]);
pub struct Ed25519VerifyingKey(pub [u8; 32]);
pub struct Ed25519Signature(pub [u8; 64]);
}

These wrappers use fixed-size arrays for type safety and delegate to ed25519_dalek internally. They expose a stable API independent of the underlying library. They enable future algorithm migration without changing application code. They provide type safety across crate boundaries.

Effect Traits

Effect trait definitions live in crates/aura-core/src/effects/. The CryptoCoreEffects trait inherits from RandomCoreEffects and provides core cryptographic operations.

#![allow(unused)]
fn main() {
#[async_trait]
pub trait CryptoCoreEffects: RandomCoreEffects + Send + Sync {
    // Key derivation
    async fn kdf_derive(&self, ikm: &[u8], salt: &[u8], info: &[u8], output_len: u32) -> Result<Vec<u8>, CryptoError>;
    async fn derive_key(&self, master_key: &[u8], context: &KeyDerivationContext) -> Result<Vec<u8>, CryptoError>;

    // Ed25519 signatures
    async fn ed25519_generate_keypair(&self) -> Result<(Vec<u8>, Vec<u8>), CryptoError>;
    async fn ed25519_sign(&self, message: &[u8], private_key: &[u8]) -> Result<Vec<u8>, CryptoError>;
    async fn ed25519_verify(&self, message: &[u8], signature: &[u8], public_key: &[u8]) -> Result<bool, CryptoError>;

    // Utility methods
    fn is_simulated(&self) -> bool;
    fn crypto_capabilities(&self) -> Vec<String>;
    fn constant_time_eq(&self, a: &[u8], b: &[u8]) -> bool;
    fn secure_zero(&self, data: &mut [u8]);
}
}

The CryptoExtendedEffects trait provides additional operations with default implementations that return errors:

#![allow(unused)]
fn main() {
#[async_trait]
pub trait CryptoExtendedEffects: CryptoCoreEffects + Send + Sync {
    // Unified signing API
    async fn generate_signing_keys(&self, threshold: u16, max_signers: u16) -> Result<SigningKeyGenResult, CryptoError>;
    async fn generate_signing_keys_with(&self, method: KeyGenerationMethod, threshold: u16, max_signers: u16) -> Result<SigningKeyGenResult, CryptoError>;
    async fn sign_with_key(&self, message: &[u8], key_package: &[u8], mode: SigningMode) -> Result<Vec<u8>, CryptoError>;
    async fn verify_signature(&self, message: &[u8], signature: &[u8], public_key_package: &[u8], mode: SigningMode) -> Result<bool, CryptoError>;

    // FROST threshold signatures
    async fn frost_generate_keys(&self, threshold: u16, max_signers: u16) -> Result<FrostKeyGenResult, CryptoError>;
    async fn frost_generate_nonces(&self, key_package: &[u8]) -> Result<FrostNonces, CryptoError>;
    async fn frost_create_public_signing_package(&self, message: &[u8], commitments: &[FrostPublicCommitment], public_key_package: &[u8], threshold: u16) -> Result<FrostSigningPackage, CryptoError>;
    async fn frost_sign_share_for_message(&self, package: &FrostSigningPackage, local_key_share: &[u8], nonces: RetiredFrostNonces, expected_message: &[u8], expected_public_key_package: &[u8], expected_threshold: u16) -> Result<Vec<u8>, CryptoError>;
    async fn frost_aggregate_signatures(&self, signing_package: &FrostSigningPackage, signature_shares: &[Vec<u8>]) -> Result<Vec<u8>, CryptoError>;
    async fn frost_verify(&self, message: &[u8], signature: &[u8], group_public_key: &[u8]) -> Result<bool, CryptoError>;
    async fn ed25519_public_key(&self, private_key: &[u8]) -> Result<Vec<u8>, CryptoError>;

    // Symmetric encryption
    async fn chacha20_encrypt(&self, plaintext: &[u8], key: &[u8; 32], nonce: &[u8; 12]) -> Result<Vec<u8>, CryptoError>;
    async fn chacha20_decrypt(&self, ciphertext: &[u8], key: &[u8; 32], nonce: &[u8; 12]) -> Result<Vec<u8>, CryptoError>;
    async fn aes_gcm_encrypt(&self, plaintext: &[u8], key: &[u8; 32], nonce: &[u8; 12]) -> Result<Vec<u8>, CryptoError>;
    async fn aes_gcm_decrypt(&self, ciphertext: &[u8], key: &[u8; 32], nonce: &[u8; 12]) -> Result<Vec<u8>, CryptoError>;

    // Key rotation and conversion
    async fn frost_rotate_keys(&self, old_shares: &[Vec<u8>], old_threshold: u16, new_threshold: u16, new_max_signers: u16) -> Result<FrostKeyGenResult, CryptoError>;
    async fn convert_ed25519_to_x25519_public(&self, ed25519_public_key: &[u8]) -> Result<[u8; 32], CryptoError>;
    async fn convert_ed25519_to_x25519_private(&self, ed25519_private_key: &[u8]) -> Result<[u8; 32], CryptoError>;
}

pub trait CryptoEffects: CryptoCoreEffects + CryptoExtendedEffects {}
}

The core trait provides key derivation and Ed25519 signatures. The extended trait provides unified signing that routes between single-signer and threshold modes, FROST threshold operations, symmetric encryption, and key conversion. Hashing is not included because it is a pure operation. Use aura_core::hash::hash() for synchronous hashing instead.

The RandomCoreEffects trait provides cryptographically secure random number generation.

#![allow(unused)]
fn main() {
#[async_trait]
pub trait RandomCoreEffects: Send + Sync {
    async fn random_bytes(&self, len: usize) -> Vec<u8>;
    async fn random_bytes_32(&self) -> [u8; 32];
    async fn random_u64(&self) -> u64;
}

#[async_trait]
pub trait RandomExtendedEffects: RandomCoreEffects + Send + Sync {
    async fn random_range(&self, min: u64, max: u64) -> u64;
    async fn random_uuid(&self) -> Uuid;
}
}

The core trait provides basic random generation. The extended trait adds range and UUID generation with default implementations. All randomness flows through these traits for testability and simulation.

Pure functions in crates/aura-core/src/crypto/ implement hash functions, signature verification, and other deterministic operations. These require no side effects and can be called directly.

2.2 Layer 3: aura-effects

The aura-effects crate contains the only production implementations that directly use cryptographic libraries.

The production handler lives in crates/aura-effects/src/crypto.rs. RealCryptoHandler can operate with OS entropy (production) or with a seed (deterministic testing). It implements all methods from CryptoCoreEffects and RandomCoreEffects.

The following direct imports are allowed in Layer 3:

• ed25519_dalek
• frost_ed25519
• chacha20poly1305
• aes_gcm
• getrandom
• rand_core::OsRng
• rand_chacha
• blake3

2.3 Threshold Lifecycle (K1/K2/K3) and Transcript Binding

Aura separates key generation from agreement/finality:

• K1: Single-signer (Ed25519). No DKG required.
• K2: Dealer-based DKG. A trusted coordinator produces dealer packages.
• K3: Consensus-finalized DKG. The BFT-DKG transcript is finalized by consensus.

Transcript hashing uses the following rules:

• All DKG transcripts are hashed using canonical DAG‑CBOR encoding.
• DkgTranscriptCommit binds transcript_hash, prestate_hash, and operation_hash.

Dealer packages (K2) follow these rules:

• Deterministic dealer packages are acceptable in trusted settings.
• Dealer packages must include encrypted shares for every participant.

BFT‑DKG (K3) follows these rules:

• A transcript is only usable once consensus finalizes the commit fact.
• All K3 ceremonies must reference the finalized transcript (hash or blob ref).

2.4 Layer 8: aura-testkit

The aura-testkit crate provides mock implementations for deterministic testing.

The mock handler lives in crates/aura-testkit/src/stateful_effects/crypto.rs. MockCryptoHandler uses a seed and counter for deterministic behavior, enabling reproducible test results, simulation of edge cases, and faster test execution.

3. Usage Boundary

Application code accesses cryptographic operations exclusively through effect traits. Direct imports of cryptographic libraries are forbidden outside Layer 3 handlers. Randomness flows through RandomCoreEffects for testability and simulation. See Effects and Handlers Guide for usage patterns and anti-patterns.

4. Allowed Locations

Direct cryptographic library usage is restricted to the following locations.

5. Security Invariants

The cryptographic architecture maintains these invariants.

1. All production crypto operations flow through RealCryptoHandler
2. Security review focuses on Layer 3 handlers, not scattered usage
3. All crypto is controllable via mock handlers for testing
4. Private keys remain in wrapper types, not exposed as raw bytes
5. Production randomness comes from OS entropy via OsRng
6. Identity and key bytes decoded from a remote payload are untrusted until checked against an authoritative local key source. A signature by the same key that signed an imported invitation proves continuity of that invitation, not trusted device identity.
7. A response is constructed from a completed signature over its canonical transcript; production response construction does not create an unsigned placeholder.
8. Imported authority tree operations require the verifying package and threshold policy of their parent epoch from an authenticated source. A matching parent commitment, a sibling transport session, or a key delivered beside the operation does not authenticate the operation. An enrolling device needs an explicit, ceremony-bound trust bootstrap before it can adopt a baseline tree. Required parent-policy reads distinguish absent records from storage and decoding failures. Participant inventory is complete and unique, and single-signer policy has exactly one participant and a threshold of one. An unreadable trusted record cannot authorize migration to a substitute verifier.
9. A transport receipt signed under a key carried in the receipt proves transcript integrity under that key. It does not authenticate the AuthorityId in the envelope. Promoting the source to verified authority or device identity requires comparison with an independently trusted key and an authenticated authority/device binding. A nonzero nonce is not replay protection without a checked replay state.

6. Signing Modes

Aura supports two signing modes to handle different account configurations.

6.1 SigningMode Enum

#![allow(unused)]
fn main() {
pub enum SigningMode {
    SingleSigner,  // Standard Ed25519 for 1-of-1
    Threshold,     // FROST for m-of-n where m >= 2
}
}

The SingleSigner mode is used for new user onboarding with single device accounts. It is also used for bootstrap scenarios before multi-device setup and for simple personal accounts that do not need threshold security.

The Threshold mode is used for multi-device accounts such as 2-of-3 or 3-of-5 configurations. It is also used for guardian-protected accounts and group decisions requiring multiple approvals.

6.2 Why Two Modes?

FROST requires at least 2 signers. For 1-of-1 configurations, we use standard Ed25519.

Ed25519 uses the same curve as FROST and produces compatible signatures for verification. Single signatures do not require nonce coordination or aggregation.

6.3 API Usage

The unified signing API selects between SingleSigner and Threshold modes based on the threshold parameter. For implementation patterns, see Effects and Handlers Guide.

6.4 Storage Separation

Single-signer and threshold keys use separate storage paths managed by SecureStorageEffects. Path conventions are documented in Effects and Handlers Guide.

7. FROST and Threshold Signatures

Aura provides a unified threshold signing architecture for all scenarios requiring m-of-n signatures where m >= 2.

7.1 Architecture Layers

The trait definition lives in aura-core/src/effects/threshold.rs.

#![allow(unused)]
fn main() {
#[async_trait]
pub trait ThresholdSigningEffects: Send + Sync {
    async fn bootstrap_authority(&self, authority: &AuthorityId) -> Result<PublicKeyPackage, ThresholdSigningError>;
    async fn sign(&self, context: SigningContext) -> Result<ThresholdSignature, ThresholdSigningError>;
    async fn threshold_config(&self, authority: &AuthorityId) -> Option<ThresholdConfig>;
    async fn threshold_state(&self, authority: &AuthorityId) -> Option<ThresholdState>;
    async fn has_signing_capability(&self, authority: &AuthorityId) -> bool;
    async fn public_key_package(&self, authority: &AuthorityId) -> Option<PublicKeyPackage>;
    async fn rotate_keys(&self, authority: &AuthorityId, new_threshold: u16, new_total_participants: u16, participants: &[ParticipantIdentity]) -> Result<(u64, Vec<Vec<u8>>, PublicKeyPackage), ThresholdSigningError>;
    async fn commit_key_rotation(&self, authority: &AuthorityId, new_epoch: u64) -> Result<(), ThresholdSigningError>;
    async fn rollback_key_rotation(&self, authority: &AuthorityId, failed_epoch: u64) -> Result<(), ThresholdSigningError>;
}
}

The trait provides methods for bootstrapping authorities, signing operations, querying configurations and state, checking capabilities, and key rotation lifecycle management.

Context types live in aura-core/src/threshold/context.rs.

#![allow(unused)]
fn main() {
pub struct SigningContext {
    pub authority: AuthorityId,
    pub operation: SignableOperation,
    pub approval_context: ApprovalContext,
}

pub enum SignableOperation {
    TreeOp(TreeOp),
    RecoveryApproval { target: AuthorityId, new_root: TreeCommitment },
    GroupProposal { group: AuthorityId, action: GroupAction },
    Message { domain: String, payload: Vec<u8> },
    OTAActivation { ceremony_id: [u8; 32], upgrade_hash: [u8; 32], prestate_hash: [u8; 32], activation_epoch: Epoch, ready: bool },
}

pub enum ApprovalContext {
    SelfOperation,
    RecoveryAssistance { recovering: AuthorityId, session_id: String },
    GroupDecision { group: AuthorityId, proposal_id: String },
    ElevatedOperation { operation_type: String, value_context: Option<String> },
}
}

The SignableOperation enum defines what is being signed. Its OTA activation variant should be interpreted as scoped activation approval evidence. activation_epoch is meaningful only when the chosen scope actually owns an epoch fence. The ApprovalContext enum provides context for audit and display purposes.

The service implementation lives in aura-agent/src/runtime/services/threshold_signing.rs. ThresholdSigningService manages per-authority signing state and key storage using SecureStorageEffects for key material persistence.

Bootstrap preserves an existing signing identity. Recovery loads the persisted active epoch, policy, participants and public package instead of regenerating epoch-zero keys. Invalid or incomplete persisted material is a recovery failure and cannot authorize replacement keys. Decrypting an existing signing share is a read-only operation on its wrapping key; a missing key or failed storage read must not create new wrapping material. A setup code signed before recovery must retain the same verifier afterward.

An enrollment response must verify under the exact provisional signing package, epoch, mode and threshold policy selected by explicit user transfer. The initiator retains that statement, its canonical digest and ceremony binding before starting response owners; proof material supplied by the responder cannot choose the expected verifier. Restored records retain the original package and validity bounds. Missing legacy verifier state requires a new transfer rather than self-certifying a response's key.

The setup validity interval governs admission to issuance. A successfully retained ceremony may verify a response after setup expiry within the invitation/ceremony's own response deadline; expiry does not substitute another key or grant a new issuance. These deadlines are distinct from nonce consumption and atomic activation, whose durable receipts remain separate requirements.

Historical setup-response signing is limited to a retained, admitted setup request and its exact invitation/ceremony transcript. Possession of an old encrypted key does not authorize signing after local revocation, cancellation or completion. A response permit requires authenticated initiator-manifest provenance, a durable setup admission receipt and current owner-controlled lifecycle eligibility. It cannot accept an arbitrary payload, domain or epoch. Setup admission must not infer validity from another device's exact wall-clock timestamp; each owner's recorded admission evidence governs its validity gate.

For a threshold setup policy, response signing requires the authenticated historical participant inventory and its quorum under the same narrow response permit. Single-signer fallback cannot satisfy that policy. Retained shares remain available while authorized pending requests need them; expiry, cancellation, revocation and terminal outcomes govern retirement without removing active keys.

A retained local threshold share must match its authenticated signer identity, threshold policy, group verifying key and verifying share. Its signing scalar must derive that same verifying share, and the public package must contain the exact authenticated participant inventory. Package decoding alone does not establish these properties. Native FROST public packages do not encode a threshold; a conversion default is not policy evidence. Membership in a prior epoch cannot authorize signing after removal from the current participant set.

Initial signing-key readiness is distinct from bootstrap genesis completion. A pending genesis record binds the authority, physical device, epoch-zero public package digest and initialization phase before key persistence. Completion binds the authenticated, durably indexed device-creation operation. A failed genesis commit cannot publish a usable signing context. Recovery may resume creation only from a matching pending initialization; legacy keys with missing or conflicting creation evidence require explicit recovery rather than a new leaf.

Low-level primitives live in aura-core/src/crypto/tree_signing.rs. This module defines FROST types and pure coordination logic. It re-exports frost_ed25519 types for type safety.

The handler in aura-effects/src/crypto.rs implements FROST key generation and signing. This is the only location with direct frost_ed25519 library calls.

7.2 Serialized Size Invariants (FROST)

Aura treats the postcard serialization of FROST round-one data as canonical and fixed-size. This prevents malleability and makes invalid encodings unrepresentable at the boundary.

• SigningNonces (secret) must serialize to exactly 138 bytes
• SigningCommitments (public) must serialize to exactly 69 bytes

These sizes are enforced in aura-core/src/crypto/tree_signing.rs and mirrored in aura-core/src/constants.rs. See Distributed Maintenance Guide for update procedures when upstream encodings change.

7.3 Lifecycle Taxonomy (Key Generation vs Agreement)

Aura separates key generation from agreement/finality:

• K1: Local/Single-Signer (no DKG)
• K2: Dealer-Based DKG (trusted coordinator)
• K3: Quorum/BFT-DKG (consensus-finalized transcript)

Agreement modes are orthogonal:

• A1: Provisional (usable immediately, not final)
• A2: Coordinator Soft-Safe (bounded divergence + convergence cert)
• A3: Consensus-Finalized (unique, durable, non-forkable)

Leader selection (lottery/round seed/fixed coordinator) and pipelining are orthogonal optimizations, not agreement modes.

7.4 Usage Pattern

High-level signing operations use AppCore or direct ThresholdSigningEffects trait calls. See Effects and Handlers Guide for recommended patterns.

7.5 Threshold PRF for Shared Symmetric Keys

FROST DKG leaves the group secret s unknown to every participant, so a symmetric key that all members of a relational context share (AMP channel base keys, AMP §4) is derived with a DDH-based threshold PRF over the DKG shares rather than from any public value.

• H(x) hashes the input to a prime-order Ed25519 point whose discrete log is unknown (domain-separated try-and-increment; canonical decoding rejects identity and small-order points).
• Participant i with share s_i publishes σ_i = s_i · H(x) and a Chaum-Pedersen proof that log_B(Y_i) = log_H(σ_i) for its public verifying share Y_i = s_i · B. Partials that do not verify are discarded, so a faulty member cannot corrupt the key.
• Any threshold of verified partials from distinct participants combine by Lagrange interpolation at zero to s · H(x); the key is KDF(s · H(x), x). Every member derives the same key, and data available to non-members (the group verifying key, verifying shares, x) does not determine it.
• The proof nonce comes from RandomEffects; the primitive is pure and lives in aura-core::crypto::threshold_prf.

7.6 FROST Minimum Threshold

FROST requires threshold >= 2. Calling frost_generate_keys(1, 1) returns an error. For single-signer scenarios, use generate_signing_keys(1, 1) which routes to Ed25519 automatically.

8. Extensibility

The wrapper and trait abstraction enables algorithm migration and HSM integration without changing application code. Migration procedures are documented in Distributed Maintenance Guide.

See Also

• Effect System for effect trait patterns
• Project Structure for 8-layer architecture
• Effects and Handlers Guide for handler implementation guidance

Independently transferred enrollment manifest

The current version-three manifest requires an explicit final active verifier inventory. Enrollment transfer version four requires the original setup binding and invitee authority. Acceptance requires the exact manifest digest; persisted activation version three requires its signed epoch fence, original baseline and that digest. Omitted or null required evidence fails decoding. Obsolete enrollment transport, manifest and activation representations are not admitted.

Enrollment baseline admission requires a signed EnrollmentTrustManifest and an independently transferred initiator verifier statement. The verifier statement binds the subject authority, physical initiator device, and confirmation key. A key embedded in an invitation or manifest cannot establish this pin. Decoding a transfer statement does not authorize admission; the explicit app transfer owner selects it.

The signed manifest binds the exact setup nonce and digest, reserved invitation and ceremony identifiers, actual provisional invitee authority and physical device, pending epoch, encrypted participant share, public package, canonical provisional threshold policy, and complete ordered baseline digest. Every attested baseline operation requires an exact parent epoch, commitment, signing node, group verifier, ordered participant inventory, threshold, signing mode, and agreement policy from that independently authenticated inventory. Replay checks each signature and reduction before any baseline/key mutation, rejects unused or missing inventory, and requires the exact final commitment. An epoch root key is not proof of an arbitrary node verifier.

Runtime admission rechecks the actual locally retained exported setup request and its signed policy bounds. The immutable secure admission record retains the selected verifier and original local admission time; recovery re-verifies its evidence rather than deserializing a trusted witness. Missing, corrupt, expired, mismatched, or legacy unbound evidence fails closed. Admission is a ceremony-scoped bootstrap permission, not authority adoption, durable peer membership, or permission to use retired signing shares. Acceptance binds the issuer-retained exact manifest digest in addition to the setup and ceremony binding.

Committed enrollment confirmation receipts

An invitee activation requires an issuer-pinned signed committed confirmation bound to the exact independently admitted enrollment manifest, invitation, ceremony, physical device and pending epoch. A cached accepted status, unsigned confirmation or received signing package is insufficient. The committed confirmation and original admitted budget acknowledgement are retained in an immutable authenticated local receipt before activation.

Recovery verifies the original transfer signature, exact baseline and setup binding, the actual committed confirmation signature, and the recorded original budget state before producing activation evidence. Historical verification is scoped to that retained receipt; it grants no historical signing authority and cannot extend an admission window. Actual retained share, public package and canonical provisional configuration must match the signed manifest. Generic rotation activation cannot consume an enrollment import generation, and activation cannot roll back a later retained epoch.

Enrollment verifier origin enforcement

Retained enrollment response verification uses the independently retained setup verifier. Enrollment control verification uses the sealed independently admitted manifest. A remote key field and a trusted-looking local name do not establish either origin. Domain manifest signature verification establishes integrity under the explicitly independent input key and does not establish admission or current membership. Lexical test-only scopes do not relax production verifier contracts.

Public enrollment configuration digest

The enrollment manifest's pending configuration digest is a Hash32 content hash of the exact issued configuration encoding. It is public commitment material, not a threshold configuration or secret signing share. Its canonical encoding remains the original 32-byte array representation. Admission and generation validation compare this digest with freshly computed hashes of exact retained bytes; the digest alone confers no authority.

Enrollment signing roster and authenticated topology

Enrollment keeps the original independently pinned signing quorum separate from the authenticated tree child topology. A signed AddLeaf changes observed child edges before the original signing key attests the RotateEpoch activation fence. Verification retains the exact signed quorum minimum and signer-roster upper bound while deriving topology cardinality solely from authenticated branch and leaf-parent edges. A verification projection does not materialize a canonical branch. A policy already materialized by authenticated tree operations remains an independent minimum; invalid or incompatible canonical policy metadata fails closed and requires an authenticated policy transition rather than a local repair. Missing node-specific verifier inventory cannot be replaced with the epoch root package.

Individual participant possession proofs

An individual possession proof authenticates a transcript under one exact participant verifier from the independently authenticated current signing inventory. A FROST verifying share is distinct from the aggregate group key. Proof verification under a share does not satisfy the authority quorum or authorize an epoch transition. The signed transcript binds the protocol and version, subject ceremony and proposal, physical participant, active epoch, signing mode and index, and exact group package commitment. Legacy unbound responses cannot acquire current participant authority.

The primitive preserves canonical FROST scalar encoding and uses the standard ciphersuite Schnorr nonce/challenge/signature operations. A scalar is never reinterpreted as an Ed25519 seed. Runtime authorization additionally requires held current generation and tree custody and canonical physical membership.

Required active signing material

The runtime effect signer selects its epoch, policy, participant, and public package from required retained state under signing-generation custody. Missing or malformed state is a source-bearing failure. A solo signature additionally requires agreement between the retained public package and the public key derived by the cryptographic effect from the selected private package. A local share does not establish quorum; multi-party signing requires its owned threshold-agreement producer. Historical enrollment confirmation keys remain selected only by the retained original issuance witness.

Legacy bootstrap representation migration

A legacy epoch-zero participant representation may change from the authority's Guardian identifier to its authenticated physical Device identifier only while preserving the original signing secret and public package. Admission requires the authenticated original creation operation and its durable commit evidence. The converted canonical policy binds an immutable original migration decision; required signing and recovery reject missing or contradictory decision evidence. This representation migration provides neither a new signing epoch nor quorum agreement and does not renew any enrollment validity window.

Final active enrollment verifier inventory

Manifest v2 authenticates a final active exact-node verifier inventory separately from the historical parents that validate baseline operations. Each tuple binds the final epoch and tree commitment, signing node, mode, ordered participant roster, quorum, agreement and actual public package. Historical signatures do not promote an old package into a later epoch. Version-1 manifests preserve their original bytes and signature domain as historical evidence; a missing final inventory cannot authorize a new enrollment peer response.

Imported historical public verifier continuity

An imported authority's historical verifier inventory is evidence from its independently pinned enrollment manifest and authenticated committed transition. Its durable archive binds the physical profile/device, original admission, subject, invitation, manifest digest and committed history digest. Recovery revalidates the original admission and committed proof before granting access to archived verifier evidence. Possession of serialized public tuples is insufficient. The imported pending generation extends that evidence only when its exact public package and canonical provisional policy match the original signed commitments. Historical evidence does not certify absence of a later revocation, and it does not authorize substitution of an epoch root package for another signing node.

Archive v2 retains the imported pending generation's exact public package and canonical provisional policy from the original authenticated invitation, at its verified committed head. Verification can therefore continue after private share retirement without reconstructing public trust from a missing native key record. An already verified extension at that same epoch may use the same exact root verifier at its authenticated parent head; this does not grant trust to another node or epoch. Immutable v1 archives retain their original bytes and do not confer v2 admission. V2 publication requires explicit revalidation of the original locally retained confirmed receipt and uses a separate versioned namespace.

Threshold enrollment issuer evidence

A locally retained threshold participant package proves ownership of one exact share under the authenticated active policy. It is not a completed threshold signature and cannot authorize a solo enrollment manifest. Required issuer selection distinguishes missing quorum ownership from malformed signing policy, missing retained material, and private/public mismatch. Enrollment issuance after a threshold epoch requires a completed signature from the owned multi-party signing protocol, bound to the original allocation window and authenticated final verifier inventory.

The threshold policy domain permits k = 1 with multiple participants. The selected FROST backend requires at least two signers. A retained threshold package with k = 1 therefore reports an explicit backend capability failure; it is never normalized to a solo package or a higher threshold. Native backend operations retain their actual InvalidMinSigners failure.

Public signature input provenance

Bounded parsing of a public package and signature has typed input-encoding failures and does not establish signature validity, authority or quorum custody. Enrollment setup possession validates those encodings before invoking the verification effect. Malformed peer encodings and an invalid signature verdict are request rejection; an effect-provider verification failure retains its original required-runtime cause.

Unified threshold verification accepts the canonical native FROST public key package. The low-level FROST verification primitive accepts the extracted group verifying point. These inputs are distinct and have no repair fallback.

Deterministic random stream custody

Cloning a runtime crypto subsystem retains the same deterministic random stream owner. Draws through any clone consume that one stream in execution order; cloning cannot duplicate the next nonce or key-generation sequence. Separately constructed simulations with the same seed retain independent owners and reproduce the same sequence when their draw ordering matches. Concurrent scheduling does not imply a deterministic assignment of draws to individual callers.

Allocation-owned wrapping secrets

Permanent immutable wrapping records retain their original protection. An allocation-owned wrapping secret has a separately acknowledged immutable birth and a first-decision lifetime. Positive and negative decisions are mutually exclusive. Negative retirement removes normal live access only after the original provider acknowledges its tombstone; copied old ciphertext and backup erasure are separate guarantees. Existing permanent records cannot be relabeled as retirable allocations.

Private allocation lifetime persistence encoding

The selected filesystem lifetime provider serializes its private ledger record only to produce authenticated encrypted persistence. Serialized and decrypted plaintext buffers require zeroizing ownership; the decoded record zeroizes its secret field on drop. The codec does not provide logging, cloning, or public secret export. Its serialization derives require an explicit scoped security justification and the security policy gate. Retirement acknowledgement denies subsequent ledger reads; this does not prove cryptographic erasure of historical ciphertext copies decryptable under the retained profile key.

Secret field decoding itself requires zeroizing ownership and a bounded byte sequence. This applies before complete record construction, including malformed secret elements and failures in subsequent fields; record-level Drop alone is insufficient. Existing authenticated JSON byte-array encoding remains compatible.

Lifetime record plaintext serialization uses one zeroizing allocation from its first encoded byte. Encoding cannot release secret-bearing intermediate growth allocations. Authenticated envelope limits include magic, nonce and AEAD tag; codec failures retain their original serialization cause.

Platform-selected allocation lifetime custody

A production platform credential provider may issue allocation lifetime custody only from the same exclusive profile and credential namespace owner that was selected for ordinary secure records. A filesystem fallback, another keyring namespace, or a newly constructed provider cannot stand in for that owner. The provider must authenticate a bounded whole-profile allocation inventory before handing out any recovered allocation. Each inventory entry binds its original allocation identity, scope, provider identity and protected record; serialized references and directory names confer no authority. Missing, unknown, conflicting or unauthenticated entries fail closed. A previously completed handoff cannot be interpreted as a fresh empty profile after loss of its inventory.

Birth, first decision and negative retirement are durable, ordered transitions under the selected namespace lock. A birth is acknowledged only when its exact protected bytes and inventory binding can be recovered together after a crash. The first positive or negative decision is immutable; replay of the same decision is idempotent, while an opposite or byte-different decision fails. Negative retirement requires that original negative decision and returns an acknowledgment only after a recoverable tombstone denies live reads. An interruption between credential-store and inventory publication must be reconciled from authenticated original intent, never by generating a new allocation, discarding an unknown credential, or treating a partial write as success. Native provider failures remain typed and retain their original cause.

The credential store and profile inventory are separate durability domains. Their implementation must prove crash recovery across every interleaving and must not assume that a credential-store write is an atomic transaction with a profile file. A provider acknowledgment states only its documented local persistence contract; it does not prove erasure from backups or resistance to rollback of the complete local profile and credential namespace.

Participant envelope ownership across runtime consumers

A participant package's version selects its canonical authenticated decoder. Legacy version 1 binds authority, epoch and participant; allocation version 2 also requires the original selected-provider allocation custody. Retained setup verification and threshold-signing retrieval use that same decoder. A consumer cannot reinterpret an allocation envelope as a legacy package, accept raw package bytes as envelope evidence, or discard the concrete codec/provider failure while selecting an alternate identity.

Protected initial lifetime publications retain recoverable target-bound staged ciphertext through process death. Recovery requires the original physical owner, authenticated ciphertext and independently retained original lifecycle binding before acknowledgment. Once-live target loss cannot be repaired from an old stage; conflicting first-decision evidence is retained and rejected.

Original invitation transfer signer

A non-enrollment invitation transfer and its issuer response use the original locally retained physical signing identity. Its binding includes the original invitation identifier, recipient, context, creation time, canonical public payload, physical device, signing epoch and verifier. The binding is retained from fresh issuance before publication and is immutable. Restart and rotation recovery validate the original binding and exact original private package. Missing original evidence is a required failure; recovery cannot select an active replacement or infer an epoch from a peer-supplied public key. The retained identity selects signing material and does not authorize a response decision or establish current membership. Enrollment transfer remains governed by its separately pinned manifest and original-window authorization.

Required invitation response cryptography

Canonical invitation response transcripts distinguish evaluated invalid signatures from cryptographic provider failures. Required signing, verification and response encoding failures preserve their original error source; provider failure does not prove that a response is invalid or absent.

Selected-provider initialization inventories staged entries throughout its bounded record tree before allocating original lifetime evidence. Inventory memory and\nstructural depth are bounded; ordinary record count is not clamped. Only target-bound initialization candidates at their exact retained parent are eligible for subsequent cryptographic validation; names alone never authorize publication. Unknown staged evidence is retained and rejects initialization. Root handoff requires an exhausted stage inventory. A publication conflict discovered after observation retains the original ciphertext and native conflict cause.

A post-link original publication can temporarily have exactly two names for one private ciphertext inode. Recovery recognizes that pair only at the exact original target and matching stage, verifies its original owner evidence and bytes, acknowledges the target, then removes the stage. Other aliases and missing once-live targets do not authorize restoration. Ordinary required readers remain unaliased; this exception is private to original initialization.

Required transcript codec failures

Required local invitation signature boundaries retain the canonical transcript codec cause through a process-local error chain. The required encoder preserves the existing domain/schema/payload wire envelope; encoding failure occurs before signing or verification. Invalid signature results remain distinct from a failed cryptographic provider invocation.

Required invitation import validity uses the selected physical-time provider and the canonical expiration boundary: an invitation is expired when now >= expiry. A failed required observation preserves its original provider cause and cannot produce a validated import, persist an invitation, or authorize subsequent issuance or publication. An observational clock fallback cannot satisfy this required validity check. Physical expiration remains local validity evidence, never distributed ordering or renewed ceremony time.

Native authentication challenge issuance and signed-response verification require the selected physical-time provider. Provider failures retain their native causes. An issuance clock failure cannot create a pending challenge; failed required verification cannot publish an authenticated result or fact. The original signed expiry is excluded from the validity interval, consistently with authentication guards and views; retries cannot replace that endpoint with a newly constructed window.

Guardian recovery key reads require the original private and public pair. A missing half or a mismatched pair cannot authorize replacement. Fresh allocation and required reads share the actual runtime's exclusive keypair lease, and fresh allocation publishes its identity capability only after both storage writes acknowledge. This lease does not itself establish restart authority for an interrupted fresh allocation or distinguish complete historical key loss from an unused profile; those require separate durable lifetime evidence.

Original initialization successor custody

Interrupted initial checkpoint publication may complete only the original empty Preparing to Ready, Ready to Handed, and protected lifecycle Preparing to Handed transitions. Eligibility requires the actual selected profile owner, original immutable birth and phase-dependent seals. Observed ciphertext grants no mutation authority. Exposed allocations, pending decisions, foreign owners, or missing original proof prevent promotion.

Before cutover, a bounded authenticated journal retains both exact original ciphertexts and physical inode identities. Acknowledged predecessor and successor custody precedes atomic exchange. Exchange preserves any displaced current target; conflicting source/target evidence is never deleted as repair. Success requires both installed and displaced identities to match, directory acknowledgment, and no-replace archival of original evidence. Historical transaction records remain authenticated against the original birth; they cannot authorize live checkpoint restoration or a new root. Ordinary secure records keep their existing alias rules; only closed private initialization custody admits the additional retained links.

Recovery of mutable checkpoints after allocation exposure and a builder execution window around native profile IO are separate required contracts.

Ready validation authenticates each archived journal and then requires its exact original and successor ciphertexts at the retained predecessor, successor and displaced paths, with the original device/inode identities. Same ciphertext under a foreign inode is rejected. Custody paths without an authenticated active or archived journal fail closed; native alias layout alone does not authorize readiness.

Required archived-custody validation also rejects ciphertext corruption at each of the three retained paths, preserving the original birth and current root checkpoint bytes without replacement.

Runtime quorum custody

Possession of retained dealer shares does not authorize a runtime to manufacture a quorum. A raw signing context cannot establish distributed signing ownership. Required local key material is validated before an unavailable quorum owner is reported; malformed and missing material remain distinct native failures. Each admitted distributed signing participant controls its own share and one-use nonce.

Explicit enrollment transcript quorum

Current enrollment signing intent version 4 declares five ordered domains: the exact trust manifest, public version 4 invitation transport, initial version 2 enrollment Request control transcript, original issuer return mailbox statement, and finite negative terminal policy. The first four are initiation signature domains. The return statement binds the approved manifest and a public retrieval-credential commitment; the credential remains in issuer custody. Initial Request fields derive from that manifest and its transcript digest. The version 1 policy binds the same manifest digest and exactly Rejected, Cancelled, TimedOut, ChoreographyFailed, RuntimeFailed and Superseded. Public validation checks exact version, domain order, manifest, transport, initial Request and return-mailbox binding; unsupported or substituted declarations cannot gain consent.

The policy is conditional consent, not an initiation signature or evidence that an outcome occurred. Only the original runtime owner may combine its actual protected first negative decision with retained approved participant custody to sign the matching version 2 Failed control, with no committed operations. Committed controls require their separate original protected positive decision and participant custody. Neither policy grants arbitrary transcript signing, durable membership, current receiver freshness or reconstructed native custody.

The public coordinator accepts the actual typed security transcript. Its canonical required encoding must equal the original approved domain bytes before a round starts. Manifest version selection and native codec causes remain intact; raw message bytes cannot construct this signing policy.

Aggregate verification retains an active typed authority threshold key derived from the independently approved native public package and epoch. Enrollment verification retains its original sealed final inventory, issued manifest or retained generation; copied verifier bytes cannot substitute for that owner.

Each active physical participant retains only its own protected share and one-use nonce. Packet authentication proves possession of the exact individual verifying share from independently authenticated current ordered public material; it is not a whole-authority signature or user consent. Aggregate signatures must verify against the independently retained current group package. Each approved transcript domain has distinct immutable approval/nonce retirement evidence.

Confirmed imported key activation

The original signed imported share and pending configuration remain immutable. Confirmed activation retains a distinct immutable encrypted envelope, binding its original protected receipt, physical device, subject, epoch, manifest digest, share commitment and exact pending configuration. Its birth is recorded before publication; loss after birth cannot create a replacement nonce or envelope. Reactivation acknowledges the same reverified envelope. Final agreement is derived from the confirmed generation without changing the original signed configuration. Corrupt or missing original evidence fails closed.

Confirmed import wrapping secrets have managed allocation lifetime ownership. Their scope version 2 binds the original verified receipt's manifest digest, subject, physical device, epoch, ceremony, invitation and exact share commitment. Birth, read and positive sealing require that genuine original confirmation; a permanent legacy wrapping key cannot substitute for this custody. An existing original allocation prohibits replacement birth even if envelope publication was interrupted before its separate birth anchor was published.

Enrollment proposal purpose binding

Device epoch proposal transcript version 2 uses domain aura.sync.device-epoch.proposal.v2. Enrollment purpose binds the exact original manifest digest and enrolling device, separately from the existing recipient device. Rotation and Removal are distinct purposes. The authenticated proposal also binds its participant, epoch, key-package/configuration/public-package hashes and encrypted-package binding. A valid signature for another purpose, manifest or enrolling device cannot authorize this enrollment. Individual participant possession proofs remain distinct from authority quorum signatures and original user approval.

Identifiers and Boundaries

This reference defines the identifiers that appear in Aura documents. Every other document should reuse these definitions instead of restating partial variants. Each identifier preserves structural privacy by design.

1. Authority Identifiers

2. Context Identifiers

3. Communication Identifiers

4. Content Identifiers

5. Journal Identifiers

6. Consensus Identifiers

7. Social Topology Identifiers

8. Tree Identifiers

9. Ceremony and Recovery Identifiers

10. Membership Identifiers

11. Accountability Structures

Receipt

Receipt is the accountability record emitted by FlowGuard. It contains context, source authority, destination authority, epoch, cost, nonce, chained hash, and signature. Receipts prove that upstream participants charged their budget before forwarding. No receipt includes device identifiers or user handles.

Fields: ctx: ContextId, src: AuthorityId, dst: AuthorityId, epoch: Epoch, cost: FlowCost, nonce: FlowNonce, prev: Hash32, sig: ReceiptSig.

See Transport and Information Flow for receipt propagation.

12. Derived Keys

Aura derives per-context cryptographic keys from reduced account state and ContextId. Derived keys never surface on the wire. They only exist inside effect handlers to encrypt payloads, generate commitment tree secrets, or run DKD.

The derivation inputs never include device identifiers. Derived keys inherit the privacy guarantees of AuthorityId and ContextId. The derivation function uses derive(account_root, app_id, context_label) and is deterministic but irreversible.

See Also

Authority and Identity describes the authority model in detail. Relational Contexts covers cross-authority relationships. Transport and Information Flow documents receipt chains and flow budgets. Social Architecture defines homes and neighborhoods.

Authority and Identity

This document describes the architecture of authorities and identity in Aura. It defines the authority model, account state machine, commitment tree structure, and relational identity model. Identity emerges through shared contexts rather than as a global property of keys.

1. Authority Model

An authority is a cryptographic actor represented by a public key. An authority hides its internal structure. An authority may contain one or more devices. An authority is the smallest unit that can sign facts or capabilities.

An authority has an internal journal namespace. The journal namespace stores facts relevant to that authority. The authority derives its state from deterministic reduction of that fact set.

Devices are not exclusive to a single authority. A single device may hold threshold shares for multiple authorities at the same time. Joining a new authority adds signing capability for that authority without removing any existing authority memberships.

1.1 Authority Types and Membership Terms

Aura uses three authority types:

• User: individual authority
• Home: group authority that accepts User authorities as members
• Neighborhood: group authority that accepts Home authorities as members

Home membership terminology is:

• Member: authority in the home's threshold authority set
• Participant: authority granted access to the home without threshold membership
• Moderator: optional designation granted to a member for moderation operations

AuthorityId (see Identifiers and Boundaries) selects the journal namespace associated with the authority. The identifier does not encode structure or membership. The authority publishes its current public key and root commitment inside its own journal.

Authorities can interact with other authorities through Relational Contexts. These interactions do not change the authority's internal structure. The authority remains isolated except where relational state is explicitly shared.

2. Account Authorities

An account authority is an authority with long term state. An account maintains device membership through its commitment tree. An account contains its own journal namespace. An account evolves through attested operations stored as facts.

The commitment tree defines device membership and threshold policies. The journal stores facts that represent signed tree operations. The reduction function reconstructs the canonical tree state from the accumulated fact set.

An account authority exposes a single public key derived from the commitment tree root. The authority never exposes device structure. The account state changes only when an attested operation appears in the journal.

Aura supports multiple key generation methods for account authorities. K1 uses single-signer local key generation. K2 uses dealer-based DKG with a trusted coordinator. K3 uses quorum/BFT DKG with consensus-finalized transcripts. These are orthogonal to agreement modes (A1 provisional, A2 coordinator soft-safe, A3 consensus-finalized). Durable shared authority state must be finalized via A3.

#![allow(unused)]
fn main() {
pub trait Authority: Send + Sync {
    fn authority_id(&self) -> AuthorityId;
    fn public_key(&self) -> Ed25519VerifyingKey;
    fn root_commitment(&self) -> Hash32;
    async fn sign_operation(&self, operation: &[u8]) -> Result<Signature>;
    fn get_threshold(&self) -> u16;
    fn active_device_count(&self) -> usize;
}
}

The Authority trait provides the external interface for authority operations. The trait exposes only the public key, root commitment, and signing capabilities. The internal device structure remains hidden from external consumers.

An account authority derives context specific keys using deterministic key derivation. These derived authorities represent application scoped identities. See Effects and Handlers Guide for implementation examples.

3. Account State Machine

The TreeState structure represents the materialized state of an account at a specific epoch.

#![allow(unused)]
fn main() {
pub struct TreeState {
    pub epoch: Epoch,
    pub root_commitment: TreeHash32,
    pub branches: BTreeMap<NodeIndex, BranchNode>,
    pub leaves: BTreeMap<LeafId, LeafNode>,
    leaf_commitments: BTreeMap<LeafId, TreeHash32>,
    tree_topology: TreeTopology,
    branch_signing_keys: BTreeMap<NodeIndex, BranchSigningKey>,
}
}

The epoch field is monotonically increasing. The root_commitment is the hash of the entire tree structure. The branches map stores branch nodes by index. The leaves map stores leaf nodes by ID.

The leaf_commitments map caches leaf commitment hashes. The tree_topology tracks parent-child relationships. The branch_signing_keys map stores FROST group public keys for verification.

For the authority-internal reducer implementation (AuthorityTreeState), topology is explicitly materialized as ordered binary edges with parent pointers. Active leaves are canonically sorted by LeafId, paired in stable order, and assigned deterministic branch indices (NodeIndex(0) root, then breadth-first). This allows path-local commitment recomputation for non-structural updates while preserving deterministic replay semantics.

TreeState is derived state and is never stored directly in the journal. It is computed on-demand from the OpLog via the reduction function.

#![allow(unused)]
fn main() {
pub struct TreeStateSummary {
    epoch: Epoch,
    commitment: Hash32,
    threshold: u16,
    device_count: u32,
}
}

The TreeStateSummary provides a public view with only epoch, commitment, threshold, and device count. This summary hides internal device structure for external consumers while the full TreeState is used for internal operations.

4. Commitment Tree Structure

A commitment tree contains branch nodes and leaf nodes. A leaf node represents a device or guardian inside the account. A branch node represents a subpolicy with threshold requirements. The root node defines the account-level threshold policy.

Node Kinds

#![allow(unused)]
fn main() {
pub enum NodeKind {
    Leaf(LeafNode),
    Branch,
}
}

This type defines leaf and branch variants. The Leaf variant contains a LeafNode with device information. The Branch variant is a marker indicating an internal node.

Leaf and Branch Nodes

#![allow(unused)]
fn main() {
pub struct LeafNode {
    pub leaf_id: LeafId,
    pub device_id: DeviceId,
    pub role: LeafRole,
    pub public_key: LeafPublicKey,
    pub meta: LeafMetadata,
}

pub enum LeafRole {
    Device,
    Guardian,
}
}

The LeafNode structure stores device information required for threshold signing. The leaf_id is a stable identifier across tree modifications. The device_id identifies the device within the authority. The role distinguishes devices from guardians.

#![allow(unused)]
fn main() {
pub struct BranchNode {
    pub node: NodeIndex,
    pub policy: Policy,
    pub commitment: TreeHash32,
}
}

The BranchNode structure stores policy data for internal nodes. The node field is the branch index. The policy defines the threshold requirement. The commitment is the cryptographic hash of the branch structure.

#![allow(unused)]
fn main() {
pub struct BranchSigningKey {
    pub group_public_key: [u8; 32],
    pub key_epoch: Epoch,
}
}

A BranchSigningKey stores the FROST group public key for threshold signing at a branch node. The key_epoch tracks when the key was established via DKG. Signing keys are updated when membership changes under the branch or when policy changes affect the signing group.

5. Tree Topology

The TreeTopology structure tracks parent-child relationships for efficient navigation.

#![allow(unused)]
fn main() {
pub struct TreeTopology {
    parent_pointers: BTreeMap<NodeIndex, NodeIndex>,
    children_pointers: BTreeMap<NodeIndex, BTreeSet<NodeIndex>>,
    leaf_parents: BTreeMap<LeafId, NodeIndex>,
    root_node: Option<NodeIndex>,
}
}

The parent_pointers map links nodes to their parents. The children_pointers map links parents to their children. The leaf_parents map links leaves to their parent branches. The root_node tracks the root of the tree.

This structure enables efficient path-to-root traversal and affected node computation during commitment updates.

graph TD
    R["Root Commitment<br/>(policy)"]
    L1["Branch<br/>(threshold)"]
    L2["Branch<br/>(threshold)"]
    A["Leaf A<br/>(device)"]
    B["Leaf B<br/>(device)"]
    C["Leaf C<br/>(guardian)"]
    D["Leaf D<br/>(device)"]

    R --> L1
    R --> L2
    L1 --> A
    L1 --> B
    L2 --> C
    L2 --> D

Each node commitment is computed over its ordered children plus its policy metadata. The root commitment is used in key derivation and verification. Leaves represent device shares. Branches represent threshold policies.

6. Policies

A branch node contains a threshold policy. A policy describes the number of required signatures for authorization.

#![allow(unused)]
fn main() {
pub enum Policy {
    Any,
    Threshold { m: u16, n: u16 },
    All,
}
}

The Any policy accepts one signature from any device under that branch. The Threshold policy requires m signatures out of n devices. The All policy requires all devices under the branch.

Policies form a meet semilattice where the meet operation selects the stricter of two policies.

#![allow(unused)]
fn main() {
impl Policy {
    pub fn required_signers(&self, child_count: usize) -> Result<u16, PolicyError> {
        match self {
            Policy::Any => Ok(1),
            Policy::All => Ok(child_count as u16),
            Policy::Threshold { m, n } => {
                if child_count as u16 != *n {
                    return Err(PolicyError::ChildCountMismatch { expected: *n, actual: child_count as u16 });
                }
                Ok(*m)
            }
        }
    }
}
}

The required_signers method derives the concrete threshold from the policy given the current child count. It returns an error if the child count does not match the policy's expected total. This is used during signature verification to determine how many signers must have participated.

7. Tree Operations

Tree operations modify the commitment tree. Each operation references a parent epoch and parent commitment. Each operation is signed through threshold signing.

#![allow(unused)]
fn main() {
pub enum TreeOpKind {
    AddLeaf { leaf: LeafNode, under: NodeIndex },
    RemoveLeaf { leaf: LeafId, reason: u8 },
    ChangePolicy { node: NodeIndex, new_policy: Policy },
    RotateEpoch { affected: Vec<NodeIndex> },
}
}

The AddLeaf operation inserts a new leaf under a branch. The RemoveLeaf operation removes an existing leaf with a reason code. The ChangePolicy operation updates the policy of a branch. The RotateEpoch operation increments the epoch for affected nodes and invalidates derived context keys.

#![allow(unused)]
fn main() {
pub struct TreeOp {
    pub parent_epoch: Epoch,
    pub parent_commitment: TreeHash32,
    pub op: TreeOpKind,
    pub version: u16,
}
}

The TreeOp structure binds an operation to its parent state. The parent_epoch and parent_commitment prevent replay attacks. The version field enables protocol upgrades.

#![allow(unused)]
fn main() {
pub struct AttestedOp {
    pub op: TreeOp,
    pub agg_sig: Vec<u8>,
    pub signer_count: u16,
}
}

The agg_sig field stores the FROST aggregate signature. The signer_count records how many devices contributed. The signature validates under the parent root commitment. Devices refuse to sign if the local tree state does not match.

8. Tree Operation Verification

Tree operations use a two-phase verification model that separates cryptographic verification from state consistency checking.

8.1 Cryptographic Verification

The verify_attested_op function performs cryptographic signature checking only.

#![allow(unused)]
fn main() {
pub fn verify_attested_op(
    attested: &AttestedOp,
    signing_key: &BranchSigningKey,
    threshold: u16,
    current_epoch: Epoch,
) -> Result<(), VerificationError>;
}

Verification checks that the signer count meets the threshold requirement. It computes the binding message including the group public key. It verifies the FROST aggregate signature. Verification is self-contained and can be performed offline.

8.2 State Consistency Check

The check_attested_op function performs full verification plus TreeState consistency.

#![allow(unused)]
fn main() {
pub fn check_attested_op<S: TreeStateView>(
    state: &S,
    attested: &AttestedOp,
    target_node: NodeIndex,
) -> Result<(), CheckError>;
}

Check verifies the operation cryptographically. It ensures the signing key exists for the target node. It validates that the operation epoch and parent commitment match state.

An imported operation is admissible only when its parent-epoch verifying key and threshold policy have authenticated provenance independent of the operation being imported. A device with no local parent key must first receive an authenticated enrollment baseline and its verifier chain. Import validates each operation against the previous reduced state and rejects the complete uncommitted batch if any signature, parent binding, or transition is invalid. Duplicate operations may be treated idempotently; peer-supplied keys cannot establish the trust anchor.

8.3 TreeStateView Trait

#![allow(unused)]
fn main() {
pub trait TreeStateView {
    fn get_signing_key(&self, node: NodeIndex) -> Option<&BranchSigningKey>;
    fn get_policy(&self, node: NodeIndex) -> Option<&Policy>;
    fn child_count(&self, node: NodeIndex) -> usize;
    fn current_epoch(&self) -> Epoch;
    fn current_commitment(&self) -> TreeHash32;
}
}

This trait abstracts over TreeState for verification. It enables verification without a direct dependency on the journal crate.

8.4 Binding Message Security

#![allow(unused)]
fn main() {
pub fn compute_binding_message(
    attested: &AttestedOp,
    current_epoch: Epoch,
    group_public_key: &[u8; 32],
) -> Vec<u8>;
}

The binding message contains a domain separator, parent epoch and commitment for replay prevention, protocol version, current epoch, group public key, and serialized operation content. Including the group public key ensures signatures are bound to a specific signing group.

8.5 Error Types

Verification produces two error categories. VerificationError covers cryptographic issues: missing signing keys, insufficient signers, signature failures, epoch mismatches, and parent commitment mismatches. CheckError covers state consistency issues: verification failures, key epoch mismatches, and missing nodes or policies.

9. Reduction and Conflict Resolution

The account journal is a join semilattice. It stores AttestedOp facts. All replicas merge fact sets using set union. The commitment tree state is recovered using deterministic reduction.

Reduction applies the following rules. Group operations by parent state using ParentKey (epoch + commitment tuple). Select a single winner using a deterministic ordering based on operation hash. Discard superseded operations. Apply winners in parent epoch order.

Conflicts arise when multiple operations reference the same parent epoch and commitment. The reduction algorithm resolves conflicts using a total order on operations. The winning operation applies. Losing operations are ignored.

The reduction algorithm builds a DAG from operations, performs topological sort with tie-breaking, and applies operations sequentially to build the final TreeState.

Conflict resolution uses operation hash as the tie-breaker. When multiple operations share the same parent, they are sorted by hash and the maximum hash wins. This ensures deterministic winner selection across all replicas.

graph TD
    OpLog["OpLog<br/>(CRDT OR-set of AttestedOp)"]
    Verify["verify_attested_op()"]
    Check["check_attested_op()"]
    Reduce["reduce()"]
    TreeState["TreeState<br/>(derived on-demand)"]

    OpLog -->|cryptographic| Verify
    Verify -->|state consistency| Check
    Check -->|valid ops| Reduce
    Reduce -->|derives| TreeState

This diagram shows the data flow from OpLog to TreeState. Operations are verified cryptographically first. Then they are checked for state consistency. Valid operations are reduced to produce the materialized TreeState.

10. Epochs and Derived Keys

The epoch is an integer stored in the tree state that scopes deterministic key derivation. Derived keys depend on the current epoch. Rotation invalidates previous derived keys. The RotateEpoch operation updates the epoch for selected subtrees.

Epochs also scope flow budgets and context presence tickets. All context identities must refresh when the epoch changes.

Derived context keys bind relationship data to the account state. The deterministic key derivation function uses the commitment tree root commitment and epoch. This ensures that all devices compute the same context keys. Derived keys do not modify the tree state.

11. Operators and Devices

An operator controls an authority by operating its devices. An operator is not represented in the protocol. Devices are internal to the authority and hold share material required for signing.

Devices produce partial signatures during threshold signing. The operator coordinates these partial signatures to produce the final signature.

The commitment tree manages device membership. The AddLeaf and RemoveLeaf operations modify device presence in the authority. Device identifiers do not appear outside the authority. No external party can link devices to authorities.

When a device is enrolled or replaced, Aura performs session delegation alongside tree updates. Runtime delegation transfers active protocol session ownership to the receiving device authority and records a SessionDelegation fact for auditability. The commitment tree update (AddLeaf/RemoveLeaf) remains the source of truth for membership, while delegation preserves in-flight protocol continuity during migration.

12. Relational Identity Model

Aura defines identity as contextual and relational. Identity exists only inside a specific relationship and does not exist globally. Authorities represent cryptographic actors rather than people. Identity emerges when two authorities form a shared context.

A shared context exists inside a relational context. A relational context stores relational facts that define how two authorities relate. Profile data may appear in a relational context if both authorities choose to share it. This profile data is scoped to that context.

ContextId (see Identifiers and Boundaries) identifies a relational context. It does not encode membership. It does not reveal which authorities participate. The context stores only the relational facts required by the participants.

Identity inside a context may include nickname suggestions or other profile attributes. These values are private to that context. See Identifiers and Boundaries for context isolation mechanisms. Nicknames (local mappings) allow a device to associate multiple authorities with a single local contact.

13. Authority Relationships

Authorities interact through relational contexts to create shared state. Relational contexts do not modify authority structure. Each relational context has its own journal. Facts in the relational context reference commitments of participating authorities.

Authorities may form long lived or ephemeral relationships. These relationships do not affect global identity. The authority model ensures that each relationship remains isolated.

graph TD
    A[Authority A] --> C(Context)
    B[Authority B] --> C(Context)

This diagram shows two authorities interacting through a relational context. The context holds the relational facts that define the relationship. Neither authority exposes its internal structure to the other.

14. Privacy and Isolation

Authorities reveal no internal structure and contexts do not reveal participants. Identity exists only where authorities choose to share information. Nicknames remain local to devices. There is no global identifier for people or devices.

Every relationship is private to its participants. Each relationship forms its own identity layer. Authorities can operate in many contexts without linking those contexts together.

15. Interaction with Consensus

Consensus is used when a tree operation must have strong agreement across a committee. Consensus produces a commit fact containing a threshold signature. This fact becomes an attested operation in the journal.

Consensus is used when multiple devices must agree on the same prestate. Simple device-initiated changes may use local threshold signing. The account journal treats both cases identically.

Consensus references the root commitment and epoch of the account. This binds the commit fact to the current state.

16. Security Properties

The commitment tree provides fork resistance. Devices refuse to sign under mismatched parent commitments. The reduction function ensures that all replicas converge. Structural opacity hides device membership from external parties.

The threshold signature scheme prevents unauthorized updates. All operations must be signed by the required number of devices. An attacker cannot forge signatures or bypass policies.

The tree design ensures that no external party can identify device structure. The only visible values are the epoch and the root commitment.

17. Implementation Architecture

17.1 Critical Invariants

The implementation enforces these rules.

1. TreeState is never stored in the journal. It is always derived on-demand via reduction.
2. OpLog is the only persisted tree data. All tree state can be recovered from the operation log.
3. Reduction is deterministic across all replicas. The same OpLog always produces the same TreeState.
4. DeviceId is authority-internal only. It is never exposed in public APIs.

17.2 Data Flow

graph TD
    A["Tree Operation Initiated"]
    B["TreeOperationProcessor validates"]
    C["Convert to AttestedOp fact"]
    D["Journal stores fact"]
    E["verify_attested_op (crypto)"]
    F["check_attested_op (state)"]
    G["reduce processes valid facts"]
    H["apply_operation builds TreeState"]
    I["TreeState materialized"]

    A --> B
    B --> C
    C --> D
    D --> E
    E --> F
    F --> G
    G --> H
    H --> I

This diagram shows the complete lifecycle of a tree operation from initiation to materialization.

17.3 Key Module Locations

Implementation files are in aura-journal/src/commitment_tree/.

• state.rs: TreeState structure and TreeStateView implementation
• reduction.rs: Deterministic reduction algorithm
• operations.rs: TreeOperationProcessor and TreeStateQuery
• application.rs: Operation application to TreeState
• compaction.rs: Garbage collection of superseded operations
• attested_ops.rs: AttestedOp fact handling

Verification code is in aura-core/src/tree/verification.rs. Type definitions are in aura-core/src/tree/types.rs and aura-core/src/tree/policy.rs.

See Also

• Journal System for fact semantics and reduction flows
• Relational Contexts for cross-authority relationship management
• Consensus for threshold signing and agreement
• Identifiers and Boundaries for context isolation mechanisms
• Cryptographic Architecture for FROST and signing modes
• Effects and Handlers Guide for practical implementation patterns
• Privacy and Information Flow for privacy guarantees

Enrollment roster decision custody

Device enrollment key generation is authorized by a held authenticated current-tree decision and the independently granted invitee setup. The physical issuer is a current Device member, the new device is not yet a member, and active signing epoch/configuration agree with the verified tree. The complete ordered signing roster and prestate are derived within generation-before-tree custody and retained through original issuer registration. Raw identifiers, participant vectors, observed tree state, and missing-current-device repair do not authorize rotation. A historical allocation can authorize negative secret retirement without conferring current live enrollment authority.

Bootstrap participant consistency

A new physical single-device authority bootstrap represents its sole signer as that actual Device participant and commits a matching signed Device genesis leaf. Authority identifiers and guardian participants do not substitute for physical membership. Historical guardian-labeled bootstrap configuration requires independently verified original genesis/device/key evidence before migration can confer physical signer representation; successful historical signing alone is insufficient enrollment authority.

Original enrollment reservation evidence

An enrollment reservation retains the original invitation identifier, subject, physical issuer device and creation time before signing generation allocation. The original immutable reservation is operation identity and clock evidence, not an enrollment authorization. Recovery eligibility requires the retained independent setup grant, original allocated window and generation, and authenticated current membership. Recovery cannot replace the original creation time or deadline with a later observation.

Enrollment setup validity attenuation

An issued enrollment manifest is bounded by its selected, independently verified setup grant. Its expiry must be strictly after that grant's issuance and no later than its expiry. Shortening validity is allowed; extending it is a typed SetupValidity rejection before signing. This bound complements the original registered execution interval and cannot renew that interval on retry or recovery.

Effect System

Overview

Aura uses algebraic effects to abstract system capabilities. Effect traits define abstract interfaces for cryptography, storage, networking, time, and randomness. Handlers implement these traits with concrete behavior. Context propagation ensures consistent execution across async boundaries.

This document covers effect trait design, handler patterns, and the context model. See Runtime for lifecycle management, service composition, and guard chain execution. See Ownership Model for the repo-wide Pure/MoveOwned/ActorOwned/Observed taxonomy.

The aura-agent runtime uses structured concurrency with explicit session ownership. Session-bound effects execute only under the current owner via canonical ingress. For complete details on async ownership, session ownership, typed runtime errors, and instrumentation policy, see crates/aura-agent/ARCHITECTURE.md.

The runtime contract is intentionally split:

• actor services supervise long-lived runtime structure
• move semantics govern session and endpoint ownership

Effect execution that touches session state belongs to the second category, not the first.

Typed Error Sources

Effect failures converted into AuraError retain their original concrete cause as the immediate standard std::error::Error::source. Cloning the error preserves that cause and its nested source chain. Shared storage of a cause does not add a wrapper node to the chain. Source objects are process-local: serialization keeps the error category and message and intentionally omits the source chain.

Native app/runtime boundaries preserve the same source contract. A RuntimeBridgeError carries a structural failure category and the actual underlying error; diagnostic wording cannot determine an idempotent success, retry, authorization result, or protocol confirmation. Foreign callback payloads explicitly omit process-local sources. Their diagnostic representation does not constitute native failure provenance and cannot reconstruct it.

Ownership At Effect Boundaries

Effect traits sit at an ownership boundary and should preserve the repo-wide ownership model rather than hide it.

• Effect trait definitions in aura-core are primarily Pure.
• Long-lived mutable async ownership belongs to ActorOwned runtime services, not to effect trait definitions or ad hoc handler-local state.
• Exclusive authority transfer belongs to MoveOwned handles, owner tokens, or transfer records rather than shared mutable rewrites.
• Effect handlers may implement capabilities, but parity-critical mutation and publication should remain capability-gated in the exposed API shape.

Practical implications:

• define trait methods so callers can preserve typed ownership and typed failure
• do not use effect handlers as a loophole for bypassing authority checks
• do not let observation-facing layers gain semantic mutation power through convenience helpers
• ensure long-running effect-driven flows report typed terminal outcomes rather than implicit success or silent hangs
• prefer the canonical aura-core ownership vocabulary at effect-facing boundaries:
  • OperationContext for move-owned workflow ownership
  • exact progress/terminal publication wrappers plus consumed TerminalPublisher for lifecycle
  • OwnedTaskSpawner, OwnedShutdownToken, and BoundedActorIngress for actor-owned task and ingress boundaries

Effect Traits

Aura defines effect traits as abstract interfaces for system capabilities. Core traits expose essential functionality. Extended traits expose optional operations and coordinated behaviors. Each trait is independent and does not assume global state.

Core traits include CryptoCoreEffects, NetworkCoreEffects, StorageCoreEffects, time domain traits, RandomCoreEffects, and JournalEffects. Extended traits include CryptoExtendedEffects, NetworkExtendedEffects, StorageExtendedEffects, RandomExtendedEffects, and system-level traits such as SystemEffects and ChoreographicEffects.

#![allow(unused)]
fn main() {
#[async_trait]
pub trait CryptoCoreEffects: RandomCoreEffects + Send + Sync {
    async fn ed25519_sign(
        &self,
        message: &[u8],
        private_key: &[u8],
    ) -> Result<Vec<u8>, CryptoError>;

    async fn ed25519_verify(
        &self,
        message: &[u8],
        signature: &[u8],
        public_key: &[u8],
    ) -> Result<bool, CryptoError>;

    async fn kdf_derive(
        &self,
        ikm: &[u8],
        salt: &[u8],
        info: &[u8],
        output_len: u32,
    ) -> Result<Vec<u8>, CryptoError>;
}
}

This example shows a core effect trait for cryptographic operations. Traits contain async methods for compatibility with async runtimes. Extension traits add optional capabilities without forcing all handlers to implement them. The hash() function is intentionally pure in aura-core::hash rather than an effect because it is deterministic and side-effect-free.

Time Traits

The legacy monolithic TimeEffects trait is replaced by domain-specific traits. PhysicalTimeEffects returns wall-clock time with uncertainty and provides sleep operations. LogicalClockEffects advances and reads causal vector clocks and Lamport scalars. OrderClockEffects produces opaque total order tokens without temporal meaning.

Callers select the domain appropriate to their semantics. Guards and transport use physical time. CRDT operations use logical clocks. Privacy-preserving ordering uses order tokens.

Cross-domain comparisons are explicit via TimeStamp::compare(policy). Total ordering across domains must use OrderTime or consensus sequencing. Direct SystemTime::now() or chrono usage is forbidden outside effect implementations.

Time Domain System

The unified TimeStamp type provides five domains for different use cases.

Application code accesses time exclusively through effect traits. Direct SystemTime::now() calls are forbidden outside effect implementations. Cross-domain comparisons require explicit TimeStamp::compare(policy). OrderClock must not leak timing information.

Timeout And Backoff Contract

Timeout and backoff behavior is part of the ownership model. Each parity-critical async path must identify a deadline owner, retry policy owner, and terminal consequence. See Effects and Handlers Guide for timeout patterns and Ownership Model for timeout ownership rules.

Threshold Signing

Aura provides a unified ThresholdSigningEffects trait in aura-core/src/effects/threshold.rs for all threshold signing scenarios. The trait supports multi-device personal signing, guardian recovery approvals, and group operation approvals.

The trait uses a unified SigningContext that pairs a SignableOperation with an ApprovalContext. This design allows the same FROST signing machinery to handle all scenarios with proper audit context. The ThresholdSigningService in aura-agent provides the production implementation.

Key components include ThresholdSigningEffects for async signing operations, lifecycle traits for provisional and consensus modes, and AppCore.sign_tree_op() for high-level signing. See Cryptography for detailed threshold signature architecture.

When to Create Effect Traits

New effect traits are warranted when multiple crates need the same async capability and the operation involves OS integration or external state. Convenience wrappers belong in composite extension traits rather than new base traits. See Effects and Handlers Guide for trait design guidance.

Database Effects

Database operations use existing StorageEffects, JournalEffects, and AuthorizationEffects rather than a dedicated DatabaseEffects trait. See Database Architecture for query patterns.

Handler Design

Handlers are stateless per-request processors. They do not store global state. The handler taxonomy includes stateless infrastructure handlers, application handlers, typed composite handlers, and type-erased composite handlers. See Effects and Handlers Guide for implementation patterns.

Unified Encrypted Storage

Aura uses StorageEffects as the single persistence interface in application code. The production runtime wires StorageEffects through a unified encryption-at-rest wrapper. FilesystemStorageHandler provides raw bytes persistence. RealSecureStorageHandler uses Keychain or TPM for master-key persistence.

EncryptedStorage implements StorageEffects by encrypting and decrypting transparently. It generates or loads the master key on first use. Runtime assembly remains synchronous.

#![allow(unused)]
fn main() {
use aura_effects::{
    EncryptedStorage, EncryptedStorageConfig, FilesystemStorageHandler,
    RealCryptoHandler, RealSecureStorageHandler,
};
use std::sync::Arc;

let secure = Arc::new(RealSecureStorageHandler::with_base_path(base_path.clone()));
let storage = EncryptedStorage::new(
    FilesystemStorageHandler::from_path(base_path.clone()),
    Arc::new(RealCryptoHandler::new()),
    secure,
    EncryptedStorageConfig::default(),
);
}

This example shows the encryption wrapper assembly. RealCryptoHandler lives in aura-effects and implements CryptoCoreEffects. Storage configuration controls encryption enablement and opaque naming. Application code uses StorageEffects without knowledge of encryption details.

Context Model

The effect system propagates an EffectContext through async tasks. The context carries authority identity, context scope, session identification, execution mode, and metadata. No ambient state exists.

#![allow(unused)]
fn main() {
pub struct EffectContext {
    authority_id: AuthorityId,
    context_id: ContextId,
    session_id: SessionId,
    execution_mode: ExecutionMode,
    metadata: HashMap<String, String>,
}
}

This structure defines the operation-scoped effect context. The context flows through all effect calls and identifies which authority, context, and session the operation belongs to. The execution_mode controls handler selection for production versus test environments.

Context propagation uses scoped execution. A task local stores the current context. Nested tasks inherit the context. This ensures consistent behavior across async boundaries.

ReactiveEffects Trait

The ReactiveEffects trait provides type-safe signal-based state management. Signals are phantom-typed identifiers that reference reactive state. The phantom type ensures compile-time type safety.

#![allow(unused)]
fn main() {
pub struct Signal<T> {
    id: SignalId,
    _phantom: PhantomData<T>,
}

#[async_trait]
pub trait ReactiveEffects: Send + Sync {
    async fn read<T>(&self, signal: &Signal<T>) -> Result<T, ReactiveError>
    where T: Clone + Send + Sync + 'static;

    async fn emit<T>(&self, signal: &Signal<T>, value: T) -> Result<(), ReactiveError>
    where T: Clone + Send + Sync + 'static;

    fn subscribe<T>(&self, signal: &Signal<T>) -> Result<SignalStream<T>, ReactiveError>
    where T: Clone + Send + Sync + 'static;

    async fn register<T>(&self, signal: &Signal<T>, initial: T) -> Result<(), ReactiveError>
    where T: Clone + Send + Sync + 'static;

    async fn ensure_registered<T>(&self, signal: &Signal<T>, initial: T) -> Result<(), ReactiveError>
    where T: Clone + Send + Sync + 'static;
}
}

The read method returns the current value. The emit method updates the value. The subscribe method returns a stream of changes. The register method creates a new signal and rejects a duplicate ID. ensure_registered creates a missing signal while preserving the value and subscriptions of a matching existing signal; a different value type under the same ID is an error. See Runtime for reactive scheduling implementation. Subscribing an unregistered signal fails fast. Aura does not permit "dead stream" subscription success for missing registrations.

QueryEffects Trait

The QueryEffects trait provides typed Datalog queries with capability-based authorization. Queries implement the Query trait which defines typed access to journal facts.

#![allow(unused)]
fn main() {
pub trait Query: Send + Sync + Clone + 'static {
    type Result: Clone + Send + Sync + Default + 'static;

    fn to_datalog(&self) -> DatalogProgram;
    fn required_capabilities(&self) -> Vec<QueryCapability>;
    fn dependencies(&self) -> Vec<FactPredicate>;
    fn parse(bindings: DatalogBindings) -> Result<Self::Result, QueryParseError>;
    fn query_id(&self) -> String;
}

#[async_trait]
pub trait QueryEffects: Send + Sync {
    async fn query<Q: Query>(&self, query: &Q) -> Result<Q::Result, QueryError>;
    async fn query_raw(&self, program: &DatalogProgram) -> Result<DatalogBindings, QueryError>;
    fn subscribe<Q: Query>(&self, query: &Q) -> QuerySubscription<Q::Result>;
    async fn check_capabilities(&self, caps: &[QueryCapability]) -> Result<(), QueryError>;
    async fn invalidate(&self, predicate: &FactPredicate);
}
}

The Query trait converts queries to Datalog programs and defines capability requirements. The QueryEffects trait executes queries and manages subscriptions. Query isolation levels control consistency requirements. See Database Architecture for complete query system documentation.

A query-bound signal is active only after its initial query and signal emission succeed. Failed binding leaves no partial query subscription; retry keeps any existing signal value and subscribers and installs the binding once the query succeeds.

Determinism Rules

Effect boundaries determine native and WASM conformance parity. Protocol code must follow these rules to ensure deterministic execution.

The pure transition core requires identical outputs given the same input stream. No hidden state may affect observable behavior. All state must flow through explicit effect calls. Non-determinism is permitted only through explicit algebraic effects. Time comes from time traits. Randomness comes from RandomEffects. Storage comes from StorageEffects.

Conformance lanes compare logical steps rather than wall-clock timing. Time-dependent behavior uses simulated time through effect handlers. Conformance artifacts use canonical encoding with deterministic field ordering. See Testing Guide for conformance testing patterns.

Session-Local VM Bridge Effects

Production choreography execution uses a narrow synchronous bridge trait at the Aura and Telltale boundary. VmBridgeEffects in aura-core exposes only immediate session-local queue and snapshot operations. It does not expose async transport, storage, or journal methods.

This split exists because Telltale host callbacks are synchronous. The callback path may enqueue outbound payloads, record blocked receive edges, consume branch choices, and snapshot scheduler signals. It must not perform network I/O or journal work directly.

Async host work resumes outside the VM step boundary in Layer 6 runtime services. vm_host_bridge observes VmBridgeEffects state, performs transport and guard-chain work, and injects completed results back into the VM. This preserves deterministic VM progression while keeping Aura's runtime async.

aura-agent runtime code preserves this boundary through canonical ingress and explicit session ownership. Network callbacks, timers, and background tasks route typed session-ingress messages to the current local owner. Each active session has exactly one owner at any time.

That owner may be hosted by an actor, but the effect-routing rule is still ownership-based: session-bound effects execute because the caller is the current owner, not merely because it runs inside a service actor.

The runtime must also distinguish owner identity from owner capability:

• owner identity identifies the current fragment/session owner
• owner capability authorizes specific session-bound effects within fragment scope

Both checks matter for effect routing, especially across delegation boundaries.

See System Internals Guide for VM bridge implementation patterns and crates/aura-agent/ARCHITECTURE.md for the complete ownership model.

Layer Placement

The effect system spans several crates with strict dependency boundaries. aura-core defines effect traits, identifiers, and core data structures. It contains no implementations.

aura-effects contains stateless and single-party effect handlers. It provides default implementations for cryptography, storage, networking, and randomness. aura-protocol contains orchestrated and multi-party behavior. It bridges session types to effect calls.

aura-agent assembles handlers into runnable systems. It configures effect pipelines for production environments. aura-simulator provides deterministic execution with simulated time, networking, and controlled failure injection.

Performance

Aura includes several performance optimizations. Parallel initialization reduces startup time. Caching handlers reduce repeated computation. Buffer pools reduce memory allocation. The effect system avoids OS threads for WASM compatibility.

#![allow(unused)]
fn main() {
let builder = EffectSystemBuilder::new()
    .with_handler(Arc::new(RealCryptoHandler))
    .with_parallel_init();
}

This snippet shows parallel initialization of handlers. The builder pattern allows flexible handler composition. Lazy initialization creates handlers on first use. Async tasks and cooperative scheduling provide efficient execution.

Testing Support

The effect system supports deterministic testing through mock handlers. A simulated runtime provides control over time and network behavior. The simulator exposes primitives to inject delays or failures.

#![allow(unused)]
fn main() {
let system = TestRuntime::new()
    .with_mock_crypto()
    .with_deterministic_time()
    .build();
}

This snippet creates a test runtime with mock handlers for all effects. It provides deterministic time and network control. Tests use in-memory storage and mock networking to execute protocols without side effects. See Test Infrastructure Reference for test patterns.

Local timeout failure identity

Local budget failures distinguish policy rejection, clock unavailability, deadline expiry, and attempt exhaustion. A required clock failure remains observable through the standard error source chain and cannot be treated as deadline evidence. Native clock causes are omitted from serialized diagnostic errors. The local timeout result retains operation failures as distinct typed causes.

Storage profile exclusivity and immutable publication

Profile storage ownership is a move-owned infrastructure lease covering one physical profile lifetime. It does not authorize domain actions. Cooperative persistent writers require the same profile owner; unsupported exclusivity is a typed failure. Resource release on cancellation or process death permits a new owner, whose durable recovery still requires authenticated domain evidence.

Immutable secure publication has two outcomes: Created acknowledges complete encrypted and durable publication; AlreadyExists identifies an existing record without proving equality or trust. Publication does not replace existing bytes. A failure after publication can leave a complete record, so recovery validates the original stored record rather than assuming rollback. Backends without these transactional guarantees report unsupported semantics explicitly. Multi-record profile handoff requires a separately owned durable transaction and recovery contract; a runtime mutex or several atomic file replacements do not establish that contract.

The selected production provider's private concrete lease, rather than an arbitrary core trait implementation, establishes physical profile ownership. Persistent writer clones retain that resource owner. Browser ownership is scoped to the actual origin and storage namespace through Web Locks; immutable records require strict-durability IndexedDB transaction completion. Historical plaintext secret namespaces cannot authorize fresh signing-state creation. Shared platform credential namespaces need their own supported ownership contract; filesystem-profile ownership does not substitute for it.

Local timeout observation contract

A local timeout owner preserves its original deadline and the greatest required physical-clock observation across awaited operations, timer completion, retries, and child deadlines. Physical-clock rollback terminates that owner as a required service failure; it does not extend its allowance or imply deadline expiration. Observation contention is an ownership failure. Successful timer completion latches exhaustion. Persisted timeout state must include and validate the original window, observation, rollback, and exhaustion state; missing state cannot reconstruct an active allowance.

Window coordinate separation

Physical timeout intervals and receipt-generation intervals share checked half-open arithmetic with distinct sealed coordinate types. A coordinate cannot cross domains. A valid interval alone grants no observation, admission or persistence authority. Physical execution windows have positive millisecond extent and a fixed representable deadline; empty generation allowances admit no receipts. Restored owner state must preserve its original bound interval and observation history.

Required enhanced-time scheduling propagates actual provider query and sleep failures. A failed timer does not constitute deadline expiration or successful wake-up. Native source traversal retains the concrete time-effect error through runtime scheduling and effect-system forwarding.

VM bridge delivery custody

Synchronous VM callbacks enqueue frames; asynchronous transport delivery requires an exclusive VmBridgeSendLease. Queue snapshots are observations and do not remove frames. The lease retains the oldest frame through the awaited send and removes it only after acknowledgment. Concurrent enqueue preserves FIFO order, and a second delivery owner fails explicitly. Providers without this contract reject owned delivery instead of emulating it by draining a queue.

Dropping an in-flight lease retains the frame with an unknown delivery outcome. Unknown delivery blocks automatic replay; it requires protocol reconciliation or terminal session teardown. A native definitely-unsent result may release the frame for an owned retry. Display text cannot establish that result. These states are local delivery custody, not peer consensus or durable receipt proof.

Required choreography clock and timeout effects preserve their native source through ChoreographyError::RequiredTime. Failed clock reads do not provide timestamps or expiry evidence. Session cleanup remains required when its clock observation fails; the runtime retains both primary and secondary typed failures.

Secure storage distinguishes atomic initial publication of mutable owner state (secure_create_mutable) from lifetime-immutable evidence (secure_store_immutable). Both preserve an existing record and acknowledge a new publication; an interrupted call requires rereading the actual original. Atomic creation alone does not authorize later mutation or generation renewal. Providers without the atomic-create contract return a typed unsupported failure.

Secure publication classes

Secure storage distinguishes atomic initial mutable publication from lifetime immutable publication. Both preserve an existing original. Mutable records permit subsequent updates under their domain owner. Immutable records carry authenticated provider protection in the same atomic publication and reject generic replacement, deletion, and key-generation writes. Legacy sealing preserves the exact original bytes. A capability list or caller-supplied retirement label cannot override lifetime protection. Unsupported providers fail with a typed error. Interrupted writes have an uncertain publication outcome; successful retries validate and acknowledge the original record. Ordinary storage has no authority over the secure provider's physical subtree.

An enrollment mailbox record may acquire a retirement birth only in its first immutable publication. The birth must be authorized by the original approved issuer registration under its independently retained baseline and setup proof, and bound to the actual selected profile provider, exact record location and bytes, and the registration's signed expiry. A later registration, raw signed bytes, self-certified signer package, or caller-selected expiry cannot amend an existing immutable record. Issuer credential and setup records published before the registration is signed require separate original birth authority; the registration cannot retroactively authorize their deletion.

Required secure retrieval reports an absent record through a typed logical absence cause with the exact requested location. This differs from a provider I/O failure, whose concrete native cause remains intact. Observational existence checks may report false; required absence cannot authorize replacement keys, default signing policy or a weaker record selection.

The crypto extended effect exposes individual participant-key proof signing separately from authority threshold signing. A handler that lacks this primitive returns a typed unsupported cause; it cannot fabricate a proof or substitute a group signature. The stateless handler signs the supplied actual package, while the runtime owner supplies current-device/epoch/ceremony authorization.

Required runtime construction adapters preserve native initialization causes in both production and testing/simulation presets. Returning-profile authorization failure cannot be converted into a flat runtime diagnostic or treated as fresh credential absence. Serialized presentation remains separate from the native source chain used to diagnose the failing provider or verification boundary.

Fixed window attenuation and restore

A physical timeout window may be narrowed to an earlier authenticated deadline while preserving its original start and clock observation owner. Attenuation does not observe a synthetic timestamp, allocate a new allowance, or modify the original interval. A child retains its own sticky exhaustion; parent and child share high-water and rollback evidence. Restoring a child requires the exact attenuated bounds and matching acknowledged clock history. It must preserve exhaustion and cannot enlarge either deadline.

These pure continuity checks do not establish checkpoint provenance or runtime admission. The domain owner must authenticate the policy, retain actual custody, and acknowledge the original and attenuated snapshots through its required checkpoint path. Generation/epoch windows do not authorize physical expiry.

Selected-provider allocation custody

Allocation references are observations, not authority. A selected physical profile owner transfers opaque whole-inventory custody before runtime sharing. Provider transitions dispatch through the retained original backend and preserve actual storage, codec and cryptographic failures. Recovery may complete an acknowledged pre-live birth using its original retained evidence. Missing once-live allocation or checkpoint evidence fails closed. Unsupported selected providers fail structurally; provider substitution does not repair custody.

Selected provider migration contract

A legacy selected profile may adopt allocation lifetime custody only through its original exclusive physical provider owner and original retained decryption material. Required bounded inventory authentication precedes immutable root birth acknowledgment. Existing permanent secret policy and ciphertext are preserved. The independently acknowledged completed-handoff evidence prevents missing live checkpoint data from being treated as a new or unmigrated profile. Recovery retains original allocation identity and first-decision history; a serialized locator grants no recovery authority.

A provider acknowledgment confirms its transactional persistence contract. It does not attest physical media erasure, external backup deletion, or absence of a complete rollback of all local evidence.

Selected provider continuity

An explicitly configured effect provider remains the source of its required operations after shared runtime ownership transfer. Shared crypto handles preserve extended operations as well as core operations; shared ownership cannot substitute optional defaults for the selected implementation. Required provider faults retain their original cause across persistence, journal and network adapter boundaries. Such faults do not authorize implicit selection of a default provider. Ordinary storage customization preserves encrypted storage and the independent selected secure profile's lifetime custody.

Required invitation transcript encoding and Guardian cryptographic calls retain process-local native error sources. A verified invalid signature is a boolean rejection; codec failure or selected cryptographic provider failure is a typed error and cannot be converted into absence or a successful response. Native sources are local diagnostic evidence, not serialized protocol authority.

Newly composed diagnostics and retained causes

A diagnostic category and message contain no causal provenance or mutation authority. Attaching a native failure to a new diagnostic preserves the original concrete standard error and its existing source chain. Existing cause-bearing errors and terminal outcomes are not converted to source-free diagnostics or overwritten by a later cause. Cloning a cause-bearing error preserves its original native source identity.

Deterministic entropy admission

A production assembly rejects an explicit deterministic entropy seed before acquiring profile custody or invoking configured providers. Simulated cryptographic handlers and deterministic random streams require a private seed capability admitted from the actual nonproduction execution mode. Selecting a custom cryptographic handler does not bypass this admission decision.

Absolute physical deadline observations

PhysicalTimeEffects::wait_until_physical_deadline accepts a WindowPosition<PhysicalMillis> for an existing fixed endpoint. Its successful result is an actual selected-provider observation at or beyond that endpoint. It neither allocates a new window nor proves domain completion. Registration must not depend on an awaited caller clock read or a caller's cached timestamp. The selected provider owns timer cancellation and preserves native clock/timer failures. A provider lacking this contract returns AbsoluteDeadlineUnsupported; it cannot silently substitute a relative sleep. Native error sources are process-local and are omitted from serialized diagnostics.

Terminal resource acknowledgment requires the original observation lease, required current time, window validation and checkpoint to complete within the same absolute endpoint. Expiry or provider failure cannot publish success. A fixed-endpoint witness can latch expiry without a second awaited clock read. Domain owners retain responsibility for the actual manager/task/disposal proof.

Runtime

Overview

The Aura runtime assembles effect handlers into working systems. It manages lifecycle, executes the guard chain, schedules reactive updates, and exposes services through AuraAgent. The AppCore provides a unified interface for all frontends.

This document covers runtime composition and execution. See Effect System for trait definitions and handler design. See Ownership Model for the repo-wide ownership taxonomy. The aura-agent crate-level runtime contract, including structured concurrency, canonical ingress, ownership, typed errors, and CI policy gates, lives in crates/aura-agent/ARCHITECTURE.md.

That contract is intentionally opinionated about the split of responsibilities:

• actor services own long-lived runtime supervision, lifecycle, and maintenance
• move semantics own session and endpoint ownership transfer

Those are related concerns, but they are not the same abstraction boundary.

For shared semantic operations, the split is stricter still:

• aura-app::workflows owns authoritative semantic lifecycle publication
• aura-agent owns long-lived runtime actors and readiness/state coordination
• frontend crates and the harness submit through sanctioned handoff boundaries and observe authoritative publication afterward

No runtime, frontend, or harness path should keep a parallel terminal publication helper once the shared workflow owner has taken over.

The same visibility rule applies to runtime-owned mutation helpers. Raw VM admission helpers, fragment ownership registry mutation, and the mutable reconfiguration controller stay inside aura-agent runtime internals. Shared consumers go through sanctioned ingress, session-owner, or manager surfaces.

Enrollment setup export belongs to the signing runtime owner. Device identity, key epoch, mode, policy and package are one coherent snapshot; frontend or harness identity staging cannot substitute for this snapshot. The runtime verifies and retains the signed request before returning its code. Export failures preserve typed time, readiness, admission, proof and storage causes across the app's runtime bridge. Signing recovery preserves prior verifier identity and fails closed on incomplete persisted material, as specified in Cryptography.

Signing-material preparation, activation, recovery and rollback have one serialized lifecycle owner. Activation validates the prospective context and local membership before persisting the active epoch and exposing the context. An active or historical epoch cannot be rolled back as a failed pending rotation. Existing pending material cannot be silently replaced by a second preparation for the same epoch.

Bootstrap publishes its signing context only after genesis completion. Its pending/complete record is independent of the active key epoch, so persisted keys cannot turn a failed tree commit into readiness on retry. A cached tree operation without its persisted operation and index entry is insufficient completion evidence. Legacy migration requires an existing authenticated creation witness; restoration cannot silently recreate a missing lineage.

Adaptive Privacy Runtime Ownership

Adaptive privacy policy is runtime-owned local state, not shared truth.

• the Neighborhood Plane and Web of Trust Plane provide permit and candidate inputs
• rendezvous descriptor views provide service-surface advertisement inputs
• SelectionManagerService fuses those inputs with local health and budget signals into runtime-local LocalSelectionProfile and SelectionState
• LocalHealthObserverService owns smoothing, hysteresis, and local health snapshots
• MoveManager owns bounded movement queues, replay windows, flush scheduling, congestion state, and the current routing profile used for MoveEnvelope delivery
• HoldManager owns held-object custody, selector rotation, bounded holder residency, local Hold GC, verified witness handling, and neighborhood-scoped provider scoring
• AnonymousPathManager owns reusable anonymous established-path lifecycle and protected encrypted establish-session state
• CoverTrafficGeneratorService owns cover-floor planning and reserved cover budget

This split is strict:

• final route, holder, and path reuse decisions are runtime-local
• those decisions must not be published as authoritative facts or descriptor fields
• retrieval, cover, accountability replies, and ordinary movement share one MoveEnvelope family where applicable rather than regaining separate transport families

The production adaptive policy is fixed by deployment rather than user configuration. The current fixed policy uses path-diversity floor 2, cover floor 2 packets per second, delay gain denominator 3, neighborhood hold retention window 120s, and retrieval-capability rotation beginning 10s before expiry. Development and simulation may tune those values, but production nodes do not expose per-user privacy knobs.

LocalRoutingProfile::passthrough() remains the pre-privacy baseline. It uses mixing depth 0, delay 0, cover rate 0, and path diversity 1. Hold remains active under passthrough because custody and selector retrieval are availability services rather than privacy-profile parameters.

Transparent Onion Quarantine

transparent_onion is a debug, test, and simulation tool only.

• it may expose transparent anonymous setup and envelope headers for inspection
• the production runtime path is encrypted; transparent objects exist only on the explicit debug/simulation feature surface
• it must remain excluded from parity-critical harness and shared-flow lanes
• production policy ownership does not change when the feature is enabled
• the feature must not become an implicit dependency of browser, TUI, or conformance behavior

Ownership Categories In The Runtime

The runtime is the main place where Aura's ownership categories become concrete:

• long-lived runtime services, supervisors, readiness coordinators, and caches are ActorOwned
• session, endpoint, and delegation transfer surfaces are MoveOwned
• runtime views, projections, and exported state are Observed
• reducers, validators, and typed contracts remain Pure

Two runtime rules follow from that split:

1. Actor mailboxes are for mutation of actor-owned state, not as a substitute for move-style ownership transfer.
2. Runtime-facing lifecycle and readiness publication should be capability-gated and should terminate explicitly with typed success, failure, or cancellation.
3. Long-lived mutable async domains should be declared through #[aura_macros::actor_owned(...)], and small parity-critical runtime lifecycle enums should prefer #[aura_macros::ownership_lifecycle(...)] over hand-written transition helpers.

Instrumentation Contract

All long-lived runtime services emit structured events from the following families: runtime startup/shutdown, service lifecycle transition, task spawn/completion/failure/abort, session claim/release/failure, ingress accepted/rejected/dropped, delegation start/commit/rollback/reject, link boundary route/reject, concurrency profile select/fallback, and invariant violation.

Required fields include service, task, session_id, fragment_key, owner, from_owner, to_owner, profile, error_kind, and correlation_id where applicable. These families ensure that runtime behavior is reconstructible from structured logs. Envelope admission, delegation witnesses, and fallback decisions must all be visible in instrumentation output.

Structured Concurrency

aura-agent uses structured concurrency as the only production async model.

Rules:

• Every long-lived async subsystem has one named owner.
• Every owner has one rooted task group.
• Child tasks belong to exactly one task group.
• Detached fire-and-forget tasks are forbidden in production runtime code.
• Shutdown is hierarchical and parent-driven.

Runtime shutdown ordering remains an orchestration-level invariant, not a compile-time type property. Aura keeps a targeted integration check for the final shutdown sequence in aura-agent::runtime::system:

1. stop the reactive pipeline
2. cancel the runtime task tree
3. tear down services
4. shut down the lifecycle manager

That check is governance for the final runtime owner graph, not a replacement for the compile-time ownership model.

See System Internals Guide for implementation patterns and preferred primitives.

Lifecycle Management

aura-agent uses an explicit service lifecycle contract with authoritative service states, structured task ownership, and deterministic teardown. The crate-level runtime contract in crates/aura-agent/ARCHITECTURE.md is the source of truth.

All long-lived services implement a shared lifecycle state machine:

• new: Initial state before startup.
• starting: Initialization in progress.
• Running: Actor alive and command path available.
• stopping: Graceful shutdown in progress.
• Stopped: No live owned tasks and no live command handling.
• Failed: Observable failure state.

Long-lived runtimes periodically prune caches and stale in-memory state through owned service actors and supervised task groups. Domain crates expose cleanup APIs but do not self-schedule. The agent runtime owns the scheduling model.

Required periodic work terminates with typed success, failure, or cancellation. A timer or callback failure remains a failed task with its concrete source and must be observable through owning service health and drain. An invalid interval policy fails before invoking domain work. Intentional callback completion is distinct from a failed callback. Supervisor clock failures are distinct from observed drain deadline expiry.

Task-group supervision covers descendants even after callers drop their group handles. Shutdown closes admission across the owned subtree before waiting; late submissions cannot schedule work. Forced abort requests cancellation but does not establish drain. Task registrations remain active until the owned future and its resources have actually dropped. Descendant failures propagate to ancestor health and retain their original cause. Group depth, live groups and active tasks have explicit admission bounds; dead group entries are pruned.

See System Internals Guide for service lifecycle implementation.

Runtime Timeout Policy

A choreography receive owns its local deadline for the lifetime of that receive future. Inbox notifications cannot renew it, and dropping the future leaves no registered timer resource. Required clock and sleep observations determine expiry through the shared typed timeout budget. A zero configured receive timeout remains immediate when no matching message is already queued.

Choreography session admission requires a successful physical clock read before installing session state or task bindings. A failed read is a typed required-time failure with its original source; zero is not substitute clock evidence. Session retirement removes owned session resources even if its required clock read fails. The clock failure remains primary, and any retirement failure is retained as a separate typed cause. Duration metrics are updated only when the required observation exists. Receive-timeout issuance and waiting preserve native time-effect causes through the choreography error boundary.

Runtime timeout behavior must preserve Aura's time-system contract:

• physical time drives local waiting, retry, and backoff policy
• logical, order, and provenanced time remain semantic ordering tools
• runtime owners publish typed timeout failure when local waiting is exhausted
• required clock and backoff failures retain their actual cause and remain distinct from deadline expiry; an unavailable clock cannot fabricate an observed deadline or authorize timeout retry
• pending invitation lookup errors remain required failures even when observed pending or accepted history exists; history recovery requires a typed readiness exhaustion outcome, and clock or policy failures cannot select it
• runtime-to-app deadline errors retain the typed deadline cause through the standard error source chain; semantic observers classify deadlines from that cause rather than matching display text
• harness and simulation may scale timeout policy, but they should not invent a different semantic model

In practice this means:

• long-lived owners should consume a remaining timeout budget across nested stages instead of resetting fresh wall-clock literals at each call site
• enrollment retries and child VM attempts remain bounded by the ceremony's original deadline; restoration does not grant a new acceptance window
• retry loops should use shared backoff policy rather than duplicated sleeps
• timeout policy belongs to owner/coordinator code, not UI observation layers
• reducing timeout duration in tests or harness mode is acceptable. Changing what timeout means is not.
• runtime-facing workflow/task boundaries should carry OperationTimeoutBudget, OwnedShutdownToken, and OwnedTaskSpawner rather than raw Duration, raw cancellation traits, or ad hoc spawn helpers
• parity-critical runtime waits should consume strong typed authoritative references once context is known. They must not re-derive ownership or context from weaker ids inside later readiness/wait helpers.

Runtime Authority Discipline

Runtime-owned coordinators follow the same authority rule as app workflows:

• resolve authoritative typed input once at the boundary
• carry that typed input through later parity-critical readiness, retry, and terminal steps
• do not re-resolve context from raw ids after authoritative handoff
• do not keep fallback/default repair helpers on parity-critical paths

If a later step needs context, the API should require the strong typed reference rather than accepting a raw identifier and looking it up again.

Guard Chain Execution

The runtime enforces guard chain sequencing defined in Authorization. Each projected choreography message expands to three phases. First, snapshot preparation gathers capability frontier, budget headroom, and metadata. Second, pure guard evaluation runs synchronously over the snapshot. Third, command interpretation executes the resulting effect commands.

flowchart LR
    A[Snapshot prep] -->|async| B[Guard eval]
    B -->|sync| C[Interpreter]
    C -->|async| D[Transport]

This diagram shows the guard execution flow. Snapshot preparation is async. Guard evaluation is pure and synchronous. Command interpretation is async and performs actual I/O.

GuardSnapshot

The runtime prepares a GuardSnapshot immediately before entering the guard chain. It contains every stable datum a guard may inspect while remaining read-only.

#![allow(unused)]
fn main() {
pub struct GuardSnapshot {
    pub now: TimeStamp,
    pub caps: Cap,
    pub budgets: FlowBudgetView,
    pub metadata: MetadataView,
    pub rng_seed: [u8; 32],
}
}

Guards evaluate synchronously against this snapshot and the incoming request. They cannot mutate state or perform I/O. This keeps guard evaluation deterministic, replayable, and WASM-compatible.

EffectCommands

Guards do not execute side effects directly. Instead, they return EffectCommand items for the interpreter to run. Each command is a minimal description of work.

#![allow(unused)]
fn main() {
pub enum EffectCommand {
    ChargeBudget {
        context: ContextId,
        authority: AuthorityId,
        peer: AuthorityId,
        amount: FlowCost,
    },
    AppendJournal { entry: JournalEntry },
    RecordLeakage { bits: u32 },
    StoreMetadata { key: String, value: String },
    SendEnvelope {
        to: NetworkAddress,
        peer_id: Option<uuid::Uuid>,
        envelope: Vec<u8>
    },
    GenerateNonce { bytes: usize },
}
}

Commands describe what happened rather than how. Interpreters can batch, cache, or reorder commands as long as the semantics remain intact. This vocabulary keeps the guard interface simple.

EffectInterpreter

The EffectInterpreter trait encapsulates async execution of commands. Production runtimes hook it to aura-effects handlers. The simulator hooks deterministic interpreters that record events instead of hitting the network.

#![allow(unused)]
fn main() {
#[async_trait]
pub trait EffectInterpreter: Send + Sync {
    async fn execute(&self, cmd: EffectCommand) -> Result<EffectResult>;
    fn interpreter_type(&self) -> &'static str;
}
}

ProductionEffectInterpreter performs real I/O for storage, transport, and journal. SimulationEffectInterpreter records deterministic events and consumes simulated time. This design lets the guard chain enforce authorization, flow budgets, and journal coupling without leaking implementation details.

Reactive Scheduling

The ReactiveScheduler in aura-agent processes journal facts and drives UI signal updates. It receives facts from multiple sources including journal commits, network receipts, and timers. It batches them in a 5ms window and drives all signal updates.

Intent → Fact Commit → FactPredicate → Query Invalidation → Signal Emit → UI Update

This flow shows how facts propagate to UI. Services emit facts rather than directly mutating view state. The scheduler processes fact batches and updates registered signal views. This eliminates dual-write bugs where different signal sources could desync.

Signal Views

Domain signals are driven by signal views in the reactive scheduler. ChatSignalView, ContactsSignalView, and InvitationsSignalView process facts and emit full state snapshots to their respective signals.

The six observed entity projections (chat, contacts, homes, invitations, recovery, and neighborhood) have one typed publication path through aura-app::ProjectionOwner. A synchronous delta updates the current graph value atomically and returns the committed value with a source revision. A full replacement derived from an earlier snapshot must compare that revision before publication; stale replacements do not emit. Failed deltas leave the graph value unchanged. AppCore copies a projection into ViewState only when its source revision is newer than the last copy, so a delayed refresh cannot regress the render snapshot.

App-owned navigation transitions that pair a homes selection with a neighborhood position share a gate with the homes mirror. The mirror revalidates the homes source revision after reconciliation and retries when a runtime publication arrives during the transition. The gate serializes local paired transitions; runtime publications remain graph-owned and are reconciled at the next mirror pass.

#![allow(unused)]
fn main() {
// Define application signals
pub static CHAT_SIGNAL: LazyLock<Signal<ChatState>> =
    LazyLock::new(|| Signal::new("app:chat"));

// Bind signal to query at initialization
pub async fn register_app_signals_with_queries<R: ReactiveEffects>(
    handler: &R,
) -> Result<(), ReactiveError> {
    handler.register_query(&*CHAT_SIGNAL, ChatQuery::default()).await?;
    Ok(())
}
}

This example shows signal definition and query binding. Signals are defined as static lazy values. They are bound to queries during initialization. When facts change, queries invalidate and signals update automatically.

Fact Processing

The scheduler integrates with the effect system through fact sinks. Facts flow from journal commits through the scheduler to signal views.

#![allow(unused)]
fn main() {
// In RuntimeSystem (aura-agent)
effect_system.attach_fact_sink(pipeline.fact_sender());

// The scheduler processes fact batches and updates signal views.
}

Terminal screens subscribe and automatically receive updates. This enables push-based UI updates without polling.

UnifiedHandler

The UnifiedHandler composes Query and Reactive effects into a single cohesive handler. It holds a QueryHandler, a shared ReactiveHandler, and an optional capability context.

The commit_fact method adds a fact and invalidates affected queries. The query method checks capabilities and executes the query. BoundSignal<Q> pairs a signal with its source query for registration and invalidation tracking.

Service Pattern

The runtime uses a three-tier service architecture. Domain crates define stateless handlers that produce pure GuardOutcome plans without performing I/O. The agent layer wraps these handlers with services that gather snapshots, run guard evaluation, and interpret effect commands. The agent exposes services through typed accessor methods on AuraAgent, with a ServiceRegistry holding Arc references initialized at startup.

See System Internals Guide for the handler/service/API implementation pattern.

Session Management

The runtime manages the lifecycle of distributed protocols. Choreographies define protocol logic. Sessions represent single stateful executions of choreographies. The runtime uses structured concurrency with explicit session ownership.

Session Ownership

Each active session or fragment has exactly one current local owner. The owner is either a per-session actor or an authoritative choreography runtime loop. This invariant is enforced through the canonical ingress pattern.

This is the move-semantics side of the runtime model:

• one current owner
• explicit transfer
• stale-owner rejection
• owner-routed session effects

Owner identity and capability are separate:

• ownership says who currently controls the fragment
• capability says what fragment-scoped work that owner may perform

Network, timer, and external events are queued before touching session state. Session ownership and task ownership move together. Session-bound effects execute only under the current owner.

The owner may be implemented by an actor, but the transfer of ownership is still an explicit move boundary rather than shared actor state.

See Choreography Development Guide for session ownership implementation.

Ownership Transitions

Owner-visible state transitions:

• Unowned -> Claimed
• Claimed -> Running
• Running -> DelegatingOut
• DelegatingOut -> Released
• Running -> Stopping
• Stopping -> Stopped
• Any -> Failed

No transition may create overlapping owners.

Session Interface

The SessionManagementEffects trait provides the abstract interface for all session operations. Application logic remains decoupled from the underlying implementation. Sessions can use in-memory or persistent state.

Session State

Concrete implementations act as the engine for the session system. Each session maintains:

• SessionId for unique identification.
• SessionStatus indicating the current phase.
• Epoch for coordinating state changes.
• Participant list.

Session creation and lifecycle are managed as choreographic protocols. The SessionLifecycleChoreography in aura-protocol ensures consistency across all participants.

Telltale Integration

Aura executes production choreography sessions through the Telltale protocol machine in Layer 6. Production startup is manifest-driven. Generated CompositionManifest metadata defines the protocol id, required capabilities, determinism profile reference, link constraints, and delegation constraints for each choreography. AuraChoreoEngine runs admitted protocol-machine sessions and exposes deterministic trace, replay, and envelope-validation APIs.

Aura is aligned with Telltale 10.0.0's public runtime model rather than a private compatibility surface. Runtime admission, canonical finalization, semantic handoff, and runtime-upgrade execution all use public protocol-machine concepts. Delegation witnesses now carry Telltale-native ownership receipts and post-upgrade reconfiguration snapshots rather than Aura-local transition wrappers. Fail-closed receipt and authority handling is explicit at Aura's runtime boundaries, and timeout expiry is modeled from issued timeout witnesses rather than from late elapsed-time inference. For the upstream capability/finalization/runtime-upgrade contract, read Telltale docs/38_capability_model.md.

Runtime ownership is fragment-scoped. One admitted protocol fragment has one local owner at a time. A choreography without link metadata is one fragment. A choreography with link metadata yields one fragment per linked bundle. Ownership claims, transfer, and release flow through AuraEffectSystem and ReconfigurationManager.

This is why the runtime uses both abstractions at once:

• actor services for host-side runtime structure
• explicit move-style ownership for fragment/session transfer

When delegation changes ownership, the runtime must also define whether the moved capability is transferred intact or attenuated to a narrower scope. That decision is part of the protocol/runtime contract, not a host-side convenience choice.

The synchronous callback boundary is VmBridgeEffects. AuraVmEffectHandler and AuraQueuedVmBridgeHandler use it for session-local payload queues, blocked receive snapshots, branch choices, and scheduler signals. Async transport, guard-chain execution, journal coupling, and storage remain outside protocol-machine callbacks in vm_host_bridge and service loops.

A received frame (BlockedVmReceive) is not Clone, and delivering it consumes it. The engine, not the caller, assigns each frame its inbound sequence: AuraChoreoEngine keeps one SequenceOwner per session edge, and that owner admits exactly the next sequence for each delivered frame. Replay-enforcing protocol profiles run Telltale in CommunicationReplayMode::Nullifier through the single seam protocol_replay_mode, so a duplicate frame faults as DuplicateIdentity. Fully deterministic profiles (which Telltale does not allow with nullifiers) enforce the engine-assigned per-edge sequence instead. Telltale 17 derives that nullifier with its built-in non-cryptographic model; Task 208 tracks a pluggable crypto-hash model.

Dynamic reconfiguration follows the same rule. Runtime code must go through ReconfigurationManager for link and delegation so bundle evidence, capability admission, and coherence checks are enforced before any transfer occurs.

Dynamic reconfiguration also carries typed upgrade artifacts end to end. When a delegation also performs a runtime upgrade, Aura persists the delegation fact, records the typed upgrade request/execution pair, and rejects missing source ownership or invalid upgrade evidence rather than repairing state implicitly.

Runtime Profiles

Telltale protocol-machine execution is configured through two profile axes:

• AuraVmHardeningProfile controls safety posture: Dev (assertions + full trace), Ci (strict allow-lists + replay), Prod (safety checks with bounded overhead).
• AuraVmParityProfile controls deterministic cross-target lanes: NativeCooperative (native baseline) and WasmCooperative (WASM lane), both using cooperative scheduling and strict effect determinism.

Determinism and scheduler policy are protocol-driven. Admission resolves the protocol class, applies the configured determinism tier and replay mode, validates the selected runtime profile, and chooses scheduler controls. Production code should not mutate these settings directly after admission.

Mixed workloads are allowed. Cooperative and threaded fragments may coexist in the same runtime. The contract is per fragment.

See System Internals Guide for VM configuration patterns.

Boundary Review Checklist

Changes to VM/Aura boundaries require review against the checklist in System Internals Guide.

Concurrency Profiles and Envelope Admission

aura-agent recognizes three runtime concurrency profiles for choreography work:

• Canonical: Exact single-owner reference path. Telltale canonical execution at concurrency n = 1 is the reference behavior.
• EnvelopeAdmitted: Disjoint or admitted work preserving safety-visible meaning. Higher concurrency is a refinement only when it stays inside the admitted envelope relation.
• Fallback: Immediate degradation to canonical execution when envelope admission fails.

Correctness never depends on uncontrolled host scheduling. If the runtime cannot show that a path is envelope-safe, it serializes execution.

Envelope Admission Contract

Operational envelope admission is a runtime gate, not a comment-level convention. The runtime must record and enforce:

• which determinism / concurrency profile was requested
• which evidence or certificate admitted the profile
• whether execution stayed canonical or entered an admitted refinement
• why fallback occurred when admission failed

Safety-visible observations must remain equivalent to the canonical reference. Every admitted step must have a declared witness path. Profile-side obligations must be checked before execution widens.

Link and Delegate Boundaries

Link Boundary

link is a static composition boundary. Linked bundles define ownership boundaries as well as composition boundaries. Linked protocols remain session-disjoint unless composition explicitly shares state. Cross-boundary effect routing is explicit. Ad hoc shared mutable state across linked boundaries is forbidden. link must preserve Telltale coherence and harmony obligations at runtime, not just compile-time compatibility.

A boundary object must carry enough information to answer:

• which bundle/fragment boundary this effect belongs to
• which owner capability scope is valid at that boundary
• whether a route crosses a boundary that requires explicit reconfiguration handling

Wrong-boundary routing is a runtime error and must be rejected before the VM observes the step.

Delegate Boundary

delegate is an ownership-transfer boundary. Endpoint/session ownership transfer is atomic. Capability/effect context transfers with the endpoint. Stale-owner access after delegation is forbidden. Ambiguous local ownership is rejected before the VM observes the transfer. Fragment ownership and session footprint state move with the transfer rather than lagging behind it.

Transfer and attenuation are separate concepts:

• transfer changes the authoritative owner
• attenuation narrows the capability scope that moves with the new owner

If the runtime cannot state which one is happening and under which protocol rule, it must reject the delegation path.

A successful delegation must move one owned bundle: session owner record, owner capability, protocol fragment ownership, runtime footprint / reconfiguration state, and delegation audit witness. If these do not move together, the transfer is incomplete and must be treated as a runtime error.

Theorem-pack / Invariant Alignment

The runtime must preserve coherence-sensitive session and edge state, harmony-sensitive reconfiguration steps, adequacy-relevant observable traces, determinism-profile obligations, and replay / communication identity stability across async ingress. Advanced runtime modes should be capability- and evidence-gated. Missing invariant evidence must cause rejection or fallback, never silent widening.

Fact Registry

The FactRegistry provides domain-specific fact type registration and reduction for reactive scheduling. It lives in aura-journal and is integrated via AuraEffectSystem::fact_registry(). Registered domains include Chat for message threading, Invitation for device invitations, Contact for relationship management, and Moderation for home and mute facts.

Reactive subscription policy is explicit:

• signal source revisions are distinct from frontend semantic and render revisions; exports observing the same graph compare source revisions directly, while independent LAN runtimes compare each export to its own AppCore source revision and require their entity sets to converge
• application signal setup ensures every required signal individually; retry after partial setup preserves registered values and subscriptions
• query-bound signal setup registers the same required signal set; a failed query binding leaves no partial binding and a later retry can attach it without resetting the signal
• runtime refresh hooks attach one receiver per required signal and acknowledge every listener's startup before reporting readiness; failure rolls back the group and permits retry with a typed reactive failure
• chat and recovery have initial replay mirrors during hook installation; the runtime recovery projection also has an owned listener that copies later RECOVERY_SIGNAL revisions into the app view, so exported snapshots converge after replay
• each attached signal has one owned refresh loop: it receives an update, completes one refresh pass, then receives again; a second task cannot race that signal's refresh or clear its pending work
• detaching an AppCore runtime cancels its hook group before another generation attaches
• subscribing to an unregistered signal fails fast with ReactiveError::SignalNotFound
• there is no implicit wait-for-registration or dead-stream fallback
• subscriber delivery is eventually consistent rather than lossless
• if a subscriber lags behind the bounded broadcast buffer, intermediate values may be dropped and the subscriber resumes from a newer snapshot after a lag warning is logged
• a refresh pass reads current authoritative state after its trigger; updates that arrive during the pass remain in the bounded stream, and the next receive runs another pass against current state even if intermediate snapshots were dropped

Production code obtains the registry via effect_system.fact_registry(). Tests may use build_fact_registry() for isolation. The registry assembly stays in Layer 6 rather than Layer 1.

See Effects and Handlers Guide for fact registration patterns.

Delivery Policy

The DeliveryPolicy trait enables domain crates to define custom acknowledgment retention and garbage collection behavior. This keeps policy decisions in the appropriate layer while the journal provides generic ack storage.

Domain crates implement the trait to control acknowledgment lifecycle. Key methods include min_retention and max_retention for time bounds, requires_ack to check tracking needs, and can_gc to determine GC eligibility.

#![allow(unused)]
fn main() {
let chat_policy = ChatDeliveryPolicy {
    min_retention: Duration::from_secs(30 * 24 * 60 * 60),
    max_retention: Duration::from_secs(90 * 24 * 60 * 60),
};
effect_system.register_delivery_policy("chat", Arc::new(chat_policy));
}

This example shows domain-specific retention configuration. Chat messages retain acks for 30 to 90 days. Different domains can have vastly different retention needs. The maintenance system uses registered policies during GC passes.

AppCore

The AppCore in aura-app provides a unified portable interface for all frontend platforms. It is headless and runtime-agnostic. It can run without a runtime bridge for offline or demo modes. It can be wired to a concrete runtime via the RuntimeBridge trait.

Architecture

AppCore sits between frontends and a runtime bridge.

flowchart TB
    subgraph Frontends
        A[TUI]
        B[CLI]
        C[iOS]
        D[Web]
    end
    A --> E[AppCore]
    B --> E
    C --> E
    D --> E
    E --> F[RuntimeBridge]
    F --> G[AuraAgent]

This diagram shows the AppCore architecture. Frontends import UI-facing types from aura-app. They may additionally depend on a runtime crate to obtain a concrete RuntimeBridge. This keeps aura-app portable while allowing multiple runtime backends.

Construction Modes

AppCore supports two construction modes: demo/offline mode (no runtime bridge, for development and testing) and production mode (wired to a concrete RuntimeBridge for full effect system capabilities).

See Hello World Guide for AppCore usage.

Reactive Flow

All state changes flow through the reactive pipeline. Services emit facts rather than directly mutating view state. UI subscribes to signals using signal.for_each(). This preserves push semantics and avoids polling.

Local Intent ───┐
                │
Service Result ─┼──► Fact ──► Journal ──► Reduce ──► ViewState
                │                                      │
Remote Sync ────┘                                      ↓
                                               Signal<T> ──► UI

This flow shows the push-based reactive model. Facts from any source flow through the journal. Reduction computes view state. Signals push updates to UI subscribers.

Runtime Access

When AppCore has a runtime, it provides access to runtime-backed operations through the RuntimeBridge trait. The runtime bridge exposes async capabilities while keeping aura-app decoupled from any specific runtime implementation. Frontends import app-facing types from aura-app and runtime types from aura-agent directly.

Enrollment restart and activation ownership

Enrollment recovery follows active signing-context restoration. Service startup alone does not establish signing readiness. An active enrollment retains its canonical invitation, original start time and deadline, participant inventory, prestate, setup binding, and exact pending signing-generation identity. Restoring those records does not establish acceptance. Original signed responses must be reverified against their retained setup verifier before an acceptance capability can be restored.

Activation owns one ceremony decision lease from its eligibility check through terminal settlement. Required durable preparation identifies the exact signed tree operation. Once irreversible preparation is retained, cancellation and timeout may not replace its owner; restart reconciles that exact operation and generation without adding a duplicate leaf. First terminal decisions are durably retained before becoming visible, and historical result observation grants no activation capability.

An enrollment allocation owns its reserved invitation identity before pending keys become visible. Completing registration establishes a process-local capability for launching the canonical initiator. Failed or unissued generation retirement retains the original decision, rejects already prepared activation, and releases the generation only after required key deletion succeeds. A historical retirement receipt permits observation of the original decision and never deletion of a later generation that reused its epoch.

Enrollment acceptance binds the original setup and the independently admitted signed trust manifest. Recovery selects the expected manifest and confirmation verifier from issuer-owned retention, revalidates the actual signed response at its original admission time, and does not deserialize an acceptance capability. Local serialization is not a guarantee of exclusive profile ownership between concurrent processes.

Durable enrollment time windows

Retirement after original enrollment cancellation requires the sealed original terminal decision, the same registered allocation and runtime, and the original authorized negative-cleanup window. Completed retirement writes remain in their original receipt destination before readiness is published, independently of later observation failure. This retention does not change signing authority or establish a full resource acknowledgment: that acknowledgment requires original-window validation and durable cleanup evidence.

Enrollment execution retains the original allocated local deadline and acknowledged clock history across retries and restart. A child allowance cannot replace its parent's durable window. Required clock observations and sticky failures are durably acknowledged before protocol progression or terminal result publication. Missing retained observation state is a required recovery failure. A reimport preserves its original admitted window. Historical completed evidence retains its immutable acknowledged window and cannot grant fresh protocol or signing authority.

An authentic rollback reported by the original selected provider's required timer irreversibly refuses positive execution under that budget. Returning the native timer failure preserves its concrete cause independently of the shared refusal history. Clones, child budgets and validated serialized recovery retain that history, including when snapshot access was contended; later forward time cannot renew the original allowance. Retaining local refusal does not establish durable acknowledgment or authorize a replacement cleanup window.

The original durable allocation birth records pending execution in the same bound clock record before handing out a usable root. Only the actual in-process birth acknowledgment transfers that nonserialized root custody. Initial provider time may establish the allocation deadline; no required observation of an existing window or potentially state-changing operation may precede the pending acknowledgment. Restart with pending state refuses positive execution; a previously usable budget cannot be restored across an unacknowledged observation. An uncertain, failed, or stalled allocation publication grants no usable root or semantic success. Nested children retain the same pending root and may persist its observation high-water mark, but cannot clear it.

Only the original move-owned root may settle pending execution. Positive settlement requires independent domain completion and actual disposal of its own sealed child subtree, followed by the original durable acknowledgment. The currently executing root task is outside that subtree. Task-group disposal is a repeatable observation, not root completion authority: cancelled, never-executed, failed, or incompletely cleaned-up children cannot establish positive completion. Dropping a bounded disposal observation retains the seal and pending root custody. Failure or endpoint exhaustion preserves refusal without allocating a new positive window or awaiting an unbounded post-expiry checkpoint.

Owned ceremony maintenance terminates with a typed failure when required clock, storage, or timer effects fail. Health projections may describe that outcome, while the runtime retains its original error source.

Native identity query failures

Required native identity and settings queries retain structural runtime failures and original IO/codec causes. Missing optional account configuration remains explicit absence; corruption cannot be interpreted as absence. Device inventory is derived from canonical device leaves, including a current device only when it is present there. Presentation contact counts and uninitialized threshold summaries do not prove runtime readiness.

Native failure projection

Native runtime error category survives workflow context wrapping. Required settings queries and mutations accept structural native errors at their workflow failure boundary; source-free diagnostic errors do not satisfy that contract. Foreign notification payloads preserve a stable native code at their terminal projection boundary. Crypto and serialization failures remain distinct from Internal; semantic failures classify them as failed commands rather than fabricated timeout or invalid argument evidence.

Native semantic failure codes

Native runtime crypto, serialization, storage, journal, and reactive failures have distinct semantic codes. Category-preserving workflow wrappers retain concrete error sources; foreign/shared operation snapshots retain the stable category code and operation domain. Generic crypto failure does not imply an authorization decision.

Shared window contracts and admission phases

Physical execution and receipt-generation allowance use domain-separated checked half-open interval arithmetic. Physical owners retain a fixed positive-millisecond deadline; flow owners retain authorized generation progression and current/previous epoch policy. Serialized interval bounds are arithmetic evidence only. They do not admit protocol execution or confer signing authority.

Enrollment allocation retains the original window before execution becomes live. An interrupted allocation can retain its missing initial clock only while neither immutable live-boundary evidence nor canonical registration evidence exists, and only from the exact secure original allocation. The immutable live-boundary marker precedes registry insertion. Once that boundary is retained, missing clock history is a required failure; recovery cannot reconstruct a duration or start from current time. A historical record can acquire missing live-boundary evidence only when its original secure allocation and clock both validate.

Checkpoint acknowledgment preserves exact allocation identity and the same shared clock and exhaustion owner. The durable maximum observation and sticky failures cannot regress. The registry retains allocation continuity through the required checkpoint write. Terminal decisions may advance for the same allocation; they do not authorize a renewed window, and historical completed evidence does not grant fresh execution.

Native account bootstrap failures

Account bootstrap never treats a failed configuration read as absent configuration. Required signing initialization propagates original native faults under its bounded operation window. Failure publication projects the native semantic category and returns the original error, preserving both failures if terminal publication itself fails. Account configuration and authority-record persistence remain separate writes and are not claimed as one transaction.

Selected-profile physical resource binding

An exclusively owned native filesystem profile binds its lifetime ownership to actual lock and directory resources. Every attached writer and clone retains that physical directory binding; changing process working directory or replacing a pathname cannot reauthorize a different directory. A filesystem secure provider admits its wrapping key only under the selected owner's physical directory and retains the original provider key. Invalid persisted key material fails closed without replacement.

Reads and mutations reject descendant directory aliases. Durable acknowledgment concerns the actual held data and directory resources. An interrupted or failed acknowledgment can leave an uncertain publication outcome and requires validation of the canonical record. These single-record guarantees do not imply atomicity across selected-profile metadata, enrollment handoff, admission receipts, and signing activation. That multi-record transition requires its own durable recovery owner.

Required timeout checkpoints preserve storage and codec causes in TimeoutBudgetError::CheckpointFailure. This failure does not represent clock unavailability or elapsed time. Native and semantic classification follows its retained cause; unclassified checkpoint faults remain internal. Serialized diagnostics omit native error sources and grant no checkpoint authority.

Required one-shot runtime work

Enrollment issuer cleanup retains the original accepted task control across cancelled or failed reconciliation. Once the exact cancelled generation is retired, any remaining resource reconciliation uses that same control and its original authorized negative-cleanup window. Actual reconciliation failure and final selected-provider validation remain independently required. Observing already completed resource disposal grants no positive domain completion or new execution authority.

Required owned tasks retain their concrete execution failure in supervisor health and drain. Terminal lifecycle settlement does not erase that failure. If terminal publication also fails, both causes remain available, with the original execution cause preserved in the standard error chain and the secondary publication cause retained as typed evidence.

Sync command service ownership requires source-preserving timer, shutdown-signal and runtime supervision outcomes. Every daemon run exit awaits service stop. Failed execution remains primary when stop also fails, with a separately retained typed cleanup cause. A failed timer or backward physical clock cannot publish a tick or successful shutdown. Native terminal diagnostics retain concrete sources; cloned source-bearing errors compare retained source identity rather than matching message text.

VM host send ownership

The runtime owns one exclusive pending-send lease per VM bridge flush. It marks a frame in flight immediately before the transport await, acknowledges only a successful send, and retains failed or unattempted frames in their original order. New callbacks enqueue behind retained frames. Cancellation or an ambiguous failure leaves an unknown delivery outcome and prevents automatic replay on that bridge. Configuration failure before delivery leaves frames pending. Native session-not-started and destination-unreachable failures occur before delivery and retain replay eligibility; retry still requires the protocol owner's original admitted time window and exact request contract.

Enrollment failure receipt ownership

An invitee publishes a failed enrollment readout only after verifying the issuer's pinned signed terminal control and acknowledging the original owned window checkpoint. The immutable failure receipt binds the exact manifest, invitation, ceremony, physical device, signed reason, and frozen acknowledged clock snapshot. Failure and confirmation receipts occupy distinct namespaces; contradictory receipts are rejected. Repeated reads revalidate the original admission and signed evidence without allocating another duration or issuing activation authority.

An issuer records rejection only from a verified refusal capability and under the same terminal decision gate as commitment and cancellation. The first persisted terminal decision is immutable. Closing the VM is required on both success and failure; a secondary close failure remains available structurally alongside the original execution error.

Parallel window observations

Parallel children of a physical timeout owner share observation ordering as well as the original high-water mark and expiry state. Each required physical read, its high-water update, and its durable acknowledgment form one owned sequence. A later query cannot overtake an earlier incomplete query and fabricate rollback from scheduling. Cancellation releases observation ownership; genuine backward clock movement remains a sticky failure and the original deadline is unchanged.

Required refresh failure ownership

Runtime-backed app refresh attachments retain their first source-bearing failure independently of instrumentation. Signal receipt, required refresh, and interval-provider failures have distinct typed stages, cancel the attachment, and fail runtime supervision. A failed attachment is not active readiness. Intentional attachment cancellation completes successfully. Reattachment cannot erase the enclosing runtime generation's retained supervision failure.

Bounded attempt teardown

Selecting a bounded-attempt timeout cancels the borrowed operation, while its owner retains the runtime resources needed for required teardown. The owner closes the actual VM before returning or retrying. Closing does not renew the operation window or authorize additional business work. A failed close remains a typed terminal task failure alongside the original execution cause.

Signed enrollment failure diagnostics

Native enrollment failures retain the verified terminal reason independently of flat foreign diagnostics and preserve the original typed standard error source. Rejected, cancelled, timed-out, choreography-failed, runtime-failed, and superseded outcomes have distinct semantic projections. A remote signed failure reason does not claim the original remote provider exception or grant retry, activation, membership, or adoption authority. Diagnostic text cannot reconstruct a reason or an authenticated terminal capability.

Live pending enrollment registration custody

An initial pending enrollment registration belongs to the still-held physical signing-generation reservation. Its bindings and participant policy must match that allocation, and it cannot inject accepted participants or a prior terminal decision. The registration must continue the immutable original allocation's start, deadline and budget observation history. Recovery uses independently revalidated original durable evidence rather than manufacturing a live reservation from stored identifiers.

Persistent enrollment allocation authorization

A held physical signing-generation reservation authorizes initial persistent enrollment allocation. Plain ceremony identifiers, policies or snapshots cannot substitute for that owner even when a reservation for the same generation exists. Generic guardian registration and nonpersistent state-model registration remain distinct from persistent enrollment admission. Verified recovery restores original evidence through its recovery owner and cannot reset the allocated lifetime through fresh generic registration.

Enrollment sender cancellation reads its required persisted sender record and the exact retained issued manifest. Guard preparation precedes the terminal CAS; local InvitationCancelled publication follows the actual durable Failed(Cancelled) first decision. A different first terminal decision cannot be changed, and a failed cancellation cannot publish a canceled invitation. The resulting negative capability is bound to that invitation and ceremony; it grants neither device membership nor profile activation. Cancellation preserves the original deadline and acknowledged clock observations, including sticky expiry and rollback. Required record, codec, guard, budget, and clock failures retain their native cause and cannot be interpreted as absence.

Before negative resource acknowledgment, the durable clock checkpoint retains the latest history of the original positive interval, including rollback detected after its earlier checkpoint write. The live history must continue the retained interval, highwater and sticky refusal evidence. Negative cleanup retains its separately born original budget; persistence and readback must succeed before acknowledgment. Reopening a terminal cancellation restores negative observations and cannot recreate positive execution authority.

Pre-live enrollment clock continuity

Recovery of a device enrollment allocation uses protected original allocation and signing-generation evidence under the same runtime generation owner. A ceremony identifier selects that original; caller state cannot replace its start, deadline, or observation history. Live admission must checkpoint eligibility against the original clock before publication and reject terminated or expired allocations. Clock and generation profiles are owned mutable records with atomic initial publication. First terminal and retirement decisions remain lifetime-protected immutable evidence; a competing decision cannot be overwritten during recovery.

Cancellation preparation consumes required sender-record custody and borrows retained issued control; observed invitation values cannot substitute. Both retain the exact native runtime owner. Guard-issued preparation and the tracker-issued negative terminal token must agree with the publication runtime, including when authority and physical device identifiers are equal. A different runtime cannot sign through borrowed control or publish its cancellation. The required regular sender-record decoder rejects records larger than 1 MiB before decoding; oversized and malformed data remain distinct typed failures.

Required sender enrollment custody combines the bounded regular record with its separately retained secure original payload. Secure reads, decoding and exact immutable metadata comparison must succeed before custody is minted; a redacted record alone cannot substitute. Only regular lifecycle status overlays the retained original. The regular decoder is bounded to 1 MiB and the retained secret decoder to 4 MiB. Cancellation status publication redacts the hydrated payload again and preserves the secure original bytes.

Supervised execution identity comes from successful bounded registry admission, not from a caller identifier or an executor thread. Each registered future poll and destructor has its original owned identity; nested scopes restore their caller and cancellation cannot leave an ambient owner installed. Identity is stable across suspension and executor migration and distinguishes sibling groups with identical local task counters. Native and browser choreography session bindings use that identity for supervised tasks. Identity observation grants no ability to admit a task or enter an execution scope, and identity carries no cryptographic peer, membership or signing authority.

Forced VM owner retirement

Session owner authority includes the physical identity of the actual claim or transfer. Session IDs, labels, generations and scopes are read-only observations and cannot reconstruct that authority. A capability from another runtime is invalid even when all of those observations are identical. Copying a current capability retains its original claim; transfer invalidates all copies of the previous claim.

A dropped move-owned VM session retires its exact registered choreography owner and local fragment custody synchronously. Owner generation and scope validation share the ownership-transfer lock order, so stale handles cannot retire a newer owner. This resource retirement supplies no signed terminal decision and performs no asynchronous close or physical-time observation. Ordinary paths retain the required explicit close contract. Unknown transport delivery remains unknown; retirement neither acknowledges nor replays pending frames.

Registered task destructors retain concrete retirement failures in the existing service task health owner before cancellation completion and idle publication. Task poll identity scopes remain lexical during destructors.

Enrollment negative terminal notification

Authenticated enrollment cancellation uses the separately admitted finite aura.invitation.device_enrollment_terminal_notice protocol. Its session identity is domain separated from the request/response session and binds the original invitation and admitted manifest digest. A notification never advances the request/response VM's program counter. The wire envelope is untrusted: only the independently pinned issuer signature and exact original manifest, invitation, ceremony and physical-device bindings issue negative terminal evidence.

The issuer sends only after the durable cancelled terminal decision. The receiver's listener belongs to the existing invitation service task tree and shares the original admitted window's lease, checkpoint and observations. It retains a distinct immutable signed failure receipt before reporting failure. Negative evidence cannot authorize device adoption or committed recovery. Cancellation and ordinary response races close their actual owned session slots; forced drop retires exact session custody without claiming asynchronous close or terminal evidence. Required failure causes remain in native observation and service task health. Notification retries retain the original deadline and only reconcile definitely unsent, exactly scoped transport failures.

Exact notice identity and bounded execution

The original registered enrollment window retains a single sealed notice identity from the actual retained issued control. It binds the canonical manifest transcript and digest, including signed expiry, to the original runtime and registered generation. Clones use the same binding; rebinding to a different digest, transcript or expiry fails closed. Admitted notice guards match the retained original expiry explicitly. No serialized value constructs this runtime-local binding.

Enrollment progression preserves its original lexical owner and acceptance window across delegated work. Caller futures have a bounded size independent of executor stack settings; delegation cannot acquire a second execution owner or extend the original window.

Signed notice validity attenuation

Issuer notice execution is bounded by both the original registered ceremony interval and signed manifest validity. An original owner derives its child endpoint from one acknowledged physical observation; a later read cannot shift that endpoint forward. The child shares original lease, observations and checkpoint, and never renews the registration. An already elapsed manifest validity is a retained typed domain expiry, not an invented clock failure or retryable transport diagnosis. Active cancellation checks this signed validity before the durable terminal CAS. Already-cancelled idempotent local replay retains the first decision without authorizing a new expired notification.

Required session teardown failures

Required VM close and runtime choreography close retain their concrete producer errors through the standard error source chain. Forced retirement retains a VM close failure even when exact ownership retirement succeeds. If both fail, the close failure is primary and the ownership failure remains separately typed. Cleanup failure cannot acknowledge successful terminal publication or remote delivery. A provider that exposes only textual lifecycle detail retains that limitation; wrapping it does not establish additional structured evidence.

Enrollment custody ordering

All enrollment publication and activation owners share one physical signing custody order: generation, tracker decision, then tree mutation. A composite runtime capability retains the actual generation and decision guards for the same effect system and tracker; a foreign runtime, a deserialized record or a caller-supplied lock cannot manufacture that custody. Fresh roster preparation, original allocation recovery and activation retain this owner through their tree decision. Registration and supersession reuse the held decision instead of reacquiring it. Verified signing activation requires the same physical generation capability and does not acquire that guard a second time. Readiness, immutable receipts and canonical identifiers remain evidence, rather than substitutes for a held lifecycle owner.

Original cancellation preparation scope

An active enrollment cancellation observes the actual original registered clock and checkpoint owner. Its preparation authority is distinct from protocol execution admission: it does not reacquire the execution lease or admit another VM session. Required guard preparation, first terminal decision and local publication share the original fixed deadline attenuated to signed validity. Required observation acknowledgment precedes continuation, and a replaced clock or allocation fails closed.

The complete cancellation ingress request has a separate local bound of five seconds, covering selector lookup, active preparation and historical negative publication. Active preparation is additionally bounded by the original registered/signed interval; the tighter bound stops continuation. Neither bound can extend enrollment validity or authorize protocol execution. An existing durable Cancelled decision supplies a negative publication capability, preserving the first decision and original interval without reopening execution or permitting new expired notification signing.

An enrollment registration handoff retains the actual runtime owner reference. Original protected record validation and matching logical identifiers alone do not permit a different runtime to consume that live registration capability. The generation decision lease can end after durable registration; the physical owner binding continues through protocol and deferred delivery admission.

Targeted VM disposal acknowledgment

Required VM retirement disposes only the owned target session, including live or blocked coroutines, scheduling eligibility, handoffs and scoped communication and resource state. Unrelated sessions remain usable. Host metadata removal follows the actual backend acknowledgment. The cooperative backend retains stable coroutine IDs through its existing index rebuild; the threaded backend validates and rebuilds its explicit ID index after removal.

Threaded worker execution is joined by the engine's synchronous worker scope before exclusive disposal begins. Acknowledgment means no target job remains; it does not require destroying the shared pool or other sessions. Naturally terminal session status and epoch are preserved, and repeated disposal returns its original compact acknowledgment. New close epoch advancement is checked only for a genuinely active target.

Concrete backend failure remains in the standard native source chain. Required closure cannot succeed by parsing or suppressing an unsupported error, merely removing host metadata, or disposing an entire engine containing other sessions. Historical compact summaries and diagnostic traces follow the dependency's explicit archive policy. Shared global guard state is not claimed as exclusively owned by the target session. VM disposal is local cleanup and does not establish remote delivery, a signed terminal decision or protocol completion.

Final active enrollment inventory custody

An enrollment duplicate-start observation requires both the original canonical invitation binding and the still-live task registration admitted from its original execution root. A missing root, busy lease, recovered phase record, cancelled task, or rejected spawn cannot establish that execution is running. Repeated observation neither creates another task nor renews the original provider or deadline. Running observations confer no execution or terminal acknowledgment authority and become unusable when their registration ceases to be live.

The issuer captures final active verification material while the original generation, tracker decision and tree reservation remains held. The exporter requires that sealed capture and compares the exact manifest binding before signing; caller-supplied manifest tuples do not authorize export. Receiver admission requires the signed final inventory and authenticates its roster against baseline membership. Existing-peer recording retains its original registered issuance capability rather than reloading weaker identifiers. Exact nonroot package persistence remains required before nonroot enrollment can be admitted; an absent provider fails closed and cannot be replaced by the root package.

Cancelled enrollment notification recovery

Post-bootstrap recovery distinguishes a retained Cancelled first decision from an active enrollment registration. Pending generation secrets remain retired. A separate move-owned notice capability binds the independently retained issued manifest, actual runtime, immutable first decision, original clock checkpoint and original execution semaphore. It authorizes only the finite signed terminal-notice protocol; it grants no Request, Accept, Confirm, activation or membership authority.

Notification eligibility ends at the earlier of the original registered deadline and the signed manifest expiry. Restoring a terminal decision does not renew either bound. Required observation and checkpoint acknowledgment precede signing and continuation. Signing uses the currently owned issuer identity only while its key still matches the independently retained issuer verifier. Known original or signed expiry completes the finite recovery owner with a typed eligibility-ended disposition and prevents further sends. Required clock, checkpoint, signer, transport and teardown faults retain their original typed cause through task failure and drain. Both preserve the Cancelled decision.

Failed enrollment generation retirement

A failed generation retires its required secret inventory before publishing and acknowledging the exact immutable retirement receipt. That receipt makes retirement retries idempotent. The original protected allocation record remains immutable evidence; generic secure deletion cannot release or rewrite it. An explicitly mutable pending slot has a separate owned release contract. Immutable participant wrapping secrets likewise require an explicit retirement lifetime. Fresh allocation ownership must distinguish that history from its live pending slot, including when the next canonical epoch is unchanged by a failed ceremony.

Enrollment allocation history and live epoch slots

An enrollment allocation's original ordered policy, independent setup binding, reserved invitation, prestate and clock interval are immutable history. Its registered first decision has a separate immutable seal. An epoch-addressed mutable live slot identifies the currently held allocation; neither its phase flag nor its participant vector independently authorizes registration or recovery. Required reads compare the slot against its protected original history and registered seal before exposing a live generation capability. A registered seal acknowledged before an interrupted slot update remains the first decision.

Retirement releases the mutable slot only after required cleanup and the exact completed cleanup receipt are acknowledged. A negative decision recorded before cleanup does not certify that cleanup completed. Replaying that decision permits only cleanup of the same original generation, never resumed signing. Original allocation and registration evidence remains protected when a later ceremony allocates the same pending epoch. Legacy protected epoch records require explicit original-history validation before migration into a separate mutable slot.

Participant wrapping secrets require generation-specific lifetime ownership. Their creator custody must survive reconstruction under the original selected profile and distinguish two ceremonies at the same pending epoch. A generic Delete capability, namespace match or caller-supplied digest does not authorize retirement of such a secret.

Admitted enrollment clock publication

The original invitee admission interval is retained as immutable evidence, separate from the mutable highwater checkpoint. Fresh admission retains the full signed manifest interval beginning at the original recorded admission time. Explicit migration of a legacy clock preserves its actually recorded attenuation; it cannot extend that interval to the newer fresh policy.

Finishing an interrupted initial publication requires the original protected admission, cryptographic revalidation and exclusive execution custody of the actual runtime. It may publish only the original clock bytes. Required observation and reimport do not allocate clocks. The immutable first-live decision ends this initial completion authority: subsequent missing original or checkpoint records fail closed, rather than deriving another clock from the current time. Required publication, reread and checkpoint faults retain their concrete causes.

Enrollment signing and response policies

An enrollment generation commits its signing threshold and ordered signing roster separately from the remote response policy. The local issuer belongs to the signing roster and is not a remote responder. The original allocation fixes the response threshold and responder count before registration; subsequent registration, recovery and interrupted completion compare those committed values exactly. A signing threshold does not become response-policy evidence through clamping recovered records. Historical allocations lacking a distinct protected response-policy commitment require explicit proved migration before live reuse.

Historical enrollment response-policy evidence

An old allocation without a distinct response commitment may acquire a separate immutable supplement only from its original protected allocation and original protected tracker registration. The supplement binds the exact bytes of both records and retains the registration's response threshold and count directly. Original subject, ceremony, epoch, prestate, setup and responder roster must agree. Missing original proof cannot be replaced by arithmetic on the signing threshold or a reconstructed participant count.

Explicit migration holds the actual generation owner. Required reads validate the supplement and its original evidence without writing new authority. Neither old allocation bytes nor the original clock interval are changed. Deserializing an old allocation cannot reconstruct this verified supplemental authority; missing or contradictory supplemental evidence fails closed.

Verified enrollment parent heads

A commitment change within an epoch does not change the original signing-key policy. An enrollment AddLeaf followed by RotateEpoch therefore has an intermediate original-epoch parent head. Required verifier inventory captures that exact parent only after its operation cryptographically verifies against the independently admitted node key and policy. Neither an epoch match nor a public package template independently authorizes a new parent commitment.

Sealed committed-transition and local-extension evidence retains the captured inventory. Archive consumers require that evidence and its original manifest binding before exposing verifier data. The immutable archive continues binding the complete original committed-history digest and admitted public policies; operation verification reconstructs exact intermediate heads. A replayed fence, another node/epoch, substituted policy or divergent history cannot supply the required evidence.

Registered notice identity assignment

A registered enrollment window retains one runtime-local notice identity binding for its original manifest digest, canonical transcript and expiration. Repeated submission must compare all three fields against that original assignment; contradictory submission cannot replace it. This binding is not decoded from peer or storage data and does not establish signing authority or freshness on its own.

Registered enrollment execution-window admission requires the original registered generation capability, bound to its actual runtime, tracker and signed canonical invitation. An observed ceremony snapshot or a ceremony identifier alone cannot reacquire execution custody. Pre-live allocation clock ownership and registered execution ownership remain distinct stages.

Original enrollment allocation policy

Device enrollment has a maximum original allocation interval of 600,000 physical milliseconds. A signed quorum request must be validated against this same policy. A longer setup-code validity interval cannot widen that allocation. Signed expiry attenuates the active child while preserving the original interval and its retained observation continuity.

Enrollment allocation lifetime ownership

Enrollment wrapping births retain the authenticated rotation plan and original immutable allocation scope. Read, activation and retirement capabilities bind to the actual runtime registry. Negative cleanup retains original generation and first-decision custody through provider acknowledgment before releasing the generation. Restart recovers that original custody and deadline; same-epoch reissuance cannot be retired by replaying an earlier allocation's negative owner.

Configured provider fidelity

An explicitly configured runtime effect provider remains the provider for its required operations throughout assembly and service ownership. Ordinary storage configuration preserves unified encryption at rest and does not replace secure allocation custody. A configured provider failure remains a failure of that operation with its native cause. It cannot authorize selecting an implicit default provider. Configured transport selection precedes emission; receive absence permits inspection of another configured provider, while a typed fault terminates that attempt. Synchronous and asynchronous builders have the same provider-fidelity contract.

Rendezvous identity selection failures

Local rendezvous descriptor and channel identity material is bound to the selected runtime's active physical participant and epoch policy. The retained identity context authorizes the canonical package read. Failure of that read retains its concrete cause and prevents publication or channel preparation; a companion package or historical epoch cannot replace failed authoritative material. Contact response signing retains the original issued identity under the same required physical package-read contract.

Filesystem lifetime initialization may finish an acknowledged pre-link intent only under original selected profile custody and protected pre-live origin. Staged observations do not count as acknowledged once-live metadata. Recovery preserves the original root and finishes Preparing/Birth/Ready/Handed ordering without a new root allocation; ambiguous, conflicting or missing live evidence returns a retained failure.

Contact, guardian and channel invitation issuance captures its original physical signer under the fresh reservation before publication. Subsequent export, response and profile reopen load that protected identity and canonical sender record; neither active-epoch replacement nor a historical search can repair missing original evidence. The identity capability binds the actual runtime, physical device, original epoch, invitation digest and public verifier. Export preserves native selected-provider signing failures through its typed error chain.

Initial staged-publication recovery retains the opened source through link, linked-target identity and ciphertext validation, then acknowledges the target before removing staged evidence. Conflict or substitution cannot acknowledge handoff. Interruption after link and before staged-name removal may leave two names for one original private ciphertext inode. Only the exact original source/target pair, authenticated under held profile custody, admits this initialization exception; unrelated aliases and missing once-live targets fail. Target acknowledgement precedes stage removal and its directory acknowledgement. Stage inventories and exact target-prefix lookup stream entries under retained directory descriptors, without imposing a total ordinary-record cap. Traversal bounds follow the secure-storage namespace/key/subkey layout; full native scan latency remains proportional to the stored directory inventory.

Required shutdown completion provenance

Closing runtime admission establishes Stopping, not completed shutdown. A shutdown request observing an already closed owner fails with its native state and cannot publish Stopped. Recorded task-tree, service or lifecycle teardown failures retain Stopping. Only the internal successful completion path publishes Stopped; an observed activity handle cannot mint that state. The complete admitted-operation and owned-service drainage protocol remains a separate prerequisite for profile handoff.

Contact confirmation operation windows

A Contact confirmation continuation retains the original acceptance operation's attenuated physical interval and observation owner. Retrying the same signed acceptance cannot renew that interval. Physical rollback after observed progress is a required failure even when the new timestamp is later than the original start. Required clock and sleep failures retain their native causes and do not become invitation expiry. A runtime-owned decision lease serializes required imported-state verification and the resulting materialization and status publication.

Required current identity signing availability

A supported active threshold identity reports quorum-service unavailability only after its current native public verifier, exact ordered physical participant policy and actual local encrypted share have been validated together. Malformed or unsupported native packages remain cryptographic failures; missing local backing records remain storage failures with their original record location. A local share alone never establishes completed group signing.

Guardian recovery pair access is serialized by the original runtime's private keypair lease. A response identity capability retains that runtime and its zeroizing private bytes; partial or mismatched original evidence fails before response publication. Both fresh writes must acknowledge before capability issuance. The in-process lease is not a durable recovery witness for interrupted initial pair publication or complete historical loss.

Required regular imported-invitation reads and terminal decisions share the original runtime's imported-invitation decision lease across Contact and Guardian handlers. Required Guardian response code reads bounded stored metadata, retains native read/codec failures, and checks the imported invocation binding before allocating recovery keys or opening the VM. A cached invitation cannot turn failed backing reads into absence. VM, canonical codec, physical clock and confirmation storage failures retain process-local original causes.

Guardian sender-code context and the receiver-local materialized context are distinct. The response binds retained original payload fields and actual receiver authority while retaining original code context/version as import evidence; re-encoding a receiver-local projection cannot reconstruct the original code.

Guardian principal and receiver operations establish their original effect-backed physical window before the first required import, key, or VM await. Preparation and the VM loop consume the same budget and observation owner; waiting for import custody cannot start a new window. Required clock/provider failures retain native causes. Expiration/cancellation is failure evidence and does not acknowledge session disposal or authorize a runtime/profile transfer.

Guardian VM terminal processing consumes the actual owned session and requires its close acknowledgment before a successful return. A failed primary operation and failed close retain both typed process-local causes; standard source traversal follows the primary, while the terminal failure retains cleanup separately. The primary timeout category survives a combined failure. Outer-window cancellation may still force owner retirement; it is failure evidence, never close ACK or completed runtime/profile drain.

Original runtime shutdown window and retained operation admission

Public invitation, authentication, chat, OTA, recovery and session mutations retain one admission lease from their actual runtime until completion or cancellation. Admission closure and operation count changes are atomic. Each runtime admits at most 256 simultaneous public operations; exhaustion rejects before mutation and only the original lease's destruction releases its slot. This local resource policy grants no ceremony, signing, or membership authority.

Shutdown closes admission and owns one required physical resource window of 30 seconds. It settles admitted operations before stopping their reactive publication scheduler, then waits for actual supervised descendant destruction and required service teardown under that same original window. Failed clock, checkpoint, deadline, service, or destruction evidence withholds successful stopped publication. Forced abort requests do not constitute destruction ACK. Cancellation does not reopen the original runtime.

This shutdown contract does not establish transferable profile custody. Unleased advanced effects, lower signing/bridge mutation routes, current membership validation, provider-preserving profile reassembly and genuine quorum signing require their own completed ownership boundaries.

Runtime admission observations expose state without authority to close admission or publish shutdown completion. Closure remains internal to runtime ownership; external callers use the sanctioned shutdown operation. Runtime operation leases are issued through declaration-layer proof boundaries and retain the actual activity gate; a foreign gate cannot authorize an original runtime continuation.

Original runtime service-stop continuation

Successful public admission closure creates a move-only shutdown window tied to the actual gate, effect system and task root. Required service disposal and health acknowledgments consume that same original resource window; the common service helper cannot allocate another deadline. Authority termination is published only after all required pipeline, task-tree, service-health and lifecycle acknowledgments, within the original window. Provider, deadline and authority-state failures retain their native causes and withhold successful runtime termination.

This contract does not authorize profile transfer. Internal service cleanup windows and whole provider/registry/RNG reassembly require their own completed owner integration before a full handoff can be acknowledged.

Exact reactive publication observation

An exact processing target is issued by the original scheduler ingress after accepted ordered enqueue. Its queue envelope and retained processing observation are bound to that same ingress owner. The scheduler acknowledges only after all registered views complete the selected batch. Retained highwater allows exact completed targets to be observed despite coalesced or missed diagnostic notifications. Original scheduler failures retain their native causes for pending targets. Processing acknowledgment establishes completion of configured view updates; canonical commit provenance and protocol eligibility remain bound to their respective runtime-issued evidence.

Required Chat mutation and processing share one admitted operation owner and its original physical resource window. Runtime startup shares one physical resource window across service admission, start, health and required initial replay. Startup readiness requires that replay's exact target to be processed. Failed partial startup owns cleanup of its admitted services and retains primary and secondary failures. Optional descriptor publication has subsidiary supervision and cannot delay primary startup readiness. Latency diagnostics explicitly represent unavailable measurement rather than inventing physical timestamps.

Canonical runtime ingress retains the exact runtime captured by pipeline construction. A standalone scheduler cannot authorize runtime attachment, and a foreign runtime cannot adopt another pipeline's processing acknowledgment. Processing completion does not assert successful signal emission or application semantic readiness. Observers retain receive-only diagnostic subscriptions; a diagnostic notification never supplies publication sequence or processing authority.

Runtime-issued command services

A public command's startup admission is handed into the actual registered runtime service before the startup lease is released. Long-lived service lifetime is owned by the runtime task root, rather than an ordinary admitted operation held while awaiting user input. Each required command round has one original effect-backed resource interval shared by its helper awaits. The local public-operation resource policy is thirty seconds; it cannot replace or renew a signed protocol interval or a stronger existing operation window.

Managed command cleanup acknowledges actual service stop and task completion under the original shutdown owner before disposal of reactive processing and root tasks. Required cleanup failure withholds whole-runtime completion.

Local cleanup deadlines and terminal evidence

A resource deadline is a local physical-time budget chosen by its authoritative owner. It cannot establish causal/protocol ordering, consensus finality, shared Range validity, or distributed completion. Service progress publication requires actual disposal/task acknowledgment and a bounded required observation under the original shutdown owner. Observation-lock acquisition, clock access and checkpoint retain that same fixed endpoint and selected provider. Expired, unsupported or failed provider observations cannot publish successful cleanup. Frontends and observers cannot substitute another clock, allocate a replacement window, or turn timeout diagnostics into domain completion evidence.

Prepared enrollment quorum ownership

Preparation retains the original issuer generation/tree reservation and protected physical window while explicit participants approve the exact versioned intent. An approved participant belongs to its actual active runtime/profile and current native ordered signing policy. Provisional or merely matching authority ids cannot provide participant custody; missing, malformed and foreign material remain typed failures.

The issuer transfers only a restricted HeldIssuerCompletionObserver to its registered completion holder. This move-only observer retains the original protected clock/checkpoint continuation and exact result/task observation; it carries no execution permit, arbitrary executor, child, nonce or raw-clock API. The actual issuer task keeps execution custody. Participant and issuer task handles remain owned by bounded runtime ingress until actual group destruction acknowledgment under their original windows. Capacity is admitted before spawning. Registry collisions and shutdown failures preserve original concrete causes and never treat dropped handles as successful drainage.

A retained initial Request signature is immutable, independently reverified and bound to the exact issued manifest, original runtime and current native signing policy. Required execution eligibility expires with the original protected window; cached signatures cannot renew it. Successful initial quorum initiation does not prove later confirmation quorum, complete enrollment or restart custody.

Device quorum signing for tree operations

An authority signature whose current policy needs more than one device (a tree operation or a typed message such as a device-rotation proposal or commit) is produced by ThresholdSigningService::sign_with_device_quorum. The coordinating device sends each co-signer a request carrying the full signing context, proven with the coordinator's own share. The co-signer authenticates it against the coordinator's verifying share in its own retained current package, recomputes the exact message from its own state, and only then consults its consent policy. Every round packet is share-proven in both directions. Nonces exist only in memory after consent and are consumed by the one share they produce. A threshold of one signs locally; a raw sign call never starts a distributed round.

Consent is a device-local setting (DeviceSigningConsent): escalate to the user on that device (the default) or sign automatically after verification. It is stored locally, never replicated, and consulted on every request. An escalated request waits as a pending signing request until the user approves or declines it. A decline is a share-proven cancel that fails the coordinator's operation with a typed refusal. Granular per-operation rules are future work.

A device-rotation participant accepts with a proof of its current share, which the initiator checks against that device's verifying share. It stores its new share wrapped like every other participant share. Both devices then activate the same rotated package. The commit is the participant's final step: an applied, verified commit completes its session.

Confirmed import activation custody

Only the original durable confirmed enrollment capability can publish its activation envelope. Key readers retain that original receipt or the reverified committed profile receipt; raw authority, epoch and participant identifiers only check the held reference. A committed profile may supply read custody for its original device before reopening, but active subject signing still requires the actual adopted runtime identity and explicit original-device approval. The separate envelope leaves immutable signed import bytes unchanged. The original birth anchor prevents missing-envelope recovery from refreshing nonce or key custody. Repeated handoff reuses and verifies the exact original envelope, and required readers preserve provider and codec sources.

Confirmed activation wrapping custody uses the same native allocation manager as issuer generation custody, with distinct confirmed import origins on the sealed birth and positive capabilities. Required reads verify the original receipt, imported generation and exact allocation reference. A recovered original scope without its required envelope is a storage failure; retry or reopening cannot allocate a replacement wrapping secret for that scope.

Consuming enrollment execution and terminal custody

Admitted, held-issuer, registered and approved-signing execution require their actual original durable Pending birth. The consuming root retains its native material acquisition, task admission and protocol continuation. Closed requires its independent domain evidence, exact sealed descendant disposal and original durable acknowledgment. Approved-signing completion additionally binds the actual native participant completion to the same approved intent and effect owner. A successful checkpoint alone, transcript bytes, task disposal or a historical Closed record cannot reconstruct that authority.

Negative or unresolved execution retains the completed operation, actual checkpoint disposition, first native failure and independent final validation without minting a new cleanup owner. Cleanup belongs to the originally retained negative-only custody, including partial acquisition and refused task admission. Observation cancellation does not release that obligation, renew the physical endpoint or recover signing authority. Packet progress and completed native IO remain in their original holder before final validation; unresolved started sends cannot be replaced by another send under a reconstructed owner. Opaque disposal observations identify the exact original required task and grant no terminal authority. The original runtime and approved finite negative policy remain required for conditional negative signing (100_crypto.md).

Journal

This document describes the journal architecture and state reduction system in Aura. It explains how journals implement CRDT semantics, how facts are structured, and how reduction produces deterministic state for account authorities and relational contexts.

It describes the reduction pipeline, flow budget semantics, and integration with the effect system. It defines the invariants that ensure correctness. See Maintenance for the end-to-end snapshot and garbage collection pipeline.

Hybrid Journal Model (Facts + Capabilities)

Aura’s journal state is a composite of:

• Fact Journal: the canonical, namespaced CRDT of immutable facts.
• Capability Frontier: the current capability lattice for the namespace.
• Composite journal view: the runtime carries facts and capabilities together when evaluating effects.

The fact journal is stored and merged as a semilattice. Capabilities are refined via meet. The runtime always treats these as orthogonal dimensions of state.

1. Journal Namespaces

Aura maintains a separate journal namespace for each authority and each relational context. A journal namespace stores all facts relevant to the entity it represents. A namespace is identified by an AuthorityId (see Authority and Identity) or a ContextId and no namespace shares state with another. Identifier definitions appear in Identifiers and Boundaries.

A journal namespace evolves through fact insertion. Facts accumulate monotonically. No fact is removed except through garbage collection rules that preserve logical meaning.

#![allow(unused)]
fn main() {
pub struct Journal {
    pub namespace: JournalNamespace,
    pub facts: BTreeSet<Fact>,
}

pub enum JournalNamespace {
    Authority(AuthorityId),
    Context(ContextId),
}
}

This type defines a journal as a namespaced set of facts. The namespace identifies whether this journal tracks an authority's commitment tree or a relational context. The journal is a join semilattice under set union where merging two journals produces a new journal containing all facts from both inputs. Journals with different namespaces cannot be merged.

2. Fact Model

Facts represent immutable events or operations that contribute to the state of a namespace. Facts have ordering tokens, timestamps, and content. Facts do not contain device identifiers used for correctness.

#![allow(unused)]
fn main() {
pub struct Fact {
    pub order: OrderTime,
    pub timestamp: TimeStamp,
    pub content: FactContent,
}

pub enum FactContent {
    AttestedOp(AttestedOp),
    Relational(RelationalFact),
    Snapshot(SnapshotFact),
    RendezvousReceipt {
        envelope_id: [u8; 32],
        authority_id: AuthorityId,
        timestamp: TimeStamp,
        signature: Vec<u8>,
    },
}
}

The order field provides an opaque, privacy-preserving total order for deterministic fact ordering in the BTreeSet. The timestamp field provides semantic time information for application logic. Facts implement Ord via the OrderTime field. Do not use TimeStamp for cross-domain indexing or total ordering. Use OrderTime or consensus/session sequencing instead.

This model supports account operations, relational context operations, snapshots, and rendezvous receipts. Each fact is self contained. Facts are validated before insertion into a namespace.

Bootstrap genesis completion requires an authenticated device-creation AttestedOp under the retained epoch-zero key, together with its durable operation bytes and tree index entry. An in-memory reducer/cache entry alone cannot prove commit after a failed storage write. A persisted completion record binds the exact creation-operation digest; matching device IDs without matching keys and signed creation evidence cannot establish bootstrap readiness.

2.2 Protocol-Level vs Domain-Level Relational Facts

RelationalFact has only two variants:

• Protocol(ProtocolRelationalFact): Protocol-level facts that must live in aura-journal because reduction semantics depend on them.
• Generic { .. }: Extensibility hook for domain facts (DomainFact + FactReducer).

Criteria for ProtocolRelationalFact (all must hold):

1. Reduction-coupled: the fact directly affects core reduction invariants in reduce_context() (not just a view).
2. Cross-domain: the fact’s semantics are shared across multiple protocols or layers.
3. Non-derivable: the state cannot be reconstructed purely via FactReducer + RelationalFact::Generic.

If a fact does not meet all three criteria, it must be implemented as a domain fact and stored via RelationalFact::Generic.

Enforcement:

• All protocol facts are defined in crates/aura-journal/src/protocol_facts.rs.
• Any new protocol fact requires a doc update in this section and a matching reduction rule.

2.1 Domain Fact Contract

Domain facts are the extensibility mechanism for feature crates. They are stored as RelationalFact::Generic envelopes and reduced by registered FactReducers. Every domain fact family follows the canonical domain fact model of §4.2.1: one derive codec, one declared schema version, registration in the agent FactRegistry, and a reduction that is a pure function of the fact set.

3. Semilattice Structure

Journals use a join semilattice. The semilattice uses set union as the join operator with partial order defined by subset inclusion. The journal never removes facts during merge. Every merge operation increases or preserves the fact set.

The join semilattice ensures convergence across replicas. Any two replicas that exchange facts eventually converge to identical fact sets. All replicas reduce the same fact set to the same state.

The merge operation asserts namespace equality, unions the fact sets, and returns the combined journal. The result is monotonic and convergent.

4. Reduction Pipeline

Aura maintains two replicated state machines. Account journals describe commitment trees for authorities. Relational context journals describe cross-authority coordination. Both use the same fact-only semilattice and deterministic reducers.

flowchart TD
    A[Ledger append] --> B[Journal merge];
    B --> C[Group by parent];
    C --> D[Resolve conflicts via max hash];
    D --> E[Apply operations in topological order];
    E --> F[Recompute commitments bottom-up];

Ledger append writes facts durably. Journal merge unions the fact set. Reducers group operations by parent commitment, resolve conflicts deterministically using max hash tie-breaking, and then apply winners in topological order. The final step recomputes commitments bottom-up which downstream components treat as the canonical state.

4.1 Fact Production

Account operations originate from local threshold signing or Aura Consensus. Relational context operations always run through Aura Consensus because multiple authorities must agree on the prestate. Each successful operation produces an AttestedOp fact. Receipts that must be retained for accountability are stored as RendezvousReceipt facts scoped to the context that emitted them. Implementations must only emit facts after verifying signatures and parent commitments.

4.2 Determinism Invariants

The reduction pipeline maintains strict determinism:

1. No HashMap iteration: All maps use BTreeMap for consistent ordering
2. No system time: OrderTime tokens provide opaque ordering
3. No floating point: All arithmetic uses exact integer/fixed-point
4. Pure functions only: Reducers have no side effects

These properties are verified by test_reduction_determinism() which confirms all fact permutations produce identical state.

4.2.1 Canonical Domain Fact Model

Facts reach replicas late, duplicated and out of order through sync. A domain fact family is therefore reduced by a pure function of its fact set: every permutation of the same facts yields the same state, and neither arrival order nor physical time decides an outcome.

Encoding, versioning and registration

Each domain fact type has one shape and one codec.

• Derive codec. The type uses #[derive(DomainFact)] (aura-macros). The derive writes a DAG-CBOR FactEnvelope and decodes only DAG-CBOR. Hand-written impl DomainFact blocks and JSON envelopes are not used. The shared aura-core decode helpers reject a JSON envelope with FactError::NonCanonicalEncoding.
• One schema version. #[domain_fact(type_id = ..., schema_version = N)] declares the only version, carried by the envelope. Decoding accepts exactly N. When the shape changes, the version is bumped and the old shape is replaced, not decoded: there is no supported-version range, no legacy decoder and no compatibility shim. The payload carries no version field of its own, and the type id carries no version suffix.
• Type id and context. The type id is a plain string (a literal, a *_FACT_TYPE_ID constant or a zero-argument accessor), unique across the registry and listed in crates/aura-agent/src/fact_types.rs. The derive's context or context_fn names the fact's ContextId.
• Keys and registration. Reducers and views address facts through the family's FactKey helpers, never ad hoc strings. Each type is registered with its FactReducer in build_fact_registry (crates/aura-agent/src/fact_registry.rs); a Layer 2 crate that cannot depend on aura-journal is registered through a transparent derive wrapper in a higher crate (maintenance facts use aura-sync::MaintenanceJournalFact).

Reduction patterns

aura-journal::causal_reduction provides the shared rules. A family composes them; it does not reimplement them.

• Tagged observed-remove set. An add is identified by its tag. A reversal names the tags of the adds of the same key that its writer observed. The set keeps every add that no reversal revokes, so a concurrent add the reversal's writer did not observe survives. Contacts (existence per owner and contact), web-of-trust introductions, home bans and mutes, and social lifecycle pairs use this pattern.
• Multi-value register. A write names the writes of the same key it supersedes. The register keeps every write that no observing write supersedes and that is not causally before another write. The family resolves the remaining concurrent writes by an explicit domain policy, then by causal order. Contact nicknames and read-receipt policy, access overrides, storage readings and chat message revisions use this pattern.
• Episodes. State that can end and restart, such as a friendship, a channel membership or a home neighborhood join, is a sequence of episodes. A terminal fact ends the episodes its writer observed, and only a fact that starts a new episode re-admits the subject. A late or replayed fact from an ended episode cannot reopen it.
• Explicit terminal precedence. Families whose outcomes are terminal rather than reversible, such as recovery and invitation outcomes, define a total precedence over terminal states and resolve ties by causal order or canonical bytes. Protocol facts follow the same rule: AMP channel bootstraps resolve to the smallest bootstrap_id, then full fact order.

Causal stamps and time

A reversible or overwritable fact carries aura_core::time::CausalMetadata, stamped by the writer before commit:

• clock: the writer's LogicalClock after observing every fact of the family it holds.
• revokes: for a reversal, the tags of the observed adds of the same key.
• supersedes: for a register write, the tags of the observed writes of the same key.

The tag itself is not carried. Every reader derives it as the hash of the fact's type id and canonical re-encoding, which names the author and includes the clock. A peer cannot claim another fact's tag to revoke or shadow it, and distinct content never shares a tag.

Writers obtain the metadata through RuntimeBridge::causal_stamp(CausalStampKey), which advances the runtime's logical clock past the family's committed facts for that key. CausalStampKey names the family and key: HomeGovernance, Contact, Friendship, Chat and InvitationOutcome.

Causal order (causal_cmp) is happens-before, then TimeStamp::sort_compare with OrderingPolicy::DeterministicTieBreak, then causal depth, Lamport scalar and tag. It is the tie-break of last resort and the order for display. Physical time is for user-visible timestamps and expiry only. Expiry is evaluated at query time against a caller-supplied instant, never during reduction.

Verification and enforcement

assert_permutation_invariant is the shared test harness: it reduces every permutation of a small fact set and requires identical state. Every reversible family keeps such a regression next to its reducer.

just ci-domain-fact-model (also run by just ci-ownership-policy) is a Rust-native syntax check in toolkit/xtask. Over production code it requires that every DomainFact type uses the derive, has a resolvable unversioned type id and no in-payload version field, and is registered in the FactRegistry. It rejects JSON envelopes in domain fact crates. It keeps a typed inventory of reversible families; a fact carrying CausalMetadata must belong to a listed family, and each family must keep a test-scope assert_permutation_invariant call. The derive itself rejects a min_supported_schema_version key.

Home governance (docs/115 §3.4), social lifecycle (docs/115 §3.5), contacts (aura-relational::contacts), the web of trust (aura-relational::wot), recovery (aura-recovery::state), invitation outcomes (aura-invitation::lifecycle), chat revisions (aura-chat::revisions) and AMP channel membership (aura-amp::channel) follow this model.

4.3 Canonical Entity Materialization

A channel, home, invitation, or contact exists in a projection only after its domain creation fact or an equivalent authenticated creation outcome supplies the canonical identity and required metadata. A membership, relationship, status, rename, or activity fact may change an existing entity but cannot establish one. Raw identifiers identify a candidate; they are not evidence of canonical name, context, type, or relationship.

Reduction is independent of delivery order. Enrichment facts that arrive before creation remain applicable when matching creation evidence arrives. Facts for a different entity or context cannot contribute members, counts, labels, or status. Duplicate facts do not create duplicate entities or inflate counts. Replaying the same fact set after restart yields the same materialized entities and metadata as live reduction.

For homes, an accepted inviter reloads its committed HomeCreated fact before applying membership enrichment. The app's home creation witness can be derived only from that fact shape; acceptance or membership alone cannot create the home projection. Nonempty home snapshots round-trip typed home and authority identifiers through JSON without changing their identities or counts.

5. Account Journal Reduction

Account journals store attested operations for commitment tree updates. Reduction computes a TreeStateSummary (epoch, commitment, threshold, device count) from the fact set. See Authority and Identity for structure details. The summary is a lightweight public view that hides internal device structure. For the full internal representation with branches, leaves, and topology, see TreeState in aura-journal::commitment_tree.

Internally, AuthorityTreeState materializes explicit branch topology to support incremental commitment updates. It keeps ordered branch children, branch/leaf parent pointers, and branch depth metadata. The topology is deterministic: active leaves are sorted by LeafId, paired in stable order, and materialized with NodeIndex(0) as root followed by breadth-first branch assignment. This guarantees identical branch structure for identical active leaf sets across replicas.

Commitment recomputation for non-structural mutations is path-local. Aura marks affected branches dirty, collects their paths to root, then recomputes only those branches bottom-up. Structural mutations (AddLeaf, RemoveLeaf) currently use deterministic rebuild of topology and branch commitments (correctness-first baseline). Merkle proof paths are derived from the same materialized topology so proof generation and commitment caches share one source of truth.

Maintenance note: do not change topology construction or branch indexing rules without updating replay fixtures and root commitment fixtures. Determinism depends on stable leaf sort order, stable pair composition, and stable branch index assignment.

Reduction follows these steps:

1. Identify all AttestedOp facts.
2. Group operations by their referenced parent state (epoch + commitment).
3. For concurrent operations (same parent), select winner using max hash tie-breaking: H(op) comparison.
4. Apply winners in topological order respecting parent dependencies.
5. Recompute commitments bottom-up after each operation.

The max hash conflict resolution (max_by_key(hash_op)) ensures determinism by selecting a single winner from concurrent operations. The result is a single TreeStateSummary for the account derived by extracting AttestedOp facts and applying them in deterministic order.

6. RelationalContext Journal Reduction

Relational contexts store relational facts. These facts reference authority commitments. Reduction produces a RelationalState that captures the current relationship between authorities.

#![allow(unused)]
fn main() {
pub struct RelationalState {
    pub bindings: Vec<RelationalBinding>,
    pub flow_budgets: BTreeMap<(AuthorityId, AuthorityId, u64), u64>,
    pub leakage_budget: LeakageBudget,
    pub channel_epochs: BTreeMap<ChannelId, ChannelEpochState>,
}

pub struct RelationalBinding {
    pub binding_type: RelationalBindingType,
    pub context_id: ContextId,
    pub data: Vec<u8>,
}
}

This structure represents the reduced relational state. It contains relational bindings, flow budget tracking between authorities, leakage budget totals for privacy accounting, and AMP channel epoch state for message ratcheting.

Reduction processes the following protocol fact types wrapped in Protocol(...):

1. GuardianBinding maps to RelationalBinding for guardian relationships
2. RecoveryGrant creates recovery permission bindings between authorities
3. Consensus stores generic bindings with consensus metadata
4. AmpChannelCheckpoint anchors channel state snapshots for AMP messaging
5. AmpProposedChannelEpochBump and AmpCommittedChannelEpochBump track channel epoch transitions
6. AmpChannelPolicy defines channel-specific policy overrides for skip windows
7. DkgTranscriptCommit stores consensus-finalized DKG transcripts
8. ConvergenceCert records soft-safe convergence certificates
9. ReversionFact tracks explicit reversion events
10. RotateFact marks lifecycle rotation or upgrade events

Domain-specific facts use Generic { context_id, binding_type, binding_data } and are reduced by registered FactReducer implementations.

Reduction verifies that relational facts reference valid authority commitments and applies them in dependency order.

Enrollment response evidence and recovery

Enrollment acceptance requires the expected verifier selected by explicit setup transfer and retained for that ceremony. A participant count, a persisted terminal outcome, or a deserialized response does not establish acceptance provenance. Recording and activation require an opaque witness minted after verification of the exact response against that retained verifier.

Durable recovery retains the original response and its subject, invitation, ceremony, device, pending epoch and setup binding. Recovery revalidates this material before issuing a new process-local witness. Missing, corrupt or legacy active records without verifier evidence fail closed. Observing a historical terminal result does not authorize a new activation.

The first durable response decision is stable under duplicate, concurrent and contradictory delivery. Required persistence failure must prevent acceptance from becoming visible to activation owners. Runtime receipts and committed journal facts have distinct provenance; a receipt alone cannot establish a consensus-finalized membership transition.

Enrollment VM control messages are authenticated against the independently selected initiator verifier retained with the signed manifest. Requests and confirmations bind the exact manifest digest and ceremony decision. Peer receipt keys or supplied digest strings cannot select that verifier. A response signer derives its physical identity and policy from locally retained setup possession and the sealed admitted manifest. Live response signing requires the current signer to match that original setup; retained evidence does not grant historical signing authority.

An established confirmation requires the authoritative committed terminal decision. Pending state is not a timeout. Recovery revalidates original retained independent pins before minting process-local admission evidence.

6.1 AMP Channel Epoch Transition Reduction

Reduced AMP epoch entries may contain staged policies, bootstrap metadata, or transition observations before creation. Canonical materialization requires the selected checkpoint for the exact context and channel. The reduced state retains checkpoint presence explicitly; an absent checkpoint cannot establish channel existence, readiness, or duplicate creation. Checkpoint evidence is observed journal content, not an authorization capability.

AMP channel epoch transition reduction is fact-only and deterministic. It refines the existing A1/A2/A3 operation model for channel epoch state without changing authority-root membership or account commitment tree rules.

Every AMP transition proposal, certificate, commit, abort, conflict, or supersession fact binds the same canonical transition_id when it refers to the same transition. The identity is the typed digest over:

• context_id
• channel_id
• parent_epoch
• parent_commitment
• successor_epoch
• successor_commitment
• membership_commitment
• transition_policy

Reducers group transition facts by (context_id, channel_id, parent_epoch, parent_commitment) and validate all facts in the group before exposing live state. Reducer validation covers parent binding, successor epoch validity, membership commitment validity, witness committee validity, A2 certificate thresholds, A3 commit evidence, and abort/conflict/supersession evidence.

For each parent group, reduction exposes one of:

If exactly one valid unsuppressed A3 commit exists, that transition is both the durable and live successor. Otherwise, if exactly one valid unsuppressed A2 certificate exists, that transition is the live successor but remains non-durable. If conflicting valid A2 certificates exist and facts do not resolve the conflict, reduction exposes no live successor and marks the parent state conflict-tainted.

Reducers must not use local wall-clock time, network connectivity, operator preference, arrival order, or hash tie-breaking between conflicting valid A2 certificates to choose a live successor. Single-winner exposure must come from fact validation: a valid AMP certificate, a valid A3 commit, explicit equivocation evidence, abort evidence, or supersession evidence.

The aura-journal context reducer exposes this state as structured AMP transition reduction data. RelationalState::amp_transitions is keyed by AmpTransitionParentKey { context, channel, parent_epoch, parent_commitment }. Each AmpTransitionReduction records observed, certified, finalized, suppressed, conflict, and emergency evidence ids for that parent. ChannelEpochState::transition points at the current parent transition, and ChannelEpochState::pending_bump is populated only when the current parent is A2Live. Emergency reducer fields include suspect authorities, quarantine successor epochs, and prune-before epochs derived from emergency alarms and emergency transition facts.

The reduced channel view distinguishes:

• stable_epoch: last durable committed epoch
• live_successor: optional A2-certified successor for the stable epoch
• durable_successor: optional A3-finalized successor
• transition_state: one of the states above
• conflict_evidence: optional witness or transition evidence when conflict-tainted
• emergency policy fields such as suspect authority, quarantine epoch, and prune-before epoch when an emergency transition is active

The AMP message ratchet consumes this reducer output. It does not author membership truth, choose between transitions, or repair missing control-plane facts.

7. Flow Budgets

Flow budgets track message sending allowances between authorities. The FlowBudget structure uses semilattice semantics for distributed convergence:

#![allow(unused)]
fn main() {
pub struct FlowBudget {
    pub limit: u64,
    pub spent: u64,
    pub epoch: Epoch,
}

impl FlowBudget {
    pub fn merge(&self, other: &Self) -> Self {
        Self {
            limit: self.limit.min(other.limit),
            spent: self.spent.max(other.spent),
            epoch: if self.epoch.value() >= other.epoch.value() {
                self.epoch
            } else {
                other.epoch
            },
        }
    }
}
}

The spent field uses join-semilattice (max) because charges only increase. The limit field uses meet-semilattice (min) because the most restrictive limit wins. The epoch field advances monotonically. Spent resets on epoch rotation.

Flow budget tracking operates at the runtime layer via FlowBudgetManager. The RelationalState includes a flow_budgets map for CRDT-based replication of budget state across replicas.

8. Receipts and Accountability

Receipts reference the current epoch commitment so reducers can reject stale receipts automatically. The RendezvousReceipt variant in FactContent stores accountability proofs (envelope ID, authority, timestamp, signature). Receipts are stored as relational facts scoped to the emitting context. This coupling ensures that receipt validity follows commitment tree epochs.

9. Snapshots and Garbage Collection

Snapshots summarize all prior facts. A snapshot fact contains a state hash, the list of superseded facts, and a sequence number. A snapshot establishes a high water mark. Facts older than the snapshot can be pruned.

#![allow(unused)]
fn main() {
pub struct SnapshotFact {
    pub state_hash: Hash32,
    pub superseded_facts: Vec<OrderTime>,
    pub sequence: u64,
}
}

Garbage collection removes pruned facts while preserving logical meaning. Pruning does not change the result of reduction. The GC algorithm uses safety margins to prevent premature pruning:

• Default skip window: 1024 generations
• Safety margin: skip_window / 2
• Pruning boundary: max_generation - (2 * skip_window) - safety_margin

Helper functions (compute_checkpoint_pruning_boundary, can_prune_checkpoint, can_prune_proposed_bump) determine what can be safely pruned based on generation boundaries.

10. Journal Effects Integration

The effect system provides journal operations through JournalEffects. This trait handles persistence, merging, and flow budget tracking:

#![allow(unused)]
fn main() {
#[async_trait]
pub trait JournalEffects: Send + Sync {
    async fn merge_facts(&self, target: Journal, delta: Journal) -> Result<Journal, AuraError>;
    async fn refine_caps(&self, target: Journal, refinement: Journal) -> Result<Journal, AuraError>;
    async fn get_journal(&self) -> Result<Journal, AuraError>;
    async fn persist_journal(&self, journal: &Journal) -> Result<(), AuraError>;
    async fn get_flow_budget(&self, context: &ContextId, peer: &AuthorityId) -> Result<FlowBudget, AuraError>;
    async fn update_flow_budget(&self, context: &ContextId, peer: &AuthorityId, budget: &FlowBudget) -> Result<FlowBudget, AuraError>;
    async fn charge_flow_budget(&self, context: &ContextId, peer: &AuthorityId, cost: FlowCost) -> Result<FlowBudget, AuraError>;
}
}

The effect layer writes facts to persistent storage. Replica synchronization loads facts through effect handlers into journal memory. The effect layer guarantees durability but does not affect CRDT merge semantics.

At the choreography runtime boundary, journal coupling is always driven by guard/effect commands. Generated choreography annotations and runtime guard checks emit EffectCommand values, and JournalCoupler ensures journal commits occur before transport observables. In VM execution, AuraVmEffectHandler emits envelopes, but journal writes still flow through the same EffectInterpreter + JournalEffects path.

11. AttestedOp Structure

AttestedOp exists in two layers with different levels of detail:

Layer 1 (aura-core) - Full operation metadata:

#![allow(unused)]
fn main() {
pub struct AttestedOp {
    pub op: TreeOp,
    pub agg_sig: Vec<u8>,
    pub signer_count: u16,
}

pub struct TreeOp {
    pub parent_epoch: Epoch,
    pub parent_commitment: TreeHash32,
    pub op: TreeOpKind,
    pub version: u16,
}
}

Layer 2 (aura-journal) - Flattened for journal storage:

#![allow(unused)]
fn main() {
pub struct AttestedOp {
    pub tree_op: TreeOpKind,
    pub parent_commitment: Hash32,
    pub new_commitment: Hash32,
    pub witness_threshold: u16,
    pub signature: Vec<u8>,
}
}

The aura-core version includes epoch and version for full verification. The aura-journal version includes computed commitments for efficient reduction.

12. Invariants

The journal and reduction architecture satisfy several invariants:

• Convergence: All replicas reach the same state when they have the same facts
• Idempotence: Repeated merges or reductions do not change state
• Determinism: Reduction produces identical output for identical input across all replicas
• No HashMap iteration: Uses BTreeMap for deterministic ordering
• No system time: Uses OrderTime tokens for ordering
• No floating point: All arithmetic is exact

These invariants guarantee correct distributed behavior. They also support offline operation with eventual consistency. They form the foundation for Aura's account and relational context state machines.

13. Fact Validation Pipeline

Every fact inserted into a journal must be validated before merge. The following steps outline the required checks and the effect traits responsible for each fact type:

13.1 AttestedOp Facts

Checks

• Verify the threshold signature (agg_sig) using the two-phase verification model from aura-core::tree::verification:
  • verify_attested_op(): Cryptographic signature check against BranchSigningKey stored in TreeState
  • check_attested_op(): Full verification plus state consistency (epoch, parent commitment)
• Ensure the referenced parent state exists locally. Otherwise request missing facts.
• Confirm the operation is well-formed (e.g., AddLeaf indexes a valid parent node).

See Tree Operation Verification for details on the verify/check model and binding message security.

Responsible Effects

• CryptoEffects for FROST signature verification via verify_attested_op().
• JournalEffects for parent lookup, state consistency via check_attested_op(), and conflict detection.
• StorageEffects to persist the fact once validated.

13.2 Relational Facts

Checks

• Validate that each authority commitment referenced in the fact matches the current reduced state (AuthorityState::root_commitment).
• Verify Aura Consensus proofs if present (guardian bindings, recovery grants).
• Enforce application-specific invariants (e.g., no duplicate guardian bindings).

Responsible Effects

• AuthorizationEffects / RelationalEffects for context membership checks.
• CryptoEffects for consensus proof verification.
• JournalEffects for context-specific merge.

13.3 FlowBudget Facts

Checks

• Ensure spent deltas are non-negative and reference the active epoch for the (ContextId, peer) pair.
• Reject facts that would decrease the recorded spent (monotone requirement).
• Validate receipt signatures associated with the charge (see 111_transport_and_information_flow.md).

Responsible Effects

• FlowBudgetEffects (or FlowGuard) produce the fact and enforce monotonicity before inserting.
• JournalEffects gate insertion to prevent stale epochs from updating headroom.

13.4 Snapshot Facts

Checks

• Confirm the snapshot state_hash matches the hash of all facts below the snapshot.
• Ensure no newer snapshot already exists for the namespace (check sequence number).
• Verify that pruning according to the snapshot does not remove facts still referenced by receipts or pending consensus operations.

Responsible Effects

• JournalEffects compute and validate snapshot digests.
• StorageEffects persist the snapshot atomically with pruning metadata.

By clearly separating validation responsibilities, runtime authors know which effect handlers must participate before a fact mutation is committed. This structure keeps fact semantics consistent across authorities and contexts.

14. Consistency Metadata Schema

Facts carry consistency metadata for tracking agreement level, propagation status, and acknowledgments. See Operation Categories for the full consistency metadata type definitions.

14.1 Fact Schema Fields

The base Fact structure (section 2) is extended with consistency metadata fields (added via serde defaults for backwards compatibility):

14.2 Ack Storage Table

For facts with ack_tracked = true, acknowledgments are stored in a separate table:

14.3 Journal API for Consistency

The Journal API provides methods for acknowledgment tracking: record_ack records an acknowledgment from a peer, get_acks retrieves all acknowledgments for a fact, and gc_ack_tracking garbage collects acknowledgment data based on policy.

See Also

• Database Architecture for query system and Datalog integration
• Operation Categories for consistency metadata types
• Maintenance for snapshot and garbage collection pipeline
• Relational Contexts for context journal structure
• Authority and Identity for commitment tree operations

Required moderation evidence

Required moderation queries reject corrupt ban/mute and reversal payloads, unsupported schemas, declared-codec mismatch, oversized inventories, and wrapper/payload context mismatch before returning a denial decision. Observational compatibility decoding is separate; decoding success alone is not journal commit/authentication provenance.

Canonical codec failure provenance

Required canonical serialization retains the original concrete ciborium failure through the standard error source chain. Display diagnostics keep their existing prefixes; pure canonical-format validation failures have no invented codec source. Canonical bytes and strict decoding rules are unchanged. Native semantic classification remains SerializationFailure, including when a codec cause is carried through storage or checkpoint context. Serialized presentation diagnostics do not establish native failure provenance.

Enrollment baseline publication

An enrollment baseline is installed only after independent manifest verification. Its storage owner retains the original local history digest before replacement and publishes complete operation content before the canonical ordered index. Failed index acknowledgment is an uncertain publication outcome and requires canonical reread. Replaying an already installed baseline preserves later local operations. An original-publication record is coordination evidence, not authorization.

Immutable local enrollment decision records

Locally retained enrollment setup, pending-generation, registration, response, and issued-manifest records preserve the first canonical decision via atomic absent-only provider publication. A competing existing value must pass bounded exact binding validation; accepted-response and issued-manifest evidence must be cryptographically revalidated. Different valid signature bytes do not replace the original decision. These local records are recovery evidence, not consensus facts. Generic mutable secure-provider write access does not establish domain authorization or lifetime immutability.

Required envelope decoding failures

Required domain-fact decoding validates the declared domain, exact current schema, payload bound and canonical DAG-CBOR encoding before consuming a payload. An existing envelope and its canonical encoded form have the same validation contract. Retired and future schemas and JSON envelopes are rejected; malformed DAG-CBOR retains the original canonical serialization cause. A decode failure is not fact absence. Successful decoding establishes value shape, not journal commitment or canonical entity materialization authority.

Authorization

Overview

Aura authorizes every observable action through Biscuit capability evaluation combined with sovereign policy and flow budgets. The authorization pipeline spans AuthorizationEffects, the guard chain, and receipt accounting. This document describes the data flow and integration points.

Canonical Capability Vocabulary

Aura uses one canonical capability vocabulary based on validated CapabilityName values.

• First-party capabilities are declared in the crate that owns the behavior, using typed capability families generated from #[capability_family(...)].
• Token issuance uses explicit grant profiles or explicit validated CapabilityName sets at the issuance boundary. There is no implicit "grant every declared capability" path.
• Guard snapshots carry evaluated frontiers only. They do not carry declared families, candidate sets, or fallback broad grants.
• Raw capability strings are admitted only at explicit parsing boundaries such as Biscuit decoding and choreography DSL parsing, where invalid values fail closed.

Out-of-tree modules follow the same shape, but their capability families must be declared in admitted module manifests rather than handwritten in host runtime code.

Biscuit Capability Model

Biscuit tokens encode attenuation chains. Each attenuation step applies additional caveats that shrink authority through meet composition. Aura stores Biscuit material outside the replicated CRDT. Local runtimes evaluate tokens at send time against typed candidate sets supplied by the owning domain and cache the resulting lattice element for the active ContextId.

Cached entries expire on epoch change or when policy revokes a capability. Policy data always participates in the meet. A token can only reduce authority relative to local policy.

flowchart LR
    A[frontier, token] -->|verify signature| B[parsed token]
    B -->|apply caveats| C[frontier ∩ caveats]
    C -->|apply policy| D[result ∩ policy]
    D -->|return| E[Cap element]

This algorithm produces a meet-monotone capability frontier. Step 1 ensures provenance. Steps 2 and 3 ensure evaluation never widens authority. Step 4 feeds the guard chain with a cached outcome.

Guard Chain

Authorization evaluation feeds the transport guard chain. All documents reference this section to avoid divergence.

flowchart LR
    A[Send request] --> B[CapGuard]
    B --> C[FlowGuard]
    C --> D[JournalCoupler]
    D --> E[Transport send]

This diagram shows the guard chain sequence. CapGuard performs Biscuit evaluation. FlowGuard charges the budget. JournalCoupler commits facts before transport.

Guard evaluation is pure and synchronous over a prepared GuardSnapshot. CapGuard reads an evaluated frontier and any inline Biscuit token already present in the snapshot. Snapshot builders may begin with a typed candidate set, but they must evaluate that set against the Biscuit/policy frontier before publishing capabilities into the snapshot. FlowGuard and JournalCoupler emit EffectCommand items rather than executing I/O directly. An async interpreter executes those commands in production or simulation.

Only after all guards pass does transport emit a packet. Any failure returns locally and leaves no observable side effect. DKG payloads require proportional budget charges before any transport send.

Telltale Integration

Aura uses Telltale runtime admission and VM guard checkpoints. Runtime admission gates whether a runtime profile may execute. VM acquire and release guards gate per-session resource leases inside VM execution. The Aura guard chain remains the authoritative policy and accounting path for application sends.

Failure handling is layered. Admission failure rejects engine startup. VM acquire deny blocks the guarded VM action. Aura guard-chain failure denies transport and returns deterministic effect errors.

Runtime Capability Admission

Aura uses a dedicated admission surface for theorem-pack and runtime capability checks before choreography execution. RuntimeCapabilityEffects in aura-core defines capability inventory queries and admission checks. RuntimeCapabilityHandler in aura-effects stores a boot-time immutable capability snapshot. The aura-protocol::admission module declares protocol requirements and maps them to capability keys.

Current protocol capability keys include byzantine_envelope for consensus ceremony admission, termination_bounded for sync epoch-rotation admission, reconfiguration for dynamic topology transfer paths, and mixed_determinism for cross-target mixed lanes.

Execution order is runtime capability admission first, then VM profile gates, then the Aura guard chain. Admission diagnostics must respect Aura privacy constraints. Production runtime paths must not emit plaintext capability inventory events. Admission failures use redacted capability references.

Failure Handling and Caching

Runtimes cache evaluated capability frontiers per context and predicate with an epoch tag. Cache entries invalidate when journal policy facts change or when the epoch rotates.

CapGuard failures return AuthorizationError::Denied without charging flow or touching the journal. FlowGuard failures return FlowError::InsufficientBudget without emitting transport traffic. JournalCoupler failures surface as JournalError::CommitAborted and instruct the protocol to retry after reconciling journal state.

This isolation keeps the guard chain deterministic and side-channel free.

Biscuit Token Workflow

Biscuit tokens guarantee cryptographically verifiable, attenuated delegation chains. Each token carries a signature chain that prevents forgery and supports offline verification without contacting the issuer. Attenuation is monotone: each delegation step can only reduce authority, never widen it. Epoch rotation provides revocation by invalidating old tokens. Aura does not maintain a separate per-token revocation list in aura-authorization; revocation is authority-wide and anchored to the currently trusted root key for that authority.

Issuance is explicit. The runtime selects a reviewed token grant profile and materializes a concrete Vec<CapabilityName> at the issuance boundary. That issuance profile is separate from the evaluated frontier that later appears in guard snapshots. The two must not be conflated: profiles declare what may be granted, while snapshots publish what is currently admitted after Biscuit and policy evaluation.

See Effects and Handlers Guide for Biscuit workflow implementation.

Guard Chain Integration

Biscuit authorization integrates with the guard chain through three phases: cryptographic verification, synchronous guard evaluation over a prepared GuardSnapshot, and effect command interpretation. If any phase fails, the operation returns an error without observable side effects.

Guard operation identifiers are typed guard inputs, not ambient raw strings. Empty or whitespace-only custom operations are rejected before evaluation, and missing authorization metadata is a denial rather than a bypass.

Sync peer-token validation follows the same fail-closed model. Production sync validation requires a configured Biscuit root public key and a concrete authority/operation scope; deterministic roots and dummy scopes are test fixtures only.

See Effects and Handlers Guide for guard chain integration patterns.

Authorization Scenarios

All authorization scenarios (local device operations, cross-authority delegation, API access control, guardian recovery, storage, and relaying) are handled through Biscuit token attenuation and sovereign policy integration. Token scope and restrictions vary by scenario but follow the same meet-monotone evaluation path.

See Effects and Handlers Guide for authorization scenario patterns.

Performance and Caching

Authorization results are cached per authority, token hash, and resource scope with epoch-based invalidation. Cache entries invalidate on epoch rotation or policy update. Signature verification scales with chain length. Datalog evaluation scales with facts times rules. Attenuation is constant-cost.

See Distributed Maintenance Guide for cache configuration.

Security Model

Signature-chain verification establishes token integrity under the supplied root key. Authorization additionally requires that root to be selected independently from trusted authority state. A root carried alongside serialized capability bytes is algebraic metadata and cannot establish its own issuer trust or authorize an operation.

Cryptographic signature verification prevents token forgery. Epoch scoping limits token lifetime and replay attacks. Attenuation preserves security while growing verification cost proportional to chain length. Root key compromise invalidates all derived tokens.

Authority-based ResourceScope prevents cross-authority access. Local sovereign policy integration provides an additional security layer. Guard chain isolation ensures authorization failures leak no sensitive information.

Implementation References

The Cap type in aura-core/src/domain/journal.rs wraps serialized Biscuit tokens with optional root key storage. The Cap::meet() implementation computes capability intersection. Tokens from the same issuer return the more attenuated token. Tokens from different issuers return bottom.

BiscuitAuthorizationBridge in aura-guards/src/authorization.rs handles guard chain integration. TokenAuthority, TokenGrantProfile, and BiscuitTokenManager in aura-authorization/src/biscuit_token.rs handle token creation and attenuation. Capability families live in the owning feature or domain crates, not in one central global enum. ResourceScope in aura-core/src/types/scope.rs defines authority-centric resource patterns.

See Transport and Information Flow for flow budget details. See Journal for fact commit semantics.

Persisted startup authorization

Startup distinguishes confirmed absence of a persisted authority Biscuit from a failed required read. Absent credentials permit the explicit new-account bootstrap path; storage failure and malformed or unverifiable persisted tokens prevent runtime assembly. A restored cache is published only after bounded record validation and token verification against its retained root key. These checks preserve concrete verification and storage causes.

Authorization cache publication is runtime-private. Observed cache snapshots cannot be submitted as authority to a public cache setter. Bootstrap and verified hydration retain the production publication path; deliberately malformed cache fixtures use a test-only crate-local adapter.

Guardian invitation first binding

A Guardian acceptance is bound to the retained original issued invitation and its issuer verifier. Acceptance recording requires that invitation's owned identity evidence and its original runtime; response fields cannot substitute another issuer key, invitation type or subject. The recovery-key signature proves possession for this particular invitation. Recording that key establishes the Guardian recovery binding and does not authorize device membership. Original imported invitation continuity and local recovery-pair integrity are distinct verification roles.

Database Architecture

This document specifies the architecture for Aura's query system. The journal is the database. Datalog is the query language. Biscuit provides authorization.

1. Core Principles

1.1 Database-as-Journal Equivalence

Aura's fact-based journal functions as the database. There is no separate database layer. The equivalence maps traditional database concepts to Aura components.

Aura treats database state as a composite of the fact journal and the capability frontier. Query execution always combines the reduced fact state with the current capability lattice (the JournalState composite) to enforce authorization and isolate contexts.

1.2 Authority-First Data Model

Aura's database is partitioned by cryptographic authorities. An AuthorityId owns facts that implement JoinSemilattice. State is derived from those facts.

Data is naturally sharded by authority. Cross-authority operations require explicit choreography. Privacy is the default because no cross-authority visibility exists without permission.

2. Query System

2.1 Query Trait

The Query trait defines typed queries that compile to Datalog:

#![allow(unused)]
fn main() {
pub trait Query: Send + Sync + Clone + 'static {
    /// The result type of this query
    type Result: Clone + Send + Sync + Default + 'static;

    /// Compile this query to a Datalog program
    fn to_datalog(&self) -> DatalogProgram;

    /// Get required Biscuit capabilities for authorization
    fn required_capabilities(&self) -> Vec<QueryCapability>;

    /// Get fact predicates for invalidation tracking
    fn dependencies(&self) -> Vec<FactPredicate>;

    /// Parse Datalog bindings to typed result
    fn parse(bindings: DatalogBindings) -> Result<Self::Result, QueryParseError>;

    /// Unique identifier for caching and subscriptions
    fn query_id(&self) -> String;
}
}

This design separates query definition from execution, enabling:

• Portable query definitions across runtimes
• Authorization checking before execution
• Reactive subscriptions via dependency tracking

2.2 Datalog Types

Queries compile to DatalogProgram, the intermediate representation:

#![allow(unused)]
fn main() {
pub struct DatalogProgram {
    pub rules: Vec<DatalogRule>,
    pub facts: Vec<DatalogFact>,
    pub goal: Option<String>,
}

pub struct DatalogRule {
    pub head: DatalogFact,
    pub body: Vec<DatalogFact>,
}

pub struct DatalogFact {
    pub predicate: String,
    pub args: Vec<DatalogValue>,
}

pub enum DatalogValue {
    String(String),
    Integer(i64),
    Boolean(bool),
    Variable(String),
    Symbol(String),
    Null,
}
}

Programs convert to Datalog source via to_datalog_source():

#![allow(unused)]
fn main() {
let program = DatalogProgram::new(vec![
    DatalogRule::new(DatalogFact::new("active_user", vec![DatalogValue::var("name")]))
        .when(DatalogFact::new("user", vec![DatalogValue::var("name")]))
        .when(DatalogFact::new("online", vec![DatalogValue::var("name")]))
])
.with_goal("active_user($name)");

let source = program.to_datalog_source();
// Output:
// active_user($name) :- user($name), online($name).
// ?- active_user($name).
}

2.3 Fact Predicates

FactPredicate patterns determine query invalidation:

#![allow(unused)]
fn main() {
pub struct FactPredicate {
    /// The predicate name to match
    pub name: String,
    /// Optional positional argument patterns (None = wildcard)
    pub arg_patterns: Vec<Option<String>>,
    /// Named field constraints for structured facts
    pub named_constraints: BTreeMap<String, String>,
}

impl FactPredicate {
    /// Match any fact with the given name
    pub fn named(name: impl Into<String>) -> Self;

    /// Match facts with specific named field constraints
    pub fn with_args(name: impl Into<String>, args: Vec<(&str, &str)>) -> Self;

    /// Add a positional argument pattern
    pub fn with_arg(self, pattern: Option<String>) -> Self;

    /// Add a named field constraint
    pub fn with_named_constraint(self, name: impl Into<String>, value: impl Into<String>) -> Self;

    /// Check if this predicate matches another
    pub fn matches(&self, other: &FactPredicate) -> bool;

    /// Check if this predicate matches a fact with positional arguments
    pub fn matches_fact(&self, fact_name: &str, fact_args: &[String]) -> bool;

    /// Check if this predicate matches a fact with named fields
    pub fn matches_named_fact(&self, fact_name: &str, fact_fields: &BTreeMap<String, String>) -> bool;
}
}

When facts change, subscriptions matching the predicate re-evaluate.

2.4 Query Capabilities

Authorization integrates with Biscuit via QueryCapability:

#![allow(unused)]
fn main() {
pub struct QueryCapability {
    pub resource: String,
    pub action: String,
    pub constraints: Vec<(String, String)>,
}

impl QueryCapability {
    pub fn read(resource: impl Into<String>) -> Self;
    pub fn list(resource: impl Into<String>) -> Self;
    pub fn with_constraint(self, key: impl Into<String>, value: impl Into<String>) -> Self;
    pub fn to_biscuit_check(&self) -> String;
}
}

Capabilities convert to Biscuit checks:

#![allow(unused)]
fn main() {
let cap = QueryCapability::read("channels").with_constraint("owner", "alice");
assert_eq!(
    cap.to_biscuit_check(),
    "check if right(\"channels\", \"read\"), owner == \"alice\""
);
}

3. Query Effects

3.1 QueryEffects Trait

QueryEffects executes queries against the journal:

#![allow(unused)]
fn main() {
#[async_trait]
pub trait QueryEffects: Send + Sync {
    /// Execute a one-shot typed query
    async fn query<Q: Query>(&self, query: &Q) -> Result<Q::Result, QueryError>;

    /// Execute a raw Datalog program
    async fn query_raw(&self, program: &DatalogProgram) -> Result<DatalogBindings, QueryError>;

    /// Subscribe to query updates when facts change
    fn subscribe<Q: Query>(&self, query: &Q) -> QuerySubscription<Q::Result>;

    /// Pre-check authorization
    async fn check_capabilities(&self, capabilities: &[QueryCapability]) -> Result<(), QueryError>;

    /// Trigger re-evaluation for matching subscriptions
    async fn invalidate(&self, predicate: &FactPredicate);
}
}

3.2 Query Execution Flow

flowchart TD
    A[Query::to_datalog] --> B[QueryEffects::query];
    B --> C{Check capabilities};
    C -->|Pass| D[Load journal facts];
    C -->|Fail| E[QueryError::AuthorizationFailed];
    D --> F[Execute Datalog];
    F --> G[Query::parse];
    G --> H[Typed result];

3.3 Reactive Subscriptions

QuerySubscription wraps SignalStream for live updates:

#![allow(unused)]
fn main() {
pub struct QuerySubscription<T: Clone + Send + 'static> {
    stream: SignalStream<T>,
    query_id: String,
}

impl<T: Clone + Send + 'static> QuerySubscription<T> {
    pub fn query_id(&self) -> &str;
    pub fn try_recv(&mut self) -> Option<T>;
    pub async fn recv(&mut self) -> Result<T, QueryError>;
}
}

Usage pattern:

#![allow(unused)]
fn main() {
let mut subscription = effects.subscribe(&ChannelsQuery::default());
while let Ok(channels) = subscription.recv().await {
    println!("Channels updated: {} total", channels.len());
}
}

3.4 Query Isolation

QueryIsolation specifies consistency requirements for queries:

#![allow(unused)]
fn main() {
pub enum QueryIsolation {
    /// See all facts including uncommitted (CRDT state) - fastest
    ReadUncommitted,
    /// Only see facts with consensus commit
    ReadCommitted { wait_for: Vec<ConsensusId> },
    /// Snapshot at specific prestate (time-travel query)
    Snapshot { prestate_hash: Hash32 },
    /// Wait for all pending consensus in scope
    ReadLatest { scope: ResourceScope },
}
}

Usage:

#![allow(unused)]
fn main() {
// Fast query - may see uncommitted facts
let result = effects.query(&ChannelsQuery::default()).await?;

// Wait for specific consensus before querying
let result = effects.query_with_isolation(
    &ChannelsQuery::default(),
    QueryIsolation::ReadCommitted { wait_for: vec![consensus_id] },
).await?;
}

3.5 Query Statistics