# Bounded event-interleaving experiment

This directory contains a new, self-contained research model for **Evidence-Bound Completion**. It is not a copy, benchmark, or verification of a production application. Its purpose is to make a narrowly stated concurrency claim executable: a successful preflight does not justify a later completion when relevant state can change between them.

## Reproduce

Requirements: Node.js 22 or later; no packages, API keys, network access, or datasets. The stored result was generated with Node.js v22.23.0.

```sh
node experiment.mjs
node experiment.mjs --check
```

The first command regenerates `results.json`. The second reruns the entire experiment and asserts byte-for-byte agreement with that file, including the SHA-256 digest of `experiment.mjs`. Both commands print the bounds and aggregate table. The source uses neither randomness nor wall-clock time. Assertions are enabled in an ordinary Node invocation.

The three artifacts are:

- `experiment.mjs`: simulator, topological-order enumerator, history oracle, assertions, and result writer.
- `results.json`: exact counts per scenario and protocol, shortest counterexamples, negative controls, bounds, and source digest.
- `experiment-README.md`: experimental design and interpretation.

## Model and event order

One fixed task asks for twice an integer input. Its accepted behavioral contract is `behavior-v1`. One authenticated worker, one attempt, one input object, and one artifact slot participate in the candidate workflow. A second worker can acquire the assignment but does not produce a second candidate in this model.

The workflow has five ordered events:

```text
read → candidate → trusted-verify → preflight → commit
```

`read` captures the input version and value. `candidate` writes an artifact and records its digest and read provenance. `trusted-verify` checks the artifact against the captured input and records immutable evidence in a trusted store. `preflight` evaluates a proposed completion. `commit` decides whether to create a new authoritative receipt.

Here `candidate` writes a **mutable working artifact slot**, while the event history preserves an immutable candidate description and its original bytes. The output-digest check asks whether the working slot still equals that candidate snapshot. `commit` only registers a completion receipt: it does **not** publish an immutable candidate into a target, check a target base with compare-and-swap, or implement a multi-file transaction. Those are broader protocol requirements, not features evaluated by this experiment.

The candidate writes this staging slot before completion admission. An `artifact-edit` that happens before `candidate` is overwritten by the candidate write and can therefore be protocol-safe in this model. This does **not** demonstrate freedom from lost updates to a real publication target.

The enumerator inserts zero, one, two, or three distinct environment events from this set:

| Environment event | Effect |
|---|---|
| `input-edit` | Replace input version 0, value 7 with version 1, value 11. |
| `artifact-edit` | Replace the artifact-slot bytes. A later candidate write can overwrite an earlier edit. |
| `lease-expire` | Mark the current lease no longer live. |
| `reassign` | Give the task to another principal and unique attempt, advance the numeric fence, and establish a live lease. |
| `revoke` | Revoke the original worker's completion authority. |
| `publish-behavior-v2` | Publish a new behavior policy while leaving this task's fixed v1 contract in effect. |

Every environment event occurs at most once. If expiry and reassignment both occur, expiry precedes reassignment. Apart from that edge and the five workflow events, every topological order is enumerated. Events may occur before the initial read or after commit. A change before a read or a write is therefore not automatically a failure; the history determines which version was actually used.

Lease liveness is a discrete **admission condition at the completion linearization event**. This model does not promise that an eventual database flush or client response finishes before a real-time lease deadline. `reassign` changes the entire attempt identity as well as its numeric fence.

Publishing a new behavior policy and revoking a grant are different events. Existing tasks keep their fixed behavior contract; live revocation takes effect at the next new completion. Treating every publication as revocation is tested as an unnecessarily restrictive alternative.

## Exact enumeration bounds

There are `1 + 6 + 15 + 20 = 42` environment subsets. With five ordered workflow events, the number of orders for a subset of size `k` without the extra expiry/reassignment edge is `(5+k)! / 5!`.

| Environment events | Subsets | Total schedules |
|---|---:|---:|
| 0 | 1 | 1 |
| 1 | 6 | 36 |
| 2 | 15 | 609 |
| 3 | 20 | 6,048 |
| **Total** | **42** | **6,694** |

The one two-event subset containing expiry and reassignment contributes 21 rather than 42 orders. Four three-event subsets contain that pair and contribute 168 rather than 336 orders each.

Each of the 6,694 schedules runs under 13 protocols: **87,022 primary protocol runs**. Seven separate directed negative controls add **91 protocol runs**. Additional sanity assertions check generator cardinalities, a known TOCTOU counterexample, benign policy publication, evidence failures, and the weak-checker limitation. The primary and negative-control denominators do not include these sanity assertions.

These are complete **schedule counts within the stated bound**, not a distribution of real workloads. Different schedules can have identical prefixes at commit and differ only in later events; these suffixes are retained because replay is tested after them. Do not interpret the counts as independent trials, probabilities, model accuracy, throughput, or production failure rates.

## Compared protocols

`self-report` accepts a completion statement. `lease-fence-only` checks the current principal, attempt, numeric fence, and lease, but ignores input and artifact changes, evidence, and revocation. `atomic-contract` checks all modeled conditions and writes the receipt in one indivisible event. `check-then-commit` evaluates the same complete checks at preflight, caches the result, and uses it later without revalidation.

The remaining protocols remove specific checks from the atomic contract or add a deliberately overstrict policy condition:

- `no-fence`: remove only the numeric fence comparison, preserving current principal and unique-attempt matching.
- `no-attempt-binding`: remove principal, attempt, and fence binding together; retain task-level lease liveness.
- `no-lease`: keep attempt binding but omit lease liveness.
- `no-readset`: omit current input-revision validation.
- `no-current-authorization`: omit live revocation validation.
- `no-evidence`: omit trusted-verifier membership, outcome, and evidence binding.
- `no-artifact-binding`: omit current-content and attested-content digest binding.
- `no-contract-binding`: omit task identity and fixed behavioral-contract binding.
- `latest-policy-only`: require the newest behavior policy even for a task with a valid fixed contract.

**The numeric fence is redundant in this particular model.** Attempt identifiers are unique and never reused; reassignment changes both the identifier and fence. Keeping unique-attempt matching while removing the number catches all of the same primary failures. The separate `no-attempt-binding` result concerns the whole ownership binding, and must not be presented as evidence that the numeric fence independently caused that result. Reused attempt identities, ABA behavior, independently fenced downstream resources, and real storage fencing are outside this model.

## Independent history oracle

The system under test consults mutable simulator state in `gate()`. The oracle does not call `gate()`, read its booleans, inspect a protocol's settings, or read simulator state. It reconstructs the input version, current ownership, lease status, revocation, artifact bytes, read provenance, and actual trusted verification events from the history before commit.

The oracle considers a new completion protocol-safe only when:

1. The submitted worker and attempt still own the task and the lease is live.
2. Its observed input is still current.
3. Completion authority remains granted.
4. The candidate names this task and its fixed behavior contract.
5. The artifact bytes still match the candidate bytes and digest.
6. A designated trusted verifier actually produced a passing record for the same candidate, read provenance, bytes, task, and contract.

Thus an attacker-supplied evidence identifier is not itself evidence. The oracle checks recorded verifier events and observed bytes, not only the fields claimed by the candidate.

Oracle independence here is **implementation separation**, not an independent formal proof: the gate and oracle intentionally implement the same written safety specification, and a common specification error remains possible. The finite enumeration checks modeled races; it cannot establish properties outside the model.

## Primary results

At commit, the history oracle labels 470 schedules safe and 6,224 unsafe under every protocol. The decision table is:

| Protocol | Accept safe | Accept unsafe | Reject unsafe | Reject safe |
|---|---:|---:|---:|---:|
| Self-report | 470 | 6,224 | 0 | 0 |
| Lease/fence only | 470 | 1,914 | 4,310 | 0 |
| Atomic contract | 470 | 0 | 6,224 | 0 |
| Check then commit | 470 | 718 | 5,506 | 0 |
| No numeric fence | 470 | 0 | 6,224 | 0 |
| No attempt binding | 470 | 667 | 5,557 | 0 |
| No live lease | 470 | 517 | 5,707 | 0 |
| No readset | 470 | 328 | 5,896 | 0 |
| No current authorization | 470 | 512 | 5,712 | 0 |
| No evidence | 470 | 0 | 6,224 | 0 |
| No artifact binding | 470 | 134 | 6,090 | 0 |
| No task/contract binding | 470 | 0 | 6,224 | 0 |
| Require latest behavior policy | 234 | 0 | 6,224 | 236 |

The atomic contract admits all 470 safe schedules and no unsafe schedule **within these bounds**. Reporting both columns is essential: the experiment does not award success merely for refusing every candidate.

Two zero-difference primary ablations require careful interpretation. Primary candidates always use the correct task contract and originate from a genuine verification step. Consequently `no-evidence` and `no-contract-binding` are not distinguished by these benign-candidate schedules. Directed controls below test those assumptions rather than inventing concurrency failures for them.

### Short counterexamples

The result file records shortest examples, their violated conditions, and the historical records before commit. Representative traces are:

```text
TOCTOU:
read → candidate → trusted-verify → preflight → artifact-edit → commit

Missing input revision check:
read → candidate → input-edit → trusted-verify → preflight → commit

Missing attempt binding:
read → candidate → reassign → trusted-verify → preflight → commit

Unnecessary policy rejection:
publish-behavior-v2 → read → candidate → trusted-verify → preflight → commit
```

In the TOCTOU case, verification and preflight both legitimately succeed; an edit afterwards invalidates the result before its receipt is written. In the input case, a trusted check against the saved input can pass even though that input is now stale. In the policy case, the task's v1 contract remains valid and the oracle considers the candidate safe.

## Directed negative controls

These seven controls use the clean five-event workflow and are reported separately from schedule totals.

| Control | Atomic outcome | Ablation that admits the invalid completion |
|---|---|---|
| Forged evidence identifier, absent from trusted history | Reject | No evidence |
| Genuine evidence for another candidate | Reject | No evidence |
| Genuine record with a wrong content digest | Reject | No artifact binding; no evidence |
| Candidate and evidence name another task | Reject | No task/contract binding |
| Candidate and evidence name the wrong behavior contract | Reject | No task/contract binding |
| Actual checker rejects a wrong answer | Reject | No evidence |
| Deliberately weak checker accepts an integer that is the wrong answer | **Accept** | All protocols accept; this exposes a specification limit |

The last control uses `answer = 999` while the required answer is 14. Its deliberately inadequate checker only tests whether the answer is an integer. The independent semantic oracle checks the actual doubling requirement. The atomic contract therefore accepts a **protocol-safe but semantically wrong** artifact. Valid provenance and atomicity do not make a checker sound, complete, or honest. This experiment must not be described as proving task correctness.

The other baselines' exact outcomes are stored in `negativeControls` in `results.json`.

## Idempotency and replay

All protocols share the same idempotency wrapper so this feature does not unfairly distinguish the baselines. After every accepted primary completion, the simulator executes the remaining environment events, then:

1. Retries the identical request with the same idempotency key and asserts that the exact original receipt is returned.
2. Changes the candidate digest while reusing that key and asserts an idempotency-conflict rejection.
3. Asserts that exactly one terminal receipt write occurred.

Replays are historical receipt retrievals, not new completions. Returning a prior receipt after revocation does not reauthorize a new action. The `exactReplays` and `changedReplaysRejected` fields count these checks and equal each protocol's number of accepted primary completions. A dedicated assertion includes revocation, reassignment, and input mutation after an atomic acceptance. Rejected first submissions do not enter this replay count. Alternate idempotency keys, crash recovery, concurrent duplicate transactions, and receipt-read authorization are not modeled.

## Limits of the claim

The atomic completion step is an **assumed linearization point for receipt registration**. No actual transaction engine, filesystem, distributed service, cryptographic signing system, or network protocol is verified. Publication of candidate contents, target-base compare-and-swap, and multi-file publication atomicity are not implemented. Actual implementations must bind the authenticated caller and ensure that actual writes are a subset of the fixed contract scope intersected with the live grant. Here the caller and target slot are fixed; path authorization is not evaluated.

The model excludes multiple simultaneously executing candidate writers, repeated environment changes, wall-clock expiry races inside a transaction, crash and recovery behavior, multi-object dependency graphs, and external side effects. Read-access permissions are not evaluated: a read event simply records an observed snapshot, even when a later completion would lack authority. The trusted store is a provenance abstraction, not a substitute for a real trust root.

The experiment uses synthetic integers and bytes only. It contains no LLM runs, private user data, production traces, human evaluations, latency measurements, or task-success benchmark. The supported conclusion is that the enumerated reference model exposes concrete stale-completion races and demonstrates their rejection by the stated atomic contract, while retaining safe completion and showing exactly which assumptions remain outside it.