0.10: correct-by-construction tensor-native compiler core

[jgoppert]

Summary

This branch rebuilds Rumoca around a correct-by-construction, tensor-native compiler and execution pipeline. The intended refinement claim is stronger than “the compiler did not crash”: a model accepted through the checked pipeline must initialize and simulate with the semantics represented by its source. OMC remains the differential oracle. A completed but inaccurate trace is an actionable counterexample unless the exact model is classified as a reviewed boundary where raw pointwise comparison is not identifying.

The branch deliberately does not claim that this theorem is complete. It makes the claim more defensible by moving semantic obligations into constructors, removing parallel legacy representations, and requiring every observed counterexample to be reproduced, explained, fixed at its owning phase, or recorded as a typed oracle-comparison boundary.

Compiler and IR

• Rebuilt canonical DAE and Solve aggregates around private storage, typed IDs, checked constructors, exact provenance, construction/replay operations, and phase-owned invariants.
• Preserved compact tensor structure through Flat, DAE, structural analysis, Solve lowering, evaluation, and code generation. Ranges, comprehensions, affine stencils, record arrays, indexed writes, field projections, and dependent function shapes remain structured until a scalar view is genuinely required.
• Added compact structured event-relation families. A relation inside a tensor family owns one checked domain; scalar root programs are generated views in canonical order, not a second semantic owner.
• Made structured function execution exact for dependent loops, sequential array and record assembly, conditional multi-target assignment, early return, call-scoped assertions, and multi-output calls.
• Reworked dependency projection so function results follow only the requested scalar and its transitive carried values. Unrelated loop contexts no longer multiply the dependency graph.
• Retained explicit ownership for equations, algorithms, clocks, conditions, roots, assertions, termination, pre, sampled values, dynamic deadlines, and discrete updates.
• Removed permissive fallbacks and model-specific recovery paths. Unsupported semantics fail at their owning phase with typed diagnostics.

Solver and FMI execution

• Unified linked simulation behind the checked FMI 3 Model Exchange component boundary; concrete integrators consume that host contract rather than compiler IR directly.
• Added construction-owned refresh schedules, exact BLT remainders, sparse structural patterns, Jacobian coloring support, and sparse linear algebra through faer.
• Made nonlinear projection branch-stable with compiler-issued causal seeds, scaled residuals, bounded continuation, and exact fallback restoration.
• Reuse of settled coordinates is permitted only through explicit checked coverage and bitwise-identical state/derivative/parameter snapshots.
• Automatic integrator selection is a capability decision: only typed directional-derivative unavailability makes BDF ineligible. Numerical or semantic failures are not hidden by retrying another integrator.
• Added regressions for structured roots, event iteration, sensitivity, automatic host selection, singular/scaled systems, and FMI ME host divergence.

GALEC, eFMI, FMI, and deployment targets

• Rebuilt GALEC lowering around typed signal contracts, deterministic clock schedules, causal outputs, expression projections, user functions, assertion effects, and explicit error-signal status.
• eFMI Algorithm Code and Production Code packages are generated from the checked GALEC path and validated for manifest integrity, typed cross-references, checksums, lifecycle, and numerical equivalence.
• FMI 2 and FMI 3 expose both Model Exchange and Co-Simulation source-FMU profiles over the shared component semantics.
• FMI-LS-Wasm and FMI-LS-DAE remain standards-oriented layered targets with pinned contracts and target-local runtime checks.
• Code-generation target names describe their artifact/use case while manifests explicitly declare the IR they consume. Removed aliases and incomplete targets fail before rendering.

Embedded-C assurance boundary

The generated embedded C is now designed for an auditable, MISRA-oriented assurance profile:

• strict C99 compilation with pedantic warnings in the checked fixture suite;
• bounded static storage, no allocation or recursion, explicit-width status fields, tagged structures, and guarded header interfaces;
• single-evaluation helpers, explicit control flow, deterministic symbol generation, and no token-pasting convenience macros;
• statement-level source identifiers and byte spans carried from checked IR into generated comments;
• explicit status propagation for error signals and runtime contract failures.

This is not a claim of MISRA C or DO-178C compliance. MISRA compliance requires a documented guideline selection, deviations, tool reports, and process evidence. DO-178C approval requires project-specific planning, requirements traceability, verification independence, configuration management, coverage evidence, and a certification-authority decision. The compiler now preserves evidence useful to those activities without placing an unsupported compliance claim in generated banners.

MSL oracle evidence and counterexamples

The verification workflow uses the pinned 566-model MSL root-example cohort and accounts for every successful Rumoca simulation. The resolved quality baseline owns the exact 113-model certified strict-high roster; prior workflow artifacts remain diagnostics and cannot silently redefine that ratchet:

• models in cohort: 566
• compiled to checked DAE in the current local run: 230
• Rumoca sim_ok: 122
• strict-high OMC pointwise comparisons: 113
• current reviewed pointwise-oracle boundaries: 9
• near/deviation/missing-trace results: 0
• unclassified or actionable compile-sim counterexamples: 0

Reviewed boundaries are not hidden passes. Their exact model names and reasons are checked into msl_trace_compare_exclusions.json, and the baseline migration pins both the old/new classification counts and the SHA-256 of that artifact. The catalog covers chaotic trajectory separation, event-side trace conventions, integration-residue-scale period aggregates, and nonsmooth contact timing. Changes to comparator policy must increment the gate schema and provide exact migration accounting; unrelated quality metrics remain monotonic.

Verification

Final tip 28138a9b passes cargo xtask verify quick inside the project Nix environment with four workers. The branch also completed cargo xtask verify full locally during development; the final change is covered by the quick suite plus an exact replay of the failed hosted four-shard MSL merge:

• 5,870 workspace tests plus doctests
• exact replay of hosted run 31249111264 shard artifacts through the corrected merge gate
• architecture, specification, complexity, traversal, and workflow gates
• pinned 566-model MSL/OMC differential run
• template rendering and runtime checks for the declared deployment targets
• generated C compile/link/execution tests
• coverage line gate
• Rust/API documentation and both mdBooks
• VS Code extension tests, native/Wasm bindings, release Wasm builds, and full-MSL LSP timing budgets

Optional local external-tool checks reported their prerequisites explicitly rather than masquerading as proof: NVCC, the FMI validator stack (cmake, FMPy, Java), wasm-tools, and headless browser/VS Code smoke prerequisites were unavailable in this local environment. Hosted CI is responsible for the corresponding provisioned-tool checks. The coverage gate passed; its non-fatal trim-candidate report remains visible for follow-up and is not described as a coverage-quality proof.

Formal model checking is intentionally narrow. The retained Kani manifest names the production kernel, bounded symbolic domain, property, and counterexample meaning. It proves transactional pre-event history behavior for the production atomic fixed-point kernel; it is not advertised as proof of parsing, typing, tensor lowering, structural balance, code generation, floating-point accuracy, or the general compile-to-correct-simulation theorem.

Specifications and process

The implementation updates the active pipeline, tensor, construction, FMI, GALEC/eFMI, and development-process specs and their normative catalogs. In particular, the specs now define compact root ownership, call-scoped action schedules, checked refresh reuse, sparse projection evidence, automatic integrator selection, comparator-baseline migrations, and the certification claim boundary.

The branch contains 63 chronological, thematically titled commits. Every commit has James Goppert’s DCO sign-off. Four relevant eFMI/GALEC commits credit Pradyunn Kale with the GitHub-recognized Co-authored-by trailer. No commit contains an AI co-author or sign-off trailer.

Reviewer checklist

• Correct-by-construction and tensor-native ownership rules are specified and architecture-gated.
• Unsupported semantics fail closed at their owning phase.
• verify quick and verify full pass locally.
• Every current sim_ok trace is strict-high or a reviewed typed comparison boundary.
• Zero unclassified/actionable counterexamples in the complete local MSL run.
• DCO sign-off is present on all 63 branch commits; Pradyunn is credited on relevant work; no AI trailers.
• Current-tip hosted CI is green.
• At least one approving review and no unresolved conversations.