Merge pull request #2 from verus-lang/fun_ext_2

Replace fun_ext_2 (was deprecated, is now removed) with =~=
verus-lang · Jan 23, 2025 · 40286ee · 40286ee
2 parents 4d6efdf + 3efc59d
commit 40286ee
Show file tree

Hide file tree

Showing 3 changed files with 18 additions and 21 deletions.
diff --git a/ironsht/src/marshal_ironsht_specific_v.rs b/ironsht/src/marshal_ironsht_specific_v.rs
@@ -7,7 +7,6 @@
 use builtin::*;
 use builtin_macros::*;
 use vstd::bytes::*;
-use vstd::function::*;
 use vstd::map::*;
 use vstd::modes::*;
 use vstd::multiset::*;
@@ -283,7 +282,7 @@ verus! {
                 assert(vec[i].ghost_serialize().len() < max_len);
             }
             lemma_seq_fold_left_sum_le(vec@, 0, max_len, f);
-            fun_ext_2(ag, af);
+            assert(ag =~= af);
         }
 
         assert(
@@ -299,9 +298,9 @@ verus! {
             let sa = |acc: Seq<u8>, x: CKeyKV| acc + s(x);
             lemma_seq_fold_left_append_len_int(vec@, emp, s);
             assert(vec@.fold_left(emp, sa).len() as int == vec@.fold_left(0, asl));
-            fun_ext_2(sa, sg);
+            assert(sa =~= sg);
             assert(vec@.fold_left(emp, sg).len() as int == vec@.fold_left(0, asl));
-            fun_ext_2(agl, asl);
+            assert(agl =~= asl);
             assert(vec@.fold_left(emp, sg).len() == vec@.fold_left(0, agl));
         }
 

diff --git a/ironsht/src/marshal_v.rs b/ironsht/src/marshal_v.rs
@@ -5,7 +5,6 @@
 use builtin::*;
 use builtin_macros::*;
 use vstd::bytes::*;
-use vstd::function::*;
 use vstd::map::*;
 use vstd::modes::*;
 use vstd::multiset::*;
@@ -649,7 +648,7 @@ impl<T: Marshalable> Marshalable for Vec<T> {
             }
           };
           let sl = |x: T| x.ghost_serialize().len() as int;
-          fun_ext_2::<int, T, int>(|acc: int, x: T| acc + x.ghost_serialize().len() as int, |acc: int, x: T| acc + sl(x));
+          assert((|acc: int, x: T| acc + x.ghost_serialize().len() as int) =~= (|acc: int, x: T| acc + sl(x)));
           let s = self@.subrange(0 as int, i as int);
           seq_lib_v::lemma_seq_fold_left_sum_right::<T>(s, 0, sl);
           assert(s.subrange(0, s.len() - 1) =~= self@.subrange(0 as int, i - 1 as int));
@@ -666,11 +665,11 @@ impl<T: Marshalable> Marshalable for Vec<T> {
               let f = |x: T| x.ghost_serialize();
               let sl = |x: T| x.ghost_serialize().len() as int;
               let s = self@.subrange(0 as int, i as int + 1);
-              fun_ext_2::<int, T, int>(|acc: int, x: T| acc + x.ghost_serialize().len() as int, |acc: int, x: T| acc + sl(x));
+              assert((|acc: int, x: T| acc + x.ghost_serialize().len() as int) =~= (|acc: int, x: T| acc + sl(x)));
               seq_lib_v::lemma_seq_fold_left_sum_right::<T>(s, 0, sl);
               assert(s.subrange(0, s.len() - 1) =~= self@.subrange(0 as int, i as int));
               seq_lib_v::lemma_seq_fold_left_append_len_int_le(self@, i as int + 1, 0, f);
-              fun_ext_2(|acc: int, x: T| acc + x.ghost_serialize().len() as int, |acc: int, x: T| acc + f(x).len());
+              assert((|acc: int, x: T| acc + x.ghost_serialize().len() as int) =~= (|acc: int, x: T| acc + f(x).len()));
             };
           } else {
             assert(!self@[i as int].is_marshalable());
@@ -708,11 +707,11 @@ impl<T: Marshalable> Marshalable for Vec<T> {
     {
       proof {
         let f = |x: T| x.ghost_serialize();
-        fun_ext_2::<int, T, int>(|acc: int, x: T| acc + f(x).len(), |acc: int, x: T| acc + x.ghost_serialize().len());
+        assert((|acc: int, x: T| acc + f(x).len()) =~= (|acc: int, x: T| acc + x.ghost_serialize().len()));
         seq_lib_v::lemma_seq_fold_left_append_len_int_le::<T, u8>(self@, i + 1 as int, 0, f);
         let sl = |x: T| x.ghost_serialize().len() as int;
         let accl = |acc: int, x: T| acc + x.ghost_serialize().len() as int;
-        fun_ext_2::<int, T, int>(accl, |acc: int, x: T| acc + sl(x));
+        assert(accl =~= (|acc: int, x: T| acc + sl(x)));
         let s = self@.subrange(0 as int, i + 1 as int);
         seq_lib_v::lemma_seq_fold_left_sum_right::<T>(s, 0, sl);
         assert(s.subrange(0, s.len() - 1 as int) =~= self@.subrange(0 as int, i as int));
@@ -723,7 +722,7 @@ impl<T: Marshalable> Marshalable for Vec<T> {
       i = i + 1;
       proof {
         let sl = |x: T| x.ghost_serialize().len() as int;
-        fun_ext_2::<int, T, int>(|acc: int, x: T| acc + x.ghost_serialize().len() as int, |acc: int, x: T| acc + sl(x));
+        assert((|acc: int, x: T| acc + x.ghost_serialize().len() as int) =~= (|acc: int, x: T| acc + sl(x)));
         let s = self@.subrange(0 as int, i as int);
         seq_lib_v::lemma_seq_fold_left_sum_right::<T>(s, 0, sl);
         assert(s.subrange(0, s.len() - 1) =~= self@.subrange(0 as int, i - 1 as int));
@@ -733,8 +732,8 @@ impl<T: Marshalable> Marshalable for Vec<T> {
     proof {
       let f = |x: T| x.ghost_serialize();
       seq_lib_v::lemma_seq_fold_left_append_len_int::<T, u8>(self@, Seq::<u8>::empty(), f);
-      fun_ext_2::<Seq<u8>, T, Seq<u8>>(|acc: Seq<u8>, x: T| acc + f(x), |acc: Seq<u8>, x: T| acc + x.ghost_serialize());
-      fun_ext_2::<int, T, int>(|acc: int, x: T| acc + f(x).len(), |acc: int, x: T| acc + x.ghost_serialize().len());
+      assert((|acc: Seq<u8>, x: T| acc + f(x)) =~= (|acc: Seq<u8>, x: T| acc + x.ghost_serialize()));
+      assert((|acc: int, x: T| acc + f(x).len()) =~= (|acc: int, x: T| acc + x.ghost_serialize().len()));
       assert(self@.subrange(0 as int, i as int) =~= self@);
     }
 
@@ -781,7 +780,7 @@ impl<T: Marshalable> Marshalable for Vec<T> {
           let f = |x: T| x.ghost_serialize();
           let t = s.subrange(0, i as int);
 
-          fun_ext_2(accf, |acc: Seq<u8>, x: T| acc + f(x));
+          assert(accf =~= (|acc: Seq<u8>, x: T| acc + f(x)));
           assert(t.subrange(0, t.len() - 1) =~= s.subrange(0, i - 1));
           seq_lib_v::lemma_seq_fold_left_append_right(t, emp, f);
           assert(
@@ -859,7 +858,7 @@ impl<T: Marshalable> Marshalable for Vec<T> {
         //        seq_lib_v::seq_fold_left(old_res@, emp@, accf@) + f(x));
         seq_lib_v::lemma_seq_fold_left_append_right(res@, emp@, f);
         assert(accf@ == (|acc: Seq<u8>, x: T| acc + f(x))) by {
-          fun_ext_2(accf@, |acc: Seq<u8>, x: T| acc + f(x));
+          assert(accf@ =~= (|acc: Seq<u8>, x: T| acc + f(x)));
         }
         assert(old_res@ =~= res@.subrange(0, res@.len() - 1));
         // assert(data@.subrange(mid as int, end as int) == seq_lib_v::seq_fold_left(res@, emp@, accf@));
@@ -870,7 +869,7 @@ impl<T: Marshalable> Marshalable for Vec<T> {
         let l = |x: T| x.ghost_serialize().len() as int;
         let suml = |acc: int, x: T| acc + l(x);
         seq_lib_v::lemma_seq_fold_left_sum_right(res@, 0, l);
-        fun_ext_2(|acc: int, x: T| acc + x.ghost_serialize().len(), suml);
+        assert((|acc: int, x: T| acc + x.ghost_serialize().len()) =~= suml);
         assert(old_res@ =~= res@.subrange(0, res@.len() - 1));
       }
 
@@ -904,7 +903,7 @@ impl<T: Marshalable> Marshalable for Vec<T> {
       let accg = |acc: Seq<u8>, x: T| acc + g(x);
       let accgs = |acc: Seq<u8>, x: T| acc + x.ghost_serialize();
       let gs = |s: Seq<T>, start: int, end: int| s.subrange(start, end).fold_left(emp, accg);
-      fun_ext_2(accg, accgs);
+      assert(accg =~= accgs);
       assert(self.ghost_serialize() =~= ((self@.len() as usize).ghost_serialize() + gs(self@, 0, idx)) + g(self@[idx]) + gs(self@, idx + 1, self.len() as int)) by {
         assert(gs(self@, 0, self.len() as int) == gs(self@, 0, idx) + gs(self@, idx, self.len() as int)) by {
           let s1 = self@.subrange(0, idx);

diff --git a/ironsht/src/verus_extra/seq_lib_v.rs b/ironsht/src/verus_extra/seq_lib_v.rs
@@ -1,6 +1,5 @@
 use builtin::*;
 use builtin_macros::*;
-use vstd::function::*;
 use vstd::seq::*;
 use vstd::seq_lib::*;
 
@@ -78,7 +77,7 @@ pub proof fn lemma_seq_fold_left_sum_right<A>(s: Seq<A>, low: int, f: spec_fn(A)
     s.fold_left(low, |b: int, a: A| b + f(a))
 {
   let g = |x: int, y: int| x + y;
-  fun_ext_2::<int, A, int>(|b: int, a: A| b + f(a), |b: int, a: A| g(b, f(a)));
+  assert((|b: int, a: A| b + f(a)) =~= (|b: int, a: A| g(b, f(a))));
   lemma_seq_fold_left_merge_right_assoc::<A, int>(s, low, f, g);
 }
 
@@ -93,7 +92,7 @@ pub proof fn lemma_seq_fold_left_append_right<A, B>(s: Seq<A>, prefix: Seq<B>, f
   assert forall |x, y, z| #[trigger g(x,y)] g(g(x, y), z) == g(x, g(y, z)) by {
     assert_seqs_equal!(g(g(x, y), z) == g(x, g(y, z)));
   };
-  fun_ext_2::<Seq<B>, A, Seq<B>>(|b: Seq<B>, a: A| b + f(a), |b: Seq<B>, a: A| g(b, f(a)));
+  assert((|b: Seq<B>, a: A| b + f(a)) =~= (|b: Seq<B>, a: A| g(b, f(a))));
   lemma_seq_fold_left_merge_right_assoc::<A, Seq<B>>(s, prefix, f, g);
 }
 
@@ -144,7 +143,7 @@ pub proof fn lemma_seq_fold_left_append_len_int_le<A, B>(s: Seq<A>, i: int, low:
     lemma_seq_fold_left_append_len_int_le::<A, B>(s.subrange(1, s.len() as int), i - 1, low + f(s[0]).len() as int, f);
   } else if i == s.len() - 1 {
     let fl = |x| f(x).len() as int;
-    fun_ext_2::<int, A, int>(accfl, |acc: int, x: A| acc + fl(x));
+    assert(accfl =~= (|acc: int, x: A| acc + fl(x)));
     lemma_seq_fold_left_sum_right::<A>(s, low, fl);
   } else {
     lemma_seq_fold_left_append_len_int_le::<A, B>(s.subrange(0, s.len() - 1), i, low, f);