Simd models

.gitignore

@@ -52,3 +52,4 @@ package-lock.json
 # already existing elements were commented out
 
 #/target
+testable-simd-models/target

testable-simd-models/Cargo.toml

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

testable-simd-models/README.md

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

testable-simd-models/hax.sh

@@ -0,0 +1,91 @@
+#!/usr/bin/env bash
+set -e
+
+function extract_all() {
+    go_to "./"
+    cargo hax into fstar --z3rlimit 80
+}
+
+function prove() {
+    case "$1" in
+        --admit)
+            shift 1
+            export OTHERFLAGS="--admit_smt_queries true";;
+        *);;
+    esac
+    go_to "./"
+    JOBS="${JOBS:-$(nproc --all)}"
+    JOBS="${JOBS:-4}"
+    make -C proofs/fstar/extraction -j $JOBS "$@"
+}
+
+function init_vars() {
+    SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
+    SCRIPT_NAME="$(basename "${BASH_SOURCE[0]}")"
+    SCRIPT_PATH="${SCRIPT_DIR}/${SCRIPT_NAME}"
+
+    if [ -t 1 ]; then
+        BLUE='\033[34m'
+        GREEN='\033[32m'
+        BOLD='\033[1m'
+        RESET='\033[0m'
+    else
+        BLUE=''
+        GREEN=''
+        BOLD=''
+        RESET=''
+    fi
+}
+
+function go_to() {
+    ROOT="$SCRIPT_DIR"
+    cd "$ROOT"
+    cd "$1"
+}
+
+function msg() {
+    echo -e "$1[$SCRIPT_NAME]$RESET $2"
+}
+
+function help() {
+    echo "Libcrux script to extract Rust to F* via hax."
+    echo ""
+    echo "Usage: $0 [COMMAND]"
+    echo ""
+    echo "Comands:"
+    echo ""
+    grep '[#]>' "$SCRIPT_PATH" | sed 's/[)] #[>]/\t/g'
+    echo ""
+}
+
+function cli() {
+    if [ -z "$1" ]; then
+        help
+        exit 1
+    fi
+    # Check if an argument was provided
+
+    case "$1" in
+        --help) #> Show help message
+            help;;
+        extract) #> Extract the F* code for the proofs.
+            extract_all
+            msg "$GREEN" "done"
+            ;;
+        prove) #> Run F*. This typechecks the extracted code. To lax-typecheck use --admit.
+            shift 1
+            prove "$@";;
+        extract+prove) #> Equivalent to extracting and proving.
+            shift 1
+            extract_all
+            prove "$@";;
+        *)
+            echo "Invalid option: $1"
+            help
+            exit 1;;
+    esac
+}
+
+init_vars
+
+cli "$@"