From 1806769f5e29dbf9755325b6641a8270c84f7914 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 23 Jul 2026 21:51:46 +0200 Subject: [PATCH 1/8] =?UTF-8?q?coord:=20DD-026=20=E2=80=94=20relay->jess?= =?UTF-8?q?=20flight-component=20consumption=20contract=20(jess#167=20posi?= =?UTF-8?q?tion)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit relay opened jess#167 asking jess to pin the consumption contract for how it integrates relay's flight components (WASM on all 3 cores) before relay mints interfaces. DD-026 records jess's POSITION (status: proposed, pending relay's falcon-rate worked example): 1. GRANULARITY: relay delivers fine-grained Level-1 verified stream components as cosign OCI + a placement manifest; JESS owns per-core meld_fuse + lowering (loom->synth per-ISA->gale) + the flashable-set attestation. Not pre-fused bundles (DD-018 + jess signs its own fused output, TEST-PIX-026/029). 2. SEAM SHAPE: synchronous step(sensor-sample)->actuator-cmd at the ARINC-653 partition window (DD-025 outer, WCET-bounded); relay keeps stream for Level-1 intra-bundle composition (inner kiln-async). 3. SEAM TYPES: spar-generated from jess's AADL, 1:1 with the HAL seams — already realized (ActuatorCmd.pwm / VehicleState.nav, REQ-PIX-007/TEST-PIX-023). 4. F100 FAILSAFE: maximal-wasm on M3 (TEST-PIX-028) with gale's VERIFIED HM FSM (VER-OS-HM-001, v0.5.0) as the mechanism — not a parallel relay-fsafe. 5. DELIVERY: OCI-per-component; jess's V-gates (scry/witness/repro/sigil) run on jess's fused set. Endorsed relay's falcon-rate worked example. Stated the sequencing honesty: the M7 cascade can't lower yet (float gate, AFD-035); the F100/M3 path is the green-today validation target. Replied on jess#167 with the full position. rivet validate PASS. Co-Authored-By: Claude Opus 4.8 --- artifacts/design-decisions.yaml | 56 +++++++++++++++++++++++++++++++++ 1 file changed, 56 insertions(+) diff --git a/artifacts/design-decisions.yaml b/artifacts/design-decisions.yaml index f9307f8..2adc017 100644 --- a/artifacts/design-decisions.yaml +++ b/artifacts/design-decisions.yaml @@ -1396,3 +1396,59 @@ artifacts: target: DD-023 - type: traces-to target: DD-011 + + - id: DD-026 + type: design-decision + title: relay->jess flight-component consumption contract - Level-1 fine-grained streams delivered as OCI, jess owns per-core meld-fuse + on-target lowering + attestation; synchronous step() seam per ARINC-653 window; spar-generated seam types; F100 failsafe on gale's verified HM FSM + status: proposed + description: > + Answers relay's consumption-contract discussion (jess#167, 2026-07-23): with a WASM Component + Model runtime now on all three cores and falcon-flight published as a cosign-signed OCI component, + relay asked jess (the system-integration + on-target authority) to pin HOW jess consumes relay's + flight components before relay mints interfaces. jess's POSITION (proposed; to be validated by + relay's falcon-rate worked example before -> accepted): + 1. GRANULARITY: relay delivers the FINE-GRAINED Level-1 verified stream components (falcon-iekf/ + position/attitude/rate/mixer-stream, relay-fsafe) as cosign-signed OCI + a wiring/placement + manifest; JESS owns the per-core meld_fuse + lowering (loom -> synth per-target-ISA fpv5-d16/ + fpv4-sp/soft-float -> gale-link) + the flashable-set attestation. NOT pre-fused per-core + bundles - DD-018 puts wasm->ARM on jess, and jess's pipeline signs its OWN fused output + (path-independent-reproducible TEST-PIX-026 + sigil TEST-PIX-029). relay's falcon-cascade- + stream-fused is a REFERENCE fusion to cross-check, not the delivery unit. + 2. SEAM SHAPE: layered per DD-025's two levels. The per-core seam jess SCHEDULES is synchronous + `step(sensor-sample) -> actuator-cmd` = the ARINC-653 partition-window activation (bounded + per-tick -> WCET-analyzable via spar timing + kiln fuel). relay keeps `stream` for Level-1 + INTRA-bundle composition (the inner cooperative kiln-async). Streams compose intra-core; the + partition tick drives one step per window. + 3. SEAM TYPES: spar-generated from jess's AADL, 1:1 with the HAL peripheral seams (jess#62/ + relay#214). Already realized: actuator-cmd = ActuatorCmd.pwm, NavState = VehicleState.nav + (REQ-PIX-007/TEST-PIX-023). jess's AADL is the type source of truth; same records flow + driver->estimator->core->mixer->failsafe. + 4. F100 FAILSAFE: maximal-WASM on the F100/M3 (confirmed all-cores-wasm; gust pass-through proven + TEST-PIX-027/028), but the safety FSM = gale's VERIFIED HM/failsafe (VER-OS-HM-001, gale v0.5.0), + NOT a parallel wasm-wrapped relay-fsafe. relay owns the value-domain policy above gale's verified + mechanism (REQ-PIX-009). + 5. DELIVERY: OCI-per-Level-1-component per relay release (cosign), one ghcr repo each. jess's + right-side-of-V gates (scry TEST-PIX-022, witness jess#91, repro TEST-PIX-026, sigil TEST-PIX-029) + run on the FUSED flashable set jess produces - complementing relay's source-level DWARF MC/DC. + SEQUENCING HONESTY (stated on jess#167): the contract can be designed+prototyped now, but the M7 + CASCADE cannot lower on-target yet (AFD-035/synth#782, 13 skips). The F100 failsafe is lowerable NOW + (the best end-to-end validation target this cycle); the M4 estimator is next (modulo f64); the M7 + cascade lowering-validation waits on synth's falcon-skip-to-zero lane. relay's falcon-rate example is + endorsed for the SHAPE; on-target lowering validation runs first on the green-today F100/M3 path. + tags: [phase-2, consumption-contract, relay, oci, meld-fuse, on-target, wit, dd-018, dd-025, req-pix-007, jess-167, coordination] + fields: + rationale: >- + jess is the system-integration + on-target authority (jess#62<->relay#214); the lowering + + attestation pipeline (DD-018, TEST-PIX-026/029) must operate on jess's own fused output, so jess + owns the fusion and relay delivers verified Level-1 parts + a manifest. The seam shape falls out + of DD-025's two-level schedule (step at the partition boundary, streams inside). Proposed, not + accepted, pending relay's falcon-rate worked example validating the seam end-to-end. + links: + - type: satisfies + target: REQ-PIX-007 + - type: traces-to + target: DD-018 + - type: traces-to + target: DD-025 + - type: traces-to + target: DD-023 From ce739f6b82bc6097da3730566e794630e5afaadb Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 23 Jul 2026 22:03:04 +0200 Subject: [PATCH 2/8] =?UTF-8?q?coord:=20DD-026=20delivery=20=E2=80=94=20as?= =?UTF-8?q?ked=20gale=20to=20publish=20verified=20components=20as=20OCI=20?= =?UTF-8?q?(gale#223),=20aligning=20with=20relay's=20falcon-flight?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Per the consumption contract's OCI-per-component delivery: gale ships release-tarball .o/.wasm (not OCI) while relay went to ghcr-OCI, so jess's per-core meld-fuse would pull from two paths. Filed gale#223 asking gale to publish its verified consumable components (HM/failsafe FSM, gust:os, sync primitives, the fused gale-nano subset) as cosign-signed OCI wasm components - uniform acquisition + sidesteps the standalone-.o unshipped-scheduler-seam problem. RECORD (float-gated), aligned now while the contract shape is fresh. Co-Authored-By: Claude Opus 4.8 --- artifacts/design-decisions.yaml | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/artifacts/design-decisions.yaml b/artifacts/design-decisions.yaml index 2adc017..1af9e23 100644 --- a/artifacts/design-decisions.yaml +++ b/artifacts/design-decisions.yaml @@ -1430,6 +1430,15 @@ artifacts: 5. DELIVERY: OCI-per-Level-1-component per relay release (cosign), one ghcr repo each. jess's right-side-of-V gates (scry TEST-PIX-022, witness jess#91, repro TEST-PIX-026, sigil TEST-PIX-029) run on the FUSED flashable set jess produces - complementing relay's source-level DWARF MC/DC. + GALE ALIGNMENT (filed gale#223, 2026-07-24): gale is a co-supplier of what jess fuses per core + (F100 failsafe = gale VER-OS-HM-001 FSM; all cores = gust:os + msgq/mutex/sem + executor) but + ships RELEASE-TARBALL .o/.wasm assets, NOT OCI - so per-core meld-fuse would pull relay from + ghcr-OCI and gale from a tarball (two acquisition paths). Asked gale to publish its verified + consumable components (incl. the fused gale-nano subset) as cosign-signed OCI wasm components + like falcon-flight, so jess pulls all 3 cores' inputs uniformly (one OCI+cosign path) AND an + OCI-published *component* sidesteps the standalone-.o unshipped-scheduler-seam problem (jess + meld-fuses a component, not a bag of objects). RECORD not build-ahead (float-gated), but aligned + now while the contract shape is fresh. SEQUENCING HONESTY (stated on jess#167): the contract can be designed+prototyped now, but the M7 CASCADE cannot lower on-target yet (AFD-035/synth#782, 13 skips). The F100 failsafe is lowerable NOW (the best end-to-end validation target this cycle); the M4 estimator is next (modulo f64); the M7 From 7f6b476d0a9d53b5133ad81afc9ab46c80bb5df3 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 23 Jul 2026 22:10:30 +0200 Subject: [PATCH 3/8] =?UTF-8?q?coord:=20DD-026=20gale#223=20AGREED=20?= =?UTF-8?q?=E2=80=94=20gale's=20consumable=20=3D=20fused=20gale-nano=20OCI?= =?UTF-8?q?=20component=20(residual=20host=20=3D=20gust:hal),=20v0.6=20cut?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit gale maintainer agreed on gale#223. Updated the DD-026 delivery decision: - Artifact shapes pinned: v0.5.0 msgq .o = self-contained decision fragment (0 undef); .wasm = core module with the 9-symbol scheduler seam. Neither is the consumable unit (corrects my earlier '.o needs 9 symbols' imprecision). - Resolution: gale delivers a cosign OCI wasm COMPONENT = the fused gale-nano subset (msgq/mutex/sem + gust:os + executor) resolving the scheduler seam internally, residual host contract = gust:hal (DD-018 thin native seam) and stays that thin. jess's per-core meld_fuse pulls relay Level-1 + gale's fused component (both OCI). Cross-linked DD-026 <-> gale's forthcoming DD; tracked for gale v0.6. F100=VER-OS-HM-001 half already consistent. Co-Authored-By: Claude Opus 4.8 --- artifacts/design-decisions.yaml | 26 +++++++++++++++++--------- 1 file changed, 17 insertions(+), 9 deletions(-) diff --git a/artifacts/design-decisions.yaml b/artifacts/design-decisions.yaml index 1af9e23..73fd9c2 100644 --- a/artifacts/design-decisions.yaml +++ b/artifacts/design-decisions.yaml @@ -1430,15 +1430,23 @@ artifacts: 5. DELIVERY: OCI-per-Level-1-component per relay release (cosign), one ghcr repo each. jess's right-side-of-V gates (scry TEST-PIX-022, witness jess#91, repro TEST-PIX-026, sigil TEST-PIX-029) run on the FUSED flashable set jess produces - complementing relay's source-level DWARF MC/DC. - GALE ALIGNMENT (filed gale#223, 2026-07-24): gale is a co-supplier of what jess fuses per core - (F100 failsafe = gale VER-OS-HM-001 FSM; all cores = gust:os + msgq/mutex/sem + executor) but - ships RELEASE-TARBALL .o/.wasm assets, NOT OCI - so per-core meld-fuse would pull relay from - ghcr-OCI and gale from a tarball (two acquisition paths). Asked gale to publish its verified - consumable components (incl. the fused gale-nano subset) as cosign-signed OCI wasm components - like falcon-flight, so jess pulls all 3 cores' inputs uniformly (one OCI+cosign path) AND an - OCI-published *component* sidesteps the standalone-.o unshipped-scheduler-seam problem (jess - meld-fuses a component, not a bag of objects). RECORD not build-ahead (float-gated), but aligned - now while the contract shape is fresh. + GALE ALIGNMENT (gale#223, 2026-07-24 - AGREED with the gale maintainer): gale is a co-supplier + of what jess fuses per core (F100 failsafe = gale VER-OS-HM-001 FSM; all cores = gust:os + + msgq/mutex/sem + the Verus-proven executor) but ships RELEASE-TARBALL assets, NOT OCI. ARTIFACT + SHAPES pinned: the v0.5.0 msgq `.o` is the self-contained DECISION FRAGMENT (gale_k_msgq_put_decide, + 0 undef); the `.wasm` is the CORE MODULE carrying the 9-symbol env scheduler seam + (k_spin_lock/unlock, z_ready_thread, z_reschedule, z_unpend_first_thread, gale_w_msgq_pend/ + thread_swap_data/memcpy, arch_thread_return_value_set) - NEITHER is the consumable unit. + RESOLUTION (gale to record its own DD, mirroring this one, tracked for the gale v0.6 cut): gale's + consumable delivery = a cosign-signed OCI wasm COMPONENT = the FUSED gale-nano runtime subset + (msgq/mutex/sem + gust:os + executor) that resolves the scheduler seam INTERNALLY, leaving only a + thin documented host contract. DELIVERY INVARIANT jess asked gale to hold: that residual host + surface = `gust:hal` (bus/MMIO/PWM/time = DD-018's thin native seam jess provides per core) and + stays that thin (no leaking scheduler/heap imports). Then jess's per-core meld_fuse pulls relay's + Level-1 flight components + gale's fused gale-nano component (both OCI) and fuses+lowers them - the + gale component is the SUBSTRATE INPUT, not competing with jess's fusion. Cross-linked DD-026 <-> the + forthcoming gale DD; F100-failsafe=VER-OS-HM-001 half already consistent (v0.5.0). RECORD not + build-ahead (both float-gated), aligned now while the contract shape is fresh. SEQUENCING HONESTY (stated on jess#167): the contract can be designed+prototyped now, but the M7 CASCADE cannot lower on-target yet (AFD-035/synth#782, 13 skips). The F100 failsafe is lowerable NOW (the best end-to-end validation target this cycle); the M4 estimator is next (modulo f64); the M7 From 5f2971ebb87ce0f069b4ff81830734cb06d0570b Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 23 Jul 2026 22:14:35 +0200 Subject: [PATCH 4/8] =?UTF-8?q?coord:=20DD-026=20correction=20=E2=80=94=20?= =?UTF-8?q?gust:os=20is=20the=20composition=20abstraction=20(not=20gust:ha?= =?UTF-8?q?l);=20three=20WIT=20layers?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Corrected per the gale component-model architecture: the app<->runtime COMPOSITION seam is gust:os (gale's typed capability world = 'the OS surface an app sees'), which relay's flight imports and gale's OCI component exports. gust:hal is the deeper NATIVE residual (mmio, jess- provided), not the composition seam. Three WIT layers, each owned right: (i) gust:os = capability abstraction (gale) - the composition seam (ii) data seams (sensor-sample/actuator-cmd/NavState) = app<->app (jess-AADL, REQ-PIX-007) (iii) gust:hal = native mmio residual (jess) Scheduler primitives live BELOW gust:os (resolved by the composed executor), never exposed. gale delivers the gust:os PROVIDERS as the OCI component; jess composes flight+providers along gust:os -> residual gust:hal. Refined on gale#223. Co-Authored-By: Claude Opus 4.8 --- artifacts/design-decisions.yaml | 30 +++++++++++++++++++++--------- 1 file changed, 21 insertions(+), 9 deletions(-) diff --git a/artifacts/design-decisions.yaml b/artifacts/design-decisions.yaml index 73fd9c2..9c24c46 100644 --- a/artifacts/design-decisions.yaml +++ b/artifacts/design-decisions.yaml @@ -1438,15 +1438,27 @@ artifacts: (k_spin_lock/unlock, z_ready_thread, z_reschedule, z_unpend_first_thread, gale_w_msgq_pend/ thread_swap_data/memcpy, arch_thread_return_value_set) - NEITHER is the consumable unit. RESOLUTION (gale to record its own DD, mirroring this one, tracked for the gale v0.6 cut): gale's - consumable delivery = a cosign-signed OCI wasm COMPONENT = the FUSED gale-nano runtime subset - (msgq/mutex/sem + gust:os + executor) that resolves the scheduler seam INTERNALLY, leaving only a - thin documented host contract. DELIVERY INVARIANT jess asked gale to hold: that residual host - surface = `gust:hal` (bus/MMIO/PWM/time = DD-018's thin native seam jess provides per core) and - stays that thin (no leaking scheduler/heap imports). Then jess's per-core meld_fuse pulls relay's - Level-1 flight components + gale's fused gale-nano component (both OCI) and fuses+lowers them - the - gale component is the SUBSTRATE INPUT, not competing with jess's fusion. Cross-linked DD-026 <-> the - forthcoming gale DD; F100-failsafe=VER-OS-HM-001 half already consistent (v0.5.0). RECORD not - build-ahead (both float-gated), aligned now while the contract shape is fresh. + consumable delivery = a cosign-signed OCI wasm COMPONENT = the `gust:os` PROVIDERS (executor + + the capability world), NOT a monolithic runtime blob. THREE WIT LAYERS, each owned by the right + party (corrected 2026-07-24 - the composition seam is gust:os, gale's component-model abstraction, + not gust:hal): + (i) `gust:os` = the CAPABILITY abstraction (app<->runtime, the component-model seam): a typed + capability world (log/channel/io/spawn/taskdisp) = "the OS surface an app sees". relay's + flight components IMPORT gust:os; gale's OCI component EXPORTS gust:os. Composition happens + ALONG gust:os (gale's wac plug + meld fuse --memory shared pipeline). GALE OWNS its shape. + (ii) the DATA seams (`sensor-sample`/`actuator-cmd`/NavState = the step() dataflow) = app<->app, + JESS-AADL-DEFINED (spar codegen, REQ-PIX-007). + (iii) `gust:hal` = the NATIVE residual (runtime<->silicon, mmio): after the gust:os composition + dissolves, the ONLY undefined symbols are gust:hal (bus/MMIO/PWM/time = DD-018's thin + native base) - JESS provides it per core. The scheduler primitives (z_ready_thread/ + z_reschedule/gale_w_msgq_pend/...) live BELOW gust:os, resolved by the composed executor, + never exposed to the flight app OR the native host. + So jess's per-core meld_fuse composes relay-flight(imports gust:os) + gale gust:os-providers + (both OCI) -> one image whose residual is gust:hal (jess native). Delivery invariant is two-part: + (a) the app-composition seam is the STABLE gust:os capability world (gale-owned), (b) the native + residual stays exactly gust:hal (no leaking scheduler/heap). Cross-linked DD-026 <-> the forthcoming + gale DD; F100-failsafe=VER-OS-HM-001 half already consistent (v0.5.0). RECORD not build-ahead (both + float-gated), aligned now while the contract shape is fresh. SEQUENCING HONESTY (stated on jess#167): the contract can be designed+prototyped now, but the M7 CASCADE cannot lower on-target yet (AFD-035/synth#782, 13 skips). The F100 failsafe is lowerable NOW (the best end-to-end validation target this cycle); the M4 estimator is next (modulo f64); the M7 From 3d1c3c235aad9d0818e0897f5ecb8e646b5a7bb7 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 23 Jul 2026 22:29:38 +0200 Subject: [PATCH 5/8] =?UTF-8?q?coord:=20DD-026=20=E2=80=94=20relay=20CONVE?= =?UTF-8?q?RGED=20on=20jess#167=20(option=20a=20+=202=20principles:=20inte?= =?UTF-8?q?grator=20owns=20seam,=20loop-complete=20closed-loop-proof)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit relay settled on jess#167: option (a) + two principles jess accepted. P1: integrator (jess) owns the cross-core seam + width + airframe binding; relay stays airframe/target-agnostic (ActuatorCmd.pwm=4xf32 is jess's X500-V2/quad specialization; hex = jess seam-width + manifest change, relay mixer parameterized underneath). Confirms decision 3. P2: loop-complete minimality (smallest seam that closes the loop) + every relay component ships a closed-loop proof (not a step stub). Proof division: relay proves loop-closes- in-source (SIL); jess proves loop-survives-lowering (SIL-vs-Renode differential) = jess's on-target value-add; stacks to the full V per stage. Bonus: falcon-rate as its own OCI entity gives jess the per-stage skip inventory -> a falcon-skip-to-zero priority signal. DD-026 stays 'proposed' until falcon-rate validates the seam end-to-end (relay building it). Replied on jess#167. rivet validate PASS. Co-Authored-By: Claude Opus 4.8 --- artifacts/design-decisions.yaml | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/artifacts/design-decisions.yaml b/artifacts/design-decisions.yaml index 9c24c46..3a1c656 100644 --- a/artifacts/design-decisions.yaml +++ b/artifacts/design-decisions.yaml @@ -1464,6 +1464,22 @@ artifacts: (the best end-to-end validation target this cycle); the M4 estimator is next (modulo f64); the M7 cascade lowering-validation waits on synth's falcon-skip-to-zero lane. relay's falcon-rate example is endorsed for the SHAPE; on-target lowering validation runs first on the green-today F100/M3 path. + RELAY CONVERGED 2026-07-24 (jess#167) on option (a) + two principles jess accepted: + P1 - INTEGRATOR OWNS THE SEAM; relay stays airframe/target-agnostic. The cross-core seam + (VehicleState.nav, ActuatorCmd.pwm) is jess's, spar-generated from jess's AADL, fixed per + target at fuse-time INCLUDING the airframe-coupled actuator width. ActuatorCmd.pwm=4xf32 is + jess's X500-V2/quad specialization (DD-022); a later hex = a jess-side seam-WIDTH change + + the mix-matrix in the placement manifest, relay's mixer parameterized UNDERNEATH an unchanged + relay component (no relay fork). Confirms decision 3. + P2 - LOOP-COMPLETE minimality + CLOSED-LOOP-PROOF evidence. Seam floor: smallest that still CLOSES + the control loop, no smaller (can't shrink NavState below the 16-state or drop gyro from a + rate input). Every relay component ships a CLOSED-loop proof (torque->plant->gyro->back, + tracking over N ticks), not an open-loop step stub. PROOF DIVISION: relay proves the loop + closes IN-SOURCE (SIL); jess proves it STILL closes AFTER wasm->ARM lowering (the SIL-vs-Renode + differential jess already runs for gust + the fused falcon) = jess's on-target value-add; the + two stack into the full V per stage. BONUS: falcon-rate as its OWN OCI entity lets jess measure + the PER-STAGE synth skip inventory (vs the whole-fused 13, AFD-035) -> tells relay+synth which + cascade stage blocks first on the float gate (a falcon-skip-to-zero priority signal). tags: [phase-2, consumption-contract, relay, oci, meld-fuse, on-target, wit, dd-018, dd-025, req-pix-007, jess-167, coordination] fields: rationale: >- From 0346f7b11bc53aac3e178be514fb14c4c799609f Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 23 Jul 2026 22:31:43 +0200 Subject: [PATCH 6/8] =?UTF-8?q?coord:=20DD-026=20bilaterally=20pinned=20?= =?UTF-8?q?=E2=80=94=20gale=20landed=20DD-OS-DELIVERY-001=20(gale#225)=20+?= =?UTF-8?q?=20build=20target=20gale#224=20(v0.6)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit gale landed its mirror decision with the gust:os correction baked in: DD-OS-DELIVERY-001 (gale#225, rivet PASS) - the consumable cut is a cosign OCI component EXPORTING gust:os, scheduler resolved below it, residual = gust:hal. Build target gale#224 (the fused gale-nano component) bound to v0.6, acceptance invariant = wasm-tools confirms a component exporting gust:os + after wac plug/meld/loom/synth the only undefined syms are the gust:hal mmio seam (no scheduler/heap leak). Already demonstrated at the tl/ts node level (VER-OS-SYSCALL-001). DD-026 <-> DD-OS-DELIVERY-001 cross-linked; consumption contract bilaterally pinned across relay/jess/gale. Co-Authored-By: Claude Opus 4.8 --- artifacts/design-decisions.yaml | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/artifacts/design-decisions.yaml b/artifacts/design-decisions.yaml index 3a1c656..b9200bb 100644 --- a/artifacts/design-decisions.yaml +++ b/artifacts/design-decisions.yaml @@ -1456,8 +1456,16 @@ artifacts: So jess's per-core meld_fuse composes relay-flight(imports gust:os) + gale gust:os-providers (both OCI) -> one image whose residual is gust:hal (jess native). Delivery invariant is two-part: (a) the app-composition seam is the STABLE gust:os capability world (gale-owned), (b) the native - residual stays exactly gust:hal (no leaking scheduler/heap). Cross-linked DD-026 <-> the forthcoming - gale DD; F100-failsafe=VER-OS-HM-001 half already consistent (v0.5.0). RECORD not build-ahead (both + residual stays exactly gust:hal (no leaking scheduler/heap). BILATERALLY PINNED 2026-07-24: gale + landed its side as `DD-OS-DELIVERY-001` (gale#225, rivet PASS, refines SAC-BYOOS-LIBOS) - the + gust:os correction baked in (component EXPORTS gust:os; scheduler resolved below it; residual = + gust:hal) - with the build target `gale#224` (the fused gale-nano component) bound to the gale v0.6 + cut. ACCEPTANCE INVARIANT (gale's, matches jess's ask): wasm-tools confirms a *component* exporting + gust:os, and after `wac plug (+) meld fuse --memory shared -> loom -> synth` the ONLY undefined + symbols are the gust:hal mmio seam (no scheduler/heap leak) - already demonstrated at the tl/ts node + level (VER-OS-SYSCALL-001: residual = exactly the gust:hal seam + typed taskdisp), gale#224 + generalizes it to a published self-contained component. DD-026 <-> DD-OS-DELIVERY-001 cross-linked. + F100-failsafe=VER-OS-HM-001 half already consistent (v0.5.0). RECORD not build-ahead (both float-gated), aligned now while the contract shape is fresh. SEQUENCING HONESTY (stated on jess#167): the contract can be designed+prototyped now, but the M7 CASCADE cannot lower on-target yet (AFD-035/synth#782, 13 skips). The F100 failsafe is lowerable NOW From 6e66e1f794e1348612e758f446ac8f840c55f488 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 23 Jul 2026 22:37:15 +0200 Subject: [PATCH 7/8] =?UTF-8?q?coord:=20DD-015=20driver-path=20refinement?= =?UTF-8?q?=20=E2=80=94=20gale's=20verified=20thin-seam=20drivers=20shrink?= =?UTF-8?q?=20jess-native=20to=20gust:hal=20(the=20DD-026=20driver=20half)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit gale v0.5.0's verified + silicon-validated thin-seam driver suite (spi/i2c/adc/can/pwm/gpio/ wdg over gust:hal) refines the DD-015 driver seam: the bus TRANSPORT that DD-015 put in jess's native host moves DOWN into gale-verified wasm, shrinking jess's native TCB to just gust:hal. New layering: gust:hal[jess] -> gale verified thin-seam bus driver -> relay protocol/decode/ voting -> sensor-sample[jess AADL] -> relay flight app. Open reconciliation (raised on jess#167): the gale-bus-driver <-> relay-protocol-driver boundary = the embedded-hal-async transport traits (gale implements, relay consumes) so the register bus is owned once; + gust-target-gen AADL vs jess's AADL needs one owner (jess). To pin in the DD-026 driver-path extension. Co-Authored-By: Claude Opus 4.8 --- artifacts/design-decisions.yaml | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/artifacts/design-decisions.yaml b/artifacts/design-decisions.yaml index b9200bb..fc916d8 100644 --- a/artifacts/design-decisions.yaml +++ b/artifacts/design-decisions.yaml @@ -583,6 +583,22 @@ artifacts: device SEMANTICS. Consistent with DD-011 (the gust TCB is the same tiny host-import shape) and DD-012 (relay abstracts / jess binds). Detailed per-seam spec posted to relay on jess#62. + REFINED AGAIN 2026-07-24 (gale v0.5.0 verified DRIVER SUITE - the driver-path half of the + DD-026 consumption contract): gale now ships VERIFIED thin-seam bus drivers (spi/i2c/adc/can/pwm/ + gpio/dac/wdg) - Kani-proven + SILICON-VALIDATED (adc read Vrefint on a real STM32F100; wdg fired on + a G474) - each a dissolved wasm FSM touching silicon ONLY over gust:hal (the raw mmio seam). This + pushes the BUS TRANSPORT that this DD put in jess's NATIVE host DOWN into gale-verified WASM, so + jess's native TCB SHRINKS to just gust:hal (the RT1176 mmio addresses / thin native shim) - MORE + gale-maximal-wasm, the exact principle this DD cited. NEW LAYERING (bottom-up): gust:hal [JESS + native] -> gale verified thin-seam bus driver [GALE, implements the embedded-hal-async transport + SpiDevice/I2c/AdcIn] -> relay protocol/decode/voting [RELAY, imu reg-map, UBX, DroneCAN, EKF + voting] -> sensor-sample [the data seam, JESS AADL/spar] -> relay flight app. OPEN RECONCILIATION + (raised on jess#167): the gale-bus-driver <-> relay-protocol-driver boundary must be a named seam - + cleanest = the embedded-hal-async transport traits (gale IMPLEMENTS verified; relay CONSUMES for + reg-map/decode), so the register-level bus is owned once (gale), not double-claimed vs DD-015's + "relay owns drivers". Also: gale's gust-target-gen AADL device model overlaps jess's + hardware/pixhawk6x-rt.aadl - the RT1176 target model needs ONE owner (jess owns it; gale generates + per-target constants FROM it). To pin in the DD-026 driver-path extension once gale/relay confirm. REFINED by DD-018: the transport trait SHAPE named here (bespoke RegBus/SerialBus, read-reg) is SUPERSEDED - the seam now anchors on embedded-hal-async SpiDevice/I2c + embedded-io-async at TRANSACTION granularity (register helpers move relay-side). From 80eee150a7d8bb4a324e8ead98758718545629fd Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 23 Jul 2026 22:53:53 +0200 Subject: [PATCH 8/8] =?UTF-8?q?feature:=20add=20ImuSample.raw=20seam=20(je?= =?UTF-8?q?ss#167)=20=E2=80=94=20raw=20IMU=20fan-out=20(M4=20ekf=20+=20M7?= =?UTF-8?q?=20rate=20loop);=20NavState=20confirmed=20biases-not-rates?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit relay found the cascade seams already exist (falcon:cascade@0.7.0) and asked jess (seam owner) to confirm the M4<->M7 data flow. Confirmed + added jess's side: - VehicleState.nav (16, biases + NO rates) is the canonical IEKF state; the rate loop takes the RAW gyro as a SEPARATE co-scheduled-on-M7 sample and bias-corrects it with NavState's gyro-bias (freshest inner-loop gyro, no cross-core/filter lag) - the standard PX4 fan-out. - Added ImuSample.raw (6xf32 = gyro3+accel3) to hardware/pixhawk6x-rt.aadl; spar emits `record imu-sample-raw` on both falcon.wit (rate loop) + estimator.wit (ekf) = the fan-out. WIT-derivation gate green (committed wit/ == spar codegen). - innovation stays OUT of the controller crossing (separate Health-Monitor signal, VER-OS-HM-001). - Recorded in DD-026. relay's one seam edit: rate re-feeds gyro from imu-sample, not vehicle-state. Verified: rivet validate PASS; spar parse+instance OK; WIT-derivation gate OK. Co-Authored-By: Claude Opus 4.8 --- hardware/pixhawk6x-rt.aadl | 10 ++++++++++ wit/estimator.wit | 9 +++++++++ wit/falcon.wit | 9 +++++++++ 3 files changed, 28 insertions(+) diff --git a/hardware/pixhawk6x-rt.aadl b/hardware/pixhawk6x-rt.aadl index b74c5bd..3e901ff 100644 --- a/hardware/pixhawk6x-rt.aadl +++ b/hardware/pixhawk6x-rt.aadl @@ -128,6 +128,13 @@ public m0 : data F32; m1 : data F32; m2 : data F32; m3 : data F32; end ActuatorCmd.pwm; + data ImuSample end ImuSample; -- raw IMU seam (jess#167): FANS OUT to M4 ekf AND M7 rate loop + data implementation ImuSample.raw -- 6 x f32 = gyro(3) + accel(3). The M7 rate loop reads the raw + subcomponents -- gyro here (freshest, no cross-core delay) and bias-corrects it + gx : data F32; gy : data F32; gz : data F32; -- with VehicleState.nav's gyro-bias; the M4 ekf + ax : data F32; ay : data F32; az : data F32; -- consumes gyro+accel. Rates are NOT in NavState. + end ImuSample.raw; + -------------------------------------------------------------------------- -- Sensor + power devices -------------------------------------------------------------------------- @@ -270,6 +277,8 @@ public process Falcon_Flight features state_in : in data port VehicleState.nav; -- <- estimator (cross-core RPC) + imu_in : in data port ImuSample.raw; -- <- raw IMU (M7-co-scheduled): the rate loop's + -- fresh gyro, bias-corrected by state_in (jess#167) cmd_out : out data port ActuatorCmd.pwm; -- -> failsafe (cross-MCU RPC) end Falcon_Flight; process implementation Falcon_Flight.cascade @@ -279,6 +288,7 @@ public -- M4 core as its own fused component. Emits VehicleState to the M7. process Estimator features + imu_in : in data port ImuSample.raw; -- <- raw IMU: gyro+accel feed the IEKF state_out : out data port VehicleState.nav; end Estimator; process implementation Estimator.iekf diff --git a/wit/estimator.wit b/wit/estimator.wit index d77abfe..ab81db9 100644 --- a/wit/estimator.wit +++ b/wit/estimator.wit @@ -2,6 +2,14 @@ package pixhawk6-x-r-t:estimator; interface estimator-ports { + record imu-sample-raw { + gx: f32, + gy: f32, + gz: f32, + ax: f32, + ay: f32, + az: f32, + } record vehicle-state-nav { qw: f32, qx: f32, @@ -21,6 +29,7 @@ interface estimator-ports { baz: f32, } + imu-in: func() -> imu-sample-raw; set-state-out: func(val: vehicle-state-nav); } diff --git a/wit/falcon.wit b/wit/falcon.wit index 14d10fb..8a03fa9 100644 --- a/wit/falcon.wit +++ b/wit/falcon.wit @@ -8,6 +8,14 @@ interface falcon-ports { m2: f32, m3: f32, } + record imu-sample-raw { + gx: f32, + gy: f32, + gz: f32, + ax: f32, + ay: f32, + az: f32, + } record vehicle-state-nav { qw: f32, qx: f32, @@ -28,6 +36,7 @@ interface falcon-ports { } state-in: func() -> vehicle-state-nav; + imu-in: func() -> imu-sample-raw; set-cmd-out: func(val: actuator-cmd-pwm); }