Release Rumoca 0.10.0 with checked Solve, GALEC, and FMI 3 pipelines - #340
Open
jgoppert wants to merge 194 commits into
Open
Release Rumoca 0.10.0 with checked Solve, GALEC, and FMI 3 pipelines#340jgoppert wants to merge 194 commits into
jgoppert wants to merge 194 commits into
Conversation
Member
Author
|
Release hardening update at
Focused receipts: both new regressions pass; foreign-product protection passes; packaging transaction tests 13/13 pass; |
MSL Quality Gate SummaryGenerated by
Deltas compare numerator/denominator against the resolved MSL quality baseline. CI Gate SnapshotThese are the baseline-relative MSL stats checked by CI; IC progress is contextual unless simulation successes regress, and speed metrics are informational only.
CI gate details
Package Pass Rates
Per-package pass rates
MLS Contract Coverage
Trace Accuracy vs OMC
Speed vs OMCCompilation and simulation are reported separately for the 131 trace-agreeing models with valid timings on both tools. Aggregate speed summary
Speed breakdownWhere rumoca's time goes
Speed by system sizeTable 1 — Total (model → simulated results)Rumoca = front-end compile + Solve-IR/JIT build + integration; OMC =
Per-model speedup: min 0.34, median 26.87, max 85.01. Table 2 — Compilation (build-to-runnable)Rumoca = front-end compile + Solve-IR/JIT build; OMC =
Per-model speedup: min 1.85, median 35.19, max 86.17. Table 3 — Simulation (integration only)Rumoca =
Per-model speedup: min 0.01, median 3.00, max 38.35. Top 10 slowest modelsTop 10 slowest rumoca compilation modelsTrace-agreeing models ranked by rumoca time.
Top 10 slowest rumoca simulation modelsTrace-agreeing models ranked by rumoca time.
Additional Artifacts
|
jgoppert
force-pushed
the
msl-trace-parity-50
branch
4 times, most recently
from
August 20, 2026 13:52
4e40d23 to
2e28b37
Compare
This was referenced Aug 23, 2026
Establish the repository specifications, contract fixtures, CI workflows, documentation, and developer commands that govern strict compiler phase ownership and reproducible verification. Signed-off-by: James Goppert <james.goppert@gmail.com>
Introduce the common compiler primitives, reference representations, syntax IR, parsing behavior, and AST evaluation needed by the typed lowering pipeline. Signed-off-by: James Goppert <james.goppert@gmail.com>
Resolve scopes and stable identities, validate semantic references, and type-check expressions, components, and functions before structural lowering. Signed-off-by: James Goppert <james.goppert@gmail.com>
Expand component arrays, apply type and connection overrides, and represent instantiated models with explicit flat clocks, expressions, and equations. Signed-off-by: James Goppert <james.goppert@gmail.com>
Compute phase-constant values and lower function bodies, component connections, dimensions, and injected constants into deterministic flat model structures. Signed-off-by: James Goppert <james.goppert@gmail.com>
Lower equations, algorithms, event relations, aliases, and post-processing passes into the complete checked flat model consumed by structural analysis. Signed-off-by: James Goppert <james.goppert@gmail.com>
Build incidence ownership, eliminate structural aliases, scalarize solvable domains, and establish same-tick and causal-definition invariants. Signed-off-by: James Goppert <james.goppert@gmail.com>
Apply index reduction, differentiation, initialization planning, event ownership, and equation reconstruction while preserving structural proofs. Signed-off-by: James Goppert <james.goppert@gmail.com>
Add the valid DAE aggregate, expression vocabulary, discrete state, event metadata, and validation surfaces required by execution and Solve lowering. Signed-off-by: James Goppert <james.goppert@gmail.com>
Derive structural dependencies, expression ownership, function result shapes, and construction inventories before emitting checked DAE programs. Signed-off-by: James Goppert <james.goppert@gmail.com>
Build equations, algorithms, function bodies, variables, clocks, discrete values, and model-event transactions as validated DAE-owned products. Signed-off-by: James Goppert <james.goppert@gmail.com>
Convert typed equations, bindings, conditions, algorithms, start values, runtime precomputation, and scalar metadata into executable DAE form. Signed-off-by: James Goppert <james.goppert@gmail.com>
Remove the superseded GALEC generator surface and introduce the grammar and parsing ownership used by the checked production-code pipeline. Signed-off-by: James Goppert <james.goppert@gmail.com>
Execute DAE expressions, statements, numerical programs, projections, and initialization values through validated runtime access paths. Signed-off-by: James Goppert <james.goppert@gmail.com>
Introduce the Solve model, typed scalar and tensor operations, structural dependency patterns, refresh ownership, and wire validation required by solver backends. Signed-off-by: James Goppert <james.goppert@gmail.com>
Translate derivative right-hand sides, array values, compact tensor operations, scalar expressions, and continuous assignments into checked Solve programs. Signed-off-by: James Goppert <james.goppert@gmail.com>
Preserve typed function calls, statements, clocks, event actions, discrete updates, and call-scoped effects in the executable Solve representation. Signed-off-by: James Goppert <james.goppert@gmail.com>
Complete Solve emission, source mapping, initialization projections, assignment certification, diagnostics, and lowering-specific regression coverage. Signed-off-by: James Goppert <james.goppert@gmail.com>
Construct solver memory layouts, automatic differentiation, stencil evaluation, initial values, implicit equations, runtime assignments, and model-level validation. Signed-off-by: James Goppert <james.goppert@gmail.com>
Prepare and execute typed Solve programs, scalarize compute blocks, derive causal refresh plans, and expose checked runtime evaluation interfaces. Signed-off-by: James Goppert <james.goppert@gmail.com>
Deleting SolveRoundingMode (a9f1fe0) changed a user-visible serde dump: --emit solve-json no longer carries "rounding". On Vehicles.Rdd2.NavigationEstimator the dump goes from 2,347,860 bytes with 1704 "rounding": "nearest_ties_to_even" entries to 2,234,140 with none, and deleting exactly those entries from the old dump reproduces the new one byte for byte, so the change is precisely that and nothing else. No consumer in this repository or its docs reads the field, and --target output is byte-identical, but an IR dump is a surface a downstream tool can be reading, so state it rather than let it surprise someone. Record the schema-bundle sharing in the same entry: galec-production no longer holds a schemas/ directory, which a downstream that vendored that path would notice, while the containers it emits are unchanged. Signed-off-by: James Goppert <jgoppert@cognipilot.com>
The AssetBundle doc pointed at TargetSource::asset_files; the type is TargetBundle, so rustdoc could not resolve the link and the Documentation job would have carried the warning. Signed-off-by: James Goppert <jgoppert@cognipilot.com>
A shared-call node is built from the memo the earlier nodes left, so a nested call in a later node's own argument tree could take an earlier node's result temporary. Nothing recorded that. The lowerer was told which calls were shared only after every node had been built, so a node under construction recorded nothing at all, and what it did record was keyed by the call owner, which collapses when two nodes materialize one owner under two different activations. No node-to-node edge reached the scheduler, the greedy worklist was free to emit the reader first, and it did: the emitted DoStep read a result temporary at a point where nothing had written it. The strict profile reports that as a definite-assignment defect, and where the slot happened to hold the previous tick's value the numbers were merely wrong rather than obviously so. Key the record by the memo entry instead of by the call owner, and write it as each node completes rather than after all of them. A node's entries are the difference between the memo it inherited and the memo it leaves, so nothing inside the materialization has to cooperate and no entry a nested argument lowering produced can be missed. Everything that takes an entry now records the node that wrote THAT entry: a consumer group as before, and now a node under construction as well, which is the edge that was missing. On top of that each node declares a read of every node whose memo it started from, so an inherited entry it takes without a recorded hit is still ordered. Where those edges close a cycle the schedule fails to order and re-lowers without sharing, which is the existing fail-safe. Three further findings from the same review: A node trial that fails to lower now declines the sharing instead of aborting the compile. Sharing is never a reason to refuse a model. A discrete-value owner's `Always` branch is no longer scanned when the owner also has a conditional branch. `compose_discrete_value_branches` emits it as the `else_body` of the when-chain in that case, so it runs on strictly fewer ticks than the domain does and a call it names must not be hoisted anywhere unguarded. The shared-call plan moves out of `clocked_assignments` and the memo it carries moves out of `lower`, which puts every file back under the SPEC_0021 size threshold. Both plan steps now take one context struct, so the argument-count waiver is gone rather than documented. Fixture 17 is the reproducer, built on the shape that fails: `outr(ia)` inside an `if`, `ia` from a call shared at domain entry, and `alt(v)` reading a `v` the `if` writes. It pins the hand-computed closed form, which shares no code with either executing leg, and compiles the emitted unit under the strict profile. The trap needs a node whose arguments are rewritten later in the same tick, which `simulate_dae` refuses as a same-tick discrete loop, so this one fixture is gated on the two executing legs as `LimitSmoke` is. Signed-off-by: James Goppert <james.goppert@gmail.com>
A call written once in the source was re-evaluated at every lowered definition that used it: the RDD2 Bezier trajectory planner performed one tuple call sixteen times per tick. Repeated calls are now materialized once into a scheduled node, under the activation guard or conditional branch they already ran under, so the call executes on exactly the ticks it executed on before. Nodes declare reads of the nodes whose memo entries they take, so a node is ordered after the node whose temporary it reads. Planner: 247,287 to 30,154 executed Cortex-M7 instructions, 6,648 to 3,995 generated C lines, flash 30,050 to 14,860 bytes, with trajectory outputs identical to the previous compiler. Signed-off-by: James Goppert <jgoppert@cognipilot.com>
The dae-modelica emitter rendered string literals with the tojson filter. JSON spells BEL and VT as backslash-u escapes, and the Modelica grammar has no backslash-u escape at all, so a model whose description or unit carried either character was emitted in a form the parser that produced it could not read back. The correct escaper already existed and is what every other string rendering path uses; the emitter now routes through it as a modelica_string filter. Covered by an emit and re-parse round trip over a description carrying bell, vertical tab and tab. Signed-off-by: James Goppert <james.goppert@gmail.com>
A GALEC function leaves its outputs in its own context region and the caller copies each one out. On the Bezier planner that read-back was 74 of the 192 kernel copy calls a tick executes, moving values that already had a home. The C emission now places such an output at the caller's slot. The callee's region holds no storage for it; the callee's entry declares a typed pointer at the destination, the same shape an arena slot already uses, and the caller emits no read-back. GALEC keeps its value semantics throughout: no out parameter is invented, no statement changes, and the `.alg` prints the same bytes. The permission is minted in one expression and carries the whole proof: one call site so the address is unique, a destination that is a plain member of the calling function's own region with the output's exact shape, no actual that can reach it, and a syntactic witness that the callee writes every element. Everything else declines. Planner, one dostep on Cortex-M7 -Os: 30,154 executed instructions to 28,530; 192 kernel copy calls to 146; scratch 2,564 B to 2,468 B; the floating-point mix and the driver's printed line unchanged. Signed-off-by: James Goppert <james.goppert@gmail.com>
The plan decides emitted storage, so its sets and maps now iterate in one order on every run; the generated planner and estimator are byte-identical across repeated runs. Ordering also satisfies the string-hashing gate, which refuses a derived Hash over string-shaped fields. The three-leg harness gains the fixture the placement's whole risk lives in. `stage` calls two identical blends: one assigns its result to a slot no operand names, the other assigns it back over the argument it read. Both bodies read element 1 on every iteration after writing element 1 on the first, so a placement taken on the aliasing call would feed elements 2 and 3 a value the model never computes. The generated C, the GALEC oracle and the Modelica reference agree on every tick, and the emitted unit is checked for the alias declaration on one call and the read-back on the other. Signed-off-by: James Goppert <james.goppert@gmail.com>
A callee writes its placed output through a pointer at a moment neither the arm overlay, nor the value arena, nor the marshalling rewrite can see, so a destination has to be a slot none of the three claimed. The first attempt forced that by withholding the destination from all three. That inverted the trade on the artifact that flies: the RDD2 estimator's scratch grew 20,572 B to 23,044 B, buying copies with storage those mechanisms were saving. Which slots own their storage outright is an output of a projection, not an input to one, so the projection now runs twice where anything is placed: the first pass places nothing and the plan reads its answer, the second emits against it. Nothing is withheld from anything, so every input the callers' own layout is derived from is identical between the passes; that the chosen slot is still a plain member is checked, not assumed, and a mismatch fails the projection. The generated estimator is byte-identical to what it was before this mechanism existed: every candidate there is a slot the arena was already sharing, and all of them decline. The planner keeps its win at 28,614 executed instructions from 30,154, 146 kernel copy calls a tick from 192, and scratch 2,492 B from 2,564 B. A function whose header says outputs may be placed now only says it when one is, so a unit with no placement carries no text about the mechanism. Signed-off-by: James Goppert <james.goppert@gmail.com>
Each shape the witness admits performs exactly one write to the output, so a statement that writes it twice is doing something the coverage argument does not cover: a whole assignment beside a subscripted one, or a second target of the same multi-assignment. Both are now refused rather than reasoned about. Two references also differ when one is reached through a typed pointer and the other is not, which is what `same_reference` means by identical storage spelling; the arena flag joins the two it already compared. Neither changes the planner or the estimator, which is the point: the witness was already tight on both, and this closes the shapes a future model could bring. Signed-off-by: James Goppert <james.goppert@gmail.com>
The middle link of a placement chain names its output nowhere. Its one write was a read-back the inner placement dropped, and every read belongs to the caller, so the pointer it declared was a line no path reached: two of them in the Bezier planner, each an `unused variable` error under the strict assurance profile and, either way, code a reviewer has to account for and cannot. The emission now asks whether the body still spells the output before declaring the pointer, using the same rule the template prints by: a result whose read-back is dropped is not a mention. The placement itself is unaffected, because a link that names its output nowhere contributes nothing but the pass-through it already performs. Planner: 4,009 C lines from 4,019, and the emitted unit has no unused declaration left. Every other measure is unchanged. Signed-off-by: James Goppert <james.goppert@gmail.com>
The gate decided deadness by counting bare identifiers over the whole workspace and reporting only names whose total count was exactly one. Any `pub` item whose bare name collided with any other identifier anywhere was therefore exempt, and the hole was live: `PhaseResult::is_success` was excused by `InstantiationOutcome::is_success`, `OptModel::set_parameter_value` by the sim one, `Rk45Session::set_inputs` by `SimulationSession::set_inputs`, and `rumoca_phase_parse::parse_file` by roughly fifteen `syn::parse_file` calls in the test suites. None of the five had a caller. Resolve instead by declaration identity, `(crate, module path, name)`: two crates that both name something `helpers` must not vouch for each other. A name is recorded from the constructs that can actually reach a declaration (paths, `use` trees, method calls, macro token streams) rather than from a bare ident visit, so a struct field named like its accessor no longer keeps the accessor alive. `spec/` and `docs/` leave the usage corpus, because a mnemonic in a specification table is prose about the code and not a caller of it, and an item an FFI attribute hands to a non-Rust caller is exempt by construction since no Rust reference can resolve to it. Disposing of what the audit finds at this commit: of eighteen reported items, sixteen are deleted and two stay, recorded as contracts SPEC_0041 names as crate-owned. The exemption dies with the row that grants it. Two further deletions came out of that work by hand: `Session::all_class_names_cached`, whose only caller was the deleted snapshot wrapper, and `PhaseResult::needs_inner`, which the resolver still misses because a local binding of that name is written in the same crate. Codegen is byte-identical. MLS N/A: repository verification gate. Signed-off-by: James Goppert <james.goppert@gmail.com>
SPEC_0008 states that a warning MUST NOT be minted in an `E` range, with `ES001`/`ES002` recorded as the only sanctioned drift, and AST constant evaluation was minting `ET006` and `ET007` through `emit_warning`. The gate missed both twice over: it recognized two call spellings, `structural_warning` and `CommonDiagnostic::warning`, and it read only the files a hand-kept registry list named, which does not name this phase. A warning minted in a phase nobody remembered to list is exactly the violation the property exists to catch, so the list was the wrong instrument. Rename the two to `WT006`/`WT007`, give `WT0xx` its own row in the SPEC_0008 range table alongside the `WT003` variability warning already shipping there, and update the three typecheck assertions that name them. Then widen the gate so it cannot go blind the same way again: * the mnemonic is read from any call whose name ends in `warning(`, so a helper the workspace adds tomorrow is recognized the moment it is named for what it does, and the two narrow readers collapse into one; * the corpus is every crate's `src` tree rather than a list of files, read through the totality scan's production filter so a comment about a mint and a `#[cfg(test)]` fixture that performs one answer nothing about shipped code. That filter gains a policy for keeping string-literal text, with the punctuation that shapes an item removed from it so a brace in a format string still cannot move the item scan; * the scan is held to still see: canaries assert that each recognized spelling is still read, and that the workspace scan still finds mnemonics the shipped tree really mints. A text scan that quietly matches nothing reports a clean workspace while a violation ships, which is worse than having no scan at all; * a mnemonic-named constant must hold the mnemonic it names, since the scan reads the name and the compiler ships the value; * the double-mint check runs over every registry rather than instantiate alone, with `EI001`'s two presentation variants recorded as the one deliberate sharing. Restoring `ET006`/`ET007` makes the new gate fail and names the file. Codegen is byte-identical. MLS N/A: repository verification gate. Signed-off-by: James Goppert <james.goppert@gmail.com>
`uses_scratch` decides whether a body declares its region alias, and it was set while PROJECTING a reference rather than while printing one. A call target whose result the placement delivers directly is still projected, because the checked Algorithm Code still spells the assignment and `model.alg` still prints it, but the read-back that named it is gone. In a thin wrapper that read-back is the only emitted use of the region, so the alias became a declaration nothing reads: an `unused variable` error under the profile every GALEC C product is preflighted with, and an unreachable declaration a structural-coverage argument has to account for either way. The projection now asks the same question about a call target that the emission already asks about a callee's own output, through one shared predicate. The RDD2 artifacts never showed it because their regions all hold other live members. The wrapper shape is a permanent three-leg fixture now, and it is load-bearing: with the suppression mutated out it fails on the harness's own strict compile. Signed-off-by: James Goppert <james.goppert@gmail.com>
The liveness walk answered "this body names the output" for every branch guarded by a signal check, for every output. That was written as the safe direction and it was, until the walk started deciding whether to DECLARE a destination pointer: a wrong "named" now emits a declaration no path reaches, which the assurance profile reports as an unused variable. A signal check tests signals, and its only expression is the optional `or expr` fallback, so the walk reads that and neither guess is needed. Nothing in the GALEC phase constructs a signal check today, so no emitted artifact moves. Signed-off-by: James Goppert <james.goppert@gmail.com>
A callee that reads its own output before writing it reads persistent storage either way, but not the SAME storage: without a placement it reads what its own previous activation left there, and with one it reads the caller's destination, which the caller may have written in between. The theorem's value-preservation argument depends on that never happening and never said so. The front end already refuses such a body with ED019, so no artifact moves. The witness checks it anyway: a proof that leans on another phase's diagnostic without naming it stops holding the moment that phase changes, and silently. Signed-off-by: James Goppert <james.goppert@gmail.com>
The destination pointer adopts its destination's final extents, which is sound for the one difference the bound equalization can introduce: a wider LEADING extent moves no element, because it is not a stride. A different rank or element type is different address arithmetic, and the pointer would have carried it silently into the artifact. Nothing emits that today. A future pass that did now meets a diagnostic instead, beside the membership check that was already there. Signed-off-by: James Goppert <james.goppert@gmail.com>
An adversarial review found the refusal unreachable by mutation and argued it redundant: a descendant's formal can alias an ancestor slot only if that slot was passed at the very call whose result lands there, which the by-name operand check already refuses. The argument is believable, and it is also an inductive claim about everything a formal can alias across the whole call graph, which is the reasoning this calling convention exists to avoid having to get right. The refusal stays, and what it costs is written down beside it: 20 read-back copies a tick on the Bezier planner, about 0.7 percent of the step. Retire it against evidence, not against the argument. Signed-off-by: James Goppert <james.goppert@gmail.com>
Real comparisons signal, so a guard is not a pure test: it writes ErrorSignalStatus. Two measured optimizations are blocked on the claim that evaluating such a guard N times and once produce the same word, and nobody had established it. State it as SPEC_0034 GAL-040 rather than assume it. The word is cleared exactly once on entry to each method, every other emitted write is a bitwise OR of a constant mask, and nothing reads it, so inside one method the final word depends on the SET of raising evaluations, never on their count or order. The rule also names what breaks it: a signal check catches, clearing the bits it tests, so the monotone argument holds only between a method's reset and its first check, and an optimization may never make a raise reachable that the source form did not. Enforce it two ways, per D1 and D2 of the architecture decision record. rumoca_ir_galec::signal_effect classifies every expression, condition and statement over exhaustive matches, so a construct added to the AST cannot be silently treated as safe; RepeatableSignalEffect is a branded token whose field is private to that module and whose only constructor is a proof. The classification is a claim about emitted C, which no Rust type constrains, so galec_c_error_signal.rs scans both the template source and rendered C and accepts only a reset, an OR with a decimal-literal mask, a declaration, or an address handed to a helper the same scan covers. The template scan is the one that catches a kernel no fixture exercises: injecting `*status = UINT32_C(4)` into the unrendered compare_lt kernel fails it while the rendered scan stays green. SPEC_0034 stood at 2,491 of its 2,500-word budget, so the new rule needs room. Move the two lookup tables that are catalog material by SPEC_0000 section 3, the variable-classification table and the checked-construction-scope table, into SPEC_0042 section 5 alongside the GAL-040 rationale, and cite them as normative by reference exactly as the language traps already are. SPEC_0034 ends at 2,472 words, below where it started. Signed-off-by: James Goppert <jgoppert@cognipilot.com>
An array actual that is not a whole-aggregate copy is staged element by element, and when the element value came from a conditional every element carries the same test. On Planning.Bezier.WaypointTrajectoryPlanner twelve such nests evaluated the plan-acceptance guard 269 times per tick, at nineteen Cortex-M7 instructions each; the guard mentions no iterator, so 257 of those evaluations recomputed bits that could not have changed. fuse_guarded_tensor_loop does not reach this: it PAIRS an already-hoisted prefix guard with a matching body guard, and here nothing was hoisted because the conditional's arms are entirely index-dependent. Bind the condition to a Boolean ahead of the nest instead, and let the nest test the Boolean. The rewrite is gated on a token, not a predicate. HoistableGuard::prove discharges four obligations before it will mint one: the condition is an expression and not a signal check, it is worth binding, it mentions no iterator and no name the body assigns, and it holds no call. It then requires GAL-040's RepeatableSignalEffect on top. The nest is refused outright if any body statement classifies Consume or Opaque, and if any axis could run zero times: hoisting out of a possibly-empty loop would raise on an execution that raised nothing, which is the one clause that makes the status word identical rather than merely equivalent. The token owns the expression it was minted against and is consumed by the rewrite, so there is no second look and no assertion. Measured on the planner from mm-base, driver output byte-identical: guard evaluations 322 to 62 per tick, and 269 to 0 inside staging nests; executed instructions on the guard lines 6,179 to 1,272, and 43,927 against 48,076 over the whole model translation unit. Flash grows 392 bytes. Vehicles.Rdd2.NavigationEstimator is byte-identical: its NaN guards are index-dependent, so the rewrite correctly declines there. Fixture 18 is the evidence for the contract, not for the speed. Its staged guard is `zeroGain / zeroGain > 1.0`, which raises NAN whenever it runs, so the per-tick ErrorSignalStatus word records whether the guard ran at all that tick. The nest sits inside `if ticks > 2.5`, so the pinned word [0,0,4,4,4] would catch a guard lifted out of THAT. Ablating the rewrite and re-running the fixture leaves every status and value assertion passing and fails only the shape assertion, which is the measurement the contract predicts. Signed-off-by: James Goppert <jgoppert@cognipilot.com>
Argument-staging loop nests re-evaluated a loop-invariant guard once per element: the Bezier trajectory planner evaluated its plan-acceptance guard 269 times per tick inside staging nests alone. Binding the guard to a Boolean ahead of the nest is only sound if repeating a guard is unobservable, which nobody had established, so the accumulation contract is now written down as SPEC_0034 GAL-040 and enforced by a branded permission plus a scan of both the kernel template and the rendered C. Guard evaluations per tick fall from 322 to 62, and the instructions those lines execute from 6,179 to 1,272, with outputs identical.
Two workspace lint budgets, both tripped by the last two changes: the leading-extent comparison nested a conditional inside a closure inside a call, and routing an assignment's target through the call-target rule pushed the statement projection past its line budget. Both are now named functions saying what they decide. No emitted artifact moves. Signed-off-by: James Goppert <james.goppert@gmail.com>
A callee wrote its array output into its own scratch region and the caller copied the result out, so every call paid a full read-back traversal. A callee's output slot may now live in a slot the caller already owns, reached through a typed pointer the callee declares, and the read-back is not emitted at all. The C signature is unchanged and no out parameter is introduced: out pointers were removed here once before because a callee writing a caller object during its body corrupts an operand that aliases it, and that reason still stands. Placement is minted only by a proof discharging single call site, caller ownership, disjointness from every operand, a total write, no self read, injectivity, reentrant addressing, and chain resolution. Declining costs one copy and nothing else. Planner: 192 to 146 kernel copy calls a tick, State 4,360 to 4,288 bytes. Controller: overlay groups 6 to 5, State 1,632 to 1,588 bytes. Outputs identical on both, and the flight estimator is byte-identical. Signed-off-by: James Goppert <james.goppert@gmail.com>
The compiler had no way to say how much of a model's structure the emitted C should keep. `GalecOptions` carried one field, every caller built it with `::default()`, and `lower_algorithm_code` hardcoded that default, so no CLI flag could reach the projection even in principle. Add the two axes, and keep them two, because they differ in kind and not in degree. Inlining changes CALL structure and is information-preserving: an inlined contraction is still a contraction, its shape and index sets arrive intact, and no floating-point operation is reordered. Scalarization changes DATA structure and is information-destroying: index sets, symmetry, bandedness and tensor identity are gone the moment a contraction becomes N statements, and only a recognizer guessing at emitted shapes can pretend to get them back. So `--inline-policy none|annotated|cost-model|all` defaults to `cost-model` and never taints the artifact, while `--scalarize-policy never|cost-model|all` defaults to `never` and taints at every other setting. A single dial would have made the one combination this compiler is uniquely able to emit, inlined code that keeps its tensors, unaskable. `--emission-policy reviewable|balanced|flat` survives as shorthand over the pair and is never the only way to name a point. Expansion is not implemented. Asking for it is refused by name rather than silently ignored: a no-op there would emit structured code under a header claiming a tradeoff the compiler never made. `--inline-policy none --scalarize-policy never` is today's compiler exactly. Verified on Planning.Bezier.WaypointTrajectoryPlanner, Vehicles.Rdd2.GuidanceController (embedded-c-galec) and Vehicles.Rdd2.NavigationEstimator (galec-production): all 65 generated files byte-identical, masking only the container UUIDs, the generation timestamp and the SHA-1s derived from them, which differ run to run at HEAD as well. At this commit the default differs from that baseline by the disclosure header and nothing else. Every emitted block that collapsed or expanded anything states both axes and whether it is still eligible for the certification path. Nothing is emitted when nothing was collapsed or expanded: the absence of that notice IS the statement that the emitted functions are the model's functions and the emitted tensor operations are the model's tensor operations. Two shapes fell out of the threading rather than being sought. The five facts every block-lowering step reads (the DAE view, its causal definitions, the classified variables, the `pre()` names, and now the policy) became `BlockLowering`, because a step holding four of them cannot build an `ExpressionLowerer` and every one of these steps builds one; four functions that would otherwise have crossed the argument limit now take fewer arguments than before. `dependent_assignment` moved next to its only caller, and the clap-facing emission selectors moved out of `cli.rs`, both to stay under the SPEC_0021 file-size threshold. Signed-off-by: James Goppert <jgoppert@cognipilot.com>
An `if`/`elseif` chain in a clocked algorithm reaches the checked DAE twice over: as one guarded definition per branch, and as one n-ary conditional per value that reads what the chain assigned. The guarded shared-call node already evaluated a repeated call once for the definitions, but the conditional's branch evaluated it again, because a memo entry is admitted only where the guard facts it was emitted under hold again and a guarded node states its guard as an emitted `if` rather than as a fact. Where the node's guard IS one branch's selection, the fact does exist and it is exactly that branch. The DAE builds a branch guard and a conditional's branch condition from the identical expression identities, so the proof is a literal-set comparison and not a decision procedure: the guard has to be a conjunction of predicates over those expressions plus this domain's own clock, and its positive and negative literals have to be exactly `c_k` and `not c_0 .. not c_(k-1)`. The node's entries are then published a second time under that branch's activation key, and `dominates` admits them inside the branch and nowhere else. Each alias is attributed to the node that wrote the temporaries, so a consumer taking one still declares the schedule edge that keeps the node ahead of it. Declining is free and three cases take it: an entry that already carries a guard fact of its own, a branch whose own conditions evaluate the same call owner, since the branch key is pushed for the condition too and the condition runs before its branch is selected, and a key some earlier node already published. `Ekf2.DifferentialStep` emitted its one source `predictStep` tuple call at three call sites and now emits one: 64,282 to 26,139 executed Cortex-M7 instructions per predict dostep at -Os on the corrected instrument, FLOP equivalent 6,552 to 2,184, block state unchanged at 29,048 bytes. Outputs are bit-identical over a differential driver covering all four branches of the block. The flight estimator and the Bezier planner emit byte-identical C. Signed-off-by: James Goppert <james.goppert@gmail.com>
Fixture 22 is the shape the branch alias opens: an `if`/`elseif` chain whose three definitions share one guarded node, and one value that reads what the chain assigned. Only one value reads it, so nothing in that branch looks repeated and fixture 16's conditional-branch node does not fire; what removes the second evaluation is the proof that the node's guard IS this branch's selection. The shared function raises NAN on every call, so the compared `ErrorSignalStatus` word is a per-tick record of the ticks it ran on: the branch is unselected on ticks 1 and 2, and temporaries taken where the guard had not held would either raise NAN there or hand back a stale slot. All three legs agree tick for tick, the emitted unit compiles under the strict profile, and the DoStep is pinned to one call site standing inside its guard. Without the compiler change that count is two. Signed-off-by: James Goppert <james.goppert@gmail.com>
A tuple call written once was still evaluated three times in the Ekf2 covariance block: twice through guarded state definitions and once more inside a conditional branch that the same guard selects. The guard and the branch condition are the same expression identities, so a node emitted under the guard runs on exactly the ticks the branch is reached, and the branch may be served from it. The alias is published only when the guard normalises to the branch's own selection, and declines otherwise. Ekf2 predict step: three call sites to one, 64,282 to 26,139 executed Cortex-M7 instructions, flop-equivalent exactly one third, outputs bit identical over all four branch selections. The flight estimator and the trajectory planner emit byte-identical C.
`annotation(Inline = true)`, `Inline = false` and `LateInline = true` are MLS §18.3 and are the spec-grounded way a model author states, per function, whether a call should disappear. The parser read them into an untyped `Vec<Expression>` and every later phase dropped them; a repository-wide search for `"Inline"` in `crates/*/src/` returned nothing. Carry the request from the declaration that wrote it: `InlineAnnotation` on `rumoca_core::Function`, filled where `derivative` annotations are already read, through `FunctionSignature::with_inline` onto the checked DAE function, and out through `FunctionView::inline`. Reading it late is not an option: by the time a backend decides, the annotation expressions are gone, and a compiler that has to guess the author's intent is a compiler that ignores it. Substituting a body is then a decision with an order of authority. `Inline = false` refuses at every setting, because a refusal a compiler flag can override is not a refusal. Legality refuses next: a callee already being expanded at this site would expand forever, and a callee returning a tensor would be lowered one element at a time, which is scalarization by another route and is what the scalarization axis declines. Only then does `--inline-policy` decide, from `annotated` upward. The tensor refusal is measured, not assumed. Substituting aggregate results took the RDD2 trajectory planner's emitted translation unit from 4,033 lines to 136,464 and its compile from one second to thirty-one, because each element of each result re-lowered the callee's defining expression. It is also why inlining does not yet close the working-memory gap against a flat generator: the chain holding the flight estimator's residual scratch live is a chain of matrix-returning callees, and every one of them is refused here. Collapsing those needs an inliner that splices the callee's statements, loop nests included, which keeps the tensors AND removes the boundary. Declining is free, so it is free at every step. The substitution runs on a clone of the lowerer: a body that cannot be substituted leaves no temporary, no cached value, no emitted statement and no recorded call behind, and the call the ABI can always represent is emitted instead. Traceability survives the transform rather than being traded for it. The selected output is lowered through its own function-value definition instead of through the bare right-hand side, so the emitted statement carries the CALLEE's span rather than the call site's: without this, inlining `MathUtilities.clip` removed `clip.mo` from the guidance controller's trace legend entirely. The local that holds the value is named after the whole chain of callees it was substituted through, the callee value it realizes, and the call it replaced, so a temporary that used to read `rumoca.tmp.<ns>.<callee>.<result>.call<n>` does not become a counter. `--inline-policy none --scalarize-policy never` stays byte-identical to a build with no dial: all 65 generated files across the two flight controllers and the flight estimator, under the same mask for container UUIDs and timestamps. Signed-off-by: James Goppert <jgoppert@cognipilot.com>
This is the cost model's first rule and the only one that needs no tuning. A callee with one call site has nothing to duplicate: the body moves rather than being copied, so there is no flash to trade, and what it removes is unconditional, namely the argument staging and result read-back at that boundary and one edge of the call chain that the storage overlay refuses to let a caller and a callee share. The rule is not a heuristic; it is the statement that a boundary crossed once buys nothing. The census is counted once per projection over the expression arena and keyed by the construction-issued call OWNER, never by the expression: one source call to a four-result function reaches lowering as many scalar projections of one owner, and counting projections would make every multi-result call look duplicated when it is not. It covers the whole DAE rather than one block, which is the conservative direction. Two corrections to the surface land with it. The flag defaults are now `--inline-policy none` and `--scalarize-policy never`, so passing no flag emits what a compiler with no dial emits. The cost model acts under `--emission-policy balanced` or an explicit `--inline-policy cost-model`, never silently: a structural decision is taken deliberately or not at all. Verified again on the two flight controllers and the flight estimator: all 65 generated files byte-identical to a build without the dial, with no flag, with `--emission-policy reviewable`, and with the two axes named explicitly. An eFMI container target now refuses a policy that would reshape it. A container ships AlgorithmCode as the reviewable semantic reference and ProductionCode as its optimized C, and this compiler renders both from one projection, so a policy that collapses call structure would collapse it in the reference too. Refusing names what is being protected; silently dropping the flag would hand back an artifact that does not match the request. The transform's end-state home is the GALEC-to-Solve refinement, where the two representations can legitimately diverge, and both the refusal and the module header record that as relocation debt rather than a settled location. Every emitted block that collapsed anything now states its budget in the units the settings act on: emitted statements, emitted functions, and working memory against the floor any sound overlay of the same regions could reach. MEASURED, and the headline is a negative result worth having. On the trajectory planner the rule fires nowhere at all (58 emitted functions, 48,039 executed instructions per tick, 15,012 B of ARM -Os .text, and 2,492 B of scratch, all unchanged); on the guidance controller and the flight estimator it collapses four and eight functions and moves working memory by ZERO bytes (604 B and 20,572 B, identical), while the estimator's .text GROWS 820 bytes. The reason is structural, not a tuning failure. This projection substitutes EXPRESSIONS, so a callee returning a tensor would be lowered one element at a time, which is scalarization by another route and is refused. The chain that holds the estimator's 20,572 B of scratch live is a chain of matrix-returning callees, so every member of it is refused, and inlining as implemented recovers none of the working-memory gap against a flat generator. Closing that gap needs an inliner that splices the callee's STATEMENTS, loop nests included, which keeps the tensors AND removes the boundary. Pushing the existing mechanism harder goes the wrong way: `--inline-policy all` on the planner doubles the executed instructions to 94,824 and nearly triples .text to 43,546 B while still freeing no memory. Outputs are unchanged at every setting. The planner driver prints `t=1.200 seg=1 pos=2.4054 -0.2177 2.0000 vel=3.5856 acc=-2.7648 jerk=-15.8400 snap=40.7999 yaw=0.1944` byte for byte under `none`, `cost-model` and `all`. Traceability is checked rather than asserted: every anchor the structured artifact carries survives substituting every legal call, except the spans of the call expressions that no longer exist, and each of those losses is checked to name a model line that writes one of the substituted calls. Naming those call sites in the artifact is the inline-chain breadcrumb D6 asks for; the GALEC statement carries a span and no annotation channel, so it is not emitted yet and is owed. Signed-off-by: James Goppert <jgoppert@cognipilot.com>
Function inlining and array scalarization differ in kind: inlining changes call structure and preserves every tensor fact, scalarization destroys index sets and structure and can only be undone by a recognizer. They are therefore independent flags, --inline-policy (none, annotated, cost-model, all) and --scalarize-policy (never, and refused otherwise), with the certifiable defaults emitting today's exact bytes and every block disclosing the policy it was built under. Modelica's standard Inline and LateInline annotations are honored, with Inline=false absolute. Measured: expression substitution cannot recover the call-chain working memory, because a tensor-returning callee would be lowered element by element, which is scalarization by another route and is refused. Closing that axis needs a statement-splicing inliner in the GALEC to Solve refinement, where the transform's home is recorded.
dougdew64
added a commit
to dougdew64/rumoca
that referenced
this pull request
Sep 4, 2026
…ng the fix Doug ruled: do not fix the initialization defect in the fork, wait for the release. That was in the conversation only, so a fresh session reading the Current work box would have found a located defect with a scoped fix and proposed it again. The box now carries the ruling and the reason it is not caution — 0.10.0 already contains initial_pins.rs, whose doc describes the exact formulation this project derived, and has deleted the der-to-zero arm. Also corrects the box's implicit premise. Upstream is not abandoned; it is mid-release, which reads identically from outside: main last moved 2026-07-29 and outreach went unanswered, while PR CogniPilot#340 (194 commits, 2,377 files) was updated 2026-08-27. The work waits on git fetch, not on a person. DECISIONS.md records the CLAUDE.md backup hazard, because the instinct behind it was sound and will recur. A copy in a parent directory is auto-loaded as authority rather than sitting inertly beside the original, and repos/ is not a git repo so nothing tracked it. Measured cost from ad1856b..HEAD: nothing superseded, but one rule added 2026-09-02 was invisible for a session — answer through HRW when HRW can show it — which is that rule's own documented failure mode, silent. A backup of a tracked file is redundant with git; the pre-maintenance text was read out of ad1856b. Use a tag. Fast gate: 874 passed. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
This release candidate advances Rumoca to 0.10.0 and completes the checked compiler path needed by current Modelica flight-control consumers.
The branch is a linear 31-commit series directly on public main. It replaces intermediate development history with semantic commits covering the IR, Solve construction and evaluation, generated targets, runtime behavior, regression evidence, and the final version update.
Major user-visible outcomes:
Specification alignment
The implementation was reviewed against:
RDD2 integration evidence
The consolidated compiler exported the west-pinned RDD2 Plant as FMI 3 source, compiled the generated C under strict C99 warnings-as-errors, executed a 32-second co-simulation run, preserved invalid-parameter assertion failure, and passed the landing-contact runner.
Generated RDD2 Guidance and Navigation artifacts also compiled with their shared kernel translation unit under strict warnings. Focused runtime probes produced finite, status-zero guidance outputs with discriminating position-mode thrust and accepted the nominal GPS and optical-flow corrections in Navigation.
These receipts establish the compiler capability used by the downstream flight branch. They do not replace downstream firmware, FastDyn, or hardware qualification.
Risk and design notes
This is a large compiler-architecture change. The principal correctness risk is a mismatch between checked producer ownership and a later scalar or generated-code view. The series addresses that risk with construction-time certificates, earliest-layer fixes, strict target rejection, generated-runtime discriminators, and adversarial model probes.
The principal maintenance risk is the breadth of target and runtime surfaces. Shared typed programs and shared generated kernels reduce duplicated lowering, while target-specific checks remain fail-closed.
No superseded internal compatibility reader, optional legacy eFMI path, or silent capability fallback is introduced.
Verification
Completed on the final source content before the version-only 0.10.0 metadata commit:
The broad full run reached the documentation stage after its earlier build, test, and coverage work; it stopped on the two rustdoc links. The focused documentation rerun passed after the fix. Per the flight-release schedule, the complete full command was not restarted from zero on commit 030fc05; CI is the final aggregate gate for this PR.
History and release