tests: Re-activate some equivalence tests, and document better the cause for the ones that still cannot be activated.

Author: maximebuyse

tests/rust_lean_equiv_test/source/src/alloc/slice.rs

@@ -124,5 +124,8 @@ pub fn test_slice_to_vec_then_push() -> bool {
 
 // ----- closure-using methods (excluded) --------------------------------------
 
-// TODO(closure-extraction): `[T]::sort_by_key`, `[T]::sort_by`, and other
-// closure-taking slice methods are skipped until Fn/FnMut extraction lands.
+// TODO(slice-method-missing): `[T]::sort_by_key`, `[T]::sort_by`, and other
+// closure-taking slice methods are skipped — Aeneas handles closures
+// (see core::array::from_fn) but these methods are not in the model:
+// `alloc_models::slice::_::sort_by` is in `ALLOC_CHARON_EXCLUDES` and the
+// generic slice impl is not provided either.

tests/rust_lean_equiv_test/source/src/alloc/vec.rs

@@ -7,9 +7,6 @@
 //! - Indexing `v[i]` is in `ALLOC_CHARON_EXCLUDES` (see top-level `Makefile`),
 //!   so we verify per-element contents by sequential `pop()`s instead of
 //!   `v[i] == x`.
-//! - Several methods (`remove`, `clear`, `swap_remove`, `truncate`,
-//!   `resize`, `drain`) are `#[hax_lib::opaque]` in the model, so the Lean
-//!   side cannot observe their effect. Those are commented out.
 
 use rust_lean_test_macro::rust_lean_test;
 
@@ -254,21 +251,17 @@ pub fn test_vec_from_elem_zero_len() -> bool {
 // TODO(vec-index-excluded): Vec::from_iter is in ALLOC_CHARON_EXCLUDES.
 
 // ----- remove ----------------------------------------------------------------
-//
-// `Vec::remove` is `#[hax_lib::opaque]` in the model, but Aeneas still
-// extracts the underlying `seq_remove` body, so the Lean side mirrors
-// the real removal semantics.
 
 // TODO(vec-extraction-arity-mismatch: the Lean model marks `Vec.is_empty`/`as_slice`/`pop`/... with implicit `{A}`, but Aeneas extracts the call applying the allocator explicitly. Until that mismatch is fixed in the model, `Vec::*` tests fail.)
-/*
-#[rust_lean_test]
+
+/* #[rust_lean_test]
 pub fn test_vec_remove_only_element() -> bool {
     let mut v: Vec<u8> = Vec::new();
     v.push(7);
     let x = v.remove(0);
     x == 7 && v.is_empty()
-}
-*/
+} */
+
 
 // ----- swap_remove -----------------------------------------------------------
 
@@ -311,11 +304,14 @@ pub fn test_vec_swap_remove_back() -> bool {
 
 // ----- drain (iterator) ------------------------------------------------------
 
-// TODO(closure-extraction): Vec::drain returns an iterator we don't have
+// TODO(vec-iter-extraction): Vec::drain returns an iterator we don't have
 // a stable way to drive in extracted Lean yet.
 
 // ----- closure-using methods (excluded) --------------------------------------
 
-// TODO(closure-extraction): Vec::retain takes a closure; revisit when we
-// exercise Fn/FnMut.
-// TODO(closure-extraction): Vec::iter / Vec::into_iter use iterator traits.
+// TODO(closure-extraction + vec-extraction-arity-mismatch): Vec::retain takes
+// a closure. Aeneas can extract the closure (see core::array::from_fn) but
+// every Vec method first trips on the arity-mismatch issue above. Revisit
+// once Vec tests can compile in the first place.
+// TODO(vec-iter-extraction): Vec::iter / Vec::into_iter use iterator traits
+// whose Lean models we don't have yet.

tests/rust_lean_equiv_test/source/src/core/array.rs

@@ -61,27 +61,26 @@ pub fn test_eq_all_zeros() -> bool {
     a == b
 }
 
+#[rust_lean_test]
+pub fn test_from_fn_identity() -> bool {
+    let a: [u8; 4] = core::array::from_fn(|i| i as u8);
+    a == [0, 1, 2, 3]
+}
+
 // ----- map / from_fn / each_ref ---------------------------------------------
 
-// TODO(closure-extraction): `[T; N]::map` takes a closure; Aeneas emits an
-// opaque def for the closure and the `Fn` instance has to live in the type
-// universe. Revisit when closure extraction lands.
-// pub fn test_map_add_one() -> bool {
-//     let a: [u8; 4] = [1, 2, 3, 4];
-//     a.map(|x| x + 1) == [2, 3, 4, 5]
-// }
+// TODO: `[T; N]::map` is not defined yet
+/* pub fn test_map_add_one() -> bool {
+    let a: [u8; 4] = [1, 2, 3, 4];
+    a.map(|x| x + 1) == [2, 3, 4, 5]
+} */
 
-// TODO(closure-extraction): `core::array::from_fn` takes a closure.
-// pub fn test_from_fn_identity() -> bool {
-//     let a: [u8; 4] = core::array::from_fn(|i| i as u8);
-//     a == [0, 1, 2, 3]
-// }
 
 // TODO(each-ref-refs): `each_ref` returns `[&T; N]`; arrays of references
 // through Aeneas extraction are tricky. Revisit when references-in-arrays
 // modelling lands.
-// pub fn test_each_ref_first() -> bool {
-//     let a: [u8; 4] = [1, 2, 3, 4];
-//     let refs: [&u8; 4] = a.each_ref();
-//     *refs[0] == 1
-// }
+/* pub fn test_each_ref_first() -> bool {
+    let a: [u8; 4] = [1, 2, 3, 4];
+    let refs: [&u8; 4] = a.each_ref();
+    *refs[0] == 1
+} */

tests/rust_lean_equiv_test/source/src/core/iter.rs

@@ -37,18 +37,26 @@ pub fn test_range_count_offset() -> bool {
 
 // ----- skipped: closure-based iterator combinators --------------------------
 
-// TODO(closure-extraction): `Iterator::fold` takes a closure; Aeneas emits
-// an opaque def for the closure and the `Fn` instance has to live in the
-// type universe.
+// TODO(slice-iter-extraction): closure-based iterator combinators like
+// `fold` extract through Aeneas, but they bottom out in `slice::Iter::fold`
+// (and friends) which are missing from the extracted Lean. Tried
+// `[1u32,2,3,4].iter().fold(0u32, |acc, &x| acc + x)` — Aeneas emits the
+// closure fine, then Lean fails with
+//   `Unknown constant CoreModels.core.slice.Slice.iter`
+//   `Unknown constant CoreModels.core.slice.iter.Iter.Insts...fold`.
+// Revisit once slice iterators are modelled.
 // pub fn test_fold_sum() -> bool {
 //     let v = [1u32, 2, 3, 4];
 //     v.iter().fold(0u32, |acc, &x| acc + x) == 10
 // }
 
-// TODO(closure-extraction): `Iterator::map` / `Iterator::filter` /
+// TODO(slice-iter-extraction): `Iterator::map` / `Iterator::filter` /
 // `Iterator::any` / `Iterator::all` / `Iterator::find` /
 // `Iterator::find_map` / `Iterator::position` / `Iterator::for_each` /
-// `Iterator::reduce` all take closures.
+// `Iterator::reduce` all take closures. Aeneas handles the closure side
+// (see `core::array::test_from_fn_identity`), but on slice iterators they
+// bottom out in `slice::Iter::*` which is missing from the model — same
+// blocker as `fold` above.
 // pub fn test_map_collect_sum() -> bool {
 //     let v = [1u32, 2, 3];
 //     v.iter().map(|x| x + 1).fold(0u32, |a, b| a + b) == (2 + 3 + 4)
@@ -66,7 +74,10 @@ pub fn test_range_count_offset() -> bool {
 //     [10u32, 20, 30].iter().position(|x| *x == 20) == Some(1)
 // }
 
-// TODO(closure-extraction): `core::iter::from_fn` takes a closure.
+// `core::iter::from_fn` builds an iterator from a closure. Aeneas extracts
+// the closure, but the resulting `iter::FromFn` adapter is not modelled, so
+// any observation (`count`, `fold`, etc.) hits an unknown-constant error in
+// Lean. Revisit once `iter::FromFn` is added to the model.
 // pub fn test_from_fn() -> bool { ... }
 
 // TODO(slice-iter-extraction): `[T; N]::iter()` / `[T]::iter()` produce a

tests/rust_lean_equiv_test/source/src/core/option.rs

@@ -55,11 +55,37 @@ pub fn test_is_none_some_max() -> bool {
 
 // ----- is_some_and -----------------------------------------------------------
 
-// TODO(closure-extraction): is_some_and takes a closure; revisit when we exercise FnOnce.
+#[rust_lean_test]
+pub fn test_is_some_and_some_true() -> bool {
+    Some(4u8).is_some_and(|x| x > 0) == true
+}
+
+#[rust_lean_test]
+pub fn test_is_some_and_some_false() -> bool {
+    Some(0u8).is_some_and(|x| x > 0) == false
+}
+
+#[rust_lean_test]
+pub fn test_is_some_and_none() -> bool {
+    none_u8().is_some_and(|x| x > 0) == false
+}
 
 // ----- is_none_or ------------------------------------------------------------
 
-// TODO(closure-extraction): is_none_or takes a closure; revisit when we exercise FnOnce.
+#[rust_lean_test]
+pub fn test_is_none_or_some_true() -> bool {
+    Some(4u8).is_none_or(|x| x > 0) == true
+}
+
+#[rust_lean_test]
+pub fn test_is_none_or_some_false() -> bool {
+    Some(0u8).is_none_or(|x| x > 0) == false
+}
+
+#[rust_lean_test]
+pub fn test_is_none_or_none() -> bool {
+    none_u8().is_none_or(|x| x > 0) == true
+}
 
 // ----- as_ref ----------------------------------------------------------------
 
@@ -154,7 +180,20 @@ pub fn test_unwrap_or_none_default_max() -> bool {
 
 // ----- unwrap_or_else --------------------------------------------------------
 
-// TODO(closure-extraction): unwrap_or_else takes a closure; revisit when we exercise FnOnce.
+#[rust_lean_test]
+pub fn test_unwrap_or_else_some_zero() -> bool {
+    Some(0u8).unwrap_or_else(|| 42) == 0
+}
+
+#[rust_lean_test]
+pub fn test_unwrap_or_else_some_max() -> bool {
+    Some(u8::MAX).unwrap_or_else(|| 0) == u8::MAX
+}
+
+#[rust_lean_test]
+pub fn test_unwrap_or_else_none() -> bool {
+    none_u8().unwrap_or_else(|| 7) == 7
+}
 
 // ----- unwrap_or_default -----------------------------------------------------
 
@@ -184,19 +223,60 @@ pub fn test_unwrap_or_default_none() -> bool {
 
 // ----- map -------------------------------------------------------------------
 
-// TODO(closure-extraction): map takes a closure; revisit when we exercise FnOnce.
+// TODO(closure-extraction-map): `Option::map` returns `Option<U>`; observing the
+// result requires either `Option::PartialEq` (blocked by option-eq-extraction)
+// or destructuring through `match`, but the latter goes back through
+// `Option::PartialEq` once we compare the inner value. Revisit alongside
+// option-eq-extraction.
+
+#[rust_lean_test]
+pub fn test_map_some_via_unwrap_or() -> bool {
+    Some(3u8).map(|x| x + 1).unwrap_or(0) == 4
+}
+
+#[rust_lean_test]
+pub fn test_map_none_via_unwrap_or() -> bool {
+    none_u8().map(|x| x + 1).unwrap_or(99) == 99
+}
+
+#[rust_lean_test]
+pub fn test_map_some_is_some() -> bool {
+    Some(3u8).map(|x| x + 1).is_some()
+}
+
+#[rust_lean_test]
+pub fn test_map_none_is_none() -> bool {
+    none_u8().map(|x| x + 1).is_none()
+}
 
 // ----- map_or ----------------------------------------------------------------
 
-// TODO(closure-extraction): map_or takes a closure; revisit when we exercise FnOnce.
+#[rust_lean_test]
+pub fn test_map_or_some_zero() -> bool {
+    Some(3u8).map_or(0u8, |x| x + 1) == 4
+}
+
+#[rust_lean_test]
+pub fn test_map_or_some_max() -> bool {
+    Some(0u8).map_or(99u8, |x| x + 1) == 1
+}
+
+#[rust_lean_test]
+pub fn test_map_or_none() -> bool {
+    none_u8().map_or(99u8, |x| x + 1) == 99
+}
 
 // ----- map_or_else -----------------------------------------------------------
 
-// TODO(closure-extraction): map_or_else takes two closures; revisit when we exercise FnOnce.
+// TODO(closure-extraction-order): `Option::map_or_else` takes (default: D, f: F)
+// in source order but the model lists the trait instances in (F, D) order, so
+// Aeneas emits them swapped and the Lean elaboration fails for the `None`
+// branch. Revisit once the closure-instance ordering is fixed.
 
 // ----- map_or_default --------------------------------------------------------
 
-// TODO(closure-extraction): map_or_default takes a closure; revisit when we exercise FnOnce.
+// TODO(map_or_default-unstable): `Option::map_or_default` is gated behind
+// `result_option_map_or_default` on stable. Revisit once it stabilises.
 
 // ----- ok_or -----------------------------------------------------------------
 
@@ -220,9 +300,40 @@ pub fn test_ok_or_none_err_max() -> bool {
     matches!(none_u8().ok_or(u8::MAX), Err(v) if v == u8::MAX)
 }
 
+// ----- ok_or_else ------------------------------------------------------------
+
+#[rust_lean_test]
+pub fn test_ok_or_else_some() -> bool {
+    matches!(Some(7u8).ok_or_else(|| 99u8), Ok(7))
+}
+
+#[rust_lean_test]
+pub fn test_ok_or_else_none() -> bool {
+    matches!(none_u8().ok_or_else(|| 42u8), Err(42))
+}
+
+// ----- and_then --------------------------------------------------------------
+
+#[rust_lean_test]
+pub fn test_and_then_some_to_some() -> bool {
+    Some(3u8).and_then(|x| Some(x + 1)).unwrap_or(0) == 4
+}
+
+#[rust_lean_test]
+pub fn test_and_then_some_to_none() -> bool {
+    Some(3u8).and_then(|_| none_u8()).is_none()
+}
+
+#[rust_lean_test]
+pub fn test_and_then_none() -> bool {
+    none_u8().and_then(|x| Some(x + 1)).is_none()
+}
+
 // ----- filter ----------------------------------------------------------------
 
-// TODO(closure-extraction): filter takes a closure; revisit when we exercise FnOnce.
+// TODO(closure-by-ref-extraction): `Option::filter` takes `FnOnce(&T) -> bool`;
+// Aeneas trips on the borrow with "Region ids should not be visited directly".
+// Revisit once closures whose parameter is a reference extract.
 
 // ----- or --------------------------------------------------------------------
 
@@ -257,7 +368,25 @@ pub fn test_or_none_none() -> bool {
 
 // ----- or_else ---------------------------------------------------------------
 
-// TODO(closure-extraction): or_else takes a closure; revisit when we exercise FnOnce.
+#[rust_lean_test]
+pub fn test_or_else_some_kept() -> bool {
+    Some(0u8).or_else(|| Some(99u8)).unwrap_or(7) == 0
+}
+
+#[rust_lean_test]
+pub fn test_or_else_some_max_kept() -> bool {
+    Some(u8::MAX).or_else(|| none_u8()).unwrap_or(0) == u8::MAX
+}
+
+#[rust_lean_test]
+pub fn test_or_else_none_to_some() -> bool {
+    none_u8().or_else(|| Some(42u8)).unwrap_or(0) == 42
+}
+
+#[rust_lean_test]
+pub fn test_or_else_none_to_none() -> bool {
+    none_u8().or_else(|| none_u8()).is_none()
+}
 
 // ----- xor -------------------------------------------------------------------
 
@@ -337,7 +466,9 @@ pub fn test_zip_none_none() -> bool {
 
 // ----- inspect ---------------------------------------------------------------
 
-// TODO(closure-extraction): inspect takes a closure; revisit when we exercise FnOnce.
+// TODO(closure-by-ref-extraction): `Option::inspect` takes `FnOnce(&T)`;
+// Aeneas trips on the borrow with "Region ids should not be visited directly".
+// Revisit once closures whose parameter is a reference extract.
 
 // ----- flatten ---------------------------------------------------------------