deterministic-replay — immutable facts, reproducible state

The rule:

Nondeterminism may propose state; only deterministic mechanisms commit state.

Required transition model

Define a pure semantic function:

Transition(previous_state, canonical_record) -> next_state

Given identical prior committed state and identical canonical input, the result must not depend on:

• wall-clock time
• scheduler timing
• CPU/core placement
• agent/model randomness
• retry timing
• unordered map iteration
• process-local hidden state

Immutability

Committed records never mutate.

A correction is another committed record.

Mutable current-state views must be reconstructable from immutable committed facts.

Deterministic recovery

Target:

checkpoint
+ immutable committed suffix
-> current canonical state

Full replay and checkpoint+suffix replay must converge.

Canonical encoding

Before hashing, signing, comparing, or storing a persistent record, specify:

• schema/version
• fixed field order
• exact integer widths
• endianness
• string/Unicode normalization
• optional/default-field representation
• byte/string encoding
• hash domain separation

Never persist/hash compiler-native structure layout.

Do not rely on ordinary unordered JSON serialization.

JS executable model

For tiny persistence/state-machine work, prefer exhaustive exploration before random fuzzing.

Model semantic states, not transistor/cache internals.

Useful abstract states:

PROPOSED
COHERENT_VISIBLE
DEVICE_COMPLETE
PERSISTENT
TRUSTED_COMPLETE

Enumerate actions such as:

submit
duplicate_submit
durable_ack
publish_completion
reset
recover
replay_old_epoch

Explore all reachable action sequences to a useful depth and retain counterexamples as regression fixtures.

Assertions

At minimum:

CommittedRecordNeverMutates
SameStateAndInputImpliesSameNextState
ReplayOfCommittedPrefixIsDeterministic
CheckpointPlusSuffixEqualsFullReplay
CompletionImpliesPersistent
RecoveryDoesNotCreateCommit
DuplicateRequestCommitsAtMostOnce
CanonicalRecordHashIsStable

Scheduling

Do NOT require deterministic scheduling by default.

Require deterministic outcome semantics:

same ordered committed facts
-> same reconstructed state

Formal-to-hardware ladder

semantic model
-> TLA+/PlusCal model check
-> JS executable oracle
-> RTL
-> SVA/SymbiYosys
-> FPGA differential traces
-> ASIC only after evidence

JS and RTL should consume the same trace fixtures whenever possible.

Trusted-head experiment

Prefer testing whether hardware can retain only:

(epoch, last_tid, root_hash)

while immutable history remains external.

Canonical references

• docs/CONSTRAINTS.md
• scaffolds/durable-tid/docs/FORMAL.md
• scaffolds/durable-tid/docs/DESIGN.md
• rfcs/0005-formal-verification-before-rtl.md