spec: add behavioral test subsections to SIM_SPEC.md
Six per-component property-test subsections (§4.10 engine, §5.8 network, §6.4 hosting, §8.4 scenario loader, §9.6 bundle writer, §10.5 assertion evaluator) written in property-language form. Each names the property the component must have; how the property is verified is the test author's call. These were drafted in conversation but never committed, causing the boundary check to flag SIM_SPEC.md on iteration 1 of the implementation loop. Committing now puts them at HEAD so future loop iterations diff cleanly. Authored by Claude, lovingly guided by Zachery Aaron Shores-Chmielewski
This commit is contained in:
parent
6df2943920
commit
98ad5e3370
1 changed files with 225 additions and 0 deletions
|
|
@ -392,6 +392,53 @@ The engine's virtual clock is in integer nanoseconds. The manifest records
|
|||
the unit so post-processors render times consistently. Sub-nanosecond
|
||||
ordering is not modelled.
|
||||
|
||||
### 4.10 Behavioral tests
|
||||
|
||||
The engine's contract is the dispatch and action-processing behaviour of
|
||||
§4. Its tests assert that it has the properties below; how each is
|
||||
verified is the test author's call.
|
||||
|
||||
**Tick cadence.** Each host receives ticks at its declared period,
|
||||
starting at a stable seed-derived offset. The offset is identical
|
||||
across runs and differs across hosts in the same scenario.
|
||||
|
||||
**Action ordering.** A host's emitted actions are processed in returned
|
||||
order. The effects of action N are fully observable before action N+1's
|
||||
effects begin.
|
||||
|
||||
**Send semantics.** A `Send` whose network query returns `Arrive` results
|
||||
in the recipient's `recv` being called at the returned arrival time with
|
||||
the codec-produced bytes. A `Send` the network drops results in the
|
||||
sender's `recv` being called with `SendFailed`, a `DropOnSend` record in
|
||||
the bundle, and no recipient call.
|
||||
|
||||
**Timer fidelity.** A `ScheduleTimer { at_ns, token }` causes a
|
||||
`TimerFired(token)` envelope to reach the host's `recv` at exactly
|
||||
`at_ns`.
|
||||
|
||||
**Halt.** A halted host receives no further ticks; it continues to
|
||||
receive deliveries.
|
||||
|
||||
**Closed action set.** An action outside the closed set §4.6 names
|
||||
aborts the run with a structured error. The engine never silently
|
||||
ignores or invents an action.
|
||||
|
||||
**Tie-break.** Events scheduled at the same virtual time pop in enqueue
|
||||
order. The order is identical across runs and architectures.
|
||||
|
||||
**Mutation propagation.** Deliveries the network invalidates are removed
|
||||
from the engine's queue; each emits a `DropOnDelivery` record at the
|
||||
mutation's virtual time. No invalidated delivery reaches a host's `recv`.
|
||||
|
||||
**Snapshot fanout.** A scheduled snapshot produces exactly one record
|
||||
per live host at the scheduled virtual time.
|
||||
|
||||
**Early termination is clean.** Every record emitted before the
|
||||
termination time is preserved; no record carries a later virtual time.
|
||||
|
||||
**Determinism.** Same scenario, same seed ⇒ byte-identical
|
||||
`events.ndjson`.
|
||||
|
||||
---
|
||||
|
||||
## 5. The network
|
||||
|
|
@ -506,6 +553,66 @@ style backpressure, NAT state, or inter-peer clock skew. These limits are
|
|||
named in the known-gaps document and re-entered when an algorithm under
|
||||
test is sensitive to them.
|
||||
|
||||
### 5.8 Behavioral tests
|
||||
|
||||
The network is a pure function of (state, query). Its tests assert that
|
||||
it has the properties §5 names; how each property is verified is the
|
||||
test author's call.
|
||||
|
||||
**Reachability.** A `send` over an ordered pair returns `Arrive` iff
|
||||
that pair is declared as an edge and the active partition set does not
|
||||
cut it. A `send` the network refuses leaves the network's state
|
||||
unchanged.
|
||||
|
||||
**Partition heals to identity.** A `Partition` followed by a `Heal` at
|
||||
later virtual times leaves the network indistinguishable on subsequent
|
||||
sends from one that experienced neither.
|
||||
|
||||
**Mutation invalidation is exact.** Every delivery a mutation renders
|
||||
impossible appears in the mutation's invalidated-deliveries return. No
|
||||
delivery the mutation does not invalidate appears in that return.
|
||||
|
||||
**Loss is Bernoulli.** Drops on a link are independent draws with the
|
||||
link's declared probability. A `LossBurst` substitutes its override
|
||||
probability for the duration it names and only the duration it names.
|
||||
|
||||
**Bandwidth serializes.** A link with finite bandwidth never overlaps
|
||||
two messages' wire-occupancy intervals: each message's arrival is
|
||||
delayed at least until the previous message's arrival plus that
|
||||
message's transmission time.
|
||||
|
||||
**Latency is additive.** A send's arrival decomposes into base latency,
|
||||
serialization delay, jitter, cold-dial penalty when applicable, and the
|
||||
contributions of active mutations. The terms are independent in the
|
||||
policy and combine without interaction beyond what §5.4 specifies.
|
||||
|
||||
**Jitter is symmetric and integer-valued.** Jitter samples come from
|
||||
the precomputed table of §7, are symmetric around zero, and are never
|
||||
non-integer.
|
||||
|
||||
**Cache state follows traffic.** The link's `cache_state` reflects
|
||||
recent traffic: warm after sufficient activity, cold again after
|
||||
sufficient idleness, with the thresholds the policy names. The
|
||||
cold-dial penalty is paid by exactly the sends the network classifies
|
||||
cold.
|
||||
|
||||
**Cache transitions are observable.** Every cold↔warm transition emits
|
||||
exactly one `CacheStateChange` notification at the transition's virtual
|
||||
time. No transition is silent and no notification fires without a
|
||||
transition.
|
||||
|
||||
**Mutation scoping.** A mutation affects exactly the links its `links`
|
||||
field names and exactly the duration it declares. Sends on other links,
|
||||
or on the named links outside the duration, are unaffected.
|
||||
|
||||
**Substream isolation.** Editing one link's policy does not change any
|
||||
draw the network makes on any other link. This is the property that
|
||||
makes bisecting scenario edits possible.
|
||||
|
||||
**Determinism.** Same topology, same seed, same query sequence ⇒
|
||||
identical `SendOutcome` sequence and identical invalidated-deliveries
|
||||
returns.
|
||||
|
||||
---
|
||||
|
||||
## 6. Hosting an entity
|
||||
|
|
@ -570,6 +677,38 @@ Existing host kinds continue to work without change. The network, the
|
|||
bundle writer, the engine main loop, and the determinism contract are
|
||||
host-kind-agnostic.
|
||||
|
||||
### 6.4 Behavioral tests
|
||||
|
||||
Host-kind tests come in two layers: kind-agnostic properties every
|
||||
registered kind must satisfy, and per-kind properties specific to the
|
||||
algorithm a kind hosts. The list below is what the tests must assert;
|
||||
how is the test author's call.
|
||||
|
||||
**Trait conformance (every kind).** The kind exposes the §6.1 surface
|
||||
with the §6.1 signatures. `kind_tag()` is a non-empty string unique
|
||||
among registered kinds.
|
||||
|
||||
**Codec is invertible (every kind).** Encoding then decoding a message
|
||||
is the identity on the kind's message type.
|
||||
|
||||
**Host determinism (every kind).** Same `HostKindConfig`, same RNG
|
||||
seed, same `tick`/`recv` sequence ⇒ identical action sequence.
|
||||
|
||||
**SWIM emits no novel kinds.** Every event a SWIM host emits is of a
|
||||
kind production's diagnostics also emits. The simulator invents no SWIM
|
||||
event kind for itself.
|
||||
|
||||
**SWIM codec parity with production.** The SWIM host's encoding of an
|
||||
outgoing message is byte-identical to the production transport's
|
||||
encoding of the same message. Drift breaks the build.
|
||||
|
||||
**SWIM snapshot parity with production.** A SWIM host's `snapshot()`
|
||||
conforms to the production tier-2 SWIM-state schema.
|
||||
|
||||
**SWIM unknown-output is loud.** A production state-machine output the
|
||||
SWIM adapter does not route aborts the run with a structured error.
|
||||
Silent fallback is a test failure.
|
||||
|
||||
---
|
||||
|
||||
## 7. Determinism
|
||||
|
|
@ -729,6 +868,34 @@ Every scenario carries a top-of-file prose comment naming what it
|
|||
reproduces, the expected verdict (pass-now / fail-until-fix /
|
||||
sensitivity-study), and any base scenario it extends.
|
||||
|
||||
### 8.4 Behavioral tests
|
||||
|
||||
The loader's contract is the schema and validation rules of §8. Its
|
||||
tests assert that it has the properties below.
|
||||
|
||||
**Examples are well-formed.** Every shipped example scenario parses
|
||||
and satisfies every rule in §8.2.
|
||||
|
||||
**Parse is invertible.** Parsing, re-emitting to TOML, and re-parsing
|
||||
is the identity on scenario values.
|
||||
|
||||
**Validation is complete.** Every rule §8.2 names is enforced. A
|
||||
scenario violating any rule is rejected; a scenario violating none is
|
||||
accepted.
|
||||
|
||||
**Errors are structured.** A rejection names the file, the offending
|
||||
field, and the violated rule in one line each. Generic errors are a
|
||||
test failure.
|
||||
|
||||
**Host-kind validation is delegated.** A host-kind-config error
|
||||
surfaces the kind's own rule, not a loader-generic one.
|
||||
|
||||
**Merge is leaves-override, lists-append.** Extending a base scenario
|
||||
replaces leaf values and appends list entries, with no other effect.
|
||||
|
||||
**Loading is pure.** Loading the same file twice produces equal values
|
||||
and performs no filesystem writes.
|
||||
|
||||
---
|
||||
|
||||
## 9. The bundle
|
||||
|
|
@ -806,6 +973,35 @@ the renderer requires inputs the simulator does not have (collector-side
|
|||
receive timestamps, for instance), the simulator substitutes the virtual-
|
||||
clock equivalent and records the substitution in the manifest.
|
||||
|
||||
### 9.6 Behavioral tests
|
||||
|
||||
The writer's contract is the layout and schema of §9. Its tests assert
|
||||
that it has the properties below.
|
||||
|
||||
**Layout.** Every produced bundle has the §9.1 entries. (`verdicts.json`
|
||||
is the assertion evaluator's responsibility; §10.5.)
|
||||
|
||||
**Envelope conformance.** Every line of `events.ndjson` is valid JSON
|
||||
conforming to the §9.2 envelope shape.
|
||||
|
||||
**Hash integrity.** Every manifest-recorded hash equals the actual hash
|
||||
of the file it names.
|
||||
|
||||
**Snapshot organization.** Each `SnapshotRecord` corresponds to exactly
|
||||
one file at `snapshots/<host_id>/<snapshot_seq>.json`. Sequence numbers
|
||||
are monotonically increasing per host from zero.
|
||||
|
||||
**Ordering is deterministic and documented.** Identical record streams
|
||||
produce byte-identical bundles. The ordering rule is named in §9 and the
|
||||
writer obeys it.
|
||||
|
||||
**Arrival-order independence.** Records may arrive in any order; the
|
||||
produced bundle depends only on the multiset of records and the
|
||||
documented ordering rule, not on arrival order.
|
||||
|
||||
**Idempotency.** Writing the same record stream to a fresh output path
|
||||
twice produces byte-identical bundles.
|
||||
|
||||
---
|
||||
|
||||
## 10. Assertions
|
||||
|
|
@ -889,6 +1085,35 @@ are determinable from the prefix. The engine polls this side after each
|
|||
event dispatch. The streaming side is an optimization; the post-run side
|
||||
remains the authoritative source for `verdicts.json`.
|
||||
|
||||
### 10.5 Behavioral tests
|
||||
|
||||
The evaluator's contract is the assertion catalog of §10.1, the verdict
|
||||
shape of §10.2, and the streaming side of §10.4. Its tests assert that
|
||||
it has the properties below.
|
||||
|
||||
**Per-kind soundness.** For every kind in §10.1: `Pass` is returned
|
||||
exactly when the kind's stated condition holds over the bundle; `Fail`
|
||||
exactly when the condition is violated; `Inconclusive` exactly when the
|
||||
preconditions did not fire.
|
||||
|
||||
**Verdict shape.** Every verdict conforms to §10.2. `Fail` verdicts
|
||||
carry evidence referencing the event or snapshot responsible.
|
||||
|
||||
**Verdict order is scenario-declared.** `verdicts.json` lists verdicts
|
||||
in the order the scenario declared the corresponding assertions.
|
||||
|
||||
**Streaming agrees with post-run.** On any bundle, the streaming side
|
||||
either does not resolve or resolves to the same verdict the post-run
|
||||
side will return. The two are never inconsistent.
|
||||
|
||||
**Streaming resolves as early as possible.** When a verdict is
|
||||
determinable from a prefix, the streaming side resolves no later than
|
||||
the end of that prefix.
|
||||
|
||||
**Property failures replay exactly.** A library-property failure
|
||||
recorded with seed S, replayed with seed S, produces the identical
|
||||
scenario and the identical `Fail` verdict.
|
||||
|
||||
---
|
||||
|
||||
## 11. Calibration
|
||||
|
|
|
|||
Loading…
Reference in a new issue