Chapel parallel proof-search: cross-repo wave-2 follow-on (after echidna#146)

[hyperpolymath]

Breadcrumb tracking issue.

echidna#146 is the Chapel
metalayer rehabilitation (closes echidna#133). It rewrites `src/chapel/*.chpl`
to compile under chpl 2.3.0 / 2.8.0, flips chapel-build / zig-ffi CI to strict,
adds L2.2 `parallelProofSearchSpeculative` (atomic-CAS first-success-wins),
and proves the aggregation invariants in
`proofs/agda/ParallelSoundness.agda` (zero postulate/admit/believe_me).

Wave 2 of the same arc reaches `proven`: any Chapel-backed parallel proof
dispatch we add here should follow the same shape — static lib because the
apt-shipped Chapel is `CHPL_LIB_PIC=none` only, `require` directive + `extern
record` to bridge the C ABI without LLVM, smoke target decoupled from the
main metalayer surface, Agda aggregation invariants reused / extended.

Action items (deferred to Wave 2, no work in this issue yet):

• Identify proven's parallel-dispatch surface (if any)
• If applicable, port the echidna pattern (`smoke.chpl` + `chapel-build`
  recipe + `require`+`extern record` skeleton)
• Decide whether the proven build oracle wants its own
  `ParallelSoundness` Agda module or imports the echidna one

Pointers for the future agent / author:

• Rehabilitation ADR: `docs/decisions/2026-05-30-chapel-rehabilitation.md`
  inside echidna#146
• Soundness theorems: `proofs/agda/ParallelSoundness.agda` (3 theorems
  • sanity checks)
• L2.2 implementation: `src/chapel/parallel_proof_search.chpl ::
  parallelProofSearchSpeculative`

[hyperpolymath]

Wave-2 closure rationale

Audit confirms proven has no parallel-dispatch surface to rehabilitate and the echidna pattern is already applied at the only Chapel surface that exists. Closing this tracker with a concrete write-up so future Chapel work in proven doesn't re-litigate.

Action item (a): Identify proven's parallel-dispatch surface (if any)

None. Per proven's .claude/CLAUDE.md (ADR-008, "FFI-only bindings"):

Bindings in bindings/rust/, bindings/zig/, bindings/deno/, etc. must ONLY wrap Idris FFI calls, NOT reimplement algorithms

Proven is a formally-verified safety primitives library. The Chapel surface at bindings/chapel/src/*.chpl is 11 Tier-1 binding wrappers (Proven.chpl, SafeCrypto.chpl, SafeDateTime.chpl, SafeEmail.chpl, SafeHeader.chpl, SafeJson.chpl, SafeMath.chpl, SafePath.chpl, SafeString.chpl, SafeUrl.chpl, LibProven.chpl). Each one is a thin shim that calls libproven.so via the require "proven.h" + extern proc C-ABI bridge.

grep -E "forall|coforall|cobegin|sync\b|atomic\b" bindings/chapel/src/ returns zero hits (one match for begin is in a comment string). No parallel_proof_search.chpl analogue exists, nor should one — the architecture explicitly forbids implementing logic in bindings, including parallel-dispatch logic.

Action item (b): If applicable, port the echidna pattern

Already applied via #135. The binding-tier-1 detachable-harness pilot landed 2026-05-30 ships:

• require "proven.h" + extern proc bridges throughout LibProven.chpl and the per-primitive modules
• Decoupled smoke at bindings/chapel/smoke/hello_smoke.chpl (exercises SafePath / SafeHeader / library-version surface without depending on anything beyond the WIRED subset)
• Strict CI workflow .github/workflows/chapel-ci.yml with the 6-job detachable shape (detachability-guard / build / symbol-audit / smoke / tests / detachable-build) — extractable to a standalone proven-chapel repo
• symbol-manifest.txt + scripts/symbol-audit.sh for ABI-drift detection
• ADR-0001 (template) + ADR-0002 (pilot) at docs/adr/

This is the binding-flavor of the echidna pattern; the metalayer-flavor (smoke + require+extern record + strict CI) is structurally identical but at binding-layer granularity. No additional port work is needed.

Action item (c): Decide whether the proven build oracle wants its own ParallelSoundness Agda module or imports the echidna one

Moot — no parallel dispatch means no aggregation invariants to formalise. Echidna's three theorems (first-success-wins soundness, completeness under retry, cancellation safety) characterise speculative search; proven has neither speculation nor search. The safety guarantees relevant to proven are the Idris-side totality + dependent-type proofs already in src/Proven/, formalised at a different level entirely (per-primitive correctness, not aggregation).

Comparison vs Wave 3 (docudactyl)

• echidna (Wave 1): speculative parallel-search metalayer — ParallelSoundness.agda 3 theorems
• proven (Wave 2): no parallel-dispatch surface — N/A
• docudactyl (Wave 3): embarrassingly-parallel + deterministic-reduction metalayer — different invariants (at-most-once / aggregation-commutativity / cache-coherence / checkpoint-resumability), formalisation deferred (docudactyl#32)

The cross-repo Chapel rehabilitation arc is now closed in the only sense it can be: each repo's pattern is settled, applied, and documented.

Closure

Closing this tracker. If proven ever grows a Chapel-side parallel surface (e.g. parallel batch verification of large primitive inputs), that would be a new design discussion that explicitly relaxes the FFI-only-bindings rule — and would warrant a new Wave-N tracker rather than reopening this one.

References:

• echidna#146 (Wave 1)
• proven#135 (binding-tier-1 pilot — the actual application of the pattern in proven)
• docudactyl#31 (Wave 3) closing docudactyl#29