Merge branch 'coq-8.5'

Conflicts: README.md cfi/abstract.v cfi/preservationAS.v cfi/refinementAS.v cfi/refinementSC.v cfi/symbolic.v common/types.v compartmentalization/main.v compartmentalization/refinementSA.v compartmentalization/symbolic.v concrete/concrete.v lib/partmap_utils.v lib/word_utils.v memory_safety/abstract.v memory_safety/main.v memory_safety/refinementAS.v sealing/abstract.v sealing/refinementSA.v symbolic/fault_handler.v symbolic/refinement_common.v
micro-policies · May 7, 2016 · bc26b47 · bc26b47
2 parents d5841f6 + b62b3fc
commit bc26b47
Show file tree

Hide file tree

Showing 53 changed files with 154 additions and 190 deletions.
diff --git a/README.md b/README.md
@@ -7,9 +7,8 @@ Coq formalization accompanying the paper:
 
 ### Prerequisites
 
-- Coq 8.4pl4 or 8.4pl5 (https://coq.inria.fr/download)
-- SSReflect 1.5 (http://ssr.msr-inria.inria.fr/FTP/)
-- The Mathematical Components library 1.5
+- Coq 8.5 (https://coq.inria.fr/download)
+- The Mathematical Components library 1.6 (for Coq 8.5)
   (http://www.msr-inria.fr/projects/mathematical-components-2/)
 - The CoqUtils library (https://github.com/arthuraa/coq-utils)
 

diff --git a/cfi/abstract.v b/cfi/abstract.v
@@ -1,6 +1,6 @@
-Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.ssrnat Ssreflect.seq.
-Require Import CoqUtils.word CoqUtils.fset CoqUtils.partmap.
-Require Import lib.utils common.types.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
+From CoqUtils Require Import word fset partmap.
+Require Import lib.utils lib.ssr_list_utils common.types.
 Require Import cfi.property cfi.classes.
 
 Set Implicit Arguments.

diff --git a/cfi/classes.v b/cfi/classes.v
@@ -1,4 +1,4 @@
-Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.ssrnat.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
 Require Import common.types.
 
 Set Implicit Arguments.

diff --git a/cfi/concrete.v b/cfi/concrete.v
@@ -1,5 +1,5 @@
-Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.ssrnat Ssreflect.seq.
-Require Import CoqUtils.ord CoqUtils.word CoqUtils.partmap.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
+From CoqUtils Require Import ord word partmap.
 
 Require Import lib.utils lib.partmap_utils.
 Require Import common.types.

diff --git a/cfi/main.v b/cfi/main.v
@@ -1,5 +1,5 @@
-Require Import Ssreflect.ssreflect Ssreflect.ssrbool Ssreflect.ssrfun Ssreflect.ssrnat Ssreflect.eqtype Ssreflect.seq Ssreflect.fintype MathComp.ssrint.
-Require Import CoqUtils.ord CoqUtils.hseq CoqUtils.word CoqUtils.partmap.
+From mathcomp Require Import ssreflect ssrbool ssrfun ssrnat eqtype seq fintype ssrint.
+From CoqUtils Require Import ord hseq word partmap.
 
 Require Import lib.utils.
 Require Import common.types.

diff --git a/cfi/preservation.v b/cfi/preservation.v
@@ -1,5 +1,5 @@
-Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.seq.
-Require Import CoqUtils.word CoqUtils.partmap.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype seq.
+From CoqUtils Require Import word partmap.
 Require Import lib.utils common.types cfi.property.
 
 Set Implicit Arguments.

diff --git a/cfi/preservationAS.v b/cfi/preservationAS.v
@@ -1,5 +1,5 @@
-Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.ssrnat Ssreflect.seq.
-Require Import CoqUtils.ord CoqUtils.word CoqUtils.partmap.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
+From CoqUtils Require Import ord word partmap.
 
 Require Import lib.utils.
 Require Import common.types.
@@ -111,7 +111,7 @@ Qed.
 
 Lemma untag_data_implies_dmem_refinement mem :
   RefinementAS.refine_dmemory
-    (mapm RefinementAS.untag_atom (filterm (fun _ => RefinementAS.is_data) mem)) mem.
+    (mapm RefinementAS.untag_atom (filterm [fun _ => RefinementAS.is_data] mem)) mem.
 Proof.
    intros addr v.
    split.
@@ -136,7 +136,7 @@ Definition is_instr (a : atom (mword mt) cfi_tag) :=
 
 Lemma untag_instr_implies_imem_refinement mem :
   RefinementAS.refine_imemory
-    (mapm RefinementAS.untag_atom (filterm (fun _ => is_instr) mem)) mem.
+    (mapm RefinementAS.untag_atom (filterm [fun _ => is_instr] mem)) mem.
 Proof.
    intros addr v.
    split.
@@ -329,8 +329,8 @@ Qed.
 Next Obligation. (*initial state*)
   destruct H as [TPC [ITG [VTG [ETG [RTG ?]]]]].
   destruct cst as [mem reg [pc tpc] int].
-  exists (Abs.State (mapm RefinementAS.untag_atom (filterm (fun _ => is_instr) mem))
-                    (mapm RefinementAS.untag_atom (filterm (fun _ => RefinementAS.is_data) mem))
+  exists (Abs.State (mapm RefinementAS.untag_atom (filterm [fun _ => is_instr] mem))
+                    (mapm RefinementAS.untag_atom (filterm [fun _ => RefinementAS.is_data] mem))
                     (mapm RefinementAS.untag_atom reg) pc true).
   split.
   - unfold Abs.initial. reflexivity.

diff --git a/cfi/property.v b/cfi/property.v
@@ -1,5 +1,5 @@
-Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.ssrnat Ssreflect.seq.
-Require Import CoqUtils.word CoqUtils.partmap.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
+From CoqUtils Require Import word partmap.
 Require Import lib.utils common.types.
 
 Set Implicit Arguments.

diff --git a/cfi/refinementAS.v b/cfi/refinementAS.v
@@ -1,5 +1,5 @@
-Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.ssrnat Ssreflect.seq.
-Require Import CoqUtils.ord CoqUtils.word CoqUtils.fset CoqUtils.partmap.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
+From CoqUtils Require Import ord word fset partmap.
 
 Require Import lib.utils lib.partmap_utils.
 Require Import common.types.
@@ -788,10 +788,10 @@ Lemma dmem_domain_preserved_by_equiv :
     refine_dmemory dmem' mem' ->
     domm dmem = domm dmem'.
 Proof.
-move=> dmem dmem' mem mem' REF EQUIV REF'; apply/eq_fset.
-have /eq_fset DOMAINMM' := Sym.equiv_same_domain EQUIV.
+move=> dmem dmem' mem mem' REF EQUIV REF'.
+have DOMAINMM' := Sym.equiv_same_domain EQUIV.
 rewrite (refine_dmemory_domains REF') (refine_dmemory_domains REF).
-apply/eq_fset/filter_domains=> // addr; move: (EQUIV addr).
+apply/filter_domains=> // addr; move: (EQUIV addr).
 by case E: (mem addr) => [[v [o|]]|];
 case E': (mem' addr) => [[v' [o'|]]|] //=; case.
 Qed.

diff --git a/cfi/refinementSC.v b/cfi/refinementSC.v
@@ -1,5 +1,5 @@
-Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.ssrnat Ssreflect.seq.
-Require Import CoqUtils.ord CoqUtils.word CoqUtils.fset CoqUtils.partmap.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
+From CoqUtils Require Import ord word partmap.
 
 Require Import lib.utils lib.partmap_utils.
 Require Import common.types.
@@ -101,7 +101,7 @@ Lemma mem_refinement_equiv :
     Sym.equiv smem smem'.
 Proof.
   intros smem cmem cmem' REF EQUIV.
-  exists (mapm (coerce Symbolic.M) (filterm (fun _ => is_user Symbolic.M) cmem')).
+  exists (mapm (coerce Symbolic.M) (filterm [fun _ => is_user Symbolic.M] cmem')).
   split.
   { (*refinement proof*)
     split.
@@ -168,7 +168,7 @@ Lemma reg_refinement_equiv :
     Sym.equiv sregs sregs'.
 Proof.
   intros sreg creg creg' cmem REF EQUIV.
-  exists (mapm (coerce Symbolic.R) (filterm (fun _ => is_user Symbolic.R) creg')).
+  exists (mapm (coerce Symbolic.R) (filterm [fun _ => is_user Symbolic.R] creg')).
   split.
   { (*Refinement proof*)
     split.

diff --git a/cfi/rules.v b/cfi/rules.v
@@ -1,5 +1,5 @@
-Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.ssrnat.
-Require Import CoqUtils.hseq.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+From CoqUtils Require Import hseq.
 
 Require Import lib.utils common.types symbolic.symbolic.
 Require Import cfi.classes.

diff --git a/cfi/symbolic.v b/cfi/symbolic.v
@@ -1,6 +1,5 @@
-Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool.
-Require Import Ssreflect.eqtype Ssreflect.ssrnat Ssreflect.seq.
-Require Import CoqUtils.ord CoqUtils.word CoqUtils.fset CoqUtils.partmap.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
+From CoqUtils Require Import ord word partmap fset.
 
 Require Import lib.utils lib.partmap_utils.
 Require Import common.types.
@@ -80,8 +79,8 @@ Inductive step_a : Symbolic.state mt ->
 Lemma equiv_same_domain (T : ordType)
            (m m' : {partmap T -> atom (mword mt) cfi_tag}) :
   equiv m m' ->
-  domm m =i domm m'.
-Proof. move=> h; apply/eq_fset; move: h; exact: pointwise_same_domain. Qed.
+  domm m = domm m'.
+Proof. exact: pointwise_same_domain. Qed.
 
 Local Notation "x .+1" := (x + 1)%w.
 

diff --git a/common/printing.v b/common/printing.v
@@ -3,7 +3,7 @@ Require Import Coq.Strings.String.
 Require Import Coq.Strings.Ascii.
 Require Import ZArith.
 Require Import NPeano.
-Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.ssrnat Ssreflect.seq.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
 
 Import String.
 

diff --git a/common/segment.v b/common/segment.v
@@ -1,6 +1,7 @@
-Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.ssrnat Ssreflect.seq Ssreflect.choice Ssreflect.fintype.
-Require Import MathComp.div MathComp.ssrint MathComp.ssralg MathComp.intdiv.
-Require Import CoqUtils.ord CoqUtils.word CoqUtils.partmap.
+From mathcomp Require Import
+  ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype div ssrint ssralg
+  intdiv.
+From CoqUtils Require Import ord word partmap.
 
 Require Import lib.utils common.types.
 

diff --git a/common/types.v b/common/types.v
@@ -1,6 +1,6 @@
-Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.ssrnat Ssreflect.seq Ssreflect.choice Ssreflect.fintype.
-Require Import MathComp.div MathComp.ssrint MathComp.ssralg MathComp.intdiv.
-Require Import CoqUtils.ord CoqUtils.word CoqUtils.partmap.
+From mathcomp Require Import
+  ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype div ssrint ssralg intdiv.
+From CoqUtils Require Import ord word partmap.
 
 Require Import lib.utils.
 
@@ -176,15 +176,10 @@ Proof. by do !case. Qed.
 Definition opcode_choiceMixin := PcanChoiceMixin pickle_opcodeK.
 Canonical opcode_choiceType :=
   Eval hnf in ChoiceType opcode opcode_choiceMixin.
-
-Definition opcode_partOrdMixin := PcanPartOrdMixin pickle_opcodeK.
-Canonical opcode_partOrdType :=
-  Eval hnf in PartOrdType opcode opcode_partOrdMixin.
-Definition opcode_ordMixin := PcanOrdMixin pickle_opcodeK.
-Canonical opcode_ordType := Eval hnf in OrdType opcode opcode_ordMixin.
-
 Definition opcode_countMixin := CountMixin pickle_opcodeK.
 Canonical opcode_countType := Eval hnf in CountType opcode opcode_countMixin.
+Definition opcode_ordMixin := PcanOrdMixin pickle_opcodeK.
+Canonical opcode_ordType := Eval hnf in OrdType opcode opcode_ordMixin.
 
 Definition max_opcode := 24.
 

diff --git a/compartmentalization/abstract.v b/compartmentalization/abstract.v
@@ -1,5 +1,6 @@
-Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.ssrnat Ssreflect.seq MathComp.bigop Ssreflect.choice Ssreflect.fintype MathComp.finset.
-Require Import CoqUtils.word CoqUtils.partmap.
+From mathcomp Require Import
+  ssreflect ssrfun ssrbool eqtype ssrnat seq bigop choice fintype finset.
+From CoqUtils Require Import word partmap.
 Require Import lib.utils common.types.
 Require Import lib.ssr_list_utils lib.ssr_set_utils.
 Require Import compartmentalization.isolate_sets compartmentalization.common.

diff --git a/compartmentalization/common.v b/compartmentalization/common.v
@@ -1,5 +1,5 @@
-Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.ssrnat Ssreflect.seq.
-Require Import CoqUtils.word CoqUtils.partmap.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
+From CoqUtils Require Import word partmap.
 Require Import lib.utils common.types.
 Set Bullet Behavior "Strict Subproofs".
 

diff --git a/compartmentalization/isolate_sets.v b/compartmentalization/isolate_sets.v
@@ -1,5 +1,6 @@
-Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.ssrnat Ssreflect.seq Ssreflect.fintype MathComp.finset MathComp.ssrint.
-Require Import CoqUtils.word CoqUtils.partmap.
+From mathcomp Require Import
+  ssreflect ssrfun ssrbool eqtype ssrnat seq fintype finset ssrint.
+From CoqUtils Require Import word partmap.
 
 Require Import lib.utils common.types.
 Require Import compartmentalization.ranges.

diff --git a/compartmentalization/main.v b/compartmentalization/main.v
@@ -1,5 +1,5 @@
-Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.fintype Ssreflect.seq MathComp.ssrint MathComp.finset.
-Require Import CoqUtils.ord CoqUtils.hseq CoqUtils.word CoqUtils.partmap.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype fintype seq ssrint finset.
+From CoqUtils Require Import ord hseq word partmap.
 
 Require Import lib.utils lib.partmap_utils.
 Require Import common.types.
@@ -137,7 +137,7 @@ Definition decode_pc_tag (mem : Concrete.memory mt) (tg : mword mt) : option (Sy
 
 Instance encodable_stags : encodable mt (@Sym.stags mt) := {
   decode tk :=
-    match tk return Concrete.memory mt -> mword mt -> option (wtag _ tk) with
+    match tk return Concrete.memory mt -> mword mt -> option (wtag (@Sym.stags mt) tk) with
     | Symbolic.R => decode_reg_tag
     | Symbolic.M => decode_data_tag
     | Symbolic.P => decode_pc_tag

diff --git a/compartmentalization/ranges.v b/compartmentalization/ranges.v
@@ -1,5 +1,5 @@
-Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.ssrnat.
-Require Import CoqUtils.ord CoqUtils.word.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+From CoqUtils Require Import ord word.
 Require Import common.types.
 
 Section WithClasses.

diff --git a/compartmentalization/refinementSA.v b/compartmentalization/refinementSA.v
@@ -1,5 +1,6 @@
-Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.ssrnat Ssreflect.seq Ssreflect.fintype MathComp.finset.
-Require Import CoqUtils.ord CoqUtils.word CoqUtils.partmap.
+From mathcomp Require Import
+  ssreflect ssrfun ssrbool eqtype ssrnat seq fintype finset.
+From CoqUtils Require Import ord word fset partmap.
 
 Require Import lib.utils lib.partmap_utils common.types.
 Require Import symbolic.symbolic.
@@ -597,8 +598,8 @@ Proof.
   by rewrite (Sym.get_supd_none E UPD).
 Qed.
 
-Lemma sget_supd_good_internal (sst sst' : sstate) p c I1 W1 I2 W2 :
-  (forall c' : word, c' \in I2 :|: W2 -> (c' < Sym.next_id (Symbolic.internal sst))%ord) ->
+Lemma sget_supd_good_internal (sst sst' : sstate) p (c : mword mt) I1 W1 I2 W2 :
+  (forall c' : mword mt, c' \in I2 :|: W2 -> (c' < Sym.next_id (Symbolic.internal sst))%ord) ->
   Sym.sget sst p ?= Sym.DATA c I1 W1 ->
   Sym.supd sst p (Sym.DATA c I2 W2) ?= sst' ->
   Sym.good_internal sst ->
@@ -1835,7 +1836,9 @@ Proof.
       case: OR_Is => [-> // | <-{I2}].
       rewrite inE in_set1.
       suff: cid != Snext by move=> /negbTE-> //.
-      suff: (cid < Snext)%ord by rewrite Ord.ltNge; apply: contra => /eqP ->; rewrite Ord.leqxx.
+      suff: (cid < Snext)%ord.
+        rewrite Ord.ltNge.
+        by apply: contra => /eqP ->; rewrite Ord.leqxx.
       move: RPREV; rewrite /get_compartment_id.
       case: pickP => // x /eqP cid_set []?; subst x.
       have: Some cid == Some cid by apply eq_refl.
@@ -1886,7 +1889,9 @@ Proof.
       case: OR_Is => [-> // | <-{I2}].
       rewrite inE in_set1.
       suff: cid' != Snext by move=> /negbTE-> //.
-      suff: (cid' < Snext)%ord by rewrite Ord.ltNge; apply: contra => /eqP ->; rewrite Ord.leqxx.
+      suff: (cid' < Snext)%ord.
+        rewrite Ord.ltNge.
+        by apply: contra => /eqP ->; rewrite Ord.leqxx.
       move: GCI_cid'; rewrite /get_compartment_id.
       case: pickP => // x /eqP cid'_set []?; subst x.
       have: Some cid' == Some cid' by apply eq_refl.
@@ -1987,7 +1992,7 @@ Proof.
     case/and3P: RSC => ? Hs ?.
     apply/and3P.
     split=> //; apply/allP=> x /(allP Hs).
-    by rewrite -(Sym.retag_set_preserves_get_definedness def_s') /=.
+    by rewrite -!mem_domm -(Sym.retag_set_preserves_get_definedness def_s') /=.
   - have := (Sym.retag_set_preserves_good_internal _ RINT def_s').
     apply => //.
     + move=> sc cid' I' W' sc_is_sc.

diff --git a/compartmentalization/symbolic.v b/compartmentalization/symbolic.v
@@ -1,6 +1,7 @@
-Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype Ssreflect.ssrnat Ssreflect.seq Ssreflect.fintype MathComp.finset.
+From mathcomp Require Import
+  ssreflect ssrfun ssrbool eqtype ssrnat seq fintype finset.
 
-Require Import CoqUtils.ord CoqUtils.hseq CoqUtils.word CoqUtils.partmap.
+From CoqUtils Require Import ord hseq word partmap fset.
 
 Require Import lib.utils lib.word_utils lib.ssr_set_utils common.types.
 Require Import symbolic.symbolic.
@@ -391,7 +392,7 @@ Definition isolate (s : Symbolic.state mt) : option (Symbolic.state mt) :=
     do! s' <- retag_set (do_ok c A' J' S')
                         (do_retag c c' A' J' S')
                         (enum_set (A' :|: J' :|: S')) s;
-    
+
     do! pc' @ _              <- RR ra;
     do! DATA c_next I_next _ <- sget s' pc';
     do! guard c == c_next;
@@ -702,12 +703,12 @@ Qed.
 
 Lemma retag_one_preserves_get_definedness ok retag s p s' :
   retag_one ok retag s p ?= s' ->
-  forall p, Symbolic.mem s p = Symbolic.mem s' p :> bool.
+  domm (Symbolic.mem s) = domm (Symbolic.mem s').
 Proof.
   rewrite /retag_one.
   case GET: (sget _ _) => [[cid I W]|] //=.
   case: (ok _ _ _ _) => //=.
-  case: (retag _ _ _ _) => [cid' I' W'] //= UPD p'.
+  case: (retag _ _ _ _) => [cid' I' W'] //= UPD; apply/eq_fset=> p'; rewrite !mem_domm.
   have [{p'} ->|NEQ] := (p' =P p).
   - case GET': (Symbolic.mem s p) => [[x L]|].
     + by rewrite (get_supd_eq GET' UPD).
@@ -717,11 +718,11 @@ Qed.
 
 Lemma retag_set_preserves_get_definedness ok retag ps s s' :
   retag_set ok retag ps s ?= s' ->
-  forall p, Symbolic.mem s p = Symbolic.mem s' p :> bool.
+  domm (Symbolic.mem s) = domm (Symbolic.mem s').
 Proof.
 move=> H.
 have := (@ofoldl_preserve _ _ _ _ _ _ _ (@retag_one_preserves_get_definedness ok retag) _ _ H).
-by apply; eauto.
+apply=> // *; congruence.
 Qed.
 
 Lemma retag_one_preserves_registers ok retag s p s' :

diff --git a/concrete/concrete.v b/concrete/concrete.v
@@ -1,7 +1,6 @@
-Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool.
-Require Import Ssreflect.eqtype Ssreflect.ssrnat Ssreflect.choice.
-Require Import Ssreflect.seq MathComp.ssrint.
-Require Import CoqUtils.ord CoqUtils.word CoqUtils.partmap.
+From mathcomp Require Import
+  ssreflect ssrfun ssrbool eqtype ssrnat seq choice ssrint.
+From CoqUtils Require Import ord word partmap.
 
 Require Import lib.utils common.types.
 
@@ -60,9 +59,6 @@ Proof. by case. Qed.
 
 Definition mvec_choiceMixin := CanChoiceMixin tuple_of_mvecK.
 Canonical mvec_choiceType := Eval hnf in ChoiceType (mvec mt) mvec_choiceMixin.
-Definition mvec_partOrdMixin := CanPartOrdMixin tuple_of_mvecK.
-Canonical mvec_partOrdType :=
-  Eval hnf in PartOrdType (mvec mt) mvec_partOrdMixin.
 Definition mvec_ordMixin := CanOrdMixin tuple_of_mvecK.
 Canonical mvec_ordType := Eval hnf in OrdType (mvec mt) mvec_ordMixin.