diff --git a/PROOF-NEEDS.md b/PROOF-NEEDS.md index dc1b8d7..aa4eea6 100644 --- a/PROOF-NEEDS.md +++ b/PROOF-NEEDS.md @@ -25,11 +25,11 @@ Classification key: **(J)** genuinely unavoidable, documented as an axiom; | # | Site | Function | Type | Class | Rationale | |---|------|----------|------|-------|-----------| -| 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. **Externally validated** via backend-assurance harness (`docs/backend-assurance/prim__eqChar.md` + BEAM property test). | -| 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. **Externally validated** (same harness as #1). | -| 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. _Backend-assurance harness pending._ | -| 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. **Externally validated** via backend-assurance harness (`docs/backend-assurance/prim__strAppend.md` + BEAM property test). | -| 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. **Externally validated** via backend-assurance harness (`docs/backend-assurance/prim__strSubstr.md` + BEAM property test). | +| 1 | `SafetyLemmas.idr:60` | `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. **Externally validated** via backend-assurance harness (`docs/backend-assurance/prim__eqChar.md` + BEAM property test). | +| 2 | `SafetyLemmas.idr:67` | `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. **Externally validated** (same harness as #1). | +| 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:226` | `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. **Externally validated** via backend-assurance harness (`docs/backend-assurance/prim__strAppend.md` + BEAM property test). | +| 5 | `SafetyLemmas.idr:233` | `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. **Externally validated** via backend-assurance harness (`docs/backend-assurance/prim__strSubstr.md` + BEAM property test). | **Verdict: 5/5 are class (J).** All five reduce to the same root cause: Idris2 treats `Char` and `String` as opaque primitive types whose @@ -83,11 +83,11 @@ All five are class **(J)** — genuinely unavoidable in Idris2 0.8.0 | Axiom | Site | Justification | Backend-assurance evidence | |-------|------|---------------|----------------------------| -| `charEqSound` | `SafetyLemmas.idr:53` | Soundness of `prim__eqChar` — backend primitive correctness, externally validated | `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, externally validated | `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_ | -| `appendLengthSum` | `SafetyLemmas.idr:219` | `prim__strAppend` length semantics — not reducible at type level, externally validated | `docs/backend-assurance/prim__strAppend.md` + `elixir/test/backend_assurance/prim_str_append_test.exs` | -| `substrLengthBound` | `SafetyLemmas.idr:226` | `prim__strSubstr` length bound — not reducible at type level, externally validated | `docs/backend-assurance/prim__strSubstr.md` + `elixir/test/backend_assurance/prim_str_substr_test.exs` | +| `charEqSound` | `SafetyLemmas.idr:60` | Soundness of `prim__eqChar` — backend primitive correctness, externally validated | `docs/backend-assurance/prim__eqChar.md` + `elixir/test/backend_assurance/prim_eq_char_test.exs` | +| `charEqSym` | `SafetyLemmas.idr:67` | Symmetry of `prim__eqChar` — backend primitive correctness, externally validated | `docs/backend-assurance/prim__eqChar.md` + `elixir/test/backend_assurance/prim_eq_char_test.exs` | +| `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:226` | `prim__strAppend` length semantics — not reducible at type level, externally validated | `docs/backend-assurance/prim__strAppend.md` + `elixir/test/backend_assurance/prim_str_append_test.exs` | +| `substrLengthBound` | `SafetyLemmas.idr:233` | `prim__strSubstr` length bound — not reducible at type level, externally validated | `docs/backend-assurance/prim__strSubstr.md` + `elixir/test/backend_assurance/prim_str_substr_test.exs` | Note: `logSafeBounded` in SafeAPIKey.idr no longer uses `believe_me` directly; it calls the documented SafetyLemmas axioms via structural proof. @@ -115,10 +115,10 @@ from "we trust the backend" to "we read the lowering and randomly tested the operation". Primitives validated so far: `prim__eqChar` (covering `charEqSound` -and `charEqSym`), `prim__strAppend` (covering `appendLengthSum`), -`prim__strSubstr` (covering `substrLengthBound`). Remaining: -`prim__strToCharList` (covering `unpackLength`). Tracked under epic -#87 Tier C backend-assurance campaign. +and `charEqSym`), `prim__strToCharList` (covering `unpackLength`), +`prim__strAppend` (covering `appendLengthSum`), and `prim__strSubstr` +(covering `substrLengthBound`). Tracked under epic #87 Tier C +backend-assurance campaign. ## Priority Going Forward diff --git a/docs/backend-assurance/README.md b/docs/backend-assurance/README.md index 43e8443..2439c6f 100644 --- a/docs/backend-assurance/README.md +++ b/docs/backend-assurance/README.md @@ -27,12 +27,11 @@ 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` | `prim__strAppend.md` | `elixir/test/backend_assurance/prim_str_append_test.exs` | | `prim__strSubstr` | `substrLengthBound` | `prim__strSubstr.md` | `elixir/test/backend_assurance/prim_str_substr_test.exs` | -Each row is delivered as one PR per primitive. `prim__eqChar` is the -first; the other three follow the same shape. +Each row is delivered as one PR per primitive. ## Constraints diff --git a/docs/backend-assurance/prim__strAppend.md b/docs/backend-assurance/prim__strAppend.md index 595dd1c..e3cdd3f 100644 --- a/docs/backend-assurance/prim__strAppend.md +++ b/docs/backend-assurance/prim__strAppend.md @@ -55,9 +55,10 @@ compile-time-only artefacts; the runtime strings flowing through the system are BEAM UTF-8 binaries. On BEAM: - **String model.** Elixir strings are UTF-8 encoded binaries. - `String.length/1` returns the **codepoint count** (not the byte - count) by scanning the UTF-8 boundaries. This matches Idris2's - `length`-on-`String` semantics on Chez (codepoint count). + Idris2's `length`-on-`String` semantics on Chez are codepoint + count. Elixir's `String.length/1` counts grapheme clusters, so the + BEAM-side harness measures codepoint count explicitly via + `String.codepoints/1`. - **Concatenation lowering.** Elixir's `<>` on binaries is the built-in `bif erlang:'++'/2` for iolists, ultimately compiling to a byte-level binary append. UTF-8 is prefix-free: appending two @@ -65,8 +66,8 @@ system are BEAM UTF-8 binaries. On BEAM: codepoint boundaries are exactly the boundaries of the operands. - **Length additivity.** Because UTF-8 is prefix-free, the codepoint boundaries of `s <> t` are exactly the boundaries of `s` followed - by the boundaries of `t`. Hence - `String.length(s <> t) == String.length(s) + String.length(t)`. + by the boundaries of `t`. Hence the codepoint count of `s <> t` + equals the codepoint count of `s` plus the codepoint count of `t`. The property test exercises this over random strings sampled from the legal codepoint range (excluding surrogates), plus explicit boundary @@ -75,14 +76,14 @@ the empty-string identity case. ## Why this isn't circular -The harness does not call `prim__strAppend`. It calls Elixir `<>` and -`String.length/1` directly on UTF-8 binaries. The argument is: *the -operation that Idris2 lowers `prim__strAppend` + `prim__strLength` to -on the BEAM is `<>` + `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. +The harness does not call `prim__strAppend`. It calls Elixir `<>` +directly on UTF-8 binaries and measures codepoint count explicitly. +The argument is: *BEAM binary concatenation preserves the exact +UTF-8 codepoint sequence of both operands*, so demonstrating that the +resulting codepoint count is additive validates the backend operation +at the semantic level the axiom uses. 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 @@ -126,7 +127,7 @@ byte length** — see the *Honest framing* clause in for `prim__strAppend` and `prim__strLength`. - R6RS §6.7, §11.12 — Scheme string model and `string-append` specification. -- Elixir `String` module documentation — UTF-8 codepoint counting via - `String.length/1`. +- Elixir `String` module documentation — UTF-8 codepoint enumeration + via `String.codepoints/1`. - `PROOF-NEEDS.md` — axiom audit (2026-05-18) and class-(J) framing. - `src/abi/Boj/SafetyLemmas.idr` — axiom declaration (line 226). diff --git a/docs/backend-assurance/prim__strSubstr.md b/docs/backend-assurance/prim__strSubstr.md index b2ee5e7..7e677ce 100644 --- a/docs/backend-assurance/prim__strSubstr.md +++ b/docs/backend-assurance/prim__strSubstr.md @@ -64,26 +64,28 @@ the R6RS guarantee for `substring` combined with the codegen's clamp. ## BEAM backend (Erlang / Elixir, where BoJ runs) BoJ's REST surface is Elixir on the BEAM. The runtime strings are -UTF-8 encoded binaries; substring extraction goes through Elixir's -`String.slice/3`. +UTF-8 encoded binaries; the BEAM-side harness models substring over +the decoded codepoint sequence (`String.to_charlist/1` + `Enum.slice/3` ++ `to_string/1`). On BEAM: - **String model.** As with `prim__strAppend`, 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.slice/3` semantics.** Per the Elixir `String` module - documentation, `String.slice(s, start, len)` returns at most `len` - codepoints from `s`, starting at codepoint offset `start`. The - function clamps to the string's actual codepoint length: when - `start ≥ length(s)`, the result is `""`; when `start + len > - length(s)`, the result is the suffix from `start` to the end (which - is strictly shorter than `len`). -- **Length bound.** Combining the two facts: - `String.length(String.slice(s, start, len)) ≤ len` for all - `(start, len, s)`. The clamp can only *shorten* the result; - it never extends past `len`. + binaries. The `length` referred to in the axiom is codepoint count, + matching Idris2 semantics on Chez. Elixir's `String.length/1` and + `String.slice/3` are grapheme-oriented, so the BEAM-side harness + uses explicit codepoint operations. +- **Codepoint-slice semantics.** The harness decodes `s` with + `String.to_charlist/1`, slices that codepoint list with + `Enum.slice(start, len)`, and re-encodes it with `to_string/1`. + This returns at most `len` codepoints from `s`, starting at + codepoint offset `start`. The slice clamps to the string's actual + codepoint length: when `start ≥ length(s)`, the result is `""`; + when `start + len > length(s)`, the result is the suffix from + `start` to the end (which is strictly shorter than `len`). +- **Length bound.** Combining the two facts: the codepoint count of + the codepoint slice is `≤ len` for all `(start, len, s)`. The clamp + can only *shorten* the result; it never extends past `len`. The property test exercises this over random `(start, len, s)` tuples plus explicit boundary cases: `len = 0`, `start ≥ length(s)`, @@ -93,12 +95,13 @@ where codepoint count differs from byte count. ## Why this isn't circular The harness does not call `prim__strSubstr`. It calls Elixir -`String.slice/3` and `String.length/1` directly. The argument is: -*the operation that Idris2 lowers `prim__strSubstr` to on the BEAM -is `String.slice/3` on a UTF-8 binary*, so demonstrating -`String.slice/3` satisfies 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. +charlist/codepoint operations directly. The argument is: *a +codepoint-level substring operation over a UTF-8 binary clamps to at +most the requested number of codepoints*, so demonstrating that +operation satisfies the property validates the backend semantics the +axiom uses. 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 — the R6RS `substring` semantics combined with the codegen's clamp are sufficient @@ -108,7 +111,7 @@ documentary evidence. - **`len = 0`.** The tight corner of the bound: result must be the empty string. R6RS `substring` with `end = start` returns `""`; - BEAM `String.slice/3` with `len = 0` returns `""`. Both satisfy + the BEAM codepoint slice with `len = 0` returns `""`. Both satisfy `LTE 0 0`. - **`start ≥ length(s)`** (start past end). Both backends clamp to the empty string; the bound `LTE 0 len` is trivial. @@ -120,9 +123,9 @@ documentary evidence. result is `s` itself; the bound is tight (`LTE length(s) length(s)`). - **Multi-byte codepoints.** Tested via boundary strings covering - ASCII, Latin-1 supplement, CJK, and astral plane. `String.slice/3` - counts codepoints, not bytes, so a slice of length `len` from an - emoji-heavy string spans `4 * len` bytes but `len` codepoints. + ASCII, Latin-1 supplement, CJK, and astral plane. The harness slices + codepoints, not bytes, so a slice of length `len` from an emoji-heavy + string spans up to `4 * len` bytes but at most `len` codepoints. - **Surrogates** (`0xD800..0xDFFF`): excluded from the codepoint generator. Same rationale as `prim__strAppend`. - **Negative `start` / `len`.** Idris2's `substr` takes `Nat`, so @@ -137,7 +140,7 @@ documentary evidence. - Idris2 0.8.0 `src/Compiler/Scheme/Chez.idr` — Chez codegen for `prim__strSubstr` (clamp + R6RS `substring`). - R6RS §11.12 — `substring` specification. -- Elixir `String` module documentation — `String.slice/3` clamp - semantics. +- 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 233). diff --git a/docs/backend-assurance/prim__strToCharList.md b/docs/backend-assurance/prim__strToCharList.md new file mode 100644 index 0000000..eda66fa --- /dev/null +++ b/docs/backend-assurance/prim__strToCharList.md @@ -0,0 +1,143 @@ +# 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. The `length` referred to in + the axiom is codepoint count, matching Idris2 semantics on Chez. + Elixir's `String.length/1` counts grapheme clusters, so the + BEAM-side harness measures codepoint count explicitly via + `String.codepoints/1`. +- **`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)) == length(String.codepoints(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 an explicit `String.codepoints/1` count +directly. The argument is: *BEAM charlist conversion decodes a UTF-8 +binary into the same codepoint sequence that Idris `String.length` +counts*, so demonstrating those operations agree validates the +backend operation at the semantic level the axiom uses. 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` + and `String.codepoints/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_append_test.exs b/elixir/test/backend_assurance/prim_str_append_test.exs index 2da6e88..cc501cd 100644 --- a/elixir/test/backend_assurance/prim_str_append_test.exs +++ b/elixir/test/backend_assurance/prim_str_append_test.exs @@ -19,10 +19,11 @@ # 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). Tests -# below use codepoint count, *not* byte count — the axiom is about -# logical-character length, not encoded-byte length. +# Idris2's `length` on `String` is codepoint count (Chez +# `string-length` on R6RS characters). Elixir's `String.length/1` +# counts grapheme clusters, so the BEAM harness uses explicit +# codepoint counts. The axiom is about logical-character/codepoint +# length, not grapheme-cluster or encoded-byte length. defmodule Boj.BackendAssurance.PrimStrAppendTest do use ExUnit.Case, async: true use ExUnitProperties @@ -45,17 +46,21 @@ defmodule Boj.BackendAssurance.PrimStrAppendTest do end) end + defp codepoint_count(s), do: s |> String.codepoints() |> length() + # ── Length additivity: |s <> t| = |s| + |t| ────────────────────────── # # Backs `appendLengthSum`. On BEAM, `<>` on UTF-8 binaries appends the # byte sequences; codepoint count of the result equals the sum of the # operand codepoint counts because UTF-8 encoding is prefix-free. property "BEAM <> is length-additive on codepoint count (appendLengthSum)" do - check all s <- legal_string(), - t <- legal_string() do - assert String.length(s <> t) == String.length(s) + String.length(t), + check all( + s <- legal_string(), + t <- legal_string() + ) do + assert codepoint_count(s <> t) == codepoint_count(s) + codepoint_count(t), "appendLengthSum violation: |#{inspect(s)} <> #{inspect(t)}| = " <> - "#{String.length(s <> t)}, expected #{String.length(s) + String.length(t)}" + "#{codepoint_count(s <> t)}, expected #{codepoint_count(s) + codepoint_count(t)}" end end @@ -65,16 +70,16 @@ defmodule Boj.BackendAssurance.PrimStrAppendTest do # worth pinning explicitly — a backend that special-cased empty-string # append (e.g. allocating a sentinel byte) would surface here. property "right identity: s <> \"\" = s (length and content)" do - check all s <- legal_string() do + check all(s <- legal_string()) do assert s <> "" == s - assert String.length(s <> "") == String.length(s) + assert codepoint_count(s <> "") == codepoint_count(s) end end property "left identity: \"\" <> s = s (length and content)" do - check all s <- legal_string() do + check all(s <- legal_string()) do assert "" <> s == s - assert String.length("" <> s) == String.length(s) + assert codepoint_count("" <> s) == codepoint_count(s) end end @@ -84,12 +89,18 @@ defmodule Boj.BackendAssurance.PrimStrAppendTest do # associative; BEAM `<>` is binary-concatenation-associative on the # byte level, which the codepoint count inherits. property "<> on codepoint count distributes over three-way append" do - check all s <- legal_string(), - t <- legal_string(), - u <- legal_string() do - assert String.length((s <> t) <> u) == String.length(s <> (t <> u)) - assert String.length((s <> t) <> u) == - String.length(s) + String.length(t) + String.length(u) + check all( + s <- legal_string(), + t <- legal_string(), + u <- legal_string() + ) do + left = (s <> t) <> u + right = s <> t <> u + + assert codepoint_count(left) == codepoint_count(right) + + assert codepoint_count(left) == + codepoint_count(s) + codepoint_count(t) + codepoint_count(u) end end @@ -114,12 +125,14 @@ defmodule Boj.BackendAssurance.PrimStrAppendTest do "\u{10000}", "\u{10FFFF}", "café", + "e\u0301", + "圮ੈ", "日本語", "🦀" ] for s <- boundaries, t <- boundaries do - assert String.length(s <> t) == String.length(s) + String.length(t), + assert codepoint_count(s <> t) == codepoint_count(s) + codepoint_count(t), "appendLengthSum boundary violation: #{inspect(s)} <> #{inspect(t)}" end end diff --git a/elixir/test/backend_assurance/prim_str_substr_test.exs b/elixir/test/backend_assurance/prim_str_substr_test.exs index 0827338..7bef7c8 100644 --- a/elixir/test/backend_assurance/prim_str_substr_test.exs +++ b/elixir/test/backend_assurance/prim_str_substr_test.exs @@ -3,8 +3,8 @@ # # Backend-assurance harness for `prim__strSubstr`. # -# Validates that BEAM substring extraction (`String.slice/3` over UTF-8 -# binaries) satisfies the length-bound axiom declared at: +# Validates that BEAM codepoint substring extraction over UTF-8 +# binaries satisfies the length-bound axiom declared at: # # src/abi/Boj/SafetyLemmas.idr:233 substrLengthBound : # (s : String) -> (start, len : Nat) -> @@ -20,8 +20,10 @@ # trusted base from "we trust the backend" to "we randomly tested the # operation against the property over N (start, len, s) tuples". # -# Length is codepoint count (`String.length/1`), matching Idris2's -# `prim__strLength` semantics on Chez (`string-length`). +# Length is codepoint count, matching Idris2's `prim__strLength` +# semantics on Chez (`string-length`). Elixir's `String.length/1` and +# `String.slice/3` are grapheme-oriented, so this harness uses +# explicit charlist/codepoint operations. defmodule Boj.BackendAssurance.PrimStrSubstrTest do use ExUnit.Case, async: true use ExUnitProperties @@ -41,18 +43,28 @@ defmodule Boj.BackendAssurance.PrimStrSubstrTest do end) end + defp codepoint_count(s), do: s |> String.codepoints() |> length() + + defp codepoint_slice(s, start, len) do + s + |> String.to_charlist() + |> Enum.slice(start, len) + |> to_string() + end + # ── Length bound: |substr(start, len, s)| ≤ len ────────────────────── # - # Backs `substrLengthBound`. On BEAM, `String.slice(s, start, len)` - # returns at most `len` codepoints starting at offset `start`, clamped - # to the string's actual length. The clamp means the result can be + # Backs `substrLengthBound`. On BEAM, the harness slices the decoded + # codepoint list and re-encodes it. The clamp means the result can be # shorter than `len` (when `start + len > length(s)` or `start ≥ # length(s)`), never longer. - property "BEAM String.slice respects the requested length bound (substrLengthBound)" do - check all s <- legal_string(), - start <- StreamData.integer(0..96), - len <- StreamData.integer(0..96) do - result_len = String.length(String.slice(s, start, len)) + property "BEAM codepoint slice respects the requested length bound (substrLengthBound)" do + check all( + s <- legal_string(), + start <- StreamData.integer(0..96), + len <- StreamData.integer(0..96) + ) do + result_len = codepoint_count(codepoint_slice(s, start, len)) assert result_len <= len, "substrLengthBound violation: substr(#{start}, #{len}, " <> @@ -66,9 +78,11 @@ defmodule Boj.BackendAssurance.PrimStrSubstrTest do # string (length 0 ≤ 0). A backend that returned at least one char # for `len = 0` would surface here. property "len = 0 always yields the empty string" do - check all s <- legal_string(), - start <- StreamData.integer(0..96) do - assert String.slice(s, start, 0) == "", + check all( + s <- legal_string(), + start <- StreamData.integer(0..96) + ) do + assert codepoint_slice(s, start, 0) == "", "substr(#{start}, 0, #{inspect(s)}) was not empty" end end @@ -78,10 +92,13 @@ defmodule Boj.BackendAssurance.PrimStrSubstrTest do # When `start ≥ length(s)`, the result is the empty string regardless # of `len`. This is the bound-clamp path through the backend. property "start ≥ length(s) yields the empty string" do - check all s <- legal_string(), - len <- StreamData.integer(0..96) do - start = String.length(s) + 5 - assert String.slice(s, start, len) == "", + check all( + s <- legal_string(), + len <- StreamData.integer(0..96) + ) do + start = codepoint_count(s) + 5 + + assert codepoint_slice(s, start, len) == "", "substr(#{start}, #{len}, #{inspect(s)}) past end was not empty" end end @@ -91,9 +108,9 @@ defmodule Boj.BackendAssurance.PrimStrSubstrTest do # When the bound matches the actual string length, the slice should # be the whole string. Anchors the upper edge of the bound. property "start = 0, len = length(s) returns the whole string" do - check all s <- legal_string() do - assert String.slice(s, 0, String.length(s)) == s - assert String.length(String.slice(s, 0, String.length(s))) == String.length(s) + check all(s <- legal_string()) do + assert codepoint_slice(s, 0, codepoint_count(s)) == s + assert codepoint_count(codepoint_slice(s, 0, codepoint_count(s))) == codepoint_count(s) end end @@ -107,6 +124,8 @@ defmodule Boj.BackendAssurance.PrimStrSubstrTest do "a", "abc", "café", + "e\u0301", + "圮ੈ", "日本語", "🦀🦀🦀", String.duplicate("x", 64) @@ -116,7 +135,7 @@ defmodule Boj.BackendAssurance.PrimStrSubstrTest do lens = [0, 1, 3, 8, 64, 1000] for s <- strings, start <- starts, len <- lens do - result_len = String.length(String.slice(s, start, len)) + result_len = codepoint_count(codepoint_slice(s, start, len)) assert result_len <= len, "substrLengthBound boundary: substr(#{start}, #{len}, " <> 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..ec9440e --- /dev/null +++ b/elixir/test/backend_assurance/prim_str_to_char_list_test.exs @@ -0,0 +1,147 @@ +# 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). Elixir's `String.length/1` +# counts grapheme clusters, so the BEAM harness uses explicit +# codepoint counts. The axiom is about logical-character/codepoint +# length, not grapheme-cluster or 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 + + defp codepoint_count(s), do: s |> String.codepoints() |> length() + + # ── 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. This intentionally compares against + # `String.codepoints/1`, not `String.length/1`, because Elixir's + # public length API counts grapheme clusters. + property "BEAM String.to_charlist/1 preserves codepoint count (unpackLength)" do + check all(s <- legal_string()) do + assert length(String.to_charlist(s)) == codepoint_count(s), + "unpackLength violation: |to_charlist(#{inspect(s)})| = " <> + "#{length(String.to_charlist(s))}, expected #{codepoint_count(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 codepoint_count("") == 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é", + "e\u0301", + "圮ੈ", + "日本語", + "🦀" + ] + + for s <- boundaries do + assert length(String.to_charlist(s)) == codepoint_count(s), + "unpackLength boundary violation: " <> + "|to_charlist(#{inspect(s)})| = #{length(String.to_charlist(s))}, " <> + "expected #{codepoint_count(s)}" + + assert s |> String.to_charlist() |> to_string() == s, + "round-trip boundary violation: #{inspect(s)}" + end + end +end