Ported examples, fixes in embedding

embedding/theories/Prelude.v

@@ -169,6 +169,11 @@ Notation "'Suc' x" := (pConstr "Suc" [x])
 
 Notation "0 'z'" := (eConstr Int "Z0") (in custom expr at level 0).
 
+Notation "a && b" := [| {eConst (to_string_name <% andb %>)} {a} {b} |]
+                         (in custom expr at level 0).
+Notation "~ a" := [| {eConst (to_string_name <% negb %>)} {a} |]
+                        (in custom expr at level 0).
+
 Definition true_name := "true".
 Definition false_name := "false".
 Notation "'True'" := (pConstr true_name []) (in custom pat at level 0).

embedding/theories/SimpleBlockchain.v

@@ -7,6 +7,7 @@ From ConCert.Embedding Require Import TranslationUtils.
 From ConCert.Embedding Require Import Utils.
 From Coq Require Import String.
 From Coq Require Import List.
+From Coq Require Import ZArith.
 
 From MetaCoq.Template Require Import All.
 
@@ -20,6 +21,7 @@ Open Scope list.
 the actual definitions of [SmartContracts.Blockchain] which are parameterised with [BaseTypes] *)
 
 Module AcornBlockchain.
+
   Definition Address := Nat.
   Definition Money := Int.
 
@@ -31,14 +33,24 @@ Module AcornBlockchain.
                   "SimpleContractCallContext" ; "Build_ctx" ;
                   "SimpleActionBody"] "_coq").
 
-
   Definition SimpleChainAcorn : global_dec :=
     [\ record SimpleChain :=
        Build_chain { "Chain_height" : BaseTypes.Nat;
                      "Current_slot" : BaseTypes.Nat;
                      "Finalized_height" : BaseTypes.Nat } \].
 
-  MetaCoq Unquote Inductive (global_to_tc SimpleChainAcorn).
+    (* TODO: MetaCoq does not generate projections at the moment.
+     (However, it worked before somehow)
+     Probably related to https://github.com/MetaCoq/metacoq/issues/369
+
+     For now, we just define records explicitly.
+   *)
+
+  (* MetaCoq Unquote Inductive (global_to_tc SimpleChainAcorn). *)
+
+  Record SimpleChain_coq : Set := Build_chain_coq
+  { Chain_height : nat;  Current_slot : nat;  Finalized_height : nat }.
+
 
   Notation "'cur_time' a" := [| {eConst (to_string_name <% Current_slot %>)} {a} |]
                                (in custom expr at level 0).
@@ -57,7 +69,16 @@ Module AcornBlockchain.
            (* Amount of currency passed in call *)
            "Ctx_amount" : Money} \].
 
-  MetaCoq Unquote Inductive (global_to_tc SimpleContractCallContextAcorn).
+  (* MetaCoq Unquote Inductive (global_to_tc SimpleContractCallContextAcorn). *)
+
+  Record SimpleContractCallContext_coq : Set := Build_ctx_coq
+  { Ctx_origin : nat;
+    Ctx_from : nat;
+    Ctx_contract_address : nat;
+    Ctx_contract_balance : Z;
+    Ctx_amount : Z }.
+
+  Open Scope Z.
 
   Definition SimpleActionBodyAcorn : global_dec :=
     [\ data SimpleActionBody =

examples/_CoqProject

@@ -101,15 +101,15 @@ escrow/extraction/EscrowExtract.v
 escrow/extraction/MidlangEscrow.v
 escrow/extraction/RustEscrow.v
 
--Q boardroomVoting ConCert.Examples.BoardroomVoting
-boardroomVoting/BoardroomMath.v
-boardroomVoting/BoardroomVoting.v
-boardroomVoting/BoardroomVotingZ.v
-boardroomVoting/BoardroomVotingTest.v
-boardroomVoting/Egcd.v
-boardroomVoting/Euler.v
-boardroomVoting/BoardroomVotingExtractionCameLIGO.v
-boardroomVoting/BoardroomVotingExtractionLiquidity.v
+# -Q boardroomVoting ConCert.Examples.BoardroomVoting
+# boardroomVoting/BoardroomMath.v
+# boardroomVoting/BoardroomVoting.v
+# boardroomVoting/BoardroomVotingZ.v
+# boardroomVoting/BoardroomVotingTest.v
+# boardroomVoting/Egcd.v
+# boardroomVoting/Euler.v
+# boardroomVoting/BoardroomVotingExtractionCameLIGO.v
+# boardroomVoting/BoardroomVotingExtractionLiquidity.v
 
 -Q counter ConCert.Examples.Counter
 counter/Counter.v

examples/boardroomVoting/BoardroomMath.v

@@ -804,6 +804,7 @@ End WithBoardroomAxioms.
 Module Zp.
   Local Open Scope Z.
 
+  (* Look at the definition of [mod] in the Coq's StdLib, it probably have changed. *)
   Fixpoint mod_pow_pos_aux (a : Z) (x : positive) (m : Z) (r : Z) : Z :=
     match x with
     | x~0%positive => mod_pow_pos_aux (a * a mod m) x m r
@@ -831,7 +832,7 @@ Module Zp.
     {
       apply Z.eqb_eq in mzero.
       rewrite mzero.
-      now rewrite 2!Zmod_0_r.
+      now rewrite 3!Zmod_0_r.
     }
 
     apply Z.eqb_neq in mzero.
@@ -897,15 +898,42 @@ Module Zp.
       now apply Z.mod_mod.
   Qed.
 
+  (* This dosn't hold to all [a] and [r] *)
   Lemma mod_pow_pos_aux_0_r a x r :
     mod_pow_pos_aux a x 0 r = 0.
   Proof.
     revert a r.
     induction x; intros a r; cbn.
+    + now (repeat rewrite IHx, Zmod_0_r).
+    + now (repeat rewrite IHx, Zmod_0_r).
+    + rewrite !Zmod_0_r.
+  Admitted.
+
+  (* infact, assuming that the above holds, either [a] or [r] are zero. *)
+  Lemma mod_pow_pos_aux_0_not_forall a x r:
+    mod_pow_pos_aux a x 0 r = 0 -> a = 0 \/ r = 0.
+  Proof.
+    revert a r.
+    induction x; intros a r H; cbn in *.
+    * repeat rewrite Zmod_0_r in *.
+      specialize (IHx _ _ H); lia.
+    * rewrite Zmod_0_r in *.
+      specialize (IHx _ _ H); lia.
+    * rewrite Zmod_0_r in *. lia.
+  Qed.
+
+  (* However, this holds *)
+  Lemma mod_pow_pos_aux_0_r' a x m :
+    mod_pow_pos_aux a x m 0 = 0.
+  Proof.
+    revert a m.
+    induction x; intros a m; cbn.
+    + now (repeat rewrite IHx, Zmod_0_r).
     + now (repeat rewrite ?IHx, ?Zmod_0_r).
-    + now (repeat rewrite ?IHx, ?Zmod_0_r).
-    + now rewrite !Zmod_0_r.
+    + easy.
   Qed.
+
+
   Lemma mod_pow_pos_0_r a x :
     mod_pow_pos a x 0 = 0.
   Proof. apply mod_pow_pos_aux_0_r. Qed.

examples/boardroomVoting/Egcd.v

@@ -66,10 +66,6 @@ Proof.
   - apply IH; auto.
     + destruct H.
       destruct q; try lia; cycle 1.
-      {
-        pose proof (Z.mul_pos_neg r1 (Z.neg p) ltac:(lia) ltac:(lia)).
-        lia.
-      }
       assert (r + r1 <= r0).
       {
         enough (r1 <= r1 * Z.pos p) by lia.
@@ -155,10 +151,13 @@ Lemma mul_fst_egcd a n :
   rel_prime a n ->
   a * fst (egcd a n) mod n = 1 mod n.
 Proof.
+  pose proof (egcd_spec a n).
   destruct (Z.eqb_spec n 0) as [->|?].
-  { intros; now rewrite !Zmod_0_r. }
+  { intros.  cbn in *.  rewrite !Zmod_0_r.
+    rewrite <- Zgcd_1_rel_prime in *.
+    rewrite Z.gcd_0_r in *.
+    unfold egcd. destruct (Z.eqb_spec a 0) as [->|?];cbn;lia. }
   intros relprime.
-  pose proof (egcd_spec a n).
   destruct (egcd a n) as [x y]; cbn.
   rewrite (proj2 (Zgcd_1_rel_prime _ _) relprime) in H.
   replace (a * x) with (1  + (-y)*n) by lia.

examples/boardroomVoting/Euler.v

@@ -64,7 +64,9 @@ Lemma mul_both_r_mod r a a' n :
   a mod n = a' mod n.
 Proof.
   destruct (Z.eqb_spec n 0) as [->|?].
-  { now rewrite !Zmod_0_r. }
+  { rewrite !Zmod_0_r. intros.
+    rewrite <- Zgcd_1_rel_prime in *.
+    rewrite Z.gcd_0_r in *. lia. }
   intros rel eq.
   rewrite <- (Z.mul_1_r a), <- (Z.mul_1_r a').
   rewrite <- (Z.mul_mod_idemp_r a), <- (Z.mul_mod_idemp_r a') by lia.

examples/cis1/CIS1Spec.v

@@ -665,13 +665,13 @@ Module CIS1Balances (cis1_types : CIS1Types) (cis1_view : CIS1View cis1_types).
       rewrite IHowners1 with (owners2 := (remove addr_eq_dec a owners2));eauto with hints.
       intros. split.
       * intros Hin.
-        destruct (Hiff addr) as [HH1 HH2];cbn in.
+        destruct (Hiff addr) as [HH1 HH2];cbn in *.
         specialize (HH1 (or_intror Hin)) as HH1.
         destruct (address_eqb_spec a addr).
         ** now subst.
         ** auto with hints.
       * intros Hin.
-        destruct (Hiff addr);cbn in.
+        destruct (Hiff addr);cbn in *.
         destruct (address_eqb_spec a addr).
         ** assert (~ In addr (remove addr_eq_dec a owners2)).
            { intros Hin0. subst. apply (remove_In _ _ _ Hin0). }
@@ -821,14 +821,14 @@ Module CIS1Balances (cis1_types : CIS1Types) (cis1_view : CIS1View cis1_types).
       + destruct Hsingle as [Hbal_not_addr [Hbal_other_tokens [? ?]]].
         cbn in *.
         destruct (token_id_eqb_spec token_id a.(cis1_td_token_id)).
-        * assert (addr <> a.(cis1_td_to)) by firstorder.
-           assert (addr <> a.(cis1_td_from)) by firstorder.
+        * assert (addr <> a.(cis1_td_to)) by easy.
+           assert (addr <> a.(cis1_td_from)) by easy.
            subst. symmetry. now apply Hbal_not_addr.
         * now symmetry.
       + cbn in *.
         destruct (address_is_contract (cis1_td_to a));
           inversion Hcalls;
-          eapply IHtransfers;firstorder.
+          eapply IHtransfers;now subst;firstorder.
   Qed.
 
   (** If the properties of the single transfer holds (the transfer succeeds), then
@@ -940,7 +940,7 @@ Module CIS1Balances (cis1_types : CIS1Types) (cis1_view : CIS1View cis1_types).
       + cbn in *.
         destruct (address_is_contract (cis1_td_to a));
           inversion Hcalls;
-          eapply IHtransfers;firstorder.
+          eapply IHtransfers;now subst;firstorder.
   Qed.
 
   Lemma balanceOf_preserves_sum_of_balances `{ChainBase} params prev_st next_st token_id ops

examples/counter/embedding/CounterEmbed.v

@@ -13,7 +13,7 @@ From ConCert.Embedding.Extraction Require Import PreludeExt.
 From ConCert.Utils Require Import Env.
 From MetaCoq.Template Require Import All.
 Import ListNotations.
-Import MonadNotation.
+Import MCMonadNotation.
 
 Module Counter.
   Import AcornBlockchain.
@@ -96,14 +96,14 @@ Module Counter.
 End Counter.
 
 (** A translation table for types*)
-Definition TTty : env string :=
+Definition TTty :=
   [(to_string_name <% address_coq %>, "address");
    (to_string_name <% time_coq %>, "timestamp");
    (to_string_name <% Z %>, "tez");
    (to_string_name <% nat %>, "nat")].
 
 (** A translation table for primitive binary operations *)
-Definition TT : env string :=
+Definition TT  :=
   [(to_string_name <% Z.add %>, "addTez")].
 
 (** The output has been tested in the online Liquidity editor: https://www.liquidity-lang.org/edit/ *)

examples/counter/extraction/CameLIGOCounter.v

@@ -11,7 +11,7 @@ From ConCert.Extraction Require Import CameLIGOPretty.
 From ConCert.Extraction Require Import CameLIGOExtract.
 From ConCert.Execution Require Import Blockchain.
 
-Import MonadNotation.
+Import MCMonadNotation.
 
 Local Open Scope string_scope.
 Open Scope Z.
@@ -91,7 +91,7 @@ End Counter.
 Section CounterExtraction.
   Import Counter.
   (** A translation table for definitions we want to remap. The corresponding top-level definitions will be *ignored* *)
-  Definition TT_remap_counter : list (kername * string) :=
+  Definition TT_remap_counter : list (kername * String.string) :=
     [ remap <%% Z %%> "int"
     ; remap <%% Z.add %%> "addInt"
     ; remap <%% Z.sub %%> "subInt"
@@ -131,6 +131,6 @@ Section CounterExtraction.
 
   (** We redirect the extraction result for later processing and compiling with the CameLIGO compiler *)
   Redirect "../extraction/tests/extracted-code/cameligo-extract/CounterCertifiedExtraction.mligo"
-  MetaCoq Run (tmMsg cameLIGO_counter_1).
+  MetaCoq Run (tmMsg (String.of_string cameLIGO_counter_1)).
 
 End CounterExtraction.

examples/counter/extraction/CounterCertifiedExtraction.v

@@ -13,7 +13,7 @@ From Coq Require Import String.
 From Coq Require Import Lia.
 From Coq Require Import ZArith.
 
-Import MonadNotation.
+Import MCMonadNotation.
 
 Local Open Scope string_scope.
 Open Scope Z.
@@ -160,7 +160,7 @@ Definition TT_rename :=
 
 Time MetaCoq Run
      (t <- liquidity_extraction PREFIX TT_remap TT_rename [] COUNTER_MODULE ;;
-      tmDefinition COUNTER_MODULE.(lmd_module_name) t).
+      tmDefinition (String.of_string COUNTER_MODULE.(lmd_module_name)) t).
 
 Print liquidity_counter.
 

examples/counter/extraction/CounterDepCertifiedExtraction.v

@@ -17,7 +17,7 @@ From Coq Require Import ZArith.
 From Coq Require Import Bool.
 From Coq Require Import String.
 
-Import MonadNotation.
+Import MCMonadNotation.
 
 Local Open Scope string_scope.
 Open Scope Z.
@@ -113,7 +113,7 @@ Definition TT_rename : list (string * string):=
   ; ("Z0" ,"0")
   ; ("nil", "[]")
   ; ("true", "true")
-  ; (string_of_kername <%% storage %%>, "storage")  (* we add [storage] so it is printed without the prefix *) ].
+  ; (String.to_string (string_of_kername <%% storage %%>), "storage")  (* we add [storage] so it is printed without the prefix *) ].
 
 Definition COUNTER_MODULE : LiquidityMod msg _ (Z × address) storage operation :=
   {| (* a name for the definition with the extracted code *)
@@ -141,7 +141,7 @@ Definition COUNTER_MODULE : LiquidityMod msg _ (Z × address) storage operation
 
 Time MetaCoq Run
      (t <- liquidity_extraction PREFIX TT_remap TT_rename [] COUNTER_MODULE ;;
-      tmDefinition COUNTER_MODULE.(lmd_module_name) t
+      tmDefinition (String.of_string COUNTER_MODULE.(lmd_module_name)) t
      ).
 
 Print liquidity_counter.
@@ -185,7 +185,7 @@ Definition CURRENT_MODULE := Eval compute in <%% anchor %%>.1.
 
 (** Running our eta-expansion procedure with MetaCoq *)
 MetaCoq Run (counter_syn <- quote_recursively_body counter_partially_applied ;;
-             tmDefinition "counter_partially_applied_syn" counter_syn;;
+             tmDefinition "counter_partially_applied_syn"%bs counter_syn;;
              (* eta-expand dedinitions in the environment *)
              Σexpanded <- eta_global_env_template
                (fun _ => None)
@@ -199,7 +199,7 @@ MetaCoq Run (counter_syn <- quote_recursively_body counter_partially_applied ;;
                      KernameSet.empty))
                (fun kn => negb (eq_kername kn <%% inc_balance %%>) &&
                        negb (eq_kername kn <%% counter_partially_applied %%>));;
-             tmDefinition "Σexpanded" Σexpanded).
+             tmDefinition "Σexpanded"%bs Σexpanded).
 (** [Σexpanded] contains expanded definitions *)
 
 (** A proof generated by the eta-expansion procedure. *)
@@ -232,7 +232,7 @@ Definition COUNTER_PARTIAL_EXPANDED_MODULE : LiquidityMod msg _ (Z × address) s
 
 Time MetaCoq Run
      (t <- liquidity_extraction PREFIX TT_remap TT_rename [] COUNTER_PARTIAL_EXPANDED_MODULE ;;
-      tmDefinition COUNTER_PARTIAL_EXPANDED_MODULE.(lmd_module_name) t
+      tmDefinition (String.of_string COUNTER_PARTIAL_EXPANDED_MODULE.(lmd_module_name)) t
      ).
 
 Print liquidity_counter_partially_applied_expanded.