Extensions#15
Open
maximebuyse wants to merge 6 commits into
Open
Conversation
maximebuyse
force-pushed
the
spqr-extensions
branch
from
4ea35ec to
0dd2fb8
Compare
abentkamp
approved these changes
Jun 8, 2026
abentkamp
left a comment
abentkamp
left a comment
Collaborator
There was a problem hiding this comment.
The solution for Vec looks great! I have a couple of comments.
Comment on lines
+12
to
+14
| pub trait Allocator { | ||
| fn dummy(); | ||
| } |
Collaborator
There was a problem hiding this comment.
Why the dummy function? Can we document why it's here?
Comment on lines
+256
to
+268
| fn eq(&self, other: &[U]) -> bool { | ||
| if self.len() != other.len() { | ||
| false | ||
| } else { | ||
| let mut res = true; | ||
| for i in 0..self.len() { | ||
| if !self[i].eq(&other[i]) { | ||
| res = false; | ||
| } | ||
| } | ||
| res | ||
| } | ||
| } |
Collaborator
There was a problem hiding this comment.
I think this should short-circuit when a mismatch is found, right? Later comparisons might panic, which would cause a behavior that's different from the official implementation.
Comment on lines
+51
to
+56
| The `@[rust_fun "…"]` attribute binds the Rust path of the provided method to | ||
| this body, so the downstream name-map lands here. The body just builds the | ||
| `Map` adapter; iteration then runs through `Map`'s own `Iterator` instance. | ||
| `F` is the closure, `T` the item, `O` its output (the `FnMut` instance is | ||
| irrelevant to the model, hence `_`-prefixed). -/ | ||
| @[rust_fun "alloc::vec::into_iter::{core::iter::traits::iterator::Iterator<alloc::vec::into_iter::IntoIter<@T, @A>, @T>}::map"] |
Collaborator
There was a problem hiding this comment.
Is the @[rust_fun] attribute necessary? Isn't that needed only for Aeneas's core setup?
| super-instance (the `iteratorIteratorInst` field was dropped), so there is no | ||
| `next` to drive a fold here. Refine if downstream reasoning depends on the | ||
| contents of a `VecDeque::from_iter` result. -/ | ||
| @[rust_trait_impl "core::iter::traits::collect::FromIterator<alloc::collections::vec_deque::VecDeque<@T, alloc::alloc::Global>, @T>"] |
Comment on lines
+72
to
+87
| NOTE: this is a *stub* — `from_iter` returns an empty deque. We cannot model | ||
| the real collect: core-models' `IntoIterator` carries no `Iterator` | ||
| super-instance (the `iteratorIteratorInst` field was dropped), so there is no | ||
| `next` to drive a fold here. Refine if downstream reasoning depends on the | ||
| contents of a `VecDeque::from_iter` result. -/ | ||
| @[rust_trait_impl "core::iter::traits::collect::FromIterator<alloc::collections::vec_deque::VecDeque<@T, alloc::alloc::Global>, @T>"] | ||
| def collections.vec_deque.VecDequeTGlobal.Insts.CoreIterTraitsCollectFromIterator | ||
| (T : Type) : | ||
| core.iter.traits.collect.FromIterator | ||
| (collections.vec_deque.VecDeque T alloc.Global) T := { | ||
| from_iter := fun {U Item IntoIter} | ||
| (_IntoIteratorInst : core.iter.traits.collect.IntoIterator U Item IntoIter) | ||
| (_iter : U) => do | ||
| let s ← rust_primitives.sequence.seq_empty T | ||
| Aeneas.Std.Result.ok (s, core.marker.PhantomData.mk) | ||
| } |
Collaborator
There was a problem hiding this comment.
Maybe we can use Lean's opaque command instead of a def?
opaque collections.vec_deque.VecDequeTGlobal.Insts.CoreIterTraitsCollectFromIterator.from_iter
(T : Type) : {T_1 Clause0_Item Clause0_IntoIter : Type} →
core.iter.traits.collect.IntoIterator T_1 Clause0_Item Clause0_IntoIter →
T_1 → Aeneas.Std.Result (VecDeque T alloc.Global)
def collections.vec_deque.VecDequeTGlobal.Insts.CoreIterTraitsCollectFromIterator
(T : Type) :
core.iter.traits.collect.FromIterator
(collections.vec_deque.VecDeque T alloc.Global) T := {
from_iter := collections.vec_deque.VecDequeTGlobal.Insts.CoreIterTraitsCollectFromIterator.from_iter T
}That will make the constant available without giving a definition, similar to an axiom. But in contrast to an axiom, it will not introduce extra logical assumptions (using the fact that Aeneas.Std.Result is inhabited).
That way we could avoid defining a model that is not accurate.
Comment on lines
+114
to
+119
| -- `vec.Vec.new` / `vec.Vec.with_capacity` are now extracted directly into | ||
| -- `CoreModels.Alloc` (and `vec.VecTGlobal` no longer exists, since `vec.Vec` | ||
| -- dropped its allocator type parameter), so these manual re-exports are | ||
| -- obsolete: | ||
| -- def vec.Vec.new := @vec.VecTGlobal.new | ||
| -- def vec.Vec.with_capacity := @vec.VecTGlobal.with_capacity |
Comment on lines
+22
to
+33
| /-! ## PhantomData — replaces Aeneas's reducible alias | ||
|
|
||
| Aeneas extracts `core::marker::PhantomData` as the reducible alias | ||
| `def marker.PhantomData (T) := T` and builds phantom values with `()` (Charon | ||
| models it as a ZST). That alias is unusable here: where `PhantomData A` is the | ||
| second component of a pair (e.g. `vec.drain.Drain T A := Seq T × PhantomData A`), | ||
| Lean unfolds it and loses `A` during unification. | ||
|
|
||
| So we model it as a *non-reducible* `structure` instead, which keeps `A` | ||
| syntactically present. `patch_lean.py`'s `rewrite_phantom_data` rewires the | ||
| Aeneas output onto this carrier: it comments out the generated alias and | ||
| rewrites the `()` constructor sites to `core.marker.PhantomData.mk`. |
Collaborator
There was a problem hiding this comment.
I think this explanation is wrong. The issue is not unfolding during unification.
The issue is that when A is abstract (or any type other than alloc.Global or Unit), the value () does not have the right type because () is of type Unit and not of type PhantomData A or A.
A simpler solution might be to define
def marker.PhantomData (A : Type) := Unit
and to remove the () -> core.marker.PhantomData.mk replacement.
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
2 participants
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.
Various extensions needed for a proof project. The main decision was to switch the
Vecmodel to take no allocator, this goes together with a change in aeneas (merged to our core-models option in cryspen/aeneas/dev)