String Operations v1
September 10, 2026 · View on GitHub
Audience: language users, tool authors, and compiler contributors.
Status: implemented in this tranche. Three prelude-style intrinsic functions
admitted wherever owned string values are already admitted.
Operations
| Source name | Reserved stable identity | Signature | Argument ownership |
|---|---|---|---|
string_len | core.string.len | (s: string) -> i64 | borrowed read |
string_concat | core.string.concat | (a: string, b: string) -> string | both consumed by move |
string_is_empty | core.string.is_empty | (s: string) -> bool | borrowed read |
Length is the UTF-8 byte length on every backend; string_is_empty(s) is
exactly string_len(s) == 0.
Admission shape
Free-function intrinsics with compiler-reserved identities were chosen over the two alternatives:
- Method-call syntax (
s.len()) would require primitive-receiver dispatch in the verifier, resolver, validator, cleanup planner, graph projection, and both backends. Method calls currently require class receivers only. - Prelude declarations (like the compiler-owned
Option/Resultvariants) would change every program's revision digest because the Graph binds the whole prelude contract unconditionally, breaking pinned digests for programs that never use strings.
Instead, a call to one of the three reserved names resolves to an ordinary
monomorphic [hir::ResolvedExprKind::Call] whose callee carries the reserved
core.string.* identity. Consequences:
- Parser, canonical formatter, and graph JSON need no new syntax or node
kinds; intrinsic calls project as ordinary
"call"nodes bound to their reserved identity, so projections stay deterministic and programs that never name the operations keep byte-identical output (verified against the base revision: identical revision digest and identical Graph JSON bytes). - No new diagnostic codes were needed. Intrinsic calls verify through the
ordinary monomorphic call machinery with synthetic signatures, so they reuse
the established families exactly:
SPX-T204(arity),SPX-T205(argument type),SPX-T225(type arguments),SPX-S113(reserved name),SPX-H006(HIR invariant failures including resolved use-after-move). - The names are compiler-reserved: declaring a function named
string_len,string_concat, orstring_is_emptyis rejected withSPX-S113, mirroring how prelude type names are protected.
Ownership
Consumption mirrors existing String move-checking exactly:
string_concatarguments use the same syntheticownparameter shape as an ordinary declaredstringparameter, so the shared transfer machinery marks them moved. A later use of a consumed argument is a compile-time diagnostic (resolved value ... used after it was moved,SPX-H006), never a backend accident.string_len/string_is_emptyuse non-transferring parameters, so reads leave the operand available.
Backends
- Native C11: gated runtime helpers (
spx_string_len,spx_string_concat,spx_string_is_empty) appended after the string runtime only when a program reaches the operations, so existing projections keep their exact committed bytes. Consuming operations free their input buffers exactly at the operation site, like owned string equality. - Wasm32: two optional host imports (
spx_string_len,spx_string_concat) appended after the base string imports only when used;is_emptylowers aslen+i64.eqz. Modules for programs without the operations keep their exact bytes. - Interpreter: intrinsic calls evaluate inside the scalar profile with the same byte semantics; user functions taking strings remain outside the profile exactly as before.
The separately selected Internal String Interpreter v1
adds implemented internal String-call regression evidence behind unchanged external
scalar/borrowed inputs and scalar results. Its distinct command/report does
not widen ordinary interpret or any Project execution profile.
Evidence
The later native inline String settlement correction adds hosted-green release failure-path allocation evidence for ordinary C11 and stdout-transcript execution. It intentionally changes String-bearing native function bodies while preserving intrinsic signatures and diagnostics. It is complemented by the authored native String contents correction, which preserves embedded NUL through all ordinary/native stdout operations. Both native corrections have hosted-green release evidence. Ordinary Wasm String drop remains a distinct profile requirement; the value fixtures below are not themselves physical settlement evidence.
The explicit Standalone Wasm Internal String Settlement v1 adds hosted-green release compiler/host ownership evidence without changing ordinary Wasm imports or package admission. Its bounded capacity outcomes and absorbing unexpected-failure state are separate from language failures.
tests/language/string_ops_v1.rs proves canonical round-trip, deterministic graph JSON
with pinned fragments, HIR binding to the reserved identities, stable
diagnostics (type error, arity, shadowing, use-after-move), borrowed-read
non-movement, interpreter agreement, native C11 O0/O2 execution equality, Node
Wasm execution equality, and the byte-gating of helpers/imports for programs
that do not use the operations. examples/string_ops.spx is the canonical
committed example exercised by the examples suite.
String operations breadth v2 (2026-08-24)
Status: implemented in the feat/string-ops-breadth-v2 tranche. Four more
prelude-style intrinsics extend the same admission shape; everything above is
unchanged.
Operations
| Source name | Reserved stable identity | Signature | Argument ownership |
|---|---|---|---|
string_starts_with | core.string.starts_with | (s: string, prefix: string) -> bool | both borrowed reads |
string_contains | core.string.contains | (s: string, needle: string) -> bool | both borrowed reads |
string_len_chars | core.string.len_chars | (s: string) -> i64 | borrowed read |
string_from_char | core.string.from_char | (c: char) -> string | copied scalar, no transfer |
string_len_chars counts Unicode scalar values, so "héllo" has a char
length of 5 while its UTF-8 byte length (string_len) is 6 on every backend.
An empty needle/prefix follows the ordinary substring convention: every string
starts with and contains the empty string.
Why string_char_at did not land
A character-indexing operation (string_char_at(s, index) -> char) was part
of the planned wave but is not admitted. Its negative/out-of-bounds story has
no home: the compiler's normalized runtime failure lattice carries exactly two
classes today (semaprax.contract.v1, semaprax.arithmetic.v1; see the
OpenAPI status schema and the native status runtime), with no range/bounds
class, and inventing one would require editing the shared failure machinery
far beyond the additive intrinsic-table seams this wave committed to. The
contingency named in the plan applies: Option<char> is not an alternative
because char payloads are not admitted inside Option. string_len_chars
lands instead as the third borrowed read, and indexing stays out of scope
along with slicing and mutation.
Admission and gating
Same architecture as v1: reserved names resolve through the synthetic
signatures into ordinary monomorphic calls bound to their core.string.*
identities; parser, canonical formatter, resolver/HIR, verifier, semantic
graph, cleanup planning/replay, interpreter, and both backends consume the
extended table without new node kinds or diagnostic codes. The only table
extension beyond name/id/arity bookkeeping is per-parameter expected types:
resolved_params, ast_params, and the two HIR argument checks now consult
StringOp::param_types() so string_from_char admits exactly one char.
Backends gate breadth-v2 lowering as one separate group:
- Native C11 appends
NATIVE_STRING_OPS_V2_RUNTIME_C(helpersspx_string_starts_with,spx_string_contains,spx_string_len_chars,spx_string_from_char) only when a program reaches a v2 call. Borrowed operations free their staged input buffers at the operation site exactly like the first-wave reads;string_from_charallocates one fresh owned buffer from the scalar's UTF-8 encoding and consumes nothing. - Wasm32 emits four host imports as one group directly after any first-wave imports (deterministic gap-free indexes computed from which groups are present). First-wave-only programs keep byte-identical modules, and programs without any operations keep byte-identical output on both backends.
- Interpreter evaluates all four inside the scalar profile with identical
semantics (
chars().count()for scalar counting).
Evidence
tests/language/string_ops_v2.rs proves canonical round-trip, deterministic graph JSON
with pinned fragments for the four new identities (and their absence for
first-wave-only and operation-free programs), HIR binding with ownership
modes, stable diagnostics (argument type including the char parameter,
arity for one- and two-argument forms, reserved-name shadowing,
use-after-move behind a borrowed read), borrow non-movement, interpreter
agreement, native C11 O0/O2 execution equality over ASCII, empty strings,
whole-value prefixes, and 1–4-byte scalar content, Node/Wasm execution
equality, and the group-gating byte guarantees. examples/string_ops_v2.spx
is the canonical committed example exercised by the examples suite.
Canonical numeric text v1 (2026-09-05)
Status: locally evidenced additive implementation.
Two compiler-owned conversions remove the need for handwritten digit tables:
| Source name | Reserved stable identity | Signature | Result |
|---|---|---|---|
string_from_i64 | core.string.from_i64 | (value: i64) -> string | canonical base-10 signed text |
string_from_usize | core.string.from_usize | (value: usize) -> string | canonical base-10 unsigned text |
There are no leading zeroes. Zero is "0"; negative i64 values carry one
leading ASCII -; every i64 and every semantic 64-bit usize value is
representable. Both parameters are copied scalars and each result is one fresh
owned UTF-8 string. The operations are infallible within the existing bounded
runtime allocation contract and introduce no effect or ambient authority.
They use the same reserved-call admission, diagnostics, deterministic graph projection, and cleanup rules as the earlier operations. Native C11 adds two reachability-gated helpers, and Core Wasm adds a separate two-import group after the earlier string-operation groups. Programs that do not use numeric text, including every earlier v1/v2 string fixture, keep their generated bytes. The reference interpreter renders the same decimal spelling directly.
tests/language/string_numeric_text.rs covers canonical round-trip, graph and
HIR identities, exact type and reserved-name diagnostics, interpreter results,
native execution, Wasm validation and Node execution, maximum usize, negative
i64, and helper/import gating. This is focused local evidence; it does not
promote the broader cross-backend or standard-library completion rows.