From 6cd748ec44661799706b25eff9389b8671291f29 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 23 Jul 2026 06:52:07 +0200 Subject: [PATCH 1/2] =?UTF-8?q?coord:=20gale=20v0.4.0=20delivered=20the=20?= =?UTF-8?q?TCB=20substrate=20=E2=80=94=20gust:os=20seam=20+=20verified=20m?= =?UTF-8?q?sgq/mutex/sem=20(cortex-m4f);=20msgq=20=3D=20the=20verified=20N?= =?UTF-8?q?avState=20IPC=20carrier?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit User-flagged supplier movement; jess SHA-verified the gale v0.4.0 assets. Records in the DD-023 coordination map what GALE now supplies: - gust:os typed capability seam (log + spawn on the Verus-proven executor via a WIT-typed taskdisp boundary; VER-OS-SYSCALL-001 verified, no-lost-wakeups tri-track). - Verified sync primitives DISSOLVED to cortex-m4f: gale-wasm-msgq (Zephyr k_msgq), -mutex, -sem. SHA-verified (msgq .o 74646afb, .wasm 6c990474). jess consequence: the k_msgq is the VERIFIED inter-core IPC carrier for the NavState crossing (REQ-PIX-007 / TEST-PIX-030, PR#161). jess's oracle currently uses a hand-rolled SHMEM flag handshake; the next rung grounds it on gale's k_msgq over the shmem vring + the MU doorbell already in rt1176-dualcore.repl — closing gale#65's gust ipc-rx on jess's side. gust:os + executor = the gale-nano substrate for REQ-PIX-002 (M7 base) / REQ-PIX-009 (F100). rivet validate PASS. Co-Authored-By: Claude Opus 4.8 --- artifacts/design-decisions.yaml | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/artifacts/design-decisions.yaml b/artifacts/design-decisions.yaml index f9b071f..be4e175 100644 --- a/artifacts/design-decisions.yaml +++ b/artifacts/design-decisions.yaml @@ -1235,6 +1235,17 @@ artifacts: (RC-in, 4x failsafe-PWM, 4S low-batt trip) + THE INTER-CORE IPC: gale#65 (MU-map + gust ipc-rx) is the open thread for (3). gale = the native trusted base under the all-wasm seam. + DELIVERED — gale v0.4.0 (verified 2026-07-16, jess SHA-verified the assets 2026-07-23): + ships (a) the `gust:os` typed capability seam (log.line + spawn on a Verus-proven + executor, 1081+ obligations, via a WIT-typed `gust:os/taskdisp` boundary; VER-OS-SYSCALL-001 + verified, no-lost-wakeups tri-track Verus+Kani+Rocq) and (b) verified sync primitives + DISSOLVED to cortex-m4f objects: `gale-wasm-msgq` (Zephyr k_msgq: exports z_impl_k_msgq_put / + gale_k_msgq_put_decide; undefined syms = the gale_w_* kernel seam), `-mutex`, `-sem`. + jess CONSEQUENCE: the msgq is the VERIFIED inter-core IPC carrier for the NavState crossing + (REQ-PIX-007 / TEST-PIX-030) - jess's current oracle uses a hand-rolled SHMEM flag handshake; + the next rung grounds it on gale's k_msgq (over the shmem vring + the MU doorbell already in + rt1176-dualcore.repl), closing gale#65's gust ipc-rx on jess's side. The gust:os seam + + executor are the gale-nano substrate for REQ-PIX-002 (M7 native base) / REQ-PIX-009 (F100). - RELAY (falcon + relay-hal): PARTITION the stack along the core boundaries (flight / estimator / failsafe) so each is separately fuse+compilable; plus the DD-022 driver asks (TF02 rangefinder REQ-PIX-020, dual-M9N blend, 4S AdcIn). Sequenced From e07bc374238c9c72c92bb5f6bb19de594171ecb0 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 23 Jul 2026 06:58:59 +0200 Subject: [PATCH 2/2] =?UTF-8?q?coord:=20sharpen=20gale=20track=20disciplin?= =?UTF-8?q?e=20=E2=80=94=20v0.4.0=20(cut,=20functional)=20delivered=20vs?= =?UTF-8?q?=20the=200.5=20SAFETY=20track=20(in-progress=20on=20main,=20VER?= =?UTF-8?q?s=20proposed,=20NOT=20released)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Per user: the safety substance is on gale's 0.5 track. Making the delivered-vs-proposed split crisp so jess doesn't build against unreleased safety artifacts: - CUT v0.4.0 (functional): gust:os + msgq/mutex/sem — jess consumes NOW (SHA-verified). - 0.5 SAFETY track (rivet backbone v0.5.0->v0.8.0, in-progress on main, VERs proposed, no cut release yet): I-ISO MPU core, partition-switch FSM (REQ-PIX-004/DD-025), HM/failsafe FSM (REQ-PIX-009) — the pieces jess's failsafe+partition need. WATCH item, not a current dependency; consume when gale cuts v0.5.0+ with the VERs verified. rivet validate PASS. Co-Authored-By: Claude Opus 4.8 --- artifacts/design-decisions.yaml | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/artifacts/design-decisions.yaml b/artifacts/design-decisions.yaml index be4e175..c67b9e2 100644 --- a/artifacts/design-decisions.yaml +++ b/artifacts/design-decisions.yaml @@ -1246,6 +1246,16 @@ artifacts: the next rung grounds it on gale's k_msgq (over the shmem vring + the MU doorbell already in rt1176-dualcore.repl), closing gale#65's gust ipc-rx on jess's side. The gust:os seam + executor are the gale-nano substrate for REQ-PIX-002 (M7 native base) / REQ-PIX-009 (F100). + TRACK DISCIPLINE (do NOT treat proposed-as-delivered): the above are on gale's CUT v0.4.0 + FUNCTIONAL line (SHA-verified assets on the release). gale's SAFETY line is a SEPARATE + "0.5 track" - a rivet backbone numbered v0.5.0->v0.8.0 that is IN-PROGRESS ON MAIN (branches + feat/gust-close-{adc,can,dac,dma,i2c,pwm}, feat/gust-mini-os), with every VER staying + `proposed` until its full oracle passes; there is NO cut v0.5.0 release yet (latest tag = + v0.4.0). The safety-critical pieces jess's failsafe + partition actually need - the I-ISO MPU + region-program core, the PARTITION-SWITCH FSM (REQ-PIX-004 / DD-025 ARINC-653), the value- + domain HM/FAILSAFE FSM (REQ-PIX-009) - live on that 0.5 safety track and are NOT yet released. + jess consumes the v0.4.0 msgq/gust:os now; the safety FSMs are a WATCH item (consume when gale + cuts v0.5.0+ with the VERs verified), NOT a current dependency to build against. - RELAY (falcon + relay-hal): PARTITION the stack along the core boundaries (flight / estimator / failsafe) so each is separately fuse+compilable; plus the DD-022 driver asks (TF02 rangefinder REQ-PIX-020, dual-M9N blend, 4S AdcIn). Sequenced