feat(proof): backend-assurance harness for prim__eqChar (1/4)

[hyperpolymath]

Summary

First backend-assurance deliverable for epic #87 Tier C — the
class-(J) believe_me axioms in src/abi/Boj/SafetyLemmas.idr that
the 2026-05-18 audit ruled irreducible in Idris2 0.8.0 (opaque Char
/ String primitives, foreign-backed). Covers charEqSound and
charEqSym — both ride on prim__eqChar.

The in-language proof does not change. The %unsafe /
believe_me sites stay in SafetyLemmas.idr. The harness shrinks the
trusted base from "we trust the backend" to "we read the backend
lowering and randomly tested the operation".

Artefacts

• elixir/test/backend_assurance/prim_eq_char_test.exs — BEAM-native
  property tests via stream_data over the legal codepoint space
  (0..0xD7FF ∪ 0xE000..0x10FFFF, surrogates excluded). Covers
  soundness, reflexivity, symmetry, distinct-codepoints negative
  edge, plus an explicit boundary table. 4 properties + 1 unit test;
  all pass locally on Elixir 1.18.4 / OTP 27 in ~0.09 s.
• docs/backend-assurance/prim__eqChar.md — trusted-extraction prose
  argument citing Idris2 0.8.0's lowering for each shipping backend:
  Chez (R6RS char=? is a total equivalence relation per §11.11) and
  BEAM (=:= on codepoint integers per erlang(3)). Discusses
  surrogates (excluded), normalisation (out of scope), case folding
  (out of scope and explicitly guarded by the negative-edge property).
• docs/backend-assurance/README.md — campaign overview, coverage
  table (1 done / 3 pending), and constraints.
• tests/backend-assurance/README.md — pointer to where the runnable
  harness lives.
• PROOF-NEEDS.md — new Backend-assurance-evidence column on the
  axiom audit table; other three primitives marked pending.
• .github/workflows/backend-assurance.yml — path-filtered CI job
  running mix test --only backend_assurance on PRs touching
  SafetyLemmas.idr, the harness, or workflow itself. Pinned to
  erlef/setup-beam@fc68ffb9 (v1.24.0) per estate post-rotation
  workflow-pinning policy. Concurrency-cancel guard included.

Scope & coordination

This PR is one slice of four:

1. prim__eqChar (this PR) — backs charEqSound, charEqSym
2. prim__strToCharList — backs unpackLength (pending follow-on)
3. prim__strAppend — backs appendLengthSum (pending)
4. prim__strSubstr — backs substrLengthBound (pending)

One PR per primitive keeps review chunks small. Estimate ~3 months
end-to-end.

Heads-up for the reviewer: a parallel work-stream is staging an
Agda abstract-model lane and a SPARK/Ada systems-boundary lane for
the same campaign (untracked proofs/agda/, spark/, and
tests/backend-assurance/run.sh in the working tree at PR time;
not in this PR). Those will land as a follow-on PR with the
matching doc cross-references — this PR's docs link only to the
artefacts it ships.

Constraints honoured

Per the backend-assurance framing in PROOF-NEEDS.md:

• No new believe_me — purely external evidence.
• No in-language discharge — ruled out by 2026-05-18 audit.
• Two backends — Chez argued from R6RS; BEAM exercised by tests.
• Honest framing — if a primitive ever fails its axiom, adjust
  the axiom; don't paper over.

Test plan

• cd elixir && mix test --only backend_assurance — 4 properties + 1 test pass
• CI: backend-assurance workflow runs and goes green
• CI: existing workflows unaffected (no path-filter collisions)

Refs #87 (Tier C backend-assurance campaign). One PR per primitive;
this is 1/4.

🤖 Generated with Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 30 issues detected

Severity	Count
🔴 Critical	18
🟠 High	5
🟡 Medium	7

⚠️ 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 quality.yml",
    "type": "missing_workflow",
    "file": "quality.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in security-policy.yml",
    "type": "missing_workflow",
    "file": "security-policy.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "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"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

[github-actions]

🔍 Hypatia Security Scan

Findings: 30 issues detected

Severity	Count
🔴 Critical	18
🟠 High	5
🟡 Medium	7

⚠️ 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 quality.yml",
    "type": "missing_workflow",
    "file": "quality.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in security-policy.yml",
    "type": "missing_workflow",
    "file": "security-policy.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "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"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

[github-actions]

🔍 Hypatia Security Scan

Findings: 30 issues detected

Severity	Count
🔴 Critical	18
🟠 High	5
🟡 Medium	7

⚠️ 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 quality.yml",
    "type": "missing_workflow",
    "file": "quality.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in security-policy.yml",
    "type": "missing_workflow",
    "file": "security-policy.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "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"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence