Test Infrastructure Reference

This document describes the architecture of aura-testkit, the test infrastructure crate that provides fixtures, mock handlers, and verification utilities for testing Aura protocols.

Overview

The aura-testkit crate occupies Layer 8 in the Aura architecture. It provides reusable test infrastructure without containing production code. All test utilities follow effect system guidelines to ensure deterministic execution.

The crate serves three purposes. It provides stateful effect handlers for controllable test environments. It offers fixture builders for consistent test setup. It includes verification utilities for property testing and differential testing.

Complete-flow fixture contract

Reusable fixtures support deterministic execution of the actual runtime and app workflow. Generic providers, fault controls and evidence utilities belong in aura-testkit; runtime-specific assembly belongs in sanctioned runtime test support or simulation factories. Testkit utilities do not introduce upward production dependencies or a second implementation of a protocol.

Positive evidence comes from canonical producers: real signing and verification, explicit transferred trust, committed journal state, acknowledged storage and actual owned task disposal. MockRuntimeBridge projections and mock crypto remain useful for component tests, but cannot establish authenticated distributed success or profile restart continuity.

A complete lifecycle fixture retains participant identity, selected clock/provider, original operation and window ownership, storage profile and typed failure sources across its stages. Restart requires acknowledged old-owner shutdown and reacquisition of the same original profile, with durable evidence revalidated. Scenario checkpoints and copied metadata cannot substitute for that custody. Fault and replay evidence distinguishes actual runtime execution from observational model steps.

Failure after partial assembly or issuance still requires acknowledged cleanup of every acquired runtime owner. Dropping a fixture is not shutdown evidence. Cleanup preserves the original concrete failure and reports any required cleanup failure separately; it cannot manufacture a cancellation or successful terminal receipt.

Enrollment is the first complete-flow fixture target; its implementation and migration remain explicit work until actual execution covers setup, issuance, acceptance/rejection, host persistence, terminal publication, cleanup and reopen. Simulation Guide defines the development workflow and coverage sequence.

Reusable lifecycle support

A reusable fixture exposes deterministic fault boundaries and retains the original owners through failure and cleanup. Its observations distinguish domain outcome, persistence acknowledgment, semantic terminal publication and required resource disposal. Failure in one stage cannot manufacture evidence for another. Participant setup and restart custody are shared infrastructure, rather than independently reconstructed state in each regression. Platform-specific storage and network behavior remain separately identified coverage requirements.

Fixture coverage identity

Fixture evidence identifies the original participants, operation, selected providers and durable profile, together with the supported lifecycle stages. Required host persistence names the actual storage producer: a generic callback write does not establish native or browser identity persistence. Unsupported stages remain explicit dependencies rather than implied fixture capabilities.

Stateful Effect Handlers

Stateful effect handlers maintain internal state across calls. They enable deterministic testing by controlling time, randomness, and storage. These handlers implement the same traits as production handlers but store state for inspection and manipulation.

Handler Categories

The stateful_effects module provides handlers for each effect category.

Time Handler

The SimulatedTimeHandler provides controllable time for tests.

#![allow(unused)]
fn main() {
use aura_testkit::stateful_effects::SimulatedTimeHandler;
use aura_core::effects::PhysicalTimeEffects;

let time = SimulatedTimeHandler::new_with_time(5_000);
let now = time.physical_time().await?;
time.advance_time(5000);
let later = time.physical_time().await?;
}

The existing new() constructor starts at current system time; deterministic fixtures select new_at_epoch() or new_with_time(start_ms) explicitly. Concurrent runtime fixtures instead retain ManualPhysicalClock for exact fault boundaries or a shared QuiescentClock with paused Tokio time. Clock reads never provide distributed ordering authority, and provider sleep semantics must not silently advance another owner's deadline. See Testing Guide for runtime assembly and restart contracts.

Random Handler

The MockRandomHandler provides seeded randomness for reproducible tests.

#![allow(unused)]
fn main() {
use aura_testkit::stateful_effects::MockRandomHandler;

let random = MockRandomHandler::with_seed(42);
let bytes = random.random_bytes(32).await;
}

Given the same seed, this handler produces identical sequences across runs. This enables deterministic property testing and failure reproduction.

Fixture System

The fixture system provides consistent test environment setup. Fixtures encapsulate common configuration patterns and reduce boilerplate.

TestFixture

The TestFixture type provides a complete test environment.

#![allow(unused)]
fn main() {
use aura_testkit::infrastructure::harness::{TestFixture, TestConfig};

let fixture = TestFixture::new().await?;
let device_id = fixture.device_id();
let context = fixture.context();
}

A fixture creates deterministic identifiers, initializes effect handlers, and provides access to test context. The default configuration suits most unit tests.

TestConfig

Custom configurations enable specialized test scenarios.

#![allow(unused)]
fn main() {
let config = TestConfig {
    name: "threshold_test".to_string(),
    deterministic_time: true,
    capture_effects: true,
    timeout: Some(Duration::from_secs(60)),
};
let fixture = TestFixture::with_config(config).await?;
}

The deterministic_time flag enables StatefulTimeHandler. The capture_effects flag records effect calls for later inspection.

Builder Utilities

Builder functions create test data with deterministic inputs. They live in the builders module.

Account Builders

#![allow(unused)]
fn main() {
use aura_testkit::builders::test_account_with_seed;

let account = test_account_with_seed(42).await;
}

This creates an account with deterministic keys derived from the seed. Multiple calls with the same seed produce identical accounts.

Key Builders

#![allow(unused)]
fn main() {
use aura_testkit::builders::test_key_pair;

let (signing_key, verifying_key) = test_key_pair(1337);
}

Key pairs derive from the provided seed. This enables testing signature verification with known keys.

Identifier Generation

Tests must use deterministic identifiers to ensure reproducibility.

#![allow(unused)]
fn main() {
use aura_core::types::identifiers::AuthorityId;

let auth1 = AuthorityId::from_entropy([1u8; 32]);
let auth2 = AuthorityId::from_entropy([2u8; 32]);
}

Never use Uuid::new_v4() or similar entropy-consuming methods in tests. Incrementing byte patterns create distinct but reproducible identifiers.

Verification Utilities

The verification module provides utilities for property testing and differential testing.

Proptest Strategies

The strategies module defines proptest strategies for Aura types.

#![allow(unused)]
fn main() {
use aura_testkit::verification::strategies::{arb_device_id, arb_account_id, arb_key_pair};
use proptest::prelude::*;

proptest! {
    #[test]
    fn device_id_deterministic(id in arb_device_id()) {
        assert_ne!(id.to_string(), "");
    }

    #[test]
    fn key_pair_valid((sk, vk) in arb_key_pair()) {
        assert_eq!(sk.verifying_key(), vk);
    }
}
}

Available strategies include arb_device_id, arb_account_id, arb_session_id, and arb_key_pair. These generate valid, deterministic instances for property testing.

Lean Oracle

The lean_oracle module provides integration with Lean theorem proofs.

#![allow(unused)]
fn main() {
use aura_testkit::verification::lean_oracle::LeanOracle;

let oracle = LeanOracle::new()?;
let result = oracle.verify_journal_merge(&state1, &state2)?;
}

The oracle invokes compiled Lean code to verify properties. This enables differential testing against proven implementations.

Capability Soundness

The capability_soundness module provides formal verification for capability system properties.

#![allow(unused)]
fn main() {
use aura_testkit::verification::capability_soundness::{
    CapabilitySoundnessVerifier, SoundnessProperty, CapabilityState
};

let mut verifier = CapabilitySoundnessVerifier::with_defaults();
let result = verifier.verify_property(
    SoundnessProperty::NonInterference,
    initial_state
).await?;
assert!(result.holds);
}

The verifier checks five soundness properties: NonInterference, Monotonicity, TemporalConsistency, ContextIsolation, and AuthorizationSoundness. Use verify_all_properties to check all properties at once.

Consensus Testing

The consensus module provides infrastructure for consensus protocol testing.

ITF Loader

The itf_loader module loads ITF traces for replay testing.

#![allow(unused)]
fn main() {
use aura_testkit::consensus::itf_loader::ITFLoader;

let trace = ITFLoader::load("artifacts/traces/consensus_happy_path.itf.json")?;
for state in trace.states {
    // Verify state against implementation
}
}

ITF traces come from Quint model checking. The loader parses them into Rust types for conformance testing.

Reference Implementation

The reference module provides a minimal consensus implementation for differential testing.

#![allow(unused)]
fn main() {
use aura_testkit::consensus::reference::ReferenceConsensus;

let reference = ReferenceConsensus::new(config);
let expected = reference.process_vote(vote)?;
let actual = production_consensus.process_vote(vote)?;
assert_eq!(expected.outcome, actual.outcome);
}

The reference implementation prioritizes clarity over performance. It serves as a specification against which production code is tested.

Mock Runtime Bridge

The MockRuntimeBridge simulates the runtime environment for TUI testing.

#![allow(unused)]
fn main() {
use aura_testkit::mock_runtime_bridge::MockRuntimeBridge;

let bridge = MockRuntimeBridge::new();
bridge.inject_chat_update(chat_state);
bridge.inject_contact_update(contacts);
}

This bridge injects signals that would normally come from the reactive pipeline. It enables testing TUI state machines without a full runtime.

Conformance Framework

The conformance module provides artifact validation for native/WASM parity testing.

Artifact Format

The AuraConformanceArtifactV1 captures execution state for comparison. The type is defined in aura_core::conformance:

#![allow(unused)]
fn main() {
use aura_core::{AuraConformanceArtifactV1, AuraConformanceRunMetadataV1, ConformanceSurfaceName};

let mut artifact = AuraConformanceArtifactV1::new(AuraConformanceRunMetadataV1 {
    target: "native".to_string(),
    profile: "native_coop".to_string(),
    scenario: "test_scenario".to_string(),
    seed: Some(42),
    commit: None,
    async_host_transcript_entries: None,
    async_host_transcript_digest_hex: None,
});

// Insert required surfaces
artifact.insert_surface(ConformanceSurfaceName::Observable, observable_surface);
artifact.insert_surface(ConformanceSurfaceName::SchedulerStep, scheduler_surface);
artifact.insert_surface(ConformanceSurfaceName::Effect, effect_surface);

artifact.validate_required_surfaces()?;
}

Every conformance artifact must capture three surfaces:

Missing surfaces cause validation failure.

Metadata aids debugging but does not affect comparison:

#![allow(unused)]
fn main() {
pub struct AuraConformanceRunMetadataV1 {
    pub target: String,
    pub profile: String,
    pub scenario: String,
    pub seed: Option<u64>,
    pub commit: Option<String>,
    pub async_host_transcript_entries: Option<u64>,
    pub async_host_transcript_digest_hex: Option<String>,
}
}

Effect Envelope Classification

Each effect kind has a comparison class that determines how differences are evaluated:

The strict class requires exact matches. The commutative class normalizes order before comparison. The algebraic class applies domain-specific reduction before comparison.

New effect kinds must be classified before use:

#![allow(unused)]
fn main() {
use aura_core::conformance::AURA_EFFECT_ENVELOPE_CLASSIFICATIONS;

AURA_EFFECT_ENVELOPE_CLASSIFICATIONS.insert(
    "new_effect_kind",
    ComparisonClass::Strict,
);

aura_core::assert_effect_kinds_classified(&effect_trace)?;
}

Unclassified effect kinds cause conformance checks to fail.

Module Structure

aura-testkit/
├── src/
│   ├── builders/           # Test data builders
│   ├── configuration/      # Test configuration
│   ├── consensus/          # Consensus testing utilities
│   ├── conformance.rs      # Conformance artifact support
│   ├── differential.rs     # Differential testing
│   ├── fixtures/           # Reusable test fixtures
│   ├── foundation.rs       # Core test utilities
│   ├── handlers/           # Mock effect handlers
│   ├── infrastructure/     # Test harness infrastructure
│   ├── mock_effects.rs     # Simple mock implementations
│   ├── stateful_effects/   # Stateful effect handlers
│   └── verification/       # Property testing utilities
├── tests/                  # Integration tests
└── benches/                # Performance benchmarks

Related Documentation

See Testing Guide for how to write tests using this infrastructure. See Effect System for effect trait definitions.