vstd: add spec for Option::Clone

verus-lang · Nov 14, 2024 · 71aac59 · 71aac59
1 parent 4edba7d
commit 71aac59
Showing 1 changed file with 9 additions and 0 deletions.
diff --git a/source/vstd/std_specs/option.rs b/source/vstd/std_specs/option.rs
@@ -179,4 +179,13 @@ pub fn ex_map<T, U, F: FnOnce(T) -> U>(a: Option<T>, f: F) -> (ret: Option<U>)
     a.map(f)
 }
 
+#[verifier::external_fn_specification]
+pub fn ex_vec_clone<T: Clone>(opt: &Option<T>) -> (res: Option<T>)
+    ensures
+        opt.is_none() ==> res.is_none(),
+        opt.is_some() ==> res.is_some() && call_ensures(T::clone, (&opt.unwrap(),), res.unwrap()),
+{
+    opt.clone()
+}
+
 } // verus!