Pinning the Semantics a Six-Target Compiler Silently Inherits: String Units, Sized and Trapping Integers, Total Division, Iteration Order and Injective Mangling

Pitch

When one IR feeds six host languages, every unspecified detail (what a string's length counts, what happens at integer overflow, how a map is iterated, whether two identifiers can collapse into one) is silently decided six different ways, and each time revl decided it once, wrote the choice down, and turned it into a probe that runs on every tier.

Abstract

A compiler that emits Python, TypeScript, Go, Rust, Java and WebAssembly from one typed IR inherits, for every operation the specification leaves open, six host-language answers. We report on a series of decisions in revl that closed such gaps, in each case the same way: measure what each tier actually computes on a separating input, choose one meaning by an argument from the language's own rules, make the frontend mark the information the backends lacked, add an execution probe on every tier that can run it, and document the closure so it cannot regress. The cases are: the unit of a string (code points; "😀".length() was 1, 2, 4 or a rejected literal depending on the tier), Int as 64-bit with trapping overflow on all six tiers (a measured cost of about 9% on a dependent scalar chain, with an Int32 type for kernels that are about 34% faster), division named by rounding rule with a Result-returning total form, canonical sorted-key map iteration, an implicit Int-to-Float coercion marked on the IR, and reserved-word mangling that was not injective (lambda and lambda_ collided, so Python returned a different value than the other five tiers). We list the divergences found, which were not found by the specification but by execution, and the three ways the checks themselves were found to be switched off in CI. We are explicit about what is not closed: arbitrary-precision Integer is a proposal, WebAssembly still refuses Float, maps and non-integer float rendering, and the cost figures come from single measurements stated in prose.

Problem and claim

Cross-target agreement is usually argued from the emitters: if every backend accepts a construct, the construct is portable. revl's own errata say why that fails: "tests/test_cross_tier.py checks that every emitter accepts a construct, which catches a tier that refuses and cannot catch a tier that accepts and then means something else" (docs/contract-errata.md:271-274). The failures that mattered were silent: a value that differs, not a build that breaks.

The claim of this paper is a procedure and its history, not a theory. Cross-target divergence appears first in decisions nobody wrote down. Deciding each once, giving the backends the missing information through the IR (for example operands on arithmetic nodes, "widen": "Float" on coercion sites), and attaching a probe that executes on each tier converts a silent divergence into either agreement, a named refusal, or a failing test. The docs also give the cost of each decision where it was measured.

The scope is deliberately limited to what the tree shows. Several decisions are only partly landed, and some documentation is stale; both are noted below instead of smoothed over.

Contributions

1. A decision write-up for five families, each with the measured pre-fix divergence table, the chosen meaning and the argument: string unit (docs/strings.md:99-135), integer width and overflow (docs/arithmetic.md:213-245), division and remainder conventions (docs/arithmetic.md:31-82), map iteration order (docs/collections.md:85-129), and identifier mangling (docs/v2.0-roadmap.md:1584).
2. The pattern "frontend marks, backends emit": operands on bin nodes for / and %, and "widen": "Float" on coercion sites, both additive with no ir_version bump (docs/arithmetic.md:377-412; operands defined at :172 and :355).
3. A counterexample to cross-tier equivalence of a different kind: non-injective keyword mangling, where Python silently returned a different value than the other five tiers. The roadmap notes that an injectivity assertion failed on the pristine self-host tree; this is not reproduced in the tree.
4. Cost figures stated in the docs (single prose measurements, not reproduced in the tree): about 9% for 64-bit trapping Int on a scalar chain (0.98 to 1.07 ns/iter), and about 34% for an Int32 vectorisable loop.
5. A baseline discipline for known divergences: pinned current behaviour that fails both when it worsens and when it starts passing (tests/test_cross_tier_execution.py:740-745, :930-940).
6. An honest ledger of what escaped: probes sitting behind an environment variable nothing sets, a skipped TypeScript column, a doc that called a defective tier "already correct".

Related work

Evidence on main

Numbers that exist

• Int overflow check: 0.98 to 1.07 ns/iter on a dependent scalar chain, "about 9%" (docs/arithmetic.md:222-228). One measurement, no n, no machine stated.
• Int32 vectorisable loop "~34% faster than i64" (docs/arithmetic.md:414-420). Stated twice (also docs/int32-proposal.md:15), no harness or raw values.
• String probe: "😀" is 1 code point, 2 UTF-16 units, 4 UTF-8 bytes (docs/strings.md:29-31); the pre-fix per-tier values are a six-cell table (docs/strings.md:37-47).
• Pairing law: 8 (trunc/rem) plus 8 (euclid/mod) sign-combination assertions per tier (tests/test_cross_tier_execution.py:1409-1418).
• Mangling: the roadmap names five fixed emitters and five self-host emitters (docs/v2.0-roadmap.md:1584,1687).
• No count of how many silent divergences the decisions closed in total exists in one place. The "Semantic divergences (closed...)" section (docs/contract-errata.md:203 onward) lists them individually.

Paper outline

1. Introduction: the emoji-length table as the opening example; why accept-only checks pass.
2. Method: measure, choose, mark in the IR, probe, document. The DIVERGENCES baseline discipline.
3. Five decisions in turn: strings (unit and ordering and bounds), integers (width, trap, literal range, Int32, Int.MIN edges), division and remainder (names, pairing law, total forms), iteration order, mangling injectivity.
4. Costs: the two measurements and what they do and do not show; the Wasm tier's refusals as a cost in coverage.
5. How the checks failed: the env var nothing set, the skipped TypeScript column, the "already correct" Java claim.
6. Related work and lessons.

Threats to validity and limits

• Costs are single measurements stated in prose. The docs themselves say the check "is much worse" on vectorisable reductions and give no figure for that case (docs/arithmetic.md:225-228).
• One language, one team: the decisions are argued from revl's own rule that "syntax revl shares with TypeScript means what TypeScript means" (docs/arithmetic.md:10-12). A reader may reject that rule; the code-point choice in particular departs from the JS prior and is justified by internal consistency with split.
• Wasm is an incomplete participant. It refuses Float values, maps, Int / Int, string ordering and repeat by name (docs/arithmetic.md:582-590, docs/collections.md:131-150, tests/test_458_str_ordering.py:262). Cross-tier agreement on those is vacuous for Wasm, and non-integer float rendering still traps at runtime there (docs/strings.md:340-376).
• Java columns are often read from emitter source; execution of rust and java sits behind REVL_CROSS_TIER_SLOW, which docs/contract-errata.md:276-300 notes was unset in CI until later fixed.
• NaN != NaN makes IEEE == non-reflexive, which the docs call "a caveat on the spec's wording", and it produces a Java HashMap/ArrayList anomaly described in docs/contract-errata.md:241-262. The pinned semantics are therefore not an equivalence relation on Float.
• Arbitrary-precision Integer is design-only; Float-to-string for exponent forms on Wasm is fenced; none of this paper claims otherwise.
• The agreement theorem models only three axes (numeric default, string unit, map order) and states what is outside it; this paper does not claim it covers the full set of decisions.

Fact-check

Claims in this draft were checked against revl main at commit 45bec431f: 28 checked, 6 corrected.

Cite this draft

@misc{revlp50,
  author       = {Thomas Moussajee},
  title        = {Pinning the Semantics a Six-Target Compiler Silently Inherits: String Units, Sized and Trapping Integers, Total Division, Iteration Order and Injective Mangling},
  year         = {2026},
  howpublished = {\url{https://inso1337.github.io/revl/research/P50.html}},
  note         = {Research draft, not peer reviewed. Written against revl commit 45bec431f. Licensed CC BY 4.0.}
}

Text licensed CC BY 4.0, author Thomas Moussajee.