How rewrites are checked
A rewrite is checked three times: by the verifier, in the VM, and by the proof.
The loader and verifier
The optimized program is loaded and verified by the real Agave loader and verifier, the same as the program before it.
VM differential checks
Each rewrite rule runs against generated register and memory states and its boundary cases: whole registers, the stack, the heap, the input region, and errors. The original and the rewritten sequence must end the same.
The proof
tare prove compares the final Tare program, after this stage, with the stock build. Everything the stage did is inside every proof and every record. Prove