You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Cryptol's evaluation order allows proving this property without ever triggering the error:
Cryptol> :prove \b -> b ==> (b \/ error "uh oh")
Q.E.D.
(Total Elapsed Time: 0.021s, using "Z3")
SAW's simulator, on the other hand, will not short-circuit during evaluation, and as a result, it will trigger this error:
sawscript> prove_print z3 {{ \b -> b ==> (b \/ error "uh oh") }};
Run-time error: encountered call to the Cryptol 'error' function
This is something that I originally discovered while investigating #1807. While the example above is somewhat contrived, my proposed fix for #1807 would cause SAW to eagerly evaluate errors in more places, such as in the following property:
\(x : [2]) (i : [2]) -> (i < 2) ==> (x @ i) >= 42
Note that array indexing (@) calls error under the hood when the index value exceeds the length of the array. Due to #1807, SAW's simulator will effectively "clamp" the index value to be less than the length of the array, which means that SAW's simulator never even considers the cases where i = 2 or i = 3. But if I implement my proposed fix, then SAW does consider these cases, and due the aforementioned differences in short-circuiting behavior between Cryptol and SAW, adding (i < 2) ==> ... isn't enough to avoid out-of-bounds indexes.
To put it more directly: this issue is a blocker for fixing #1807.
The text was updated successfully, but these errors were encountered:
Cryptol is very careful not to invoke errors on one side of a symbolic merge when the condition being merged on allows short-circuiting (see this code). One possible approach to fixing this issue is to implement something similar in saw-core's muxValue function. Unfortunately, this wouldn't be quite as straightforward as in Cryptol, as calls to error in SAWCore become raw Haskell exceptions.
Consider the following Cryptol property:
Cryptol's evaluation order allows proving this property without ever triggering the
error
:SAW's simulator, on the other hand, will not short-circuit during evaluation, and as a result, it will trigger this
error
:This is something that I originally discovered while investigating #1807. While the example above is somewhat contrived, my proposed fix for #1807 would cause SAW to eagerly evaluate
error
s in more places, such as in the following property:Note that array indexing (
@
) callserror
under the hood when the index value exceeds the length of the array. Due to #1807, SAW's simulator will effectively "clamp" the index value to be less than the length of the array, which means that SAW's simulator never even considers the cases wherei = 2
ori = 3
. But if I implement my proposed fix, then SAW does consider these cases, and due the aforementioned differences in short-circuiting behavior between Cryptol and SAW, adding(i < 2) ==> ...
isn't enough to avoid out-of-bounds indexes.To put it more directly: this issue is a blocker for fixing #1807.
The text was updated successfully, but these errors were encountered: