From 9c1a4b878551897b3d4ffebe35ca6181cf5452d4 Mon Sep 17 00:00:00 2001 From: Arena Agent Date: Fri, 9 Oct 2026 18:24:46 +0000 Subject: [PATCH] docs(plans): ultraplan and cross-repo hand-offs (plan only) Recon-based plan for RSR/standards compliance, deed migration gating, issues #105, #104, #84, and bot/repo hand-offs. No A2ML converted; all migration gated on owner decisions D1-D10. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- .../plans/CROSS-REPO-HANDOFFS-2026-10-09.adoc | 370 ++++++++++ docs/plans/ULTRAPLAN-2026-10-09.adoc | 692 ++++++++++++++++++ 2 files changed, 1062 insertions(+) create mode 100644 docs/plans/CROSS-REPO-HANDOFFS-2026-10-09.adoc create mode 100644 docs/plans/ULTRAPLAN-2026-10-09.adoc diff --git a/docs/plans/CROSS-REPO-HANDOFFS-2026-10-09.adoc b/docs/plans/CROSS-REPO-HANDOFFS-2026-10-09.adoc new file mode 100644 index 0000000..34aa6a9 --- /dev/null +++ b/docs/plans/CROSS-REPO-HANDOFFS-2026-10-09.adoc @@ -0,0 +1,370 @@ += Cross-repo and bot hand-offs +:toc: left +:toclevels: 2 +:icons: font +:date: 2026-10-09 +:status: DRAFT - nothing below has been filed. Each brief is filed only after owner approval. + +Companion to `docs/plans/ULTRAPLAN-2026-10-09.adoc`. IDs match the ultraplan: +`R-` standards, `T-` rsr-template-repo, `E-` echidna, `B-` echidnabot, +`H-` hypatia, `F-` fleet bots, `A-` affinescript. + +Ground rules that apply to every brief: + +* Hand-offs go to a repo's maintainers, or to the named bot through that repo's + normal intake. No standalone MCP servers; route through BoJ. +* Each brief is self-contained. The receiving side does not need this repo to + act on it, except where a link is given. +* No brief asks another repo to convert A2ML by hand. Any A2ML-to-deed work + follows the family mapping specs in `1-formats/deed/mappings/`. + +== Summary + +[cols="1,2,3,2", options="header"] +|=== +| ID | Target | Ask | Blocks + +| R-1 | `hyperpolymath/standards` | Add gated Rust-workspace entries to root allowlist (D3) | G-ROOT-1, G-ROOT-3 +| R-2 | `hyperpolymath/standards` | Reconcile RSR 2.1.0-draft (A2ML) with the deed; move `check-rsr-profile.sh` to the deed | G-FMT, 2.2.1 +| R-3 | `hyperpolymath/standards` | Rule the ply mapping (no ruled mapping exists) | G-FMT-PLY +| R-4 | `hyperpolymath/standards` | Rule the `0-AI-MANIFEST` mapping (D1) | G-ID-2, W3 +| R-5 | `hyperpolymath/standards` | Decide whether proof-burrower belongs in `bot_exclusion_registry` external-repos (G-ECO-1) | G-ECO-1 +| R-6 | `hyperpolymath/standards` | Exemption mechanism for historical audit reports in `check-no-placeholders` (G-PH-1) | G-PH-1 +| R-7 | `hyperpolymath/standards` | Make `check-lock-sync.sh` and `check-invisible-characters.sh` runnable without gawk / with documented args | Verification +| T-1 | `hyperpolymath/rsr-template-repo` | Confirm canonical name: `coordination.k9` vs `coordination.k9.ncl` (D8) | G-ROOT-2 +| T-2 | `hyperpolymath/rsr-template-repo` | Mirror R-1 in the template's `.machine_readable/root-allow.txt` once decided | G-ROOT-3 +| E-1 | `hyperpolymath/echidna` | Tag a release carrying the `echidna.prove.result/1` contract, so consumers pin a tag, not a SHA | G-CI-4, B-1 +| E-2 | `hyperpolymath/echidna` | Stepwise proof-state contract with real state transitions and sub-goal counts | #105 P3, #104 P4 +| E-3 | `hyperpolymath/echidna` | `suggest --output json` contract (`echidna.suggest.result/1`) | Optional, EI-2 +| E-4 | `hyperpolymath/echidna` | End-to-end tests for `timeout` and `unknown` statuses | Trust of contract +| E-5 | `hyperpolymath/echidna` | Optional `corpus near --format json` for dedupe | Low priority +| B-1 | `hyperpolymath/echidnabot` | Re-pin echidna to a tagged release with the contract; keep handshake at `MIN_ECHIDNA_VERSION` 2.3.0 | Pin consistency +| B-2 | `hyperpolymath/echidnabot` | Encrypt or hash webhook secrets at rest (currently plaintext in SQLite) | Security +| B-3 | `hyperpolymath/echidnabot` | Creusot crate rename follow-up | Hygiene +| B-4 | `hyperpolymath/echidnabot` | Fitness consumer (only if #104 P3 ships and the owner wants it) | Deferred +| H-1 | `hyperpolymath/hypatia` | Implement `hypatia:rsr-conformance` so the presence-proxy can be replaced by the normative oracle | Tier scoring +| F-1 | rhodibot (fleet) | Remake brief for `rhodibot.yml`, if D4 = remake | G-CI-5 +| F-2 | sustainabot (fleet) | Dependency-health advisory: Cargo deps and GitHub Action pins | 8.1.2 +| F-3 | seambot (fleet) | Contract tests for the Burrower-echidna seam, using golden fixtures for each status | #105/#104 safety +| F-4 | glambot (fleet) | Doc reconciliation after W1 version alignment | G-VER-1 +| F-5 | finishbot (fleet) | Track W1–W4 gates as tasks; report when each gate passes | Wave tracking +| A-1 | `hyperpolymath/affinescript` | Receive #84 if D5 = transfer | #84 +|=== + +== Standards (`hyperpolymath/standards`) + +=== R-1 Root allowlist: Rust-workspace entries + +*Ask.* Add gated `?` entries to the RSR root allowlist for Rust workspaces: +`Cargo.toml`, `Cargo.lock`, `crates/`, `rust-toolchain.toml`. The gate should +apply only when a `rust` capability is declared. + +*Why.* Proof-burrower is a Rust workspace (`crates/burrower-cli`, +`burrower-core`, `burrower-wasm`). The template allowlist has no Rust entries, +so `check-root-shape.sh` flags a correct layout. + +*Acceptance.* `check-root-shape.sh` passes on proof-burrower with no repo moves. +A repo without the `rust` capability still fails on those entries. + +=== R-2 RSR 2.1.0-draft vs the deed + +*Ask.* Reconcile the criteria file, which still requires A2ML descriptiles, with +the deed format (`1-formats/deed/spec/abnf/deed.abnf` v1.1.0). Add the deed as +an accepted record for `rsr-profile`, `anchor`, and `clade`. Move `scripts/check-rsr-profile.sh` from +`.machine_readable/rsr-profile.a2ml` to the deed clause. + +*Why.* `rsr-criteria-v2.a2ml` criteria 3.1.8, 3.1.9, and 3.2.2 point to A2ML +paths. The deed is the target format for new work. + +*Acceptance.* A repo with a deed `(rsr-profile …)` clause and no A2ML passes +3.2.2 under the checker. The 2.1.0-draft status is stated explicitly in the spec. + +=== R-3 Ply mapping ruling + +*Ask.* Write the ruled ply mapping in `1-formats/deed/mappings/`. The template +precedent is the `(ply …)` clause (pilot emitter). Also update +`2-protocols/0-ai-gatekeeper/docs/AI-MANIFEST-SPEC.adoc`, which still describes +ply prefixes. + +*Acceptance.* A mapping spec exists and `check-manifest-ply.sh` checks the +deed form. + +=== R-4 `0-AI-MANIFEST` mapping ruling + +*Ask.* Rule the mapping for `0-AI-MANIFEST.a2ml` (D1). Recommended: Option A, +as the mapping's own recommendation. + +*Acceptance.* The AI-MANIFEST mapping is ruled and cited from the deed spec. + +=== R-5 Bot exclusion registry + +*Ask.* Decide whether proof-burrower should appear in +`bot_exclusion_registry.a2ml` `external-repos`. The registry currently lists +only robot-repo-automaton and rhodibot/echidnabot source paths. + +*Acceptance.* A recorded decision, either way. + +=== R-6 Placeholder exemption for historical reports + +*Ask.* Let `check-no-placeholders` exempt historical audit reports, or +explicitly state that a dated audit record is out of scope. Proof-burrower's +hit is `docs/reports/audit/2026-04-07-template-standards-audit.adoc`. + +*Acceptance.* The checker passes on a repo whose only placeholder hits are in +dated, historical audit records. Other placeholders still fail. + +=== R-7 Checker portability + +*Ask.* `check-lock-sync.sh` needs gawk (3-arg `match`). Either make it POSIX +or state the requirement in its header. `check-invisible-characters.sh` takes +`SCAN_ROOT RESULTS_FILE` but its usage line should say so. + +*Acceptance.* Both run on a stock Linux CI runner, or their requirements are +documented. + +== rsr-template-repo (`hyperpolymath/rsr-template-repo`) + +=== T-1 Canonical coordination file name + +*Ask.* Decide `coordination.k9.ncl` (template) vs `coordination.k9` (standards +`2-protocols/k9-coordination/` and this repo). Recommended: follow the +template and rename the other side, unless standards rules otherwise (D8). + +*Acceptance.* One name in the template, the standards k9 directory, and the +root allowlist. + +=== T-2 Mirror the Rust allowlist + +*Ask.* After R-1 is decided, mirror the gated Rust entries in +`.machine_readable/root-allow.txt`. + +*Acceptance.* Template and standards allowlists agree. `check-root-shape.sh` +passes on the template. + +== echidna (`hyperpolymath/echidna`) + +=== E-1 Tag the prove-result contract + +*Ask.* Cut a tagged release that includes the `echidna.prove.result/1` contract +(first in commit `a71aa2c`, 2026-10-05, PR #409). Current `main` is `822cfc9`. +Echidna's Cargo version is `2.3.0` and `echidna-core` is `0.2.0`. + +*Why.* proof-burrower's `proof-safety.yml` pins a commit SHA +(`556d6468…`, pre-contract). A tag is easier to pin and review. + +*Acceptance.* A tag exists. `prove --output json` at that tag emits the +contract for all five statuses (see E-4 for the two untested ones). + +=== E-2 Stepwise proof-state contract (the blocker) + +*Ask.* Provide a real stepwise proof-state interface, with: + +* `apply_tactic` returning a *new* state, not a clone of the input. Today the + FFI path (`src/interfaces/graphql/ffi_wrapper.rs`, `FfiProverBackend::apply_tactic`) + sends `format!("{:?}", tactic)` and returns `CoreTacticResult::Success(state.clone())`. +* A proof-state type that carries the open goals, so a consumer can read a + sub-goal count. Today `CoreProofState::new(Term::Var(content))` holds the raw + file text. +* `verify_proof` that reports on the state, not the file text + (`verify_proof(&self, _state)` ignores the state). +* A JSON schema (`echidna.proofstate/1`) with a CLI or server surface, and a + stable identifier for the state so consumers can cache by it. + +*Why.* proof-burrower #105 (P3) needs step-level caching. #104 (P4) needs +`GoalReduction`. Neither can be implemented on the current surface. + +*Acceptance.* A two-goal fixture lemma: applying one tactic yields one +remaining goal, and the sub-goal count is reported in JSON. Same input gives +the same state id. Tests run in CI. + +=== E-3 `suggest` JSON contract (optional) + +*Ask.* `echidna suggest` JSON output as `echidna.suggest.result/1`, following +the same discipline as the prove contract (versioned schema, JCS-canonical +output, unknown fields ignored). + +*Acceptance.* A golden-output test for the schema. Not needed for #105 or #104. + +=== E-4 `timeout` and `unknown` end-to-end + +*Ask.* The contract spec states that `timeout` and `unknown` are covered only +by golden unit tests, because no backend that runs without an external prover +produces them. Add an end-to-end test that produces each status from a fixture +(for example, a test prover with a configurable delay or an unknown verdict). + +*Why.* echidnabot and proof-burrower both act on these statuses. + +*Acceptance.* `tests/prove_output_json.rs` covers `timeout` and `unknown` +end-to-end. + +=== E-5 Corpus near-duplicate query (optional, low priority) + +*Ask.* `echidna corpus near --format json`, so proof-burrower can dedupe against +echidna's corpus without growing its own indexer. Only after E-1 and only if +the owner wants the overlap removed. + +=== E-6 Estate tidy (route to standards) + +echidna tracks 55 `.a2ml` files, has no deed, and its root holds many entries +outside the template allowlist. Treat this as a standards decision (R-1, R-2), +not an echidna-only fix. Do not hand-convert. + +== echidnabot (`hyperpolymath/echidnabot`) + +=== B-1 Re-pin echidna to a tag + +*Ask.* echidnabot pins echidna git rev `b761b3a8…`, which was live-traced on +2026-10-05 against `a71aa2c`. Re-pin to the tag from E-1, or to a commit at or +after `a71aa2c`. Keep the startup handshake at `MIN_ECHIDNA_VERSION` 2.3.0 +(`src/dispatcher/echidna_client.rs:23`). + +*Acceptance.* The handshake passes against the new pin. The strict parser +(`src/dispatcher/prove_result.rs`) accepts the `echidna.prove.result/1` output +on the pin. + +=== B-2 Webhook secrets at rest + +*Ask.* Webhook secrets are stored in plaintext in SQLite. Encrypt them with a +key from the environment, or store a keyed hash if verification only needs +comparison. Rotate existing secrets on migration. + +*Acceptance.* A migration removes plaintext secrets. Tests show verification +still works. The owner signs off the approach. + +=== B-3 Creusot crate rename follow-up + +*Ask.* Upstream intends to rename `echidna-core-creusot` (its name in +`Cargo.toml` line 34 comment and `docs/ECHIDNA-INTEGRATION.adoc` line 37 say +"being renamed"). When echidna ships the rename, update echidnabot's dependency +and docs. Until then, track the follow-up; do not rename early. + +*Acceptance.* Build and tests pass with the upstream crate name. Docs match. + +=== B-4 Fitness consumer (deferred) + +*Ask.* Only if proof-burrower #104 P3 ships and the owner wants echidnabot to +query burrower fitness. Consumer side only, through the line-delimited JSON +surface (`burrower serve`). Do not build it before P3 exists. + +== Hypatia (`hyperpolymath/hypatia`) + +=== H-1 Implement `hypatia:rsr-conformance` + +*Ask.* Implement the normative RSR oracle that standards names in +`docs/AFFIRMATION.adoc` and `docs/AUDIT.adoc`. It must produce a tier score +per repo. + +*Why.* Every compliance statement in the ultraplan is currently a repo-local +check or a presence proxy. The oracle is what the standards actually ratify. + +*Acceptance.* Run against proof-burrower, the oracle returns a per-criterion +verdict that matches the presence-proxy table where a file is absent, and +explains each `manual` criterion. + +== Fleet bots + +The roster is in standards `docs/proofs/spec-templates/T2-high/gitbot-fleet.adoc`. +Roles (from standards docs): rhodibot (structure and format conformance), +echidnabot (proof verification), sustainabot (dependency health), glambot +(documentation), seambot (integration), finishbot (task completion). + +=== F-1 rhodibot: remake brief (only if D4 = remake) + +*Ask.* `rhodibot.yml` is 78% red and marked "retire or remake" in the standards +CI catalog. If remake: enforce the template root allowlist and deed format, not +A2ML. Keep it report-only until the owner accepts its results on proof-burrower. +The green-run threshold is the owner's call, not a value this plan sets. + +*Depends on.* R-1, R-2. + +=== F-2 sustainabot: dependency-health advisory + +*Ask.* Advisory report (no auto-merge) on: + +* `Cargo.toml` and `Cargo.lock` dependencies of `crates/burrower-core`, + `burrower-cli`, `burrower-wasm`; +* GitHub Action pins in `.github/workflows/` (the template's + `check-action-pinning` rule applies). + +*Acceptance.* A report, with each finding tagged by severity. Nothing is merged +or bumped without an owner decision. + +=== F-3 seambot: Burrower-echidna contract tests + +*Ask.* Contract tests for the seam between `burrower attempt` and +`echidna prove --output json`. Use golden fixtures for each status (verified, +failed, error, timeout, unknown). Test the flags the seam sends: `--prover`, +`--project-root`, `--sandbox`, `--output json`. + +*Why.* Burrower already depends on this contract (`attempt.rs`). The seam is +where a silent break would happen. + +*Acceptance.* Tests run in proof-burrower CI. A deliberately malformed payload +fails closed (the strict parser rejects it). + +=== F-4 glambot: documentation reconciliation + +*Ask.* After W1's version alignment, reconcile `README.adoc`, `STATE.a2ml` +(via the deed), `CHANGELOG.adoc`, and the Justfile version. Report +inconsistencies. Do not rewrite the README without owner review. + +*Depends on.* W1 version alignment. + +=== F-5 finishbot: W-gate tracking + +*Ask.* Track the W1–W4 gates from the ultraplan as tasks. Report when each +gate command passes: `must-spdx-headers`, `check-no-vlang`, +`check-no-placeholders`, `validate-state`, `validate-rsr`, `check-no-a2ml`, +and the deed lint. + +*Acceptance.* A task list with a status per gate. + +== affinescript (`hyperpolymath/affinescript`) + +=== A-1 Receive #84 (only if D5 = transfer) + +*Ask.* Accept the transfer of #84 (or its tracking) from proof-burrower. The +acceptance criteria travel with it: + +* establish the provenance and intended dependency boundary of the embedded + copy; +* implement or remove each unsupported public capability, with tests; +* reconcile with the canonical repo (this one); +* keep the distinction from the independently tested Rust `burrower-core` / + ECHIDNA Isabelle integration; +* do not treat tracking the debt as completing it. + +The debt list: editor and bridge placeholders; a stub formatter; linter effect +checks incomplete; trait conversion, signature, overlap, and unification checks +incomplete; Phase 6 runtime placeholders; Phase 8 package-manager +placeholders; LSP fix suggestions incomplete. + +*Acceptance.* The issue has a provenance statement and a status per debt item. + +== Sequencing of these briefs + +[cols="1,4", options="header"] +|=== +| Order | Briefs + +| First (no dependencies) +| R-1, R-3, R-4 (rulings), R-5, R-6, R-7, E-1, B-2, F-2, F-3 + +| After standards rulings +| R-2, T-1, T-2, F-1 (if remake), H-1 + +| After E-1 +| B-1, E-5 + +| On the blocker +| E-2 (needed by #105 P3 and #104 P4). Start early: it is the longest item. + +| On owner decision +| A-1 (D5), B-4 (deferred), E-3 (optional) +|=== + +== Not filed + +Nothing in this file has been filed. Filing creates visible issues in other +repos. Each brief is filed only after the owner approves it, and this +repo's ultraplan has been reviewed. diff --git a/docs/plans/ULTRAPLAN-2026-10-09.adoc b/docs/plans/ULTRAPLAN-2026-10-09.adoc new file mode 100644 index 0000000..c98a420 --- /dev/null +++ b/docs/plans/ULTRAPLAN-2026-10-09.adoc @@ -0,0 +1,692 @@ += Proof Burrower Ultraplan +:toc: left +:toclevels: 2 +:icons: font +:source-highlighter: rouge +:date: 2026-10-09 +:status: PLAN ONLY - no bulk edits performed; decisions gate migration + +[abstract] +This plan says how to bring `proof-burrower` in line with the hyperpolymath +standards repository and the RSR template format, how to resolve the three open +issues (#105, #104, #84), and which hand-offs go to which bot in which repo. +Companion file: `docs/plans/CROSS-REPO-HANDOFFS-2026-10-09.adoc`. + +== 0. Ground rules for executing this plan + +* *Plan, not bulk edit.* No A2ML is converted by hand. The retired A2ML files + move to the deed format only through the family mapping specs in + `standards/1-formats/deed/mappings/`, using the tooling named there. +* *Normative sources.* Deed grammar: `1-formats/deed/spec/abnf/deed.abnf` + (v1.1.0). RSR criteria: `0-canon/rsr/rsr-criteria-v2.a2ml` (2.1.0-draft). + Root shape: template `.machine_readable/root-allow.txt`, checked by + `scripts/check-root-shape.sh`. +* *Oracle caveat.* The normative RSR oracle, `hypatia:rsr-conformance`, is not + implemented yet. Every compliance statement below is a repo-local check or a + file-presence proxy, and is labelled as such. +* *Owner decisions* are listed in section 7 and block the steps that depend on + them. Nothing in section 7 is decided by this plan. + +== 1. Evidence baseline (what was run, 2026-10-09) + +[cols="3,2,5", options="header"] +|=== +| Check | Result | Notes + +| `check-root-shape.sh` +| error +| No allowlist at `.machine_readable/root-allow.txt`. + +| `check-no-a2ml.sh` +| FAIL +| 119 tracked `.a2ml` files. Template tracks 0. + +| `check-no-md-in-docs.sh` +| PASS +| 5 `.md` under `docs/`, none allow-listed. + +| `check-no-placeholders.sh` +| FAIL +| 13 files still carry `{{...}}` tokens (listed in section 2.3). + +| `check-no-vlang.sh` +| FAIL +| 3 hits: `Justfile:273`, `.machine_readable/contractiles/Justfile:272`, + `.machine_readable/integrations/groove.a2ml:4`. + +| `check-lock-sync.sh` +| not run +| Needs `gawk` (`awk` lacks 3-arg `match`). + +| `check-invisible-characters.sh` +| not run +| Needs `SCAN_ROOT RESULTS_FILE` arguments. + +| `just validate-rsr` +| FAIL +| Missing `licensing/exhibits/EXHIBIT-{A-ETHICAL-USE,B-QUANTUM-SAFE}.txt`, + `licensing/texts/MPL-2.0.txt`, and META/MAINTENANCE-AXES/CHECKLIST fields. + The recipe still requires the retired A2ML files. + +| `just validate-state` +| FAIL +| `STATE.a2ml: INVALID (missing required sections)`. + +| `just verify-template` +| FAIL +| Justfile still says `rsr-template-repo`; `{{REGISTRY}}/{{SERVICE_NAME}}` in + `container/compose.toml`; Groove manifest port 0. + +| `scripts/validate-template.sh` +| FAIL +| Phase 1: `src/interface/abi` missing. + +| `just must-spdx-headers`, `just must-no-banned-files` +| PASS +| 6 of 109 source-like files lack an SPDX header in their first 12 lines. + +| `proof-safety.yml` (run 37371572643, `main`, 2026-10-05) +| failure +| Job `cancelled`, no retrievable logs. *Cause unknown; not diagnosed.* +|=== + +Other `main` workflows (Rust CI, Hypatia, Governance, Secret Scanner, +Scorecard) were green on 2026-10-05 through 2026-10-09. + +=== 1.1 Presence-proxy RSR baseline + +Method: `rsr-criteria-v2.a2ml` was parsed. Criteria were kept if their gate is +`universal` or matches a *provisional* declared capability set: +`rust, cli, library, bash, governance-tier, docs-site`. Each criterion's +`template_ref` was then checked for existence. Criteria with `template_ref = "-"` +or no path were counted as manual. This is a *file-presence proxy*. It does +not check content, so a file that is present can still fail its content gate. + +[cols="2,6", options="header"] +|=== +| Result | Count + +| Applicable criteria +| 60 (of 78; 18 gated off by capability) + +| Present +| 38 + +| Missing (presence) +| 8 + +| Manual / no template path +| 14 +|=== + +Missing by presence (criterion, tier, template path): + +[cols="1,1,4", options="header"] +|=== +| Id | Tier | Path expected by template + +| 1.2.2 git-hooks | silver | `ci/.pre-commit-config.yaml` (repo has root `.pre-commit-config.yaml`, which is not allowed at root) +| 1.2.4 tool-versions | silver | `.tool-versions` +| 2.2.1 wellknown-core | silver | `.well-known/` +| 3.1.8 anchor | gold | `.machine_readable/descriptiles/anchors/ANCHOR.a2ml` (see section 2.2 for the deed route) +| 3.1.9 clade | gold | `.machine_readable/descriptiles/CLADE.a2ml` (deed route, section 2.2) +| 3.2.2 rsr-profile | silver | `.machine_readable/rsr-profile.a2ml` (deed route, section 2.2) +| 5.1.1 no-python | bronze | `.github/workflows/estate-rules.yml` (repo has none) +| 10.1.3 affirmation | gold | `docs/AFFIRMATION.adoc` +|=== + +Manual criteria, with the evidence this recon actually produced: + +* no-vlang (5.1.4): FAIL (3 hits, section 1). +* spdx-headers (4.1.1): 6 source-like files lack the header (section 1). +* no-makefile (1.1.3): PASS (no Makefile tracked). +* no-go (5.1.5), no-rescript (5.1.3), no-secrets (4.1.2), a2ml-valid (3.2.1): + *not checked* in this recon. Their status is unknown, not passing. + +The bronze tier cannot be claimed until 5.1.1 (no-python estate-rules workflow) +and 5.1.4 (no-vlang) are fixed. + +The baseline is an input to the work in section 2, not a score. + +== 2. Standards and RSR compliance gaps + +Each gap has an ID (`G-…`), a current state, a target, the gating reference, +and a wave (section 5). Gaps that need an owner decision say so. + +=== 2.1 Root shape + +[cols="1,4,4", options="header"] +|=== +| ID | Current | Target + +| G-ROOT-1 +| Not allowed at root under the template allowlist: `.bot_directives/`, + `.gitlab-ci.yml`, `.guix-channel`, `.pre-commit-config.yaml`, + `0-AI-MANIFEST.a2ml`, `Cargo.lock`, `Cargo.toml`, `Containerfile`, + `agents/`, `audits/`, `container/`, `contractile.just`, `coordination.k9`, + `crates/`, `eclexiaiser.toml`, `rust-toolchain.toml`, `selur-compose.toml`, + `setup.sh`, `stapeln.toml`, `tools/`. +| Each entry is moved, retired, or allow-listed. The Rust workspace + (`Cargo.toml`, `Cargo.lock`, `crates/`, `rust-toolchain.toml`) needs an + allowlist ruling, *owner decision D3*. Moves are not made until D3 is decided. + +| G-ROOT-2 +| Required by the template allowlist but absent: `CLAUDE.md`, `launcher.sh`, + `coordination.k9.ncl`, `.gitleaksignore`, `.cicd-hygiene-allow`, + `.gitmessage`, `.mailmap`, `.clinerules`, `.cursorrules`, `.windsurfrules` + (inert under `.machine_readable/ai/`), `build/`, `ci/`. +| Create the ones that apply. `CLAUDE.md` and the agent rule files are + templates. `coordination.k9` vs `coordination.k9.ncl` is *decision D8*. + +| G-ROOT-3 +| The allowlist has no Rust-workspace entries. +| Standards-side decision, not a repo move (see D3). +|=== + +=== 2.2 Format: A2ML to deed + +The RSR criteria 2.1.0-draft still require A2ML descriptiles and do not +mention the deed. The deed format (standards `1-formats/deed/`) is the target +for new work. The repo carries *119 tracked `.a2ml` files* in these groups: + +[cols="3,2,5", options="header"] +|=== +| Group | Count | Plan + +| `docs/` +| 45 +| Docs that are prose should be `.adoc`. Structured records move to the deed through the mapping. + +| `src/` +| 17 +| Examples and code-adjacent data. Check each: some are real config, some are sample text. + +| `.machine_readable/descriptiles/` +| 11 +| Includes `anchor/`. Anchor and CLADE map to deed `(anchor …)` and `(clade …)`. + +| `verification/` +| 9 +| Proof-status records. Check against the proof policy first. + +| `.machine_readable/integrations/` +| 5 +| Groove and similar. Groove's `port 0` is a bug and needs fixing in its mapping. + +| `.machine_readable/contractiles/` +| 5 +| Contractile mappings. One of these is the Justfile `vlang` hit. + +| `features/` +| 4 +| Feature records. + +| `.machine_readable/scripts/` +| 4 +| Scripts that read A2ML. They must be rewritten to read the deed before the A2ML is removed. + +| `.machine_readable/policies/` +| 4 +| Policy records. Map to deed `(policy …)` clauses once the mapping says so. + +| `.bot_directives/` +| 3 +| Untouched template boilerplate (`methodology`, `coverage`, `debt`). Migrates to `(bot-directives …)` (section 2.4). + +| `.machine_readable/ai/` +| 2 +| AI-facing records. Depends on D1. + +| root, examples, container, audits, `.github`, anchors, configs +| 1 each (plus `ENSAID_CONFIG.a2ml`, `CLADE.a2ml`, `0.1-AI-MANIFEST.a2ml`, `0-AI-MANIFEST.a2ml`) +| Per-file mapping. `0-AI-MANIFEST` mapping is *decision D1*. +|=== + +Rules for the conversion: + +* Every family is converted under its own mapping spec in + `1-formats/deed/mappings/`. The mapping set covers CLADE, META/ECOSYSTEM, + AGENTIC/NEUROSYM/PLAYBOOK, STATE v1, AI-MANIFEST, and scorecard. +* *Ply has no ruled mapping yet.* The per-directory `0.x-AI-MANIFEST.a2ml` + files form a ply tree. The template precedent is a `(ply …)` clause in its + deed (the pilot emitter). Until the standards owners rule, the ply tree is + left in place and nothing is deleted. (*Gap G-FMT-PLY*, depends on standards R4.) +* The deed for this repo currently has *identity, clade, forges, lineage, status, + maturity, ecosystem* and lints OK. It is *missing* `rsr-profile`, `meta`, + `agentic`, `neurosym`, `playbook`, `bot-directives`, `contractiles`, + `manifest`, `ply`, `anchor`, `ensaid`, `integrations`, `policies`. + The template deed has all of them and is the worked model. +* Each mapping is applied one family at a time. After each family the repo's + own gates (`check-no-a2ml`, `validate-rsr`) and the deed lint run. Deletions + come only after the deed and every reader have been switched. + +==== 2.2.1 `rsr-profile` + +Template value (the model to follow): +`(rsr-profile :version "1.0.0" :spec "rsr-criteria-v2" :declares-against "2.1.1-draft" :role "spine" :capabilities (...))`. + +The template capability set is: `zig, idris2, bash, cli, library, ffi, abi, +formal-proofs, docs-site, container, reproducible-build, benchmarks, +governance-tier`. For this repo the capability list must be *earned*, not +copied. Proposed provisional set: `rust, cli, library, bash, governance-tier, +docs-site`. Decide `ffi` (the `burrower-wasm` crate exposes a C-ABI surface), +`container` (the root `Containerfile` is an unfilled template; see D2), +`formal-proofs` (`verification/proofs/` has Lean4, TLA+, Agda, and Coq files; +Coq `TypeSafety.v` needs real proof markers), and `reproducible-build`. + +Upstream tension: `scripts/check-rsr-profile.sh` still reads +`.machine_readable/rsr-profile.a2ml`. Standards must reconcile (R2). + +=== 2.3 Identity and placeholders + +* G-ID-1: `rsr-template-repo` appears in 23 files. The Justfile sets + `project` and `REPO` to `rsr-template-repo` (lines 23–25), copied from the + template. Replace with `proof-burrower` / the right repo name. +* G-ID-2: `0-AI-MANIFEST.a2ml` describes itself as the *template's* manifest. + Rewrite for this repo, or retire through D1. +* G-ID-3: `.bot_directives/methodology.a2ml` lists `rsr-template-repo` as a + reject pattern. Fix via the bot-directives migration (2.4). +* G-PH-1: Placeholder tokens in 13 files: + `container/*` (`{{PORT}}`, `{{SERVICE_NAME}}`, `{{REGISTRY}}`), + `.github/settings.yml` (`{{REPO}}` / `{{DESCRIPTION}}` appear only inside + explanatory comments; this is a checker false positive that a rewording + fixes, and the file has no identity keys), `.bot_directives/methodology.a2ml`, + `.github/CODE_OF_CONDUCT.md`, `docs/reports/audit/2026-04-07-template-standards-audit.adoc`, + `.machine_readable/self-validating/methodology-guard.k9.ncl`, plus the root + `Containerfile` (`{{project}}`, `TODO` stages). + The audit report is a historical record. Either reword it or add an + allowlist entry (R8). +* G-VER-1: Version drift. `Justfile` `version := "0.1.0"`, `Cargo.toml` + `version = "0.0.1"`, `STATE.a2ml` `phase: pre-alpha`, `CHANGELOG.adoc` is + `[Unreleased]` only, and there are no git tags. Pick one version, align + Justfile, Cargo, and the deed status, and tag only after an owner decision. + +=== 2.4 Bot directives + +Template keeps them as deed clauses: `(bot-directives (methodology))`, +`(coverage)`, `(debt)`, `(rra)`. The repo's `.machine_readable/bot_directives/` +holds only `README.adoc`. The repo's `.bot_directives/{methodology,coverage,debt}.a2ml` +is untouched template boilerplate: coverage `total-components = 0`, debt empty. +Migration: replace with real values and move them into deed clauses using +`scripts/deed-clause.sh`. Methodology defaults from the template (hybrid mode, +ring-ceiling 2, wave-cap 2, spike-required true, priority weights +must/should/could = 3/2/1, convergent budget 70/20/10) should be kept only +where they are actually used. The template value is not automatically correct. + +=== 2.5 Language policy + +[cols="2,5", options="header"] +|=== +| Gap | Action + +| `check-no-vlang` (3 hits) +| Remove the V reference from `Justfile:273`, `.machine_readable/contractiles/Justfile:272`, and `.machine_readable/integrations/groove.a2ml:4`. Rewrite the groove record as part of the integrations mapping. + +| Inline Python: `.github/workflows/dogfood-gate.yml:268` (`python3 -c` tomllib check of `eclexiaiser.toml`) +| Replace with a Rust or shell check. If it has to stay for now, add a shrink-only ledger at `.machine_readable/inline-python-allow.txt` (absent today) and track it in `check-inline-python.sh`. + +| Coq `verification/proofs/coq/TypeSafety.v` +| Add real proof markers. Do not count a file with placeholder proofs as verified. + +| Lean4, TLA+, Agda proofs +| Confirm each is on the allowed-list before the `formal-proofs` capability is claimed. + +| `agents/*.007` (DSL files) +| Carry MPL-2.0 SPDX headers. The 007 DSL may be ARR-licensed. *Decision D6* before any change. + +| SPDX gaps (6 files) +| `.github/copilot/coding-agent.yml`, `.github/funding.yml`, `.machine_readable/scripts/forge/git-cleanup.sh`, `scripts/invariant-path.sh`, `session/dispatch.sh`, `session/local-hooks.sh`. Add headers that match the file's licence. +|=== + +=== 2.6 Build, container, and gates + +* G-CI-1: `just validate-rsr` cannot pass until the licensing files exist + (`licensing/exhibits/EXHIBIT-A-ETHICAL-USE.txt`, + `EXHIBIT-B-QUANTUM-SAFE.txt`, `licensing/texts/MPL-2.0.txt`) and the + META/MAINTENANCE-AXES/CHECKLIST fields are filled. Retiring the A2ML files + first would break it, so the recipe must move to the deed first. +* G-CI-2: `just validate-state` fails because `STATE.a2ml` is missing required + sections. The fix is the STATE v1 mapping (`1-formats/deed/mappings/`), + not a hand rewrite. +* G-CI-3: `just verify-template` and `scripts/validate-template.sh` fail. + Fix the Justfile identity and the `container/compose.toml` placeholders, + and decide what Phase 1's `src/interface/abi` means for a CLI with no ABI + surface. Either add the directory or mark the phase not applicable with a + recorded reason. +* G-CI-4: `proof-safety.yml` pins echidna `556d6468…` (pre-contract). The + run on 2026-10-05 failed with a cancelled job and no logs. *Do not guess + the cause.* First re-run on a branch and capture logs, then decide (D7 is the pin bump). +* G-CI-5: `rhodibot.yml` is marked "78% red; retire or remake" in the + standards CI workflow catalog and the cicd-regularisation spec. + *Decision D4.* +* G-CI-6: Template workflows the repo lacks: `build-notification`, + `deed-validate`, `docker-build`, `dogfood-summary`, + `dot-wellknown-enforcement`, `e2e.yml.template`, `eclexiaiser-validate`, + `empty-linter`, `estate-rules`, `groove-check`, `guix-policy`, + `k9-validate`, `lock-sync-gate`, `ossf-best-practices`, + `rsr-compliance-canary`, `sonarqube`. Adopt the ones that apply to a Rust CLI + (`deed-validate`, `k9-validate`, `lock-sync-gate`, `estate-rules`, + `rsr-compliance-canary`, `ossf-best-practices`). Mark the rest N/A with a + reason. Do not copy all of them. +* G-CI-7: `.github/` duplicates. `FUNDING.yml` and `funding.yml` are both + present. Keep one. Extras vs template (`.mailmap`, `.nojekyll`, + `0.1-AI-MANIFEST.a2ml`, `DIRECTORY.adoc`, `MAINTAINERS`, `SUPPORT`) need a + keep/move decision each. +* G-CONT-1: The root `Containerfile` is an unfilled template: `TODO` stages, + `{{project}}` tokens, and a runtime stage with no binary. It is not a + working build for the Burrower CLI. *Decision D2:* keep and make it build + the `burrower` binary, or remove it and drop the `container` capability. + The `container/` scaffold follows the same decision. + +=== 2.7 Ecosystem registration + +* G-ECO-1: The standards `bot_exclusion_registry.a2ml` lists only + robot-repo-automaton and rhodibot/echidnabot source paths. Proof-burrower + is not in its `external-repos` list. Standards R6 decides whether it + should be. +* G-ECO-2: The gitbot-fleet roster (`docs/proofs/spec-templates/T2-high/gitbot-fleet.adoc`) + is rhodibot, echidnabot, sustainabot, glambot, seambot, finishbot. Each + hand-off in the companion file goes to one of these or to the named repo's + own maintainers. Policy: no standalone MCP servers; route through BoJ. + +== 3. Issue-by-issue path + +=== 3.1 #105 - combinatorial tactic-playbook synthesis (ParadisEO-mo) + +*Status:* open, `enhancement`, updated 2026-10-09. Acceptance criteria: +(a) the swarm synthesises multi-step proofs on benchmark lemmas that fail under +static single-specialist playbooks; (b) intermediate goal caching cuts redundant +prover invocations by at least 40% during local search; (c) full compatibility +with `burrow.jsonl` ledger formats. + +*Feasibility, from the code:* + +* `TacticTemplate` (`crates/burrower-core/src/attempt.rs:50`) is + `{name, script, description}`. `generate_probe` builds one + `lemma probe_lemma: … {script}` per attempt. There is *no multi-step tactic + AST*, so the neighbourhood operators (swap adjacent steps, substitute premise, + flip flags) have nothing to operate on yet. +* Step-level delta caching needs a stepwise proof-state interface from ECHIDNA. + echidna's stepwise surface is *thin*. The FFI `apply_tactic` sends a + Debug-formatted string and returns a clone of the input state. `verify_proof` + reads the file text. A proof state is `Term::Var(content)`. So no real + intermediate goal is available. The CLI has `interactive`, but no contracted + stepwise protocol exists. +* ParadisEO is C++. The language policy does not allow C++. *Recommendation: + reimplement the required pieces (tabu, VNS, neighbourhood evaluation) in + Rust.* No C++ dependency. + +*Phased path:* + +[cols="1,4,3", options="header"] +|=== +| Phase | Work | Exit + +| P1 - Tactic AST (Burrower only) +| Define a `TacticScript` as a list of steps for the Isabelle subset that the + swarm already emits. Add parse/print round-trip tests. Add the three + neighbourhood operators (swap, premise substitution by signature Jaccard + distance, flag change) as pure functions. +| Round-trip and operator unit tests pass. No prover calls. + +| P2 - Whole-script memoisation (Burrower only) +| Cache results keyed by `hash(lemma, script)`. Count prover invocations with + and without the cache on the benchmark set. This is an *honest interim*. A + memo hit requires an exact repeat, so it may not reach 40%. +| Measured invocation counts, reported as they are. + +| P3 - Stepwise caching (blocked) +| Needs the ECHIDNA stepwise contract (hand-off E-2 in the companion file). + Only then can "replay steps 1…k−1 from cache, evaluate from k" be + implemented. +| Blocked on echidna. Do not fake it. + +| P4 - Local search driver +| Tabu/VNS driver in the swarm, with strict attempt bounds and timeouts, and + a fall-back to manual review. +| Attempt bound and timeout tests pass. + +| P5 - Benchmark and acceptance +| Define the benchmark lemma set (lemmas that fail under static playbooks). + Reuse `docs/experiments/2026-04-26-tropical-comparison/` if it fits (20 + ledger records there). Owner decides the set (D9). Report (a) and (b) + against it. +| Acceptance (a) and (b) reported with numbers. (b) is marked not met if P3 is still blocked. + +| P6 - Ledger compatibility (c) +| Only *additive* optional fields in `LedgerRecord` (`crates/burrower-core/src/ledger.rs`). + Existing `pattern_kind` values (`positive|anti-pattern|specialisation|boundary`) + stay. Add a test that reads an old-format ledger unchanged. +| Old ledger fixtures parse. Round-trip test passes. +|=== + +*Hand-offs:* E-2 (echidna stepwise contract) for P3. The echidna-side +`suggest` JSON contract (E-3) is not needed for #105 and should not be bundled +with it. + +=== 3.2 #104 - anti-pattern mining and fitness formulation + +*Status:* open, `enhancement`, updated 2026-10-09. Acceptance criteria: +(a) unit tests show known ledger anti-patterns get significant negative fitness +penalties; (b) fitness evaluation under 1 ms per candidate script, in memory, +no live prover call; (c) CLI and socket endpoints follow the existing +line-delimited JSON API. + +*Feasibility, from the code:* + +* The ledger already has `pattern_kind` and `anti_patterns_for()` + (`crates/burrower-core/src/ledger.rs:182`). `burrower ledger anti-patterns` + reports them as text (`crates/burrower-cli/src/main.rs:218`). Reuse them. +* The issue uses `burrow.jsonl`. That file is not tracked in the repo (it is + produced at runtime by `attempt --ledger burrow.jsonl`). The tracked sample is + `docs/experiments/2026-04-26-tropical-comparison/ledger.jsonl` (20 records). + Use the tracked sample for unit tests. Do not commit a live `burrow.jsonl`. +* The socket surface is `burrower serve --socket /tmp/burrower.sock` + (`crates/burrower-cli/src/main.rs:130–138`; protocol in + `crates/burrower-core/src/serve.rs`). +* The `GoalReduction` term needs a remaining-sub-goal count from the prover. + echidna's stepwise path does not provide one (see 3.1). So `GoalReduction` + is *blocked*. +* The weights w1…w4 are not specified anywhere in the issue. *Decision D10.* + +*Phased path:* + +[cols="1,4,3", options="header"] +|=== +| Phase | Work | Exit + +| P1 - Ledger-only terms +| Implement `AntiPatternPenalty` (from `pattern_kind = anti-pattern` + records, matched by signature/learning), `EstimatedTime` (from recorded + durations), and `SignatureSimilarity` (token Jaccard, sharing code with the + indexer). `burrower_core::fitness` module, pure functions. +| Unit tests: anti-pattern fixtures from the tracked ledger get a large + negative penalty (acceptance a). + +| P2 - Latency +| Benchmark the in-memory evaluation (not the CLI process spawn). Target + under 1 ms per candidate. +| Benchmark result recorded (acceptance b). + +| P3 - Surfaces +| `burrower fitness "" ""` CLI subcommand. Matching + socket op in `serve.rs`, following the existing line-delimited JSON. +| Golden JSON tests for both (acceptance c). + +| P4 - GoalReduction (blocked) +| Add the term once E-2 (stepwise contract) provides sub-goal counts. +| Blocked on echidna. + +| P5 - Mining and calibration +| Mine the ledger for high-frequency failure loops (looping simplifier + rewrites, diverged inductions). Calibrate w1…w4 with the owner (D10). +| Weights and penalty matrix versioned and documented. +|=== + +*Hand-offs:* E-2 for P4; B-2 (echidnabot) only if echidnabot is to query fitness. +The issue says "ECHIDNA can query fitness". That is a consumer contract, +which can only follow the socket surface in P3. + +=== 3.3 #84 - embedded AffineScript tree (misfiled) + +*Status:* open, no label. Author `hyperpolymath`, created 2026-09-07. +The body lists the debt in the embedded `affinescript/` tree: placeholders in +the editor and bridge sources, a stub formatter, incomplete trait/unification +checks, Phase 6 runtime placeholders, Phase 8 package-manager placeholders, and +incomplete LSP fix suggestions. It asks for provenance, a dependency boundary, +reconciliation with the canonical repo, and no claim that tracking completes +the work. + +*Finding:* `affinescript/` is *absent from this repo*, and `git log --all -- affinescript` +returns *zero commits*. It was never committed here. The canonical repo +`hyperpolymath/affinescript` exists and is active (not archived). + +*Path:* + +. Confirm with the reporter (owner) that this is misfiled. (D5) +. Leave a comment on #84 pointing to `hyperpolymath/affinescript`, and state + that no affinescript code exists in this repo. +. Transfer the issue to `hyperpolymath/affinescript`, or close it here as + misfiled and reopen the tracking there. Either way, the acceptance criteria + (provenance, placeholder removal, tests) move with it. The owner decides + transfer vs close. +. Do not add an `affinescript/` directory to this repo. +. Keep the distinction the issue asks for: the independently tested + `burrower-core` / ECHIDNA Isabelle integration is not affinescript. + +== 4. Sequencing + +[cols="1,4,3", options="header"] +|=== +| Wave | Work | Gate + +| W0 - Decide +| Owner resolves D1–D10 (section 7). Standards reconciles R1–R8 (companion file). +| Decisions recorded in the repo (a short `docs/plans/DECISIONS-…` note). + +| W1 - Mechanical, no decision needed +| SPDX headers on the 6 files. Reword `.github/settings.yml` comments. Remove the duplicate `funding.yml`. Fix Justfile identity (`project`/`REPO`) and version alignment. Fix `phase` and version in `STATE.a2ml`. Remove the 3 `vlang` hits. Add the missing root items that apply (G-ROOT-2, e.g. `CLAUDE.md`, `.gitmessage`, `.mailmap`). Add `.tool-versions`. +| `must-spdx-headers`, `check-no-vlang`, `check-no-placeholders` (after the decided exemptions), `validate-state` passes. + +| W2 - Deed +| Extend `proof-burrower_chora.deed` with the missing clauses (`rsr-profile`, `meta`, `agentic`, `neurosym`, `playbook`, `bot-directives`, `contractiles`, `manifest`, `ply` (when ruled), `anchor`, `ensaid`, `integrations`, `policies`). Each clause follows its mapping spec. Lint with `deed_lint.js` and the bun CI gate. +| Deed lints; `validate-rsr` field checks pass for the clauses that exist. + +| W3 - Retire A2ML +| Family by family, switch readers (`.machine_readable/scripts/`, `validate-*`) to the deed, then remove the A2ML. Start with the smallest family. `0-AI-MANIFEST` and the ply tree last. +| `check-no-a2ml` passes. No reader references a removed file. + +| W4 - Gates and CI +| Adopt the applicable template workflows (G-CI-6). Decide `rhodibot.yml` (D4). Capture the 2026-10-05 `proof-safety` logs and fix. Bump the echidna pin only after the contract is confirmed (D7). +| `main` CI green. `proof-safety.yml` passes on the new pin. + +| W5 - Issues +| #105 P1–P2 and #104 P1–P3 can start in parallel after W0. #105 P3 and #104 P4 wait on E-2. #84 follows D5. +| Each phase's exit row in sections 3.1–3.3. +|=== + +Parallelism: W1 is independent of everything. W2 needs the mappings +(already in standards). W3 needs W2 per family. The issue work in W5 touches +only `crates/burrower-core` and does not depend on the repo tidy-up, so it can +run alongside W1–W3 with separate PRs. + +== 5. Acceptance for this plan + +This plan is accepted when: + +* Every gap in section 2 has an ID, a current state, a target, and a wave. +* #105, #104, and #84 each have a phased path, exit conditions, and the + acceptance criteria mapped to phases. +* Each cross-repo hand-off in `CROSS-REPO-HANDOFFS-2026-10-09.adoc` names a + target repo, a bot or maintainer, an ask, and an acceptance test. +* All owner decisions (section 7) are listed with a recommendation. +* No file outside `docs/plans/` has been changed by this plan. + +== 6. Risks and unknowns + +* *Oracle not implemented.* Compliance is inferred. `hypatia:rsr-conformance` + (named in standards `docs/AFFIRMATION.adoc` and `docs/AUDIT.adoc`) does not + yet produce a tier score. +* *`proof-safety.yml` run 37371572643 (2026-10-05)* failed with a cancelled job + and no logs. The cause is unknown. +* *Upstream tension.* RSR criteria 2.1.0-draft require A2ML; the deed is the + format for new work. Until standards reconciles them, any A2ML removal is + premature. +* *Ply mapping.* No ruled mapping. Ply content is referenced in + `meta-ecosystem-to-repo-deed.adoc` and `ai-manifest-decision.adoc`, and + `2-protocols/0-ai-gatekeeper/docs/AI-MANIFEST-SPEC.adoc` still describes ply + prefixes. +* *Echidna stepwise contract absent.* Blocks #105 P3 and #104 P4. +* *`timeout` and `unknown` untested end-to-end.* The echidna contract spec says + these statuses are covered only by golden unit tests (no backend without an + external prover produces them). echidnabot and Burrower both rely on them. +* *Language policy vs ParadisEO.* C++ is not allowed. A Rust reimplementation + is slower to build than a binding, but no policy exception is assumed. +* *Presence-proxy baseline* (section 1.1) is not a score. + +== 7. Owner decisions + +[cols="1,4,5", options="header"] +|=== +| ID | Question | Recommendation + +| D1 +| `0-AI-MANIFEST` mapping: which option? +| Option A (the mapping's recommended option). Ply left in place until ruled. + +| D2 +| Keep the root `Containerfile` and `container/`, or remove them? +| Remove unless the CLI is to be shipped as a container. A CLI with no container use case should not claim the `container` capability. If kept, make it build the `burrower` binary. + +| D3 +| Rust-workspace allowlist entries (`Cargo.toml`, `Cargo.lock`, `crates/`, `rust-toolchain.toml`). +| Standards adds gated `?` entries for Rust workspaces. Repo keeps the layout. No repo moves. + +| D4 +| `rhodibot.yml`: retire or remake? +| Retire, and rebuild from the template gate that replaces it. It is 78% red. + +| D5 +| #84: transfer to `hyperpolymath/affinescript`, or close as misfiled? +| Confirm misfiled, comment with the pointer, then transfer (keeps the acceptance criteria attached). + +| D6 +| `agents/*.007` licence (MPL-2.0 headers vs possible ARR)? +| Owner checks the DSL licence before any header change. + +| D7 +| Bump the echidna pin in `proof-safety.yml` from `556d6468…` to current `main` (`822cfc9`) or any commit at or after `a71aa2c`? +| Bump after the 2026-10-05 failure is diagnosed, so the cause is not confused with the pin change. + +| D8 +| `coordination.k9` vs `coordination.k9.ncl`? +| Follow the template (`coordination.k9.ncl`) and rename, unless standards rules the other way. + +| D9 +| Benchmark lemma set for #105 P5. +| Owner names the lemmas. Reuse the tropical-comparison set if it fits. + +| D10 +| Fitness weights w1…w4 and penalty matrix for #104. +| Start with equal weights and calibrate on the tracked ledger. Owner signs off the values. +|=== + +== Appendix A. Source paths + +* Repo: `proof-burrower_chora.deed`, `Justfile`, `Containerfile`, `container/`, + `.github/workflows/proof-safety.yml`, `.github/workflows/dogfood-gate.yml`, + `crates/burrower-core/src/{attempt,ledger,serve}.rs`, + `crates/burrower-cli/src/main.rs`, `docs/ECHIDNA-INTEGRATION.adoc`, + `docs/experiments/2026-04-26-tropical-comparison/ledger.jsonl`. +* Standards (`hyperpolymath/standards`): `0-canon/rsr/rsr-criteria-v2.a2ml`, + `0-canon/rsr/RSR-SPEC-v2.adoc`, `0-canon/TEMPLATE-APPLICABILITY-POLICY.adoc`, + `1-formats/deed/spec/abnf/deed.abnf`, `1-formats/deed/mappings/`, + `1-formats/deed/tools/deed_lint.js`, `.meta/REQUIRED-FILES.adoc`, + `scripts/check-rsr-profile.sh`, `docs/proofs/spec-templates/T2-high/gitbot-fleet.adoc`. +* Template (`hyperpolymath/rsr-template-repo`): `.machine_readable/root-allow.txt`, + `rsr-template-repo_chora.deed` (worked model), `scripts/check-root-shape.sh`. +* Echidna (`hyperpolymath/echidna`, `822cfc9`): `docs/PROVE-RESULT-CONTRACT.adoc`, + `src/interfaces/graphql/{resolvers,ffi_wrapper}.rs`, `src/rust/server.rs`, + `Cargo.toml` (2.3.0). +* Echidnabot (`hyperpolymath/echidnabot`, `ac67dc3`): `src/dispatcher/echidna_client.rs` + (`MIN_ECHIDNA_VERSION` 2.3.0), `src/dispatcher/prove_result.rs`.