Commit 34d5980a authored by Jakob Botsch Nielsen's avatar Jakob Botsch Nielsen
Browse files

Minor cleanups and add .editorconfig

parent c9329d33
Pipeline #11089 passed with stage
in 4 minutes and 46 seconds
# editorconfig.org
# top-most EditorConfig file
root = true
[*]
insert_final_newline = true
indent_size = 2
indent_style = space
trim_trailing_whitespace = true
From Coq Require Import String.
From Coq Require OrderedTypeEx.
From SmartContracts Require Import Oak.
From SmartContracts Require Import Monads.
......@@ -72,45 +73,47 @@ Instance impl_interface : interface :=
todo: come back to this and understand universe polymorphism in depth. *)
Polymorphic Record ChainInterface :=
build_chain_interface {
ifc_chain_type : Type;
ifc_chain_at : ifc_chain_type -> BlockId -> option ifc_chain_type;
ifc_head_block : ifc_chain_type -> Block;
ifc_incoming_txs : ifc_chain_type -> Address -> list Tx;
ifc_outgoing_txs : ifc_chain_type -> Address -> list Tx;
ifc_contract_deployment : ifc_chain_type -> Address -> option ContractDeployment;
ifc_contract_state : ifc_chain_type -> Address -> option OakValue;
(* Would be nice to encapsulate ChainInterface somewhat here
and avoid these ugly prefixed names *)
ci_chain_type : Type;
ci_chain_at : ci_chain_type -> BlockId -> option ci_chain_type;
ci_head_block : ci_chain_type -> Block;
ci_incoming_txs : ci_chain_type -> Address -> list Tx;
ci_outgoing_txs : ci_chain_type -> Address -> list Tx;
ci_contract_deployment : ci_chain_type -> Address -> option ContractDeployment;
ci_contract_state : ci_chain_type -> Address -> option OakValue;
}.
Record Chain :=
build_chain {
chain_ifc : ChainInterface;
chain_val : ifc_chain_type chain_ifc
chain_ci : ChainInterface;
chain_val : chain_ci.(ci_chain_type);
}.
Definition chain_at (c : Chain) (bid : BlockId) : option Chain :=
do x <- c.(chain_ifc).(ifc_chain_at) c.(chain_val) bid;
do x <- c.(chain_ci).(ci_chain_at) c.(chain_val) bid;
Some {| chain_val := x |}.
Definition head_block (c : Chain) :=
c.(chain_ifc).(ifc_head_block) c.(chain_val).
c.(chain_ci).(ci_head_block) c.(chain_val).
Definition block_at (c : Chain) (bid : BlockId) : option Block :=
do c <- chain_at c bid; Some (head_block c).
Definition incoming_txs (c : Chain) :=
c.(chain_ifc).(ifc_incoming_txs) c.(chain_val).
c.(chain_ci).(ci_incoming_txs) c.(chain_val).
Definition outgoing_txs (c : Chain) :=
c.(chain_ifc).(ifc_outgoing_txs) c.(chain_val).
c.(chain_ci).(ci_outgoing_txs) c.(chain_val).
Definition contract_deployment (c : Chain) :=
c.(chain_ifc).(ifc_contract_deployment) c.(chain_val).
c.(chain_ci).(ci_contract_deployment) c.(chain_val).
Definition contract_state (c : Chain) :=
c.(chain_ifc).(ifc_contract_state) c.(chain_val).
c.(chain_ci).(ci_contract_state) c.(chain_val).
Inductive ContractCallContext :=
build_contract_call_ctx {
build_contract_call_ctx {
(* Chain *)
ctx_chain : Chain;
(* Address sending the funds *)
......@@ -119,12 +122,12 @@ build_contract_call_ctx {
ctx_contract_address : Address;
(* Amount of GTU passed in call *)
ctx_amount : Amount;
}.
}.
Inductive ChainAction :=
| act_transfer (to : Address) (amount : Amount)
| act_call (to : Address) (amount : Amount) (msg : OakValue)
| act_deploy
| act_transfer (to : Address) (amount : Amount)
| act_call (to : Address) (amount : Amount) (msg : OakValue)
| act_deploy
{setup_ty msg_ty state_ty : Type}
(version : Version)
(init : ContractCallContext -> setup_ty -> option state_ty)
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment