New approach to specifying iterators via a prophetic sequence encoding

CONTRIBUTING.md

@@ -184,3 +184,7 @@ vargo build --vstd-no-verify
 # for tests
 vargo test --vstd-no-verify -p rust_verify_test --test <test file> <test name>
 ```
+
+If you modify the syntax parsing inside of the `dependencies/syn/src` directory,
+be sure to regenerate the auto-generated files in the `dependencies/syn/src/gen` directory.
+See `dependencies/syn/README.md` for details.

dependencies/syn/README.md

@@ -189,6 +189,13 @@ warning: come on, pick a more creative name
 
 <br>
 
+## Building
+
+**IMPORTANT**: If you introduce new items (e.g., `ast_struct`s) or modify the
+fields in existing items, you need to go into the `codegen`directory and run
+`cargo run` to regenerate the files in the `src/gen` directory.
+
+
 ## Testing
 
 When testing macros, we often care not just that the macro can be used

dependencies/syn/src/expr.rs

@@ -450,7 +450,9 @@ ast_struct! {
         pub in_token: Token![in],
         pub expr_name: Option<Box<(Ident, Token![:])>>,
         pub expr: Box<Expr>,
+        pub invariant_except_break: Option<InvariantExceptBreak>,
         pub invariant: Option<Invariant>,
+        pub ensures: Option<Ensures>,
         pub decreases: Option<Decreases>,
         pub body: Block,
     }
@@ -2534,7 +2536,9 @@ pub(crate) mod parsing {
                     None
                 };
             let expr: Expr = input.call(Expr::parse_without_eager_brace)?;
+            let invariant_except_break = input.parse()?;
             let invariant = input.parse()?;
+            let ensures = input.parse()?;
             let decreases = input.parse()?;
 
             let content;
@@ -2550,7 +2554,9 @@ pub(crate) mod parsing {
                 in_token,
                 expr_name,
                 expr: Box::new(expr),
+                invariant_except_break,
                 invariant,
+                ensures,
                 decreases,
                 body: Block { brace_token, stmts },
             })
@@ -3936,7 +3942,9 @@ pub(crate) mod printing {
                 colon.to_tokens(tokens);
             }
             print_expr(&self.expr, tokens, FixupContext::new_condition());
+            self.invariant_except_break.to_tokens(tokens);
             self.invariant.to_tokens(tokens);
+            self.ensures.to_tokens(tokens);
             self.decreases.to_tokens(tokens);
             self.body.brace_token.surround(tokens, |tokens| {
                 inner_attrs_to_tokens(&self.attrs, tokens);

examples/exec_termination_example.rs

@@ -70,7 +70,7 @@ verus! {
     fn exec_for_loop() {
         let mut n: u64 = 0;
         for x in iter: 0..10
-            invariant n == iter.cur * 3,
+            invariant n == x * 3,
             // You can write a `decreases` if you want, but it's not needed
             // because Verus inserts a decreases automatically for `for` loops:
             //   decreases 10 - iter.cur,
@@ -84,7 +84,7 @@ verus! {
         let mut end = 10;
         for x in iter: 0..end 
             invariant 
-                n == iter.cur * 3,
+                n == x * 3,
                 end == 10,
             // You can write a `decreases` if you want, but it's not needed
             // because Verus inserts a decreases automatically for `for` loops:
@@ -111,4 +111,4 @@ verus! {
             i -= 1;
         }
     }
-}
+}

examples/mergesort.rs

@@ -16,6 +16,7 @@ fn extend_from_idx(r: &mut Vec<u64>, v: &Vec<u64>, start: usize)
 {
     for i in start..v.len()
         invariant
+            start <= i <= v.len(),  // REVIEW: We didn't need this previously
             r@ =~= old(r)@ + v@.subrange(start as int, i as int),
     {
         r.push(v[i]);