GarageDoorTop: assert some types

mit-plv · Apr 5, 2024 · d31b3a3 · d31b3a3
1 parent 2173acf
commit d31b3a3
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/src/Bedrock/End2End/X25519/GarageDoorTop.v b/src/Bedrock/End2End/X25519/GarageDoorTop.v
@@ -258,6 +258,11 @@ Import bedrock2.Map.Separation. Local Open Scope sep_scope.
 Require Import bedrock2.ReversedListNotations.
 Local Notation run1 := (mcomp_sat (run1 Decode.RV32IM)).
 Local Notation RiscvMachine := MetricRiscvMachine.
+Goal True.
+  pose (run1 : RiscvMachine -> (RiscvMachine -> Prop) -> Prop).
+  pose (always(iset:=Decode.RV32IM) : (RiscvMachine -> Prop) -> RiscvMachine -> Prop).
+Abort.
+
 Implicit Types mach : RiscvMachine.
 Local Coercion word.unsigned : word.rep >-> Z.