Various extensions

COVERAGE.md

@@ -8,7 +8,7 @@ Some platform and runtime modules are not targeted and taken out of the count. S
 
 ## `core`
 
-**Targeted coverage: 683/3888 items (18%) across 35 modules — 21 have at least a partial model.**
+**Targeted coverage: 706/3888 items (18%) across 35 modules — 21 have at least a partial model.**
 
 | module | covered | total | coverage |
 |---|--:|--:|---|
@@ -30,13 +30,13 @@ Some platform and runtime modules are not targeted and taken out of the count. S
 | `f64` | 0 | 107 | 0% |
 | `fmt` | 9 | 111 | 8% |
 | `from` | 0 | 1 | 0% |
-| `hash` | 3 | 29 | 10% |
+| `hash` | 5 | 29 | 17% |
 | `hint` | 2 | 15 | 13% |
 | `index` | 0 | 2 | 0% |
 | `iter` | 27 | 170 | 16% |
 | `marker` | 6 | 35 | 17% |
 | `mem` | 19 | 80 | 24% |
-| `num` | 417 | 1835 | 23% |
+| `num` | 435 | 1835 | 24% |
 | `ops` | 84 | 151 | 56% |
 | `option` | 26 | 57 | 46% |
 | `panicking` | 2 | 31 | 6% |
@@ -45,18 +45,18 @@ Some platform and runtime modules are not targeted and taken out of the count. S
 | `ptr` | 0 | 191 | 0% |
 | `range` | 0 | 19 | 0% |
 | `result` | 30 | 42 | 71% |
-| `slice` | 8 | 205 | 4% |
+| `slice` | 11 | 205 | 5% |
 | `str` | 6 | 160 | 4% |
-| **subtotal** | **683** | **3888** | **18%** |
+| **subtotal** | **706** | **3888** | **18%** |
 
-<details><summary>Non-targeted modules: 20 modules, 0/14842 items</summary>
+<details><summary>Non-targeted modules: 20 modules, 1/14842 items</summary>
 
 `alloc`, `arch`, `async_iter`, `autodiff`, `bstr`, `contracts`, `ffi`, `future`, `intrinsics`, `io`, `net`, `os`, `panic`, `pat`, `random`, `simd`, `sync`, `task`, `time`, `unsafe_binder`
 </details>
 
 ## `alloc`
 
-**Targeted coverage: 44/608 items (7%) across 11 modules — 7 have at least a partial model.**
+**Targeted coverage: 45/608 items (7%) across 11 modules — 7 have at least a partial model.**
 
 | module | covered | total | coverage |
 |---|--:|--:|---|
@@ -70,8 +70,8 @@ Some platform and runtime modules are not targeted and taken out of the count. S
 | `slice` | 0 | 6 | 0% |
 | `str` | 0 | 1 | 0% |
 | `string` | 5 | 63 | 8% |
-| `vec` | 19 | 80 | 24% |
-| **subtotal** | **44** | **608** | **7%** |
+| `vec` | 20 | 80 | 25% |
+| **subtotal** | **45** | **608** | **7%** |
 
 <details><summary>Non-targeted modules: 4 modules, 0/106 items</summary>
 

alloc/src/lib.rs

@@ -457,6 +457,13 @@ pub mod vec {
         }
     }
 
+    /// See [`std::vec::Vec::default`]: an empty `Vec`.
+    impl<T> Default for Vec<T> {
+        fn default() -> Vec<T> {
+            Vec::new()
+        }
+    }
+
     #[hax_lib::attributes]
     impl<T> Vec<T> {
         pub fn len(&self) -> usize {
@@ -512,6 +519,13 @@ pub mod vec {
             seq_concat(&mut self.0, &mut other.0);
             other.0 = seq_empty()
         }
+        /// See [`std::vec::Vec::split_off`]: truncate `self` to `[0, at)` and
+        /// return the tail `[at, len)` as a new `Vec`.
+        #[hax_lib::requires(at <= self.len())]
+        pub fn split_off(&mut self, at: usize) -> Vec<T> {
+            let l = seq_len(&self.0);
+            Vec(seq_drain(&mut self.0, at, l))
+        }
         #[hax_lib::opaque]
         pub fn drain<R /* : RangeBounds<usize> */>(
             &mut self,
@@ -673,6 +687,18 @@ pub mod vec {
                 }
             }
 
+            #[test]
+            fn test_split_off(v in prop::collection::vec(any::<u8>(), 0..50), at in 0usize..50) {
+                if at <= v.len() {
+                    let mut model = v.inject();
+                    let mut std_v = v.clone();
+                    let model_tail = model.split_off(at);
+                    let std_tail = std_v.split_off(at);
+                    prop_assert_eq!(model, std_v.inject());
+                    prop_assert_eq!(model_tail, std_tail.inject());
+                }
+            }
+
             #[test]
             fn test_append(v1 in prop::collection::vec(any::<u8>(), 0..50), v2 in prop::collection::vec(any::<u8>(), 0..50)) {
                 let mut model1 = v1.inject();
@@ -739,5 +765,12 @@ pub mod vec {
             let std_v: std::vec::Vec<u8> = std::vec::Vec::with_capacity(10);
             assert_eq!(model, std_v.inject());
         }
+
+        #[test]
+        fn test_default() {
+            let model: super::Vec<u8> = Default::default();
+            let std_v: std::vec::Vec<u8> = Default::default();
+            assert_eq!(model, std_v.inject());
+        }
     }
 }

core-models/src/core/clone.rs

@@ -23,7 +23,7 @@ impl<T> Clone for T {
     }
 }
 
-macro_rules! clone_impl_for_int {
+macro_rules! clone_impl_for_copy {
     ($($t:ty),*) => {
         $(
             impl crate::clone::Clone for $t {
@@ -36,7 +36,8 @@ macro_rules! clone_impl_for_int {
 }
 
 #[cfg(not(hax))]
-clone_impl_for_int!(
+clone_impl_for_copy!(
+    core::primitive::bool,
     core::primitive::u8,
     core::primitive::u16,
     core::primitive::u32,
@@ -62,5 +63,10 @@ mod tests {
             let model = x.inject();
             prop_assert_eq!(model.clone(), model);
         }
+
+        #[test]
+        fn test_clone_bool(x in any::<bool>()) {
+            prop_assert_eq!(crate::clone::Clone::clone(x), x);
+        }
     }
 }

core-models/src/core/convert.rs

@@ -19,7 +19,7 @@ trait Into<T> {
 
 /// See [`std::convert::From`]
 #[hax_lib::attributes]
-trait From<T> {
+pub trait From<T> {
     /// See [`std::convert::From::from`]
     #[hax_lib::requires(true)]
     fn from(x: T) -> Self;
@@ -55,7 +55,12 @@ use crate::array::TryFromSliceError;
 impl<T: Copy, const N: usize> TryFrom<&[T]> for [T; N] {
     type Error = TryFromSliceError;
     fn try_from(x: &[T]) -> Result<[T; N], TryFromSliceError> {
-        if x.len() == N {
+        // Use the primitive length directly rather than `x.len()`: the latter
+        // extracts to a reference to `slice::Slice::len`, which (under
+        // `-core-models-lib`) Aeneas emits as an external-looking name with no
+        // dependency edge, producing a forward reference here (this `convert`
+        // module is extracted before `slice`).
+        if rust_primitives::slice::slice_length(x) == N {
             Result::Ok(rust_primitives::slice::array_from_fn(|i| {
                 *rust_primitives::slice::slice_index(x, i)
             }))
@@ -80,14 +85,18 @@ impl<T> From<T> for T {
 
 /// See [`std::convert::AsRef`]
 #[hax_lib::attributes]
-trait AsRef<T> {
+pub trait AsRef<T: ?Sized> {
     /// See [`std::convert::AsRef::as_ref`]
     #[hax_lib::requires(true)]
-    fn as_ref(self) -> T;
+    fn as_ref(&self) -> &T;
 }
 
-impl<T> AsRef<T> for T {
-    fn as_ref(self) -> T {
+/// `impl AsRef<[T]> for [T]`. std exposes many concrete `AsRef` impls; the model
+/// used a single `impl<T> AsRef<T> for T` blanket, but that can't cover the
+/// unsized `[T]` (and Aeneas references the per-type impl name anyway), so we
+/// provide the concrete slice impl.
+impl<T> AsRef<[T]> for [T] {
+    fn as_ref(&self) -> &[T] {
         self
     }
 }
@@ -250,8 +259,9 @@ mod tests {
         }
 
         #[test]
-        fn test_as_ref_identity(x in any::<u8>()) {
-            prop_assert_eq!(super::AsRef::as_ref(x.inject()), x);
+        fn test_as_ref_slice_identity(v in prop::collection::vec(any::<u8>(), 0..=8)) {
+            let s: &[u8] = &v[..];
+            prop_assert_eq!(super::AsRef::as_ref(s), s);
         }
     }
 

core-models/src/core/fmt.rs

@@ -36,6 +36,36 @@ impl<T> Debug for T {
     }
 }
 
+// `Display` has no blanket impl (unlike `Debug` above), so we spell out the
+// integer impls std keeps under `core::fmt::num`. Formatting is stubbed to
+// `Ok(())` like the rest of this module.
+macro_rules! impl_display_for_int {
+    ($($t:ty),*) => {
+        $(
+            impl Display for $t {
+                fn fmt(&self, f: &mut Formatter) -> Result {
+                    Result::Ok(())
+                }
+            }
+        )*
+    };
+}
+
+impl_display_for_int!(
+    core::primitive::u8,
+    core::primitive::u16,
+    core::primitive::u32,
+    core::primitive::u64,
+    core::primitive::u128,
+    core::primitive::usize,
+    core::primitive::i8,
+    core::primitive::i16,
+    core::primitive::i32,
+    core::primitive::i64,
+    core::primitive::i128,
+    core::primitive::isize
+);
+
 impl<'a> Arguments<'a> {}
 impl<'a> Arguments<'a> {}
 impl<'a> Arguments<'a> {}

core-models/src/core/hash.rs

@@ -1,17 +1,49 @@
 /// See [`std::hash::Hasher`]
-pub trait Hasher {}
+pub trait Hasher {
+    /// See [`std::hash::Hasher::finish`]
+    fn finish(&self) -> u64;
+    /// See [`std::hash::Hasher::write`]
+    fn write(&mut self, bytes: &[u8]);
+}
 
 /// See [`std::hash::Hash`]
 #[hax_lib::attributes]
 pub trait Hash {
-    /// See [`std::hash::Hash::hash`]
+    /// See [`std::hash::Hash::hash`]. As in the rest of the model, the hasher is
+    /// threaded by value (`h: H` in, `H` out) rather than by `&mut`.
     #[hax_lib::requires(true)]
     fn hash<H: Hasher>(&self, h: H) -> H;
 }
 
-// Temporary
-impl<T> Hash for T {
-    fn hash<H: Hasher>(&self, h: H) -> H {
-        crate::panicking::internal::panic()
-    }
+// The integer `Hash` impls that std keeps in `core::hash::impls`. The model's
+// `Hasher` is abstract, so the hashed value is not meaningful — each impl just
+// feeds a byte to `write` (a single cast byte keeps the bodies uniform without
+// needing `to_ne_bytes`).
+macro_rules! impl_hash_for_int {
+    ($($t:ty),*) => {
+        $(
+            #[hax_lib::attributes]
+            impl Hash for $t {
+                fn hash<H: Hasher>(&self, mut h: H) -> H {
+                    h.write(&[*self as u8]);
+                    h
+                }
+            }
+        )*
+    };
 }
+
+impl_hash_for_int!(
+    core::primitive::u8,
+    core::primitive::u16,
+    core::primitive::u32,
+    core::primitive::u64,
+    core::primitive::u128,
+    core::primitive::usize,
+    core::primitive::i8,
+    core::primitive::i16,
+    core::primitive::i32,
+    core::primitive::i64,
+    core::primitive::i128,
+    core::primitive::isize
+);

core-models/src/core/intrinsics.rs

@@ -0,0 +1,8 @@
+/// See [`core::intrinsics::unreachable`]. Reaching this is undefined behaviour
+/// in Rust; in the model we treat it as an (unreachable) panic, with a
+/// `requires(false)` precondition so callers must prove it is never hit.
+#[hax_lib::opaque]
+#[hax_lib::requires(false)]
+pub fn unreachable() -> ! {
+    panic!()
+}