feat: assay / assimilate / aggregate — proof-integration subcommands#121
Merged
Conversation
Three a-themed subcommands wiring panic-attack into the PROOF-PROGRAMME loop (survey -> swap -> fold-in-proofs): - assay (src/assay/mod.rs): survey a target for code with a formally proven drop-in equivalent in a proven / proven-servers library; operationalises the "Proven cross-fit" table in PROOF-PROGRAMME.md. Built-in catalogue: SafePath, SafeUrl. - assimilate (src/assay/mod.rs): perform a swap -- stage the proven module, back up the original (*.orig), and record provenance (source BLAKE3 hash + proof backing + pending call-site rewires) under .assimilated/. Call-site rewiring is reported, never auto-edited. - aggregate (src/aggregate/mod.rs): fold external prover output (Agda/Idris2/Coq/Lean/Isabelle/TSTP/Alethe/DRAT) into a report. Each artifact is BLAKE3-hashed for non-repudiation, classified (comment-stripped so prose markers do not false-trigger), and reconciled against findings (backed/corroborated/contradicted), with every verdict conditioned on the named checker's trust. Wired into lib.rs + main.rs (3 Commands variants + dispatch + helpers). 17 unit tests; full lib suite (395) green; zero new warnings. Idris2 0.8.0 installed; PA1/PA2/Stripping/Types proofs re-verified (typecheck). https://claude.ai/code/session_01K2TJLeQSyz4tpydZ18aRcb
main.rs hardcoded `#[command(version = "2.1.0")]`, four minor versions behind Cargo.toml (2.5.5). Switch to `#[command(version)]` so the version is read from CARGO_PKG_VERSION and cannot drift again. https://claude.ai/code/session_01K2TJLeQSyz4tpydZ18aRcb
![github-advanced-security[bot]](https://avatars.githubusercontent.com/in/57789?s=60&v=4){kind=small}
| @@ -0,0 +1,724 @@ | |||
| // SPDX-License-Identifier: MPL-2.0 | |||
🔍 Hypatia Security ScanFindings: 113 issues detected
View findings[
{
"reason": "Action uses: dtolnay/rust-toolchain@4be9e76fd7c4901c61fb841f5599 needs attention",
"type": "unpinned_action",
"file": "e2e.yml",
"action": "pin_sha",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Action es: Swatinem/rust-cache@779680da715d629ac1d338a641029a2f4372abb needs attention",
"type": "unpinned_action",
"file": "e2e.yml",
"action": "pin_sha",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Action perpolymath/standards/.github/workflows/governance-reusable.yml@main\n needs attention",
"type": "unpinned_action",
"file": "governance.yml",
"action": "pin_sha",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in boj-build.yml",
"type": "missing_timeout_minutes",
"file": "boj-build.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in cargo-audit.yml",
"type": "missing_timeout_minutes",
"file": "cargo-audit.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in casket-pages.yml",
"type": "missing_timeout_minutes",
"file": "casket-pages.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in casket-pages.yml",
"type": "missing_timeout_minutes",
"file": "casket-pages.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in chapel-ci.yml",
"type": "missing_timeout_minutes",
"file": "chapel-ci.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in chapel-ci.yml",
"type": "missing_timeout_minutes",
"file": "chapel-ci.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in chapel-ci.yml",
"type": "missing_timeout_minutes",
"file": "chapel-ci.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
}
]Powered by Hypatia Neurosymbolic CI/CD Intelligence |
hyperpolymath
added a commit
that referenced
this pull request
Jun 4, 2026
…adata (#122) Follow-up close-out batch after #121. Four coherent commits: ### `ef1e235` — CI hardening (Hypatia `missing_timeout_minutes`) Adds `timeout-minutes` to **27 `runs-on` jobs across 12 workflow files** that lacked one; reusable-workflow-call jobs are correctly exempt (GitHub rejects job-level `timeout-minutes` there). Purely additive (27 insertions, 0 deletions); all 19 workflow files still parse as YAML. (The remaining Hypatia "unpinned_action" flags are either false positives — `dtolnay`/`Swatinem` are already full-SHA-pinned — or the policy-governed `standards/...@main` reusable workflow.) ### `b4fb18e` — flagged unwrap + a real proof - `assay::assimilate`: replaced the Hypatia-flagged `source.unwrap()` (CWE-754, though guarded) with a `let Some(source) = source else { … }` that folds in the already-handled `None` branch. No behaviour change; zero unwrap. - `storage`: new proptest `hexad_json_roundtrip_is_identity` (PROOF-PROGRAMME §3.1, **faithful form**). The gateway octad projection is *lossy by design*, so the load-bearing integrity property is the on-disk serde round-trip used by `write_*_hexad → load_hexad_dir`; this proves it is the identity on the hexad JSON representation. ### `94aed04` — doc accuracy `20 → 38` subcommands and `47 → 49` languages across CLAUDE.md / EXPLAINME / README; `assay`/`assimilate`/`aggregate` added to the module tree and CLI examples. ### `37e73ea` — 6a2 metadata Completes `.machine_readable/6a2/` to the echidna/standards shape: new `AGENTIC` / `NEUROSYM` / `PLAYBOOK` / `ANCHOR` (`clade=diagnostic`), fleshed-out `META` / `ECOSYSTEM`; `STATE.a2ml` untouched. ## Tests Full library suite green; the new proptest and the refactored `assimilate` pass. Zero new warnings. ## Still open (not in this PR) - Attestation-chain unforgeability proof (Idris2) — the second proof "easy win". - Contractile-layout reconciliation (three overlapping representations + missing `INDEX.a2ml`) — pending location of the `CONTRACTILE-SPEC`. https://claude.ai/code/session_01K2TJLeQSyz4tpydZ18aRcb --- _Generated by [Claude Code](https://claude.ai/code/session_01K2TJLeQSyz4tpydZ18aRcb)_ --------- Co-authored-by: Claude <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What
Three new a-themed subcommands that wire panic-attack into the PROOF-PROGRAMME loop (survey → swap → fold-in-proofs), plus a small version-drift fix.
assay— proven-library substitution survey (src/assay/mod.rs)Surveys a target for code that has a formally proven drop-in equivalent in a
proven/proven-serverslibrary, reporting each candidate with the proof artifact that backs it. Operationalises the "Proven cross-fit" table inPROOF-PROGRAMME.mdmechanically. Built-in catalogue:SafePath,SafeUrl.On this repo it reports
safe-pathOffered (port present insrc/safe_path.rs, 5 call sites still to rewire) andsafe-urlNoReplacementSource (14VERISIMDB_URLhits, not yet ported).assimilate— perform the swap (src/assay/mod.rs)Stages the proven module into the tree, backs up the original (
*.orig), and records provenance — source BLAKE3 hash + proof backing + pending call-site rewires — under.assimilated/. Module swaps are automatic; call-site rewiring is reported, never auto-edited (mechanically editing arbitrary call sites is not a reviewable operation).aggregate— fold external prover output into a report (src/aggregate/mod.rs)Ingests prover artifacts (Agda / Idris2 / Coq·Rocq / Lean / Isabelle / TSTP / Alethe / DRAT·LRAT). Each artifact is BLAKE3-hashed for non-repudiation, given a friendly name, classified (
Closed/Holes/Refuted/Indeterminate— comment-stripped so prose mentioningpostulate/Admitteddoes not false-trigger), and reconciled against an existing report's findings (Backed / Corroborated / Contradicted).Every verdict is explicitly conditioned on the named checker's trust; the recorded hash lets the tool show exactly which bytes it was handed if the assessment is later challenged.
@name/@covers [claim:]kind:valueannotations travel inside the artifact; CLI--label/--coversoverride.Proof foundation
Idris2 0.8.0 installed and the existing foundation re-verified from first principles (all typecheck):
Types,Stripping(Layer 1.0),PatternCompleteness(PA1),ClassificationSoundness(PA2).Tests
17 new unit tests; full library suite (395) green; zero new compiler warnings.
Naming note
assay/assimilateare clean, no clashes.aggregatehas no CLI clash but conceptually overlapsadjudicate(aggregates panic-attack's own reports) andassemblyline("aggregate results"). A thematically tighter alternative for "bring an external proof forward as evidence" isadduce(orannex) — trivial rename if preferred.Still open (not in this PR)
README.adoc/EXPLAINME.adoc(CLAUDE.md count corrected).https://claude.ai/code/session_01K2TJLeQSyz4tpydZ18aRcb
Generated by Claude Code