Skip to content

Issue references #13

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
maximebuyse merged 2 commits into from
Jun 3, 2026
Merged

Issue references #13

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
41f4ae9
fix: suppress error messages
abentkamp Jun 2, 2026
82cd363
doc: add issue references
abentkamp Jun 2, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
37 changes: 19 additions & 18 deletions core-models/src/core/iter.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -82,7 +82,7 @@ pub mod traits {

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

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

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

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

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

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

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

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

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

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

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

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

// opaque: while-let loop is not supported by hax FunctionalizeLoops
#[hax_lib::opaque]
#[cfg_attr(charon, aeneas::exclude)]
#[cfg_attr(charon, aeneas::exclude)] // https://github.com/AeneasVerif/aeneas/issues/1098
fn iter_max<I: Iterator>(mut iter: I) -> Option<I::Item>
where
I::Item: crate::cmp::Ord,
Expand Down Expand Up @@ -410,7 +411,7 @@ pub mod adapters {
iter: I,
count: usize,
}
#[cfg_attr(charon, aeneas::exclude)]
#[cfg_attr(charon, aeneas::exclude)] // https://github.com/AeneasVerif/aeneas/issues/1098
impl<I> Enumerate<I> {
pub fn new(iter: I) -> Enumerate<I> {
Enumerate { iter, count: 0 }
Expand Down Expand Up @@ -442,7 +443,7 @@ pub mod adapters {
iter: I,
step: usize,
}
#[cfg_attr(charon, aeneas::exclude)]
#[cfg_attr(charon, aeneas::exclude)] // https://github.com/AeneasVerif/aeneas/issues/1098
impl<I> StepBy<I> {
pub fn new(iter: I, step: usize) -> Self {
StepBy { iter, step }
Expand Down Expand Up @@ -470,7 +471,7 @@ pub mod adapters {
iter: I,
f: F,
}
#[cfg_attr(charon, aeneas::exclude)]
#[cfg_attr(charon, aeneas::exclude)] // https://github.com/AeneasVerif/aeneas/issues/1098
impl<I, F> Map<I, F> {
pub fn new(iter: I, f: F) -> Self {
Self { iter, f }
Expand All @@ -497,7 +498,7 @@ pub mod adapters {
iter: I,
n: usize,
}
#[cfg_attr(charon, aeneas::exclude)]
#[cfg_attr(charon, aeneas::exclude)] // https://github.com/AeneasVerif/aeneas/issues/1098
impl<I> Take<I> {
pub fn new(iter: I, n: usize) -> Take<I> {
Take { iter, n }
Expand Down Expand Up @@ -633,7 +634,7 @@ pub mod adapters {
iter: I,
predicate: P,
}
#[cfg_attr(charon, aeneas::exclude)]
#[cfg_attr(charon, aeneas::exclude)] // https://github.com/AeneasVerif/aeneas/issues/1098
impl<I, P> Filter<I, P> {
pub fn new(iter: I, predicate: P) -> Self {
Self { iter, predicate }
Expand Down Expand Up @@ -697,7 +698,7 @@ pub mod adapters {
iter: I,
n: usize,
}
#[cfg_attr(charon, aeneas::exclude)]
#[cfg_attr(charon, aeneas::exclude)] // https://github.com/AeneasVerif/aeneas/issues/1098
impl<I> Skip<I> {
pub fn new(iter: I, n: usize) -> Self {
Self { iter, n }
Expand Down
2 changes: 2 additions & 0 deletions core-models/src/core/option.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -178,6 +178,7 @@ impl<T> Option<T> {
/// See [`std::option::Option::filter`]
// opaque: F* cannot prove that the Fn output projection equals bool in an if-condition
#[hax_lib::opaque]
#[cfg_attr(charon, aeneas::exclude)] // https://github.com/AeneasVerif/aeneas/issues/891
pub fn filter<P: FnOnce(&T) -> bool>(self, predicate: P) -> Option<T> {
match self {
Some(x) => {
Expand Down Expand Up @@ -225,6 +226,7 @@ impl<T> Option<T> {
}

/// See [`std::option::Option::inspect`]
#[cfg_attr(charon, aeneas::exclude)] // https://github.com/AeneasVerif/aeneas/issues/891
pub fn inspect<F: FnOnce(&T)>(self, f: F) -> Option<T> {
if let Some(ref x) = self {
f(x);
Expand Down
10 changes: 5 additions & 5 deletions core-models/src/core/slice.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ pub mod iter {
/// See [`std::slice::Iter`]
pub struct Iter<'a, T>(pub Seq<&'a T>);

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

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

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

#[hax_lib::attributes]
#[cfg_attr(hax_backend_lean, hax_lib::exclude)]
#[cfg_attr(charon, aeneas::exclude)]
#[cfg_attr(charon, aeneas::exclude)] // https://github.com/AeneasVerif/aeneas/issues/805
impl<'a, T> crate::iter::traits::collect::IntoIterator for &'a [T] {
type Item = &'a T;
type IntoIter = iter::Iter<'a, T>;
Expand Down
Loading