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: Temporal isolation of budget and receipt state
• 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.

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.

Epoch rotation 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.

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<Vec<u8>, CryptoError>;
    async fn frost_create_signing_package(&self, message: &[u8], nonces: &[Vec<u8>], participants: &[u16], public_key_package: &[u8]) -> Result<FrostSigningPackage, CryptoError>;
    async fn frost_sign_share(&self, signing_package: &FrostSigningPackage, key_share: &[u8], nonces: &[u8]) -> 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. 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.

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.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

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.

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

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.

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;
}
}

The trait defines four core operations for reactive state. The read method returns the current value. The emit method updates the value. The subscribe method returns a stream of changes. The register method initializes a signal with a default value. See Runtime for reactive scheduling implementation. Subscribing an unregistered signal fails fast. Aura no longer permits "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.

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.

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.

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.

See System Internals Guide for service lifecycle implementation.

Runtime Timeout Policy

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
• 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
• 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.

#![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.

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:

• 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

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.

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.

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 (Checklist + Lint)

Domain facts are the extensibility mechanism for Layer 2 crates. Every domain fact must follow this contract to ensure cross-replica determinism and schema stability:

• Type ID: define a *_FACT_TYPE_ID constant (unique, registered in crates/aura-agent/src/fact_types.rs).
• Schema version: specify a schema version (via #[domain_fact(schema_version = N)] or *_FACT_SCHEMA_VERSION).
• Canonical encoding: use #[derive(DomainFact)] or explicit encode_domain_fact / VersionedMessage helpers.
• Context derivation: declare context / context_fn for DomainFact or implement a stable context_id() derivation.
• Reducer registration: provide a FactReducer and register it in the central registry (crates/aura-agent/src/fact_registry.rs).

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.

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.

6.1 AMP Channel Epoch Transition Reduction

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

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

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.

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

QueryStats provides execution metrics:

#![allow(unused)]
fn main() {
pub struct QueryStats {
    pub execution_time: Duration,
    pub facts_scanned: u32,
    pub facts_matched: u32,
    pub cache_hit: bool,
    pub isolation_used: QueryIsolation,
    pub consensus_wait_time: Option<Duration>,
    /// Consistency metadata for matched facts
    pub consistency: ConsistencyMap,
}
}

Usage:

#![allow(unused)]
fn main() {
let (channels, stats) = effects.query_with_stats(&ChannelsQuery::default()).await?;
println!("Query took {:?}, scanned {} facts", stats.execution_time, stats.facts_scanned);
}

3.6 Query Errors

#![allow(unused)]
fn main() {
pub enum QueryError {
    AuthorizationFailed { reason: String },
    MissingCapability { capability: String },
    ExecutionError { reason: String },
    ParseError(QueryParseError),
    SubscriptionNotFound { query_id: String },
    JournalError { reason: String },
    HandlerUnavailable,
    Internal { reason: String },
    ConsensusTimeout { consensus_id: ConsensusId },
    SnapshotNotAvailable { prestate_hash: Hash32 },
    IsolationNotSupported { reason: String },
}
}

4. Concrete Query Examples

Concrete queries (such as ChannelsQuery and MessagesQuery) implement the Query trait by compiling to Datalog programs, declaring required Biscuit capabilities, specifying fact predicate dependencies for invalidation, and parsing typed results from Datalog bindings.

See Effects and Handlers Guide for query implementation examples.

5. Indexing Layer

5.1 IndexedJournalEffects

The IndexedJournalEffects trait provides efficient indexed lookups:

#![allow(unused)]
fn main() {
pub trait IndexedJournalEffects: Send + Sync {
    /// Subscribe to journal fact updates as they are added
    fn watch_facts(&self) -> Box<dyn FactStreamReceiver>;

    /// Get all facts with the given predicate/key
    async fn facts_by_predicate(&self, predicate: &str) -> Result<Vec<IndexedFact>, AuraError>;

    /// Get all facts created by the given authority
    async fn facts_by_authority(&self, authority: &AuthorityId) -> Result<Vec<IndexedFact>, AuraError>;

    /// Get all facts within the given time range (inclusive)
    async fn facts_in_range(&self, start: TimeStamp, end: TimeStamp) -> Result<Vec<IndexedFact>, AuraError>;

    /// Return all indexed facts (append-only view)
    async fn all_facts(&self) -> Result<Vec<IndexedFact>, AuraError>;

    /// Fast membership test using Bloom filter
    fn might_contain(&self, predicate: &str, value: &FactValue) -> bool;

    /// Get the Merkle root commitment for the current index state
    async fn merkle_root(&self) -> Result<[u8; 32], AuraError>;

    /// Verify a fact against the Merkle tree
    async fn verify_fact_inclusion(&self, fact: &IndexedFact) -> Result<bool, AuraError>;

    /// Get the Bloom filter for fast membership tests
    async fn get_bloom_filter(&self) -> Result<BloomFilter, AuraError>;

    /// Get statistics about the index
    async fn index_stats(&self) -> Result<IndexStats, AuraError>;
}
}

The might_contain method uses Bloom filters for fast negative answers with O(1) lookup and less than 1% false positive rate.

5.2 Index Structure

#![allow(unused)]
fn main() {
pub struct AuthorityIndex {
    merkle_tree: MerkleTree<FactHash>,
    predicate_filters: BTreeMap<String, BloomFilter>,
    by_predicate: BTreeMap<String, Vec<FactId>>,
    by_authority: BTreeMap<AuthorityId, Vec<FactId>>,
    by_time: BTreeMap<TimeStamp, Vec<FactId>>,
}
}

• Merkle trees: Integrity verification
• Bloom filters: Fast membership tests (<1% false positive rate)
• B-trees: Ordered lookups (O(log n))

Indexes update on fact commit. Performance target: <10ms for 10k facts.

6. Biscuit Integration

6.1 AuraQuery Wrapper

AuraQuery wraps Biscuit's authorizer for query execution:

#![allow(unused)]
fn main() {
pub struct AuraQuery {
    authorizer: biscuit_auth::Authorizer,
}

impl AuraQuery {
    pub fn add_journal_facts(&mut self, facts: &[Fact]) -> Result<()> {
        for fact in facts {
            self.authorizer.add_fact(fact.to_biscuit_fact()?)?;
        }
        Ok(())
    }

    pub fn query(&self, rule: &str) -> Result<Vec<biscuit_auth::Fact>> {
        self.authorizer.query(rule)
    }
}
}

6.2 Guard Chain Integration

Database operations flow through the guard chain:

flowchart LR
    A[Query Request] --> B[CapGuard];
    B --> C[FlowGuard];
    C --> D[JournalCoupler];
    D --> E[QueryEffects];

1. CapGuard: Evaluates Biscuit token authorization
2. FlowGuard: Charges budget for query cost
3. JournalCoupler: Logs query execution
4. QueryEffects: Executes the query

Each guard must succeed before the next executes.

7. Transaction Model

7.1 Coordination Matrix

Database operations use two orthogonal dimensions:

7.2 Examples

• Monotone + Single: Append message to own channel (journal.insert_fact())
• Monotone + Cross-Authority: Guardian adds trust fact (journal.insert_relational_fact())
• Consensus + Single: Remove device from account (consensus_single_shot())
• Consensus + Cross-Authority: Recovery grant with guardian approval (federated_consensus())

Aura Consensus is not linearizable by default. Each consensus instance independently agrees on a single operation and prestate. To sequence operations, use session types (see MPST and Choreography).

Agreement modes are orthogonal to the coordination matrix: A1 (provisional) and A2 (soft-safe) may provide immediate usability, but any durable shared database state must be A3 (consensus-finalized) with prestate binding. Soft-safe windows should be bounded with convergence certificates and explicit reversion facts.

BFT-DKG integration: When key material is required (K3), the database must bind operations to a consensus-finalized DkgTranscriptCommit. This ensures the transaction prestate and the cryptographic prestate are aligned.

MutationReceipt indicates whether a mutation completed immediately (monotone/CRDT) or was submitted to consensus.

See Choreography Development Guide for mutation receipt patterns and BFT-DKG transaction integration.

8. Temporal Database Model

Aura uses a Datomic-inspired immutable database model where all changes are represented as append-only facts with temporal metadata.

8.1 Core Concepts

Facts are never deleted. They are either:

• Asserted: Added to a scope
• Retracted: Marked as no longer valid (but remain queryable in history)
• Epoch-bumped: Bulk invalidation of facts in a scope
• Checkpointed: Snapshotted for temporal queries

Facts are organized in hierarchical scopes:

#![allow(unused)]
fn main() {
// Scope path examples
"authority:abc123"                    // Authority-level
"authority:abc123/chat"               // Named sub-scope
"authority:abc123/chat/channel:xyz"   // Typed sub-scope
}

Facts progress through finality levels:

#![allow(unused)]
fn main() {
pub enum Finality {
    Local,                           // Written locally only
    Replicated { ack_count: u16 },   // Acknowledged by N peers
    Checkpointed,                    // In a durable checkpoint
    Consensus { proof: ConsensusId }, // Confirmed via consensus
    Anchored { anchor: AnchorProof }, // External chain anchor
}
}

8.2 Fact Operations

Fact operations are classified by monotonicity. Assert and Checkpoint are monotonic (no coordination required). Retract and EpochBump are non-monotonic (may require consensus). The FactEffects trait provides the write interface, supporting single operations, atomic transactions, finality waiting, and temporal queries.

The hybrid transaction model uses direct apply_op() for simple monotonic operations and explicit Transaction grouping for atomic multi-operation batches. Temporal queries support as-of, since, and history range modes. Per-scope finality configuration controls default and minimum finality levels with optional per-content overrides.

See Effects and Handlers Guide for temporal query patterns and finality configuration.

9. Consistency Metadata

Query results include consistency metadata that tracks the agreement, propagation, and acknowledgment status of each fact.

9.1 ConsistencyMap

The ConsistencyMap type provides per-item consistency status in query results:

#![allow(unused)]
fn main() {
pub struct ConsistencyMap {
    entries: HashMap<String, Consistency>,
}

impl ConsistencyMap {
    pub fn get(&self, id: &str) -> Option<&Consistency>;
    pub fn is_finalized(&self, id: &str) -> bool;
    pub fn acked_by(&self, id: &str) -> Option<&[AckRecord]>;
}
}

9.2 Querying with Consistency

Use query_with_consistency() to get both results and consistency metadata:

#![allow(unused)]
fn main() {
let (messages, consistency) = handler.query_with_consistency(&MessagesQuery::default()).await?;

for msg in &messages {
    let status = if consistency.is_finalized(&msg.id) {
        "finalized"
    } else {
        "pending"
    };
    println!("{}: {}", msg.content, status);
}
}

9.3 QueryStats with Consistency

QueryStats now includes a ConsistencyMap for tracking consistency of scanned facts:

#![allow(unused)]
fn main() {
let (result, stats) = handler.query_with_stats(&query).await?;
if stats.consistency.any_finalized() {
    println!("Some results are finalized");
}
}

9.4 Consistency Dimensions

Each Consistency entry tracks three orthogonal dimensions:

See Operation Categories for full details on these types and their usage.

10. Implementation Location

See Also

• Journal System - Fact storage, reduction, and flow budgets
• Operation Categories - Agreement, propagation, acknowledgment, and ceremony contract
• Authorization - Biscuit token evaluation
• Effect System - Effect implementation patterns

Consensus

This document describes the architecture of Aura Consensus. It defines the problem model, protocol phases, data structures, and integration with journals. It explains how consensus provides single-shot agreement for non-monotone operations such as account updates or relational context operations.

1. Problem Model

Aura uses consensus only for operations that cannot be expressed as monotone growth. Consensus produces a commit fact. The commit fact is inserted into one or more journals and drives deterministic reduction. Aura does not maintain a global log. Consensus operates in the scope of an authority or a relational context.

Consensus is single-shot. It agrees on a single operation and a single prestate. Commit facts are immutable and merge by join in journal namespaces.

A consensus instance uses a context-scoped committee. The committee contains witnesses selected by the authority or relational context. Committee members may be offline. The protocol completes even under partitions.

Consensus finalization is the single source of durable shared state. Fast-path coordination (provisional or soft-safe) may run in parallel for liveness, but its outputs must be superseded by commit facts. For BFT-DKG, consensus finalizes a transcript and emits DkgTranscriptCommit facts.

1.2 Witness Terminology

Aura uses witness (not validator) for consensus attestation participants.

• witness: attests that an operation is valid for a specific prestate and contributes consensus evidence.
• signer: contributes threshold signature shares in FROST.

Keeping witness and signer distinct avoids conflating consensus attestation responsibilities with cryptographic share-generation roles.

1.3 Consensus is NOT Linearizable by Default

Aura Consensus is single-shot agreement, not log-based linearization.

Each consensus instance independently agrees on:

• A single operation
• A single prestate
• Produces a single commit fact

Consensus does NOT provide global operation ordering, sequential linearization across instances, or automatic operation dependencies.

To sequence operations, use session types (docs/110_mpst_and_choreography.md) executed through Aura’s Telltale-backed choreography runtime (execute_as runners or VM backend):

#![allow(unused)]
fn main() {
use aura_mpst::{choreography, Role};

#[choreography]
async fn sequential_device_updates<C: EffectContext>(
    ctx: &C,
    account: Role<Account>,
    witnesses: Vec<Role<Witness>>,
) -> Result<(), AuraError> {
    // Session type enforces ordering:
    // 1. Update policy (must complete first)
    let policy_commit = consensus_single_shot(
        ctx,
        account.clone(),
        witnesses.clone(),
        TreeOp::UpdatePolicy { new_policy },
        prestate1.hash(),
    ).await?;

    // 2. Remove device (uses policy_commit as prestate)
    // Session type prevents op2 from starting until op1 completes
    let prestate2 = account.read_tree_state(ctx).await?;
    assert_eq!(prestate2.hash(), policy_commit.result_id.prestate_hash);

    let remove_commit = consensus_single_shot(
        ctx,
        account,
        witnesses,
        TreeOp::RemoveLeaf { target: device_id },
        prestate2.hash(),
    ).await?;

    Ok(())
}
}

Cross-reference: See docs/107_database.md §8 for database transaction integration.

2. Core Protocol

Aura Consensus has two paths. The fast path completes in one round trip. The fallback path uses epidemic gossip and a threshold race. Both paths produce the same commit fact once enough matching witness shares exist.

The fast path uses direct communication. The initiator broadcasts an execute message. Witnesses run the operation against the prestate. Witnesses return FROST shares. The initiator aggregates shares and produces a threshold signature. FROST primitives are in aura-core::crypto::tree_signing.

The fallback path triggers when witnesses disagree or when the initiator stalls. Witnesses exchange share proposals using bounded fanout gossip. Any witness that assembles a valid threshold signature broadcasts a complete commit fact.

3. Common Structures and Notation

Consensus uses the following core concepts and notation throughout the protocol.

Core Variables

• cid : ConsensusId - consensus instance identifier
• Op - operation being agreed on (application-defined)
• prestate - local pre-state for this instance (e.g., journal snapshot)
• prestate_hash = H(prestate) - hash of prestate
• rid = H(Op, prestate) - result identifier
• t - threshold. Adversary controls < t key shares.
• W - finite set of witnesses for this consensus instance

Per-Instance Tracking

Each consensus participant maintains per-cid state. The decided flags prevent double-voting. Proposals are keyed by (rid, prestate_hash) to group matching shares.

Equivocation Detection

Equivocation occurs when the same witness signs two different rid values under the same (cid, prestate_hash). This violates safety. The protocol detects and excludes equivocating shares.

4. Data Structures

Consensus instances use identifiers for operations and results.

#![allow(unused)]
fn main() {
/// Consensus instance identifier (derived from prestate and operation)
pub struct ConsensusId(pub Hash32);

impl ConsensusId {
    pub fn new(prestate_hash: Hash32, operation_hash: Hash32, nonce: u64) -> Self {
        // Hash of domain separator, prestate, operation, and nonce
    }
}
}

This structure identifies consensus instances. The result is identified by H(Op, prestate) computed inline.

A commit fact contains full consensus evidence including the operation, threshold signature, and participant list. Participants are recorded as AuthorityId values to preserve device privacy.

#![allow(unused)]
fn main() {
/// From crates/aura-consensus/src/types.rs
pub struct CommitFact {
    pub consensus_id: ConsensusId,
    pub prestate_hash: Hash32,
    pub operation_hash: Hash32,
    pub operation_bytes: Vec<u8>,
    pub threshold_signature: ThresholdSignature,
    pub group_public_key: Option<PublicKeyPackage>,
    pub participants: Vec<AuthorityId>,
    pub threshold: u16,
    pub timestamp: ProvenancedTime,
    pub fast_path: bool,
    pub byzantine_attestation: Option<ByzantineSafetyAttestation>,
}
}

The commit fact is the output of consensus. Every peer merges CommitFact into its journal CRDT. A peer finalizes when it accepts a valid threshold signature and inserts the corresponding CommitFact.

The commit fact is inserted into the appropriate journal namespace. This includes account journals for account updates and relational context journals for cross-authority operations.

Ordering of committed facts relies on OrderTime (or session/consensus sequencing), not on timestamps. ProvenancedTime is semantic metadata and must not be used for cross-domain total ordering or indexing.

4.1 Byzantine Admission and Attestation

Consensus-backed ceremonies (including BFT-DKG finalization) are admitted only after runtime capability checks for the consensus profile. Aura currently enforces theorem-pack/runtime capability requirements such as byzantine_envelope before executing DKG and threshold-signing paths.

Today this admission lives in the runtime bridge and threshold-signing services, not in the consensus choreography source. The current consensus choreography source file (crates/aura-consensus/src/protocol/choreography.tell) remains theorem-pack-free because it still models the message skeleton rather than the authoritative admission/evidence profile. Adding a theorem pack there now would be decorative.

Aura should revisit consensus theorem packs only when all of the following are true:

• the choreography owns a concrete consensus-profile admission surface rather than relying on runtime-local capability checks
• the required guarantee is better expressed as a choreography-level envelope, ordering, or synchrony contract
• Aura has a real runtime admission consumer for those choreography-level requirements beyond the existing byzantine_envelope capability gate

At admission, Aura captures a CapabilitySnapshot and records a ByzantineSafetyAttestation with:

• protocol id (aura.consensus)
• required capability keys for the profile
• snapshot of admitted/not-admitted runtime capabilities
• optional runtime evidence references

The attestation is attached to CommitFact and DkgTranscriptCommit. Capability mismatches fail before ceremony execution and emit redacted capability references for operational diagnostics.

5. Prestate Model

Consensus binds operations to explicit prestates. A prestate hash commits to the current reduced state of all participants.

#![allow(unused)]
fn main() {
let prestate_hash = H(C_auth1, C_auth2, C_context);
}

This value includes root commitments of participating authorities. It may also include the current relational context commitment. Witnesses verify that their local reduced state matches the prestate hash. This prevents forks.

The result identifier binds the operation to the prestate.

#![allow(unused)]
fn main() {
let rid = H(Op, prestate);
}

Witnesses treat matching (rid, prestate_hash) pairs as belonging to the same bucket. The protocol groups shares by these pairs to detect agreement.

6. Fast Path Protocol

The fast path optimistically assumes agreement. It completes in one round trip when all participants share the same prestate.

Messages

• Execute(cid, Op, prestate_hash, evidΔ) - initiator requests operation execution
• WitnessShare(cid, rid, share, prestate_hash, evidΔ) - witness returns threshold share
• Commit(cid, rid, sig, attesters, evidΔ) - initiator broadcasts commit fact
• StateMismatch(cid, expected_pre_hash, actual_pre_hash, evidΔ) - optional debugging signal

Each message carries evidence delta evidΔ for the consensus instance. Evidence propagates along with protocol messages.

Initiator Protocol

The initiator i coordinates the fast path.

State at initiator i:
    cid       : ConsensusId       // fresh per instance
    Op        : Operation
    shares    : Map[WitnessId -> (rid, share, prestate_hash)]
    decided   : Map[ConsensusId -> Bool]   // initially decided[cid] = false
    W         : Set[WitnessId]
    t         : Nat

The initiator maintains per-witness shares and tracks decision status.

Start Operation

Start(cid, Op):
    prestate       := ReadState()
    prestate_hash  := H(prestate)
    decided[cid]   := false
    shares         := {}

    For all w in W:
        Send Execute(cid, Op, prestate_hash, EvidenceDelta(cid)) to w

The initiator reads local state and broadcasts the operation to all witnesses.

Process Witness Shares

On WitnessShare(cid, rid, share, prestate_hash, evidΔ) from w:
    MergeEvidence(cid, evidΔ)

    If decided[cid] = false and w not in shares:
        shares[w] := (rid, share, prestate_hash)

        // collect all shares for this specific (rid, prestate_hash)
        Hset := { (w', s') in shares | s'.rid = rid
                                     ∧ s'.prestate_hash = prestate_hash }

        If |Hset| ≥ t:
            sig := CombineShares( { s'.share | (_, s') in Hset } )
            attesters := { w' | (w', _) in Hset }

            CommitFact(cid, rid, sig, attesters)
            For all v in W:
                Send Commit(cid, rid, sig, attesters, EvidenceDelta(cid)) to v

            decided[cid] := true

The initiator collects shares. When t shares agree on (rid, prestate_hash), it combines them into a threshold signature.

Witness Protocol

Each witness w responds to execute requests.

State at witness w:
    proposals : Map[(rid, prestate_hash) -> Set[(WitnessId, Share)]]
    decided   : Map[ConsensusId -> Bool]
    timers    : Map[ConsensusId -> TimerHandle]
    W         : Set[WitnessId]
    t         : Nat

Witnesses maintain proposals and fallback timers.

Process Execute Request

On Execute(cid, Op, prestate_hash, evidΔ) from i:
    MergeEvidence(cid, evidΔ)

    if decided.get(cid, false) = true:
        return

    prestate := ReadState()
    if H(prestate) != prestate_hash:
        Send StateMismatch(cid, prestate_hash, H(prestate), EvidenceDelta(cid)) to i
        StartTimer(cid, T_fallback)
        return

    rid   := H(Op, prestate)
    share := ProduceShare(cid, rid)

    proposals[(rid, prestate_hash)] := { (w, share) }

    Send WitnessShare(cid, rid, share, prestate_hash, EvidenceDelta(cid)) to i

    StartTimer(cid, T_fallback)

Witnesses verify prestate agreement before computing shares. Mismatches trigger fallback timers.

Process Commit

On Commit(cid, rid, sig, attesters, evidΔ) from any v:
    if decided.get(cid, false) = false
       and VerifyThresholdSig(rid, sig, attesters):

        MergeEvidence(cid, evidΔ)
        CommitFact(cid, rid, sig, attesters)
        decided[cid] := true
        StopTimer(cid)

Witnesses accept valid commit facts from any source.

7. Evidence Propagation

Evidence tracks equivocation and accountability information for consensus instances. The system uses CRDT-based incremental propagation. Evidence deltas attach to all protocol messages. Witnesses merge incoming evidence automatically.

Equivocation occurs when a witness signs conflicting result IDs for the same prestate. The protocol detects this pattern and generates cryptographic proofs. Each proof records both conflicting signatures with witness identity and timestamp.

#![allow(unused)]
fn main() {
pub struct EquivocationProof {
    pub witness: AuthorityId,
    pub consensus_id: ConsensusId,
    pub prestate_hash: Hash32,
    pub first_result_id: Hash32,
    pub second_result_id: Hash32,
    pub timestamp_ms: u64,
}
}

The proof structure preserves both conflicting votes. This enables accountability and slashing logic in higher layers.

Evidence deltas propagate via incremental synchronization. Each delta contains only new proofs since the last exchange. Timestamps provide watermark-based deduplication. The delta structure is lightweight and merges idempotently.

#![allow(unused)]
fn main() {
pub struct EvidenceDelta {
    pub consensus_id: ConsensusId,
    pub equivocation_proofs: Vec<EquivocationProof>,
    pub timestamp_ms: u64,
}
}

Every consensus message includes an evidence delta field. Coordinators attach deltas when broadcasting execute and commit messages. Witnesses attach deltas when sending shares. Receivers merge incoming deltas into local evidence trackers. This piggybacking ensures evidence propagates without extra round trips.

8. Fallback Protocol

Fallback activates when the fast path stalls. Triggers include witness disagreement or initiator failure. Fallback uses leaderless gossip to complete consensus.

Messages

• Conflict(cid, conflicts, evidΔ) - initiator seeds fallback with known conflicts
• AggregateShare(cid, proposals, evidΔ) - witnesses exchange proposal sets
• ThresholdComplete(cid, rid, sig, attesters, evidΔ) - any witness broadcasts completion

Equivocation Detection

Equivocation means signing two different rid values under the same (cid, prestate_hash).

HasEquivocated(proposals, witness, cid, pre_hash, new_rid):
    For each ((rid, ph), S) in proposals:
        if ph = pre_hash
           and rid ≠ new_rid
           and witness ∈ { w' | (w', _) in S }:
            return true
    return false

The protocol excludes equivocating shares from threshold computation.

Fallback Gossip

Witnesses periodically exchange proposals with random peers.

OnPeriodic(cid) for fallback gossip when decided[cid] = false:
    peers := SampleRandomSubset(W \ {w}, k)

    For each p in peers:
        Send AggregateShare(cid, proposals, EvidenceDelta(cid)) to p