WIP: add many models extending the Aeneas standard library coverage#947
Draft
oliver-butterley wants to merge 28 commits intoAeneasVerif:mainfrom
Draft
WIP: add many models extending the Aeneas standard library coverage#947oliver-butterley wants to merge 28 commits intoAeneasVerif:mainfrom
oliver-butterley wants to merge 28 commits intoAeneasVerif:mainfrom
Conversation
Tracks the Lean models we're adding for Rust core/alloc stdlib items that currently appear as axioms in downstream FunsExternal.lean files. Each row has: Rust item, Lean name, docs link, pinned source link, status, dependencies, Lean file, test file, and proof file. A reviewer can chase these links to audit each model's authenticity to the Rust function. Initial state: 1 of 58 entries complete (Iterator::enumerate from earlier PR); 2 deferred (fmt functions pending an impure-effect story); the rest pending.
Adds Lean models for: - Option::as_ref (identity since refs are erased) - Option::ok_or (Some -> Ok, None -> Err) - Clone for Option<T>::clone - Default for Option<T>::default (returns None) - PartialEq for Option<T>::eq (lifts PartialEq<T>) Each model has an English docstring with links to doc.rust-lang.org and the pinned rust-lang/rust source at 1.85.0. Tests in tests/src/option_methods.rs translate the Rust docs examples verbatim where possible; adapted ones are noted with explanation (main adaptation: replacing assert_eq! on Result with pattern-match, pending Result::PartialEq support). Foundation: PartialEq<Option<T>> is the first of the three foundation dependencies for the Iterator::enumerate verbatim docs example.
Adds Lean models for: - Result::is_ok - Result::map (with FnOnce closure) - Result::map_err (with FnOnce closure) - Result::unwrap_or - Try<Result<Infallible,E>> for Result<T,E>::branch (plus FromResidual with From conversion) for the '?' operator The Try/FromResidual impl lives in Core/Convert.lean (not Core/Result.lean) because it references core::convert::Infallible, which Convert.lean declares. Tests in tests/src/result_methods.rs: is_ok/unwrap_or adapted from docs (u32 error instead of &str); map/map_err heavily adapted (docs use String/format!/parse/println!); Try/branch exercised via '?' operator.
Adds Lean models for: Vec::is_empty, Vec::clear, Vec::truncate, Vec::as_slice, Vec::remove, Vec::append, Vec::split_off, and the Default instance for Vec<T>. Convention for mutating Vec methods: the returned tuple is (explicit_rust_return, new_self). For methods that mutate two Vecs (append), the return is (new_self, new_other). Vec::split_off in Rust returns the right half and mutates self to the left half, so the Aeneas model returns (right_half, new_self_as_left_half). Tests in tests/src/vec_methods.rs translate the Rust docs examples verbatim where possible; adaptations (using len() instead of vec!+ PartialEq<Vec>) are noted per test.
… for u8/usize - core::hint::black_box (identity) - core::borrow::Borrow trait + Borrow<T> for T identity-blanket impl (subsumes Borrow for &T after Aeneas reference erasure) - Eq for u8/usize assert_receiver_is_total_eq: satisfied by existing core.cmp.Eq.assert_receiver_is_total_eq.default trait-default handler Tests in tests/src/core_misc.rs exercise black_box, Borrow on references, and Eq via derive(Eq) on structs containing u8 and usize.
- Core/Convert.lean: core.num.error.TryFromIntError type - Core/Result.lean: Result::is_err - Scalar/CoreConvertNum.lean: U32::try_from(U64) impl returning core.result.Result<U32, TryFromIntError> - tests/src/convert_tryfrom.rs: verbatim docs example (overflow, fits, boundary cases)
…between)
Exercised via `for i in a..b { ... }` ranges on i32. The Step trait itself
is unstable Rust internals; test uses the public iteration surface.
…lEq<Array>), Range foundation (Bound, RangeFull, RangeBounds) - core.ops.range.RangeFull, core.ops.range.Bound<T>, core.ops.range.RangeBounds trait - RangeBounds impl for Range<T> and RangeFrom<T> - SliceIndex<RangeFull, [T], [T]> impl - Slice::clone_from_slice, Slice::copy_within (generic over RangeBounds) - Cross-type PartialEq<[U;N]> for [T] and Ord<[T]>
Modeled as a bounded list (same as Vec); the front/back distinction affects only constant factors, not semantics. Uses keepParams to erase allocator.
- `core.array.from_fn`: generic over closure type F with FnMut bound, builds array by calling the closure on indices 0..N. - Noted `char` is natively mapped to Lean's `Char` by the backend — added a test exercising char equality.
… to verbatim docs example - `core.array.iter.IntoIter<T, N>` struct and `Array::into_iter` constructor - `Iterator::next` impl for `IntoIter<T, N>` - Upgraded enumerate docs-example test to verbatim `['a', 'b', 'c']` (char + Option + Array now all modeled, so the example translates directly) - EnumerateProofs updated to reference Char values
- `Iterator::map::default`: wraps self+closure in Map adapter. - `Iterator::next` for Map<I, F>: pulls from inner, applies closure.
- Range::collect and Range::map forwarding to trait defaults - Iterator<Map<I,F>, B>::collect + IteratorMap instance for nested maps - Slice Iter<T>::collect and Iter<T>::map - VecIntoIter::collect delegating through FromIteratorVec
…orrow<[T]> for Vec<T> - alloc::slice::Concat trait - Borrow<Vec<T>, [T]>::borrow: canonical slice view - Concat<[V], T, Vec<T>>::concat: flattens via Borrow - [T]::concat method dispatch
Aeneas's InterpExpressions.read_place_check fails on `&str -> String` returns through move semantics. The stdlib model (opaque `String`) is already in place in Alloc.lean; the blocker is compiler-side. Parked in the tracker as deferred (like the fmt functions).
Str is already modeled as Slice U8; this converts the u8 slice back to
a Lean native String via UTF-8.
The earlier deferral was a misdiagnosis: the failing test was triggered
by a helper function returning a string literal directly
(`fn f() -> &'static str { "hello" }`), which is an independent Aeneas
translation bug. Using a top-level `const` workaround, `to_owned` itself
translates and runs cleanly.
- ProofHelpers.lean: `test_correct_of_native` lifts `native_decide` evaluation of `Result Unit` programs to WP postcondition proofs. - CharMethodsProofs (1), StrToOwnedProofs (1), CoreMiscProofs (4), ConvertTryfromProofs (3), ArrayFromFnProofs (1). Each theorem `test_X_correct : test_X ⦃ _ => True ⦄` asserts that the generated Aeneas test returns `.ok ()` — strictly stronger than the `#assert` line because it produces a kernel-checked proof term.
OptionMethodsProofs (10), ResultMethodsProofs (10), VecMethodsProofs (10). Each theorem asserts that the generated Aeneas test returns .ok ().
SliceMethodsProofs (3), SliceConcatProofs (1), VecDequeMethodsProofs (2), IteratorCollectProofs (1).
- StepI32Proofs: 2 theorems (range sum, range count) - EnumerateProofs: 3 more theorems (basic, empty, single) alongside the existing hand-driven `test_enumerate_docs_example_correct` WP proof. All native_decide-based proofs close via kernel reduction (partial_fixpoint loops evaluate cleanly).
…Methods (15) Replace `native_decide` with `unfold; step*` proofs that exercise library spec theorems. Existing @[simp, step_simps] on as_ref/black_box/ borrow + ok_or_some/none simp lemmas are sufficient for step* to close. Trailing `all_goals simp_all` handles residual equalities after step*-driven case splits.
…ack for complex tests - StrToOwnedProofs: simp-based (structural). 1 theorem. - SliceMethodsProofs (3), VecDequeMethodsProofs (2), ConvertTryfromProofs (3): documented fallback to test_correct_of_native for tests whose structural proof would require a new library spec theorem per method. Still produces a kernel-checked proof term via native_decide. Where specs are needed for a full structural upgrade: clone_from_slice_spec, copy_within_spec, PartialEqSliceArray.eq_spec, VecDeque.push_back_spec, VecDeque.pop_front_spec, U32.try_from_*_spec.
Updated `funs-external-stdlib.md` with a per-file proof-style breakdown and a punch list of library spec theorems that would unlock structural proofs for the remaining 16 native_decide tests.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The goal is to add to the Aeneas standard library models for everything which is required for curve25519-dalek, libsignal and SparsePostQuantumRatchet.
To make this easier to review, this can be split into separate PRs for each of the different groups of models.
Further work in progress to make it very easy for reviews to see easily that the added models are correct.
Progress is tracked in funs-external-stdlib.md.
char(Lean nativeChar),IntoIter<T, N>,Array::into_iteras_ref,ok_or,Clone,Default,PartialEqis_ok,is_err,unwrap_or,map,map_err,Try::branchtruncate,as_slice,remove,append,clear,is_empty,split_off,Defaultnew,len,push_back,pop_frontclone_from_slice,copy_within,Ord::cmp,concat,Concat<[V], T, Vec<T>>,PartialEq<[U;N]>Bound<T>,RangeFull,RangeBoundstrait, bounds impls,SliceIndex<RangeFull>, Range::collect/mapMap::next,Iterator::map, collect/map for Range/Iter/IntoIter/Mapfrom_fnwith FnMut closureforward_checked,backward_checked,steps_betweenBorrowblanket,Eqfor u8/usizeblack_box,TryFrom<u64> for u32,TryFromIntError,str::to_ownedfmtfunctions (impure effects)