The VM circuits constrain every satisfying witness to follow the RISC-V semantics of the Sail specification, so a valid witness corresponds to a real execution. A second theorem extends this to OpenVM’s extensions beyond base RISC-V.
This map shows the components of each argument. Follow their connections to see how they support the theorems.
