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}