Contents:
Library ConCert.Examples.EIP20.EIP20TokenCorrect
From Coq Require Import ZArith_base.
From Coq Require Import List. Import ListNotations.
From Coq Require Import Lia.
From ConCert.Execution Require Import Blockchain.
From ConCert.Execution Require Import Containers.
From ConCert.Execution Require Import Monad.
From ConCert.Execution Require Import ResultMonad.
From ConCert.Execution Require Import ContractCommon.
From ConCert.Utils Require Import Automation.
From ConCert.Utils Require Import Extras.
From ConCert.Examples.EIP20 Require Import EIP20Token.
From Coq Require Import List. Import ListNotations.
From Coq Require Import Lia.
From ConCert.Execution Require Import Blockchain.
From ConCert.Execution Require Import Containers.
From ConCert.Execution Require Import Monad.
From ConCert.Execution Require Import ResultMonad.
From ConCert.Execution Require Import ContractCommon.
From ConCert.Utils Require Import Automation.
From ConCert.Utils Require Import Extras.
From ConCert.Examples.EIP20 Require Import EIP20Token.
Lemma EIP20_not_payable : forall prev_state new_state chain ctx msg new_acts,
receive chain ctx prev_state msg = Ok (new_state, new_acts) ->
((ctx_amount ctx) <= 0)%Z.
Proof.
intros * receive_some.
unfold receive in receive_some.
destruct_match eqn:amount in receive_some.
- (* case: ctx_amount > 0 *)
discriminate.
- (* case: ctx_amount <= 0 *)
now rewrite Z.gtb_ltb, Z.ltb_ge in amount.
Qed.
receive chain ctx prev_state msg = Ok (new_state, new_acts) ->
((ctx_amount ctx) <= 0)%Z.
Proof.
intros * receive_some.
unfold receive in receive_some.
destruct_match eqn:amount in receive_some.
- (* case: ctx_amount > 0 *)
discriminate.
- (* case: ctx_amount <= 0 *)
now rewrite Z.gtb_ltb, Z.ltb_ge in amount.
Qed.
Lemma for simplifying the receive function by eliminating the case
where sender amount is larger than zero
Lemma receive_not_payable : forall prev_state new_state chain ctx msg new_acts,
receive chain ctx prev_state (Some msg) = Ok (new_state, new_acts) ->
match msg with
| transfer to amount => (try_transfer (ctx_from ctx) to amount prev_state) >>= (fun new_state : State => Ok (new_state, []))
| transfer_from from to amount =>
(try_transfer_from (ctx_from ctx) from to amount prev_state) >>= (fun new_state : State => Ok (new_state, []))
| approve delegate amount =>
(try_approve (ctx_from ctx) delegate amount prev_state) >>= (fun new_state : State => Ok (new_state, []))
end = Ok (new_state, new_acts).
Proof.
intros * receive_some.
apply EIP20_not_payable in receive_some as amount_zero.
unfold receive in receive_some.
rewrite <- Z.ltb_ge, <- Z.gtb_ltb in amount_zero.
now rewrite amount_zero in receive_some.
Qed.
receive chain ctx prev_state (Some msg) = Ok (new_state, new_acts) ->
match msg with
| transfer to amount => (try_transfer (ctx_from ctx) to amount prev_state) >>= (fun new_state : State => Ok (new_state, []))
| transfer_from from to amount =>
(try_transfer_from (ctx_from ctx) from to amount prev_state) >>= (fun new_state : State => Ok (new_state, []))
| approve delegate amount =>
(try_approve (ctx_from ctx) delegate amount prev_state) >>= (fun new_state : State => Ok (new_state, []))
end = Ok (new_state, new_acts).
Proof.
intros * receive_some.
apply EIP20_not_payable in receive_some as amount_zero.
unfold receive in receive_some.
rewrite <- Z.ltb_ge, <- Z.gtb_ltb in amount_zero.
now rewrite amount_zero in receive_some.
Qed.
Lemma EIP20_no_acts : forall prev_state new_state chain ctx msg new_acts,
receive chain ctx prev_state msg = Ok (new_state, new_acts) ->
new_acts = [].
Proof.
intros * receive_some.
unfold receive, option_map in receive_some.
repeat (destruct_match in receive_some; cbn in *); easy.
Qed.
Lemma receive_no_acts : forall prev_state new_state chain ctx msg new_acts,
receive chain ctx prev_state (Some msg) = Ok (new_state, new_acts) ->
receive chain ctx prev_state (Some msg) = Ok (new_state, []).
Proof.
intros.
now erewrite <- EIP20_no_acts.
Qed.
receive chain ctx prev_state msg = Ok (new_state, new_acts) ->
new_acts = [].
Proof.
intros * receive_some.
unfold receive, option_map in receive_some.
repeat (destruct_match in receive_some; cbn in *); easy.
Qed.
Lemma receive_no_acts : forall prev_state new_state chain ctx msg new_acts,
receive chain ctx prev_state (Some msg) = Ok (new_state, new_acts) ->
receive chain ctx prev_state (Some msg) = Ok (new_state, []).
Proof.
intros.
now erewrite <- EIP20_no_acts.
Qed.
Default entrypoint always fail
Lemma default_none : forall prev_state chain ctx,
receive chain ctx prev_state None = Err default_error.
Proof.
intros.
unfold receive.
now destruct_match.
Qed.
receive chain ctx prev_state None = Err default_error.
Proof.
intros.
unfold receive.
now destruct_match.
Qed.
Definition transfer_balance_update_correct old_state new_state from to tokens :=
let get_balance addr state := with_default 0 (FMap.find addr state.(balances)) in
let from_balance_before := get_balance from old_state in
let to_balance_before := get_balance to old_state in
let from_balance_after := get_balance from new_state in
let to_balance_after := get_balance to new_state in
let get_balance addr state := with_default 0 (FMap.find addr state.(balances)) in
let from_balance_before := get_balance from old_state in
let to_balance_before := get_balance to old_state in
let from_balance_after := get_balance from new_state in
let to_balance_after := get_balance to new_state in
if the transfer is a self-transfer, balances should remain unchained
if address_eqb from to
then
(from_balance_before =? from_balance_after) &&
(to_balance_before =? to_balance_after)
else
(from_balance_before =? from_balance_after + tokens) &&
(to_balance_before + tokens =? to_balance_after).
Definition transfer_from_allowances_update_correct (old_state new_state : State) (from delegate : Address) (tokens : TokenValue) :=
let delegate_allowance_before := get_allowance old_state from delegate in
let delegate_allowance_after := get_allowance new_state from delegate in
delegate_allowance_before =? delegate_allowance_after + tokens.
Definition approve_allowance_update_correct (new_state : State) (from delegate : Address) (tokens : TokenValue) :=
let delegate_allowance_after := get_allowance new_state from delegate in
delegate_allowance_after =? tokens.
then
(from_balance_before =? from_balance_after) &&
(to_balance_before =? to_balance_after)
else
(from_balance_before =? from_balance_after + tokens) &&
(to_balance_before + tokens =? to_balance_after).
Definition transfer_from_allowances_update_correct (old_state new_state : State) (from delegate : Address) (tokens : TokenValue) :=
let delegate_allowance_before := get_allowance old_state from delegate in
let delegate_allowance_after := get_allowance new_state from delegate in
delegate_allowance_before =? delegate_allowance_after + tokens.
Definition approve_allowance_update_correct (new_state : State) (from delegate : Address) (tokens : TokenValue) :=
let delegate_allowance_after := get_allowance new_state from delegate in
delegate_allowance_after =? tokens.
Lemma try_transfer_balance_correct : forall prev_state new_state chain ctx to amount new_acts,
receive chain ctx prev_state (Some (transfer to amount)) = Ok (new_state, new_acts) ->
transfer_balance_update_correct prev_state new_state ctx.(ctx_from) to amount = true.
Proof.
intros * receive_some.
unfold transfer_balance_update_correct.
contract_simpl.
rename H0 into sender_enough_balance.
apply N.ltb_ge in sender_enough_balance.
destruct_address_eq; destruct (FMap.find (ctx_from ctx) (balances prev_state)) eqn:from_prev;
try congruence; subst; try (rewrite from_prev || setoid_rewrite from_prev);
clear from_prev new_acts chain; cbn in *.
- (* case: from = to && find from = Some n && amount <= n *)
FMap_simpl.
now rewrite N.sub_add, N.eqb_refl.
- (* case: from = to && find from = None && amount = 0 *)
apply N.lt_eq_cases in sender_enough_balance as []; [lia | subst].
now FMap_simpl.
- (* case: from <> to && find from = Some n && amount <= n *)
FMap_simpl.
rewrite N.sub_add; auto.
now rewrite !N.eqb_refl.
- (* case: from <> to && find from = None && amount = 0 *)
apply N.lt_eq_cases in sender_enough_balance as []; [lia | subst].
FMap_simpl.
apply N.eqb_refl.
Qed.
receive chain ctx prev_state (Some (transfer to amount)) = Ok (new_state, new_acts) ->
transfer_balance_update_correct prev_state new_state ctx.(ctx_from) to amount = true.
Proof.
intros * receive_some.
unfold transfer_balance_update_correct.
contract_simpl.
rename H0 into sender_enough_balance.
apply N.ltb_ge in sender_enough_balance.
destruct_address_eq; destruct (FMap.find (ctx_from ctx) (balances prev_state)) eqn:from_prev;
try congruence; subst; try (rewrite from_prev || setoid_rewrite from_prev);
clear from_prev new_acts chain; cbn in *.
- (* case: from = to && find from = Some n && amount <= n *)
FMap_simpl.
now rewrite N.sub_add, N.eqb_refl.
- (* case: from = to && find from = None && amount = 0 *)
apply N.lt_eq_cases in sender_enough_balance as []; [lia | subst].
now FMap_simpl.
- (* case: from <> to && find from = Some n && amount <= n *)
FMap_simpl.
rewrite N.sub_add; auto.
now rewrite !N.eqb_refl.
- (* case: from <> to && find from = None && amount = 0 *)
apply N.lt_eq_cases in sender_enough_balance as []; [lia | subst].
FMap_simpl.
apply N.eqb_refl.
Qed.
try_transfer does not change the total supply of tokens
Lemma try_transfer_preserves_total_supply : forall prev_state new_state chain ctx to amount new_acts,
receive chain ctx prev_state (Some (transfer to amount)) = Ok (new_state, new_acts) ->
(total_supply prev_state) = (total_supply new_state).
Proof.
intros * receive_some.
now contract_simpl.
Qed.
receive chain ctx prev_state (Some (transfer to amount)) = Ok (new_state, new_acts) ->
(total_supply prev_state) = (total_supply new_state).
Proof.
intros * receive_some.
now contract_simpl.
Qed.
try_transfer does not change allowances
Lemma try_transfer_preserves_allowances : forall prev_state new_state chain ctx to amount new_acts,
receive chain ctx prev_state (Some (transfer to amount)) = Ok (new_state, new_acts) ->
(allowances prev_state) = (allowances new_state).
Proof.
intros * receive_some.
now contract_simpl.
Qed.
receive chain ctx prev_state (Some (transfer to amount)) = Ok (new_state, new_acts) ->
(allowances prev_state) = (allowances new_state).
Proof.
intros * receive_some.
now contract_simpl.
Qed.
Lemma try_transfer_preserves_other_balances : forall prev_state new_state chain ctx to amount new_acts,
receive chain ctx prev_state (Some (transfer to amount)) = Ok (new_state, new_acts) ->
forall account, account <> (ctx_from ctx) -> account <> to ->
FMap.find account (balances prev_state) = FMap.find account (balances new_state).
Proof.
intros * receive_some account account_not_sender account_not_receiver.
contract_simpl.
cbn.
FMap_simpl.
Qed.
receive chain ctx prev_state (Some (transfer to amount)) = Ok (new_state, new_acts) ->
forall account, account <> (ctx_from ctx) -> account <> to ->
FMap.find account (balances prev_state) = FMap.find account (balances new_state).
Proof.
intros * receive_some account account_not_sender account_not_receiver.
contract_simpl.
cbn.
FMap_simpl.
Qed.
If the requirements are met then receive on transfer msg must succeed and
if receive on transfer msg succeeds then requirements must hold
Lemma try_transfer_is_some : forall state chain ctx to amount,
(ctx_amount ctx <= 0)%Z /\
amount <= with_default 0 (FMap.find (ctx_from ctx) (balances state))
<-> isOk (receive chain ctx state (Some (transfer to amount))) = true.
Proof.
intros.
split.
- intros (amount_positive & sender_enough_balance);
contract_simpl; destruct_match eqn:amount_from; auto.
+ now propify.
+ rewrite <- N.ltb_ge in sender_enough_balance.
now setoid_rewrite sender_enough_balance.
- intros receive_some.
contract_simpl.
destruct_match eqn:amount_positive in receive_some;
try now inversion receive_some.
destruct_match eqn:amount_from in receive_some.
+ destruct_match eqn:amount_from_ in amount_from.
* discriminate.
* now propify.
+ now propify.
Qed.
(ctx_amount ctx <= 0)%Z /\
amount <= with_default 0 (FMap.find (ctx_from ctx) (balances state))
<-> isOk (receive chain ctx state (Some (transfer to amount))) = true.
Proof.
intros.
split.
- intros (amount_positive & sender_enough_balance);
contract_simpl; destruct_match eqn:amount_from; auto.
+ now propify.
+ rewrite <- N.ltb_ge in sender_enough_balance.
now setoid_rewrite sender_enough_balance.
- intros receive_some.
contract_simpl.
destruct_match eqn:amount_positive in receive_some;
try now inversion receive_some.
destruct_match eqn:amount_from in receive_some.
+ destruct_match eqn:amount_from_ in amount_from.
* discriminate.
* now propify.
+ now propify.
Qed.
Lemma try_transfer_from_balance_correct : forall prev_state new_state chain ctx from to amount new_acts,
receive chain ctx prev_state (Some (transfer_from from to amount)) = Ok (new_state, new_acts) ->
transfer_balance_update_correct prev_state new_state from to amount = true /\
transfer_from_allowances_update_correct prev_state new_state from ctx.(ctx_from) amount = true.
Proof.
intros * receive_some.
unfold transfer_balance_update_correct,
transfer_from_allowances_update_correct,
get_allowance.
contract_simpl.
rename H0 into from_allowances.
rename H1 into sender_allowance.
rewrite result_of_option_eq_some in from_allowances.
rewrite result_of_option_eq_some in sender_allowance.
propify.
destruct H2 as (sender_enough_allowance & from_enough_balance).
split.
+ (* proof of balance updated correct *)
destruct_address_eq;
destruct (FMap.find from (balances prev_state)) eqn:from_bal_prev;
subst; try (rewrite from_bal_prev || setoid_rewrite from_bal_prev); cbn in *.
* (* case: from = to && find from = Some n && amount <= n *)
FMap_simpl.
now rewrite N.sub_add, N.eqb_refl.
* (* case: from = to && find from = None && amount = 0 *)
apply N.lt_eq_cases in from_enough_balance as []; [lia | subst].
now FMap_simpl.
* (* case: from <> to && find from = Some n && amount <= n *)
FMap_simpl.
rewrite N.sub_add by auto.
now rewrite ?N.eqb_refl.
* (* case: from <> to && find from = None && amount = 0 *)
apply N.lt_eq_cases in from_enough_balance as []; [lia | subst].
FMap_simpl.
apply N.eqb_refl.
+ (* proof of allowances updated correct *)
rewrite from_allowances.
cbn.
setoid_rewrite sender_allowance.
FMap_simpl.
now rewrite N.sub_add.
Qed.
receive chain ctx prev_state (Some (transfer_from from to amount)) = Ok (new_state, new_acts) ->
transfer_balance_update_correct prev_state new_state from to amount = true /\
transfer_from_allowances_update_correct prev_state new_state from ctx.(ctx_from) amount = true.
Proof.
intros * receive_some.
unfold transfer_balance_update_correct,
transfer_from_allowances_update_correct,
get_allowance.
contract_simpl.
rename H0 into from_allowances.
rename H1 into sender_allowance.
rewrite result_of_option_eq_some in from_allowances.
rewrite result_of_option_eq_some in sender_allowance.
propify.
destruct H2 as (sender_enough_allowance & from_enough_balance).
split.
+ (* proof of balance updated correct *)
destruct_address_eq;
destruct (FMap.find from (balances prev_state)) eqn:from_bal_prev;
subst; try (rewrite from_bal_prev || setoid_rewrite from_bal_prev); cbn in *.
* (* case: from = to && find from = Some n && amount <= n *)
FMap_simpl.
now rewrite N.sub_add, N.eqb_refl.
* (* case: from = to && find from = None && amount = 0 *)
apply N.lt_eq_cases in from_enough_balance as []; [lia | subst].
now FMap_simpl.
* (* case: from <> to && find from = Some n && amount <= n *)
FMap_simpl.
rewrite N.sub_add by auto.
now rewrite ?N.eqb_refl.
* (* case: from <> to && find from = None && amount = 0 *)
apply N.lt_eq_cases in from_enough_balance as []; [lia | subst].
FMap_simpl.
apply N.eqb_refl.
+ (* proof of allowances updated correct *)
rewrite from_allowances.
cbn.
setoid_rewrite sender_allowance.
FMap_simpl.
now rewrite N.sub_add.
Qed.
try_transfer_from does not change total supply of tokens
Lemma try_transfer_from_preserves_total_supply : forall prev_state new_state chain ctx from to amount new_acts,
receive chain ctx prev_state (Some (transfer_from from to amount)) = Ok (new_state, new_acts) ->
(total_supply prev_state) = (total_supply new_state).
Proof.
intros * receive_some.
now contract_simpl.
Qed.
receive chain ctx prev_state (Some (transfer_from from to amount)) = Ok (new_state, new_acts) ->
(total_supply prev_state) = (total_supply new_state).
Proof.
intros * receive_some.
now contract_simpl.
Qed.
Lemma try_transfer_from_preserves_other_balances : forall prev_state new_state chain ctx from to amount new_acts,
receive chain ctx prev_state (Some (transfer_from from to amount)) = Ok (new_state, new_acts) ->
forall account, account <> from -> account <> to ->
FMap.find account (balances prev_state) = FMap.find account (balances new_state).
Proof.
intros * receive_some account account_not_from account_not_to.
contract_simpl.
cbn.
FMap_simpl.
Qed.
receive chain ctx prev_state (Some (transfer_from from to amount)) = Ok (new_state, new_acts) ->
forall account, account <> from -> account <> to ->
FMap.find account (balances prev_state) = FMap.find account (balances new_state).
Proof.
intros * receive_some account account_not_from account_not_to.
contract_simpl.
cbn.
FMap_simpl.
Qed.
try_transfer_from only changes allowance map of from
Lemma try_transfer_from_preserves_other_allowances : forall prev_state new_state chain ctx from to amount new_acts,
receive chain ctx prev_state (Some (transfer_from from to amount)) = Ok (new_state, new_acts) ->
forall account, account <> from ->
FMap.find account (allowances prev_state) = FMap.find account (allowances new_state).
Proof.
intros * receive_some account account_not_from.
contract_simpl.
cbn.
FMap_simpl.
Qed.
receive chain ctx prev_state (Some (transfer_from from to amount)) = Ok (new_state, new_acts) ->
forall account, account <> from ->
FMap.find account (allowances prev_state) = FMap.find account (allowances new_state).
Proof.
intros * receive_some account account_not_from.
contract_simpl.
cbn.
FMap_simpl.
Qed.
try_transfer_from only changes allowance of sender
Lemma try_transfer_from_preserves_other_allowance : forall prev_state new_state chain ctx from to amount new_acts,
receive chain ctx prev_state (Some (transfer_from from to amount)) = Ok (new_state, new_acts) ->
forall account, account <> (ctx_from ctx) ->
get_allowance prev_state from account = get_allowance new_state from account.
Proof.
intros * receive_some account account_not_sender.
unfold get_allowance.
contract_simpl.
rewrite result_of_option_eq_some in H0.
rewrite result_of_option_eq_some in H1.
rewrite H0.
cbn.
FMap_simpl.
Qed.
Set Keyed Unification.
receive chain ctx prev_state (Some (transfer_from from to amount)) = Ok (new_state, new_acts) ->
forall account, account <> (ctx_from ctx) ->
get_allowance prev_state from account = get_allowance new_state from account.
Proof.
intros * receive_some account account_not_sender.
unfold get_allowance.
contract_simpl.
rewrite result_of_option_eq_some in H0.
rewrite result_of_option_eq_some in H1.
rewrite H0.
cbn.
FMap_simpl.
Qed.
Set Keyed Unification.
If the requirements are met then receive on transfer_from msg must succeed and
if receive on transfer_from msg succeeds then requirements must hold
Lemma try_transfer_from_is_some : forall state chain ctx from to amount,
let get_allowance_ account := FMap.find account (with_default (@FMap.empty (FMap Address TokenValue) _) (FMap.find from (allowances state))) in
(ctx_amount ctx >? 0)%Z = false ->
isSome (FMap.find from (allowances state)) = true
/\ isSome (get_allowance_ (ctx_from ctx)) = true
/\ amount <= with_default 0 (FMap.find from (balances state))
/\ amount <= with_default 0 (get_allowance_ (ctx_from ctx))
<-> isOk (receive chain ctx state (Some (transfer_from from to amount))) = true.
Proof.
intros * sender_amount_zero.
split; contract_simpl; rewrite sender_amount_zero in *;
unfold get_allowance_; clear get_allowance_; cbn.
- intros (from_allowances_some &
sender_allowance &
from_enough_balance%N.ltb_ge &
sender_enough_allowance%N.ltb_ge).
destruct_match eqn:receive_some; cbn in *; auto.
destruct_match eqn:allowances_ctx in receive_some;
try (apply result_of_option_eq_none in allowances_ctx; now rewrite allowances_ctx in from_allowances_some).
rewrite result_of_option_eq_some in allowances_ctx.
rewrite allowances_ctx in *.
clear from_allowances_some allowances_ctx.
cbn in *.
destruct_match eqn:allowance_ctx in receive_some;
try (apply result_of_option_eq_none in allowance_ctx; now rewrite allowance_ctx in sender_allowance).
rewrite result_of_option_eq_some in allowance_ctx.
rewrite allowance_ctx in *.
clear allowance_ctx sender_allowance.
destruct_match eqn:amount_from in receive_some; try discriminate.
rewrite from_enough_balance in amount_from.
now rewrite sender_enough_allowance in amount_from.
- intros receive_some.
destruct_match eqn:H in receive_some; try discriminate.
destruct_match eqn:allowances_ctx in H; try discriminate.
destruct_match eqn:allowance_ctx in H; try discriminate.
destruct_match eqn:amount_from in H; try discriminate.
cbn in *.
propify.
rewrite result_of_option_eq_some in allowances_ctx.
rewrite result_of_option_eq_some in allowance_ctx.
now rewrite allowances_ctx, allowance_ctx.
Qed.
let get_allowance_ account := FMap.find account (with_default (@FMap.empty (FMap Address TokenValue) _) (FMap.find from (allowances state))) in
(ctx_amount ctx >? 0)%Z = false ->
isSome (FMap.find from (allowances state)) = true
/\ isSome (get_allowance_ (ctx_from ctx)) = true
/\ amount <= with_default 0 (FMap.find from (balances state))
/\ amount <= with_default 0 (get_allowance_ (ctx_from ctx))
<-> isOk (receive chain ctx state (Some (transfer_from from to amount))) = true.
Proof.
intros * sender_amount_zero.
split; contract_simpl; rewrite sender_amount_zero in *;
unfold get_allowance_; clear get_allowance_; cbn.
- intros (from_allowances_some &
sender_allowance &
from_enough_balance%N.ltb_ge &
sender_enough_allowance%N.ltb_ge).
destruct_match eqn:receive_some; cbn in *; auto.
destruct_match eqn:allowances_ctx in receive_some;
try (apply result_of_option_eq_none in allowances_ctx; now rewrite allowances_ctx in from_allowances_some).
rewrite result_of_option_eq_some in allowances_ctx.
rewrite allowances_ctx in *.
clear from_allowances_some allowances_ctx.
cbn in *.
destruct_match eqn:allowance_ctx in receive_some;
try (apply result_of_option_eq_none in allowance_ctx; now rewrite allowance_ctx in sender_allowance).
rewrite result_of_option_eq_some in allowance_ctx.
rewrite allowance_ctx in *.
clear allowance_ctx sender_allowance.
destruct_match eqn:amount_from in receive_some; try discriminate.
rewrite from_enough_balance in amount_from.
now rewrite sender_enough_allowance in amount_from.
- intros receive_some.
destruct_match eqn:H in receive_some; try discriminate.
destruct_match eqn:allowances_ctx in H; try discriminate.
destruct_match eqn:allowance_ctx in H; try discriminate.
destruct_match eqn:amount_from in H; try discriminate.
cbn in *.
propify.
rewrite result_of_option_eq_some in allowances_ctx.
rewrite result_of_option_eq_some in allowance_ctx.
now rewrite allowances_ctx, allowance_ctx.
Qed.
Lemma try_approve_allowance_correct : forall prev_state new_state chain ctx delegate amount new_acts,
receive chain ctx prev_state (Some (approve delegate amount)) = Ok (new_state, new_acts) ->
approve_allowance_update_correct new_state ctx.(ctx_from) delegate amount = true.
Proof.
intros * receive_some.
unfold approve_allowance_update_correct, get_allowance.
contract_simpl.
destruct_match eqn:from_allowance in H;
inversion H; cbn;
FMap_simpl; apply N.eqb_refl.
Qed.
receive chain ctx prev_state (Some (approve delegate amount)) = Ok (new_state, new_acts) ->
approve_allowance_update_correct new_state ctx.(ctx_from) delegate amount = true.
Proof.
intros * receive_some.
unfold approve_allowance_update_correct, get_allowance.
contract_simpl.
destruct_match eqn:from_allowance in H;
inversion H; cbn;
FMap_simpl; apply N.eqb_refl.
Qed.
try_approve does not change total supply of tokens
Lemma try_approve_preserves_total_supply : forall prev_state new_state chain ctx delegate amount new_acts,
receive chain ctx prev_state (Some (approve delegate amount)) = Ok (new_state, new_acts) ->
(total_supply prev_state) = (total_supply new_state).
Proof.
intros * receive_some.
contract_simpl.
destruct_match in H;
now inversion H.
Qed.
receive chain ctx prev_state (Some (approve delegate amount)) = Ok (new_state, new_acts) ->
(total_supply prev_state) = (total_supply new_state).
Proof.
intros * receive_some.
contract_simpl.
destruct_match in H;
now inversion H.
Qed.
try_approve does not change balances
Lemma try_approve_preserves_balances : forall prev_state new_state chain ctx delegate amount new_acts,
receive chain ctx prev_state (Some (approve delegate amount)) = Ok (new_state, new_acts) ->
(balances prev_state) = (balances new_state).
Proof.
intros * receive_some.
contract_simpl.
destruct_match in H;
now inversion H.
Qed.
receive chain ctx prev_state (Some (approve delegate amount)) = Ok (new_state, new_acts) ->
(balances prev_state) = (balances new_state).
Proof.
intros * receive_some.
contract_simpl.
destruct_match in H;
now inversion H.
Qed.
try_approve does not change allowances map of other addresses
Lemma try_approve_preserves_other_allowances : forall prev_state new_state chain ctx delegate amount new_acts,
receive chain ctx prev_state (Some (approve delegate amount)) = Ok (new_state, new_acts) ->
forall account, account <> (ctx_from ctx) ->
FMap.find account (allowances prev_state) = FMap.find account (allowances new_state).
Proof.
intros * receive_some account account_not_sender.
contract_simpl.
destruct_match in H;
inversion H;
cbn; FMap_simpl.
Qed.
receive chain ctx prev_state (Some (approve delegate amount)) = Ok (new_state, new_acts) ->
forall account, account <> (ctx_from ctx) ->
FMap.find account (allowances prev_state) = FMap.find account (allowances new_state).
Proof.
intros * receive_some account account_not_sender.
contract_simpl.
destruct_match in H;
inversion H;
cbn; FMap_simpl.
Qed.
try_approve does not change allowance of other addresses
Lemma try_approve_preserves_other_allowance : forall prev_state new_state chain ctx delegate amount new_acts,
receive chain ctx prev_state (Some (approve delegate amount)) = Ok (new_state, new_acts) ->
forall account, account <> delegate ->
get_allowance prev_state (ctx_from ctx) account = get_allowance new_state (ctx_from ctx) account.
Proof.
intros * receive_some account account_not_delegate.
contract_simpl.
unfold get_allowance.
destruct_match eqn:allowances_from in H;
inversion H;
cbn; FMap_simpl.
Qed.
receive chain ctx prev_state (Some (approve delegate amount)) = Ok (new_state, new_acts) ->
forall account, account <> delegate ->
get_allowance prev_state (ctx_from ctx) account = get_allowance new_state (ctx_from ctx) account.
Proof.
intros * receive_some account account_not_delegate.
contract_simpl.
unfold get_allowance.
destruct_match eqn:allowances_from in H;
inversion H;
cbn; FMap_simpl.
Qed.
If the requirements are met then receive on approve msg must succeed and
if receive on approve msg succeeds then requirements must hold
Lemma try_approve_is_some : forall state chain ctx delegate amount,
(ctx_amount ctx >? 0)%Z = false <-> isOk (receive chain ctx state (Some (approve delegate amount))) = true.
Proof.
split; contract_simpl.
- intros sender_amount_zero.
rewrite sender_amount_zero.
destruct_match eqn:H; auto.
destruct_match in H; discriminate.
- intros receive_some.
now destruct_match in receive_some.
Qed.
(ctx_amount ctx >? 0)%Z = false <-> isOk (receive chain ctx state (Some (approve delegate amount))) = true.
Proof.
split; contract_simpl.
- intros sender_amount_zero.
rewrite sender_amount_zero.
destruct_match eqn:H; auto.
destruct_match in H; discriminate.
- intros receive_some.
now destruct_match in receive_some.
Qed.
EIP20 functions preserve sum of balances
Lemma try_transfer_preserves_balances_sum : forall prev_state new_state chain ctx to amount new_acts,
receive chain ctx prev_state (Some (transfer to amount)) = Ok (new_state, new_acts) ->
(sum_balances prev_state) = (sum_balances new_state).
Proof.
intros * receive_some.
contract_simpl.
propify.
unfold sum_balances. cbn.
now apply sumN_FMap_add_sub.
Qed.
receive chain ctx prev_state (Some (transfer to amount)) = Ok (new_state, new_acts) ->
(sum_balances prev_state) = (sum_balances new_state).
Proof.
intros * receive_some.
contract_simpl.
propify.
unfold sum_balances. cbn.
now apply sumN_FMap_add_sub.
Qed.
Sum of all balances remain the same after processing transfer_from msg
Lemma try_transfer_from_preserves_balances_sum : forall prev_state new_state chain ctx from to amount new_acts,
receive chain ctx prev_state (Some (transfer_from from to amount)) = Ok (new_state, new_acts) ->
(sum_balances prev_state) = (sum_balances new_state).
Proof.
intros * receive_some.
contract_simpl.
propify.
unfold sum_balances. cbn.
now apply sumN_FMap_add_sub.
Qed.
receive chain ctx prev_state (Some (transfer_from from to amount)) = Ok (new_state, new_acts) ->
(sum_balances prev_state) = (sum_balances new_state).
Proof.
intros * receive_some.
contract_simpl.
propify.
unfold sum_balances. cbn.
now apply sumN_FMap_add_sub.
Qed.
Sum of all balances remain the same after approve transfer msg
Lemma try_approve_preserves_balances_sum : forall prev_state new_state chain ctx delegate amount new_acts,
receive chain ctx prev_state (Some (approve delegate amount)) = Ok (new_state, new_acts) ->
(sum_balances prev_state) = (sum_balances new_state).
Proof.
intros * receive_some.
contract_simpl.
destruct_match in H;
now inversion H.
Qed.
receive chain ctx prev_state (Some (approve delegate amount)) = Ok (new_state, new_acts) ->
(sum_balances prev_state) = (sum_balances new_state).
Proof.
intros * receive_some.
contract_simpl.
destruct_match in H;
now inversion H.
Qed.
Lemma outgoing_acts_nil : forall (bstate : ChainState) (caddr : Address),
reachable bstate ->
env_contracts bstate caddr = Some (contract : WeakContract) ->
outgoing_acts bstate caddr = [].
Proof.
intros * reach deployed.
apply (lift_outgoing_acts_nil contract); eauto.
intros.
unfold Blockchain.receive in *.
now eapply EIP20_no_acts.
Qed.
reachable bstate ->
env_contracts bstate caddr = Some (contract : WeakContract) ->
outgoing_acts bstate caddr = [].
Proof.
intros * reach deployed.
apply (lift_outgoing_acts_nil contract); eauto.
intros.
unfold Blockchain.receive in *.
now eapply EIP20_no_acts.
Qed.
Lemma total_supply_eq_init_supply bstate caddr (trace : ChainTrace empty_state bstate) :
env_contracts bstate caddr = Some (contract : WeakContract) ->
exists deploy_info cstate,
deployment_info _ trace caddr = Some deploy_info
/\ contract_state bstate caddr = Some cstate
/\ let init_supply := init_amount deploy_info.(deployment_setup) in
init_supply = total_supply cstate.
Proof.
apply (lift_dep_info_contract_state_prop contract); intros *.
- intros init_some.
now inversion init_some.
- intros IH receive_some.
destruct_message.
+ now apply try_transfer_preserves_total_supply in receive_some.
+ now apply try_transfer_from_preserves_total_supply in receive_some.
+ now apply try_approve_preserves_total_supply in receive_some.
Qed.
env_contracts bstate caddr = Some (contract : WeakContract) ->
exists deploy_info cstate,
deployment_info _ trace caddr = Some deploy_info
/\ contract_state bstate caddr = Some cstate
/\ let init_supply := init_amount deploy_info.(deployment_setup) in
init_supply = total_supply cstate.
Proof.
apply (lift_dep_info_contract_state_prop contract); intros *.
- intros init_some.
now inversion init_some.
- intros IH receive_some.
destruct_message.
+ now apply try_transfer_preserves_total_supply in receive_some.
+ now apply try_transfer_from_preserves_total_supply in receive_some.
+ now apply try_approve_preserves_total_supply in receive_some.
Qed.
Lemma sum_balances_eq_total_supply bstate caddr :
reachable bstate ->
env_contracts bstate caddr = Some (contract : WeakContract) ->
exists cstate,
contract_state bstate caddr = Some cstate
/\ (total_supply cstate) = (sum_balances cstate).
Proof.
intros.
apply (lift_contract_state_prop contract); eauto; intros *.
- intros init_some.
inversion_clear init_some.
unfold sum_balances.
setoid_rewrite FMap.elements_add; auto.
setoid_rewrite FMap.elements_empty. cbn. lia.
- intros IH receive_some.
unfold Blockchain.receive in *.
cbn in *.
destruct_message.
+ now erewrite try_transfer_preserves_balances_sum,
try_transfer_preserves_total_supply in IH.
+ now erewrite try_transfer_from_preserves_balances_sum,
try_transfer_from_preserves_total_supply in IH.
+ now erewrite try_approve_preserves_balances_sum,
try_approve_preserves_total_supply in IH.
Qed.
End Theories.
reachable bstate ->
env_contracts bstate caddr = Some (contract : WeakContract) ->
exists cstate,
contract_state bstate caddr = Some cstate
/\ (total_supply cstate) = (sum_balances cstate).
Proof.
intros.
apply (lift_contract_state_prop contract); eauto; intros *.
- intros init_some.
inversion_clear init_some.
unfold sum_balances.
setoid_rewrite FMap.elements_add; auto.
setoid_rewrite FMap.elements_empty. cbn. lia.
- intros IH receive_some.
unfold Blockchain.receive in *.
cbn in *.
destruct_message.
+ now erewrite try_transfer_preserves_balances_sum,
try_transfer_preserves_total_supply in IH.
+ now erewrite try_transfer_from_preserves_balances_sum,
try_transfer_from_preserves_total_supply in IH.
+ now erewrite try_approve_preserves_balances_sum,
try_approve_preserves_total_supply in IH.
Qed.
End Theories.