Merge pull request #14 from cryspen/bump-aeneas

feat: update to latest cryspen/aeneas

Author: abentkamp

.github/workflows/ci.yml

@@ -9,8 +9,8 @@ on:
 # All version pins live here.
 env:
   RUST_TOOLCHAIN: nightly-2026-02-07
-  CHARON_REV:    1ec8d4bb0116abf4486bac234ac01acf84e2a83a
-  AENEAS_REV:    2c0bf87600a4bdcd65e41e9c4eb4066200a48308
+  CHARON_REV:    a535e914f74db4fd9e6be7048f4233270d8945c0
+  AENEAS_REV:    8d2077ce4946b52d2d199fe9d2f2d520a4bf8184
   # Where the cache step stages the charon / aeneas binaries.
   AENEAS_DIR: ${{ github.workspace }}/.tools/aeneas
 

lean/CoreModels/Alloc/Funs.lean

@@ -23,13 +23,13 @@ set_option maxRecDepth 2048
 
 namespace CoreModels.alloc
 
-/-- [alloc::borrow::{alloc::borrow::ToOwned for T}::to_owned]:
+/-- [alloc::borrow::{impl alloc::borrow::ToOwned for T}::to_owned]:
     Source: 'src/lib.rs', lines 23:8-25:9
     Visibility: public -/
 def borrow.ToOwned.Blanket.to_owned {T : Type} (self : T) : Result T := do
   ok self
 
-/-- Trait implementation: [alloc::borrow::{alloc::borrow::ToOwned for T}]
+/-- Trait implementation: [alloc::borrow::{impl alloc::borrow::ToOwned for T}]
     Source: 'src/lib.rs', lines 22:4-26:5 -/
 @[reducible]
 def borrow.ToOwned.Blanket (T : Type) : borrow.ToOwned T := {
@@ -78,7 +78,7 @@ def collections.vec_deque.VecDeque.pop_front
     let (t, s1) ← rust_primitives.sequence.seq_remove s 0#usize
     ok (core.option.Option.Some t, (s1, pd))
 
-/-- [alloc::collections::vec_deque::{core::ops::index::Index<usize, T> for alloc::collections::vec_deque::VecDeque<T, A>}::index]:
+/-- [alloc::collections::vec_deque::{impl core::ops::index::Index<usize, T> for alloc::collections::vec_deque::VecDeque<T, A>}::index]:
     Source: 'src/lib.rs', lines 215:12-217:13
     Visibility: public -/
 def collections.vec_deque.VecDeque.Insts.CoreOpsIndexIndexUsizeT.index
@@ -89,7 +89,7 @@ def collections.vec_deque.VecDeque.Insts.CoreOpsIndexIndexUsizeT.index
   let (s, _) := self
   rust_primitives.sequence.seq_index s i
 
-/-- Trait implementation: [alloc::collections::vec_deque::{core::ops::index::Index<usize, T> for alloc::collections::vec_deque::VecDeque<T, A>}]
+/-- Trait implementation: [alloc::collections::vec_deque::{impl core::ops::index::Index<usize, T> for alloc::collections::vec_deque::VecDeque<T, A>}]
     Source: 'src/lib.rs', lines 212:8-218:9 -/
 @[reducible]
 def collections.vec_deque.VecDeque.Insts.CoreOpsIndexIndexUsizeT (T : Type) (A
@@ -147,14 +147,16 @@ def vec.VecTGlobal.with_capacity
 /-- [alloc::vec::{alloc::vec::Vec<T, A>}::len]:
     Source: 'src/lib.rs', lines 371:8-373:9
     Visibility: public -/
-def vec.Vec.len {T : Type} (A : Type) (self : vec.Vec T A) : Result Std.Usize := do
+def vec.Vec.len
+  {T : Type} {A : Type} (self : vec.Vec T A) : Result Std.Usize := do
   let (s, _) := self
   rust_primitives.sequence.seq_len s
 
 /-- [alloc::vec::{alloc::vec::Vec<T, A>}::push]:
     Source: 'src/lib.rs', lines 375:8-377:9
     Visibility: public -/
-def vec.Vec.push {T : Type} (A : Type) (self : vec.Vec T A) (x : T) :
+def vec.Vec.push
+  {T : Type} {A : Type} (self : vec.Vec T A) (x : T) :
   Result (vec.Vec T A)
   := do
   let (s, pd) := self
@@ -189,7 +191,8 @@ def vec.Vec.is_empty
 /-- [alloc::vec::{alloc::vec::Vec<T, A>}::insert]:
     Source: 'src/lib.rs', lines 391:8-396:9
     Visibility: public -/
-def vec.Vec.insert {T : Type} (A : Type) (self : vec.Vec T A) (index : Std.Usize) (element : T)
+def vec.Vec.insert
+  {T : Type} {A : Type} (self : vec.Vec T A) (index : Std.Usize) (element : T)
   :
   Result (vec.Vec T A)
   := do
@@ -281,7 +284,7 @@ def vec.Vec.drain
   let (s1, s2) ← rust_primitives.sequence.seq_drain s 0#usize l
   ok ((s1, core.marker.PhantomData.mk), (s2, pd))
 
-/-- [alloc::vec::drain::{core::iter::traits::iterator::Iterator<T> for alloc::vec::drain::Drain<T, A>}::next]:
+/-- [alloc::vec::drain::{impl core::iter::traits::iterator::Iterator<T> for alloc::vec::drain::Drain<T, A>}::next]:
     Source: 'src/lib.rs', lines 431:12-438:13
     Visibility: public -/
 def vec.drain.Drain.Insts.CoreIterTraitsIteratorIterator.next
@@ -296,7 +299,7 @@ def vec.drain.Drain.Insts.CoreIterTraitsIteratorIterator.next
     let (res, s1) ← rust_primitives.sequence.seq_remove s 0#usize
     ok (core.option.Option.Some res, (s1, pd))
 
-/-- Trait implementation: [alloc::vec::drain::{core::iter::traits::iterator::Iterator<T> for alloc::vec::drain::Drain<T, A>}]
+/-- Trait implementation: [alloc::vec::drain::{impl core::iter::traits::iterator::Iterator<T> for alloc::vec::drain::Drain<T, A>}]
     Source: 'src/lib.rs', lines 429:8-439:9 -/
 @[reducible]
 def vec.drain.Drain.Insts.CoreIterTraitsIteratorIterator (T : Type) (A : Type)
@@ -306,22 +309,23 @@ def vec.drain.Drain.Insts.CoreIterTraitsIteratorIterator (T : Type) (A : Type)
 
 /-- [alloc::vec::{alloc::vec::Vec<T, A>}::extend_from_slice]:
     Source: 'src/lib.rs', lines 445:8-447:9 -/
-def vec.Vec.extend_from_slice {T : Type} (A : Type) (corecloneCloneInst : core.clone.Clone T)
+def vec.Vec.extend_from_slice
+  {T : Type} {A : Type} (corecloneCloneInst : core.clone.Clone T)
   (self : vec.Vec T A) (other : Slice T) :
   Result (vec.Vec T A)
   := do
   let (s, pd) := self
   let s1 ← rust_primitives.sequence.seq_extend corecloneCloneInst s other
   ok (s1, pd)
 
-/-- [alloc::vec::{core::ops::deref::Deref<[T]> for alloc::vec::Vec<T, A>}::deref]:
+/-- [alloc::vec::{impl core::ops::deref::Deref<[T]> for alloc::vec::Vec<T, A>}::deref]:
     Source: 'src/lib.rs', lines 478:8-480:9
     Visibility: public -/
 def vec.Vec.Insts.CoreOpsDerefDerefSlice.deref
   {T : Type} {A : Type} (self : vec.Vec T A) : Result (Slice T) := do
   vec.Vec.as_slice self
 
-/-- Trait implementation: [alloc::vec::{core::ops::deref::Deref<[T]> for alloc::vec::Vec<T, A>}]
+/-- Trait implementation: [alloc::vec::{impl core::ops::deref::Deref<[T]> for alloc::vec::Vec<T, A>}]
     Source: 'src/lib.rs', lines 475:4-481:5 -/
 @[reducible]
 def vec.Vec.Insts.CoreOpsDerefDerefSlice (T : Type) (A : Type) :