fix(proofs): add allTake/fromLteTrue lemmas + extend path_claims tests

[hyperpolymath]

Summary

• SafetyLemmas.idr: two new exported lemmas needed for SafeHTTP/SafeCORS proof chains:
  • allTake: if allRec p xs = True then allRec p (take n xs) = True
  • fromLteTrue: converts a Bool lte witness (a <= b) = True to LTE a b
  • falseImpliesNotTrue: refactored from case-split to rewrite prf in Refl so it works for any Bool b, not just the False constructor
• mcp-bridge/tests/path_claims_test.js: additional claim coverage

These were in the working tree during the foundry/truthfulness-gate rebase (PR #220) and stashed for a clean PR.

Test plan

• idris2 --typecheck src/abi/boj.ipkg passes
• node mcp-bridge/tests/path_claims_test.js passes

🤖 Generated with Claude Code

[github-actions]

🏁 path-claims bench

Commit 2d230b7

Numbers

path-claims bench  (node v22.22.3)

  scenario                                              iters       ms        ns/op          ops/s
  --------------------------------------------------------------------------------------------------------------
  register: 10 active claims, 3 new paths               50000 iters    183 ms      3.67 µs/op    272.5k ops/s
  register: 100 active claims, 3 new paths              20000 iters    334 ms     16.70 µs/op     59.9k ops/s
  register: 1000 active claims, 3 new paths              5000 iters   1119 ms    223.97 µs/op      4.5k ops/s
  register: 100 active claims, 20 new paths              5000 iters    359 ms     71.90 µs/op     13.9k ops/s

  pathsOverlap: deep diverge at segment 4             1000000 iters    163 ms     163.7 ns/op     6.11M ops/s
  pathsOverlap: short prefix match                    1000000 iters    134 ms     134.5 ns/op     7.43M ops/s

  refresh (existing claim)                             100000 iters     10 ms     106.5 ns/op     9.39M ops/s
  list (100 active claims)                              50000 iters    286 ms      5.73 µs/op    174.5k ops/s

  (Bench numbers depend on host; use deltas across commits, not absolute values.)

Host-dependent — compare deltas across commits, not absolute values.

[github-actions]

🔍 Hypatia Security Scan

Findings: 249 issues detected

Severity	Count
🔴 Critical	15
🟠 High	163
🟡 Medium	71

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Stale AI session file -- delete",
    "type": "stale",
    "file": "GEMINI.md",
    "action": "delete",
    "rule_module": "root_hygiene",
    "severity": "medium"
  },
  {
    "reason": "Issue in scorecard-enforcer.yml",
    "type": "missing_timeout_minutes",
    "file": "scorecard-enforcer.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in scorecard-enforcer.yml",
    "type": "scorecard_publish_with_run_step",
    "file": "scorecard-enforcer.yml",
    "action": "split_scorecard_publish_job",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in instant-sync.yml",
    "type": "secret_action_without_presence_gate",
    "file": "instant-sync.yml",
    "action": "peter-evans/repository-dispatch",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in codeql.yml",
    "type": "codeql_missing_actions_language",
    "file": "codeql.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/boj-server/boj-server/cartridges/academic-workflow-mcp/adapter/mod.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/boj-server/boj-server/cartridges/ephapax-mcp/adapter/mod.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/boj-server/boj-server/cartridges/bofig-mcp/adapter/mod.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/boj-server/boj-server/cartridges/fireflag-mcp/adapter/mod.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/boj-server/boj-server/cartridges/sanctify-mcp/adapter/mod.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence