Skip to content

Commit 7766c18

Browse files
fix(proofs): align Idris Lang enum with Rust (Chapel not C) — closes #41 (#46)
## Summary Closes #41 — the Rust `Language` enum and the Idris `Lang` enum both claimed "49 variants + Unknown" but disagreed on which 49: | Variant | Rust `src/types.rs` | Idris `src/abi/PatternCompleteness.idr` | |---|---|---| | `Chapel` | ✅ | ❌ (now ✅) | | `C` | ❌ | ✅ (now ❌) | Result: the totality theorem `completeScanForAll` was technically vacuous for `C` (no Rust dispatch existed to verify) and silently missing coverage for `Chapel`. ## Fix — Option 1 from the issue Drop `C` from Idris, add `Chapel`. Rationale: `Cpp` already represents the unified C/C++ 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 — the original Idris enum had a phantom constructor. ## Changes | Location | Change | |---|---| | `Lang` data declaration | Remove `C`, add `Chapel` (in new `-- HPC / parallel` group, mirroring its position in `types.rs`) | | Header comment | Note that `Cpp` is the C/C++ unified analyzer | | `analyzerFor` | Drop `analyzerFor C = SpecificAnalyzer`; add `analyzerFor Chapel = SpecificAnalyzer` | | `detectorsFor` | 8 lists updated: `[C, Cpp]` → `[Cpp]` (UncheckedAllocation, UnboundedLoop, UnsafeCode, RaceCondition, DeadlockPotential, ResourceLeak, InsecureProtocol, HardcodedSecret, UncheckedError) | Net diff: -11 / +16 lines, single file. ## Acceptance criteria (from #41) - [x] `cargo build --release` clean - [x] `idris2 --check src/abi/PatternCompleteness.idr` — totality OK - [x] Bijection between the two enumerations: ``` $ comm -23 /tmp/rust-langs /tmp/idris-langs # in Rust, not Idris (empty) $ comm -13 /tmp/rust-langs /tmp/idris-langs # in Idris, not Rust (empty) 50 = 50 — match (49 named + Unknown on both sides) ``` ## Why this is the right fix - The Rust enum is the operational source of truth (it's what `analyze_inner()` actually dispatches against). - The Idris file is the **mirror** that has to follow. - `Cpp` analyzer subsumes `.c` files via the unified `analyze_c_cpp` path, so there is no behavioural regression. - `Chapel` analyzer is now provably covered by `completeScanForAll`. ## Verification - [x] `cargo build --release` ✅ - [x] `cargo clippy --all-targets --features signing,http -- -D warnings` ✅ - [x] `idris2 --check` (totality) ✅ - [x] Signed commit (GPG) 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent edf8d6e commit 7766c18

1 file changed

Lines changed: 16 additions & 11 deletions

File tree

src/abi/PatternCompleteness.idr

Lines changed: 16 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -23,9 +23,12 @@ module PanicAttack.ABI.PatternCompleteness
2323

2424
||| All 49 programming languages supported by the scanner.
2525
||| This MUST stay in sync with src/types.rs Language enum.
26+
||| Note: Cpp is the C/C++ unified analyzer (analyze_c_cpp dispatches
27+
||| on .c / .cpp / .h / .hpp / .cc / .hh — there is no separate C
28+
||| constructor in the Rust enum).
2629
public export
2730
data Lang
28-
= Rust | C | Cpp | Go | Java | Python | JavaScript | Ruby
31+
= Rust | Cpp | Go | Java | Python | JavaScript | Ruby
2932
-- BEAM family
3033
| Elixir | Erlang | Gleam
3134
-- ML family
@@ -44,6 +47,8 @@ data Lang
4447
| Nickel | Nix
4548
-- Scripting / data
4649
| Shell | Julia | Lua
50+
-- HPC / parallel
51+
| Chapel
4752
-- Nextgen custom DSLs
4853
| WokeLang | Eclexia | MyLang | JuliaTheViper | Oblibeny
4954
| Anvomidav | AffineScript | Ephapax | BetLang | ErrorLang
@@ -70,7 +75,6 @@ data HasAnalyzer : Lang -> Type where
7075
public export
7176
analyzerFor : (lang : Lang) -> HasAnalyzer lang
7277
analyzerFor Rust = SpecificAnalyzer
73-
analyzerFor C = SpecificAnalyzer
7478
analyzerFor Cpp = SpecificAnalyzer
7579
analyzerFor Go = SpecificAnalyzer
7680
analyzerFor Java = SpecificAnalyzer
@@ -106,6 +110,7 @@ analyzerFor Nix = SpecificAnalyzer
106110
analyzerFor Shell = SpecificAnalyzer
107111
analyzerFor Julia = SpecificAnalyzer
108112
analyzerFor Lua = SpecificAnalyzer
113+
analyzerFor Chapel = SpecificAnalyzer
109114
analyzerFor WokeLang = SpecificAnalyzer
110115
analyzerFor Eclexia = SpecificAnalyzer
111116
analyzerFor MyLang = SpecificAnalyzer
@@ -206,24 +211,24 @@ data HasDetector : WPCategory -> Type where
206211
||| matching code in analyzer.rs.
207212
public export
208213
detectorsFor : (cat : WPCategory) -> HasDetector cat
209-
detectorsFor UncheckedAllocation = DetectedBy [C, Cpp]
210-
detectorsFor UnboundedLoop = DetectedBy [Rust, C, Cpp, Go, Python, JavaScript]
214+
detectorsFor UncheckedAllocation = DetectedBy [Cpp]
215+
detectorsFor UnboundedLoop = DetectedBy [Rust, Cpp, Go, Python, JavaScript]
211216
detectorsFor BlockingIO = DetectedBy [Rust, Go, Python, JavaScript]
212-
detectorsFor UnsafeCode = DetectedBy [Rust, C, Cpp, Zig, Nim, DLang]
217+
detectorsFor UnsafeCode = DetectedBy [Rust, Cpp, Zig, Nim, DLang]
213218
detectorsFor PanicPath = DetectedBy [Rust, Go, Haskell]
214-
detectorsFor RaceCondition = DetectedBy [Rust, C, Cpp, Go]
215-
detectorsFor DeadlockPotential = DetectedBy [Rust, C, Cpp, Go]
216-
detectorsFor ResourceLeak = DetectedBy [Rust, C, Cpp]
219+
detectorsFor RaceCondition = DetectedBy [Rust, Cpp, Go]
220+
detectorsFor DeadlockPotential = DetectedBy [Rust, Cpp, Go]
221+
detectorsFor ResourceLeak = DetectedBy [Rust, Cpp]
217222
detectorsFor CommandInjection = DetectedBy [Python, Ruby, JavaScript, Shell, Elixir, Erlang]
218223
detectorsFor UnsafeDeserialization = DetectedBy [Python, Ruby, JavaScript, Java]
219224
detectorsFor DynamicCodeExecution = DetectedBy [Python, JavaScript, Ruby, Elixir, Shell]
220225
detectorsFor UnsafeFFI = DetectedBy [Elixir, Erlang, Haskell, Pony, OCaml, Zig]
221226
detectorsFor AtomExhaustion = DetectedBy [Elixir, Erlang]
222-
detectorsFor InsecureProtocol = DetectedBy [Rust, C, Cpp, Go, Python, JavaScript, Ruby]
227+
detectorsFor InsecureProtocol = DetectedBy [Rust, Cpp, Go, Python, JavaScript, Ruby]
223228
detectorsFor ExcessivePermissions = DetectedBy [Shell]
224229
detectorsFor PathTraversal = DetectedBy [Python, JavaScript, Ruby, Go, Java]
225-
detectorsFor HardcodedSecret = DetectedBy [Rust, C, Cpp, Go, Python, JavaScript, Ruby]
226-
detectorsFor UncheckedError = DetectedBy [Go, Rust, C, Cpp]
230+
detectorsFor HardcodedSecret = DetectedBy [Rust, Cpp, Go, Python, JavaScript, Ruby]
231+
detectorsFor UncheckedError = DetectedBy [Go, Rust, Cpp]
227232
detectorsFor InfiniteRecursion = DetectedBy [Haskell, PureScript, Scheme, Racket]
228233
detectorsFor UnsafeTypeCoercion = DetectedBy [OCaml, Haskell, DLang, Nim]
229234
detectorsFor ProofDrift = DetectedBy [Idris, Lean, Agda, Isabelle, Coq, Julia]

0 commit comments

Comments
 (0)