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
f6574768
Commit
f6574768
authored
Mar 27, 2020
by
Freek Wiedijk
Browse files
CompCert <-> gcc answer
parent
4833f977
Changes
1
Hide whitespace changes
Inline
Side-by-side
paper/answer-Usenix.md
View file @
f6574768
...
...
@@ -28,7 +28,13 @@ REVIEW A:
beyond what is acceptable?
For the X25519 implementation in TweetNaCl, CompCert generates code that is
about 6x slower than code generated with gcc. While this sounds like a lot, it
about 6x slower than code generated with gcc. But our verification also
applies to compilers like gcc and clang. The CompCert semantics is more
strict than the C17 standard with certain parameers (like integer sizes)
fixed. Therefore, if a compiler obeys the standard, then our correctness
proof also applies there.
While this sounds like a lot, it
may not be too much of an issue for projects that use TweetNaCl, because they
chose for a library that prioritizes simplicity over performance in the first
place. A more serious issue however can be the non-free CompCert license.
...
...
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