Lightweight ways to prove an assembly language steps from a certain state to another state after variable number of instructions in Coq
I want to prove that a compiler that I wrote for a toy language is correct. I defined a predicate P which relates the runtime configuration of the source toy language and the target toy assembly.