Merge pull request #431 from OwenConoly/leakage_traces

Leakage traces

bedrock2/src/bedrock2/FE310CSemantics.v

@@ -1,5 +1,5 @@
 Require Import Coq.ZArith.ZArith.
-Require Import bedrock2.Syntax bedrock2.Semantics.
+Require Import bedrock2.Syntax bedrock2.Semantics bedrock2.LeakageSemantics bedrock2.MetricLeakageSemantics.
 Require coqutil.Datatypes.String coqutil.Map.SortedList coqutil.Map.SortedListString.
 Require Import coqutil.Word.Interface.
 Require Export coqutil.Word.Bitwidth32.
@@ -27,24 +27,25 @@ Section WithParameters.
   Definition isMMIOAligned (n : nat) (addr : word) :=
     n = 4%nat /\ word.unsigned addr mod 4 = 0.
 
-  Global Instance ext_spec: ExtSpec :=
-    fun (t : trace) (mGive : mem) a (args: list word) (post: mem -> list word -> Prop) =>
+(* FE310 is a simple enough processor that our leakage assumptions are likely to hold.  There is no official documentation of whether multiply always takes the maximum time or not, but both https://eprint.iacr.org/2019/794.pdf and https://pure.tue.nl/ws/portalfiles/portal/169647601/Berg_S._ES_CSE.pdf quote a fixed number of cycles for FE310 multiplication in the context of cryptography. *)
+  Global Instance leakage_ext_spec: LeakageSemantics.ExtSpec :=
+    fun (t : trace) (mGive : mem) a (args: list word) (post: mem -> list word -> list word -> Prop) =>
     if String.eqb "MMIOWRITE" a then
       exists addr val,
         args = [addr; val] /\
         (mGive = Interface.map.empty /\ isMMIOAddr addr /\ word.unsigned addr mod 4 = 0) /\
-        post Interface.map.empty nil
+        post Interface.map.empty nil [addr]
     else if String.eqb "MMIOREAD" a then
       exists addr,
         args = [addr] /\
         (mGive = Interface.map.empty /\ isMMIOAddr addr /\ word.unsigned addr mod 4 = 0) /\
-        forall val, post Interface.map.empty [val]
+        forall val, post Interface.map.empty [val] [addr]
     else False.
 
-  Global Instance ext_spec_ok : ext_spec.ok ext_spec.
+  Global Instance leakage_ext_spec_ok : ext_spec.ok leakage_ext_spec.
   Proof.
     split;
-    cbv [ext_spec Morphisms.Proper Morphisms.respectful Morphisms.pointwise_relation Basics.impl];
+    cbv [leakage_ext_spec Morphisms.Proper Morphisms.respectful Morphisms.pointwise_relation Basics.impl];
     intros.
     all :
     repeat match goal with
@@ -53,9 +54,16 @@ Section WithParameters.
       | H: exists _, _ |- _ => destruct H
       | H: _ /\ _ |- _ => destruct H
       | H: False |- _ => destruct H
-    end; subst; eauto 8 using Properties.map.same_domain_refl.
+    end; subst;
+    repeat match goal with
+      | H: _ :: _ = _ :: _ |- _ => injection H; intros; subst; clear H
+    end;
+    eauto 8 using Properties.map.same_domain_refl.
   Qed.
 
+  Global Instance ext_spec : Semantics.ExtSpec := deleakaged_ext_spec.
+  Global Instance ext_spec_ok : Semantics.ext_spec.ok ext_spec := deleakaged_ext_spec_ok.
+
   Global Instance locals: Interface.map.map String.string word := SortedListString.map _.
   Global Instance env: Interface.map.map String.string (list String.string * list String.string * cmd) :=
     SortedListString.map _.