Skip to content

Commit 6c72f41

Browse files
maximebuysemaximebuyse
committed
Generalize the use of the patch_lean workaround for aeneas issue 1098.
1 parent 657581a commit 6c72f41

3 files changed

Lines changed: 689 additions & 166 deletions

File tree

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

Lines changed: 2 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -82,7 +82,6 @@ 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)] // https://github.com/AeneasVerif/aeneas/issues/1098
8685
fn iter_fold<I: Iterator, B, F: Fn(B, I::Item) -> B>(mut iter: I, init: B, f: F) -> B {
8786
let mut accum = init;
8887
while let Option::Some(x) = iter.next() {
@@ -93,7 +92,6 @@ pub mod traits {
9392

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

106104
// opaque: while-let loop is not supported by hax FunctionalizeLoops
107105
#[hax_lib::opaque]
108-
#[cfg_attr(charon, aeneas::exclude)] // https://github.com/AeneasVerif/aeneas/issues/1098
109106
fn iter_any<I: Iterator, F: Fn(I::Item) -> bool>(mut iter: I, f: F) -> bool {
110107
while let Option::Some(x) = iter.next() {
111108
if f(x) {
@@ -115,9 +112,8 @@ pub mod traits {
115112
false
116113
}
117114

118-
// opaque: while-let loop is not supported by hax FunctionalizeLoops
119115
#[hax_lib::opaque]
120-
#[cfg_attr(charon, aeneas::exclude)] // https://github.com/AeneasVerif/aeneas/issues/1098
116+
#[cfg_attr(charon, aeneas::exclude)] // https://github.com/AeneasVerif/aeneas/issues/891
121117
fn iter_find<I: Iterator, P: Fn(&I::Item) -> bool>(
122118
iter: &mut I,
123119
predicate: P,
@@ -132,7 +128,6 @@ pub mod traits {
132128

133129
// opaque: while-let loop is not supported by hax FunctionalizeLoops
134130
#[hax_lib::opaque]
135-
#[cfg_attr(charon, aeneas::exclude)] // https://github.com/AeneasVerif/aeneas/issues/1098
136131
fn iter_find_map<I: Iterator, B, F: Fn(I::Item) -> Option<B>>(
137132
mut iter: I,
138133
f: F,
@@ -147,7 +142,6 @@ pub mod traits {
147142

148143
// opaque: while-let loop is not supported by hax FunctionalizeLoops
149144
#[hax_lib::opaque]
150-
#[cfg_attr(charon, aeneas::exclude)] // https://github.com/AeneasVerif/aeneas/issues/1098
151145
fn iter_position<I: Iterator, P: Fn(I::Item) -> bool>(
152146
mut iter: I,
153147
predicate: P,
@@ -164,7 +158,6 @@ pub mod traits {
164158

165159
// opaque: while-let loop is not supported by hax FunctionalizeLoops
166160
#[hax_lib::opaque]
167-
#[cfg_attr(charon, aeneas::exclude)] // https://github.com/AeneasVerif/aeneas/issues/1098
168161
fn iter_count<I: Iterator>(mut iter: I) -> usize {
169162
let mut n: usize = 0;
170163
while let Option::Some(_) = iter.next() {
@@ -173,9 +166,8 @@ pub mod traits {
173166
n
174167
}
175168

176-
// opaque: for-loop generates Rust_primitives.Hax.Folds, causing F* dependency cycle
177169
#[hax_lib::opaque]
178-
#[cfg_attr(charon, aeneas::exclude)] // https://github.com/AeneasVerif/aeneas/issues/1098
170+
#[cfg_attr(charon, aeneas::exclude)] // forward reference in lean (`core.Usize.Insts.CoreIterRangeStep`)
179171
fn iter_nth<I: Iterator>(mut iter: I, n: usize) -> Option<I::Item> {
180172
for _ in 0..n {
181173
if let Option::None = iter.next() {
@@ -187,7 +179,6 @@ pub mod traits {
187179

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

199190
// opaque: while-let loop is not supported by hax FunctionalizeLoops
200191
#[hax_lib::opaque]
201-
#[cfg_attr(charon, aeneas::exclude)] // https://github.com/AeneasVerif/aeneas/issues/1098
202192
fn iter_for_each<I: Iterator, F: Fn(I::Item)>(mut iter: I, f: F) {
203193
while let Option::Some(x) = iter.next() {
204194
f(x);
@@ -207,7 +197,6 @@ pub mod traits {
207197

208198
// opaque: while-let loop is not supported by hax FunctionalizeLoops
209199
#[hax_lib::opaque]
210-
#[cfg_attr(charon, aeneas::exclude)] // https://github.com/AeneasVerif/aeneas/issues/1098
211200
fn iter_reduce<I: Iterator, F: Fn(I::Item, I::Item) -> I::Item>(
212201
mut iter: I,
213202
f: F,
@@ -224,7 +213,6 @@ pub mod traits {
224213

225214
// opaque: while-let loop is not supported by hax FunctionalizeLoops
226215
#[hax_lib::opaque]
227-
#[cfg_attr(charon, aeneas::exclude)] // https://github.com/AeneasVerif/aeneas/issues/1098
228216
fn iter_min<I: Iterator>(mut iter: I) -> Option<I::Item>
229217
where
230218
I::Item: crate::cmp::Ord,
@@ -243,7 +231,6 @@ pub mod traits {
243231

244232
// opaque: while-let loop is not supported by hax FunctionalizeLoops
245233
#[hax_lib::opaque]
246-
#[cfg_attr(charon, aeneas::exclude)] // https://github.com/AeneasVerif/aeneas/issues/1098
247234
fn iter_max<I: Iterator>(mut iter: I) -> Option<I::Item>
248235
where
249236
I::Item: crate::cmp::Ord,
@@ -411,7 +398,6 @@ pub mod adapters {
411398
iter: I,
412399
count: usize,
413400
}
414-
#[cfg_attr(charon, aeneas::exclude)] // https://github.com/AeneasVerif/aeneas/issues/1098
415401
impl<I> Enumerate<I> {
416402
pub fn new(iter: I) -> Enumerate<I> {
417403
Enumerate { iter, count: 0 }
@@ -497,7 +483,6 @@ pub mod adapters {
497483
iter: I,
498484
n: usize,
499485
}
500-
#[cfg_attr(charon, aeneas::exclude)] // https://github.com/AeneasVerif/aeneas/issues/1098
501486
impl<I> Take<I> {
502487
pub fn new(iter: I, n: usize) -> Take<I> {
503488
Take { iter, n }
@@ -633,7 +618,6 @@ pub mod adapters {
633618
iter: I,
634619
predicate: P,
635620
}
636-
#[cfg_attr(charon, aeneas::exclude)] // https://github.com/AeneasVerif/aeneas/issues/1098
637621
impl<I, P> Filter<I, P> {
638622
pub fn new(iter: I, predicate: P) -> Self {
639623
Self { iter, predicate }
@@ -697,7 +681,6 @@ pub mod adapters {
697681
iter: I,
698682
n: usize,
699683
}
700-
#[cfg_attr(charon, aeneas::exclude)] // https://github.com/AeneasVerif/aeneas/issues/1098
701684
impl<I> Skip<I> {
702685
pub fn new(iter: I, n: usize) -> Self {
703686
Self { iter, n }

0 commit comments

Comments
 (0)