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