feat(proof): backend-assurance harness for prim__strToCharList (2/4) — campaign complete

[hyperpolymath]

Summary

Closes the backend-assurance campaign for epic #87 Tier C. With
this slice merged alongside #129 (slice 1/4) and #139 (slices 3/4 +
4/4), all 5 class-(J) believe_me axioms in
src/abi/Boj/SafetyLemmas.idr have external evidence.

Discharges external evidence for the final class-(J) axiom:

Site	Axiom	Type
:218	unpackLength	(s : String) -> length (unpack s) = length s

The in-language proof does not change. The %unsafe /
believe_me site stays 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 / #139 template)

• elixir/test/backend_assurance/prim_str_to_char_list_test.exs —
  BEAM property tests over the legal codepoint space (surrogates
  excluded). 4 properties + 1 boundary table:
  • length preservation: length(String.to_charlist(s)) == String.length(s)
  • empty-string corner: String.to_charlist("") == []
  • round-trip identity: to_string(to_charlist(s)) == s
  • charlist element-type sanity (legal codepoints, no surrogates)
• docs/backend-assurance/prim__strToCharList.md — trusted-extraction
  prose. Chez argued from R6RS §6.7 (string model) + §11.12
  (string->list); BEAM argued from UTF-8 prefix-free codepoint
  counting via Elixir String.to_charlist/1 + String.length/1.
• docs/backend-assurance/README.md — coverage-table row flipped
  from pending.
• PROOF-NEEDS.md — backend-assurance evidence column filled for
  unpackLength. Class column updated to J ✓ marker (convention
  introduced by feat(proof): backend-assurance harness for prim__strAppend (3/4) + prim__strSubstr (4/4) #139). Site line number corrected from :211 to
  :218 (the file has shifted since the 2026-05-18 audit; previous
  PRs didn't sync this row).

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 module
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; round-trip property guards against a
  backend whose charlist conversion drops or duplicates codepoints
  in a way that happens to preserve length.

Test plan

• Elixir parse-check on the new test file (syntax-only, via
  Code.string_to_quoted!)
• BEAM operation smoke on boundary strings — 9 strings
  (empty, ASCII, Latin-1, CJK, astral, max codepoint, etc.); direct
  String.to_charlist/1 + String.length/1 + to_string calls
  outside the test harness. Length preservation and round-trip
  identity both hold across all 9.
• 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 slices 1/4 and 3/4+4/4 followed; CI is the gate.

Expected conflicts with #139

Both this PR and #139 branch off origin/main (per saved
stacked-PR-avoidance feedback), so they share a base. Conflicts on
merge are limited and trivial:

File	Conflict shape	Resolution
docs/backend-assurance/README.md	This PR flips the prim__strToCharList row; #139 flips the prim__strAppend and prim__strSubstr rows.	Different rows of the same table — line-level conflict only; accept both.
PROOF-NEEDS.md audit table	This PR updates row 3; #139 updates rows 1/2/4/5 and adds the J ✓ explanation paragraph.	Different rows; accept both.
PROOF-NEEDS.md remaining-axiomatic-surface table	This PR updates unpackLength row; #139 updates the other four.	Different rows; accept both.
PROOF-NEEDS.md standing note "Primitives validated so far"	#139 bumps it to 3/4; reviewer should apply 4/4 (campaign complete) once both merge.	Manual one-line edit during merge of whichever PR lands second.

The J ✓ marker is used on row 3 here even though the
explanation paragraph is contributed by #139 — post-#139-merge the
explanation is in place, and the marker's meaning is self-evident
from the value.

Heads-up for the reviewer

After this PR + #139 merge, the 4-slice backend-assurance harness is
complete. All 5 class-(J) axioms in SafetyLemmas.idr have
external evidence:

• charEqSound, charEqSym via prim__eqChar (feat(proof): backend-assurance harness for prim__eqChar (1/4) #129)
• unpackLength via prim__strToCharList (this PR)
• appendLengthSum via prim__strAppend (feat(proof): backend-assurance harness for prim__strAppend (3/4) + prim__strSubstr (4/4) #139)
• substrLengthBound via prim__strSubstr (feat(proof): backend-assurance harness for prim__strAppend (3/4) + prim__strSubstr (4/4) #139)

Future trusted-extraction work would only be needed if BoJ ships a
new codegen backend (e.g. JavaScript, native ML).

Refs #87 (Tier C backend-assurance campaign — closes the harness
sequence).

🤖 Generated with Claude Code