fix event loop

mit-plv · Jan 6, 2025 · fdd4c79 · fdd4c79
1 parent 4a6f0a6
commit fdd4c79
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 4 deletions.
diff --git a/compiler/src/compiler/RiscvEventLoop.v b/compiler/src/compiler/RiscvEventLoop.v
@@ -72,7 +72,7 @@ Section EventLoop.
       let state' := (withPc pc_start
                     (withNextPc (word.add pc_start (word.of_Z 4))
                     (withMetrics newMetrics
-                    (withLeakageEvents newLeakage state)))) in
+                    (withLeakageEvents (Some newLeakage) state)))) in
       valid_machine state' ->
       goodReadyState false state'.
 
@@ -138,7 +138,7 @@ Section EventLoop.
         repeat f_equal.
         all: try solve_word_eq word_ok.
         destruct getTrace; simpl.
-        { instantiate (1 := Some [_;_]). reflexivity. }
+        { instantiate (1 := [_;_]). reflexivity. }
         reflexivity.
       + simpl.
         match goal with

diff --git a/compiler/src/compiler/ToplevelLoop.v b/compiler/src/compiler/ToplevelLoop.v
@@ -150,6 +150,7 @@ Section Pipeline1.
       exists mH,
         isReady spec mach.(getLog) mH /\ goodTrace spec mach.(getLog) /\
         mach.(getPc) = word.add loop_pos (word.of_Z (if done then 4 else 0)) /\
+        (exists kL0, mach.(getTrace) = Some kL0) /\
         machine_ok functions_pos ml.(stack_start) ml.(stack_pastend) functions_instrs mH R
                    (program iset init_sp_pos (init_sp_insts ++
                                               init_insts init_fun_pos ++
@@ -461,6 +462,7 @@ Section Pipeline1.
              | |- _ => reflexivity
              end.
       + cbn. solve_word_eq word_ok.
+      + cbn. simpl in Hp5p3. subst. simpl. reflexivity.
       + cbn. destruct mlOk. subst. simpl in *. subst loop_pos init_pos. solve_divisibleBy4.
     - unfold ll_good, machine_ok.
       intros. fwd. assumption.
@@ -523,7 +525,7 @@ Section Pipeline1.
           do 4 eexists. split. 1: eassumption. split. 1: reflexivity.
           eapply (*ExprImp.weaken_exec*)MetricLeakageSemantics.exec.weaken.
           - eapply loop_body_correct; eauto.
-          - cbv beta. intros * _ HP. exists []. split. 1: reflexivity. exact HP.
+          - cbv beta. intros _ * _ HP. exists []. split. 1: reflexivity. exact HP.
         }
         all: try eassumption.
         all: simpl_MetricRiscvMachine_get_set.
@@ -535,6 +537,7 @@ Section Pipeline1.
         { reflexivity. }
         { reflexivity. }
         { reflexivity. }
+        { reflexivity. }
         unfold loop_pos, init_pos.
         unfold machine_ok.
         unfold_RiscvMachine_get_set.
@@ -579,6 +582,7 @@ Section Pipeline1.
           { f_equal. solve_word_eq word_ok. }
           { solve_word_eq word_ok. }
           { solve_word_eq word_ok. }
+          { f_equal. f_equal. f_equal. f_equal. solve_word_eq word_ok. }
       + cbv beta.
         intros.
         destruct_RiscvMachine final.
@@ -597,7 +601,7 @@ Section Pipeline1.
         * wcancel_assumption.
         * eapply rearrange_footpr_subset. 1: eassumption.
           wwcancel.
-    Unshelve. exact MetricLogging.EmptyMetricLog.
+    Unshelve. 1: exact nil. 1: exact MetricLogging.EmptyMetricLog.
   Qed.
 
   Lemma ll_inv_implies_prefix_of_good: forall st,