|
| 1 | +# Backend-Assurance: `prim__eqChar` |
| 2 | + |
| 3 | +Trusted-extraction validation for the two class-(J) axioms over |
| 4 | +Idris2's `prim__eqChar` primitive: |
| 5 | + |
| 6 | +- `charEqSound : (c1, c2 : Char) -> c1 == c2 = True -> c1 = c2` |
| 7 | + (`src/abi/Boj/SafetyLemmas.idr:53`) |
| 8 | +- `charEqSym : (x, y : Char) -> (x == y) = (y == x)` |
| 9 | + (`src/abi/Boj/SafetyLemmas.idr:60`) |
| 10 | + |
| 11 | +Both are `%unsafe` `believe_me` declarations in Idris2 0.8.0 because |
| 12 | +`Char` is an opaque primitive type with no in-language induction |
| 13 | +principle. This document argues — by inspecting the backend lowerings |
| 14 | +that BoJ actually ships against — that the believed properties hold. |
| 15 | + |
| 16 | +The companion property test |
| 17 | +(`elixir/test/backend_assurance/prim_eq_char_test.exs`) exercises the |
| 18 | +BEAM half of this argument over the codepoint space. |
| 19 | + |
| 20 | +## What `prim__eqChar` is |
| 21 | + |
| 22 | +`prim__eqChar : Char -> Char -> Int` is a primitive arithmetic |
| 23 | +operation declared in `Core.Primitives` in the Idris2 compiler. The |
| 24 | +`==` method on `Char` calls it via the `Eq Char` instance in |
| 25 | +`Prelude.EqOrd`: |
| 26 | + |
| 27 | + public export |
| 28 | + Eq Char where |
| 29 | + x == y = boolOp prim__eqChar x y |
| 30 | + x /= y = not (x == y) |
| 31 | + |
| 32 | +so the question reduces to: does `prim__eqChar` satisfy soundness and |
| 33 | +symmetry on each shipping backend? |
| 34 | + |
| 35 | +## Chez Scheme backend (Idris2 default codegen) |
| 36 | + |
| 37 | +In `Compiler.Scheme.Chez`, `prim__eqChar` is one of the arithmetic |
| 38 | +primitives lowered directly to the R6RS predicate `char=?` (via the |
| 39 | +generic `op` translation table that maps `EQ CharType` to |
| 40 | +`char=?`). On Chez 9.x: |
| 41 | + |
| 42 | +- **Soundness.** R6RS §11.11 specifies `char=?` returns `#t` iff its |
| 43 | + arguments denote the same Unicode codepoint. The Char value is the |
| 44 | + codepoint; two Chars for which `char=?` returns `#t` are the same |
| 45 | + value. Hence `c1 == c2 = True -> c1 = c2` holds. |
| 46 | +- **Symmetry.** R6RS §11.11 specifies `char=?` is a total |
| 47 | + equivalence relation. Symmetry is part of "equivalence relation"; |
| 48 | + hence `(x == y) = (y == x)` holds. |
| 49 | + |
| 50 | +Both properties are part of the Scheme standard and are upheld by the |
| 51 | +Chez implementation. No further evidence needed beyond citing the |
| 52 | +standard. |
| 53 | + |
| 54 | +## BEAM backend (Erlang / Elixir, where BoJ runs) |
| 55 | + |
| 56 | +BoJ's REST surface is Elixir on the BEAM. The Idris2 proofs are |
| 57 | +compile-time-only artefacts; the runtime characters that flow through |
| 58 | +the system are BEAM codepoints (Erlang integers in the range |
| 59 | +`0..0x10FFFF` excluding the surrogate gap `0xD800..0xDFFF`). On BEAM: |
| 60 | + |
| 61 | +- **Char encoding.** Erlang represents a character as an |
| 62 | + integer codepoint. Strings are either lists-of-integers ("traditional" |
| 63 | + Erlang strings) or UTF-8 binaries — but the per-character equality |
| 64 | + operation that matters for the axioms is integer equality on |
| 65 | + codepoints. |
| 66 | +- **Lowering of `==`.** Integer equality on the BEAM is `=:=` |
| 67 | + (the strict-equality operator). It returns `true` iff both |
| 68 | + operands are the same term; for two integer codepoints `a` and `b` |
| 69 | + this is exactly value equality. |
| 70 | +- **Soundness.** `a =:= b = true` implies `a` and `b` are the same |
| 71 | + integer codepoint, hence the same `Char`. Trivially. |
| 72 | +- **Symmetry.** `=:=` is documented in OTP `erlang(3)` as a total |
| 73 | + commutative operator on terms; for any `a`, `b`, `a =:= b` ⟺ |
| 74 | + `b =:= a`. |
| 75 | + |
| 76 | +The property test exercises both properties over random codepoints |
| 77 | +sampled from the legal range (excluding surrogates), plus explicit |
| 78 | +boundary codepoints (`0`, ASCII boundary `0x7F`, BMP boundaries |
| 79 | +`0xD7FF`/`0xE000`, BMP/astral boundary `0xFFFF`/`0x10000`, max |
| 80 | +`0x10FFFF`). |
| 81 | + |
| 82 | +## Why this isn't circular |
| 83 | + |
| 84 | +The harness does not call `prim__eqChar`. It calls Erlang `=:=` |
| 85 | +directly on integers. The argument is: *the operation that Idris2 |
| 86 | +lowers `prim__eqChar` to on the BEAM is `=:=` on the codepoint |
| 87 | +integer*, so demonstrating `=:=` satisfies the properties is |
| 88 | +sufficient. The trusted-extraction step is reading the lowering; the |
| 89 | +property-test step is verifying the operation behaves as the lowering |
| 90 | +claims. |
| 91 | + |
| 92 | +For Chez, we do not run a Scheme harness — R6RS is sufficient |
| 93 | +documentary evidence that `char=?` is a total equivalence relation. If |
| 94 | +BoJ ever ships a backend whose Char equality is not a built-in |
| 95 | +equivalence-checked primitive, this document gets a new section and a |
| 96 | +matching property test. |
| 97 | + |
| 98 | +## Edge cases considered |
| 99 | + |
| 100 | +- **Surrogates** (`0xD800..0xDFFF`): excluded from the codepoint |
| 101 | + generator. These are illegal as standalone Char values per Unicode; |
| 102 | + if the test layer ever needs to assert behaviour on them, that is a |
| 103 | + bug in the system under test, not in `prim__eqChar`. |
| 104 | +- **Normalisation** (`é` as one codepoint vs two): not in scope. The |
| 105 | + axiom is about codepoint equality, not grapheme-cluster equality. |
| 106 | + `prim__eqChar` is per-codepoint; `é` (`U+00E9`) and `e` (`U+0065`) + |
| 107 | + combining acute (`U+0301`) are *correctly* different chars under the |
| 108 | + axiom. |
| 109 | +- **Case folding.** Not in scope; `prim__eqChar` is case-sensitive by |
| 110 | + spec, and the property-test `distinct codepoints are not =:=` |
| 111 | + invariant guards against a backend slipping case-insensitive |
| 112 | + collation into char equality. |
| 113 | + |
| 114 | +## References |
| 115 | + |
| 116 | +- Idris2 0.8.0 `src/Core/Primitives.idr` — primitive operation table. |
| 117 | +- Idris2 0.8.0 `src/Compiler/Scheme/Chez.idr` — Chez codegen lowerings. |
| 118 | +- R6RS §11.11 "Characters" — `char=?` specification. |
| 119 | +- OTP `erlang(3)` — `=:=`/`=/=` specification. |
| 120 | +- `PROOF-NEEDS.md` — axiom audit (2026-05-18). |
| 121 | +- `src/abi/Boj/SafetyLemmas.idr` — axiom declarations (lines 53, 60). |
0 commit comments