Concurrency testing
Concurrency is modelled at the scenario/execution level. The repository’s simulator is deliberately single-threaded and deterministic — pretending it is concurrent would defeat reproducibility — so operations that would race in a live system are composed sequentially here, and the scenarios pin the ordering semantics the ledger must honor. A concurrency regression in the real system (a lost update, an interference bug, a commitment inconsistency, a replay slip) shows up as a failed sequential composition.
The properties under test
- No lost updates — two spends from the same account compose: the second spend must see the ledger after the first.
- No interference — transfers on different accounts must not clobber each other’s state; each moves exactly its declared amount.
- Commitment bookkeeping — interleaved operations (merge then transfer) keep commitment statuses reachable from the fixture posture.
- Proof pipeline independence — proof generation and verification are order-independent (each proof binds its own statement) and side-effect-free (verification never touches the ledger).
Scenarios
The concurrency pack (CT-CONC-001..004):
| Id | What it pins |
|---|---|
| CT-CONC-001 | alice spends 200 to bob then the remaining 100 to issuer; no state is lost between the two spends |
| CT-CONC-002 | alice→bob and bob→issuer compose without interference |
| CT-CONC-003 | a merge followed by a transfer keeps commitment bookkeeping consistent |
| CT-CONC-004 | two proofs are generated and verified before either proved transfer executes; both then compose |
Every scenario is judged with the built-in invariant registry attached (ownership, commitment-consistency, replay-protection, privacy; the proof pipeline also holds proof-binding and input-binding), and the pack’s tests require every run to pass with zero invariants failed.
Run them with:
cargo run -p cli --bin crucible-scenarios -- run --category concurrency
cargo run -p cli --bin crucible-scenarios -- report
What is and is not covered
- Covered: sequential-composition correctness over the fixture posture, and the ordering semantics listed above.
- Not covered: true multi-threaded execution, live-race detection, or contention timing — those require the real simulator or a Soroban environment and are future work behind the adapter contracts.