The &mut/& split makes a same-array mem_copy unrepresentable in Rust, where C expresses it

[gHashTag]

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) -> bool

and 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 test and an invariant, and gen-rust lowers neither.
• The emitted Rust contains the definition of mem_copy and zero call sites.
• E0502 count 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

1. 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 existing NOT LOWERED BY THIS BACKEND header line, so the omission is disclosed rather than silent.
2. Lower it as one slice plus indices, matching what slice::copy_within does. That changes the spec surface, not just the backend.
3. Accept it and say so in the spec, marking mem_copy as 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.

[gHashTag]

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 []T mean &[T] in parameter position and Vec<T> everywhere else. In the shipped version an unmarked parameter is a byte-for-byte no-op, so:

pub fn mem_copy(dst: &mut [TernaryWord], dst_addr: u32, src: Vec<TernaryWord>, src_addr: u32, count: usize) -> bool

src stays Vec<TernaryWord> because the fixpoint does not mark it. So there is no E0502 here and never was in the shipped code — a same-array call would be a move of the Vec into src, 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_copy is 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

• The two same-array calls are at lines 388 and 472, inside a test and an invariant, and gen-rust lowers neither.
• The emitted Rust holds the definition of mem_copy at line 132 and zero call sites.
• E0502 in 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 BACKEND line — is still the one that matches the disclosure mechanism the repository already has.