Documentation changes

Author: satiscugcat

testable-simd-models/Cargo.toml

@@ -1,16 +1,16 @@
 [package]
-name = "core-models"
+name = "testable-simd-models"
 version = "0.0.2"
 authors = ["Cryspen"]
 license = "Apache-2.0"
-homepage = "https://github.com/cryspen-ext/core-models"
+homepage = "https://github.com/cryspen/verify-rust-std/testable-simd-models"
 edition = "2021"
-repository = "https://github.com/cryspen-ext/core-models"
+repository = "https://github.com/cryspen/verify-rust-std/testable-simd-models"
 readme = "README.md"
 
 [dependencies]
 rand = "0.9"
 pastey = "0.1.0"
 
 [lints.rust]
-unexpected_cfgs = { level = "warn", check-cfg = ['cfg(hax)'] }
+unexpected_cfgs = { level = "warn" }

testable-simd-models/README.md

@@ -1,2 +1,2 @@
-# core-models
-Rust models for the Core Library (extending work from libcrux/minicore)
+# testable-simd-models
+Rust models for the Core Library

testable-simd-models/hax.sh

@@ -1,5 +1,6 @@
-/// A fixed-size array wrapper with functional semantics and F* integration.
-///
+//! This module implements a fixed-size array wrapper with functional semantics
+//! which are used in formulating abstractions.
+
 /// `FunArray<N, T>` represents an array of `T` values of length `N`, where `N` is a compile-time constant.
 /// Internally, it uses a fixed-length array of `Option<T>` with a maximum capacity of 512 elements.
 /// Unused elements beyond `N` are filled with `None`.

testable-simd-models/src/abstractions/funarr.rs

@@ -1,5 +1,5 @@
 //! This module provides abstractions that are useful for writing
-//! specifications in minicore. Currently it provides two abstractions: bits and
+//! specifications for the intrinsics. Currently it provides two abstractions: bits and
 //! bit vectors.
 //!
 //! # Examples

testable-simd-models/src/abstractions/mod.rs

@@ -1,6 +1,6 @@
-//! `core-models`: A Rust Model for the `core` Library
+//! `testable-simd-models`: A Rust Model for the `core` Library
 //!
-//! `core-models` is a simplified, self-contained model of Rust’s `core` library. It aims to provide
+//! `testable-simd-models` is a simplified, self-contained model of Rust’s `core` library. It aims to provide
 //! a purely Rust-based specification of `core`'s fundamental operations, making them easier to
 //! understand, analyze, and formally verify. Unlike `core`, which may rely on platform-specific
 //! intrinsics and compiler magic, `core-models` expresses everything in plain Rust, prioritizing
@@ -21,11 +21,11 @@
 //!
 //! ## Intended Use
 //!
-//! `core-models` is designed as a reference model for formal verification and reasoning about Rust programs.
-//! By providing a readable, well-specified version of `core`'s behavior, it serves as a foundation for
+//! `testable-simd-models` is designed as a reference model for formal verification and reasoning about Rust programs.
+//! By providing a readable, testable, well-specified version of `core`'s behavior, it serves as a foundation for
 //! proof assistants and other verification tools.
 
-// This recursion limit is necessary for macro `core-models::core_arch::x86::interpretations::int_vec::tests::mk!`.
+// This recursion limit is necessary for mk! macro sued for tests.
 // We test functions with const generics, the macro generate a test per possible (const generic) control value.
 #![recursion_limit = "4096"]
 pub mod abstractions;