Repository navigation
feat(assail): route languages through a tested table; retire the vacuous PA1 - #282
Open
hyperpolymath wants to merge 3 commits into
Open
hyperpolymath wants to merge 3 commits into
hyperpolymath wants to merge 3 commits into
Conversation
…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
# Conflicts: # PROOF-NEEDS.adoc
Contributor
|
Warning Review limit reachedYou've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository. Next included review available in 16 minutes. View limit details
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. |
|
hyperpolymath
marked this pull request as ready for review
November 9, 2026 15:49
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 branch has not been deployed
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.
Stacked on #279 (Idris2 gate), which is stacked on #277 (proof-status reconcile). Review and merge in that order.
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, and so did 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
PatternCompleteness.idr, for three reasons:GenericAnalyzerinhabited its witness for every language.0-AI-MANIFEST.a2mlis deleted. This is a deletion only.Found, not fixed here (recorded in PROOF-NEEDS open obligations)
http://URLs are missed by the cross-language check.analyze_cross_languagestrips//comments from every file. That also cutscurl http://hostin shell and Justfile recipes. The fix is a follow-up stacked PR.Verification
cargo fmt --check.cargo clippy -D warnings, with all features and with default features.cargo test: 789 passed.idris2 --typecheck src/abi/panic-attack-abi.ipkg(Idris2 0.7.0): exit 0, noError:line.cargo test --lib routingre-run after merging ci(abi): gate the Idris2 proofs on every PR, with module-shaped paths #279's head: 4 passed.Generated by Claude Code