un-admit TODOS, broadcast group vstd_axioms -> vstd_default

verus-lang · Apr 20, 2024 · cee2883 · cee2883
1 parent 72ed4d7
commit cee2883
Show file tree

Hide file tree

Showing 3 changed files with 19 additions and 21 deletions.
diff --git a/source/vstd/seq_lib.rs b/source/vstd/seq_lib.rs
@@ -1007,7 +1007,6 @@ impl<A> Seq<Seq<A>> {
     {
         broadcast use Seq::add_empty_right, Seq::push_distributes_over_add;
 
-        admit();  // TODO
         if self.len() != 0 {
             self.drop_last().lemma_flatten_and_flatten_alt_are_equivalent();
             seq![self.last()].lemma_flatten_one_element();

diff --git a/source/vstd/std_specs/bits.rs b/source/vstd/std_specs/bits.rs
@@ -707,25 +707,24 @@ 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,
 {
-    admit();  // TODO
-    // 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;
-    // assert(i >> 0 == i) by (bit_vector);
-    // assert(1u64 & 1u64 == 1u64) by (bit_vector);
-    // assert(0 < x < 64 ==> ((i >> 1) >> sub(63u64, x)) == (i >> sub(63u64, sub(x, 1))))
-    //     by (bit_vector);
-    // assert(0 < x <= 64 ==> (i >> 1) >> sub(64, x) == 0 ==> i >> sub(64, sub(x, 1)) == 0)
-    //     by (bit_vector);
-    // if i != 0 {
-    //     axiom_u64_leading_zeros(i / 2);
-    // }
-    // assert forall|j: u64| 64 - u64_leading_zeros(i) <= j < 64 implies #[trigger] (i >> j) & 1u64
-    //     == 0u64 by {
-    //     let y = u64_leading_zeros(i) as u64;
-    //     assert(y <= 64 ==> i >> sub(64, y) == 0 ==> sub(64, y) <= j < 64 ==> (i >> j) & 1u64
-    //         == 0u64) by (bit_vector);
-    // }
+    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;
+    assert(i >> 0 == i) by (bit_vector);
+    assert(1u64 & 1u64 == 1u64) by (bit_vector);
+    assert(0 < x < 64 ==> ((i >> 1) >> sub(63u64, x)) == (i >> sub(63u64, sub(x, 1))))
+        by (bit_vector);
+    assert(0 < x <= 64 ==> (i >> 1) >> sub(64, x) == 0 ==> i >> sub(64, sub(x, 1)) == 0)
+        by (bit_vector);
+    if i != 0 {
+        axiom_u64_leading_zeros(i / 2);
+    }
+    assert forall|j: u64| 64 - u64_leading_zeros(i) <= j < 64 implies #[trigger] (i >> j) & 1u64
+        == 0u64 by {
+        let y = u64_leading_zeros(i) as u64;
+        assert(y <= 64 ==> i >> sub(64, y) == 0 ==> sub(64, y) <= j < 64 ==> (i >> j) & 1u64
+            == 0u64) by (bit_vector);
+    }
 }
 
 pub broadcast proof fn axiom_u64_leading_ones(i: u64)

diff --git a/source/vstd/vstd.rs b/source/vstd/vstd.rs
@@ -60,7 +60,7 @@ use prelude::*;
 verus! {
 
 #[verifier::broadcast_use_by_default_when_this_crate_is_imported]
-pub broadcast group vstd_axioms {
+pub broadcast group vstd_default {
     seq::seq_axioms,
     seq_lib::seq_lib_default,
     map::map_axioms,