Contents:
Library ConCert.Embedding.Extraction.SimpleBlockchainExt
(* 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 ConCert.Embedding.Extraction Require Import PreludeExt.
From Stdlib Require Import String.
From Stdlib Require Import List.
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 ConCert.Embedding.Extraction Require Import PreludeExt.
From Stdlib Require Import String.
From Stdlib Require Import List.
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 := address.
Definition Money := money.
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 } \].
MetaRocq Unquote Inductive (global_to_tc SimpleChainAcorn).
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 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).
Definition SimpleActionBodyAcorn : global_dec :=
[\ data SimpleActionBody =
"Act_transfer" [Address, Money,_] \].
MetaRocq Unquote Inductive (global_to_tc SimpleActionBodyAcorn).
Definition SActionBody := (to_string_name <% SimpleActionBody_rocq %>).
End AcornBlockchain.