Contents:
Library ConCert.Embedding.SimpleBlockchain
(* We develop some blockchain infrastructure relevant for the contract execution. *)
From ConCert.Embedding Require Import Ast.
From ConCert.Embedding Require Import Notations.
From ConCert.Embedding Require Import PCUICTranslate.
From ConCert.Embedding Require Import TranslationUtils.
From ConCert.Embedding Require Import Utils.
From Stdlib Require Import String.
From Stdlib Require Import List.
From Stdlib Require Import ZArith.
From MetaRocq.Template Require Import All.
Import MRMonadNotation.
Import ListNotations.
Import BaseTypes.
Open Scope list.
From ConCert.Embedding Require Import Ast.
From ConCert.Embedding Require Import Notations.
From ConCert.Embedding Require Import PCUICTranslate.
From ConCert.Embedding Require Import TranslationUtils.
From ConCert.Embedding Require Import Utils.
From Stdlib Require Import String.
From Stdlib Require Import List.
From Stdlib Require Import ZArith.
From MetaRocq.Template Require Import All.
Import MRMonadNotation.
Import ListNotations.
Import BaseTypes.
Open Scope list.
We create a simply-typed records and data types corresponding for
the actual definitions of SmartContracts.Blockchain which are parameterized with BaseTypes
Module AcornBlockchain.
Definition Address := Nat.
Definition Money := Int.
MetaRocq Run
(mp_ <- tmCurrentModPath tt ;;
let mp := (Utils.string_of_modpath mp_ ++ "@")%string in
mkNames mp
["SimpleChain" ; "Build_chain";
"SimpleContractCallContext" ; "Build_ctx" ;
"SimpleActionBody"] "_rocq").
Definition SimpleChainAcorn : global_dec :=
[\ record SimpleChain :=
Build_chain { "Chain_height" : BaseTypes.Nat;
"Current_slot" : BaseTypes.Nat;
"Finalized_height" : BaseTypes.Nat } \].
(* TODO: MetaRocq does not generate projections at the moment.
(However, it worked before somehow)
Probably related to https://github.com/MetaRocq/metarocq/issues/369
For now, we just define records explicitly.
*)
(* MetaRocq Unquote Inductive (global_to_tc SimpleChainAcorn). *)
Record SimpleChain_rocq : Set := Build_chain_rocq
{ 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).
Definition SimpleContractCallContextAcorn : global_dec :=
[\ record SimpleContractCallContext :=
Build_ctx {
(* Address initiating the transaction *)
"Ctx_origin" : Address;
(* Address sending the funds *)
"Ctx_from" : Address;
(* Address of the contract being called *)
"Ctx_contract_address" : Address;
"Ctx_contract_balance" : Money;
(* Amount of currency passed in call *)
"Ctx_amount" : Money} \].
(* MetaRocq Unquote Inductive (global_to_tc SimpleContractCallContextAcorn). *)
Record SimpleContractCallContext_rocq : Set := Build_ctx_rocq
{ 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 =
"Act_transfer" [Address, Money,_] \].
MetaRocq Unquote Inductive (global_to_tc SimpleActionBodyAcorn).
Notation SActionBody := (to_string_name <% SimpleActionBody_rocq %>).
End AcornBlockchain.