Evidence

Distributed-systems benchmark tasks and execution semantics

This benchmark exercises the distributed-systems checker with implementation, diagnosis, property-review, deployment, authentication, and secrecy tasks. The tasks do not all use one file layout or ask for the same kind of answer.

Most implementation tasks separate a protocol.bosatsu, checker.bosatsu, and reference/ variants. Diagnosis tasks provide a system to judge. Property-review tasks provide candidate properties and witnesses. The mixed-version task supplies old and new deployments together, while the mutant task supplies several adversarial variants of an earlier protocol.

The engine runs node starts, atomic message activations, network choices, declared faults, and invariant checks under finite bounds. holds means all allowed schedules were explored to completion without a violation. violated includes a concrete counterexample schedule. inconclusive means exploration was truncated before a holding result could be certified. Read the execution-semantics reference for activation, network, fault, invariant, and adversary rules.

One recorded result: task 010 reflection counterexample

This is a measured run, separate from the task briefs below. In task 010, the direction-bound reference answered with Mac(1,·), accepted Mac(0,·), and held over a complete 13,641-schedule run. The reflectable variant used Mac(0,·) in both directions and was violated. Its counterexample has the attacker challenge the server with the server's own nonce, receive Mac(0/10), and replay that tag into a second session. The final state records session 2 as authenticated while the honest client completed no session. The served iteration-009 artifact contains the exact task result, reviewer prompts and responses, labels, schedule count, and token counts; the task 010 source tree contains both variants.

Ten task briefs, sources, and expected failure modes

There are ten tasks so far, in three families: state under an unreliable network (001–005, 007), authentication against an active attacker (006, 008, 010), and secrecy (009). Each name links the task's sources in the repository. The description states what the task asks the checker or reviewer to distinguish. These briefs are task definitions and expected failure modes, not claims that every expected failure occurred in a recorded run.

001 idempotent-counter

Exactly-once apply when the network reorders and duplicates deliveries (duplicates model client retries). The naive server counts a retry twice.

002 lost-update

Two app servers increment a shared counter through a versioned store. Delivery order is the only adversary: read-modify-write loses an update; compare-and-swap with retry does not.

003 diagnosis-dedup-cache

A diagnosis task supplies the system under review: an LRU-1 dedup cache in task 001's world. The reviewer must judge it. The cache evicts the one id it needed to remember.

004 property-review-jobs

Property review rather than implementation: do the declared properties actually pin the English intent (“every queued job runs exactly once, and only fetched jobs run”), or do they pass a system that violates it?

005 adversarial-mutants

Three generator-produced mutants of task 002's CAS solution, each checker-verified defective but written to read as correct. They have no self-refuting comments, defects only in cross-handler logic under contended interleavings.

006 replay-auth

Challenge-response authentication that must not accept a replayed answer: the nonce exists so each proof is single-use, and the property catches servers that forget which nonce they issued.

007 mixed-version-deploy

Deploy safety asks whether a rolling upgrade remains safe while the old blind-write version runs beside the fixed CAS version. The checker also verifies the homogeneous new fleet.

008 forgery-auth

Authentication against an active man-in-the-middle that observes signatures, opens its own sessions, and replays what it learns across them. First task on the branching adversary node.

009 secrecy-transit

Confidential delivery over an eavesdropped network: the secret must reach the server without the wire-reading attacker ever holding its plaintext.

010 reflection-auth

Mutual authentication at protocol scale. The keyless attacker reflects the server's own challenge back through a second interleaved session, using the server as a MAC oracle. The evidence index explains the three-cell reviewer experiment, and iteration-009.md contains its prompts, responses, labels, and token counts.

The committed results directory contains per-iteration benchmark records. The evidence index summarizes the recorded experiments and links the artifacts served on this site.