Repository navigation
The &mut/& split makes a same-array mem_copy unrepresentable in Rust, where C expresses it #3404
Description
Found by adversarial review of #3403. Latent: population 0 in todays emitted Rust. Filed so it is not discovered later as a surprise.
The shape
specs/isa/ternary_memory.t27:226:
fn mem_copy(dst: []TernaryWord, dst_addr: u32, src: []TernaryWord, src_addr: u32, count: usize) -> bool
Its body carries an explicit two-branch overlap handler — "Handle overlap (copy direction matters)" — forward when dst_addr < src_addr, backward otherwise. That branch exists for exactly one situation: dst and src are the same array. And the spec exercises it that way, twice:
- line 388,
test mem_block_copy_overlap→mem_copy(memory, 0, memory, 1, 2) - line 472,
invariant mem_copy_handles_overlap→mem_copy(memory, 0, memory, 1, 2)
What #3403 does to it
dst is index-assigned so the fixpoint marks it; src is not. The emitted signature becomes
pub fn mem_copy(dst: &mut [TernaryWord], dst_addr: u32, src: &[TernaryWord], src_addr: u32, count: usize) -> booland the spec own call is then unrepresentable in safe Rust:
error[E0502]: cannot borrow `memory` as immutable because it is also borrowed as mutable
mem_copy(&mut memory, 0, &memory, 1, 2)
The backward-copy branch becomes dead by type. C takes two pointers and can express the call; Verilog can too. So this is a place where the four backends do not agree about what the spec means — the property the project exists to hold.
Why it is not urgent, stated precisely
- The two same-array calls are inside a
testand aninvariant, andgen-rustlowers neither. - The emitted Rust contains the definition of
mem_copyand zero call sites. E0502count in that file: 0 on master, 0 after fix(rust-backend): a written []T parameter is &mut [T], to a fixpoint #3403. Measured, not assumed.
It becomes live the moment tests or invariants are lowered to Rust — which is a direction this project wants to go, so the cost is deferred rather than avoided.
Options, none of them free
- Refuse the shape. When one function has both a written slice parameter and a read slice parameter of the same element type, the
&mut/&split cannot express a same-array call. Leave that function parameters as they were and declare it on the existingNOT LOWERED BY THIS BACKENDheader line, so the omission is disclosed rather than silent. - Lower it as one slice plus indices, matching what
slice::copy_withindoes. That changes the spec surface, not just the backend. - Accept it and say so in the spec, marking
mem_copyas a construct whose Rust lowering is weaker than its C and Verilog lowerings.
Option 1 is the one that keeps the honesty property this repository already has a mechanism for. Which of the three is the owner call.
Boundary
specs/isa/ternary_memory.t27
Activity
gHashTag commentedon Sep 7, 2026
Correcting this issue against the version that actually shipped. The review was done on an earlier draft, and the narrowing changed the picture.
What the emitted signature really is
The reviewer read the wide draft, in which every slice parameter became a reference. That draft was withdrawn (see #3403, commit
05848b42e) after two other reviewers showed it made[]Tmean&[T]in parameter position andVec<T>everywhere else. In the shipped version an unmarked parameter is a byte-for-byte no-op, so:srcstaysVec<TernaryWord>because the fixpoint does not mark it. So there is noE0502here and never was in the shipped code — a same-array call would be a move of theVecintosrc, not a borrow conflict against&mut dst.What survives, and it is still worth recording
The expressiveness point holds in a weaker and more precise form.
mem_copyis written to be called with one array in both positions — that is what its forward/backward branch exists for — and neither shape expresses that:&mut [T]+Vec<T>(shipped): the caller must hand over a copy, so the overlap branch computes on data the mutation cannot affect. The branch is not dead by type, it is dead by semantics, which is worse to detect.&mut [T]+&[T](withdrawn):E0502, dead by type.C takes two pointers and expresses the aliased call directly. So the disagreement between backends is real in both shapes; only its diagnosis differs.
The population claim is unchanged and was measured on the shipped version
testand aninvariant, andgen-rustlowers neither.mem_copyat line 132 and zero call sites.E0502in that file: 0 on master, 0 after fix(rust-backend): a written []T parameter is &mut [T], to a fixpoint #3403.The three options above stand. Option 1 — refuse the shape and declare it on the
NOT LOWERED BY THIS BACKENDline — is still the one that matches the disclosure mechanism the repository already has.gHashTag commentedon Sep 23, 2026
A boundary drafted from the paths this issue already names, so a bee can take it. Nothing is reserved until this is in the issue body - the Queen reads the body, not comments. Check the paths first: a wrong boundary reserves files the work does not own.
Boundary
specs/isa/ternary_memory.t27github-actions commentedon Sep 26, 2026
Re-filed as #4825.
An attempt claimed this issue on 2026-09-23 and left an empty branch. A dispatch row that has spent its retry ceiling is released once and then keeps its issue for good, which is the right rule for a third identical failure and the wrong outcome for an issue nobody ever attempted twice. The new issue carries the same work, the same boundary, and today's brief.
Closing this one so the swarm can take the work again.
salvage(queen-3404): commit what the turn left uncommitted