Skip to content

More simulation interpreter proofs using Valid predicate

Guillaume Claret requested to merge guillaume-claret@more-proofs-simulation-interpreter-valid-instr into master

In this MR we use the Valid predicate over instructions and Michelson values to unlock some of the cases of the proof of the simulation of the interpreter. @deepmindster this is using the predicate you defined.

Edited by Guillaume Claret

Merge request reports