feat(proof): backend-assurance harness for prim__strAppend (3/4) + prim__strSubstr (4/4)

[hyperpolymath]

Summary

Continues the backend-assurance campaign for epic #87 Tier C. Slice
1/4 (prim__eqChar, covering charEqSound + charEqSym) landed via
#129. This PR bundles slices 3/4 and 4/4 per explicit owner
direction — both prim__strAppend and prim__strSubstr are
length-arithmetic on opaque strings and share the same Chez-vs-BEAM
trusted-extraction argument shape, so a combined slice trades the
nominal "one PR per primitive" rule for review ergonomics.

Slice 2/4 (prim__strToCharList, covering unpackLength) remains
pending; ships as a follow-on PR.

Discharges external evidence for two class-(J) believe_me
axioms in src/abi/Boj/SafetyLemmas.idr:

Site	Axiom	Type
:226	appendLengthSum	length (s ++ t) = length s + length t
:233	substrLengthBound	LTE (length (substr start len s)) len

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

Artefacts (matching the #129 template)

• elixir/test/backend_assurance/prim_str_append_test.exs — BEAM
  property tests over the legal codepoint space (surrogates
  excluded). 4 properties + 1 boundary table covering all four UTF-8
  encoding widths (ASCII / Latin-1 / CJK / astral).
• elixir/test/backend_assurance/prim_str_substr_test.exs — BEAM
  property tests for the length bound. 4 properties + boundary
  table covering len=0, start-past-end, full-string slice tightness,
  and multi-byte codepoint slices.
• docs/backend-assurance/prim__strAppend.md — trusted-extraction
  prose. Chez argued from R6RS §6.7 (string model) + §11.12
  (string-append); BEAM argued from UTF-8 prefix-free codepoint
  counting via Elixir <> + String.length/1.
• docs/backend-assurance/prim__strSubstr.md — trusted-extraction
  prose. Chez argued from R6RS §11.12 (substring) + codegen clamp;
  BEAM argued from String.slice/3 codepoint-counting clamp.
• docs/backend-assurance/README.md — coverage-table rows flipped
  from pending for both primitives.
• PROOF-NEEDS.md — backend-assurance evidence column filled.
  Class column updated to J ✓ marker for the externally-
  validated rows (a bare J indicates harness not yet landed).
  Audit-table rationales updated to note the harness; remaining-
  axiomatic-surface justifications reworded; standing-note
  "primitives landed" line bumped to reflect 3/4 done.

The existing CI workflow .github/workflows/backend-assurance.yml
already path-filters on elixir/test/backend_assurance/** and
docs/backend-assurance/**, so it picks up the new test modules
automatically — no workflow change in this PR.

Constraints honoured

Per docs/backend-assurance/README.md:

• No new believe_me. External evidence only.
• No in-language discharge. Ruled out by 2026-05-18 audit.
• Two backends. Chez argued from R6RS; BEAM exercised by tests.
• Honest framing. Surrogates excluded; normalisation out of
  scope and documented; negative len/start ruled out by upstream
  Nat typing.

Test plan

• Elixir parse-check on both new test files (syntax-only, via
  Code.string_to_quoted!)
• BEAM operation smoke on boundary strings — String.length /
  String.slice/3 direct, outside the test harness. 25
  appendLengthSum cases + 80 substrLengthBound cases all hold.
• CI backend-assurance workflow: BEAM property tests green
• CI: existing workflows unaffected (no path-filter collisions)

Note: this session could not run mix test --only backend_assurance
locally — the asdf elixir 1.18.4-otp-25 install on the work
machine is empty (only .mix archives, no binary), and system
elixir 1.14 fails the project's ~> 1.15 requirement. Same gap
pattern slice 1/4 followed; CI is the gate.

Heads-up for the reviewer

PROOF-NEEDS.md now uses a J ✓ marker on the audit-table
Class column for the three externally-validated axioms
(charEqSound, charEqSym from #129; appendLengthSum,
substrLengthBound from this PR). The fifth axiom (unpackLength)
remains bare J until slice 2/4 lands. The wording change is
deliberate per owner direction — the underlying classification is
still class (J); the marker reflects external validation.

Refs #87 (Tier C backend-assurance campaign).

🤖 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