[WIP] Formal verification #14
Conversation
sources/u256.spec.move
Outdated
| spec split_u128 { | ||
| pragma opaque; | ||
| spec fun num_val(a: U256): num { | ||
| a.v0 + (a.v1 << 64) + (a.v2 << 128) + (a.v3 << 192) |
There was a problem hiding this comment.
I have a suspicion that, since this function is central for the other specs, the shift operation may be a source of timeouts or other problems. One thing you may want to try is break this down into multiplication.
In general, unfortunately, the prover uses right now an Integer theory which is not well suited for bit oriented numbers, but very well for other arithm. We are thinking in the future to make a choice for the right theory based on operator usage.
There was a problem hiding this comment.
It's very strange that prover numbers don't overflow, but we are getting:
a.v0 + (a.v1 * 0x10000000000000000) + (a.v2 * 0x100000000000000000000000000000000) + (a.v3 * 0x1000000000000000000000000000000000000000000000000)
│ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Invalid number literal. The given literal is too large to fit into the largest possible integer type, 'u128'
error: invalid number literal
In case we want to have some large integer constant or variable defined in spec.
There was a problem hiding this comment.
It's very strange that prover numbers don't overflow, but we are getting:
a.v0 + (a.v1 * 0x10000000000000000) + (a.v2 * 0x100000000000000000000000000000000) + (a.v3 * 0x1000000000000000000000000000000000000000000000000) │ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Invalid number literal. The given literal is too large to fit into the largest possible integer type, 'u128' error: invalid number literalIn case we want to have some large integer constant or variable defined in spec.
This is because the literals are from the Move language, and the error you are seeing stems from the parser. Are you able to workaround by using an expression on constants?
There was a problem hiding this comment.
We avoid it, yes, but would be good feature
No description provided.