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 nameReserved stable identitySignatureArgument ownership
string_lencore.string.len(s: string) -> i64borrowed read
string_concatcore.string.concat(a: string, b: string) -> stringboth consumed by move
string_is_emptycore.string.is_empty(s: string) -> boolborrowed 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/Result variants) 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, or string_is_empty is rejected with SPX-S113, mirroring how prelude type names are protected.

Ownership

Consumption mirrors existing String move-checking exactly:

  • string_concat arguments use the same synthetic own parameter shape as an ordinary declared string parameter, 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_empty use 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_empty lowers as len + 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 nameReserved stable identitySignatureArgument ownership
string_starts_withcore.string.starts_with(s: string, prefix: string) -> boolboth borrowed reads
string_containscore.string.contains(s: string, needle: string) -> boolboth borrowed reads
string_len_charscore.string.len_chars(s: string) -> i64borrowed read
string_from_charcore.string.from_char(c: char) -> stringcopied 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 (helpers spx_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_char allocates 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 nameReserved stable identitySignatureResult
string_from_i64core.string.from_i64(value: i64) -> stringcanonical base-10 signed text
string_from_usizecore.string.from_usize(value: usize) -> stringcanonical 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.