From f1f98e9f7db33ccf5d518af66f47497e20f58bc9 Mon Sep 17 00:00:00 2001 From: Zachery Aaron Shores-Chmielewski Date: Fri, 22 May 2026 08:08:01 +0000 Subject: [PATCH] spec: add behavioral test subsections to SIM_SPEC.md MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. Signed-off-by: Zachery Aaron Shores-Chmielewski --- .../pipeline-parallel-inference/SIM_SPEC.md | 225 ++++++++++++++++++ 1 file changed, 225 insertions(+) diff --git a/examples/pipeline-parallel-inference/SIM_SPEC.md b/examples/pipeline-parallel-inference/SIM_SPEC.md index b06174d..c9ef587 100644 --- a/examples/pipeline-parallel-inference/SIM_SPEC.md +++ b/examples/pipeline-parallel-inference/SIM_SPEC.md @@ -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//.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