|
| 1 | +# Backend-Assurance: `prim__strAppend` |
| 2 | + |
| 3 | +Trusted-extraction validation for the class-(J) axiom over Idris2's |
| 4 | +`prim__strAppend` primitive: |
| 5 | + |
| 6 | +- `appendLengthSum : (s, t : String) -> length (s ++ t) = length s + length t` |
| 7 | + (`src/abi/Boj/SafetyLemmas.idr:226`) |
| 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. This document argues — by inspecting |
| 12 | +the backend lowerings that BoJ actually ships against — that the |
| 13 | +length-additivity property holds. |
| 14 | + |
| 15 | +The companion property test |
| 16 | +(`elixir/test/backend_assurance/prim_str_append_test.exs`) exercises |
| 17 | +the BEAM half of this argument over the codepoint space. |
| 18 | + |
| 19 | +## What `prim__strAppend` is |
| 20 | + |
| 21 | +`prim__strAppend : String -> String -> String` is a primitive |
| 22 | +arithmetic operation declared in Idris2's `Core.Primitives`. The |
| 23 | +`++` operator on `String` is the `Semigroup String` instance, which |
| 24 | +is `prim__strAppend` directly. Length is `prim__strLength` (the |
| 25 | +`length : String -> Nat` definition in `Data.String`). |
| 26 | + |
| 27 | +The question reduces to: does the operation `prim__strAppend` followed |
| 28 | +by `prim__strLength` satisfy `|prim__strAppend(s, t)| = |s| + |t|` on |
| 29 | +each shipping backend? Both `length` and `++` agree on a single notion |
| 30 | +of "character count" — what that notion is depends on the backend. |
| 31 | + |
| 32 | +## Chez Scheme backend (Idris2 default codegen) |
| 33 | + |
| 34 | +In `Compiler.Scheme.Chez`, `prim__strAppend` lowers to the R6RS |
| 35 | +procedure `string-append`, and `prim__strLength` lowers to |
| 36 | +`string-length`. On Chez 9.x: |
| 37 | + |
| 38 | +- **String model.** R6RS §6.7 specifies that a Scheme string is a |
| 39 | + sequence of Unicode characters (codepoints), not a byte sequence. |
| 40 | + `string-length` returns the number of characters. |
| 41 | +- **`string-append` semantics.** R6RS §11.12 specifies `string-append` |
| 42 | + returns a newly-allocated string whose characters are the |
| 43 | + concatenation, in order, of the characters of the argument strings. |
| 44 | +- **Length additivity.** Combining the two: the number of characters |
| 45 | + in `(string-append s t)` equals the number of characters in `s` |
| 46 | + plus the number of characters in `t`. This is part of the Scheme |
| 47 | + standard, not an implementation detail. |
| 48 | + |
| 49 | +No further evidence needed beyond citing the standard. |
| 50 | + |
| 51 | +## BEAM backend (Erlang / Elixir, where BoJ runs) |
| 52 | + |
| 53 | +BoJ's REST surface is Elixir on the BEAM. The Idris2 proofs are |
| 54 | +compile-time-only artefacts; the runtime strings flowing through the |
| 55 | +system are BEAM UTF-8 binaries. On BEAM: |
| 56 | + |
| 57 | +- **String model.** Elixir strings are UTF-8 encoded binaries. |
| 58 | + Idris2's `length`-on-`String` semantics on Chez are codepoint |
| 59 | + count. Elixir's `String.length/1` counts grapheme clusters, so the |
| 60 | + BEAM-side harness measures codepoint count explicitly via |
| 61 | + `String.codepoints/1`. |
| 62 | +- **Concatenation lowering.** Elixir's `<>` on binaries is the |
| 63 | + built-in `bif erlang:'++'/2` for iolists, ultimately compiling to |
| 64 | + a byte-level binary append. UTF-8 is prefix-free: appending two |
| 65 | + valid UTF-8 byte sequences yields a valid UTF-8 byte sequence whose |
| 66 | + codepoint boundaries are exactly the boundaries of the operands. |
| 67 | +- **Length additivity.** Because UTF-8 is prefix-free, the codepoint |
| 68 | + boundaries of `s <> t` are exactly the boundaries of `s` followed |
| 69 | + by the boundaries of `t`. Hence the codepoint count of `s <> t` |
| 70 | + equals the codepoint count of `s` plus the codepoint count of `t`. |
| 71 | + |
| 72 | +The property test exercises this over random strings sampled from the |
| 73 | +legal codepoint range (excluding surrogates), plus explicit boundary |
| 74 | +strings spanning all four UTF-8 encoding widths (1/2/3/4 bytes) and |
| 75 | +the empty-string identity case. |
| 76 | + |
| 77 | +## Why this isn't circular |
| 78 | + |
| 79 | +The harness does not call `prim__strAppend`. It calls Elixir `<>` |
| 80 | +directly on UTF-8 binaries and measures codepoint count explicitly. |
| 81 | +The argument is: *BEAM binary concatenation preserves the exact |
| 82 | +UTF-8 codepoint sequence of both operands*, so demonstrating that the |
| 83 | +resulting codepoint count is additive validates the backend operation |
| 84 | +at the semantic level the axiom uses. The trusted-extraction step is |
| 85 | +reading the lowering; the property-test step is verifying the |
| 86 | +operation behaves as the lowering claims. |
| 87 | + |
| 88 | +For Chez, we do not run a Scheme harness — R6RS is sufficient |
| 89 | +documentary evidence. If BoJ ever ships a backend whose string model |
| 90 | +is not Unicode codepoints (e.g. a byte-oriented C backend without |
| 91 | +UTF-8 awareness), this document gets a new section and a matching |
| 92 | +property test, **and the axiom may need to be restated in terms of |
| 93 | +byte length** — see the *Honest framing* clause in |
| 94 | +`docs/backend-assurance/README.md`. |
| 95 | + |
| 96 | +## Edge cases considered |
| 97 | + |
| 98 | +- **Empty strings.** `s <> "" = s` and `"" <> s = s` are tested |
| 99 | + explicitly. Length additivity reduces to `|s| + 0 = |s|` and |
| 100 | + `0 + |s| = |s|` respectively — corner cases of the main property |
| 101 | + but worth pinning to catch a backend that allocates a sentinel byte |
| 102 | + on empty append. |
| 103 | +- **Multi-byte codepoints.** Tested via boundary strings covering |
| 104 | + all four UTF-8 widths: ASCII (1 byte), Latin-1 supplement (2 bytes, |
| 105 | + e.g. `café`), CJK (3 bytes, e.g. `日本語`), and astral plane |
| 106 | + (4 bytes, e.g. `🦀`). Each width has a different number of bytes |
| 107 | + per codepoint, but the codepoint count is invariant. |
| 108 | +- **Surrogates** (`0xD800..0xDFFF`): excluded from the codepoint |
| 109 | + generator. These are illegal as standalone codepoints in |
| 110 | + well-formed Unicode; their presence would indicate a system-under- |
| 111 | + test bug, not a `prim__strAppend` failure. |
| 112 | +- **Normalisation.** Out of scope. `prim__strAppend` is byte-level |
| 113 | + (per UTF-8 prefix-free property) and does not compose canonical |
| 114 | + decompositions. A grapheme that is `e` + combining acute (two |
| 115 | + codepoints) appended to nothing remains two codepoints, regardless |
| 116 | + of whether the precomposed `é` (one codepoint) would canonically |
| 117 | + equal it. |
| 118 | +- **Three-way associativity.** Not in the axiom but cheap to assert. |
| 119 | + Length of `(s <> t) <> u` equals length of `s <> (t <> u)` equals |
| 120 | + `|s| + |t| + |u|`. Catches a backend whose concatenation |
| 121 | + associates differently on length than on byte order. |
| 122 | + |
| 123 | +## References |
| 124 | + |
| 125 | +- Idris2 0.8.0 `src/Core/Primitives.idr` — primitive operation table. |
| 126 | +- Idris2 0.8.0 `src/Compiler/Scheme/Chez.idr` — Chez codegen lowerings |
| 127 | + for `prim__strAppend` and `prim__strLength`. |
| 128 | +- R6RS §6.7, §11.12 — Scheme string model and `string-append` |
| 129 | + specification. |
| 130 | +- Elixir `String` module documentation — UTF-8 codepoint enumeration |
| 131 | + via `String.codepoints/1`. |
| 132 | +- `PROOF-NEEDS.md` — axiom audit (2026-05-18) and class-(J) framing. |
| 133 | +- `src/abi/Boj/SafetyLemmas.idr` — axiom declaration (line 226). |
0 commit comments