Port to MathComp 2

default.nix

@@ -19,6 +19,8 @@ let coqPackages =
   if coqMaster then
     pkgs.coqPackages.overrideScope (self: super: {
       coq = super.coq.override { version = "master"; };
+      coq-elpi = super.coq-elpi.override { version = "coq-master"; };
+      hierarchy-builder = super.hierarchy-builder.override { version = "1.7.0"; };
     })
   else coqPackages_8_19
 ; in

opam

@@ -27,10 +27,10 @@ depends: [
   "yojson" {>= "1.6.0"}
   "angstrom"
   "ocamlfind" { build }
-  "coq" {>= "8.14.0" & < "8.19~"}
-  "coq-mathcomp-ssreflect" {>= "1.17" & < "1.20~"}
+  "coq" {>= "8.18.0" & < "8.20~"}
+  "coq-mathcomp-ssreflect" {>= "2.0" & < "2.3~"}
   "coq-mathcomp-algebra"
-  "coq-mathcomp-word" {>= "2.4" & < "3.0~"}
+  "coq-mathcomp-word" {>= "3.2"}
 ]
 conflicts: [
   "ez-conf-lib"

proofs/3rdparty/ssrring.v

@@ -5,6 +5,7 @@
  * -------------------------------------------------------------------- *)
 
 (* -------------------------------------------------------------------- *)
+From HB Require Import structures.
 From mathcomp Require Import ssreflect eqtype ssrbool ssrnat ssrfun seq.
 From mathcomp Require Import choice ssralg bigop.
 From mathcomp Require Export word_ssrZ.
@@ -277,7 +278,8 @@ Proof.
   by move=> z1 z2 /=; rewrite addm oppm.
 Qed.
 
-Canonical R_of_Z_additive (R : ringType) := Additive (R_of_Z_is_additive R).
+HB.instance Definition _ (R : ringType) :=
+  GRing.isAdditive.Build _ _ (R_of_Z (R:=R)) (R_of_Z_is_additive R).
 
 Lemma R_of_Z_is_multiplicative (R : ringType): multiplicative (R_of_Z (R := R)).
 Proof.
@@ -286,7 +288,8 @@ Proof.
     by rewrite nat_of_P_mult_morphism natrM.
 Qed.
 
-Canonical R_of_Z_rmorphism (R : ringType) := AddRMorphism (R_of_Z_is_multiplicative R).
+HB.instance Definition _ (R : ringType) :=
+  GRing.isMultiplicative.Build _ _ (R_of_Z (R:=R)) (R_of_Z_is_multiplicative R).
 
 Local Notation REeval :=
   (@PEeval _ 0 +%R *%R (fun x y => x - y) -%R Z R_of_Z nat nat_of_N (@GRing.exp _)).

proofs/_CoqProject

@@ -9,6 +9,8 @@
 -arg "-w -hiding-delimiting-key"
 -arg "-w +deprecated-since-mathcomp-1.17.0"
 -arg "-w -argument-scope-delimiter"
+-arg "-w -redundant-canonical-projection"
+-arg "-w -projection-no-head-constant"
 
 -R 3rdparty Jasmin
 -R arch Jasmin

proofs/arch/arch_decl.v

@@ -1,4 +1,5 @@
 (* -------------------------------------------------------------------- *)
+From HB Require Import structures.
 From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype ssralg.
 From mathcomp Require Import word_ssrZ.
 From Coq Require Import
@@ -116,7 +117,7 @@ Variant address :=
 | Arip of pointer.    (* Address relative to instruction pointer. *)
 
 Definition oeq_reg (x y:option reg_t) :=
-  @eq_op (option_eqType ceqT_eqType) x y.
+  @eq_op (option ceqT_eqType) x y.
 
 Definition reg_address_beq (addr1: reg_address) addr2 :=
   match addr1, addr2 with
@@ -131,8 +132,7 @@ case=> [d1 b1 s1 o1] [d2 b2 s2 o2]; apply: (iffP idP) => /=.
 by case; do 4! move=> ->; rewrite /oeq_reg !eqxx.
 Qed.
 
-Definition reg_address_eqMixin := Equality.Mixin reg_address_eq_axiom.
-Canonical reg_address_eqType := EqType reg_address reg_address_eqMixin.
+HB.instance Definition _ := hasDecEq.Build reg_address reg_address_eq_axiom.
 
 (* -------------------------------------------------------------------- *)
 
@@ -148,8 +148,7 @@ Proof.
   by case=> []? []? /=; (constructor || apply: reflect_inj eqP => ?? []).
 Qed.
 
-Definition address_eqMixin := Equality.Mixin address_eq_axiom.
-Canonical address_eqType := EqType address address_eqMixin.
+HB.instance Definition _ := hasDecEq.Build address address_eq_axiom.
 
 (* -------------------------------------------------------------------- *)
 (* Arguments to assembly instructions. *)
@@ -190,8 +189,7 @@ Proof.
   by move=> /Imm_inj [? ];subst => /= ->;rewrite !eqxx.
 Qed.
 
-Definition asm_arg_eqMixin := Equality.Mixin asm_arg_eq_axiom.
-Canonical asm_arg_eqType := EqType asm_arg asm_arg_eqMixin.
+HB.instance Definition _ := hasDecEq.Build asm_arg asm_arg_eq_axiom.
 
 (* -------------------------------------------------------------------- *)
 (* Writing a large word to register or memory
@@ -209,8 +207,7 @@ Proof.
   exact: (eq_axiom_of_scheme internal_msb_flag_dec_bl internal_msb_flag_dec_lb).
 Qed.
 
-Definition msb_flag_eqMixin := Equality.Mixin msb_flag_eq_axiom.
-Canonical msb_flag_eqType := EqType msb_flag msb_flag_eqMixin.
+HB.instance Definition _ := hasDecEq.Build msb_flag msb_flag_eq_axiom.
 
 (* -------------------------------------------------------------------- *)
 (* Implicit arguments.
@@ -233,8 +230,7 @@ Proof.
   by case=> []? []? /=; (constructor || apply: reflect_inj eqP => ?? []).
 Qed.
 
-Definition implicit_arg_eqMixin := Equality.Mixin implicit_arg_eq_axiom.
-Canonical implicit_arg_eqType := EqType _ implicit_arg_eqMixin.
+HB.instance Definition _ := hasDecEq.Build implicit_arg implicit_arg_eq_axiom.
 
 (* -------------------------------------------------------------------- *)
 (* Address kinds.
@@ -292,8 +288,7 @@ Proof.
   exact: (eq_axiom_of_scheme internal_arg_kind_dec_bl internal_arg_kind_dec_lb).
 Qed.
 
-Definition arg_kind_eqMixin := Equality.Mixin arg_kind_eq_axiom.
-Canonical  arg_kind_eqType  := EqType _ arg_kind_eqMixin.
+HB.instance Definition _ := hasDecEq.Build arg_kind arg_kind_eq_axiom.
 
 
 (* An argument position where different argument kinds are allowed is
@@ -564,8 +559,7 @@ Definition asm_typed_reg_beq r1 r2 :=
 Lemma asm_typed_reg_eq_axiom : Equality.axiom asm_typed_reg_beq.
 Proof. case => r1 [] r2 /=; try by (constructor || apply: reflect_inj eqP => ?? []). Qed.
 
-Definition asm_typed_reg_eqMixin := Equality.Mixin asm_typed_reg_eq_axiom.
-Canonical asm_typed_reg_eqType := EqType asm_typed_reg asm_typed_reg_eqMixin.
+HB.instance Definition _ := hasDecEq.Build asm_typed_reg asm_typed_reg_eq_axiom.
 
 (* -------------------------------------------------------------------- *)
 (* Function declaration                                                 *)
@@ -658,8 +652,7 @@ Proof.
   exact: (eq_axiom_of_scheme internal_rflagv_dec_bl internal_rflagv_dec_lb).
 Qed.
 
-Definition rflagv_eqMixin := Equality.Mixin rflagv_eq_axiom.
-Canonical rflagv_eqType := EqType _ rflagv_eqMixin.
+HB.instance Definition _ := hasDecEq.Build rflagv rflagv_eq_axiom.
 
 (* -------------------------------------------------------------------- *)
 (* Assembly declaration. *)

proofs/arch/arch_extra.v

@@ -1,4 +1,5 @@
 (* -------------------------------------------------------------------- *)
+From HB Require Import structures.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
 Require Import xseq strings utils var type values sopn expr fexpr arch_decl.
 Require Import compiler_util.
@@ -279,7 +280,7 @@ Variant extended_op :=
 
 Definition extended_op_beq o1 o2 :=
   match o1, o2 with
-  | BaseOp o1, BaseOp o2 => eq_op (T:= prod_eqType _ ceqT_eqType) o1 o2
+  | BaseOp o1, BaseOp o2 => o1 == o2 :> _ * ceqT_eqType
   | ExtOp o1, ExtOp o2 => o1 == o2 ::>
   | _, _               => false
   end.
@@ -289,8 +290,7 @@ Proof.
   by case=> [] o1 [] o2 /=; (constructor || apply: reflect_inj eqP => ?? []).
 Qed.
 
-Definition extended_op_eqMixin := Equality.Mixin extended_op_eq_axiom.
-Definition extended_op_eqType := EqType extended_op extended_op_eqMixin.
+HB.instance Definition _ := hasDecEq.Build extended_op extended_op_eq_axiom.
 
 Definition get_instr_desc (o: extended_op) : instruction_desc :=
  match o with

proofs/arch/asm_gen.v

@@ -594,13 +594,13 @@ Definition assemble_prog (p : lprog) : cexec asm_prog :=
   let rsp := mk_ptr (lp_rsp p) in
   Let _ :=
     assert
-      ((to_reg  rip == None :> option_eqType ceqT_eqType) && 
-       (to_regx rip == None :> option_eqType ceqT_eqType))  
+      ((to_reg  rip == None :> option ceqT_eqType) &&
+       (to_regx rip == None :> option ceqT_eqType))
       (E.gen_error true None None (pp_s "Invalid RIP"))
   in
   Let _ :=
     assert
-      (of_ident (lp_rsp p) == Some ad_rsp :> option_eqType ceqT_eqType)
+      (of_ident (lp_rsp p) == Some ad_rsp :> option ceqT_eqType)
       (E.gen_error true None None (pp_s "Invalid RSP"))
   in
   Let fds :=

proofs/compiler/arm_extra.v

@@ -1,3 +1,4 @@
+From HB Require Import structures.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssralg.
 
 Require Import
@@ -37,10 +38,7 @@ Proof.
        internal_arm_extra_op_dec_lb).
 Qed.
 
-Definition arm_extra_op_eqMixin :=
-  Equality.Mixin arm_extra_op_eq_axiom.
-Canonical arm_extra_op_eqType :=
-  Eval hnf in EqType arm_extra_op arm_extra_op_eqMixin.
+HB.instance Definition _ := hasDecEq.Build arm_extra_op arm_extra_op_eq_axiom.
 
 #[ export ]
 Instance eqTC_arm_extra_op : eqTypeC arm_extra_op :=

proofs/compiler/byteset.v

@@ -1,4 +1,5 @@
 (* ** Imports and settings *)
+From HB Require Import structures.
 From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat seq eqtype.
 Require Import utils Wellfounded.
 Import Lexicographic_Product Relation_Operators.
@@ -174,7 +175,7 @@ Proof. case: t => //=; rewrite andbT; symmetry; apply/ZltP; lia. Qed.
 Record Bytes := mkBytes { tobytes :> bytes; _wf : wf tobytes; }.
 Definition t := Bytes.
 
-Canonical Bytes_subType := Eval hnf in [subType for tobytes].
+HB.instance Definition _ := [isSub for tobytes].
 
 (* ----------------------------------------- *)
 Fixpoint _memi (t: bytes) i :=

proofs/compiler/compiler.v

@@ -1,3 +1,4 @@
+From HB Require Import structures.
 From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat seq eqtype fintype.
 From mathcomp Require Import ssralg.
 Require Import ZArith Uint63.
@@ -150,8 +151,7 @@ Proof.
        internal_compiler_step_dec_bl
        internal_compiler_step_dec_lb).
 Qed.
-Definition compiler_step_eqMixin := Equality.Mixin compiler_step_eq_axiom.
-Canonical  compiler_step_eqType  := Eval hnf in EqType compiler_step compiler_step_eqMixin.
+HB.instance Definition _ := hasDecEq.Build compiler_step compiler_step_eq_axiom.
 
 Lemma compiler_step_list_complete : Finite.axiom compiler_step_list.
 Proof. by case. Qed.

proofs/compiler/constant_prop.v

@@ -1,4 +1,5 @@
 (* ** Imports and settings *)
+From HB Require Import structures.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssralg.
 From mathcomp Require Import word_ssrZ.
 Require Import expr ZArith sem_op_typed compiler_util.
@@ -334,8 +335,7 @@ subst => /=.
 by apply:(iffP idP) => [ /eqP | [] ] ->.
 Qed.
 
-Definition const_v_eqMixin     := Equality.Mixin const_v_eq_axiom.
-Canonical  const_v_eqType      := Eval hnf in EqType const_v const_v_eqMixin.
+HB.instance Definition _ := hasDecEq.Build const_v const_v_eq_axiom.
 
 Local Notation cpm := (Mvar.t const_v).
 

proofs/compiler/linearization_proof.v

@@ -3923,10 +3923,10 @@ Section PROOF.
             have hgetr2 : get_var true vm2 (vid saved_stack) = ok (Vword (top_stack (emem s1))).
             + rewrite  -(get_var_eq_ex _ saved_stack_not_written K2).
               exact: hgetr.
-            rewrite (spec_lmove
-                 hliparams (lp:= p')
-                 (x:= (vid (sp_rsp (p_extra p)))) (y:= vid saved_stack)
-                 (ls := (setpc (lset_estate ls1 (escs s2') m2 vm2) (size P + size lbody)))
+            rewrite (@spec_lmove _
+                 hliparams p'
+                 (setpc (lset_estate ls1 (escs s2') m2 vm2) (size P + size lbody))
+                 (vid (sp_rsp (p_extra p))) (vid saved_stack) _
                  erefl erefl hgetr2) addnS; reflexivity.
 
         + rewrite to_save_empty Sv_diff_empty. clear - ok_rsp K2 hvm.
@@ -4147,7 +4147,7 @@ Section PROOF.
         have [read_in_m3 read_spilled] := read_after_spill top_no_overflow1 stk_sz_pos ok_to_save1 ok_m3.
         set to_restore := (sf_to_save (f_extra fd)) ++ [:: (vrsp, stack_saved_rsp)].
         have read_in_spilled :
-          ∀ (x : var_eqType) (ofs : Z_eqType),
+          ∀ (x : var) (ofs : Z),
              (x, ofs) \in to_restore ->
              exists2 ws, vtype x = sword ws /\ lip_check_ws liparams ws &
              exists2 w: word ws, read m3 Aligned (top + wrepr Uptr ofs)%R ws = ok w &

proofs/compiler/stack_alloc.v

@@ -1,4 +1,5 @@
 (* ** Imports and settings *)
+From HB Require Import structures.
 From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat seq eqtype ssralg.
 From mathcomp Require Import word_ssrZ.
 Require Import strings word utils type var expr.
@@ -82,12 +83,11 @@ Proof.
   by apply:(iffP and3P) => /= [[/eqP -> /eqP -> /eqP ->] | [-> -> ->]].
 Qed.
 
-Definition region_eqMixin := Equality.Mixin region_axiom.
-Canonical  region_eqType  := Eval hnf in EqType region region_eqMixin.
+HB.instance Definition _ := hasDecEq.Build region region_axiom.
 
 Module CmpR.
 
-  Definition t := [eqType of region].
+  Definition t : eqType := region.
 
   Definition cmp (r1 r2: t) :=
     Lex (bool_cmp r1.(r_writable) r2.(r_writable))
@@ -121,8 +121,7 @@ Proof.
   exact: (eq_axiom_of_scheme internal_zone_dec_bl internal_zone_dec_lb).
 Qed.
 
-Definition zone_eqMixin := Equality.Mixin zone_eq_axiom.
-Canonical  zone_eqType  := EqType zone zone_eqMixin.
+HB.instance Definition _ := hasDecEq.Build zone zone_eq_axiom.
 
 Definition disjoint_zones z1 z2 :=
   (((z1.(z_ofs) + z1.(z_len))%Z <= z2.(z_ofs)) ||
@@ -144,8 +143,7 @@ Proof.
   by apply:(iffP andP) => /= [[/eqP -> /eqP ->] | [-> ->]].
 Qed.
 
-Definition sub_region_eqMixin := Equality.Mixin sub_region_eq_axiom.
-Canonical sub_region_eqType := EqType sub_region sub_region_eqMixin.
+HB.instance Definition _ := hasDecEq.Build sub_region sub_region_eq_axiom.
 
 (* ------------------------------------------------------------------ *)
 (* idea: could we use a gvar instead of var & v_scope? *)

proofs/compiler/unionfind.v

@@ -301,7 +301,7 @@ End NaiveUnionFind.
 
 
 Module LblEqType <: EqType.
-  Definition T := [eqType of label].
+  Definition T : eqType := label.
 End LblEqType.