m

mit-plv · Jan 10, 2025 · 6d7f24c · 6d7f24c
1 parent 2653496
commit 6d7f24c
Showing 1 changed file with 16 additions and 11 deletions.
diff --git a/processor/src/processor/KamiRiscvStep.v b/processor/src/processor/KamiRiscvStep.v
@@ -1642,10 +1642,8 @@ Section Equiv.
       unblock_subst kupd.
 
       (** Evaluate (invert) the two fetchers *)
-      rt. eval_kami_fetch. r || t.
-      r || t. Print inst'.
-      subst inst'. rewrite H11 in *. (*this let comes from a let that I typed in run1... apparently this rewrite H11 in * happened sometime a while ago, but it didnt work because inst' was stuck in a let or something.  anyway, this would go away if i hadn't typed the let in run1.*)
-      rt.
+      rt. eval_kami_fetch. rt.
+      subst inst'. rewrite H11 in *.
 
       (** Begin symbolic evaluation of Kami decode/execute *)
       kami_cbn_hint Heqic.
@@ -1822,7 +1820,8 @@ Section Equiv.
       unblock_subst kupd.
 
       (** Evaluate (invert) the two fetchers *)
-      rt. eval_kami_fetch. r || t. r || t. subst inst'. rewrite H11 in *. rt.
+      rt. eval_kami_fetch. rt.
+      subst inst'. rewrite H11 in *.
 
       (** Symbolic evaluation of Kami decode/execute *)
       clear Heqic0.
@@ -2092,7 +2091,8 @@ Section Equiv.
       unblock_subst kupd.
 
       (** Evaluate (invert) the two fetchers *)
-      rt. eval_kami_fetch. r || t. r || t. subst inst'. rewrite H11 in *. rt.
+      rt. eval_kami_fetch. rt.
+      subst inst'. rewrite H11 in *.
 
       (** Begin symbolic evaluation of Kami decode/execute *)
       kami_cbn_hint Heqic.
@@ -2256,7 +2256,8 @@ Section Equiv.
       unblock_subst kupd.
 
       (** Evaluate (invert) the two fetchers *)
-      rt. eval_kami_fetch. r || t. r || t. subst inst'. rewrite H11 in *. rt.
+      rt. eval_kami_fetch. rt.
+      subst inst'. rewrite H11 in *.
 
       (** Symbolic evaluation of Kami decode/execute *)
       clear Heqic0.
@@ -2419,7 +2420,8 @@ Section Equiv.
       unblock_subst kupd.
 
       (** Evaluate (invert) the two fetchers *)
-      rt. eval_kami_fetch. r || t. r || t. subst inst'. rewrite H11 in *. rt.
+      rt. eval_kami_fetch. rt.
+      subst inst'. rewrite H11 in *.
 
       (** Begin symbolic evaluation of Kami decode/execute *)
       kami_cbn_hint Heqic.
@@ -2588,7 +2590,8 @@ Section Equiv.
       unblock_subst kupd.
 
       (** Evaluate (invert) the two fetchers *)
-      rt. eval_kami_fetch. r || t. r || t. subst inst'. rewrite H11 in *. rt.
+      rt. eval_kami_fetch. rt.
+      subst inst'. rewrite H11 in *.
 
       (** Symbolic evaluation of Kami decode/execute *)
       clear Heqic0.
@@ -2857,7 +2860,8 @@ Section Equiv.
     unblock_subst kupd.
 
     (** Evaluate (invert) the two fetchers *)
-    rt. eval_kami_fetch. r || t. r || t. subst inst'. rewrite H11 in *. rt.
+    rt. eval_kami_fetch. rt.
+    subst inst'. rewrite H11 in *.
 
     (** Symbolic evaluation of Kami decode/execute *)
     kami_cbn_all.
@@ -3205,7 +3209,8 @@ Section Equiv.
     unblock_subst kupd.
 
     (** Evaluate (invert) the two fetchers *)
-    rt. eval_kami_fetch. r || t. r || t. subst inst'. rewrite H11 in *. rt.
+    rt. eval_kami_fetch. rt.
+    subst inst'. rewrite H11 in *.
 
     (** Symbolic evaluation of Kami decode/execute *)
     kami_cbn_all.