-
Notifications
You must be signed in to change notification settings - Fork 58
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
Interpreter handles opaque inconsistently #944
Comments
A result of this is that this passes:
whereas this does not:
This is obviously unexpected behavior. Because of the way "pruning" works, and because To make a fix, we need to decide: should assert-by-compute unfold opaque functions by default, or should it require |
I would tend to think that |
Based on discussions in today's Verus meeting, the consensus was that the interpreter should default to opening |
Based on a discussion with @Chris-Hawblitzel, the current plan is to add assert-by-compute to the list of assertions that cause us to spinoff a separate query, and in that context we can tell the pruning phase to not remove opaque functions (or their transitive dependencies). |
This program
uses
u64_leading_zeros
, which is defined aspublic
andopen
:verus/source/pervasive/std_specs/bits.rs
Line 655 in 2b607f7
Oddly, when the interpreter tries to run, when it reaches the point of trying to apply
u64_leading_zeros
, it does a lookup for the function's body and the lookup fails, specifically we getNone
here:verus/source/vir/src/interpreter.rs
Line 1365 in 2b607f7
where
fun_ssts
is passed into the interpreter from thestate
object in theast_to_sst
conversion.If I inline the definition in the same file, there's no trouble finding and using the definition.
Is this expected behavior? Or is something going wrong in the collection of
fun_ssts
?The text was updated successfully, but these errors were encountered: