From 4d37a812a8390bcc2d0c6755c6845f79c10319af Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Thu, 21 May 2026 10:06:24 +0100 Subject: [PATCH] feat(proof): backend-assurance harness for prim__strToCharList (2/4) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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) --- PROOF-NEEDS.md | 4 +- docs/backend-assurance/README.md | 2 +- docs/backend-assurance/prim__strToCharList.md | 140 +++++++++++++++++ .../prim_str_to_char_list_test.exs | 144 ++++++++++++++++++ 4 files changed, 287 insertions(+), 3 deletions(-) create mode 100644 docs/backend-assurance/prim__strToCharList.md create mode 100644 elixir/test/backend_assurance/prim_str_to_char_list_test.exs diff --git a/PROOF-NEEDS.md b/PROOF-NEEDS.md index cc4a22e..8a8dfab 100644 --- a/PROOF-NEEDS.md +++ b/PROOF-NEEDS.md @@ -27,7 +27,7 @@ Classification key: **(J)** genuinely unavoidable, documented as an axiom; |---|------|----------|------|-------|-----------| | 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. | | 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. | -| 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. | +| 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). | | 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. | | 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. | @@ -76,7 +76,7 @@ All five are class **(J)** — genuinely unavoidable in Idris2 0.8.0 |-------|------|---------------|----------------------------| | `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` | | `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` | -| `unpackLength` | `SafetyLemmas.idr:211` | `prim__strToCharList` preserves length — backend primitive correctness | _pending_ | +| `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` | | `appendLengthSum` | `SafetyLemmas.idr:219` | `prim__strAppend` length semantics — not reducible at type level | _pending_ | | `substrLengthBound` | `SafetyLemmas.idr:226` | `prim__strSubstr` length bound — not reducible at type level | _pending_ | diff --git a/docs/backend-assurance/README.md b/docs/backend-assurance/README.md index 9e2e826..0eb5b85 100644 --- a/docs/backend-assurance/README.md +++ b/docs/backend-assurance/README.md @@ -27,7 +27,7 @@ companion property-test harness lives under | Primitive | Axioms covered | Trusted-extraction | Property test | |--------------------|--------------------------------------|----------------------------------|----------------------------------------------------------------| | `prim__eqChar` | `charEqSound`, `charEqSym` | `prim__eqChar.md` | `elixir/test/backend_assurance/prim_eq_char_test.exs` | -| `prim__strToCharList` | `unpackLength` | _pending_ | _pending_ | +| `prim__strToCharList` | `unpackLength` | `prim__strToCharList.md` | `elixir/test/backend_assurance/prim_str_to_char_list_test.exs` | | `prim__strAppend` | `appendLengthSum` | _pending_ | _pending_ | | `prim__strSubstr` | `substrLengthBound` | _pending_ | _pending_ | diff --git a/docs/backend-assurance/prim__strToCharList.md b/docs/backend-assurance/prim__strToCharList.md new file mode 100644 index 0000000..8cc81fe --- /dev/null +++ b/docs/backend-assurance/prim__strToCharList.md @@ -0,0 +1,140 @@ +# Backend-Assurance: `prim__strToCharList` + +Trusted-extraction validation for the class-(J) axiom over Idris2's +`prim__strToCharList` primitive: + +- `unpackLength : (s : String) -> length (unpack s) = length s` + (`src/abi/Boj/SafetyLemmas.idr:218`) + +Declared `%unsafe` with `believe_me ()` in Idris2 0.8.0 because +`String` is an opaque primitive type with no constructors and no +in-language induction principle relating its primitive length to the +length of the derived `List Char`. This document argues — by +inspecting the backend lowerings that BoJ actually ships against — +that the length-preservation property holds. + +The companion property test +(`elixir/test/backend_assurance/prim_str_to_char_list_test.exs`) +exercises the BEAM half of this argument over the codepoint space. + +## What `prim__strToCharList` is + +`prim__strToCharList : String -> List Char` is a primitive operation +declared in Idris2's `Core.Primitives`. The `unpack : String -> List +Char` definition in `Data.String` calls it directly: + + public export + unpack : String -> List Char + unpack = prim__strToCharList + +Length is `prim__strLength` on the `String` side and the constructive +`length : List a -> Nat` on the `List Char` side. The axiom asserts +the two counts agree. + +The question reduces to: does `prim__strToCharList` produce a list +whose length equals the codepoint count of the input string, on +each shipping backend? + +## Chez Scheme backend (Idris2 default codegen) + +In `Compiler.Scheme.Chez`, `prim__strToCharList` lowers to the R6RS +procedure `string->list`, and `prim__strLength` lowers to +`string-length`. On Chez 9.x: + +- **String model.** R6RS §6.7 specifies that a Scheme string is a + sequence of Unicode characters (codepoints). +- **`string->list` semantics.** R6RS §11.12 specifies `string->list` + returns a newly-allocated list of the characters that make up the + given string, in the same order. +- **Length preservation.** Combining the two: the length of + `(string->list s)` (counting list cells) equals `(string-length + s)`. This is part of the Scheme standard, not an implementation + detail. + +No further evidence needed beyond citing the standard. + +## BEAM backend (Erlang / Elixir, where BoJ runs) + +BoJ's REST surface is Elixir on the BEAM. The runtime strings are +UTF-8 encoded binaries; the analogue of `unpack` on the BEAM is +`String.to_charlist/1`. + +On BEAM: + +- **String model.** As with the other string primitives in this + campaign, strings are UTF-8 binaries and `String.length/1` returns + codepoint count. The `length` referred to in the axiom is codepoint + count, matching Idris2 semantics on Chez. +- **`String.to_charlist/1` semantics.** Per the Elixir `String` + module documentation, `String.to_charlist/1` decodes a UTF-8 binary + to a list of codepoint integers. Each codepoint becomes exactly one + list cell; UTF-8 is prefix-free, so the decode is unambiguous and + the cell count equals the codepoint count. +- **Length preservation.** Combining the two facts: + `length(String.to_charlist(s)) == String.length(s)` for every + legal UTF-8 binary `s`. The harness exercises this directly. + +The property test exercises this over random strings sampled from the +legal codepoint range (excluding surrogates), plus explicit boundary +strings covering all four UTF-8 encoding widths (1/2/3/4 bytes) and +the empty-string corner. + +## Why this isn't circular + +The harness does not call `prim__strToCharList`. It calls Elixir +`String.to_charlist/1` and `String.length/1` directly. The argument +is: *the operation that Idris2 lowers `prim__strToCharList` + +`prim__strLength` to on the BEAM is `String.to_charlist/1` + +`String.length/1` on UTF-8 binaries*, so demonstrating those +operations satisfy the property is sufficient. The trusted-extraction +step is reading the lowering; the property-test step is verifying +the operation behaves as the lowering claims. + +For Chez, we do not run a Scheme harness — R6RS is sufficient +documentary evidence. If BoJ ever ships a backend whose string model +is not Unicode codepoints, this document gets a new section and a +matching property test, **and the axiom may need to be restated** — +see the *Honest framing* clause in +`docs/backend-assurance/README.md`. + +## Edge cases considered + +- **Empty string.** `String.to_charlist("") == []`; both lengths + are 0. Tested explicitly. A backend that allocated a sentinel + codepoint on empty input would surface here. +- **Multi-byte codepoints.** Tested via boundary strings covering + all four UTF-8 widths: ASCII (1 byte), Latin-1 supplement (2 bytes, + e.g. `café`), CJK (3 bytes, e.g. `日本語`), and astral plane + (4 bytes, e.g. `🦀`). Each width has a different number of bytes + per codepoint, but the codepoint count (and hence the list length) + is invariant. +- **Surrogates** (`0xD800..0xDFFF`): excluded from the codepoint + generator. These are illegal as standalone codepoints in + well-formed Unicode; the harness also asserts that no surrogate + ever appears in the output of `String.to_charlist/1` on a legal + input, as a sanity check. +- **Normalisation.** Out of scope. The axiom is about codepoint + count, not grapheme-cluster count. `é` (`U+00E9`) yields a + one-element charlist; `e` (`U+0065`) + combining acute (`U+0301`) + yields a two-element charlist. Both are "correct" under the axiom. +- **Round-trip.** Not in the axiom but tested as a sanity check. + `to_string(String.to_charlist(s)) == s` for every legal `s`. This + guards against a backend whose `to_charlist` drops or duplicates + codepoints in a way that happens to preserve length (e.g. + replacing a malformed codepoint with U+FFFD on decode error). +- **Charlist element type.** The harness asserts every codepoint in + the output is a legal integer in `0..0x10FFFF` excluding the + surrogate range. Not the axiom but a sanity check that the + `length` we're measuring is over real codepoints. + +## References + +- Idris2 0.8.0 `src/Core/Primitives.idr` — primitive operation table. +- Idris2 0.8.0 `src/Compiler/Scheme/Chez.idr` — Chez codegen lowerings + for `prim__strToCharList` and `prim__strLength`. +- R6RS §6.7, §11.12 — Scheme string model and `string->list` + specification. +- Elixir `String` module documentation — `String.to_charlist/1` + semantics over UTF-8 binaries. +- `PROOF-NEEDS.md` — axiom audit (2026-05-18) and class-(J) framing. +- `src/abi/Boj/SafetyLemmas.idr` — axiom declaration (line 218). diff --git a/elixir/test/backend_assurance/prim_str_to_char_list_test.exs b/elixir/test/backend_assurance/prim_str_to_char_list_test.exs new file mode 100644 index 0000000..a9ff7c9 --- /dev/null +++ b/elixir/test/backend_assurance/prim_str_to_char_list_test.exs @@ -0,0 +1,144 @@ +# SPDX-License-Identifier: PMPL-1.0-or-later +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# Backend-assurance harness for `prim__strToCharList`. +# +# Validates that BEAM string-to-charlist conversion (Elixir +# `String.to_charlist/1` on UTF-8 binaries) satisfies the +# length-preservation axiom declared at: +# +# src/abi/Boj/SafetyLemmas.idr:218 unpackLength : +# (s : String) -> length (unpack s) = length s +# +# `unpack` in Idris2 calls `prim__strToCharList`. The axiom is class +# (J) — irreducible in Idris2 0.8.0 because `String` is an opaque +# primitive with no constructors and no induction principle relating +# its primitive length to the length of the derived `List Char`. See +# PROOF-NEEDS.md and docs/backend-assurance/prim__strToCharList.md for +# the campaign framing and the Chez (R6RS) lowering argument. +# +# This is *external* evidence: it does not change the in-language proof, +# and the believe_me site stays in source. The harness shrinks the +# trusted base from "we trust the backend" to "we randomly tested the +# operation against the property over N strings". +# +# Idris2's `length` on `String` is codepoint count (Chez +# `string-length` on R6RS characters; BEAM `String.length/1` on UTF-8 +# binaries). `String.to_charlist/1` returns a list of codepoint +# integers; `length/1` on that list returns the same count. Tests +# below use codepoint count, *not* byte count — the axiom is about +# logical-character length, not encoded-byte length. +defmodule Boj.BackendAssurance.PrimStrToCharListTest do + use ExUnit.Case, async: true + use ExUnitProperties + + @moduletag :backend_assurance + + # Random codepoint generator: covers ASCII, BMP, and astral planes + # excluding surrogates (which are illegal as standalone code units). + # Mirrors the codepoint generator in prim_eq_char_test.exs. + defp legal_codepoint do + StreamData.one_of([ + StreamData.integer(0..0xD7FF), + StreamData.integer(0xE000..0x10FFFF) + ]) + end + + defp legal_string do + StreamData.bind(StreamData.list_of(legal_codepoint(), max_length: 64), fn cps -> + StreamData.constant(List.to_string(cps)) + end) + end + + # ── Length preservation: |to_charlist(s)| = |s| ────────────────────── + # + # Backs `unpackLength`. On BEAM, `String.to_charlist/1` decodes a + # UTF-8 binary to a list of codepoint integers; the list length is + # the codepoint count, which matches `String.length/1` because UTF-8 + # is prefix-free (each codepoint occupies a self-delimiting + # 1-/2-/3-/4-byte sequence with no ambiguity). + property "BEAM String.to_charlist/1 preserves codepoint count (unpackLength)" do + check all s <- legal_string() do + assert length(String.to_charlist(s)) == String.length(s), + "unpackLength violation: |to_charlist(#{inspect(s)})| = " <> + "#{length(String.to_charlist(s))}, expected #{String.length(s)}" + end + end + + # ── Empty-string corner ────────────────────────────────────────────── + # + # `String.to_charlist("")` must yield the empty list, and both + # lengths are 0. A backend that allocated a sentinel codepoint on + # empty input would surface here. + test "empty string maps to empty charlist (both lengths zero)" do + assert String.to_charlist("") == [] + assert length(String.to_charlist("")) == 0 + assert String.length("") == 0 + end + + # ── Round-trip: to_string(to_charlist(s)) = s ──────────────────────── + # + # Not in the axiom but cheap to assert. The round-trip property + # guards against a backend whose charlist conversion drops or + # duplicates codepoints in a way that happens to preserve length + # (e.g. a 1-codepoint replacement on decode error). If round-trip + # fails, length preservation is suspect even when the counts agree. + property "to_string ∘ to_charlist is identity on legal strings" do + check all s <- legal_string() do + assert s |> String.to_charlist() |> to_string() == s, + "round-trip violation on #{inspect(s)}" + end + end + + # ── Charlist element type ─────────────────────────────────────────── + # + # `String.to_charlist/1` returns a list whose every element is a + # legal codepoint integer (non-negative, ≤ 0x10FFFF, not in the + # surrogate range). Not the axiom but a sanity check that the + # `length` we are measuring is over real codepoints. + property "to_charlist elements are legal codepoint integers" do + check all s <- legal_string() do + for cp <- String.to_charlist(s) do + assert is_integer(cp), "non-integer codepoint: #{inspect(cp)}" + assert cp >= 0 and cp <= 0x10FFFF, "out-of-range codepoint: #{cp}" + refute cp in 0xD800..0xDFFF, "surrogate codepoint in charlist: #{cp}" + end + end + end + + # ── Boundary cases the property generator may rarely hit ───────────── + # + # Multi-byte codepoint boundaries (ASCII, Latin-1 supplement + # boundary, BMP boundary, BMP→astral boundary, max codepoint, + # emoji) — each is a different UTF-8 encoding width (1/2/3/4 + # bytes). Length preservation must hold across all of them. + test "boundary strings satisfy unpackLength" do + boundaries = [ + "", + "a", + "ab", + "", + "", + "߿", + "ࠀ", + "퟿", + "", + "￿", + "\u{10000}", + "\u{10FFFF}", + "café", + "日本語", + "🦀" + ] + + for s <- boundaries do + assert length(String.to_charlist(s)) == String.length(s), + "unpackLength boundary violation: " <> + "|to_charlist(#{inspect(s)})| = #{length(String.to_charlist(s))}, " <> + "expected #{String.length(s)}" + + assert s |> String.to_charlist() |> to_string() == s, + "round-trip boundary violation: #{inspect(s)}" + end + end +end