SIR — the Semantic Intermediate Representation

1 · What SIR is

SIR is the format a rederive package ships instead of trusted bytes. Where npm hands you a prebuilt implementation and a name to trust, a rederive package hands you a contract: a structural spec (the .sir file) plus a differential oracle (the oracles/ vectors). You verify the shipped code against it, or re-derive the code from it.

A SIR artifact is one recursive tree of KIND-discriminated nodes. It describes a single unit of behavior — a function, a handler, a leaf — at the level of what crosses its boundaries and what shape its control flow takes, not at the level of source syntax. Two implementations in two languages with the same choreography have the same SIR body.

Crucially, SIR is not a proof system and the prose in it is not load-bearing. The ground truth of a unit's behavior is its oracle — input→output (or input→trace) vectors whose expected values were produced by executing the original. The .sir text orients a human and a re-emitter; the oracle is what a build is graded against.

2 · The four invariants

Everything below is downstream of four rules. They hold for every unit, every package, every version.

i. The discriminator leads

Every node declares its KIND first; kind is never inferred from the node's shape. A reader (human or machine) knows whether they are looking at a pure computation or a world effect before parsing anything else.

ii. The firewall

iii. The oracle is the substrate

A SIR artifact is self-contained = spec + frozen differential vectors. Prose fields (INVARIANT, NOTES) are an unverified prior — useful, optional, never load-bearing. (Proven twice on held-out repos: structural skeleton + coverage reaches 18/18 held-out with the prose stripped — and prose can be outright wrong.)

iv. Expecteds are differential, earned with the original deleted

Expected outputs are produced by running the original implementation, never hand-authored. A unit's verified status is earned by passing the held-out round-trip gate after the original source has been deleted — the re-emitter reconstructs from the contract alone, so a pass is evidence of the contract, not a copy of the source.

3 · The unit header

Every .sir file opens with a fixed header. Fields in grey are placeholders.

unit header grammarSIR     <name>                          # snake_case; a "name worth saying"
KIND    FUNCTIONAL | EFFECT
SRC     <file>:<Class.>?<symbol>        # provenance; review diffs anchor here
SIG     (<params>) -> <result>
TRIGGER call | http(<route>) | cli | cron | <custom>   # OPTIONAL; default call
REACH   entry | internal | off-path
ORACLE  value | trace  @vectors: <path>  [VERIFIED <evidence>] | [not captured]

4 · Kinds & the firewall

There are two kinds. The firewall (invariant ii) keeps them from mixing. But "is this unit pure?" has a third, honest answer — when a unit looks pure but calls something the analyzer can't see through.

The tri-state firewall

The third bucket exists so that unknown externals never silently pass as pure (the soundness fix) and never falsely claim a world effect (the noise fix). A suspect unit whose value-oracle round-trip passes is behaviorally pinned even though its purity is only assumed — the passing oracle upgrades trust, not kind.

The known-pure allowlist is a versioned artifact (it starts with language builtins, path.*, semver, minimatch, …). Opaque dependencies must be named — see DEPENDS-ON OPAQUE in §5.

Reachability (REACH)

The decompiler computes reach from the export table and call graph. Off-path units are kept, not dropped — an exported-but-uncalled function is still part of the public behavior surface, and silently dropping it is API loss in a migration.

5 · Control & data nodes

STATE — accumulators are declared once, at unit level

A LOOP gets no first-class accumulator binding. A unit that reads or writes an accumulator declares it once:

STATE  <name> (in) | (out) | (in/out)     # e.g. STATE map (in/out)   STATE cache (out)

The oracle carries the fold semantics — a unit-level STATE marker plus differential vectors is enough to round-trip a stateful fold (proven on dotenv's parse and editorconfig's caches). A caller-provided accumulator (a passed-in Map/array) is STATE, not a world effect — it stays FUNCTIONAL.

BRANCH — including on-error

A BRANCH selects an arm by a predicate. Error handling is not a separate kind — on-error is sugar that desugars to a BRANCH with an error predicate, because an error arm carries the same verification obligation as any branch arm (arm coverage by captured inputs).

BRANCH on-error(<op>) { <arm> -> … }       # desugars to BRANCH with an error predicate

DEPENDS-ON — and the OPAQUE rule

In-module dependencies are named so the call graph is explicit. External calls that are not on the known-pure allowlist must be named as OPAQUE — this is what makes the firewall's blind spot visible (the unit becomes FUNCTIONAL?).

DEPENDS-ON <unit>, <unit>                      # in-module units
DEPENDS-ON OPAQUE(<module>.<symbol>), …        # external, not on the known-pure allowlist

6 · Effects & the boundary

An EFFECT unit's behavior is its sequence of boundary crossings. Outbound calls are EMIT (recorded, not performed during verification); inbound reads are REQUEST (injected at verify time from the captured trace).

boundary grammarEMIT    <boundary.op>(<args>) -> <name>    # outbound WITH a meaningful reply: one node
EMIT    <boundary.op>(<args>)              # outbound, fire-and-forget
REQUEST <boundary.op>(<args>) -> <name>    # purely inbound (fs.read, env.read, clock, rand)

An outbound call that returns a meaningful reply (a spawn whose stdout you read) is one protocol step — the trace records the emission and the injected reply together, so there is no artificial ordering ambiguity.

Boundary descriptors are <domain>.<verb>, two levels

Not per-API-function. fs.readFileSync and fs.readFile are both fs.read — sync/async is calling-convention metadata, proven irrelevant to the trace. The args stay on the node, so finer-grained audit is still possible.

The verb is an operation class: read · write · stat · spawn · query · exec · fetch · set · timer · … A new net.fetch edge appearing in a review diff is exactly the red line an auditor must see.

Reading the clock vs. owning it — the scheduler is a control effect

A clock read (REQUEST time.now) returns a value and is injected like any other inbound read. Scheduling against the clock is a different effect. A timer (time.timer — setTimer / clearTimer) and the microtask scheduler are not point reads; they are a control effect that decides when deferred work runs relative to everything else. A timer race — does a timeout fire before the awaited reply settles? — is nondeterministic on the wall clock, so it is verified on virtual time: the event loop is injected as a scheduler the harness drives (schedule for microtasks, setTimer/clearTimer/advance for timers), making resolution order a deterministic, replayable function of the timeline. (Specimens: q's delay/timeout and its microtask core.)

Ordering, PAR & concurrency

A trace is an ordered sequence of EMIT/REQUEST records. Canonicalization may normalize representation (key formatting, serialization) but never ordering. The one exception is an explicit concurrent window:

PAR { … }    # a concurrent window: sub-traces whose relative order is not fixed

A PAR block's canonical form depends on whether its sub-traces are independent. When they commute (touch no shared state — order is observationally irrelevant), the canonical form is the sorted multiset of sub-traces and verification collapses to one representative. When they are dependent (a shared resource — order changes the observable), sorting is unsound: the unit is verified over the space of interleavings against the retained reference's reachable-outcome set + invariants (safety, ordering, conservation), with the message-delivery order injected as the boundary the harness owns.

Coverage of that space is reported on a ladder: exhaustive (small inputs — proven over all interleavings) → sampled (coverage-counted, when the space explodes) → partial-order reduction (one representative per equivalence class of independent reorderings — cheap exactly when the unit is correctly order-independent, thorough exactly when a refactor is not). A control effect additionally carries a resource-lifecycle channel (§7). (Specimens: p-map's concurrency contract — interleaving-invariant output + a max-concurrency bound — verified exhaustively for small inputs and POR-scaled past 10¹² interleavings; a two-account transfer whose outcome is interleaving-dependent; request's redirect state machine.)

A third option collapses the space at design time: a token RING. When the unit coordinates through a single circulating permission — only the token-holder acts — the interleaving reduces to a deterministic schedule (one outcome per token order; fixed-rotation is one schedule, verified in O(1)). It is the design-time dual of partial-order reduction: POR detects independence to shrink the space; a ring imposes coordination to shrink it. A ring is a behavior refinement — R_ring ⊆ R_free always (every ring run is a valid free run, so it can only drop outcomes, never invent one). The decomposer may recognize a ring (verify R_ring = R_free, behavior-preserving) or be directed to impose one — a behavior-changing transform that emits a mandatory divergence report, the dropped outcomes split into benign-determinization, safety-fix (a dropped outcome violated an invariant — a race removed), and narrowed-nondeterminism (a valid alternative dropped — confirm or refactor). (Specimen: ringbuf.js's SPSC producer protocol, modeled at Atomics-operation granularity — its single-producer contract is the ring; two-producer use admits the lost-write race the ring drops.)

TRIGGER is metadata, never structure

7 · The oracle

Each unit names exactly one oracle mode.

Both are differential: the expected value (or trace) is captured by instrumenting and running the original. An oracle asserts behavior — wire bytes, claims, status, the trace shape — and never the source library's representation (error-string wording, object-vs-string body). Freezing representation is a trap; freezing behavior is the contract.

For greenfield units with no original to run, the oracle can instead be a (generator, properties) pair — round-trip, idempotence, determinism, conservation — verifying correctness-of-contract rather than identity to a reference. (This property mode is part of the rederive toolchain; the frozen .sir grammar above covers the value/trace migration case that ships in today's packages.)

A control effect — a timer, a subscription, a lock — carries a second observable beyond value-and-order: its resource lifecycle (armed / fired / cancelled; subscribed / torn-down). Cancellation is invisible to the trace: a leaked timer still fires, but its effect is a no-op on already-settled state, so the emit/reply sequence is byte-identical while a real resource leak goes uncaught. The oracle for such a unit therefore also asserts the lifecycle channel — timers cleared, handles closed. (Specimen: request's redirect timeout — a dropped clearTimer passes value+order but leaks; caught only on the lifecycle channel.)

8 · Worked example: strip.sir

This is the actual SIR shipped in @rederive/colors — the re-derivation of colors.strip from colors@1.4.0, the last release before the January-2022 maintainer sabotage. Eight lines; every one carries weight.

packages/colors/sir/strip.sirSIR    strip
KIND   FUNCTIONAL
SRC    colors@1.4.0 lib/colors.js:strip  (alias stripColors)
SIG    (str: string) -> string
REACH  entry
CONTROL LOOP x1
ORACLE value @vectors: oracles/strip.json [VERIFIED value 10/10 ho, quorum 3/3, original deleted]
# Removes single-parameter SGR codes (ESC[<digits>m) only; combined-SGR / CSI / OSC survive (faithful).
# GENERATED by sir decompile (structural, SIR Schema v0.1) + verified-recompose.

Reading it as a contract:

• KIND FUNCTIONAL — pure; the firewall guarantees no file, network, or env access hides inside.
• SIG (str: string) -> string — one string in, one string out.
• ORACLE value … [VERIFIED 10/10 ho, quorum 3/3, original deleted] — the load-bearing line. Ten held-out vectors (disjoint from the ten the re-emitter saw), passed by three independent re-derivations that agreed, with the original source deleted before any of them ran.
• The comment pins a real finding as a documented limitation: strip removes only single-parameter SGR codes, so combined-SGR / CSI / OSC terminal-injection escapes survive. rederive states that in the contract rather than hiding it — the held-out oracle includes the surviving-escape cases, so the limitation is tested, not just claimed.

The shipped src/strip.ts is graded against oracles/strip.json by rdv check. Anyone who distrusts the shipped bytes runs rdv resynth and re-derives them from this contract locally.

9 · Module-level SIR

A multi-unit package also carries a MODULE.sir — the auditor's one-page surface. It draws the firewall cut explicitly, lists every unit and its .sir file, sketches the call tree (marking ║CALL across the firewall and · dependencies within FUNCTIONAL), and — the key line for a security review — declares the effect surface: the complete set of inbound injections and outbound emissions the whole module's traces may touch. Nothing outside SURFACE is allowed to appear in a trace.

MODULE.sir — the shape (abridged from dotenv-core, the first EFFECT-tier decompile)MODULE  dotenv-core
FIREWALL  FUNCTIONAL ⊅ EFFECT
  pure   (FUNCTIONAL): parser.ts, common.ts, utils.ts   — no fs / env / process
  shell  (EFFECT):     index.ts                          — every effect lives here

UNITS
  EFFECT      load          effect/load.sir       index.ts:DotEnv.load
  FUNCTIONAL  parse         functional/parse.sir  parser.ts:Parser.parse
  … one row per unit, with its .sir file and provenance …

SURFACE
  inbound  (REQUEST, injected at verify):  fs.readFileSync ; child spawn stdout
  outbound (EMIT, recorded not performed): process.env[set] ; fs.writeFileSync ; console.error

This is the artifact a PR reviewer or a compliance auditor reads first: a new edge in SURFACE — a module that suddenly emits net.fetch — is the diff that must not pass silently.

10 · The bundle & the verification contract

A self-contained, shippable rederive unit is a bundle:

bundle layoutbundle/
  sir/<unit>.sir            # specs per this schema
  oracles/<cluster>.json    # { unit, captured_from, vectors: [{name, input|args, expected}] }

Three rules make the bundle verifiable rather than merely descriptive:

• Frozen + held-out. Vectors are frozen at capture. Coverage rounds may append fresh inputs, but a disjointness guard refuses any held-out string that leaked into the set the re-emitter sees. Train and test never overlap.
• The original is deleted. The re-emit gate consumes only the bundle. The implementation is reconstructed from the contract, never copied from the source.
• Closure by density, not by a single pass. A round closes only when (a) the full held-out set is re-run — a new vector can regress a previously-passing seam — and (b) N≥2 independent emissions agree. One passing emission on an uncovered class is luck; agreement is evidence. Priors are outvoted by evidence density, never overridden by a single contradiction.

11 · Non-normative annotations

Decompilers emit human-facing prose to orient a reader: ABOUT, INVARIANT, NOTES, CONTROL, CHOREOGRAPHY, TRACE-INVARIANT. These are annotations, not contract. By invariant iii they carry no verification weight — they can be incomplete, and they have been observed to be wrong. A re-emitter may read them; a verifier ignores them. If an annotation and the oracle disagree, the oracle wins, every time.

The practical consequence: never encode a behavioral guarantee in a comment and expect it to hold. If a behavior matters, it belongs in a vector, where execution proves it and the held-out gate enforces it.

12 · Conformance & governance

This specification is normative. The key words MUST, MUST NOT, SHOULD, and MAY are interpreted as in RFC 2119. SIR is intended to develop as an open, royalty-free standard for verified software contracts — implementable by anyone, in any language, without license or fee.

Conformance classes

Three independent conformance targets. An implementation may conform as any one of them.

The whole pipeline — bundle, checker, and producer — is in scope of the open standard. The standard defines what conformance is; it does not mandate how a producer reconstructs an implementation (the quality of that engine is where implementations compete).

Standardization & licensing posture

SIR is developed as an open, royalty-free standard. The format and the rdv reference checker are licensed Apache-2.0 and free to implement — in any language, by anyone, with no fee, no license negotiation, and no patent assertion against conforming implementations. The format is not encumbered, and our commitment to keep it that way is written down and binding in The rederive Promise.

Versioning

Schema v0.3 (2026-06-22) adds the token-coordinated RING shape (§6) — concurrency that flows through a single circulating permission, reduced to a deterministic schedule. v0.2 added concurrency/PAR semantics, the scheduler/timer control effect + virtual time, and the resource-lifecycle oracle channel — extending the frozen v0.1. Each is forced by a named specimen (p-map, q, a two-account transfer, request's redirect, ringbuf.js). Every decision still cites the specimen that forced it — nothing is resolved from taste alone. Changes are versioned, never silent; a conforming bundle records the version it targets.

Deferred (named, not frozen)

• Transactions / compensation; multi-process effects across machines — the wire (message loss, partial failure, cross-machine clocks). Intra-process concurrency is addressed in §6; the network boundary stays record/replay-or-bespoke.
• Optimal source-set DPOR for the interleaving ladder (§6) — sleep/persistent-set reduction is validated; the optimal variant (one explored execution per class) is future.
• An ambient-read tier (env.cwd, locale, timezone).
• The ui domain verbs (a frontend target is a non-goal at this phase).

SIR is the representation produced by Semcom's verified-recompose engine. The format and the rdv checker are open (Apache-2.0); the engine is a separate implementation that competes on quality, not on access to the standard.

13 · The two modes — re-derivation & verified normalization

The verified-recompose method runs in two modes, differing in what plays the oracle and whether the original survives. Both produce the same SIR units under the same firewall (§4); only the source of ground truth differs.

Mode 1 — catalog re-derivation

What §10's bundle describes: a unit with a compact spec and a frozen, held-out oracle. The original is deleted before re-emit; N isolated rebuilds must agree on the full held-out set (quorum). This is how the catalog ships verified packages.

Mode 2 — verified normalization

For a monolith whose behavior won't compress into a compact contract — a large stateful class, an async state machine, a concurrent coordinator — the original is retained as a live differential oracle. You propose a firewall-clean factoring (the same kinds and FUNCTIONAL ⊅ EFFECT firewall as §4) and verify it reproduces the original on generated, held-out scenarios it never saw. Mode 1 guards against hallucination; Mode 2 guards against an incomplete refactor (regression). A Phase-0 feasibility gate decides normalizable vs. genuinely bespoke before any cut: if no faithful, deterministic oracle can be captured, the honest answer is to stop.

Effects, time & concurrency under Mode 2

The boundary descriptors of §6 are injected and replayed: net/fs/env via record/replay, the clock as a value, and the event loop itself as an injectable scheduler. Timers verify on virtual time (a timer race is nondeterministic on the wall clock, deterministic once the loop is owned). Genuinely concurrent units are verified by owning the message scheduler and checking the space of interleavings — exhaustively for small inputs, and partial-order-reduced beyond (one representative per equivalence class of independent reorderings). A control effect additionally carries a resource-lifecycle channel — a cancelled timer, a torn-down subscription — that value-and-order observation alone is blind to.

The honest ceiling

Mode 2 is testing, not proof: a normalized unit is proven-equivalent on the exercised, coverage-reported scenario distribution — dramatically stronger than a blind rewrite, never "provably identical everywhere." The coverage rung reached — exhaustive, sampled, or partial-order-reduced — is reported, never silently assumed.

14 · Lineage (non-normative)

SIR is assembled from well-understood pieces, not invented whole. Each construct is named here with its origin — both as intellectual honesty and because a named, classical construct is one an implementer and a verifier can actually reason about. The recurrence is no accident: the abstractions that are verifiable are the ones with small, explicit, well-defined semantics — exactly what the classics, born under tight constraints, were forced to produce.

• The kind-discriminated tree (§3–5) — compiler intermediate representations and the AST; structured / stepwise refinement (Dijkstra; Wirth).
• The FUNCTIONAL ⊅ EFFECT firewall & injected boundaries (§6) — effect systems and algebraic effects & handlers (Plotkin & Power; Plotkin & Pretnar); monads (Moggi; Wadler). "Inject, never ambient" is the object-capability model (Dennis & Van Horn; Miller) and least privilege (Saltzer & Schroeder, 1975).
• The oracle — behavior over text (§7) — denotational semantics (Scott & Strachey); observational equivalence and bisimulation (Milner; Park); property-based testing (QuickCheck — Claessen & Hughes, 2000).
• Quorum re-emission (§10) — N-version programming (Avižienis): independent implementations accepted on agreement; held-out grading is cross-validation.
• PAR & concurrency (§6) — CSP and refinement (Hoare, 1978); Petri nets (Petri, 1962) for the token and place-invariants; model checking (Clarke & Emerson; Queille & Sifakis) and TLA+ (Lamport) for interleaving + refinement + invariants; Mazurkiewicz traces (1977) and partial-order reduction (Godefroid; Peled; Abdulla et al.) for the independence collapse.
• The actor shape — the actor model (Hewitt, Bishop & Steiger, 1973); E-language vats (Miller).
• The ring shape — token-passing mutual exclusion (Le Lann; Suzuki & Kasami); Kahn Process Networks (Kahn, 1974) for FIFO determinism-by-construction; the single-writer discipline as linearity (linear logic — Girard; ownership types).
• Verified normalization (Mode 2, §13) — term rewriting and confluence / Church–Rosser; Knuth–Bendix completion; the refinement calculus (Back; Morgan).
• The contract & content hashes (§10, §12) — Design by Contract (Meyer / Eiffel) and Hoare logic (1969); content-addressed code (Unison); reproducible builds (Nix — Dolstra).
• The runtime — Forth (Moore) for the concatenative dictionary; Smalltalk (Kay; Goldberg & Robson) for message passing and doesNotUnderstand:, the literal trigger for synthesis.

On the roadmap — definition hardening: lift invariants and refinement into a small declarative property language on the contract (TLA+ / refinement-calculus style), so more verification — and more deterministic codegen — keys off the definition than off hand-written checks; and abstract interpretation (Cousot & Cousot, 1977) as the soundness theory for when sampled coverage is sound.