Days v1.0.0

Days 1.0 replaces the actor-model simulator with Days AGO, an exact safe-horizon executor: one logical process per network node, with processes advancing concurrently only under a proved conservative bound. Every backend that runs a model produces byte-identical complete state.

What's in it

• Four backends, one answer: scalar, multicore CPU, Metal (Apple GPUs), and CUDA (tested on RTX 4090 and GB10), byte-identical at every worker count and device geometry. DCQCN control, PFC, RED, and collectives run on the CPU backends for now; the GPU backends refuse them at validation.
• Proved in Lean: five executor theorems covering the safe-horizon rule, with standard axioms only; LeanGuard trace certificates for DCQCN, PFC, CUBIC, AQM, DRR, and WFQ run in CI.
• Protocols: closed-loop TCP Reno and CUBIC, DCQCN with CNP, PFC, ECN, RED, strict-priority, DRR, and exact-rational WFQ scheduling, plus ring all-reduce and all-gather collectives.
• Performance (RTX 4090 vs GeDES, same machine): the TCP workload run to completion finishes 3,918× ahead; on the active TCP phase the two engines now tie (0.996×); UDP at 30% and 60% load trails by 1.06–1.08×. The CPU backend alone outperforms sequential ns-3 83× and Unison 9.0×.

Upgrading

The root days crate is now Days AGO (scenario compiler plus executor). Legacy Days is frozen at 0.4.3 as the days-legacy workspace member in legacy/; its last main commit is tagged legacy-main-final.

Full phase-by-phase record: #104. Evidence: the days-gpu repository.