Porting ConCert to Metacoq v1.0+8.14 (#187)

.github/workflows/build.yml

@@ -22,7 +22,7 @@ jobs:
   build:
     runs-on: ubuntu-latest
     container:
-      image: aucobra/concert:deps-coq-8.11-with-compilers-ligo-0.38.1
+      image: aucobra/concert:deps-8.14-with-compilers
       options: --user root
     steps:
     - name: Checkout branch ${{ github.ref_name }}
@@ -38,7 +38,7 @@ jobs:
     - name: Build core
       run: |
         echo "::group::Setting up switch"
-        eval $(opam env --switch=${COMPILER_EDGE} --set-switch)
+        eval $(opam env --switch=${COMPILER} --set-switch)
         echo "::endgroup::"
 
         echo "::group::Build utilities"
@@ -59,7 +59,7 @@ jobs:
     - name: Build examples
       run: |
         echo "::group::Setting up switch"
-        eval $(opam env --switch=${COMPILER_EDGE} --set-switch)
+        eval $(opam env --switch=${COMPILER} --set-switch)
         echo "::endgroup::"
 
         echo "::group::Build examples"
@@ -68,7 +68,7 @@ jobs:
     - name: Test extraction
       run: |
         echo "::group::Setting up switch"
-        eval $(opam env --switch=${COMPILER_EDGE} --set-switch)
+        eval $(opam env --switch=${COMPILER} --set-switch)
         echo "::endgroup::"
 
         echo "::group::Running tests"
@@ -83,7 +83,7 @@ jobs:
       if: github.event_name == 'push' && github.ref == 'refs/heads/master'
       run: |
         echo "::group::Setting up switch"
-        eval $(opam env --switch=${COMPILER_EDGE} --set-switch)
+        eval $(opam env --switch=${COMPILER} --set-switch)
         echo "::endgroup::"
 
         echo "::group::Running coqdoc"

README.md

@@ -8,17 +8,16 @@ ConCert is able to find real world attacks as explained [here](https://medium.co
 ## How to build
 
 
-Our development works with Coq 8.11.2. and depends on MetaCoq installed from source,
-std++ and coq-bignums. The tests depend on QuickChick. Most of the dependencies can be installed through `opam`.
+Our development works with Coq 8.14 and depends on MetaCoq installed from source,
+std++ and coq-equations. The tests depend on QuickChick. Most of the dependencies can be installed through `opam`.
 
 To set up a switch with the necessary dependencies run the following commands from the root of the project:
 
 ```bash
-opam switch create . 4.07.1
+opam switch create . 4.08.1
 eval $(opam env)
 opam repo add coq-released https://coq.inria.fr/opam/released
-opam install -j 4 coq.8.11.2 coq-bignums coq-stdpp.1.5.0 coq-quickchick
-opam pin -j 4 add https://github.com/MetaCoq/metacoq.git#75f0cb9b8494cd0a856b77a664c662a59ddde447
+opam install ./coq-concert.opam --deps-only
 ```
 
 After completing the procedures above, run `make` to build the development, and `make html` to build the documentation. 

coq-concert.opam

@@ -17,21 +17,13 @@ depends: [
   "ocaml" {>= "4.07.1"}
   "coq" {>= "8.11" & < "8.12~"}
   "coq-bignums" {= "8.11.0"}
-  "coq-quickchick" {= "1.3.2"}
-  "coq-metacoq-template" {pinned}
-  "coq-metacoq-pcuic" {pinned}
-  "coq-metacoq-safechecker" {pinned}
-  "coq-metacoq-erasure" {pinned}
-  "coq-metacoq-translations" {pinned}
-  "coq-equations" {= "1.2.3+8.11"}
-  "coq-stdpp" {= "1.5.0"}
-]
-pin-depends: [
-  ["coq-metacoq-template.pinned" "git+https://github.com/MetaCoq/metacoq.git#75f0cb9b8494cd0a856b77a664c662a59ddde447"]
-  ["coq-metacoq-pcuic.pinned" "git+https://github.com/MetaCoq/metacoq.git#75f0cb9b8494cd0a856b77a664c662a59ddde447"]
-  ["coq-metacoq-safechecker.pinned" "git+https://github.com/MetaCoq/metacoq.git#75f0cb9b8494cd0a856b77a664c662a59ddde447"]
-  ["coq-metacoq-erasure.pinned" "git+https://github.com/MetaCoq/metacoq.git#75f0cb9b8494cd0a856b77a664c662a59ddde447"]
-  ["coq-metacoq-translations.pinned" "git+https://github.com/MetaCoq/metacoq.git#75f0cb9b8494cd0a856b77a664c662a59ddde447"]
+  "coq-quickchick" {= "1.6.0"}
+  "coq-metacoq-template" {= "1.0+8.14"}
+  "coq-metacoq-pcuic" {= "1.0+8.14"}
+  "coq-metacoq-safechecker" {= "1.0+8.14"}
+  "coq-metacoq-erasure" {= "1.0+8.14"}
+  "coq-equations" {= "1.3+8.14"}
+  "coq-stdpp" {= "1.7.0"}
 ]
 
 build: [

embedding/examples/AcornExamples.v

@@ -1,4 +1,5 @@
 (** * Examples of library code and contracts originating from the actual Acorn implementation  *)
+From MetaCoq.Template Require Import All.
 From ConCert.Embedding Require Import Ast.
 From ConCert.Embedding Require Import Notations.
 From ConCert.Embedding Require Import PCUICTranslate.
@@ -9,9 +10,8 @@ From Coq Require Import Basics.
 From Coq Require Import String.
 From Coq Require Import List.
 From Coq Require Import PeanoNat.
-From MetaCoq.Template Require Import All.
 
-Import MonadNotation.
+Import MCMonadNotation.
 Import ListNotations.
 
 Open Scope list.

embedding/examples/Demo.v

@@ -16,7 +16,7 @@ Definition global_to_tc := compose trans_minductive_entry trans_global_dec.
 Module TC := Template.BasicAst.
 
 Import ListNotations.
-Import MonadNotation.
+Import MCMonadNotation.
 Import BaseTypes.
 Import StdLib.
 
@@ -26,22 +26,28 @@ Import BasicAst.
 
 (** MetaCoq demo *)
 
-(* Quote *)
-MetaCoq Quote Definition id_nat_syn := (fun x : nat => x).
-Print id_nat_syn.
-(* Ast.tLambda (nNamed "x")
-   (Ast.tInd {| TC.inductive_mind := "nat"; TC.inductive_ind := 0 |}
-      []) (Ast.tRel 0) : Ast.term *)
+Section MCDemo.
 
-(* Unquote *)
-MetaCoq Unquote Definition plus_one :=
-  (MC.tLambda (aRelevant (nNamed "x"))
-              (MC.tInd (mkInd (MPfile ["Datatypes"; "Init"; "Coq"], "nat") 0) nil)
-              (MC.tApp (MC.tConstruct (mkInd (MPfile ["Datatypes"; "Init"; "Coq"], "nat") 0) 1 nil)
-                       (MC.tRel 0 :: nil))).
+  Import bytestring.
 
-(* fun x : nat => S x : nat -> nat *)
+  Local Open Scope bs.
 
+  (* Quote *)
+  MetaCoq Quote Definition id_nat_syn := (fun x : nat => x).
+  Print id_nat_syn.
+  (* Ast.tLambda (nNamed "x")
+     (Ast.tInd {| TC.inductive_mind := "nat"; TC.inductive_ind := 0 |}
+        []) (Ast.tRel 0) : Ast.term *)
+
+  (* Unquote *)
+  MetaCoq Unquote Definition plus_one :=
+    (MC.tLambda (aRelevant (nNamed "x"))
+                (MC.tInd (mkInd (MPfile ["Datatypes"; "Init"; "Coq"], "nat") 0) nil)
+                (MC.tApp (MC.tConstruct (mkInd (MPfile ["Datatypes"; "Init"; "Coq"], "nat") 0) 1 nil)
+                         (MC.tRel 0 :: nil))).
+
+  (* fun x : nat => S x : nat -> nat *)
+End MCDemo.
 
 Definition x := "x".
 Definition y := "y".
@@ -91,7 +97,7 @@ Proof. reflexivity. Qed.
 
 MetaCoq Unquote Definition coq_my_negb := (expr_to_tc Σ (indexify nil my_negb_syn)).
 
-Import MonadNotation.
+Import MCMonadNotation.
 
 Definition is_zero_syn :=
   [|
@@ -322,10 +328,11 @@ MetaCoq Unquote Inductive (global_to_tc Nat_syn).
 
 Import Template.Ast.
 
+Unset Primitive Projections.
+
 Definition State_syn :=
   [\ record "State" := "mkState" { "balance" : Nat ; "day" : Nat }  \].
 
 MetaCoq Unquote Inductive (global_to_tc State_syn).
 
-Check balance.
-Check day.
+Print State.

embedding/examples/FinMap.v

@@ -12,7 +12,7 @@ From ConCert.Embedding Require Import PCUICtoTemplate.
 From ConCert.Embedding Require Import EvalE.
 From ConCert.Embedding Require Import Utils.
 
-Import MonadNotation.
+Import MCMonadNotation.
 Import BaseTypes.
 Import StdLib.
 Open Scope list.

embedding/extraction/Liquidity.v

@@ -12,6 +12,10 @@ Import ListNotations.
 
 Open Scope string.
 
+Module TCString := bytestring.String.
+
+Coercion TCString.to_string : TCString.t  >-> string.
+
 (* Names for two mandatory argument for the main function. Used when generating code for [wrapper] and for the entry point *)
 Definition MSG_ARG := "msg".
 Definition STORAGE_ARG := "st".
@@ -46,15 +50,15 @@ Fixpoint liquidifyTy (TT : env string) (ty : type) : string :=
   | tyInd nm =>
     (* ignore module path on prining *)
     let (_, nm') := PCUICTranslate.kername_of_string nm in
-    Extras.with_default nm' (look TT nm)
+    TCString.to_string (Extras.with_default nm' (option_map TCString.of_string (look TT nm)))
   | tyForall x b => "forall " ++ "'" ++ x ++ liquidifyTy TT b
   (* is it a product? *)
   | tyApp ty1 ty2 =>
     match ty1 with
       | (tyApp (tyInd ty_nm) A) =>
         (* ignore module path on prining *)
         let (_, nm') := PCUICTranslate.kername_of_string ty_nm in
-        if nm' =? "prod" then
+        if TCString.to_string nm' =? "prod" then
           inParens (liquidifyTy TT A ++ " * " ++ liquidifyTy TT ty2)
         else inParens (liquidifyTy TT ty2 ++ " " ++ liquidifyTy TT ty1)
       | _ => inParens (liquidifyTy TT ty2 ++ " " ++ liquidifyTy TT ty1)
@@ -198,7 +202,7 @@ Definition liquidify (TT TTty : env string ) : expr -> string :=
   | eConst cst =>
     (* ignore module path *)
     let (_, cst') := PCUICTranslate.kername_of_string cst in
-    Extras.with_default cst' (look TT cst)
+    Extras.with_default cst' (option_map TCString.of_string (look TT cst))
   | eCase (ind,_) _ d bs =>
     match bs with
     | [b1;b2] => (* Handling if-then-else *)

embedding/extraction/PreludeExt.v

@@ -16,7 +16,7 @@ From Coq Require Import List.
 
 From MetaCoq.Template Require Import All.
 
-Import MonadNotation.
+Import MCMonadNotation.
 Import ListNotations.
 Import BaseTypes.
 Open Scope list.
@@ -152,9 +152,39 @@ Next Obligation.
   decide equality;apply Nat.eq_dec.
 Qed.
 Next Obligation.
-Admitted.
+  assert (cnat : countable.Countable (nat + nat)) by typeclasses eauto.
+  destruct cnat as [e d H].
+  unshelve econstructor.
+  * intros addr. destruct addr.
+    exact (e (inl n)).
+    exact (e (inr n)).
+  * intros i.
+    destruct (d i).
+    ** destruct s as [n | n].
+       exact (Some (ContractAddr_coq n)).
+       exact (Some (UserAddr_coq n)).
+    ** exact None.
+  * cbn;intros addr.
+    destruct addr;
+    now rewrite H.
+Defined.
 Next Obligation.
-Admitted.
+  assert (snat : Serializable.Serializable (nat + nat)) by typeclasses eauto.
+  destruct snat as [s d H].
+  unshelve econstructor.
+  * intros addr. destruct addr.
+    exact (s (inl n)).
+    exact (s (inr n)).
+  * intros i.
+    destruct (d i) as [v | ].
+    ** destruct v as [n | n].
+       exact (Some (ContractAddr_coq n)).
+       exact (Some (UserAddr_coq n)).
+    ** exact None.
+  * cbn;intros addr.
+    destruct addr;
+      now rewrite H.
+Defined.
 
 Definition init_wrapper {setup storage}
            (init : SimpleCallCtx -> setup -> storage)

embedding/extraction/SimpleBlockchainExt.v

@@ -11,7 +11,7 @@ From Coq Require Import List.
 
 From MetaCoq.Template Require Import All.
 
-Import MonadNotation.
+Import MCMonadNotation.
 Import ListNotations.
 Import BaseTypes.
 Open Scope list.

embedding/theories/Ast.v

@@ -26,9 +26,9 @@ Record pat := pConstr {pName : ename; pVars : list ename}.
 
 (** ** λsmart AST *)
 
-(** We have both named variables and de Bruijn indices.  Translation to Meta Coq requires indices, while named representation is what we might get from the integration API. We can define relations on type of expressions ensuring that either names are used, or indices, but not both at the same time. *)
+(** We have both named variables and de Bruijn indices. Translation to MetaCoq requires indices, while named representation is what we might get from the integration API. We can define relations on type of expressions ensuring that either names are used, or indices, but not both at the same time. *)
 
-(** Note also that AST must be explicitly annotated with types. This is required for the translation to Meta Coq. *)
+(** Note also that AST must be explicitly annotated with types. This is required for the translation to MetaCoq. *)
 Inductive expr : Set :=
 | eRel       : nat -> expr (* de Bruijn index *)
 | eVar       : ename -> expr (* named variables *)
@@ -141,7 +141,7 @@ Fixpoint lookup_global ( Σ : global_env) (key : ename) : option global_dec :=
   end.
 
 (** Looks up for the given inductive by name and if succeeds, returns a list of constructors with corresponding arities *)
-Definition resolve_inductive (Σ : global_env) (ind_name : BasicTC.ident)
+Definition resolve_inductive (Σ : global_env) (ind_name : ename)
   : option (nat * list constr) :=
   match (lookup_global Σ ind_name) with
   | Some (gdInd n nparam cs _) => Some (nparam, cs)
@@ -151,7 +151,7 @@ Definition resolve_inductive (Σ : global_env) (ind_name : BasicTC.ident)
 Definition remove_proj (c : constr) := map snd (snd c).
 
 (** Resolves the given constructor name to a corresponding position in the list of constructors along with the constructor's arity *)
-Definition resolve_constr (Σ : global_env) (ind_name constr_name : BasicTC.ident)
+Definition resolve_constr (Σ : global_env) (ind_name constr_name : ename)
   : option (nat * nat * list type)  :=
   match (resolve_inductive Σ ind_name) with
   | Some n_cs =>

embedding/theories/CertifyingTranslate.v

@@ -41,6 +41,8 @@ Definition my_negb_syn :=
           | True -> False
           | False -> True |].
 
+Compute expr_to_tc Σ (indexify nil my_negb_syn).
+
 (** We translate and unquote using the ConCert embedding feature *)
 MetaCoq Unquote Definition my_negb := (expr_to_tc Σ (indexify nil my_negb_syn)).