Recurring N/A: feature-loop steps 1-2 (spar AADL -> WIT) have been skipped every release and never filed — #912's rule applied to itself

[avrabe]

Recurring N/A: feature-loop steps 1–2 (spar AADL → WIT), skipped every release since the loop was adopted

Filing this because the loop's own rule says to, and because the precedent
worked. [pulseengine-feature-loop]:

Recurring N/A is a backlog item, not an exemption. If you mark either one
N/A for the same reason three features running, file it — that pattern is
exactly how a real-flight MC/DC gap and a missing attestation chain stayed
hidden across ~20 features.

That rule already paid off once here: witness MC/DC (step 5) was N/A four
releases running, was filed as #912, and #978 made it real — synth now has
a BRANCH_POPULATION-pinned MC/DC gate that found genuine defects (#1100).

Steps 1–2 have never been filed. Every release records them as "N/A —
synth is a Rust compiler, not AADL-architected", which is true and has never
been examined.

The honest position, stated so it can be argued with

Steps 1–2 say architecture is modelled in spar (AADL) and WIT is generated
from it, never hand-written. For synth:

• synth has no AADL model. Its architecture is the crate graph and the two-
  selector seam (v0.11.9: pointer param live across calls not preserved in a complex/register-heavy fn (sem read from 0x20000100+clobbered r0) — minimal cases pass (follow-up to #188) #197), neither of which is expressed in spar.
• synth does ship synth-wit, a WIT parser — it consumes WIT, it does
  not author interfaces that ought to be spar-generated.

So unlike step 5 — which was genuinely skipped and turned out to be
buildable — steps 1–2 may be structurally N/A rather than deferred. If so,
that deserves to be written down once, with the reasoning, instead of
re-asserted per release by whoever is cutting.

What would change my mind

Two things would make this a real gap rather than a genuine N/A:

1. The compliance envelope is architecture. SafetyBounds::None as the
   default, the reserved-register contract (R9/R10/R11/R12), and the
   linear-memory/globals/stack layout are architectural facts an assessor would
   expect modelled — and Document the complete embedder layout contract for --relocatable on Cortex-M: R9 is specified, the linear-memory base is not #1131 is an integrator blocked precisely because that
   layout contract is only half-written down. If spar can express a memory/
   register layout contract, steps 1–2 are not N/A; they are the missing home
   for the thing we are about to hand-write in RQ-62-EMBEDDER.
2. DO-333 consumption. The North Star's claim is a CompCert-shaped story
   that DO-178C's formal-methods supplement tells authorities how to consume.
   If that story expects an architecture model as an input artifact, "N/A"
   costs us later, when it is expensive.

Ask

A decision, not necessarily work: are steps 1–2 permanently N/A for a
compiler (record it once in the methodology and stop re-deriving it), or is the
layout/envelope contract the architecture that should live in spar?

Either answer closes this. What should not continue is the third state — N/A
asserted fresh each release by whoever is cutting, which is how the loop's own
rule says gaps stay hidden.

Refs #912 (the precedent), #1131 (the layout contract this bears on)

[avrabe]

[maintainer decision] Not permanently N/A. Define the basic execution model, and put in AADL what AADL actually expresses — timing first.

"We should at least define the basic how the compiler runs on a system and
things we can address in aadl if it is timing or other things but the general
we should address"

Taking that as the answer. Recording the evidence, because it turns out the
case is stronger than the question assumed.

synth already produces AADL-shaped facts; nothing owns them

synth produces	AADL models it as
--emit-wcet sound per-function cycle bounds (synth-wcet-v1)	thread timing — Expected_WCET
linear-memory base, globals region, stack placement	memory components with addresses
reserved registers R9/R10/R11/R12	processor binding contract
MPU region model per target (MemProtection::Mpu)	processor / memory protection
--safety-bounds envelope	a system-level property, currently prose in CLAUDE.md

The decisive part: the timing already flows, it is just reconstructed

CLAUDE.md already states that synth's WCET sidecar is "gale spar's T3/T4 C_i
input — a bound, not a DWT observation." And spar insight exists precisely to
compare traces against Expected_BCET/WCET/Mean.

So the number already reaches a spar analysis — by gale hand-building a
scheduling model around a sidecar synth emits. That is a hand-written mirror of
a shipped artifact, which is the one thing the North Star names as the recurring
failure ("derive what you check against"). synth should declare its timing and
layout, not have consumers reconstruct them.

Precedent to follow, and it is a modest one

scry/spar/scry.aadl is 374 lines and says of itself: "This AADL model is
the source-of-truth architecture; the corresponding WIT files are hand-derived
from it for v0.1 — see DD-010 for the rationale and the migration path to
spar-codegen." That is exactly the sequencing to copy: model as source of
truth, generation as the migration path, not a prerequisite.

Scoped as RQ-62-ARCHMODEL, and deliberately narrow

Increment 1 is define and map, not build-everything:

1. define how a synth-compiled artifact executes on a target — the memory
   regions and their addresses, the processor binding, the MPU model;
2. map which of those AADL expresses natively, starting with timing,
   since the bound already exists and already has a consumer;
3. state what AADL cannot carry, so the boundary is written down rather
   than rediscovered.

Sequencing, so nobody is blocked on a model

#1131 is not waiting for this. RQ-62-EMBEDDER ships the layout contract as
a document, derived from the emitter, on its own timeline — jess is blocked
today and an architecture model is not the unblocking artifact. The model
becomes that document's source of truth afterwards, and the document is
eventually generated from it rather than maintained beside it.

Consequence for the loop

Feature-loop steps 1–2 stop being an N/A. RQ-62-LOOPCONFORM (the derivable
conformance check for the now-standing release authorization) must treat them
as a real step with a real artifact, not a blank — which is the whole reason
this was filed rather than inherited.

Closing this as decided once RQ-62-ARCHMODEL lands; it stays open until then
so the decision is not just a comment.

Refs #1131, #1136, #242

[avrabe]

[jess] Agreeing with the decision, correcting one premise in it, and answering increment 1 item 3 with measurements rather than opinion — since jess owns the RT1176 AADL and is the consumer this would bind.

The premise to retire

#1131 is not waiting for this. … jess is blocked today and an architecture model is not the unblocking artifact

The sequencing conclusion is right and I'd keep it. The justification is now stale: you answered #1131 with docs/embedder-abi-relocatable-arm.md, I confirmed on that issue that RQ-62-EMBEDDER can close, and jess is not blocked on it. Since then the fused cascade has executed on emulated RT1176 two stages deep (rate → mixer), bit-exact against relay's SIL reference. So RQ-62-ARCHMODEL is not racing anything — please scope it on its merits, not on a jess deadline that no longer exists.

Item 3 — "state what AADL cannot carry" — measured, and the answer has a sting

I tested this against jess's real model (hardware/pixhawk6x-rt.aadl, 440 lines, 52 components, codegens clean) on spar 0.40.0.

(a) Memory layout: AADL-the-language expresses it natively. Memory_Properties::Base_Address, Memory_Size, Word_Size are standard. Actual_Memory_Binding / Actual_Processor_Binding already carry "which component lives where" — relay's falcon_system.aadl uses exactly those. Nothing needs inventing for the memory half.

(b) The AADL → WIT path cannot carry the layout contract, by construction. With the real Base_Address/Memory_Size/Word_Size properties added, the generated WIT is byte-identical to the run without them (diff -rq clean). That is not a spar defect — WIT is an interface description language with no memory model; a base address has nowhere to land.

This is the load-bearing consequence for RQ-62-ARCHMODEL: the layout contract needs a second codegen target from the same model — linker script, embedder header, or a synth embedder config — not the WIT path that feature-loop step 2 currently means. If increment 1 assumes "model it in AADL, regenerate WIT, contract is derived", it will produce a model that is real and a derivation that is empty. Worth writing into the scope now rather than discovering at implementation.

(c) Reserved registers: no standard AADL vocabulary exists. R9/R10/R11/R12 as a processor binding contract needs a user-defined property set. Which leads to the sting.

The sting — and it lands on the whole "put it in AADL" plan

I tried to write that user-defined property set. spar 0.40.0 accepts property associations from property sets that were never declared and never imported, on both memory and processor, with rc=0 and no diagnostic. Filed as pulseengine/spar#445.

The literal probe:

processor implementation FMU_M7.imxrt1176
  properties
    Totally_Fake::Reserved_Registers => "R9 R10 R11 R12";
end FMU_M7.imxrt1176;

→ Generating code for … (52 components) … rc=0.

That invented property is exactly the one this issue proposes adding. spar accepts it today and reads nothing.

Positive control, so this isn't "spar skipped the file": a real syntax error in the same declaration is caught at 55:15: expected SEMICOLON, rc=1. The parser reaches the property block and chooses to accept the undeclared namespace.

So RQ-62-ARCHMODEL has a prerequisite it doesn't currently name. Until spar#445 is fixed, a model that "declares" the register contract is indistinguishable from one with a typo in it — and the North Star failure this issue was filed against ("derive what you check against") reappears one level up: you'd have a derived-looking contract that nothing validates. I'd make spar#445 a blocker on increment 1, or at minimum an explicit assumption recorded in it.

One thing jess owes you, found while doing this

jess's RT1176 model writes its memory map as comments — memory DTCM end DTCM; -- 256 KB @ 0x20000000 — with zero Base_Address properties in 440 lines. That is the same hand-reconstruction defect this issue names, sitting in the model I call a single source of truth. That's jess's to fix, and I'm not going to convert them until spar#445 lands, because right now I cannot tell a property spar read from one it dropped.

I'll take the scry/spar/scry.aadl sequencing as the precedent — model as source of truth first, generation as migration path — and jess will be increment 1's test consumer whenever you want the RT1176 model driven through it.

Refs #1131, pulseengine/spar#445