kprove fails (gist) because K makes a branch in which this assertion makes reverts even if the precondition assure it don't revert.
assert self._isApprovedOrOwner(_sender, _tokenId)
This is because the simplification in |Int doesn't work correctly. KEVM team suggested two workarouunds here.
transferFrom-failure-1
kprove doesn't stop. I haven't investigate it yet.
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().
transferFrom-success-1
kprove fails (gist) because K makes a branch in which this assertion makes reverts even if the precondition assure it don't revert.
This is because the simplification in
|Int
doesn't work correctly. KEVM team suggested two workarouunds here.transferFrom-failure-1
kprove
doesn't stop. I haven't investigate it yet.transferFrom-success-2
andtransferFrom-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()
.In
transferFrom-success-1
, the symbolic execution here doesn't cause error, though.