This PR uses an ensures clause on the #loadDexterState to force the initial state to be well-formed, including for cells which are not directly mentioned in the proof.
It similarly uses a requires clause on #storeDexterState to ensure that the final state is well-formed.
sskeirik
commented
3 years ago
This PR uses an
ensuresclause on the#loadDexterStateto force the initial state to be well-formed, including for cells which are not directly mentioned in the proof.It similarly uses a
requiresclause on#storeDexterStateto ensure that the final state is well-formed.