Merge pull request #2086 from cryspen/core-models-various-extensions

Core models extensions.

Author: maximebuyse

hax-lib/core-models/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>
 

hax-lib/core-models/alloc/src/lib.rs

@@ -469,6 +469,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 {
@@ -524,6 +531,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,
@@ -702,6 +716,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, A> {
+            let l = seq_len(&self.0);
+            Vec(seq_drain(&mut self.0, at, l), PhantomData)
+        }
         #[hax_lib::opaque]
         pub fn drain<R /* : RangeBounds<usize> */>(&mut self, _range: R) -> drain::Drain<T, A> {
             let l = seq_len(&self.0);

hax-lib/core-models/alloc/src/vec/tests.rs

@@ -101,6 +101,18 @@ proptest! {
         }
     }
 
+    #[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();
@@ -156,6 +168,16 @@ fn test_with_capacity() {
     assert_eq!(model, std_v.inject());
 }
 
+// Only the default variant models `Default`: adding the impl to the F* variant
+// would shift F*'s positional impl-block numbering and rename every `Vec` method.
+#[cfg(not(hax_backend_fstar))]
+#[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());
+}
+
 // ----- Clone / PartialEq / IntoIterator -------
 //
 // The F* variant of `vec` models none of these three, so the tests below are

hax-lib/core-models/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_backend_fstar))]
-clone_impl_for_int!(
+clone_impl_for_copy!(
+    core::primitive::bool,
     core::primitive::u8,
     core::primitive::u16,
     core::primitive::u32,
@@ -54,13 +55,25 @@ clone_impl_for_int!(
 #[cfg(test)]
 mod tests {
     use crate::testing::Inject;
+    use pastey::paste;
     use proptest::prelude::*;
 
-    proptest! {
-        #[test]
-        fn test_clone(x in any::<u8>()) {
-            let model = x.inject();
-            prop_assert_eq!(model.clone(), model);
-        }
+    // For every `Copy` type with a `Clone` impl, check the model's `Clone`
+    // agrees with std's on a random value.
+    macro_rules! clone_tests {
+        ($($t:ident),*) => {
+            paste! { $(
+                proptest! {
+                    #[test]
+                    fn [<test_clone_ $t>](x in any::<$t>()) {
+                        prop_assert_eq!(crate::clone::Clone::clone(x.inject()), x.clone().inject());
+                    }
+                }
+            )* }
+        };
     }
+
+    clone_tests!(
+        bool, u8, u16, u32, u64, u128, usize, i8, i16, i32, i64, i128, isize
+    );
 }

hax-lib/core-models/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;
@@ -80,14 +80,16 @@ 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 {
+// The blanket `AsRef<T> for T` can't cover the unsized `[T]`, so we provide the
+// concrete slice impl.
+impl<T> AsRef<[T]> for [T] {
+    fn as_ref(&self) -> &[T] {
         self
     }
 }
@@ -249,9 +251,14 @@ mod tests {
             prop_assert_eq!(super::Into::<u8>::into(x.inject()), x);
         }
 
+        // Model's `AsRef<[u8]>` vs std's, both projecting a slice to itself.
         #[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::<[u8]>::as_ref(s),
+                core::convert::AsRef::<[u8]>::as_ref(s)
+            );
         }
     }
 

hax-lib/core-models/core-models/src/core/fmt.rs

@@ -44,6 +44,35 @@ impl<T> Debug for T {
     }
 }
 
+// No blanket `Display` (unlike `Debug` above); spell out the integer impls,
+// 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> {}

hax-lib/core-models/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 elsewhere in 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 std keeps in `core::hash::impls`.
+//
+// DEVIATION(std): std feeds `to_ne_bytes()`; the abstract `Hasher` makes the
+// exact bytes unobservable, so we feed a single cast byte.
+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
+);

hax-lib/core-models/core-models/src/core/intrinsics.rs

@@ -0,0 +1,7 @@
+/// See [`core::intrinsics::unreachable`]. UB in Rust; modeled as an unreachable
+/// panic, with `requires(false)` so callers must prove it is never hit.
+#[hax_lib::opaque]
+#[hax_lib::requires(false)]
+pub fn unreachable() -> ! {
+    panic!()
+}