Update dependencies (AU-COBRA#243)

.github/coq-concert.opam.locked

@@ -10,19 +10,28 @@ homepage: "https://github.com/AU-COBRA/ConCert"
 doc: "https://au-cobra.github.io/ConCert/toc.html"
 bug-reports: "https://github.com/AU-COBRA/ConCert/issues"
 depends: [
-  "coq" {= "8.18.0"}
-  "coq-bignums" {= "9.0.0+coq8.18"}
-  "coq-metacoq-common" {= "1.2.1+8.18"}
-  "coq-metacoq-erasure" {= "1.2.1+8.18"}
-  "coq-metacoq-pcuic" {= "1.2.1+8.18"}
-  "coq-metacoq-safechecker" {= "1.2.1+8.18"}
-  "coq-metacoq-template" {= "1.2.1+8.18"}
-  "coq-metacoq-template-pcuic" {= "1.2.1+8.18"}
-  "coq-metacoq-utils" {= "1.2.1+8.18"}
-  "coq-rust-extraction" {= "dev"}
-  "coq-elm-extraction" {= "dev"}
+  "coq" {= "8.19.0"}
+  "coq-bignums" {= "9.0.0+coq8.19"}
+  "coq-metacoq-common" {= "1.3.2+8.19"}
+  "coq-metacoq-erasure" {= "1.3.2+8.19"}
+  "coq-metacoq-pcuic" {= "1.3.2+8.19"}
+  "coq-metacoq-safechecker" {= "1.3.2+8.19"}
+  "coq-metacoq-template" {= "1.3.2+8.19"}
+  "coq-metacoq-template-pcuic" {= "1.3.2+8.19"}
+  "coq-metacoq-utils" {= "1.3.2+8.19"}
+  "coq-rust-extraction" {= "0.1.0"}
+  "coq-elm-extraction" {= "0.1.0"}
   "coq-quickchick" {= "2.0.4"}
-  "coq-stdpp" {= "1.9.0"}
+  "coq-stdpp" {= "1.10.0"}
+]
+pin-depends: [
+  ["coq-metacoq-utils.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
+  ["coq-metacoq-common.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
+  ["coq-metacoq-template.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
+  ["coq-metacoq-template-pcuic.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
+  ["coq-metacoq-pcuic.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
+  ["coq-metacoq-safechecker.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
+  ["coq-metacoq-erasure.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
 ]
 build: [
   [make]
@@ -34,13 +43,3 @@ install: [
   [make "-C" "examples" "install"] {with-test}
 ]
 dev-repo: "git+https://github.com/AU-COBRA/ConCert.git"
-pin-depends: [
-  [
-    "coq-rust-extraction.dev"
-    "git+https://github.com/AU-COBRA/coq-rust-extraction.git#0053733e56008c917bf43d12e8bf0616d3b9a856"
-  ]
-  [
-    "coq-elm-extraction.dev"
-    "git+https://github.com/AU-COBRA/coq-elm-extraction.git#903320120e3f36d7857161e5680fabeb6e743c6b"
-  ]
-]

README.md

@@ -13,19 +13,19 @@ ConCert can find real-world attacks as explained
 
 ## How to build
 
-Our development works with Coq 8.17 and depends on MetaCoq, and std++.
+Our development works with Coq 8.19 and depends on MetaCoq, and std++.
 The tests depend on QuickChick.
 The dependencies can be installed through `opam`.
 
 Branches compatible with older versions of Coq can be found [here](https://github.com/AU-COBRA/ConCert/branches/all?query=coq-).
 
 ### Install dependencies and build ConCert locally
 
-Installing the necessary dependencies requires the opam package manager and a switch with Coq 8.17 installed.
+Installing the necessary dependencies requires the opam package manager and a switch with Coq 8.19 installed.
 If you don't already have a switch set up run the following commands
 
 ```bash
-opam switch create . 4.10.2 --repositories default,coq-released=https://coq.inria.fr/opam/released
+opam switch create . 4.14.2 --repositories default,coq-released=https://coq.inria.fr/opam/released
 eval $(opam env)
 ```
 

coq-concert.opam

@@ -14,24 +14,29 @@ bug-reports: "https://github.com/AU-COBRA/ConCert/issues"
 doc: "https://au-cobra.github.io/ConCert/toc.html"
 
 depends: [
-  "coq" {>= "8.17" & < "8.19~"}
+  "coq" {>= "8.19" & < "8.20~"}
   "coq-bignums" {>= "8"}
   "coq-quickchick" {>= "2.0.4"}
-  "coq-metacoq-utils" {>= "1.2" & < "1.3~"}
-  "coq-metacoq-common" {>= "1.2" & < "1.3~"}
-  "coq-metacoq-template" {>= "1.2" & < "1.3~"}
-  "coq-metacoq-template-pcuic" {>= "1.2" & < "1.3~"}
-  "coq-metacoq-pcuic" {>= "1.2" & < "1.3~"}
-  "coq-metacoq-safechecker" {>= "1.2" & < "1.3~"}
-  "coq-metacoq-erasure" {>= "1.2" & < "1.3~"}
-  "coq-rust-extraction" {= "dev"}
-  "coq-elm-extraction" {= "dev"}
-  "coq-stdpp" {= "1.9.0"}
+  "coq-metacoq-utils" {>= "1.3.1" & < "1.4~"}
+  "coq-metacoq-common" {>= "1.3.1" & < "1.4~"}
+  "coq-metacoq-template" {>= "1.3.1" & < "1.4~"}
+  "coq-metacoq-template-pcuic" {>= "1.3.1" & < "1.4~"}
+  "coq-metacoq-pcuic" {>= "1.3.1" & < "1.4~"}
+  "coq-metacoq-safechecker" {>= "1.3.1" & < "1.4~"}
+  "coq-metacoq-erasure" {>= "1.3.1" & < "1.4~"}
+  "coq-rust-extraction" {= "0.1.0"}
+  "coq-elm-extraction" {= "0.1.0"}
+  "coq-stdpp" {>= "1.9.0" & < "1.11~"}
 ]
 
 pin-depends: [
-  ["coq-rust-extraction.dev" "git+https://github.com/AU-COBRA/coq-rust-extraction.git#0053733e56008c917bf43d12e8bf0616d3b9a856"]
-  ["coq-elm-extraction.dev" "git+https://github.com/AU-COBRA/coq-elm-extraction.git#903320120e3f36d7857161e5680fabeb6e743c6b"]
+  ["coq-metacoq-utils.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
+  ["coq-metacoq-common.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
+  ["coq-metacoq-template.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
+  ["coq-metacoq-template-pcuic.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
+  ["coq-metacoq-pcuic.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
+  ["coq-metacoq-safechecker.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
+  ["coq-metacoq-erasure.1.3.2+8.19" "git+https://github.com/MetaCoq/metacoq.git#a9f5da7534b62cda3c870e64f00998e7ee5485f5"]
 ]
 
 build: [

embedding/extraction/PreludeExt.v

@@ -144,12 +144,12 @@ Next Obligation.
   intros a b. destruct a,b; simpl.
   - destruct (n =? n0)%nat eqn:Heq.
     * constructor. now rewrite Nat.eqb_eq in *.
-    * constructor. now rewrite NPeano.Nat.eqb_neq in *.
+    * constructor. now rewrite Nat.eqb_neq in *.
   - now constructor.
   - now constructor.
   - destruct (n =? n0)%nat eqn:Heq.
     * constructor. now rewrite Nat.eqb_eq in *.
-    * constructor. now rewrite NPeano.Nat.eqb_neq in *.
+    * constructor. now rewrite Nat.eqb_neq in *.
 Qed.
 Next Obligation.
   intros ??. unfold base.Decision.

embedding/theories/pcuic/PCUICCorrectnessAux.v

@@ -240,17 +240,17 @@ Lemma type_value_term_value Σ ty :
   PcbvCurr.value Σ (type_to_term ty).
 Proof.
   intros Hc Hty. induction Hty.
-  + simpl. constructor. apply tInd_atom.
-  + simpl. now constructor.
+  + simpl. constructor. constructor. apply tInd_atom.
   + simpl. now constructor.
+  + simpl. constructor. now constructor.
   + simpl in *. propify. destruct_hyps.
     erewrite decompose_inductive_mkApps by eauto.
     rewrite <- mkApps_unfold.
     eapply PcbvCurr.value_app.
     * apply tInd_value_head.
     * apply All_app_inv; eauto.
       eapply decompose_inductive_value with (t1 := ty1); eauto.
-  + constructor; eauto.
+  + do 2 constructor; eauto.
 Qed.
 
 #[export] Hint Constructors ty_val : hints.
@@ -369,9 +369,9 @@ Proof.
     inversion Hok; subst.
     eapply Wcbv_value_vars_to_apps; eauto.
     eapply All_impl_inner; eauto.
-  + destruct cm. constructor; auto.
-    simpl. now constructor.
-  + simpl in *. constructor; auto.
+  + destruct cm. do 2 constructor; auto.
+    simpl. now do 2 constructor.
+  + simpl in *. do 2 constructor; auto.
   + simpl in *.
     inversion Hok; subst. now eapply type_value_term_value.
 Qed.

embedding/theories/pcuic/PCUICTranslate.v

@@ -35,7 +35,7 @@ Reserved Notation "T⟦ ty ⟧ " (at level 5).
 Fixpoint type_to_term (ty : type) : term :=
   match ty with
   | tyInd i => tInd (mkInd (kername_of_string i) 0) []
-  | tyForall nm ty => tProd (aRelevant (nNamed (TCString.of_string nm))) (tSort Universe.type0) T⟦ty⟧
+  | tyForall nm ty => tProd (aRelevant (nNamed (TCString.of_string nm))) (tSort Sort.type0) T⟦ty⟧
   | tyVar nm => tVar (TCString.of_string nm)
   | tyApp ty1 ty2 => tApp T⟦ty1⟧ T⟦ty2⟧
   | tyArr ty1 ty2 =>
@@ -84,7 +84,7 @@ Fixpoint expr_to_term (Σ : global_env) (e : expr) : term :=
   | eRel i => tRel i
   | eVar nm => tVar (TCString.of_string nm)
   | eLambda nm ty b => tLambda (aRelevant (nNamed (TCString.of_string nm))) T⟦ty⟧ t⟦b⟧Σ
-  | eTyLam nm b => tLambda (aRelevant (nNamed (TCString.of_string nm))) (tSort Universe.type0) t⟦b⟧Σ
+  | eTyLam nm b => tLambda (aRelevant (nNamed (TCString.of_string nm))) (tSort Sort.type0) t⟦b⟧Σ
   | eLetIn nm e1 ty e2 => tLetIn (aRelevant (nNamed (TCString.of_string nm))) t⟦e1⟧Σ T⟦ty⟧ t⟦e2⟧Σ
   | eApp e1 e2 => tApp t⟦e1⟧Σ t⟦e2⟧Σ
   | eConstr i t =>
@@ -175,7 +175,7 @@ Definition trans_one_constr (ind_name : ename) (nparam : nat) (c : constr) : ter
 Fixpoint gen_params n := match n with
                          | O => []
                          | S n' => let nm := ("A" ++ string_of_nat n)%bs in
-                                  let decl := (tSort Universe.type0) in
+                                  let decl := (tSort Sort.type0) in
                                   gen_params n' ++ [mkdecl (aRelevant (nNamed nm)) None (decl)]
                          end.
 
@@ -185,7 +185,7 @@ Definition trans_global_dec (gd : global_dec) : mutual_inductive_entry :=
     let (mp,unqualified_nm) := kername_of_string nm in
     let oie := {|
           mind_entry_typename := unqualified_nm;
-          mind_entry_arity := tSort Universe.type0;
+          mind_entry_arity := tSort Sort.type0;
           mind_entry_template := false;
           mind_entry_consnames :=
             map (fun c => let (mp,unqualified_nm) := kername_of_string c.1 in

examples/boardroomVoting/BoardroomVotingTest.v

@@ -1,4 +1,5 @@
-From Coq Require Import Cyclic31.
+(* From Coq Require Import Cyclic31. *)
+From Coq.Numbers.Cyclic.Int63 Require Import Cyclic63.
 From Coq Require Import List.
 From Coq Require Import Znumtheory.
 From ConCert.Utils Require Import Extras.

examples/counter/extraction/CounterRefTypesMidlang.v

@@ -128,21 +128,30 @@ Definition ignored_concert_types :=
          <%% @ContractCallContext %%>;
          <%% @SerializedValue %%>].
 
+(* TODO: tmp, revert once https://github.com/MetaCoq/metacoq/pull/1030 is resolved *)
+From MetaCoq.Erasure.Typed Require Import Optimize.
+Definition extract_within_coq : extract_template_env_params :=
+  {| template_transforms := [];
+     check_wf_env_func Σ := Ok (assume_env_wellformed Σ);
+     pcuic_args :=
+       {| optimize_prop_discr := true;
+          extract_transforms := [dearg_transform (fun _ => None) true false true true true] |} |}.
 
 Definition counter_extract :=
-    Eval vm_compute in
-    extract_template_env_within_coq
+  Eval vm_compute in
+    extract_template_env extract_within_coq
       counter_env
       (KernameSet.singleton counter_name)
       (fun kn => List.existsb (eq_kername kn)
                               (ignored_concert_types
                                  ++ map fst midlang_translation_map
                                  ++ map fst TT)).
 
-Definition counter_result := Eval compute in
-     (env <- counter_extract ;;
-      '(_, lines) <- finish_print_lines (print_env env midlang_counter_translate);;
-      ret lines).
+Definition counter_result :=
+  Eval compute in
+    (env <- counter_extract ;;
+    '(_, lines) <- finish_print_lines (print_env env midlang_counter_translate);;
+    ret lines).
 
 Definition wrap_in_delimiters s :=
   concat Common.nl [""; "{-START-} "; s; "{-END-}"].

examples/crowdfunding/ExecFrameworkIntegration.v

@@ -35,7 +35,7 @@ Definition global_to_tc := compose trans_minductive_entry trans_global_dec.
 Global Program Instance CB : ChainBase :=
   build_chain_base nat Nat.eqb _ _ _ _ Nat.odd. (* Odd addresses are addresses of contracts :) *)
 Next Obligation.
-  eapply NPeano.Nat.eqb_spec.
+  eapply Nat.eqb_spec.
 Defined.
 
 Definition to_chain (sc : SimpleChain_coq) : Chain :=

examples/eip20/EIP20TokenCorrect.v

@@ -150,17 +150,17 @@ Section Theories.
 
   Ltac FMap_simpl_step :=
     match goal with
-      | |- context [ FMap.find ?x (FMap.add ?x _ _) ] => setoid_rewrite FMap.find_add
+      | |- context [ FMap.find ?x (FMap.add ?x _ _) ] => rewrite FMap.find_add
       | H : FMap.find ?t ?m = Some _ |- FMap.find ?t ?m = Some _ => cbn; rewrite H; f_equal; lia
-      | H : ?x <> ?y |- context [ FMap.find ?x (FMap.add ?y _ _) ] => setoid_rewrite FMap.find_add_ne; eauto
-      | H : ?y <> ?x |- context [ FMap.find ?x (FMap.add ?y _ _) ] => setoid_rewrite FMap.find_add_ne; eauto
-      | H : FMap.find ?x _ = Some _ |- context [ FMap.elements (FMap.add ?x _ _) ] => setoid_rewrite FMap.elements_add_existing; eauto
-      | |- context [ FMap.add ?x _ (FMap.add ?x _ _) ] => setoid_rewrite FMap.add_add
-      | H : FMap.find ?x _ = None |- context [ FMap.elements (FMap.add ?x _ _) ] => setoid_rewrite FMap.elements_add; eauto
+      | H : ?x <> ?y |- context [ FMap.find ?x (FMap.add ?y _ _) ] => rewrite FMap.find_add_ne; eauto
+      | H : ?y <> ?x |- context [ FMap.find ?x (FMap.add ?y _ _) ] => rewrite FMap.find_add_ne; eauto
+      | H : FMap.find ?x _ = Some _ |- context [ FMap.elements (FMap.add ?x _ _) ] => rewrite FMap.elements_add_existing; eauto
+      | |- context [ FMap.add ?x _ (FMap.add ?x _ _) ] => rewrite FMap.add_add
+      | H : FMap.find ?x _ = None |- context [ FMap.elements (FMap.add ?x _ _) ] => rewrite FMap.elements_add; eauto
       | |- context [ FMap.remove ?x (FMap.add ?x _ _) ] => rewrite fin_maps.delete_insert_delete
-      | |- context [ FMap.find ?x (FMap.partial_alter _ ?x _) ] => setoid_rewrite FMap.find_partial_alter
-      | H : ?x' <> ?x |- context [ FMap.find ?x' (FMap.partial_alter _ ?x _) ] => setoid_rewrite FMap.find_partial_alter_ne; auto
-      | H : ?x <> ?x' |- context [ FMap.find ?x' (FMap.partial_alter _ ?x _) ] => setoid_rewrite FMap.find_partial_alter_ne
+      | |- context [ FMap.find ?x (FMap.partial_alter _ ?x _) ] => rewrite FMap.find_partial_alter
+      | H : ?x' <> ?x |- context [ FMap.find ?x' (FMap.partial_alter _ ?x _) ] => rewrite FMap.find_partial_alter_ne; auto
+      | H : ?x <> ?x' |- context [ FMap.find ?x' (FMap.partial_alter _ ?x _) ] => rewrite FMap.find_partial_alter_ne
       | H : context [ AddressMap.find _ _ ] |- _ => rewrite AddressMap_find_convertible in H
       | H : context [ AddressMap.add _ _ _ ] |- _ => rewrite AddressMap_add_convertible in H
       | H : context [ increment_balance _ _ _ ] |- _ => rewrite increment_balanace_is_partial_alter_plus in H
@@ -665,6 +665,9 @@ Section Theories.
   Qed.
 
 
+  Remove Hints MCRelations.on_rel_refl : typeclass_instances.
+  Remove Hints MCRelations.on_rel_trans : typeclass_instances.
+  Remove Hints MCRelations.on_rel_sym : typeclass_instances.
 
   (** ** Sum of balances always equals total supply *)
   Lemma sum_balances_eq_total_supply bstate caddr :
@@ -680,7 +683,8 @@ Section Theories.
       inversion_clear init_some.
       unfold sum_balances.
       setoid_rewrite FMap.elements_add; auto.
-      setoid_rewrite FMap.elements_empty. cbn. lia.
+
+      rewrite FMap.elements_empty. cbn. lia.
     - intros IH receive_some.
       unfold Blockchain.receive in *.
       cbn in *.

examples/escrow/extraction/EscrowMidlang.v

@@ -62,7 +62,8 @@ Definition extract_params :=
      template_transforms := [template_inline should_inline];
      pcuic_args :=
        {| optimize_prop_discr := true;
-          extract_transforms := [Optimize.dearg_transform (fun _ => None) true true true true true] |} |}.
+          (* TODO: tmp, revert once https://github.com/MetaCoq/metacoq/pull/1030 is resolved *)
+          extract_transforms := [Optimize.dearg_transform (fun _ => None) true false true true true] |} |}.
 
 Axiom extraction_chain_base : ChainBase.
 #[local]

execution/theories/BuildUtils.v

@@ -604,7 +604,7 @@ Proof.
     split; eauto.
     do 3 try split; only 9: apply env_eq; eauto; cbn; try lia.
     + now apply finalized_heigh_chain_height.
-    + apply NPeano.Nat.sub_0_le in slot_hit.
+    + apply Nat.sub_0_le in slot_hit.
       rewrite_environment_equiv. cbn. lia.
   - specialize (forward_time_exact bstate reward creator slot) as
       (bstate' & header & reach' & header_valid & slot_hit' & queue' & env_eq); eauto.

execution/theories/Containers.v

@@ -135,10 +135,11 @@ Module FMap.
       Permutation (keys (add k v' m)) (keys m).
     Proof.
       revert k.
+      (* Search (stdpp.base.lookup _ _ = _ -> Permutation _ _). *)
       induction m using fin_maps.map_ind; intros k find_some.
       + rewrite find_empty in find_some.
         congruence.
-      + destruct (stdpp.base.decide (k = i)) as [->|].
+      + destruct (EqDecision0 k i) as [->|].
         * rewrite fin_maps.insert_insert.
           unfold keys.
           rewrite 2!fin_maps.map_to_list_insert by auto.
@@ -154,6 +155,7 @@ Module FMap.
           now rewrite IHm.
     Qed.
 
+
     Lemma ind (P : FMap K V -> Prop) :
       P empty ->
       (forall k v m, find k m = None -> P m -> P (add k v m)) ->
@@ -193,7 +195,7 @@ Module FMap.
       - rewrite elements_empty, find_empty.
         split; easy.
       - rewrite elements_add by auto.
-        destruct (stdpp.base.decide (k = k0)) as [->|?].
+        destruct (EqDecision0 k k0) as [->|?].
         + rewrite find_add.
           cbn.
           split; intros.

execution/theories/Serializable.v

@@ -470,6 +470,8 @@ Section Countable.
            (t : SerializedType) : countable.Countable (interp_type t).
   Proof. induction t; typeclasses eauto. Defined.
 
+  Import (hints) stdpp.base.
+
   Global Instance SerializedValue_EqDecision : stdpp.base.EqDecision SerializedValue.
   Proof.
     intros x y.

extraction/tests/CameLIGOExtractionTests.v

@@ -12,6 +12,8 @@ From Coq Require Import String.
 
 Import MCMonadNotation.
 
+Context `{Blockchain.ChainBase}.
+
 Local Close Scope bs_scope.
 Local Open Scope string_scope.