Verification and evidence

The generated authority summary mechanically inventories raw provenance records only. Evidence independence and semantic coverage remain review-only, not inferred counts.

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: four named cases have been executed through OpenModelica 1.25.1 against pinned Buildings and MSL sources. Nand covers all four two-input Boolean states; Toggle covers one exact stateful event schedule with initially true input, repeated rises, and clear priority; Line covers four limit modes across five finite input regions. Reliefs covers one seven-state exact-bit case for a composed G36 leaf. The global Tier-3 report remains skipped; no full-sequence, arbitrary Real, general tolerance, solver, or cross-architecture raw-byte claim follows from these cases.

CDL.Logical.Pre is outside those executed-reference claims. The engine’s fixed HostTick v1 profile delays Pre by one HostTick transition rather than one same-time Modelica event iteration. The profile is covered by exact engine contract tests, not by an OpenModelica oracle, and no broader stateful conformance claim follows from it.

What can tell this engine it is wrong?

Six evidence layers 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 references — 412 records behind a code-dependency firewall

The reference 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. Of these, 392 records check source semantics and 20 check HostTick v1:

• 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 with existing exact comparisons and 21 inventoried accepted Linux exact cases, still aligned-tolerance on unqualified platforms. The retained native receipt records run 37382761120: Linux x86_64/aarch64 × debug/release, two byte-identical runs per cell, 21 signals and 161 samples per run, zero exact mismatches against Tier-A and across cells. Raw bits, synthetic merge checkout provenance, exactly the 35 selected source paths/digests and oracle/input/CXF integrity are checked permanently, without requiring a later HEAD to equal the captured SHA. PC-037 is CURRENT only for this pinned corpus. macOS-arm64 remains unqualified until M06-PR02; neither libm mathematical correctness nor arbitrary-input or whole-engine exactness follows. No Sim policy changes. The selected-boundary receipt is admitted and the ordinary current-qualification test validates it. The original 17-source receipt from run 35492290613 remains immutable history, not current qualification. The current collection run’s successful numerical comparison is not evidence of final green hosted gates; the linked receipt distinguishes those outcomes. The reviewed 35-file map covers checker/admission/comparison/workflow/direct formula/harness and supporting sources, not the full compiled transitive facade closure. Exact-head hosted cells (x86_64 native, aarch64 QEMU-emulated) rerun oce_api::Engine per PR and catch changes under the pinned corpus’s comparison rules. An unbound transitive source change preserving all pinned outputs does not invalidate the historical raw result. Source digests alone do not prove current whole execution semantics. 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), and four select each of their 21 libm-dependent Real goldens through the inventory: exact on the two qualified Linux targets, ComparisonMode::AlignedTolerance at the unchanged 1e-12 band elsewhere: 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 inventoried. Boolean outputs in the aligned suites still compare by bits even in that mode (crates/oce-conformance/src/aligned.rs:214), so all 278 CDL goldens are exact on qualified Linux targets, versus 257 exact and 21 aligned elsewhere. 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.

The semantic claim is narrower than the 410-comparison count. 390 signal goldens check CDL / Buildings source semantics: 369 existing exact and 21 native-matrix-qualified Linux cases (conservative aligned-tolerance on unqualified platforms). The remaining 20 exact G36 signals belong to Generic.TimeSuppression, CoolingOnly.Controller, and ReliefFanGroup. Those references are independent of oce-blocks, but their CDL.Logical.Pre recurrences implement HostTick v1 and are labeled as profile checks rather than Modelica event-iteration oracles.

“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, Toggle, Line, and Reliefs 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. Toggle 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 are native linux/arm64 cases.

Line retains two repeat-identical native runs on each of linux/arm64 and linux/amd64, with both platform manifests and configs under the shared OCI index. Its canonical bytes match across the two architectures. Four closed views drive the public facade at the emitted timestamp bits and compare OpenModelica and engine outputs against an independent 40-cell expected-bit table. Each architecture retains keep-first canonical output and inspection metadata. The structural sentinel executes the explicit keep-first path again from retained raw input, compares both artifacts byte-for-byte, and derives input-schedule mismatches at rows 2, 4, 6, and 8. This projection control is not a facade-comparator control, and this stateless block can remain green when given internally consistent pre-event rows. The external limit-flag change, swapped output mapping, and four arithmetic reference mutants fail through the facade comparator at pinned rows. This proves only the fixed finite matrix; raw cross-architecture bytes, other Line inputs, non-finite values, signed zero, subnormals, and solver behavior remain outside it.

Reliefs also retains two repeat-identical native runs on each architecture and compares one strict keep-last canonical table across them. The seven retained rows are the initial state followed by the first complete five-input tuple change. The facade drives those tuples at the emitted timestamp bits and reads only the declared yOutDam and yRetDam roots; topology checks bind those roots to the internal Min and Max drivers. All 14 output cells are compared exactly against an independent bit table. A parameter-only uOutDamMax change, swapped root mapping, a nonexistent root, keep-first projection, and inconsistent final limits exercise separate failure or overwrite paths. The final limit control fixes all 21 raw input tuples plus the seven selected tuples, timestamps, and source rows before checking the overwritten outputs. This is one composed G36 leaf at one parameterization, with no claim about other G36 classes or parameters.

Each native architecture record binds every checkout file used through native artifact publication, including workflow, sandbox helpers, OCI metadata, wrappers, and canonicalizer tool inputs. Assembly and final-manifest generation happen after native publication, so their scripts are bound by the final artifact manifest rather than represented as native generator inputs.

Reliefs records one immutable generation contract in crates/oce-cxf/tests/open_modelica_reliefs_reference/generation-revision.json. Its revision is the exact checkout observed while the candidate native artifacts ran, not a reachability requirement. During generation, each record must equal checkout HEAD. The candidate assembler requires both native records to share that observation and the complete generator-input digest map, verifies the current exact input bytes, and emits the candidate contract and manifest together. Retained validation uses those committed bytes and does not inspect Git history. Zero, stale, unrelated, or rehash-substituted observations still fail the fixed contract.

The Line and Reliefs workflows install Rust 1.97.1 and Python 3.13.7 for host-side artifact processing and record compiler, Cargo, Python, and architecture identities in each native log. MSL materialization uses git archive with the explicit Modelica/package.mo -export-subst attribute override. For the pinned source, both the committed and materialized Modelica/package.mo SHA-256 values are c3a060fc29842aaf3b7a565b93dbe80fe29d6a769848e3b077f5101117a65191; separate fields preserve the boundary even though the bytes are equal. Buildings uses no local attribute override, and its committed and materialized file hashes are also recorded separately.

All four regeneration paths disable container networking. The retained Line and Reliefs workflows are manual only after evidence capture; normal CI validates committed evidence and does not run Docker. No Dymola, Spawn, FMI, whole-sequence, or Integer external case exists. These four cases cannot make the engine-wide report pass.

The Reliefs manual workflow produces and verifies one candidate native artifact per architecture, then runs the same two-architecture assembler used for ratification and uploads its candidate manifest and contract. Its green status proves that those workflow outputs enter the assembler; it does not say that the committed fixture is fresh. Admission still requires committing the emitted contract and assembled evidence, followed by retained-graph validation. Repository Python entrypoints disable bytecode writes so ignored __pycache__ files cannot pollute a generation checkout. That Python validator is POSIX-only; the equivalent Rust validator remains the cross-platform retained-evidence check and uses handle metadata on Windows.

Regeneration assumes a trusted host account, checkout, Docker client, Git and shell tools, and executable search path. Rust and Python artifact tools are pinned and recorded; that does not turn the rest of the host into sandbox inputs. 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 image executes the pinned Buildings Nand, Toggle, Line, and G36 Reliefs classes with inputs supplied by MSL sources. 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, one event schedule for Toggle, one finite four-mode/five-region matrix for Line, and one seven-state exact-bit case for the composed Reliefs leaf.

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 (the script’s report still names ubuntu-latest and ubuntu-24.04-arm; CI now runs x86_64 natively and aarch64 under QEMU emulation). 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 pr-gate.yml. Nothing verifies that mechanically. An attempt was made and withdrawn; the dormant .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 the state-determinism subset for oce-api, oce-blocks, and oce-expr — the determinism-matrix job and the corresponding steps inside the gate script, on two architectures (x86_64 native, aarch64 under QEMU emulation) 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 job also parses the aarch64 target-bound snapshot on x86_64 and requires restore_state to return the target-domain refusal.

Separately, the scoped oce-conformance strict-bit subset runs per-PR: strict_bits and the four affected per-block suite binaries, Linux x86_64 (native) / aarch64 (emulated) × debug/release, two independent process captures per cell and fail-closed cross-cell comparison. The retained receipt covers the 21 formerly banded Real cases; Linux exact comparison is not a macOS qualification.

The remainder of oce-conformance still follows release/full-gate coverage. The complete set of 410 reference comparisons — 389 existing exact plus 21 exact on qualified Linux, unchanged 1e-12 aligned elsewhere — runs in the full local gate and release workflow (release PRs, daily cron against development, and manual dispatch). Two oce-cxf input-hygiene audits also run per-PR: fixture port order and the structural oracle, including the vendored-tree and Tier-2 digest guards. A change outside these named subsets can show every check green without running its own tests. A green PR is not evidence that the rest of a changed crate passed.

One more disclosure worth knowing before you read a PR’s checks: CI OK is the single status that summarizes the per-PR gate. Confirm it reported, not merely that nothing is red.

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 against Modelica semantics. Pre is the exception to the edge-case part of that row: its HostTick profile has direct facade tests, but those tests are not an independent correctness 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 390 oracle comparisons: 369 existing exact plus 21 exact on qualified Linux and at the unchanged 1e-12 aligned band on unqualified targets. The retained strict-bit evidence applies only to the pinned corpus/toolchain. References behind the code-dependency firewall cover 128 of 133 classes; the scoped strict-bit subset runs per-PR, while the remainder needs the release/full gate.
• HostTick v1 agreement is checked separately by 20 exact G36 signals across the three Pre-dependent fixtures. Those are profile checks, not Modelica event-iteration evidence.
• 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, one stateful CDL.Logical.Toggle schedule, one finite CDL.Reals.Line matrix, and one composed G36 Reliefs leaf. 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.