diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 22fa33493f..8e42f7eea1 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -184,3 +184,7 @@ vargo build --vstd-no-verify # for tests vargo test --vstd-no-verify -p rust_verify_test --test ``` + +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. diff --git a/dependencies/syn/README.md b/dependencies/syn/README.md index 16a393b9f0..37a9f2df5a 100644 --- a/dependencies/syn/README.md +++ b/dependencies/syn/README.md @@ -189,6 +189,13 @@ warning: come on, pick a more creative name
+## 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 diff --git a/dependencies/syn/src/expr.rs b/dependencies/syn/src/expr.rs index ea7ee89f64..44222bec55 100644 --- a/dependencies/syn/src/expr.rs +++ b/dependencies/syn/src/expr.rs @@ -450,7 +450,9 @@ ast_struct! { pub in_token: Token![in], pub expr_name: Option>, pub expr: Box, + pub invariant_except_break: Option, pub invariant: Option, + pub ensures: Option, pub decreases: Option, 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); diff --git a/dependencies/syn/src/gen/clone.rs b/dependencies/syn/src/gen/clone.rs index 3c47b53a39..58776ec04f 100644 --- a/dependencies/syn/src/gen/clone.rs +++ b/dependencies/syn/src/gen/clone.rs @@ -667,7 +667,9 @@ impl Clone for crate::ExprForLoop { in_token: self.in_token.clone(), expr_name: self.expr_name.clone(), expr: self.expr.clone(), + invariant_except_break: self.invariant_except_break.clone(), invariant: self.invariant.clone(), + ensures: self.ensures.clone(), decreases: self.decreases.clone(), body: self.body.clone(), } diff --git a/dependencies/syn/src/gen/debug.rs b/dependencies/syn/src/gen/debug.rs index a8e07c07b3..b5657fa7db 100644 --- a/dependencies/syn/src/gen/debug.rs +++ b/dependencies/syn/src/gen/debug.rs @@ -1019,7 +1019,9 @@ impl crate::ExprForLoop { formatter.field("in_token", &self.in_token); formatter.field("expr_name", &self.expr_name); formatter.field("expr", &self.expr); + formatter.field("invariant_except_break", &self.invariant_except_break); formatter.field("invariant", &self.invariant); + formatter.field("ensures", &self.ensures); formatter.field("decreases", &self.decreases); formatter.field("body", &self.body); formatter.finish() diff --git a/dependencies/syn/src/gen/eq.rs b/dependencies/syn/src/gen/eq.rs index 8555ec8e95..779079b69b 100644 --- a/dependencies/syn/src/gen/eq.rs +++ b/dependencies/syn/src/gen/eq.rs @@ -673,8 +673,9 @@ impl PartialEq for crate::ExprForLoop { fn eq(&self, other: &Self) -> bool { self.attrs == other.attrs && self.label == other.label && self.pat == other.pat && self.expr_name == other.expr_name && self.expr == other.expr - && self.invariant == other.invariant && self.decreases == other.decreases - && self.body == other.body + && self.invariant_except_break == other.invariant_except_break + && self.invariant == other.invariant && self.ensures == other.ensures + && self.decreases == other.decreases && self.body == other.body } } #[cfg_attr(docsrs, doc(cfg(feature = "extra-traits")))] diff --git a/dependencies/syn/src/gen/fold.rs b/dependencies/syn/src/gen/fold.rs index e2c366142a..ace08d1d67 100644 --- a/dependencies/syn/src/gen/fold.rs +++ b/dependencies/syn/src/gen/fold.rs @@ -2115,7 +2115,10 @@ where in_token: node.in_token, expr_name: (node.expr_name).map(|it| Box::new((f.fold_ident((*it).0), (*it).1))), expr: Box::new(f.fold_expr(*node.expr)), + invariant_except_break: (node.invariant_except_break) + .map(|it| f.fold_invariant_except_break(it)), invariant: (node.invariant).map(|it| f.fold_invariant(it)), + ensures: (node.ensures).map(|it| f.fold_ensures(it)), decreases: (node.decreases).map(|it| f.fold_decreases(it)), body: f.fold_block(node.body), } diff --git a/dependencies/syn/src/gen/hash.rs b/dependencies/syn/src/gen/hash.rs index 93f0fbfd90..79e3175c2f 100644 --- a/dependencies/syn/src/gen/hash.rs +++ b/dependencies/syn/src/gen/hash.rs @@ -972,7 +972,9 @@ impl Hash for crate::ExprForLoop { self.pat.hash(state); self.expr_name.hash(state); self.expr.hash(state); + self.invariant_except_break.hash(state); self.invariant.hash(state); + self.ensures.hash(state); self.decreases.hash(state); self.body.hash(state); } diff --git a/dependencies/syn/src/gen/visit.rs b/dependencies/syn/src/gen/visit.rs index e74f6fdfa4..70be257466 100644 --- a/dependencies/syn/src/gen/visit.rs +++ b/dependencies/syn/src/gen/visit.rs @@ -2133,9 +2133,15 @@ where skip!((* * it).1); } v.visit_expr(&*node.expr); + if let Some(it) = &node.invariant_except_break { + v.visit_invariant_except_break(it); + } if let Some(it) = &node.invariant { v.visit_invariant(it); } + if let Some(it) = &node.ensures { + v.visit_ensures(it); + } if let Some(it) = &node.decreases { v.visit_decreases(it); } diff --git a/dependencies/syn/src/gen/visit_mut.rs b/dependencies/syn/src/gen/visit_mut.rs index 7fb0142796..7682335fcc 100644 --- a/dependencies/syn/src/gen/visit_mut.rs +++ b/dependencies/syn/src/gen/visit_mut.rs @@ -2095,9 +2095,15 @@ where skip!((* * it).1); } v.visit_expr_mut(&mut *node.expr); + if let Some(it) = &mut node.invariant_except_break { + v.visit_invariant_except_break_mut(it); + } if let Some(it) = &mut node.invariant { v.visit_invariant_mut(it); } + if let Some(it) = &mut node.ensures { + v.visit_ensures_mut(it); + } if let Some(it) = &mut node.decreases { v.visit_decreases_mut(it); } diff --git a/dependencies/syn/syn.json b/dependencies/syn/syn.json index 81ff107c2b..81047e7377 100644 --- a/dependencies/syn/syn.json +++ b/dependencies/syn/syn.json @@ -1,5 +1,5 @@ { - "version": "0.0.0-2025-11-09-0048", + "version": "0.0.0-2025-11-16-0050", "types": [ { "ident": "Abi", @@ -1852,11 +1852,21 @@ "syn": "Expr" } }, + "invariant_except_break": { + "option": { + "syn": "InvariantExceptBreak" + } + }, "invariant": { "option": { "syn": "Invariant" } }, + "ensures": { + "option": { + "syn": "Ensures" + } + }, "decreases": { "option": { "syn": "Decreases" diff --git a/dependencies/syn/tests/debug/gen.rs b/dependencies/syn/tests/debug/gen.rs index 6fc0d22121..ad8e2b09df 100644 --- a/dependencies/syn/tests/debug/gen.rs +++ b/dependencies/syn/tests/debug/gen.rs @@ -1112,6 +1112,20 @@ impl Debug for Lite { formatter.field("expr_name", Print::ref_cast(val)); } formatter.field("expr", Lite(&_val.expr)); + if let Some(val) = &_val.invariant_except_break { + #[derive(RefCast)] + #[repr(transparent)] + struct Print(syn::InvariantExceptBreak); + impl Debug for Print { + fn fmt(&self, formatter: &mut fmt::Formatter) -> fmt::Result { + formatter.write_str("Some(")?; + Debug::fmt(Lite(&self.0), formatter)?; + formatter.write_str(")")?; + Ok(()) + } + } + formatter.field("invariant_except_break", Print::ref_cast(val)); + } if let Some(val) = &_val.invariant { #[derive(RefCast)] #[repr(transparent)] @@ -1126,6 +1140,20 @@ impl Debug for Lite { } formatter.field("invariant", Print::ref_cast(val)); } + if let Some(val) = &_val.ensures { + #[derive(RefCast)] + #[repr(transparent)] + struct Print(syn::Ensures); + impl Debug for Print { + fn fmt(&self, formatter: &mut fmt::Formatter) -> fmt::Result { + formatter.write_str("Some(")?; + Debug::fmt(Lite(&self.0), formatter)?; + formatter.write_str(")")?; + Ok(()) + } + } + formatter.field("ensures", Print::ref_cast(val)); + } if let Some(val) = &_val.decreases { #[derive(RefCast)] #[repr(transparent)] @@ -2097,6 +2125,20 @@ impl Debug for Lite { formatter.field("expr_name", Print::ref_cast(val)); } formatter.field("expr", Lite(&self.value.expr)); + if let Some(val) = &self.value.invariant_except_break { + #[derive(RefCast)] + #[repr(transparent)] + struct Print(syn::InvariantExceptBreak); + impl Debug for Print { + fn fmt(&self, formatter: &mut fmt::Formatter) -> fmt::Result { + formatter.write_str("Some(")?; + Debug::fmt(Lite(&self.0), formatter)?; + formatter.write_str(")")?; + Ok(()) + } + } + formatter.field("invariant_except_break", Print::ref_cast(val)); + } if let Some(val) = &self.value.invariant { #[derive(RefCast)] #[repr(transparent)] @@ -2111,6 +2153,20 @@ impl Debug for Lite { } formatter.field("invariant", Print::ref_cast(val)); } + if let Some(val) = &self.value.ensures { + #[derive(RefCast)] + #[repr(transparent)] + struct Print(syn::Ensures); + impl Debug for Print { + fn fmt(&self, formatter: &mut fmt::Formatter) -> fmt::Result { + formatter.write_str("Some(")?; + Debug::fmt(Lite(&self.0), formatter)?; + formatter.write_str(")")?; + Ok(()) + } + } + formatter.field("ensures", Print::ref_cast(val)); + } if let Some(val) = &self.value.decreases { #[derive(RefCast)] #[repr(transparent)] diff --git a/examples/exec_termination_example.rs b/examples/exec_termination_example.rs index 6c62b27873..46d9be00fd 100644 --- a/examples/exec_termination_example.rs +++ b/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; } } -} \ No newline at end of file +} diff --git a/examples/std_test/vecdeque_test.rs b/examples/std_test/vecdeque_test.rs index 6683918cfb..6ceeb7709a 100644 --- a/examples/std_test/vecdeque_test.rs +++ b/examples/std_test/vecdeque_test.rs @@ -51,8 +51,8 @@ fn vec_deque_test() let mut i: usize = 0; for x in it: v1.iter() invariant - i == it.pos, - it.elements == seq![10u32, 11u32], + i == it.index@, + it.seq() == seq![10u32, 11u32].map_values(|v| &v), { assert(x > 9); assert(x < 12); diff --git a/source/builtin_macros/src/syntax.rs b/source/builtin_macros/src/syntax.rs index ab6501c37b..b711218987 100644 --- a/source/builtin_macros/src/syntax.rs +++ b/source/builtin_macros/src/syntax.rs @@ -3286,49 +3286,64 @@ impl Visitor { // 'label: for x in y: e invariant inv { body } // into: // { + // #[allow(non_snake_case)] + // let VERUS_iter_init = e; + // #[allow(non_snake_case)] + // let VERUS_iter = VerusForLoopWrapper::new( + // // Real iterator + // ::core::iter::IntoIterator::into_iter(VERUS_iter_init), + // // Spec-level iterator (relies on `when_used_as_spec` on into_iter) + // Ghost(Some(&::core::iter::IntoIterator::into_iter(VERUS_iter_init))), + // ); + // // Hold on to the initial value so that after the loop, we know it didn't change // #[allow(non_snake_case)] - // let VERUS_iter = e; + // #[verus::internal(spec)] + // let y = VERUS_OLD_y.snapshot.view(); // #[allow(non_snake_case)] - // let VERUS_loop_result = match ::core::iter::IntoIterator::into_iter(VERUS_iter) { - // #[allow(non_snake_case)] - // mut VERUS_exec_iter => { - // #[allow(non_snake_case)] - // let ghost mut y = ::vstd::pervasive::ForLoopGhostIteratorNew::ghost_iter( - // &VERUS_exec_iter); - // 'label: loop + // let VERUS_loop_result = match VERUS_iter { + // mut y => { + // #[verifier::allow_complex_invariants] + // 'label: loop + // invariant_except_break + // #[verus::internal(auto_decreases)] + // y.iter.decrease().is_Some(), // invariant - // ::vstd::pervasive::ForLoopGhostIterator::exec_invariant(&y, - // &VERUS_exec_iter), - // ::vstd::pervasive::ForLoopGhostIterator::ghost_invariant(&y, - // verus_builtin::infer_spec_for_loop_iter( - // &::vstd::pervasive::ForLoopGhostIteratorNew::ghost_iter( - // &::core::iter::IntoIterator::into_iter(VERUS_iter)), - // &::vstd::pervasive::ForLoopGhostIteratorNew::ghost_iter( - // &::core::iter::IntoIterator::into_iter(e)), - // )), - // { let x = - // ::vstd::pervasive::ForLoopGhostIterator::ghost_peek_next(&y) - // .unwrap_or(vstd::pervasive::arbitrary()); - // inv }, + // // We track the continuitiy of the snapshot and the initial iterator-creation expression + // ::vstd::prelude::spec_eq(y.snapshot, VERUS_old_snap), + // match verus_builtin::infer_spec_for_loop_iter( + // &::core::iter::IntoIterator::into_iter(VERUS_iter_init), + // &::core::iter::IntoIterator::into_iter(e), + // print_hint, + // ) { + // Some(v) => ::vstd::prelude::spec_eq(y.init, Ghost(Some(v))), + // None => true, + // }, + // y.wf(), + // ({ + // // Grab the next val for (possible) use in the user-provided inv + // let x = y.snapshot.view().peek(y.index.view()) + // .unwrap_or(vstd::pervasive::arbitrary()); + // inv + // }), // ensures - // ::vstd::pervasive::ForLoopGhostIterator::ghost_ensures(&y), + // y.snapshot.view().completes(), + // y.index.view() == y.seq().len(), // decreases - // ::vstd::pervasive::ForLoopGhostIterator::ghost_decrease(&y) + // y.iter.decrease(), // .unwrap_or(vstd::pervasive::arbitrary()), - // // { - // #[allow(non_snake_case)] - // let mut VERUS_loop_next; - // match ::core::iter::Iterator::next(&mut VERUS_exec_iter) { - // ::core::option::Option::Some(VERUS_loop_val) => { - // VERUS_loop_next = VERUS_loop_val; - // } - // ::core::option::Option::None => break, - // }; - // let x = VERUS_loop_next; - // let () = { body }; - // proof { y = ::vstd::pervasive::ForLoopGhostIterator::ghost_advance( - // &y, &VERUS_exec_iter); } + // let ghost VERUS_OLD_y = y; + // #[allow(non_snake_case)] + // let mut VERUS_loop_next; + // match y.next() { + // Some(VERUS_loop_val) => VERUS_loop_next = VERUS_loop_val, + // None => { break } + // } + // let x = VERUS_loop_next; + // // We only let the user-provided body access an immutable ghost version of the iterator + // // We use the "old" version, so that the index lines up with the loop invariant + // let ghost y = VERUS_OLD_y; + // let () = { body }; // } // } // }; @@ -3342,11 +3357,13 @@ impl Visitor { mut attrs, label, for_token, - pat, + pat, // x in_token, - expr_name, - expr, + expr_name, // y + expr, // e + invariant_except_break, invariant, + ensures, mut decreases, body, } = for_loop; @@ -3370,7 +3387,6 @@ impl Visitor { if let Some(i) = no_auto_loop_invariant { attrs.remove(i); } - if !self.erase_ghost.keep() || self.inside_external_code > 0 { return Expr::ForLoop(verus_syn::ExprForLoop { attrs, @@ -3380,15 +3396,20 @@ impl Visitor { in_token, expr_name: None, expr, + invariant_except_break: None, invariant: None, + ensures: None, decreases: None, body, }); } attrs.push(mk_verus_attr(span, quote! { for_loop })); + let decrease_is_some_msg = "Failed to prove that the iterator always returns a decreases metric. + If you don't expect the iterator to provide such a metric, try adding #[verifier::exec_allows_no_decreases_clause]. + You might also try using a `loop` instead of a `for`."; let exec_inv_msg = "For-loop iterator invariant failed. \ - This may indicate a bug in the definition of the ForLoopGhostIterator. \ + This may indicate a bug in the definition of the VerusForLoopWrapper. \ You might try using a `loop` instead of a `for`."; let ghost_inv_msg = "Automatically generated loop invariant failed. \ You can disable the automatic generation by adding \ @@ -3402,67 +3423,101 @@ impl Visitor { Expr::Verbatim(quote_spanned!(expr.span() => true)) }; - let x_exec_iter = Ident::new("VERUS_exec_iter", span); - let x_ghost_iter = if let Some(x_ghost_iter_box) = expr_name { + // Initial value of the expression (e) + let x_verus_iter_init = Ident::new("VERUS_iter_init", span); + // Name for the iterator (y) + let x_iter_name = if let Some(x_ghost_iter_box) = expr_name { let (x_ghost_iter, _) = *x_ghost_iter_box; x_ghost_iter } else { Ident::new("VERUS_ghost_iter", span) }; + // Name for the exec iterator we create from `e` + let x_exec_iter = Ident::new("VERUS_iter", span); + // Name for the result of wrapping the original iterator in a VerusForLoopWrapper + let x_wrapped_iter = Ident::new("VERUS_iter", span); + // Name that "remembers" the initial snapshot + let x_snapshot = Ident::new("VERUS_old_snap", span); + // Name that "remembers" the initial iterator at the start of the loop body + let x_iter_body_old = Ident::new("VERUS_old_iter", span); + let mut stmts: Vec = Vec::new(); let expr_inv = expr.clone(); - // ::vstd::pervasive::ForLoopGhostIterator::exec_invariant(&y, &VERUS_exec_iter), - // ::vstd::pervasive::ForLoopGhostIterator::ghost_invariant(&y, - // verus_builtin::infer_spec_for_loop_iter( - // &::vstd::pervasive::ForLoopGhostIteratorNew::ghost_iter( - // &::core::iter::IntoIterator::into_iter(VERUS_iter)), - // &::vstd::pervasive::ForLoopGhostIteratorNew::ghost_iter( - // &::core::iter::IntoIterator::into_iter(e)), - // )), - let exec_inv: Expr = Expr::Verbatim(quote_spanned_vstd!(vstd, expr.span() => + let init_inv: Expr = Expr::Verbatim(quote_spanned_vstd!(vstd, expr.span() => #[verifier::custom_err(#exec_inv_msg)] - #vstd::pervasive::ForLoopGhostIterator::exec_invariant(&#x_ghost_iter, &#x_exec_iter) + #vstd::prelude::spec_eq(#x_iter_name.snapshot.view(), #x_snapshot) + )); + let wf_inv: Expr = Expr::Verbatim(quote_spanned!( expr.span() => + #[verifier::custom_err(#exec_inv_msg)] + #x_iter_name.wf() )); let ghost_inv: Expr = Expr::Verbatim(quote_spanned_vstd!(vstd, expr.span() => #[verifier::custom_err(#ghost_inv_msg)] - #vstd::pervasive::ForLoopGhostIterator::ghost_invariant(&#x_ghost_iter, - #vstd::prelude::infer_spec_for_loop_iter( - &#vstd::pervasive::ForLoopGhostIteratorNew::ghost_iter( - &::core::iter::IntoIterator::into_iter(VERUS_iter)), - &#vstd::pervasive::ForLoopGhostIteratorNew::ghost_iter( - &::core::iter::IntoIterator::into_iter(#expr_inv)), - #print_hint, - )) + match verus_builtin::infer_spec_for_loop_iter( + &::core::iter::IntoIterator::into_iter(#x_verus_iter_init), + &::core::iter::IntoIterator::into_iter(#expr_inv), + #print_hint, + ) { + ::core::option::Option::Some(VERUS_tmp_infer) => #vstd::prelude::spec_eq( + #x_iter_name.init, + #vstd::prelude::Ghost::new(::core::option::Option::Some(VERUS_tmp_infer)) + ), + ::core::option::Option::None => true, + } + )); + let some_inv: Expr = Expr::Verbatim(quote_spanned_vstd!(vstd, expr.span() => + #[verifier::custom_err(#decrease_is_some_msg)] + #[verus::internal(auto_decreases)] + #vstd::prelude::is_variant(#vstd::std_specs::iter::IteratorSpec::decrease(&#x_iter_name.iter), "Some") )); let invariant_for = if let Some(mut invariant) = invariant { for inv in &mut invariant.exprs.exprs { *inv = Expr::Verbatim(quote_spanned_vstd!(vstd, inv.span() => { - let #pat = - #vstd::pervasive::ForLoopGhostIterator::ghost_peek_next(&#x_ghost_iter) - .unwrap_or(#vstd::pervasive::arbitrary()); + let #pat = #vstd::std_specs::iter::IteratorSpec::peek(&#x_iter_name.snapshot.view(), #x_iter_name.index.view()) + .unwrap_or(vstd::pervasive::arbitrary()); #inv })); } if no_loop_invariant.is_none() { - invariant.exprs.exprs.insert(0, exec_inv); + invariant.exprs.exprs.insert(0, init_inv); + invariant.exprs.exprs.insert(1, wf_inv); if no_auto_loop_invariant.is_none() { - invariant.exprs.exprs.insert(1, ghost_inv); + invariant.exprs.exprs.insert(2, ghost_inv); } } Some(Invariant { token: Token![invariant](span), exprs: invariant.exprs }) } else if no_loop_invariant.is_none() && no_auto_loop_invariant.is_none() { - Some(parse_quote_spanned!(span => invariant #exec_inv, #ghost_inv,)) + Some(parse_quote_spanned!(span => invariant #init_inv, #wf_inv, #ghost_inv,)) } else if no_loop_invariant.is_none() && no_auto_loop_invariant.is_some() { - Some(parse_quote_spanned!(span => invariant #exec_inv,)) + Some(parse_quote_spanned!(span => invariant #init_inv, #wf_inv,)) + } else { + None + }; + let inv_except_break = if let Some(mut invariant_except_break) = invariant_except_break { + for inv in &mut invariant_except_break.exprs.exprs { + *inv = Expr::Verbatim(quote_spanned_vstd!(vstd, inv.span() => { + let #pat = #vstd::std_specs::iter::IteratorSpec::peek(&#x_iter_name.snapshot.view(), #x_iter_name.index.view()) + .unwrap_or(vstd::pervasive::arbitrary()); + #inv + })); + } + if no_loop_invariant.is_none() { + invariant_except_break.exprs.exprs.insert(0, some_inv); + } + Some(InvariantExceptBreak { + token: Token![invariant_except_break](span), + exprs: invariant_except_break.exprs, + }) + } else if no_loop_invariant.is_none() { + Some(parse_quote_spanned!(span => invariant_except_break #some_inv,)) } else { None }; if let Some(decreases) = &mut decreases { for expr in &mut decreases.exprs.exprs { *expr = Expr::Verbatim(quote_spanned_vstd!(vstd, expr.span() => { - let #pat = - #vstd::pervasive::ForLoopGhostIterator::ghost_peek_next(&#x_ghost_iter) - .unwrap_or(#vstd::pervasive::arbitrary()); + let #pat = #vstd::std_specs::iter::IteratorSpec::peek(&#x_iter_name.snapshot.view(), #x_iter_name.index.view()) + .unwrap_or(vstd::pervasive::arbitrary()); #expr })); } @@ -3470,76 +3525,98 @@ impl Visitor { attrs.push(mk_verus_attr(span, quote! { auto_decreases })); decreases = Some(parse_quote_spanned_vstd!(vstd, span => decreases - #vstd::pervasive::ForLoopGhostIterator::ghost_decrease(&#x_ghost_iter) + #vstd::std_specs::iter::IteratorSpec::decrease(&#x_iter_name.iter) + //#x_iter_name.iter.decrease() .unwrap_or(#vstd::pervasive::arbitrary()), )) } // REVIEW: we might also want no_auto_loop_invariant to suppress the ensures, // but at the moment, user-supplied ensures aren't supported, so this would be hard to use. let ensure = if no_loop_invariant.is_none() { - Some(parse_quote_spanned_vstd!(vstd, span => - ensures #vstd::pervasive::ForLoopGhostIterator::ghost_ensures(&#x_ghost_iter), - )) + let mut auto_ensures: Ensures = parse_quote_spanned_vstd!(vstd, span => + ensures + #[verus::internal(auto_decreases)] + #vstd::std_specs::iter::IteratorSpec::completes(&#x_iter_name.snapshot.view()), + #[verus::internal(auto_decreases)] + #vstd::prelude::spec_eq(#x_iter_name.index.view(), #x_iter_name.seq().len()), + true, + ); + // REVIEW: Do we need to combine user_ensures.attrs? + if let Some(user_ensures) = ensures { + for expr in user_ensures.exprs.exprs { + auto_ensures.exprs.exprs.insert(0, expr); + } + } + Some(auto_ensures) } else { None }; - self.add_loop_specs(&mut stmts, None, invariant_for, None, ensure, decreases); - let body_exec = Expr::Verbatim(quote_spanned!(span => { + self.add_loop_specs(&mut stmts, inv_except_break, invariant_for, None, ensure, decreases); + let body_exec = Expr::Verbatim(quote_spanned_vstd!(vstd, span => { + #[verus::internal(spec)] + #[verus::internal(unwrapped_binding)] + let mut #x_iter_body_old; // REVIEW: We appear to need this to be mut so we can initialize it in a separate proof block + #[verifier::proof_block] + { + #x_iter_body_old = #x_iter_name; + } #[allow(non_snake_case)] let mut VERUS_loop_next; - match ::core::iter::Iterator::next(&mut #x_exec_iter) { + match #vstd::std_specs::iter::VerusForLoopWrapper::next(&mut #x_iter_name) { ::core::option::Option::Some(VERUS_loop_val) => { VERUS_loop_next = VERUS_loop_val; } ::core::option::Option::None => break, }; let #pat = VERUS_loop_next; + #[verus::internal(spec)] + #[verus::internal(unwrapped_binding)] // REVIEW: We appear to need this to be mut so we can initialize it in a separate proof block + let mut #x_iter_name; + #[verifier::proof_block] + { + #x_iter_name = #x_iter_body_old; + } let () = #body; })); - let mut body: Block = if no_loop_invariant.is_none() { - let body_ghost = Expr::Verbatim(quote_spanned_vstd!(vstd, span => - #[verifier::proof_block] { - #x_ghost_iter = #vstd::pervasive::ForLoopGhostIterator::ghost_advance( - &#x_ghost_iter, &#x_exec_iter); - } - )); - parse_quote_spanned!(span => { - #body_exec - #body_ghost - }) - } else { - parse_quote_spanned!(span => { - #body_exec - }) - }; + let mut body: Block = parse_quote_spanned!(span => { #body_exec }); body.stmts.splice(0..0, stmts); + let mut loop_expr: ExprLoop = parse_quote_spanned!(span => loop #body); loop_expr.label = label; loop_expr.attrs = attrs; - let full_loop: Expr = if no_loop_invariant.is_none() { - Expr::Verbatim(quote_spanned_vstd!(vstd, span => { - #[allow(non_snake_case)] - #[verus::internal(spec)] - let mut #x_ghost_iter; - #[verifier::proof_block] { - #x_ghost_iter = - #vstd::pervasive::ForLoopGhostIteratorNew::ghost_iter(&#x_exec_iter); - } - #loop_expr - })) - } else { - Expr::Verbatim(quote_spanned!(span => { #loop_expr })) - }; - Expr::Verbatim(quote_spanned!(span => { + let f = Expr::Verbatim(quote_spanned_vstd!(vstd, span => { + #[allow(non_snake_case)] + let #x_verus_iter_init = #expr; + #[allow(non_snake_case)] + let #x_exec_iter = ::core::iter::IntoIterator::into_iter(#x_verus_iter_init); + #[allow(non_snake_case)] + let #x_wrapped_iter = #vstd::std_specs::iter::VerusForLoopWrapper::new( + // Real iterator + #x_exec_iter, + // Spec-level iterator (relies on `when_used_as_spec` on into_iter) + #[verifier::ghost_wrapper] + ::vstd::prelude::ghost_exec(#[verifier::ghost_block_wrapped] Some(&#x_exec_iter)), + ); + // Hold on to the initial snapshot value so that after the loop, we know it didn't change #[allow(non_snake_case)] - let VERUS_iter = #expr; + #[verus::internal(spec)] + #[verus::internal(unwrapped_binding)] + let mut #x_snapshot; // REVIEW: We appear to need this to be mut so we can initialize it in a separate proof block + #[verifier::proof_block] + { + #x_snapshot = #x_wrapped_iter.snapshot.view(); + } #[allow(non_snake_case)] - let VERUS_loop_result = match ::core::iter::IntoIterator::into_iter(VERUS_iter) { + let VERUS_loop_result = match #x_wrapped_iter { #[allow(non_snake_case)] - mut #x_exec_iter => #full_loop + mut #x_iter_name => + #[verifier::allow_complex_invariants] + #loop_expr }; VERUS_loop_result - })) + })); + //eprintln!("{}", verus_prettyplease::unparse_expr(&f)); + f } fn extract_quant_triggers( @@ -5027,7 +5104,14 @@ pub(crate) fn for_loop_spec_attr( }; let mut spec_attr = spec_attr; visitor.visit_loop_spec(&mut spec_attr); - let verus_syn::LoopSpec { iter_name, invariants: invariant, decreases, .. } = spec_attr; + let verus_syn::LoopSpec { + iter_name, + invariants: invariant, + invariant_except_breaks: invariant_except_break, + ensures, + decreases, + .. + } = spec_attr; let syn::ExprForLoop { attrs, label, for_token, pat, in_token, expr, body, .. } = forloop; let verus_forloop = ExprForLoop { attrs: attrs.into_iter().map(|a| parse_quote_spanned! {a.span() => #a}).collect(), @@ -5040,7 +5124,9 @@ pub(crate) fn for_loop_spec_attr( in_token: Token![in](in_token.span), expr_name: iter_name.map(|(name, token)| Box::new((name, Token![:](token.span())))), expr: Box::new(Expr::Verbatim(quote_spanned! {expr.span() => #expr})), + invariant_except_break, invariant, + ensures, decreases, body: Block { brace_token: Brace(body.brace_token.span), diff --git a/source/rust_verify/src/attributes.rs b/source/rust_verify/src/attributes.rs index 7a570bbe88..38892fea8d 100644 --- a/source/rust_verify/src/attributes.rs +++ b/source/rust_verify/src/attributes.rs @@ -989,6 +989,15 @@ pub(crate) fn get_custom_err_annotations(attrs: &[Attribute]) -> Result bool { + for attr in parse_attrs_opt(attrs, None) { + if let Attr::AutoDecreases = attr { + return true; + } + } + false +} + #[derive(Debug, Clone)] pub(crate) enum AutoDerivesAttr { Regular, diff --git a/source/rust_verify/src/fn_call_to_vir.rs b/source/rust_verify/src/fn_call_to_vir.rs index 43ff5215bb..d259f76cf5 100644 --- a/source/rust_verify/src/fn_call_to_vir.rs +++ b/source/rust_verify/src/fn_call_to_vir.rs @@ -562,7 +562,16 @@ fn verus_item_to_vir<'tcx, 'a>( } let bctx = &BodyCtxt { external_body: false, in_ghost: true, ..bctx.clone() }; let vir_args = vec_map_result(&subargs, |arg| { - expr_to_vir_consume(&bctx, arg, ExprModifier::REGULAR) + let mut vir_expr = expr_to_vir_consume(&bctx, arg, ExprModifier::REGULAR)?; + // Wrap expressions with #[verus::internal(auto_decreases)] attribute + let arg_attrs = bctx.ctxt.tcx.hir_attrs(arg.hir_id); + if crate::attributes::has_auto_decreases_attr(arg_attrs) { + vir_expr = vir_expr.new_x(vir::ast::ExprX::UnaryOpr( + vir::ast::UnaryOpr::AutoDecreases, + vir_expr.clone(), + )); + } + Ok::(vir_expr) })?; let header = match spec_item { SpecItem::InvariantExceptBreak => { @@ -2111,7 +2120,16 @@ fn get_ensures_arg<'tcx>( } } } - Ok((default_ensures, expr_to_vir_consume(bctx, expr, ExprModifier::REGULAR)?)) + let mut vir_expr = expr_to_vir_consume(bctx, expr, ExprModifier::REGULAR)?; + // Wrap expressions with #[verus::internal(auto_decreases)] attribute + let expr_attrs = bctx.ctxt.tcx.hir_attrs(expr.hir_id); + if crate::attributes::has_auto_decreases_attr(expr_attrs) { + vir_expr = vir_expr.new_x(vir::ast::ExprX::UnaryOpr( + vir::ast::UnaryOpr::AutoDecreases, + vir_expr.clone(), + )); + } + Ok((default_ensures, vir_expr)) } else { err_span(expr.span, "ensures needs a bool expression") } diff --git a/source/rust_verify/src/rust_to_vir_expr.rs b/source/rust_verify/src/rust_to_vir_expr.rs index ba930732fd..f729f36017 100644 --- a/source/rust_verify/src/rust_to_vir_expr.rs +++ b/source/rust_verify/src/rust_to_vir_expr.rs @@ -2534,7 +2534,8 @@ pub(crate) fn expr_to_vir_innermost<'tcx>( let bctx = &BodyCtxt { loop_isolation, ..bctx.clone() }; let typ = typ_of_node_unadjusted(bctx, block.span, &block.hir_id, false)?; let mut body = block_to_vir(bctx, block, &expr.span, &typ, ExprModifier::REGULAR)?; - let header = vir::headers::read_header(&mut body, &vir::headers::HeaderAllows::Loop)?; + let mut header = + vir::headers::read_header(&mut body, &vir::headers::HeaderAllows::Loop)?; let label = label.map(|l| l.ident.to_string()); use crate::attributes::get_allow_exec_allows_no_decreases_clause_walk_parents; let allow_no_decreases = @@ -2544,6 +2545,12 @@ pub(crate) fn expr_to_vir_innermost<'tcx>( } else { header.decrease.clone() }; + if expr_vattrs.auto_decreases && allow_no_decreases { + // Filter out auto_decreases invariants if we're not checking for termination + // (at present, we only add them to invariant_except_break) + Arc::make_mut(&mut header.invariant_except_break) + .retain(|e| !matches!(&e.x, ExprX::UnaryOpr(UnaryOpr::AutoDecreases, _))); + } Ok(ExprOrPlace::Expr(bctx.spanned_typed_new( *header_span, &expr_typ()?, @@ -2555,6 +2562,7 @@ pub(crate) fn expr_to_vir_innermost<'tcx>( cond: None, body, invs: header.loop_invariants(), + //invs, decrease, }, ))) diff --git a/source/rust_verify_test/tests/exec_termination.rs b/source/rust_verify_test/tests/exec_termination.rs index 3c6bc8d35a..23e3a09558 100644 --- a/source/rust_verify_test/tests/exec_termination.rs +++ b/source/rust_verify_test/tests/exec_termination.rs @@ -190,8 +190,8 @@ test_verify_one_file! { fn a() { let mut i: i8 = 0; for x in iter: 0..10 - invariant i == iter.cur * 3, - decreases 10 - iter.cur + invariant i == x * 3, + decreases 10 - iter.index@ { i += 3; } @@ -222,7 +222,7 @@ test_verify_one_file! { let mut i: i8 = 0; // syntax macro inserts decreases clause automatically for x in iter: 0..10 - invariant i == iter.cur * 3, + invariant i == x * 3, { i += 3; } diff --git a/source/rust_verify_test/tests/loops.rs b/source/rust_verify_test/tests/loops.rs index c65085cd90..a80f8b72c5 100644 --- a/source/rust_verify_test/tests/loops.rs +++ b/source/rust_verify_test/tests/loops.rs @@ -1118,16 +1118,35 @@ test_verify_one_file_with_options! { } => Err(e) => assert_one_fails(e) } +test_verify_one_file! { + #[test] for_loop_history verus_code! { + use vstd::prelude::*; + fn test_basic() { + let v: Vec = vec![1, 2, 3, 4, 5, 6]; + let mut w: Vec = Vec::new(); + + for x in y: v + invariant + w@ == y.history(), + { + w.push(x); + } + assert(w.len() == v.len()); + assert(w@ == v@); + } + } => Ok(()) +} + test_verify_one_file_with_options! { #[test] for_loop1 ["exec_allows_no_decreases_clause"] => verus_code! { use vstd::prelude::*; fn test_loop() { let mut n: u64 = 0; for x in iter: 0..10 - invariant n == iter.cur * 3, + invariant n == x * 3, { assert(x < 10); - assert(x == iter.cur); + assert(x == iter.index@); n += 3; } assert(n == 30); @@ -1147,10 +1166,10 @@ test_verify_one_file_with_options! { fn test_loop_fail() { let mut n: u64 = 0; for x in iter: 0..10 - invariant n == iter.cur * 3, + invariant n == x * 3, { assert(x < 9); // FAILS - assert(x == iter.cur); + assert(x == iter.index@); n += 3; } assert(n == 30); @@ -1166,26 +1185,26 @@ test_verify_one_file_with_options! { let mut end = 10; for x in iter: 0..end invariant - n == iter.cur * 3, + n == x * 3, end == 10, { assert(x < 10); - assert(x == iter.cur); + assert(x == iter.index@); n += 3; } assert(n == 30); } + // With the modification of end, we lose all info about the initial state of iter fn test_loop_fail() { let mut n: u64 = 0; let mut end = 10; for x in iter: 0..end invariant - n == iter.cur * 3, + n == x * 3, // FAILS end == 10, { assert(x < 10); // FAILS - assert(x == iter.cur); n += 3; end = end + 0; // causes end to be non-constant, so loop needs more invariants } @@ -1193,20 +1212,21 @@ test_verify_one_file_with_options! { fn non_spec() {} + // With the modification of end, we lose all info about the initial state of iter fn test_loop_modes_transient_state() { let mut n: u64 = 0; let mut end = 10; // test Typing::snapshot_transient_state for x in iter: 0..({let z = end; non_spec(); z}) invariant - n == iter.cur * 3, + n == x * 3, // FAILS end == 10, { n += 3; end = end + 0; // causes end to be non-constant } } - } => Err(e) => assert_one_fails(e) + } => Err(e) => assert_fails(e, 3) } test_verify_one_file_with_options! { @@ -1220,7 +1240,8 @@ test_verify_one_file_with_options! { let mut v: Vec = Vec::new(); for i in iter: 0..n invariant - v@ =~= iter@, + v.len() == iter.index@, + forall |i| 0 <= i < v.len() ==> v[i] == iter.seq()[i], { v.push(i); } @@ -1235,7 +1256,8 @@ test_verify_one_file_with_options! { let mut v: Vec = Vec::new(); for i in iter: 0..n invariant - v@ =~= iter@, // FAILS + v.len() == iter.index@, + forall |i| 0 <= i < v.len() ==> v[i] == iter.seq()[i], // FAILS { v.push(0); } @@ -1244,130 +1266,130 @@ test_verify_one_file_with_options! { } => Err(e) => assert_one_fails(e) } -test_verify_one_file_with_options! { - #[test] for_loop_vec_custom_iterator ["exec_allows_no_decreases_clause"] => verus_code! { - use vstd::prelude::*; - - pub uninterp spec fn spec_phantom_data() -> core::marker::PhantomData; - - pub struct VecIterCopy<'a, T: 'a> { - pub vec: &'a Vec, - pub cur: usize, - } - - impl<'a, T: Copy> Iterator for VecIterCopy<'a, T> { - type Item = T; - fn next(&mut self) -> (item: Option) - ensures - self.vec == old(self).vec, - old(self).cur < self.vec.len() ==> self.cur == old(self).cur + 1, - old(self).cur < self.vec.len() ==> item == Some(self.vec[old(self).cur as int]), - old(self).cur >= self.vec.len() ==> item.is_none() && self.cur == old(self).cur, - { - if self.cur < self.vec.len() { - let item = self.vec[self.cur]; - self.cur = self.cur + 1; - Some(item) - } else { - None - } - } - } - - pub struct VecGhostIterCopy<'a, T> { - pub seq: Seq, - pub cur: int, - pub phantom: core::marker::PhantomData<&'a T>, - } - - impl<'a, T: 'a> vstd::pervasive::ForLoopGhostIteratorNew for VecIterCopy<'a, T> { - type GhostIter = VecGhostIterCopy<'a, T>; - - open spec fn ghost_iter(&self) -> VecGhostIterCopy<'a, T> { - VecGhostIterCopy { - seq: self.vec@, - cur: 0, - phantom: spec_phantom_data(), - } - } - } - - impl<'a, T: 'a> vstd::pervasive::ForLoopGhostIterator for VecGhostIterCopy<'a, T> { - type ExecIter = VecIterCopy<'a, T>; - type Item = T; - type Decrease = int; - - open spec fn exec_invariant(&self, exec_iter: &VecIterCopy<'a, T>) -> bool { - &&& self.seq == exec_iter.vec@ - &&& self.cur == exec_iter.cur - } - - open spec fn ghost_invariant(&self, init: Option<&Self>) -> bool { - &&& 0 <= self.cur <= self.seq.len() - &&& if let Some(init) = init { - init.seq == self.seq - } else { - true - } - } - - open spec fn ghost_ensures(&self) -> bool { - self.cur >= self.seq.len() - } - - open spec fn ghost_decrease(&self) -> Option { - Some(self.seq.len() - self.cur) - } - - open spec fn ghost_peek_next(&self) -> Option { - if 0 <= self.cur < self.seq.len() { - Some(self.seq[self.cur]) - } else { - None - } - } - - open spec fn ghost_advance(&self, _exec_iter: &VecIterCopy) -> VecGhostIterCopy<'a, T> { - VecGhostIterCopy { cur: self.cur + 1, ..*self } - } - } - - impl<'a, T: 'a> vstd::view::View for VecGhostIterCopy<'a, T> { - type V = Seq; - - open spec fn view(&self) -> Seq { - self.seq.subrange(0, self.cur) - } - } - - spec fn vec_iter_copy_spec<'a, T: 'a>(vec: &'a Vec) -> VecIterCopy<'a, T> { - VecIterCopy { vec, cur: 0 } - } - - #[verifier::when_used_as_spec(vec_iter_copy_spec)] - fn vec_iter_copy<'a, T: 'a>(vec: &'a Vec) -> (iter: VecIterCopy<'a, T>) - ensures - iter == (VecIterCopy { vec, cur: 0 }), - { - VecIterCopy { vec, cur: 0 } - } - - fn all_positive(v: &Vec) -> (b: bool) - ensures - b <==> (forall|i: int| 0 <= i < v.len() ==> v[i] > 0), - { - let mut b: bool = true; - - for x in iter: vec_iter_copy(v) - invariant - b <==> (forall|i: int| 0 <= i < iter.cur ==> v[i] > 0), - { - b = b && x > 0; - } - b - } - } => Ok(()) -} +//test_verify_one_file_with_options! { +// #[test] for_loop_vec_custom_iterator ["exec_allows_no_decreases_clause"] => verus_code! { +// use vstd::prelude::*; +// +// pub uninterp spec fn spec_phantom_data() -> core::marker::PhantomData; +// +// pub struct VecIterCopy<'a, T: 'a> { +// pub vec: &'a Vec, +// pub cur: usize, +// } +// +// impl<'a, T: Copy> Iterator for VecIterCopy<'a, T> { +// type Item = T; +// fn next(&mut self) -> (item: Option) +// ensures +// self.vec == old(self).vec, +// old(self).cur < self.vec.len() ==> self.cur == old(self).cur + 1, +// old(self).cur < self.vec.len() ==> item == Some(self.vec[old(self).cur as int]), +// old(self).cur >= self.vec.len() ==> item.is_none() && self.cur == old(self).cur, +// { +// if self.cur < self.vec.len() { +// let item = self.vec[self.cur]; +// self.cur = self.cur + 1; +// Some(item) +// } else { +// None +// } +// } +// } +// +// pub struct VecGhostIterCopy<'a, T> { +// pub seq: Seq, +// pub cur: int, +// pub phantom: core::marker::PhantomData<&'a T>, +// } +// +// impl<'a, T: 'a> vstd::pervasive::ForLoopGhostIteratorNew for VecIterCopy<'a, T> { +// type GhostIter = VecGhostIterCopy<'a, T>; +// +// open spec fn ghost_iter(&self) -> VecGhostIterCopy<'a, T> { +// VecGhostIterCopy { +// seq: self.vec@, +// cur: 0, +// phantom: spec_phantom_data(), +// } +// } +// } +// +// impl<'a, T: 'a> vstd::pervasive::ForLoopGhostIterator for VecGhostIterCopy<'a, T> { +// type ExecIter = VecIterCopy<'a, T>; +// type Item = T; +// type Decrease = int; +// +// open spec fn exec_invariant(&self, exec_iter: &VecIterCopy<'a, T>) -> bool { +// &&& self.seq == exec_iter.vec@ +// &&& self.cur == exec_iter.cur +// } +// +// open spec fn ghost_invariant(&self, init: Option<&Self>) -> bool { +// &&& 0 <= self.cur <= self.seq.len() +// &&& if let Some(init) = init { +// init.seq == self.seq +// } else { +// true +// } +// } +// +// open spec fn ghost_ensures(&self) -> bool { +// self.cur >= self.seq.len() +// } +// +// open spec fn ghost_decrease(&self) -> Option { +// Some(self.seq.len() - self.cur) +// } +// +// open spec fn ghost_peek_next(&self) -> Option { +// if 0 <= self.cur < self.seq.len() { +// Some(self.seq[self.cur]) +// } else { +// None +// } +// } +// +// open spec fn ghost_advance(&self, _exec_iter: &VecIterCopy) -> VecGhostIterCopy<'a, T> { +// VecGhostIterCopy { cur: self.cur + 1, ..*self } +// } +// } +// +// impl<'a, T: 'a> vstd::view::View for VecGhostIterCopy<'a, T> { +// type V = Seq; +// +// open spec fn view(&self) -> Seq { +// self.seq.subrange(0, self.cur) +// } +// } +// +// spec fn vec_iter_copy_spec<'a, T: 'a>(vec: &'a Vec) -> VecIterCopy<'a, T> { +// VecIterCopy { vec, cur: 0 } +// } +// +// #[verifier::when_used_as_spec(vec_iter_copy_spec)] +// fn vec_iter_copy<'a, T: 'a>(vec: &'a Vec) -> (iter: VecIterCopy<'a, T>) +// ensures +// iter == (VecIterCopy { vec, cur: 0 }), +// { +// VecIterCopy { vec, cur: 0 } +// } +// +// fn all_positive(v: &Vec) -> (b: bool) +// ensures +// b <==> (forall|i: int| 0 <= i < v.len() ==> v[i] > 0), +// { +// let mut b: bool = true; +// +// for x in iter: vec_iter_copy(v) +// invariant +// b <==> (forall|i: int| 0 <= i < iter.cur ==> v[i] > 0), +// { +// b = b && x > 0; +// } +// b +// } +// } => Ok(()) +//} test_verify_one_file_with_options! { #[test] loop_invariant_except_break_nonlinear ["exec_allows_no_decreases_clause"] => verus_code! { @@ -1609,3 +1631,121 @@ test_verify_one_file! { } } => Err(err) => assert_vir_error_msg(err, "loop invariants with 'loop_isolation(false)' cannot be invariant_except_break or ensures, unless #[verifier::allow_complex_invariants] is used") } + +test_verify_one_file! { + #[test] for_loop_after_pushes verus_code! { + use vstd::prelude::*; + fn test() { + let mut v1: Vec = Vec::new(); + let mut v2: Vec = Vec::new(); + v1.push(3); + v1.push(4); + assert(v1@ == seq![3u32, 4u32]); + + v2.push(5); + assert(v2.len() == 1); + v2.push(7); + assert(v2@.len() == 2); + v2.insert(1, 6); + assert(v2@ == seq![5u32, 6u32, 7u32]); + + v1.append(&mut v2); + assert(v2@.len() == 0); + assert(v1@.len() == 5); + assert(v1@ == seq![3u32, 4u32, 5u32, 6u32, 7u32]); + v1.remove(2); + assert(v1@ == seq![3u32, 4u32, 6u32, 7u32]); + + v1.push(8u32); + v1.push(9u32); + assert(v1@ == seq![3u32, 4u32, 6u32, 7u32, 8u32, 9u32]); + + v1.swap_remove(5); + assert(v1@ == seq![3u32, 4u32, 6u32, 7u32, 8u32]); + + let mut i: usize = 0; + for x in it: v1 + invariant + i == it.index@, + it.seq() == seq![3u32, 4u32, 6u32, 7u32, 8u32], + { + assert(x > 2); + assert(x < 10); + i = i + 1; + } + } + } => Ok(()) +} + +test_verify_one_file! { + #[test] for_loop_with_break verus_code! { + use vstd::prelude::*; + spec fn sum_u8(s: Seq) -> nat + decreases s.len(), + { + if s.len() == 0 { + 0 + } else { + (sum_u8(s.drop_last()) + s.last()) as nat + } + } + + proof fn sum_u8_monotonic(s: Seq, i: int, j: int) + requires + 0 <= i <= j < s.len(), + ensures + sum_u8(s.take(i)) <= sum_u8(s.take(j)), + decreases j - i, + { + if i == j { + } else { + sum_u8_monotonic(s, i, j - 1); + assert(sum_u8(s.take(i)) <= sum_u8(s.take(j - 1))); + assert(sum_u8(s.take(j - 1)) <= sum_u8(s.take(j))) by { + assert(s.take(j).drop_last() == s.take(j - 1)); // OBSERVE + } + } + } + + proof fn sum_u8_monotonic_forall() + ensures + forall |s: Seq, i, j| #![auto] + 0 <= i <= j < s.len() ==> + sum_u8(s.take(i)) <= sum_u8(s.take(j)), + { + assert forall |s: Seq, i, j| #![auto] 0 <= i <= j < s.len() implies + sum_u8(s.take(i)) <= sum_u8(s.take(j)) by { + sum_u8_monotonic(s, i, j); + } + } + + // Test user-supplied break + fn for_loop_test_skip(v: Vec) { + let mut sum: u8 = 0; + + for x in y: v + invariant_except_break + sum == sum_u8(v@.take(y.index@)) + ensures + (y.index@ == y.seq().len() && sum == sum_u8(y.seq().take(y.index@))) || + (sum == u8::MAX && sum_u8(v@.take(y.index@)) > u8::MAX), + { + assert(v@.take(y.index@ + 1).drop_last() == v@.take(y.index@ as int)); // OBSERVE + if x <= u8::MAX - sum { + sum += x; + } else { + sum = u8::MAX; + break; + } + } + + // Prove that we accomplished our goal + assert(v@.take(v@.len() as int) == v@); // OBSERVE + proof { + // PAPER CUT: Can't call a lemma on the prophetic sequence + sum_u8_monotonic_forall(); + } + assert(sum == sum_u8(v@) || (sum == u8::MAX && sum_u8(v@) > u8::MAX)); + } + } => Ok(()) +} diff --git a/source/rust_verify_test/tests/loops_no_spinoff.rs b/source/rust_verify_test/tests/loops_no_spinoff.rs index ea36b65403..3259afb8de 100644 --- a/source/rust_verify_test/tests/loops_no_spinoff.rs +++ b/source/rust_verify_test/tests/loops_no_spinoff.rs @@ -1107,10 +1107,10 @@ test_verify_one_file_with_options! { let mut n: u64 = 0; #[verifier::loop_isolation(false)] for x in iter: 0..10 - invariant n == iter.cur * 3, + invariant n == x * 3, { assert(x < 10); - assert(x == iter.cur); + assert(x == iter.index@); n += 3; } assert(n == 30); @@ -1132,10 +1132,10 @@ test_verify_one_file_with_options! { let mut n: u64 = 0; #[verifier::loop_isolation(false)] for x in iter: 0..10 - invariant n == iter.cur * 3, + invariant n == x * 3, { assert(x < 9); // FAILS - assert(x == iter.cur); + assert(x == iter.index@); n += 3; } assert(n == 30); @@ -1152,11 +1152,11 @@ test_verify_one_file_with_options! { #[verifier::loop_isolation(false)] for x in iter: 0..end invariant - n == iter.cur * 3, + n == x * 3, end == 10, { assert(x < 10); - assert(x == iter.cur); + assert(x == iter.index@); n += 3; } assert(n == 30); @@ -1168,11 +1168,11 @@ test_verify_one_file_with_options! { #[verifier::loop_isolation(false)] for x in iter: 0..end invariant - n == iter.cur * 3, + n == x * 3, end == 10, { assert(x < 10); - assert(x == iter.cur); + assert(x == iter.index@); n += 3; end = end + 0; // causes end to be non-constant, but ok with loop_isolation(false) } @@ -1187,7 +1187,7 @@ test_verify_one_file_with_options! { #[verifier::loop_isolation(false)] for x in iter: 0..({let z = end; non_spec(); z}) invariant - n == iter.cur * 3, + n == x * 3, end == 10, { n += 3; @@ -1209,7 +1209,8 @@ test_verify_one_file_with_options! { #[verifier::loop_isolation(false)] for i in iter: 0..n invariant - v@ =~= iter@, + v.len() == iter.index@, + forall |i| 0 <= i < v.len() ==> v[i] == iter.seq()[i], { v.push(i); } @@ -1225,7 +1226,8 @@ test_verify_one_file_with_options! { #[verifier::loop_isolation(false)] for i in iter: 0..n invariant - v@ =~= iter@, // FAILS + v.len() == iter.index@, + forall |i| 0 <= i < v.len() ==> v[i] == iter.seq()[i], // FAILS { v.push(0); } @@ -1234,131 +1236,131 @@ test_verify_one_file_with_options! { } => Err(e) => assert_one_fails(e) } -test_verify_one_file_with_options! { - #[test] for_loop_vec_custom_iterator ["exec_allows_no_decreases_clause"] => verus_code! { - use vstd::prelude::*; - - pub uninterp spec fn spec_phantom_data() -> core::marker::PhantomData; - - pub struct VecIterCopy<'a, T: 'a> { - pub vec: &'a Vec, - pub cur: usize, - } - - impl<'a, T: Copy> Iterator for VecIterCopy<'a, T> { - type Item = T; - fn next(&mut self) -> (item: Option) - ensures - self.vec == old(self).vec, - old(self).cur < self.vec.len() ==> self.cur == old(self).cur + 1, - old(self).cur < self.vec.len() ==> item == Some(self.vec[old(self).cur as int]), - old(self).cur >= self.vec.len() ==> item.is_none() && self.cur == old(self).cur, - { - if self.cur < self.vec.len() { - let item = self.vec[self.cur]; - self.cur = self.cur + 1; - Some(item) - } else { - None - } - } - } - - pub struct VecGhostIterCopy<'a, T> { - pub seq: Seq, - pub cur: int, - pub phantom: core::marker::PhantomData<&'a T>, - } - - impl<'a, T: 'a> vstd::pervasive::ForLoopGhostIteratorNew for VecIterCopy<'a, T> { - type GhostIter = VecGhostIterCopy<'a, T>; - - open spec fn ghost_iter(&self) -> VecGhostIterCopy<'a, T> { - VecGhostIterCopy { - seq: self.vec@, - cur: 0, - phantom: spec_phantom_data(), - } - } - } - - impl<'a, T: 'a> vstd::pervasive::ForLoopGhostIterator for VecGhostIterCopy<'a, T> { - type ExecIter = VecIterCopy<'a, T>; - type Item = T; - type Decrease = int; - - open spec fn exec_invariant(&self, exec_iter: &VecIterCopy<'a, T>) -> bool { - &&& self.seq == exec_iter.vec@ - &&& self.cur == exec_iter.cur - } - - open spec fn ghost_invariant(&self, init: Option<&Self>) -> bool { - &&& 0 <= self.cur <= self.seq.len() - &&& if let Some(init) = init { - init.seq == self.seq - } else { - true - } - } - - open spec fn ghost_ensures(&self) -> bool { - self.cur >= self.seq.len() - } - - open spec fn ghost_decrease(&self) -> Option { - Some(self.seq.len() - self.cur) - } - - open spec fn ghost_peek_next(&self) -> Option { - if 0 <= self.cur < self.seq.len() { - Some(self.seq[self.cur]) - } else { - None - } - } - - open spec fn ghost_advance(&self, _exec_iter: &VecIterCopy) -> VecGhostIterCopy<'a, T> { - VecGhostIterCopy { cur: self.cur + 1, ..*self } - } - } - - impl<'a, T: 'a> vstd::view::View for VecGhostIterCopy<'a, T> { - type V = Seq; - - open spec fn view(&self) -> Seq { - self.seq.subrange(0, self.cur) - } - } - - spec fn vec_iter_copy_spec<'a, T: 'a>(vec: &'a Vec) -> VecIterCopy<'a, T> { - VecIterCopy { vec, cur: 0 } - } - - #[verifier::when_used_as_spec(vec_iter_copy_spec)] - fn vec_iter_copy<'a, T: 'a>(vec: &'a Vec) -> (iter: VecIterCopy<'a, T>) - ensures - iter == (VecIterCopy { vec, cur: 0 }), - { - VecIterCopy { vec, cur: 0 } - } - - fn all_positive(v: &Vec) -> (b: bool) - ensures - b <==> (forall|i: int| 0 <= i < v.len() ==> v[i] > 0), - { - let mut b: bool = true; - - #[verifier::loop_isolation(false)] - for x in iter: vec_iter_copy(v) - invariant - b <==> (forall|i: int| 0 <= i < iter.cur ==> v[i] > 0), - { - b = b && x > 0; - } - b - } - } => Ok(()) -} +//test_verify_one_file_with_options! { +// #[test] for_loop_vec_custom_iterator ["exec_allows_no_decreases_clause"] => verus_code! { +// use vstd::prelude::*; +// +// pub uninterp spec fn spec_phantom_data() -> core::marker::PhantomData; +// +// pub struct VecIterCopy<'a, T: 'a> { +// pub vec: &'a Vec, +// pub cur: usize, +// } +// +// impl<'a, T: Copy> Iterator for VecIterCopy<'a, T> { +// type Item = T; +// fn next(&mut self) -> (item: Option) +// ensures +// self.vec == old(self).vec, +// old(self).cur < self.vec.len() ==> self.cur == old(self).cur + 1, +// old(self).cur < self.vec.len() ==> item == Some(self.vec[old(self).cur as int]), +// old(self).cur >= self.vec.len() ==> item.is_none() && self.cur == old(self).cur, +// { +// if self.cur < self.vec.len() { +// let item = self.vec[self.cur]; +// self.cur = self.cur + 1; +// Some(item) +// } else { +// None +// } +// } +// } +// +// pub struct VecGhostIterCopy<'a, T> { +// pub seq: Seq, +// pub cur: int, +// pub phantom: core::marker::PhantomData<&'a T>, +// } +// +// impl<'a, T: 'a> vstd::pervasive::ForLoopGhostIteratorNew for VecIterCopy<'a, T> { +// type GhostIter = VecGhostIterCopy<'a, T>; +// +// open spec fn ghost_iter(&self) -> VecGhostIterCopy<'a, T> { +// VecGhostIterCopy { +// seq: self.vec@, +// cur: 0, +// phantom: spec_phantom_data(), +// } +// } +// } +// +// impl<'a, T: 'a> vstd::pervasive::ForLoopGhostIterator for VecGhostIterCopy<'a, T> { +// type ExecIter = VecIterCopy<'a, T>; +// type Item = T; +// type Decrease = int; +// +// open spec fn exec_invariant(&self, exec_iter: &VecIterCopy<'a, T>) -> bool { +// &&& self.seq == exec_iter.vec@ +// &&& self.cur == exec_iter.cur +// } +// +// open spec fn ghost_invariant(&self, init: Option<&Self>) -> bool { +// &&& 0 <= self.cur <= self.seq.len() +// &&& if let Some(init) = init { +// init.seq == self.seq +// } else { +// true +// } +// } +// +// open spec fn ghost_ensures(&self) -> bool { +// self.cur >= self.seq.len() +// } +// +// open spec fn ghost_decrease(&self) -> Option { +// Some(self.seq.len() - self.cur) +// } +// +// open spec fn ghost_peek_next(&self) -> Option { +// if 0 <= self.cur < self.seq.len() { +// Some(self.seq[self.cur]) +// } else { +// None +// } +// } +// +// open spec fn ghost_advance(&self, _exec_iter: &VecIterCopy) -> VecGhostIterCopy<'a, T> { +// VecGhostIterCopy { cur: self.cur + 1, ..*self } +// } +// } +// +// impl<'a, T: 'a> vstd::view::View for VecGhostIterCopy<'a, T> { +// type V = Seq; +// +// open spec fn view(&self) -> Seq { +// self.seq.subrange(0, self.cur) +// } +// } +// +// spec fn vec_iter_copy_spec<'a, T: 'a>(vec: &'a Vec) -> VecIterCopy<'a, T> { +// VecIterCopy { vec, cur: 0 } +// } +// +// #[verifier::when_used_as_spec(vec_iter_copy_spec)] +// fn vec_iter_copy<'a, T: 'a>(vec: &'a Vec) -> (iter: VecIterCopy<'a, T>) +// ensures +// iter == (VecIterCopy { vec, cur: 0 }), +// { +// VecIterCopy { vec, cur: 0 } +// } +// +// fn all_positive(v: &Vec) -> (b: bool) +// ensures +// b <==> (forall|i: int| 0 <= i < v.len() ==> v[i] > 0), +// { +// let mut b: bool = true; +// +// #[verifier::loop_isolation(false)] +// for x in iter: vec_iter_copy(v) +// invariant +// b <==> (forall|i: int| 0 <= i < iter.cur ==> v[i] > 0), +// { +// b = b && x > 0; +// } +// b +// } +// } => Ok(()) +//} test_verify_one_file_with_options! { #[test] loop_continue_no_break_spinoff ["exec_allows_no_decreases_clause"] => verus_code! { diff --git a/source/rust_verify_test/tests/recursion.rs b/source/rust_verify_test/tests/recursion.rs index b4714dfc4e..5c9334e198 100644 --- a/source/rust_verify_test/tests/recursion.rs +++ b/source/rust_verify_test/tests/recursion.rs @@ -2061,6 +2061,20 @@ test_verify_one_file! { } => Err(e) => assert_fails(e, 3) } +test_verify_one_file! { + #[test] lemma_decreases_poly verus_code! { + spec fn dec(x: &A, y: &A) -> bool { + decreases_to!(x => y) + } + + proof fn test(x: int, y: int) { + assert(dec(&20int, &10int)); + assert(dec(&x, &y) <==> x > y >= 0); + assert(dec(&x, &y) <==> x > y); // FAILS + } + } => Err(e) => assert_one_fails(e) +} + test_verify_one_file! { #[test] commas_in_spec_sigs_github_issue947 verus_code! { spec fn add0(a: nat, b: nat) -> nat diff --git a/source/vir/src/ast.rs b/source/vir/src/ast.rs index 6d1c408b9f..ad13a7d1c4 100644 --- a/source/vir/src/ast.rs +++ b/source/vir/src/ast.rs @@ -512,6 +512,9 @@ pub enum UnaryOpr { IntegerTypeBound(IntegerTypeBoundKind, Mode), /// Custom diagnostic message CustomErr(Arc), + /// Marker for expressions with #[verus::internal(auto_decreases)] attribute + /// Used to filter out auto-generated decreases-related invariants + AutoDecreases, /// Predicate over any type that indicates its mutable references has resolved. /// For &mut T this says the prophetic value == the current value. /// For primitive types this is trivially true. diff --git a/source/vir/src/ast_to_sst.rs b/source/vir/src/ast_to_sst.rs index 6fa8800180..93408c4510 100644 --- a/source/vir/src/ast_to_sst.rs +++ b/source/vir/src/ast_to_sst.rs @@ -596,25 +596,25 @@ pub(crate) fn assume_has_typ(x: &UniqueIdent, typ: &Typ, span: &Span) -> Stm { Spanned::new(span.clone(), StmX::Assume(has_typ)) } -fn loop_body_find_break( +fn loop_body_find_breaks( loop_label: &Option, in_subloop: bool, - found_break: &mut bool, + num_breaks: &mut usize, body: &Expr, ) { let mut f = |expr: &Expr| match &expr.x { ExprX::Loop { body, .. } => { - loop_body_find_break(loop_label, true, found_break, body); + loop_body_find_breaks(loop_label, true, num_breaks, body); VisitorControlFlow::Return } ExprX::BreakOrContinue { label: break_label, is_break: true } => { if break_label.is_none() { if !in_subloop { - *found_break = true; + *num_breaks += 1; } } else { if break_label == loop_label { - *found_break = true; + *num_breaks += 1; } } VisitorControlFlow::Recurse @@ -624,10 +624,10 @@ fn loop_body_find_break( crate::ast_visitor::expr_visitor_walk(body, &mut f); } -fn loop_body_has_break(loop_label: &Option, body: &Expr) -> bool { - let mut found_break = false; - loop_body_find_break(loop_label, false, &mut found_break, body); - found_break +fn loop_body_has_breaks(loop_label: &Option, body: &Expr) -> usize { + let mut num_breaks = 0; + loop_body_find_breaks(loop_label, false, &mut num_breaks, body); + num_breaks } /// Determine if it's possible for control flow to reach the statement after the loop exit. @@ -638,7 +638,7 @@ fn loop_body_has_break(loop_label: &Option, body: &Expr) -> bool { /// be wrapped in the NeverToAny node. It's likely that this check can simply be removed. pub fn can_control_flow_reach_after_loop(expr: &Expr) -> bool { match &expr.x { - ExprX::Loop { label, cond: None, body, .. } => loop_body_has_break(label, body), + ExprX::Loop { label, cond: None, body, .. } => loop_body_has_breaks(label, body) > 0, ExprX::Loop { cond: Some(_), .. } => true, _ => { panic!("expected while loop"); @@ -2409,12 +2409,35 @@ pub(crate) fn expr_to_stm_opt( } else { invs.clone() }; - let has_break = loop_body_has_break(label, body); + let num_breaks = loop_body_has_breaks(label, body); + let has_user_break = num_breaks > if is_for_loop { 1 } else { 0 }; + let invs = if is_for_loop && has_user_break { + // If the user added a break statement, then we need to remove the auto-generated ensures + // clauses (since they typically don't apply any more) + Arc::new( + invs.iter() + .filter_map(|inv| match inv.kind { + LoopInvariantKind::InvariantExceptBreak => Some(inv.clone()), + LoopInvariantKind::InvariantAndEnsures => Some(inv.clone()), + LoopInvariantKind::Ensures => { + if matches!(inv.inv.x, ExprX::UnaryOpr(UnaryOpr::AutoDecreases, _)) + { + None + } else { + Some(inv.clone()) + } + } + }) + .collect(), + ) + } else { + invs.clone() + }; let simple_invs = invs.iter().all(|inv| inv.kind == LoopInvariantKind::InvariantAndEnsures); - let simple_while = !has_break && simple_invs && cond.is_some() && loop_isolation; + let simple_while = !has_user_break && simple_invs && cond.is_some() && loop_isolation; - if allow_complex_invariants && loop_isolation { + if allow_complex_invariants && loop_isolation && !is_for_loop { return Err(error( &expr.span, "attribute 'allow_complex_invariants' can only be used with 'loop_isolation(false)'", @@ -2465,9 +2488,12 @@ pub(crate) fn expr_to_stm_opt( let mut check_recommends: Vec = Vec::new(); let mut invs1: Vec = Vec::new(); for inv in invs.iter() { - // Ensures clauses are unnecessary if loop_isolation is true (implied by allow_complex_invariants), + // Ensures clauses are unnecessary if loop_isolation is true, // since the weakest precondition already tracks all the paths through the breaks into the code after the loop - if allow_complex_invariants && inv.kind == LoopInvariantKind::Ensures { + if !loop_isolation + && allow_complex_invariants + && inv.kind == LoopInvariantKind::Ensures + { continue; } @@ -2476,11 +2502,11 @@ pub(crate) fn expr_to_stm_opt( crate::heuristics::maybe_insert_auto_ext_equal(ctx, &exp, |x| x.invariant); check_recommends.extend(rec); - let (at_entry, at_exit) = if allow_complex_invariants + let (at_entry, at_exit) = if !loop_isolation + && allow_complex_invariants && inv.kind == LoopInvariantKind::InvariantExceptBreak { - // With loop_isolation disabled (implied by allow_complex invariants), an - // invariant_except_break simply becomes an invariant + // With loop_isolation disabled, an invariant_except_break simply becomes an invariant (true, true) } else { match inv.kind { diff --git a/source/vir/src/ast_visitor.rs b/source/vir/src/ast_visitor.rs index cde492a65e..666440368a 100644 --- a/source/vir/src/ast_visitor.rs +++ b/source/vir/src/ast_visitor.rs @@ -280,7 +280,8 @@ pub(crate) trait AstVisitor { UnaryOpr::IsVariant { .. } | UnaryOpr::Field { .. } | UnaryOpr::IntegerTypeBound(..) - | UnaryOpr::CustomErr(..) => R::ret(|| uopr.clone()), + | UnaryOpr::CustomErr(..) + | UnaryOpr::AutoDecreases => R::ret(|| uopr.clone()), } } diff --git a/source/vir/src/def.rs b/source/vir/src/def.rs index d5dfab9ed5..cbfba9abd1 100644 --- a/source/vir/src/def.rs +++ b/source/vir/src/def.rs @@ -201,7 +201,6 @@ pub const AS_TYPE: &str = "as_type"; pub const MK_FUN: &str = "mk_fun"; pub const CONST_INT: &str = "const_int"; pub const CONST_BOOL: &str = "const_bool"; -pub const CHECK_DECREASE_INT: &str = "check_decrease_int"; pub const CHECK_DECREASE_HEIGHT: &str = "check_decrease_height"; pub const HEIGHT: &str = "height"; pub const HEIGHT_LT: &str = "height_lt"; diff --git a/source/vir/src/heuristics.rs b/source/vir/src/heuristics.rs index 9f29d8eac1..905c8c9ed0 100644 --- a/source/vir/src/heuristics.rs +++ b/source/vir/src/heuristics.rs @@ -77,6 +77,9 @@ fn insert_auto_ext_equal(ctx: &Ctx, exp: &Exp) -> Exp { UnaryOpr::CustomErr(_) => { exp.new_x(ExpX::UnaryOpr(op.clone(), insert_auto_ext_equal(ctx, e))) } + UnaryOpr::AutoDecreases => { + exp.new_x(ExpX::UnaryOpr(op.clone(), insert_auto_ext_equal(ctx, e))) + } UnaryOpr::HasResolved(..) => exp.clone(), }, ExpX::Binary(op, e1, e2) => match op { diff --git a/source/vir/src/interpreter.rs b/source/vir/src/interpreter.rs index 8eb9ddda8a..aec55561f6 100644 --- a/source/vir/src/interpreter.rs +++ b/source/vir/src/interpreter.rs @@ -1363,6 +1363,7 @@ fn eval_expr_internal(ctx: &Ctx, state: &mut State, exp: &Exp) -> Result Ok(e), + AutoDecreases => Ok(e), HasResolved(_) => Ok(e), } } diff --git a/source/vir/src/loop_inference.rs b/source/vir/src/loop_inference.rs index f03cea5614..3a6f8729dd 100644 --- a/source/vir/src/loop_inference.rs +++ b/source/vir/src/loop_inference.rs @@ -19,7 +19,7 @@ pub(crate) fn make_option_exp(opt: Option, span: &Span, typ: &Typ) -> Exp { SpannedTyped::new(span, &Arc::new(option_typx), expx) } -// InferSpecForLoopIter produces None if any variables in the express are modified in the loop +// InferSpecForLoopIter produces None if any variables in the expression are modified in the loop fn vars_unmodified( modified_vars: &Arc>, exp: &Exp, diff --git a/source/vir/src/modes.rs b/source/vir/src/modes.rs index 7a7784a47d..1861b10afd 100644 --- a/source/vir/src/modes.rs +++ b/source/vir/src/modes.rs @@ -1015,14 +1015,14 @@ fn get_var_loc_mode( if (*op_mode == Mode::Exec) != (typing.block_ghostness == Ghost::Exec) { return Err(error( &expr.span, - format!("cannot perform operation with mode {}", op_mode), + format!("cannot perform operation with mode {}, {:?}", op_mode, &expr.x), )); } } if outer_mode != *op_mode { return Err(error( &expr.span, - format!("cannot perform operation with mode {}", op_mode), + format!("cannot perform operation with mode {}, {:?}", op_mode, &expr.x), )); } let (mode1, proph1) = @@ -1998,14 +1998,17 @@ fn check_expr_handle_mut_arg( if (*op_mode == Mode::Exec) != (typing.block_ghostness == Ghost::Exec) { return Err(error( &expr.span, - format!("cannot perform operation with mode {}", op_mode), + format!( + "cannot perform operation with mode {}, {:?},\n{:?}", + op_mode, &expr.x, &e1 + ), )); } } if !mode_le(outer_mode, *op_mode) { return Err(error( &expr.span, - format!("cannot perform operation with mode {}", op_mode), + format!("cannot perform operation with mode {}, {:?}", op_mode, &expr.x), )); } let param_mode = mode_join(outer_mode, *from_mode); @@ -2154,6 +2157,11 @@ fn check_expr_handle_mut_arg( check_expr_has_mode(ctxt, record, typing, Mode::Spec, e1, Mode::Spec, outer_proph)?; Ok((Mode::Spec, p)) } + ExprX::UnaryOpr(UnaryOpr::AutoDecreases, e1) => { + let p = + check_expr_has_mode(ctxt, record, typing, Mode::Spec, e1, Mode::Spec, outer_proph)?; + Ok((Mode::Spec, p)) + } ExprX::Loc(e) => { return check_expr_handle_mut_arg( ctxt, diff --git a/source/vir/src/poly.rs b/source/vir/src/poly.rs index f22de7569f..1e2e3f1812 100644 --- a/source/vir/src/poly.rs +++ b/source/vir/src/poly.rs @@ -513,13 +513,6 @@ fn visit_exp(ctx: &Ctx, state: &mut State, exp: &Exp) -> Exp { let exps = visit_exps_poly(ctx, state, exps); mk_exp(ExpX::Call(call_fun.clone(), typs.clone(), exps)) } - CallFun::InternalFun(InternalFun::CheckDecreaseInt) => { - assert!(exps.len() == 3); - let e0 = visit_exp_native(ctx, state, &exps[0]); - let e1 = visit_exp_native(ctx, state, &exps[1]); - let e2 = visit_exp_native(ctx, state, &exps[2]); - mk_exp(ExpX::Call(call_fun.clone(), typs.clone(), Arc::new(vec![e0, e1, e2]))) - } CallFun::InternalFun(InternalFun::CheckDecreaseHeight) => { assert!(exps.len() == 3); let e0 = visit_exp_poly(ctx, state, &exps[0]); @@ -623,6 +616,9 @@ fn visit_exp(ctx: &Ctx, state: &mut State, exp: &Exp) -> Exp { UnaryOpr::CustomErr(_) => { mk_exp_typ(&e1.typ, ExpX::UnaryOpr(op.clone(), e1.clone())) } + UnaryOpr::AutoDecreases => { + mk_exp_typ(&e1.typ, ExpX::UnaryOpr(op.clone(), e1.clone())) + } UnaryOpr::Field(FieldOpr { datatype, variant, diff --git a/source/vir/src/prelude.rs b/source/vir/src/prelude.rs index c6c4d46069..d2915dfc0c 100644 --- a/source/vir/src/prelude.rs +++ b/source/vir/src/prelude.rs @@ -51,7 +51,6 @@ pub(crate) fn prelude_nodes(config: PreludeConfig) -> Vec { let RMul = str_to_node(RMUL); #[allow(non_snake_case)] let RDiv = str_to_node(RDIV); - let check_decrease_int = str_to_node(CHECK_DECREASE_INT); let check_decrease_height = str_to_node(CHECK_DECREASE_HEIGHT); let height = str_to_node(HEIGHT); let height_le = nodes!(_ partial-order 0); @@ -1016,18 +1015,6 @@ pub(crate) fn prelude_nodes(config: PreludeConfig) -> Vec { (declare-fun [height] ([Poly]) [Height]) (declare-fun [height_lt] ([Height] [Height]) Bool) (declare-fun [height_rec_fun] ([Poly]) [Poly]) - (declare-fun [check_decrease_int] (Int Int Bool) Bool) - (axiom (forall ((cur Int) (prev Int) (otherwise Bool)) (! - (= ([check_decrease_int] cur prev otherwise) - (or - (and (<= 0 cur) (< cur prev)) - (and (= cur prev) otherwise) - ) - ) - :pattern (([check_decrease_int] cur prev otherwise)) - :qid prelude_check_decrease_int - :skolemid skolem_prelude_check_decrease_int - ))) (declare-fun [check_decrease_height] ([Poly] [Poly] Bool) Bool) (axiom (forall ((cur [Poly]) (prev [Poly]) (otherwise Bool)) (! (= ([check_decrease_height] cur prev otherwise) @@ -1040,6 +1027,14 @@ pub(crate) fn prelude_nodes(config: PreludeConfig) -> Vec { :qid prelude_check_decrease_height :skolemid skolem_prelude_check_decrease_height ))) + (axiom (forall ((cur Int) (prev Int)) (! + (= ([height_lt] ([height] ([box_int] cur)) ([height] ([box_int] prev))) + (and (<= 0 cur) (< cur prev)) + ) + :pattern (([height_lt] ([height] ([box_int] cur)) ([height] ([box_int] prev)))) + :qid prelude_check_decrease_int_height + :skolemid skolem_prelude_check_decrease_int_height + ))) ); prelude.extend(height_axioms); prelude diff --git a/source/vir/src/recursion.rs b/source/vir/src/recursion.rs index 7b605284c1..0eeea7c5c8 100644 --- a/source/vir/src/recursion.rs +++ b/source/vir/src/recursion.rs @@ -134,10 +134,7 @@ pub(crate) fn check_decrease( SpannedTyped::new(&exp.span, &height_typ(ctx, exp), decreases_at_entryx); // 0 <= decreases_exp < decreases_at_entry - let (args, call_fun) = if height_is_int(&exp.typ) { - let args = vec![exp_for_decrease(ctx, exp)?, decreases_at_entry, dec_exp]; - (args, CallFun::InternalFun(InternalFun::CheckDecreaseInt)) - } else { + let (args, call_fun) = { let call_fun = CallFun::InternalFun(InternalFun::CheckDecreaseHeight); // Coerce to Poly for loops (when we're called after poly.rs) // For recursive functions (loop_id.is_none()), poly.rs will handle this diff --git a/source/vir/src/scc.rs b/source/vir/src/scc.rs index 9c6db14493..b547c6b39f 100644 --- a/source/vir/src/scc.rs +++ b/source/vir/src/scc.rs @@ -271,6 +271,7 @@ impl Graph { sorted_order: Option<&HashMap>, ) -> bool { assert!(self.has_run); + assert!(self.mapping.contains_key(source)); let src = self.mapping[source]; let tgt = self.mapping[target]; let tgt_sort_index = sorted_order.map(|order| order[&self.get_scc_rep(target)]); diff --git a/source/vir/src/sst.rs b/source/vir/src/sst.rs index 428484c1d8..f19a8f8cb6 100644 --- a/source/vir/src/sst.rs +++ b/source/vir/src/sst.rs @@ -51,7 +51,6 @@ pub enum InternalFun { ClosureReq, ClosureEns, DefaultEns, - CheckDecreaseInt, CheckDecreaseHeight, OpenInvariantMask(Fun, usize), } diff --git a/source/vir/src/sst_to_air.rs b/source/vir/src/sst_to_air.rs index 7b9fe4348f..3c75cad4b9 100644 --- a/source/vir/src/sst_to_air.rs +++ b/source/vir/src/sst_to_air.rs @@ -932,7 +932,6 @@ pub(crate) fn exp_to_expr(ctx: &Ctx, exp: &Exp, expr_ctxt: &ExprCtxt) -> Result< InternalFun::ClosureReq => str_ident(crate::def::CLOSURE_REQ), InternalFun::ClosureEns => str_ident(crate::def::CLOSURE_ENS), InternalFun::DefaultEns => str_ident(crate::def::DEFAULT_ENS), - InternalFun::CheckDecreaseInt => str_ident(crate::def::CHECK_DECREASE_INT), InternalFun::CheckDecreaseHeight => { str_ident(crate::def::CHECK_DECREASE_HEIGHT) } @@ -1208,6 +1207,11 @@ pub(crate) fn exp_to_expr(ctx: &Ctx, exp: &Exp, expr_ctxt: &ExprCtxt) -> Result< // ignore it here. return exp_to_expr(ctx, exp, expr_ctxt); } + UnaryOpr::AutoDecreases => { + // AutoDecreases is just a marker for filtering invariants + // during loop construction. Unwrap and process the inner expression. + return exp_to_expr(ctx, exp, expr_ctxt); + } UnaryOpr::HasResolved(t) => { let mut exprs: Vec = typ_to_ids(t); exprs.push(exp_to_expr(ctx, exp, expr_ctxt)?); diff --git a/source/vir/src/sst_util.rs b/source/vir/src/sst_util.rs index 814ea053d9..7ae0018cfe 100644 --- a/source/vir/src/sst_util.rs +++ b/source/vir/src/sst_util.rs @@ -517,6 +517,9 @@ impl ExpX { CustomErr(_msg) => { (format!("with_diagnostic({})", exp.x.to_user_string(global)), 99) } + AutoDecreases => { + return exp.x.to_string_prec(global, precedence); + } } } Binary(op, e1, e2) => { diff --git a/source/vir/src/sst_visitor.rs b/source/vir/src/sst_visitor.rs index 275385f742..e0cc100a04 100644 --- a/source/vir/src/sst_visitor.rs +++ b/source/vir/src/sst_visitor.rs @@ -282,7 +282,8 @@ pub(crate) trait Visitor { UnaryOpr::IsVariant { .. } | UnaryOpr::Field { .. } | UnaryOpr::IntegerTypeBound(..) - | UnaryOpr::CustomErr(..) => R::ret(|| op.clone()), + | UnaryOpr::CustomErr(..) + | UnaryOpr::AutoDecreases => R::ret(|| op.clone()), }?; R::ret(|| exp_new(ExpX::UnaryOpr(R::get(op), R::get(e1)))) } diff --git a/source/vir/src/triggers.rs b/source/vir/src/triggers.rs index 632062888a..045aad03e1 100644 --- a/source/vir/src/triggers.rs +++ b/source/vir/src/triggers.rs @@ -141,6 +141,10 @@ fn check_trigger_expr_arg(state: &mut State, arg: &Exp) { // recurse inside coercions check_trigger_expr_arg(state, arg) } + UnaryOpr::AutoDecreases => { + // recurse inside marker + check_trigger_expr_arg(state, arg) + } UnaryOpr::IsVariant { .. } | UnaryOpr::Field { .. } | UnaryOpr::IntegerTypeBound(..) @@ -201,6 +205,7 @@ fn check_trigger_expr( ExpX::BinaryOpr(crate::ast::BinaryOpr::ExtEq(..), _, _) => {} ExpX::Unary(UnaryOp::Clip { .. }, _) | ExpX::Binary(BinaryOp::Arith(..), _, _) => {} ExpX::UnaryOpr(UnaryOpr::HasResolved(_), _) => {} + ExpX::UnaryOpr(UnaryOpr::AutoDecreases, _) => {} _ => { return Err(error( &exp.span, @@ -293,7 +298,7 @@ fn check_trigger_expr( }, ExpX::UnaryOpr(op, arg) => match op { UnaryOpr::Box(_) | UnaryOpr::Unbox(_) => panic!("unexpected box"), - UnaryOpr::CustomErr(_) => Ok(()), + UnaryOpr::CustomErr(_) | UnaryOpr::AutoDecreases => Ok(()), UnaryOpr::IsVariant { .. } | UnaryOpr::Field { .. } => { check_trigger_expr_arg(state, arg); Ok(()) diff --git a/source/vir/src/triggers_auto.rs b/source/vir/src/triggers_auto.rs index e68744bc54..9b2b74cf7f 100644 --- a/source/vir/src/triggers_auto.rs +++ b/source/vir/src/triggers_auto.rs @@ -351,9 +351,7 @@ fn gather_terms(ctxt: &mut Ctxt, ctx: &Ctx, exp: &Exp, depth: u64) -> (bool, Ter InternalFun::ClosureReq | InternalFun::ClosureEns | InternalFun::DefaultEns, ) => (is_pure, Arc::new(TermX::App(App::ClosureSpec, Arc::new(all_terms)))), CallFun::InternalFun( - InternalFun::CheckDecreaseInt - | InternalFun::CheckDecreaseHeight - | InternalFun::OpenInvariantMask(..), + InternalFun::CheckDecreaseHeight | InternalFun::OpenInvariantMask(..), ) => (is_pure, Arc::new(TermX::App(ctxt.other(), Arc::new(all_terms)))), } } @@ -417,7 +415,9 @@ fn gather_terms(ctxt: &mut Ctxt, ctx: &Ctx, exp: &Exp, depth: u64) -> (bool, Ter } ExpX::UnaryOpr(UnaryOpr::Box(_), _) => panic!("unexpected box"), ExpX::UnaryOpr(UnaryOpr::Unbox(_), _) => panic!("unexpected box"), - ExpX::UnaryOpr(UnaryOpr::CustomErr(_), e1) => gather_terms(ctxt, ctx, e1, depth), + ExpX::UnaryOpr(UnaryOpr::CustomErr(_) | UnaryOpr::AutoDecreases, e1) => { + gather_terms(ctxt, ctx, e1, depth) + } ExpX::UnaryOpr(UnaryOpr::HasType(_), _) => { (false, Arc::new(TermX::App(ctxt.other(), Arc::new(vec![])))) } diff --git a/source/vstd/std_specs/core.rs b/source/vstd/std_specs/core.rs index 46198085e4..9bab733774 100644 --- a/source/vstd/std_specs/core.rs +++ b/source/vstd/std_specs/core.rs @@ -69,25 +69,6 @@ pub trait ExPtrPointee: PointeeSized { Copy + Send + Sync + Ord + core::hash::Hash + Unpin + core::fmt::Debug + Sized + core::marker::Freeze; } -#[verifier::external_trait_specification] -pub trait ExIterator { - type ExternalTraitSpecificationFor: core::iter::Iterator; - - type Item; - - fn next(&mut self) -> Option; -} - -#[verifier::external_trait_specification] -pub trait ExIntoIterator { - type ExternalTraitSpecificationFor: core::iter::IntoIterator; -} - -#[verifier::external_trait_specification] -pub trait ExIterStep: Clone + PartialOrd + Sized { - type ExternalTraitSpecificationFor: core::iter::Step; -} - #[verifier::external_trait_specification] pub trait ExBorrow where Borrowed: ?Sized { type ExternalTraitSpecificationFor: core::borrow::Borrow; diff --git a/source/vstd/std_specs/iter.rs b/source/vstd/std_specs/iter.rs new file mode 100644 index 0000000000..1948f942bb --- /dev/null +++ b/source/vstd/std_specs/iter.rs @@ -0,0 +1,236 @@ +use super::super::prelude::*; +use crate::seq::{axiom_seq_subrange_index, axiom_seq_subrange_len}; + +use verus as verus_; + +use core::iter::Iterator; + +verus_! { + +#[verifier::external_trait_specification] +pub trait ExIntoIterator { + type ExternalTraitSpecificationFor: core::iter::IntoIterator; +} + +#[verifier::external_trait_specification] +pub trait ExIterStep: Clone + PartialOrd + Sized { + type ExternalTraitSpecificationFor: core::iter::Step; +} + +#[verifier::external_trait_specification] +#[verifier::external_trait_extension(IteratorSpec via IteratorSpecImpl)] +pub trait ExIterator { + type ExternalTraitSpecificationFor: Iterator; + + type Item; + + /// This iterator obeys the specifications below on `next`, + /// expressed in terms of prophetic spec functions. + /// Only iterators that terminate (i.e., eventually return None + /// and then continue to return None) should use this interface. + spec fn obeys_prophetic_iter_laws(&self) -> bool; + + /// Sequence of items that will (eventually) be returned + #[verifier::prophetic] + spec fn remaining(&self) -> Seq; + + /// Does this iterator complete with a `None` after the above sequence? + /// (As opposed to hanging indefinitely on a `next()` call) + /// Trivially true for most iterators but important for iterators + /// that apply an exec closure that may not terminate. + #[verifier::prophetic] + spec fn completes(&self) -> bool; + + /// Advances the iterator and returns the next value. + fn next(&mut self) -> (ret: Option) + ensures + // The iterator consistently obeys, completes, and decreases throughout its lifetime + self.obeys_prophetic_iter_laws() == old(self).obeys_prophetic_iter_laws(), + self.obeys_prophetic_iter_laws() ==> self.completes() == old(self).completes(), + self.obeys_prophetic_iter_laws() ==> (old(self).decrease() is Some <==> self.decrease() is Some), + // `next` pops the head of the prophesized remaining(), or returns None + self.obeys_prophetic_iter_laws() ==> + ({ + if old(self).remaining().len() > 0 { + &&& self.remaining() == old(self).remaining().drop_first() + &&& ret == Some(old(self).remaining()[0]) + } else { + self.remaining() === old(self).remaining() && ret === None && self.completes() + } + }), + // If the iterator isn't done yet, then it successfully decreases its metric (if any) + self.obeys_prophetic_iter_laws() && old(self).remaining().len() > 0 && self.decrease() is Some ==> + decreases_to!(old(self).decrease()->0 => self.decrease()->0), + ; + + /******* Mechanisms that support ergonomic `for` loops *********/ + + /// Value used by default for the decreases clause when no explicit decreases clause is provided + /// (the user can override this with an explicit decreases clause). + /// If there's no appropriate metric to decrease, this can return None, + /// and the user will have to provide an explicit decreases clause. + spec fn decrease(&self) -> Option; + + /// Invariant relating the iterator to the initial expression that created it + /// (e.g., `my_vec.iter()`). This allows for more ergonomic/intuitive invariants. + /// When the analysis can infer a spec initial value (by discovering a `when_used_as_spec` + /// annotation), the analysis places the value in init. + #[verifier::prophetic] + spec fn initial_value_inv(&self, init: &Self) -> bool; + + // If we can make a useful guess as to what the i-th value will be, return it. + // Otherwise, return None. + spec fn peek(&self, index: int) -> Option; +} + +// #[verifier::external_trait_specification] +// #[verifier::external_trait_extension(DoubleEndedIteratorSpec via DoubleEndedIteratorSpecImpl)] +// pub trait ExDoubleEndedIterator : Iterator { +// type ExternalTraitSpecificationFor: DoubleEndedIterator; + +// fn next_back(&mut self) -> (ret: Option<::Item>) +// ensures +// true, +// // The iterator consistently obeys, completes, and decreases throughout its lifetime +// //self.obeys_prophetic_iter_laws() == +// old(self).obeys_prophetic_iter_laws(), +// // self.obeys_prophetic_iter_laws() ==> self.completes() == old(self).completes(), +// // self.obeys_prophetic_iter_laws() ==> (old(self).decrease() is Some <==> self.decrease() is Some), +// // // `next` pops the tail of the prophesized remaining(), or returns None +// // self.obeys_prophetic_iter_laws() ==> +// // ({ +// // if old(self).remaining().len() > 0 { +// // self.remaining() == old(self).remaining().drop_last() +// // && ret == Some(old(self).remaining().last()) +// // } else { +// // self.remaining() === old(self).remaining() && ret === None && self.completes() +// // } +// // }), +// // // If the iterator isn't done yet, then it successfully decreases its metric (if any) +// // self.obeys_prophetic_iter_laws() && old(self).remaining().len() > 0 && self.decrease() is Some ==> +// // old(self).decrease()->0 > self.decrease()->0, +// ; + +// /******* Mechanisms that support ergonomic `for` loops *********/ + +// // If we can make a useful guess as to what the i-th value from the back will be, return it. +// // Otherwise, return None. +// spec fn peek_back(&self, index: int) -> Option; +// } + +/// REVIEW: Despite the name, VerusForLoopWrapper doesn't implement Iterator. +/// What would be a better name? +pub struct VerusForLoopWrapper<'a, I: Iterator> { + pub index: Ghost, + pub snapshot: Ghost, + pub init: Ghost>, + pub iter: I, + pub history: Ghost>, +} + +impl <'a, I: Iterator> VerusForLoopWrapper<'a, I> { + #[verifier::prophetic] + pub open spec fn seq(self) -> Seq { + self.snapshot@.remaining() + } + + // Keep the interface for history and seq the same + pub open spec fn history(self) -> Seq { + self.history@ + } + + /// These properties help maintain the properties in wf, + /// but they don't need to be exposed to the client + #[verifier::prophetic] + pub closed spec fn wf_inner(self) -> bool { + &&& self.iter.remaining().len() == self.seq().len() - self.index@ + &&& forall |i| 0 <= i < self.iter.remaining().len() ==> #[trigger] self.iter.remaining()[i] == self.seq()[self.index@ + i] + &&& self.iter.completes() ==> self.snapshot@.completes() + } + + /// These properties are needed for the client code to verify + #[verifier::prophetic] + pub open spec fn wf(self) -> bool { + &&& 0 <= self.index@ <= self.seq().len() + &&& self.init@ matches Some(init) ==> self.snapshot@.initial_value_inv(init) + &&& self.wf_inner() + &&& self.iter.obeys_prophetic_iter_laws() ==> { + &&& self.history@.len() == self.index@ + &&& forall |i| 0 <= i < self.index@ ==> #[trigger] self.history@[i] == self.seq()[i] + } + } + + /// Bundle the real iterator with its ghost state and loop invariants + pub fn new(iter: I, init: Ghost>) -> (s: Self) + requires + init@ matches Some(i) ==> iter.initial_value_inv(i), + ensures + s.index == 0, + s.snapshot == iter, + s.init == init, + s.iter == iter, + s.history@ == Seq::::empty(), + s.wf(), + { + broadcast use crate::seq::axiom_seq_empty; + VerusForLoopWrapper { + index: Ghost(0), + snapshot: Ghost(iter), + init: init, + iter, + history: Ghost(Seq::empty()), + } + } + + /// Advance the underlying (real) iterator and prove + /// that the loop invariants are preserved. + pub fn next(&mut self) -> (ret: Option) + requires + old(self).wf(), + ensures + self.seq() == old(self).seq(), + self.index@ == old(self).index@ + if ret is Some { 1int } else { 0 }, + self.snapshot == old(self).snapshot, + self.init == old(self).init, + self.iter.obeys_prophetic_iter_laws() ==> self.wf(), + self.iter.obeys_prophetic_iter_laws() && ret is None ==> + self.snapshot@.completes() && self.index@ == self.seq().len(), + self.iter.obeys_prophetic_iter_laws() ==> (ret matches Some(r) ==> + r == old(self).seq()[old(self).index@]), + // History updates always hold + ret matches Some(i) ==> self.history@ == old(self).history@.push(i), + ret is None ==> self.history@ == old(self).history@, + // TODO: Uncomment this line to replace everything below, once general mutable refs are supported + // call_ensures(I::next, (&mut old(self).iter,), ret), + self.iter.obeys_prophetic_iter_laws() == old(self).iter.obeys_prophetic_iter_laws(), + self.iter.obeys_prophetic_iter_laws() ==> self.iter.completes() == old(self).iter.completes(), + self.iter.obeys_prophetic_iter_laws() ==> (old(self).iter.decrease() is Some <==> self.iter.decrease() is Some), + self.iter.obeys_prophetic_iter_laws() ==> + ({ + if old(self).iter.remaining().len() > 0 { + &&& self.iter.remaining() == old(self).iter.remaining().drop_first() + &&& ret == Some(old(self).iter.remaining()[0]) + } else { + self.iter.remaining() === old(self).iter.remaining() && ret === None && self.iter.completes() + } + }), + self.iter.obeys_prophetic_iter_laws() && old(self).iter.remaining().len() > 0 && self.iter.decrease() is Some ==> + decreases_to!(old(self).iter.decrease()->0 => self.iter.decrease()->0), + { + let ghost old_history = self.history@; + let ret = self.iter.next(); + if ret.is_some() { + self.history = Ghost(old_history.push(ret->0)); + } + proof { + broadcast use crate::seq::group_seq_axioms; + if ret.is_some() { + self.index@ = self.index@ + 1; + } + } + ret + } +} + + +} // verus! diff --git a/source/vstd/std_specs/mod.rs b/source/vstd/std_specs/mod.rs index 19bb46fb64..0abd0a0be5 100644 --- a/source/vstd/std_specs/mod.rs +++ b/source/vstd/std_specs/mod.rs @@ -10,6 +10,7 @@ pub mod control_flow; pub mod convert; pub mod core; pub mod default; +pub mod iter; pub mod manually_drop; pub mod maybe_uninit; pub mod ops; diff --git a/source/vstd/std_specs/range.rs b/source/vstd/std_specs/range.rs index 9ccc272806..cfc29d5113 100644 --- a/source/vstd/std_specs/range.rs +++ b/source/vstd/std_specs/range.rs @@ -1,6 +1,7 @@ use super::super::prelude::*; use super::super::view::View; use super::cmp::{PartialOrdIs, PartialOrdSpec}; +use crate::std_specs::iter::IteratorSpec; use core::ops::{Range, RangeInclusive}; verus! { @@ -64,6 +65,7 @@ impl View for RangeInclusive { pub trait StepSpec where Self: Sized { // REVIEW: it would be nice to be able to use SpecOrd::spec_lt (not yet supported) + // TODO: We should now be able to use cmp_spec or partial_cmp_spec here. spec fn spec_is_lt(self, other: Self) -> bool; spec fn spec_steps_between(self, end: Self) -> Option; @@ -81,12 +83,6 @@ pub trait StepSpec where Self: Sized { pub uninterp spec fn spec_range_next(a: Range) -> (Range, Option); -pub assume_specification[ Range::::next ](range: &mut Range) -> (r: - Option) - ensures - (*range, r) == spec_range_next(*old(range)), -; - /// Range::contains method is valid and safe to use only when cmp operations are implemented to satisfy /// obeys_partial_cmp_spec. Specifically, the comparison must be deterministic, and `lt` (less than) /// and `le` (less than or equal to) must define total orders. @@ -116,76 +112,66 @@ pub assume_specification[ RangeInclusive::::new ](start: Idx, end: Idx ret@.exhausted == false, ; -pub struct RangeGhostIterator { - pub start: A, - pub cur: A, - pub end: A, -} - -impl super::super::pervasive::ForLoopGhostIteratorNew for Range { - type GhostIter = RangeGhostIterator; - - open spec fn ghost_iter(&self) -> RangeGhostIterator { - RangeGhostIterator { start: self.start, cur: self.start, end: self.end } +impl crate::std_specs::iter::IteratorSpecImpl for Range { + open spec fn obeys_prophetic_iter_laws(&self) -> bool { + true } -} - -impl< - A: StepSpec + core::iter::Step, -> super::super::pervasive::ForLoopGhostIterator for RangeGhostIterator { - type ExecIter = Range; - type Item = A; - - type Decrease = int; - - open spec fn exec_invariant(&self, exec_iter: &Range) -> bool { - &&& self.cur == exec_iter.start - &&& self.end == exec_iter.end - } - - open spec fn ghost_invariant(&self, init: Option<&Self>) -> bool { - &&& self.start.spec_is_lt(self.cur) || self.start == self.cur - &&& self.cur.spec_is_lt(self.end) || self.cur - == self.end - // TODO (not important): use new "matches ==>" syntax here - &&& if let Some(init) = init { - &&& init.start == init.cur - &&& init.start == self.start - &&& init.end == self.end - } else { - true - } + open spec fn remaining(&self) -> Seq { + Seq::new( + self.start.spec_steps_between_int(self.end) as nat, + |i: int| self.start.spec_forward_checked_int(i).unwrap(), + ) } - open spec fn ghost_ensures(&self) -> bool { - !self.cur.spec_is_lt(self.end) - } + uninterp spec fn completes(&self) -> bool; - open spec fn ghost_decrease(&self) -> Option { - Some(self.cur.spec_steps_between_int(self.end)) + #[verifier::prophetic] + open spec fn initial_value_inv(&self, init: &Self) -> bool { + // Standard invariants for the iterator itself + &&& IteratorSpec::remaining(self) == Seq::new( + self.start.spec_steps_between_int(self.end) as nat, + |i: int| self.start.spec_forward_checked_int(i).unwrap(), + ) + &&& self.start.spec_steps_between_int(self.end) >= 0 || IteratorSpec::remaining(self).len() + == 0 + // &&& (forall|index| + // 0 <= index <= self.start.spec_steps_between_int(self.end) ==> { + // let cur = #[trigger] self.start.spec_forward_checked_int(index).unwrap(); + // &&& self.start.spec_is_lt(cur) || self.start == cur + // &&& self.start.spec_is_lt(self.end) || self.start == self.end ==> cur.spec_is_lt( + // self.end, + // ) || cur == self.end + // }) + // Connections to init + &&& self.start == init.start + &&& self.end == init.end + &&& IteratorSpec::remaining(self) == Seq::new( + init.start.spec_steps_between_int(init.end) as nat, + |i: int| init.start.spec_forward_checked_int(i).unwrap(), + ) } - open spec fn ghost_peek_next(&self) -> Option { - Some(self.cur) + open spec fn decrease(&self) -> Option { + Some(self.start.spec_steps_between_int(self.end) as nat) } - open spec fn ghost_advance(&self, _exec_iter: &Range) -> RangeGhostIterator { - RangeGhostIterator { cur: self.cur.spec_forward_checked(1).unwrap(), ..*self } + open spec fn peek(&self, index: int) -> Option { + //Some(self.start.spec_forward_checked_int(index).unwrap()) + if 0 <= index <= self.start.spec_steps_between_int(self.end) { + Some(self.start.spec_forward_checked_int(index).unwrap()) + } else { + None + } } } -impl View for RangeGhostIterator { - type V = Seq; - - // generate seq![start, start + 1, start + 2, ..., cur - 1] - open spec fn view(&self) -> Seq { - Seq::new( - self.start.spec_steps_between_int(self.cur) as nat, - |i: int| self.start.spec_forward_checked_int(i).unwrap(), - ) - } -} +pub assume_specification[ as Iterator>::next ]( + range: &mut Range, +) -> (r: Option) + ensures + (*range, r) == spec_range_next(*old(range)), +; } // verus! macro_rules! step_specs { @@ -275,6 +261,7 @@ pub broadcast group group_range_axioms { axiom_spec_range_next_i64, axiom_spec_range_next_i128, axiom_spec_range_next_isize, + // axiom_spec_into_iter, } } // verus! diff --git a/source/vstd/std_specs/vec.rs b/source/vstd/std_specs/vec.rs index 3ac069624c..48e928669a 100644 --- a/source/vstd/std_specs/vec.rs +++ b/source/vstd/std_specs/vec.rs @@ -1,4 +1,5 @@ use super::super::prelude::*; +use crate::std_specs::iter::IteratorSpec; use verus_builtin::*; use alloc::collections::TryReserveError; @@ -356,107 +357,56 @@ impl, U, A1: Allocator, A2: Allocator> super::cm #[verifier::reject_recursive_types(A)] pub struct ExIntoIter(IntoIter); -impl View for IntoIter { - type V = (int, Seq); +// To allow reasoning about the "contents" of the Vec iterator, without using +// a prophecy, we need a function that gives us the underlying sequence of the original vec. +pub uninterp spec fn into_iter_elts(i: IntoIter) -> Seq; - uninterp spec fn view(self: &IntoIter) -> (int, Seq); -} - -pub assume_specification[ IntoIter::::next ]( - elements: &mut IntoIter, -) -> (r: Option) - ensures - ({ - let (old_index, old_seq) = old(elements)@; - match r { - None => { - &&& elements@ == old(elements)@ - &&& old_index >= old_seq.len() - }, - Some(element) => { - let (new_index, new_seq) = elements@; - &&& 0 <= old_index < old_seq.len() - &&& new_seq == old_seq - &&& new_index == old_index + 1 - &&& element == old_seq[old_index] - }, - } - }), -; - -pub struct IntoIterGhostIterator { - pub pos: int, - pub elements: Seq, - pub _marker: PhantomData, -} - -impl super::super::pervasive::ForLoopGhostIteratorNew for IntoIter { - type GhostIter = IntoIterGhostIterator; - - open spec fn ghost_iter(&self) -> IntoIterGhostIterator { - IntoIterGhostIterator { pos: self@.0, elements: self@.1, _marker: PhantomData } +impl crate::std_specs::iter::IteratorSpecImpl for IntoIter { + open spec fn obeys_prophetic_iter_laws(&self) -> bool { + true } -} -// This is used by `vec![x; n]` -pub assume_specification[ alloc::vec::from_elem ](elem: T, n: usize) -> (v: Vec) - ensures - v.len() == n, - forall |i| 0 <= i < n ==> cloned(elem, #[trigger] v@[i]); + uninterp spec fn remaining(&self) -> Seq; + uninterp spec fn completes(&self) -> bool; -impl super::super::pervasive::ForLoopGhostIterator for IntoIterGhostIterator< - T, - A, -> { - type ExecIter = IntoIter; - - type Item = T; - - type Decrease = int; - - open spec fn exec_invariant(&self, exec_iter: &IntoIter) -> bool { - &&& self.pos == exec_iter@.0 - &&& self.elements == exec_iter@.1 + #[verifier::prophetic] + open spec fn initial_value_inv(&self, init: &Self) -> bool { + &&& IteratorSpec::remaining(init) == IteratorSpec::remaining(self) + &&& into_iter_elts(*self) == IteratorSpec::remaining(self) } - open spec fn ghost_invariant(&self, init: Option<&Self>) -> bool { - init matches Some(init) ==> { - &&& init.pos == 0 - &&& init.elements == self.elements - &&& 0 <= self.pos <= self.elements.len() - } - } - - open spec fn ghost_ensures(&self) -> bool { - self.pos == self.elements.len() - } - - open spec fn ghost_decrease(&self) -> Option { - Some(self.elements.len() - self.pos) - } + uninterp spec fn decrease(&self) -> Option; - open spec fn ghost_peek_next(&self) -> Option { - if 0 <= self.pos < self.elements.len() { - Some(self.elements[self.pos]) + open spec fn peek(&self, index: int) -> Option { + if 0 <= index < into_iter_elts(*self).len() { + Some(into_iter_elts(*self)[index]) } else { None } } - - open spec fn ghost_advance(&self, _exec_iter: &IntoIter) -> IntoIterGhostIterator { - Self { pos: self.pos + 1, ..*self } - } } -impl View for IntoIterGhostIterator { - type V = Seq; +/* +impl crate::std_specs::iter::DoubleEndedIteratorSpecImpl for IntoIter { - open spec fn view(&self) -> Seq { - self.elements.take(self.pos) + open spec fn peek_back(&self, index: int) -> Option { + let len = into_iter_elts(*self).len(); + if 0 <= index < len { + Some(into_iter_elts(*self)[len - index - 1]) + } else { + None + } } } +*/ + +// This is used by `vec![x; n]` +pub assume_specification[ alloc::vec::from_elem ](elem: T, n: usize) -> (v: Vec) + ensures + v.len() == n, + forall |i| 0 <= i < n ==> cloned(elem, #[trigger] v@[i]); -// To allow reasoning about the ghost iterator when the executable +// To allow reasoning about the returned iterator when the executable // function `into_iter()` is invoked in a `for` loop header (e.g., in // `for x in it: v.into_iter() { ... }`), we need to specify the behavior of // the iterator in spec mode. To do that, we add @@ -469,7 +419,7 @@ pub uninterp spec fn spec_into_iter(v: Vec) -> (iter: (v: Vec) ensures - (#[trigger] spec_into_iter(v))@ == (0int, v@), + #[trigger] spec_into_iter(v).remaining() == v@, { admit(); } @@ -480,7 +430,9 @@ pub assume_specification[ Vec::::into_iter ](vec: Vec as core::iter::IntoIterator>::IntoIter) ensures - iter@ == (0int, vec@), + iter == spec_into_iter(vec), + IteratorSpec::decrease(&iter) is Some, + IteratorSpec::initial_value_inv(&iter, &iter), ; pub broadcast proof fn lemma_vec_obeys_eq_spec() diff --git a/source/vstd/std_specs/vecdeque.rs b/source/vstd/std_specs/vecdeque.rs index 57fc3954f1..47caf847be 100644 --- a/source/vstd/std_specs/vecdeque.rs +++ b/source/vstd/std_specs/vecdeque.rs @@ -1,6 +1,7 @@ /// This code adds specifications for the standard-library type /// `std::collections::VecDeque`. use super::super::prelude::*; +use crate::std_specs::iter::IteratorSpec; use alloc::collections::vec_deque::Iter; use alloc::collections::vec_deque::VecDeque; @@ -289,68 +290,37 @@ pub assume_specification<'a, T>[ Iter::<'a, T>::next ](elements: &mut Iter<'a, T }), ; -pub struct IterGhostIterator<'a, T> { - pub pos: int, - pub elements: Seq, - pub phantom: Option<&'a T>, -} - -impl<'a, T> super::super::pervasive::ForLoopGhostIteratorNew for Iter<'a, T> { - type GhostIter = IterGhostIterator<'a, T>; - - open spec fn ghost_iter(&self) -> IterGhostIterator<'a, T> { - IterGhostIterator { pos: self@.0, elements: self@.1, phantom: None } - } -} - -impl<'a, T: 'a> super::super::pervasive::ForLoopGhostIterator for IterGhostIterator<'a, T> { - type ExecIter = Iter<'a, T>; - type Item = T; - type Decrease = int; +// To allow reasoning about the "contents" of the VecDeque iterator, without using +// a prophecy, we need a function that gives us the underlying sequence of the original vec. +pub uninterp spec fn into_iter_elts<'a, T: 'a>(i: Iter<'a, T>) -> Seq<&'a T>; - open spec fn exec_invariant(&self, exec_iter: &Iter<'a, T>) -> bool { - &&& self.pos == exec_iter@.0 - &&& self.elements == exec_iter@.1 +impl <'a, T: 'a> crate::std_specs::iter::IteratorSpecImpl for Iter<'a, T> { + open spec fn obeys_prophetic_iter_laws(&self) -> bool { + true } - open spec fn ghost_invariant(&self, init: Option<&Self>) -> bool { - init matches Some(init) ==> { - &&& init.pos == 0 - &&& init.elements == self.elements - &&& 0 <= self.pos <= self.elements.len() - } - } + uninterp spec fn remaining(&self) -> Seq; + uninterp spec fn completes(&self) -> bool; - open spec fn ghost_ensures(&self) -> bool { - self.pos == self.elements.len() + #[verifier::prophetic] + open spec fn initial_value_inv(&self, init: &Self) -> bool { + &&& IteratorSpec::remaining(init) == IteratorSpec::remaining(self) + &&& into_iter_elts(*self) == IteratorSpec::remaining(self) } - open spec fn ghost_decrease(&self) -> Option { - Some(self.elements.len() - self.pos) - } + uninterp spec fn decrease(&self) -> Option; - open spec fn ghost_peek_next(&self) -> Option { - if 0 <= self.pos < self.elements.len() { - Some(self.elements[self.pos]) + open spec fn peek(&self, index: int) -> Option { + if 0 <= index < into_iter_elts(*self).len() { + Some(&into_iter_elts(*self)[index]) } else { None } } - - open spec fn ghost_advance(&self, _exec_iter: &Iter<'a, T>) -> IterGhostIterator<'a, T> { - Self { pos: self.pos + 1, ..*self } - } } -impl<'a, T> View for IterGhostIterator<'a, T> { - type V = Seq; - - open spec fn view(&self) -> Seq { - self.elements.take(self.pos) - } -} // To allow reasoning about the ghost iterator when the executable // function `iter()` is invoked in a `for` loop header (e.g., in @@ -362,7 +332,7 @@ pub uninterp spec fn spec_iter<'a, T, A: Allocator>(v: &'a VecDeque) -> (r pub broadcast proof fn axiom_spec_iter<'a, T, A: Allocator>(v: &'a VecDeque) ensures - (#[trigger] spec_iter(v))@ == (0int, v@), + #[trigger] spec_iter(v).remaining() == v@.map_values(|v| &v), { admit(); } @@ -370,9 +340,11 @@ pub broadcast proof fn axiom_spec_iter<'a, T, A: Allocator>(v: &'a VecDeque[ VecDeque::::iter ]( v: &'a VecDeque, -) -> (r: Iter<'a, T>) +) -> (iter: Iter<'a, T>) ensures - r@ == (0int, v@), + iter == spec_iter(v), + IteratorSpec::decrease(&iter) is Some, + IteratorSpec::initial_value_inv(&iter, &iter), ; pub broadcast group group_vec_dequeue_axioms {