-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
3 changed files
with
285 additions
and
8 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,266 @@ | ||
scilla_version 0 | ||
|
||
(***************************************************) | ||
(* Associated library *) | ||
(***************************************************) | ||
import IntUtils | ||
library ZRC2Interop | ||
|
||
let one_msg = | ||
fun (msg : Message) => | ||
let nil_msg = Nil {Message} in | ||
Cons {Message} msg nil_msg | ||
|
||
let two_msgs = | ||
fun (msg1 : Message) => | ||
fun (msg2 : Message) => | ||
let msgs_tmp = one_msg msg2 in | ||
Cons {Message} msg1 msgs_tmp | ||
|
||
(* Error events *) | ||
type Error = | ||
| CodeIsSender | ||
| CodeInsufficientFunds | ||
| CodeInsufficientAllowance | ||
| CodeNotOwner | ||
|
||
let make_error = | ||
fun (result : Error) => | ||
let result_code = | ||
match result with | ||
| CodeIsSender => Int32 -1 | ||
| CodeInsufficientFunds => Int32 -2 | ||
| CodeInsufficientAllowance => Int32 -3 | ||
| CodeNotOwner => Int32 -4 | ||
end | ||
in | ||
{ _exception : "Error"; code : result_code } | ||
|
||
let zero = Uint128 0 | ||
|
||
(* Dummy user-defined ADT *) | ||
type Unit = | ||
| Unit | ||
|
||
let get_val = | ||
fun (some_val: Option Uint128) => | ||
match some_val with | ||
| Some val => val | ||
| None => zero | ||
end | ||
|
||
(***************************************************) | ||
(* The contract definition *) | ||
(***************************************************) | ||
|
||
contract ZRC2Interop | ||
( | ||
contract_owner: ByStr20, | ||
name : String, | ||
symbol: String, | ||
decimals: Uint32, | ||
init_supply : Uint128 | ||
) | ||
|
||
(* Mutable fields *) | ||
|
||
field total_supply : Uint128 = init_supply | ||
|
||
field balances: Map ByStr20 Uint128 | ||
= let emp_map = Emp ByStr20 Uint128 in | ||
builtin put emp_map contract_owner init_supply | ||
|
||
field allowances: Map ByStr20 (Map ByStr20 Uint128) | ||
= Emp ByStr20 (Map ByStr20 Uint128) | ||
|
||
(**************************************) | ||
(* Procedures *) | ||
(**************************************) | ||
|
||
procedure ThrowError(err : Error) | ||
e = make_error err; | ||
throw e | ||
end | ||
|
||
procedure IsOwner(address: ByStr20) | ||
is_owner = builtin eq contract_owner address; | ||
match is_owner with | ||
| True => | ||
| False => | ||
err = CodeNotOwner; | ||
ThrowError err | ||
end | ||
end | ||
|
||
procedure IsNotSender(address: ByStr20) | ||
is_sender = builtin eq _origin address; | ||
match is_sender with | ||
| True => | ||
err = CodeIsSender; | ||
ThrowError err | ||
| False => | ||
end | ||
end | ||
|
||
procedure AuthorizedMint(recipient: ByStr20, amount: Uint128) | ||
o_recipient_bal <- balances[recipient]; | ||
bal = get_val o_recipient_bal; | ||
new_balance = builtin add amount bal; | ||
balances[recipient] := new_balance; | ||
current_total_supply <- total_supply; | ||
new_total_supply = builtin add current_total_supply amount; | ||
total_supply := new_total_supply; | ||
e = {_eventname: "Minted"; minter: _origin; recipient: recipient; amount: amount}; | ||
event e | ||
end | ||
|
||
procedure AuthorizedBurnIfSufficientBalance(from: ByStr20, amount: Uint128) | ||
o_get_bal <- balances[from]; | ||
bal = get_val o_get_bal; | ||
can_burn = uint128_le amount bal; | ||
match can_burn with | ||
| True => | ||
(* Subtract amount from from *) | ||
new_balance = builtin sub bal amount; | ||
balances[from] := new_balance; | ||
current_total_supply <- total_supply; | ||
new_total_supply = builtin sub current_total_supply amount; | ||
total_supply := new_total_supply; | ||
e = {_eventname: "Burnt"; burner: _origin; burn_account: from; amount: amount}; | ||
event e | ||
| False => | ||
err = CodeInsufficientFunds; | ||
ThrowError err | ||
end | ||
end | ||
|
||
procedure AuthorizedMoveIfSufficientBalance(from: ByStr20, to: ByStr20, amount: Uint128) | ||
o_from_bal <- balances[from]; | ||
bal = get_val o_from_bal; | ||
can_do = uint128_le amount bal; | ||
match can_do with | ||
| True => | ||
(* Subtract amount from from and add it to to address *) | ||
new_from_bal = builtin sub bal amount; | ||
balances[from] := new_from_bal; | ||
(* Adds amount to to address *) | ||
get_to_bal <- balances[to]; | ||
new_to_bal = match get_to_bal with | ||
| Some bal => builtin add bal amount | ||
| None => amount | ||
end; | ||
balances[to] := new_to_bal | ||
| False => | ||
(* Balance not sufficient *) | ||
err = CodeInsufficientFunds; | ||
ThrowError err | ||
end | ||
end | ||
|
||
(***************************************) | ||
(* Transitions *) | ||
(***************************************) | ||
|
||
(* @dev: Mint new tokens. Only contract_owner can mint. *) | ||
(* @param recipient: Address of the recipient whose balance is to increase. *) | ||
(* @param amount: Number of tokens to be minted. *) | ||
transition Mint(recipient: ByStr20, amount: Uint128) | ||
IsOwner _origin; | ||
AuthorizedMint recipient amount; | ||
(* Prevent sending to a contract address that does not support transfers of token *) | ||
msg_to_recipient = {_tag : "RecipientAcceptMint"; _recipient : recipient; _amount : zero; | ||
minter : _origin; recipient : recipient; amount : amount}; | ||
msg_to_sender = {_tag : "MintSuccessCallBack"; _recipient : _origin; _amount : zero; | ||
minter : _origin; recipient : recipient; amount : amount}; | ||
msgs = two_msgs msg_to_recipient msg_to_sender; | ||
send msgs | ||
end | ||
|
||
(* @dev: Burn existing tokens. Only contract_owner can burn. *) | ||
(* @param burn_account: Address of the token_owner whose balance is to decrease. *) | ||
(* @param amount: Number of tokens to be burned. *) | ||
transition Burn(burn_account: ByStr20, amount: Uint128) | ||
IsOwner _origin; | ||
AuthorizedBurnIfSufficientBalance burn_account amount; | ||
msg_to_sender = {_tag : "BurnSuccessCallBack"; _recipient : _origin; _amount : zero; | ||
burner : _origin; burn_account : burn_account; amount : amount}; | ||
msgs = one_msg msg_to_sender; | ||
send msgs | ||
end | ||
|
||
(* @dev: Increase the allowance of an approved_spender over the caller tokens. Only token_owner allowed to invoke. *) | ||
(* param spender: Address of the designated approved_spender. *) | ||
(* param amount: Number of tokens to be increased as allowance for the approved_spender. *) | ||
transition IncreaseAllowance(spender: ByStr20, amount: Uint128) | ||
IsNotSender spender; | ||
some_current_allowance <- allowances[_origin][spender]; | ||
current_allowance = get_val some_current_allowance; | ||
new_allowance = builtin add current_allowance amount; | ||
allowances[_origin][spender] := new_allowance; | ||
e = {_eventname : "IncreasedAllowance"; token_owner : _origin; spender: spender; new_allowance : new_allowance}; | ||
event e | ||
end | ||
|
||
(* @dev: Decrease the allowance of an approved_spender over the caller tokens. Only token_owner allowed to invoke. *) | ||
(* param spender: Address of the designated approved_spender. *) | ||
(* param amount: Number of tokens to be decreased as allowance for the approved_spender. *) | ||
transition DecreaseAllowance(spender: ByStr20, amount: Uint128) | ||
IsNotSender spender; | ||
some_current_allowance <- allowances[_origin][spender]; | ||
current_allowance = get_val some_current_allowance; | ||
new_allowance = | ||
let amount_le_allowance = uint128_le amount current_allowance in | ||
match amount_le_allowance with | ||
| True => builtin sub current_allowance amount | ||
| False => zero | ||
end; | ||
allowances[_origin][spender] := new_allowance; | ||
e = {_eventname : "DecreasedAllowance"; token_owner : _origin; spender: spender; new_allowance : new_allowance}; | ||
event e | ||
end | ||
|
||
(* @dev: Moves an amount tokens from _origin to the recipient. Used by token_owner. *) | ||
(* @dev: Balance of recipient will increase. Balance of _origin will decrease. *) | ||
(* @param to: Address of the recipient whose balance is increased. *) | ||
(* @param amount: Amount of tokens to be sent. *) | ||
transition Transfer(to: ByStr20, amount: Uint128) | ||
AuthorizedMoveIfSufficientBalance _origin to amount; | ||
e = {_eventname : "TransferSuccess"; sender : _origin; recipient : to; amount : amount}; | ||
event e; | ||
(* Prevent sending to a contract address that does not support transfers of token *) | ||
msg_to_recipient = {_tag : "RecipientAcceptTransfer"; _recipient : to; _amount : zero; | ||
sender : _origin; recipient : to; amount : amount}; | ||
msg_to_sender = {_tag : "TransferSuccessCallBack"; _recipient : _origin; _amount : zero; | ||
sender : _origin; recipient : to; amount : amount}; | ||
msgs = two_msgs msg_to_recipient msg_to_sender; | ||
send msgs | ||
end | ||
|
||
(* @dev: Move a given amount of tokens from one address to another using the allowance mechanism. The caller must be an approved_spender. *) | ||
(* @dev: Balance of recipient will increase. Balance of token_owner will decrease. *) | ||
(* @param from: Address of the token_owner whose balance is decreased. *) | ||
(* @param to: Address of the recipient whose balance is increased. *) | ||
(* @param amount: Amount of tokens to be transferred. *) | ||
transition TransferFrom(from: ByStr20, to: ByStr20, amount: Uint128) | ||
o_spender_allowed <- allowances[from][_origin]; | ||
allowed = get_val o_spender_allowed; | ||
can_do = uint128_le amount allowed; | ||
match can_do with | ||
| True => | ||
AuthorizedMoveIfSufficientBalance from to amount; | ||
e = {_eventname : "TransferFromSuccess"; initiator : _origin; sender : from; recipient : to; amount : amount}; | ||
event e; | ||
new_allowed = builtin sub allowed amount; | ||
allowances[from][_origin] := new_allowed; | ||
(* Prevent sending to a contract address that does not support transfers of token *) | ||
msg_to_recipient = {_tag: "RecipientAcceptTransferFrom"; _recipient : to; _amount: zero; | ||
initiator: _origin; sender : from; recipient: to; amount: amount}; | ||
msg_to_sender = {_tag: "TransferFromSuccessCallBack"; _recipient: _origin; _amount: zero; | ||
initiator: _origin; sender: from; recipient: to; amount: amount}; | ||
msgs = two_msgs msg_to_recipient msg_to_sender; | ||
send msgs | ||
| False => | ||
err = CodeInsufficientAllowance; | ||
ThrowError err | ||
end | ||
end |