Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Benoit Viguier
coq-verif-tweetnacl
Commits
4833f977
Commit
4833f977
authored
Mar 27, 2020
by
Peter Schwabe
Browse files
Small change to VST-i64 reply
parent
0cc07943
Changes
1
Hide whitespace changes
Inline
Side-by-side
paper/answer-Usenix.md
View file @
4833f977
...
...
@@ -50,11 +50,11 @@ REVIEW C:
*
Changed code, i64 -> int, but the size of
`int`
depends on architecture
T
his change
is required for the proof because of limitations of VST. We
recommend that TweetNaCl does not change to
int and that this issue is longer
term addressed in VST. As i64 has a larger
range than int, there is only small
concern that our proof does not extend to
TweetNaCl with i64. We will clarify
this in the paper.
We made t
his change
because VST does not support standard for-loop
verification tactics with i64. We
recommend that TweetNaCl does not change to
int and that this issue is longer
term addressed in VST. As i64 has a larger
range than int, there is only small
concern that our proof does not extend to
TweetNaCl with i64. We will clarify
this in the paper.
*
How do you know the pre/post conditions are complete? What happens if a
critical one is missed? Does this influence a full functional correctness?
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment