fix(kmir.md): handle projected operandMove callees

[Stevengre]

Summary

Fix call dispatch for projected operandMove callees.
When the callee is reached through projectionElemDeref, kmir was not computing the effective callee correctly, which left the proof stuck. This PR adds a regression for that case and updates call dispatch to use the projected place type, allowing the repro to run through to #EndProgram.

Testing

Validated as a red -> partial green -> green series with:

make test-integration TEST_ARGS="-k spl-multisig-iter-eq-copied-next-fail"

Each commit in the final branch passes that scoped command on the remote validation workspace:

• 86074df5 test(integration): add spl-multisig iter-eq copied next repro
• f04e1656 fix(call): match projected operandMove callees
• ceb4a2a0 fix(call): compute projected callee types through to EndProgram

[dkcumming]

I see that this works to solve the problem. But there are a bunch of things that I feel look different to the typical structure I would see @jberthold do to make sure the backend is happy. I feel we typically want to make functions [total] and otherwise have [preserves-definedness]. Maybe we should be having index checks too for I in range of LOCALS, not sure though. I will message Jost in slack for his opinion

[Stevengre]

Good point! I like total functions too. But this case shouldn't be a problem because we have the same check in the previous rule which is the one entrypoint for the function. Even though, let me fix it with total. It's not hard to refactor this.

[dkcumming]

Looks good

[jberthold]

Maybe the function could return TyUnknown for undesired cases, and the use site could catch that?
Then this would be TyUnknown instead of ty(-1) (which, by convention, would mean main if it exists), and the rule above would not need a side condition isTy(...) or cast {...}:>Ty.

[dkcumming]

Oh I forgot about TyUnknown! And I forgot -1 was main

[Stevengre]

Thanks! Make a commit for that.

[jberthold]

As you were asking on slack about this:
I tend to prefer total functions with optional results over partial ones. For a partial function used in an important rewrite rule, whenever there is uncertainty about the undefined points the old backend would kick in and start inventing path conditions. Therefore I think this is the right choice, except I would make the function return a MaybeTy and catch the TyUnknown cases at the use site.