add leakage to FlatToRiscvLiterals

mit-plv · Oct 30, 2024 · 8a01efb · 8a01efb
1 parent 376ec5a
commit 8a01efb
Showing 1 changed file with 17 additions and 11 deletions.
diff --git a/compiler/src/compiler/FlatToRiscvLiterals.v b/compiler/src/compiler/FlatToRiscvLiterals.v
@@ -22,9 +22,9 @@ Section FlatToRiscvLiterals.
   Context {mem: map.map word byte}.
   Context {M: Type -> Type}.
   Context {MM: Monads.Monad M}.
-  Context {RVM: Machine.RiscvProgram M word}.
+  Context {RVM: Machine.RiscvProgramWithLeakage M word}.
   Context {PRParams: Primitives.PrimitivesParams M MetricRiscvMachine}.
-  Context {ext_spec: Semantics.ExtSpec}.
+  Context {ext_spec: LeakageSemantics.ExtSpec}.
   Context {word_riscv_ok: RiscvWordProperties.word.riscv_ok word}.
   Context {locals_ok: map.ok locals}.
   Context {mem_ok: map.ok mem}.
@@ -87,25 +87,25 @@ Section FlatToRiscvLiterals.
       runsTo (withRegs (map.put initialL.(getRegs) x (word.of_Z v))
              (withPc     (add initialL.(getPc) d)
              (withNextPc (add initialL.(getNextPc) d)
-             (withMetrics (updateMetricsForLiteral v initialL.(getMetrics)) initialL))))
+             (withMetrics (updateMetricsForLiteral v initialL.(getMetrics))
+             (withLeakageEvents (Some (rev (leakage_events (initialL.(getPc)) 0 insts (leak_lit iset v)))) initialL)))))
              post ->
       runsTo initialL post.
   Proof.
     intros *. intros E1 insts d F P V Vm N.
     simpl in *.
     destruct_RiscvMachine initialL.
     subst d insts initialL_npc.
-    unfold compile_lit, updateMetricsForLiteral in *.
-    (* TODO once we're on 8.16, it should be possible to replace "F, P, N" by "*"
-       https://github.com/coq/coq/pull/15426 *)
-    rewrite bitwidth_matches in F, P, N.
+    unfold compile_lit, leakage_events, leak_lit, updateMetricsForLiteral in *.
+    rewrite bitwidth_matches in *.
     destruct_one_match_hyp; [|destruct_one_match_hyp].
-    - unfold compile_lit_12bit in *.
+    - unfold compile_lit_12bit, leak_lit_12bit in *.
       run1det.
       simpl_word_exprs word_ok.
       match_apply_runsTo.
       erewrite signExtend_nop; eauto; try blia.
-    - unfold compile_lit_32bit in *.
+      Tactics.destruct_one_match; try reflexivity.
+    - unfold compile_lit_32bit, leak_lit_32bit in *.
       simpl in P.
       run1det. run1det.
       match_apply_runsTo.
@@ -145,7 +145,9 @@ Section FlatToRiscvLiterals.
           }
       + solve_word_eq word_ok.
       + solve_word_eq word_ok.
-    - unfold compile_lit_64bit, compile_lit_32bit in *.
+      + simpl. repeat Tactics.destruct_one_match || reflexivity.
+        repeat f_equal. solve_word_eq word_ok.
+    - unfold compile_lit_64bit, leak_lit_64bit, compile_lit_32bit, compile_lit_32bit in *.
       remember (signExtend 12 (signExtend 32 (bitSlice v 32 64))) as mid.
       remember (signExtend 32 (signExtend 32 (bitSlice v 32 64))) as hi.
       protect_equalities.
@@ -188,6 +190,9 @@ Section FlatToRiscvLiterals.
         all: Btauto.btauto.
       + solve_word_eq word_ok.
       + solve_word_eq word_ok.
+      + repeat Tactics.destruct_one_match || reflexivity.
+        (*^this is kind of absurd; I should be able to rewrite somethign to get rid of it*)
+        repeat solve_word_eq word_ok || f_equal.
   Qed.
 
   Lemma compile_lit_correct_full: forall (initialL: RiscvMachineL) post x v R Rexec,
@@ -202,7 +207,8 @@ Section FlatToRiscvLiterals.
       runsTo (withRegs (map.put initialL.(getRegs) x (word.of_Z v))
              (withPc     (add initialL.(getPc) d)
              (withNextPc (add initialL.(getNextPc) d)
-             (withMetrics (updateMetricsForLiteral v initialL.(getMetrics)) initialL))))
+                (withMetrics (updateMetricsForLiteral v initialL.(getMetrics))
+                   (withLeakageEvents (Some (rev (leakage_events (initialL.(getPc)) 0 insts (leak_lit iset v)))) initialL)))))
              post ->
       runsTo initialL post.
   Proof. (* by case distinction on literal size and symbolic execution through the instructions