From 968cc4b8860e82b1b7d688b1befef944e41b1dea Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 23 Jul 2026 20:47:45 +0200 Subject: [PATCH] =?UTF-8?q?coord:=20gale=20v0.5.0=20CUT=20=E2=80=94=20the?= =?UTF-8?q?=200.5=20safety=20track=20is=20RELEASED=20with=20VERs=20verifie?= =?UTF-8?q?d=20(partition=20switch=20/=20HM-failsafe=20/=20MPU=20/=20timer?= =?UTF-8?q?)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Release-watch: the gale 0.5 safety track (the user-flagged watch item) is now CUT + verified. gale v0.5.0 ships the VERIFIED safety substrate jess's failsafe+partition need: - VER-OS-SWITCH-001: two-level partition switch (verified Switcher x verified MPU; qemu + multi-core Renode demo) -> REQ-PIX-004 / DD-025 ARINC-653. - VER-OS-HM-001: Health-Monitor cross-sensor voting + per-cause failsafe demonstrator -> REQ-PIX-009 F100 failsafe. - VER-OS-ISO-001 (I-ISO MPU isolation) + VER-OS-TIMER-001 (tickless sleep) + VER-OS-SYSCALL-001. - gust-target-gen spar/AADL model SILICON-VALIDATED on STM32F100 (jess's F100 core) + STM32G474. So the safety FSMs move from "0.5-track WATCH item" (last tick) to DELIVERED+verified. Recorded on DD-023 GALE row + REQ-PIX-004 + REQ-PIX-009 + memory. STILL BLOCKED (last-tick finding holds): consuming the FSMs/k_msgq needs the ~9-symbol scheduler seam (k_spin_lock, z_ready_thread, z_reschedule, z_unpend_first_thread, gale_w_msgq_pend/ thread_swap_data/memcpy, arch_thread_return_value_set) - the v0.5.0 release ships only msgq/mutex/ sem .o, not the standalone kernel-seam/FSM objects. jess links the fused gale-nano core (or files the seam ask when it can bind, #369/float-gated). Also (STEP 1): falcon-v1.128 wasm is BYTE-IDENTICAL to v1.127 (54020c5e) - proof-only (MATHF32-P04/ P05 sin/cos bounds) + OCI publishing, no flight-code change -> skips unchanged at 13. synth v0.50.1 is a patch. No inbound. rivet validate PASS. Co-Authored-By: Claude Opus 4.8 --- artifacts/design-decisions.yaml | 21 ++++++++++++++++++--- artifacts/phase2-pixhawk.yaml | 14 ++++++++++++++ 2 files changed, 32 insertions(+), 3 deletions(-) diff --git a/artifacts/design-decisions.yaml b/artifacts/design-decisions.yaml index f9307f8..bf17161 100644 --- a/artifacts/design-decisions.yaml +++ b/artifacts/design-decisions.yaml @@ -1260,9 +1260,24 @@ artifacts: `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. + domain HM/FAILSAFE FSM (REQ-PIX-009) - live on that 0.5 safety track. + UPDATE 2026-07-24 - GALE v0.5.0 CUT: the 0.5 safety track is now RELEASED with its VERs + VERIFIED (no longer proposed): VER-OS-ISO-001 (I-ISO MPU region-swap hardware-isolation + boundary), VER-OS-SWITCH-001 (two-level partition switch = verified Switcher x verified MPU, + end-to-end qemu + multi-core Renode placement demo -> REQ-PIX-004/DD-025 ARINC-653), + VER-OS-HM-001 (Health-Monitor cross-sensor voting + per-cause failsafe demonstrator -> + REQ-PIX-009 F100 failsafe), VER-OS-TIMER-001 (tickless component sleep over the verified + executor), VER-OS-SYSCALL-001 (gust:os seam). Plus a spar/AADL board.SoC.device model + + `gust-target-gen` (emits per-target constants / memory.x / WIT worlds), SILICON-VALIDATED on + STM32F100 (jess's F100 gust core!) + STM32G474. So the safety FSMs jess's failsafe+partition + need are now DELIVERED+verified, not a watch item. STILL NOT SHIPPED as standalone assets: the + v0.5.0 release ships only msgq/mutex/sem .o (msgq still needs the ~9-symbol 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) + the gust:os probes - the verified + FSMs/executor themselves aren't standalone linkable .o. So to CONSUME them jess still links the + fused gale-nano core (or asks gale to expose the seam) - the concrete gale ask to FILE when + jess can bind (#369/float-gated, not yet). gust-target-gen may reconcile with jess's own + hardware/pixhawk6x-rt.aadl (both model the F100) - a coordination item to check. - 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 diff --git a/artifacts/phase2-pixhawk.yaml b/artifacts/phase2-pixhawk.yaml index 122c164..77b3b11 100644 --- a/artifacts/phase2-pixhawk.yaml +++ b/artifacts/phase2-pixhawk.yaml @@ -148,6 +148,12 @@ artifacts: campaign: NavState delayed 1-2 ticks / jittered +-1 must keep hover + rotor-out passing). Per-core compiles gated on the synth float poles (#719 f32 + f64 phase-2; note falcon-flight has 4 f64-dense funcs so M7 double-FP is a real dependency - AFD-024). + GALE v0.5.0 GROUNDING 2026-07-24 (DD-023): the ARINC-653 two-level partition (DD-025) now has a + VERIFIED gale substrate - VER-OS-SWITCH-001 (two-level partition switch = verified Switcher x + verified MPU, proven end-to-end on qemu + a multi-core Renode placement demo) + VER-OS-ISO-001 + (I-ISO MPU region-swap as the hardware isolation boundary). So the partition-switch + memory- + isolation mechanism jess's 3-core partition needs is verified upstream; jess consumes it by + linking the fused gale-nano core per DD-023. fields: category: functional priority: should @@ -298,6 +304,14 @@ artifacts: default); the Renode stm32f103 confirmation runs hermetically with no board write. Offered on gale#65. Caveat: F100 = Cortex-M3 = thumbv7m (no DSP/FPU) - confirm synth M3 path + recalibrate fuel->cycles (kiln R4). + GALE v0.5.0 GROUNDING 2026-07-24 (the 0.5 safety track CUT, DD-023): gale now ships the + VERIFIED failsafe substrate this requirement needs - VER-OS-HM-001 (Health-Monitor cross-sensor + voting + per-cause failsafe demonstrator) + VER-OS-TIMER-001 (tickless component sleep over the + verified executor) + VER-OS-SYSCALL-001 (gust:os seam), and a gust-target-gen spar/AADL model + SILICON-VALIDATED on the STM32F100 (VER-TARGET-IWDG-001, + ADC/Vrefint). So the F100 gale-nano + failsafe FSM is verified upstream; jess's rung is to fuse+run it on the F100/M3 (extends the gust + pass-through TEST-PIX-028) - consumed by linking the fused gale-nano core (the standalone + kernel-seam .o is not a release asset; see DD-023). fields: category: functional priority: could