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

Beautify some proofs and introduce nested record set notation

parent 2e2b3fd0
Pipeline #12754 failed with stage
in 6 minutes and 46 seconds
...@@ -352,27 +352,20 @@ Proof. repeat intro; apply chain_equiv; assumption. Qed. ...@@ -352,27 +352,20 @@ Proof. repeat intro; apply chain_equiv; assumption. Qed.
Instance env_settable : Settable _ := Instance env_settable : Settable _ :=
settable! build_env <env_chain; env_contracts>. settable! build_env <env_chain; env_contracts>.
Definition update_chain (upd : Chain -> Chain) (e : Environment) Definition transfer_balance (from to : Address) (amount : Amount) (env : Environment) :=
: Environment := env<|env_chain; account_balance ::= add_balance to amount|>
let chain := env_chain e in <|env_chain; account_balance ::= add_balance from (-amount)|>.
let chain := upd chain in
e <|env_chain := chain|>.
Definition transfer_balance (from to : Address) (amount : Amount) :=
update_chain (fun c => c<|account_balance ::= add_balance to amount|>
<|account_balance ::= add_balance from (-amount)|>).
Definition add_contract (addr : Address) (contract : WeakContract) (e : Environment) Definition add_contract (addr : Address) (contract : WeakContract) (env : Environment)
: Environment := : Environment :=
e <| env_contracts ::= env<|env_contracts ::=
fun f a => fun f a =>
if (a =? addr)%address if (a =? addr)%address
then Some contract then Some contract
else f a |>. else f a|>.
Definition set_contract_state (addr : Address) (state : OakValue) := Definition set_contract_state (addr : Address) (state : OakValue) (env : Environment) :=
update_chain env<|env_chain; contract_state ::= set_chain_contract_state addr state|>.
(fun c => c <|contract_state ::= set_chain_contract_state addr state|>).
Ltac rewrite_environment_equiv := Ltac rewrite_environment_equiv :=
match goal with match goal with
...@@ -407,7 +400,7 @@ Global Instance set_contract_state_proper : ...@@ -407,7 +400,7 @@ Global Instance set_contract_state_proper :
Proper (eq ==> eq ==> EnvironmentEquiv ==> EnvironmentEquiv) set_contract_state. Proper (eq ==> eq ==> EnvironmentEquiv ==> EnvironmentEquiv) set_contract_state.
Proof. Proof.
repeat intro; subst. repeat intro; subst.
unfold set_contract_state, update_chain, set_chain_contract_state. unfold set_contract_state, set_chain_contract_state.
solve_proper. solve_proper.
Qed. Qed.
...@@ -578,11 +571,9 @@ Definition add_new_block ...@@ -578,11 +571,9 @@ Definition add_new_block
(header : BlockHeader) (header : BlockHeader)
(baker : Address) (baker : Address)
(env : Environment) : Environment := (env : Environment) : Environment :=
let chain := env_chain env in
let chain := chain<|block_header := header|> in
let reward := compute_block_reward (block_height header) in let reward := compute_block_reward (block_height header) in
let chain := chain<|account_balance ::= add_balance baker reward|> in env<|env_chain; block_header := header|>
env<|env_chain := chain|>. <|env_chain; account_balance ::= add_balance baker reward|>.
(* 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 *)
...@@ -602,6 +593,9 @@ Record ChainState := ...@@ -602,6 +593,9 @@ Record ChainState :=
chain_state_queue : list Action; chain_state_queue : list Action;
}. }.
Global Instance chain_state_settable : Settable _ :=
settable! build_chain_state <chain_state_env; chain_state_queue>.
Inductive ChainStep : ChainState -> ChainState -> Type := Inductive ChainStep : ChainState -> ChainState -> Type :=
| step_block : | step_block :
forall {prev : ChainState} forall {prev : ChainState}
......
...@@ -162,14 +162,10 @@ Proof. ...@@ -162,14 +162,10 @@ Proof.
- unfold circulation. - unfold circulation.
induction (elements Address); auto. induction (elements Address); auto.
- rewrite (step_circulation x). - rewrite (step_circulation x).
destruct x. destruct_chain_step.
+ rewrite_environment_equiv. + rewrite_environment_equiv.
cbn. cbn.
unfold constructor. rewrite (proj1 valid_header), IH, sumZ_seq_S; auto.
match goal with
| [H: IsValidNextBlock _ _ |- _] =>
rewrite (proj1 H), IH, sumZ_seq_S; auto
end.
+ erewrite block_header_post_action; eauto. + erewrite block_header_post_action; eauto.
+ intuition. + intuition.
Qed. Qed.
......
...@@ -226,7 +226,8 @@ Definition add_proposal (actions : list CongressAction) (chain : Chain) (state : ...@@ -226,7 +226,8 @@ Definition add_proposal (actions : list CongressAction) (chain : Chain) (state :
vote_result := 0; vote_result := 0;
proposed_in := slot_num |} in proposed_in := slot_num |} in
let new_proposals := FMap.add id proposal state.(proposals) in let new_proposals := FMap.add id proposal state.(proposals) in
state<|proposals := new_proposals|><|next_proposal_id := (id + 1)%nat|>. state<|proposals ::= FMap.add id proposal|>
<|next_proposal_id ::= S|>.
Definition vote_on_proposal Definition vote_on_proposal
(voter : Address) (voter : Address)
...@@ -242,7 +243,8 @@ Definition vote_on_proposal ...@@ -242,7 +243,8 @@ Definition vote_on_proposal
let new_votes := FMap.add voter vote proposal.(votes) in let new_votes := FMap.add voter vote proposal.(votes) in
let new_vote_result := proposal.(vote_result) - old_vote + vote in let new_vote_result := proposal.(vote_result) - old_vote + vote in
let new_proposal := let new_proposal :=
proposal<|votes := new_votes|><|vote_result := new_vote_result|> in proposal<|votes := new_votes|>
<|vote_result := new_vote_result|> in
Some (state<|proposals ::= FMap.add pid new_proposal|>). Some (state<|proposals ::= FMap.add pid new_proposal|>).
Definition do_retract_vote Definition do_retract_vote
...@@ -255,7 +257,8 @@ Definition do_retract_vote ...@@ -255,7 +257,8 @@ Definition do_retract_vote
let new_votes := FMap.remove voter proposal.(votes) in let new_votes := FMap.remove voter proposal.(votes) in
let new_vote_result := proposal.(vote_result) - old_vote in let new_vote_result := proposal.(vote_result) - old_vote in
let new_proposal := let new_proposal :=
proposal<|votes := new_votes|><|vote_result := new_vote_result|> in proposal<|votes := new_votes|>
<|vote_result := new_vote_result|> in
Some (state<|proposals ::= FMap.add pid new_proposal|>). Some (state<|proposals ::= FMap.add pid new_proposal|>).
Definition congress_action_to_chain_action (act : CongressAction) : ActionBody := Definition congress_action_to_chain_action (act : CongressAction) : ActionBody :=
...@@ -479,7 +482,7 @@ Lemma add_proposal_cacts cacts chain state : ...@@ -479,7 +482,7 @@ Lemma add_proposal_cacts cacts chain state :
num_cacts_in_raw_state (add_proposal cacts chain state) <= num_cacts_in_raw_state (add_proposal cacts chain state) <=
num_cacts_in_raw_state state + length cacts. num_cacts_in_raw_state state + length cacts.
Proof. Proof.
unfold add_proposal, num_cacts_in_raw_state, constructor. unfold add_proposal, num_cacts_in_raw_state.
cbn. cbn.
destruct (FMap.find (next_proposal_id state) (proposals state)) as [proposal|] eqn:find. destruct (FMap.find (next_proposal_id state) (proposals state)) as [proposal|] eqn:find.
- remember_new_proposal. - remember_new_proposal.
...@@ -536,7 +539,7 @@ Qed. ...@@ -536,7 +539,7 @@ Qed.
Lemma remove_proposal_cacts pid state proposal : Lemma remove_proposal_cacts pid state proposal :
FMap.find pid (proposals state) = Some proposal -> FMap.find pid (proposals state) = Some proposal ->
num_cacts_in_raw_state (state <| proposals ::= FMap.remove pid |>) + num_cacts_in_raw_state (state <|proposals ::= FMap.remove pid|>) +
length (actions proposal) = num_cacts_in_raw_state state. length (actions proposal) = num_cacts_in_raw_state state.
Proof. Proof.
intros find. intros find.
......
...@@ -58,8 +58,7 @@ Section ExecuteActions. ...@@ -58,8 +58,7 @@ Section ExecuteActions.
Definition add_balance (addr : Address) (amt : Amount) (lc : LocalChain) : LocalChain := Definition add_balance (addr : Address) (amt : Amount) (lc : LocalChain) : LocalChain :=
let update opt := Some (amt + with_default 0 opt) in let update opt := Some (amt + with_default 0 opt) in
let lc := lc<|lc_account_balances ::= FMap.partial_alter update addr|> in lc<|lc_account_balances ::= FMap.partial_alter update addr|>.
lc.
Definition transfer_balance Definition transfer_balance
(from to : Address) (amount : Amount) (lc : LocalChain) : LocalChain := (from to : Address) (amount : Amount) (lc : LocalChain) : LocalChain :=
......
...@@ -98,8 +98,14 @@ Hint Extern 1 (SetterWf _) => SetterWfInstance_t : typeclass_instances. ...@@ -98,8 +98,14 @@ Hint Extern 1 (SetterWf _) => SetterWfInstance_t : typeclass_instances.
Module RecordSetNotations. Module RecordSetNotations.
Delimit Scope record_set with rs. Delimit Scope record_set with rs.
Open Scope rs. Open Scope rs.
Notation "x <| proj := v |>" := (set proj (constructor v) x) Notation "x <| proj := v |>" := (set proj (fun _ => v) x)
(at level 12, left associativity) : record_set. (at level 12, left associativity) : record_set.
Notation "x <| proj ::= f |>" := (set proj f x) Notation "x <| proj ::= f |>" := (set proj f x)
(at level 12, f at next level, left associativity) : record_set. (at level 12, f at next level, left associativity) : record_set.
Notation "x <| proj1 ; proj2 ; .. ; projn := v |>" :=
(set proj1 (set proj2 .. (set projn (fun _ => v)) ..) x)
(at level 12, left associativity).
Notation "x <| proj1 ; proj2 ; .. ; projn ::= f |>" :=
(set proj1 (set proj2 .. (set projn f) ..) x)
(at level 12, left associativity).
End RecordSetNotations. End RecordSetNotations.
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