fix status_code of init, get_deposit_root, and get_deposit_count #316
Conversation
| [ 536 := #buf(32, 8) ] /* for slice(convert(y, bytes32), start=24, len=8) */ | ||
| [ 704 := #buf(32, 8) ++ #bufSeg(#buf(32, Y8), 24, 8) ] /* return: bytes[8] */ /* memcpy(704 <- 536, 40) */ | ||
| [ 352 /* = 320 + 32 * 1 */ := #buf(32, {RETURN_ADDR_FROM_TO_LITTLE_ENDIAN_64}) ] /* return address */ | ||
| [ 320 /* = 320 + 32 * 0 */ := #buf(32, DEPOSIT_COUNT) ] /* argument */ |
There was a problem hiding this comment.
any reason why these are out of order?
There was a problem hiding this comment.
The main reason is that K does not yet fully support the AC matching over maps. So, I had to put the map updates in the order they appear in the execution of the bytecode. The advantage of this order is that it clearly shows how the local memory is updated in each step of the bytecode execution.
| [ 672 := #buf(32, 32) ] /* ??? */ | ||
| [ 640 := #buf(32, 0) ] /* ??? */ | ||
| [ 800 /* = 320 + 32 * 15 */ := #buf(32, 32) ] /* padding loop index */ | ||
| [ 744 /* = 320 + 32 * 13 + 8 */ <- 0 ] /* padding */ |
There was a problem hiding this comment.
[ 744 /* = 320 + 32 * 13 + 8 */ := #buf(22, 0) ] would rewrite to this, no? That seems cleaner to me
There was a problem hiding this comment.
Yes, they are equivalent, but the current form is easier for K to prove. Your succinct form requires more lemmas for K to prove.
|
I noticed you assume |
|
@MrChico You're right. But note that since no
|
|
@MrChico I'll merge this PR for now, as your questions are not necessarily relevant to the changes in this PR. Please open github issues if your questions are not fully addressed by my answers, so that we can discuss further. Thanks for your detailed review! |
daejunpark
changed the title
No description provided.