Commit 56054f6d authored by Jakob Botsch Nielsen's avatar Jakob Botsch Nielsen

Add address_is_contract function

This requires that implementations have a way to determine whether an
address belongs to a contract simply from its value (i.e. from the
format of the address). This is a reasonable expectation and will also
allow contracts to be able to determine whether code will be executed
from actions. Finally, it will also simplify some checks.
parent c04a6e9e
Pipeline #12091 passed with stage
in 5 minutes and 12 seconds
......@@ -27,13 +27,13 @@ Class ChainBaseTypes :=
address_eqdec :> stdpp.base.EqDecision Address;
address_countable :> countable.Countable Address;
address_ote :> OakTypeEquivalence Address;
address_is_contract : Address -> bool;
compute_block_reward : nat -> Amount;
}.
Global Opaque Address address_eqb address_eqb_spec
address_eqdec address_countable
address_ote
compute_block_reward.
address_ote compute_block_reward.
Delimit Scope address_scope with address.
Bind Scope address_scope with Address.
......@@ -451,7 +451,7 @@ Inductive ChainStep :
(from to : Address)
(amount : Amount),
amount <= account_balance pre from ->
env_contracts pre to = None ->
address_is_contract to = false ->
act = build_act from (act_transfer to amount) ->
tx = build_tx from to amount tx_empty ->
EnvironmentEquiv new_env (add_tx tx pre) ->
......@@ -469,6 +469,7 @@ Inductive ChainStep :
amount <= account_balance pre from ->
env_contracts pre to = None ->
incoming_txs pre to = [] ->
address_is_contract to = true ->
act = build_act from (act_deploy amount wc setup) ->
tx = build_tx from to amount (tx_deploy (build_contract_deployment (wc_version wc) setup)) ->
wc_init
......@@ -645,8 +646,22 @@ Definition IsValidNextBlock (new old : BlockHeader) : Prop :=
finalized_height new >= finalized_height old /\
finalized_height new < block_height new.
Definition initial_env :=
{| env_chain :=
{| block_header :=
{| block_height := 0;
slot_number := 0;
finalized_height := 0; |};
incoming_txs a := [];
outgoing_txs a := [];
blocks_baked a := [];
contract_state a := None; |};
env_contracts a := None; |}.
Inductive ChainTrace : Environment -> Environment -> Prop :=
| ctrace_refl : forall (env : Environment),
| ctrace_initial :
forall (env : Environment),
EnvironmentEquiv env initial_env ->
ChainTrace env env
| ctrace_block :
forall (prev_start prev_end : Environment)
......@@ -657,9 +672,6 @@ Inductive ChainTrace : Environment -> Environment -> Prop :=
ChainTrace prev_start prev_end ->
IsValidNextBlock header (block_header prev_end) ->
BlockTrace block_start acts new_end [] ->
(* todo: probably unnecessary as we should have *)
(* BlockTrace a acts b acts' -> EnvironmentEquiv a a' -> *)
(* BlockTrace a' acts b acts' *)
EnvironmentEquiv
block_start
(add_new_block header baker prev_end) ->
......@@ -671,11 +683,11 @@ Context {pre post : Environment} (trace : ChainTrace pre post).
Lemma block_height_post_trace :
block_height (block_header pre) <= block_height (block_header post).
Proof.
induction trace as [| ? ? ? ? ? ? ? ? ? valid block_trace eq]; auto.
induction trace as [| ? ? ? ? ? ? ? ? ? ? block_trace eq]; auto.
apply le_trans with (block_height (block_header prev_end)); auto.
rewrite (block_header_post_steps block_trace).
rewrite eq.
unfold IsValidNextBlock in valid.
unfold IsValidNextBlock in *.
simpl.
lia.
Qed.
......
......@@ -2,7 +2,7 @@
chain implementing a chain type. More specifically, we show that the circulation
does not change during execution of blocks. This is proven under the (implicit)
assumption that the address space is finite. *)
From Coq Require Import List Permutation ZArith Psatz.
From Coq Require Import List Permutation ZArith Psatz Morphisms.
From SmartContracts Require Import Automation Blockchain Extras Finite.
From RecordUpdate Require Import RecordSet.
Import ListNotations.
......@@ -14,9 +14,6 @@ Context `{Finite Address}.
Definition circulation (chain : Chain) :=
sumZ (account_balance chain) (elements Address).
Definition coins_created (start_height end_height : nat) : Amount :=
sumZ compute_block_reward (seq (S start_height) (end_height - start_height)).
(* We then prove that over any single step, the circulation is preserved.
The idea behind this proof is that addrs contain from and to so
we can move them to the beginning of the sum and it easily follows that
......@@ -100,10 +97,10 @@ Qed.
Hint Resolve block_trace_circulation_unchanged : core.
Lemma circulation_equal (c1 c2 : Chain) :
ChainEquiv c1 c2 -> circulation c1 = circulation c2.
Instance circulation_proper :
Proper (ChainEquiv ==> eq) circulation.
Proof.
intros [].
intros x y [].
unfold circulation, account_balance.
induction (elements Address); prove.
Qed.
......@@ -144,35 +141,20 @@ Theorem chain_trace_circulation
{env_start env_end : Environment}
(trace : ChainTrace env_start env_end)
: circulation env_end =
(circulation env_start +
coins_created
(block_height (block_header env_start))
(block_height (block_header env_end)))%Z.
sumZ compute_block_reward (seq 1 (block_height (block_header env_end))).
Proof.
unfold coins_created.
induction trace as
[|prev_start prev_end header baker acts block_start new_end prev_trace IH valid block_trace eq].
- rewrite Nat.sub_diag.
simpl. lia.
- unfold IsValidNextBlock in valid.
[env eq|
prev_start prev_end header baker acts block_start new_end prev_trace IH valid block_trace eq].
- rewrite eq.
unfold circulation.
induction (elements Address); auto.
- unfold IsValidNextBlock in *.
rewrite (block_header_post_steps block_trace).
rewrite eq.
simpl.
rewrite (proj1 valid).
unfold coins_created.
pose proof (block_height_post_trace prev_trace) as height_le.
match goal with
| [|- context[S ?a - ?b]] => replace (S a - b) with (S (a - b)) by lia
end.
rewrite sumZ_seq_S.
unfold coins_created in IH.
rewrite Z.add_assoc, <- IH.
match goal with
| [|- context[S ?a + (?b - ?a)]] => replace (S a + (b - a)) with (S b) by lia
end.
rewrite (block_trace_circulation_unchanged block_trace).
rewrite (circulation_equal _ _ eq).
rewrite circulation_add_new_block.
rewrite (proj1 valid), sumZ_seq_S, <- IH.
rewrite (block_trace_circulation_unchanged block_trace), eq, circulation_add_new_block.
now rewrite (proj1 valid).
Qed.
End Circulation.
......@@ -20,12 +20,14 @@ Section LocalBlockchain.
Local Open Scope bool.
Definition AddrSize : N := 2^128.
Definition ContractAddrBase : N := AddrSize / 2.
Global Instance LocalChainBaseTypes : ChainBaseTypes :=
{| Address := BoundedN AddrSize;
address_eqb := BoundedN.eqb;
address_eqb_spec := BoundedN.eqb_spec;
compute_block_reward n := 50%Z;
address_is_contract a := (ContractAddrBase <=? BoundedN.to_N a)%N
|}.
Record LocalChain :=
......@@ -65,8 +67,8 @@ Section ExecuteActions.
Arguments add_tx : simpl never.
Definition count_contract_deployments (lc : LocalChain) : nat :=
FMap.size (lc_contracts lc).
Definition get_new_contract_addr (lc : LocalChain) : option Address :=
BoundedN.of_N (ContractAddrBase + N.of_nat (FMap.size (lc_contracts lc))).
Definition add_contract
(addr : Address)
......@@ -89,6 +91,7 @@ Section ExecuteActions.
match FMap.find to lc.(lc_contracts) with
| None =>
(* Fail if sending a message to address without contract *)
do if address_is_contract to then None else Some tt;
match msg with
| None => Some ([], add_tx (build_tx from to amount tx_empty) lc)
| Some msg => None
......@@ -115,8 +118,7 @@ Section ExecuteActions.
(lc : LocalChain)
: option (list Action * LocalChain) :=
do if amount >? account_balance lc from then None else Some tt;
let num := (1 + count_contract_deployments lc)%nat in
do contract_addr <- BoundedN.of_nat num;
do contract_addr <- get_new_contract_addr lc;
do match incoming_txs lc contract_addr with
| _ :: _ => None
| [] => Some tt
......@@ -257,6 +259,7 @@ Section ExecuteActions.
inversion sent; subst;
now apply set_contract_state_equiv, add_tx_equiv.
- (* no contract at destination, so msg should be empty *)
destruct (address_is_contract to) eqn:addr_format; simpl in *; try congruence.
destruct msg; simpl in *; try congruence.
assert (new_acts = []) by congruence; subst new_acts.
remember_tx.
......@@ -265,6 +268,20 @@ Section ExecuteActions.
inversion sent; subst; now apply add_tx_equiv.
Qed.
Lemma get_new_contract_addr_is_contract_addr lc addr :
get_new_contract_addr lc = Some addr ->
address_is_contract addr = true.
Proof.
intros get.
unfold get_new_contract_addr in get.
pose proof (BoundedN.of_N_some get) as eq.
destruct addr as [addr prf].
simpl in *; rewrite eq.
match goal with
| [|- context[N.leb ?a ?b = true]] => destruct (N.leb_spec a b); auto; lia
end.
Qed.
Lemma deploy_contract_step from amount wc setup act lc_before new_acts lc_after :
deploy_contract from amount wc setup lc_before = Some (new_acts, lc_after) ->
act = build_act from (act_deploy amount wc setup) ->
......@@ -273,8 +290,8 @@ Section ExecuteActions.
intros dep act_eq.
unfold deploy_contract in dep.
destruct (Z.gtb_spec amount (account_balance lc_before from)); [cbn in *; congruence|].
destruct (BoundedN.of_nat _) as [contract_addr|]; [|cbn in *; congruence].
change (BoundedN AddrSize) with Address in *.
destruct (get_new_contract_addr lc_before) as [contract_addr|] eqn:new_contract_addr;
[|cbn in *; congruence].
cbn -[incoming_txs] in dep.
remember_tx.
destruct (incoming_txs _ _) eqn:no_txs; [|cbn in *; congruence].
......@@ -283,8 +300,8 @@ Section ExecuteActions.
cbn in dep.
exists tx.
assert (new_acts = []) by congruence; subst new_acts.
apply (step_deploy from contract_addr amount wc setup state);
try solve [cbn in *; congruence].
Hint Resolve get_new_contract_addr_is_contract_addr : core.
apply (step_deploy from contract_addr amount wc setup state); eauto.
- rewrite <- recv.
apply wc_init_proper; auto.
now symmetry; apply add_tx_equiv.
......@@ -332,14 +349,13 @@ End ExecuteActions.
Definition lc_initial : LocalChain :=
{| lc_header :=
{| block_height := 1;
slot_number := 1;
{| block_height := 0;
slot_number := 0;
finalized_height := 0; |};
lc_incoming_txs := FMap.empty;
lc_outgoing_txs := FMap.empty;
lc_contract_state := FMap.empty;
(* zero address has mined two blocks *)
lc_blocks_baked := FMap.add (BoundedN.of_Z_const AddrSize 0) [0; 1] FMap.empty;
lc_blocks_baked := FMap.empty;
lc_contracts := FMap.empty; |}.
Record LocalChainBuilder :=
......@@ -348,9 +364,14 @@ Record LocalChainBuilder :=
lcb_trace : ChainTrace lc_initial lcb_lc;
}.
Definition lcb_initial : LocalChainBuilder :=
{| lcb_lc := lc_initial;
lcb_trace := ctrace_refl _ |}.
Definition lcb_initial : LocalChainBuilder.
Proof.
refine
{| lcb_lc := lc_initial; lcb_trace := _ |}.
apply ctrace_initial.
apply build_env_equiv; auto.
apply build_chain_equiv; auto.
Defined.
Definition validate_header (new old : BlockHeader) : option unit :=
let (prev_block_height, prev_slot_number, prev_finalized_height) := old in
......
......@@ -12,7 +12,7 @@ Import ListNotations.
Section LocalBlockchainTests.
(* Addresses *)
Definition congress_1 : Address :=
BoundedN.of_Z_const AddrSize 1.
BoundedN.of_Z_const AddrSize (Z.of_N ContractAddrBase).
Definition baker : Address :=
BoundedN.of_Z_const AddrSize 10.
......
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