This PR adds a P4light interpreter (Interpreter.v) written in Coq, based on the big-step P4light semantics. It includes a proof (in InterpreterSafe.v) that all runs of the interpreter correspond to executions in the big-step semantics.
There are a bunch of changes to the existing P4light semantics. Some make this proof easier and some were bugs or inconsistencies I found. I'd appreciate a careful read of those changes because I am not super confident in the modifications I made.
This PR adds a P4light interpreter (Interpreter.v) written in Coq, based on the big-step P4light semantics. It includes a proof (in InterpreterSafe.v) that all runs of the interpreter correspond to executions in the big-step semantics.
There are a bunch of changes to the existing P4light semantics. Some make this proof easier and some were bugs or inconsistencies I found. I'd appreciate a careful read of those changes because I am not super confident in the modifications I made.