Scenario testing (DVM-SL)

world names engine, peers, roles, threshold, setup, key, lane, aggregator, and mobile parties. score selects an existing debugger scenario. hooks injects network faults and intercepts local runtime calls at named sites. run drives deterministic execution with step counts, breakpoints, restart, and reconnect directives. expect binds assertions to lifecycle fields, artifacts, evidence, instruction-site state, publication status, and mobile binding. formal attaches the K family, mode, checks, negatives, and compare axes.

The canonical IR (ScenarioDoc) is the shared representation that native lowering, K lowering, structured reports, and customer review snapshots all consume from the same parsed source. Product teams review the .dvms file; mobile engineers see device behavior; runtime engineers bind it to debugger scores; formal engineers map the same IR to K fixtures.

The hooks block is the fault-injection surface. A hook pairs a selector with an action. Selectors target local kernel calls (call kind=bind-decision|prepare-step|advance-step|publish-gate|abort-session), inbound protocol frames (ingress phase="dkls23/share_mul_ot/ssot_round1_recv" from=s2 to=agg), outbound frames (egress), or named instruction sites (site op="ShareMulBackendOt"). All selectors accept optional peer, from, to, and macro-kind filters.

Actions are: deny code "REASON" (reject the call with a stable reason code), drop (silently discard the frame), duplicate (deliver twice), replay (replay a previous frame), equivocate variant="v" (send a conflicting version), disconnect peer <name>, reconnect peer <name>, and restart peer <name> preserve [vault, keyshare]. This lets a single scenario cover publication holds, replay attacks, equivocating peers, and mobile app restarts in a reviewable, deterministic file.

Expectations address four subject types. Path assertions use dot notation: lifecycle.state == Published, publication.state == Denied, terminal.kind == Abort. Artifact assertions check presence or absence: artifact kind="SignaturePublic" present. Evidence assertions bind to evidence class or kind: evidence class="MobileNodeReceipt" present, evidence kind="invalid-ingress" present. Instruction-site assertions stop at a named DVM op and inspect projected fields: site op="ShareMulBackendOt" pending_frontier contains "shareMulSsotRound1".

Operators are: == and != for equality, contains for set membership, present and absent for artifact/evidence existence, in and subset_of for set relations, and stable for unchanged binding checks (used for receipt.mobile_binding stable). Assertion backends are Native, K, or Cross — the IR tags each assertion so the native runner and K lowering can evaluate the same expectation list independently.

The formal block attaches K verification to the scenario. family dkls23_aff3 selects the specification family. mode is krun (execute and verify), kprove (prove symbolic claims), or both. checks lists positive fixtures: publication-boundary, operational-envelope, projection-boundary, commit-done-safety, invalid-ingress-no-accept, aff3-projection, share-mul-current-profile, current-production-blockers, security-semantics, composition-premises. negatives lists stuckness fixtures: publish-without-gate, commit-done-missing-cid, commit-abort-with-public-status, commit-pending-non-egress, local-private-sigma-rejected.

compare axes control how native and K execution traces are compared: public-observation, publication-frontier, pending-frontier, evidence-class, accepted-ingress. The K lowering produces a KScenarioBundle with definition metadata, krun terms, claim modules, and compare axis bindings. Native and formal reports share scenario ids, run axes, and expectation subjects so a divergence between the two execution paths is immediately locatable.

dvm-scenario owns the authoring AST, parser, canonical IR, registry vocabulary, formal lowering, report shapes, and shared testing harness. DvmWorldHarness resolves peer aliases into deterministic peer ids and records roles, signer indexes, aggregator, threshold, setup, lane, mobile roles, and reachability. DvmExecutionQueue<DvmHarnessFrame> carries Run, Ingress, Egress, Hook, LocalCall, and PeerLifecycle frames.

dvm-debugger compiles DvmslScenario into CompiledDvmslScenario, builds DebuggerConfig, and runs through DvmDebugger. DvmScenarioFixture::from_source packages the parsed scenario, world, queue, service registry, journal, and diagnostics for customer fixture packs and adapter tests.

A mobile participant is modeled as a peer with mobile in its roles. A scenario can include one mobile party inside a server quorum, simulate an app restart between prepare and sign, preserve vault and keyshare state across restart, reconnect the phone, and verify that the quorum still reaches a published result with a stable mobile binding receipt.

For mobile teams the boundary is explicit: the app supplies public operation facts and local keyshare references, the mobile node executes its local role inside the virtual world, and the harness records whether the resulting receipt matches the expected quorum and device binding. The same harness validates iOS and Android integrations against the same scenario source.

The scenario harness is available for customer integration, security review, backend-profile validation, and partner mobile-app testing. It ships as a review or integration artifact with fixtures matched to the deployment profile.

Coverage: native execution and K lowering for DKLS23-backed flows and mobile-node quorum paths. The scenario grammar reserves schedule blocks for time-based fault injection and K family bindings for FROST and CGGMP24 backends.