Skip to content

Commit 4d37a81

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
feat(proof): backend-assurance harness for prim__strToCharList (2/4)
Final slice of epic #87 Tier C backend-assurance campaign. Closes the 4-primitive sequence after #129 (prim__eqChar, slice 1/4) and #139 (prim__strAppend + prim__strSubstr, slices 3/4 + 4/4). With this slice merged, all 5 class-(J) believe_me axioms in src/abi/Boj/SafetyLemmas.idr have external backend-assurance evidence — modulo any future backend (JS, native, etc.) that would need a fresh trusted-extraction argument. Discharges external evidence for one class-(J) believe_me axiom: :218 unpackLength : (s : String) -> length (unpack s) = length s The in-language proof does NOT change. The %unsafe / believe_me site stays 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 against the property". Artefacts (matching the #129 / #139 template): - elixir/test/backend_assurance/prim_str_to_char_list_test.exs BEAM property tests via stream_data over UTF-8 binaries. Properties: length preservation, empty-string corner, round-trip identity (to_string ∘ to_charlist), charlist element-type sanity (legal codepoints, no surrogates), + boundary table covering all four UTF-8 encoding widths (ASCII / Latin-1 / CJK / astral). - docs/backend-assurance/prim__strToCharList.md Trusted-extraction prose: Chez (R6RS string->list + string-length, §6.7 + §11.12) and BEAM (Elixir String.to_charlist/1 + String.length/1 over UTF-8, prefix-free codepoint counting). - docs/backend-assurance/README.md Coverage table flipped from _pending_ for prim__strToCharList. - PROOF-NEEDS.md Backend-assurance evidence column filled for unpackLength; class column updated to "J ✓" marker indicating externally-validated class-(J) status (convention introduced by #139). Site line number corrected from :211 to :218 (the file has shifted since the 2026-05-18 audit; the previous PR didn't sync this row). The CI workflow .github/workflows/backend-assurance.yml already path-filters on elixir/test/backend_assurance/** and docs/backend-assurance/** so the new test module is picked up automatically — no workflow change is needed. Constraints honoured (from docs/backend-assurance/README.md): - No new believe_me. External evidence only; the axiom stays. - 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/duplicates codepoints in a way that happens to preserve length. Test plan: - [ ] CI backend-assurance workflow: BEAM property tests green - [x] elixir parse-check on the new test file (syntax-only) - [x] 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. All pass; round-trip identity holds across all 9. - [ ] 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 this 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** (open at PR time of this branch): - docs/backend-assurance/README.md: this PR flips the prim__strToCharList row; #139 flips the prim__strAppend and prim__strSubstr rows. Different table rows, line-level conflict only. - PROOF-NEEDS.md: this PR updates row 3 (unpackLength) and the remaining-axiomatic-surface row for unpackLength. #139 updates rows 1/2/4/5 and the explanation paragraph introducing the "J ✓" marker convention. Trivial to resolve — the changes are in different rows. - PROOF-NEEDS.md standing note "Primitives validated so far": #139 bumps it to 3/4; once both merge, the bump should read 4/4 (or simpler, "campaign complete"). Reviewer please apply during merge of whichever PR lands second. The "J ✓" marker introduced by #139 is used here on row 3 even though the explanation paragraph is contributed by #139 — the convention's meaning is self-evident from the value alone, and post-#139-merge the explanation is in place. Refs #87 (Tier C backend-assurance campaign — closes the harness sequence). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 1a4e12e commit 4d37a81

4 files changed

Lines changed: 287 additions & 3 deletions

File tree

‎PROOF-NEEDS.md‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,7 @@ Classification key: **(J)** genuinely unavoidable, documented as an axiom;
2727
|---|------|----------|------|-------|-----------|
2828
| 1 | `SafetyLemmas.idr:53` | `charEqSound` | `(c1,c2:Char) -> c1 == c2 = True -> c1 = c2` | **J** | `Char` is an opaque primitive; `==` is `prim__eqChar` (foreign `Bool`). Idris2 0.8.0 has no in-language soundness principle for primitive equality. Standard, well-understood axiom. |
2929
| 2 | `SafetyLemmas.idr:60` | `charEqSym` | `(x,y:Char) -> (x == y) = (y == x)` | **J** | Symmetry of `prim__eqChar`. Same reason as #1 — opaque primitive, no decision procedure to recurse on. |
30-
| 3 | `SafetyLemmas.idr:211` | `unpackLength` | `length (unpack s) = length s` | **J** | `unpack` = `prim__strToCharList` (foreign). `String` is opaque with no induction principle; the relation between primitive `String` length and `List Char` length is not reducible in-language. |
30+
| 3 | `SafetyLemmas.idr:218` | `unpackLength` | `length (unpack s) = length s` | **J ✓** | `unpack` = `prim__strToCharList` (foreign). `String` is opaque with no induction principle; the relation between primitive `String` length and `List Char` length is not reducible in-language. **Externally validated** via backend-assurance harness (`docs/backend-assurance/prim__strToCharList.md` + BEAM property test). |
3131
| 4 | `SafetyLemmas.idr:219` | `appendLengthSum` | `length (s ++ t) = length s + length t` | **J** | `++` on `String` = `prim__strAppend` (foreign). Length additivity is a backend-semantics guarantee, not type-level reducible. |
3232
| 5 | `SafetyLemmas.idr:226` | `substrLengthBound` | `LTE (length (substr start len s)) len` | **J** | `substr` = `prim__strSubstr` (foreign). The "result no longer than `len`" bound is a primitive-semantics guarantee with no in-language proof. |
3333

@@ -76,7 +76,7 @@ All five are class **(J)** — genuinely unavoidable in Idris2 0.8.0
7676
|-------|------|---------------|----------------------------|
7777
| `charEqSound` | `SafetyLemmas.idr:53` | Soundness of `prim__eqChar` — backend primitive correctness | `docs/backend-assurance/prim__eqChar.md` + `elixir/test/backend_assurance/prim_eq_char_test.exs` |
7878
| `charEqSym` | `SafetyLemmas.idr:60` | Symmetry of `prim__eqChar` — backend primitive correctness | `docs/backend-assurance/prim__eqChar.md` + `elixir/test/backend_assurance/prim_eq_char_test.exs` |
79-
| `unpackLength` | `SafetyLemmas.idr:211` | `prim__strToCharList` preserves length — backend primitive correctness | _pending_ |
79+
| `unpackLength` | `SafetyLemmas.idr:218` | `prim__strToCharList` preserves length — backend primitive correctness, externally validated | `docs/backend-assurance/prim__strToCharList.md` + `elixir/test/backend_assurance/prim_str_to_char_list_test.exs` |
8080
| `appendLengthSum` | `SafetyLemmas.idr:219` | `prim__strAppend` length semantics — not reducible at type level | _pending_ |
8181
| `substrLengthBound` | `SafetyLemmas.idr:226` | `prim__strSubstr` length bound — not reducible at type level | _pending_ |
8282

‎docs/backend-assurance/README.md‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,7 @@ companion property-test harness lives under
2727
| Primitive | Axioms covered | Trusted-extraction | Property test |
2828
|--------------------|--------------------------------------|----------------------------------|----------------------------------------------------------------|
2929
| `prim__eqChar` | `charEqSound`, `charEqSym` | `prim__eqChar.md` | `elixir/test/backend_assurance/prim_eq_char_test.exs` |
30-
| `prim__strToCharList` | `unpackLength` | _pending_ | _pending_ |
30+
| `prim__strToCharList` | `unpackLength` | `prim__strToCharList.md` | `elixir/test/backend_assurance/prim_str_to_char_list_test.exs` |
3131
| `prim__strAppend` | `appendLengthSum` | _pending_ | _pending_ |
3232
| `prim__strSubstr` | `substrLengthBound` | _pending_ | _pending_ |
3333

‎docs/backend-assurance/prim__strToCharList.md‎

Lines changed: 140 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,140 @@
1+
# Backend-Assurance: `prim__strToCharList`
2+
3+
Trusted-extraction validation for the class-(J) axiom over Idris2's
4+
`prim__strToCharList` primitive:
5+
6+
- `unpackLength : (s : String) -> length (unpack s) = length s`
7+
(`src/abi/Boj/SafetyLemmas.idr:218`)
8+
9+
Declared `%unsafe` with `believe_me ()` in Idris2 0.8.0 because
10+
`String` is an opaque primitive type with no constructors and no
11+
in-language induction principle relating its primitive length to the
12+
length of the derived `List Char`. This document argues — by
13+
inspecting the backend lowerings that BoJ actually ships against —
14+
that the length-preservation property holds.
15+
16+
The companion property test
17+
(`elixir/test/backend_assurance/prim_str_to_char_list_test.exs`)
18+
exercises the BEAM half of this argument over the codepoint space.
19+
20+
## What `prim__strToCharList` is
21+
22+
`prim__strToCharList : String -> List Char` is a primitive operation
23+
declared in Idris2's `Core.Primitives`. The `unpack : String -> List
24+
Char` definition in `Data.String` calls it directly:
25+
26+
public export
27+
unpack : String -> List Char
28+
unpack = prim__strToCharList
29+
30+
Length is `prim__strLength` on the `String` side and the constructive
31+
`length : List a -> Nat` on the `List Char` side. The axiom asserts
32+
the two counts agree.
33+
34+
The question reduces to: does `prim__strToCharList` produce a list
35+
whose length equals the codepoint count of the input string, on
36+
each shipping backend?
37+
38+
## Chez Scheme backend (Idris2 default codegen)
39+
40+
In `Compiler.Scheme.Chez`, `prim__strToCharList` lowers to the R6RS
41+
procedure `string->list`, and `prim__strLength` lowers to
42+
`string-length`. On Chez 9.x:
43+
44+
- **String model.** R6RS §6.7 specifies that a Scheme string is a
45+
sequence of Unicode characters (codepoints).
46+
- **`string->list` semantics.** R6RS §11.12 specifies `string->list`
47+
returns a newly-allocated list of the characters that make up the
48+
given string, in the same order.
49+
- **Length preservation.** Combining the two: the length of
50+
`(string->list s)` (counting list cells) equals `(string-length
51+
s)`. This is part of the Scheme standard, not an implementation
52+
detail.
53+
54+
No further evidence needed beyond citing the standard.
55+
56+
## BEAM backend (Erlang / Elixir, where BoJ runs)
57+
58+
BoJ's REST surface is Elixir on the BEAM. The runtime strings are
59+
UTF-8 encoded binaries; the analogue of `unpack` on the BEAM is
60+
`String.to_charlist/1`.
61+
62+
On BEAM:
63+
64+
- **String model.** As with the other string primitives in this
65+
campaign, strings are UTF-8 binaries and `String.length/1` returns
66+
codepoint count. The `length` referred to in the axiom is codepoint
67+
count, matching Idris2 semantics on Chez.
68+
- **`String.to_charlist/1` semantics.** Per the Elixir `String`
69+
module documentation, `String.to_charlist/1` decodes a UTF-8 binary
70+
to a list of codepoint integers. Each codepoint becomes exactly one
71+
list cell; UTF-8 is prefix-free, so the decode is unambiguous and
72+
the cell count equals the codepoint count.
73+
- **Length preservation.** Combining the two facts:
74+
`length(String.to_charlist(s)) == String.length(s)` for every
75+
legal UTF-8 binary `s`. The harness exercises this directly.
76+
77+
The property test exercises this over random strings sampled from the
78+
legal codepoint range (excluding surrogates), plus explicit boundary
79+
strings covering all four UTF-8 encoding widths (1/2/3/4 bytes) and
80+
the empty-string corner.
81+
82+
## Why this isn't circular
83+
84+
The harness does not call `prim__strToCharList`. It calls Elixir
85+
`String.to_charlist/1` and `String.length/1` directly. The argument
86+
is: *the operation that Idris2 lowers `prim__strToCharList` +
87+
`prim__strLength` to on the BEAM is `String.to_charlist/1` +
88+
`String.length/1` on UTF-8 binaries*, so demonstrating those
89+
operations satisfy the property is sufficient. The trusted-extraction
90+
step is reading the lowering; the property-test step is verifying
91+
the operation behaves as the lowering claims.
92+
93+
For Chez, we do not run a Scheme harness — R6RS is sufficient
94+
documentary evidence. If BoJ ever ships a backend whose string model
95+
is not Unicode codepoints, this document gets a new section and a
96+
matching property test, **and the axiom may need to be restated** —
97+
see the *Honest framing* clause in
98+
`docs/backend-assurance/README.md`.
99+
100+
## Edge cases considered
101+
102+
- **Empty string.** `String.to_charlist("") == []`; both lengths
103+
are 0. Tested explicitly. A backend that allocated a sentinel
104+
codepoint on empty input would surface here.
105+
- **Multi-byte codepoints.** Tested via boundary strings covering
106+
all four UTF-8 widths: ASCII (1 byte), Latin-1 supplement (2 bytes,
107+
e.g. `café`), CJK (3 bytes, e.g. `日本語`), and astral plane
108+
(4 bytes, e.g. `🦀`). Each width has a different number of bytes
109+
per codepoint, but the codepoint count (and hence the list length)
110+
is invariant.
111+
- **Surrogates** (`0xD800..0xDFFF`): excluded from the codepoint
112+
generator. These are illegal as standalone codepoints in
113+
well-formed Unicode; the harness also asserts that no surrogate
114+
ever appears in the output of `String.to_charlist/1` on a legal
115+
input, as a sanity check.
116+
- **Normalisation.** Out of scope. The axiom is about codepoint
117+
count, not grapheme-cluster count. `é` (`U+00E9`) yields a
118+
one-element charlist; `e` (`U+0065`) + combining acute (`U+0301`)
119+
yields a two-element charlist. Both are "correct" under the axiom.
120+
- **Round-trip.** Not in the axiom but tested as a sanity check.
121+
`to_string(String.to_charlist(s)) == s` for every legal `s`. This
122+
guards against a backend whose `to_charlist` drops or duplicates
123+
codepoints in a way that happens to preserve length (e.g.
124+
replacing a malformed codepoint with U+FFFD on decode error).
125+
- **Charlist element type.** The harness asserts every codepoint in
126+
the output is a legal integer in `0..0x10FFFF` excluding the
127+
surrogate range. Not the axiom but a sanity check that the
128+
`length` we're measuring is over real codepoints.
129+
130+
## References
131+
132+
- Idris2 0.8.0 `src/Core/Primitives.idr` — primitive operation table.
133+
- Idris2 0.8.0 `src/Compiler/Scheme/Chez.idr` — Chez codegen lowerings
134+
for `prim__strToCharList` and `prim__strLength`.
135+
- R6RS §6.7, §11.12 — Scheme string model and `string->list`
136+
specification.
137+
- Elixir `String` module documentation — `String.to_charlist/1`
138+
semantics over UTF-8 binaries.
139+
- `PROOF-NEEDS.md` — axiom audit (2026-05-18) and class-(J) framing.
140+
- `src/abi/Boj/SafetyLemmas.idr` — axiom declaration (line 218).

‎elixir/test/backend_assurance/prim_str_to_char_list_test.exs‎

Lines changed: 144 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,144 @@
1+
# SPDX-License-Identifier: PMPL-1.0-or-later
2+
# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
#
4+
# Backend-assurance harness for `prim__strToCharList`.
5+
#
6+
# Validates that BEAM string-to-charlist conversion (Elixir
7+
# `String.to_charlist/1` on UTF-8 binaries) satisfies the
8+
# length-preservation axiom declared at:
9+
#
10+
# src/abi/Boj/SafetyLemmas.idr:218 unpackLength :
11+
# (s : String) -> length (unpack s) = length s
12+
#
13+
# `unpack` in Idris2 calls `prim__strToCharList`. The axiom is class
14+
# (J) — irreducible in Idris2 0.8.0 because `String` is an opaque
15+
# primitive with no constructors and no induction principle relating
16+
# its primitive length to the length of the derived `List Char`. See
17+
# PROOF-NEEDS.md and docs/backend-assurance/prim__strToCharList.md for
18+
# the campaign framing and the Chez (R6RS) lowering argument.
19+
#
20+
# This is *external* evidence: it does not change the in-language proof,
21+
# and the believe_me site stays in source. The harness shrinks the
22+
# trusted base from "we trust the backend" to "we randomly tested the
23+
# operation against the property over N strings".
24+
#
25+
# Idris2's `length` on `String` is codepoint count (Chez
26+
# `string-length` on R6RS characters; BEAM `String.length/1` on UTF-8
27+
# binaries). `String.to_charlist/1` returns a list of codepoint
28+
# integers; `length/1` on that list returns the same count. Tests
29+
# below use codepoint count, *not* byte count — the axiom is about
30+
# logical-character length, not encoded-byte length.
31+
defmodule Boj.BackendAssurance.PrimStrToCharListTest do
32+
use ExUnit.Case, async: true
33+
use ExUnitProperties
34+
35+
@moduletag :backend_assurance
36+
37+
# Random codepoint generator: covers ASCII, BMP, and astral planes
38+
# excluding surrogates (which are illegal as standalone code units).
39+
# Mirrors the codepoint generator in prim_eq_char_test.exs.
40+
defp legal_codepoint do
41+
StreamData.one_of([
42+
StreamData.integer(0..0xD7FF),
43+
StreamData.integer(0xE000..0x10FFFF)
44+
])
45+
end
46+
47+
defp legal_string do
48+
StreamData.bind(StreamData.list_of(legal_codepoint(), max_length: 64), fn cps ->
49+
StreamData.constant(List.to_string(cps))
50+
end)
51+
end
52+
53+
# ── Length preservation: |to_charlist(s)| = |s| ──────────────────────
54+
#
55+
# Backs `unpackLength`. On BEAM, `String.to_charlist/1` decodes a
56+
# UTF-8 binary to a list of codepoint integers; the list length is
57+
# the codepoint count, which matches `String.length/1` because UTF-8
58+
# is prefix-free (each codepoint occupies a self-delimiting
59+
# 1-/2-/3-/4-byte sequence with no ambiguity).
60+
property "BEAM String.to_charlist/1 preserves codepoint count (unpackLength)" do
61+
check all s <- legal_string() do
62+
assert length(String.to_charlist(s)) == String.length(s),
63+
"unpackLength violation: |to_charlist(#{inspect(s)})| = " <>
64+
"#{length(String.to_charlist(s))}, expected #{String.length(s)}"
65+
end
66+
end
67+
68+
# ── Empty-string corner ──────────────────────────────────────────────
69+
#
70+
# `String.to_charlist("")` must yield the empty list, and both
71+
# lengths are 0. A backend that allocated a sentinel codepoint on
72+
# empty input would surface here.
73+
test "empty string maps to empty charlist (both lengths zero)" do
74+
assert String.to_charlist("") == []
75+
assert length(String.to_charlist("")) == 0
76+
assert String.length("") == 0
77+
end
78+
79+
# ── Round-trip: to_string(to_charlist(s)) = s ────────────────────────
80+
#
81+
# Not in the axiom but cheap to assert. The round-trip property
82+
# guards against a backend whose charlist conversion drops or
83+
# duplicates codepoints in a way that happens to preserve length
84+
# (e.g. a 1-codepoint replacement on decode error). If round-trip
85+
# fails, length preservation is suspect even when the counts agree.
86+
property "to_string ∘ to_charlist is identity on legal strings" do
87+
check all s <- legal_string() do
88+
assert s |> String.to_charlist() |> to_string() == s,
89+
"round-trip violation on #{inspect(s)}"
90+
end
91+
end
92+
93+
# ── Charlist element type ───────────────────────────────────────────
94+
#
95+
# `String.to_charlist/1` returns a list whose every element is a
96+
# legal codepoint integer (non-negative, ≤ 0x10FFFF, not in the
97+
# surrogate range). Not the axiom but a sanity check that the
98+
# `length` we are measuring is over real codepoints.
99+
property "to_charlist elements are legal codepoint integers" do
100+
check all s <- legal_string() do
101+
for cp <- String.to_charlist(s) do
102+
assert is_integer(cp), "non-integer codepoint: #{inspect(cp)}"
103+
assert cp >= 0 and cp <= 0x10FFFF, "out-of-range codepoint: #{cp}"
104+
refute cp in 0xD800..0xDFFF, "surrogate codepoint in charlist: #{cp}"
105+
end
106+
end
107+
end
108+
109+
# ── Boundary cases the property generator may rarely hit ─────────────
110+
#
111+
# Multi-byte codepoint boundaries (ASCII, Latin-1 supplement
112+
# boundary, BMP boundary, BMP→astral boundary, max codepoint,
113+
# emoji) — each is a different UTF-8 encoding width (1/2/3/4
114+
# bytes). Length preservation must hold across all of them.
115+
test "boundary strings satisfy unpackLength" do
116+
boundaries = [
117+
"",
118+
"a",
119+
"ab",
120+
"",
121+
"",
122+
"߿",
123+
"ࠀ",
124+
"퟿",
125+
"",
126+
"￿",
127+
"\u{10000}",
128+
"\u{10FFFF}",
129+
"café",
130+
"日本語",
131+
"🦀"
132+
]
133+
134+
for s <- boundaries do
135+
assert length(String.to_charlist(s)) == String.length(s),
136+
"unpackLength boundary violation: " <>
137+
"|to_charlist(#{inspect(s)})| = #{length(String.to_charlist(s))}, " <>
138+
"expected #{String.length(s)}"
139+
140+
assert s |> String.to_charlist() |> to_string() == s,
141+
"round-trip boundary violation: #{inspect(s)}"
142+
end
143+
end
144+
end

0 commit comments

Comments
 (0)