Verus snapshot update

examples/verus-snapshot/source/vstd/source/vstd/arithmetic/div_mod.rs

@@ -11,41 +11,40 @@
 //! Copyright by the contributors to the Dafny Project *
 //! SPDX-License-Identifier: MIT
 //! *******************************************************************************/
-use crate::calc_macro::*;
+use super::super::calc_macro::*;
 #[allow(unused_imports)]
-use builtin::*;
-use builtin_macros::*;
+use super::super::prelude::*;
 
 verus! {
 
 #[allow(unused_imports)]
 #[cfg(verus_keep_ghost)]
-use crate::arithmetic::internals::div_internals::{
+use super::super::arithmetic::internals::div_internals::{
     div_recursive,
     lemma_div_induction_auto,
     div_auto,
     div_pos,
     lemma_div_auto,
 };
-use crate::arithmetic::internals::div_internals_nonlinear as DivINL;
+use super::super::arithmetic::internals::div_internals_nonlinear as DivINL;
 #[cfg(verus_keep_ghost)]
-use crate::arithmetic::internals::mod_internals::{
+use super::super::arithmetic::internals::mod_internals::{
     lemma_div_add_denominator,
     lemma_mod_auto,
     mod_recursive,
 };
-use crate::arithmetic::internals::mod_internals_nonlinear as ModINL;
+use super::super::arithmetic::internals::mod_internals_nonlinear as ModINL;
 #[cfg(verus_keep_ghost)]
-use crate::arithmetic::internals::mul_internals::{
+use super::internals::mul_internals::{
     group_mul_properties_internal,
     lemma_mul_induction,
     lemma_mul_induction_auto,
 };
 #[cfg(verus_keep_ghost)]
-use crate::arithmetic::internals::general_internals::{is_le};
+use super::super::arithmetic::internals::general_internals::{is_le};
 #[cfg(verus_keep_ghost)]
-use crate::math::{add as add1, sub as sub1, div as div1};
-use crate::arithmetic::mul::*;
+use super::super::math::{add as add1, sub as sub1, div as div1};
+use super::super::arithmetic::mul::*;
 
 /*****************************************************************************
 * Division
@@ -799,7 +798,7 @@ pub broadcast proof fn lemma_div_multiples_vanish_fancy(x: int, b: int, d: int)
                 lemma_mul_basics(d);
             }
         }
-        crate::arithmetic::internals::div_internals::lemma_div_basics(d);
+        super::internals::div_internals::lemma_div_basics(d);
     }
     assert forall|i: int| i <= 0 && #[trigger] f(i) implies #[trigger] f(sub1(i, 1)) by {
         assert(d * (i - 1) + b == d * i + b - d) by {
@@ -808,7 +807,7 @@ pub broadcast proof fn lemma_div_multiples_vanish_fancy(x: int, b: int, d: int)
                 lemma_mul_basics(d);
             }
         }
-        crate::arithmetic::internals::div_internals::lemma_div_basics(d);
+        super::internals::div_internals::lemma_div_basics(d);
     }
     broadcast use group_mul_properties_internal;
 

examples/verus-snapshot/source/vstd/source/vstd/arithmetic/internals/div_internals.rs

@@ -12,27 +12,26 @@
 //! *  SPDX-License-Identifier: MIT
 //! *******************************************************************************/
 #[allow(unused_imports)]
-use builtin::*;
-use builtin_macros::*;
+use super::super::super::prelude::*;
 
 verus! {
 
 #[cfg(verus_keep_ghost)]
-use crate::arithmetic::internals::general_internals::is_le;
+use super::super::super::arithmetic::internals::general_internals::is_le;
 #[cfg(verus_keep_ghost)]
-use crate::arithmetic::internals::mod_internals::{
+use super::super::super::arithmetic::internals::mod_internals::{
     lemma_mod_induction_forall,
     lemma_mod_induction_forall2,
     mod_auto,
     lemma_mod_auto,
     lemma_mod_basics,
 };
-use crate::arithmetic::internals::mod_internals_nonlinear;
+use super::super::super::arithmetic::internals::mod_internals_nonlinear;
 #[cfg(verus_keep_ghost)]
 #[cfg(verus_keep_ghost)]
-use crate::arithmetic::internals::div_internals_nonlinear;
+use super::super::super::arithmetic::internals::div_internals_nonlinear;
 #[cfg(verus_keep_ghost)]
-use crate::math::{add as add1, sub as sub1};
+use super::super::super::math::{add as add1, sub as sub1};
 
 /// This function recursively computes the quotient resulting from
 /// dividing two numbers `x` and `d`, in the case where `d > 0`

examples/verus-snapshot/source/vstd/source/vstd/arithmetic/internals/div_internals_nonlinear.rs

@@ -13,8 +13,7 @@
 //! *  SPDX-License-Identifier: MIT
 //! *******************************************************************************/
 #[allow(unused_imports)]
-use builtin::*;
-use builtin_macros::*;
+use super::super::super::prelude::*;
 
 verus! {
 

examples/verus-snapshot/source/vstd/source/vstd/arithmetic/internals/general_internals.rs

@@ -13,10 +13,8 @@
 //! *******************************************************************************/
 //! Declares helper lemmas and predicates for non-linear arithmetic
 #[cfg(verus_keep_ghost)]
-use crate::math::{add as add1, sub as sub1};
-#[allow(unused_imports)]
-use builtin::*;
-use builtin_macros::*;
+use super::super::super::math::{add as add1, sub as sub1};
+use super::super::super::prelude::*;
 
 verus! {
 

examples/verus-snapshot/source/vstd/source/vstd/arithmetic/internals/mod_internals.rs

@@ -12,27 +12,26 @@
 //! *  SPDX-License-Identifier: MIT
 //! *******************************************************************************/
 #[allow(unused_imports)]
-use builtin::*;
-use builtin_macros::*;
+use super::super::super::prelude::*;
 
 verus! {
 
-use crate::arithmetic::internals::general_internals::*;
-use crate::arithmetic::mul::*;
+use super::super::super::arithmetic::internals::general_internals::*;
+use super::super::super::arithmetic::mul::*;
 #[cfg(verus_keep_ghost)]
-use crate::arithmetic::internals::mul_internals::group_mul_properties_internal;
+use super::mul_internals::group_mul_properties_internal;
 #[cfg(verus_keep_ghost)]
-use crate::arithmetic::internals::mul_internals_nonlinear;
+use super::super::super::arithmetic::internals::mul_internals_nonlinear;
 #[cfg(verus_keep_ghost)]
-use crate::arithmetic::internals::mod_internals_nonlinear::{
+use super::super::super::arithmetic::internals::mod_internals_nonlinear::{
     lemma_fundamental_div_mod,
     lemma_mod_range,
     lemma_small_mod,
 };
 #[cfg(verus_keep_ghost)]
-use crate::arithmetic::internals::div_internals_nonlinear;
+use super::super::super::arithmetic::internals::div_internals_nonlinear;
 #[cfg(verus_keep_ghost)]
-use crate::math::{add as add1, sub as sub1};
+use super::super::super::math::{add as add1, sub as sub1};
 
 /// This function performs the modulus operation recursively.
 #[verifier::opaque]

examples/verus-snapshot/source/vstd/source/vstd/arithmetic/internals/mod_internals_nonlinear.rs

@@ -13,8 +13,7 @@
 //! *  SPDX-License-Identifier: MIT
 //! *******************************************************************************/
 #[allow(unused_imports)]
-use builtin::*;
-use builtin_macros::*;
+use super::super::super::prelude::*;
 
 verus! {
 

examples/verus-snapshot/source/vstd/source/vstd/arithmetic/internals/mul_internals.rs

@@ -12,14 +12,15 @@
 //! *  SPDX-License-Identifier: MIT
 //! *******************************************************************************/
 #[allow(unused_imports)]
-use builtin::*;
-use builtin_macros::*;
+use super::super::super::prelude::*;
 
 #[cfg(verus_keep_ghost)]
-use crate::arithmetic::internals::general_internals::{is_le, lemma_induction_helper};
-use crate::arithmetic::internals::mul_internals_nonlinear as MulINL;
+use super::super::super::arithmetic::internals::general_internals::{
+    is_le, lemma_induction_helper,
+};
+use super::super::super::arithmetic::internals::mul_internals_nonlinear as MulINL;
 #[cfg(verus_keep_ghost)]
-use crate::math::{add as add1, sub as sub1};
+use super::super::super::math::{add as add1, sub as sub1};
 
 verus! {
 

examples/verus-snapshot/source/vstd/source/vstd/arithmetic/internals/mul_internals_nonlinear.rs

@@ -18,8 +18,7 @@
 */
 // may be try to use singular?
 #[allow(unused_imports)]
-use builtin::*;
-use builtin_macros::*;
+use super::super::super::prelude::*;
 
 verus! {
 

examples/verus-snapshot/source/vstd/source/vstd/arithmetic/logarithm.rs

@@ -12,25 +12,24 @@
 //! SPDX-License-Identifier: MIT
 //! *******************************************************************************/
 #[allow(unused_imports)]
-use builtin::*;
-use builtin_macros::*;
+use super::super::prelude::*;
 
 verus! {
 
-use crate::calc_macro::*;
+use super::super::calc_macro::*;
 #[cfg(verus_keep_ghost)]
-use crate::arithmetic::div_mod::{
+use super::div_mod::{
     lemma_div_pos_is_pos,
     lemma_div_decreases,
     lemma_div_is_ordered,
     lemma_div_multiples_vanish,
 };
 #[cfg(verus_keep_ghost)]
-use crate::math::{div as div1};
+use super::super::math::{div as div1};
 #[cfg(verus_keep_ghost)]
-use crate::arithmetic::mul::{lemma_mul_increases, lemma_mul_is_commutative};
+use super::super::arithmetic::mul::{lemma_mul_increases, lemma_mul_is_commutative};
 #[cfg(verus_keep_ghost)]
-use crate::arithmetic::power::{pow, lemma_pow_positive};
+use super::super::arithmetic::power::{pow, lemma_pow_positive};
 
 /// This function recursively defines the integer logarithm. It's only
 /// meaningful when the base of the logarithm `base` is greater than 1,

examples/verus-snapshot/source/vstd/source/vstd/arithmetic/mul.rs

@@ -12,13 +12,12 @@
 //! SPDX-License-Identifier: MIT
 //! *******************************************************************************/
 #[allow(unused_imports)]
-use builtin::*;
-use builtin_macros::*;
+use super::super::prelude::*;
 
 verus! {
 
-use crate::arithmetic::internals::mul_internals_nonlinear as MulINL;
-use crate::arithmetic::internals::mul_internals::*;
+use super::super::arithmetic::internals::mul_internals_nonlinear as MulINL;
+use super::super::arithmetic::internals::mul_internals::*;
 
 /// Proof that multiplication using `*` is equivalent to
 /// multiplication using a recursive definition. Specifically,

examples/verus-snapshot/source/vstd/source/vstd/arithmetic/power.rs

@@ -11,18 +11,17 @@
 //! *  Modifications and Extensions: Copyright by the contributors to the Dafny Project
 //! *  SPDX-License-Identifier: MIT
 //! *******************************************************************************/
-use crate::calc_macro::*;
+use super::super::calc_macro::*;
 #[allow(unused_imports)]
-use builtin::*;
-use builtin_macros::*;
+use super::super::prelude::*;
 
 verus! {
 
-use crate::arithmetic::div_mod::*;
+use super::super::arithmetic::div_mod::*;
 #[cfg(verus_keep_ghost)]
-use crate::arithmetic::internals::general_internals::{is_le};
+use super::super::arithmetic::internals::general_internals::{is_le};
 #[cfg(verus_keep_ghost)]
-use crate::arithmetic::mul::{
+use super::super::arithmetic::mul::{
     lemma_mul_inequality,
     lemma_mul_nonnegative,
     lemma_mul_strictly_increases,
@@ -34,12 +33,9 @@ use crate::arithmetic::mul::{
     lemma_mul_is_associative,
 };
 #[cfg(verus_keep_ghost)]
-use crate::arithmetic::internals::mul_internals::{
-    group_mul_properties_internal,
-    lemma_mul_induction_auto,
-};
+use super::internals::mul_internals::{group_mul_properties_internal, lemma_mul_induction_auto};
 #[cfg(verus_keep_ghost)]
-use crate::math::{sub as sub1};
+use super::super::math::{sub as sub1};
 
 /// This function performs exponentiation recursively, to compute `b`
 /// to the power of a natural number `e`

examples/verus-snapshot/source/vstd/source/vstd/arithmetic/power2.rs

@@ -12,25 +12,24 @@
 //! *  SPDX-License-Identifier: MIT
 //! *******************************************************************************/
 #[allow(unused_imports)]
-use builtin::*;
-use builtin_macros::*;
+use super::super::prelude::*;
 
 verus! {
 
 #[cfg(verus_keep_ghost)]
-use crate::arithmetic::power::{
+use super::power::{
     pow,
     lemma_pow_positive,
     group_pow_properties,
     lemma_pow_adds,
     lemma_pow_strictly_increases,
 };
 #[cfg(verus_keep_ghost)]
-use crate::arithmetic::internals::mul_internals::lemma_mul_induction_auto;
+use super::internals::mul_internals::lemma_mul_induction_auto;
 #[cfg(verus_keep_ghost)]
-use crate::arithmetic::internals::general_internals::is_le;
+use super::internals::general_internals::is_le;
 #[cfg(verus_keep_ghost)]
-use crate::calc_macro::*;
+use super::super::calc_macro::*;
 
 /// This function computes 2 to the power of the given natural number
 /// `e`. It's opaque so that the SMT solver doesn't waste time

examples/verus-snapshot/source/vstd/source/vstd/array.rs

@@ -1,9 +1,8 @@
 #![allow(unused_imports)]
-use crate::seq::*;
-use crate::slice::SliceAdditionalSpecFns;
-use crate::view::*;
-use builtin::*;
-use builtin_macros::*;
+use super::prelude::*;
+use super::seq::*;
+use super::slice::SliceAdditionalSpecFns;
+use super::view::*;
 
 verus! {
 
@@ -107,10 +106,35 @@ pub fn ex_array_as_slice<T, const N: usize>(ar: &[T; N]) -> (out: &[T])
     ar.as_slice()
 }
 
+pub spec fn spec_array_fill_for_copy_type<T: Copy, const N: usize>(t: T) -> (res: [T; N]);
+
+#[verifier::external_body]
+pub broadcast proof fn axiom_spec_array_fill_for_copy_type<T: Copy, const N: usize>(t: T)
+    ensures
+        #![trigger spec_array_fill_for_copy_type::<T, N>(t)]
+        forall|i: int|
+            0 <= i < N ==> spec_array_fill_for_copy_type::<T, N>(t).view()[i] == t,
+{
+}
+
+// The 'array fill' [t; N] where t is a Copy type
+// (Does not necessarily apply when t is a non-Copy const)
+#[doc(hidden)]
+#[verifier::external_body]
+#[verifier::when_used_as_spec(spec_array_fill_for_copy_type)]
+#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::array::array_fill_for_copy_types")]
+pub fn array_fill_for_copy_types<T: Copy, const N: usize>(t: T) -> (res: [T; N])
+    ensures
+        res == spec_array_fill_for_copy_type::<T, N>(t),
+{
+    [t;N]
+}
+
 #[cfg_attr(verus_keep_ghost, verifier::prune_unless_this_module_is_used)]
 pub broadcast group group_array_axioms {
     array_len_matches_n,
     axiom_spec_array_as_slice,
+    axiom_spec_array_fill_for_copy_type,
 }
 
 } // verus!

examples/verus-snapshot/source/vstd/source/vstd/atomic.rs

@@ -5,10 +5,9 @@ use core::sync::atomic::{
     AtomicU64, AtomicU8, AtomicUsize, Ordering,
 };
 
-use crate::modes::*;
-use crate::pervasive::*;
-use builtin::*;
-use builtin_macros::*;
+use super::modes::*;
+use super::pervasive::*;
+use super::prelude::*;
 
 macro_rules! make_unsigned_integer_atomic {
     ($at_ident:ident, $p_ident:ident, $p_data_ident:ident, $rust_ty: ty, $value_ty: ty, $wrap_add:ident, $wrap_sub:ident) => {