-
Notifications
You must be signed in to change notification settings - Fork 5
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Added some Move Prover spec by MoveBit. #22
base: master
Are you sure you want to change the base?
Conversation
@@ -21,13 +26,24 @@ module Bridge::Bytes { | |||
} else { | |||
data_len | |||
}; | |||
while (i < actual_end) { | |||
while ({ | |||
spec { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
循环里的spec,有没有可能跟代码解耦?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
loop invariant 必须放在循环头部
@@ -129,6 +142,13 @@ module Bridge::CrossChainLibrary { | |||
get_book_keeper(n, (n - (n - 1) / 3), pub_key_list) | |||
} | |||
|
|||
spec verify_pubkey { | |||
pragma verify = false; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
有部分verify 设置的为false,是打开有什么问题吗?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
因为verify_pubkey函数调用了get_book_keeper函数,get_book_keeper函数里面调用StarcoinFramework里面Hash::keccak_256和Hash::ripemd160这两个函数,这两个函数的spec有问题,导致prover编译报错,所以添加了verify = false;
No description provided.