docs(proof-debt): add canonical AXIOM: annotations to SafetyLemmas.idr

[hyperpolymath]

Summary

Follow-up to #161 (which seeded docs/proof-debt.md per the estate
Trusted-Base Reduction Policy
— hyperpolymath/standards#203, enforcement hyperpolymath/standards#211).

docs/proof-debt.md already enumerates the 5 class-(J) believe_me
sites in src/abi/Boj/SafetyLemmas.idr, so the check-trusted-base.sh
gate passes via the "documented in proof-debt.md" path. This PR closes
the second path: each marker now also has an inline AXIOM: leading
comment, the canonical keyword the script greps. The result: boj-server
satisfies both halves of the check, making it the fully canonical
reference implementation cited in standards#203 §"Precedent".

Changes

• src/abi/Boj/SafetyLemmas.idr (38 lines, 5 sites + 1 module header):
  • charEqSound, charEqSym, unpackLength, appendLengthSum,
    substrLengthBound each gain an AXIOM: <name>; class-(J) — ...
    header line citing docs/proof-debt.md §(c) and the per-primitive
    docs/backend-assurance/<primitive>.md.
  • Module-header summary updated from "Five axiomatic believe_me" to
    use the policy vocabulary ("AXIOM-tagged", "disposition-§(c)
    NECESSARY-AXIOM").
• PROOF-NEEDS.md: new header note cross-linking docs/proof-debt.md
  (strategic-goals doc ↔ schema-conformant per-repo index) — mirrors
  the pattern from standards#213.

Marker inventory (unchanged)

5 escape hatches, all believe_me, all in src/abi/Boj/SafetyLemmas.idr,
all class-(J) NECESSARY AXIOM (§(c)), all externally validated under
docs/backend-assurance/:

Site	Function	Disposition
SafetyLemmas.idr:61	charEqSound	§(c) NECESSARY AXIOM
SafetyLemmas.idr:68	charEqSym	§(c) NECESSARY AXIOM
SafetyLemmas.idr:226	unpackLength	§(c) NECESSARY AXIOM
SafetyLemmas.idr:236	appendLengthSum	§(c) NECESSARY AXIOM
SafetyLemmas.idr:246	substrLengthBound	§(c) NECESSARY AXIOM

§(a) DISCHARGED: 0. §(b) BUDGETED: 0 (the externally-validated harness
under docs/backend-assurance/ is §(b)-style discipline applied to §(c)
items per standards#203 §"Precedent"). §(d) DEBT: 0.

Test plan

• bash scripts/check-trusted-base.sh . (when the standards#211
  trusted-base job runs against this branch) reports
  [OK] All 5 escape hatch(es) are documented (inline annotation or entry in: docs/proof-debt.md PROOF-NEEDS.md).
• CI green on the trusted-base job specifically.
• No behavioural change in Idris2 build — believe_me bodies and
  signatures untouched; only doc-comments edited.

Refs: hyperpolymath/standards#203 (policy), hyperpolymath/standards#211
(enforcement), #161 (proof-debt.md seed).

🤖 Generated with Claude Code

Co-Authored-By: Claude Opus 4.7 (1M context) noreply@anthropic.com

[github-actions]

🔍 Hypatia Security Scan

Findings: 151 issues detected

Severity	Count
🔴 Critical	18
🟠 High	124
🟡 Medium	9

⚠️ 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": "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": "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/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/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/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/hesiod-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/mcp-bridge/main.d.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "believe_me undermines formal verification (1 occurrences, CWE-704)",
    "type": "believe_me",
    "file": "/home/runner/work/boj-server/boj-server/src/abi/Boj/SafeHTTP.idr",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

[github-actions]

🏁 path-claims bench

Commit a5d9ac1

Numbers

path-claims bench  (node v22.22.3)

  scenario                                              iters       ms        ns/op          ops/s
  --------------------------------------------------------------------------------------------------------------
  register: 10 active claims, 3 new paths               50000 iters    178 ms      3.57 µs/op    280.1k ops/s
  register: 100 active claims, 3 new paths              20000 iters    332 ms     16.61 µs/op     60.2k ops/s
  register: 1000 active claims, 3 new paths              5000 iters    989 ms    197.89 µs/op      5.1k ops/s
  register: 100 active claims, 20 new paths              5000 iters    360 ms     72.05 µs/op     13.9k ops/s

  pathsOverlap: deep diverge at segment 4             1000000 iters    156 ms     156.1 ns/op     6.40M ops/s
  pathsOverlap: short prefix match                    1000000 iters    136 ms     136.8 ns/op     7.31M ops/s

  refresh (existing claim)                             100000 iters     10 ms     107.6 ns/op     9.29M ops/s
  list (100 active claims)                              50000 iters    301 ms      6.04 µs/op    165.6k ops/s

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

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