build(bazel): migrate crate_universe from_specs → from_cargo (#242) by avrabe · Pull Request #422 · pulseengine/synth

avrabe · 2026-06-22T15:51:41Z

What

Replaces the 21 hand-maintained crate.spec pins + crate.from_specs() in MODULE.bazel with:

crate.from_cargo(
    cargo_lockfile = "//:Cargo.lock",
    manifests = ["//:Cargo.toml"],
)

The Bazel crate set is now resolved from the same Cargo.lock that cargo test --workspace and cargo publish use — Cargo.lock becomes the single source of truth, and the manual-spec maintenance burden is gone.

Why now (VCR-MEM-001 layer-2, #242)

Layer-2 needs scry-sai-core as a production dep of synth-cli. Under from_specs, that meant hand-adding scry + its ~27 transitive crates to MODULE.bazel (a drift-prone cascade re-audited on every scry bump). Under from_cargo, a new Cargo dep is picked up from Cargo.lock automatically — no MODULE.bazel edit at all. This PR is the dep-architecture decision for layer-2, landed as pure infra ahead of the scry wiring (kept separate so the oracle stays clean).

This is a drift correction, not "behavior-preserving"

The manual specs had silently drifted from the workspace manifests:

crate	manual spec	Cargo.lock (cargo truth)
z3	`0.12`	`0.19` (synth-verify/Cargo.toml)
wast	`219.0`	`248.0.0`

from_cargo builds the Cargo.lock versions, aligning Bazel to cargo/crates.io. Per the #383-scope lesson I'm stating this as an alignment/correction, not "binary-identical infra."

Validation

The @crates surface is only crates/BUILD.bazel (verified repo-wide; the .claude/worktrees/ hits are stale agent worktrees, not in the build). The crates hub name is unchanged, so every @crates//:<pkg> resolves as before — from_cargo aliases each direct dep of a workspace member (chrono, z3, proptest, … all confirmed direct deps).

Local (darwin):

bazel build //crates:synth → full compile, exit 0 (synth-core, synth-synthesis, synth-backend, synth bin; wasmparser 0.248, wast 248).
bazel build //crates:all --nobuild → all 21 targets analyze green, including the z3 + chrono synth-verify target (the labels most at risk of vanishing under from_cargo's direct-deps-only aliasing).
bazel build //coq:verify_proofs //tests/renode/... --nobuild → green.

The proofs/renode execution (nix + emulator) is dep-resolution-independent — its analysis passing means every transitively-needed @crates label resolves. CI's "Bazel Build & Proofs" job (bazel build //crates:synth + bazel test //coq:verify_proofs + renode) is the full gate and the real verifier for this change.

Frozen differential fixtures (control_step 0x00210A55, flight_algo 0x07FDF307, divseam) are generated by the cargo-built binary (scripts/repro/*_differential.py), so this Bazel-only change cannot move them.

Note: MODULE.bazel.lock was regenerated on darwin; CI is linux. Bazel 7.4.1 defaults to --lockfile_mode=update (no lockfile_mode=error pin in .bazelrc), so CI self-heals the cross-platform lock rather than reddening.

Refs #242 (VCR epic).

🤖 Generated with Claude Code

@crates

Replaces the 21 hand-maintained `crate.spec` pins + `crate.from_specs()` with `crate.from_cargo(cargo_lockfile="//:Cargo.lock", manifests=["//:Cargo.toml"])` so the Bazel crate set is resolved from the SAME Cargo.lock that `cargo test --workspace` and `cargo publish` use — making Cargo.lock the single source of truth and eliminating the manual-spec maintenance burden. Motivation (VCR-MEM-001 layer-2, #242): promoting a new production dep such as scry-sai-core no longer requires hand-adding it plus its ~27 transitive crates to MODULE.bazel — from_cargo picks the whole closure up from Cargo.lock automatically. This is a DRIFT CORRECTION, not behavior-preserving infra: the manual specs had drifted from the workspace manifests (z3 pinned 0.12 here vs 0.19 in synth-verify/Cargo.toml; wast 219.0 vs the resolved 248.0.0). from_cargo builds the Cargo.lock versions, aligning Bazel to cargo/crates.io. The crate `crates` hub name is unchanged, so every `@crates//:<pkg>` reference in crates/BUILD.bazel resolves as before (from_cargo aliases each direct dep of a workspace member: chrono, z3, proptest, … all confirmed present). Local validation (the @crates surface = crates/BUILD.bazel is the ONLY file referencing it repo-wide): - `bazel build //crates:synth` → full compile, exit 0 (synth-core, synth-synthesis, synth-backend, synth bin; wasmparser 0.248, wast 248). - `bazel build //crates:all --nobuild` → all 21 targets analyze green, including the z3+chrono `synth-verify` target. - `bazel build //coq:verify_proofs //tests/renode/... --nobuild` → green. The proofs/renode EXECUTION (nix + emulator) is dep-resolution-independent and is CI's "Bazel Build & Proofs" gate — the real verifier for this change. Frozen differential fixtures (control_step 0x00210A55, flight_algo 0x07FDF307, divseam) are generated by the CARGO-built binary (scripts/repro/*_differential.py), so this Bazel-only change cannot move them. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

codecov · 2026-06-22T16:17:00Z

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!

#242, #383) (#423) Closes the join the #392 spike and the shadow_budget unit suite each cover only half of: `layer2_budget_pipeline_msgq_end_to_end_383` (synth-cli main.rs cfg(test)) runs scry's `analyze()` on the REAL msgq_put_359.wasm gust fixture, maps its proven StackBound through the synth-owned StackDepthBound (the 1:1 adapter that becomes `impl From<scry::StackBound>` when 2b promotes scry to a production dep), feeds `budget_from_bound`, and asserts the 2048x over-reservation (65536 B page) collapses to a PROVEN 32-byte budget — source=ProvenStackDepth, preferred over the asserted 4096 fallback. Frozen-safe: scry-sai-core stays a DEV-dependency exercised only under cfg(test), so the production binary pulls no scry and emits identical bytes (the change is entirely in #[cfg(test)] code). No MODULE.bazel pin (tests are not in the Bazel graph). Independent of the from_cargo migration (#422) — it uses the existing dev-dep under the current resolution. This test is the oracle the gated 2b wiring (`--shadow-stack-size auto`) must match. Roadmap VCR-MEM-001 updated with the end-to-end criterion. Verification: `cargo test -p synth-cli --bin synth layer2_budget_pipeline` → pass (alongside the 9 shadow_budget units); fmt + clippy -D warnings clean; rivet check zero non-xref errors. Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>

…map (VCR-DBG-001, #242, #394) (#427) PR A of the v0.12.0 DWARF `.debug_line` release: close the encoder machine-offset gap so a later step can emit source-line debug info. `compile_wasm_to_arm` now captures a `LineMap = Vec<(machine_offset, wasm_op_index)>` during the encode loop — `code.len()` immediately before each `encode()` is the instruction's final offset within the function's `.text` (the trailing literal pool is appended at the end and the LDR patch is in-place, so earlier offsets never shift). Carried on `CompiledFunction.line_map`. Frozen-safe by construction: the map is captured but NEVER serialized, so the emitted `.text` is byte-identical with or without it. Proven by the existing differential fixtures staying green plus `test_line_map_is_wellformed_dbg001`, which asserts monotonic, in-bounds offsets and that recompilation yields identical code. ARM only; the RISC-V backend carries an empty map (DWARF emit there is a follow-up). Next (PR B): gimli as a production dep (auto-picked up by Bazel via from_cargo, #422), read the input wasm's `.debug_line`, and emit a non-ALLOC `.debug_line` section behind a `--debug-line` flag, gated by an additivity byte-diff oracle. Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>

avrabe mentioned this pull request Jun 22, 2026

test(vcr-mem): layer-2 end-to-end budget pipeline on real gust fixture (#242, #383) #423

Merged

avrabe merged commit 5c3f098 into main Jun 22, 2026
9 checks passed

avrabe deleted the spike-from-cargo-migration branch June 22, 2026 16:16

avrabe mentioned this pull request Jun 22, 2026

feat(dwarf): capture per-instruction machine-offset → wasm-op source map (VCR-DBG-001, #242) #427

Merged

avrabe mentioned this pull request Jun 22, 2026

feat(dwarf): emit DWARF debug sections behind --debug-line (VCR-DBG-001, #242, #394) #429

Merged

Navigation Menu

Uh oh!

build(bazel): migrate crate_universe from_specs → from_cargo (#242) - #422

build(bazel): migrate crate_universe from_specs → from_cargo (#242)#422
avrabe merged 1 commit into
mainfrom
spike-from-cargo-migration

avrabe commented Jun 22, 2026

Uh oh!

Uh oh!

codecov Bot commented Jun 22, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Uh oh!

Conversation

avrabe commented Jun 22, 2026

What

Why now (VCR-MEM-001 layer-2, #242)

This is a drift correction, not "behavior-preserving"

Validation

Uh oh!

Uh oh!

codecov Bot commented Jun 22, 2026

Codecov Report

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant