Module trace_determinism 

The concurrency tie made literal: determinism = contractibility, on a real machine.

proof_rewrite showed that a refutation’s independent steps commute, and that the space of reorderings is a contractible CAT(0) cube complex. That is not an analogy to concurrency — it is the same object. Here we run an actual tiny shared-memory machine and prove the identification on the nose:

• Two operations’ commutation 2-cell exists (the square commutes in the cube complex) iff running them in both orders yields the same state — and the structural test for that is exactly Bernstein’s conditions (neither writes what the other reads or writes), the independence relation of the trace monoid.
• A set of pairwise-independent operations is deterministic — every one of the n! schedules produces byte-identical state (we run them all) — and that is exactly the contractibility (χ = 1, the cube condition) of the same ProofPoset the proof tower uses.
• Cooperative ≡ work-stealing: two schedulers over independent tasks agree byte-for-byte because both are linear extensions of one contractible trace complex, joined by commutation 2-cells. This is the repo’s diff_cooperative_eq_workstealing as a homotopy — the certificate of agreement is the 2-cell path.
• A data race is a missing 2-cell: a write-write conflict makes the ops dependent (no square), and the two orders genuinely diverge. Race detection falls out of the homotopy.

So the homotopy theory of proofs and the determinism theory of concurrency are one theory, and this module is the bridge with the machine actually running underneath it.

Structs

Op

A shared-memory operation: read some cells, then write one cell with a pure function of the reads (in reads order). The minimal unit that can race.

Functions

bernstein_independent

Bernstein’s conditions — a and b commute (are independent) iff neither writes a cell the other reads or writes. This is the independence relation of the trace monoid: precisely the pairs whose commutation square is a 2-cell in ProofPoset. (Read–read sharing is fine; reads commute.)

run

Run a schedule (a sequence of op indices) from an initial state, returning the final state.

trace_poset

The commutation poset of a set of concurrent operations: independent pairs (Bernstein) are left unordered — their commutation is a 2-cell — and conflicting pairs get a program-order edge (lower index first), which is the only way to keep a deterministic execution. The trace’s cube complex.