This cannot be implemented in the script today due to disabled op_codes.
Can you please be more precise as to which parts could not be done? Not that I don't believe you, I just want to see if I can go around them.
Even if it could be, the resulting transactions for the proof of payment redemption would be prohibitively large: They'd have to contain a SPV fragment for the mixer->b,c transaction plus some block headers, and the complete mixer->b,c transaction, and the script search for the right outputs and then check the fragments.
We can simplify for now by supposing that Alice will only receive her funds at address B. I understand that the Mixer -> B tx and the header of the block that contains it will have to be referenced, but I didn't expect it to be very large. I understand that the proof verification will be more computationally intensive for verifying nodes. I'm not sure I understand that a "SPV fragment" is and google isn't helping me much.
[...] constrain your protocol that Alice must know the exact transaction the mixer intends to make [...]
I agree that might be necessary.
As an aside, your notation of "from address", "to address" suggest a pretty substantial misunderstanding of the Bitcoin system, likely inspired by block explorer sites that present things in terms of "address = account", this isn't how the protocol actually works.. but what you're describing could be restated in terms that do make sense in the Bitcoin protocol
What I mean by "from address A" is "signed by A's private key" and what I mean by a "transaction to address B" is a "transaction that can only be spent by using B's private key". I understand that accounts are not unified and that the "balance" of an address rests in the number of txins it is able to spend. Am I missing or misrepresenting something? How would you rephrase these terms?
If script is ever extended to allow compact proofs of computation (
https://bitcointalk.org/index.php?topic=277389.0) then what you're describing could work without huge transactions. If the proof of computation is zero-knowledge then your protocol could be simplified further: instead of Alice releasing the coins in the faithful execution case the your second party could redeem them using a zero-knowledge proof that Alice's rules were followed, without actually revealing what those rules were.
If the script ever gets extended in such a way, I believe that what you propose would be best indeed.