search

LayerXcom / verified-vyper-contracts

FVyper: A collection of useful Vyper contracts developed with formal methods
Apache License 2.0
55 stars 15 forks source link

[ERC721] Spec transfer functions #60

Closed nrryuya closed 5 years ago

nrryuya commented 5 years ago

For now, we use BYZANTIUM version. see https://github.com/kframework/evm-semantics/issues/287

nrryuya commented 5 years ago

transferFrom-success-2 and transferFrom-failure-2

They cause error (gist), java.lang.AssertionError: unexpected class at matching: class org.kframework.backend.java.kil.KList in the symbolic execution of this line in _removeTokenFrom(). 

    # Change count tracking
    self.ownerToNFTokenCount[_from] -= 1
nrryuya commented 5 years ago

transferFrom-success-1

kprove fails (gist) because K makes a branch in which this assertion makes reverts.

assert self._isApprovedOrOwner(_sender, _tokenId)

This is because of this issue. https://github.com/kframework/evm-semantics/issues/291

Because [the other paths succeeds (gist] and the path that fails shouldn't be considered if the above issue resolved, we can move forward.

nrryuya commented 5 years ago

For now, skip the verification of transferFrom.