Skip to content

Commit ccae446

Browse files
maximebuysemaximebuyse
authored
Merge pull request #13 from cryspen/issues
Issue references
2 parents fb2dc0f + 82cd363 commit ccae446

5 files changed

Lines changed: 614 additions & 611 deletions

File tree

‎core-models/src/core/iter.rs‎

Lines changed: 19 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -82,7 +82,7 @@ pub mod traits {
8282

8383
// opaque: while-let loop is not supported by hax FunctionalizeLoops
8484
#[hax_lib::opaque]
85-
#[cfg_attr(charon, aeneas::exclude)]
85+
#[cfg_attr(charon, aeneas::exclude)] // https://github.com/AeneasVerif/aeneas/issues/1098
8686
fn iter_fold<I: Iterator, B, F: Fn(B, I::Item) -> B>(mut iter: I, init: B, f: F) -> B {
8787
let mut accum = init;
8888
while let Option::Some(x) = iter.next() {
@@ -93,7 +93,7 @@ pub mod traits {
9393

9494
// opaque: while-let loop is not supported by hax FunctionalizeLoops
9595
#[hax_lib::opaque]
96-
#[cfg_attr(charon, aeneas::exclude)]
96+
#[cfg_attr(charon, aeneas::exclude)] // https://github.com/AeneasVerif/aeneas/issues/1098
9797
fn iter_all<I: Iterator, F: Fn(I::Item) -> bool>(mut iter: I, f: F) -> bool {
9898
while let Option::Some(x) = iter.next() {
9999
if !f(x) {
@@ -105,7 +105,7 @@ pub mod traits {
105105

106106
// opaque: while-let loop is not supported by hax FunctionalizeLoops
107107
#[hax_lib::opaque]
108-
#[cfg_attr(charon, aeneas::exclude)]
108+
#[cfg_attr(charon, aeneas::exclude)] // https://github.com/AeneasVerif/aeneas/issues/1098
109109
fn iter_any<I: Iterator, F: Fn(I::Item) -> bool>(mut iter: I, f: F) -> bool {
110110
while let Option::Some(x) = iter.next() {
111111
if f(x) {
@@ -117,6 +117,7 @@ pub mod traits {
117117

118118
// opaque: while-let loop is not supported by hax FunctionalizeLoops
119119
#[hax_lib::opaque]
120+
#[cfg_attr(charon, aeneas::exclude)] // https://github.com/AeneasVerif/aeneas/issues/1098
120121
fn iter_find<I: Iterator, P: Fn(&I::Item) -> bool>(
121122
iter: &mut I,
122123
predicate: P,
@@ -131,7 +132,7 @@ pub mod traits {
131132

132133
// opaque: while-let loop is not supported by hax FunctionalizeLoops
133134
#[hax_lib::opaque]
134-
#[cfg_attr(charon, aeneas::exclude)]
135+
#[cfg_attr(charon, aeneas::exclude)] // https://github.com/AeneasVerif/aeneas/issues/1098
135136
fn iter_find_map<I: Iterator, B, F: Fn(I::Item) -> Option<B>>(
136137
mut iter: I,
137138
f: F,
@@ -146,7 +147,7 @@ pub mod traits {
146147

147148
// opaque: while-let loop is not supported by hax FunctionalizeLoops
148149
#[hax_lib::opaque]
149-
#[cfg_attr(charon, aeneas::exclude)]
150+
#[cfg_attr(charon, aeneas::exclude)] // https://github.com/AeneasVerif/aeneas/issues/1098
150151
fn iter_position<I: Iterator, P: Fn(I::Item) -> bool>(
151152
mut iter: I,
152153
predicate: P,
@@ -163,7 +164,7 @@ pub mod traits {
163164

164165
// opaque: while-let loop is not supported by hax FunctionalizeLoops
165166
#[hax_lib::opaque]
166-
#[cfg_attr(charon, aeneas::exclude)]
167+
#[cfg_attr(charon, aeneas::exclude)] // https://github.com/AeneasVerif/aeneas/issues/1098
167168
fn iter_count<I: Iterator>(mut iter: I) -> usize {
168169
let mut n: usize = 0;
169170
while let Option::Some(_) = iter.next() {
@@ -174,7 +175,7 @@ pub mod traits {
174175

175176
// opaque: for-loop generates Rust_primitives.Hax.Folds, causing F* dependency cycle
176177
#[hax_lib::opaque]
177-
#[cfg_attr(charon, aeneas::exclude)]
178+
#[cfg_attr(charon, aeneas::exclude)] // https://github.com/AeneasVerif/aeneas/issues/1098
178179
fn iter_nth<I: Iterator>(mut iter: I, n: usize) -> Option<I::Item> {
179180
for _ in 0..n {
180181
if let Option::None = iter.next() {
@@ -186,7 +187,7 @@ pub mod traits {
186187

187188
// opaque: while-let loop is not supported by hax FunctionalizeLoops
188189
#[hax_lib::opaque]
189-
#[cfg_attr(charon, aeneas::exclude)]
190+
#[cfg_attr(charon, aeneas::exclude)] // https://github.com/AeneasVerif/aeneas/issues/1098
190191
fn iter_last<I: Iterator>(mut iter: I) -> Option<I::Item> {
191192
let mut last = Option::None;
192193
while let Option::Some(x) = iter.next() {
@@ -197,7 +198,7 @@ pub mod traits {
197198

198199
// opaque: while-let loop is not supported by hax FunctionalizeLoops
199200
#[hax_lib::opaque]
200-
#[cfg_attr(charon, aeneas::exclude)]
201+
#[cfg_attr(charon, aeneas::exclude)] // https://github.com/AeneasVerif/aeneas/issues/1098
201202
fn iter_for_each<I: Iterator, F: Fn(I::Item)>(mut iter: I, f: F) {
202203
while let Option::Some(x) = iter.next() {
203204
f(x);
@@ -206,7 +207,7 @@ pub mod traits {
206207

207208
// opaque: while-let loop is not supported by hax FunctionalizeLoops
208209
#[hax_lib::opaque]
209-
#[cfg_attr(charon, aeneas::exclude)]
210+
#[cfg_attr(charon, aeneas::exclude)] // https://github.com/AeneasVerif/aeneas/issues/1098
210211
fn iter_reduce<I: Iterator, F: Fn(I::Item, I::Item) -> I::Item>(
211212
mut iter: I,
212213
f: F,
@@ -223,7 +224,7 @@ pub mod traits {
223224

224225
// opaque: while-let loop is not supported by hax FunctionalizeLoops
225226
#[hax_lib::opaque]
226-
#[cfg_attr(charon, aeneas::exclude)]
227+
#[cfg_attr(charon, aeneas::exclude)] // https://github.com/AeneasVerif/aeneas/issues/1098
227228
fn iter_min<I: Iterator>(mut iter: I) -> Option<I::Item>
228229
where
229230
I::Item: crate::cmp::Ord,
@@ -242,7 +243,7 @@ pub mod traits {
242243

243244
// opaque: while-let loop is not supported by hax FunctionalizeLoops
244245
#[hax_lib::opaque]
245-
#[cfg_attr(charon, aeneas::exclude)]
246+
#[cfg_attr(charon, aeneas::exclude)] // https://github.com/AeneasVerif/aeneas/issues/1098
246247
fn iter_max<I: Iterator>(mut iter: I) -> Option<I::Item>
247248
where
248249
I::Item: crate::cmp::Ord,
@@ -410,7 +411,7 @@ pub mod adapters {
410411
iter: I,
411412
count: usize,
412413
}
413-
#[cfg_attr(charon, aeneas::exclude)]
414+
#[cfg_attr(charon, aeneas::exclude)] // https://github.com/AeneasVerif/aeneas/issues/1098
414415
impl<I> Enumerate<I> {
415416
pub fn new(iter: I) -> Enumerate<I> {
416417
Enumerate { iter, count: 0 }
@@ -442,7 +443,7 @@ pub mod adapters {
442443
iter: I,
443444
step: usize,
444445
}
445-
#[cfg_attr(charon, aeneas::exclude)]
446+
#[cfg_attr(charon, aeneas::exclude)] // https://github.com/AeneasVerif/aeneas/issues/1098
446447
impl<I> StepBy<I> {
447448
pub fn new(iter: I, step: usize) -> Self {
448449
StepBy { iter, step }
@@ -470,7 +471,7 @@ pub mod adapters {
470471
iter: I,
471472
f: F,
472473
}
473-
#[cfg_attr(charon, aeneas::exclude)]
474+
#[cfg_attr(charon, aeneas::exclude)] // https://github.com/AeneasVerif/aeneas/issues/1098
474475
impl<I, F> Map<I, F> {
475476
pub fn new(iter: I, f: F) -> Self {
476477
Self { iter, f }
@@ -497,7 +498,7 @@ pub mod adapters {
497498
iter: I,
498499
n: usize,
499500
}
500-
#[cfg_attr(charon, aeneas::exclude)]
501+
#[cfg_attr(charon, aeneas::exclude)] // https://github.com/AeneasVerif/aeneas/issues/1098
501502
impl<I> Take<I> {
502503
pub fn new(iter: I, n: usize) -> Take<I> {
503504
Take { iter, n }
@@ -633,7 +634,7 @@ pub mod adapters {
633634
iter: I,
634635
predicate: P,
635636
}
636-
#[cfg_attr(charon, aeneas::exclude)]
637+
#[cfg_attr(charon, aeneas::exclude)] // https://github.com/AeneasVerif/aeneas/issues/1098
637638
impl<I, P> Filter<I, P> {
638639
pub fn new(iter: I, predicate: P) -> Self {
639640
Self { iter, predicate }
@@ -697,7 +698,7 @@ pub mod adapters {
697698
iter: I,
698699
n: usize,
699700
}
700-
#[cfg_attr(charon, aeneas::exclude)]
701+
#[cfg_attr(charon, aeneas::exclude)] // https://github.com/AeneasVerif/aeneas/issues/1098
701702
impl<I> Skip<I> {
702703
pub fn new(iter: I, n: usize) -> Self {
703704
Self { iter, n }

‎core-models/src/core/option.rs‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -178,6 +178,7 @@ impl<T> Option<T> {
178178
/// See [`std::option::Option::filter`]
179179
// opaque: F* cannot prove that the Fn output projection equals bool in an if-condition
180180
#[hax_lib::opaque]
181+
#[cfg_attr(charon, aeneas::exclude)] // https://github.com/AeneasVerif/aeneas/issues/891
181182
pub fn filter<P: FnOnce(&T) -> bool>(self, predicate: P) -> Option<T> {
182183
match self {
183184
Some(x) => {
@@ -225,6 +226,7 @@ impl<T> Option<T> {
225226
}
226227

227228
/// See [`std::option::Option::inspect`]
229+
#[cfg_attr(charon, aeneas::exclude)] // https://github.com/AeneasVerif/aeneas/issues/891
228230
pub fn inspect<F: FnOnce(&T)>(self, f: F) -> Option<T> {
229231
if let Some(ref x) = self {
230232
f(x);

‎core-models/src/core/slice.rs‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -31,7 +31,7 @@ pub mod iter {
3131
/// See [`std::slice::Iter`]
3232
pub struct Iter<'a, T>(pub Seq<&'a T>);
3333

34-
#[cfg_attr(charon, aeneas::exclude)]
34+
#[cfg_attr(charon, aeneas::exclude)] // https://github.com/AeneasVerif/aeneas/issues/805
3535
impl<'a, T> crate::iter::traits::iterator::Iterator for Iter<'a, T> {
3636
type Item = &'a T;
3737
fn next(&mut self) -> Option<Self::Item> {
@@ -44,7 +44,7 @@ pub mod iter {
4444
}
4545
}
4646

47-
#[cfg_attr(charon, aeneas::exclude)]
47+
#[cfg_attr(charon, aeneas::exclude)] // https://github.com/AeneasVerif/aeneas/issues/805
4848
impl<'a, T> crate::iter::traits::iterator::Iterator for Chunks<'a, T> {
4949
type Item = &'a [T];
5050
fn next(&mut self) -> Option<Self::Item> {
@@ -62,7 +62,7 @@ pub mod iter {
6262
}
6363
}
6464

65-
#[cfg_attr(charon, aeneas::exclude)]
65+
#[cfg_attr(charon, aeneas::exclude)] // https://github.com/AeneasVerif/aeneas/issues/805
6666
impl<'a, T> crate::iter::traits::iterator::Iterator for ChunksExact<'a, T> {
6767
type Item = &'a [T];
6868
fn next(&mut self) -> Option<Self::Item> {
@@ -89,7 +89,7 @@ pub mod iter {
8989
// opaque: F* cannot prove slice bounds (1 <= length) in the else branch
9090
// This needs the invariant that size > 0
9191
#[hax_lib::opaque]
92-
#[cfg_attr(charon, aeneas::exclude)]
92+
#[cfg_attr(charon, aeneas::exclude)] // https://github.com/AeneasVerif/aeneas/issues/805
9393
impl<'a, T> crate::iter::traits::iterator::Iterator for Windows<'a, T> {
9494
type Item = &'a [T];
9595
fn next(&mut self) -> Option<Self::Item> {
@@ -254,7 +254,7 @@ impl<T> Slice<T> {
254254

255255
#[hax_lib::attributes]
256256
#[cfg_attr(hax_backend_lean, hax_lib::exclude)]
257-
#[cfg_attr(charon, aeneas::exclude)]
257+
#[cfg_attr(charon, aeneas::exclude)] // https://github.com/AeneasVerif/aeneas/issues/805
258258
impl<'a, T> crate::iter::traits::collect::IntoIterator for &'a [T] {
259259
type Item = &'a T;
260260
type IntoIter = iter::Iter<'a, T>;

0 commit comments

Comments
 (0)