Leakage traces

.gitmodules

@@ -1,6 +1,6 @@
 [submodule "deps/riscv-coq"]
 	path = deps/riscv-coq
-	url = https://github.com/mit-plv/riscv-coq.git
+	url = https://github.com/OwenConoly/riscv-coq.git
 [submodule "deps/coqutil"]
 	path = deps/coqutil
 	url = https://github.com/mit-plv/coqutil.git

bedrock2/src/bedrock2/BasicC32Semantics.v

@@ -1,5 +1,5 @@
 Require Import Coq.ZArith.ZArith.
-Require Import bedrock2.Syntax bedrock2.Semantics.
+Require Import bedrock2.Syntax bedrock2.Semantics bedrock2.LeakageSemantics.
 Require coqutil.Datatypes.String coqutil.Map.SortedList coqutil.Map.SortedListString.
 Require Import coqutil.Word.Interface coqutil.Map.SortedListWord.
 Require coqutil.Word.Naive.
@@ -10,25 +10,27 @@ Require Export coqutil.Word.Bitwidth32.
 #[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 _.
-#[global] Instance ext_spec: ExtSpec := fun _ _ _ _ _ => False.
+#[global] Instance ext_spec: LeakageSemantics.ExtSpec := fun _ _ _ _ _ => False.
 
 Arguments word: simpl never.
 Arguments mem: simpl never.
 Arguments locals: simpl never.
 Arguments env: simpl never.
 
-#[global] Instance weaken_ext_spec trace m0 act args :
+(*#[global] Instance weaken_ext_spec :
+  ext_spec.ok ext_spec.
   Morphisms.Proper
-    (Morphisms.respectful
+    ((Morphisms.respectful
        (Morphisms.pointwise_relation Interface.map.rep
-          (Morphisms.pointwise_relation (list word) Basics.impl))
-       Basics.impl) (ext_spec trace m0 act args).
+          (Morphisms.pointwise_relation _
+             (Morphisms.pointwise_relation _ Basics.impl)))
+       Basics.impl) Basics.impl) (ext_spec trace m0 act klist args).
 Proof.
   cbn in *.
   unfold Morphisms.Proper, Morphisms.respectful, Morphisms.pointwise_relation, Basics.impl.
   intros.
   assumption.
-Qed.
+Qed.*)
 
 #[global] Instance localsok: coqutil.Map.Interface.map.ok locals := SortedListString.ok _.
 #[global] Instance envok: coqutil.Map.Interface.map.ok env := SortedListString.ok _.
@@ -42,5 +44,8 @@ Add Ring wring : (Properties.word.ring_theory (word := word))
 #[global] Instance ext_spec_ok : ext_spec.ok ext_spec.
 Proof.
   constructor; intros; try contradiction.
-  apply weaken_ext_spec.
+  cbn in *.
+  unfold Morphisms.Proper, Morphisms.respectful, Morphisms.pointwise_relation, Basics.impl.
+  intros.
+  assumption.
 Qed.

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.
 Require coqutil.Datatypes.String coqutil.Map.SortedList coqutil.Map.SortedListString.
 Require Import coqutil.Word.Interface.
 Require Export coqutil.Word.Bitwidth32.
@@ -27,18 +27,18 @@ 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) =>
+  Global Instance 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.
@@ -48,12 +48,16 @@ Section WithParameters.
     intros.
     all :
     repeat match goal with
-      | H : context[(?x =? ?y)%string] |- _ =>
-          destruct (x =? y)%string in *
-      | H: exists _, _ |- _ => destruct H
-      | H: _ /\ _ |- _ => destruct H
-      | H: False |- _ => destruct H
-    end; subst; eauto 8 using Properties.map.same_domain_refl.
+        | H : context[(?x =? ?y)%string] |- _ =>
+            destruct (x =? y)%string in *
+        | H: exists _, _ |- _ => destruct H
+        | H: _ /\ _ |- _ => destruct H
+        | H: False |- _ => destruct H
+        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 locals: Interface.map.map String.string word := SortedListString.map _.