Skip to content

coord: gale v0.4.0 delivered the TCB substrate — gust:os seam + verified msgq/mutex/sem; msgq = the verified NavState IPC carrier #162

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
avrabe merged 2 commits into from
Jul 23, 2026
Merged

coord: gale v0.4.0 delivered the TCB substrate — gust:os seam + verified msgq/mutex/sem; msgq = the verified NavState IPC carrier #162

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
6cd748e
coord: gale v0.4.0 delivered the TCB substrate — gust:os seam + verif…
avrabe Jul 23, 2026
e07bc37
coord: sharpen gale track discipline — v0.4.0 (cut, functional) deliv…
avrabe Jul 23, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
21 changes: 21 additions & 0 deletions artifacts/design-decisions.yaml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1235,6 +1235,27 @@ 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).
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
Expand Down
Loading