Skip to content

testing.md

Latest commit

 

History

History
282 lines (236 loc) · 14.8 KB

testing.md

File metadata and controls

282 lines (236 loc) · 14.8 KB
Raw

Testing Doctrine

This document is the source-backed testing doctrine for Minimmit. It preserves research lessons that are useful for the project without turning AGENTS.md, skills, or assurance ledgers into long research notes.

crates/core/assurance.yaml remains the claim and evidence ledger. It should not carry testing roadmaps, source surveys, or confidence essays.

Current Doctrine

The preferred Minimmit testing loop is:

paper claim -> explicit input -> core step -> semantic effect -> trace/replay -> evidence

Use the smallest deterministic test that gives useful confidence. For current minimmit-core work, this usually means pure Rust tests over typed protocol values. Once the deterministic core exposes an input boundary, protocol scenario tests should drive that boundary directly.

When a core output depends on shell work becoming durable before release, tests should assert the protocol-visible ready outputs and the shell ordering contract. Add a core-visible shell completion input only when completion must change later core behavior. See Core And Shell Boundary for the core/shell boundary.

When sync, store, simulation, or shell work models overload, tests should assert bounded degradation through deterministic observations. See Bounded Degradation for overload vocabulary and testing implications.

Each test should protect behavior that Minimmit owns: protocol obligations, project policy, validation, state transitions, or observable semantic output. Do not add, move, or preserve tests whose failure would primarily report a change in language, library, dependency, derived, or otherwise mechanical behavior rather than a change in Minimmit behavior.

Readable Tests

Tests should read as concrete protocol stories. Keep the relevant setup, transition, and assertion visible when they are short.

Structure non-trivial input-step and scenario tests as Given / When / Then, the behavior-focused form of Arrange / Act / Assert. Use section comments when the phases are not obvious from blank lines alone. Given should set up concrete protocol state, When should drive the event or transition under test, and Then should assert semantic output or selected post-state.

Use helpers for meaningful domain fixtures that would otherwise distract from the behavior under test. Do not wrap scalar construction or simple assertions in test-only helpers; use direct public constructors such as BlockId::new, ViewNumber::new, ValidatorId::new, and TransactionId::new at the call site.

Names should spell out the protocol relation that matters. Avoid vague relative or policy-heavy names when a simpler name can identify membership, view, parent, signer, persistence, or ordering relationships directly. Literal expected values should be understandable from the test name, local variables, or a short intent comment; unexplained lists of numbers are not useful evidence.

Comments in tests should explain protocol intent, fixture relationships, deliberate ordering, or regression risk that names and assertions do not make obvious. Prefer clearer names or structure first, and do not add comments that only restate assertions or obvious control flow.

State-Fact Transition Matrix

Protocol PRs that change processor state, events, validation, or Ready outputs should name the protocol state facts they touch before implementation. For each fact, include a small state-fact transition matrix in the test, nearby protocol documentation, or PR text:

  • fact name in protocol vocabulary
  • paper claim or explicit evidence gap
  • events that establish the fact
  • events that must not establish the fact
  • later events that depend on the fact
  • event that resets the fact, or the explicit reset evidence gap
  • executable evidence that covers the cross-event path

Name facts by their protocol meaning, not by private storage. For example, proposed_current_view is an implementation detail for the fact that the local leader's current-view proposal slot is consumed. Matrix evidence should drive real Event -> Processor -> Ready transitions and assert public semantic effects such as ready output, observed artifacts, view, or selected post-state.

Test Layers

  • Small claim tests are the default. They cover thresholds, typed construction, duplicate rejection, distinct sender counting, deterministic ordering, and precise errors.
  • Input-step tests should drive one explicit protocol event through the core and inspect the returned protocol-visible output.
  • Scenario tests should feed a short ordered input trace, record step outcomes, and assert a named protocol story.
  • Overload scenario tests should assert public deterministic observations such as admission, rejection, expiry, queue age, or tracked-state pressure, not private queue internals.
  • Replay fixtures should be added only after scenario shape stabilizes. A replayed failure must include enough metadata to reproduce it exactly.
  • Model conformance should map named model actions into Rust events and compare a small semantic projection, not every transient implementation field.
  • Bounded event search should come after local scenario tests are useful. Start with seeded shuffle or small exhaustive event bags before richer scheduling.

Only input-step and scenario testing are active Codex skill guidance for now. Replay fixtures, property packs, model conformance, and bounded search should get separate skills when the implementation reaches those layers.

Properties

Use two property classes:

  • always: safety properties. A violation is a candidate bug when the property is high-level, protocol-meaningful, and independently confirmable.
  • sometimes: reachability or coverage signals. Reaching one shows the harness exercised useful protocol territory, but does not prove correctness.

Good always properties for Minimmit should be stated over protocol facts such as notarization, nullification, finalization, view progression, signer membership, and distinct sender counting. Avoid primary bug oracles based on private buffers, queue depths, scheduler internals, or implementation-specific interpretation.

Good sometimes properties include observing an M-notarization, L-notarization, nullification, higher view, non-genesis finalization, timeout path, or rejected conflicting evidence.

When the implementation reaches property-pack testing, keep the first pack small, high-level, and confirmable. always properties should be the only bug threshold. sometimes properties should stay coverage signals.

Replay Metadata

Any randomized, scheduled, or searched run that reports a candidate must record:

  • scenario family or test name
  • ordered input trace, or enough scheduler data to reconstruct it
  • seed when randomness is used
  • scheduler name and version when scheduling is used
  • triggered always properties
  • reached sometimes properties
  • implementation commit when the result leaves a local test failure report

Unreplayable failures are not acceptable evidence.

Start replay and search work with short explicit traces. Move next to seeded shuffle or small exhaustive event bags. Richer scheduling, broad simulation, chaos, Antithesis integration, Jepsen-style external testing, and VOPR-style infrastructure should wait until local Event -> Processor -> Ready scenarios prove the need.

For Quint or model conformance, map named model actions into Rust events at a protocol-local boundary. Compare semantic projected state, not every transient implementation field. Do not count model-only checks as Rust implementation evidence unless the trace drives Rust behavior.

Apply Now

  • Keep minimmit-core deterministic and free of hidden IO, wall-clock time, randomness, async scheduling, networking, storage engines, and production shell behavior.
  • Represent shell ordering through explicit ready outputs. Add core-visible shell completion input only when completion must change later core behavior.
  • Assert persist-before-broadcast behavior through protocol-visible outputs, not DB mechanics or shell queues.
  • Assert bounded degradation through explicit observations when overload policy belongs to the crate under test.
  • Prefer behavior tests through public APIs and protocol-facing outputs.
  • Keep tests readable and actionable from the test name plus assertion output.
  • Remove mechanical coverage instead of relocating it when cleanup scope permits.
  • Let crates/core/assurance.yaml drive protocol test priority.
  • Add or update a state-fact transition matrix when protocol state, events, validation, or ready outputs change.
  • Treat model-only checks as design evidence unless they are connected to Rust behavior.
  • Use explicit evidence gaps rather than implying coverage from partial tests.

Defer

Do not add these until the local Event -> Processor -> Ready shape and scenario tests justify them:

  • broad simulation or chaos framework
  • Antithesis integration
  • Jepsen-style external system testing
  • full TigerBeetle VOPR-style infrastructure
  • generic deterministic runtime
  • coverage gates or flake dashboards
  • broad property-test or fuzz dependencies in minimmit-core

Source Map

Google testing:

Private protocol-event research:

Model-based and system testing: