Contents:
Library ConCert.Examples.CIS1.CIS1Spec
Concordium's CIS1
- Specifications of transfer, balanceOf and operatorUpdate.
- Simple properties of operatorUpdate.
- Our main result: we prove that transfer, balanceOf and operatorUpdate preserve the sum of all balances for all token ids. The properties hold for any contract that satisfies the CIS1 specification defined in this formalization.
- Concordium serialization.
- The spec of operatorOf.
- Logging the events (logs are currently not supported by ConCert).
- Metadata.
- updateOperator is a bit stricter than in the actual standard: it does not allow for updating non-existing accounts.
- the standard allows for multiple tokens on a single contract, which makes it possible to define both fungible and non-fungible tokens;
- the transfers happen in batch mode.
- definitions that correspond to the standard directly are prefixed with "CIS1:"
- important remarks are prefixed with "NOTE:"
From ConCert.Utils Require Import Automation.
From ConCert.Execution Require Import Blockchain.
From ConCert.Execution Require Import Serializable.
From ConCert.Execution Require Import Monad.
From ConCert.Execution Require Import ContractCommon.
From ConCert.Examples.CIS1 Require Import CIS1Utils.
From Coq Require Import Basics.
From Coq Require Import List.
From Coq Require Import ZArith.
Import ListNotations.
Import RemoveProperties.
CIS1:
Abstract types of messages, storage (the contract's state) and token ids
ReceiveHookParameter ::= (id: TokenID) (amount: TokenAmount) (from: Address)
(contract: ContractName) (data: AdditionalData).
Module Type CIS1Types.
Parameter Msg : forall `{ChainBase}, Type.
Parameter Storage : forall `{ChainBase}, Type.
Parameter Msg : forall `{ChainBase}, Type.
Parameter Storage : forall `{ChainBase}, Type.
NOTE: In CIS1 it's an n-byte sequence, where 0 ≤ n ≤ 256.
We model it as an arbitrary serializable type with decidable equality
Parameter TokenID : Type.
Axiom serializable_token_id : Serializable TokenID.
Parameter token_id_eqb : TokenID -> TokenID -> bool.
Axiom token_id_eqb_spec :
forall (a b : TokenID), Bool.reflect (a = b) (token_id_eqb a b).
End CIS1Types.
Module ReceiveHook (cis1_types : CIS1Types).
Import cis1_types.
#[export]
Existing Instance serializable_token_id.
Axiom serializable_token_id : Serializable TokenID.
Parameter token_id_eqb : TokenID -> TokenID -> bool.
Axiom token_id_eqb_spec :
forall (a b : TokenID), Bool.reflect (a = b) (token_id_eqb a b).
End CIS1Types.
Module ReceiveHook (cis1_types : CIS1Types).
Import cis1_types.
#[export]
Existing Instance serializable_token_id.
NOTE: there is no notion of the contract name in ConCert; AdditionalData is not
handled at the moment
All addresses owning tokens must support the following interface, since all receiving
addresses are notified with a receive hook. The rest of the functionality is captured
by the other_msg constructor
Inductive CIS1ReceiverMsg (Msg : Type) `{Serializable Msg} `{ChainBase} :=
| CIS1_receiver_receive_hook : receive_hook_params -> CIS1ReceiverMsg Msg
| CIS1_receiver_other_msg : Msg -> CIS1ReceiverMsg Msg.
End ReceiveHook.
| CIS1_receiver_receive_hook : receive_hook_params -> CIS1ReceiverMsg Msg
| CIS1_receiver_other_msg : Msg -> CIS1ReceiverMsg Msg.
End ReceiveHook.
Views
Module Type CIS1View (cis1_types : CIS1Types).
Import cis1_types.
Section CISViewDefs.
Context `{ChainBase}.
Parameter get_balance_opt : Storage -> TokenID -> Address -> option TokenAmount.
Parameter get_operators : Storage -> Address -> list Address.
Parameter get_owners : Storage -> TokenID -> list Address.
Axiom get_owners_no_dup : forall st token_id, NoDup (get_owners st token_id).
Import cis1_types.
Section CISViewDefs.
Context `{ChainBase}.
Parameter get_balance_opt : Storage -> TokenID -> Address -> option TokenAmount.
Parameter get_operators : Storage -> Address -> list Address.
Parameter get_owners : Storage -> TokenID -> list Address.
Axiom get_owners_no_dup : forall st token_id, NoDup (get_owners st token_id).
Owners are determined by their balances
Axiom get_owners_balances : forall st owner token_id,
In owner (get_owners st token_id) <->
exists balance, get_balance_opt st token_id owner = Some balance.
Parameter token_id_exists : Storage -> TokenID -> bool.
End CISViewDefs.
End CIS1View.
In owner (get_owners st token_id) <->
exists balance, get_balance_opt st token_id owner = Some balance.
Parameter token_id_exists : Storage -> TokenID -> bool.
End CISViewDefs.
End CIS1View.
Definition of extra functions, based on CIS1View
Module CIS1ViewExtra (cis1_types : CIS1Types) (cis1_view : CIS1View cis1_types).
Import cis1_types.
Import cis1_view.
Definition get_balance `{ChainBase} : Storage -> TokenID -> Address -> option TokenAmount :=
fun st token_id addr => if token_id_exists st token_id then
match get_balance_opt st token_id addr with
| Some bal => Some bal
| None => Some 0
end
else None.
Definition get_balance_total `{ChainBase}
(st : Storage)
(token_id : TokenID)
(p : token_id_exists st token_id = true)
(addr : Address) : TokenAmount :=
let o := get_balance st token_id addr in
match o as o' return (o' = o -> _) with
| Some bal => fun _ => bal
| None => fun heq =>
False_rect _ (ltac:(intros; subst o; unfold get_balance in *; rewrite p in *;
destruct (get_balance_opt st token_id addr); congruence))
end eq_refl.
End CIS1ViewExtra.
Import cis1_types.
Import cis1_view.
Definition get_balance `{ChainBase} : Storage -> TokenID -> Address -> option TokenAmount :=
fun st token_id addr => if token_id_exists st token_id then
match get_balance_opt st token_id addr with
| Some bal => Some bal
| None => Some 0
end
else None.
Definition get_balance_total `{ChainBase}
(st : Storage)
(token_id : TokenID)
(p : token_id_exists st token_id = true)
(addr : Address) : TokenAmount :=
let o := get_balance st token_id addr in
match o as o' return (o' = o -> _) with
| Some bal => fun _ => bal
| None => fun heq =>
False_rect _ (ltac:(intros; subst o; unfold get_balance in *; rewrite p in *;
destruct (get_balance_opt st token_id addr); congruence))
end eq_refl.
End CIS1ViewExtra.
The module below specifies an abstract interface of the CIS1 token along with the
properties that must be satisfied by each entry point required by the standard.
Module CIS1Axioms (cis1_types : CIS1Types) (cis1_view : CIS1View cis1_types).
Import cis1_types.
Import cis1_view.
Module VExtra := CIS1ViewExtra cis1_types cis1_view.
Import VExtra.
Module RH := ReceiveHook cis1_types.
Import RH.
Import cis1_types.
Import cis1_view.
Module VExtra := CIS1ViewExtra cis1_types cis1_view.
Import VExtra.
Module RH := ReceiveHook cis1_types.
Import RH.
Contract functions
Record CIS1_transfer_data `{ChainBase} :=
{ cis1_td_token_id : TokenID;
cis1_td_amount : TokenAmount;
cis1_td_from : Address;
cis1_td_to : Address }.
Record CIS1_transfer_params `{ChainBase} :=
{ cis_tr_transfers : list CIS1_transfer_data }.
Inductive CIS1_updateOperator_kind :=
cis1_ou_remove_operator
| cis1_ou_add_operator.
Record CIS1_updateOperator_update `{ChainBase} :=
{ cis1_ou_update_kind : CIS1_updateOperator_kind;
cis1_ou_operator_address : Address }.
Record CIS1_updateOperator_params `{ChainBase} :=
{ cis1_ou_params : list CIS1_updateOperator_update }.
Record CIS1_balanceOf_query `{ChainBase} :=
{ cis1_bo_query_token_id : TokenID;
cis1_bo_query_address : Address }.
Record CIS1_balanceOf_params `{ChainBase} :=
{ cis1_bo_query : list CIS1_balanceOf_query;
cis1_bo_result_address : Address;
cis1_bo_result_address_is_contract : address_is_contract cis1_bo_result_address = true}.
{ cis1_td_token_id : TokenID;
cis1_td_amount : TokenAmount;
cis1_td_from : Address;
cis1_td_to : Address }.
Record CIS1_transfer_params `{ChainBase} :=
{ cis_tr_transfers : list CIS1_transfer_data }.
Inductive CIS1_updateOperator_kind :=
cis1_ou_remove_operator
| cis1_ou_add_operator.
Record CIS1_updateOperator_update `{ChainBase} :=
{ cis1_ou_update_kind : CIS1_updateOperator_kind;
cis1_ou_operator_address : Address }.
Record CIS1_updateOperator_params `{ChainBase} :=
{ cis1_ou_params : list CIS1_updateOperator_update }.
Record CIS1_balanceOf_query `{ChainBase} :=
{ cis1_bo_query_token_id : TokenID;
cis1_bo_query_address : Address }.
Record CIS1_balanceOf_params `{ChainBase} :=
{ cis1_bo_query : list CIS1_balanceOf_query;
cis1_bo_result_address : Address;
cis1_bo_result_address_is_contract : address_is_contract cis1_bo_result_address = true}.
CIS1: A smart contract implementing CIS1 MUST export three functions transfer, updateOperator and balanceOf.
Inductive CIS1_entry_points `{ChainBase} :=
| CIS1_transfer (params : CIS1_transfer_params)
| CIS1_updateOperator (params : CIS1_updateOperator_params)
| CIS1_balanceOf (params : CIS1_balanceOf_params).
Transfer
Parameter
Definition transfer_to `{ChainBase} : CIS1_transfer_params -> list (TokenID * Address) :=
fun params => map (fun x => (x.(cis1_td_token_id), x.(cis1_td_to))) params.(cis_tr_transfers).
Definition transfer_from `{ChainBase} : CIS1_transfer_params -> list (TokenID * Address) :=
fun params => map (fun x => (x.(cis1_td_token_id), x.(cis1_td_from))) params.(cis_tr_transfers).
Definition get_receive_hook_params `{ChainBase} (params : list CIS1_transfer_data)
: list (Address * receive_hook_params) :=
map (fun x => (x.(cis1_td_to), (x.(cis1_td_token_id), x.(cis1_td_amount), x.(cis1_td_from)))) params.
fun params => map (fun x => (x.(cis1_td_token_id), x.(cis1_td_to))) params.(cis_tr_transfers).
Definition transfer_from `{ChainBase} : CIS1_transfer_params -> list (TokenID * Address) :=
fun params => map (fun x => (x.(cis1_td_token_id), x.(cis1_td_from))) params.(cis_tr_transfers).
Definition get_receive_hook_params `{ChainBase} (params : list CIS1_transfer_data)
: list (Address * receive_hook_params) :=
map (fun x => (x.(cis1_td_to), (x.(cis1_td_token_id), x.(cis1_td_amount), x.(cis1_td_from)))) params.
Definition transfer_single_spec
`{ChainBase}
(prev_st next_st : Storage)
(token_id : TokenID)
(p : token_id_exists prev_st token_id = true)
(q : token_id_exists next_st token_id = true)
(owner : Address)
(from : Address)
(to : Address)
(amount : TokenAmount) : Prop :=
let prev_from := get_balance_total prev_st token_id p from in
let next_from := get_balance_total next_st token_id q from in
let prev_to := get_balance_total prev_st token_id p to in
let next_to := get_balance_total next_st token_id q to in
`{ChainBase}
(prev_st next_st : Storage)
(token_id : TokenID)
(p : token_id_exists prev_st token_id = true)
(q : token_id_exists next_st token_id = true)
(owner : Address)
(from : Address)
(to : Address)
(amount : TokenAmount) : Prop :=
let prev_from := get_balance_total prev_st token_id p from in
let next_from := get_balance_total next_st token_id q from in
let prev_to := get_balance_total prev_st token_id p to in
let next_to := get_balance_total next_st token_id q to in
(forall addr, addr <> from ->
addr <> to ->
get_balance_opt next_st token_id addr = get_balance_opt prev_st token_id addr) /\
addr <> to ->
get_balance_opt next_st token_id addr = get_balance_opt prev_st token_id addr) /\
The balances of all other tokens that are not equal to token_id remain unchanged for all addresses
(forall addr other_token_id, other_token_id <> token_id ->
get_balance_opt next_st other_token_id addr = get_balance_opt prev_st other_token_id addr) /\
get_balance_opt next_st other_token_id addr = get_balance_opt prev_st other_token_id addr) /\
Token ids are preserved by a single transfer
CIS1: Let operator be an operator of the address owner. A transfer of any amount
of a token type from an address owner sent by an address operator MUST be
executed as if the transfer was sent by owner.
CIS1: A transfer MUST non-strictly decrease the balance of the from address and
non-strictly increase the balance of the to address.
CIS1: A transfer of some amount of a token type MUST only transfer the exact amount of
the given token type between balances.
CIS1: The list of transfers MUST be executed in order.
Fixpoint compose_transfers
`{ChainBase}
(init_st : Storage)
(final_st : Storage)
(params : list CIS1_transfer_data)
(single_transfer :
forall (prev_st next_st : Storage)
(params : CIS1_transfer_data),
token_id_exists prev_st params.(cis1_td_token_id) = true ->
token_id_exists next_st params.(cis1_td_token_id) = true -> Prop)
: Prop :=
match params with
| [] => init_st = final_st
| pr :: ps =>
`{ChainBase}
(init_st : Storage)
(final_st : Storage)
(params : list CIS1_transfer_data)
(single_transfer :
forall (prev_st next_st : Storage)
(params : CIS1_transfer_data),
token_id_exists prev_st params.(cis1_td_token_id) = true ->
token_id_exists next_st params.(cis1_td_token_id) = true -> Prop)
: Prop :=
match params with
| [] => init_st = final_st
| pr :: ps =>
NOTE: we require that for each transfer, the updated state st becomes the initial state for the next transfer
exists (st : Storage)
(p: token_id_exists init_st pr.(cis1_td_token_id) = true)
(q : token_id_exists st pr.(cis1_td_token_id) = true),
single_transfer init_st st pr p q /\ compose_transfers st final_st ps single_transfer
end.
(p: token_id_exists init_st pr.(cis1_td_token_id) = true)
(q : token_id_exists st pr.(cis1_td_token_id) = true),
single_transfer init_st st pr p q /\ compose_transfers st final_st ps single_transfer
end.
A receive hook call is valid if the call parameters are deserialised to a CIS1_receiver_receive_hook
constructor with appropriate data
Definition is_valid_receive_hook `{cb : ChainBase} (p : receive_hook_params) (serialized_params : SerializedValue) : Prop :=
exists (Msg : Type) (sMsg : Serializable Msg) (f : Msg -> receive_hook_params) (msg : Msg),
deserialize serialized_params = Some msg /\ f msg = p.
exists (Msg : Type) (sMsg : Serializable Msg) (f : Msg -> receive_hook_params) (msg : Msg),
deserialize serialized_params = Some msg /\ f msg = p.
A specification for the batch transfer
Record transfer_spec `{ChainBase}
(ctx : ContractCallContext)
(params : CIS1_transfer_params)
(prev_st next_st : Storage)
(ret_ops : list ActionBody) : Prop :=
{
transfer_dec_inc :
compose_transfers prev_st next_st params.(cis_tr_transfers)
(fun st1 st2 x p q =>
transfer_single_spec
st1
st2
x.(cis1_td_token_id) p q
ctx.(ctx_from)
x.(cis1_td_from)
x.(cis1_td_to)
x.(cis1_td_amount));
(ctx : ContractCallContext)
(params : CIS1_transfer_params)
(prev_st next_st : Storage)
(ret_ops : list ActionBody) : Prop :=
{
transfer_dec_inc :
compose_transfers prev_st next_st params.(cis_tr_transfers)
(fun st1 st2 x p q =>
transfer_single_spec
st1
st2
x.(cis1_td_token_id) p q
ctx.(ctx_from)
x.(cis1_td_from)
x.(cis1_td_to)
x.(cis1_td_amount));
CIS1: A transfer of any amount of a token type to a contract address MUST call receive
hook function on the receiving smart contract with a receive hook parameter.
We consider only transfers to addresses that are contracts
let transfers_to_contracts := filter (fun x => address_is_contract x.(cis1_td_to)) params.(cis_tr_transfers) in
Forall2 (fun op '(to_addr, params) =>
exists val, op = act_call to_addr 0%Z val /\ is_valid_receive_hook params val)
ret_ops (get_receive_hook_params transfers_to_contracts)
}.
Forall2 (fun op '(to_addr, params) =>
exists val, op = act_call to_addr 0%Z val /\ is_valid_receive_hook params val)
ret_ops (get_receive_hook_params transfers_to_contracts)
}.
updateOperator
Parameter
Requirements
Definition updateOperator_single_spec `{ChainBase} (ctx : ContractCallContext) (prev_st next_st : Storage) (p : CIS1_updateOperator_update) : Prop :=
match p.(cis1_ou_update_kind) with
| cis1_ou_remove_operator =>
let addr := p.(cis1_ou_operator_address) in
match p.(cis1_ou_update_kind) with
| cis1_ou_remove_operator =>
let addr := p.(cis1_ou_operator_address) in
All operators, apart from addr remain the same in both states
(forall addr0, addr0 <> addr ->
In addr0 (get_operators prev_st ctx.(ctx_from)) <->
In addr0 (get_operators next_st ctx.(ctx_from))) /\
In addr0 (get_operators prev_st ctx.(ctx_from)) <->
In addr0 (get_operators next_st ctx.(ctx_from))) /\
An operator "to remove" is removed (not present) for the caller
~ In addr (get_operators next_st ctx.(ctx_from))
| cis1_ou_add_operator =>
let addr := p.(cis1_ou_operator_address) in
| cis1_ou_add_operator =>
let addr := p.(cis1_ou_operator_address) in
All operators, apart from addr remain the same in both states
(forall addr0, addr0 <> addr ->
In addr0 (get_operators prev_st ctx.(ctx_from)) <->
In addr0 (get_operators next_st ctx.(ctx_from))) /\
(* an operator "to add" is recorded for the caller *)
In addr (get_operators next_st ctx.(ctx_from))
end.
In addr0 (get_operators prev_st ctx.(ctx_from)) <->
In addr0 (get_operators next_st ctx.(ctx_from))) /\
(* an operator "to add" is recorded for the caller *)
In addr (get_operators next_st ctx.(ctx_from))
end.
CIS1: The list of updates MUST be executed in order.
Fixpoint compose_uptadeOperator_specs `{ChainBase} (ctx : ContractCallContext) (st final_st : Storage) (updates : list CIS1_updateOperator_update) :=
match updates with
| [] => st = final_st
| p :: ps => exists next_st, updateOperator_single_spec ctx st next_st p /\
compose_uptadeOperator_specs ctx next_st final_st ps
end.
match updates with
| [] => st = final_st
| p :: ps => exists next_st, updateOperator_single_spec ctx st next_st p /\
compose_uptadeOperator_specs ctx next_st final_st ps
end.
A specification of the batch operator update
Record updateOperator_spec `{ChainBase}
(ctx : ContractCallContext)
(params : CIS1_updateOperator_params)
(prev_st next_st : Storage)
(ret_ops : list ActionBody) :=
{ updateOperator_token_ids_preserved :
forall token_id,
token_id_exists prev_st token_id = token_id_exists next_st token_id;
updateOperator_balances_preserved : forall addr token_id,
get_balance_opt prev_st token_id addr = get_balance_opt next_st token_id addr;
updateOperator_add_remove :
compose_uptadeOperator_specs ctx prev_st next_st params.(cis1_ou_params)
}.
(ctx : ContractCallContext)
(params : CIS1_updateOperator_params)
(prev_st next_st : Storage)
(ret_ops : list ActionBody) :=
{ updateOperator_token_ids_preserved :
forall token_id,
token_id_exists prev_st token_id = token_id_exists next_st token_id;
updateOperator_balances_preserved : forall addr token_id,
get_balance_opt prev_st token_id addr = get_balance_opt next_st token_id addr;
updateOperator_add_remove :
compose_uptadeOperator_specs ctx prev_st next_st params.(cis1_ou_params)
}.
balanceOf
Parameter
Requirements
Definition get_balances `{ChainBase} (st : Storage) (params : CIS1_balanceOf_params) : option balanceOf_callback_type :=
monad_map
(fun q =>
let addr := q.(cis1_bo_query_address) in
let token_id := q.(cis1_bo_query_token_id) in
do balance <- get_balance st token_id addr;
Some (token_id, addr, balance)) params.(cis1_bo_query).
Record balanceOf_spec
`{ChainBase}
(params : CIS1_balanceOf_params)
(prev_st next_st : Storage)
(ret_ops : list ActionBody) : Prop :=
{ balanceOf_operators_preserved :
forall addr, get_operators next_st addr = get_operators prev_st addr;
balanceOf_token_ids_preserved :
forall token_id,
token_id_exists prev_st token_id = token_id_exists next_st token_id;
balanceOf_balances_preserved :
forall token_id addr, get_balance_opt next_st token_id addr = get_balance_opt prev_st token_id addr;
monad_map
(fun q =>
let addr := q.(cis1_bo_query_address) in
let token_id := q.(cis1_bo_query_token_id) in
do balance <- get_balance st token_id addr;
Some (token_id, addr, balance)) params.(cis1_bo_query).
Record balanceOf_spec
`{ChainBase}
(params : CIS1_balanceOf_params)
(prev_st next_st : Storage)
(ret_ops : list ActionBody) : Prop :=
{ balanceOf_operators_preserved :
forall addr, get_operators next_st addr = get_operators prev_st addr;
balanceOf_token_ids_preserved :
forall token_id,
token_id_exists prev_st token_id = token_id_exists next_st token_id;
balanceOf_balances_preserved :
forall token_id addr, get_balance_opt next_st token_id addr = get_balance_opt prev_st token_id addr;
NOTE: It's assumed that the receiving contract accepts messages of type balanceOf_callback_type
balanceOf_callback :
match get_balances prev_st params with
| Some query_results =>
let serialized_query_results := serialize query_results in
let op := act_call params.(cis1_bo_result_address) 0%Z serialized_query_results in
ret_ops = [op]
| None => False
end
}.
End CIS1Axioms.
match get_balances prev_st params with
| Some query_results =>
let serialized_query_results := serialize query_results in
let op := act_call params.(cis1_bo_result_address) 0%Z serialized_query_results in
ret_ops = [op]
| None => False
end
}.
End CIS1Axioms.
Full specification of receive
Module Type CIS1ReceiveSpec (cis1_types : CIS1Types) (cis1_view : CIS1View cis1_types).
Import cis1_types.
Import cis1_view.
Module cis1_axioms := CIS1Axioms cis1_types cis1_view.
Import cis1_axioms.
Import cis1_types.
Import cis1_view.
Module cis1_axioms := CIS1Axioms cis1_types cis1_view.
Import cis1_axioms.
We require that it is possible to convert between the entry point and the input data specified
by the standard and the actual type of messages accepted by a particular contract
Parameter get_CIS1_entry_point : forall `{ChainBase}, Msg -> option CIS1_entry_points.
Parameter get_contract_msg : forall `{ChainBase}, CIS1_entry_points -> Msg.
Parameter get_contract_msg : forall `{ChainBase}, CIS1_entry_points -> Msg.
This axiom captures the intuition that a contact that implements CIS1 can handle at least
CIS1_entry_points.
Axiom left_inverse_get_CIS1_entry_point :
forall `{ChainBase} (entry_point : CIS1_entry_points),
get_CIS1_entry_point (get_contract_msg entry_point) = Some entry_point.
Parameter contract_receive : forall `{ChainBase}, Chain -> ContractCallContext -> Storage -> option Msg -> option (Storage * list ActionBody).
forall `{ChainBase} (entry_point : CIS1_entry_points),
get_CIS1_entry_point (get_contract_msg entry_point) = Some entry_point.
Parameter contract_receive : forall `{ChainBase}, Chain -> ContractCallContext -> Storage -> option Msg -> option (Storage * list ActionBody).
The contract's receive function satisfies the CIS1 standard if for each entry points it
satisfies the corresponding specification.
Axiom receive_spec :
forall `{ChainBase}
(chain : Chain)
(ctx : ContractCallContext)
(entry : CIS1_entry_points)
(msg : Msg)
(prev_st next_st : Storage)
(ops : list ActionBody),
get_CIS1_entry_point msg = Some entry ->
contract_receive chain ctx prev_st (Some msg) = Some (next_st, ops) ->
match entry with
| CIS1_transfer params => transfer_spec ctx params prev_st next_st ops
| CIS1_updateOperator params => updateOperator_spec ctx params prev_st next_st ops
| CIS1_balanceOf params => balanceOf_spec params prev_st next_st ops
end.
End CIS1ReceiveSpec.
forall `{ChainBase}
(chain : Chain)
(ctx : ContractCallContext)
(entry : CIS1_entry_points)
(msg : Msg)
(prev_st next_st : Storage)
(ops : list ActionBody),
get_CIS1_entry_point msg = Some entry ->
contract_receive chain ctx prev_st (Some msg) = Some (next_st, ops) ->
match entry with
| CIS1_transfer params => transfer_spec ctx params prev_st next_st ops
| CIS1_updateOperator params => updateOperator_spec ctx params prev_st next_st ops
| CIS1_balanceOf params => balanceOf_spec params prev_st next_st ops
end.
End CIS1ReceiveSpec.
Module CIS1Operators (cis1_types : CIS1Types) (cis1_view : CIS1View cis1_types).
Module cis1_axioms := CIS1Axioms cis1_types cis1_view.
Import cis1_axioms.
Sanity checks for the batch operator update spec
NOTE: the properties could be extended further, if more guarantees about operator updates are
required from the standard
Import cis1_types cis1_view cis1_axioms.
Import Lia.
Lemma compose_updateOperator_add_add :
forall `{ChainBase} (ctx : ContractCallContext)
(prev_st : Storage) (next_st : Storage) (addr1 addr2 : Address),
let add_addr1 := {| cis1_ou_update_kind := cis1_ou_add_operator;
cis1_ou_operator_address := addr1 |} in
let add_addr2 := {| cis1_ou_update_kind := cis1_ou_add_operator;
cis1_ou_operator_address := addr2 |} in
compose_uptadeOperator_specs ctx prev_st next_st [add_addr1; add_addr2] ->
In addr1 (get_operators next_st ctx.(ctx_from)).
Proof.
intros ? ? ? ? ? ? ? ? H. simpl in *.
destruct H as [st1 [Hst1 [st2 [Hst2 Heq]]]]. subst. cbn in *.
destruct Hst1. destruct Hst2 as [H2 ?].
destruct (address_eqb_spec addr1 addr2); subst; auto.
apply H2; auto.
Qed.
Lemma compose_updateOperator_add_remove_same :
forall `{ChainBase} (ctx : ContractCallContext)
(prev_st : Storage) (next_st : Storage) (addr : Address),
let add_addr := {| cis1_ou_update_kind := cis1_ou_add_operator;
cis1_ou_operator_address := addr |} in
let remove_addr := {| cis1_ou_update_kind := cis1_ou_remove_operator;
cis1_ou_operator_address := addr |} in
compose_uptadeOperator_specs ctx prev_st next_st [add_addr; remove_addr] ->
~ In addr (get_operators next_st ctx.(ctx_from)).
Proof.
intros ? ? ? ? ? ? ? H. simpl in *.
destruct H as [st1 [Hst1 [st2 [Hst2 Heq]]]]. subst. cbn in *.
destruct Hst2.
assumption.
Qed.
Lemma compose_updateOperator_remove_one_remove_another :
forall `{ChainBase} (ctx : ContractCallContext)
(prev_st : Storage) (next_st : Storage) (addr1 addr2 : Address),
addr1 <> addr2 ->
let remove_addr := {| cis1_ou_update_kind := cis1_ou_remove_operator;
cis1_ou_operator_address := addr1 |} in
let add_addr := {| cis1_ou_update_kind := cis1_ou_add_operator;
cis1_ou_operator_address := addr2 |} in
compose_uptadeOperator_specs ctx prev_st next_st [remove_addr; add_addr] ->
~ In addr1 (get_operators next_st ctx.(ctx_from)).
Proof.
intros ? ? ? ? ? ? Hneq ? ? H. simpl in *.
destruct H as [st1 [Hst1 [st2 [Hst2 Heq]]]]. subst. cbn in *.
destruct Hst1. destruct Hst2 as [H2 ?].
intro. specialize (H2 _ Hneq). easy.
Qed.
End CIS1Operators.
Module CIS1Balances (cis1_types : CIS1Types) (cis1_view : CIS1View cis1_types).
Module cis1_axioms := CIS1Axioms cis1_types cis1_view.
Import cis1_axioms.
Module cis1_axioms := CIS1Axioms cis1_types cis1_view.
Import cis1_axioms.
In this module we prove properties related to the preservation of the sum of all balances for
all token ids.
These properties follow directly from the specification. That means, in particular, that all
the contracts that satisfy the specification will automatically satisfy all the properties we
prove here.
Get the balance and return zero if get_balance returns None
Definition get_balance_default `{ChainBase} : Storage -> TokenID -> Address -> TokenAmount :=
fun st token_id addr => match get_balance st token_id addr with
| Some amount => amount
| None => 0
end.
fun st token_id addr => match get_balance st token_id addr with
| Some amount => amount
| None => 0
end.
We sum up all the balances for a given token_id for a list of owners
Definition sum_balances `{ChainBase} (st : Storage) (token_id : TokenID) (owners : list Address) :=
fold_right (fun addr s => get_balance_default st token_id addr + s) 0 owners.
fold_right (fun addr s => get_balance_default st token_id addr + s) 0 owners.
This is an important lemma that is used to prove the main result about the sum of balances.
The lemma states that we can split the sum of all balances into two parts: the balance of a particular owner (which can be zero) and the sum of all other balances (with owner removed).
Lemma remove_owner `{ChainBase} st token_id (owners : list Address) (owner : Address) :
In owner owners \/ get_balance_default st token_id owner = 0 ->
NoDup owners ->
sum_balances st token_id owners = get_balance_default st token_id owner + sum_balances st token_id (remove addr_eq_dec owner owners).
Proof.
intros Hin.
destruct Hin as [Hin | Hbal].
generalize dependent owner.
-induction owners; intros owner Hin Hnodup.
+ inversion Hin.
+ inversion Hin; subst; clear Hin.
* simpl.
destruct (addr_eq_dec owner owner); try congruence.
inversion Hnodup; subst; clear Hnodup.
now rewrite not_in_remove_same.
* inversion Hnodup; subst; clear Hnodup.
simpl.
destruct (addr_eq_dec owner a).
** easy.
** simpl. rewrite (IHowners owner); auto; lia.
- rewrite Hbal; cbn.
induction owners; intros Hnodup; auto; inversion Hnodup; subst; clear Hnodup.
simpl. destruct (addr_eq_dec owner a); subst; simpl; easy.
Qed.
#[export]
Hint Resolve remove_In not_in_remove_same not_in_remove remove_remove neq_not_removed : hints.
#[export]
Hint Resolve remove_extensional NoDup_remove In_remove : hints.
In owner owners \/ get_balance_default st token_id owner = 0 ->
NoDup owners ->
sum_balances st token_id owners = get_balance_default st token_id owner + sum_balances st token_id (remove addr_eq_dec owner owners).
Proof.
intros Hin.
destruct Hin as [Hin | Hbal].
generalize dependent owner.
-induction owners; intros owner Hin Hnodup.
+ inversion Hin.
+ inversion Hin; subst; clear Hin.
* simpl.
destruct (addr_eq_dec owner owner); try congruence.
inversion Hnodup; subst; clear Hnodup.
now rewrite not_in_remove_same.
* inversion Hnodup; subst; clear Hnodup.
simpl.
destruct (addr_eq_dec owner a).
** easy.
** simpl. rewrite (IHowners owner); auto; lia.
- rewrite Hbal; cbn.
induction owners; intros Hnodup; auto; inversion Hnodup; subst; clear Hnodup.
simpl. destruct (addr_eq_dec owner a); subst; simpl; easy.
Qed.
#[export]
Hint Resolve remove_In not_in_remove_same not_in_remove remove_remove neq_not_removed : hints.
#[export]
Hint Resolve remove_extensional NoDup_remove In_remove : hints.
An important lemma stating that the sum of balances in two states is the same for the same owners, if the balances in the two states agree.
This lemma is used to make a connection between the sum of balances and the properties of transfer given by the specification
Lemma sum_of_balances_eq_extensional `{ChainBase} owners1 owners2 prev_st next_st token_id :
NoDup owners1 ->
NoDup owners2 ->
(forall addr, In addr owners1 <-> In addr owners2) ->
(forall addr, In addr owners1 -> get_balance_default next_st token_id addr = get_balance_default prev_st token_id addr) ->
sum_balances next_st token_id owners1 = sum_balances prev_st token_id owners2.
Proof.
intros.
erewrite sum_of_balances_eq by eauto.
apply sum_balances_extensional; auto.
Qed.
Lemma get_balance_opt_default `{ChainBase} next_st prev_st token_id addr :
token_id_exists prev_st token_id = token_id_exists next_st token_id ->
get_balance_opt next_st token_id addr = get_balance_opt prev_st token_id addr ->
get_balance_default next_st token_id addr = get_balance_default prev_st token_id addr.
Proof.
intros Hids Hopt.
unfold get_balance_default,get_balance.
rewrite Hids.
destruct (token_id_exists next_st token_id); auto.
destruct (get_balance_opt next_st token_id addr) eqn:Heq1;
destruct (get_balance_opt prev_st token_id addr) eqn:Heq2; auto;
inversion H; try congruence.
Qed.
NoDup owners1 ->
NoDup owners2 ->
(forall addr, In addr owners1 <-> In addr owners2) ->
(forall addr, In addr owners1 -> get_balance_default next_st token_id addr = get_balance_default prev_st token_id addr) ->
sum_balances next_st token_id owners1 = sum_balances prev_st token_id owners2.
Proof.
intros.
erewrite sum_of_balances_eq by eauto.
apply sum_balances_extensional; auto.
Qed.
Lemma get_balance_opt_default `{ChainBase} next_st prev_st token_id addr :
token_id_exists prev_st token_id = token_id_exists next_st token_id ->
get_balance_opt next_st token_id addr = get_balance_opt prev_st token_id addr ->
get_balance_default next_st token_id addr = get_balance_default prev_st token_id addr.
Proof.
intros Hids Hopt.
unfold get_balance_default,get_balance.
rewrite Hids.
destruct (token_id_exists next_st token_id); auto.
destruct (get_balance_opt next_st token_id addr) eqn:Heq1;
destruct (get_balance_opt prev_st token_id addr) eqn:Heq2; auto;
inversion H; try congruence.
Qed.
The owners are the same in two states if the balances agree. We generalize the statement to cover the case when we ignore certain addresses given by ignore_addrs.
Lemma same_owners_remove_all `{ChainBase} token_id ignore_addrs next_st prev_st :
(forall addr1, ~ In addr1 ignore_addrs ->
get_balance_opt next_st token_id addr1 = get_balance_opt prev_st token_id addr1) ->
(forall addr1, In addr1 (remove_all addr_eq_dec ignore_addrs (get_owners next_st token_id))
<-> In addr1 (remove_all addr_eq_dec ignore_addrs (get_owners prev_st token_id))).
Proof.
intros H0 addr1.
assert (Hdec : forall (a1 a2 : Address), a1 = a2 \/ a1 <> a2).
{ intros. destruct (addr_eq_dec a1 a2); auto. }
split.
+ intros Hin.
destruct (ListDec.In_decidable Hdec addr1 ignore_addrs) as [Hin_addrs | Hnotin_addrs]; subst.
* exfalso.
assert (Hall : Forall (fun x =>~In x (remove_all addr_eq_dec ignore_addrs ((get_owners next_st token_id)))) ignore_addrs)
by apply remove_all_In.
rewrite Forall_forall in Hall; easy.
* specialize (H0 _ Hnotin_addrs).
destruct (get_balance_opt next_st token_id addr1) eqn:Hnext; inversion Hnext.
** apply remove_all_not_in_to_remove; auto. apply get_owners_balances; eauto.
** apply In_remove_all in Hin; auto.
apply get_owners_balances in Hin; destruct Hin; congruence.
+ intros Hin.
destruct (ListDec.In_decidable Hdec addr1 ignore_addrs) as [Hin_addrs | Hnotin_addrs]; subst.
* exfalso.
assert (Hall : Forall (fun x =>~In x (remove_all addr_eq_dec ignore_addrs ((get_owners prev_st token_id)))) ignore_addrs)
by apply remove_all_In.
rewrite Forall_forall in Hall; easy.
* specialize (H0 _ Hnotin_addrs).
destruct (get_balance_opt next_st token_id addr1) eqn:Hnext; inversion Hnext.
** apply remove_all_not_in_to_remove; auto. apply get_owners_balances; eauto.
** apply In_remove_all in Hin; auto.
apply get_owners_balances in Hin; destruct Hin; congruence.
Qed.
(forall addr1, ~ In addr1 ignore_addrs ->
get_balance_opt next_st token_id addr1 = get_balance_opt prev_st token_id addr1) ->
(forall addr1, In addr1 (remove_all addr_eq_dec ignore_addrs (get_owners next_st token_id))
<-> In addr1 (remove_all addr_eq_dec ignore_addrs (get_owners prev_st token_id))).
Proof.
intros H0 addr1.
assert (Hdec : forall (a1 a2 : Address), a1 = a2 \/ a1 <> a2).
{ intros. destruct (addr_eq_dec a1 a2); auto. }
split.
+ intros Hin.
destruct (ListDec.In_decidable Hdec addr1 ignore_addrs) as [Hin_addrs | Hnotin_addrs]; subst.
* exfalso.
assert (Hall : Forall (fun x =>~In x (remove_all addr_eq_dec ignore_addrs ((get_owners next_st token_id)))) ignore_addrs)
by apply remove_all_In.
rewrite Forall_forall in Hall; easy.
* specialize (H0 _ Hnotin_addrs).
destruct (get_balance_opt next_st token_id addr1) eqn:Hnext; inversion Hnext.
** apply remove_all_not_in_to_remove; auto. apply get_owners_balances; eauto.
** apply In_remove_all in Hin; auto.
apply get_owners_balances in Hin; destruct Hin; congruence.
+ intros Hin.
destruct (ListDec.In_decidable Hdec addr1 ignore_addrs) as [Hin_addrs | Hnotin_addrs]; subst.
* exfalso.
assert (Hall : Forall (fun x =>~In x (remove_all addr_eq_dec ignore_addrs ((get_owners prev_st token_id)))) ignore_addrs)
by apply remove_all_In.
rewrite Forall_forall in Hall; easy.
* specialize (H0 _ Hnotin_addrs).
destruct (get_balance_opt next_st token_id addr1) eqn:Hnext; inversion Hnext.
** apply remove_all_not_in_to_remove; auto. apply get_owners_balances; eauto.
** apply In_remove_all in Hin; auto.
apply get_owners_balances in Hin; destruct Hin; congruence.
Qed.
Any address either in the list of owners, or owns zero tokens.
Lemma in_owners_or_zero_balance_default `{ChainBase} st token_id owner :
In owner (get_owners st token_id) \/ get_balance_default st token_id owner = 0.
Proof.
assert (Hdec : forall (a1 a2 : Address), a1 = a2 \/ a1 <> a2).
{ intros. destruct (addr_eq_dec a1 a2); auto. }
destruct (ListDec.In_decidable Hdec owner (get_owners st token_id)) as [Hin_addrs | Hnotin_addrs]; subst; auto.
right. unfold get_balance_default,get_balance.
destruct (token_id_exists st token_id); auto.
cbn.
destruct (get_balance_opt st token_id owner) eqn:Heq; auto.
assert (In owner (get_owners st token_id)) by (apply get_owners_balances; eauto).
easy.
Qed.
#[export]
Hint Resolve in_owners_or_zero_balance_default get_owners_no_dup : hints.
Lemma get_balance_total_get_balance_default `{ChainBase} st token_id p owner :
get_balance_total st token_id p owner = get_balance_default st token_id owner.
Proof.
unfold get_balance_total, get_balance_default, get_balance. rewrite p. cbn.
now destruct (get_balance_opt st token_id _).
Qed.
#[export]
Hint Constructors transfer_spec : hints.
In owner (get_owners st token_id) \/ get_balance_default st token_id owner = 0.
Proof.
assert (Hdec : forall (a1 a2 : Address), a1 = a2 \/ a1 <> a2).
{ intros. destruct (addr_eq_dec a1 a2); auto. }
destruct (ListDec.In_decidable Hdec owner (get_owners st token_id)) as [Hin_addrs | Hnotin_addrs]; subst; auto.
right. unfold get_balance_default,get_balance.
destruct (token_id_exists st token_id); auto.
cbn.
destruct (get_balance_opt st token_id owner) eqn:Heq; auto.
assert (In owner (get_owners st token_id)) by (apply get_owners_balances; eauto).
easy.
Qed.
#[export]
Hint Resolve in_owners_or_zero_balance_default get_owners_no_dup : hints.
Lemma get_balance_total_get_balance_default `{ChainBase} st token_id p owner :
get_balance_total st token_id p owner = get_balance_default st token_id owner.
Proof.
unfold get_balance_total, get_balance_default, get_balance. rewrite p. cbn.
now destruct (get_balance_opt st token_id _).
Qed.
#[export]
Hint Constructors transfer_spec : hints.
We can recover a statement for the whole "batch" of transfers from the transfers spec where
the same property is assumed for each transfer in the batch
Lemma transfer_token_ids_preserved `{ChainBase} ctx transfers prev_st next_st ops :
let params := Build_CIS1_transfer_params _ transfers in
transfer_spec ctx params prev_st next_st ops ->
forall token_id,
token_id_exists prev_st token_id = token_id_exists next_st token_id.
Proof.
generalize dependent prev_st.
generalize dependent ops.
cbn.
induction transfers.
- intros ops prev_st spec token_id.
destruct spec. cbn in *; now subst.
- intros ops prev_st spec token_id.
destruct spec as [Htrans Hcalls]. cbn in *.
destruct Htrans as [st [? [? [Hsingle ?]]]].
transitivity (token_id_exists st token_id).
* now destruct Hsingle.
* destruct (address_is_contract (cis1_td_to a)).
** inversion Hcalls; subst.
eapply IHtransfers; eauto with hints.
** eapply IHtransfers; eauto with hints.
Qed.
let params := Build_CIS1_transfer_params _ transfers in
transfer_spec ctx params prev_st next_st ops ->
forall token_id,
token_id_exists prev_st token_id = token_id_exists next_st token_id.
Proof.
generalize dependent prev_st.
generalize dependent ops.
cbn.
induction transfers.
- intros ops prev_st spec token_id.
destruct spec. cbn in *; now subst.
- intros ops prev_st spec token_id.
destruct spec as [Htrans Hcalls]. cbn in *.
destruct Htrans as [st [? [? [Hsingle ?]]]].
transitivity (token_id_exists st token_id).
* now destruct Hsingle.
* destruct (address_is_contract (cis1_td_to a)).
** inversion Hcalls; subst.
eapply IHtransfers; eauto with hints.
** eapply IHtransfers; eauto with hints.
Qed.
The balances of all token-address pairs NOT mentioned in the transfer batch remain unchanged
Lemma transfer_other_balances_preserved `{ChainBase} ctx transfers prev_st next_st ops :
let params := Build_CIS1_transfer_params _ transfers in
transfer_spec ctx params prev_st next_st ops ->
forall addr token_id,
~ In (token_id, addr) (transfer_from params) ->
~ In (token_id, addr) (transfer_to params) ->
get_balance_opt prev_st token_id addr = get_balance_opt next_st token_id addr.
Proof.
generalize dependent next_st.
generalize dependent prev_st.
generalize dependent ops.
induction transfers.
- cbn; intros ops prev_st next_st spec addr token_id.
destruct spec. cbn in *; now subst.
- intros ops prev_st next_st ? spec addr token_id Hfrom Hto.
destruct spec as [Htr Hcalls].
destruct Htr as [st [p [q [Hsingle Htrs]]]].
assert ((token_id, addr) <> (a.(cis1_td_token_id), a.(cis1_td_from)) /\ ~ (In (token_id,addr) (transfer_from params))) by firstorder.
assert ((token_id, addr) <> (a.(cis1_td_token_id), a.(cis1_td_to)) /\ ~ (In (token_id,addr) (transfer_to params))) by firstorder.
clear Hto. clear Hfrom.
transitivity (get_balance_opt st token_id addr).
+ destruct Hsingle as [Hbal_not_addr [Hbal_other_tokens [? ?]]].
cbn in *.
destruct (token_id_eqb_spec token_id a.(cis1_td_token_id)).
* assert (addr <> a.(cis1_td_to)) by easy.
assert (addr <> a.(cis1_td_from)) by easy.
subst. symmetry. now apply Hbal_not_addr.
* now symmetry.
+ cbn in *.
destruct (address_is_contract (cis1_td_to a));
inversion Hcalls;
eapply IHtransfers; now subst; firstorder.
Qed.
let params := Build_CIS1_transfer_params _ transfers in
transfer_spec ctx params prev_st next_st ops ->
forall addr token_id,
~ In (token_id, addr) (transfer_from params) ->
~ In (token_id, addr) (transfer_to params) ->
get_balance_opt prev_st token_id addr = get_balance_opt next_st token_id addr.
Proof.
generalize dependent next_st.
generalize dependent prev_st.
generalize dependent ops.
induction transfers.
- cbn; intros ops prev_st next_st spec addr token_id.
destruct spec. cbn in *; now subst.
- intros ops prev_st next_st ? spec addr token_id Hfrom Hto.
destruct spec as [Htr Hcalls].
destruct Htr as [st [p [q [Hsingle Htrs]]]].
assert ((token_id, addr) <> (a.(cis1_td_token_id), a.(cis1_td_from)) /\ ~ (In (token_id,addr) (transfer_from params))) by firstorder.
assert ((token_id, addr) <> (a.(cis1_td_token_id), a.(cis1_td_to)) /\ ~ (In (token_id,addr) (transfer_to params))) by firstorder.
clear Hto. clear Hfrom.
transitivity (get_balance_opt st token_id addr).
+ destruct Hsingle as [Hbal_not_addr [Hbal_other_tokens [? ?]]].
cbn in *.
destruct (token_id_eqb_spec token_id a.(cis1_td_token_id)).
* assert (addr <> a.(cis1_td_to)) by easy.
assert (addr <> a.(cis1_td_from)) by easy.
subst. symmetry. now apply Hbal_not_addr.
* now symmetry.
+ cbn in *.
destruct (address_is_contract (cis1_td_to a));
inversion Hcalls;
eapply IHtransfers; now subst; firstorder.
Qed.
If the properties of the single transfer holds (the transfer succeeds), then
we can conclude that if has been enough tokens for the transfer.
Lemma transfer_single_spec_sufficient_funds `{ChainBase}
prev_st next_st token_id from to amount owner
(p : token_id_exists prev_st token_id = true)
(q : token_id_exists next_st token_id = true)
(spec : transfer_single_spec prev_st next_st token_id p q owner from to amount) :
get_balance_total prev_st token_id p from >= amount.
Proof.
destruct spec as [? [? [? [? [Htransfer Hself_transfer]]]]].
destruct (address_eqb_spec from to) as [| Hneq].
* subst. specialize (Hself_transfer eq_refl). lia.
* specialize (Htransfer Hneq). lia.
Qed.
prev_st next_st token_id from to amount owner
(p : token_id_exists prev_st token_id = true)
(q : token_id_exists next_st token_id = true)
(spec : transfer_single_spec prev_st next_st token_id p q owner from to amount) :
get_balance_total prev_st token_id p from >= amount.
Proof.
destruct spec as [? [? [? [? [Htransfer Hself_transfer]]]]].
destruct (address_eqb_spec from to) as [| Hneq].
* subst. specialize (Hself_transfer eq_refl). lia.
* specialize (Htransfer Hneq). lia.
Qed.
An important lemma for the main result. The spec for a single transfer ensures that for a
particular token_id the sum of balances is preserved for all owners for one transfer
of an amount between from and to.
Lemma transfer_single_spec_preserves_balances `{ChainBase}
prev_st next_st token_id owner0 from to amount
(p : token_id_exists prev_st token_id = true)
(q : token_id_exists next_st token_id = true)
(spec : transfer_single_spec prev_st next_st token_id p q owner0 from to amount) :
let owners1 := get_owners prev_st token_id in
let owners2 := get_owners next_st token_id in
sum_balances next_st token_id owners2 =
sum_balances prev_st token_id owners1.
Proof.
intros ??.
destruct spec as [Hother_balances [? [? [_ [Htransfer Hself_transfer]]]]].
unfold transfer_single_spec in *.
destruct (address_eqb_spec from to) as [Haddr | Haddr].
+ subst.
rewrite remove_owner with (st := prev_st) (owner := to)
by (subst owners1; auto with hints).
rewrite remove_owner with (st := next_st) (owner := to)
by (subst owners2; auto with hints).
assert (HH :
sum_balances next_st token_id (remove addr_eq_dec to owners2) =
sum_balances prev_st token_id (remove addr_eq_dec to owners1)).
{ apply sum_of_balances_eq_extensional; subst owners2; subst owners1; eauto with hints.
intros addr.
apply same_owners_remove_all with (ignore_addrs := [to]); intros; cbn in *; auto.
intros addr Haddr. unfold is_true in *.
apply get_balance_opt_default; try congruence.
destruct (address_eqb_spec addr to); subst. exfalso; apply (remove_In _ _ _ Haddr).
eauto. }
repeat rewrite get_balance_total_get_balance_default in Htransfer, Hself_transfer.
specialize (Hself_transfer eq_refl).
lia.
+ rewrite remove_owner with (st := prev_st) (owner := from)
by (subst owners1; auto with hints).
rewrite remove_owner with (st := prev_st) (owner := to)
by (assert (In to owners1 \/ get_balance_default prev_st token_id to = 0); subst owners1; auto with hints; destruct_or_hyps; auto with hints).
rewrite remove_owner with (st := next_st) (owner := from)
by (subst owners2; auto with hints).
rewrite remove_owner with (st := next_st) (owner := to)
by (assert (In to owners2 \/ get_balance_default next_st token_id to = 0);
subst owners2; auto with hints; destruct_or_hyps; auto with hints).
specialize (Htransfer Haddr). destruct Htransfer as [Hfrom Hto].
repeat rewrite get_balance_total_get_balance_default in Hfrom,Hto.
rewrite Hfrom. rewrite Hto.
assert (HH :
sum_balances next_st token_id (remove addr_eq_dec to (remove addr_eq_dec from owners2)) =
sum_balances prev_st token_id (remove addr_eq_dec to (remove addr_eq_dec from owners1))).
{ apply sum_of_balances_eq_extensional; subst owners2; subst owners1; eauto with hints.
apply same_owners_remove_all with (ignore_addrs := [to; from]); intros; cbn in *; intuition.
intros addr Haddr0. unfold is_true in *.
apply get_balance_opt_default; try congruence.
destruct (address_eqb_spec addr to); subst. exfalso; apply (remove_In _ _ _ Haddr0).
destruct (address_eqb_spec addr from); subst. apply In_remove in Haddr0; auto. exfalso; apply (remove_In _ _ _ Haddr0).
eauto. }
lia.
Qed.
prev_st next_st token_id owner0 from to amount
(p : token_id_exists prev_st token_id = true)
(q : token_id_exists next_st token_id = true)
(spec : transfer_single_spec prev_st next_st token_id p q owner0 from to amount) :
let owners1 := get_owners prev_st token_id in
let owners2 := get_owners next_st token_id in
sum_balances next_st token_id owners2 =
sum_balances prev_st token_id owners1.
Proof.
intros ??.
destruct spec as [Hother_balances [? [? [_ [Htransfer Hself_transfer]]]]].
unfold transfer_single_spec in *.
destruct (address_eqb_spec from to) as [Haddr | Haddr].
+ subst.
rewrite remove_owner with (st := prev_st) (owner := to)
by (subst owners1; auto with hints).
rewrite remove_owner with (st := next_st) (owner := to)
by (subst owners2; auto with hints).
assert (HH :
sum_balances next_st token_id (remove addr_eq_dec to owners2) =
sum_balances prev_st token_id (remove addr_eq_dec to owners1)).
{ apply sum_of_balances_eq_extensional; subst owners2; subst owners1; eauto with hints.
intros addr.
apply same_owners_remove_all with (ignore_addrs := [to]); intros; cbn in *; auto.
intros addr Haddr. unfold is_true in *.
apply get_balance_opt_default; try congruence.
destruct (address_eqb_spec addr to); subst. exfalso; apply (remove_In _ _ _ Haddr).
eauto. }
repeat rewrite get_balance_total_get_balance_default in Htransfer, Hself_transfer.
specialize (Hself_transfer eq_refl).
lia.
+ rewrite remove_owner with (st := prev_st) (owner := from)
by (subst owners1; auto with hints).
rewrite remove_owner with (st := prev_st) (owner := to)
by (assert (In to owners1 \/ get_balance_default prev_st token_id to = 0); subst owners1; auto with hints; destruct_or_hyps; auto with hints).
rewrite remove_owner with (st := next_st) (owner := from)
by (subst owners2; auto with hints).
rewrite remove_owner with (st := next_st) (owner := to)
by (assert (In to owners2 \/ get_balance_default next_st token_id to = 0);
subst owners2; auto with hints; destruct_or_hyps; auto with hints).
specialize (Htransfer Haddr). destruct Htransfer as [Hfrom Hto].
repeat rewrite get_balance_total_get_balance_default in Hfrom,Hto.
rewrite Hfrom. rewrite Hto.
assert (HH :
sum_balances next_st token_id (remove addr_eq_dec to (remove addr_eq_dec from owners2)) =
sum_balances prev_st token_id (remove addr_eq_dec to (remove addr_eq_dec from owners1))).
{ apply sum_of_balances_eq_extensional; subst owners2; subst owners1; eauto with hints.
apply same_owners_remove_all with (ignore_addrs := [to; from]); intros; cbn in *; intuition.
intros addr Haddr0. unfold is_true in *.
apply get_balance_opt_default; try congruence.
destruct (address_eqb_spec addr to); subst. exfalso; apply (remove_In _ _ _ Haddr0).
destruct (address_eqb_spec addr from); subst. apply In_remove in Haddr0; auto. exfalso; apply (remove_In _ _ _ Haddr0).
eauto. }
lia.
Qed.
Main result
Lemma transfer_preserves_sum_of_balances `{ChainBase} ctx prev_st next_st ops transfers token_id
(spec : transfer_spec ctx (Build_CIS1_transfer_params _ transfers) prev_st next_st ops) :
let owners1 := get_owners prev_st token_id in
let owners2 := get_owners next_st token_id in
sum_balances prev_st token_id owners1 = sum_balances next_st token_id owners2.
Proof.
destruct spec as [Htr Hcalls].
generalize dependent prev_st.
generalize dependent next_st.
generalize dependent ops.
induction transfers; intros ops ? next_st prev_st Htr ? ?.
- cbn in *. now subst.
- cbn in *.
destruct Htr as [st [p [q [Hsingle Htrs]]]].
transitivity (sum_balances st token_id (get_owners st token_id)).
+ destruct (token_id_eqb_spec token_id a.(cis1_td_token_id)).
* subst. symmetry.
now eapply transfer_single_spec_preserves_balances with (next_st := st).
* destruct Hsingle as [? [HH [? ?]]].
apply sum_of_balances_eq_extensional; subst owners2; subst owners1; eauto with hints.
** intros. repeat rewrite get_owners_balances.
now rewrite HH.
** intros.
apply get_balance_opt_default; symmetry; auto.
+ cbn in *.
destruct (address_is_contract (cis1_td_to a));
inversion Hcalls;
eapply IHtransfers; now subst; firstorder.
Qed.
Lemma balanceOf_preserves_sum_of_balances `{ChainBase} params prev_st next_st token_id ops
(spec : balanceOf_spec params prev_st next_st ops) :
let owners1 := get_owners prev_st token_id in
let owners2 := get_owners next_st token_id in
sum_balances next_st token_id owners2 =
sum_balances prev_st token_id owners1.
Proof.
intros ??.
destruct spec as [H1 H2 H3 H4]. clear H4.
apply sum_of_balances_eq_extensional; subst owners1 owners2; auto with hints.
intros. now apply same_owners_remove_all with (ignore_addrs := []).
intros. now apply get_balance_opt_default.
Qed.
Lemma updateOperator_preserves_sum_of_balances `{ChainBase} params prev_st next_st token_id ops ctx
(spec : updateOperator_spec ctx params prev_st next_st ops) :
let owners1 := get_owners prev_st token_id in
let owners2 := get_owners next_st token_id in
sum_balances next_st token_id owners2 =
sum_balances prev_st token_id owners1.
Proof.
intros ??.
destruct spec as [H1 H2 H3].
apply sum_of_balances_eq_extensional; subst owners1 owners2; auto with hints.
intros. now apply same_owners_remove_all with (ignore_addrs := []).
intros. now apply get_balance_opt_default.
Qed.
End CIS1Balances.