chore(release): v0.12.0 — DWARF source-line debugging (VCR-DBG-001, #242)

CHANGELOG.md

@@ -7,6 +7,47 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## [Unreleased]
 
+## [0.12.0] - 2026-06-23
+
+**DWARF SOURCE-LINE DEBUGGING — `--debug-line` (VCR-DBG-001, #394, epic #242).**
+The first release of the north-star verified-codegen campaign. `synth compile
+--debug-line` now emits debugger-readable DWARF (`.debug_info` / `.debug_abbrev`
+/ `.debug_str` / `.debug_line`) mapping ARM `.text` addresses back to the input
+wasm's source lines, so a synth-compiled relocatable object can be debugged at
+source level in gdb/lldb (and on-silicon via Renode) after linking. Built in
+three behavior-frozen steps — the feature is **purely additive**: with the flag
+off (the default) `.text`/`.data`/`.bss` and every frozen differential fixture
+stay **bit-identical**.
+
+- **PR A (#427)** — capture a per-instruction `machine_offset → wasm_op_index`
+  source map (`CompiledFunction.line_map`) during ARM encoding. Additive: the map
+  is never serialized, so `.text` is byte-identical.
+- **PR B (#429)** — emit a full DWARF unit behind `--debug-line` (the CU's
+  `DW_AT_stmt_list` reaches the line table the normal `dwarf.units()` way).
+  Promotes `gimli` to a production dependency.
+- **PR C (#430)** — emit `.rel.debug_*` relocations against a `__synth_text_base`
+  symbol so a host linker fixes up the embedded `.text` addresses to the final
+  load address. Verified end-to-end with a real `arm-none-eabi-ld` link:
+  `readelf --debug-dump=decodedline` resolves the relocated addresses to the
+  correct source lines. Generalizes the ELF builder to per-section REL tables
+  (frozen-safe: `.rel.text` stays byte-identical).
+  - *Experimental caveat:* `__synth_text_base` is a global symbol, so linking
+    more than one `--debug-line` object into a single image collides (fails loud
+    with `multiple definition`); a local-section-symbol follow-up is tracked.
+  - On a self-contained (`ET_EXEC`) or RISC-V build, `--debug-line` is a no-op
+    and warns (DWARF is emitted only on the ARM relocatable-object path).
+
+**VCR-MEM-001 layer-2 (frozen-safe scaffolding, #383/#242).** Added the
+scry-proven shadow-stack budget decision logic (`budget_from_bound` over a
+synth-owned `StackDepthBound`) plus its end-to-end and honest-fail oracles. Pure
+analysis/test code — no production wiring, no output change. The byte-changing
+`--shadow-stack-size auto` step remains separately gated.
+
+### Internal
+
+- Adapted the DWARF emitter to gimli 0.33's 6-argument `LineProgram::new`
+  (dependabot #436; fix #439). Bumped `wast` to 252 (#438).
+
 ## [0.11.51] - 2026-06-22
 
 **NATIVE-POINTER SHADOW-STACK SHRINK — #383 (VCR-MEM-001 layer-1): the

Cargo.toml

@@ -27,7 +27,7 @@ resolver = "2"
 # semver to publish, so the convention now catches up: workspace
 # version follows the release tag, bumped pre-tag in the release
 # checklist. See docs/release-process.md.
-version = "0.11.51"
+version = "0.12.0"
 edition = "2024"
 rust-version = "1.88"
 authors = ["PulseEngine Team"]

MODULE.bazel

@@ -7,7 +7,7 @@ module(
     name = "synth",
     # Kept in lockstep with [workspace.package] version in Cargo.toml.
     # Both are bumped pre-tag — see docs/release-process.md.
-    version = "0.11.51",
+    version = "0.12.0",
 )
 
 # Bazel dependencies

artifacts/verified-codegen-roadmap.yaml

@@ -1478,20 +1478,29 @@ artifacts:
           silently-wrong source lines after host-link. The v0.12.0 TAG is HELD for
           step 5c (advisor-confirmed: PR B in main is default-off + frozen-safe, so
           it banks the work at zero risk; the tag waits for relocations).
-        - step (5c) RELOCATIONS — PR C, REQUIRED before the v0.12.0 tag:
-          C1 = generalize elf_builder's `.rel.text`-ONLY relocation machinery to
-          PER-SECTION relocations, **REL form (not RELA)** — synth/ARM32 uses REL
-          with the addend stored in-place (`.rel.debug_*`, matching the existing
-          `.rel.text` convention); frozen-safe, gated on the existing `.rel.text`
-          fixtures (cabi_arena_realloc_linkability_418) staying byte-identical.
-          C2 = emit DWARF addresses via gimli `Address::Symbol{text_sym, addend}`,
-          extract the relocations, emit `.rel.debug_line` / `.rel.debug_info`
-          against the `.text` symbol. The C2 ORACLE must APPLY the relocations at a
-          NONZERO `.text` base and verify the address resolves to the CORRECT
-          source line (not merely that a reloc record exists). Advisor caution:
-          "do NOT rush the addend math into a debug-info path — careful (even next
-          session) beats fast."
-    status: approved
+        - step (5c) RELOCATIONS LANDED (PR C #430, merged 9a34c8d; SHIPS in
+          v0.12.0): C1 generalized elf_builder's `.rel.text`-ONLY machinery to
+          PER-SECTION REL tables (`extra_relocations` + `add_section_relocations`;
+          `.rel.debug_*`, REL in-place addend); byte-identical when off — the
+          frozen gust whole-`.o` no-op oracle is the end-to-end proof, and
+          cabi_arena_realloc_linkability_418 `.rel.text` stays byte-identical.
+          C2: a custom gimli `write::Writer` (`RelocWriter`) overrides ONLY
+          `write_address`, so just the two `.text` references (line program
+          `DW_LNE_set_address` + CU `DW_AT_low_pc`) become `R_ARM_ABS32` against a
+          global `__synth_text_base` (st_shndx=.text, value 0); internal DWARF
+          cross-refs stay concrete (do NOT use gimli's blanket `RelocateWriter`).
+          Addend 0 ⇒ `.debug_*` bytes byte-identical to PR B. Oracle
+          `rel_debug_relocations_shift_addresses_to_correct_line_394` applies the
+          reloc at a NONZERO base and asserts every row shifts by exactly the base
+          with its source line preserved; CONFIRMED end-to-end with a real
+          `arm-none-eabi-ld -Ttext=0x08000000` link (readelf decodedline → correct
+          lines). FAST-FOLLOW: `__synth_text_base` is global ⇒ linking >1
+          `--debug-line` object collides (fails LOUD); local-STT_SECTION fix is
+          blocked by the hardcoded `.symtab` sh_info=1 — jumps priority iff a
+          consumer links multiple synth objects. GOTCHA recorded: dependabot #436
+          (gimli 0.31→0.33, `LineProgram::new` 5→6 args) broke main after PR C
+          merged textually-clean on a stale base; fixed in #439.
+    status: implemented
     tags: [toolchain, dwarf, debuggability, elf, meld-coordination, feature-loop, release-v0.12.0, synth-394]
     links:
       - type: derives-from

crates/synth-backend-awsm/Cargo.toml

@@ -11,6 +11,6 @@ categories.workspace = true
 description = "aWsm backend integration for the Synth compiler"
 
 [dependencies]
-synth-core = { path = "../synth-core", version = "0.11.51" }
+synth-core = { path = "../synth-core", version = "0.12.0" }
 anyhow.workspace = true
 thiserror.workspace = true

crates/synth-backend-riscv/Cargo.toml

@@ -11,8 +11,8 @@ categories.workspace = true
 description = "RISC-V encoder, ELF builder, PMP allocator, and bare-metal startup for synth"
 
 [dependencies]
-synth-core = { path = "../synth-core", version = "0.11.51" }
-synth-synthesis = { path = "../synth-synthesis", version = "0.11.51" }
+synth-core = { path = "../synth-core", version = "0.12.0" }
+synth-synthesis = { path = "../synth-synthesis", version = "0.12.0" }
 anyhow.workspace = true
 thiserror.workspace = true
 tracing.workspace = true

crates/synth-backend-wasker/Cargo.toml

@@ -11,6 +11,6 @@ categories.workspace = true
 description = "Wasker backend integration for the Synth compiler"
 
 [dependencies]
-synth-core = { path = "../synth-core", version = "0.11.51" }
+synth-core = { path = "../synth-core", version = "0.12.0" }
 anyhow.workspace = true
 thiserror.workspace = true

crates/synth-backend/Cargo.toml

@@ -15,7 +15,7 @@ default = ["arm-cortex-m"]
 arm-cortex-m = ["synth-synthesis"]
 
 [dependencies]
-synth-core = { path = "../synth-core", version = "0.11.51" }
-synth-synthesis = { path = "../synth-synthesis", version = "0.11.51", optional = true }
+synth-core = { path = "../synth-core", version = "0.12.0" }
+synth-synthesis = { path = "../synth-synthesis", version = "0.12.0", optional = true }
 anyhow.workspace = true
 thiserror.workspace = true

crates/synth-cli/Cargo.toml

@@ -27,18 +27,18 @@ verify = ["synth-verify"]
 # Path deps carry `version` so `cargo publish` rewrites them to the
 # crates.io coordinate. Bumping the workspace version requires
 # updating these in lockstep — see docs/release-process.md.
-synth-core = { path = "../synth-core", version = "0.11.51" }
-synth-frontend = { path = "../synth-frontend", version = "0.11.51" }
-synth-synthesis = { path = "../synth-synthesis", version = "0.11.51" }
-synth-backend = { path = "../synth-backend", version = "0.11.51" }
+synth-core = { path = "../synth-core", version = "0.12.0" }
+synth-frontend = { path = "../synth-frontend", version = "0.12.0" }
+synth-synthesis = { path = "../synth-synthesis", version = "0.12.0" }
+synth-backend = { path = "../synth-backend", version = "0.12.0" }
 
 # Optional external backends
-synth-backend-awsm = { path = "../synth-backend-awsm", version = "0.11.51", optional = true }
-synth-backend-wasker = { path = "../synth-backend-wasker", version = "0.11.51", optional = true }
-synth-backend-riscv = { path = "../synth-backend-riscv", version = "0.11.51", optional = true }
+synth-backend-awsm = { path = "../synth-backend-awsm", version = "0.12.0", optional = true }
+synth-backend-wasker = { path = "../synth-backend-wasker", version = "0.12.0", optional = true }
+synth-backend-riscv = { path = "../synth-backend-riscv", version = "0.12.0", optional = true }
 
 # Optional verification (requires z3)
-synth-verify = { path = "../synth-verify", version = "0.11.51", optional = true, features = ["z3-solver", "arm"] }
+synth-verify = { path = "../synth-verify", version = "0.12.0", optional = true, features = ["z3-solver", "arm"] }
 
 # Optional PulseEngine WASM optimizer
 # Uncomment when loom crate is available:

crates/synth-frontend/Cargo.toml

@@ -14,7 +14,7 @@ description = "WASM/WAT parser and module decoder frontend for the Synth compile
 # Internal path deps carry an explicit version so `cargo publish`
 # can rewrite to the crates.io coordinate. `path` is used for
 # in-workspace builds; `version` is what crates.io sees.
-synth-core = { path = "../synth-core", version = "0.11.51" }
+synth-core = { path = "../synth-core", version = "0.12.0" }
 
 wasmparser.workspace = true
 wasm-encoder.workspace = true

crates/synth-opt/Cargo.toml

@@ -11,7 +11,7 @@ categories.workspace = true
 description = "Peephole optimization passes for the Synth compiler"
 
 [dependencies]
-synth-cfg = { path = "../synth-cfg", version = "0.11.51" }
+synth-cfg = { path = "../synth-cfg", version = "0.12.0" }
 
 [dev-dependencies]
 criterion = { version = "0.8", features = ["html_reports"] }

crates/synth-synthesis/Cargo.toml

@@ -11,9 +11,9 @@ categories.workspace = true
 description = "WASM-to-ARM instruction selection and peephole optimizer"
 
 [dependencies]
-synth-core = { path = "../synth-core", version = "0.11.51" }
-synth-cfg = { path = "../synth-cfg", version = "0.11.51" }
-synth-opt = { path = "../synth-opt", version = "0.11.51" }
+synth-core = { path = "../synth-core", version = "0.12.0" }
+synth-cfg = { path = "../synth-cfg", version = "0.12.0" }
+synth-opt = { path = "../synth-opt", version = "0.12.0" }
 serde.workspace = true
 anyhow.workspace = true
 thiserror.workspace = true

crates/synth-verify/Cargo.toml

@@ -17,12 +17,12 @@ arm = ["synth-synthesis"]
 
 [dependencies]
 # Core dependencies (always required)
-synth-core = { path = "../synth-core", version = "0.11.51" }
-synth-cfg = { path = "../synth-cfg", version = "0.11.51" }
-synth-opt = { path = "../synth-opt", version = "0.11.51" }
+synth-core = { path = "../synth-core", version = "0.12.0" }
+synth-cfg = { path = "../synth-cfg", version = "0.12.0" }
+synth-opt = { path = "../synth-opt", version = "0.12.0" }
 
 # ARM synthesis (optional, behind 'arm' feature)
-synth-synthesis = { path = "../synth-synthesis", version = "0.11.51", optional = true }
+synth-synthesis = { path = "../synth-synthesis", version = "0.12.0", optional = true }
 
 # SMT solver for formal verification
 z3 = { version = "0.19", features = ["static-link-z3"], optional = true }