You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
fix(proofs): align Idris Lang enum with Rust Language (Chapel not C)
Closes#41.
Both enumerations claim "49 variants + Unknown" but disagreed on which
49: Rust has `Chapel` (no `C`), Idris had `C` (no `Chapel`). The
completeness theorem was therefore technically vacuous for `C` (no
Rust dispatch to verify) and silently missing coverage for `Chapel`.
Option 1 from the issue (preferred): drop `C` from Idris, add `Chapel`.
Cpp already represents the C/C++ unified analyzer (analyze_c_cpp
dispatches on .c/.cpp/.h/.hpp/.cc/.hh), so there was never a separate
`C` constructor in the Rust source of truth.
Changes:
- `Lang`: remove `C`, add `Chapel` (under new "HPC / parallel" group)
- `analyzerFor`: drop `C` arm, add `Chapel` arm
- `detectorsFor`: replace `C, Cpp` with `Cpp` in all 8 affected lists
(UncheckedAllocation, UnboundedLoop, UnsafeCode, RaceCondition,
DeadlockPotential, ResourceLeak, InsecureProtocol, HardcodedSecret,
UncheckedError)
- Updated header comment to clarify Cpp = analyze_c_cpp
Verification:
- `idris2 --check src/abi/PatternCompleteness.idr` — totality OK
- Bijection check: 50 = 49 named + Unknown on both sides, zero diff
- `cargo build --release` clean
- `cargo clippy --all-targets --features signing,http -D warnings` clean
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
0 commit comments