Simcraft Docs
Open the app

The reference machine#

The OSDL repository contains an executable reference machine written in Lean 4, under machine/. It is the specification's answer to a hard question: when two engines disagree, who is right?

An executable definition#

Prose specifications leave room for interpretation. The reference machine does not: it implements the kernel semantics, the standard component behaviors, and the pinned sampler algorithms as executable Lean code.

Where the prose and the machine describe the same behavior, the machine is the tiebreaker for conformance cases. The distribution samplers are the clearest case: the exact algorithms, from inverse-CDF transforms to the Box-Muller normal, live in machine/Machine/Samplers.lean, and fixed cases generate committed golden vectors that any implementation can check its own samplers against.

What conformance compares#

Conformance is a comparison of outputs, not of architectures. For each case in a suite, an implementation runs the model document and produces artifacts:

  • Recorded results, compared structurally with a declared floating-point policy. The strictest mode requires bit-equal IEEE 754 values.
  • Portable events: the event stream with telemetry removed and per-stream sequence fields ignored, order-preserved within each causal identity.

Implementations may use different calendars, storage, and telemetry cadence. Those choices are conformant when valid documents, recorded results, and portable events remain compatible.

Suites compose: the core suite covers kernel behavior, and each standard library ships its own cases that run after core. A child suite can add cases or make comparison stricter, and it must not weaken a parent's requirement.

Contracts for what core leaves open#

Some behavior is deliberately outside OSDL Core: the concrete component authoring interface, raw callback order, exact telemetry. An implementation contract, such as the reference machine contract, can pin those rules for implementations that opt in. A runner selects a contract outside the document; an OSDL model never does.

What this buys a modeller#

The practical consequence is that "the same model" means something checkable. A claim that an engine implements OSDL is a claim that its results and portable events match the reference machine on the conformance cases, and that its distributions draw the same values as the committed vectors. Trace equality, not tool loyalty, is what makes a result transferable.

Read more#