fix(rt): resolve thunk(operandCopy) in projection traversal

[Stevengre]

Summary

Add rules to resolve thunk(operandCopy(place(...))) values during projection traversal and borrow creation. Guard existing terminal rules to prevent premature matching on thunked values.

• Add #isThunkOperandCopy predicate
• Add 4 #traverseProjection rules for thunked copy-places (read, move-read, write, borrow)
• Guard existing .ProjectionElems terminal rules with notBool #isThunkOperandCopy(VAL)
• Add iter-copied-take-next-thunk-fail.rs and iter-map-eq-copied-take-thunk-fail.rs tests

Context

When closure or iterator type metadata is incomplete (e.g. missing from the SMIR type table), zero-sized constants are decoded as thunk(operandCopy(place(...))) instead of concrete values. When downstream code projects into such a thunked value — via field access, deref, or borrow creation — the #traverseProjection rules had no matching case, leaving the term stuck.

The fix composes remaining projections onto the thunked place and delegates to existing operand evaluation:

• Copy-read: => operandCopy(place(local(I), appendP(PLACEPROJ, PROJS))) — re-evaluates the original place with composed projections
• Move-read: emits #writeMoved then resolves as copy
• Write: delegates to #setLocalValue on the composed place
• Borrow (#forRef): materializes #mkRef directly to avoid re-traversal (re-entering via getValue(LOCALS, I) can reintroduce the same thunk, causing non-terminating projection growth)

This is a workaround for incomplete type metadata — miri does not have thunks since it always has complete type information. PR #957 (closure type metadata) addresses the root cause by providing the missing type info, but this PR handles thunks that still arise in other scenarios.

Without this fix, iterator patterns like keys.iter().take(n).copied() get stuck:

Leaf <k>:
  #traverseProjection(toLocal(1), thunk(operandCopy(place(local(1), ...))), ...)
    ~> #forRef(...)
  -- no matching rule, term is stuck

With this fix, the thunked place is composed and re-evaluated, allowing execution to continue.

Proof evidence

Without fix (RED): spl-multisig-iter-eq-copied-next-fail.rs gets stuck at #traverseProjection ~> #forRef

With fix (GREEN): Execution advances past the thunk-projection point (test still fails at a later point due to other unrelated issues, hence the -fail suffix).

Test plan

• -fail tests (proof advances further with fix, still fails at later point)
• make test-integration regression