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