secure-compilation · floriangru · Sep 2, 2019 · Sep 5, 2019 · Sep 9, 2019 · Sep 10, 2019
diff --git a/.gitmodules b/.gitmodules
@@ -0,0 +1,3 @@
+[submodule "coq-utils"]
+	path = coq-utils
+	url = https://github.com/arthuraa/coq-utils.git
diff --git a/Common/Definitions.v b/Common/Definitions.v
@@ -114,8 +114,7 @@ Proof.
   assert (HNone : Ciface C = None).
   { by apply /dommPn. }
   rewrite HNone.
-  destruct (Piface C) eqn:Hcase;
-    by rewrite Hcase.
+  by destruct (Piface C) eqn:Hcase.
 Qed.
 
 Class HasTurn A := {

diff --git a/Common/Maps.v b/Common/Maps.v
@@ -11,7 +11,7 @@ Set Bullet Behavior "Strict Subproofs".
 
 Definition NMap T := {fmap nat -> T}.
 
-Definition elementsm {A: Type} : NMap A -> list (nat * A) := @FMap.fmval nat_ordType A _.
+Definition elementsm {A: Type} : NMap A -> list (nat * A) := @FMap.fmval nat_ordType A.
 
 (* RB: TODO: These lemmas, with their clean proofs, probably belong in CoqUtils. *)
 
@@ -105,7 +105,7 @@ Lemma getm_filterm_notin_domm :
 Proof.
   intros T T' m1 m2 k Hnotin.
   rewrite filtermE Hnotin.
-  destruct (m2 k) as [v |] eqn:Hcase; now rewrite Hcase.
+  by destruct (m2 k) as [v |] eqn:Hcase.
 Qed.
 
 (* Set and filter commute if the key is outside the domain of filter. *)
@@ -134,7 +134,7 @@ Proof.
   apply /eq_fmap => n.
   rewrite !filtermE.
   unfold obind. unfold oapp.
-  destruct (m n) eqn:Hcase; rewrite Hcase.
+  destruct (m n) eqn:Hcase; simpl.
   -  destruct (n \notin domm m2) eqn:Hcase'; rewrite Hcase'.
      + destruct (n \notin domm m1) eqn:Hcase''; rewrite Hcase''.
        ++ assert (n \notin domm (unionm m1 m2)).
@@ -162,8 +162,8 @@ Qed.
 Lemma mapm_id : forall (T : Type) (i: NMap T), mapm id i = i.
 Proof.
   move=> T i. apply /eq_fmap => n.
-  rewrite mapmE. unfold omap, obind, oapp.
-  remember (i n) as v; simpl in *; rewrite <- Heqv.
+  rewrite mapmE. unfold omap, obind, oapp. simpl.
+  remember (i n) as v; simpl in *.
   now destruct v.
 Qed.
 
@@ -248,12 +248,12 @@ Proof.
     rewrite mem_domm in Heq1; rewrite mem_domm in Heq2.
     move: Heq1 Heq2. rewrite 2!filtermE. unfold obind. unfold oapp.
     destruct (m1 k) eqn:H';
-      rewrite H' Heq => //=. 
+      rewrite Heq => //=.
   - subst fn fn'.
     rewrite mem_domm in Heq1; rewrite mem_domm in Heq2.
     move: Heq1 Heq2. rewrite 2!filtermE. unfold obind. unfold oapp.
     destruct (m2 k) eqn:H';
-      rewrite H' Heq => //=. 
+      rewrite Heq => //=.
 Qed.
 
 
@@ -291,25 +291,25 @@ Proof.
   rewrite m2_eq_union -m0_eq_m2 domm_union.
   apply (* /fsubsetU /orP. *) /fsubsetP => x Hx.
   assert (x \in (domm i1) \/ x \notin (domm i1)).
-  { apply /orP. by destruct (x \in domm i1). } (* CA: do we have classical reasoning? *)   
-  case: H => H.  
-  move: H. apply /fsubsetP /fsubsetU /orP. 
+  { apply /orP. by destruct (x \in domm i1). } (* CA: do we have classical reasoning? *)
+  case: H => H.
+  move: H. apply /fsubsetP /fsubsetU /orP.
   left. by apply: fsubsetxx.
-      
+
   have x_in_i2 : x \in domm i2.
   { have x_in_m2 : x\in domm m2 by admit.
     move: x_in_m2.
     rewrite m2_eq_union domm_union.
     case /fsetUP => [| //].
-    move: H => /negP //. 
+    move: H => /negP //.
   } (*CA: by Hfilter deduce x \in domm m2
-               then by m2_eq_union, x \in domm i1 \/x \in domm i2 
+               then by m2_eq_union, x \in domm i1 \/x \in domm i2
                together with H we get x \in domm i2
               *)
-   move: x_in_i2. apply /fsubsetP /fsubsetU /orP.    
-   right. by apply: fsubsetxx. 
-Admitted.     
-    
+   move: x_in_i2. apply /fsubsetP /fsubsetU /orP.
+   right. by apply: fsubsetxx.
+Admitted.
+
 (* RB: NOTE: This is not a map lemma proper. More generally, absorption on
    arbitrary subsets. *)
 Lemma fsetU1in (T : ordType) (x : T) (s : {fset T}) :

diff --git a/Common/Memory.v b/Common/Memory.v
@@ -505,7 +505,7 @@ Proof.
   unfold Memory.store.
   intros mem1 mem1' mem2 ptr v Hstore.
   unfold merge_memories. rewrite unionmE.
-  destruct (mem1 (Pointer.component ptr)) eqn:Hcase1; rewrite Hcase1;
+  destruct (mem1 (Pointer.component ptr)) eqn:Hcase1;
     last discriminate.
   simpl.
   destruct (ComponentMemory.store t (Pointer.block ptr) (Pointer.offset ptr) v) eqn:Hcase2;
@@ -539,7 +539,7 @@ Proof.
   unfold Memory.alloc.
   intros mem1 mem1' mem2 C ptr size Halloc.
   unfold merge_memories. rewrite unionmE.
-  destruct (mem1 C) as [memC |] eqn:Hcase1; rewrite Hcase1;
+  destruct (mem1 C) as [memC |] eqn:Hcase1;
     last discriminate.
   simpl.
   destruct (ComponentMemory.alloc memC size) as [memC' b].
@@ -593,7 +593,7 @@ Section Partial.
     unfold to_partial_memory.
     rewrite filtermE.
     unfold obind, oapp.
-    destruct (mem Cid) eqn:Hmem; rewrite Hmem.
+    destruct (mem Cid) eqn:Hmem.
     now rewrite HCid.
     now reflexivity.
   Qed.
@@ -609,7 +609,7 @@ Section Partial.
     unfold to_partial_memory.
     rewrite filtermE.
     unfold obind, oapp.
-    destruct (mem Cid) eqn:Hmem; rewrite Hmem.
+    destruct (mem Cid) eqn:Hmem.
     now rewrite HCid.
     now reflexivity.
   Qed.

diff --git a/Intermediate/CS.v b/Intermediate/CS.v
@@ -160,7 +160,7 @@ Proof.
     destruct (Component.main \in domm (prog_interface c)) eqn:Hcase;
       first (specialize (Hdommc isT); now rewrite Hmainc in Hdommc).
     rewrite <- domm_prepare_procedures_entrypoints in Hdommp, Hcase.
-    destruct (dommP _ _ Hdommp) as [entrypointsp Hentrypointsp].
+    destruct (dommP Hdommp) as [entrypointsp Hentrypointsp].
     do 2 setoid_rewrite Hentrypointsp.
     now rewrite Nat.add_0_r.
   - (* Deal with the symmetries upfront; because of disjointness it is also
@@ -180,7 +180,7 @@ Proof.
     destruct (Component.main \in domm (prog_interface p)) eqn:Hcase;
       first (specialize (Hdommp isT); now rewrite Hmainp in Hdommp).
     rewrite <- domm_prepare_procedures_entrypoints in Hdommc, Hcase.
-    destruct (dommP _ _ Hdommc) as [entrypointsc Hentrypointsc].
+    destruct (dommP Hdommc) as [entrypointsc Hentrypointsc].
     do 2 setoid_rewrite Hentrypointsc.
     reflexivity.
   - (* Another easy/contra goal. *)

diff --git a/Intermediate/Machine.v b/Intermediate/Machine.v
@@ -15,7 +15,7 @@ Unset Printing Implicit Defensive.
 
 Set Bullet Behavior "Strict Subproofs".
 
-Variant register : Type :=
+Inductive register : Type :=
   R_ONE | R_COM | R_AUX1 | R_AUX2 | R_RA | R_SP | R_ARG.
 
 Definition label := nat.
@@ -385,22 +385,22 @@ Proof.
         -- apply proj1 in Hmain_comp2.
            specialize (Hmain_comp2 Hcase2). assumption.
       * (* Contra. *)
-        destruct (dommP _ _ Hprog_main1) as [CI HCI]. rewrite unionmE in HCI.
+        destruct (dommP Hprog_main1) as [CI HCI]. rewrite unionmE in HCI.
         apply negb_true_iff in Hcase1. apply negb_true_iff in Hcase2.
-        now rewrite (dommPn _ _ Hcase1) (dommPn _ _ Hcase2) in HCI.
+        now rewrite (dommPn Hcase1) (dommPn Hcase2) in HCI.
     + inversion Hprog_main1 as [Hmain].
       destruct (prog_main p1) as [main1 |] eqn:Hcase1;
         destruct (prog_main p2) as [main2 |] eqn:Hcase2.
       * (* Contra/easy. RB: NOTE: Three cases can be solved as instances of a
            little lemma, or a tactic. Is it useful elsewhere? *)
         apply proj2 in Hmain_comp1. specialize (Hmain_comp1 isT).
-        destruct (dommP _ _ Hmain_comp1) as [CI HCI].
+        destruct (dommP Hmain_comp1) as [CI HCI].
         apply /dommP. exists CI. now rewrite unionmE HCI.
       * apply proj2 in Hmain_comp1. specialize (Hmain_comp1 isT).
-        destruct (dommP _ _ Hmain_comp1) as [CI HCI].
+        destruct (dommP Hmain_comp1) as [CI HCI].
         apply /dommP. exists CI. now rewrite unionmE HCI.
       * apply proj2 in Hmain_comp2. specialize (Hmain_comp2 isT).
-        destruct (dommP _ _ Hmain_comp2) as [CI HCI].
+        destruct (dommP Hmain_comp2) as [CI HCI].
         apply /dommP. exists CI. simpl. now rewrite (unionmC Hdis_i) unionmE HCI.
       * discriminate.
 Qed.

diff --git a/Lib/Extra.v b/Lib/Extra.v
@@ -36,7 +36,7 @@ Lemma emptymP m : reflect (m = emptym) (domm m == fset0).
 Proof.
 apply/(iffP eqP); last by move=> ->; rewrite domm0.
 move=> e; apply/eq_fmap => x; rewrite emptymE.
-by case: (altP (dommPn m x))=> //; rewrite e.
+by case: (altP (@dommPn T S m x))=> //; rewrite e.
 Qed.
 
 End FMap.

diff --git a/Old/Intermediate/Composition.v b/Old/Intermediate/Composition.v
@@ -2117,7 +2117,7 @@ Section MultiSemantics.
       by now apply /dommP.
     rewrite unionmE in HSome.
     destruct (isSome (ctx1 ptr)) eqn:Hcase;
-      rewrite Hcase in HSome.
+      simpl in HSome.
     - left. apply /dommP. now eauto.
     - right. apply /dommP. now eauto.
   Qed.

diff --git a/Old/Intermediate/PS.v b/Old/Intermediate/PS.v
@@ -452,8 +452,7 @@ Proof.
     assert (Hctx2 : ctx2 Component.main = None)
       by (apply /dommPn; assumption).
     rewrite unionmE in Hctx12.
-    destruct (ctx1 Component.main) as [main1 |] eqn:Hcase1;
-      rewrite Hcase1 in Hctx12;
+    destruct (ctx1 Component.main) as [main1 |] eqn:Hcase1; simpl;
       simpl in Hctx12.
     + apply /dommP. now eauto.
     + congruence.
@@ -525,7 +524,7 @@ Proof.
       rewrite Hiface unionmE in HCI'.
       destruct (ctx1 C') as [CI'' |] eqn:Hcase.
       * apply /dommP. now eauto.
-      * rewrite Hcase in HCI'. simpl in HCI'.
+      * simpl in HCI'.
         (* TODO: Same artifact on dommP as above. *)
         assert (Hcontra : C' \in domm ctx2) by (apply /dommP; eauto).
         rewrite Hcontra in Hpc2.
@@ -563,7 +562,6 @@ Proof.
       unfold Program.has_component in Hhas_comp.
       rewrite Hiface unionmE in Hhas_comp.
       destruct (ctx1 (Pointer.component pc)) as [CI' |] eqn:Hcase;
-        rewrite Hcase in Hhas_comp;
         simpl in Hhas_comp.
       * apply /dommP. now eauto.
       * assert (Hcontra : ctx2 (Pointer.component pc) = None)
@@ -1153,7 +1151,7 @@ Proof.
   rewrite unionmE 2!filtermE.
   destruct (C \notin domm ctx1) eqn:Hdomm1;
     destruct (C \notin domm ctx2) eqn:Hdomm2;
-    destruct (mem C) as [memC |] eqn:Hmem; rewrite Hmem;
+    destruct (mem C) as [memC |] eqn:Hmem; simpl;
     try reflexivity.
   (* A single contradictory case is left. *)
   - exfalso.

diff --git a/README.md b/README.md
@@ -11,24 +11,52 @@ This repository contains the Coq development of the paper:
 
 ### Prerequisites ###
 
-This development requires Coq v8.7.1 to work, as well as the following libraries:
-- [Mathematical Components](https://math-comp.github.io/math-comp/) 1.6.4
-- [Extensional Structures](https://github.com/arthuraa/extructures) 0.1
-- [CoqUtils](https://github.com/arthuraa/coq-utils/releases/tag/v0.1) 0.1
+This development requires Coq v8.9.1 to work, as well as the following libraries:
+- [Mathematical Components](https://math-comp.github.io/math-comp/) 1.9.0 or dev / on branch master
+- [CoqUtils](https://github.com/arthuraa/coq-utils) on branch master (tested with commit [54c1269](https://github.com/arthuraa/coq-utils/commit/54c1269e1e85e14404e9dab3805e9db448f419f0)),
+- [Coq Void](https://github.com/arthuraa/coq-void) v0.1.0 or dev / on branch master
+  (tested with commit
+  [4a88dcd](https://github.com/arthuraa/coq-void/commit/4a88dcd55421c356e8930a4a62de1682d1bb3fa4)),
+- [Deriving](https://github.com/arthuraa/deriving) dev / on branch master
+  (tested with commit
+  [82ed345](https://github.com/arthuraa/deriving/commit/82ed3450039f51ce36833cc447be24c39dc9ef65)),
+- [Extensional Structures](https://github.com/arthuraa/extructures) on
+  branch master (tested with commit
+  [c2d88c2](https://github.com/arthuraa/extructures/commit/c2d88c2bad3b02f78ca25c41b4cb59251ae4f702)),
+- [QuickChick](https://github.com/QuickChick/QuickChick) v1.1.0 or 8.9.dev for the testing (see below).
+
+For convenience, you can install all the dependencies on opam (with
+the repo coq-released and coq-extra-dev) with
+
+```bash
+opam repo add coq-released https://coq.inria.fr/opam/released
+$ opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev
+
+# if you didn't clone with --recurse-submodules
+$ git submodule init
+$ git submodule update
+
+$ opam pin add coq-utils ./coq-utils
+$ opam install coq-quickchick
+```
+
+Note that this will activate the development repositories for many coq projects. You may
+want to pin some packages to a specific version with `opam pin
+<coq-package> <version>`
 
 ### Replaying the proofs ###
 
     $ make -j4
 
 ### Running the tests ###
 
-Our tests are known to work with [QuickChick](https://github.com/QuickChick/QuickChick) branch 8.7 and
+Our tests are known to work with [QuickChick](https://github.com/QuickChick/QuickChick) branch 8.9 and
 OCaml from 4.02.3 to 4.06.
 
 Running the tests (to be simplified):
 
-    $ make clean
-    $ make -j4
+    $ make -f Makefile.Test clean
+    $ make -f Makefile.Test -j4
     $ ./run_extracted_examples.sh --force-extraction
     $ rm sfi_safety_properties.exe
     $ ./run_sfi_tests.sh

diff --git a/S2I/Compiler.v b/S2I/Compiler.v
@@ -354,8 +354,8 @@ Proof.
     as [[code cenv2]|] eqn:Hcompiled_comps;
     try discriminate.
   simpl in Hcompile.
-  destruct (lift ((mkfmap (T:=nat_ordType) code) Component.main) cenv2) as [[]|] eqn:Hlift_mkfmap;
-    simpl in *; rewrite Hlift_mkfmap in Hcompile; try discriminate.
+  destruct (lift ((mkfmap code) Component.main) cenv2) as [[]|] eqn:Hlift_mkfmap;
+    simpl in *; try discriminate.
   destruct (lift (labels Component.main) c) as [[main_label cenv3]|] eqn:Hlift_main_label_C;
     try discriminate.
   destruct (lift (main_label Procedure.main) cenv3) as [[]|] eqn:Hlift_main_label_P;

diff --git a/Source/Language.v b/Source/Language.v
@@ -503,7 +503,7 @@ Module Source.
     rewrite mem_domm in Hnotin.
     rewrite Hnotin in Hfind.
     destruct (procs2 cid) as [C_procs |] eqn:Hprocs;
-      rewrite Hprocs in Hfind.
+      simpl.
     - unfold find_procedure.
       by rewrite Hprocs.
     - by inversion Hfind.

diff --git a/Tests/CompTestUtil.v b/Tests/CompTestUtil.v
@@ -21,7 +21,9 @@ Require Import extructures.ord.
 From mathcomp Require Import ssreflect ssrfun ssrbool ssreflect.eqtype.
 
 From QuickChick Require Import QuickChick.
-Import QcDefaultNotation. Import QcNotation. Open Scope qc_scope.
+Import QcDefaultNotation QcNotation.
+Open Scope qc_scope.
+Open Scope string_scope.
 
 Definition newline := String "010" ""%string.
 
@@ -227,4 +229,3 @@ Fixpoint sublist (l1 l2 : CompCert.Events.trace) : bool :=
          else false
        end
     end.
-
diff --git a/Tests/I2SFI/I2SFICompUtil.v b/Tests/I2SFI/I2SFICompUtil.v
@@ -7,7 +7,9 @@ Require Import Tests.CompTestUtil.
 Require Import Tests.TargetSFI.SFITestUtil.
 
 From QuickChick Require Import QuickChick.
-Import QcDefaultNotation. Import QcNotation. Open Scope qc_scope.
+Import QcDefaultNotation QcNotation.
+Open Scope qc_scope.
+Open Scope string_scope.
 
 Instance show_albl : Show AbstractMachine.label :=
   {|