search

verus-lang / verus

Verified Rust for low-level systems code
MIT License
1.06k stars 58 forks source link

Add support for array literals #1198

Open parno opened 1 week ago

parno commented 1 week ago

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 3779b06d86b9da 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.

y1ca1 commented 1 week ago

This is very cool! I played with it and it really enables a seamless experience of spec array and exec array interplays.