fix(abi): remove duplicate allTake in Boj.SafetyLemmas (core proofs green)

[hyperpolymath]

Fixes the pre-existing Idris2 failure surfaced on #234/#236 (not caused by either — they just triggered the path-gated Idris2 job by touching a .idr).

Root cause

allTake was defined twice in src/abi/Boj/SafetyLemmas.idr:

• lines ~122–130 — {p} -> {n} -> {xs} -> allRec p xs = True -> allRec p (take n xs) = True
• lines ~213–221 — same lemma, implicit args in a different order ({p} -> {xs} -> {n})

→ Error: Boj.SafetyLemmas.allTake is already defined → the core ABI package boj.ipkg failed type-check (PASS=104 FAIL=1). It was masked normally because the Idris2 job is path-gated and skips unless a .idr changes.

Fix

Kept the first definition — a complete, total proof (no postulate, no believe_me) — and removed the redundant second copy. No proof is weakened or stubbed.

Both callers use inferred implicits, so the removed copy's argument order didn't matter to them:

• Boj/SafePromptInjection.idr:168 — MkDelimiterCharsafe (take n cs) {prf = allTake prf}
• Boj/SafeHTTP.idr:139 — MkHeaderCharsafe (take n cs) {prf = allTake prf}

Verification

Expected: scripts/typecheck-proofs.sh → PASS=105 FAIL=0. Idris2 isn't available in the authoring environment, so the Idris2 type-check CI job is the proof verification here — it should go from failing to green on this PR (and this is the first PR that should pass it cleanly when the job runs).

🤖 Generated with Claude Code

---

Generated by Claude Code

[github-actions]

🏁 path-claims bench

Commit de9267e

Numbers

path-claims bench  (node v22.22.3)

  scenario                                              iters       ms        ns/op          ops/s
  --------------------------------------------------------------------------------------------------------------
  register: 10 active claims, 3 new paths               50000 iters    189 ms      3.79 µs/op    263.7k ops/s
  register: 100 active claims, 3 new paths              20000 iters    329 ms     16.50 µs/op     60.6k ops/s
  register: 1000 active claims, 3 new paths              5000 iters    930 ms    186.01 µs/op      5.4k ops/s
  register: 100 active claims, 20 new paths              5000 iters    360 ms     72.17 µs/op     13.9k ops/s

  pathsOverlap: deep diverge at segment 4             1000000 iters    163 ms     163.1 ns/op     6.13M ops/s
  pathsOverlap: short prefix match                    1000000 iters    134 ms     134.1 ns/op     7.45M ops/s

  refresh (existing claim)                             100000 iters     11 ms     110.9 ns/op     9.02M ops/s
  list (100 active claims)                              50000 iters    278 ms      5.57 µs/op    179.6k 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: 214 issues detected

Severity	Count
🔴 Critical	15
🟠 High	130
🟡 Medium	69

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "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"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/boj-server/boj-server/cartridges/hesiod-mcp/adapter/mod.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence