Below we describe ERC777-K, our formal specification of a refined variant of the ERC777 standard token in K. Here we assume the reader is already familiar with K, ERC20, and basic formal specification notions and notations. We strongly recommend the reader who is not already familiar with the K formal specification of ERC20 to consult ERC20-K.
Our objective is to define ERC777-K in such a way that it can be imported by an arbitrary programming language semantics, whose programs can then make use of the ERC777-K functions. Our immediate reason for doing so is to test ERC777-K programmatically. But this design choice can have other advantages, too. For example, it can be seen as a way to plug-and-play ERC777-K support to your favorite language, provided you have a K semantics for it.
As is customary for a K definition, we divide it into 2 modules:
ERC777-SYNTAX for the syntax and ERC777 for the actual semantic rules.
We start by defining the module ERC777-SYNTAX.
It contains the syntactic definitions for the entities defined in the
ERC777 standard, such as the syntactic categories with their relationships,
the functions and the events.
Additional, auxiliary syntactic definitions are included in module ERC777.
module ERC777-SYNTAX
imports DOMAINS
ERC777 refers to three major data types: uint256, address and bytes.
Type uint256 is used for token values, and corresponds to ValueType in
ERC777-K.
(We use ValueType here to avoid name collision with variables called Value.)
Type address corresponds to Address here.
These two types are natural numbers, so we model them as K unbounded integers
using the builtin sort Int.
The third essential type, bytes, is essentially used to pass messages across
various operations.
It corresponds to Data in ERC777-K, modeled as String.
syntax Address ::= Int
syntax ValueType ::= Int
syntax Data ::= String
Additionally, ERC777 mentions the type string, which is modeled by K's
String, and bool, which is modeled by K's Bool.
Next we define expression sorts that are later used to define ERC777 functions.
All numeric expressions are captured by AExp.
It thus includes both Address and ValueType.
BExp captures boolean expressions.
The auxiliary construct #void represents the return value of functions that
don't have a return type.
It allows a more uniform semantics for functions.
In addition, we need the base expression type Exp which captures all possible
expressions, including those not captured by more particular sorts.
(SetExp will be described later).
syntax AExp ::= ValueType | Address
syntax BExp ::= Bool
syntax Void ::= "#void"
syntax Exp ::= AExp | BExp | SetExp | Data | Void
Next we define the ERC777 functions.
The two functions below are constant, returning String:
syntax Exp ::= name ( )
| symbol ( )
Since ERC777 doesn't define any operations over strings, we don't need a
separate sort for string expressions.
Thus we subsort them directly to Exp.
Here are the remaining functions from the standard:
syntax AExp ::= totalSupply ( )
| balanceOf ( AExp ) [strict]
| granularity ( )
syntax SetExp ::= defaultOperators ( )
| Set
syntax BExp ::= isOperatorFor ( AExp , AExp ) [strict]
syntax Exp ::= authorizeOperator ( AExp ) [strict]
| revokeOperator ( AExp ) [strict]
| send ( AExp , AExp , Data ) [strict]
| operatorSend ( AExp , AExp , AExp , Data , Data ) [strict]
| burn ( AExp ) [strict]
| operatorBurn ( AExp , AExp , Data ) [strict]
| "revert"
We use the K strictness mechanism to allow these functions to be used in
programs, with expressions passed as arguments.
Note that although not used in
ERC20-K, K supports
the sugared notation symbol(Sort1,Sort2,...,SortN) for declaring syntactic
constructs, which desugars as expected to
"symbol" "(" Sort1 "," Sort2 "," ... "," SortN ")".
The function defaultOperators returns an address[] in the standard.
Here we use the sort SetExp for the function, and generic Set for the
actual array of addresses.
All functions that don't return a value are subsorted directly to Exp.
The construct revert above represents the function execution result revert
mentioned in the standard.
In addition, we define one more function that is not part of the standard:
syntax Exp ::= operatorMint ( AExp , //from
AExp , //amount
Data , //data
Data //operatorData.
) [strict]
ERC-777 does not define a specific function for minting, but it allows the
minting operation through additional functions and defines a set of rules that
must be followed when minting tokens.
To capture these rules formally, it is convenient to define the function
operatorMint with a semantics symmetrical to operatorBurn (as seen shortly).
The ERC777 functions are required, at success, to log the following events:
syntax Event ::= Sent ( Address , Address , Address , ValueType , Data , Data )
| Minted ( Address , Address , ValueType , Data , Data )
| Burned ( Address , Address , ValueType , Data )
| AuthorizedOperator ( Address , Address )
| RevokedOperator ( Address , Address )
The events are then collected in a log.
The precise syntax of the log is not specified in the ERC777 standard, so
in ERC777-K we take the freedom to choose the same syntax that was used in
ERC20-K, that is, Events: <event1> <event2> ... <eventn>:
syntax EventLog ::= "Events:" | EventLog Event
The syntax of the event log is unconstrained (by semantic rules) and is irrelevant for implementations. All the above is saying is that implementations of ERC777-K must implement the notion of an event log, together with an empty event log and the capability to append a new event to an existing event log.
The main addition of ERC-777 over ERC-20 are two function "hooks":
tokensToSend and tokensReceived.
These are function interfaces which can be registered by an address, and will
be called whenever an operation that removes tokens, or adds tokens to the
respective address is invoked.
Below we define the 2 hooks:
syntax Stmt ::= AExp "." "tokensToSend" "(" AExp "," AExp "," AExp "," AExp "," Data "," Data ")" [strict]
syntax Stmt ::= AExp "." "tokensReceived" "(" AExp "," AExp "," AExp "," AExp "," Data "," Data ")" [strict]
Here the qualifier (before ".") represents the hook address, and the function arguments are the same as in the standard.
ERC777 defines additional rules that must be preserved when an ERC777 token contract is specified to be compatible with ERC20 (note that compatibility with ERC20 is optional). There are additional rules both for ERC777 functions and for ERC20. To capture them, we decided to fully model ERC777+ERC20 in ERC777-K. Thus, we also define all ERC20 functions and events:
syntax AExp ::= allowance ( AExp , AExp ) [strict]
| decimals ( )
syntax BExp ::= approve ( AExp , AExp ) [strict]
| transfer ( AExp , AExp ) [strict]
| transferFrom ( AExp , AExp , AExp ) [strict]
syntax Event ::= Transfer ( Address , Address , ValueType)
| Approval ( Address , Address , ValueType)
This completes the syntax module.
endmodule
The second module contains the configuration and the actual execution rules.
module ERC777
imports ERC777-SYNTAX
imports INT
imports BOOL
imports STRING
imports MAP
imports SET
imports LIST
imports KCELLS
Next we present the configuration and the meaning of each cell:
configuration
<ERC777>
<caller> 0:Address </caller>
<k> $PGM:K </k>
<accounts>
<account multiplicity="*">
<id> 0:Address </id>
<balance> 0:ValueType </balance>
<operators> .Set </operators>
<senderHook> 0:Address </senderHook>
<receiverHook> 0:Address </receiverHook>
<isContract> . </isContract>
<allowances>
<allow multiplicity="*">
<spender> 0:Address </spender>
<amount> 0:ValueType </amount>
</allow>
</allowances>
</account>
</accounts>
<supply> 0:ValueType </supply>
<nameC> "" </nameC>
<symbolC> "" </symbolC>
<granularityC> 1 </granularityC>
<defaultOperatorsC> .Set </defaultOperatorsC>
<ERC20CompatibleC> true </ERC20CompatibleC>
<acceptRegularNoReceiverHook> true </acceptRegularNoReceiverHook>
<burnAllowed> true </burnAllowed>
<log> Events: </log> // event*
<atomic> . </atomic>
</ERC777>
<caller>- the caller address.<k>- computation cell.<account>- all information relevant to one account.<id>- account address, key to the account.<balance>- token balance.<operators>- the set of operators for this account. Initialized with the default operators.<senderHook>- address of the sender hook registered for this account, or 0 if there is no hook.<receiverHook>- address of the receiver hook registered for this account, or 0 if there is no hook.<isContract>- whether this account is a contract or a regular account.<allowances>- ERC20 allowances associated with this account, which are completely separated from ERC777's<operators>, as required by the standard; the allowances are initialized with an allowance entry for any account in the configuration, with allowance 0.<spender>- spender account for this particular account.<amount>- allowance amount for this <account, spender> pair.
<supply>- total supply in this contract.<nameC>- token name, returned byname().<symbolC>- symbol of the token, returned bysymbol().<granularityC>- contract granularity.<defaultOperatorsC>- set of default operators, used to initialize<operators>when a new account is created.<ERC20CompatibleC>- contract parameter: says whether the contract is ERC20 compatible; it affects the types of logs created.<acceptRegularNoReceiverHook>- contract parameter: if true, regular addresses with no receiver hook can receive tokens through send or mint operations; if false, such operations will result in revert.<burnAllowed>- contract parameter: if true, burn operations are allowed; otherwise they result in revert.<log>- events log.<atomic>- backup cell that stores old values of certain cells at the beginning of an ERC-777 function; used to define therevertoperation.
For the remainder of the semantics, we assume the configuration is already
correctly initialized: all the account <id/>s are distinct, their
<balance/>s are non-negative, and the total <supply/> is the sum of all
the balances) and the <caller/> is known.
In our simple IMP programming language that we define on top of the ERC777-K
semantics (in erc777-imp.k) we define macros that can be used to
initialize the configuration.
ERC777 was originally designed for the EVM, whose integers
(of type uint256) are unsigned and have 256 bits, so can go up
to 2^256.
The exact size of integers is important for arithmetic overflow,
which needs to be rigorously defined in the formal specification.
However, the precise size of integers can be a parameter of the
ERC777-K specification.
This way, the specification can easily be used with various execution
environments, such as eWASM or
IELE, or
with various programming languages
(e.g., Viper appears to converge
towards integers up to 2^128).
The syntax declaration and the rule below define an integer
constant #MAXVALUE and initialize it with the largest integer
on 256 bits (one can set it to "infinity" if one does not care about
overflows or if one's computational infrastructure supports unbounded
integers, like
IELE does):
syntax Int ::= "#MAXVALUE" [function]
rule #MAXVALUE => 2 ^Int 256 -Int 1
The rules below define the semantics of four constant functions, simply by reading the value from corresponding cell:
rule <k> name ( ) => NAME ...</k>
<nameC> NAME </nameC>
rule <k> symbol ( ) => SYMBOL ...</k>
<symbolC> SYMBOL </symbolC>
rule <k> granularity ( ) => G ...</k>
<granularityC> G </granularityC>
rule <k> defaultOperators ( ) => DefOps ...</k>
<defaultOperatorsC> DefOps </defaultOperatorsC>
Similar to above, reading the value from <supply>:
rule <k> totalSupply ( ) => TotalSupply ...</k>
<supply> TotalSupply </supply>
For balanceOf we need two rules:
rule <k> balanceOf ( Holder:Int ) => Balance ...</k>
<id> Holder </id>
<balance> Balance </balance>
requires Holder =/=Int 0
//Required for send/operatorSend revert cases.
rule balanceOf(0) => 0
The first rule represents the regular case, similar to ERC20:
it rewrites into the <balance> value associated with the given parameter.
The second rule is required for the case when parameter Holder is 0.
Since 0 is an invalid address, we don't have an <account> cell for it,
thus the semantics for this case have to be defined through a separate rule.
This was not required to be special-cased in the specification of ERC20, but it
it required here in order to properly define the semantics of revert.
Similar to balanceOf:
rule <k> isOperatorFor ( Operator:Int , Holder:Int )
=> Operator in Operators ...</k>
<id> Holder </id>
<operators> Operators:Set </operators>
requires Holder =/=Int 0
rule isOperatorFor(_, 0) => false
rule <k> authorizeOperator ( Operator:Int ) => #void ...</k>
<caller> Holder </caller>
<id> Holder </id>
<operators> Operators => Operators SetItem(Operator) </operators>
<log> Log => Log AuthorizedOperator ( Operator , Holder ) </log>
requires Holder =/=Int Operator andBool Operator =/=Int 0
rule <k> authorizeOperator ( Operator:Int ) => revert ...</k>
<caller> Holder </caller>
requires Holder ==Int Operator orBool Operator ==Int 0
The first rule above corresponds to the valid call of authorizeOperator:
caller different from argument and argument different from 0.
ERC777 states that an account (caller) cannot authorize or revoke authorization
from itself.
The rule adds the argument to the list of operators of the caller, and
generates the log event AuthorizedOperator.
The second rule represents the invalid call, all other cases, which generates
a revert.
The revert construct has no other semantics in this module, but is printed
to the output for debug purposes in the ERC777-IMP module.
Requires two similar rules.
Successful operation generates the log event RevokedOperator.
rule <k> revokeOperator ( Operator:Int ) => #void ...</k>
<caller> Holder </caller>
<id> Holder </id>
<operators> Operators => Operators -Set SetItem(Operator) </operators>
<log> Log => Log RevokedOperator ( Operator , Holder ) </log>
requires Holder =/=Int Operator andBool Operator =/=Int 0
rule <k> revokeOperator ( Operator:Int ) => revert ...</k>
<caller> Holder </caller>
requires Holder ==Int Operator orBool Operator ==Int 0
The send function is simply an alias to operatorSend with first argument
the caller:
rule <k> send ( To:Int , Value:Int , Data )
=> operatorSend ( Holder , To , Value , Data , "" ) ...</k>
<caller> Holder </caller>
The operatorSend function requires many steps defined through auxiliary
constructs.
All together they represent the bulk of the semantics.
We start with two initial rules:
rule <k> operatorSend ( 0 => Caller , _,_,_,_ ) ...</k>
<caller> Caller </caller>
requires Caller =/=Int 0 //just for safety
rule operatorSend ( From , To , Value , Data , OperatorData )
=> #operatorSendAux ( From , To , Value , Data , OperatorData , balanceOf(From), balanceOf(To) )
requires From =/=Int 0 //just for safety
The first rule deals with the case when the first argument (From) is 0.
According to ERC777, in this case the From value should become the caller.
The second rule rewrites operatorSend into the auxiliary construct
#operatorSendAux and uses K's strictness mechanism to compute a few more
values: the balance of From and the balance of To.
Here we define the bulk of the logic of operatorSend.
The #operatorSendAux is rewritten into a sequence of operations, each
carrying a specific step defined in ERC777.
Recall that the K infix construct ~>, read "followed by", is used to
sequentialize computational tasks.
syntax K ::= "#operatorSendAux" "(" Address "," Address "," ValueType "," Data "," Data "," AExp "," AExp ")" [seqstrict(6,7)]
rule <k> #operatorSendAux ( From , To , Value , Data , OperatorData , BalanceFrom:Int, BalanceTo:Int )
=> #atomicBegin
~> #ensure( #and(
From =/=Int 0,
To =/=Int 0,
isOperatorFor ( Operator , From ),
Value >=Int 0,
BalanceFrom >=Int Value,
#isMultipleOf ( Value , granularity() ) ))
~> #callSender ( Operator , From , To , Value , Data , OperatorData )
~> #transfer ( From , To , Value )
~> #callRecipient ( Operator , From , To , Value , Data , OperatorData , false )
~> #log( Sent(Operator , From , To , Value , Data , OperatorData) )
~> #logERC20( Transfer(From , To , Value) )
~> #atomicEnd(#void) ...</k>
<caller> Operator </caller>
The first construct, #atomicBegin, saves the relevant part of the
configuration into the cell <atomic>.
It is then later used to revert all changes in case the operation ends in
revert.
The #ensure clause checks all the preconditions that must be true in order
for the operation to succeed.
If its argument expression evaluates to false, the operation ends in revert.
Note that overflow is not checked here, because the new balance is guaranteed
to be less than or equal to totalSupply, and thus cannot overflow.
The #callSender calls the sender hook for the From address, if it exists.
The #transfer performs the actual balance transfer.
Next, #callRecipient calls the receiver hook for the To address,
if it exists.
Because the call is performed after the balance transfer, the new balances
will be visible inside the receiver hook.
The #log construct will log the ERC777-specific event Send.
Then the #logERC20 construct will log the ERC20-specific Transfer, only
when ERC20 compatibility is enabled.
The last construct, #atomicEnd, deletes the backup data created by
#atomicBegin if the operation completed successfully.
The argument of #atomicEnd is required in order to correctly and uniformly
model function return, as discussed shortly.
There are two rules for #callSender, one for the case when Hook is
registered (i.e., different from 0) and the other for the case when it's
not registered:
syntax Stmt ::= #callSender ( Address , // operator
Address , // from
Address , // to
ValueType , // amount
Data , // userData
Data // operatorData
)
rule <k> #callSender ( Operator , From , To , Value , Data , OperatorData )
=> Hook . tokensToSend ( Operator , From , To , Value , Data , OperatorData ) ...</k>
<id> From </id>
<senderHook> Hook </senderHook>
requires Hook =/=Int 0
rule <k> #callSender ( Operator , From , To , Value , Data , OperatorData ) => . ...</k>
<id> From </id>
<senderHook> 0 </senderHook>
When a hook is registered, #callSender is rewritten into tokensToSend
qualified by the hook registration address.
ERC777-K does not define any specific behavior for tokensToSend.
In the extension module ERC777-IMP we provide two implementations, for
testing purposes:
one that accepts the operation and another that reverts.
Note that the behavior of the hook is not part of the ERC777 standard, which
is why we do not define it as part of our ERC777-K.
If the hook produces revert, it will be propagated by rules that are
presented shortly.
The second rule, for the case when the hook is not registered,
simply dissolves #callSender.
Recall that in K . means the "empty computation".
There are two rules here, similar to the rules for #callSender:
syntax Stmt ::= #callRecipient ( Address , // operator
Address , // from
Address , // to
ValueType , // amount
Data , // userData
Data , // operatorData
Bool // fromERC20: called by ERC20 functions
)
rule <k> #callRecipient ( Operator , From , To , Value , Data , OperatorData , _ )
=> Hook . tokensReceived ( Operator , From , To , Value , Data , OperatorData ) ...</k>
<id> To </id>
<receiverHook> Hook </receiverHook>
requires Hook =/=Int 0
rule <k> #callRecipient ( Operator , From , To , Value , Data , OperatorData , FromERC20 )
=> #ite( #or(FromERC20, #and(AcceptRegular, notBool ISCONTRACT) ) , . , revert ) ...</k>
<id> To </id>
<receiverHook> 0 </receiverHook>
<isContract> ISCONTRACT </isContract>
<acceptRegularNoReceiverHook> AcceptRegular </acceptRegularNoReceiverHook>
There is one additional rule when receiver account does not register a
tokensReceived hook. If token transfer happens during a send or mint
operation and receiver is a contract account, then operation "MUST revert".
If transfer happens as part of ERC20 transfer operation, then
the receiver "SHOULD accept" the operation (wording from ERC777).
This functionality is implemented in the 2nd rule above, through the
conditional construct #ite (if-then-else).
This construct performs the actual balance transfer. There are two rules. The first one is for the case when the sender and the recipient are different, when actual balance changes happen. The second rule is for the case when the sender and the recipient are the same. In this case, as expected, the balance remains unchanged.
syntax Stmt ::= #transfer ( Address , Address , ValueType )
rule <k> #transfer ( From , To , Value ) => . ...</k>
<account>
<id> From </id>
<balance> ValueFrom => ValueFrom -Int Value </balance>
...
</account>
<account>
<id> To </id>
<balance> ValueTo => ValueTo +Int Value </balance>
...
</account>
requires From =/=Int To
rule <k> #transfer ( From , To , Value ) => . ...</k>
requires From ==Int To
There is no need for side conditions checking for operation validity, because
validity was already checked by the #ensures construct generated by the rule
for operationSend.
Another functionality required to define operationSend is the construct
#isMultipleOf, which checks whether the amount involved in an operation
is a multiple of the global granularity:
syntax BExp ::= #isMultipleOf ( AExp , AExp ) [seqstrict]
rule #isMultipleOf ( Value:Int , Granularity:Int )
=> (Value /Int Granularity) *Int Granularity ==Int Value
The last auxiliary constructs, used by all state-altering operations in
ERC777-K, are related to logging.
The construct #log(Event) is used for events defined in ERC777.
It simply appends the event to the <log> cell.
The construct #logERC20 is used for ERC20-specific events.
It logs the given event only when ERC20 compatibility is enabled.
syntax Stmt ::= #log ( Event )
| #logERC20 ( Event )
rule <k> #log(Log) => . ...</k>
<log> Logs => Logs Log </log>
rule <k> #logERC20(Log) => . ...</k>
<log> Logs => Logs Log </log>
<ERC20CompatibleC> true </ERC20CompatibleC>
rule <k> #logERC20(Log) => . ...</k>
<ERC20CompatibleC> false </ERC20CompatibleC>
These are defined similarly to send and operatorSend.
They reuse many of the auxiliary constructs.
The ERC777 standard stipulates "Contract MAY prevent some/all holders from
burning for any reason".
We model this choice in a simplified way through either allowing burn
operations, or disallowing them globally.
This behavior is controlled by the cell<burnAllowed>.
If it holds true, the burn operation will proceed according to other rules.
If it holds false, burn operation will revert.
rule <k> burn( Amount:Int )
=> operatorBurn(Caller, Amount, "") ...</k>
<caller> Caller </caller>
rule <k> operatorBurn(0 => Caller, _,_) ...</k>
<caller> Caller </caller>
requires Caller =/=Int 0 //just for safety
rule <k> operatorBurn(Holder:Int, Amount:Int, OperatorData)
=> #atomicBegin
~> #ensure(#and(isOperatorFor(Operator, Holder),
#isMultipleOf(Amount, granularity()),
Amount >=Int 0,
Balance >=Int Amount,
Holder =/=Int 0,
BurnAllowed))
~> #callSender(Operator, Holder, 0, Amount, "", OperatorData)
~> #burn(Holder, Amount)
~> #log(Burned(Operator, Holder, Amount, OperatorData))
~> #logERC20(Transfer(Holder, 0, Amount)) // ERC20
~> #atomicEnd(#void) ...</k>
<caller> Operator </caller>
<id> Holder </id>
<balance> Balance </balance>
<burnAllowed> BurnAllowed </burnAllowed>
requires Holder =/=Int 0
syntax Stmt ::= #burn ( Address , ValueType )
rule <k> #burn(Holder, Amount) => . ...</k>
<account>
<id> Holder </id>
<balance> Balance => Balance -Int Amount </balance>
...
</account>
<supply> Supply => Supply -Int Amount </supply>
requires Balance >=Int Amount andBool Supply >=Int Amount
Calling operatorBurn with first argument 0 is allowed:
in this case Holder will become the caller
If holder has a sender hook registered, it is called before the operation by
using the already defined #callSender.
The actual balance decrease is performed by #burn.
Here, in addition to decreasing the balance, the total supply also decreases.
The burn operation uses the same mechanism as send for transaction atomicity,
enforcing preconditions and logging.
The ERC20 Transfer event has the To argument 0, to represent burning.
ERC777 does not define specific functions to mint tokens.
Instead, it specifies several rules that MUST be respected when minting tokens.
The definition of below is a minimal realization of minting that conforms to
those rules.
We define the function operationMint, which must be called by an operator on
behalf of a recipient.
It follows the same structure as operatorSend and operatorBurn.
This function is not allowed to have its Holder argument 0; that is, it
reverts when Holder is 0.
The relevant hook for the mint operation is tokensReceived.
When the hook is not defined, this semantics allows all addresses to receive
tokens through minting.
rule operatorMint(0,_,_,_) => revert
rule <k> operatorMint(Holder, Amount, Data, OperatorData)
=> #atomicBegin
~> #ensure(#and(Amount >=Int 0,
Supply +Int Amount <=Int #MAXVALUE,
#isMultipleOf(Amount, granularity()),
Holder =/=Int 0,
isOperatorFor( Operator , Holder )))
~> #mint(Holder, Amount)
~> #callRecipient(Operator, 0, Holder, Amount, Data, OperatorData, false)
~> #log(Minted(Operator, Holder, Amount, Data, OperatorData))
~> #logERC20(Transfer(0, Holder, Amount))
~> #atomicEnd(#void) ...</k>
<caller> Operator </caller>
<id> Holder </id>
<supply> Supply </supply>
requires Holder =/=Int 0
syntax Stmt ::= #mint ( Address , ValueType )
rule <k> #mint(Holder, Amount) => . ...</k>
<account>
<id> Holder </id>
<balance> Balance => Balance +Int Amount </balance>
...
</account>
<supply> Supply => Supply +Int Amount </supply>
In this section we have the rules for ERC20 functions.
There are several differences compared to the same rules in
ERC20-K.
First, the transfer operation logs two events: the ERC20 Transfer
and the ERC777 Sent.
Second, we use the #atomicBegin ... #atomicEnd transaction mechanism that we
defined, in order to rollback the transaction if it ends in revert.
Third, the transfer operation calls the sender and the recipient hooks,
as required by the ERC777 standard.
Another, more subtle difference, is the return type.
ERC777 state-changing functions don't return a value, while ERC20 functions
should return boolean value true st success.
This return value is represented by the argument of #atomicEnd, which we
define later.
rule <k> allowance(Owner:Int, Spender:Int) => Allowance ...</k>
<id> Owner </id>
<spender> Spender </spender>
<amount> Allowance </amount>
ERC777 restricts this function value to 18. E.g. 1 unit in user representation = 10^18 tokens. Similar to Wei vs Ether relation.
rule <k> decimals() => 18 ...</k>
rule <k> approve(Spender:Int, Allowance:Int) => true ...</k>
<caller> Owner </caller>
<id> Owner </id>
<spender> Spender </spender>
<amount> _ => Allowance </amount>
<log> Log => Log Approval(Owner, Spender, Allowance) </log>
requires Allowance >=Int 0
rule <k> approve(Spender:Int, Allowance:Int) => revert ...</k>
<caller> Owner </caller>
<id> Owner </id>
<spender> Spender </spender>
<amount> _ => Allowance </amount>
requires Allowance <Int 0
rule <k> transfer(To:Int, Value:Int) => #transferAux(To, Value, balanceOf(From), balanceOf(To)) ...</k>
<caller> From </caller>
syntax K ::= "#transferAux" "(" Address "," ValueType "," AExp "," AExp ")" [seqstrict(3,4)]
rule <k> #transferAux(To:Int, Value:Int, BalanceFrom:Int, BalanceTo:Int)
=> #atomicBegin
~> #ensure(#and(Value >=Int 0,
BalanceFrom >=Int Value,
#isMultipleOf(Value, granularity()),
#or(From ==Int To, BalanceTo +Int Value <=Int #MAXVALUE)))
~> #callSender(From, From, To, Value, "", "")
~> #transfer(From, To, Value)
~> #callRecipient(From, From, To, Value, "", "", true) // should accept even if To isn't registered and To is contract )
~> #log(Transfer(From, To, Value))
~> #log(Sent(From, From, To, Value, "", ""))
~> #atomicEnd(true) ...</k>
<caller> From </caller>
rule transferFrom(From:Int, To:Int, Value:Int)
=> #transferFromAux(From, To, Value, balanceOf(From), balanceOf(To))
syntax K ::= "#transferFromAux" "(" Address "," Address "," ValueType "," AExp "," AExp ")" [seqstrict(4,5)]
rule <k> #transferFromAux(From, To, Value, BalanceFrom:Int, BalanceTo:Int)
=> #atomicBegin
~> #ensure(#and(Value >=Int 0,
BalanceFrom >=Int Value,
#isMultipleOf(Value, granularity()),
#or(From ==Int To, BalanceTo +Int Value <=Int #MAXVALUE),
Allowed >=Int Value))
~> #callSender(Operator, From, To, Value, "", "")
~> #transferWithAllowance(Operator, From, To, Value)
~> #callRecipient(Operator, From, To, Value, "", "", true)
~> #log(Transfer(From, To, Value))
~> #log(Sent(From, From, To, Value, "", ""))
~> #atomicEnd(true) ...</k>
<caller> Operator </caller>
<id> From </id>
<spender> Operator </spender>
<amount> Allowed </amount>
syntax Stmt ::= #transferWithAllowance ( Address , Address , Address , ValueType )
rule <k> #transferWithAllowance(Operator, From, To, Value) => . ...</k>
<account>
<id> From </id>
<balance> BalanceFrom => BalanceFrom -Int Value </balance>
<spender> Operator </spender>
<amount> Allowed => Allowed -Int Value </amount>
...
</account>
<account>
<id> To </id>
<balance> BalanceTo => BalanceTo +Int Value </balance>
...
</account>
requires From =/=Int To
rule <k> #transferWithAllowance(Operator, From, To, Value) => . ...</k>
<account>
<id> From </id>
<balance> Balance </balance>
<spender> Operator </spender>
<amount> Allowed => Allowed -Int Value </amount>
...
</account>
requires From ==Int To
The construct #atomicBegin is the first operation performed by operatoSend,
operatorBurn, operatorMint:
syntax KItem ::= "#atomicBegin"
| "#atomicEnd" "(" K /*output*/ ")"
| #snapshot ( K , EventLog , ValueType )
rule <k> #atomicBegin => . ...</k>
<accounts> Accounts </accounts>
<log> Log </log>
<supply> Supply </supply>
<atomic> . => #snapshot ( Accounts , Log , Supply ) </atomic>
It stores the contents (or a "snapshot") of cells <accounts>, <log>, and
<supply> into <atomic>, to be used in case a revert operation happens.
Note that this semantics, which is sufficient for ERC777, allows only one
snapshot to be stored; in particular, snapshots cannot be stacked.
rule <k> #atomicEnd(OUT:K) => OUT ...</k>
<atomic> _ => . </atomic>
The construct #atomicEnd marks the end of the operation/function.
If this construct is reached, it means that the operation/function was
executed successfully, so the contents of <atomic> is unnecessary and thus
discarded.
Additionally, the #atomicEnd is rewritten into its argument, which contains
the return value.
This value is true for functions that return true in case of success
(ERC20), or #void for functions that don't have return values (ERC777).
We have two rules for revert:
rule <k> revert ~> (KI:KItem => .) ...</k>
<atomic> #snapshot(_,_,_) </atomic>
requires (KI =/=K #atomicEnd(#void)) andBool (KI =/=K #atomicEnd(true))
rule <k> revert ~> (#atomicEnd(_) => .) ...</k>
<accounts> _ => Accounts </accounts>
<log> _ => Log </log>
<supply> _ => Supply </supply>
<atomic> #snapshot ( Accounts , Log , Supply ) => . </atomic>
Both rules match only in the case when <atomic> is not empty, that is, when
we are inside an ERC777 or ERC20 function.
The first rule deletes any K item after revert, except atomicEnd, the only
item with which revert can interact.
The second rule matches when revert is followed by #atomicEnd.
It restores the state stored in <atomic> and keeps revert at the top of
computation.
Thus, once triggered, revert is always propagated outside the function that
generated it.
In module ERC777-IMP there are additional rules that print a message to the
output when revert is encountered, and allow the computation to continue.
The last section of the ERC777 module contains a collection of K utility
functions:
#ensureevaluates the preconditions of a function; if the argument evaluates totruethen the computation is allowed to continue, otherwise arevertis generated.#iterepresents a general-purpose conditional operator with support for strictness.#andand#oroperators implement boolean expressions with strictness, to be used as arguments to#ensures.
syntax Stmt ::= #ensure ( BExp ) [strict]
rule #ensure ( B:Bool ) => . requires B
rule #ensure ( B:Bool ) => revert requires notBool B
syntax K ::= #ite ( BExp , K , K ) [strict(1)]
rule #ite ( true , T , F ) => T
rule #ite ( false , T , F ) => F
Here we define multiple versions of #and that differ only in the number of
parameters.
Although we could have used only the 2-parameter version and nesting, we prefer
these multiple versions for readability.
syntax BExp ::= "#and" "(" BExp "," BExp ")" [strict]
| "#and" "(" BExp "," BExp "," BExp ")" [strict]
| "#and" "(" BExp "," BExp "," BExp "," BExp ")" [strict]
| "#and" "(" BExp "," BExp "," BExp "," BExp "," BExp ")" [strict]
| "#and" "(" BExp "," BExp "," BExp "," BExp "," BExp "," BExp ")" [strict]
| "#and" "(" BExp "," BExp "," BExp "," BExp "," BExp "," BExp "," BExp ")" [strict]
| "#or" "(" BExp "," BExp ")" [strict]
rule #and ( A:Bool , B:Bool ) => A andBool B
rule #and ( A:Bool , B:Bool , C:Bool ) => A andBool B andBool C
rule #and ( A:Bool , B:Bool , C:Bool , D:Bool ) => A andBool B andBool C andBool D
rule #and ( A:Bool , B:Bool , C:Bool , D:Bool , E:Bool ) => A andBool B andBool C andBool D andBool E
rule #and ( A:Bool , B:Bool , C:Bool , D:Bool , E:Bool , F:Bool ) => A andBool B andBool C andBool D andBool E andBool F
rule #and ( A:Bool , B:Bool , C:Bool , D:Bool , E:Bool , F:Bool , G:Bool )
=> A andBool B andBool C andBool D andBool E andBool F andBool G
rule #or ( A:Bool , B:Bool ) => A orBool B
endmodule
One way to use ERC777-K, illustrated in module ERC777-IMP and tests,
is to import it in other programming language semantics and thus offer ERC777
support to those languages.
In particular, this can be useful to test the ERC777-K specification
programmatically, as well as for producing tests that can be then used with
implementations of ERC777.
Another way to use ERC777-K is as a standard for ERC777 compliance. That is, as an answer to what needs to be proved about a smart contract claiming to implement an ERC777 token. Each of the rules above is one reachability claim that needs to be proved.
See the ERC20-K project for a similar (but simpler) formal semantics, for the ERC20 standard, as well as for more explanations about K.