Skip to content

Commit 39010ce

Browse files
avrabeclaude
andauthored
feat(#374): lower memory.copy/memory.fill (bulk-memory) — bounds-checked, trap-correct + v0.11.49 (#376)
* track(#374): memory.copy/memory.fill repro — bulk-mem lowering gap 19 falcon sites (11 fill + 8 copy). Same _ => None class as #369/#372; loud-skips on v0.11.47. No WasmOp::MemoryCopy/MemoryFill, no decoder arm, no lowering — a real lowering to build (decode + stack-effect + bounds-checked copy/fill loop with memmove-overlap + OOB trap). Repro only; fix = next block, own release. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> * feat(#374): lower memory.copy/memory.fill (bulk-memory) — bounds-checked, trap-correct memory.copy/memory.fill fell through the decoder `_ => None` and (since v0.11.46/GI-FPU-001) loud-skipped the whole function — 19 falcon sites, the largest remaining bulk-mem gap. Unlike #372 the lowering did not exist at all. - WasmOp::MemoryCopy / MemoryFill + decoder arms (memory 0 only; non-zero memory index loud-skips, preserving the GI-FPU-001 honesty contract) - stack effect: pop 3, push 0 (wasm_stack_check) - optimizer decline -> direct selector fallback (#120/#188/#372 pattern) - select_with_stack lowering: fill = STRB byte loop (low byte of val); copy = memmove byte loop with direction by dst/src order (dst>src copies backward). Bounds (Software mode) trap via inline UDF guarded by a LOCAL skip branch, end-EXCLUSIVE (off+len>size or u32-overflow traps; ==size ok), matching wasmtime. The 3 dead popped operands are reused as walking pointers (only R12 extra) — no temp allocation. Gate (value-level, no silicon): bulk_memory_374_differential.py 16/16 vs wasmtime over discriminating vectors (forward, overlap dst>src backward, overlap dst<src forward, self-copy, len==0, dst/src+len==size boundaries NO trap, OOB dst/src TRAP, low-byte fill). Frozen-safe: control_step 0x00210A55 13/13, flight_seam 0x07FDF307, div_const 338/338 byte-identical. Unit tests for decoder/stack-check/selector. rivet GI-MEM-002 (+VER-001). Falcon silicon (falcon-v1.56.fused.wasm) gates the release before #374 closes. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> * chore(release): v0.11.49 — #374 bulk-memory (memory.copy/fill) + pin sweep + changelog Pin sweep 0.11.48 -> 0.11.49 (workspace.package + 10 path-dep pins + MODULE.bazel + Cargo.lock synth-* packages). CHANGELOG v0.11.49 with falsification. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>
1 parent 636d95e commit 39010ce

22 files changed

Lines changed: 838 additions & 42 deletions

File tree

CHANGELOG.md

Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,48 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
77

88
## [Unreleased]
99

10+
## [0.11.49] - 2026-06-19
11+
12+
**BULK-MEMORY — #374: `memory.copy` / `memory.fill` now lower to bounds-checked
13+
byte loops, closing the largest remaining falcon on-target gap (19 sites: 11
14+
fill + 8 copy).** Self-contained, value-level differential vs wasmtime (16/16);
15+
falcon-v1.56 silicon confirmation gates closing #374.
16+
17+
- **#374`memory.copy` / `memory.fill` lowered** (was unsupported): like the
18+
scalar floats (#369) and the former `i64.load/store` (#372), bulk-memory fell
19+
through the decoder `_ => None` and (since v0.11.46 / GI-FPU-001) **loud-skipped
20+
the whole function**. Unlike #372 the lowering did not exist at all — no
21+
`WasmOp` variant, no decoder arm, no selector handler. Added:
22+
- `WasmOp::MemoryCopy` / `MemoryFill` + decoder arms for **memory 0** (a
23+
non-zero memory index still loud-skips — the GI-FPU-001 honesty contract);
24+
- stack effect `pop 3, push 0`;
25+
- optimizer **decline → direct-selector fallback** (the `#120/#188/#372`
26+
pattern; the optimized path has no bulk-mem IR opcode);
27+
- a bounds-checked byte-loop lowering in `select_with_stack`:
28+
`memory.fill(dst,val,len)``STRB` loop writing the **low byte** of `val`;
29+
`memory.copy(dst,src,len)` → a **memmove** byte loop whose direction follows
30+
`dst`/`src` order (`dst > src` copies **backward**, so overlapping copies
31+
don't corrupt the source). Under `--safety-bounds software` an **inline
32+
`UDF`**, guarded by a local skip branch, traps **end-exclusive** (`off+len >
33+
size`, or a `u32` overflow; `off+len == size` is in-bounds) to match
34+
wasmtime. (A body branch to the external `Trap_Handler` is only relocated in
35+
`--relocatable` mode, not in the self-contained image, so the trap is a
36+
self-contained `UDF`; on silicon UsageFault/HardFault routes to
37+
`Trap_Handler` via the vector table.) The three dead popped operands are
38+
reused as walking pointers — only `R12` extra, no temp allocation.
39+
- **Falsification:** `scripts/repro/bulk_memory_374_differential.py` runs 16
40+
discriminating vectors against wasmtime (forward, overlap `dst>src`
41+
backward, overlap `dst<src` forward, self-copy, `len==0`, `dst+len==size` &
42+
`src+len==size` boundaries that must **not** trap, OOB `dst`/`src` that
43+
**must** trap, fill with high bits set → only low byte written), comparing
44+
the full 64 KiB image **and** the trap outcome — **16/16**. Were the
45+
direction logic, the pop order, or the end-exclusive bound wrong, a vector
46+
flips. The RISC-V backend continues to loud-skip bulk-mem (symbol absent,
47+
warning names the op) — the silent-drop class is not reintroduced.
48+
- **Frozen-safe:** `control_step` `0x00210A55` (13/13), `flight_seam`
49+
`0x07FDF307`, `div_const` 338/338 stay byte-identical (no fixture uses
50+
bulk-mem; the change is purely additive). rivet `GI-MEM-002` (+`VER-001`).
51+
1052
## [0.11.48] - 2026-06-18
1153

1254
**ON-TARGET — #359 closed on silicon (G474RE `rc=0`): the dissolved msgq

Cargo.lock

Lines changed: 17 additions & 17 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

Cargo.toml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,7 @@ resolver = "2"
2727
# semver to publish, so the convention now catches up: workspace
2828
# version follows the release tag, bumped pre-tag in the release
2929
# checklist. See docs/release-process.md.
30-
version = "0.11.48"
30+
version = "0.11.49"
3131
edition = "2024"
3232
rust-version = "1.88"
3333
authors = ["PulseEngine Team"]

MODULE.bazel

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@ module(
77
name = "synth",
88
# Kept in lockstep with [workspace.package] version in Cargo.toml.
99
# Both are bumped pre-tag — see docs/release-process.md.
10-
version = "0.11.48",
10+
version = "0.11.49",
1111
)
1212

1313
# Bazel dependencies

artifacts/gale-integration.yaml

Lines changed: 66 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -785,3 +785,69 @@ artifacts:
785785
div_const 338/338) byte-identical; native_pointer_shadow_stack
786786
differential PASS; 32 cli tests green; gale G474RE silicon rc=0 +
787787
val=0xABCD round-trip on an empty queue (was rc=-35/val=0x0).
788+
789+
- id: GI-MEM-002
790+
type: sw-req
791+
title: Lower memory.copy/memory.fill (bulk-memory) — bounds-checked, trap-correct (#374)
792+
description: >
793+
gale/jess #374 (surfaced by the GI-FPU-001 loud-skip): memory.copy/
794+
memory.fill were unsupported (`_ => None`) — 19 falcon sites (11 fill,
795+
8 copy), the largest remaining bulk-mem gap. Unlike #372 the lowering did
796+
NOT exist: no WasmOp::MemoryCopy/MemoryFill, no decoder arm, no selector
797+
handler. IMPLEMENTED (next release): WasmOp::MemoryCopy/MemoryFill +
798+
decoder arms (memory 0 only; non-zero memory index loud-skips) + stack
799+
effect (pop 3, push 0) + optimizer decline->direct fallback (#120/#188/#372
800+
pattern) + a bounds-checked byte-loop lowering in select_with_stack. fill
801+
= STRB loop (low byte of val); copy = memmove byte loop with direction by
802+
dst/src order (dst>src copies backward). Bounds (Software mode) trap via an
803+
inline UDF guarded by a LOCAL skip branch — end-EXCLUSIVE (`off+len>size`
804+
or u32-overflow trap; `==size` ok), matching wasmtime. (An external
805+
Trap_Handler branch is only relocated in --relocatable mode, not the
806+
self-contained image, so a self-contained UDF is used; on silicon
807+
UsageFault/HardFault routes to Trap_Handler via the vector table.) The 3
808+
dead popped operands are reused as walking pointers (only R12 extra), so no
809+
temp allocation. Frozen-safe (no fixture uses bulk-mem). Ships its own
810+
release. Same honesty class as GI-FPU-001/GI-MEM-001.
811+
status: implemented
812+
tags: [gale, jess, bulk-memory, memory-copy, memory-fill, falcon, release-pending]
813+
links:
814+
- type: derives-from
815+
target: GI-005
816+
- type: traces-to
817+
target: gale:374
818+
fields:
819+
req-type: functional
820+
priority: must
821+
verification-criteria: >
822+
scripts/repro/bulk_memory_374_differential.py: 16/16 vs wasmtime
823+
(forward, overlap dst>src backward, overlap dst<src forward, self-copy,
824+
len==0, dst+len==size & src+len==size boundaries NO trap, OOB dst/src
825+
TRAP, low-byte fill); the three frozen fixtures (control_step 0x00210A55,
826+
flight_seam 0x07FDF307, div_const 338/338) byte-identical; gale falcon
827+
silicon round-trip (falcon-v1.56.fused.wasm) before verified.
828+
829+
- id: GI-MEM-002-VER-001
830+
type: sw-verification
831+
title: "Bulk-memory copy/fill (#374) — numeric differential + frozen byte-identity"
832+
description: >
833+
Verifies GI-MEM-002. scripts/repro/bulk_memory_374_differential.py runs
834+
wasmtime (ground truth) vs unicorn (synth Thumb-2, --safety-bounds
835+
software) over 16 DISCRIMINATING vectors comparing the full 64 KiB image
836+
AND trap outcome: copy non-overlap (asymmetric, catches pop-order swap),
837+
overlap dst>src (backward), overlap dst<src (forward), dst==src, len==0 at
838+
dst==size, dst+len==size & src+len==size boundaries (must NOT trap), OOB
839+
dst+len/src+len (must TRAP), fill with high bits set (only low byte
840+
written). Unit tests: wasm_decoder test_decode_bulk_memory_374,
841+
wasm_stack_check bulk_memory_pops_three_374, instruction_selector
842+
test_bulk_memory_{fill,copy}_lowers_374. Frozen byte-identity confirmed
843+
(the three oracles PASS unchanged — no fixture uses bulk-mem).
844+
status: implemented
845+
tags: [gale, bulk-memory, verification, differential, unit-test, frozen]
846+
links:
847+
- type: verifies
848+
target: GI-MEM-002
849+
fields:
850+
method: test
851+
pass-criteria: >
852+
bulk_memory_374_differential.py 16/16; cargo test 374/bulk_memory green;
853+
control_step / flight_seam / div_const differentials byte-identical.

crates/synth-backend-awsm/Cargo.toml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,6 @@ categories.workspace = true
1111
description = "aWsm backend integration for the Synth compiler"
1212

1313
[dependencies]
14-
synth-core = { path = "../synth-core", version = "0.11.48" }
14+
synth-core = { path = "../synth-core", version = "0.11.49" }
1515
anyhow.workspace = true
1616
thiserror.workspace = true

crates/synth-backend-riscv/Cargo.toml

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -11,8 +11,8 @@ categories.workspace = true
1111
description = "RISC-V encoder, ELF builder, PMP allocator, and bare-metal startup for synth"
1212

1313
[dependencies]
14-
synth-core = { path = "../synth-core", version = "0.11.48" }
15-
synth-synthesis = { path = "../synth-synthesis", version = "0.11.48" }
14+
synth-core = { path = "../synth-core", version = "0.11.49" }
15+
synth-synthesis = { path = "../synth-synthesis", version = "0.11.49" }
1616
anyhow.workspace = true
1717
thiserror.workspace = true
1818
tracing.workspace = true

crates/synth-backend-wasker/Cargo.toml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,6 @@ categories.workspace = true
1111
description = "Wasker backend integration for the Synth compiler"
1212

1313
[dependencies]
14-
synth-core = { path = "../synth-core", version = "0.11.48" }
14+
synth-core = { path = "../synth-core", version = "0.11.49" }
1515
anyhow.workspace = true
1616
thiserror.workspace = true

crates/synth-backend/Cargo.toml

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ default = ["arm-cortex-m"]
1515
arm-cortex-m = ["synth-synthesis"]
1616

1717
[dependencies]
18-
synth-core = { path = "../synth-core", version = "0.11.48" }
19-
synth-synthesis = { path = "../synth-synthesis", version = "0.11.48", optional = true }
18+
synth-core = { path = "../synth-core", version = "0.11.49" }
19+
synth-synthesis = { path = "../synth-synthesis", version = "0.11.49", optional = true }
2020
anyhow.workspace = true
2121
thiserror.workspace = true

crates/synth-cli/Cargo.toml

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -27,18 +27,18 @@ verify = ["synth-verify"]
2727
# Path deps carry `version` so `cargo publish` rewrites them to the
2828
# crates.io coordinate. Bumping the workspace version requires
2929
# updating these in lockstep — see docs/release-process.md.
30-
synth-core = { path = "../synth-core", version = "0.11.48" }
31-
synth-frontend = { path = "../synth-frontend", version = "0.11.48" }
32-
synth-synthesis = { path = "../synth-synthesis", version = "0.11.48" }
33-
synth-backend = { path = "../synth-backend", version = "0.11.48" }
30+
synth-core = { path = "../synth-core", version = "0.11.49" }
31+
synth-frontend = { path = "../synth-frontend", version = "0.11.49" }
32+
synth-synthesis = { path = "../synth-synthesis", version = "0.11.49" }
33+
synth-backend = { path = "../synth-backend", version = "0.11.49" }
3434

3535
# Optional external backends
36-
synth-backend-awsm = { path = "../synth-backend-awsm", version = "0.11.48", optional = true }
37-
synth-backend-wasker = { path = "../synth-backend-wasker", version = "0.11.48", optional = true }
38-
synth-backend-riscv = { path = "../synth-backend-riscv", version = "0.11.48", optional = true }
36+
synth-backend-awsm = { path = "../synth-backend-awsm", version = "0.11.49", optional = true }
37+
synth-backend-wasker = { path = "../synth-backend-wasker", version = "0.11.49", optional = true }
38+
synth-backend-riscv = { path = "../synth-backend-riscv", version = "0.11.49", optional = true }
3939

4040
# Optional verification (requires z3)
41-
synth-verify = { path = "../synth-verify", version = "0.11.48", optional = true, features = ["z3-solver", "arm"] }
41+
synth-verify = { path = "../synth-verify", version = "0.11.49", optional = true, features = ["z3-solver", "arm"] }
4242

4343
# Optional PulseEngine WASM optimizer
4444
# Uncomment when loom crate is available:

0 commit comments

Comments
 (0)