Chapel: docudactyl-specific Agda formalisation (DistributedAggregationInvariants.agda) #32

Follow-up to #29 / #31 (Wave-3 Chapel rehabilitation).

The ADR landed in #31 (docs/decisions/2026-05-30-docudactyl-chapel-rehab.md) records that docudactyl's parallel-dispatch surface is embarrassingly-parallel with deterministic reduction, not speculative like echidna's parallelProofSearchSpeculative. Echidna's proofs/agda/ParallelSoundness.agda theorems (first-success-wins soundness / completeness under retry / cancellation safety) do NOT apply — they cover a different proof shape.

If formal proofs become load-bearing, docudactyl wants its own module at proofs/agda/DistributedAggregationInvariants.agda covering these 7 invariants (listed in the ADR §"Parallel-dispatch invariants"):

1. At-most-once — every document index processed at most once; per-locale isAlreadyProcessed + recordCheckpoint. Caveat: cross-locale resume after topology change isn't global-atomic.
2. Abort-bounded — beyond failure-rate threshold, shouldAbort() short-circuits; unprocessed indices remain observable.
3. Aggregation commutativity — accumulate writes only to perLocaleStats[here.id]; computeGlobal reduces by integer addition (commutative by construction).
4. L1 cache coherence — (path, mtime, size)-keyed LMDB lookups; no concurrent writers to same key.
5. L2 cache coherence — Dragonfly L2 keyed by SHA-256; concurrent stores tolerated because deterministic.
6. Checkpoint resumability — resume reproduces the same aggregated stats modulo per-locale ordering.
7. Content-type determinism — magic-byte detection is deterministic per file.

This is deferred — file this issue so the intent isn't lost. Open this only when formal proofs of these invariants become load-bearing (e.g. before a production deployment over real BL-scale corpora).

Suggested toolchain: agda 2.6.3 + agda-stdlib (matches echidna's setup; see session_2026_05_30_chapel_rehabilitation).