proof: discharge charEqSym axiom (5→4) + TLA+ model of the Elixir JsWorker

[hyperpolymath]

Proof-completion work across two layers. Both pieces share this branch because the session is pinned to it; they are logically independent and reviewable as separate commits.

---

1 — ABI: discharge charEqSym axiom → constructive theorem (666c3e0)

charEqSym : (x, y : Char) -> (x == y) = (y == x) was a class-(J) believe_me axiom classified "genuinely unavoidable." It isn't — it is derivable from charEqSound (which the repo already has):

• x == y = True → charEqSound gives x = y, collapsing both sides → both True;
• a mixed True/False split is impossible (soundness forces the contradiction);
• both False → trivially equal.

No new axiom is introduced. This is the first (a) DISCHARGED entry under the trusted-base reduction policy (standards#203), dropping the sanctioned count 5 → 4. Survivors (charEqSound, unpackLength, appendLengthSum, substrLengthBound) remain genuinely irreducible over opaque Char/String primitives.

Verified: cd src/abi && idris2 --typecheck boj.ipkg → 17/17 modules clean (Idris2 0.8.0, Chez 9.5.8); bash scripts/check-trusted-base.sh → OK, 4 axioms. (Same run confirms Boj.CartridgeDispatch/BJ1 still type-checks.)

Count reconciled across check-trusted-base.sh (EXPECTED_AXIOMS 5→4), PROOF-NEEDS.md, docs/proof-debt.md (charEqSym → §(a)), STATE.a2ml, and docs/backend-assurance/prim__eqChar.md. Also fixed pre-existing drift in src/abi/README.adoc: it wrongly listed logSafeBounded as a believe_me (constructive since #116), said "graded D" (READINESS says C), and called CartridgeDispatch "WIP / not in boj.ipkg" (it's in-package and type-checks).

2 — Elixir: TLA+ model of BojRest.JsWorker (836c977)

specs/elixir-harness/ — a TLA+ model of elixir/lib/boj_rest/js_worker.ex (GenServer pipelining concurrent requests to one persistent Deno Port, per-request 30 s timeout, crash-replies-all + :one_for_one restart). Closes the "Elixir harness has no formal coverage" gap on the proof axis (the Idris2 proofs stop at the Zig FFI boundary).

Verified with TLC (Requests = {r1,r2,r3}, 341 states, no error):

• ReplyOnce — no caller replied twice under any response/timeout/crash interleaving (the Map.pop guard). Headline.
• Consistent, NoPendingWhileDown — crash clears pending atomically.
• EventuallyReplied (liveness) — the 30 s timer guarantees termination even if Deno hangs.
• Non-vacuity: ReachOk/ReachTimeout/ReachCrashed sanity controls all refuted (all terminal outcomes reachable).

Deferred (noted in the README): the JsWorkerPool routing/supervision layer, and the Invoker pool once it exists (it's fork-per-request today — ADR-0005/0006).

---

Scope

Items 1 + 2 (Idris ABI) and item 4 (Elixir model). Zig FFI/invariants (item 3) is out of scope (separate workstream). Also carries ef959f0 (prior allTake dedup, not yet on main). Neither piece moves the CRG grade — both are on the formal-proof axis, not the empirical/dogfooding axis.

🤖 Generated with Claude Code

https://claude.ai/code/session_01XrPAh7eBSUcVKauTVdXH9Y

---

Generated by Claude Code

[cloudflare-workers-and-pages]

Deploying with    Cloudflare Workers

The latest updates on your project. Learn more about integrating Git with Workers.

Status	Name	Latest Commit	Updated (UTC)
❌ Deployment failed View logs	boj-server	c5956d7	Jun 24 2026, 05:52 PM

[github-actions]

🔍 Hypatia Security Scan

Findings: 219 issues detected

Severity	Count
🔴 Critical	15
🟠 High	131
🟡 Medium	73

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Action actions/checkout@v4 needs attention",
    "type": "unpinned_action",
    "file": "pages-deploy.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in pages-deploy.yml",
    "type": "missing_timeout_minutes",
    "file": "pages-deploy.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in push-email-notify.yml",
    "type": "missing_timeout_minutes",
    "file": "push-email-notify.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "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"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

[github-actions]

🏁 path-claims bench

Commit f7025ae

Numbers

path-claims bench  (node v22.23.0)

  scenario                                              iters       ms        ns/op          ops/s
  --------------------------------------------------------------------------------------------------------------
  register: 10 active claims, 3 new paths               50000 iters    185 ms      3.71 µs/op    269.5k ops/s
  register: 100 active claims, 3 new paths              20000 iters    323 ms     16.16 µs/op     61.9k ops/s
  register: 1000 active claims, 3 new paths              5000 iters    964 ms    192.92 µs/op      5.2k ops/s
  register: 100 active claims, 20 new paths              5000 iters    366 ms     73.31 µs/op     13.6k ops/s

  pathsOverlap: deep diverge at segment 4             1000000 iters    155 ms     155.7 ns/op     6.42M ops/s
  pathsOverlap: short prefix match                    1000000 iters    137 ms     137.5 ns/op     7.27M ops/s

  refresh (existing claim)                             100000 iters     11 ms     112.9 ns/op     8.85M ops/s
  list (100 active claims)                              50000 iters    285 ms      5.71 µs/op    175.0k ops/s

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

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