diff --git a/.github/issues/echidnabot-01-adaptive-ci-portfolio-scheduler.md b/.github/issues/echidnabot-01-adaptive-ci-portfolio-scheduler.md index 45a1d7da..9258aef1 100644 --- a/.github/issues/echidnabot-01-adaptive-ci-portfolio-scheduler.md +++ b/.github/issues/echidnabot-01-adaptive-ci-portfolio-scheduler.md @@ -21,7 +21,7 @@ Applying Automated Algorithm Selection and Parameter Tuning principles from Para ## Current State Verified against echidnabot@ae5283323b815f82d2a556080b59e0bb648de62b: -- `enqueue_repo_jobs` in `src/api/webhooks.rs` creates one job per enabled prover (VERIFIED: iterates over `repo.enabled_provers`) +- `enqueue_repo_jobs` in `echidnabot/src/api/webhooks.rs` creates one job per enabled prover (VERIFIED: iterates over `repo.enabled_provers`) - `JobLimiter` defaults to 10 global / 3 per repo concurrent jobs (VERIFIED: in limiter.rs) - Static 300 second timeouts are used as default (VERIFIED: `default_timeout()` returns 300 in config.rs) - `manifest [provers.] timeout_seconds` is wired into dispatch (VERIFIED: accessed in manifest.rs, used in echidna_client.rs) diff --git a/.hypatia-baseline.json b/.hypatia-baseline.json index 693f097d..8036d320 100644 --- a/.hypatia-baseline.json +++ b/.hypatia-baseline.json @@ -1,539 +1 @@ -[ - { - "severity": "high", - "rule_module": "code_safety", - "type": "from_raw", - "file": "src/rust/ffi/mod.rs", - "tracking_issue": "hyperpolymath/echidna#314" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "from_raw", - "file": "src/rust/provers/opensmt.rs", - "tracking_issue": "hyperpolymath/echidna#314" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "lock_unwrap", - "file": "src/rust/dispatch.rs", - "tracking_issue": "hyperpolymath/echidna#314" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "lock_unwrap", - "file": "src/rust/fault_tolerance/resilience.rs", - "tracking_issue": "hyperpolymath/echidna#314" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "lock_unwrap", - "file": "src/rust/provers/lean.rs", - "tracking_issue": "hyperpolymath/echidna#314" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "mem_forget", - "file": "src/rust/ffi/mod.rs", - "tracking_issue": "hyperpolymath/echidna#314" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "panic_macro", - "file": "src/rust/verification/axiom_tracker.rs", - "tracking_issue": "hyperpolymath/echidna#314" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "crates/typed_wasm/src/lib.rs", - "tracking_issue": "hyperpolymath/echidna#314" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/interfaces/graphql/schema.rs", - "tracking_issue": "hyperpolymath/echidna#314" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/agent/actors.rs", - "tracking_issue": "hyperpolymath/echidna#314" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/coprocessor/graphics.rs", - "tracking_issue": "hyperpolymath/echidna#314" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/coprocessor/macaulay2.rs", - "tracking_issue": "hyperpolymath/echidna#314" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/coprocessor/maxima.rs", - "tracking_issue": "hyperpolymath/echidna#314" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/coprocessor/parigp.rs", - "tracking_issue": "hyperpolymath/echidna#314" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/coprocessor/singular.rs", - "tracking_issue": "hyperpolymath/echidna#314" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/dispatch.rs", - "tracking_issue": "hyperpolymath/echidna#314" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/fault_tolerance/resilience.rs", - "tracking_issue": "hyperpolymath/echidna#314" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/ipc/mod.rs", - "tracking_issue": "hyperpolymath/echidna#314" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/proof_search.rs", - "tracking_issue": "hyperpolymath/echidna#314" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/coq.rs", - "tracking_issue": "hyperpolymath/echidna#314" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/framac.rs", - "tracking_issue": "hyperpolymath/echidna#314" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/lean.rs", - "tracking_issue": "hyperpolymath/echidna#314" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/mizar.rs", - "tracking_issue": "hyperpolymath/echidna#314" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/repl/diagnostics.rs", - "tracking_issue": "hyperpolymath/echidna#314" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/repl/proof.rs", - "tracking_issue": "hyperpolymath/echidna#314" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/server.rs", - "tracking_issue": "hyperpolymath/echidna#314" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/verification/portfolio.rs", - "tracking_issue": "hyperpolymath/echidna#314" - }, - { - "severity": "medium", - "rule_module": "code_safety", - "type": "expect_in_hot_path", - "file": "src/rust/learning/design_search.rs", - "note": "expect() triage tracked with existing unwrap_without_check debt", - "tracking_issue": "hyperpolymath/echidna#314" - }, - { - "severity": "medium", - "rule_module": "code_safety", - "type": "expect_in_hot_path", - "file": "src/rust/provers/z3.rs", - "note": "expect() triage tracked with existing unwrap_without_check debt", - "tracking_issue": "hyperpolymath/echidna#314" - }, - { - "severity": "medium", - "rule_module": "code_safety", - "type": "expect_in_hot_path", - "file": "src/rust/coprocessor/julia_bridge.rs", - "note": "expect() triage tracked with existing unwrap_without_check debt", - "tracking_issue": "hyperpolymath/echidna#314" - }, - { - "severity": "medium", - "rule_module": "code_safety", - "type": "expect_in_hot_path", - "file": "src/rust/coprocessor/math.rs", - "note": "expect() triage tracked with existing unwrap_without_check debt", - "tracking_issue": "hyperpolymath/echidna#314" - }, - { - "severity": "medium", - "rule_module": "code_safety", - "type": "expect_in_hot_path", - "file": "src/rust/gnn/client.rs", - "note": "expect() triage tracked with existing unwrap_without_check debt", - "tracking_issue": "hyperpolymath/echidna#314" - }, - { - "severity": "medium", - "rule_module": "code_safety", - "type": "expect_in_hot_path", - "file": "src/rust/llm.rs", - "note": "expect() triage tracked with existing unwrap_without_check debt", - "tracking_issue": "hyperpolymath/echidna#314" - }, - { - "severity": "medium", - "rule_module": "code_safety", - "type": "expect_in_hot_path", - "file": "src/rust/neural.rs", - "note": "expect() triage tracked with existing unwrap_without_check debt", - "tracking_issue": "hyperpolymath/echidna#314" - }, - { - "severity": "medium", - "rule_module": "code_safety", - "type": "expect_in_hot_path", - "file": "src/rust/corpus/octad.rs", - "note": "expect() triage tracked with existing unwrap_without_check debt", - "tracking_issue": "hyperpolymath/echidna#314" - }, - { - "severity": "medium", - "rule_module": "code_safety", - "type": "expect_in_hot_path", - "file": "src/interfaces/graphql/resolvers.rs", - "note": "expect() triage tracked with existing unwrap_without_check debt", - "tracking_issue": "hyperpolymath/echidna#314" - }, - { - "severity": "medium", - "rule_module": "code_safety", - "type": "unsafe_block", - "file": "src/rust/ffi/mod.rs", - "note": "FFI boundary; SAFETY-comment sweep pending", - "tracking_issue": "hyperpolymath/echidna#314" - }, - { - "severity": "medium", - "rule_module": "code_safety", - "type": "unsafe_block", - "file": "src/rust/ffi/spark_axiom.rs", - "note": "FFI boundary; SAFETY-comment sweep pending", - "tracking_issue": "hyperpolymath/echidna#314" - }, - { - "severity": "medium", - "rule_module": "code_safety", - "type": "unsafe_block", - "file": "src/rust/coprocessor/flint.rs", - "note": "FFI boundary; SAFETY-comment sweep pending", - "tracking_issue": "hyperpolymath/echidna#314" - }, - { - "severity": "medium", - "rule_module": "code_safety", - "type": "unsafe_block", - "file": "src/rust/proof_search.rs", - "note": "FFI boundary; SAFETY-comment sweep pending", - "tracking_issue": "hyperpolymath/echidna#314" - }, - { - "severity": "medium", - "rule_module": "code_safety", - "type": "unsafe_block", - "file": "src/interfaces/grpc/ffi_wrapper.rs", - "note": "FFI boundary; SAFETY-comment sweep pending", - "tracking_issue": "hyperpolymath/echidna#314" - }, - { - "severity": "medium", - "rule_module": "code_safety", - "type": "unsafe_block", - "file": "src/interfaces/rest/ffi_wrapper.rs", - "note": "FFI boundary; SAFETY-comment sweep pending", - "tracking_issue": "hyperpolymath/echidna#314" - }, - { - "severity": "medium", - "rule_module": "code_safety", - "type": "unsafe_block", - "file": "src/interfaces/graphql/ffi_wrapper.rs", - "note": "FFI boundary; SAFETY-comment sweep pending", - "tracking_issue": "hyperpolymath/echidna#314" - }, - { - "severity": "medium", - "rule_module": "code_safety", - "type": "as_ptr", - "file": "src/rust/ffi/mod.rs", - "note": "FFI boundary; pointer-lifetime audit pending", - "tracking_issue": "hyperpolymath/echidna#314" - }, - { - "severity": "medium", - "rule_module": "code_safety", - "type": "as_ptr", - "file": "src/rust/ffi/spark_axiom.rs", - "note": "FFI boundary; pointer-lifetime audit pending", - "tracking_issue": "hyperpolymath/echidna#314" - }, - { - "severity": "medium", - "rule_module": "code_safety", - "type": "as_ptr", - "file": "src/rust/coprocessor/flint.rs", - "note": "FFI boundary; pointer-lifetime audit pending", - "tracking_issue": "hyperpolymath/echidna#314" - }, - { - "severity": "medium", - "rule_module": "code_safety", - "type": "as_ptr", - "file": "src/rust/proof_search.rs", - "note": "FFI boundary; pointer-lifetime audit pending", - "tracking_issue": "hyperpolymath/echidna#314" - }, - { - "severity": "medium", - "rule_module": "code_safety", - "type": "as_ptr", - "file": "src/interfaces/grpc/ffi_wrapper.rs", - "note": "FFI boundary; pointer-lifetime audit pending", - "tracking_issue": "hyperpolymath/echidna#314" - }, - { - "severity": "medium", - "rule_module": "code_safety", - "type": "as_ptr", - "file": "src/interfaces/rest/ffi_wrapper.rs", - "note": "FFI boundary; pointer-lifetime audit pending", - "tracking_issue": "hyperpolymath/echidna#314" - }, - { - "severity": "medium", - "rule_module": "code_safety", - "type": "as_ptr", - "file": "src/interfaces/graphql/ffi_wrapper.rs", - "note": "FFI boundary; pointer-lifetime audit pending", - "tracking_issue": "hyperpolymath/echidna#314" - }, - { - "severity": "medium", - "rule_module": "structural_drift", - "type": "SD022", - "file": ".machine_readable/descriptiles/STATE.a2ml", - "note": "Paths cited are in EXTERNAL corpora repos (mirror-isabelle, viperproject/silver, vcl-ut), not this tree; SD022 cannot see that", - "tracking_issue": "hyperpolymath/echidna#314" - }, - { - "severity": "medium", - "rule_module": "structural_drift", - "type": "SD022", - "file": "docs/SSG_ROADMAP.adoc", - "note": "Roadmap doc: paths are planned future modules, not renames", - "tracking_issue": "hyperpolymath/echidna#314" - }, - { - "severity": "medium", - "rule_module": "workflow_audit", - "type": "unpinned_action", - "file": "agda-meta-checker.yml", - "tracking_issue": "hyperpolymath/echidna#314" - }, - { - "severity": "medium", - "rule_module": "workflow_audit", - "type": "unpinned_action", - "file": "codeql.yml", - "tracking_issue": "hyperpolymath/echidna#314" - }, - { - "severity": "medium", - "rule_module": "workflow_audit", - "type": "unpinned_action", - "file": "mvp-smoke.yml", - "tracking_issue": "hyperpolymath/echidna#314" - }, - { - "severity": "medium", - "rule_module": "workflow_audit", - "type": "unpinned_action", - "file": "s4-loop.yml", - "tracking_issue": "hyperpolymath/echidna#314" - }, - { - "severity": "medium", - "rule_module": "research_extensions", - "type": "RE001", - "file": ".github/workflows/labels.yml", - "tracking_issue": "hyperpolymath/echidna#314", - "note": "pre-existing on main; grandfathered at re-arm, burn down under #314" - }, - { - "severity": "medium", - "rule_module": "research_extensions", - "type": "RE001", - "file": ".github/workflows/cflite_batch.yml", - "tracking_issue": "hyperpolymath/echidna#314", - "note": "pre-existing on main; grandfathered at re-arm, burn down under #314" - }, - { - "severity": "medium", - "rule_module": "research_extensions", - "type": "RE001", - "file": ".github/workflows/cflite_pr.yml", - "tracking_issue": "hyperpolymath/echidna#314", - "note": "pre-existing on main; grandfathered at re-arm, burn down under #314" - }, - { - "severity": "medium", - "rule_module": "research_extensions", - "type": "RE001", - "file": ".github/workflows/ghcr-publish.yml", - "tracking_issue": "hyperpolymath/echidna#314", - "note": "pre-existing on main; grandfathered at re-arm, burn down under #314" - }, - { - "severity": "medium", - "rule_module": "research_extensions", - "type": "RE001", - "file": ".github/workflows/label-triage.yml", - "tracking_issue": "hyperpolymath/echidna#314", - "note": "pre-existing on main; grandfathered at re-arm, burn down under #314" - }, - { - "severity": "medium", - "rule_module": "research_extensions", - "type": "RE004", - "file": ".github/workflows/s4-loop.yml", - "tracking_issue": "hyperpolymath/echidna#314", - "note": "pre-existing on main; grandfathered at re-arm, burn down under #314" - }, - { - "severity": "medium", - "rule_module": "research_extensions", - "type": "RE004", - "file": ".github/workflows/container-ci.yml", - "tracking_issue": "hyperpolymath/echidna#314", - "note": "pre-existing on main; grandfathered at re-arm, burn down under #314" - }, - { - "severity": "medium", - "rule_module": "research_extensions", - "type": "RE005", - "file": ".github/workflows/server-boot-gate.yml", - "tracking_issue": "hyperpolymath/echidna#314", - "note": "pre-existing on main; grandfathered at re-arm, burn down under #314" - }, - { - "severity": "medium", - "rule_module": "research_extensions", - "type": "RE005", - "file": ".github/workflows/live-provers.yml", - "tracking_issue": "hyperpolymath/echidna#314", - "note": "pre-existing on main; grandfathered at re-arm, burn down under #314" - }, - { - "severity": "medium", - "rule_module": "workflow_hardening", - "type": "WH008", - "file": ".github/workflows/scorecard.yml", - "tracking_issue": "hyperpolymath/echidna#314", - "note": "pre-existing on main; grandfathered at re-arm, burn down under #314" - }, - { - "severity": "medium", - "rule_module": "workflow_hardening", - "type": "WH008", - "file": ".github/workflows/secret-scanner.yml", - "tracking_issue": "hyperpolymath/echidna#314", - "note": "pre-existing on main; grandfathered at re-arm, burn down under #314" - }, - { - "severity": "medium", - "rule_module": "workflow_hardening", - "type": "WH008", - "file": ".github/workflows/hypatia-scan.yml", - "tracking_issue": "hyperpolymath/echidna#314", - "note": "pre-existing on main; grandfathered at re-arm, burn down under #314" - }, - { - "severity": "medium", - "rule_module": "workflow_hardening", - "type": "WH008", - "file": ".github/workflows/mirror.yml", - "tracking_issue": "hyperpolymath/echidna#314", - "note": "pre-existing on main; grandfathered at re-arm, burn down under #314" - }, - { - "severity": "medium", - "rule_module": "structural_drift", - "type": "SD022", - "file": "docs/STALE-REFERENCE-TOMBSTONES.adoc", - "tracking_issue": "hyperpolymath/echidna#314", - "note": "tombstone document: references to removed paths are intentional" - }, - { - "severity": "medium", - "rule_module": "content_patterns", - "type": "download_then_run_shell", - "file": "echidna-playground/.github/workflows/mirror.yml", - "tracking_issue": "hyperpolymath/echidna#314", - "note": "pre-existing on main; grandfathered at re-arm, burn down under #314" - } -] +[{"file":"src/rust/ffi/mod.rs","rule_module":"code_safety","severity":"high","tracking_issue":"hyperpolymath/echidna#314","type":"from_raw"},{"file":"src/rust/provers/opensmt.rs","rule_module":"code_safety","severity":"high","tracking_issue":"hyperpolymath/echidna#314","type":"from_raw"},{"file":"src/rust/dispatch.rs","rule_module":"code_safety","severity":"high","tracking_issue":"hyperpolymath/echidna#314","type":"lock_unwrap"},{"file":"src/rust/fault_tolerance/resilience.rs","rule_module":"code_safety","severity":"high","tracking_issue":"hyperpolymath/echidna#314","type":"lock_unwrap"},{"file":"src/rust/provers/lean.rs","rule_module":"code_safety","severity":"high","tracking_issue":"hyperpolymath/echidna#314","type":"lock_unwrap"},{"file":"src/rust/ffi/mod.rs","rule_module":"code_safety","severity":"high","tracking_issue":"hyperpolymath/echidna#314","type":"mem_forget"},{"file":"src/rust/verification/axiom_tracker.rs","rule_module":"code_safety","severity":"high","tracking_issue":"hyperpolymath/echidna#314","type":"panic_macro"},{"file":"crates/typed_wasm/src/lib.rs","rule_module":"code_safety","severity":"high","tracking_issue":"hyperpolymath/echidna#314","type":"unwrap_without_check"},{"file":"src/interfaces/graphql/schema.rs","rule_module":"code_safety","severity":"high","tracking_issue":"hyperpolymath/echidna#314","type":"unwrap_without_check"},{"file":"src/rust/agent/actors.rs","rule_module":"code_safety","severity":"high","tracking_issue":"hyperpolymath/echidna#314","type":"unwrap_without_check"},{"file":"src/rust/coprocessor/graphics.rs","rule_module":"code_safety","severity":"high","tracking_issue":"hyperpolymath/echidna#314","type":"unwrap_without_check"},{"file":"src/rust/coprocessor/macaulay2.rs","rule_module":"code_safety","severity":"high","tracking_issue":"hyperpolymath/echidna#314","type":"unwrap_without_check"},{"file":"src/rust/coprocessor/maxima.rs","rule_module":"code_safety","severity":"high","tracking_issue":"hyperpolymath/echidna#314","type":"unwrap_without_check"},{"file":"src/rust/coprocessor/parigp.rs","rule_module":"code_safety","severity":"high","tracking_issue":"hyperpolymath/echidna#314","type":"unwrap_without_check"},{"file":"src/rust/coprocessor/singular.rs","rule_module":"code_safety","severity":"high","tracking_issue":"hyperpolymath/echidna#314","type":"unwrap_without_check"},{"file":"src/rust/dispatch.rs","rule_module":"code_safety","severity":"high","tracking_issue":"hyperpolymath/echidna#314","type":"unwrap_without_check"},{"file":"src/rust/fault_tolerance/resilience.rs","rule_module":"code_safety","severity":"high","tracking_issue":"hyperpolymath/echidna#314","type":"unwrap_without_check"},{"file":"src/rust/ipc/mod.rs","rule_module":"code_safety","severity":"high","tracking_issue":"hyperpolymath/echidna#314","type":"unwrap_without_check"},{"file":"src/rust/proof_search.rs","rule_module":"code_safety","severity":"high","tracking_issue":"hyperpolymath/echidna#314","type":"unwrap_without_check"},{"file":"src/rust/provers/coq.rs","rule_module":"code_safety","severity":"high","tracking_issue":"hyperpolymath/echidna#314","type":"unwrap_without_check"},{"file":"src/rust/provers/framac.rs","rule_module":"code_safety","severity":"high","tracking_issue":"hyperpolymath/echidna#314","type":"unwrap_without_check"},{"file":"src/rust/provers/lean.rs","rule_module":"code_safety","severity":"high","tracking_issue":"hyperpolymath/echidna#314","type":"unwrap_without_check"},{"file":"src/rust/provers/mizar.rs","rule_module":"code_safety","severity":"high","tracking_issue":"hyperpolymath/echidna#314","type":"unwrap_without_check"},{"file":"src/rust/repl/diagnostics.rs","rule_module":"code_safety","severity":"high","tracking_issue":"hyperpolymath/echidna#314","type":"unwrap_without_check"},{"file":"src/rust/repl/proof.rs","rule_module":"code_safety","severity":"high","tracking_issue":"hyperpolymath/echidna#314","type":"unwrap_without_check"},{"file":"src/rust/server.rs","rule_module":"code_safety","severity":"high","tracking_issue":"hyperpolymath/echidna#314","type":"unwrap_without_check"},{"file":"src/rust/verification/portfolio.rs","rule_module":"code_safety","severity":"high","tracking_issue":"hyperpolymath/echidna#314","type":"unwrap_without_check"},{"file":"src/rust/learning/design_search.rs","note":"expect() triage tracked with existing unwrap_without_check debt","rule_module":"code_safety","severity":"medium","tracking_issue":"hyperpolymath/echidna#314","type":"expect_in_hot_path"},{"file":"src/rust/provers/z3.rs","note":"expect() triage tracked with existing unwrap_without_check debt","rule_module":"code_safety","severity":"medium","tracking_issue":"hyperpolymath/echidna#314","type":"expect_in_hot_path"},{"file":"src/rust/coprocessor/julia_bridge.rs","note":"expect() triage tracked with existing unwrap_without_check debt","rule_module":"code_safety","severity":"medium","tracking_issue":"hyperpolymath/echidna#314","type":"expect_in_hot_path"},{"file":"src/rust/coprocessor/math.rs","note":"expect() triage tracked with existing unwrap_without_check debt","rule_module":"code_safety","severity":"medium","tracking_issue":"hyperpolymath/echidna#314","type":"expect_in_hot_path"},{"file":"src/rust/gnn/client.rs","note":"expect() triage tracked with existing unwrap_without_check debt","rule_module":"code_safety","severity":"medium","tracking_issue":"hyperpolymath/echidna#314","type":"expect_in_hot_path"},{"file":"src/rust/llm.rs","note":"expect() triage tracked with existing unwrap_without_check debt","rule_module":"code_safety","severity":"medium","tracking_issue":"hyperpolymath/echidna#314","type":"expect_in_hot_path"},{"file":"src/rust/neural.rs","note":"expect() triage tracked with existing unwrap_without_check debt","rule_module":"code_safety","severity":"medium","tracking_issue":"hyperpolymath/echidna#314","type":"expect_in_hot_path"},{"file":"src/rust/corpus/octad.rs","note":"expect() triage tracked with existing unwrap_without_check debt","rule_module":"code_safety","severity":"medium","tracking_issue":"hyperpolymath/echidna#314","type":"expect_in_hot_path"},{"file":"src/interfaces/graphql/resolvers.rs","note":"expect() triage tracked with existing unwrap_without_check debt","rule_module":"code_safety","severity":"medium","tracking_issue":"hyperpolymath/echidna#314","type":"expect_in_hot_path"},{"file":"src/rust/ffi/mod.rs","note":"FFI boundary; SAFETY-comment sweep pending","rule_module":"code_safety","severity":"medium","tracking_issue":"hyperpolymath/echidna#314","type":"unsafe_block"},{"file":"src/rust/ffi/spark_axiom.rs","note":"FFI boundary; SAFETY-comment sweep pending","rule_module":"code_safety","severity":"medium","tracking_issue":"hyperpolymath/echidna#314","type":"unsafe_block"},{"file":"src/rust/coprocessor/flint.rs","note":"FFI boundary; SAFETY-comment sweep pending","rule_module":"code_safety","severity":"medium","tracking_issue":"hyperpolymath/echidna#314","type":"unsafe_block"},{"file":"src/rust/proof_search.rs","note":"FFI boundary; SAFETY-comment sweep pending","rule_module":"code_safety","severity":"medium","tracking_issue":"hyperpolymath/echidna#314","type":"unsafe_block"},{"file":"src/interfaces/grpc/ffi_wrapper.rs","note":"FFI boundary; SAFETY-comment sweep pending","rule_module":"code_safety","severity":"medium","tracking_issue":"hyperpolymath/echidna#314","type":"unsafe_block"},{"file":"src/interfaces/rest/ffi_wrapper.rs","note":"FFI boundary; SAFETY-comment sweep pending","rule_module":"code_safety","severity":"medium","tracking_issue":"hyperpolymath/echidna#314","type":"unsafe_block"},{"file":"src/interfaces/graphql/ffi_wrapper.rs","note":"FFI boundary; SAFETY-comment sweep pending","rule_module":"code_safety","severity":"medium","tracking_issue":"hyperpolymath/echidna#314","type":"unsafe_block"},{"file":"src/rust/ffi/mod.rs","note":"FFI boundary; pointer-lifetime audit pending","rule_module":"code_safety","severity":"medium","tracking_issue":"hyperpolymath/echidna#314","type":"as_ptr"},{"file":"src/rust/ffi/spark_axiom.rs","note":"FFI boundary; pointer-lifetime audit pending","rule_module":"code_safety","severity":"medium","tracking_issue":"hyperpolymath/echidna#314","type":"as_ptr"},{"file":"src/rust/coprocessor/flint.rs","note":"FFI boundary; pointer-lifetime audit pending","rule_module":"code_safety","severity":"medium","tracking_issue":"hyperpolymath/echidna#314","type":"as_ptr"},{"file":"src/rust/proof_search.rs","note":"FFI boundary; pointer-lifetime audit pending","rule_module":"code_safety","severity":"medium","tracking_issue":"hyperpolymath/echidna#314","type":"as_ptr"},{"file":"src/interfaces/grpc/ffi_wrapper.rs","note":"FFI boundary; pointer-lifetime audit pending","rule_module":"code_safety","severity":"medium","tracking_issue":"hyperpolymath/echidna#314","type":"as_ptr"},{"file":"src/interfaces/rest/ffi_wrapper.rs","note":"FFI boundary; pointer-lifetime audit pending","rule_module":"code_safety","severity":"medium","tracking_issue":"hyperpolymath/echidna#314","type":"as_ptr"},{"file":"src/interfaces/graphql/ffi_wrapper.rs","note":"FFI boundary; pointer-lifetime audit pending","rule_module":"code_safety","severity":"medium","tracking_issue":"hyperpolymath/echidna#314","type":"as_ptr"},{"file":".machine_readable/descriptiles/STATE.a2ml","note":"Paths cited are in EXTERNAL corpora repos (mirror-isabelle, viperproject/silver, vcl-ut), not this tree; SD022 cannot see that","rule_module":"structural_drift","severity":"medium","tracking_issue":"hyperpolymath/echidna#314","type":"SD022"},{"file":"docs/SSG_ROADMAP.adoc","note":"Roadmap doc: paths are planned future modules, not renames","rule_module":"structural_drift","severity":"medium","tracking_issue":"hyperpolymath/echidna#314","type":"SD022"},{"file":"agda-meta-checker.yml","rule_module":"workflow_audit","severity":"medium","tracking_issue":"hyperpolymath/echidna#314","type":"unpinned_action"},{"file":"codeql.yml","rule_module":"workflow_audit","severity":"medium","tracking_issue":"hyperpolymath/echidna#314","type":"unpinned_action"},{"file":"mvp-smoke.yml","rule_module":"workflow_audit","severity":"medium","tracking_issue":"hyperpolymath/echidna#314","type":"unpinned_action"},{"file":"s4-loop.yml","rule_module":"workflow_audit","severity":"medium","tracking_issue":"hyperpolymath/echidna#314","type":"unpinned_action"},{"file":".github/workflows/labels.yml","note":"pre-existing on main; grandfathered at re-arm, burn down under #314","rule_module":"research_extensions","severity":"medium","tracking_issue":"hyperpolymath/echidna#314","type":"RE001"},{"file":".github/workflows/cflite_batch.yml","note":"pre-existing on main; grandfathered at re-arm, burn down under #314","rule_module":"research_extensions","severity":"medium","tracking_issue":"hyperpolymath/echidna#314","type":"RE001"},{"file":".github/workflows/cflite_pr.yml","note":"pre-existing on main; grandfathered at re-arm, burn down under #314","rule_module":"research_extensions","severity":"medium","tracking_issue":"hyperpolymath/echidna#314","type":"RE001"},{"file":".github/workflows/ghcr-publish.yml","note":"pre-existing on main; grandfathered at re-arm, burn down under #314","rule_module":"research_extensions","severity":"medium","tracking_issue":"hyperpolymath/echidna#314","type":"RE001"},{"file":".github/workflows/label-triage.yml","note":"pre-existing on main; grandfathered at re-arm, burn down under #314","rule_module":"research_extensions","severity":"medium","tracking_issue":"hyperpolymath/echidna#314","type":"RE001"},{"file":".github/workflows/s4-loop.yml","note":"pre-existing on main; grandfathered at re-arm, burn down under #314","rule_module":"research_extensions","severity":"medium","tracking_issue":"hyperpolymath/echidna#314","type":"RE004"},{"file":".github/workflows/container-ci.yml","note":"pre-existing on main; grandfathered at re-arm, burn down under #314","rule_module":"research_extensions","severity":"medium","tracking_issue":"hyperpolymath/echidna#314","type":"RE004"},{"file":".github/workflows/server-boot-gate.yml","note":"pre-existing on main; grandfathered at re-arm, burn down under #314","rule_module":"research_extensions","severity":"medium","tracking_issue":"hyperpolymath/echidna#314","type":"RE005"},{"file":".github/workflows/live-provers.yml","note":"pre-existing on main; grandfathered at re-arm, burn down under #314","rule_module":"research_extensions","severity":"medium","tracking_issue":"hyperpolymath/echidna#314","type":"RE005"},{"file":".github/workflows/scorecard.yml","note":"pre-existing on main; grandfathered at re-arm, burn down under #314","rule_module":"workflow_hardening","severity":"medium","tracking_issue":"hyperpolymath/echidna#314","type":"WH008"},{"file":".github/workflows/secret-scanner.yml","note":"pre-existing on main; grandfathered at re-arm, burn down under #314","rule_module":"workflow_hardening","severity":"medium","tracking_issue":"hyperpolymath/echidna#314","type":"WH008"},{"file":".github/workflows/hypatia-scan.yml","note":"pre-existing on main; grandfathered at re-arm, burn down under #314","rule_module":"workflow_hardening","severity":"medium","tracking_issue":"hyperpolymath/echidna#314","type":"WH008"},{"file":".github/workflows/mirror.yml","note":"pre-existing on main; grandfathered at re-arm, burn down under #314","rule_module":"workflow_hardening","severity":"medium","tracking_issue":"hyperpolymath/echidna#314","type":"WH008"},{"file":"docs/STALE-REFERENCE-TOMBSTONES.adoc","note":"tombstone document: references to removed paths are intentional","rule_module":"structural_drift","severity":"medium","tracking_issue":"hyperpolymath/echidna#314","type":"SD022"}] diff --git a/docs/handover/PARADISEO-ROADMAP-PROMPT.adoc b/docs/handover/PARADISEO-ROADMAP-PROMPT.adoc index b6e87554..8fd4d7b4 100644 --- a/docs/handover/PARADISEO-ROADMAP-PROMPT.adoc +++ b/docs/handover/PARADISEO-ROADMAP-PROMPT.adoc @@ -212,7 +212,7 @@ PB-01 wants partial progress (for example `subgoals_remaining`). The hazard: `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` +* *echidnabot's own parser rejects them*: `echidnabot/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. diff --git a/echidna-playground/ci-templates/README.adoc b/echidna-playground/ci-templates/README.adoc index 52b6930d..b2726d6a 100644 --- a/echidna-playground/ci-templates/README.adoc +++ b/echidna-playground/ci-templates/README.adoc @@ -1,7 +1,7 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 = Playground CI templates (not executed) -These nine workflow files were under `echidna-playground/.github/workflows/`. +These workflow files were under `echidna-playground/.github/workflows/`. GitHub reads workflows only from the repository-root `.github/workflows/`, so they never ran. They were moved here (ultraplan Phase 0.6, tracking issue #416) so that they cannot be mistaken for active CI. @@ -10,3 +10,7 @@ They are kept as templates. Before any of them is revived, check it against the root workflow of the same concern. Most of them duplicate one. Revive a file by moving it to the root and removing the duplicate. Do not leave a copy here that looks like CI. + +`mirror.yml` was removed (2026-10-14): the root `.github/workflows/mirror.yml` +covers mirroring through the standards reusable workflow, and the template's +Radicle job installed by piping a remote script to `sh`. diff --git a/echidna-playground/ci-templates/mirror.yml b/echidna-playground/ci-templates/mirror.yml deleted file mode 100644 index 03b8066c..00000000 --- a/echidna-playground/ci-templates/mirror.yml +++ /dev/null @@ -1,138 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 -# SPDX-FileCopyrightText: 2025 Jonathan D.A. Jewell -name: Mirror to Git Forges - -on: - push: - branches: [main] - workflow_dispatch: - -permissions: read-all - -jobs: - mirror-gitlab: - runs-on: ubuntu-latest - if: vars.GITLAB_MIRROR_ENABLED == 'true' - steps: - - uses: actions/checkout@b4ffde65f46336ab88eb53be808477a3936bae11 # v4 - with: - fetch-depth: 0 - - - uses: webfactory/ssh-agent@dc588b651fe13675774614f8e6a936a468676387 # v0.9.0 - with: - ssh-private-key: ${{ secrets.GITLAB_SSH_KEY }} - - - name: Mirror to GitLab - run: | - ssh-keyscan -t ed25519 gitlab.com >> ~/.ssh/known_hosts - git remote add gitlab git@gitlab.com:hyperpolymath/${{ github.event.repository.name }}.git || true - git push --force gitlab main - - mirror-bitbucket: - runs-on: ubuntu-latest - if: vars.BITBUCKET_MIRROR_ENABLED == 'true' - steps: - - uses: actions/checkout@b4ffde65f46336ab88eb53be808477a3936bae11 # v4 - with: - fetch-depth: 0 - - - uses: webfactory/ssh-agent@dc588b651fe13675774614f8e6a936a468676387 # v0.9.0 - with: - ssh-private-key: ${{ secrets.BITBUCKET_SSH_KEY }} - - - name: Mirror to Bitbucket - run: | - ssh-keyscan -t ed25519 bitbucket.org >> ~/.ssh/known_hosts - git remote add bitbucket git@bitbucket.org:hyperpolymath/${{ github.event.repository.name }}.git || true - git push --force bitbucket main - - mirror-codeberg: - runs-on: ubuntu-latest - if: vars.CODEBERG_MIRROR_ENABLED == 'true' - steps: - - uses: actions/checkout@b4ffde65f46336ab88eb53be808477a3936bae11 # v4 - with: - fetch-depth: 0 - - - uses: webfactory/ssh-agent@dc588b651fe13675774614f8e6a936a468676387 # v0.9.0 - with: - ssh-private-key: ${{ secrets.CODEBERG_SSH_KEY }} - - - name: Mirror to Codeberg - run: | - ssh-keyscan -t ed25519 codeberg.org >> ~/.ssh/known_hosts - git remote add codeberg git@codeberg.org:hyperpolymath/${{ github.event.repository.name }}.git || true - git push --force codeberg main - - mirror-sourcehut: - runs-on: ubuntu-latest - if: vars.SOURCEHUT_MIRROR_ENABLED == 'true' - steps: - - uses: actions/checkout@b4ffde65f46336ab88eb53be808477a3936bae11 # v4 - with: - fetch-depth: 0 - - - uses: webfactory/ssh-agent@dc588b651fe13675774614f8e6a936a468676387 # v0.9.0 - with: - ssh-private-key: ${{ secrets.SOURCEHUT_SSH_KEY }} - - - name: Mirror to SourceHut - run: | - ssh-keyscan -t ed25519 git.sr.ht >> ~/.ssh/known_hosts - git remote add sourcehut git@git.sr.ht:~hyperpolymath/${{ github.event.repository.name }} || true - git push --force sourcehut main - - mirror-disroot: - runs-on: ubuntu-latest - if: vars.DISROOT_MIRROR_ENABLED == 'true' - steps: - - uses: actions/checkout@b4ffde65f46336ab88eb53be808477a3936bae11 # v4 - with: - fetch-depth: 0 - - - uses: webfactory/ssh-agent@dc588b651fe13675774614f8e6a936a468676387 # v0.9.0 - with: - ssh-private-key: ${{ secrets.DISROOT_SSH_KEY }} - - - name: Mirror to Disroot - run: | - ssh-keyscan -t ed25519 git.disroot.org >> ~/.ssh/known_hosts - git remote add disroot git@git.disroot.org:hyperpolymath/${{ github.event.repository.name }}.git || true - git push --force disroot main - - mirror-gitea: - runs-on: ubuntu-latest - if: vars.GITEA_MIRROR_ENABLED == 'true' - steps: - - uses: actions/checkout@b4ffde65f46336ab88eb53be808477a3936bae11 # v4 - with: - fetch-depth: 0 - - - uses: webfactory/ssh-agent@dc588b651fe13675774614f8e6a936a468676387 # v0.9.0 - with: - ssh-private-key: ${{ secrets.GITEA_SSH_KEY }} - - - name: Mirror to Gitea - run: | - ssh-keyscan -t ed25519 ${{ vars.GITEA_HOST }} >> ~/.ssh/known_hosts - git remote add gitea git@${{ vars.GITEA_HOST }}:hyperpolymath/${{ github.event.repository.name }}.git || true - git push --force gitea main - - mirror-radicle: - runs-on: ubuntu-latest - if: vars.RADICLE_MIRROR_ENABLED == 'true' - steps: - - uses: actions/checkout@b4ffde65f46336ab88eb53be808477a3936bae11 # v4 - with: - fetch-depth: 0 - - - name: Install Radicle - run: | - curl -sSf https://radicle.xyz/install | sh - echo "$HOME/.radicle/bin" >> $GITHUB_PATH - - - name: Mirror to Radicle - run: | - echo "${{ secrets.RADICLE_KEY }}" > ~/.radicle/keys/radicle - chmod 600 ~/.radicle/keys/radicle - rad sync --announce || echo "Radicle sync attempted" diff --git a/issues/echidnabot-01-adaptive-ci-portfolio-scheduler.md b/issues/echidnabot-01-adaptive-ci-portfolio-scheduler.md index feaa2f49..9e0105c1 100644 --- a/issues/echidnabot-01-adaptive-ci-portfolio-scheduler.md +++ b/issues/echidnabot-01-adaptive-ci-portfolio-scheduler.md @@ -15,10 +15,10 @@ For each push or PR event, echidnabot enqueues one job per enabled prover, each ## 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]* `echidnabot/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]* `echidnabot/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]* `echidnabot/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.