Skip to content

fix(proofs): align Idris Lang enum with Rust (Chapel not C) — closes #41#46

Merged
hyperpolymath merged 2 commits into
mainfrom
fix/idris-lang-chapel-not-c
May 26, 2026
Merged

fix(proofs): align Idris Lang enum with Rust (Chapel not C) — closes #41#46
hyperpolymath merged 2 commits into
mainfrom
fix/idris-lang-chapel-not-c

Conversation

@hyperpolymath
Copy link
Copy Markdown
Owner

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)

  • cargo build --release clean
  • idris2 --check src/abi/PatternCompleteness.idr — totality OK
  • 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

  • cargo build --release
  • cargo clippy --all-targets --features signing,http -- -D warnings
  • idris2 --check (totality) ✅
  • Signed commit (GPG)

🤖 Generated with Claude Code

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>
@hyperpolymath hyperpolymath enabled auto-merge (squash) May 26, 2026 09:34
@github-actions
Copy link
Copy Markdown

🔍 Hypatia Security Scan

Findings: 48 issues detected

Severity Count
🔴 Critical 4
🟠 High 16
🟡 Medium 28

⚠️ Action Required: Critical security issues found!

View findings
[
  {
    "reason": "Action hyperpolymath/standards/.github/workflows/governance-reusable.yml@main needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Nickel file missing SPDX-License-Identifier header (1 occurrences, CWE-1104)",
    "type": "ncl_missing_spdx",
    "file": "/home/runner/work/panic-attack/panic-attack/reports/panic-attack-20260211180017.ncl",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "expect() in hot path (2 occurrences, CWE-754)",
    "type": "expect_in_hot_path",
    "file": "/home/runner/work/panic-attack/panic-attack/src/attestation/chain.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "unwrap_or(0) with dangerous default (1 occurrences, CWE-754)",
    "type": "unwrap_dangerous_default",
    "file": "/home/runner/work/panic-attack/panic-attack/src/attestation/evidence.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "unwrap_or(0) with dangerous default (1 occurrences, CWE-754)",
    "type": "unwrap_dangerous_default",
    "file": "/home/runner/work/panic-attack/panic-attack/src/ambush/mod.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "unwrap_or(0) with dangerous default (3 occurrences, CWE-754)",
    "type": "unwrap_dangerous_default",
    "file": "/home/runner/work/panic-attack/panic-attack/src/kanren/strategy.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "unwrap_or(0) with dangerous default (3 occurrences, CWE-754)",
    "type": "unwrap_dangerous_default",
    "file": "/home/runner/work/panic-attack/panic-attack/src/axial/mod.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "expect() in hot path (4 occurrences, CWE-754)",
    "type": "expect_in_hot_path",
    "file": "/home/runner/work/panic-attack/panic-attack/src/assail/analyzer.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "unwrap() without prior check -- DoS via panic (4 occurrences, CWE-754)",
    "type": "unwrap_without_check",
    "file": "/home/runner/work/panic-attack/panic-attack/benches/scan_bench.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  },
  {
    "reason": "expect() in hot path (2 occurrences, CWE-754)",
    "type": "expect_in_hot_path",
    "file": "/home/runner/work/panic-attack/panic-attack/benches/scan_bench.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

@github-actions
Copy link
Copy Markdown

🔍 Hypatia Security Scan

Findings: 49 issues detected

Severity Count
🔴 Critical 4
🟠 High 16
🟡 Medium 29

⚠️ Action Required: Critical security issues found!

View findings
[
  {
    "reason": "Action hyperpolymath/standards/.github/workflows/governance-reusable.yml@main needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Nickel file missing SPDX-License-Identifier header (1 occurrences, CWE-1104)",
    "type": "ncl_missing_spdx",
    "file": "/home/runner/work/panic-attack/panic-attack/reports/panic-attack-20260211180017.ncl",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "expect() in hot path (2 occurrences, CWE-754)",
    "type": "expect_in_hot_path",
    "file": "/home/runner/work/panic-attack/panic-attack/src/attestation/chain.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "unwrap_or(0) with dangerous default (1 occurrences, CWE-754)",
    "type": "unwrap_dangerous_default",
    "file": "/home/runner/work/panic-attack/panic-attack/src/attestation/evidence.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "unwrap_or(0) with dangerous default (1 occurrences, CWE-754)",
    "type": "unwrap_dangerous_default",
    "file": "/home/runner/work/panic-attack/panic-attack/src/ambush/mod.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "unwrap_or(0) with dangerous default (3 occurrences, CWE-754)",
    "type": "unwrap_dangerous_default",
    "file": "/home/runner/work/panic-attack/panic-attack/src/kanren/strategy.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "unwrap_or(0) with dangerous default (3 occurrences, CWE-754)",
    "type": "unwrap_dangerous_default",
    "file": "/home/runner/work/panic-attack/panic-attack/src/axial/mod.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "expect() in hot path (4 occurrences, CWE-754)",
    "type": "expect_in_hot_path",
    "file": "/home/runner/work/panic-attack/panic-attack/src/assail/analyzer.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "unwrap() without prior check -- DoS via panic (4 occurrences, CWE-754)",
    "type": "unwrap_without_check",
    "file": "/home/runner/work/panic-attack/panic-attack/benches/scan_bench.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  },
  {
    "reason": "expect() in hot path (2 occurrences, CWE-754)",
    "type": "expect_in_hot_path",
    "file": "/home/runner/work/panic-attack/panic-attack/benches/scan_bench.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

@hyperpolymath hyperpolymath merged commit 7766c18 into main May 26, 2026
26 checks passed
@hyperpolymath hyperpolymath deleted the fix/idris-lang-chapel-not-c branch May 26, 2026 09:59
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Proof-drift: src/types.rs Language enum disagrees with src/abi/PatternCompleteness.idr (Chapel vs C)

1 participant