Specification

Scenario language (TSS-SL)

A scheme-independent language describes worlds, workflows, causal stimuli, run control, expectations, and formal targets; every scenario lowers to a canonical, content-addressed IR.

A scenario is the unit of conformance. It declares the quorum world and randomness policy, the protocol workflow that drives execution, a deterministic stimulus schedule, run control, expectations over lifecycle and publication state, and the formal-backend target with its compare axes.

Both runners consume the same canonical IR, so the compared executions share their scenario root, stimulus-schedule root, and expectations byte for byte.

Scenario structure

Six sections compose a scenario; vocabulary within them is family-defined.

Publication-boundary scenario

text

//@ category: publication
//@ support: formal
//@ backend: dkls23-aff3
//@ doc: signature is published through the publish gate
scenario "aff3.publication.boundary" {
  world {
    engine synthetic
    peer alice roles [signer] peer bob roles [signer]
    peer carol roles [signer, agg]
    threshold 2/3 key "key-1" lane 0 agg carol
    randomness production-rng compare_random_outputs public-validity
  }
  workflow { use scenario "l2-aff3.sign-and-publish" }
  run      { continue until breakpoint site "publish_sig" }
  expect {
    publication.state == NotPublished
    public_observation absent
    artifact kind="local_signature" present
  }
  formal { k { family dkls23-aff3 mode krun
    checks  [publication-boundary]
    compare [public-observation, publication-frontier, leakage-boundary] } }
}

Causal stimulus schedule

Faults and timing are causes and belong to the IR: delivery, drops, replays, duplicates, equivocation, timeouts, restarts, and denials are scheduled in logical time — ticks, rounds, and event or call triggers. Runner pairs compare scenarios with identical canonical stimulus roots, so both sides replay the same execution.

Canonical stimulus IR

rust

struct Stimulus {
    id:       StimulusId,
    trigger:  StimulusTrigger,   // AtTick(u64) | AfterEvent(..) | OnCall(..)
    selector: StimulusSelector,
    action:   StimulusAction,    // Deliver | Drop | Replay | Duplicate
                                 // | Equivocate { variant_root } | Timeout
                                 // | Disconnect | Reconnect
                                 // | Restart { preserve } | Deny { code }
    payload:  Option<Cid>,
}

Randomness policies

Randomness generation and observation comparison are declared separately: generation as deterministic-test-rng, production-rng, or symbolic-random; comparison as raw-bytes, shape-only, public-validity, abstract-token, or order-insensitive-set. A runner honours the declared policy or reports the affected axes as Unsupported.

Corpus organization

The core corpus is scheme-independent; family extensions add scheme-specific obligations. Every scenario carries a //@ metadata overlay — category, support level, backend, tags — read by the harness and transparent to the parser.

Corpus layout

text

core:       lifecycle · keygen · signing · publication · aborts
            ingress-faults · leakage · policy · threshold
extensions: dkls23.share-mul · frost.nonce-binding
            cggmp.mta-paillier · ice-frost.resharing · bip32.derivation