Bounded driver simulation v1

Independent Python model · 5 September 2026 · not transport conformance

Result

Thirteen targeted schedules and 64 seeded runs of 2,000 events each pass the model's invariants. Five observer/scheduling tests also pass, including deliberately invalid states that must trigger invariant failures. The run records 128,000 generated events; this is sampled sequence testing, not exhaustive model checking.

Targeted schedules cover handshake limits and expiry, slow input/output, verification expiry, lease expiry before commit, epoch changes between verification and commit, stalled writes, sync errors with surviving/lost unacknowledged data, restart, lost acknowledgements, invalid floods, both commit lanes filling, and successful sync after the caller's writer deadline.

In the full-lane schedule, each lane accepts 16 of 17 verified offers and refuses one (5.88%); successful setup admissions are excluded from these denominators. Service alternates between the local-evidence and ordinary lanes. This is a finite workload observation, not a steady-state throughput or fairness result.

The attack-first schedule fills all 32 sessions and all 128 preverification slots. The newcomer is refused at session establishment. Only eight jobs can be processed from the initial 32-credit budget, even when every signature is invalid; a long idle interval replenishes to 32 credits, never more. Invalid local-slot hints do not enter the reserved lane. Session scarcity remains an unresolved attack surface.

Modeled state and invariants

The driver has a virtual monotonic millisecond clock, node-assigned source handles, 4 handshake slots, 32 sessions, bounded partial frames, a per-source FIFO verifier, two 16-entry commit lanes, one writer, and one response slot per session. Verification and commit-time revalidation each receive a separate 32-credit/100-ms budget; each attempt costs four credits. The model bounds admission accounting to 64 local slots and 64 foreign tombstones within an epoch.

Every event checks source, payload, queue, response, task, credit, and ledger bounds. Payload accounting is conservative: claims cost 442 bytes and evidence 884 bytes. This model does not include the smaller open-cost claim variant. No acknowledgement may enter the output queue or be delivered without a committed observation for that operation identity. An acknowledgement records a commit, not continued receipt usability after expiry, quarantine, or an epoch change.

Commit-time validation rejects stale epochs, expired jobs, conflicts, or exhausted accounting. No second writer starts while one exists. A writer timeout poisons the handle without cancelling the operation; recovery refuses to proceed until it ends or a modeled process restart terminates it. Even a later successful sync does not clear the poisoned state or automatically send an acknowledgement. Recovery and retry preserve one allocation per slot.

Assumptions and deliberate omissions

Cryptographic validity, descriptor availability, successful recovery sync, and atomic epoch rollover are explicit oracles. No real keys, sockets, files, or cryptographic verification are used. An error-with-surviving-data outcome represents a complete unacknowledged write; the restart-loses-in-flight outcome represents another permitted outcome. This does not enumerate all hardware failures.

The model accounts for logical payload bytes and object/task counts. It does not measure allocator metadata, deque retained capacity, kernel buffers, CPU time, or actual RAM. Observer histories of delivered and committed identities are unbounded test instrumentation, outside modeled node state. Epoch counters and validity are abstracted; full policy time mapping remains in the separate ledger tests.

Generated schedules use Python's seeded random generator and sorted session choices; the report records seeds and Python version. They are separate from the frozen Rust discovery RNG and regression control. Handshake cryptography, physical clock drift, peer topology, admission economics, and semantic utility are outside scope.

Reproduce and next gate

python3 model/driver.py
python3 -m unittest discover -s model -p test_driver.py

The report is docs/results/driver-model-v1.json; source/evidence hashes are in docs/results/driver-model-v1-manifest.json. No production Rust behavior changed. Next: drive a bounded Rust scheduler with the same event traces and compare its observable decisions with the model, using the real queue and ledger. Add actual framing, memory accounting, and controlled socket faults only after that refinement surface is reviewable. Public admission remains disabled.

Follow-up comparison

A restricted synchronous Rust/model comparison is now recorded in docs/DRIVER_RUST_V1.md. It covers 13 shared traces, not the entire simulation or its generated event set. The production driver remains unimplemented.