x64 crefine: handle allIOPortsIssued_asrt

Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
seL4 · Nov 27, 2024 · c9c4d49 · c9c4d49
1 parent fb10847
commit c9c4d49
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/proof/crefine/X64/Arch_C.thy b/proof/crefine/X64/Arch_C.thy
@@ -4869,6 +4869,7 @@ lemma invokeX86PortControl_ccorres:
    apply (clarsimp cong: StateSpace.state.fold_congs globals.fold_congs)
    apply (rule ccorres_Guard_Seq)
    apply (clarsimp simp: liftE_def bind_assoc return_returnOk)
+   apply (rule ccorres_stateAssert)
    apply (ctac add: setIOPortMask_ccorres)
      apply csymbr
      apply (ctac(no_vcg) add: cteInsert_ccorres)