Repository navigation
feat(assail): route languages through a tested table; retire the vacuous PA1 - #288
Merged
Merged
Conversation
Checked with Idris2 0.7.0 (the version proven-tests.yml pins). On main, two of the five src/abi modules did not compile: - Stripping.idr: a dangling `|||` doc block at the end of the file was a parse error. Behind it, `stripLineCommentsIdempotent` had two real type errors: a `case c of '/' => Refl` branch the comment called impossible was not refuted, and `decEq` was used without importing it. Matching on a Char literal only reduces when the character is a literal, so the proof stuck on a variable head. The model now classifies each character once (`cls`: Slash, Newline, Other) and steps on the class; each proof carries the class with the equation `cls c = k`, so every case reduces. The theorem statements and all seven sanity checks are unchanged and pass. The new model computes the same function as the old pattern-matching one: checked exhaustively on all 349,525 strings of length <= 9 over `/`, newline, `x` and space, with no mismatch. - Types.idr: a named field in a one-line data declaration, and an Ord instance with no Eq instance. Both fixed without changing meaning. Its header claimed three proofs the file does not contain; it now says it declares types only, and notes its drift from src/types.rs. Negative controls: a planted false lemma and a planted non-terminating definition are both rejected, so the check can fail. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Jma5ixtpeZyJRmfoSsC98u
PROOF-NEEDS.adoc now uses the proof policy's §5 status tokens and §1.2 verifier mapping, pinned to standards 9bdf864, in place of check marks. Each status rests on a recorded receipt: Idris2 0.7.0 run over src/abi at 3dc4728, with the invocation, pass criterion and negative controls. What the re-check found, and how it is now recorded: - Stripping: did not compile on main; repaired in 3dc4728. PROVEN for the model; model-to-Rust correspondence ASSUMED. - Attestation: PROVEN relative to its hypotheses. Two of them, an injective chain hash and perfect unforgeability, are symbolic-model idealisations stronger than collision resistance and EUF-CMA, so no computational result is claimed. - PA1 (pattern completeness): compiles but is vacuous, because a generic analyzer witness inhabits every language. rustc's exhaustiveness check on the `_ => analyze_generic` match already gives the guarantee. The model is also stale (50 of 52 languages; cross-language checks are now skipped for configuration files). - Implementation obligations on Rust behaviour (stripping, Patch Bridge reachability, taint analysis) are OPEN for Creusot/Pearlite and Verus. The missing CI gate for src/abi is OPEN. - The Kani note is backed by compiling every non-example target with unsafe_code forbidden. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Jma5ixtpeZyJRmfoSsC98u
The Idris2 modules are named PanicAttack.ABI.<M> but lived in src/abi/, so `idris2 --check src/abi/<M>.idr` failed on a module-name mismatch from any directory. No CI job checked them, which is how Stripping.idr sat on main not compiling while PROOF-NEEDS called it closed. - Move src/abi/*.idr to src/abi/PanicAttack/ABI/ (pure renames) and add src/abi/panic-attack-abi.ipkg listing the five modules. - Add the `abi-proofs` job to proven-tests.yml: every PR and push to main runs `idris2 --typecheck src/abi/panic-attack-abi.ipkg` and fails on a non-zero exit or any `Error:` line. It reuses the framework job's pinned installer and Idris2 cache key, and only the actions that workflow already locks, so actions.lock is unchanged. - PROOF-NEEDS.adoc: the gate is now the receipt; the first local receipt is kept; the gate row leaves the open list. EXPLAINME and PROOF-PROGRAMME point at the new paths. CHANGELOG history and the retired .a2ml files are left as they are. Checked locally: the package type-checks (Idris2 0.7.0); a planted false lemma and a planted missing import both fail it; the job's run step passes as written; actionlint 1.7.7 is clean; validate-sha-pins and check-allowed-actions pass with the checksum-pinned yq v4.54.1. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Jma5ixtpeZyJRmfoSsC98u
…ous PA1
PA1 was an Idris2 model of the analyzer dispatch whose theorem could not
fail: `GenericAnalyzer : HasAnalyzer lang` inhabited its witness for every
language. It was also stale (50 of 52 languages) and partly false (it said
cross-language checks always run; they are skipped for configuration).
The routing is now real code with claims that can fail:
- src/assail/routing.rs: `route(Language) -> Route`,
`Route::analyzer()`, and `runs_cross_language(is_configuration)`.
`analyze_inner` matches on `route(file_lang)` and calls
`runs_cross_language`. Only the arm heads changed; every arm body is
byte-identical. `route` and the dispatch are exhaustive with no
wildcard (Chapel, the one language without a dedicated analyzer, is
routed to Generic explicitly).
- src/types.rs: `Language::ALL` (52 variants), kept complete by an
exhaustive `ordinal` match test, following WeakPointCategory::ALL.
- Tests, exhaustive over Language::ALL:
(a) every language analyzer in analyzer.rs is reached;
(b) no language falls back to analyze_generic while a dedicated
analyzer for it exists;
(c) cross-language checks run exactly off configuration, and on
scripts embedded in it (Justfile + Lua scan, end to end);
(d) README's language counts equal the supported count.
Each was seen to fail on a planted fault.
- README: 49 -> 51 languages (badge, capabilities, summary); (d) caught
the drift. C and Php were added after the count was written.
- PatternCompleteness.idr removed from src/abi and the ipkg; PROOF-NEEDS,
EXPLAINME, PROOF-PROGRAMME and the 0-AI-MANIFEST entry updated. PA1's
status is TESTED; the Creusot/Pearlite and Verus proof is OPEN.
Found while testing (c), recorded as an open obligation, not fixed here:
the cross-language check strips `//` comments before matching, which
also cuts unquoted `http://` URLs (shell, Justfile recipes).
Checked: cargo fmt; clippy -D warnings with all and default features;
cargo test --all-features (789 passed, 0 failed); the Idris2 package
type-checks (4 modules); panic-attack's self-scan reports nothing new.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Jma5ixtpeZyJRmfoSsC98u
Addresses the CodeRabbit review of this PR. Each Rust claim was run against strip_proof_comments copied verbatim from main: - `//x`: the model gives three spaces, Rust gives "". The model-to-Rust row now records a mismatch instead of ASSUMED, and the Stripping.idr header and section comment say the model does not reproduce the Rust output. The 349,525-input check is labelled model against model. - `a//*x*/*b*/c` -> `a/*b*/c` -> `ac`: Rust is not idempotent. - `a/*x*/b` -> `ab`: Rust does not preserve positions. - Found while checking: blocks are stripped before line comments, so a block opener inside a line comment hides the code after it. The Lean, Agda/Haskell and Coq ProofDrift detectors use this function. The open obligation now says the implementation must change first. - sigOnlySigner states that a matching key exists, not who signed; authenticity inherits that. - The dispatch row notes that Unknown files with no adapter are marked unsupported and skipped before the match. - The hexad property test's bounds are recorded from its generators. - Stripping.idr: PROOF-NEEDS.md -> PROOF-NEEDS.adoc. Stripping.idr still type-checks under Idris2 0.7.0. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Jma5ixtpeZyJRmfoSsC98u
# Conflicts: # PROOF-NEEDS.adoc
…ceipt From CodeRabbit's second review, checked against analyzer.rs: - The block-before-line ordering bug reaches every caller that passes both markers: analyze_rust, is_rust_ffi_safe_wrapper, analyze_idris, analyze_lean and analyze_agda. analyze_haskell does not call the function, and analyze_isabelle and analyze_coq pass no line marker. (The review listed Idris, Lean and Agda; the two Rust callers are affected too.) - The receipt now records that Stripping.idr was rechecked after the comment-only edits in ab0fdb2. All five modules pass again under Idris2 0.7.0, and the diff from 3dc4728 touches only comment lines. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Jma5ixtpeZyJRmfoSsC98u
# Conflicts: # PROOF-NEEDS.adoc
Main took #281, which re-proved Stripping.idr and gated src/abi/ in CI (idris-abi), and #275, which added a model-checked TLA+ entry. - src/abi/Stripping.idr: main's re-proof. It states every theorem this branch's repair did, plus idempotence (stripLineCommentsIdempotent), stripIsIdOnClean, stripKeepsHead and two more sanity cases. - src/abi/Types.idr: this branch's version (its header no longer claims theorems the module does not contain), plus main's doc line on Eq. - PROOF-NEEDS.adoc: this branch's structure, with main's receipts paragraph, main's Stripping row text (it describes the file kept), main's TLA+ section and its Generation-publish obligation. The receipt section now names the idris-abi gate, which passed on main at 36f1055, and the open 'Gate the Idris2 modules in CI' row is removed because #281 did it. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0136P7ZnmBahbhfkFEP6ark4
The merge placed '||| Equality on severity' between 'public export' and 'Eq Severity where'. Idris2 then rejects 'public export' as a declaration start (idris-abi on b332b5f). Doc comment first, as on main. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0136P7ZnmBahbhfkFEP6ark4
Rebuild #282 on the flat src/abi/ layout that main keeps after #281. Move the ABI modules back to src/abi/, drop the ipkg, and retire PatternCompleteness.idr at its flat path. Point PROOF-PROGRAMME, PROOF-NEEDS and EXPLAINME at src/assail/routing.rs for PA1. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0136P7ZnmBahbhfkFEP6ark4
Resolve PROOF-NEEDS.adoc in favour of this branch: main still carries the PA1 rows from #277 (the vacuous PatternCompleteness model and the "replace or retire PA1" open row), which this branch replaces with the tested routing-table rows. cargo test --lib: 482 passed. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0136P7ZnmBahbhfkFEP6ark4
Contributor
|
Caution Review failedThe pull request is closed. Summary
Merge Risk:
 |
|
Codex Review Summary: ❌ FailedThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
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
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.
This replaces #282, which GitHub would not retarget from the closed #279's branch ("part of a stack"). The branch and its changes are the same, now merged with current main.
What
The Idris2
PatternCompleteness.idr(PA1) is replaced by the code that actually does the routing, plus exhaustive tests.src/assail/routing.rs:route(Language) -> Routeis an exhaustive match with no wildcard.Route::analyzer()names the analyzer each route reaches.runs_cross_language(is_configuration)returns!is_configuration.analyzer.rs: the dispatch inanalyze_innernow matches onroute(file_lang). So the table is the code that runs, not a model of it. Only the match arm heads changed, plus the cross-language guard.src/types.rs: addsLanguage::ALL(52 variants). An exhaustiveordinaltest keeps it complete.Claims and how they are tested (status
TESTED)Each test was seen to fail on a planted fault.
every_language_analyzer_is_reachedanalyze_chapelno_language_falls_back_while_a_dedicated_analyzer_existsGenericcross_language_checks_run_exactly_off_configuration(a Justfile plusmain.lua, end to end)runs_cross_languageforced totruereadme_language_counts_match_the_tableRouting is not coverage.
Language::Unknowngoes toInputAdapter, and a file there with no adapter is marked unsupported and skipped.PROOF-NEEDS.adocsays so.Retired
src/abi/PatternCompleteness.idr, for three reasons:GenericAnalyzerinhabited its witness for every language.PROOF-PROGRAMME,PROOF-NEEDSandEXPLAINMEnow point PA1 atsrc/assail/routing.rs.0-AI-MANIFEST.a2mlis deleted (a deletion only).Found, not fixed here (recorded as open obligations in PROOF-NEEDS)
http://URLs are missed by the cross-language check.analyze_cross_languagestrips//comments from every file, which also cutscurl http://hostin shell and Justfile recipes.Not changed
.machine_readable/6a2/{META,NEUROSYM,STATE}.a2mlstill namePatternCompleteness.idr. They are legacy A2ML files, so they are left for the owner or the deed conversion.Verification
cargo test --lib: 482 passed, 0 failed, after merging current main.cargo fmt --checkpasses.Generated by Claude Code