fix failing proofs, use new broadcast mechanism for array_as_slice

source/vstd/array.rs

@@ -68,11 +68,11 @@ pub open spec fn array_index<T, const N: usize>(ar: &[T; N], i: int) -> T {
 
 pub open spec fn spec_array_as_slice<T, const N: usize>(ar: &[T; N]) -> (out: &[T]);
 
-#[verifier(external_body)]
 pub broadcast proof fn axiom_spec_array_as_slice<T, const N: usize>(ar: &[T; N])
     ensures
         (#[trigger] spec_array_as_slice(ar))@ == ar@,
 {
+    admit();
 }
 
 // Referenced by Verus' internal encoding for array -> slice coercion
@@ -98,6 +98,7 @@ pub fn ex_array_as_slice<T, const N: usize>(ar: &[T; N]) -> (out: &[T])
 #[verifier::prune_unless_this_module_is_used]
 pub broadcast group array_axioms {
     array_len_matches_n,
+    axiom_spec_array_as_slice,
 }
 
 } // verus!

source/vstd/seq_lib.rs

@@ -1009,9 +1009,16 @@ impl<A> Seq<Seq<A>> {
 
         if self.len() != 0 {
             self.drop_last().lemma_flatten_and_flatten_alt_are_equivalent();
+            // let s = self.drop_last().flatten();
+            // let s2 = self.drop_last().flatten_alt();
+            // assert(s == s2);
             seq![self.last()].lemma_flatten_one_element();
+            assert(seq![self.last()].flatten() == self.last());
             lemma_flatten_concat(self.drop_last(), seq![self.last()]);
-            assert(self =~= self.drop_last().push(self.last()));
+            assert((self.drop_last() + seq![self.last()]).flatten() == self.drop_last().flatten()
+                + self.last());
+            assert(self.drop_last() + seq![self.last()] =~= self);
+            assert(self.flatten_alt() == self.drop_last().flatten_alt() + self.last());
         }
     }
 }

source/vstd/std_specs/bits.rs

@@ -707,6 +707,7 @@ pub broadcast proof fn axiom_u64_leading_zeros(i: u64)
         forall|j: u64| 64 - u64_leading_zeros(i) <= j < 64 ==> #[trigger] (i >> j) & 1u64 == 0u64,
     decreases i,
 {
+    reveal(u64_leading_zeros);
     assert(i / 2 == (i >> 1u64)) by (bit_vector);
     assert(((i >> 1) >> sub(63u64, 0)) & 1u64 == 0u64) by (bit_vector);
     let x = u64_leading_zeros(i / 2) as u64;