Verification and evidence

This page is for someone deciding whether to trust this engine near real equipment. It answers one question: what has actually been proven about the Open Control Engine, and what has not.

Three questions are worth asking of any system that claims to be verified. What can tell it that it is wrong? Is that thing independent of the system it is judging? And will it tell you which checks it is not running? This page answers them in that order, and every count on it can be reproduced from a clone with find and grep.

The short version first, because it is the part that matters most: two elementary cases have been executed through OpenModelica 1.25.1 against pinned Buildings and MSL sources. The Nand case covers all four two-input Boolean states; the Toggle case covers one exact stateful event schedule with initially true input, repeated rises, and clear priority. The global Tier-3 report remains skipped; no sequence-wide, numeric, or cross-architecture OpenModelica claim follows from these cases.

What can tell this engine it is wrong?

Five different artifacts here are called “tests”. They prove different things, and the most visible of them proves nothing about correctness at all.

Tier-2 determinism goldens — they catch drift, not wrongness

Each of the 46 ASHRAE Guideline 36 fixtures carries a committed whole-sequence trace and a sidecar provenance record. All 46 records say the same two things:

{ "tier": "2",
  "source": "engine self-output (determinism snapshot); NOT a correctness oracle",
  "depends_on_oce_blocks": true }

That is not a caveat added by this page; it is a field in every one of the 46 files, and it is the whole meaning of the layer. These goldens were produced by running this engine and committing what it printed. If the engine computes a sequence wrongly and keeps computing it wrongly, all 46 pass forever. They detect one thing well: that a code change moved a number that was not supposed to move. Call that drift detection, and do not call it correctness.

Each record also carries a content_sha256 binding it to the bytes of its CSV, checked per PR by crates/oce-cxf/tests/golden_provenance/mod.rs. That guard is honest about its own limit in its first paragraph: editing a CSV together with its digest passes by design. It detects drift between two checked-in artifacts, not fabrication of both.

Tier-A oracles — 412 records behind a code-dependency firewall

The correctness layer is generated by tools/golden-gen, a crate deliberately held off the workspace. The repository’s workspace is members = ["crates/*"] (Cargo.toml:24), and tools/golden-gen/Cargo.toml declares an empty [workspace] table so the root workspace cannot absorb it. Its entire dependency list is libm, ryu, and serde_json — no oce-* crate.

That is enforced mechanically rather than by convention. .github/scripts/check-golden-gen-anti-tautology.sh runs cargo metadata over the generator and fails if any package named oce-* appears anywhere in its dependency graph. It fails closed: a cargo metadata error, or output that does not contain the golden-gen package itself, is a failure rather than a pass. It runs as its own CI job and again inside .agents/gate.sh.

The layer contains 412 Tier-A provenance records, every one of them recording "tier": "A" and "depends_on_oce_blocks": false — counts verified across the tree, with zero records carrying true:

• 280 CDL records — 278 per-signal goldens, plus two fold-time provenance-only records with no CSV beside them (goldens/CDL/Types/types.prov.json, pinning enum ordinals, and goldens/CDL/Constants/constants.prov.json).
• 132 G36 sequence signal goldens, spanning all 46 fixtures.

410 of those are signal goldens — 389 compared bit-exactly, 21 under a documented aligned-tolerance band. The 278 CDL signals are compared by the 15 crates/oce-conformance/tests/per_block_*.rs suites through a shared harness that drives each block through the frozen facade, asserts the comparison is unmasked, and asserts compared_points == reference.n_rows so a zero-row comparison cannot pass vacuously. Twelve of the 15 suites run ComparisonMode::Exact with zero tolerances (crates/oce-conformance/tests/block_harness/mod.rs:106-140), and four run their 21 libm-dependent Real goldens through ComparisonMode::AlignedTolerance at 1e-12 (block_harness/mod.rs:142-158, tolerances pinned at :323-332): per_block_reals_transcendental.rs, per_block_reals_sources_transcendental.rs, per_block_psychrometrics.rs, and per_block_utilities.rs — with per_block_reals_sources_transcendental.rs counted in both, because its two CalendarTime cases compare exactly while its single Sin case is banded. Boolean outputs in the aligned suites still compare by bits even in that mode (crates/oce-conformance/src/aligned.rs:214), so 257 of the 278 CDL goldens are bit-exact. The 132 G36 signals are compared by 23 *_funnel.rs and four *_oracle.rs per-fixture suites in the same directory. Their recorded comparison regimes tally exactly: 102 Value::bit_eq f64, 18 exact encoded integer, 12 exact 0.0/1.0.

“Bit-exact” here has a precise definition, in crates/oce-conformance/src/exact.rs: finite Reals compare by IEEE-754 bits, NaN compares equal to any NaN payload, and each signed infinity compares only to itself. Integer and Boolean cells compare their encoded values exactly.

The L1 funnel band is an additional layer applied over the 102 Real G36 outputs, never the primary check. Boolean and Integer outputs are deliberately kept off it, because the funnel is type-blind and a band could otherwise admit a value between two discrete levels (crates/oce-conformance/tests/g36_funnel_band/policy.rs:17-21).

The structural oracle — it bounds fixture fidelity, not block behavior

Every conformance test in the workspace derives from the same 46 catalog fixture documents. The 47th CXF document, member_list_interface.jsonld, is a resolver contract fixture and has no conformance trace. A structurally wrong catalog fixture therefore fails nothing — it makes the entire suite validate the wrong sequence, consistently and permanently. Neither goldens nor oracles can see that, because both are computed from the fixture.

The check that can is crates/oce-cxf/tests/fixture_structural_oracle.rs. It compares each fixture against modelica-json’s independent CXF translation of the same upstream G36 class — 44 .jsonld documents vendored under third_party/modelica-buildings-cdl/cxf/, at Buildings commit a131864e4c4df22ebcd52bb8da439de0087ac365 and modelica-json commit 85721b828a6ff8d9d3c1a48ff9a59808d2fa31fb, pinned and byte-checked by a hash manifest in both directions. The comparison flattens the oracle’s composite hierarchy, resolves every conditional against the fixture’s own parameter values on both sides, canonicalizes array instances and vector ports, and compares instances and undirected edges — counting orientation flips separately, since CXF §8.2 admits either endpoint as the isConnectedTo subject.

The verdict table is itself a committed golden (crates/oce-cxf/tests/fixtures/golden/structural_oracle_verdicts.txt), and its VERDICTS line reads:

VERDICTS: EXACT=30 EXACT-XFOLD=1   EXCLUDED=15

So: 30 EXACT plus 1 EXACT-XFOLD over the 31 comparable fixtures. The XFOLD case is multizone_vav_economizer_controller_single_damper_relief_damper_fixed_21, where one constant-folded subtree (ecoHigLim, 146 reference instances against 0 of ours) is excluded and named in the golden. The 15 excluded fixtures are listed with reasons and are never counted as passes: three are this repository’s own compositions with no upstream class, and twelve are parameter-specialized reductions of AirEconomizerHighLimits that are structurally unverifiable by design.

State the limit next to the result: this compares graph structure only. It contains no numerics and executes no engine code path. It bounds how faithfully the fixture corpus represents upstream G36. It says nothing whatsoever about whether a block computes the right number.

Tier 1 and the global Tier-3 report

This is not a footnote. It is the boundary of everything above.

When conformance report assembly succeeds, it emits five tiers. Tier 1 and Tier 3 are hard-coded as skipped on every successful path:

• Tier 1 — per-block “same response” against the Buildings library. Skipped with the summary "per-block Buildings-oracle comparison is the per-block corpus, not a full-sequence run" (report.rs:131-136). A per-block corpus does exist — the per_block_*.rs suites described above — but it compares against re-derived references, not against Buildings executed output, and it is not wired into the tier report.
• Tier 3 — the global row remains skipped because the report cannot represent partial external coverage (report.rs:138-143). The separate Nand and Toggle tests do not enter the report.

The scoped Nand fixture retains two byte-identical raw OMC runs, one semantic And control, strict raw-to-canonical projection, and the exact facade comparison. The separate Toggle fixture retains two byte-identical raw runs, a one-token Latch control, and the same class of projection and facade checks at explicit event instants. Both regeneration commands are network-disabled and native linux/arm64; CI validates committed evidence and never runs Docker. No Dymola, Spawn, FMI, whole sequence, Real, or Integer external case exists. Two Boolean cases therefore cannot make the engine-wide report pass.

Regeneration assumes a trusted host account, checkout, Docker client, and executable search path. The recorded sandbox limits the OpenModelica container; it does not defend against another process running as the invoking user.

Is the thing that judges it independent of it?

The answer differs by layer.

Tier-2: no, and it never claimed to be. The reference is prior engine output. Its provenance records say so in a field a script can read.

Tier-A: yes at the code level, mechanically enforced, with one honest caveat. The firewall guarantees the generator cannot import the implementation under test, so a Tier-A golden can never be a replay of oce-blocks. What the firewall cannot guarantee is derivational independence. tools/golden-gen/src/main.rs:9-11 states the caveat itself: some exact oracles share a pinned math kernel or restate the same documented recurrence the engine uses. Where that is true, a Tier-A pass is evidence about plumbing and transcription of a shared formula — not an independent check that the formula is right. A mechanical shared-kernel detector is filed as follow-up work and does not exist today, so treat the boundary between “independently derived” and “independently transcribed” as un-audited per class.

The structural oracle: yes. modelica-json is an LBL tool, not one of ours, translating upstream .mo sources this project did not author, at a pinned commit whose bytes are gated. It is also the narrowest claim: structure only, over 31 of 46 fixtures.

The scoped OpenModelica cases: yes at execution and source boundaries. A digest-pinned native arm64 image executes the pinned Buildings Nand and Toggle classes with inputs supplied by MSL BooleanTable. The wrappers contain no expected output. Each comparison remains a discrepancy detector rather than an oracle verdict: analytical evidence comes first in adjudication, and a mismatch cannot change a golden, tolerance, or report status. Their scope is four Boolean pairs for Nand and one event schedule for Toggle.

One more thing an evaluator should weigh: independence of the oracle does not make the comparison independent of when it runs. See the next section.

Will it tell you which checks it is not running?

Yes, and it does so in the place where it is hardest to ignore — the end of every gate run.

The gate prints what it does not cover

.agents/gate.sh finishes by printing a literal block headed NOT COVERED BY THIS SCRIPT — a green run here does not prove these pass, listing:

• The cross-architecture determinism matrix (ubuntu-latest and ubuntu-24.04-arm). One machine cannot reproduce it; CI is the only place it runs.
• The cargo public-api surface gates for oce-api and oce-store. They need a gate-only nightly toolchain and run in release-gate.yml.
• cargo deny check advisories. It needs network access and a writable advisory database, so it runs in advisories.yml and in the release gate’s cargo-deny job instead.
• That these commands still match ci.yml. Nothing verifies that mechanically. An attempt was made and withdrawn; .github/workflows/ci.yml:293-321 records why — every design either compared argv strings, which RUSTFLAGS=--cap-lints=allow leaves byte-identical while neutering clippy, or reimplemented enough of if: / needs: / matrix semantics to become its own untested gate. CI does execute the script (gate (light)), so every command in it gates a PR; the script says outright that this is coverage, not parity.

A light run adds a fifth line: it did not run the workspace test suite or the doctests, because the per-PR gate does not run them either.

The CI split, read in the dangerous direction

CI is dev-light and release-heavy. The per-PR gate into development runs engine tests for oce-api, oce-blocks, and oce-expr only — the determinism-matrix job (.github/workflows/ci.yml:148-168) and the identical step inside the gate script (.agents/gate.sh:120-124), on two architectures in debug and release codegen. The matrix emits populated portable and target-bound engine-state vectors. It requires both to match across codegen profiles, the portable bytes to match across architectures, and the target-bound bytes to differ. The x86_64 comparison job also parses the arm64 target-bound snapshot and requires restore_state to return the target-domain refusal.

Read that in the direction that costs you something. A change confined to oce-cxf, oce-store, oce-conformance, or oce-diag can show every check green having run none of its own tests. A green PR is not evidence that a change’s own tests pass.

That has a direct consequence for everything on this page. The oce-api comparison tests now run per PR, but crates/oce-conformance/tests/ does not, so the complete set of 410 oracle comparisons — 389 bit-exact, 21 aligned-tolerance — still runs only on development → main release PRs, on a daily cron against the development tip, and on manual dispatch (.github/workflows/release-gate.yml). Two input-hygiene audits do run per PR, because .agents/gate.sh invokes them directly: the fixture port-order audit and the structural oracle, the latter also carrying the vendored-tree hash manifest and the Tier-2 provenance digest guard.

One more disclosure worth knowing before you read a PR’s checks: every job in ci.yml is conditioned on github.event.pull_request.draft == false. A draft PR runs no gates at all — not a reduced set, none.

Full detail is in CI and the gate.

Coverage, stated as a fraction rather than a claim

Per-block Tier-A goldens cover 128 of the 133 CDL classes in the registry. The registry pins 136 entries — 133 CDL classes plus 3 reserved internal lowering classes (crates/oce-blocks/src/registry/manifest_tests.rs:21) — and the golden tree contains exactly 128 distinct CDL block class_path values, once the two non-block fold-time records are set aside.

The five without a per-block oracle, and why:

“Indirect G36-sequence evidence” means the class is exercised inside sequences whose outputs are oracle-compared, so a gross error would likely surface — but nothing pins that class’s behavior in isolation, and no per-class edge cases are covered by an oracle. Which classes exist and what “supported” means for sequences is in CDL coverage.

What this adds up to

If you are evaluating this engine, the defensible summary is:

• Determinism is tested, on two architectures, per PR, against committed goldens.
• Agreement with CDL / Buildings source semantics is bounded by 410 oracle comparisons (389 bit-exact, 21 under the documented 1e-12 aligned-tolerance band) against references generated behind a mechanically enforced code-dependency firewall — covering 128 of 133 classes, and running on the release gate rather than per PR.
• Fixture fidelity is bounded structurally against an independent LBL translation of upstream sources, per PR, for 31 of 46 fixtures.
• Agreement with an executed Buildings implementation is bounded for one exhaustive CDL.Logical.Nand Boolean case and one stateful CDL.Logical.Toggle schedule. Global Tier 3 remains skipped.

The gate will tell you which broader checks it skipped. The scoped OMC artifacts do not change those disclosures.

See also: Testing standard for the bar every change is held to, and CI and the gate for what runs when.