vstd/pervasive.rs
1#![allow(internal_features)]
2
3#[allow(unused_imports)]
4use super::prelude::*;
5
6#[cfg(not(feature = "std"))]
7macro_rules! println {
8 ($($arg:tt)*) => {};
9}
10verus! {
11
12// TODO: remove this
13pub proof fn assume(b: bool)
14 ensures
15 b,
16{
17 admit();
18}
19
20// TODO: remove this
21#[verifier(custom_req_err("assertion failure"))]
22pub proof fn assert(b: bool)
23 requires
24 b,
25 ensures
26 b,
27{
28}
29
30pub proof fn affirm(b: bool)
31 requires
32 b,
33{
34}
35
36// An artificial trigger that can be used in case no expression naturally serves as a trigger
37pub open spec fn trigger<A>(a: A) -> bool {
38 true
39}
40
41// TODO: when default trait methods are supported, most of these should be given defaults
42pub trait ForLoopGhostIterator {
43 type ExecIter;
44
45 type Item;
46
47 type Decrease;
48
49 // Connect the ExecIter to the GhostIter
50 // Always enabled
51 // Always true before and after each loop iteration
52 spec fn exec_invariant(&self, exec_iter: &Self::ExecIter) -> bool;
53
54 // Additional optional invariants about the GhostIter
55 // May be disabled with #[verifier::no_auto_loop_invariant]
56 // If enabled, always true before and after each loop iteration
57 // (When the analysis can infer a spec initial value, the analysis places the value in init)
58 spec fn ghost_invariant(&self, init: Option<&Self>) -> bool;
59
60 // True upon loop exit
61 spec fn ghost_ensures(&self) -> bool;
62
63 // Value used by default for decreases clause when no explicit decreases clause is provided
64 // (the user can override this with an explicit decreases clause).
65 // (If there's no appropriate decrease, this can return None,
66 // and the user will have to provide an explicit decreases clause.)
67 spec fn ghost_decrease(&self) -> Option<Self::Decrease>;
68
69 // If there will be Some next value, and we can make a useful guess as to what the next value
70 // will be, return Some of it.
71 // Otherwise, return None.
72 // TODO: in the long term, we could have VIR insert an assertion (or warning)
73 // that ghost_peek_next returns non-null if it is used in the invariants.
74 // (this will take a little bit of engineering since the syntax macro blindly inserts
75 // let bindings using ghost_peek_next, even if they aren't needed, and we only learn
76 // what is actually needed later in VIR.)
77 spec fn ghost_peek_next(&self) -> Option<Self::Item>;
78
79 // At the end of the for loop, advance to the next position.
80 // Future TODO: this may be better as a proof function
81 spec fn ghost_advance(&self, exec_iter: &Self::ExecIter) -> Self where Self: Sized;
82}
83
84pub trait ForLoopGhostIteratorNew {
85 type GhostIter;
86
87 // Create a new ghost iterator from an exec iterator
88 // Future TODO: this may be better as a proof function
89 spec fn ghost_iter(&self) -> Self::GhostIter;
90}
91
92#[cfg(verus_keep_ghost)]
93pub trait FnWithRequiresEnsures<Args, Output>: Sized {
94 spec fn requires(self, args: Args) -> bool;
95
96 spec fn ensures(self, args: Args, output: Output) -> bool;
97}
98
99#[cfg(verus_keep_ghost)]
100impl<Args: core::marker::Tuple, Output, F: FnOnce<Args, Output = Output>> FnWithRequiresEnsures<
101 Args,
102 Output,
103> for F {
104 #[verifier::inline]
105 open spec fn requires(self, args: Args) -> bool {
106 call_requires(self, args)
107 }
108
109 #[verifier::inline]
110 open spec fn ensures(self, args: Args, output: Output) -> bool {
111 call_ensures(self, args, output)
112 }
113}
114
115// Non-statically-determined function calls are translated *internally* (at the VIR level)
116// to this function call. This should not actually be called directly by the user.
117// That is, Verus treats `f(x, y)` as `exec_nonstatic_call(f, (x, y))`.
118// (Note that this function wouldn't even satisfy the borrow-checker if you tried to
119// use it with a `&F` or `&mut F`, but this doesn't matter since it's only used at VIR.)
120#[cfg(verus_keep_ghost)]
121#[verifier(custom_req_err("Call to non-static function fails to satisfy `callee.requires(args)`"))]
122#[doc(hidden)]
123#[verifier::external_body]
124#[rustc_diagnostic_item = "verus::vstd::vstd::exec_nonstatic_call"]
125fn exec_nonstatic_call<Args: core::marker::Tuple, Output, F>(f: F, args: Args) -> (output:
126 Output) where F: FnOnce<Args, Output = Output>
127 requires
128 call_requires(f, args),
129 ensures
130 call_ensures(f, args, output),
131{
132 unimplemented!();
133}
134
135#[cfg(verus_keep_ghost)]
136#[verifier(custom_req_err("Call to non-static function fails to satisfy `callee.requires(args)`"))]
137#[doc(hidden)]
138#[verifier::external_body]
139#[rustc_diagnostic_item = "verus::vstd::vstd::proof_nonstatic_call"]
140proof fn proof_nonstatic_call<Args: core::marker::Tuple, Output, F>(
141 tracked f: F,
142 tracked args: Args,
143) -> (tracked output: Output) where F: FnOnce<Args, Output = Output>
144 requires
145 call_requires(f, args),
146 ensures
147 call_ensures(f, args, output),
148{
149 unimplemented!();
150}
151
152/// A tool to check one's reasoning while writing complex spec functions.
153/// Not intended to be used as a mechanism for instantiating quantifiers, `spec_affirm` should
154/// be removed from spec functions once they are complete.
155///
156/// ## Example
157///
158/// ```rust
159/// #[spec(checked)] fn some_predicate(a: nat) -> bool {
160/// recommends(a < 100);
161/// if (a >= 50) {
162/// let _ = spec_affirm(50 <= a && a < 100);
163/// a >= 75
164/// } else {
165/// let _ = spec_affirm(a < 50);
166/// // let _ = spec_affirm(a < 40); would raise a recommends note here
167/// a < 25
168/// }
169/// }
170/// ```
171pub closed spec fn spec_affirm(b: bool) -> bool
172 recommends
173 b,
174{
175 b
176}
177
178/// In spec, all types are inhabited
179#[verifier::external_body] /* vattr */
180#[allow(dead_code)]
181pub uninterp spec fn arbitrary<A>() -> A;
182
183pub axiom fn proof_from_false<A>() -> (tracked a: A)
184 requires
185 false,
186;
187
188#[verifier::external_body] /* vattr */
189#[allow(dead_code)]
190pub fn unreached<A>() -> A
191 requires
192 false,
193{
194 panic!("unreached_external")
195}
196
197#[allow(unused_variables)] // when built with cfg(not(feature = "std"))
198#[verifier::external_body] /* vattr */
199pub fn print_u64(i: u64) {
200 println!("{}", i);
201}
202
203#[verifier::external_body]
204pub fn runtime_assert(b: bool)
205 requires
206 b,
207{
208 runtime_assert_internal(b);
209}
210
211} // verus!
212#[inline(always)]
213#[cfg_attr(verus_keep_ghost, verifier::external)]
214fn runtime_assert_internal(b: bool) {
215 assert!(b);
216}
217
218/// Allows you to prove a boolean predicate by assuming its negation and proving
219/// a contradiction.
220///
221/// `assert_by_contradiction!(b, { /* proof */ });`
222/// Equivalent to writing `if !b { /* proof */; assert(false); }`
223/// but is more concise and documents intent.
224///
225/// ```rust
226/// assert_by_contradiction!(b, {
227/// // assume !b here
228/// // prove `false`
229/// });
230/// ```
231
232#[macro_export]
233macro_rules! assert_by_contradiction {
234 ($($a:tt)*) => {
235 verus_proof_macro_exprs!($crate::assert_by_contradiction_internal!($($a)*))
236 }
237}
238
239#[doc(hidden)]
240#[macro_export]
241macro_rules! assert_by_contradiction_internal {
242 ($predicate:expr, $bblock:block) => {
243 ::verus_builtin::assert_by($predicate, {
244 if !$predicate {
245 $bblock::verus_builtin::assert_(false);
246 }
247 });
248 };
249}
250
251/// Macro to help set up boilerplate for specifying invariants when using
252/// invariant-based datatypes.
253///
254/// This currently supports the `AtomicInvariant` and `LocalInvariant`
255/// types, as well as all the `atomic_ghost` types (e.g., `AtomicU64`, `AtomicBool`, and so on).
256/// It is important to first understand how these types work.
257/// In particular, `LocalInvariant` (for example) takes three type parameters,
258/// `K`, `V`, and `Pred: InvariantPredicate`.
259/// The `InvariantPredicate` trait lets the user specify an invariant at the static type
260/// level, while `K` allows the user to configure the invariant upon construction.
261/// `AtomicInvariant` uses the same system, and the `atomic_ghost` types are similar
262/// but use a different trait (`AtomicInvariantPredicate`).
263///
264/// However, setting all this up in a typical application tends to involve a bit
265/// of boilerplate. That's where this macro comes in.
266///
267/// # Usage
268///
269/// The `struct_with_invariants!` macro is used at the item level, and it should contains
270/// a single struct declaration followed by a single declaration of a `spec` function
271/// returning `bool`. However, this spec function should not contain a boolean predicate
272/// as usual, but instead a series of _invariant declarations_.
273/// Each invariant declaration applies to a single field of the struct.
274///
275/// ```rust
276/// struct_with_invariants!{
277/// (pub)? struct $struct_name (<...>)? (where ...)? {
278/// ( (pub)? $field_name: $type, )*
279/// }
280///
281/// (pub)? (open|closed)? spec fn(&self (, ...)?) $fn_name {
282/// ( InvariantDecl | BoolPredicateDecl )*
283/// }
284/// }
285/// ```
286///
287/// A field of the struct, if it uses a supported type, may leave the type _incomplete_ by
288/// omitting some of its type parameters.
289/// The following are valid incomplete types:
290///
291/// * `LocalInvariant<_, V, _>`
292/// * `AtomicInvariant<_, V, _>`
293/// * `AtomicBool<_, G, _>`
294/// * `AtomicU64<_, G, _>`
295/// * ... and so on for the other `atomic_ghost` types.
296///
297/// There must be exactly one invariant declaration for each incomplete type used in the
298/// struct declaration. The macro uses invariant declarations to fill in the type parameters.
299///
300/// The user can also provide boolean predicate declarations, which are copied verbatim
301/// into the `$fn_name` definition. This is a convenience, since it is common to want
302/// to add extra conditions, and it is fairly straightforward.
303/// The complex part of the macro expansion in the invariant declarations.
304///
305/// ```rust
306/// BoolPredicateDecl := predicate { $bool_expr }
307///
308/// InvariantDecl :=
309/// invariant on $field_name
310/// ( with ($dependencies) )?
311/// ( forall | ($ident: $type, )* | )?
312/// ( where ($where_expr) )?
313/// ( specifically ($specifically_expr) )?
314/// is ($params) {
315/// $bool_expr
316/// }
317/// ```
318///
319/// In the `InvariantDecl`, the user always needs to provide the following data:
320///
321/// * The `$field_name` is the field that this invariant applies to
322/// (which must have an incomplete type as described above)
323/// * The `$params` are the values constrained by the invariant.
324/// * For a `LocalInvariant<V>` or `AtomicInvariant<V>`, this should be a single
325/// parameter of type `V`.
326/// * For an `atomic_ghost` type, this should consist of two parameters,
327/// first the primitive type stored by the atomic, and secondly one of the ghost type, `G`.
328/// (For example, the type `AtomicBool<_, G, _>` should have two parameters
329/// here, `b: bool, g: G`.)
330/// * Finally, the `$bool_expr` is the invariant predicate, which may reference any of
331/// the fields declared in `$dependencies`, or any of the params.
332///
333/// The other input clauses handle additional complexities that often comes up.
334/// For example, it is often necessary for the invariant to refer to the values of other fields
335/// in the struct.
336///
337/// * The `with` input gives the list of field names (other fields
338/// from the struct definition) that may be referenced from
339/// the body of this invariant.
340/// The graph of dependencies across all fields must be acyclic.
341///
342/// Finally, when the field is a _container_ type, e.g., `vec: Vec<AtomicU64<_, G, _>>` or
343/// `opt: Option<AtomicU64<_, G, _>>`, there are some additional complexities.
344/// We might need the invariant to be conditional (e.g., for an optional, the invariant would only
345/// exist if `opt is Some`).
346/// We might need to quantify over a variable (e.g., in a vector, we want to specify an invariant
347/// for each element, element `i` where `0 <= i < vec.len()`).
348/// Finally, we need to indicate the value actually getting the invariant (e.g., `self.vec[i]`).
349///
350/// * The `forall` lets you specify additional bound variables. Everything after the `forall`---the
351/// `where`, the `specifically`, and finally the `$bool_expr$`---can all reference these bound variables.
352/// * The `where` lets you specify an additional hypothesis that the invariant is dependent on.
353/// * The `specifically` lets you indicate the value getting the invariant.
354///
355/// This all roughly means, "forall instantiations of the quantified variables, if the condition `$where_expr` holds,
356/// then the value given by `$specifically_expr` has the invariant given by `$bool_expr`.
357/// See the detailed information on the macro-expansion below for more details.
358///
359/// Given all the information from the `InvariantDecl`, the macro fills in the `_` placeholders as follows:
360///
361/// * The macro fills in the `K` type as the types of the fields marked as dependencies and
362/// the quantified variables in the forall (packing all these types into a tuple if necessary).
363/// * The macro fills in the `Pred` type by creating a new type and implementing the appropriate
364/// trait with the user-provided predicate.
365///
366/// # Example (TODO)
367///
368/// # Example using a container type (TODO)
369///
370/// # Macro Expansion (TODO)
371pub use verus_builtin_macros::struct_with_invariants;
372
373verus! {
374
375use super::view::View;
376
377#[cfg(feature = "alloc")]
378#[verifier::external]
379pub trait VecAdditionalExecFns<T> {
380 fn set(&mut self, i: usize, value: T);
381
382 fn set_and_swap(&mut self, i: usize, value: &mut T);
383}
384
385#[cfg(feature = "alloc")]
386impl<T> VecAdditionalExecFns<T> for alloc::vec::Vec<T> {
387 /// Replacement for `self[i] = value;` (which Verus does not support for technical reasons)
388 #[verifier::external_body]
389 fn set(&mut self, i: usize, value: T)
390 requires
391 i < old(self).len(),
392 ensures
393 self@ == old(self)@.update(i as int, value),
394 {
395 self[i] = value;
396 }
397
398 /// Replacement for `swap(&mut self[i], &mut value)` (which Verus does not support for technical reasons)
399 #[verifier::external_body]
400 fn set_and_swap(&mut self, i: usize, value: &mut T)
401 requires
402 i < old(self).len(),
403 ensures
404 self@ == old(self)@.update(i as int, *old(value)),
405 *value == old(self)@.index(i as int),
406 {
407 core::mem::swap(&mut self[i], value);
408 }
409}
410
411/// Predicate indicating `b` could be the result of calling `a.clone()`
412///
413/// It is usually recommended to use [`cloned`] instead,
414/// which takes the reflexive closure.
415pub open spec fn strictly_cloned<T: Clone>(a: T, b: T) -> bool {
416 call_ensures(T::clone, (&a,), b)
417}
418
419/// Predicate indicating `b` is "a clone" of `a`; i.e., `b` could be the result of
420/// calling `a.clone()` or is equal to `a`.
421///
422/// By always considering a value to be a clone of itself, regardless of the definition
423/// of `T::clone`, this definition is useful in places where 'clone' calls might be
424/// optimized to copies. This is particularly common in the Rust stdlib.
425pub open spec fn cloned<T: Clone>(a: T, b: T) -> bool {
426 strictly_cloned(a, b) || a == b
427}
428
429} // verus!
430
431verus! {
432/// The default behavior of the vstd library enforces writing panic-free code.
433/// While developers may still use panic, verification should ensure that any
434/// panic is provably unreachable.
435/// cfg!(feature = "allow_panic") explicily allows code to panic.
436pub open spec fn allow_panic() -> bool {
437 cfg!(feature = "allow_panic")
438}
439
440#[doc(hidden)]
441#[verifier(external_body)]
442pub fn __call_panic(out: &[&str]) -> !
443requires
444 allow_panic()
445{
446 core::panic!("__call_panic {:?}", out);
447}
448
449// rt::Argument is a private type and we cannot add specification directly
450#[cfg(feature = "alloc")]
451#[doc(hidden)]
452#[verifier(external_body)]
453pub fn __new_argument<T: core::fmt::Debug>(v: &T) -> alloc::string::String {
454 alloc::format!("{:?}", v)
455}
456
457} // verus!
458
459/// Replace panic macro with vpanic when needed.
460/// panic!{} may call panic_fmt with private rt::Argument, which could not
461/// be supported in verus.
462#[macro_export]
463macro_rules! vpanic {
464 // Case: Format string with arguments
465 ($fmt:expr $(,$val:expr)*) => {
466 vstd::pervasive::__call_panic(
467 &[vstd::pervasive::__new_argument(&$fmt).as_str(),
468 $(
469 vstd::pervasive::__new_argument(&$val).as_str(),
470 )*]
471 );
472 };
473 () => {
474 vstd::pervasive::__call_panic(&[]);
475 };
476}