If we can show that KEVM+DSS is a refinement of the mkr-mcd-spec, then we can do our high-level property verification over the mkr-mcd-spec, and we'll know that it corresponds to the actual EVM bytecode.
We can think of a couple issues already:
Cell-name clashes between the two specs (specifically the <k> cell, we can rename it in mkr-mcd-spec to a <step> cell).
Need to come up with simulation relation between mkr-mcd-spec and KEVM+DSS (perhaps start with a single contract, eg. Vat).
If we can show that KEVM+DSS is a refinement of the mkr-mcd-spec, then we can do our high-level property verification over the mkr-mcd-spec, and we'll know that it corresponds to the actual EVM bytecode.
We can think of a couple issues already:
<k>cell, we can rename it in mkr-mcd-spec to a<step>cell).