Journal

This document describes the journal architecture and state reduction system in Aura. It explains how journals implement CRDT semantics, how facts are structured, and how reduction produces deterministic state for account authorities and relational contexts.

It describes the reduction pipeline, flow budget semantics, and integration with the effect system. It defines the invariants that ensure correctness. See Maintenance for the end-to-end snapshot and garbage collection pipeline.

Hybrid Journal Model (Facts + Capabilities)

Aura’s journal state is a composite of:

Fact Journal: the canonical, namespaced CRDT of immutable facts.
Capability Frontier: the current capability lattice for the namespace.
Composite journal view: the runtime carries facts and capabilities together when evaluating effects.

The fact journal is stored and merged as a semilattice. Capabilities are refined via meet. The runtime always treats these as orthogonal dimensions of state.

1. Journal Namespaces

Aura maintains a separate journal namespace for each authority and each relational context. A journal namespace stores all facts relevant to the entity it represents. A namespace is identified by an AuthorityId (see Authority and Identity) or a ContextId and no namespace shares state with another. Identifier definitions appear in Identifiers and Boundaries.

A journal namespace evolves through fact insertion. Facts accumulate monotonically. No fact is removed except through garbage collection rules that preserve logical meaning.

#![allow(unused)]
fn main() {
pub struct Journal {
    pub namespace: JournalNamespace,
    pub facts: BTreeSet<Fact>,
}

pub enum JournalNamespace {
    Authority(AuthorityId),
    Context(ContextId),
}
}

This type defines a journal as a namespaced set of facts. The namespace identifies whether this journal tracks an authority's commitment tree or a relational context. The journal is a join semilattice under set union where merging two journals produces a new journal containing all facts from both inputs. Journals with different namespaces cannot be merged.

2. Fact Model

Facts represent immutable events or operations that contribute to the state of a namespace. Facts have ordering tokens, timestamps, and content. Facts do not contain device identifiers used for correctness.

#![allow(unused)]
fn main() {
pub struct Fact {
    pub order: OrderTime,
    pub timestamp: TimeStamp,
    pub content: FactContent,
}

pub enum FactContent {
    AttestedOp(AttestedOp),
    Relational(RelationalFact),
    Snapshot(SnapshotFact),
    RendezvousReceipt {
        envelope_id: [u8; 32],
        authority_id: AuthorityId,
        timestamp: TimeStamp,
        signature: Vec<u8>,
    },
}
}

The order field provides an opaque, privacy-preserving total order for deterministic fact ordering in the BTreeSet. The timestamp field provides semantic time information for application logic. Facts implement Ord via the OrderTime field. Do not use TimeStamp for cross-domain indexing or total ordering. Use OrderTime or consensus/session sequencing instead.

This model supports account operations, relational context operations, snapshots, and rendezvous receipts. Each fact is self contained. Facts are validated before insertion into a namespace.

Bootstrap genesis completion requires an authenticated device-creation AttestedOp under the retained epoch-zero key, together with its durable operation bytes and tree index entry. An in-memory reducer/cache entry alone cannot prove commit after a failed storage write. A persisted completion record binds the exact creation-operation digest; matching device IDs without matching keys and signed creation evidence cannot establish bootstrap readiness.

2.2 Protocol-Level vs Domain-Level Relational Facts

RelationalFact has only two variants:

Protocol(ProtocolRelationalFact): Protocol-level facts that must live in aura-journal because reduction semantics depend on them.
Generic { .. }: Extensibility hook for domain facts (DomainFact + FactReducer).

Criteria for ProtocolRelationalFact (all must hold):

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

Domain facts are the extensibility mechanism for feature crates. They are stored as RelationalFact::Generic envelopes and reduced by registered FactReducers. Every domain fact family follows the canonical domain fact model of §4.2.1: one derive codec, one declared schema version, registration in the agent FactRegistry, and a reduction that is a pure function of the fact set.

3. Semilattice Structure

Journals use a join semilattice. The semilattice uses set union as the join operator with partial order defined by subset inclusion. The journal never removes facts during merge. Every merge operation increases or preserves the fact set.

The join semilattice ensures convergence across replicas. Any two replicas that exchange facts eventually converge to identical fact sets. All replicas reduce the same fact set to the same state.

The merge operation asserts namespace equality, unions the fact sets, and returns the combined journal. The result is monotonic and convergent.

4. Reduction Pipeline

Aura maintains two replicated state machines. Account journals describe commitment trees for authorities. Relational context journals describe cross-authority coordination. Both use the same fact-only semilattice and deterministic reducers.

flowchart TD
    A[Ledger append] --> B[Journal merge];
    B --> C[Group by parent];
    C --> D[Resolve conflicts via max hash];
    D --> E[Apply operations in topological order];
    E --> F[Recompute commitments bottom-up];

Ledger append writes facts durably. Journal merge unions the fact set. Reducers group operations by parent commitment, resolve conflicts deterministically using max hash tie-breaking, and then apply winners in topological order. The final step recomputes commitments bottom-up which downstream components treat as the canonical state.

4.1 Fact Production

Account operations originate from local threshold signing or Aura Consensus. Relational context operations always run through Aura Consensus because multiple authorities must agree on the prestate. Each successful operation produces an AttestedOp fact. Receipts that must be retained for accountability are stored as RendezvousReceipt facts scoped to the context that emitted them. Implementations must only emit facts after verifying signatures and parent commitments.

4.2 Determinism Invariants

The reduction pipeline maintains strict determinism:

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.

4.2.1 Canonical Domain Fact Model

Facts reach replicas late, duplicated and out of order through sync. A domain fact family is therefore reduced by a pure function of its fact set: every permutation of the same facts yields the same state, and neither arrival order nor physical time decides an outcome.

Encoding, versioning and registration

Each domain fact type has one shape and one codec.

Derive codec. The type uses #[derive(DomainFact)] (aura-macros). The derive writes a DAG-CBOR FactEnvelope and decodes only DAG-CBOR. Hand-written impl DomainFact blocks and JSON envelopes are not used. The shared aura-core decode helpers reject a JSON envelope with FactError::NonCanonicalEncoding.
One schema version. #[domain_fact(type_id = ..., schema_version = N)] declares the only version, carried by the envelope. Decoding accepts exactly N. When the shape changes, the version is bumped and the old shape is replaced, not decoded: there is no supported-version range, no legacy decoder and no compatibility shim. The payload carries no version field of its own, and the type id carries no version suffix.
Type id and context. The type id is a plain string (a literal, a *_FACT_TYPE_ID constant or a zero-argument accessor), unique across the registry and listed in crates/aura-agent/src/fact_types.rs. The derive's context or context_fn names the fact's ContextId.
Keys and registration. Reducers and views address facts through the family's FactKey helpers, never ad hoc strings. Each type is registered with its FactReducer in build_fact_registry (crates/aura-agent/src/fact_registry.rs); a Layer 2 crate that cannot depend on aura-journal is registered through a transparent derive wrapper in a higher crate (maintenance facts use aura-sync::MaintenanceJournalFact).

Reduction patterns

aura-journal::causal_reduction provides the shared rules. A family composes them; it does not reimplement them.

Tagged observed-remove set. An add is identified by its tag. A reversal names the tags of the adds of the same key that its writer observed. The set keeps every add that no reversal revokes, so a concurrent add the reversal's writer did not observe survives. Contacts (existence per owner and contact), web-of-trust introductions, home bans and mutes, and social lifecycle pairs use this pattern.
Multi-value register. A write names the writes of the same key it supersedes. The register keeps every write that no observing write supersedes and that is not causally before another write. The family resolves the remaining concurrent writes by an explicit domain policy, then by causal order. Contact nicknames and read-receipt policy, access overrides, storage readings and chat message revisions use this pattern.
Episodes. State that can end and restart, such as a friendship, a channel membership or a home neighborhood join, is a sequence of episodes. A terminal fact ends the episodes its writer observed, and only a fact that starts a new episode re-admits the subject. A late or replayed fact from an ended episode cannot reopen it.
Explicit terminal precedence. Families whose outcomes are terminal rather than reversible, such as recovery and invitation outcomes, define a total precedence over terminal states and resolve ties by causal order or canonical bytes. Protocol facts follow the same rule: AMP channel bootstraps resolve to the smallest bootstrap_id, then full fact order.

Causal stamps and time

A reversible or overwritable fact carries aura_core::time::CausalMetadata, stamped by the writer before commit:

clock: the writer's LogicalClock after observing every fact of the family it holds.
revokes: for a reversal, the tags of the observed adds of the same key.
supersedes: for a register write, the tags of the observed writes of the same key.

The tag itself is not carried. Every reader derives it as the hash of the fact's type id and canonical re-encoding, which names the author and includes the clock. A peer cannot claim another fact's tag to revoke or shadow it, and distinct content never shares a tag.

Writers obtain the metadata through RuntimeBridge::causal_stamp(CausalStampKey), which advances the runtime's logical clock past the family's committed facts for that key. CausalStampKey names the family and key: HomeGovernance, Contact, Friendship, Chat and InvitationOutcome.

Causal order (causal_cmp) is happens-before, then TimeStamp::sort_compare with OrderingPolicy::DeterministicTieBreak, then causal depth, Lamport scalar and tag. It is the tie-break of last resort and the order for display. Physical time is for user-visible timestamps and expiry only. Expiry is evaluated at query time against a caller-supplied instant, never during reduction.

Verification and enforcement

assert_permutation_invariant is the shared test harness: it reduces every permutation of a small fact set and requires identical state. Every reversible family keeps such a regression next to its reducer.

just ci-domain-fact-model (also run by just ci-ownership-policy) is a Rust-native syntax check in toolkit/xtask. Over production code it requires that every DomainFact type uses the derive, has a resolvable unversioned type id and no in-payload version field, and is registered in the FactRegistry. It rejects JSON envelopes in domain fact crates. It keeps a typed inventory of reversible families; a fact carrying CausalMetadata must belong to a listed family, and each family must keep a test-scope assert_permutation_invariant call. The derive itself rejects a min_supported_schema_version key.

Home governance (docs/115 §3.4), social lifecycle (docs/115 §3.5), contacts (aura-relational::contacts), the web of trust (aura-relational::wot), recovery (aura-recovery::state), invitation outcomes (aura-invitation::lifecycle), chat revisions (aura-chat::revisions) and AMP channel membership (aura-amp::channel) follow this model.

4.3 Canonical Entity Materialization

A channel, home, invitation, or contact exists in a projection only after its domain creation fact or an equivalent authenticated creation outcome supplies the canonical identity and required metadata. A membership, relationship, status, rename, or activity fact may change an existing entity but cannot establish one. Raw identifiers identify a candidate; they are not evidence of canonical name, context, type, or relationship.

Reduction is independent of delivery order. Enrichment facts that arrive before creation remain applicable when matching creation evidence arrives. Facts for a different entity or context cannot contribute members, counts, labels, or status. Duplicate facts do not create duplicate entities or inflate counts. Replaying the same fact set after restart yields the same materialized entities and metadata as live reduction.

For homes, an accepted inviter reloads its committed HomeCreated fact before applying membership enrichment. The app's home creation witness can be derived only from that fact shape; acceptance or membership alone cannot create the home projection. Nonempty home snapshots round-trip typed home and authority identifiers through JSON without changing their identities or counts.

5. Account Journal Reduction

Account journals store attested operations for commitment tree updates. Reduction computes a TreeStateSummary (epoch, commitment, threshold, device count) from the fact set. See Authority and Identity for structure details. The summary is a lightweight public view that hides internal device structure. For the full internal representation with branches, leaves, and topology, see TreeState in aura-journal::commitment_tree.

Internally, AuthorityTreeState materializes explicit branch topology to support incremental commitment updates. It keeps ordered branch children, branch/leaf parent pointers, and branch depth metadata. The topology is deterministic: active leaves are sorted by LeafId, paired in stable order, and materialized with NodeIndex(0) as root followed by breadth-first branch assignment. This guarantees identical branch structure for identical active leaf sets across replicas.

Commitment recomputation for non-structural mutations is path-local. Aura marks affected branches dirty, collects their paths to root, then recomputes only those branches bottom-up. Structural mutations (AddLeaf, RemoveLeaf) currently use deterministic rebuild of topology and branch commitments (correctness-first baseline). Merkle proof paths are derived from the same materialized topology so proof generation and commitment caches share one source of truth.

Maintenance note: do not change topology construction or branch indexing rules without updating replay fixtures and root commitment fixtures. Determinism depends on stable leaf sort order, stable pair composition, and stable branch index assignment.

Reduction follows these steps:

Identify all AttestedOp facts.
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(...):

GuardianBinding maps to RelationalBinding for guardian relationships
RecoveryGrant creates recovery permission bindings between authorities
Consensus stores generic bindings with consensus metadata
AmpChannelCheckpoint anchors channel state snapshots for AMP messaging
AmpProposedChannelEpochBump and AmpCommittedChannelEpochBump track channel epoch transitions
AmpChannelPolicy defines channel-specific policy overrides for skip windows
DkgTranscriptCommit stores consensus-finalized DKG transcripts
ConvergenceCert records soft-safe convergence certificates
ReversionFact tracks explicit reversion events
RotateFact marks lifecycle rotation or upgrade events

Domain-specific facts use Generic { context_id, binding_type, binding_data } and are reduced by registered FactReducer implementations.

Reduction verifies that relational facts reference valid authority commitments and applies them in dependency order.

Enrollment response evidence and recovery

Enrollment acceptance requires the expected verifier selected by explicit setup transfer and retained for that ceremony. A participant count, a persisted terminal outcome, or a deserialized response does not establish acceptance provenance. Recording and activation require an opaque witness minted after verification of the exact response against that retained verifier.

Durable recovery retains the original response and its subject, invitation, ceremony, device, pending epoch and setup binding. Recovery revalidates this material before issuing a new process-local witness. Missing, corrupt or legacy active records without verifier evidence fail closed. Observing a historical terminal result does not authorize a new activation.

The first durable response decision is stable under duplicate, concurrent and contradictory delivery. Required persistence failure must prevent acceptance from becoming visible to activation owners. Runtime receipts and committed journal facts have distinct provenance; a receipt alone cannot establish a consensus-finalized membership transition.

Enrollment VM control messages are authenticated against the independently selected initiator verifier retained with the signed manifest. Requests and confirmations bind the exact manifest digest and ceremony decision. Peer receipt keys or supplied digest strings cannot select that verifier. A response signer derives its physical identity and policy from locally retained setup possession and the sealed admitted manifest. Live response signing requires the current signer to match that original setup; retained evidence does not grant historical signing authority.

An established confirmation requires the authoritative committed terminal decision. Pending state is not a timeout. Recovery revalidates original retained independent pins before minting process-local admission evidence.

6.1 AMP Channel Epoch Transition Reduction

Reduced AMP epoch entries may contain staged policies, bootstrap metadata, or transition observations before creation. Canonical materialization requires the selected checkpoint for the exact context and channel. The reduced state retains checkpoint presence explicitly; an absent checkpoint cannot establish channel existence, readiness, or duplicate creation. Checkpoint evidence is observed journal content, not an authorization capability.

AMP channel epoch transition reduction is fact-only and deterministic. It refines the existing A1/A2/A3 operation model for channel epoch state without changing authority-root membership or account commitment tree rules.

Every AMP transition proposal, certificate, commit, abort, conflict, or supersession fact binds the same canonical transition_id when it refers to the same transition. The identity is the typed digest over:

context_id
channel_id
parent_epoch
parent_commitment
successor_epoch
successor_commitment
membership_commitment
transition_policy

Reducers group transition facts by (context_id, channel_id, parent_epoch, parent_commitment) and validate all facts in the group before exposing live state. Reducer validation covers parent binding, successor epoch validity, membership commitment validity, witness committee validity, A2 certificate thresholds, A3 commit evidence, and abort/conflict/supersession evidence.

For each parent group, reduction exposes one of:

State	Live successor exposed?	Meaning
`Observed`	No	One or more syntactically valid proposals exist without a live certificate.
`A2Live`	Yes	Exactly one valid unsuppressed AMP-certified successor exists.
`A2Conflict`	No	Multiple conflicting valid certificates or unresolved equivocation evidence exist.
`A3Finalized`	Yes	Consensus-backed commit finalizes one successor.
`A3Conflict`	No	Multiple conflicting durable commits or unresolved durable-commit evidence exist.
`Aborted`	No	Explicit abort evidence suppresses live use.
`Superseded`	Depends on successor	Authorized supersession replaces the earlier transition path.

If exactly one valid unsuppressed A3 commit exists, that transition is both the durable and live successor. Otherwise, if exactly one valid unsuppressed A2 certificate exists, that transition is the live successor but remains non-durable. If conflicting valid A2 certificates exist and facts do not resolve the conflict, reduction exposes no live successor and marks the parent state conflict-tainted.

Reducers must not use local wall-clock time, network connectivity, operator preference, arrival order, or hash tie-breaking between conflicting valid A2 certificates to choose a live successor. Single-winner exposure must come from fact validation: a valid AMP certificate, a valid A3 commit, explicit equivocation evidence, abort evidence, or supersession evidence.

The aura-journal context reducer exposes this state as structured AMP transition reduction data. RelationalState::amp_transitions is keyed by AmpTransitionParentKey { context, channel, parent_epoch, parent_commitment }. Each AmpTransitionReduction records observed, certified, finalized, suppressed, conflict, and emergency evidence ids for that parent. ChannelEpochState::transition points at the current parent transition, and ChannelEpochState::pending_bump is populated only when the current parent is A2Live. Emergency reducer fields include suspect authorities, quarantine successor epochs, and prune-before epochs derived from emergency alarms and emergency transition facts.

The reduced channel view distinguishes:

stable_epoch: last durable committed epoch
live_successor: optional A2-certified successor for the stable epoch
durable_successor: optional A3-finalized successor
transition_state: one of the states above
conflict_evidence: optional witness or transition evidence when conflict-tainted
emergency policy fields such as suspect authority, quarantine epoch, and prune-before epoch when an emergency transition is active

The AMP message ratchet consumes this reducer output. It does not author membership truth, choose between transitions, or repair missing control-plane facts.

7. Flow Budgets

Flow budgets track message sending allowances between authorities. The FlowBudget structure uses semilattice semantics for distributed convergence:

#![allow(unused)]
fn main() {
pub struct FlowBudget {
    pub limit: u64,
    pub spent: u64,
    pub epoch: Epoch,
}

impl FlowBudget {
    pub fn merge(&self, other: &Self) -> Self {
        Self {
            limit: self.limit.min(other.limit),
            spent: self.spent.max(other.spent),
            epoch: if self.epoch.value() >= other.epoch.value() {
                self.epoch
            } else {
                other.epoch
            },
        }
    }
}
}

The spent field uses join-semilattice (max) because charges only increase. The limit field uses meet-semilattice (min) because the most restrictive limit wins. The epoch field advances monotonically. Spent resets on epoch rotation.

Flow budget tracking operates at the runtime layer via FlowBudgetManager. The RelationalState includes a flow_budgets map for CRDT-based replication of budget state across replicas.

8. Receipts and Accountability

Receipts reference the current epoch commitment so reducers can reject stale receipts automatically. The RendezvousReceipt variant in FactContent stores accountability proofs (envelope ID, authority, timestamp, signature). Receipts are stored as relational facts scoped to the emitting context. This coupling ensures that receipt validity follows commitment tree epochs.

9. Snapshots and Garbage Collection

Snapshots summarize all prior facts. A snapshot fact contains a state hash, the list of superseded facts, and a sequence number. A snapshot establishes a high water mark. Facts older than the snapshot can be pruned.

#![allow(unused)]
fn main() {
pub struct SnapshotFact {
    pub state_hash: Hash32,
    pub superseded_facts: Vec<OrderTime>,
    pub sequence: u64,
}
}

Garbage collection removes pruned facts while preserving logical meaning. Pruning does not change the result of reduction. The GC algorithm uses safety margins to prevent premature pruning:

Default skip window: 1024 generations
Safety margin: skip_window / 2
Pruning boundary: max_generation - (2 * skip_window) - safety_margin

Helper functions (compute_checkpoint_pruning_boundary, can_prune_checkpoint, can_prune_proposed_bump) determine what can be safely pruned based on generation boundaries.

10. Journal Effects Integration

The effect system provides journal operations through JournalEffects. This trait handles persistence, merging, and flow budget tracking:

#![allow(unused)]
fn main() {
#[async_trait]
pub trait JournalEffects: Send + Sync {
    async fn merge_facts(&self, target: Journal, delta: Journal) -> Result<Journal, AuraError>;
    async fn refine_caps(&self, target: Journal, refinement: Journal) -> Result<Journal, AuraError>;
    async fn get_journal(&self) -> Result<Journal, AuraError>;
    async fn persist_journal(&self, journal: &Journal) -> Result<(), AuraError>;
    async fn get_flow_budget(&self, context: &ContextId, peer: &AuthorityId) -> Result<FlowBudget, AuraError>;
    async fn update_flow_budget(&self, context: &ContextId, peer: &AuthorityId, budget: &FlowBudget) -> Result<FlowBudget, AuraError>;
    async fn charge_flow_budget(&self, context: &ContextId, peer: &AuthorityId, cost: FlowCost) -> Result<FlowBudget, AuraError>;
}
}

The effect layer writes facts to persistent storage. Replica synchronization loads facts through effect handlers into journal memory. The effect layer guarantees durability but does not affect CRDT merge semantics.

At the choreography runtime boundary, journal coupling is always driven by guard/effect commands. Generated choreography annotations and runtime guard checks emit EffectCommand values, and JournalCoupler ensures journal commits occur before transport observables. In VM execution, AuraVmEffectHandler emits envelopes, but journal writes still flow through the same EffectInterpreter + JournalEffects path.

11. AttestedOp Structure

AttestedOp exists in two layers with different levels of detail:

Layer 1 (aura-core) - Full operation metadata:

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

pub struct TreeOp {
    pub parent_epoch: Epoch,
    pub parent_commitment: TreeHash32,
    pub op: TreeOpKind,
    pub version: u16,
}
}

Layer 2 (aura-journal) - Flattened for journal storage:

#![allow(unused)]
fn main() {
pub struct AttestedOp {
    pub tree_op: TreeOpKind,
    pub parent_commitment: Hash32,
    pub new_commitment: Hash32,
    pub witness_threshold: u16,
    pub signature: Vec<u8>,
}
}

The aura-core version includes epoch and version for full verification. The aura-journal version includes computed commitments for efficient reduction.

12. Invariants

The journal and reduction architecture satisfy several invariants:

Convergence: All replicas reach the same state when they have the same facts
Idempotence: Repeated merges or reductions do not change state
Determinism: Reduction produces identical output for identical input across all replicas
No HashMap iteration: Uses BTreeMap for deterministic ordering
No system time: Uses OrderTime tokens for ordering
No floating point: All arithmetic is exact

These invariants guarantee correct distributed behavior. They also support offline operation with eventual consistency. They form the foundation for Aura's account and relational context state machines.

13. Fact Validation Pipeline

Every fact inserted into a journal must be validated before merge. The following steps outline the required checks and the effect traits responsible for each fact type:

13.1 AttestedOp Facts

Checks

Verify the threshold signature (agg_sig) using the two-phase verification model from aura-core::tree::verification:
- verify_attested_op(): Cryptographic signature check against BranchSigningKey stored in TreeState
- check_attested_op(): Full verification plus state consistency (epoch, parent commitment)
Ensure the referenced parent state exists locally. Otherwise request missing facts.
Confirm the operation is well-formed (e.g., AddLeaf indexes a valid parent node).

See Tree Operation Verification for details on the verify/check model and binding message security.

Responsible Effects

CryptoEffects for FROST signature verification via verify_attested_op().
JournalEffects for parent lookup, state consistency via check_attested_op(), and conflict detection.
StorageEffects to persist the fact once validated.

13.2 Relational Facts

Checks

Validate that each authority commitment referenced in the fact matches the current reduced state (AuthorityState::root_commitment).
Verify Aura Consensus proofs if present (guardian bindings, recovery grants).
Enforce application-specific invariants (e.g., no duplicate guardian bindings).

Responsible Effects

AuthorizationEffects / RelationalEffects for context membership checks.
CryptoEffects for consensus proof verification.
JournalEffects for context-specific merge.

13.3 FlowBudget Facts

Checks

Ensure spent deltas are non-negative and reference the active epoch for the (ContextId, peer) pair.
Reject facts that would decrease the recorded spent (monotone requirement).
Validate receipt signatures associated with the charge (see 111_transport_and_information_flow.md).

Responsible Effects

FlowBudgetEffects (or FlowGuard) produce the fact and enforce monotonicity before inserting.
JournalEffects gate insertion to prevent stale epochs from updating headroom.

13.4 Snapshot Facts

Checks

Confirm the snapshot state_hash matches the hash of all facts below the snapshot.
Ensure no newer snapshot already exists for the namespace (check sequence number).
Verify that pruning according to the snapshot does not remove facts still referenced by receipts or pending consensus operations.

Responsible Effects

JournalEffects compute and validate snapshot digests.
StorageEffects persist the snapshot atomically with pruning metadata.

By clearly separating validation responsibilities, runtime authors know which effect handlers must participate before a fact mutation is committed. This structure keeps fact semantics consistent across authorities and contexts.

14. Consistency Metadata Schema

Facts carry consistency metadata for tracking agreement level, propagation status, and acknowledgments. See Operation Categories for the full consistency metadata type definitions.

14.1 Fact Schema Fields

The base Fact structure (section 2) is extended with consistency metadata fields (added via serde defaults for backwards compatibility):

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.

Keyboard shortcuts

Aura