vstd/std_specs/
array.rs

1use super::super::prelude::*;
2
3verus! {
4
5// array == array
6pub assume_specification<T: PartialEq<U>, U, const N: usize>[ <[T; N] as PartialEq<[U; N]>>::eq ](
7    left: &[T; N],
8    right: &[U; N],
9) -> bool
10;
11
12impl<T, U, const N: usize> super::cmp::PartialEqSpecImpl<[U; N]> for [T; N] where
13    T: PartialEq<U> + super::cmp::PartialEqSpec<U>,
14 {
15    open spec fn obeys_eq_spec() -> bool {
16        <T as super::cmp::PartialEqSpec<U>>::obeys_eq_spec()
17    }
18
19    open spec fn eq_spec(&self, other: &[U; N]) -> bool {
20        forall|i: int|
21            #![auto]
22            0 <= i < N ==> <T as super::cmp::PartialEqSpec<U>>::eq_spec(&self@[i], &other@[i])
23    }
24}
25
26// slice ref == array
27pub assume_specification<'a, T: PartialEq<U>, U, const N: usize>[ <&'a [T] as PartialEq<
28    [U; N],
29>>::eq ](left: &&'a [T], right: &[U; N]) -> bool
30;
31
32impl<'a, T, U, const N: usize> super::cmp::PartialEqSpecImpl<[U; N]> for &'a [T] where
33    T: PartialEq<U> + super::cmp::PartialEqSpec<U>,
34 {
35    open spec fn obeys_eq_spec() -> bool {
36        <T as super::cmp::PartialEqSpec<U>>::obeys_eq_spec()
37    }
38
39    open spec fn eq_spec(&self, other: &[U; N]) -> bool {
40        &&& (*self)@.len() == other@.len()
41        &&& forall|i: int|
42            #![auto]
43            0 <= i < (*self)@.len() ==> <T as super::cmp::PartialEqSpec<U>>::eq_spec(
44                &(*self)@[i],
45                &other@[i],
46            )
47    }
48}
49
50// array == slice ref
51pub assume_specification<'a, T: PartialEq<U>, U, const N: usize>[ <[T; N] as PartialEq<&[U]>>::eq ](
52    left: &[T; N],
53    right: &&[U],
54) -> bool
55;
56
57impl<'a, T, U, const N: usize> super::cmp::PartialEqSpecImpl<&'a [U]> for [T; N] where
58    T: PartialEq<U> + super::cmp::PartialEqSpec<U>,
59 {
60    open spec fn obeys_eq_spec() -> bool {
61        <T as super::cmp::PartialEqSpec<U>>::obeys_eq_spec()
62    }
63
64    open spec fn eq_spec(&self, other: &&'a [U]) -> bool {
65        &&& self@.len() == (*other)@.len()
66        &&& forall|i: int|
67            #![auto]
68            0 <= i < self@.len() ==> <T as super::cmp::PartialEqSpec<U>>::eq_spec(
69                &self@[i],
70                &(*other)@[i],
71            )
72    }
73}
74
75// slice == array
76pub assume_specification<T: PartialEq<U>, U, const N: usize>[ <[T] as PartialEq<[U; N]>>::eq ](
77    left: &[T],
78    right: &[U; N],
79) -> bool
80;
81
82impl<T, U, const N: usize> super::cmp::PartialEqSpecImpl<[U; N]> for [T] where
83    T: PartialEq<U> + super::cmp::PartialEqSpec<U>,
84 {
85    open spec fn obeys_eq_spec() -> bool {
86        <T as super::cmp::PartialEqSpec<U>>::obeys_eq_spec()
87    }
88
89    open spec fn eq_spec(&self, other: &[U; N]) -> bool {
90        &&& self@.len() == other@.len()
91        &&& forall|i: int|
92            #![auto]
93            0 <= i < self@.len() ==> <T as super::cmp::PartialEqSpec<U>>::eq_spec(
94                &self@[i],
95                &other@[i],
96            )
97    }
98}
99
100// array == slice
101pub assume_specification<T: PartialEq<U>, U, const N: usize>[ <[T; N] as PartialEq<[U]>>::eq ](
102    left: &[T; N],
103    right: &[U],
104) -> bool
105;
106
107impl<T, U, const N: usize> super::cmp::PartialEqSpecImpl<[U]> for [T; N] where
108    T: PartialEq<U> + super::cmp::PartialEqSpec<U>,
109 {
110    open spec fn obeys_eq_spec() -> bool {
111        <T as super::cmp::PartialEqSpec<U>>::obeys_eq_spec()
112    }
113
114    open spec fn eq_spec(&self, other: &[U]) -> bool {
115        &&& self@.len() == other@.len()
116        &&& forall|i: int|
117            #![auto]
118            0 <= i < self@.len() ==> <T as super::cmp::PartialEqSpec<U>>::eq_spec(
119                &self@[i],
120                &other@[i],
121            )
122    }
123}
124
125} // verus!
vstd/std_specs/array.rs

vstd/std_specs/
array.rs
