Commit 93a90727 authored by Benoit Viguier's avatar Benoit Viguier
Browse files

formalizm

parent 3aebe807
......@@ -148,7 +148,7 @@ This solution does not generate all the possible cases of aliasing over 3 pointe
To make the verification the smoothest, the Coq formal definition of the function
should be as close as possible to the C implementation behavior.
Optimizations of such definitions are often counter-productive as they increase the
amount of proofs required for \eg bounds checking, loops invariants\ldots.
amount of proofs required for \eg bounds checking, loops invariants.
In order to further speed-up the verification process, to prove the specification
\TNaCle{crypto_scalarmult}, we only need the specification of the subsequently
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment