chore: Shan-readiness — docs/AGENTS/.bazelversion + Verus quickstart doc - #32
Merged
Conversation
…kstart Punch-list items from the second-pass "Shan reviewer" audit. Lands the in-progress quickstart doc together with the surrounding doc hygiene needed for it to be honest: 1. AGENTS.md L107-121 — drop `nix develop --command` prefix from the four bazel test invocations. There is no flake.nix in the repo; the prefix was misleading. Replaced with plain `bazel test ...` plus a one-paragraph note that nix-build must be on PATH (and how to put it there) because rules_rocq_rust pulls Nix for toolchain resolution. 2. .bazelversion — new file pinning Bazel 9.1.0 (matches what bazelisk currently resolves to on Linux runners and locally on macOS). Without the pin, Bazelisk's default would silently drift the day a new release lands. 3. docs/safety/verification-honesty.md — append a "Trusted code: external_body, assume_specification, --no-cheating" section. Closes the only real correctness gap in the honesty story: the doc was silent on Verus's trusted-base annotations. New table enumerates 133 external_body instances + 2 assume_specification calls per file (net_buf 36, pm 22, ipc 22, mmu 20, usage 18, thread_lifecycle 5, sched 4, poll 3, mpu 3). Notes that today's CI does NOT pass --no-cheating, intentionally, and that a --no-cheating run would correctly fail until those trust units are discharged. 4. README.md L21 — anchor the headline "805 verified, 0 errors" claim with a footnote linking to verification-honesty.md and stating that the number is gated by the formal-verification.yml CI job (i.e., when that job is red, the number is stale until it goes green again). No change to the number itself; PR #31 is the companion fix that gets the Verus job back green. 5. docs/research/verus-quickstart-for-shan.md — new file. The hand-off doc for arsene1995 (Shan) following microsoft/verus-proof-synthesis#45. Includes the two table-cell patches from the punch list: - --verify-module: caveat that Verus parses the whole crate from src/lib.rs before isolating to the named module, so a parse error elsewhere poisons even targeted runs. - --no-cheating: now lists assume_specification alongside assume / admit / external_body, and points at the trusted- base inventory in verification-honesty.md. Companion to PR #31 (which fixes the parse error in src/ring_buf.rs that has had formal-verification.yml red on main since Apr 24). This PR is doc/process hygiene only — no Rust source touched. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Codecov Report✅ All modified and coverable lines are covered by tests. 📢 Thoughts on this report? Let us know! |
avrabe
added a commit
that referenced
this pull request
May 10, 2026
Pushed the wasm-cross-LTO experiment all the way to a buildable bench ELF integrated via wasm-ld+arm-ar+linker-substitute. Discovered an additional synth backend bug while attempting silicon measurement: synth's emitted memset/memcpy/memmove don't terminate correctly on Zephyr's startup `memset(bss, 0, sizeof(bss))` invocation. The chip hangs in memset+0x4c forever, bouncing between offsets 0x668 and 0x67e in a tight inner loop. The synth disassembly reveals i64 shift instructions (`subs.w r3, r2, #32; rsb r3, r2, #32; lsl.w r3, r1, r3`) lowered into what should be a byte-counter loop — same root cause as the u64-packed FFI return codegen issue documented earlier: synth's i64 codegen is incomplete. End-to-end status: - wasm-ld static-merging: WORKS. shim.wasm.o + libgale_ffi.a → 1MB merged.wasm with z_impl_k_sem_give and gale_k_sem_give_decide both present. - synth inlining at merged-module scope: STRUCTURALLY WORKS. The output `z_impl_k_sem_give` body has zero bl gale_k_sem_give_decide instructions. Verified by disassembly. 138 bytes vs LLVM-LTO's 82 bytes — 1.68x larger but inlined. - Bench integration: BUILDS. CMake bench builds with -DGALE_WASM_LTO_OVERRIDE_SEM_GIVE=1 + custom libgale_ffi.a + --allow-multiple-definition. Final ELF 219 KB FLASH, 66 KB RAM. - Chip boot: BLOCKED. PC stuck in synth-emitted memset. Workarounds via objcopy --weaken-symbol, --strip-symbol, --redefine-sym all failed to evict synth's broken memset bytes from the final ELF. Three synth backend issues filed against pulseengine/synth, ordered: 1. (blocker) memset/memcpy/memmove i64-codegen non-termination — prevents the merged-wasm bench from booting at all. 2. u64-packed FFI return unpacking — ~50% of the LTO-parity size delta. Same i64-codegen root cause as #1. 3. wasm linear-memory access lowering — ~20% of the size delta. Cosmetic compared to #1 and #2. Plus one issue against pulseengine/loom: - Z3 SortDiffers panic in inline_functions pass on i64-heavy wasm modules. Without loom, the verified-LTO claim doesn't hold. The structural claim — "wasm-cross-LTO via PulseEngine pipeline dissolves the C↔Rust seam at wasm IR level" — is **proven by disassembly**. The cyclical claim — "silicon timing matches LLVM-LTO" — is **blocked on synth's memset codegen**. Neither is a fundamental architectural barrier; both are well-scoped engineering work. This commit only updates the NOTES with the integration findings. The bench source is restored to clean state (the gale_sem.c #ifndef edit was transient) and verified building unchanged at 27 KB FLASH at the canonical rustc-direct path. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
avrabe
added a commit
that referenced
this pull request
Jun 24, 2026
…ves its toolchain via execroot path The Bazel 8 pin got the module loading, analyzing, building (16 actions) and the three tests EXECUTING — they then died at runtime, all three: ...renode_1.15.3+...-dotnet_portable/renode-test: No such file or directory Root cause: rules_renode's renode_test wrapper (defs.bzl:104) invokes the toolchain binary by its EXECROOT-relative path "external/rules_renode++renode+renode_toolchain/.../renode-test". Inside the test's runfiles tree (CWD = ...runfiles/_main) that path only resolves if Bazel materialises the legacy "_main/external/<repo>" symlinks — i.e. --legacy_external_runfiles. Its default flipped to false in recent Bazel, so the wrapper can't find renode-test. The rule was authored when it defaulted true (matching upstream's bazelisk-latest CI at the time). Setting it true in the module .bazelrc restores resolution. Verified in 8.7.0 that the flag exists and defaults false (bazel help test). This is the same upstream-friction item (task #32): the rule should rlocation the toolchain binary instead of relying on the execroot path + legacy symlinks. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
avrabe
added a commit
that referenced
this pull request
Jun 24, 2026
…stack (north-star end-to-end) (#105) * feat(gust): gust_stack — the dissolved CM composition driven ON the kiln stack (north-star end-to-end) gust_fused proved the dissolve (CM → meld fuse → synth → run-demo()=53, one-shot). gust_stack proves the other half — "running on our stack": the kiln-async Scheduler (gust's executor) drives the SAME dissolved composition (gale-app-demo + gale-kiln, fused → native) as the body of a kiln task, re-polled every scheduler round. Bare-metal qemu Cortex-M3: 5000 poll rounds, dissolved run-demo()=53 each round, 0 mismatches, no wasm runtime. So the whole BYO-OS north-star executes end-to-end: components on top (Component Model) → meld fuse (one merged-memory module) → synth dissolve (native) → driven by the kiln-async scheduler on the gust stack. - src/bin/gust_stack.rs — kiln Scheduler + the dissolved run-demo as the task body. - build.rs — links fused.o into gust_stack too (scoped -bin=). - DEMONSTRATOR.md — the on-stack section. - rivet FIND-BYOOS-008 (verifies REQ-BYOOS-MULTIRT-001, related-to SAC-BYOOS-EXEC); rivet validate PASS. Next rungs: a richer driven example (engine_control control-loop as the task body) and the same on real silicon (G474RE/F100). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * feat(gust): rung 1 — engine_control driven on the kiln stack (realistic sensors→actuators loop) gust_control: the kiln-async scheduler drives the dissolved engine_control algorithm (synth-dissolved control_step, same as control.c / the WIT component) as its task body — one control tick per scheduler round: synthesize a crank sample → control_step → spark/fuel actuators. Where gust_stack drives the fixed-result run-demo, this drives a real control loop, the workload an engine node runs. Bare-metal qemu Cortex-M3: gate control_step(3000,50,80,0) = spark 33° fuel 2300µs (== C/wasmtime); 5000 ticks; last sample control_step(4700,75,80,0) = spark 38° fuel 2440µs (== wasmtime). Dissolved, no runtime, on the gust/kiln stack. Two TCB-integration findings (documented): - control_step needs synth --native-pointer-abi (it reads ignition/fuel TABLES from wasm linmem; the plain --relocatable .o emits no data section → reads 0) + --shadow-stack-size 8192 (else it reserves the full 128KB linmem as .bss and overflows RAM — synth#383 class). And an r11=0 TCB trampoline: native-pointer-abi pins the linmem base to r11==0, which the kiln scheduler clobbers, so in-loop calls need r11 re-zeroed (same shim the dissolved gust kernel uses). - Built with SYNTH_NO_LOCAL_PROMOTE=1: v0.14.0's default-on local promotion register-exhausts on this denser function (filing to synth — the promotion cost-gate needs register-pressure awareness; the non-promoted lowering is fine). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * feat(gust): rung 2 — engine_control on the kiln stack runs on REAL Cortex-M4 silicon (G474RE) gust_control flashed on the physical NUCLEO-G474RE (probe-rs): the kiln-async scheduler drives the dissolved engine_control control loop on real hardware — control_step(3000,50,80,0)=spark33/fuel2300 (== C/wasmtime), 5000 ticks, last (4700,75,80,0)=spark38/fuel2440 (== wasmtime). The full north-star executes on silicon: components (CM) → meld fuse / synth dissolve → driven by kiln on gust, Cortex-M4, no runtime. - wasm-kernel/control_step-cm4.o — cortex-m4 dissolve (native-pointer-abi + shadow-stack-size 8192, SYNTH_NO_LOCAL_PROMOTE per synth#474); build.rs picks cm4 for thumbv7em / cm3 for qemu+F100 (the cortex-m3 .o won't link into M4). - silicon/RESULTS-g474re.md — the on-silicon rung-2 record. F100/M3 silicon pending the board. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * feat(gust): rules_renode CI-cycle gate — 3 M3 device classes (kernel 8K + control 64K + real STM32F100) The durable answer to "why not renode": a one-off `renode --console` on a dev box isn't reproducible — a Bazel `renode_test` target is. Extend the existing self-contained renode-test module (own MODULE.bazel + git_override on pulseengine/renode-bazel-rules) from one target to three M3 device classes, each with a checked-in hermetic .repl (no dependency on the pinned Renode's bundled platform set): - gust-renode generic M3 8K — dissolved gust kernel (existing) - gust-control-renode M3 64K (F103RE)— north-star rung 1: kiln driving the dissolved engine_control control_step; deterministic cycle count - gust-f100-renode STM32F100RB — the real STM32VLDISCOVERY part (8K/128K), dissolved kernel pinned to its memory class gust_control's 9408 B .bss needs the 64K class — it does NOT fit the F100's 8K SRAM, so the F100 target runs the kernel and the 64K F103RE-class runs the control loop (honest device-fit constraint). Verified locally on the same Renode engine (1.16.1): gust_control = 0x162CB6 = 1,453,238 instr over RunFor 2s, no fault, SP at the 64K top; the kernel on F100 = 200,000,000 instr, bss fits (ends 0x200012B4 under the 8K top 0x20002000), no fault. M3 is cacheless so instr ≈ cycles — this is the CI-reproducible cycle- class seed, complementary to the qemu correctness gate and the G474RE DWT bench. Honest finding (documented in README): the SemihostingUart heartbeat is NOT capturable headless on the macOS portable (CreateFileBackend on cpu.uartSemihosting captures nothing), and the repo's proven `Wait For Line` tests assert on a real USART, not a SemihostingUart — so a content assertion is deferred to CI rather than added blind (would risk a 120s timeout -> CI-red). Correctness stays gated by the qemu exit-code run + gale_decider_diff; Renode adds the cycle dimension. Also adds a targeted .gitignore rule for .claude/pulseengine/ agent working state (per the issue-hunt skill) so per-package working-context.md can't be committed by accident. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * ci(gust): wire the renode-test bazel targets into CI + fix Bazel-9 load break No workflow ran the gust renode-test bazel targets — so the module's "first green is in CI" was aspirational, and a latent break went unnoticed: under the repo's pinned Bazel 9.1.0, rules_renode (pinned 5fc76ad) fails to LOAD because its renode/defs.bzl uses PyInfo / py_* as builtins, which Bazel 8+ removed ("name 'PyInfo' is not defined", defs.bzl:10 and :179). The existing gust-renode target was equally broken; nothing exercised it. Fixes: - benches/gust/renode-test/.bazelrc: re-inject the legacy Python globals via --incompatible_autoload_externally so the pinned rule loads unmodified, and --check_direct_dependencies=off for the rules_python 0.36.0->1.7.0 transitive skew. Verified locally: `bazel query //:*` now resolves all three targets on Bazel 9.1.1 (was: load error). - .github/workflows/gust-renode.yml: a dedicated Linux job running `bazel test //:gust-renode //:gust-control-renode //:gust-f100-renode`. This is the actual CI runner that makes the dissolved-artifact, real-M3-model, deterministic-cycle gate reproducible (no board), complementing renode-tests.yml (Zephyr sem robots) and zephyr-tests.yml (qemu M3 functional). Upstream friction to file on pulseengine/renode-bazel-rules: defs.bzl should `load("@rules_python//python:defs.bzl", "PyInfo", ...)` rather than rely on the removed builtins (breaks on Bazel 8/9 without the autoload shim). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * ci(gust): pin renode-test module to Bazel 8 (rules_renode is Bazel-9-incompatible) First CI run failed at analysis on Bazel 9.1 with a second, deeper break beyond PyInfo: "@@rules_shell+//shell/runfiles:runfiles_impl must produce a single file". Root cause: the pinned rules_renode (5fc76ad == upstream HEAD, nothing newer to bump to) is authored against Bazel 8 — it relies on the PyInfo/py_*/sh_* globals AND the old rules_shell runfiles_impl single-file behavior, all of which Bazel 8 provides via the DEFAULT --incompatible_autoload_externally migration set. Bazel 9 emptied that set (migration window closed), so gale's root-pinned 9.1.0 breaks the module at both load and analysis. Upstream's own CI uses bazelisk-latest with no .bazelversion (i.e. Bazel 8), so 8.x is the known-good config. Fix: a module-local .bazelversion (8.7.0) — bazelisk picks the nearest one from cwd, so it overrides root 9.1.0 only for this self-contained module (own MODULE.bazel; the rest of gale stays on 9.1.0). Dropped the explicit --incompatible_autoload_externally override from .bazelrc: on Bazel 8 its default set already covers both py_* and sh_*; replacing it with only the py symbols would have broken the sh_* autoload the runfiles path needs. Verified: `bazel query //:*` resolves all three targets on 8.7.0 with no autoload flag. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * ci(gust): --legacy_external_runfiles=true — renode_test wrapper resolves its toolchain via execroot path The Bazel 8 pin got the module loading, analyzing, building (16 actions) and the three tests EXECUTING — they then died at runtime, all three: ...renode_1.15.3+...-dotnet_portable/renode-test: No such file or directory Root cause: rules_renode's renode_test wrapper (defs.bzl:104) invokes the toolchain binary by its EXECROOT-relative path "external/rules_renode++renode+renode_toolchain/.../renode-test". Inside the test's runfiles tree (CWD = ...runfiles/_main) that path only resolves if Bazel materialises the legacy "_main/external/<repo>" symlinks — i.e. --legacy_external_runfiles. Its default flipped to false in recent Bazel, so the wrapper can't find renode-test. The rule was authored when it defaulted true (matching upstream's bazelisk-latest CI at the time). Setting it true in the module .bazelrc restores resolution. Verified in 8.7.0 that the flag exists and defaults false (bazel help test). This is the same upstream-friction item (task #32): the rule should rlocation the toolchain binary instead of relying on the execroot path + legacy symlinks. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.8 (1M context) <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.
Summary
Punch-list items from the second-pass "Shan reviewer" audit. Lands the in-progress Verus quickstart doc together with the doc hygiene needed for it to be honest. Companion to #31 (the Verus parse-error fix); this PR is doc/process only — no Rust source touched.
Changes
Audit cross-references
This PR addresses items from the punch list:
Test plan
🤖 Generated with Claude Code