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 inaura-journalbecause reduction semantics depend on them.Generic { .. }: Extensibility hook for domain facts (DomainFact+FactReducer).
Criteria for ProtocolRelationalFact (all must hold):
- Reduction-coupled: the fact directly affects core reduction invariants in
reduce_context()(not just a view). - Cross-domain: the fact’s semantics are shared across multiple protocols or layers.
- 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_IDconstant (unique, registered incrates/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 explicitencode_domain_fact/VersionedMessagehelpers. - Context derivation: declare
context/context_fnforDomainFactor implement a stablecontext_id()derivation. - Reducer registration: provide a
FactReducerand 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:
- No HashMap iteration: All maps use BTreeMap for consistent ordering
- No system time: OrderTime tokens provide opaque ordering
- No floating point: All arithmetic uses exact integer/fixed-point
- 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:
- Identify all
AttestedOpfacts. - Group operations by their referenced parent state (epoch + commitment).
- For concurrent operations (same parent), select winner using max hash tie-breaking:
H(op)comparison. - Apply winners in topological order respecting parent dependencies.
- 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(...):
GuardianBindingmaps toRelationalBindingfor guardian relationshipsRecoveryGrantcreates recovery permission bindings between authoritiesConsensusstores generic bindings with consensus metadataAmpChannelCheckpointanchors channel state snapshots for AMP messagingAmpProposedChannelEpochBumpandAmpCommittedChannelEpochBumptrack channel epoch transitionsAmpChannelPolicydefines channel-specific policy overrides for skip windowsDkgTranscriptCommitstores consensus-finalized DKG transcriptsConvergenceCertrecords soft-safe convergence certificatesReversionFacttracks explicit reversion eventsRotateFactmarks 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 fromaura-core::tree::verification:verify_attested_op(): Cryptographic signature check againstBranchSigningKeystored in TreeStatecheck_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.,
AddLeafindexes a valid parent node).
See Tree Operation Verification for details on the verify/check model and binding message security.
Responsible Effects
CryptoEffectsfor FROST signature verification viaverify_attested_op().JournalEffectsfor parent lookup, state consistency viacheck_attested_op(), and conflict detection.StorageEffectsto 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/RelationalEffectsfor context membership checks.CryptoEffectsfor consensus proof verification.JournalEffectsfor context-specific merge.
13.3 FlowBudget Facts
Checks
- Ensure
spentdeltas 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.JournalEffectsgate insertion to prevent stale epochs from updating headroom.
13.4 Snapshot Facts
Checks
- Confirm the snapshot
state_hashmatches the hash of all facts below the snapshot. - Ensure no newer snapshot already exists for the namespace (check
sequencenumber). - Verify that pruning according to the snapshot does not remove facts still referenced by receipts or pending consensus operations.
Responsible Effects
JournalEffectscompute and validate snapshot digests.StorageEffectspersist 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):
| Field | Type | Purpose |
|---|---|---|
agreement | Agreement | Finalization level (A1 Provisional, A2 SoftSafe, A3 Finalized) |
propagation | Propagation | Anti-entropy sync status (Local, Syncing, Complete, Failed) |
ack_tracked | bool | Opt-in flag for per-peer acknowledgment tracking |
14.2 Ack Storage Table
For facts with ack_tracked = true, acknowledgments are stored in a separate table:
| fact_id | peer_id | acked_at |
|---|---|---|
| msg-001 | alice_authority_id | 2024-01-15T10:30:00Z |
| msg-001 | bob_authority_id | 2024-01-15T10:30:05Z |
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