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

Refactor to remove compute_block_reward

- No longer require that block reward can be computed from height.
- Remove Chain's dependence on BlockHeader. Instead inline appropriate
  fields in Chain structure.
- Change step_block to use a BlockHeader now instead of manually
  specifying all the fields. The new BlockHeader now additionally
  contains the creator and reward of that block, so step_block in effect
  contains the reward.
- These refactorings means that the circulation proof changes. Introduce
  created_blocks to get list of blocks created by user, and prove
  instead that the circulation equals the sum of rewards in blocks.
- Rename "baker" to a more general "creator" globally
parent 4ff6fa50
Pipeline #12836 failed with stage
in 6 minutes and 18 seconds
...@@ -27,12 +27,10 @@ Class ChainBase := ...@@ -27,12 +27,10 @@ Class ChainBase :=
address_countable :> countable.Countable Address; address_countable :> countable.Countable Address;
address_ote :> OakTypeEquivalence Address; address_ote :> OakTypeEquivalence Address;
address_is_contract : Address -> bool; address_is_contract : Address -> bool;
compute_block_reward : nat -> Amount;
}. }.
Global Opaque Address address_eqb address_eqb_spec Global Opaque Address address_eqb address_eqb_spec
address_eqdec address_countable address_eqdec address_countable address_ote.
address_ote compute_block_reward.
Delimit Scope address_scope with address. Delimit Scope address_scope with address.
Bind Scope address_scope with Address. Bind Scope address_scope with Address.
...@@ -67,21 +65,13 @@ Global Ltac destruct_address_eq := ...@@ -67,21 +65,13 @@ Global Ltac destruct_address_eq :=
Section Blockchain. Section Blockchain.
Context {BaseTypes : ChainBase}. Context {BaseTypes : ChainBase}.
Record BlockHeader :=
build_block_header {
block_height : nat;
slot_number : nat;
finalized_height : nat;
}.
Global Instance block_header_settable : Settable _ :=
settable! build_block_header <block_height; slot_number; finalized_height>.
(* This represents the view of the blockchain that a contract (* This represents the view of the blockchain that a contract
can access and interact with. *) can access and interact with. *)
Record Chain := Record Chain :=
build_chain { build_chain {
block_header : BlockHeader; chain_height : nat;
current_slot : nat;
finalized_height : nat;
account_balance : Address -> Amount; account_balance : Address -> Amount;
contract_state : Address -> option OakValue; contract_state : Address -> option OakValue;
}. }.
...@@ -91,7 +81,9 @@ We will later require that all deployed contracts respect this relation. ...@@ -91,7 +81,9 @@ We will later require that all deployed contracts respect this relation.
This equivalence is equality if funext 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; chain_height_eq : chain_height c1 = chain_height c2;
current_slot_eq : current_slot c1 = current_slot c2;
finalized_height_eq : finalized_height c1 = finalized_height c2;
account_balance_eq : forall addr, account_balance c1 addr = account_balance c2 addr; account_balance_eq : forall addr, account_balance c1 addr = account_balance c2 addr;
contract_state_eq : forall addr, contract_state c1 addr = contract_state c2 addr; contract_state_eq : forall addr, contract_state c1 addr = contract_state c2 addr;
}. }.
...@@ -101,9 +93,15 @@ Next Obligation. repeat intro; apply build_chain_equiv; reflexivity. Qed. ...@@ -101,9 +93,15 @@ Next Obligation. repeat intro; apply build_chain_equiv; reflexivity. Qed.
Next Obligation. intros x y []; apply build_chain_equiv; congruence. Qed. Next Obligation. intros x y []; apply build_chain_equiv; congruence. Qed.
Next Obligation. intros x y z [] []; apply build_chain_equiv; congruence. Qed. Next Obligation. intros x y z [] []; apply build_chain_equiv; congruence. Qed.
Global Instance chain_equiv_header_proper : Global Instance chain_equiv_chain_height :
Proper (ChainEquiv ==> eq) block_header. Proper (ChainEquiv ==> eq) chain_height.
Proof. repeat intro; auto using header_eq. Qed. Proof. repeat intro; auto using chain_height_eq. Qed.
Global Instance chain_equiv_current_slot :
Proper (ChainEquiv ==> eq) current_slot.
Proof. repeat intro; auto using current_slot_eq. Qed.
Global Instance chain_equiv_finalized_height :
Proper (ChainEquiv ==> eq) finalized_height.
Proof. repeat intro; auto using finalized_height_eq. Qed.
Global Instance chain_equiv_account_balance_proper : Global Instance chain_equiv_account_balance_proper :
Proper (ChainEquiv ==> eq ==> eq) account_balance. Proper (ChainEquiv ==> eq ==> eq) account_balance.
Proof. repeat intro; subst; auto using account_balance_eq. Qed. Proof. repeat intro; subst; auto using account_balance_eq. Qed.
...@@ -301,7 +299,8 @@ Definition get_contract_interface ...@@ -301,7 +299,8 @@ Definition get_contract_interface
Section Semantics. Section Semantics.
Instance chain_settable : Settable _ := Instance chain_settable : Settable _ :=
settable! build_chain <block_header; account_balance; contract_state>. settable! build_chain <chain_height; current_slot; finalized_height;
account_balance; contract_state>.
Definition add_balance (addr : Address) (amount : Amount) (map : Address -> Amount) : Definition add_balance (addr : Address) (amount : Amount) (map : Address -> Amount) :
Address -> Amount := Address -> Amount :=
...@@ -422,7 +421,9 @@ Inductive ActionEvaluation : ...@@ -422,7 +421,9 @@ Inductive ActionEvaluation :
amount <= account_balance pre from -> amount <= account_balance pre from ->
address_is_contract to = false -> address_is_contract to = false ->
act = build_act from (act_transfer to amount) -> act = build_act from (act_transfer to amount) ->
EnvironmentEquiv new_env (transfer_balance from to amount pre) -> EnvironmentEquiv
new_env
(transfer_balance from to amount pre) ->
ActionEvaluation pre act new_env [] ActionEvaluation pre act new_env []
| eval_deploy : | eval_deploy :
forall {pre : Environment} forall {pre : Environment}
...@@ -552,7 +553,13 @@ Proof. ...@@ -552,7 +553,13 @@ Proof.
lia. lia.
Qed. Qed.
Lemma block_header_post_action : block_header post = block_header pre. Lemma chain_height_post_action : chain_height post = chain_height pre.
Proof. destruct eval; rewrite_environment_equiv; auto. Qed.
Lemma current_slot_post_action : current_slot post = current_slot pre.
Proof. destruct eval; rewrite_environment_equiv; auto. Qed.
Lemma finalized_height_post_action : finalized_height post = finalized_height pre.
Proof. destruct eval; rewrite_environment_equiv; auto. Qed. Proof. destruct eval; rewrite_environment_equiv; auto. Qed.
Lemma contracts_post_pre_none contract : Lemma contracts_post_pre_none contract :
...@@ -567,26 +574,41 @@ Qed. ...@@ -567,26 +574,41 @@ Qed.
End Theories. End Theories.
Section Trace. Section Trace.
Definition add_new_block
(header : BlockHeader) Record BlockHeader :=
(baker : Address) build_block_Header {
(env : Environment) : Environment := block_height : nat;
let reward := compute_block_reward (block_height header) in block_slot : nat;
env<|env_chain; block_header := header|> block_finalized_height : nat;
<|env_chain; account_balance ::= add_balance baker reward|>. block_reward : Amount;
block_creator : Address;
}.
Definition add_new_block_to_env
(header : BlockHeader) (env : Environment) : Environment :=
env<|env_chain; chain_height := block_height header|>
<|env_chain; current_slot := block_slot header|>
<|env_chain; finalized_height := block_finalized_height header|>
<|env_chain; account_balance ::=
add_balance (block_creator header) (block_reward header)|>.
(* Todo: this should just be a computation. But I still do not *) (* Todo: this should just be a computation. But I still do not *)
(* know exactly what the best way of working with reflect is *) (* know exactly what the best way of working with reflect is *)
Local Open Scope nat. Local Open Scope nat.
Definition IsValidNextBlock (new old : BlockHeader) : Prop := Definition act_is_from_account (act : Action) : Prop :=
block_height new = S (block_height old) /\
slot_number new > slot_number old /\
finalized_height new >= finalized_height old /\
finalized_height new < block_height new.
Definition ActIsFromAccount (act : Action) : Prop :=
address_is_contract (act_from act) = false. address_is_contract (act_from act) = false.
Record IsValidNextBlock (header : BlockHeader) (chain : Chain) : Prop :=
build_is_valid_next_block {
valid_height : block_height header = S (chain_height chain);
valid_slot : block_slot header > current_slot chain;
valid_finalized_height :
block_finalized_height header >= finalized_height chain /\
block_finalized_height header < block_height header;
valid_creator : address_is_contract (block_creator header) = false;
valid_reward : (block_reward header >= 0)%Z;
}.
Record ChainState := Record ChainState :=
build_chain_state { build_chain_state {
chain_state_env :> Environment; chain_state_env :> Environment;
...@@ -598,40 +620,36 @@ Global Instance chain_state_settable : Settable _ := ...@@ -598,40 +620,36 @@ Global Instance chain_state_settable : Settable _ :=
Inductive ChainStep : ChainState -> ChainState -> Type := Inductive ChainStep : ChainState -> ChainState -> Type :=
| step_block : | step_block :
forall {prev : ChainState} forall {prev next : ChainState}
{header : BlockHeader} (header : BlockHeader),
{baker : Address}
{next : ChainState},
chain_state_queue prev = [] -> chain_state_queue prev = [] ->
IsValidNextBlock header (block_header prev) -> IsValidNextBlock header prev ->
Forall ActIsFromAccount (chain_state_queue next) -> Forall act_is_from_account (chain_state_queue next) ->
EnvironmentEquiv EnvironmentEquiv
next next
(add_new_block header baker prev) -> (add_new_block_to_env header prev) ->
ChainStep prev next ChainStep prev next
| step_action : | step_action :
forall {prev : ChainState} forall {prev next : ChainState}
{act : Action} (act : Action)
{acts : list Action} (acts : list Action)
{next : ChainState} (new_acts : list Action),
{new_acts : list Action},
chain_state_queue prev = act :: acts -> chain_state_queue prev = act :: acts ->
ActionEvaluation prev act next new_acts -> ActionEvaluation prev act next new_acts ->
chain_state_queue next = new_acts ++ acts -> chain_state_queue next = new_acts ++ acts ->
ChainStep prev next ChainStep prev next
| step_permute : | step_permute :
forall {prev new : ChainState}, forall {prev next : ChainState},
chain_state_env prev = chain_state_env new -> chain_state_env prev = chain_state_env next ->
Permutation (chain_state_queue prev) (chain_state_queue new) -> Permutation (chain_state_queue prev) (chain_state_queue next) ->
ChainStep prev new. ChainStep prev next.
Definition empty_state : ChainState := Definition empty_state : ChainState :=
{| chain_state_env := {| chain_state_env :=
{| env_chain := {| env_chain :=
{| block_header := {| chain_height := 0;
{| block_height := 0; current_slot := 0;
slot_number := 0; finalized_height := 0;
finalized_height := 0; |};
account_balance a := 0%Z; account_balance a := 0%Z;
contract_state a := None; |}; contract_state a := None; |};
env_contracts a := None; |}; env_contracts a := None; |};
...@@ -680,7 +698,7 @@ Fixpoint trace_txs {from to : ChainState} (trace : ChainTrace from to) : list Tx ...@@ -680,7 +698,7 @@ Fixpoint trace_txs {from to : ChainState} (trace : ChainTrace from to) : list Tx
match trace with match trace with
| snoc trace' step => | snoc trace' step =>
match step with match step with
| step_action _ eval _ => eval_tx eval :: trace_txs trace' | step_action _ _ _ _ eval _ => eval_tx eval :: trace_txs trace'
| _ => trace_txs trace' | _ => trace_txs trace'
end end
| _ => [] | _ => []
...@@ -698,28 +716,32 @@ Definition outgoing_txs ...@@ -698,28 +716,32 @@ Definition outgoing_txs
(addr : Address) : list Tx := (addr : Address) : list Tx :=
filter (fun tx => (tx_from tx =? addr)%address) (trace_txs trace). filter (fun tx => (tx_from tx =? addr)%address) (trace_txs trace).
Fixpoint blocks_baked {from to : ChainState} Fixpoint trace_blocks {from to : ChainState}
(trace : ChainTrace from to) (addr : Address) : list nat := (trace : ChainTrace from to) : list BlockHeader :=
match trace with match trace with
| snoc trace' step => | snoc trace' step =>
match step with match step with
| @step_block _ header baker _ _ _ _ _ => | step_block header _ _ _ _ =>
if (baker =? addr)%address header :: trace_blocks trace'
then block_height header :: blocks_baked trace' addr | _ => trace_blocks trace'
else blocks_baked trace' addr
| _ => blocks_baked trace' addr
end end
| clnil => [] | clnil => []
end. end.
Definition created_blocks
{from to : ChainState} (trace : ChainTrace from to)
(creator : Address) : list BlockHeader :=
filter (fun b => (block_creator b =? creator)%address)
(trace_blocks trace).
Section Theories. Section Theories.
Ltac destruct_chain_step := Ltac destruct_chain_step :=
match goal with match goal with
| [step: ChainStep _ _ |- _] => | [step: ChainStep _ _ |- _] =>
destruct step as destruct step as
[prev header baker next queue_prev valid_header acts_from_accs env_eq| [prev next header queue_prev valid_header acts_from_accs env_eq|
prev act acts next new_acts queue_prev step queue_new| prev next act acts new_acts queue_prev eval queue_new|
prev new prev_new perm] prev next prev_next perm]
end. end.
Ltac destruct_action_eval := Ltac destruct_action_eval :=
...@@ -859,7 +881,7 @@ Local Open Scope Z. ...@@ -859,7 +881,7 @@ Local Open Scope Z.
Lemma account_balance_trace state (trace : ChainTrace empty_state state) addr : Lemma account_balance_trace state (trace : ChainTrace empty_state state) addr :
account_balance state addr = account_balance state addr =
sumZ tx_amount (incoming_txs trace addr) + sumZ tx_amount (incoming_txs trace addr) +
sumZ compute_block_reward (blocks_baked trace addr) - sumZ block_reward (created_blocks trace addr) -
sumZ tx_amount (outgoing_txs trace addr). sumZ tx_amount (outgoing_txs trace addr).
Proof. Proof.
unfold incoming_txs, outgoing_txs. unfold incoming_txs, outgoing_txs.
...@@ -869,16 +891,17 @@ Proof. ...@@ -869,16 +891,17 @@ Proof.
- (* Block *) - (* Block *)
rewrite_environment_equiv. rewrite_environment_equiv.
cbn. cbn.
fold (created_blocks trace addr).
unfold add_balance. unfold add_balance.
rewrite IHtrace by auto. rewrite IHtrace by auto.
destruct_address_eq; subst; cbn; lia. destruct_address_eq; subst; cbn; lia.
- (* Step *) - (* Step *)
cbn. cbn.
destruct_action_eval; cbn; rewrite_environment_equiv; cbn. destruct_action_eval; cbn; rewrite_environment_equiv; cbn.
all: unfold add_balance; rewrite IHtrace by auto. all: fold (created_blocks trace addr); unfold add_balance; rewrite IHtrace by auto.
all: destruct_address_eq; cbn; lia. all: destruct_address_eq; cbn; lia.
- cbn. - cbn.
rewrite <- prev_new. rewrite <- prev_next.
auto. auto.
Qed. Qed.
...@@ -896,7 +919,6 @@ Class ChainBuilderType := ...@@ -896,7 +919,6 @@ Class ChainBuilderType :=
builder_add_block builder_add_block
(builder : builder_type) (builder : builder_type)
(baker : Address)
(header : BlockHeader) (header : BlockHeader)
(actions : list Action) : (actions : list Action) :
option builder_type; option builder_type;
...@@ -919,9 +941,9 @@ Ltac destruct_chain_step := ...@@ -919,9 +941,9 @@ Ltac destruct_chain_step :=
match goal with match goal with
| [step: ChainStep _ _ |- _] => | [step: ChainStep _ _ |- _] =>
destruct step as destruct step as
[prev header baker next queue_prev valid_header acts_from_accs env_eq| [prev next header queue_prev valid_header acts_from_accs env_eq|
prev act acts next new_acts queue_prev step queue_new| prev next act acts new_acts queue_prev eval queue_new|
prev new prev_new perm] prev next prev_next perm]
end. end.
Ltac destruct_action_eval := Ltac destruct_action_eval :=
......
...@@ -101,11 +101,11 @@ Proof. ...@@ -101,11 +101,11 @@ Proof.
end. end.
Qed. Qed.
Lemma circulation_add_new_block header baker env : Lemma circulation_add_new_block header env :
circulation (add_new_block header baker env) = circulation (add_new_block_to_env header env) =
(circulation env + compute_block_reward (block_height header))%Z. (circulation env + block_reward header)%Z.
Proof. Proof.
assert (Hperm: exists suf, Permutation ([baker] ++ suf) (elements Address)). assert (Hperm: exists suf, Permutation ([block_creator header] ++ suf) (elements Address)).
{ apply NoDup_incl_reorganize; repeat constructor; unfold incl; auto. } { apply NoDup_incl_reorganize; repeat constructor; unfold incl; auto. }
destruct Hperm as [suf perm]. destruct Hperm as [suf perm].
symmetry in perm. symmetry in perm.
...@@ -119,12 +119,14 @@ Proof. ...@@ -119,12 +119,14 @@ Proof.
| [|- ?a + ?b + ?c = ?b + ?d + ?a] => enough (c = d) by lia | [|- ?a + ?b + ?c = ?b + ?d + ?a] => enough (c = d) by lia
end. end.
pose proof (in_NoDup_app baker [baker] suf ltac:(intuition) perm_set) as not_in_suf. pose proof (in_NoDup_app
(block_creator header)
[block_creator header] suf ltac:(intuition) perm_set) as not_in_suf.
clear perm perm_set. clear perm perm_set.
induction suf as [| x xs IH]; auto. induction suf as [| x xs IH]; auto.
cbn in *. cbn in *.
apply Decidable.not_or in not_in_suf. apply Decidable.not_or in not_in_suf.
destruct (address_eqb_spec x baker); try tauto. destruct (address_eqb_spec x (block_creator header)); try tauto.
specialize (IH (proj2 not_in_suf)). specialize (IH (proj2 not_in_suf)).
lia. lia.
Qed. Qed.
...@@ -132,16 +134,12 @@ Qed. ...@@ -132,16 +134,12 @@ Qed.
Lemma step_circulation {prev next} (step : ChainStep prev next) : Lemma step_circulation {prev next} (step : ChainStep prev next) :
circulation next = circulation next =
match step with match step with
| step_block _ _ _ _ => | step_block header _ _ _ _ =>
circulation prev + compute_block_reward (block_height (block_header next)) circulation prev + block_reward header
| _ => circulation prev | _ => circulation prev
end%Z. end%Z.
Proof. Proof.
destruct step; destruct_chain_step; try rewrite_environment_equiv.
repeat
match goal with
| [H: EnvironmentEquiv _ _ |- _] => rewrite H in *; clear H
end.
- (* New block *) - (* New block *)
now rewrite circulation_add_new_block. now rewrite circulation_add_new_block.
- (* New action *) - (* New action *)
...@@ -151,22 +149,19 @@ Proof. ...@@ -151,22 +149,19 @@ Proof.
Qed. Qed.
Theorem chain_trace_circulation Theorem chain_trace_circulation
{state : ChainState} : {state : ChainState}
reachable state -> (trace : ChainTrace empty_state state) :
circulation state = circulation state = sumZ block_reward (trace_blocks trace).
sumZ compute_block_reward (seq 1 (block_height (block_header state))).
Proof. Proof.
intros [trace].
remember empty_state as from eqn:eq. remember empty_state as from eqn:eq.
induction trace as [| from mid to xs IH x]; rewrite eq in *; clear eq. induction trace as [| from mid to xs IH x]; subst.
- unfold circulation. - unfold circulation.
induction (elements Address); auto. induction (elements Address); auto.
- rewrite (step_circulation x). - rewrite (step_circulation x).
destruct_chain_step. cbn.
+ rewrite_environment_equiv. destruct_chain_step; auto.
cbn. cbn.
rewrite (proj1 valid_header), IH, sumZ_seq_S; auto. rewrite <- IH by auto.
+ erewrite block_header_post_action; eauto. lia.
+ intuition.
Qed. Qed.
End Circulation. End Circulation.
...@@ -220,7 +220,7 @@ Definition init ...@@ -220,7 +220,7 @@ Definition init
Definition add_proposal (actions : list CongressAction) (chain : Chain) (state : State) : State := Definition add_proposal (actions : list CongressAction) (chain : Chain) (state : State) : State :=
let id := state.(next_proposal_id) in let id := state.(next_proposal_id) in
let slot_num := chain.(block_header).(slot_number) in let slot_num := chain.(current_slot) in
let proposal := {| actions := actions; let proposal := {| actions := actions;
votes := FMap.empty; votes := FMap.empty;
vote_result := 0; vote_result := 0;
...@@ -285,7 +285,7 @@ Definition do_finish_proposal ...@@ -285,7 +285,7 @@ Definition do_finish_proposal
do proposal <- FMap.find pid state.(proposals); do proposal <- FMap.find pid state.(proposals);
let rules := state.(state_rules) in let rules := state.(state_rules) in
let debate_end := (proposal.(proposed_in) + rules.(debating_period_in_blocks))%nat in let debate_end := (proposal.(proposed_in) + rules.(debating_period_in_blocks))%nat in
let cur_slot := chain.(block_header).(slot_number) in let cur_slot := chain.(current_slot) in
if (cur_slot <? debate_end)%nat then if (cur_slot <? debate_end)%nat then
None None
else else
...@@ -421,7 +421,7 @@ Qed. ...@@ -421,7 +421,7 @@ Qed.
Lemma num_outgoing_acts_block l contract : Lemma num_outgoing_acts_block l contract :
address_is_contract contract = true -> address_is_contract contract = true ->
Forall ActIsFromAccount l -> Forall act_is_from_account l ->
num_outgoing_acts l contract = 0. num_outgoing_acts l contract = 0.
Proof. Proof.
intros is_contract all. intros is_contract all.
...@@ -709,7 +709,7 @@ Local Ltac simpl_exp_invariant exp := ...@@ -709,7 +709,7 @@ Local Ltac simpl_exp_invariant exp :=
| context G[filter ?f (?hd :: ?tl)] => | context G[filter ?f (?hd :: ?tl)] =>
let newexp := context G[filter f tl] in let newexp := context G[filter f tl] in
replace exp with newexp by solve_single replace exp with newexp by solve_single
| context G[add_new_block _ _ ?env] => | context G[add_new_block_to_env _ ?env] =>
let newexp := context G[env] in let newexp := context G[env] in
replace exp with newexp by solve_single replace exp with newexp by solve_single
| context G[transfer_balance _ _ _ ?env] => | context G[transfer_balance _ _ _ ?env] =>
...@@ -855,13 +855,13 @@ Proof. ...@@ -855,13 +855,13 @@ Proof.
- (* Permute queue *) - (* Permute queue *)
unfold num_outgoing_acts. unfold num_outgoing_acts.
cbn. cbn.
rewrite <- perm, prev_new in *; auto. rewrite <- perm, prev_next in *; auto.
Qed. Qed.
Corollary congress_txs_after_block Corollary congress_txs_after_block
{ChainBuilder : ChainBuilderType} {ChainBuilder : ChainBuilderType}
prev baker header acts new : prev new header acts :
builder_add_block prev baker header acts = Some new -> builder_add_block prev header acts = Some new ->
forall addr, forall addr,
env_contracts new addr = Some (Congress.contract : WeakContract) ->