Commit ee50d5ed authored by Jakob Botsch Nielsen's avatar Jakob Botsch Nielsen
Browse files

Rename some things for technical report

parent 7c0f29b5
Pipeline #12352 failed with stage
in 1 minute and 31 seconds
...@@ -20,11 +20,12 @@ Definition Amount := Z. ...@@ -20,11 +20,12 @@ Definition Amount := Z.
Bind Scope Z_scope with Amount. Bind Scope Z_scope with Amount.
Class ChainBaseTypes := Class ChainBase :=
build_chain_base_types { build_chain_base {
Address : Type; Address : Type;
address_eqb : Address -> Address -> bool; address_eqb : Address -> Address -> bool;
address_eqb_spec : forall (a b : Address), Bool.reflect (a = b) (address_eqb a b); address_eqb_spec :
forall (a b : Address), Bool.reflect (a = b) (address_eqb a b);
address_eqdec :> stdpp.base.EqDecision Address; address_eqdec :> stdpp.base.EqDecision Address;
address_countable :> countable.Countable Address; address_countable :> countable.Countable Address;
address_ote :> OakTypeEquivalence Address; address_ote :> OakTypeEquivalence Address;
...@@ -48,7 +49,7 @@ Global Ltac destruct_address_eq := ...@@ -48,7 +49,7 @@ Global Ltac destruct_address_eq :=
end. end.
Section Blockchain. Section Blockchain.
Context {BaseTypes : ChainBaseTypes}. Context {BaseTypes : ChainBase}.
Lemma address_eq_refl x : Lemma address_eq_refl x :
address_eqb x x = true. address_eqb x x = true.
...@@ -66,12 +67,6 @@ Proof. destruct_address_eq; auto; congruence. Qed. ...@@ -66,12 +67,6 @@ Proof. destruct_address_eq; auto; congruence. Qed.
Record ContractDeployment := Record ContractDeployment :=
build_contract_deployment { build_contract_deployment {
deployment_version : Version; deployment_version : Version;
(* todo: model any type/constraints so we can have this. Right now the
problem is that Congress messages can contain _any_ oak value (for
the congress to send out), so there is no bijection from its message type
to oak type.
deployment_msg_ty : OakType;
deployment_state_ty : OakType; *)
deployment_setup : OakValue; deployment_setup : OakValue;
}. }.
...@@ -108,7 +103,7 @@ Record Chain := ...@@ -108,7 +103,7 @@ Record Chain :=
(* Two chains are said to be equivalent if they are extensionally equal. (* Two chains are said to be equivalent if they are extensionally equal.
We will later require that all deployed contracts respect this relation. We will later require that all deployed contracts respect this relation.
This equivalence is equality if univalence is assumed. *) This equivalence is equality if funext is assumed. *)
Record ChainEquiv (c1 c2 : Chain) : Prop := Record ChainEquiv (c1 c2 : Chain) : Prop :=
build_chain_equiv { build_chain_equiv {
header_eq : block_header c1 = block_header c2; header_eq : block_header c1 = block_header c2;
...@@ -206,24 +201,25 @@ where Address -> WeakContract would be some operation that the chain provides ...@@ -206,24 +201,25 @@ where Address -> WeakContract would be some operation that the chain provides
to allow access to contracts in deployments. to allow access to contracts in deployments.
*) *)
with WeakContract := with WeakContract :=
| build_weak_contract | build_weak_contract
(version : Version) (version : Version)
(init : Chain -> (init :
ContractCallContext -> Chain ->
OakValue -> ContractCallContext ->
option OakValue) OakValue (* setup *) ->
(* Init respects chain equivalence *) option OakValue)
(init_proper : (* Init respects chain equivalence *)
Proper (ChainEquiv ==> eq ==> eq ==> eq) init) (init_proper :
(receive : Proper (ChainEquiv ==> eq ==> eq ==> eq) init)
Chain -> (receive :
ContractCallContext -> Chain ->
OakValue (* state *) -> ContractCallContext ->
option OakValue (* message *) -> OakValue (* state *) ->
option (OakValue * list ActionBody)) option OakValue (* message *) ->
(* And so does receive *) option (OakValue * list ActionBody))
(receive_proper : (* And so does receive *)
Proper (ChainEquiv ==> eq ==> eq ==> eq ==> eq) receive). (receive_proper :
Proper (ChainEquiv ==> eq ==> eq ==> eq ==> eq) receive).
Definition wc_version (wc : WeakContract) : Version := Definition wc_version (wc : WeakContract) : Version :=
let (v, _, _, _, _) := wc in v. let (v, _, _, _, _) := wc in v.
...@@ -267,25 +263,25 @@ use and interact with when they want deployment. We keep the weak contract ...@@ -267,25 +263,25 @@ use and interact with when they want deployment. We keep the weak contract
only "internally" for blockchains, while any strongly-typed contract can only "internally" for blockchains, while any strongly-typed contract can
be converted to and from *) be converted to and from *)
Record Contract Record Contract
(setup_ty msg_ty state_ty : Type) (Setup Msg State : Type)
`{setup_eq : OakTypeEquivalence setup_ty} `{OakTypeEquivalence Setup}
`{msg_eq : OakTypeEquivalence msg_ty} `{OakTypeEquivalence Msg}
`{state_eq : OakTypeEquivalence state_ty} := `{OakTypeEquivalence State} :=
build_contract { build_contract {
version : Version; version : Version;
init : init :
Chain -> Chain ->
ContractCallContext -> ContractCallContext ->
setup_ty -> Setup ->
option state_ty; option State;
init_proper : init_proper :
Proper (ChainEquiv ==> eq ==> eq ==> eq) init; Proper (ChainEquiv ==> eq ==> eq ==> eq) init;
receive : receive :
Chain -> Chain ->
ContractCallContext -> ContractCallContext ->
state_ty -> State ->
option msg_ty -> option Msg ->
option (state_ty * list ActionBody); option (State * list ActionBody);
receive_proper : receive_proper :
Proper (ChainEquiv ==> eq ==> eq ==> eq ==> eq) receive; Proper (ChainEquiv ==> eq ==> eq ==> eq ==> eq) receive;
}. }.
...@@ -296,11 +292,11 @@ Arguments receive {_ _ _ _ _ _}. ...@@ -296,11 +292,11 @@ Arguments receive {_ _ _ _ _ _}.
Arguments build_contract {_ _ _ _ _ _}. Arguments build_contract {_ _ _ _ _ _}.
Program Definition contract_to_weak_contract Program Definition contract_to_weak_contract
{setup_ty msg_ty state_ty : Type} {Setup Msg State : Type}
`{setup_eq : OakTypeEquivalence setup_ty} `{OakTypeEquivalence Setup}
`{msg_eq : OakTypeEquivalence msg_ty} `{OakTypeEquivalence Msg}
`{state_eq : OakTypeEquivalence state_ty} `{OakTypeEquivalence State}
(c : Contract setup_ty msg_ty state_ty) : WeakContract := (c : Contract Setup Msg State) : WeakContract :=
let weak_init chain ctx oak_setup := let weak_init chain ctx oak_setup :=
do setup <- deserialize oak_setup; do setup <- deserialize oak_setup;
do state <- c.(init) chain ctx setup; do state <- c.(init) chain ctx setup;
...@@ -343,33 +339,33 @@ Coercion contract_to_weak_contract : Contract >-> WeakContract. ...@@ -343,33 +339,33 @@ Coercion contract_to_weak_contract : Contract >-> WeakContract.
(* Deploy a strongly typed contract with some amount and setup *) (* Deploy a strongly typed contract with some amount and setup *)
Definition create_deployment Definition create_deployment
{setup_ty msg_ty state_ty : Type} {Setup Msg State : Type}
`{OakTypeEquivalence setup_ty} `{OakTypeEquivalence Setup}
`{OakTypeEquivalence msg_ty} `{OakTypeEquivalence Msg}
`{OakTypeEquivalence state_ty} `{OakTypeEquivalence State}
(amount : Amount) (amount : Amount)
(contract : Contract setup_ty msg_ty state_ty) (contract : Contract Setup Msg State)
(setup : setup_ty) : ActionBody := (setup : Setup) : ActionBody :=
act_deploy amount contract (serialize setup). act_deploy amount contract (serialize setup).
(* The contract interface is the main mechanism allowing a deployed (* The contract interface is the main mechanism allowing a deployed
contract to interact with another deployed contract. This hides contract to interact with another deployed contract. This hides
the ugly details of everything being OakValue away from contracts. *) the ugly details of everything being OakValue away from contracts. *)
Record ContractInterface {setup_ty msg_ty state_ty : Type} := Record ContractInterface {Setup Msg State : Type} :=
build_contract_interface { build_contract_interface {
(* The address of the contract being interfaced with *) (* The address of the contract being interfaced with *)
contract_address : Address; contract_address : Address;
(* Version of the contract *) (* Version of the contract *)
contract_version : Version; contract_version : Version;
(* The setup that was passed when the contract was deployed *) (* The setup that was passed when the contract was deployed *)
contract_setup : setup_ty; contract_setup : Setup;
(* Obtain the state at some point of time *) (* Obtain the state at some point of time *)
get_state : Chain -> option state_ty; get_state : Chain -> option State;
(* Make an action transferring money to the contract without (* Make an action transferring money to the contract without
a message *) a message *)
transfer : Amount -> ActionBody; transfer : Amount -> ActionBody;
(* Make an action calling the contract *) (* Make an action calling the contract *)
call : Amount -> msg_ty -> ActionBody; call : Amount -> Msg -> ActionBody;
}. }.
Arguments ContractInterface _ _ _ : clear implicits. Arguments ContractInterface _ _ _ : clear implicits.
...@@ -377,14 +373,14 @@ Arguments ContractInterface _ _ _ : clear implicits. ...@@ -377,14 +373,14 @@ Arguments ContractInterface _ _ _ : clear implicits.
Definition get_contract_interface Definition get_contract_interface
(chain : Chain) (chain : Chain)
(addr : Address) (addr : Address)
(setup_ty msg_ty state_ty : Type) (Setup Msg State : Type)
`{OakTypeEquivalence setup_ty} `{OakTypeEquivalence Setup}
`{OakTypeEquivalence msg_ty} `{OakTypeEquivalence Msg}
`{OakTypeEquivalence state_ty} `{OakTypeEquivalence State}
: option (ContractInterface setup_ty msg_ty state_ty) := : option (ContractInterface Setup Msg State) :=
do 'build_contract_deployment ver ov_setup <- contract_deployment chain addr; do 'build_contract_deployment ver ov_setup <- contract_deployment chain addr;
do setup <- deserialize ov_setup; do setup <- deserialize ov_setup;
let ifc_get_state chain := deserialize =<< (contract_state chain addr) in let ifc_get_state chain := contract_state chain addr >>= deserialize in
let ifc_transfer := act_transfer addr in let ifc_transfer := act_transfer addr in
let ifc_call amount msg := act_call addr amount (serialize msg) in let ifc_call amount msg := act_call addr amount (serialize msg) in
Some {| contract_address := addr; Some {| contract_address := addr;
...@@ -722,28 +718,28 @@ Record ChainState := ...@@ -722,28 +718,28 @@ Record ChainState :=
}. }.
Inductive ChainEvent : ChainState -> ChainState -> Type := Inductive ChainEvent : ChainState -> ChainState -> Type :=
| evt_block : | evt_block :
forall {prev : ChainState} forall {prev : ChainState}
{header : BlockHeader} {header : BlockHeader}
{baker : Address} {baker : Address}
{next : ChainState}, {next : ChainState},
chain_state_queue prev = [] -> chain_state_queue prev = [] ->
IsValidNextBlock header (block_header prev) -> IsValidNextBlock header (block_header prev) ->
Forall ActIsFromAccount (chain_state_queue next) -> Forall ActIsFromAccount (chain_state_queue next) ->
EnvironmentEquiv EnvironmentEquiv
next next
(add_new_block_header header baker prev) -> (add_new_block_header header baker prev) ->
ChainEvent prev next ChainEvent prev next
| evt_step : | evt_step :
forall {prev : ChainState} forall {prev : ChainState}
{act : Action} {act : Action}
{acts : list Action} {acts : list Action}
{next : ChainState} {next : ChainState}
{new_acts : list Action}, {new_acts : list Action},
chain_state_queue prev = act :: acts -> chain_state_queue prev = act :: acts ->
ChainStep prev act next new_acts -> ChainStep prev act next new_acts ->
chain_state_queue next = new_acts ++ acts -> chain_state_queue next = new_acts ++ acts ->
ChainEvent prev next ChainEvent prev next
| evt_permute : | evt_permute :
forall {prev new : ChainState}, forall {prev new : ChainState},
chain_state_env prev = chain_state_env new -> chain_state_env prev = chain_state_env new ->
...@@ -936,7 +932,7 @@ Class ChainBuilderType := ...@@ -936,7 +932,7 @@ Class ChainBuilderType :=
(finalized_height : nat) : (finalized_height : nat) :
option builder_type; option builder_type;
builder_trace (b : builder_type) : builder_reachable (b : builder_type) :
reachable (build_chain_state (builder_env b) []); reachable (build_chain_state (builder_env b) []);
}. }.
......
...@@ -6,12 +6,12 @@ also a snoc list. Note that this is not unlike fhlist from CPDT, ...@@ -6,12 +6,12 @@ also a snoc list. Note that this is not unlike fhlist from CPDT,
except we place further restrictions on it. *) except we place further restrictions on it. *)
From SmartContracts Require Import Automation. From SmartContracts Require Import Automation.
Section ChainedList. Section ChainedList.
Context {point : Type} {link : point -> point -> Type}. Context {Point : Type} {Link : Point -> Point -> Type}.
Inductive ChainedList : point -> point -> Type := Inductive ChainedList : Point -> Point -> Type :=
| clnil : forall {elm}, ChainedList elm elm | clnil : forall {p}, ChainedList p p
| snoc : forall {from mid to}, | snoc : forall {from mid to},
ChainedList from mid -> link mid to -> ChainedList from to. ChainedList from mid -> Link mid to -> ChainedList from to.
Fixpoint clist_app Fixpoint clist_app
{from mid to} {from mid to}
......
...@@ -8,7 +8,7 @@ From RecordUpdate Require Import RecordSet. ...@@ -8,7 +8,7 @@ From RecordUpdate Require Import RecordSet.
Import ListNotations. Import ListNotations.
Section Circulation. Section Circulation.
Context {ChainBaseTypes : ChainBaseTypes}. Context {ChainBase : ChainBase}.
Context `{Finite Address}. Context `{Finite Address}.
Definition circulation (chain : Chain) := Definition circulation (chain : Chain) :=
......
...@@ -16,7 +16,7 @@ Import ListNotations. ...@@ -16,7 +16,7 @@ Import ListNotations.
Import RecordSetNotations. Import RecordSetNotations.
Section Congress. Section Congress.
Context {BaseTypes : ChainBaseTypes}. Context {BaseTypes : ChainBase}.
Local Open Scope Z. Local Open Scope Z.
Set Primitive Projections. Set Primitive Projections.
...@@ -890,7 +890,7 @@ Corollary congress_txs_after_block ...@@ -890,7 +890,7 @@ Corollary congress_txs_after_block
length (outgoing_txs new addr) <= num_acts_created_in_proposals new addr. length (outgoing_txs new addr) <= num_acts_created_in_proposals new addr.
Proof. Proof.
intros add_block contract congress_at_addr. intros add_block contract congress_at_addr.
pose proof (congress_txs_well_behaved _ _ (builder_trace new) congress_at_addr). pose proof (congress_txs_well_behaved _ _ (builder_reachable new) congress_at_addr).
cbn in *. cbn in *.
lia. lia.
Qed. Qed.
......
...@@ -24,7 +24,7 @@ Local Open Scope bool. ...@@ -24,7 +24,7 @@ Local Open Scope bool.
Definition AddrSize : N := 2^128. Definition AddrSize : N := 2^128.
Definition ContractAddrBase : N := AddrSize / 2. Definition ContractAddrBase : N := AddrSize / 2.
Global Instance LocalChainBaseTypes : ChainBaseTypes := Global Instance LocalChainBase : ChainBase :=
{| Address := BoundedN AddrSize; {| Address := BoundedN AddrSize;
address_eqb := BoundedN.eqb; address_eqb := BoundedN.eqb;
address_eqb_spec := BoundedN.eqb_spec; address_eqb_spec := BoundedN.eqb_spec;
...@@ -511,12 +511,12 @@ Global Instance LocalChainBuilderDepthFirst : ChainBuilderType := ...@@ -511,12 +511,12 @@ Global Instance LocalChainBuilderDepthFirst : ChainBuilderType :=
builder_initial := lcb_initial; builder_initial := lcb_initial;
builder_env lcb := lcb_lc lcb; builder_env lcb := lcb_lc lcb;
builder_add_block := add_block true; builder_add_block := add_block true;
builder_trace := lcb_trace; |}. builder_reachable := lcb_trace; |}.
Definition LocalChainBuilderBreadthFirst : ChainBuilderType := Definition LocalChainBuilderBreadthFirst : ChainBuilderType :=
{| builder_type := LocalChainBuilder; {| builder_type := LocalChainBuilder;
builder_initial := lcb_initial; builder_initial := lcb_initial;
builder_env lcb := lcb_lc lcb; builder_env lcb := lcb_lc lcb;
builder_add_block := add_block false; builder_add_block := add_block false;
builder_trace := lcb_trace; |}. builder_reachable := lcb_trace; |}.
End LocalBlockchain. End LocalBlockchain.
Markdown is supported
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