feat(safety): Phase 1 — --safety-bounds umbrella + RV32 software bounds + RV32 div trap + safety-manifest.json

[avrabe]

Implements Phase 1 of the binary-safety roadmap landed in #110.

What's new

• CLI: --safety-bounds <mpu|software|mask|none> flag. --bounds-check remains as a deprecated alias mapping to --safety-bounds software and prints a one-line deprecation notice.
• safety-manifest.json alongside every emitted ELF when any safety flag is enabled. Schema: synth_version, target_triple, safety_bounds, safety_div_zero, safety_div_overflow, linear_memory_bytes. Verifiers/disasm tools can consume this.
• RV32 software-bounds: ported the ARM bgeu addr, mem_size, trap_label pattern to every i32 load/store + sub-word variant in the RISC-V selector.
• RV32 div trap: bne rs2, x0, ok; ebreak; ok: div (and divu/rem/remu) — mirrors ARM's trap pattern. Closes the RV32 div-by-zero gap noted in docs: binary safety checks design — ARM + RISC-V opt-in safety profiles #110 §2.

Hand-tested

$ synth compile examples/wat/simple_add.wat --safety-bounds mpu -o /tmp/sa.elf --cortex-m
$ cat /tmp/sa.safety-manifest.json
{
  "synth_version": "0.1.0",
  "target_triple": "thumbv7m-none-eabi",
  "safety_bounds": "mpu",
  "safety_div_zero": true,
  "safety_div_overflow": true,
  "linear_memory_bytes": 65536
}

$ synth compile examples/wat/simple_add.wat --bounds-check -o /tmp/sa.elf --cortex-m
warning: --bounds-check is deprecated; use --safety-bounds=software instead
[INFO] Wrote safety manifest: /tmp/sa.safety-manifest.json

$ synth compile /tmp/rv_div.wat --backend riscv --target riscv32imac --safety-bounds software --all-exports -o /tmp/rv_div.elf
$ cat /tmp/rv_div.safety-manifest.json   # target_triple: riscv32imac-unknown-none-elf

Scope respected per design doc

• Phase 1 only. Phase 2 (stack overflow, CFI BTI/PAC), Phase 3 (linear memory poisoning), Phase 4 (component-model type confusion), Phase 5 (Rocq parameterisation) deferred per the roadmap in docs: binary safety checks design — ARM + RISC-V opt-in safety profiles #110 §6.

Verification

• cargo test --workspace --exclude synth-verify — all pass (z3-sys download was blocked locally; synth-verify excluded accordingly. CI will exercise the full workspace.)
• cargo clippy --workspace --exclude synth-verify --all-targets -- -D warnings — clean
• cargo fmt --check — clean

🤖 Generated with Claude Code