fix(tla): stage primed arguments in the compiled + execute_branch action paths

[zoratu]

Problem

An action operator called with a primed variable as an argument is an action by virtue of the call site. The canonical shape is NanoBlockchain's constant-operator override:

CalculateHashImpl(blk, oldL, newL) == LET h == HashOf(blk) IN /\ newL = h /\ hashFunction' = [hashFunction EXCEPT ![h] = blk]
...
ProcessSendBlock(node, signedBlock) == ... /\ CalculateHash(block, lastHash, lastHash')  \* newL binds to lastHash'
                                           /\ distributedLedger' = [.. EXCEPT ![node][lastHash'] = signedBlock]  \* reads staged lastHash'

Here newL aliases lastHash', so the body clause newL = h is really the primed assignment lastHash' = h. Expressing that needs textual argument substitution (macro semantics), turning newL into the literal lastHash'.

The interpreted eval_action_body_multi already did this. The other two action evaluators did not:

• try_eval_compiled_guard_as_action substituted only when the body had no direct prime. CalculateHashImpl also stages hashFunction' directly, so it was classified transitively-action and took the value-binding path — binding newLastHash to the unstaged value of lastHash'. newLastHash = h then evaluated as a boolean guard, lastHash' was never staged, and the later ![node][lastHash'] indexed a bogus value → the action silently produced no successor.
• execute_branch substituted only when the body primed a parameter (Lose(q) == q' = ...), never when an argument was primed — same value-binding failure.

Symptom: silent under-exploration (a false-safe soundness bug) for the "operator staging a prime through a primed argument, read by a later conjunct" shape — the Specifying-Systems Send(p,d,mem,mem') memory-interface pattern and Nano's hash-assignment pattern.

Fix

Both paths now substitute the argument text whenever any argument is primed, matching the interpreted path — all three action evaluators are now consistent. arg_is_primed_expr is lifted to pub(crate) and shared.

Validation (on spot)

• New diff_tlc gate spec PrimedArgActionStaging (CHOOSE-free so state counts pin exactly): pre-fix froze at 1 state / no violation; post-fix 4 states == TLC v2.19 with the reachable violation. Verified it genuinely regresses — neutering both fixes reproduces the 1-state freeze.
• scripts/diff_tlc.sh: 15/15.
• cargo test --release: 0 failures.

Scope note

Found while investigating the NanoBlockchain MCNanoSmall under-exploration (1563 vs TLC 3003). This fix resolves the primed-argument-staging class but not MCNanoSmall itself, whose dominant blocker is a separate residual: ValidateOpenBlock's nested reads (ledger[block.source].block.type/.destination) evaluate over-restrictively, so ours rejects valid open blocks (relaxing them recovers ours to ~1163 ≈ TLC 1179). That residual is documented and parked for follow-up.