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>
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