From 23a9a36c9c3948cdc4e5682eae733b805f2b0068 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Fri, 9 Oct 2026 19:23:58 +0000 Subject: [PATCH 1/3] docs(issues): draft ParadisEO roadmap issue specs ECH-01..04 Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- issues/README.md | 20 +++++++ issues/echidna-01-pareto-moeo.md | 55 +++++++++++++++++++ issues/echidna-02-cmaes-julia-gnn.md | 52 ++++++++++++++++++ issues/echidna-03-chapel-island-migration.md | 50 +++++++++++++++++ issues/echidna-04-ffi-abi-bridge.md | 56 ++++++++++++++++++++ 5 files changed, 233 insertions(+) create mode 100644 issues/README.md create mode 100644 issues/echidna-01-pareto-moeo.md create mode 100644 issues/echidna-02-cmaes-julia-gnn.md create mode 100644 issues/echidna-03-chapel-island-migration.md create mode 100644 issues/echidna-04-ffi-abi-bridge.md diff --git a/issues/README.md b/issues/README.md new file mode 100644 index 00000000..28f8085b --- /dev/null +++ b/issues/README.md @@ -0,0 +1,20 @@ + + +# Issue specifications + +Drafted issue specifications for the ParadisEO metaheuristic integration roadmap. +Each file is the body for one GitHub issue; the title and labels are in the file header. + +| ID | Repository | File | +|--------|-----------------------|--------------------------------------------------| +| ECH-01 | hyperpolymath/echidna | `echidna-01-pareto-moeo.md` | +| ECH-02 | hyperpolymath/echidna | `echidna-02-cmaes-julia-gnn.md` | +| ECH-03 | hyperpolymath/echidna | `echidna-03-chapel-island-migration.md` | +| ECH-04 | hyperpolymath/echidna | `echidna-04-ffi-abi-bridge.md` | +| PB-01 | hyperpolymath/proof-burrower | `proof-burrower-01-combinatorial-tactic-synthesis.md` (not in this repo) | +| PB-02 | hyperpolymath/proof-burrower | `proof-burrower-02-ledger-fitness-formulation.md` (not in this repo) | +| EB-01 | hyperpolymath/echidnabot | `echidnabot-01-adaptive-ci-portfolio-scheduler.md` (not in this repo) | + +The PB and EB specifications belong to their own repositories and are not included here. diff --git a/issues/echidna-01-pareto-moeo.md b/issues/echidna-01-pareto-moeo.md new file mode 100644 index 00000000..d7422dee --- /dev/null +++ b/issues/echidna-01-pareto-moeo.md @@ -0,0 +1,55 @@ + + +# ECH-01: feat(pareto): integrate exact hypervolume indicator and MOEO non-dominated sorting in verification/pareto.rs + +- **Repository:** hyperpolymath/echidna +- **Labels:** enhancement, area:verification, rust, optimization +- **Area:** Rust / Multi-Objective Search + +## Summary + +`src/rust/verification/pareto.rs` currently computes the Pareto frontier with an O(n²) pairwise dominance check (`ParetoFrontier::compute`) and ranks candidates with a weighted sum (`ParetoFrontier::weighted_rank`). Add: + +1. **Non-dominated sorting** (front-peeling, MOEO-style), so every candidate receives a front rank, not just a frontier/not-frontier flag. +2. **An exact hypervolume indicator** for the four proof-search objectives, so that portfolio results and strategy configurations can be compared by a single quality number that respects Pareto structure. + +## Context + +- `ProofObjective` holds four objectives: `proof_time_ms` (minimise), `trust_level` (maximise, via `TrustLevel::value()`), `memory_bytes` (minimise), `proof_steps` (minimise). +- `ProofCandidate.is_pareto_optimal` is a boolean. Front rank is not stored. +- `weighted_rank` uses inverse-scaled objectives, so it is sensitive to unit choice and to zero handling. Hypervolume requires a consistent minimisation transform, which should be defined in one place. +- `src/rust/verification/pareto_arbiter.rs` is the existing consumer of frontier results. It must be checked before any signature change. +- ParadisEO is referenced only in the roadmap; nothing in the repository depends on it yet. This issue is about the *algorithms* (non-dominated sorting, hypervolume), and does not require vendoring ParadisEO code. + +## Proposed Work + +- Define an explicit minimisation transform: `f = [proof_time_ms, -trust_level, memory_bytes, proof_steps]` (all minimised), with a documented reference point strictly worse than the observed worst on each axis. +- Add `ParetoFrontier::non_dominated_sort(candidates) -> Vec>` returning fronts F₁, F₂, … (O(MN²) acceptable; document complexity). +- Add `ParetoFrontier::hypervolume(points, reference) -> f64` as an **exact** computation: + - 2-D: sweep-line. + - ≥3-D: exact algorithm (e.g. WFG or HSO-style slicing). Monte Carlo estimates are out of scope and must not be labelled "exact". +- Add a `ParetoFrontier::hypervolume_contribution(...)` helper (exclusive hypervolume per candidate) for ranking within a front. +- Keep `compute` and `weighted_rank` public behaviour unchanged, or deprecate them with a note. Do not silently change existing test expectations. +- Keep the module free of network, FFI, or external crate dependencies beyond what `Cargo.toml` already provides. + +## Acceptance Criteria + +- [ ] Non-dominated sorting agrees with the existing `compute` result for front F₁ on the existing test fixtures. +- [ ] Hypervolume matches hand-computed values on known 2-D and 3-D fixtures, including degenerate cases (duplicate points, a point equal to the reference, empty set → 0.0). +- [ ] Property test: adding a non-dominated point never decreases hypervolume; adding a dominated point leaves it unchanged. +- [ ] Hypervolume is invariant under permutation of candidates. +- [ ] Reference point and transform are documented in rustdoc, and the exactness claim is stated precisely. +- [ ] `cargo test` and `cargo clippy` pass for the workspace; no new `unsafe`. +- [ ] Existing `pareto_arbiter.rs` behaviour is unchanged, verified by its tests. + +## Out of Scope + +- Changing the set of objectives or how `TrustLevel` is assigned. +- Wiring hypervolume into the dispatcher. That is a follow-up once the metric is validated. +- Any ParadisEO dependency. + +## Open Questions + +- Should the reference point be fixed (configurable constant) or derived per query? Per-query values make hypervolume values non-comparable across runs. diff --git a/issues/echidna-02-cmaes-julia-gnn.md b/issues/echidna-02-cmaes-julia-gnn.md new file mode 100644 index 00000000..a7f813b7 --- /dev/null +++ b/issues/echidna-02-cmaes-julia-gnn.md @@ -0,0 +1,52 @@ + + +# ECH-02: feat(ml): black-box hyperparameter & temperature calibration for GNN premise rankers via CMA-ES / EDO + +- **Repository:** hyperpolymath/echidna +- **Labels:** enhancement, area:ml, julia, tuning +- **Area:** Julia / Neurosymbolic ML + +## Summary + +Premise rankers used by ECHIDNA's guided search have hyperparameters (learning rate, weight decay, dropout, embedding size, message-passing depth) and a softmax/contrastive **temperature** that are currently set by hand or by grid search. Add a black-box optimiser based on CMA-ES (and, as a comparison baseline, an estimation-of-distribution variant, "EDO") to tune these values against a held-out ranking metric. + +## Context + +- `src/julia/training/train.jl` defines `contrastive_loss(scores, relevant_indices; temperature=0.1f0)`. The temperature is a keyword default with no calibration path. +- `src/julia/run_training.jl`, `run_training_cpu.jl` and `eval_held_out.jl` already contain the training and evaluation entry points. Reuse them; do not fork a second training loop. +- `src/julia/Project.toml` is the dependency manifest, and `src/julia/Manifest.toml` is tracked in git. Adding the optimiser dependency therefore requires updating both files together. The root-level `/Manifest.toml` is git-ignored, but that does not cover `src/julia/`. +- On the Rust side, `src/rust/gnn/guided_search.rs` consumes the ranker scores. Calibrated temperature affects score scale, so calibration must be evaluated on the same score path the Rust side uses. +- The root-level `metrics/` directory (e.g. `MetricsSuite.jl`) contains existing Julia metric code, and `src/chapel/bench_mrr.chpl` computes MRR on the Chapel side. Use the same metric definitions. + +## Proposed Work + +- Add a tuning module (e.g. `src/julia/training/calibration.jl`) with: + - A parameter-space encoding with explicit bounds and log-scale handling for learning rate, weight decay and temperature. + - A CMA-ES objective: validation MRR (or top-k recall) at a fixed budget, with the seed, budget and wall-clock recorded. + - A baseline EDO/univariate EDA optimiser, with the same interface, for comparison. +- Temperature calibration as a separate, cheap, post-hoc step: fit temperature on a validation split by minimising negative log-likelihood of relevant premises, with the ranker frozen. +- Write results (best parameters, trial history, seed, data hash) to a JSON file under `reports/` or a path set by the caller. Do not commit large trial logs. +- Add a `Justfile` recipe for the tuning run, consistent with existing recipes. + +## Acceptance Criteria + +- [ ] Tuning runs end to end on the CPU path with a small budget, from a clean checkout after instantiating the Julia project. +- [ ] Same seed → same best parameters (deterministic given the same data split). +- [ ] Temperature calibration reduces validation NLL relative to the default `0.1f0`, or the issue documents that it does not. +- [ ] Improvement is reported against a fixed-budget random-search baseline, using the same validation split. +- [ ] Held-out test set is never used during tuning; this is checked in code, not only by convention. +- [ ] No change to the default training behaviour unless the tuned config is explicitly loaded. +- [ ] `src/julia/Project.toml` and `src/julia/Manifest.toml` are updated together and the project instantiates cleanly. + +## Out of Scope + +- Changing the GNN architecture or the Rust graph construction. +- Distributed or parallel trial execution (see ECH-03). +- Claims of general accuracy gains beyond the evaluated split. + +## Open Questions + +- Which validation metric is authoritative for the proof-search use case: MRR, top-k recall at the dispatcher's budget, or time-to-proof? +- Is CMA-ES available as a maintained Julia package that is acceptable under the repository's licence policy? Check before adding the dependency. diff --git a/issues/echidna-03-chapel-island-migration.md b/issues/echidna-03-chapel-island-migration.md new file mode 100644 index 00000000..d9cc509c --- /dev/null +++ b/issues/echidna-03-chapel-island-migration.md @@ -0,0 +1,50 @@ + + +# ECH-03: feat(chapel): island-model asynchronous migration topologies & dynamic solver portfolio budget allocation + +- **Repository:** hyperpolymath/echidna +- **Labels:** enhancement, area:parallel, chapel, concurrency +- **Area:** Chapel / Distributed PGAS + +## Summary + +Model parallel proof search as an island model: each island runs a search (a prover portfolio or a search configuration) and periodically migrates its best candidates to neighbouring islands according to a configurable topology. Add asynchronous migration and a dynamic budget allocator that moves compute time between solvers based on observed progress. + +## Context + +- `src/chapel/parallel_proof_search.chpl` is the existing parallel dispatch implementation. `bench_mrr.chpl` and `smoke.chpl` are the existing benchmark and smoke tests. `RESULTS.adoc` and `README.adoc` document current results. +- `src/zig_ffi/chapel_bridge.zig`, `chapel_ffi_exports.h` and `chapel_stubs.c` are the C-ABI boundary. Any new cross-language message type must go through this boundary, not through an ad hoc channel. +- The Rust side is built with `--features chapel` (see `CLAUDE.md`). The feature must still build when Chapel is absent. +- Portfolio logic on the Rust side (`src/rust/verification/portfolio.rs`, `PortfolioConfig`, `PortfolioSolver`) defines solver sets and timeouts. The Chapel budget allocator must not contradict those semantics. Decide which layer owns budgets before writing code. +- Results must be reproducible enough to compare. Record the topology, migration interval, seed and budget schedule with every run. + +## Proposed Work + +- Implement topology options as an enum: ring, 2-D torus, fully connected, and random-k neighbour. Each is a pure function from island id to neighbour set. +- Implement asynchronous migration with `begin`/`sync`-free message passing, or Chapel `sync`/`single` variables. Migration must not block the sending island. Document the chosen concurrency primitive and why. +- Migration policy: send top-k by a configured objective (proof time or trust level) at interval T, with a bounded inbox; drop oldest on overflow and count drops. +- Budget allocator: a bandit-style rule (e.g. successive halving or UCB over solver progress) that reallocates a fixed total budget among solvers. Budget changes are logged. +- Expose topology, interval, k and allocator settings as config fields, with defaults equal to the current single-island behaviour. + +## Acceptance Criteria + +- [ ] With one island (or migration disabled), results match the current `parallel_proof_search.chpl` output on the smoke test. +- [ ] All four topologies have unit tests checking neighbour sets for small N (including edge islands in the torus). +- [ ] Migration never blocks an island for longer than a documented bound in a benchmark run, and dropped-message counts are reported. +- [ ] Total budget is conserved by the allocator (sum of allocations equals the configured total, within a documented rounding rule). +- [ ] Benchmark reports wall-clock, solved count and budget trace for single-island vs. island configurations, on the same problem set. +- [ ] Rust build and tests pass without Chapel installed, and with `--features chapel` where Chapel is available. +- [ ] No new FFI symbols without matching entries in `chapel_ffi_exports.h`. + +## Out of Scope + +- Multi-node deployment and cluster scheduling. +- Changes to individual prover backends. +- Any claim of speed-up that is not backed by the benchmark above. + +## Open Questions + +- Which layer owns solver budgets: the Chapel allocator or `PortfolioConfig` on the Rust side? +- Is a fixed total budget the right model, or should islands also have per-island wall-clock caps? diff --git a/issues/echidna-04-ffi-abi-bridge.md b/issues/echidna-04-ffi-abi-bridge.md new file mode 100644 index 00000000..79d80c6b --- /dev/null +++ b/issues/echidna-04-ffi-abi-bridge.md @@ -0,0 +1,56 @@ + + +# ECH-04: feat(ffi): C-ABI / Zig bridge specification for embedding ParadisEO metaheuristics engine with Idris2 contracts + +- **Repository:** hyperpolymath/echidna +- **Labels:** enhancement, area:abi, zig, idris2, ffi +- **Area:** ABI / FFI / Multi-Language + +## Summary + +Write the specification for a C-ABI boundary through which a metaheuristics engine (ParadisEO or a compatible implementation) can be called from ECHIDNA's Rust core, with the Zig layer as the bridge and Idris2 providing the contracts. This issue is a **specification and a minimal proof-of-boundary**, not a full integration. + +## Context + +- `src/abi/` holds the Idris2 ABI (`echidnaabi.ipkg`, `EchidnaABI/`, `Types.idr`, `Layout.idr`, and per-subsystem `*Foreign.idr` modules such as `CoprocessorForeign.idr`, `OverlayForeign.idr`, `TentaclesForeign.idr`). +- `ffi/zig/` (`build.zig`, `src/main.zig`, `src/boj.zig`, `src/capnp_bridge.zig`, `src/provers/`) and `src/zig_ffi/` (`chapel_bridge.zig`, `chapel_ffi_exports.h`) are the existing Zig bridges. +- `CLAUDE.md` states that Idris2 ABI modules must have zero `believe_me`, zero postulates and zero admits, enforced by `idris2-abi-ci.yml`. The specification must satisfy the same gate. +- The Rust side has an existing `src/rust/ffi/` module. Reuse its conventions for pointer ownership and error codes. +- No ParadisEO code is present in the repository. Its licence must be checked before any source or binary is vendored or linked. + +## Proposed Work + +1. **Specification document** (`docs/design/` or `src/abi/`, consistent with existing ABI docs) defining: + - The minimal call surface: create engine, configure (algorithm id, parameters, seed), step / run with budget, query best solutions, destroy. + - Data layout for objective vectors and candidate identifiers, with explicit sizes and alignment, and a version field. + - Ownership rules: who allocates, who frees, lifetimes across the boundary. + - Error model: integer status codes mapped to a closed Idris2 sum type. +2. **Idris2 contracts** in `src/abi/` (new module, e.g. `MetaheuristicsForeign.idr`): + - Total functions for layout size/alignment computation. + - Proofs that status-code mapping is total and that every handle is destroyed at most once (typed handle state, or a linear-style discipline if supported by the Idris2 version in use). + - No `believe_me`, postulates or admits. +3. **Zig bridge skeleton** in `ffi/zig/src/` exporting the specified symbols with a stub implementation (no external engine linked). Symbols must match the Idris2 declarations exactly. +4. **Rust side**: an `extern "C"` declaration module plus a test that calls the stub through the bridge and checks the status-code round-trip. + +## Acceptance Criteria + +- [ ] Specification states every exported symbol, its C signature, ownership and error behaviour. +- [ ] `idris2` type-checks the new ABI module with zero holes, zero `believe_me`, zero postulates and zero admits. +- [ ] Layout proofs cover the objective-vector record: size and alignment match the Zig `extern struct` and the Rust `#[repr(C)]` type (checked by a test or static assertion). +- [ ] Zig build (`ffi/zig/build.zig`) produces the stub library; `zig build test` passes. +- [ ] Rust test links the stub and round-trips at least one call per status code. +- [ ] Existing `idris2-abi-ci.yml` gate passes. +- [ ] No ParadisEO source or binary is added to the repository. + +## Out of Scope + +- Linking a real ParadisEO build. +- Cross-language memory sharing beyond the specified layouts. +- Performance tuning of the boundary. + +## Open Questions + +- Is ParadisEO's licence compatible with the repository's MPL-2.0 licence for linking, and does that affect whether the bridge can ship in-tree? +- Should the engine boundary reuse the existing `ffi/zig` naming, or live in a new `ffi/metaheuristics/` directory? From 9a6d2dbb7fe2cc2eb5bca36e15371e249840f259 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Fri, 9 Oct 2026 19:36:05 +0000 Subject: [PATCH 2/3] docs(issues): add PB and EB issue specs; README index Draft PB-01 and PB-02 (hyperpolymath/proof-burrower) and EB-01 (hyperpolymath/echidnabot) in the same format as ECH-01..04. Claims about the sibling repos are marked [unverified]: they come from a read-only look at proof-burrower@be897dd and echidnabot@ae52833. Update the README index with the GitHub issue numbers for ECH-01..04, the body-extraction command, the provenance note, and the labels the target repos are missing. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- issues/README.md | 52 ++++++++++++---- ...abot-01-adaptive-ci-portfolio-scheduler.md | 57 +++++++++++++++++ ...rower-01-combinatorial-tactic-synthesis.md | 62 +++++++++++++++++++ ...-burrower-02-ledger-fitness-formulation.md | 61 ++++++++++++++++++ 4 files changed, 221 insertions(+), 11 deletions(-) create mode 100644 issues/echidnabot-01-adaptive-ci-portfolio-scheduler.md create mode 100644 issues/proof-burrower-01-combinatorial-tactic-synthesis.md create mode 100644 issues/proof-burrower-02-ledger-fitness-formulation.md diff --git a/issues/README.md b/issues/README.md index 28f8085b..60cf54ec 100644 --- a/issues/README.md +++ b/issues/README.md @@ -7,14 +7,44 @@ SPDX-License-Identifier: CC-BY-SA-4.0 Drafted issue specifications for the ParadisEO metaheuristic integration roadmap. Each file is the body for one GitHub issue; the title and labels are in the file header. -| ID | Repository | File | -|--------|-----------------------|--------------------------------------------------| -| ECH-01 | hyperpolymath/echidna | `echidna-01-pareto-moeo.md` | -| ECH-02 | hyperpolymath/echidna | `echidna-02-cmaes-julia-gnn.md` | -| ECH-03 | hyperpolymath/echidna | `echidna-03-chapel-island-migration.md` | -| ECH-04 | hyperpolymath/echidna | `echidna-04-ffi-abi-bridge.md` | -| PB-01 | hyperpolymath/proof-burrower | `proof-burrower-01-combinatorial-tactic-synthesis.md` (not in this repo) | -| PB-02 | hyperpolymath/proof-burrower | `proof-burrower-02-ledger-fitness-formulation.md` (not in this repo) | -| EB-01 | hyperpolymath/echidnabot | `echidnabot-01-adaptive-ci-portfolio-scheduler.md` (not in this repo) | - -The PB and EB specifications belong to their own repositories and are not included here. +To produce an issue body from a file (everything after the `# ` title line, without the SPDX header): + +```sh +awk 'f;/^# /{f=1}' issues/ | sed '1{/^$/d}' > /tmp/body.md +``` + +| ID | Repository | GitHub issue | File | +|--------|------------------------------|--------------|-------------------------------------------------------| +| ECH-01 | hyperpolymath/echidna | #420 | `echidna-01-pareto-moeo.md` | +| ECH-02 | hyperpolymath/echidna | #421 | `echidna-02-cmaes-julia-gnn.md` | +| ECH-03 | hyperpolymath/echidna | #422 | `echidna-03-chapel-island-migration.md` | +| ECH-04 | hyperpolymath/echidna | #424 | `echidna-04-ffi-abi-bridge.md` | +| PB-01 | hyperpolymath/proof-burrower | not filed | `proof-burrower-01-combinatorial-tactic-synthesis.md` | +| PB-02 | hyperpolymath/proof-burrower | not filed | `proof-burrower-02-ledger-fitness-formulation.md` | +| EB-01 | hyperpolymath/echidnabot | not filed | `echidnabot-01-adaptive-ci-portfolio-scheduler.md` | + +#423 on hyperpolymath/echidna is unrelated to this roadmap. + +## Status + +- **ECH-01..04** are filed on hyperpolymath/echidna. Their GitHub bodies and labels still need to be synchronised from these files; only `enhancement` is attached. +- **PB-01, PB-02, EB-01** are drafts for copying to their own repositories. They are not filed. + +## Provenance of the PB and EB drafts + +The PB and EB specifications were written from this repository. Statements about +proof-burrower and echidnabot are marked *[unverified]*: they come from a read-only look +at `proof-burrower@be897dd` and `echidnabot@ae52833`, and were not built, run or confirmed +by those repositories' maintainers. Re-check them against the current code before filing. +Statements about echidna were checked against echidna `main` at `7fd369d`. + +## Labels missing in the target repositories + +Labels named in the drafts that did not exist when they were written (checked 2026-10-09): + +| Repository | Missing labels | +|------------------------------|---------------------------------------------------------------------| +| hyperpolymath/proof-burrower | `area:swarm`, `rust`, `search-tactics`, `area:ledger`, `heuristics` | +| hyperpolymath/echidnabot | `area:dispatcher`, `ci-optimization` (`rust` exists) | + +All labels used by ECH-01..04 exist on hyperpolymath/echidna. diff --git a/issues/echidnabot-01-adaptive-ci-portfolio-scheduler.md b/issues/echidnabot-01-adaptive-ci-portfolio-scheduler.md new file mode 100644 index 00000000..feaa2f49 --- /dev/null +++ b/issues/echidnabot-01-adaptive-ci-portfolio-scheduler.md @@ -0,0 +1,57 @@ + + +# EB-01: feat(dispatcher): adaptive portfolio timeout and solver selection scheduling for CI PR gates + +- **Repository:** hyperpolymath/echidnabot +- **Labels:** enhancement, area:dispatcher, rust, ci-optimization +- **Area:** Rust / Scheduling / Algorithm Selection +- **Provenance:** Drafted from hyperpolymath/echidna. Claims about echidnabot are marked *[unverified]*: they come from a read-only look at `echidnabot@ae52833` and have not been built, run or checked by a maintainer. Claims about echidna were checked against echidna `main` at `7fd369d`. + +## Summary + +For each push or PR event, echidnabot enqueues one job per enabled prover, each with a static timeout. Add an **adaptive scheduler** that uses recorded run history to (1) choose per-prover timeouts from observed runtime distributions and (2) order or select solvers for a PR gate, so the gate reaches a verdict faster within a fixed compute budget. The verdict rules and trust semantics stay the same. + +## Context + +- *[unverified]* `src/api/webhooks.rs::enqueue_repo_jobs` loops over `repo.enabled_provers` and creates one `ProofJob` per prover with the event's `JobPriority` (`High` for PR checks). There is no per-prover ordering and no selection. +- *[unverified]* `src/scheduler/` contains `JobScheduler` (a priority-ordered queue), `JobLimiter` (global limit 10 and per-repo limit 3 by default) and `retry.rs` (exponential backoff and a circuit breaker for transient errors). None of these use historical runtimes. +- *[unverified]* Timeouts are static: `EchidnaConfig.timeout_secs` (default 300), `ExecutorConfig.timeout_secs` (default 300) and the Podman executor default of 300 s. +- *[unverified]* `src/modes/manifest.rs` parses a per-prover `timeout_seconds` (`[provers.]`). Its doc comment says it falls back to `[scheduler] job_timeout_seconds`, but `SchedulerConfig` has only `max_concurrent` and `queue_size`. In the source examined, the per-prover value appears only in manifest parsing and tests. Confirm whether it is wired into dispatch before building on it. +- *[unverified]* History is already stored. In SQLite, `proof_jobs` holds prover, status and timestamps, `proof_results` holds `duration_ms` and success, and `tactic_outcomes` holds prover, goal fingerprint, tactic, success and `duration_ms`. +- *[unverified]* Regulator mode gates merges on a coverage percentage (`regulator_coverage_threshold`). Verified in echidna: `.machine_readable/bot_directives/echidnabot.a2ml` sets `mode = "regulator"` and `coverage-threshold = 90`, and `.echidnabot.toml` sets `[verification] timeout_secs = 300` with per-prover `priority` hints (`idris2` high, `z3`/`cvc5` medium, `coq`/`lean` low). +- Verified in echidna: `src/rust/verification/portfolio.rs` (`PortfolioConfig`) already models solver sets per problem class (SMT / ATP / ITP), a per-solver timeout (300 s) and a `wait_factor` (2.0) for cross-checking. echidnabot's scheduler should use compatible terminology and must not contradict these semantics. ECH-03 (#422) covers budget allocation on the echidna side. Decide which layer owns which budget before implementing. +- Verified in echidna: a `timeout` status in `echidna.prove.result/1` means "budget ran out; retry with a larger `--timeout`". It is not a failure, and the scheduler must keep that distinction. + +## Proposed Work + +- **Runtime model.** For each `(repo, prover)` (optionally also per file-path bucket), keep an empirical runtime distribution of successful runs from `proof_results` / `proof_jobs`. Use a robust quantile estimate (for example P90 or P95) with a minimum sample count, and fall back to the static timeout when history is too short. +- **Adaptive timeout.** `timeout = clamp(q_p * margin, floor, ceiling)`, where `ceiling` is the configured static timeout, so adaptation can only **shorten** waiting on known-fast provers and never makes an existing gate stricter. A timeout under the adaptive limit triggers one retry at the static ceiling before it is reported, so tightening never creates a new failure. +- **Solver ordering and selection for PR gates.** Order jobs by expected time-to-verdict (success probability ÷ expected runtime, from history). Where the repo's config marks provers as interchangeable for a goal class, allow "first verified wins" with cancellation of the rest. Otherwise run all required provers, because coverage gating needs them. Default: ordering only, with no skipping. +- **Exploration.** Use a small, configurable exploration rate (for example ε-greedy or UCB) so that rarely chosen provers keep current statistics. It is off by default for regulator-mode repos. +- **Config.** Add a new `[scheduler.adaptive]` section (enabled, quantile, margin, floor, min_samples, exploration). It is disabled by default. Also fix or wire up the `job_timeout_seconds` doc/code mismatch noted above. +- **Observability.** Log the chosen timeout, its source (adaptive or static) and the ordering rationale in the job record and the check-run summary. + +## Acceptance Criteria + +- [ ] With `[scheduler.adaptive]` disabled, job creation, timeouts and verdicts are unchanged (existing tests pass without modification). +- [ ] An adaptive timeout never exceeds the configured static timeout, and never goes below `floor` (property test). +- [ ] A job that times out under an adaptive timeout is retried once at the static ceiling before a `timeout` verdict is reported. The test uses a stub executor. +- [ ] With fewer than `min_samples` history rows, the static timeout is used, and the reported source says so. +- [ ] Regulator-mode coverage percentages are computed over the same set of required provers as before. Ordering changes never change which provers count towards coverage. +- [ ] Replaying a recorded job history in a simulation shows lower median time-to-verdict, with an identical verdict on every replayed job. Attach the simulation script and results to the PR. +- [ ] `cargo test` and `cargo clippy` pass for the workspace; no new `unsafe`; no new external service dependency. + +## Out of Scope + +- Changing echidna's prover backends, the `echidna.prove.result/1` contract, or echidna-side portfolio reconciliation. +- Learned (neural) algorithm selection. Start with statistics only. +- Changing regulator thresholds or mode resolution. +- Multi-tenant fairness across repositories beyond what `JobLimiter` already does *[unverified]*. + +## Open Questions + +- Which layer owns per-solver budgets: echidnabot's scheduler, echidna's `PortfolioConfig`, or the ECH-03 Chapel allocator? One owner is needed to avoid conflicting timeouts. +- Is "first verified wins" ever acceptable under regulator mode, or must every enabled prover always run? +- Should runtime history be keyed by file-path bucket, or by goal fingerprint (`tactic_outcomes.goal_fingerprint` *[unverified]*)? Fingerprints are more precise but sparser. diff --git a/issues/proof-burrower-01-combinatorial-tactic-synthesis.md b/issues/proof-burrower-01-combinatorial-tactic-synthesis.md new file mode 100644 index 00000000..42c9b151 --- /dev/null +++ b/issues/proof-burrower-01-combinatorial-tactic-synthesis.md @@ -0,0 +1,62 @@ + + +# PB-01: feat(swarm): combinatorial tactic playbook synthesis using delta/partial neighborhood evaluation (ParadisEO-mo) + +- **Repository:** hyperpolymath/proof-burrower +- **Labels:** enhancement, area:swarm, rust, search-tactics +- **Area:** Rust / Local Search over Tactic Scripts +- **Provenance:** Drafted from hyperpolymath/echidna. Claims about proof-burrower are marked *[unverified]*: they come from a read-only look at `proof-burrower@be897dd` and have not been built, run or checked by a maintainer. Claims about echidna were checked against echidna `main` at `7fd369d`. + +## Summary + +Today each specialist's playbook is a fixed, hand-written list of single tactic scripts that is tried in order. Add a **local-search synthesiser** that builds composite tactic scripts (sequences and combinators of existing `TacticTemplate`s) by exploring a neighbourhood of moves. Use the ParadisEO-MO idea of **delta (incremental) evaluation**: score a neighbour from cached ledger outcomes and cheap partial checks wherever possible, and pay for a full `echidna prove` call only when that is unavoidable. + +## Context + +- *[unverified]* `crates/burrower-core/src/attempt.rs` defines `TacticTemplate { name, script, description }` and `Playbook { specialist, tactics: Vec }`. `run_playbook` tries every tactic in order, writes one probe file per tactic (`generate_probe`, an Isabelle theory that `imports Main`), and runs `run_probe` for each. +- *[unverified]* `crates/burrower-core/src/specialist.rs` has three built-in specialists (`Algebraist`, `OrderTheorist`, `Combinatorialist`), each with a static `playbook()`. `Swarm::attempt_all` skips specialists below `SWARM_RELEVANCE_THRESHOLD` (0.02) and runs each remaining playbook in full. There is no early exit after the first success, no reordering and no composition. +- *[unverified]* Some playbook entries are already hand-made composites (for example `by (simp; linarith)` and `by (transfer, simp add: algebra_simps)`). This shows that combinators are useful, but they are not generated. +- *[unverified]* `AttemptResult` has the variants `Succeeded { duration_ms, receipt }`, `Failed { error, duration_ms }`, `Timeout` and `Skipped { reason }`. `Timeout` carries no duration. +- *[unverified]* `derive_learning` records successes as `positive` learnings and failures as `anti-pattern` learnings in the ledger. Failures are sorted into `undefined-reference`, `tactic-mismatch`, `structural-mismatch` and `generic-failure`. These classes can drive move selection. +- Verified in echidna: probes are checked by `echidna prove`, which can emit one `echidna.prove.result/1` JSON line (`docs/PROVE-RESULT-CONTRACT.adoc`). Its `status` is one of `verified`, `failed`, `error`, `timeout`, `unknown`, and it includes `duration_ms` and `trust.axioms`. The contract has **no partial-progress field** (for example, remaining subgoals). Any partial evaluation that needs subgoal counts would either need a new, additive contract field in echidna or have to parse prover output inside proof-burrower. +- ParadisEO is referenced only in the roadmap. This issue is about the *algorithms* (neighbourhoods, delta evaluation, local search). It does not require a C++ ParadisEO dependency. + +## Proposed Work + +- **Solution representation.** A candidate is a short sequence of tactic steps joined by combinators (`;`, `,`, `<|>`-style fallback where the prover supports it). Each step is drawn from the specialist's existing `TacticTemplate`s plus their simplifier-set variants. Cap the length (for example ≤ 3 steps) so the space stays small. +- **Neighbourhood moves.** Define these as pure functions: insert a step, delete a step, swap adjacent steps, replace a step's tactic, add or remove a simp-set argument. Each move must have a stable textual identity, so results can be cached. +- **Delta / partial evaluation, cheapest first:** + 1. *Ledger lookup:* if `(goal_id, script)` already has a recorded outcome, reuse it at no prover cost. + 2. *Anti-pattern pruning:* reject neighbours whose prefix matches a recorded `anti-pattern` learning for this specialist and goal shape. + 3. *Prefix evaluation (optional, behind a flag):* when a prefix's outcome is known to fail with `tactic-mismatch`, skip all extensions of that prefix. + 4. *Full evaluation:* run `run_probe` only for surviving neighbours, within a per-goal prover-call budget. +- **Search driver.** Use first-improvement hill climbing with a tabu list over move identities, plus an iteration cap and a prover-call cap. Stop on the first `Succeeded`. Make the driver deterministic for a given seed. +- **Fitness.** Lexicographic: (1) verified beats everything else; (2) fewer `trust.axioms`; (3) shorter script; (4) lower `duration_ms`. Treat `Timeout` and `Skipped` as the worst values and never count them as evidence that a tactic is wrong. +- **Ledger.** Record each synthesised attempt the same way `run_playbook` already does. Put the move trace in `extra` so that later runs can replay or prune it. +- **CLI.** Add an opt-in flag on `burrower attempt` (for example `--synthesise --budget N`). Default behaviour stays the same. + +## Acceptance Criteria + +- [ ] With `--synthesise` off, `burrower attempt` output and ledger records are byte-for-byte unchanged on the existing tests. +- [ ] Unit tests for every move operator, including empty-sequence and maximum-length edge cases. +- [ ] Delta evaluation is tested with a stub prover: a neighbour whose `(goal_id, script)` is already in the ledger triggers **no** prover call, and the stub's call count proves it. +- [ ] The prover-call budget is a hard limit: the stub prover is never called more than `N` times per goal. +- [ ] The search is deterministic for a fixed seed and a fixed ledger. +- [ ] `Timeout` and `Skipped` outcomes never create `anti-pattern` learnings through the synthesiser. +- [ ] On a fixed goal set where a known composite closes a goal that no single playbook tactic closes, the synthesiser finds it within the budget. Record the goal set and results in the PR. +- [ ] `cargo test` and `cargo clippy` pass for the workspace; no new `unsafe`; no new network dependency. + +## Out of Scope + +- Changing echidna's `echidna.prove.result/1` contract. If subgoal counts are needed, file a separate echidna issue for an additive field. +- Provers other than the ones proof-burrower already targets (Isabelle probes today *[unverified]*). +- Learned (neural) move selection. That belongs to the GNN/ranking roadmap. +- Any ParadisEO C++ dependency. + +## Open Questions + +- Should synthesised scripts that succeed be added back to the specialist's static playbook, or stay only in the ledger? +- What per-goal prover-call budget is acceptable in CI and locally? It drives the useful neighbourhood size. +- Is prefix evaluation sound for every combinator? (`;` applies to all subgoals and `,` sequences, so a failing prefix does not always mean a failing extension under fallback combinators.) diff --git a/issues/proof-burrower-02-ledger-fitness-formulation.md b/issues/proof-burrower-02-ledger-fitness-formulation.md new file mode 100644 index 00000000..ae3cfa05 --- /dev/null +++ b/issues/proof-burrower-02-ledger-fitness-formulation.md @@ -0,0 +1,61 @@ + + +# PB-02: feat(ledger): anti-pattern mining and objective fitness formulation from burrow.jsonl for heuristic guidance + +- **Repository:** hyperpolymath/proof-burrower +- **Labels:** enhancement, area:ledger, rust, heuristics +- **Area:** Rust / Ledger Analytics / Search Heuristics +- **Provenance:** Drafted from hyperpolymath/echidna. Claims about proof-burrower are marked *[unverified]*: they come from a read-only look at `proof-burrower@be897dd` and have not been built, run or checked by a maintainer. Claims about echidna were checked against echidna `main` at `7fd369d`. + +## Summary + +The Burrow Ledger (`burrow.jsonl`, append-only JSON Lines) records every reading and attempt, but it is read only through simple filters (`recent`, `by-specialist`, `anti-patterns`, `digest`). Add (1) **anti-pattern mining**, which aggregates the raw per-attempt learnings into ranked, support-counted rules, and (2) a documented **objective fitness function** computed from ledger records. Together they give the swarm (and the PB-01 synthesiser) a single, consistent signal for ordering and pruning tactics. + +## Context + +- *[unverified]* `crates/burrower-core/src/ledger.rs` defines `LedgerRecord { id, timestamp, goal_hash, goal_id?, goal_excerpt, specialist, approach?, result?, learning?, extra }`. `Ledger` is a file handle with `append`, `read_all`, `query`, `recent`, `by_specialist`, `by_goal_hash` and `anti_patterns_for`. +- *[unverified]* `anti_patterns_for` returns every `Learning` with `pattern_kind == "anti-pattern"` that is visible to the specialist. There is no de-duplication, counting, recency weighting or confidence. One failure and a hundred failures look the same. +- *[unverified]* `RecordResult.status` is documented as `succeeded | failed | partial | abandoned | proposed`. However, `run_playbook` writes `AttemptResult::status_string()`, which also produces `timeout` and `skipped`. Those values are outside the documented set. A miner must handle every value that is actually written, and the doc comment should be fixed. +- *[unverified]* `Learning.pattern_kind` is documented as `positive | anti-pattern | specialisation | boundary`. The oracle path writes `oracle-counter-example` (`crates/burrower-core/src/oracle.rs` module docs), which is also outside the documented set. +- *[unverified]* `goal_hash` is a 16-hex-character non-cryptographic hash. `goal_id` (a UUIDv8 content id) is present only on records written since 2026-10-05. Grouping must prefer `goal_id` and fall back to `goal_hash`. +- *[unverified]* `read_all` skips malformed lines with a warning on stderr. Mining must keep that tolerance and report the skipped count. +- *[unverified]* Successful attempts may carry an `echidna.prove.result/1` receipt in `extra` (`receipt_extra`). Verified in echidna: that receipt's `trust.axioms` lists escape hatches (`sorry`, `Admitted`, ...), and `trust.confidence` is `null` unless it is receipt-backed (`docs/PROVE-RESULT-CONTRACT.adoc`, "Receipt, not warrant"). Fitness must not treat a `null` confidence as zero or as one. + +## Proposed Work + +- **Normalised view.** Add a pure function that maps a `LedgerRecord` to an `Observation { goal_key, specialist, tactic_script, outcome, failure_class?, duration_ms?, axioms?, timestamp }`. `outcome` covers every status that is actually written (`succeeded`, `failed`, `timeout`, `skipped`, plus the documented ones). Unknown values map to `Other(String)` and are never dropped silently. +- **Anti-pattern mining.** Aggregate observations into rules `(specialist, tactic_script, failure_class, goal-shape feature) → {failures, successes, last_seen}`. Rank them with a smoothed failure rate (for example a Beta prior, or a Wilson lower bound), with optional exponential recency decay. Expose `Ledger::mine_anti_patterns(&MiningConfig) -> Vec`. +- **Goal-shape feature.** Start simple and deterministic: the specialist's domain plus the set of keyword hits already computed by `Specialist::read`/`relevance` *[unverified]*. Do not add learned embeddings in this issue. +- **Fitness formulation.** Document and implement `fitness(observations for (goal_key, script)) -> Fitness` as a lexicographic tuple, consistent with PB-01: + 1. verified (yes/no); + 2. axiom count from the receipt (fewer is better; unknown is ranked below known-zero); + 3. script length; + 4. median `duration_ms`. + `Timeout` and `Skipped` count as "no information" for correctness and as worst-case for time. They must not raise the failure rate. +- **CLI.** Add `burrower ledger mine [--min-support K] [--decay HALF_LIFE]` and `burrower ledger fitness --goal `. Use human-readable output by default and add a `--json` option. +- **Doc fix.** Update the `RecordResult.status` and `Learning.pattern_kind` doc comments to list every value that is actually written. + +## Acceptance Criteria + +- [ ] The normaliser is tested against a fixture ledger that includes every status and pattern kind actually written, plus legacy records without `goal_id`, plus one malformed line. +- [ ] Mining is deterministic and order-independent: shuffling ledger lines gives the same rules in the same order (ties broken by a documented key). +- [ ] A rule with one failure never ranks above a rule with many failures and the same failure rate (support is respected). +- [ ] `Timeout` and `Skipped` observations do not change a rule's failure rate (property test). +- [ ] Fitness ordering matches hand-computed expectations on fixtures, including `null` confidence and missing receipts. +- [ ] The existing `ledger recent | by-specialist | anti-patterns | digest` output is unchanged. +- [ ] `cargo test` and `cargo clippy` pass for the workspace; no new `unsafe`; the ledger file format is unchanged (read-only analytics). + +## Out of Scope + +- Changing the on-disk ledger schema or rewriting existing records. +- Using mined rules to change playbooks automatically. PB-01 consumes them, and humans decide on promotion. +- Cross-repo ledger aggregation (for example with echidnabot's `tactic_outcomes` table *[unverified]*). +- ML-based pattern extraction. + +## Open Questions + +- Should mined rules be cached in a sidecar file, or recomputed on every run? This depends on typical ledger size, which is unknown. +- Which recency half-life is reasonable when prover versions change (for example Isabelle releases that rename facts)? +- Should `skipped` caused by a missing prover binary be filtered out completely rather than counted as "no information"? From e06fd1439d3878d792050a421cfd7bed30afa8a0 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Fri, 9 Oct 2026 19:57:04 +0000 Subject: [PATCH 3/3] docs(handover): ParadisEO roadmap continuation prompt; issue sync script Add docs/handover/PARADISEO-ROADMAP-PROMPT.adoc, a self-contained brief for the next agent: branch and issue state, ground rules, and work packages WP0-WP6 (issue-body reconciliation, ECH-01 hypervolume, #408 Chapel link failure, budget-ownership ADR, the prove-result field hazard with echidnabot's deny_unknown_fields parser, ECH-04, ECH-02/03). Add scripts/issues/sync-roadmap-issues.sh (bash): syncs #420-#424 bodies and labels from issues/, dry run by default, verifies afterwards, and refuses to replace hand-edited bodies without --overwrite. Index the prompt in HANDOVER-INDEX.adoc and record in issues/README.md that the live bodies were edited by hand and differ from the specs. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- docs/handover/HANDOVER-INDEX.adoc | 4 + docs/handover/PARADISEO-ROADMAP-PROMPT.adoc | 258 ++++++++++++++++++++ issues/README.md | 2 +- scripts/issues/sync-roadmap-issues.sh | 150 ++++++++++++ 4 files changed, 413 insertions(+), 1 deletion(-) create mode 100644 docs/handover/PARADISEO-ROADMAP-PROMPT.adoc create mode 100755 scripts/issues/sync-roadmap-issues.sh diff --git a/docs/handover/HANDOVER-INDEX.adoc b/docs/handover/HANDOVER-INDEX.adoc index a2beb31b..4987218a 100644 --- a/docs/handover/HANDOVER-INDEX.adoc +++ b/docs/handover/HANDOVER-INDEX.adoc @@ -32,6 +32,10 @@ backends (Wave-2 follow-on) |Wave-2 done |~1 sprint |link:SUGGEST-CLI-PROMPT.adoc[`+SUGGEST-CLI-PROMPT.adoc+`] |`+suggest+` verb implementation |None |~3 days + +|link:PARADISEO-ROADMAP-PROMPT.adoc[`+PARADISEO-ROADMAP-PROMPT.adoc+`] +|ParadisEO roadmap (ECH-01..04, #408, budget-ownership ADR) |Owner picks +canonical issue bodies (WP0) |WP1 ~2 days; others vary |=== === Active runbooks (live workstream is in production) diff --git a/docs/handover/PARADISEO-ROADMAP-PROMPT.adoc b/docs/handover/PARADISEO-ROADMAP-PROMPT.adoc new file mode 100644 index 00000000..b6e87554 --- /dev/null +++ b/docs/handover/PARADISEO-ROADMAP-PROMPT.adoc @@ -0,0 +1,258 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) += ParadisEO roadmap: continuation prompt +:revdate: 2026-10-09 +:toc: macro + +*What this is.* A self-contained brief for the next coding agent working on +the ParadisEO metaheuristic roadmap (ECH-01..04) and the work around it. Read +it fully before changing anything. Facts are dated 2026-10-09 and were checked +against the commits named below. Re-check anything you rely on. + +toc::[] + +== 1. State on 2026-10-09 + +=== Branches + +[cols="1,1,3",options="header"] +|=== +| Branch | Head | Contents +| `main` | `7fd369d` | Base. No roadmap files. +| `arena/16d27c7e-echidna` | `23a9a36` | `issues/` with ECH-01..04 specs and README. +| `arena/9aef7602-echidna` | ahead of `23a9a36` | Adds the PB/EB specs, the README index, `scripts/issues/sync-roadmap-issues.sh` and this file. Fast-forward of the branch above. +|=== + +The owner may fast-forward `arena/16d27c7e-echidna` to the head of +`arena/9aef7602-echidna`. Work on whichever branch the owner names. Never force-push. + +=== Specs (`issues/`) + +[cols="1,2,1,3",options="header"] +|=== +| ID | Repository | GitHub | File +| ECH-01 | hyperpolymath/echidna | #420 | `issues/echidna-01-pareto-moeo.md` +| ECH-02 | hyperpolymath/echidna | #421 | `issues/echidna-02-cmaes-julia-gnn.md` +| ECH-03 | hyperpolymath/echidna | #422 | `issues/echidna-03-chapel-island-migration.md` +| ECH-04 | hyperpolymath/echidna | #424 | `issues/echidna-04-ffi-abi-bridge.md` +| PB-01 | hyperpolymath/proof-burrower | not filed | `issues/proof-burrower-01-combinatorial-tactic-synthesis.md` +| PB-02 | hyperpolymath/proof-burrower | not filed | `issues/proof-burrower-02-ledger-fitness-formulation.md` +| EB-01 | hyperpolymath/echidnabot | not filed | `issues/echidnabot-01-adaptive-ci-portfolio-scheduler.md` +|=== + +#423 is unrelated (CI checkers in bash+jq). Do not touch it. + +=== Live GitHub issues: two body texts exist + +* All four ECH issues have the right labels (checked 2026-10-09 ~20:00 UTC): + #420 `enhancement, rust, area:verification, optimization`; #421 + `enhancement, area:ml, julia, tuning`; #422 `enhancement, area:parallel, + chapel, concurrency`; #424 `enhancement, area:abi, zig, idris2, ffi`. +* Their bodies were *replaced by hand* at 19:51–19:52 UTC with a different + text (starting `**ID:** ECH-0n`, `**Target Repository:**`). It is not the + committed spec. Problems in that text, checked against the code: +** ECH-01 names an objective `proof_size_nodes`. `pareto.rs` has `proof_steps`. +** All four link to `../ROADMAP-PARADISEO.md`, which does not exist. +** ECH-01 cites `tests/pareto_tests.rs`, which does not exist (`proptest` is a + dev-dependency, so property tests are possible). +** ECH-01 proposes adding hypervolume and front rank to `echidna.prove.result/1`. + That would break echidnabot (see <>), and the committed + spec lists wiring hypervolume into output as out of scope. +* The committed spec and the live text must be reconciled by the *owner*. + Do not overwrite the live bodies without the owner's explicit decision. + +=== GitHub permissions seen in earlier sessions + +Issue writes from the Arena integration returned `403 Resource not accessible +by integration`; `git push` worked. If you hit the same 403, stop and report. +Do not look for tokens. + +== 2. Ground rules (from `CLAUDE.md`, `.claude/CLAUDE.md` and practice) + +* *No Python anywhere in the repo* (estate ban). Use Rust for systems, Julia + for data or batch, bash+jq for small CI scripts. +* SPDX header on every new file: `MPL-2.0` for code, `CC-BY-SA-4.0` for docs. +* Conventional commits (`feat(pareto): ...`, `docs(decisions): ...`), atomic. +* Docs are AsciiDoc (`.adoc`). `issues/*.md` is Markdown on purpose (GitHub bodies). +* Rust toolchain is pinned in `rust-toolchain.toml` (1.99.0, with clippy and rustfmt). +* `--features chapel` must still build when Chapel is absent. +* No new crates without a stated reason. ECH-01 needs none. +* Do not claim speed-ups, exactness or guarantees that a test does not back. +* `rust-ci.yml` runs on `pull_request` and on pushes to `main`/`master` only. + A push to a feature branch alone runs no Rust CI. If you cannot run + `cargo` locally, you need a draft PR (ask the owner first). +* Do not open PRs, file issues or create labels in other repos without the owner's say-so. + +Local checks (when a toolchain is available): + +[source,sh] +---- +cargo fmt --all -- --check # as rust-ci.yml +cargo clippy --locked --workspace --all-targets -- -D warnings # as rust-ci.yml +cargo test --locked --workspace --all-targets # as rust-ci.yml +cargo test --lib verification::pareto # fast loop +cargo test --lib agent::meta_controller +just check # fmt-check + lint + test roll-up +---- + +== 3. Work packages, in recommended order + +Each package is independent unless it says otherwise. Do one per PR. + +=== WP0: Reconcile and sync issue bodies (owner decision first) + +* Ask the owner which text is canonical for #420–#424: the committed specs + in `issues/`, the hand-edited live bodies, or a merge. +* If the specs win, run the sync script. It defaults to a dry run, refuses to + replace hand-edited bodies, and verifies afterwards: ++ +[source,sh] +---- +scripts/issues/sync-roadmap-issues.sh # dry run +scripts/issues/sync-roadmap-issues.sh --apply --overwrite # only with owner approval +scripts/issues/sync-roadmap-issues.sh --verify +---- +* If the live text wins, fix the factual problems listed in section 1 in + the specs too, so the repo and GitHub agree. +* Then update the "Status" section of `issues/README.md`. + +=== WP1: ECH-01: non-dominated sorting and exact hypervolume (`pareto.rs`) + +Spec: `issues/echidna-01-pareto-moeo.md`. This is the best first coding task: +pure Rust, no new dependencies, one small module. + +Current code (`src/rust/verification/pareto.rs`, 247 lines, `main@7fd369d`): + +* `ProofObjective { proof_time_ms: u64, trust_level: TrustLevel, memory_bytes: u64, proof_steps: usize }`. + `TrustLevel::value()` returns `u8` (1–5, `src/rust/verification/confidence.rs`). +* `ProofCandidate { .., is_pareto_optimal: bool }`. `ParetoFrontier::compute(&mut [ProofCandidate]) -> Vec` + is O(n²) with a private `dominates`. `ParetoFrontier::weighted_rank(..)` uses inverse scaling. +* Existing tests: `test_single_candidate_is_pareto_optimal`, `test_dominated_candidate_excluded`, + `test_tradeoff_candidates_both_on_frontier`, `test_three_way_frontier`, + `test_weighted_rank`, `test_empty_candidates`. These must stay unchanged and pass. +* Consumers: `src/rust/agent/meta_controller.rs` (around lines 634–637: + `compute`, then `weighted_rank(&candidates, 1.0, 0.5, 0.0, 0.0)`), re-exports in + `src/rust/verification/mod.rs:55`, and `src/rust/verification/pareto_arbiter.rs`. + Keep public signatures stable. Add new functions rather than changing old ones. + +Step 1 (decision, record it in rustdoc and the PR): the hypervolume +*reference point*. Recommended: an explicit, caller-supplied reference point, +plus a helper that derives one from a candidate set (worst observed value × a +documented margin). Document that hypervolumes are comparable only under the +same reference point and transform. + +Step 2: implement, as in the spec: + +* One minimisation transform in one place: `[time, -trust, memory, steps]` as `f64`. +* `non_dominated_sort(&[ProofCandidate]) -> Vec>`. F₁ must equal `compute`'s result. +* `hypervolume(points, reference) -> f64`: exact. 2-D by sweep line; 3-D and 4-D + by an exact slicing method (HSO or WFG style). Points not strictly better than the + reference on every axis contribute 0. Monte Carlo is out of scope. +* `hypervolume_contribution(..)`: exclusive contribution per point. +* Tests: hand-computed 2-D/3-D fixtures (worked out on paper in the PR + description); empty → 0.0; duplicates; point equal to reference; permutation + invariance; `proptest` properties (adding a dominated point leaves HV unchanged, + adding a non-dominated point never decreases it; no point in Fₖ dominates any + point in Fⱼ for j < k). + +Out of scope: adding these numbers to `echidna.prove.result/1` (see <>) +or to the dispatcher. + +=== WP2: #408: "Rust Build — Real Chapel Library" fails to link + +* Symptom (from #408): `cargo build --features chapel` against the real Chapel + library fails in `rust-lld` with undefined `chapel_is_available`, + `chapel_parallel_search`, `chapel_free_result`, `chapel_get_version`, + `chapel_available_prover_count`, `chapel_is_prover_available`. These are referenced from + `src/zig_ffi/chapel_bridge.zig` (lines ~209–292). `libechidna_chapel_ffi.a` + is linked, but the Chapel-compiled object defining them is not on the link line. +* Files: `.github/workflows/chapel-ci.yml` (the job runs + `chpl --library --static -I ../zig_ffi ...` around line 88), + `src/chapel/chapel_ffi_exports.chpl`, `src/zig_ffi/{build.zig,chapel_ffi_exports.h,chapel_stubs.c}`, + `build.rs`. +* Acceptable outcomes (from #408): either the job links and runs on a PR head + with the real library, or the job is skipped with a stated reason so it is + not red on every PR. Either way update the "Chapel parallel search" row in + `docs/wikis/Home.md` (line ~54). +* Start by reading the failing job's log: `gh run list --workflow chapel-ci.yml`, + then `gh run view --log-failed`. Check link order and whether `build.rs` emits + `cargo:rustc-link-lib` / `-search` for the Chapel static library and its runtime. +* Zig in CI is 0.15.2 (`zig-ffi-ci.yml`). Locally, `pip install ziglang==0.15.2` + provides a matching `python -m ziglang` binary if no Zig is installed (tooling + only. Do not commit Python). + +=== WP3: ADR: who owns solver time budgets + +ECH-03, EB-01 and the existing portfolio code all ask the same question. Write +`docs/decisions/2026-10-NN-solver-budget-ownership.adoc` in the style of +`docs/decisions/2026-10-05-id-minting.adoc`, with `:status: proposed`. The owner accepts it. + +Inputs: + +* `src/rust/verification/portfolio.rs` `PortfolioConfig`: `solver_timeout: 300`, + `wait_factor: 2.0`, solver sets per SMT / ATP / ITP, `enabled: false` by default. +* `.echidnabot.toml` `[verification] timeout_secs = 300`, per-prover `priority`. +* echidnabot (read-only at `ae52833`, unverified): static 300 s timeouts in `EchidnaConfig`, + `ExecutorConfig` and the Podman executor; manifest `timeout_seconds` parsed but apparently + not wired; the documented `[scheduler] job_timeout_seconds` does not exist. +* ECH-03 (Chapel budget allocator) and EB-01 (adaptive CI timeouts). + +Recommended shape: one owner per scope. echidna `PortfolioConfig` owns +per-solver limits within one proof request; the Chapel allocator may only +redistribute *within* that total; echidnabot owns per-job wall-clock in CI and may only +*shorten* waits, never lengthen past echidna's limit. + +[[contract-hazard]] +=== WP4: partial-progress field in `echidna.prove.result/1` (proposal; blocked) + +PB-01 wants partial progress (for example `subgoals_remaining`). The hazard: + +* echidna's contract says adding a field is compatible and consumers must + ignore unknown fields (`docs/PROVE-RESULT-CONTRACT.adoc`, "Versioning"). + `echidna_core::prove_result::ProveResult::parse` tolerates unknown fields. +* proof-burrower's parser tolerates unknown fields (read-only at `be897dd`, + `crates/burrower-core/src/echidna_contract.rs`; unverified). +* *echidnabot's own parser rejects them*: `src/dispatcher/prove_result.rs:79` + has `#[serde(deny_unknown_fields)]` and a `rejects_unknown_fields` test + (read-only at `ae52833`; unverified). Any new top-level field breaks echidnabot. + +So: (1) file or fix in echidnabot first (tolerate unknown top-level fields, as the +contract requires); (2) only then add the field to echidna as `Option<_>` with +`skip_serializing_if = "Option::is_none"`, so existing golden JCS bytes +(`crates/echidna-core/src/prove_result.rs` `golden_jcs_bytes_for_every_status`, +`src/rust/prove_contract.rs` tests) stay unchanged when it is absent. Until (1) +is done, deliver only a written proposal. + +=== WP5: ECH-04: C-ABI header and Zig bridge + +Spec: `issues/echidna-04-ffi-abi-bridge.md`. There are two Zig trees. Choose +one and say why: + +* `ffi/zig/` (`main.zig`, `capnp_bridge.zig`, `boj.zig`, `overlay.zig`), CI-gated by `zig-ffi-ci.yml`. +* `src/zig_ffi/` (Chapel bridge, `chapel_ffi_exports.h`). + +Idris2 contracts live in `src/abi/` (`Foreign.idr`, `Types.idr`, `Layout.idr`, +`echidnaabi.ipkg`; `.echidnabot.toml` treats `Foreign`, `Types`, `Layout` as +critical, totality and coverage required). The header and Zig can be built and +tested with Zig and a C compiler. The Idris2 side needs `idris2` to type-check, so do not +claim it checks if you could not run it. + +=== WP6: ECH-02 (Julia) and ECH-03 (Chapel) + +Implement only where `julia` / `chpl` are available to run the tests the specs +require. Otherwise produce a design note under `docs/architecture/` and stop. +ECH-03 depends on WP3. + +== 4. Out of scope for this brief + +* Filing PB-01, PB-02 or EB-01 in their repositories, or creating labels + there. Missing labels: proof-burrower `area:swarm`, `rust`, `search-tactics`, + `area:ledger`, `heuristics`; echidnabot `area:dispatcher`, `ci-optimization`. + Owner approval is needed. +* Any ParadisEO (C++) dependency. + +== 5. Report back + +For each package attempted: what changed (files, commit hashes), which +checks ran and their results, what was *not* verified and why, and any owner +decision needed. diff --git a/issues/README.md b/issues/README.md index 60cf54ec..f10324a6 100644 --- a/issues/README.md +++ b/issues/README.md @@ -27,7 +27,7 @@ awk 'f;/^# /{f=1}' issues/ | sed '1{/^$/d}' > /tmp/body.md ## Status -- **ECH-01..04** are filed on hyperpolymath/echidna. Their GitHub bodies and labels still need to be synchronised from these files; only `enhancement` is attached. +- **ECH-01..04** are filed on hyperpolymath/echidna and carry all their labels. On 2026-10-09 their bodies were replaced by hand with a different text that is not these files; the owner decides which is canonical (see `docs/handover/PARADISEO-ROADMAP-PROMPT.adoc`, WP0). `scripts/issues/sync-roadmap-issues.sh` syncs the bodies from these files (dry run by default; refuses to replace hand-edited bodies without `--overwrite`). - **PB-01, PB-02, EB-01** are drafts for copying to their own repositories. They are not filed. ## Provenance of the PB and EB drafts diff --git a/scripts/issues/sync-roadmap-issues.sh b/scripts/issues/sync-roadmap-issues.sh new file mode 100755 index 00000000..78edc136 --- /dev/null +++ b/scripts/issues/sync-roadmap-issues.sh @@ -0,0 +1,150 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# Synchronise the ParadisEO roadmap issues (ECH-01..04) on +# hyperpolymath/echidna with their specs under issues/. +# +# For each issue the body is generated fresh from its own spec file +# (everything after the "# " title line, so the SPDX header is dropped), +# and the spec's labels are added. Existing labels are kept. Nothing is +# closed, recreated or retitled. +# +# Usage: +# scripts/issues/sync-roadmap-issues.sh # dry run (default) +# scripts/issues/sync-roadmap-issues.sh --apply # write to GitHub +# scripts/issues/sync-roadmap-issues.sh --apply --overwrite +# # also replace bodies a human has edited +# scripts/issues/sync-roadmap-issues.sh --verify # check only +# +# Needs: gh (authenticated with Issues: write for --apply), jq, awk, sed. +# A 403 "Resource not accessible by integration" means the token or App +# lacks Issues: write. The script stops at the first failed write. +# +# Safety: --apply only replaces a body that still carries the original +# SPDX header (the known-bad first upload) or already equals the spec. +# Any other body was edited deliberately; it is left alone and reported +# unless --overwrite is also given. + +set -euo pipefail + +REPO="${REPO:-hyperpolymath/echidna}" +ROOT="$(git rev-parse --show-toplevel)" +SPECS="$ROOT/issues" +WORK="$(mktemp -d)" +trap 'rm -rf "$WORK"' EXIT + +# issue-number spec-file labels (space-separated; enhancement is already attached) +MAP=( + "420|echidna-01-pareto-moeo.md|area:verification rust optimization" + "421|echidna-02-cmaes-julia-gnn.md|area:ml julia tuning" + "422|echidna-03-chapel-island-migration.md|area:parallel chapel concurrency" + "424|echidna-04-ffi-abi-bridge.md|area:abi zig idris2 ffi" +) + +mode="dry-run" +overwrite=0 +for arg in "$@"; do + case "$arg" in + --apply) mode="apply" ;; + --verify) mode="verify" ;; + --dry-run) mode="dry-run" ;; + --overwrite) overwrite=1 ;; + *) echo "unknown argument: $arg" >&2; exit 2 ;; + esac +done + +body_of() { + # Everything after the first "# " heading, minus one leading blank line. + awk 'f;/^# /{f=1}' "$1" | sed '1{/^$/d}' +} + +# Pre-flight: every spec exists, every body is well formed and distinct. +declare -A seen=() +for row in "${MAP[@]}"; do + IFS='|' read -r n file labels <<<"$row" + spec="$SPECS/$file" + [[ -f "$spec" ]] || { echo "missing spec: $spec" >&2; exit 1; } + body_of "$spec" >"$WORK/body-$n.md" + head -1 "$WORK/body-$n.md" | grep -q '^- \*\*Repository:\*\* ' \ + || { echo "#$n: body does not start with '- **Repository:**'" >&2; exit 1; } + ! grep -q 'SPDX' "$WORK/body-$n.md" \ + || { echo "#$n: body contains SPDX" >&2; exit 1; } + sum="$(sha256sum <"$WORK/body-$n.md" | cut -d' ' -f1)" + [[ -z "${seen[$sum]:-}" ]] || { echo "#$n: body identical to #${seen[$sum]}" >&2; exit 1; } + seen[$sum]="$n" +done + +# Make sure every label exists before writing anything. +existing="$(gh label list --repo "$REPO" --limit 500 --json name --jq '.[].name')" +for row in "${MAP[@]}"; do + IFS='|' read -r n _ labels <<<"$row" + for l in $labels; do + grep -qxF "$l" <<<"$existing" || { echo "label missing on $REPO: $l" >&2; exit 1; } + done +done + +# Classify the live body: spdx (known-bad upload), spec (in sync), edited. +classify() { + local n="$1" live + live="$(gh issue view "$n" --repo "$REPO" --json body --jq .body | tr -d '\r')" + if [[ "$live" == "$(cat "$WORK/body-$n.md")" ]]; then echo spec + elif grep -q 'SPDX-License-Identifier' <<<"$live"; then echo spdx + else echo edited + fi +} + +skipped=0 +if [[ "$mode" == "apply" ]]; then + for row in "${MAP[@]}"; do + IFS='|' read -r n _ labels <<<"$row" + state="$(classify "$n")" + if [[ "$state" == "spec" ]]; then + echo "#$n: body already matches spec" + elif [[ "$state" == "edited" && "$overwrite" -eq 0 ]]; then + echo "#$n: live body was edited by hand; NOT replacing (use --overwrite)" + skipped=1 + else + echo "#$n: updating body (was: $state)" + gh api -X PATCH "repos/$REPO/issues/$n" -F "body=@$WORK/body-$n.md" --silent + fi + args=() + for l in $labels; do args+=(-f "labels[]=$l"); done + echo "#$n: adding labels: $labels" + gh api -X POST "repos/$REPO/issues/$n/labels" "${args[@]}" --silent + done +elif [[ "$mode" == "dry-run" ]]; then + for row in "${MAP[@]}"; do + IFS='|' read -r n file labels <<<"$row" + state="$(classify "$n")" + case "$state" in + spec) action="body already matches spec" ;; + spdx) action="would replace body (live body is the SPDX upload)" ;; + edited) action="live body was edited by hand; would replace only with --overwrite" ;; + esac + echo "#$n: $action; would ensure labels: $labels" + done +fi + +# Verification (all modes): compare live state with the specs. +fail=0 +for row in "${MAP[@]}"; do + IFS='|' read -r n _ labels <<<"$row" + live="$(gh issue view "$n" --repo "$REPO" --json body,labels)" + live_body="$(jq -r .body <<<"$live" | tr -d '\r')" + live_labels="$(jq -r '.labels[].name' <<<"$live")" + status="ok" + [[ "$live_body" == "$(cat "$WORK/body-$n.md")" ]] || status="body differs from spec" + for l in enhancement $labels; do + grep -qxF -- "$l" <<<"$live_labels" || status="$status; missing label $l" + done + echo "#$n: $status (labels: $(paste -sd, <<<"$live_labels"))" + [[ "$status" == "ok" ]] || fail=1 +done + +if [[ "$mode" == "dry-run" && "$fail" -ne 0 ]]; then + echo "dry run: differences above are expected until --apply is run" + exit 0 +fi +[[ "$skipped" -eq 0 ]] || echo "some bodies were left alone because they were edited by hand" +exit "$fail"