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.

To accomplish this, Aura uses threshold cryptography so no single device holds complete keys. Network topology reflects social relationships, forming a web of trust that provides discovery, availability, and recovery. State converges through CRDT journals without central coordination. 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.

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.

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.

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.

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. It covers the core abstractions, data flow patterns, and component interactions that define the system. Formal definitions live in Theoretical Model, an overview of the implementation can be found in Project Structure.

Overview

Aura is a peer-to-peer identity and communication system built on three pillars. Threshold cryptography distributes trust across multiple devices. Session-typed protocols ensure safe multi-party coordination. CRDT journals provide conflict-free replicated state.

The system operates without dedicated servers. Discovery, availability, and recovery are provided by the web of trust. Peers relay messages for each other based on social relationships. No single party can observe all communication or deny service.

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

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. Dual Semilattice Model

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() {
// Facts grow by join (⊔)
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. The system evaluates Biscuit tokens against policy to derive the current capability frontier. Delegation can only attenuate. No operation can widen capability scope. See Theoretical Model for formal definitions of these lattices.

2. Authority and Identity Architecture

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

This diagram shows authority structure. Externally, observers see only the threshold public key. Internally, the commitment tree tracks device membership. Each device holds a key share. Threshold signing combines shares without exposing internal structure.

2.1 Account authorities

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.

#![allow(unused)]
fn main() {
pub struct AuthorityId(Uuid);
}

AuthorityId is an opaque identifier for the authority namespace. It does not encode membership or reveal device count. Key derivation utilities provide context-scoped keys without exposing internal structure. See Identifiers and Boundaries for identifier semantics.

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.

#![allow(unused)]
fn main() {
pub struct ContextId(Uuid);
}

ContextId identifies the shared namespace. 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.

3. Journal and State Reduction

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

3.1 Journal namespaces

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.

#![allow(unused)]
fn main() {
enum JournalNamespace {
    Authority(AuthorityId),
    Context(ContextId),
}
}

Namespace scoping provides isolation. Facts in one namespace cannot reference or affect facts in another namespace. Cross-namespace coordination requires explicit protocols.

3.2 Fact model

Facts are content-addressed immutable records. Each fact includes a type identifier, payload, attestation, and metadata. Facts are validated against type-specific rules before acceptance.

#![allow(unused)]
fn main() {
pub struct Fact {
    pub type_id: FactTypeId,
    pub payload: FactPayload,
    pub attestation: Attestation,
    pub metadata: FactMetadata,
}
}

Facts accumulate through CRDT merge. Duplicate facts are deduplicated by content hash. Conflicting facts are resolved by type-specific merge rules. The journal guarantees eventual consistency across replicas.

Attestations prove that an authority endorsed the fact. Threshold signatures require multiple devices to attest. Single-device signatures are used for local facts. The attestation type determines validation requirements.

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

#![allow(unused)]
fn main() {
trait FactReducer {
    type State;
    fn reduce(facts: &FactSet) -> Self::State;
}
}

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 complete reduction architecture.

3.4 Flow budget facts

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.

#![allow(unused)]
fn main() {
pub struct FlowBudget {
    limit: u64,   // derived from capabilities
    spent: u64,   // stored as facts
    epoch: Epoch, // stored as facts
}
}

Budget charges are facts that increment spent. Epoch rotation resets counters through new epoch facts. This design keeps replicated state minimal while enabling runtime limit computation.

4. Effect System Architecture

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

This diagram shows effect layering. Infrastructure effects wrap OS primitives. Application effects encode domain logic. Composite effects combine lower layers for convenience.

4.1 Effect trait classification

Infrastructure effects are implemented in aura-effects. These include CryptoEffects, NetworkEffects, StorageEffects, PhysicalTimeEffects, RandomEffects, and TraceEffects.

Application effects encode domain logic in domain crates. These include JournalEffects, AuthorizationEffects, FlowBudgetEffects, and LeakageEffects. Application effects compose infrastructure effects.

Composite effects are extension traits that combine multiple lower-level effects. These include TreeEffects for commitment tree operations and choreography extension traits for protocol execution.

4.2 Unified time system

The time system provides four domains for different use cases. PhysicalClock uses wall-clock time with optional uncertainty bounds. LogicalClock uses vector and Lamport clocks for causal ordering.

OrderClock uses opaque 32-byte tokens for deterministic ordering without temporal leakage. Range uses earliest and latest bounds for validity windows.

#![allow(unused)]
fn main() {
enum TimeStamp {
    PhysicalClock(PhysicalTime),
    LogicalClock(LogicalTime),
    OrderClock(OrderTime),
    Range(RangeTime),
}
}

Time access happens through PhysicalTimeEffects, LogicalClockEffects, and OrderClockEffects. Application code does not call system time directly. See Effect System for handler implementation patterns.

4.3 Context propagation

EffectContext is the operation scope that flows through async call chains. It carries authority id, context id, session id, execution mode, and metadata.

#![allow(unused)]
fn main() {
pub struct EffectContext {
    pub authority: AuthorityId,
    pub context: Option<ContextId>,
    pub session: SessionId,
    pub mode: ExecutionMode,
    pub metadata: ContextMetadata,
}
}

Context propagation ensures that all operations within a call chain share the same scope. Guards access context to make authorization decisions. Handlers access context to route operations to the correct namespace.

4.4 Impure function control

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.

#![allow(unused)]
fn main() {
async fn operation<E: PhysicalTimeEffects + RandomEffects>(
    effects: &E
) -> Result<Nonce> {
    let now = effects.current_time().await;
    let bytes = effects.random_bytes(32).await?;
    Ok(Nonce { now, bytes })
}
}

The type signature makes dependencies explicit. Tests can inject mock handlers with controlled behavior. Simulations can replay exact sequences for debugging.

5. Guard Chain and Authorization

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.

5.1 Guard responsibilities

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.

FlowBudgetGuard charges flow budgets and emits receipts. It verifies that the sender has sufficient budget for the message cost. Budget charges are atomic with receipt generation.

JournalCouplingGuard commits facts alongside budget changes. It ensures that budget charges and other facts are durably recorded before the message leaves. This coupling provides atomicity.

LeakageTrackingGuard records privacy budget usage. It tracks information flow to different observer classes. Operations that exceed leakage budgets are blocked.

5.2 Receipts and accountability

Flow budget charges emit receipts. Receipts include context, sender, receiver, epoch, cost, and a hash chain link. Relays can verify that prior hops paid their budget cost.

#![allow(unused)]
fn main() {
pub struct Receipt {
    pub ctx: ContextId,
    pub src: AuthorityId,
    pub dst: AuthorityId,
    pub epoch: Epoch,
    pub cost: FlowCost,
    pub nonce: FlowNonce,
    pub prev: Hash32,
    pub sig: ReceiptSig,
}
}

The prev field links receipts in a per-hop chain. This chain provides accountability for multi-hop message forwarding. See Transport and Information Flow for receipt verification and Authorization for Biscuit integration.

6. Choreographic Protocols

Choreographies define global protocols using multi-party session types. The choreography! macro generates local session types and effect bridge helpers. Guard requirements are expressed through annotations.

6.1 Global protocol specification

A global type describes the entire protocol from a bird's-eye view. Each message specifies sender, receiver, payload type, and guard annotations.

#![allow(unused)]
fn main() {
choreography! {
    #[namespace = "key_rotation"]
    protocol KeyRotation {
        roles: Initiator, Witness1, Witness2;
        Initiator[guard_capability = "rotate", flow_cost = 10]
            -> Witness1, Witness2: Proposal(data: RotationData);
        Witness1[flow_cost = 5] -> Initiator: Vote(vote: bool);
        Witness2[flow_cost = 5] -> Initiator: Vote(vote: bool);
    }
}
}

The namespace attribute scopes the protocol. Annotations compile into guard requirements. The macro validates that the protocol is well-formed before generating code.

6.2 Projection and execution

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.

Production execution uses AuraChoreoEngine with the Telltale VM and the host bridge in Layer 6. Startup is manifest-driven and admitted by construction. Generated runner surfaces still exist for testing and migration support, but they are not the production execution model. See MPST and Choreography for projection rules and runtime details.

6.3 Annotation effects

Annotations drive guard chain behavior. guard_capability specifies required Biscuit capabilities. flow_cost specifies budget charges. journal_facts specifies facts to commit. leak specifies leakage budget allocation.

The guard chain interprets these annotations before each send. Annotation values are validated at compile time where possible. Runtime checks handle dynamic values.

7. Consensus and Agreement

Aura Consensus provides single-shot agreement for non-monotone operations. It produces CommitFact entries that are inserted into journals. The protocol is scoped to individual operations.

7.1 When consensus is needed

Monotone operations use CRDT merge without consensus. Facts accumulate through join. Capabilities restrict through meet. These operations converge without coordination.

Non-monotone operations require consensus. Examples include key rotation, membership changes, and authoritative state transitions. These operations cannot be safely executed with CRDT merge alone.

7.2 Operation categories

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

#![allow(unused)]
fn main() {
enum OperationCategory {
    A, // CRDT, immediate
    B, // Pending until agreement
    C, // Blocking consensus
}
}

The category determines user experience and system behavior. See Operation Categories for classification rules and ceremony contracts.

7.3 Fast path and fallback

The fast path completes in one round trip when witnesses agree on prestate. Witnesses validate the operation, sign their shares, and return them to the initiator. The initiator aggregates shares into a threshold signature.

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.

7.4 CommitFact and journal integration

CommitFact represents a consensus decision. It includes prestate hash, operation hash, participant set, threshold signature, and timestamp.

#![allow(unused)]
fn main() {
pub struct CommitFact {
    pub consensus_id: ConsensusId,
    pub prestate: Hash32,
    pub operation: Hash32,
    pub participants: ParticipantSet,
    pub signature: ThresholdSignature,
    pub timestamp: ProvenancedTime,
}
}

CommitFacts are inserted into the relevant journal namespace. Reducers process CommitFacts to update derived state. The signature proves that a threshold of participants agreed.

The consensus_id binds the decision to a specific prestate and operation. This binding prevents reusing signatures across unrelated operations. Prestate binding ensures that consensus decisions apply to the expected state. See Consensus for protocol details.

8. Transport and Networking

Transport abstractions provide secure channels between authorities. The system does not assume persistent connections. Messages may be relayed through multiple hops.

8.1 SecureChannel abstraction

SecureChannel provides encrypted, authenticated communication between two authorities. Channels use context-scoped keys derived through DKD. Channel state is not stored in journals.

#![allow(unused)]
fn main() {
trait SecureChannel {
    async fn send(&self, msg: &[u8]) -> Result<()>;
    async fn recv(&self) -> Result<Vec<u8>>;
    fn peer(&self) -> AuthorityId;
}
}

Channels are established through rendezvous or direct connection. The abstraction hides transport details from application code. See Rendezvous Architecture for channel establishment.

8.2 Rendezvous and peer discovery

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. Home and neighborhood membership influences relay selection. Authorities prefer relays operated by trusted peers. Fallback uses public rendezvous servers when social relays are unavailable.

Envelope encryption ensures that rendezvous servers learn nothing about message content or recipients. The sender encrypts to the recipient's public key. The server sees only opaque blobs with timing metadata. See Social Architecture for topology details.

8.3 Asynchronous message patterns

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. The pattern choice depends on operation requirements. See Asynchronous Message Patterns for implementation details.

9. Crate Architecture

Aura uses eight layers with strict dependency ordering. Dependencies flow downward. No crate imports from a higher layer.

flowchart TB
    L1[Layer 1: Foundation<br/>aura-core]
    L2[Layer 2: Specification<br/>aura-journal, aura-authorization, aura-mpst]
    L3[Layer 3: Implementation<br/>aura-effects, aura-composition]
    L4[Layer 4: Orchestration<br/>aura-protocol, aura-guards, aura-consensus]
    L5[Layer 5: Feature<br/>aura-chat, aura-recovery, aura-social]
    L6[Layer 6: Runtime<br/>aura-agent, aura-app, aura-simulator]
    L7[Layer 7: Interface<br/>aura-terminal]
    L8[Layer 8: Testing<br/>aura-testkit, aura-harness]

    L1 --> L2 --> L3 --> L4 --> L5 --> L6 --> L7
    L8 -.-> L1 & L2 & L3 & L4 & L5 & L6

This diagram shows dependency flow. Testing crates can depend on any layer for test support.

9.1 Layer descriptions

Layer 1, Foundation — aura-core with effect traits, identifiers, and cryptographic utilities.

Layer 2, Specification — domain crates defining semantics without runtime. No OS access, no Tokio. Facts use DAG-CBOR.

Layer 3, Implementation — aura-effects for production handlers, aura-composition for handler assembly.

Layer 4, Orchestration — multi-party coordination via aura-protocol, aura-guards, aura-consensus, aura-amp, aura-anti-entropy.

Layer 5, Feature — end-to-end protocols. Each crate declares OPERATION_CATEGORIES. Runtime caches live in Layer 6.

Layer 6, Runtime — aura-agent for assembly, aura-app for portable logic, aura-simulator for deterministic simulation.

Layer 7, Interface — aura-terminal for CLI and TUI entry points.

Layer 8, Testing — aura-testkit, aura-quint, and aura-harness for test infrastructure.

9.2 Code location guidance

The layer determines where code belongs. Stateless single-party operations go in Layer 3. Multi-party coordination goes in Layer 4. Complete protocols go in Layer 5. Runtime assembly goes in Layer 6.

Effect traits are defined only in aura-core. Infrastructure handlers live in aura-effects. Mock handlers live in aura-testkit. This separation keeps the dependency graph clean.

For practical guidance on effects and handlers, see Effects Guide. For choreography development, see Choreography Guide. For complete crate breakdown and dependency graph, see Project Structure.

10. Security Model

Aura's security model eliminates single points of trust. No central server holds keys or can read messages. Trust is distributed across devices and social relationships.

10.1 Threshold cryptography

Account authorities use threshold signatures. Key operations require a threshold of devices to participate. Compromising fewer than the threshold reveals nothing about the key.

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 Cryptographic Architecture for implementation details.

The threshold is configurable per authority. A 2-of-3 threshold balances security and availability for typical users. Higher thresholds provide stronger security at the cost of requiring more devices to be online.

10.2 Capability-based authorization

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

The guard chain enforces capabilities at runtime. Biscuit Datalog queries check predicates against facts. See Authorization for token structure and evaluation.

10.3 Context isolation

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

Leakage tracking monitors information flow to observer classes. Operations that exceed privacy budgets are blocked. See Privacy and Information Flow for the leakage model.

11. Reactive State Management

The system uses reactive signals for state propagation. Journal changes trigger signal updates. UI components subscribe to signals. This pattern decouples state producers from consumers.

11.1 Signal architecture

ReactiveEffects defines the signal interface. ReactiveHandler implements batched processing with configurable windows. Signals carry typed state that observers can query.

#![allow(unused)]
fn main() {
trait ReactiveEffects {
    async fn emit<T: Signal>(&self, signal: T);
    async fn subscribe<T: Signal>(&self) -> Receiver<T>;
}
}

Signal emission is non-blocking. Handlers batch rapid updates to reduce overhead. Subscribers receive the latest state when they poll.

11.2 Journal to UI flow

Journal fact changes flow through reducers to signals. Reducers compute derived state from facts. Signals expose that state to UI observers. The flow is unidirectional and predictable.

The aura-app crate defines application signals. The aura-terminal crate consumes these signals for rendering. This separation keeps UI concerns out of core logic.

12. Error Handling

Errors are unified through the AuraError type in aura-core. Domain crates define specific error variants. Effects propagate errors through Result types.

11.1 Error classification

Errors are classified by recoverability. Transient errors may succeed on retry. Permanent errors indicate invalid operations. System errors indicate infrastructure failures.

#![allow(unused)]
fn main() {
pub enum ErrorKind {
    Transient,  // Retry may succeed
    Permanent,  // Invalid operation
    System,     // Infrastructure failure
}
}

Error classification guides retry behavior and user feedback. Transient errors trigger automatic retry with backoff. Permanent errors are reported to the user. System errors may require recovery procedures.

11.2 Error propagation

Effects propagate errors through Result types. Handlers convert low-level errors to domain errors. The error chain preserves context for debugging. Logging captures error details without exposing sensitive data.

#![allow(unused)]
fn main() {
async fn operation<E: JournalEffects>(effects: &E) -> Result<(), AuraError> {
    effects.merge_facts(facts)
        .await
        .map_err(|e| AuraError::journal(e, "merge failed"))?;
    Ok(())
}
}

Error context includes the operation name and relevant identifiers. Stack traces are available in debug builds. Production builds log structured error data for monitoring.

11.3 Consensus and recovery

Consensus failures have specific handling. Fast path failures fall back to gossip. Network partitions delay but do not corrupt state. Recovery procedures restore operation after failures.

The journal provides durability. Uncommitted facts are replayed after restart. Committed facts are immutable. This design simplifies recovery logic.

Device recovery uses guardian protocols. Guardians hold encrypted recovery shares. A threshold of guardians can restore account access. See Relational Contexts for recovery patterns.

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

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 information flows across privacy boundaries:

• Flow budgets: Per-context per-peer spending limits enforced by FlowGuard
• 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

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 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.
• Optional privacy enhancements such as Tor and cover traffic are correctly configured when enabled.

1.3 Non-goals

• This contract does not guarantee traffic-analysis resistance against global passive adversaries without optional privacy overlays.
• This contract does not define social policy decisions such as who should trust whom.

2. Privacy Philosophy

Traditional privacy systems force users to choose between complete isolation and complete exposure. Aura recognizes that privacy is relational. Sharing information with trusted parties is not a privacy violation, it's the foundation of meaningful collaboration.

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

2.2 Privacy Layers

Verified by: Aura.Proofs.KeyDerivation, authorization.qnt

3. Flow Budget System

3.1 Budget Structure

For each context and peer pair, the journal records charge facts that contribute to a flow budget:

FlowBudget {
    limit: u64,   // derived at runtime from Biscuit + policy
    spent: u64,   // replicated fact (merge = max)
    epoch: Epoch, // replicated fact
}

Only spent and epoch appear as journal facts. The limit is computed at runtime by intersecting Biscuit-derived capabilities with sovereign policy.

3.2 Limit Computation

The limit for a context and peer is computed as:

limit(ctx, peer) = base(ctx) ⊓ policy(ctx) ⊓ role(ctx, peer)
                   ⊓ relay_factor(ctx) ⊓ peer_health(peer)

Each term is a lattice element. Merges occur via meet (⊓), ensuring convergence and preventing widening.

3.3 Charge-Before-Send

Every transport observable is preceded by guard evaluation:

1. CapGuard: Verify Biscuit authorization
2. FlowGuard: Charge cost to (context, peer) budget
3. JournalCoupler: Atomically commit charge fact and protocol deltas
4. Transport: Emit packet only after successful charge

If spent + cost > limit, the send is blocked locally with no observable behavior.

Invariants:

• spent ≤ limit at all times (InvariantFlowBudgetNonNegative)
• Charging never increases available budget (monotonic_decrease)
• Guard chain order is fixed (guardChainOrder)
• Attenuation only narrows, never widens (attenuationOnlyNarrows)

Verified by: Aura.Proofs.FlowBudget, authorization.qnt, transport.qnt

3.4 Multi-Hop Enforcement

For forwarding, each hop independently executes the guard chain:

• Relay validates upstream receipt before forwarding
• Relay charges its own budget before emitting
• Receipt facts are scoped to (context, epoch) with chained hashes
• Downstream peers can audit budget usage via receipt chain

Because spent is monotone (merge = max), convergence holds even if later hops fail.

Verified by: transport.qnt (InvariantSentMessagesHaveFacts)

3.5 Receipts and Epochs

Per-hop receipts are required for forwarding and bound to the epoch:

Receipt { ctx, src, dst, epoch, cost, nonce, prev_hash, sig }

This schema is the canonical receipt shape used across core contracts.

• Acceptance window: Current epoch only
• Rotation trigger: Journal fact Epoch(ctx) increments
• On rotation: spent(ctx, *) resets, and old receipts become invalid

Invariants:

• Receipts only valid within their epoch (InvariantReceiptValidityWindow)
• Old epoch receipts cannot be replayed (InvariantCrossEpochReplayPrevention)

Verified by: epochs.qnt

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:

LeakageBudget {
    observer: DeviceId,
    leakage_type: LeakageType,  // Metadata, Timing, Participation
    limit: u64,
    spent: u64,
    refresh_interval: Duration,
}

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

4.3 Policy Modes

Verified by: Aura.Proofs.ContextIsolation

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
• Enforcement: DKD ensures unique identity per context

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
• Enforcement: Flow budgets, onion routing, cover traffic

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
• Enforcement: Group-specific DKD identity, k-anonymity for sensitive operations

5.4 External Boundary

External observers have no relationship with you:

• With Tor: Only encrypted Tor traffic visible
• Without Tor: ISP sees connections to Aura nodes only
• Enforcement: Fixed-size envelopes, no central directory, flow budgets

6. Time Domain Semantics

Time handling affects privacy through leakage:

• Cross-domain comparisons require explicit TimeStamp::compare(policy)
• Physical time obtained only through PhysicalTimeEffects (never direct SystemTime::now())
• Privacy mode (ignorePhysical = true) hides physical timestamps

Verified by: Aura.Proofs.TimeSystem

7. Adversarial Model

7.1 Direct Relationship

A party in a direct relationship sees everything within that context by consent.

• Cannot: Link identity across contexts, access undisclosed contexts
• Attack vector: Social engineering, context correlation
• Mitigation: UI clearly indicates active context

7.2 Group Insider

A group member sees all group activity by consent.

• Cannot: Determine member identities outside group, access other groups
• Attack vector: Threshold signing timing correlation
• Mitigation: k-anonymity, random delays in signing rounds

7.3 Gossip Neighbor

Devices forwarding your traffic observe encrypted metadata.

• Cannot: Decrypt content, identify ultimate sender/receiver, link rtags to identities
• Attack vector: Traffic correlation through sustained observation
• Mitigation: Onion routing, cover traffic, batching, rtag rotation

7.4 Network Observer

An ISP-level adversary sees IP connections and packet timing.

• With Tor: Only Tor usage visible
• Without Tor: Connections to known Aura nodes visible
• Attack vector: Confirmation attacks, traffic correlation
• Mitigation: Tor integration, fixed-size envelopes, cover traffic

7.5 Compromised Device

A single compromised device reveals its key share and synced journal state.

• Cannot: Perform threshold operations alone, derive account root key
• Attack vector: Compromise M-of-N devices for full control
• Mitigation: Threshold cryptography, device revocation via resharing, epoch invalidation

8. Privacy Metrics

Tests instantiate adversary observers and measure inference confidence against these bounds.

9. Cover Traffic

Cover traffic is an optional enhancement layered on mandatory flow-budget enforcement:

• Adaptive: Matches real usage patterns (e.g., 20 messages/hour during work hours)
• Group-leveraged: Groups naturally provide steady traffic rates
• Scheduled slots: Real messages inserted into fixed intervals
• Indistinguishable: Only recipient can distinguish real from cover by decryption attempt

Target: P(real | observed) ≈ 0.5

10. Hub Node Mitigation

Hub nodes with high connectivity observe metadata for many relationships:

11. Implementation Requirements

11.1 Key Derivation

• Use HKDF with domain separation
• Path: (account_root, app_id, context_label, "aura.key.derive.v1")
• Never reuse keys across contexts

Verified by: Aura.Proofs.KeyDerivation

11.2 Envelope Format

• Fixed-size with random padding
• Encrypted and authenticated
• Onion-routed through multiple hops
• Rtags rotate on negotiated schedule

11.3 Guard Chain

• All transport calls pass through FlowGuard
• Charge failure branches locally with no packet emitted
• Multi-hop forwarding attaches and validates per-hop receipts

Verified by: authorization.qnt (chargeBeforeSend, spentWithinLimit)

11.4 Secure Storage

• Use platform secure storage (Keychain, Secret Service, Keystore)
• Never store keys in plaintext files
• Audit logs for security-critical operations in journal

11.5 Error-Channel Privacy Requirements

• 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 whether failure came from capability checks, budget checks, or local storage faults beyond allowed protocol-level status codes.

12. Verification Coverage

This contract's guarantees are formally verified: Canonical invariant names are indexed in Project Structure. Canonical proof and coverage status are indexed in Verification Coverage Report.

See Verification Coverage Report for metrics and Aura Formal Verification for the Quint-Lean correspondence map.

13. References

Distributed Systems Contract covers safety, liveness, and consistency.

Theoretical Model covers the formal calculus and semilattice laws.

Aura System Architecture describes runtime layering and the guard chain.

Authorization covers CapGuard, FlowGuard, 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.

14. Implementation References

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, latency expectations, 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 Aura 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 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.3 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.

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

Verified by: Aura.Proofs.Journal, journal/core.qnt

2.2 Charge-Before-Send

Every transport observable is preceded by CapGuard, FlowGuard, and JournalCoupler. See Runtime and Authorization. No packet is emitted without a successful charge. Guard evaluation is pure over a prepared snapshot and yields commands that an interpreter executes, so the chain never blocks on embedded I/O.

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

Verified by: Aura.Proofs.FlowBudget, authorization.qnt, transport.qnt

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

Verified by: Aura.Proofs.Consensus.Agreement, consensus/core.qnt

2.3.1 Runtime Byzantine Admission

Before consensus-backed ceremonies execute, Aura validates runtime theorem-pack capability profiles and rejects missing requirements at admission time. This prevents silent downgrade of BFT assumptions.

Capability keys are mapped to threat-model assumptions as follows:

• byzantine_envelope: Byzantine threshold/fault model assumptions (f < n/3), authenticated participants, evidence validity, conflict exclusion.
• termination_bounded: bounded progress/termination assumptions for long-running protocol lanes.
• mixed_determinism: declared native/wasm determinism envelope and conformance constraints.
• reconfiguration: coherent delegation/link assumptions for live topology changes.

Successful admissions are recorded as ByzantineSafetyAttestation payloads attached to consensus outputs (CommitFact, DKG transcript commits). Admission mismatches fail closed and surface redacted capability references for debugging.

2.3.2 Quantitative Termination Bounds

Category C choreography executions are bounded by deterministic step budgets derived from Telltale weighted measures:

• W = 2 * sum(depth(local_type)) + sum(buffer_sizes)
• max_steps = ceil(k_sigma * W * budget_multiplier)

Aura enforces this budget per execution and fails with BoundExceeded when the bound is crossed. This removes wall-clock coupling from safety/liveness enforcement and keeps bound checks replay-deterministic across native and wasm conformance lanes.

2.3.3 Threshold Parameterization

Consensus parameterization uses n participants, threshold t, and Byzantine budget f. Threshold signatures require t distinct valid shares. Safety requires f < t. Byzantine quorum-style assumptions additionally require f < n/3. Profiles must declare which bound is active for a given ceremony.

2.3.4 Runtime Parity Guarantees and Limits

Aura uses telltale parity lanes to compare runtime artifacts under declared conformance envelopes. These checks provide implementation conformance signals. They do not replace domain theorem claims from Quint and Lean.

Guarantees:

• parity lanes use canonical surfaces (observable, scheduler_step, effect)
• mismatch reports include first mismatch location for deterministic triage
• strict and envelope-bounded classifications are explicit in report artifacts

Limits:

• parity checks validate observed runtime behavior, not full state-space reachability
• parity checks depend on scenario and seed coverage
• parity success does not imply new consensus or CRDT theorem coverage

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

Verified by: Aura.Proofs.Consensus.Evidence, consensus/core.qnt

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.

Verified by: Aura.Proofs.Consensus.Equivocation, consensus/adversary.qnt

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

Verified by: Aura.Proofs.Consensus.Frost, consensus/frost.qnt

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.

Verified by: transport.qnt (InvariantContextIsolation)

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)

Verified by: transport.qnt

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.

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

Verified by: keys/dkg.qnt, keys/resharing.qnt

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

Verified by: invitation.qnt

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

Verified by: epochs.qnt

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

Verified by: interaction.qnt

4. Liveness Guarantees

4.1 Fast-Path Consensus

Fast-path consensus completes in 2×Δ_net (two message delays) when all witnesses are online. Responses are gathered synchronously before committing.

4.2 Fallback Consensus

Fallback consensus eventually completes under partial synchrony with bounded message delays. The fallback timeout is T_fallback = 2×Δ_net in formal verification (implementations may use up to 3×Δ_net for margin). Gossip ensures progress if a majority of witnesses re-transmit proposals. See Consensus for timeout configuration.

Verified by: Aura.Proofs.Consensus.Liveness, consensus/liveness.qnt

4.3 Anti-Entropy

Journals converge under eventual delivery. Periodic syncs or reorder-resistant CRDT merges reconcile fact sets even after partitions. Vector clocks accurately track causal dependencies (InvariantVectorClockConsistent). Authorities exchange their complete fact journals with neighbors to ensure diverged state is healed.

Verified by: journal/anti_entropy.qnt

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 derived limit(ctx, peer) > 0 in a future epoch and epoch updates converge, FlowGuard 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.

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

Verified by: Aura.Proofs.TimeSystem

6. Synchrony and Timing Model

Aura assumes partial synchrony. There exists a bound Δ_net on message delay and processing time once the network stabilizes (Global Stabilization Time, GST). This bound is possibly unknown before stabilization occurs.

Before stabilization, timeouts may be conservative. Handlers must tolerate jitter but assume eventual delivery of periodic messages.

Epoch rotation relies on loosely synchronized clocks. The journal serves as the source of truth. Authorities treat an epoch change as effective once they observe it in the journal. This design avoids hard synchronization requirements.

7. Latency Expectations

8. Adversarial Model

8.1 Network Adversary

A network adversary controls a subset of transport links. It can delay or drop packets but cannot break cryptography. It cannot forge receipts without FlowGuard grants. Receipts are protected by signatures and epoch binding.

The network adversary may compromise up to f authorities per consensus instance within the active threshold profile. Safety requires the bounds declared in §2.3.3 (f < t, and f < n/3 when that profile is selected).

8.2 Byzantine Witness

A Byzantine witness may equivocate during consensus. The system detects equivocation via the evidence CRDT (see §2.5). Equivocators are excluded from threshold calculations.

A Byzantine witness cannot cause multiple commits. Threshold signature verification rejects tampered results. The t of t-of-n threshold signatures prevents this attack. Honest majority can always commit (InvariantHonestMajorityCanCommit).

Verified by: Aura.Proofs.Consensus.Adversary, consensus/adversary.qnt

8.3 Malicious Relay

A malicious relay may drop or delay envelopes. It cannot forge flow receipts because receipts require cryptographic signatures. It cannot read payloads because of context-specific encryption.

Downstream peers detect misbehavior via missing receipts or inconsistent budget charges. The transport layer detects relay failures automatically.

8.4 Device Compromise

A compromised device reveals its share and journal copy. It cannot reconstitute the account without meeting the branch policy. Recovery relies on relational contexts as described in Relational Contexts.

Device compromise is recoverable because the threshold prevents a single device from acting unilaterally. Guardians can revoke the compromised device and issue a new one. Compromised nonces are excluded from future consensus (InvariantCompromisedNoncesExcluded).

9. Consistency Model

Journals eventually converge after replicas exchange all facts. This is eventual consistency. Authorities that have seen the same fact set arrive at identical states.

Operations guarded by Aura Consensus achieve operation-scoped agreement. Once a commit fact is accepted, all honest replicas agree on that operation result. See Consensus. This does not define a single global linearizable log for all operations.

Causal delivery is not enforced at the transport layer. Choreographies enforce ordering via session types instead. See Multi-party Session Types and Choreography.

Each authority's view of its own journal is monotone. Once it observes a fact locally, it will never un-see it. This is monotonic read-after-write consistency.

10. Failure Handling

Timeouts trigger fallback consensus. See Consensus for T_fallback guidelines. Fallback consensus allows the system to make progress during temporary network instability.

Partition recovery relies on anti-entropy. Authorities merge fact sets when connectivity returns. The journal is the single source of truth for state.

Budget exhaustion causes local blocking. Protocols must implement backoff or wait for epoch rotation. Budgets are described in Privacy and Information Flow Contract.

Guard-chain failures return local errors. These errors include AuthorizationDenied, InsufficientBudget, and JournalCommitFailed. Protocol authors must handle these errors without leaking information. Proper error handling is critical for security.

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

11. Deployment Guidance

Configure witness sets using the parameter bounds declared in §2.3.3 for the active ceremony profile.

Tune gossip fanout and timeout parameters based on observed round-trip times and network topology. Conservative parameters ensure liveness under poor conditions.

Monitor receipt acceptance rates, consensus backlog, and budget utilization. See Distributed Maintenance Architecture for monitoring guidance. Early detection of synchrony violations prevents cascading failures.

12. Verification Coverage

This contract's guarantees are formally verified: Canonical invariant names are indexed in Project Structure. Canonical proof and coverage status are indexed in Verification Coverage Report.

See Verification Coverage Report for metrics and Aura Formal Verification for the Quint-Lean correspondence map.

13. References

Aura System Architecture describes runtime layering.

Authorization describes guard chain 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 CapGuard and FlowGuard 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 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 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 hkdf_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
• hkdf

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. Code Organization Patterns

3.1 Correct Usage

Application code should use effect traits.

#![allow(unused)]
fn main() {
async fn authenticate<E: CryptoCoreEffects>(effects: &E, private_key: &[u8], data: &[u8]) -> Result<Vec<u8>, CryptoError> {
    effects.ed25519_sign(data, private_key).await
}
}

This pattern ensures all cryptographic operations flow through the effect system. The generic constraint allows both production and mock implementations.

Application code should use aura-core wrappers for type safety.

#![allow(unused)]
fn main() {
use aura_core::crypto::ed25519::{Ed25519SigningKey, Ed25519VerifyingKey, Ed25519Signature};

fn verify_authority(key: &Ed25519VerifyingKey, data: &[u8], sig: &Ed25519Signature) -> Result<(), AuraError> {
    key.verify(data, sig)
}
}

The wrapper types provide a stable API and enable algorithm migration without changing application code.

3.2 Incorrect Usage

Do not import crypto libraries directly in application code.

#![allow(unused)]
fn main() {
// INCORRECT: Direct crypto library import
use ed25519_dalek::{SigningKey, VerifyingKey};  // BAD

// INCORRECT: Direct randomness
use rand_core::OsRng;  // BAD (outside Layer 3)
let mut rng = OsRng;
}

Direct imports bypass the effect system and break testability. They also scatter cryptographic usage throughout the codebase.

3.3 Randomness Patterns

All randomness should flow through RandomCoreEffects.

#![allow(unused)]
fn main() {
async fn generate_nonce<E: RandomCoreEffects>(effects: &E) -> [u8; 12] {
    let bytes = effects.random_bytes(12).await;
    bytes.try_into().expect("12 bytes")
}
}

For encryption in feature crates, use parameter injection.

#![allow(unused)]
fn main() {
pub struct EncryptionRandomness {
    nonce: [u8; 12],
    padding: Vec<u8>,
}

pub fn encrypt_with_randomness(data: &[u8], key: &[u8], randomness: EncryptionRandomness) -> Vec<u8> {
    // Deterministic given the randomness parameter
}
}

This pattern enables deterministic testing by externalizing randomness.

4. Allowed Locations

The following locations may directly use cryptographic libraries.

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, however single signature does not require nonce coordination or aggregation.

6.3 API Usage

The unified API handles mode selection automatically.

#![allow(unused)]
fn main() {
// Generate keys - mode is determined by threshold
let keys = crypto.generate_signing_keys(threshold, max_signers).await?;
// keys.mode == SingleSigner if (1, 1), Threshold otherwise

// Sign with the key package (single-signer only)
let signature = crypto.sign_with_key(message, &key_package, keys.mode).await?;

// Verify the signature
let valid = crypto.verify_signature(message, &signature, &keys.public_key_package, keys.mode).await?;
}

For threshold mode where m >= 2, the sign_with_key() method returns an error. Threshold signing requires the full FROST protocol flow with nonce coordination across signers.

6.4 Storage Separation

Single-signer and threshold keys use different storage paths.

signing_keys/<authority>/<epoch>/1       # SingleSignerKeyPackage (Ed25519)
frost_keys/<authority>/<epoch>/<index>   # FROST KeyPackage

The storage location is managed by SecureStorageEffects. The authority is the AuthorityId in display format. The epoch is the current key epoch. The index is the signer index for FROST keys.

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. If the upstream FROST or postcard encoding changes, update the constants and add/adjust tests to lock in the new canonical sizes.

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

The recommended pattern uses AppCore for high-level operations.

#![allow(unused)]
fn main() {
// Sign a tree operation
let attested_op = app_core.sign_tree_op(&tree_op).await?;

// Bootstrap 1-of-1 keys for single-device accounts (uses Ed25519)
let public_key = app_core.bootstrap_signing_keys().await?;
}

For direct trait usage, import and call the service.

#![allow(unused)]
fn main() {
use aura_core::effects::ThresholdSigningEffects;

let context = SigningContext::self_tree_op(authority, tree_op);
let signature = signing_service.sign(context).await?;
}

7.5 Design Rationale

The unified trait abstraction enables a consistent interface across multi-device, guardian, and group scenarios. It provides proper audit context via ApprovalContext for UX and logging. It enables testability via mock implementations in aura-testkit. It provides key isolation with secure storage integration.

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

8.1 Algorithm Migration

The wrapper pattern enables algorithm migration.

1. Update wrappers in aura-core/src/crypto/
2. Update handler in aura-effects/src/crypto.rs
3. Application code remains unchanged

8.2 HSM Integration

Hardware Security Module support would require a new HsmCryptoHandler implementing CryptoCoreEffects. Runtime selection between RealCryptoHandler and HsmCryptoHandler would be needed. Application code would require no changes.

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

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

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

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

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.

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.

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

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 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 the cached frontier and any inline Biscuit token already present in 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 provide cryptographically verifiable, attenuated delegation chains. The typical workflow creates root authority via TokenAuthority::new(authority_id). Issue tokens via authority.create_token(recipient_authority_id). Attenuate for delegation via BiscuitTokenManager::attenuate_read(). Authorize via BiscuitAuthorizationBridge::authorize(&token, operation, &resource_scope).

flowchart TB
    A[Root Authority Token] -->|append caveats| B[Device Token<br/>read + write]
    B -->|check operation = read| C[Read-Only Token]
    C -->|check resource starts_with public/| D[Public Read-Only Token]

This diagram shows token attenuation. Each block appends restrictions to the chain. Attenuation preserves the cryptographic signature chain while reducing authority.

Biscuit tokens are secure through cryptographic signature chains that prevent forgery. They support offline verification without contacting the issuer. Epoch rotation provides revocation by invalidating old tokens.

Guard Chain Integration

Biscuit authorization integrates with the guard chain in three phases. Cryptographic verification calls bridge.authorize(token, operation, resource_scope) to perform Datalog evaluation. Guard evaluation prepares a GuardSnapshot asynchronously and then calls guards.evaluate(&snapshot, &request) synchronously. Effect execution interprets the EffectCommand items from the guard outcome.

If any phase fails, the operation returns an error without observable side effects.

Authorization Scenarios

Biscuit tokens handle all authorization scenarios through cryptographic verification. Local device operations use device tokens with full capabilities. Cross-authority delegation uses attenuated tokens with resource restrictions. Policy enforcement integrates sovereign policy into Datalog evaluation.

API access control uses scoped tokens with operation restrictions. Guardian recovery uses guardian tokens with recovery capabilities. Storage operations use storage-scoped tokens with path restrictions. Relaying and forwarding use context tokens with relay permissions.

Performance and Caching

Biscuit token authorization has predictable performance characteristics. Signature verification requires O(chain length) cryptographic operations. Authorization evaluation takes O(facts × rules) time for Datalog evaluation. Attenuation costs O(1) to append blocks.

Token results are cacheable with epoch-based invalidation. Cache authorization results per authority, token hash, and resource scope. Invalidate cache on epoch rotation or policy update.

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 and BiscuitTokenManager in aura-authorization/src/biscuit_token.rs handle token creation and attenuation. 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.

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.

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

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

Create new effect traits when abstracting OS or external system integration. Use them when defining domain-specific operations that multiple implementations might provide. They isolate side effects for testing and simulation. They enable deterministic simulation of complex behaviors.

Follow YAGNI principles. Defer abstraction when only one implementation exists. Avoid abstractions that add complexity without clear benefit. Do not abstract without concrete need.

Application-specific effect traits should remain in their application layer. Do not move CliEffects or ConfigEffects from aura-terminal to aura-core when only one implementation exists. The aura-core crate provides infrastructure effects. Application layers compose these into domain-specific abstractions.

Database Effects

Database operations use existing effect traits rather than a dedicated DatabaseEffects layer. JournalEffects in aura-core provides fact insertion for monotone operations. Non-monotone operations use aura-consensus protocols driven by session types and the guard chain.

Reactive queries are handled via QueryEffects and ReactiveEffects. The coordination pattern follows two orthogonal dimensions described in Database Architecture. Authority scope determines single versus cross-authority operations. Agreement level determines monotone versus consensus operations.

Handler Design

Effect handlers implement effect traits. Stateless handlers execute operations without internal state. Stateful handlers coordinate multiple effects or maintain internal caches. Typed handlers implement concrete effect traits. Type-erased handlers allow dynamic dispatch through the effect executor.

Handlers do not store global state. All required inputs flow through method parameters. This avoids hidden dependencies and enables deterministic testing.

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>) -> SignalStream<T>
    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.

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. Tests must not depend on execution speed. Time-dependent behavior uses simulated time through effect handlers. Conformance artifacts use canonical encoding with deterministic field ordering.

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.

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.

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
• Automatic operation dependencies

To sequence operations, use session types (docs/108_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/113_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.

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

Gossip fanout k controls redundancy. Typical values are 3-5.

Threshold Checking

Witnesses check for threshold completion after each update.

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

    For each ((rid, pre_hash), S) in proposals:
        if |S| ≥ t:
            sig := CombineShares({ sh | (_, sh) in S })

            if VerifyThresholdSig(rid, sig):
                attesters := { w' | (w', _) in S }

                CommitFact(cid, rid, sig, attesters)

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

                decided[cid] := true
                return

Any witness reaching threshold broadcasts the commit fact. The first valid threshold signature wins.

9. Integration with Journals

Consensus emits commit facts. Journals merge commit facts using set union. Reduction interprets commit facts as confirmed non-monotone events.

Account journals integrate commit facts that represent tree operations. Relational context journals integrate commit facts that represent guardian bindings or recovery grants.

Reduction remains deterministic. Commit facts simply appear as additional facts in the semilattice.

A commit fact is monotone even when the event it represents is non-monotone. This supports convergence.

9.1 Context Isolation and Guard Integration

Every consensus instance binds to a context identifier. The context provides isolation for capability checking and flow budget enforcement. Authority-scoped ceremonies derive context from authority identity. Relational ceremonies use explicit context identifiers from the relational binding.

The protocol integrates with the guard chain at message send boundaries. Guards evaluate before constructing messages. The guard chain sequences capability checks, flow budget charges, leakage tracking, and journal coupling. Journal facts commit at the runtime bridge layer after guard evaluation completes.

#![allow(unused)]
fn main() {
// Protocol evaluates guards before sending
let guard = SignShareGuard::new(context_id, coordinator);
let guard_result = guard.evaluate(effects).await?;

if !guard_result.authorized {
    return Err(AuraError::permission_denied("Guard denied SignShare"));
}

// Construct and send message after guard approval
let message = ConsensusMessage::SignShare { ... };
}

The dependency injection pattern passes effect systems as parameters. Protocol methods accept generic effect trait bounds. This enables testing with mock effects and production use with real implementations. The pattern avoids storing effects in protocol state.

10. Integration Points

Consensus is used for account tree operations that require strong agreement. Examples include membership changes and policy changes when local signing is insufficient.

Consensus is also used for relational context operations. Guardian bindings use consensus to bind authority state. Recovery grants use consensus to approve account modifications. Application specific relational contexts may also use consensus.

11. FROST Threshold Signatures

Consensus uses FROST to produce threshold signatures. Each witness holds a secret share. Witnesses compute partial signatures. The initiator or fallback proposer aggregates the shares. The final signature verifies under the group public key stored in the commitment tree. See Authority and Identity for details on the TreeState structure.

#![allow(unused)]
fn main() {
/// From crates/aura-consensus/src/messages.rs
pub enum ConsensusMessage {
    SignShare {
        consensus_id: ConsensusId,
        /// The result_id (hash of execution result) this witness computed
        result_id: Hash32,
        share: PartialSignature,
        /// Optional commitment for the next consensus round (pipelining optimization)
        next_commitment: Option<NonceCommitment>,
        /// Epoch for commitment validation
        epoch: Epoch,
    },
    // ... other message variants
}
}

Witness shares validate only for the current consensus instance. They cannot be replayed. Witnesses generate only one share per (consensus_id, prestate_hash).

The attester set in the commit fact contains only devices that contributed signing shares. This provides cryptographic proof of participation.

11.1 Integration with Tree Operation Verification

When consensus produces a commit fact for a tree operation, the resulting AttestedOp is verified using the two-phase model from aura-core::tree::verification:

1. Verification (verify_attested_op): Cryptographic check against the BranchSigningKey stored in TreeState
2. Check (check_attested_op): Full verification plus state consistency validation

The binding message includes the group public key to prevent signature reuse attacks. This ensures an attacker cannot substitute a different signing key and replay a captured signature. See Tree Operation Verification for details.

#![allow(unused)]
fn main() {
// Threshold derived from policy at target node
let threshold = state.get_policy(target_node)?.required_signers(child_count);

// Signing key from TreeState
let signing_key = state.get_signing_key(target_node)?;

// Verify against stored key and policy-derived threshold
verify_attested_op(&attested_op, signing_key, threshold, current_epoch)?;
}

The verification step ensures signature authenticity. The check step validates state consistency. Both steps must pass before applying tree operations.

11.2 Type-Safe Share Collection

The implementation provides type-level guarantees for threshold signature aggregation. Share collection uses sealed and unsealed types to prevent combining signatures before reaching threshold. The type system enforces this invariant at compile time.

#![allow(unused)]
fn main() {
pub struct LinearShareSet {
    shares: BTreeMap<AuthorityId, PartialSignature>,
    sealed: bool,
}

pub struct ThresholdShareSet {
    shares: BTreeMap<AuthorityId, PartialSignature>,
}
}

The unsealed type accepts new shares via insertion. When threshold is reached the set seals into the threshold type. Only the threshold type provides the combine method. This prevents calling aggregation before sufficient shares exist.

The current protocol uses hash map based tracking for signature collection. The type-safe approach exists but awaits integration. Future work will replace runtime threshold checks with compile-time proofs. The sealed type pattern eliminates an entire class of bugs.

12. FROST Commitment Pipeline Optimization

The pipelined commitment optimization reduces steady-state consensus from 2 RTT (round-trip times) to 1 RTT by bundling next-round nonce commitments with current-round signature shares.

12.1 Overview

The FROST pipelining optimization improves consensus performance by bundling next-round nonce commitments with current-round signature shares. This allows the coordinator to start the next consensus round immediately without waiting for a separate nonce commitment phase.

Standard FROST Consensus (2 RTT):

1. Execute → NonceCommit (1 RTT): Coordinator sends execute request, witnesses respond with nonce commitments
2. SignRequest → SignShare (1 RTT): Coordinator sends aggregated nonces, witnesses respond with signature shares

Pipelined FROST Consensus (1 RTT) (after warm-up):

1. Execute+SignRequest → SignShare+NextCommitment (1 RTT):
   • Coordinator sends execute request with cached commitments from previous round
   • Witnesses respond with signature share AND next-round nonce commitment

12.2 Core Components

WitnessState (aura-consensus/src/witness.rs) manages persistent nonce state for each witness:

#![allow(unused)]
fn main() {
pub struct WitnessState {
    /// Witness identifier
    witness_id: AuthorityId,

    /// Current epoch to detect when cached commitments become stale
    epoch: Epoch,

    /// Precomputed nonce for the next consensus round
    next_nonce: Option<(NonceCommitment, NonceToken)>,

    /// Active consensus instances this witness is participating in
    active_instances: HashMap<ConsensusId, WitnessInstance>,
}
}

Key methods:

• get_next_commitment(): Returns cached commitment if valid for current epoch
• take_nonce(): Consumes cached nonce for use in current round
• set_next_nonce(): Stores new nonce for future use
• invalidate(): Clears cached state on epoch change

Message Schema Updates: The SignShare message now includes optional next-round commitment:

#![allow(unused)]
fn main() {
SignShare {
    consensus_id: ConsensusId,
    share: PartialSignature,
    /// Optional commitment for the next consensus round (pipelining optimization)
    next_commitment: Option<NonceCommitment>,
    /// Epoch for commitment validation
    epoch: Epoch,
}
}

ConsensusProtocol (aura-consensus/src/protocol.rs) integrates the pipelining optimization via FrostConsensusOrchestrator and WitnessTracker. The pipelining logic is distributed across these components rather than isolated in a separate orchestrator.

Key methods:

• run_consensus(): Determines fast path vs slow path based on cached commitments
• can_use_fast_path(): Checks if sufficient cached commitments available
• handle_epoch_change(): Invalidates all cached state on epoch rotation

12.3 Epoch Safety

All cached commitments are bound to epochs to prevent replay attacks:

1. Epoch Binding: Each commitment is tied to a specific epoch
2. Automatic Invalidation: Epoch changes invalidate all cached commitments
3. Validation: Witnesses reject commitments from wrong epochs

#![allow(unused)]
fn main() {
// Epoch change invalidates all cached nonces
if self.epoch != current_epoch {
    self.next_nonce = None;
    self.epoch = current_epoch;
    return None;
}
}

12.4 Fallback Handling

The system gracefully falls back to 2 RTT when:

1. Insufficient Cached Commitments: Less than threshold witnesses have cached nonces
2. Epoch Change: All cached commitments become invalid
3. Witness Failures: Missing or invalid next_commitment in responses
4. Initial Bootstrap: First round after startup (no cached state)

#![allow(unused)]
fn main() {
if has_quorum {
    // Fast path: 1 RTT using cached commitments
    self.run_fast_path(...)
} else {
    // Slow path: 2 RTT standard consensus
    self.run_slow_path(...)
}
}

12.5 Performance Impact

Latency Reduction:

• Before: 2 RTT per consensus
• After: 1 RTT per consensus (steady state)
• Improvement: 50% latency reduction

Message Count:

• Before: 4 messages per witness (Execute, NonceCommit, SignRequest, SignShare)
• After: 2 messages per witness (Execute+SignRequest, SignShare+NextCommitment)
• Improvement: 50% message reduction

Trade-offs:

• Memory: Small overhead for caching one nonce per witness
• Complexity: Additional state management and epoch tracking
• Bootstrap: First round still requires 2 RTT

12.6 Implementation Guidelines

Adding Pipelining to New Consensus Operations:

1. Update message schema: Add next_commitment and epoch fields to response messages
2. Generate next nonce: During signature generation, also generate next-round nonce
3. Cache management: Store next nonce in WitnessState for future use
4. Epoch handling: Always validate epoch before using cached commitments

Example Witness Implementation:

#![allow(unused)]
fn main() {
pub async fn handle_sign_request<R: RandomEffects + ?Sized>(
    &mut self,
    consensus_id: ConsensusId,
    aggregated_nonces: Vec<NonceCommitment>,
    current_epoch: Epoch,
    random: &R,
) -> Result<ConsensusMessage> {
    // Generate signature share
    let share = self.create_signature_share(consensus_id, aggregated_nonces)?;
    
    // Generate or retrieve next-round commitment
    let next_commitment = if let Some((commitment, _)) = self.witness_state.take_nonce(current_epoch) {
        // Use cached nonce
        Some(commitment)
    } else {
        // Generate fresh nonce
        let (nonces, commitment) = self.generate_nonce(random).await?;
        let token = NonceToken::from(nonces);
        
        // Cache for future
        self.witness_state.set_next_nonce(commitment.clone(), token, current_epoch);
        
        Some(commitment)
    };
    
    Ok(ConsensusMessage::SignShare {
        consensus_id,
        share,
        next_commitment,
        epoch: current_epoch,
    })
}
}

12.7 Security Considerations

1. Nonce Reuse Prevention: Each nonce is used exactly once and tied to specific epoch
2. Epoch Isolation: Nonces from different epochs cannot be mixed
3. Forward Security: Epoch rotation provides natural forward security boundary
4. Availability: Fallback ensures consensus continues even without optimization

12.8 Testing Strategy

Unit Tests:

• Epoch invalidation logic
• Nonce caching and retrieval
• Message serialization with new fields

Integration Tests:

• Fast path vs slow path selection
• Epoch transition handling
• Performance measurement

Simulation Tests:

• Network delay impact on 1 RTT vs 2 RTT
• Behavior under partial failures
• Convergence properties

12.9 Future Enhancements

1. Adaptive Thresholds: Dynamically adjust quorum requirements based on cached state
2. Predictive Caching: Pre-generate multiple rounds of nonces during idle time
3. Compression: Batch multiple commitments in single message
4. Cross-Context Optimization: Share cached state across related consensus contexts

13. Fallback Protocol Details

Fallback Trigger

The initiator can proactively trigger fallback when it detects conflicts.

Fallback_Trigger_Initiator(cid):
    // Extract conflicts from shares (same prestate_hash, different rid)
    conflicts := Map[(rid, prestate_hash) -> Set[(w, share)]]

    For each (w, (rid, share, prestate_hash)) in shares:
        conflicts[(rid, prestate_hash)] :=
            conflicts.get((rid, prestate_hash), ∅) ∪ { (w, share) }

    For all w in W:
        Send Conflict(cid, conflicts, EvidenceDelta(cid)) to w

This optimization seeds fallback with known conflicts. Witnesses also start fallback independently on timeout.

Fallback Message Handlers

Witnesses process fallback messages to accumulate shares.

On Conflict(cid, conflicts, evidΔ) from any peer:
    MergeEvidence(cid, evidΔ)

    For each ((rid, pre_hash), S) in conflicts:
        if not HasEquivocatedInSet(proposals, S, pre_hash):
            proposals[(rid, pre_hash)] :=
                proposals.get((rid, pre_hash), ∅) ∪ S

    CheckThreshold(cid)
    Fallback_Start(cid)

Conflict messages bootstrap the fallback phase. The witness merges non-equivocating shares.

On AggregateShare(cid, proposals', evidΔ) from any peer:
    MergeEvidence(cid, evidΔ)

    For each ((rid, pre_hash), S') in proposals':
        For each (w', sh') in S':
            if not HasEquivocated(proposals, w', cid, pre_hash, rid):
                proposals[(rid, pre_hash)] :=
                    proposals.get((rid, pre_hash), ∅) ∪ { (w', sh') }

    CheckThreshold(cid)

Aggregate shares spread proposal sets through gossip. Each witness checks for threshold after updates. Threshold-complete messages carry the final aggregated signature; once validated, the witness commits and stops its timers.

14. Safety Guarantees

Consensus satisfies agreement. At most one commit fact forms for a given (cid, prestate_hash). The threshold signature ensures authenticity. No attacker can forge a threshold signature without the required number of shares.

Consensus satisfies validity. A commit fact references a result computed from the agreed prestate. All honest witnesses compute identical results. Malformed shares are rejected.

Consensus satisfies deterministic convergence. Evidence merges through CRDT join. All nodes accept the same commit fact.

Formal Verification Status

These properties are formally verified through complementary approaches:

• Lean 4 Proofs (verification/lean/Aura/Consensus/):

  • Agreement.agreement: Unique commit per consensus instance
  • Validity.validity: Committed values bound to prestates
  • Validity.prestate_binding_unique: Hash collision resistance for prestate binding
  • Equivocation.detection_soundness: Conflicting signatures are detectable

• Quint Model Checking (verification/quint/protocol_consensus*.qnt):

  • AllInvariants: Combined safety properties pass 1000-sample model checking
  • InvariantByzantineThreshold: Byzantine witnesses bounded below threshold
  • InvariantEquivocationDetected: Equivocation detection correctness
  • InvariantProgressUnderSynchrony: Liveness under partial synchrony

See verification/quint/ and verification/lean/ for verification artifacts and run notes.

Binding Message Security

The binding message for tree operations includes the group public key. This prevents key substitution attacks where an attacker captures a valid signature and replays it with a different key they control. The full binding includes:

• Domain separator for domain isolation
• Parent epoch and commitment for replay prevention
• Protocol version for upgrade safety
• Current epoch for temporal binding
• Group public key for signing group binding
• Serialized operation content

This security property is enforced by compute_binding_message() in the verification module.

15. Liveness Guarantees

The fast path completes in one round trip when the initiator and witnesses are online. The fallback path provides eventual completion under asynchrony. Gossip ensures that share proposals propagate across partitions.

The protocol does not rely on stable leaders. No global epoch boundaries exist. Witnesses can rejoin by merging the journal fact set.

Fallback State Diagram

stateDiagram-v2
    [*] --> FastPath
    FastPath --> FallbackPending: timeout or conflict
    FallbackPending --> FallbackGossip: send Conflict/AggregateShare
    FallbackGossip --> Completed: threshold signature assembled
    FastPath --> Completed: Commit broadcast
    Completed --> [*]

• FastPath: initiator collecting shares.
• FallbackPending: timer expired or conflicting (rid, prestate_hash) observed.
• FallbackGossip: witnesses exchange proposal sets until CheckThreshold succeeds.
• Completed: commit fact accepted and timers stopped.

Design Trade-offs: Latency vs Availability

The two protocol paths optimize for different objectives:

Why leaderless gossip for fallback?

We intentionally sacrifice tight timing bounds (the theoretical 2Δ from optimal protocols) for:

1. Partition tolerance: Any connected component with k honest witnesses can complete independently. No leader election needed across partitions.

2. No single point of failure: If the initiator fails, any witness can drive completion. View-based protocols require leader handoff.

3. Simpler protocol: No view numbers, no leader election, no synchronization barriers. Witnesses simply gossip until threshold is reached.

4. Natural CRDT integration: Evidence propagates as a CRDT set. Gossip naturally merges evidence without coordination.

What we can prove:

• Fast path: Commits within 2δ when all witnesses online (verified: TemporalFastPathBound)
• Slow path: Commits when any connected component has k honest witnesses (not time-bounded)
• Safety: Always holds regardless of network conditions

What we cannot prove (by design):

• Slow path completion in fixed time (would require synchrony assumption)
• Termination under permanent partition (FLP impossibility)

Parameter Guidance

• T_fallback: set to roughly 2-3 times the median witness RTT. Too aggressive causes unnecessary fallback. Too lax delays recovery when an initiator stalls.
• Gossip fanout f: see the fanout adequacy analysis below for principled selection.
• Gossip interval: 250-500 ms is a good default. Ensure at least a few gossip rounds occur before timers retrigger. This gives the network time to converge.

These parameters should be tuned per deployment. The ranges above keep fallback responsive without overwhelming the network.

Fanout Adequacy for Slow Path

The slow path requires the gossip network to be connected for evidence propagation. The key question is how many gossip peers (fanout f) are needed.

Random Graph Connectivity Theory

For a random graph G(n, p) to be connected with high probability (w.h.p.), the classical Erdős-Rényi result states:

p ≥ (1 + ε) × ln(n) / n    for any ε > 0

Translating to gossip: each node selects f random peers, giving edge probability p ≈ f/n. For connectivity:

f ≥ c × ln(n)    where c ≈ 1.1-1.2 for practical certainty

Recommended Fanout by Witness Count

Failure Tolerance

With fanout f and n witnesses, the graph remains connected under random node failures as long as:

• At least f + 1 nodes remain (sufficient edges for spanning tree)
• Failed nodes are randomly distributed (not targeted attacks)

For k-of-n threshold where k ≤ n - f:

• The k honest witnesses form a connected subgraph w.h.p.
• Each honest witness can reach at least one other honest witness via gossip
• Evidence propagates to all honest witnesses in O(log(n)) gossip rounds

Adversarial Considerations

Random graph analysis assumes non-adversarial peer selection. Against Byzantine adversaries:

1. Eclipse attacks: If adversary controls gossip peer selection, connectivity guarantees fail
2. Mitigation: Use deterministic peer selection based on witness IDs (e.g., consistent hashing)
3. Stronger bound: For Byzantine tolerance, use f ≥ 2t + 1 where t is Byzantine threshold

Verified Properties (Quint)

The following properties are model-checked in protocol_consensus_liveness.qnt:

• PropertyQuorumSufficient: k honest witnesses in same connected component can progress
• PropertyPartitionTolerance: largest connected component with k honest succeeds
• AvailabilityGuarantee: combined availability invariant

With adequate fanout, these properties ensure slow path completion when quorum exists.

16. Relation to FROST

Consensus uses FROST as the final stage of agreement. FROST ensures that only one threshold signature exists per result. FROST signatures provide strong cryptographic proof.

Consensus and FROST remain separate. Consensus orchestrates communication. FROST proves final agreement. Combining the two yields a single commit fact.

17. Operation Categories

Not all operations require consensus. Aura classifies operations into three categories based on their security requirements and execution timing.

17.1 Category A: Optimistic Operations

Operations that can proceed immediately without consensus. These use CRDT facts with eventual consistency.

Characteristics:

• Immediate local effect
• Background sync via anti-entropy
• Failure shows indicator, doesn't block functionality
• Partial success is acceptable

Examples:

• Send message (within established context)
• Create channel (within established relational context)
• Update channel topic
• Block/unblock contact
• Pin message

These operations work because the cryptographic context already exists. Keys derive deterministically from shared journal state. No new agreement is needed.

17.2 Category B: Deferred Operations

Operations that apply locally but require agreement for finalization. Effect is pending until confirmed.

Characteristics:

• Immediate local effect shown as "pending"
• Background ceremony for agreement
• Failure triggers rollback with user notification
• Multi-moderator operations use this pattern

Examples:

• Change channel permissions (requires moderator consensus)
• Remove channel member (may be contested)
• Transfer channel ownership
• Rename channel

17.3 Category C: Consensus-Gated Operations

Operations where partial state is dangerous. These block until consensus completes.

Characteristics:

• Operation does NOT proceed until consensus achieved
• Partial state would be dangerous or irrecoverable
• User must wait for confirmation

Examples:

• Guardian rotation (key shares distributed atomically)
• Recovery execution (account state replacement)
• OTA hard fork activation (breaking protocol change)
• Device revocation (security-critical removal)
• Add contact / Create group (establishes cryptographic context)
• Add member to group (changes group encryption keys)

These use Aura Consensus as described in this document.

17.4 Decision Tree

Does this operation establish or modify cryptographic relationships?
│
├─ YES: Does the user need to wait for completion?
│       │
│       ├─ YES (new context, key changes) → Category C (Consensus)
│       │   Examples: add contact, create group, guardian rotation
│       │
│       └─ NO (removal from existing context) → Category B (Deferred)
│           Examples: remove from group, revoke device
│
└─ NO: Does this affect other users' access or policies?
       │
       ├─ YES: Is this high-security or irreversible?
       │       │
       │       ├─ YES → Category B (Deferred)
       │       │   Examples: transfer ownership, delete channel
       │       │
       │       └─ NO → Category A (Optimistic)
       │           Examples: pin message, update topic
       │
       └─ NO → Category A (Optimistic)
           Examples: send message, create channel, block contact

17.5 Key Insight

Ceremonies establish shared cryptographic context. Operations within that context are cheap.

Once a relational context exists (established via Category C invitation ceremony), channels and messages within that context are Category A. The expensive part is establishing WHO is in the relationship. Once established, operations WITHIN the relationship derive keys deterministically from shared state.

See work/optimistic.md for detailed design and effect policy integration.

18. BFT‑DKG Transcript Finalization (K3)

Consensus is also used to finalize BFT-DKG transcripts. The output of the DKG is a DkgTranscriptCommit fact that is consensus-finalized and then merged into the relevant journal.

Inputs

• DkgConfig: epoch, threshold, max_signers, participants, membership_hash.
• DealerPackage[]: one package per dealer, containing encrypted shares for all participants and a deterministic commitment.
• prestate_hash and operation_hash: bind the transcript to the authority/context state and the intended ceremony operation.

Transcript formation

1. Validate DkgConfig and dealer packages (unique dealers, complete share sets).
2. Assemble the transcript deterministically.
3. Hash the transcript using canonical DAG-CBOR encoding.

Finalize with consensus

1. Build DkgTranscriptCommit with:
   • transcript_hash
   • blob_ref (optional, if stored out‑of‑line)
   • prestate_hash
   • operation_hash
   • config and participants
2. Run consensus over the commit fact itself.
3. Insert both CommitFact evidence and the DkgTranscriptCommit fact into the authority or context journal.

The transcript commit is the single durable artifact used to bootstrap all subsequent threshold operations. Any K3 ceremony that depends on keys must bind to this commit by reference (direct hash or blob ref).

19. Decentralized Coordinator Selection (Lottery)

Coordinator-based fast paths (A2) require a deterministic, decentralized selection mechanism so every participant can independently derive the same leader without extra coordination.

Round seed

• round_seed is a 32‑byte value shared by all participants for the round.
• Sources:
  • VRF output (preferred when available).
  • Trusted oracle or beacon.
  • Initiator‑provided seed (acceptable in trusted settings).

Selection rule

score_i = H("AURA_COORD_LOTTERY" || round_seed || authority_id_i)
winner = argmin_i score_i

Fencing + safety

• The coordinator must hold a monotonic fencing token (coord_epoch).
• Proposals are rejected if coord_epoch does not advance or if prestate_hash mismatches local state.

Convergence

• Coordinators emit a ConvergenceCert once a quorum acks the proposal.
• Fast-path results remain soft-safe until a consensus CommitFact is merged.

20. Summary

Aura Consensus produces monotone commit facts that represent non-monotone operations. It integrates with journals through set union. It uses FROST threshold signatures and CRDT evidence structures. It provides agreement, validity, and liveness. It supports authority updates and relational operations. It requires no global log and no central coordinator. The helper HasEquivocatedInSet excludes conflict batches that contain conflicting signatures from the same witness. Fallback_Start transitions the local state machine into fallback mode and arms gossip timers. Implementations must provide these utilities alongside the timers described earlier.

See Also

• Operation Categories - When consensus is required and ceremony lifecycle
• Relational Contexts - Consensus integration for relational operations

Operation Categories

This document defines the three-tier classification system for distributed operations in Aura. It specifies the ceremony contract for Category C operations, the consistency metadata types for each category, and the decision framework for categorizing new operations. The core insight is that not all operations require consensus. Many can proceed optimistically with background reconciliation.

1. Overview

Operations in Aura fall into three categories based on their effect timing and security requirements.

Agreement modes are orthogonal to categories. Operations can use provisional or soft-safe fast paths, but any durable shared state must be consensus-finalized (A3). See Consensus for the fast-path and finalization taxonomy.

1.1 Key Generation Methods

Aura separates key generation from agreement: