The differential oracle

A program specification executes the same MIR twice: once as native machine code and once in a MIR interpreter. The test compares a structured record containing output, errors, traps, source traces, host changes, and live objects.

What agreement means

TranscriptPrinted bytes captured byte for byte, including whitespace and line endings.

FailureRaised error code, message, and origin—or the absence of one.

TrapStable code, message, call frames, source positions, and dropped-frame count.

WorldFiles and bytes, keys and lines read, clock observations, and other host fixture state.

LifetimeLive-object census after success, error, trap, or explicit exit.

End stateSuccess, uncaught error, trap, exhaustion, or chosen exit status.

Independent dispatch, shared semantics

The agreement harnessThe World starts identical and must end identical

source → MIRone compiler result

⋔

LLVM + loadCapture host

compare recordsevery observable field

MIR interpreterReference host

same runtimeARC and operations beneath both

The interpreter owns instruction dispatch, frames, traceback, and host adaptation. Both paths call the same runtime implementations for containers, ARC, text, and other dynamic operations, so the comparison focuses on compiler lowering and MIR dispatch. Keeping the two dispatch mechanisms independent lets a mismatch reveal an error in either path.

What the execution record adds

Printed text covers one observable channel. The execution record also captures leaked objects, trap frames, ownership after a failed store, and mutations to host fixtures. Every program specification receives these checks from the harness automatically.

The oracle's responsibilities

Serve the test harnessThe product build graph leaves the interpreter out of luce and loom.
Interpret MIR independentlyIts own instruction switch, register file, and frame stack exercise a second route through the protocol.
Call shared semanticsDynamic operations go through the runtime used by native code.
Compare every program specificationContinuous use makes a drift visible as soon as the two records differ.

Why program tests are specifications

Anything that runs a Luce program makes a claim about observable behavior and therefore belongs under src/luce/specs/, where both paths run. A test that inspects an internal structure—parser node shape, verifier rejection, or interpreter frame storage—lives beside that implementation.

How a disagreement is resolved

The interpreter has exposed native lowering bugs, and the native path has exposed a stale-register bug in the interpreter. A mismatch identifies the affected program and every differing field. The source contract and focused structural tests then determine which implementation must change.

oracle design agreement harness independent dispatch shared test world