Add support for array literals #1198
Conversation
with the design in our OOPSLA formalization. This eliminates the error that Verus previously produced when declaring a constant using any of these types, e.g., ``` const a: [usize; 2] = [0, 1]; ``` where Verus concluded that the expression on the right-hand side was spec, which made it invalid for use in the exec aspect of the constant.
unless the sequence is empty.
This reverts commit 1314993.
…iterals," Save the seq! for a separate PR This reverts commit edb9c31.
|
This is very cool! I played with it and it really enables a seamless experience of spec array and exec array interplays. |
| @@ -9,7 +9,9 @@ verus! { | |||
| impl<T, const N: usize> View for [T; N] { | |||
| type V = Seq<T>; | |||
There was a problem hiding this comment.
Should we mark the view of arrays to be just [T; N] (like those primitive integer types)?
There was a problem hiding this comment.
My guess is that a sequence view will be more useful, since the spec writer can then make use of all the features in the sequence library.
|
@Chris-Hawblitzel Thanks for adding the mode test. Did you get a chance to review the rest of the code? No hurry on my side; I'm just not sure if we're ready to merge. |
I think you can go ahead and squash and merge. |
This introduces an AIR-level array literal, which we then connect all the way up to the rust_verify level. This includes updating the interpreter to handle the new array literals.
The AIR-level approach allows an efficient encoding to associate array indices to values. A future PR will take advantage of this new encoding to optimize sequence literals by changing how
seq!behaves.Commit 3779b06 is small, but it should be carefully reviewed, since it changes the mode checking for tuples, arrays, datatypes. The change is consistent with our formalization, but it's worth double checking. @Chris-Hawblitzel plans to add a few additional tests as a sanity check.