coord: gale v0.4.0 delivered the TCB substrate — gust:os seam + verified msgq/mutex/sem; msgq = the verified NavState IPC carrier - #162
Merged
Conversation
…ied msgq/mutex/sem (cortex-m4f); msgq = the verified NavState IPC carrier 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 <noreply@anthropic.com>
…ered vs the 0.5 SAFETY track (in-progress on main, VERs proposed, NOT released) 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 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
User-flagged supplier movement ("gale has tools now"). jess SHA-verified the gale v0.4.0 assets and records in the DD-023 coordination map what GALE now supplies.
What gale v0.4.0 delivered
gust:ostyped capability seam —log.line+spawnon the Verus-proven executor (1081+ obligations, no-lost-wakeups/bounded-poll/fair-pick) through a WIT-typedgust:os/taskdispboundary.VER-OS-SYSCALL-001verified; no-lost-wakeups discharged tri-track (Verus+Kani+Rocq)..o:gale-wasm-msgq(Zephyr k_msgq — exportsz_impl_k_msgq_put/gale_k_msgq_put_decide; undefined syms = thegale_w_*kernel seam),-mutex,-sem. SHA-verified (msgq.o74646afb…,.wasm6c990474…).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 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. Thegust:osseam + executor are the gale-nano substrate for REQ-PIX-002 (M7 native base) / REQ-PIX-009 (F100).rivet validate→ PASS. (Architecture-sync only; design-decisions.yaml.)🤖 Generated with Claude Code