feature: the complete wasm stack composes and RUNS — flight-app + gust-hal-stub close the DD-026 seam (AFD-043 -> AFD-044) - #191
Merged
Conversation
…rts no gust:os, so the DD-026 seam has nothing to plug (AFD-043, jess-owned)
Prompted by a direct question jess could not answer honestly: "have you worked to have this
integrated with gale to build the complete wasm stack". The answer was NO — and checking revealed
it is not merely undone but currently IMPOSSIBLE with what is published.
DD-026 pins: "The flight app IMPORTS gust:os; gale's OCI component EXPORTS it; composition happens
ALONG gust:os". That is not what ships.
MEASURED:
falcon rate@1.134.1 imports pulseengine:falcon-cascade/types (TYPE-ONLY); gust: refs = 0
falcon flight imports: NONE
fused cascade core imports: 0
gale-nano 0.7.0 exports gust:os/{time,log,spawn,exec,timer}; imports gust:hal/mmio + taskdisp
EMPIRICAL: `wac plug rate.wasm --plug gale-nano.wasm` fails — "the socket component had no matching
imports for the plugs that were provided". The halves are disjoint.
NEITHER SUPPLIER IS WRONG. falcon being a pure computation library with zero OS dependency is why it
self-contains and reached 5/5 on both flight cores. gale-nano exporting gust:os is its contract.
What is missing is the piece BETWEEN them: a flight APPLICATION component importing gust:os
(scheduling/time), importing the cascade, exporting an entry the runtime starts. Today nothing calls
the cascade on a schedule — the lowered image blx'es one export at reset and spins.
OWNERSHIP SETTLED: this mapping is JESS'S — we own integration under DD-026. Asked gale on #223 for
the intended SHAPE of the gust:os side (which interface drives a periodic loop under DD-025's
ARINC-653 outer scheduler; whether there is a canonical app world; who provides taskdisp; which way
round the wac plug goes) rather than inventing it and having everyone build against a guess.
Second missing piece, also jess-owned: gust:hal read32/write32, gale-nano's residual. The stack needs
BOTH before "complete" means anything.
Status open — a live gap with jess as owner, not a resolved finding.
rivet validate PASS.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…ured warnings that change jess's partition sizing
gale's answer to the four questions, recorded on AFD-043:
METHOD CORRECTION: use `wac compose` with a WAC script, NOT `wac plug`. jess's error had a cause
unrelated to the components — a plug result exports only the SOCKET's exports, and plug wires plugs
into the socket's imports only, never plug->plug. So plug can never produce a composite exporting
five capabilities from five components. gale hit this themselves and moved off plug.
CANONICAL WORLD: `world app` — imports time/log/spawn/channel/io/timer, exports `run: func() -> u32`,
the entry the runtime calls. Examples app-time / app-tl / app-ts (closest to us). gale volunteered
that `world app-timer` is declared but UNIMPLEMENTED — building the first is new ground.
taskdisp IS JESS'S alongside gust:hal — one function, poll-task(id)->u32 — and it is ENFORCED: the
fused build gates the residual to exactly gust:hal/* + gust:os/taskdisp. The gate also REJECTS a
gust:sched/* residual, which would mean spawn/timer were never bound to the one executor.
TWO MEASURED WARNINGS THAT CHANGE OUR PARTITION SIZING (DD-025):
(i) do NOT size a budget from a DWT high-water mark — T4 static WCET bounds only 3 of 31 functions
(scry#144 loop-bound inference). An observed budget is an observation, not a bound.
(ii) THE SWITCH COSTS A TICK PER WINDOW — Switcher::tick fires at offset+budget-1, so a partition
owning k windows receives Theta-k, NOT Theta. Sizing against the raw budget is UNSOUND,
machine-checked in Lean, first violation t=2560 (one window) / t=828 (three). A 1 kHz loop sized
that way 'will look fine in short tests and fail later'. This directly constrains the
two-partition MPU split jess was designing.
STILL OPEN, and gale says so: timer-ISR vs partition-window for driving poll-round. gale asked jess to
report which way the integration forces it, as DD-025 evidence.
rivet validate PASS.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…built from the SHIPPED artifacts
AFD-043 identified the missing piece: falcon imports no gust:os, gale-nano exports it, nothing
connected them. jess owns integration under DD-026, so this world is jess's to define. gale supplied
the shape on gale#223.
THE MAPPING (wit/flight-app/world.wit) — resolves clean, negative-controlled:
world app
import gust:os/time, gust:os/spawn (gale runtime, DD-026 layer i)
import pulseengine:falcon-cascade/{types,rate,mixer} (relay data seams, layer ii)
export run: func() -> u32 (gale's canonical entry)
EVERY DEPENDENCY EXTRACTED FROM THE SHIPPED WASM, not a repo copy — the artifact is the contract, and
a repo copy can drift from what shipped. (gale's wit-os/ paths also 404, but that is the weaker reason.)
THE FALCON PACKAGE HAD TO BE RECONSTRUCTED: each component ships a TREE-SHAKEN types interface
carrying only the records it uses, so the complete type set exists in NO SINGLE COMPONENT. A naive
merge fails with "name 'imu-sample' is not defined" — the ekf interface references a record only
iekf's copy defines. The package here is the UNION of all five, the only form that parses.
imu-sample is the raw-IMU seam jess specified on jess#167 and relay adopted; it appears as shipped
(ax ay az gx gy gz).
CAPABILITY SUBSET IS DELIBERATE: follows gale's WORKING app-ts (time + spawn), not the full app
world. gale volunteered that app-timer is DECLARED BUT UNIMPLEMENTED, and the periodicity design it
serves (timer-ISR vs partition-window) is explicitly UNSETTLED. This rung proves the seam composes;
periodicity waits for that question to have evidence.
Verified: world resolves (exit 0, all five imports bound); negative control — a bogus import errors
"interface not found in package", so resolution is real not permissive. rivet validate PASS.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…'s derivation gate caught it correctly The WIT-derivation gate failed on the previous commit: WIT-DERIVATION DRIFT — wit/ is stale or hand-edited; run tools/wit/regen.sh Only in .../wit: flight-app That gate is right. `wit/` is spar codegen from hardware/pixhawk6x-rt.aadl and CI asserts `wit/ == spar codegen` so a hand-edit cannot masquerade as generated output. The flight-app world is legitimately hand-authored — it describes a COMPOSITION, not the hardware architecture — so it does not belong in that tree. Fixed by moving the file, NOT by loosening the gate. The repo now has three WIT trees with distinct provenance and rules, documented in wit-app/README.md: wit/ spar codegen from the AADL — never hand-edited, CI-gated wit-deps/ extracted from shipped supplier .wasm — never hand-edited, re-extract instead wit-app/ authored by jess — the integration surface jess owns Verified: tools/wit/regen.sh --check now reports WIT-DERIVATION OK; the world still resolves from its new location; rivet validate PASS. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…ules_wasm_component#626) rules_wasm_component filed #627 for the single-component wit_from_component case but explicitly DECLINED the union case, because "the failure mode of getting it subtly wrong is silent data loss, not a build error" — and asked jess to contribute its working version. That caution landed on jess: the earlier ad-hoc merge used dict.setdefault, which keeps the FIRST definition and silently discards a differing one. Exactly the flaw they warned about. MEASURED EXPOSURE — it was luck, not safety: 4 of 7 falcon-cascade records are defined in MORE THAN ONE component (attitude-setpoint, rate-setpoint, torque-setpoint, vehicle-state). All four are currently byte-identical, so setdefault produced correct output. It would not have stayed lucky. tools/wit/merge_component_wit.py implements the semantics rules_wasm_component named: interfaces union by name type defs union by name identical duplicate -> keep one DIFFERING duplicate -> HARD ERROR, never resolved silently Comparison is on whitespace-normalised bodies so cosmetic formatting differences between extractions do not raise a false conflict. --self-test is a NEGATIVE CONTROL, not a claim — it proves the conflict path fires: identical definitions -> merged cleanly (expected clean) PASS whitespace-only difference -> merged cleanly (expected clean) PASS REAL conflict (f32 vs f64) -> conflict raised (expected conflict) PASS wit-deps/falcon/pulseengine-falcon-cascade.wit is now REGENERATED BY THIS TOOL rather than by an inline script, and the flight-app world still resolves against it. rivet validate PASS. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…needs the user's go-ahead) hardware/silicon/rt1176-blhost/sig.S is the H1 "does the silicon execute our code at all" probe: blhost write-memory into OCRAM, blhost call, blhost read-memory back. It is deliberately a normal thumb function ending in `bx lr` rather than a spin loop, because blhost `call` RETURNS to the ROM bootloader — a spin loop would hang the bootloader and look identical to a dead chip. It carries its own negative control. It writes TWO words: a fixed signature 0x1E55F00D, and a value COMPUTED from the argument (r0 + 0x55). The computed word is the one that matters — a fixed signature alone could be matched by a stale RAM read from an earlier attempt, which would report success for a chip that never ran anything. The computed word cannot. Observable purely over USB via blhost read-memory: no UART, no debug probe, no soldering. STATUS: BUILT, NOT RUN. Running it means entering ISP mode and writing to the vehicle, which is outside the standing read-only default and needs the user's explicit go-ahead each time. It is staged here so the go-ahead is a one-command step rather than a build session. Outputs (.o/.elf/.bin) are gitignored; build.sh regenerates them. logs/ (Renode per-run robot output) gitignored too — falcon-cascade-m7.robot is the committed evidence, not its run logs. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…y AFD-044
AFD-043 said the stack could not be composed: falcon imports no gust:os, gale-nano exports it, and
the piece between them did not exist. Two pieces were missing, both jess-owned. Both are now built,
and the whole stack composes, executes, and agrees with an independent reference.
app/flight-app imports gust:os/time + falcon rate/mixer, exports run: func() -> u32
app/gust-hal-stub exports gust:hal/mmio + gust:os/taskdisp (stub — real MMIO is on-target)
app/bump-alloc shared no_std allocator over __heap_base; never calls memory.grow
THE RESIDUAL WAS DERIVED, NOT DESIGNED. Composing flight-app against gale-nano + falcon left
EXACTLY three unsatisfied imports: gust:os/taskdisp, gust:hal/mmio, falcon types. That list of what
jess still owes the embedder used to be a guess. It is now a wac output.
wac compose flight-app + gale-nano + rate + mixer -> step1.wasm
wac compose step1 + gust-hal-stub -> full.wasm (types-only import left)
wasm-tools validate -> VALID
wasmtime run --invoke run() -> 2147484996
low 31 bits = 1348 the falcon cascade fold
bit 31 = 1 gale's clock did real arithmetic on OUR argument
THE CLOCK BIT WAS FIRST WRITTEN VACUOUSLY AND CORRECTED BEFORE REPORTING. It initially came from
`elapsed(now, deadline) == false` — which an inert clock also returns, the same trap that voided the
CRC claim in AFD-037. It now tests `deadline(t0,1) != t0`, which no zero-returning stub can produce.
DIFFERENTIAL, NOT A GOLDEN NUMBER. cascade_ref.py recomputes the same fold by a completely different
route: fused core module, raw canonical-ABI pointers, no component model, no wac, no gust:os. Both
give 1348. Torque reproduces the SIL reference exactly (tx=1 ty=0.472507507 tz=-0.147003502
thrust=0.5). A golden value would be satisfied by both sides sharing one bug; two routes agreeing
would not. Note the ABI is NOT uniform — `tick` takes a pointer, `mix` takes 4 flattened f32s;
assuming pointer-in for both silently passes garbage.
THREE NEGATIVE CONTROLS, ALL RUN:
(i) reference perturbed (wx 0.30 -> 0.35) -> 2000, DISTINCT — 1348 tracks its input, so it is
not a constant that a miscompile dropping the state would also produce
(ii) reference falsified (x1000 -> x1001) -> oracle EXITS 1, "composed=1348 reference=1350";
restored -> PASS. The gate can fail.
(iii) missing upstream artifact -> preflight EXITS 2 with an explanatory message
JESS FAILED ITS OWN PUBLISH GATE. flight-app was NOT CONSUMABLE on first build — no reloc.* and no
__heap_base, the exact defect jess reported against relay's publish path. lld defines __heap_base
synthetically but does not export it, and emits no relocations, unless asked. Fixed with
--emit-relocs / --export=__heap_base. Both jess components now pass all five checks. The gate was
not written to point outward only.
INCIDENTAL: casc_new.wasm (pre-loom) yields the same 1348 as casc_new.loom.wasm — loom is
numerically neutral ON THIS VECTOR. Recorded as an observation, not a general claim.
TOOL FRICTION: cargo-component 0.21.1 refuses a local wit/deps tree that wasm-tools resolves
without complaint (rc=0). Routed around via plain cargo + `wasm-tools component new`. To be reported.
NOT CLAIMED: this ran under wasmtime, NOT on the RT1176 and not in Renode. Periodicity is a single
call, not a schedule — the timer-ISR vs partition-window question (DD-025) is still open. gust:hal
is a STUB.
rivet validate PASS (207 warnings).
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…cation-seam # Conflicts: # artifacts/findings.yaml
…-044 — it was jess's misuse
The previous commit recorded, in AFD-044 and in its commit message, that cargo-component 0.21.1
"refuses to merge a local wit/deps tree that wasm-tools resolves without complaint", and marked it
"to be reported".
That is WRONG. A minimal 4-line repro (two packages, no jess specifics) isolated the real cause:
cargo-component does NOT auto-discover wit/deps/. It requires the dependency declared explicitly:
[package.metadata.component.target.dependencies]
"acme:dep" = { path = "wit/deps/dep/dep.wit" }
With that single line it builds cleanly. Renaming the dep directory (acme:dep, acme-dep, dep@0.1.0)
does not help, which is what made it look like a resolver bug rather than a missing declaration.
Caught BEFORE reporting it to bytecodealliance — but it was already committed into a safety-case
artifact, which is exactly the failure jess corrected synth for in AFD-042: a wrong citation sitting
in an artifact under someone's name. Withdrawn explicitly rather than quietly deleted, so the
correction is auditable.
The BUILD CHOICE is unchanged and still correct, on a different ground: cargo-component defaults to
wasm32-wasip1, which publish-gate C3 (no-wasi) REFUSES. jess needs wasm32-unknown-unknown plus
--emit-relocs and --export=__heap_base, so plain cargo + `wasm-tools component new` is right here —
but for that reason, not the one originally given.
rivet validate PASS.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
avrabe
changed the title
… (AFD-045)
AFD-044 closed the composition gap. The natural next rung was lowering the composed image for the
RT1176. It does not lower, and the reason is a meld defect jess found, minimised and filed.
BOTH TINES OF THE FORK ARE DEAD ENDS TODAY:
--memory multi (auto) validates and RUNS CORRECTLY, but meld itself states multi-memory
"has no single-address-space (MCU) lowering" (meld#172)
--memory shared --address-rebase the ONLY single-address-space route — and it emits a module that
FAILS wasm-tools validate, while meld EXITS 0
MINIMAL REPRO, two components rather than the 19-component graph:
meld fuse flight-app.wasm rate.wasm --memory shared --address-rebase -> exit 0
wasm-tools validate -> func 14: "values remaining on stack at end of block (offset 0x840)"
DISTINCT FROM THE KNOWN REBASE ISSUES, which is why it was filed rather than appended: meld#351 says
explicitly "the fused module validates cleanly", and #326/#339 are about wrong addresses in a VALID
module. Here the module is not valid and meld reports success.
THE DISCRIMINATING TABLE (all measured):
rate + mixer VALID both record-carrying, but neither imports the other
flight-app + gale-nano VALID a call crosses, but gust:os/time is scalar-only
flight-app + rate INVALID func 14
full 19-component graph INVALID func 72, "expected f32, found i32"
Hypothesis offered to meld as a search aim, NOT a diagnosis: the trigger is a wired cross-component
call carrying a RECORD via linear memory. jess has not read the rebase implementation.
RULED OUT BEFORE FILING: not relocation-driven (no --emit-relocs reproduces func 14 identically);
not a wac artefact (raw components, no wac step, fail the same); not general breakage (the falcon
fused cascade still validates); not bad inputs (the default path RUNS and reproduces 1348).
A NARROWING ERROR WAS MADE AND CORRECTED, and is recorded because the wrong version was briefly
believed: the first pass scored "INVALID" for cases where meld had produced NO OUTPUT AT ALL —
wasm-tools was validating a non-existent file and its failure was read as an invalid module. Two
distinct failures under one label. Re-run checking meld's and wasm-tools' exit codes SEPARATELY,
which produced the table above. The corrected run reaches the same conclusion, but the first pass
was not evidence for it.
IMPACT: this does NOT block the falcon cascade alone — that still lowers 5/5 on m7dp and m4f
(AFD-042). It blocks lowering the cascade TOGETHER WITH the runtime and application, which is what
DD-026 requires.
rivet validate PASS.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
… 0.41.3; 0.52.0 is latest)
A process failure, recorded rather than quietly fixed. The whole investigation and the initial
meld#390 report ran on meld 0.41.3 while 0.52.0 is latest — eleven minor versions. "Run a supplier's
DOCUMENTED pipeline before reporting a failure against it" is a standing rule and jess broke it.
Re-ran everything on 0.52.0 and corrected meld#390 in a comment.
THE DEFECT IS REAL AND REPRODUCES EXACTLY on 0.52.0 — same func 14, same offset 0x840 — so the
conclusion survives. But it was not EARNED until the re-run, and three specifics were wrong:
(a) BROADER than filed. --pack-rebase did not exist in 0.41.3 and was never tested. It fails
identically. That matters: --pack-rebase is the path the campaign actually uses.
(b) LESS SEVERE than filed. meld already ships --validate, which CATCHES this (exit 1,
"Validation failed"). The "silent, exit 0" framing was an overstatement — it is silent only by
DEFAULT. jess should have looked for the flag before calling the failure silent.
(c) the version citation in the report header was wrong.
MATRIX RE-MEASURED ON 0.52.0:
rate + mixer --pack-rebase VALID <- falcon-only cascade path NOT affected
flight-app + rate --pack-rebase INVALID
full composition --pack-rebase INVALID
full composition --address-rebase INVALID
full composition --memory multi VALID (but no MCU lowering)
The rate+mixer row matters: this does NOT regress existing cascade lowering. It breaks fusing the
cascade TOGETHER WITH an application that imports it.
SECOND-ORDER FINDING, and the more useful one: local meld was 0.41.3, CI pins v0.41.3, latest is
0.52.0 — and NOTHING DETECTED THE DRIFT because jess has no varve pin. This is the concrete cost of
that gap: an upstream report filed against tooling eleven versions old. The varve pin moves from
"nice to have" to a defect-prevention control with a demonstrated failure behind it.
rivet validate PASS.
Co-Authored-By: Claude Opus 4.8 <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.
The complete wasm stack now composes, runs, and checks out
This branch started as a finding (AFD-043: the stack cannot be composed) and ends with the gap closed. Both missing pieces were jess-owned; both are now built.
app/flight-appgust:os/time+ falconrate/mixer, exportsrun: func() -> u32app/gust-hal-stubgust:hal/mmio+gust:os/taskdisp(stub — real MMIO is the on-target rung)app/bump-allocno_stdallocator over__heap_base; never callsmemory.growThe residual was derived, not designed
The strongest part of this result. Composing
flight-appagainst gale-nano + falcon left exactly three unsatisfied imports:gust:os/taskdisp,gust:hal/mmio, and falcon types. What jess still owes the embedder used to be a guess; it is now awacoutput.It runs
Checked as a differential, not a golden number:
cascade_ref.pyrecomputes the same fold by a completely different route — fused core module, raw canonical-ABI pointers, no component model, nowac, nogust:os. Both give 1348, and the torque reproduces the SIL reference exactly. A golden value would be satisfied by both sides sharing one bug.tools/appcompose/build-and-verify.shis the whole thing in one command.Three things worth flagging against myself
The clock bit was first written vacuously. It came from
elapsed(now, deadline) == false— which an inert clock also returns, the same trap that voided the CRC claim in AFD-037. It now testsdeadline(t0,1) != t0, which no zero-returning stub can produce.jess failed its own publish gate.
flight-appwas NOT CONSUMABLE on first build — noreloc.*, no__heap_base: the exact defect jess reported against relay's publish path.llddefines__heap_basesynthetically but doesn't export it, and emits no relocations, unless asked. Both components now pass all five checks. The gate wasn't written to point outward only.A "tool friction" claim was wrong and is withdrawn (36591af). I recorded that cargo-component won't merge a local
wit/depstree; a minimal repro showed it simply requires the dep declared in[package.metadata.component.target.dependencies]. Caught before reporting it to bytecodealliance, but it had already landed in a safety-case artifact — the same failure jess corrected synth for in AFD-042. Withdrawn explicitly rather than quietly edited away.Negative controls (all run)
wx0.30 → 0.35) → 2000, distinct — 1348 tracks its inputNot claimed
Ran under wasmtime — not on the RT1176 and not in Renode. Periodicity is a single call, not a schedule; the timer-ISR vs partition-window question (DD-025) is still open.
gust:halis a stub.Also in this branch
wit-app/,wit-deps/)wit/vswit-app/vswit-deps/separation, after CI's derivation gate correctly caught hand-written WIT in the generated treetools/wit/merge_component_wit.py— the WIT union merger, offered to rules_wasm_component#626, with hard-error conflict detection and a negative control (my first version had thesetdefaultsilent-data-loss flaw they warned about)🤖 Generated with Claude Code
https://claude.ai/code/session_017EKh2onUHpWSUiAEqWxfy2