docs(release): rethink v0.7.0 — CM drivers, three hardware targets, ARINC with component tenants - #243
Open
avrabe wants to merge 2 commits into
Open
docs(release): rethink v0.7.0 — CM drivers, three hardware targets, ARINC with component tenants#243avrabe wants to merge 2 commits into
avrabe wants to merge 2 commits into
Conversation
…, signed, and checked from outside v0.6.0's gale-nano is live on ghcr, signed keyless, and tools/verify-published-component.sh run outside any gale checkout confirms it: cosign validated the claims, found the transparency-log entry, and verified the certificate against trusted CAs; the pulled bytes are a valid component whose residual imports are exactly gust:hal/mmio and gust:os/taskdisp, with gust:sched absent and five gust:os exports. All six packages verify signed. That is the first time the delivery invariant has been checked on what was actually delivered rather than on a local build, which is what the decision always meant. So DD-OS-DELIVERY-001 moves implemented -> verified. REQ-OS-PUBLISH-001 carries the delivery half as its own requirement rather than widening REQ-OS-DELIVERY-001, keeping the split that made the earlier honesty possible: while the publish had no evidence, nothing claimed it did. VER-OS-PUBLISH-001 also records how this went, because the failures are the useful part. Three publish attempts failed, each a defect in a path no PR gate could reach — the job is tag-gated, so every PR skipped it and its first execution was the release itself: a missing wac, a `wkg oci login` that never existed, and cosign left without credentials when that login was removed. The third attempt pushed gale-nano-exec and failed to sign it, leaving an unsigned artifact in the registry until the successful run signed the same digest in place. rivet validate: PASS check-v-closure: OK — 24 REQ/VER pairs Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
…re targets, ARINC with component tenants
The first v0.7.0 sketch ("Run It") scoped depth on one claim: execute the composite. That
was the right question before v0.6.0 delivered and is too narrow now that it has. With the
OS shipping as one signed, externally-verified component, the live question is how far
DOWN the component model reaches and whether it holds on more than one chip.
Three axes, each of which v0.6.0 left open in a stated way:
A — the drivers are still core modules importing raw env.mmio_read32. gust:hal already
declares nine interfaces and nothing speaks them. Componentizing the eight thin drivers
closes the typed graph from app through OS through drivers to the hardware seam. The
transformation is already proven on exec-provider, including its consequence for the
dissolved object's symbol shape.
B — two of three hardware targets are done for drivers (M4, M3). RV32 is the real gap and
it is now ours, not the compiler's: synth 0.53 lowers 8/8 with counts identical to ARM, so
what is missing is an RV32 target model and at least one driver against REAL ESP32-C3
registers. The existing eight carry STM32 maps; lowering them for RV32 proves the
toolchain crosses and would be meaningless to run. This axis absorbs the old execution
rung — running on three chips IS executing, and the host-engine run stays first because it
is the cheapest thing that can refute v0.6.0's structural claims.
C — the ARINC-653 outer switch is NOT the gap: its proofs are complete and
VER-OS-SWITCH-001 is verified. What is missing is that it has only ever run on Renode, and
that its partitions host native code rather than component tenants. Partitioning native
code is well-understood; partitioning signed gust:os-importing components, with spatial
isolation supplied by the region-swap the switch already proves ordered, is what this stack
is for. C depends on A.
Also notes why C makes one of the Research Day asks urgent rather than academic: if
partitions host components and meld fuse --memory shared has flattened their memories, the
isolation argument must come from the region-swap, not from the component model.
Co-Authored-By: Claude <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
Codecov Report✅ All modified and coverable lines are covered by tests. 📢 Thoughts on this report? Let us know! |
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.
Replaces the first v0.7.0 sketch ("Run It"). That scoped depth on a single claim — execute the composite — which was right before v0.6.0 delivered and is too narrow now that it has.
Where v0.6.0 actually left us
gust:hal/mmio+ app task poll, verified from outsideenvmmio importsA — Component-model drivers, all the way down
The composition is typed from app to OS and then falls off a cliff: drivers import
env.mmio_read32.gust:halalready declares nine interfaces (mmio,irq,gpio,spi,timer,dma,uart,uart-byte,uart-block) and nothing speaks them.Proven transformation —
exec-providerdid exactly this in v0.6.0, including the dissolved object's symbol-shape change. This is the precondition for C: you cannot put a driver in a partition as a component if it isn't one.B — Three hardware targets, one wasm
M4 and M3 are done. RV32 is the gap, and it's now ours rather than the compiler's — synth 0.53 lowers 8/8 with counts identical to ARM. What's missing: an RV32
targets/model, and at least one driver against real ESP32-C3 registers. The existing eight carry STM32 maps; lowering those for RV32 proves the toolchain crosses and would be meaningless to run.Absorbs the old execution rung — running on three chips is executing. The host-engine run stays first because it's the cheapest thing that can refute v0.6.0's structural claims.
C — ARINC-653: components in the partitions, on silicon
The switch is not the gap. Its proofs are complete,
VER-OS-SWITCH-001verified: window-end preemption un-maskable by inner code, region-swap always applied before the entering partition's first instruction.Missing: (1) it has only ever run on Renode; (2) its partitions host native code, not components. Partitioning native code is well-understood. Partitioning signed
gust:os-importing component tenants, with isolation supplied by the region-swap the switch already proves ordered, is what this stack is for.Kill-criterion: a partition running past its window on silicon, a region-swap applied after resume, or a component tenant reaching another partition's memory or scheduler state.
Sequencing
A gates C. B1 first regardless — cheap, independent, can refute. B2 has the only real unknowns, so start its target model early.
One consequence worth flagging: C makes a Research Day ask urgent rather than academic. If partitions host components and
meld fuse --memory sharedhas flattened their memories, the isolation argument has to come from the region-swap, not from the component model.🤖 Generated with Claude Code
https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo