final maychange?

awslabs · Feb 23, 2025 · 8b01ad3 · 8b01ad3
1 parent 44bc7a9
commit 8b01ad3
Show file tree

Hide file tree

Showing 3 changed files with 18 additions and 11 deletions.
diff --git a/arm/tutorial/bignum.ml b/arm/tutorial/bignum.ml
@@ -73,7 +73,8 @@ let BIGNUM_SPEC = prove(
     (\s. read PC s = word retpc /\
          read X0 s = word (if a = b then 1 else 0))
     // Registers (and memory locations) that may change after execution
-    (MAYCHANGE [PC;X0;X2;X3;X4;X5] ,, MAYCHANGE SOME_FLAGS)`,
+    (MAYCHANGE [PC;X0;X2;X3;X4;X5] ,, MAYCHANGE SOME_FLAGS ,,
+     MAYCHANGE [events])`,
 
   REPEAT STRIP_TAC THEN
   (* Convert 'bignum_from_memory' into 'memory :> bytes (..)'.

diff --git a/arm/tutorial/rel_equivtac.ml b/arm/tutorial/rel_equivtac.ml
@@ -84,9 +84,11 @@ let equiv_goal = mk_equiv_statement_simple
   eqin  (* Input state equivalence *)
   eqout (* Output state equivalence *)
   mc    (* First program machine code *)
-  `MAYCHANGE [PC; X10; X11; X12] ,, MAYCHANGE [memory :> bytes (outbuf, 8)]`
+  `MAYCHANGE [PC; X10; X11; X12] ,, MAYCHANGE [memory :> bytes (outbuf, 8)] ,,
+   MAYCHANGE [events]`
   mc2   (* Second program machine code *)
-  `MAYCHANGE [PC; X20; X21; X22] ,, MAYCHANGE [memory :> bytes (outbuf, 8)]`;;
+  `MAYCHANGE [PC; X20; X21; X22] ,, MAYCHANGE [memory :> bytes (outbuf, 8)] ,,
+   MAYCHANGE [events]`;;
 
 (* equiv_goal is:
   `forall pc pc2 inbuf outbuf.
@@ -107,11 +109,13 @@ let equiv_goal = mk_equiv_statement_simple
                 eqout (s,s2) outbuf)
            (\(s,s2) (s',s2').
                 (MAYCHANGE [PC; X10; X11; X12] ,,
-                 MAYCHANGE [memory :> bytes (outbuf,8)])
+                 MAYCHANGE [memory :> bytes (outbuf,8)] ,,
+                 MAYCHANGE [events])
                 s
                 s' /\
                 (MAYCHANGE [PC; X20; X21; X22] ,,
-                 MAYCHANGE [memory :> bytes (outbuf,8)])
+                 MAYCHANGE [memory :> bytes (outbuf,8)] ,,
+                 MAYCHANGE [events])
                 s2
                 s2')
            (\s. 4)
@@ -191,4 +195,4 @@ let EQUIV = prove(equiv_goal,
     let org_convs = !extra_word_CONV;;
     extra_word_CONV := (GEN_REWRITE_CONV I [<your_word_thm>])::org_convs;;
     ```
-*)
+*)
diff --git a/arm/tutorial/rel_reordertac.ml b/arm/tutorial/rel_reordertac.ml
@@ -101,9 +101,9 @@ let equiv_goal = mk_equiv_statement_simple
   eqin  (* Input state equivalence *)
   eqout (* Output state equivalence *)
   mc    (* First program machine code *)
-  `MAYCHANGE [PC; X10] ,, MAYCHANGE [memory :> bytes (outbuf, 16)]`
+  `MAYCHANGE [PC; X10] ,, MAYCHANGE [memory :> bytes (outbuf, 16)] ,, MAYCHANGE [events]`
   mc2   (* Second program machine code *)
-  `MAYCHANGE [PC; X10; X11] ,, MAYCHANGE [memory :> bytes (outbuf, 16)]`;;
+  `MAYCHANGE [PC; X10; X11] ,, MAYCHANGE [memory :> bytes (outbuf, 16)] ,, MAYCHANGE [events]`;;
 
 (* equiv_goal is:
   `forall pc pc2 inbuf outbuf.
@@ -124,11 +124,13 @@ let equiv_goal = mk_equiv_statement_simple
                 eqout (s,s2) inbuf outbuf)
            (\(s,s2) (s',s2').
                 (MAYCHANGE [PC; X10] ,,
-                 MAYCHANGE [memory :> bytes (outbuf,16)])
+                 MAYCHANGE [memory :> bytes (outbuf,16)] ,,
+                 MAYCHANGE [events])
                 s
                 s' /\
                 (MAYCHANGE [PC; X10; X11] ,,
-                 MAYCHANGE [memory :> bytes (outbuf,16)])
+                 MAYCHANGE [memory :> bytes (outbuf,16)] ,,
+                 MAYCHANGE [events])
                 s2
                 s2')
            (\s. 6)
@@ -182,4 +184,4 @@ let EQUIV = prove(equiv_goal,
 
     (** SUBGOAL 2. Maychange pair **)
     MONOTONE_MAYCHANGE_CONJ_TAC
-  ]);;
+  ]);;