diff --git a/.ci/install.sh b/.ci/install.sh deleted file mode 100755 index f54f504247a..00000000000 --- a/.ci/install.sh +++ /dev/null @@ -1,24 +0,0 @@ -#!/usr/bin/env bash - -set -e - -if [[ "$TRAVIS_OS_NAME" == "osx" ]]; then - brew install ocaml opam z3 gnu-sed findutils; -fi -if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then - sudo apt-get install --yes libssl-dev opam libgmp-dev libsqlite3-dev; -fi - -export OPAMYES=true -opam init -eval $(opam config env) -opam install batteries sqlite3 fileutils stdint zarith yojson pprint - -if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then - export Z3=z3-4.4.1-x64-ubuntu-14.04; - wget https://github.com/Z3Prover/z3/releases/download/z3-4.4.1/$Z3.zip; - unzip $Z3.zip; - export PATH=/home/travis/build/FStarLang/FStar/$Z3/bin:/home/travis/build/FStarLang/FStar/bin:$PATH; -fi - -ocamlfind ocamlopt -config diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json index f554b1fbaf0..13cf22644c5 100644 --- a/.devcontainer/devcontainer.json +++ b/.devcontainer/devcontainer.json @@ -1,6 +1,7 @@ { "name": "F* minimal devcontainer", "build": { + "context": "..", "dockerfile": "minimal.Dockerfile" }, "customizations": { diff --git a/.devcontainer/minimal.Dockerfile b/.devcontainer/minimal.Dockerfile index 0dfc4b789fe..c622f65d0b3 100644 --- a/.devcontainer/minimal.Dockerfile +++ b/.devcontainer/minimal.Dockerfile @@ -17,6 +17,7 @@ RUN apt-get update \ python3 \ python-is-python3 \ libgmp-dev \ + pkg-config \ opam \ && apt-get clean -y # FIXME: libgmp-dev should be installed automatically by opam, @@ -34,6 +35,10 @@ RUN mkdir -p $HOME/bin # Make sure ~/bin is in the PATH RUN echo 'export PATH=$HOME/bin:$PATH' | tee --append $HOME/.profile $HOME/.bashrc $HOME/.bash_profile +# Install Z3 +COPY ./bin/get_fstar_z3.sh /usr/local/bin +RUN get_fstar_z3.sh ~/bin + # Install dotnet ENV DOTNET_ROOT /home/$USER/dotnet RUN wget -nv https://download.visualstudio.microsoft.com/download/pr/cd0d0a4d-2a6a-4d0d-b42e-dfd3b880e222/008a93f83aba6d1acf75ded3d2cfba24/dotnet-sdk-6.0.400-linux-x64.tar.gz && \ @@ -43,17 +48,12 @@ RUN wget -nv https://download.visualstudio.microsoft.com/download/pr/cd0d0a4d-2a rm -f dotnet-sdk*.tar.gz # Install OCaml -ARG OCAML_VERSION=4.14.0 +ARG OCAML_VERSION=4.14.2 RUN opam init --compiler=$OCAML_VERSION --disable-sandboxing RUN opam option depext-run-installs=true ENV OPAMYES=1 -RUN opam install --yes batteries zarith stdint yojson dune menhir menhirLib mtime pprint sedlex ppxlib process ppx_deriving ppx_deriving_yojson memtrace - -# Get compiled Z3 -RUN wget -nv https://github.com/Z3Prover/z3/releases/download/Z3-4.8.5/z3-4.8.5-x64-ubuntu-16.04.zip \ - && unzip z3-4.8.5-x64-ubuntu-16.04.zip \ - && cp z3-4.8.5-x64-ubuntu-16.04/bin/z3 $HOME/bin/z3 \ - && rm -r z3-4.8.5-* +COPY ./fstar.opam . +RUN opam install --deps-only . && rm fstar.opam WORKDIR $HOME diff --git a/.docker/base.Dockerfile b/.docker/base.Dockerfile index e5f5e392eef..9305389d88e 100644 --- a/.docker/base.Dockerfile +++ b/.docker/base.Dockerfile @@ -33,22 +33,13 @@ RUN apt-get install -y --no-install-recommends \ sudo \ python3 \ python-is-python3 \ + pkg-config \ opam \ && apt-get clean -y -# Install the Z3 versions we want to use in CI (4.8.5, 4.13.3). Note: we -# currently also have 4.8.5 in the opam switch, as it is a dependency of -# in fstar.opam, but that should be removed. - -RUN wget -nv https://github.com/Z3Prover/z3/releases/download/Z3-4.8.5/z3-4.8.5-x64-ubuntu-16.04.zip \ - && unzip z3-4.8.5-x64-ubuntu-16.04.zip \ - && cp z3-4.8.5-x64-ubuntu-16.04/bin/z3 /usr/local/bin/z3-4.8.5 \ - && rm -r z3-4.8.5-* - -RUN wget -nv https://github.com/Z3Prover/z3/releases/download/z3-4.13.3/z3-4.13.3-x64-glibc-2.35.zip \ - && unzip z3-4.13.3-x64-glibc-2.35 \ - && cp z3-4.13.3-x64-glibc-2.35/bin/z3 /usr/local/bin/z3-4.13.3 \ - && rm -r z3-4.13.3-* +# Install the relevant Z3 versions. +COPY ./bin/get_fstar_z3.sh /usr/local/bin +RUN get_fstar_z3.sh /usr/local/bin # Create a new user and give them sudo rights # NOTE: we give them the name "opam" to keep compatibility with diff --git a/.docker/nu_base.Dockerfile b/.docker/nu_base.Dockerfile index a3373a21b28..fa6a17116e7 100644 --- a/.docker/nu_base.Dockerfile +++ b/.docker/nu_base.Dockerfile @@ -1,7 +1,7 @@ # For check-world workflow, should be coallesced to the other base. # This could definitely use a big cleanup too. # FIXME: z3.4.8.5-1 can no longer be installed on Ubuntu 24.04 because python3-distutils disappeared, and the z3 opam package has not been fixed for version 4.8.5, and 23.10 and all prior non-LTS are now EOL. Reverting to the previous LTS -FROM ubuntu:22.04 +FROM ubuntu:24.04 RUN apt-get update @@ -10,12 +10,17 @@ RUN apt-get update RUN apt-get install -y --no-install-recommends \ git \ sudo \ + ca-certificates \ python3 \ python-is-python3 \ opam \ rustc \ && apt-get clean -y +# Install the relevant Z3 versions. +COPY ./bin/get_fstar_z3.sh /usr/local/bin +RUN get_fstar_z3.sh /usr/local/bin + # Create a new user and give them sudo rights # NOTE: we give them the name "opam" to keep compatibility with # derived hierarchical CI @@ -28,18 +33,6 @@ ENV HOME /home/opam WORKDIR $HOME SHELL ["/bin/bash", "--login", "-c"] -# Install GitHub CLI -# From https://github.com/cli/cli/blob/trunk/docs/install_linux.md#debian-ubuntu-linux-raspberry-pi-os-apt -# This is only used by the workflow that makes a release and publishes -# it, but no harm in having it in the base. -RUN { type -p curl >/dev/null || sudo apt-get install curl -y ; } \ - && curl -fsSL https://cli.github.com/packages/githubcli-archive-keyring.gpg | sudo dd of=/usr/share/keyrings/githubcli-archive-keyring.gpg \ - && sudo chmod go+r /usr/share/keyrings/githubcli-archive-keyring.gpg \ - && echo "deb [arch=$(dpkg --print-architecture) signed-by=/usr/share/keyrings/githubcli-archive-keyring.gpg] https://cli.github.com/packages stable main" | sudo tee /etc/apt/sources.list.d/github-cli.list > /dev/null \ - && sudo apt-get update \ - && sudo apt-get install gh -y \ - && sudo apt-get clean - # Install OCaml ARG OCAML_VERSION=4.14.2 RUN opam init --compiler=$OCAML_VERSION --disable-sandboxing @@ -50,6 +43,7 @@ ENV OPAMYES=1 # F* dependencies. This is the only place where we read a file from # the F* repo. ADD fstar.opam $HOME/fstar.opam + RUN opam install --confirm-level=unsafe-yes --deps-only $HOME/fstar.opam && opam clean # Some karamel dependencies diff --git a/.nix/z3.nix b/.nix/z3.nix index aa697015bc8..deff193b7d5 100644 --- a/.nix/z3.nix +++ b/.nix/z3.nix @@ -1,11 +1,18 @@ -{ fetchFromGitHub, z3 }: +{ pkgs, stdenv, callPackage }: -z3.overrideAttrs (old: rec { - version = "4.8.5"; - src = fetchFromGitHub { - owner = "z3prover"; - repo = "z3"; - rev = "Z3-${version}"; - sha256 = "ytG5O9HczbIVJAiIGZfUXC/MuYH7d7yLApaeTRlKXoc="; - }; -}) +let + z3_4_8_5 = callPackage (import ./z3_4_8_5.nix) {}; + z3_4_13_3 = callPackage (import ./z3_4_13_3.nix) {}; +in +stdenv.mkDerivation { + pname = "fstar-z3"; + version = "1"; + + dontUnpack = true; + + buildPhase = '' + mkdir -p $out/bin + ln -s ${z3_4_8_5}/bin/z3 $out/bin/z3-4.8.5 + ln -s ${z3_4_13_3}/bin/z3 $out/bin/z3-4.13.3 + ''; +} diff --git a/.nix/z3_4_13_3.nix b/.nix/z3_4_13_3.nix new file mode 100644 index 00000000000..57b00805415 --- /dev/null +++ b/.nix/z3_4_13_3.nix @@ -0,0 +1,11 @@ +{ fetchFromGitHub, z3 }: + +z3.overrideAttrs (old: rec { + version = "4.13.3"; + src = fetchFromGitHub { + owner = "z3prover"; + repo = "z3"; + rev = "z3-${version}"; + sha256 = "sha256-odwalnF00SI+sJGHdIIv4KapFcfVVKiQ22HFhXYtSvA="; + }; +}) diff --git a/.nix/z3_4_8_5.nix b/.nix/z3_4_8_5.nix new file mode 100644 index 00000000000..aa697015bc8 --- /dev/null +++ b/.nix/z3_4_8_5.nix @@ -0,0 +1,11 @@ +{ fetchFromGitHub, z3 }: + +z3.overrideAttrs (old: rec { + version = "4.8.5"; + src = fetchFromGitHub { + owner = "z3prover"; + repo = "z3"; + rev = "Z3-${version}"; + sha256 = "ytG5O9HczbIVJAiIGZfUXC/MuYH7d7yLApaeTRlKXoc="; + }; +}) diff --git a/.scripts/query-stats-diff.ipynb b/.scripts/query-stats-diff.ipynb new file mode 100644 index 00000000000..fe25f44b87a --- /dev/null +++ b/.scripts/query-stats-diff.ipynb @@ -0,0 +1,249 @@ +{ + "cells": [ + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "# Customize these variables to match your environment\n", + "dump_file_v1 = (\"../dump1\", \"4.13.3\")\n", + "dump_file_v2 = (\"../dump2\", \"4.8.5\")" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "version1 = dump_file_v1[1]\n", + "version2 = dump_file_v2[1]" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "# parse lines of a file like this:\n", + "# (FStar.Seq.Properties.fsti(230,0-232,71)) Query-stats (FStar.Seq.Properties.lemma_ordering_hi_cons, 1) succeeded in 10 milliseconds with fuel 2 and ifuel 1 and rlimit 5\n", + "# and produce a dictionary with the following structure:\n", + "# { \"FStar.Seq.Properties.lemma_ordering_hi_cons, 1\" : { status:\"succeeded\" , \"time\" : 10, \"fuel\" : 2, \"ifuel\" : 1, \"rlimit\" : 5 } }\n", + "\n", + "import sys\n", + "import re\n", + "import json\n", + "\n", + "query_stats_re = re.compile(r'Query-stats \\(([^,]+, \\d+)\\)\\s+(succeeded|failed)( {[^}]+})?( \\(with hint\\))? in (\\d+) milliseconds with fuel (\\d+) and ifuel (\\d+) and rlimit (\\d+)')\n", + "splitting_query_stats = re.compile(r'Query-stats splitting query')\n", + "\n", + "def parse_line(line):\n", + " m = query_stats_re.search(line)\n", + " if m:\n", + " return { m.group(1) : { \"status\" : m.group(2), \"reason\":m.group(3), \"with_hint\":m.group(4), \"time\" : int(m.group(5)), \"fuel\" : int(m.group(6)), \"ifuel\" : int(m.group(7)), \"rlimit\" : int(m.group(8)) } }\n", + " else:\n", + " m = splitting_query_stats.search(line)\n", + " if m:\n", + " return None\n", + " else:\n", + " if \"Query-stats\" in line:\n", + " if \"{\\\"contents\\\":\" in line:\n", + " return None \n", + " print(\"Failed to parse line: \" + line)\n", + " return None" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "test_line=parse_line(\"(FStar.Seq.Properties.fsti(230,0-232,71)) Query-stats (FStar.Seq.Properties.lemma_ordering_hi_cons, 1) succeeded (with hint) in 10 milliseconds with fuel 2 and ifuel 1 and rlimit 5\")\n", + "if test_line:\n", + " print(\"Parsed line: \", test_line)\n", + " json.dumps(test_line)\n", + "else:\n", + " print(\"Failed to parse line\")" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "\n", + "def parse_file(file):\n", + " d = {}\n", + " print(\"opening file\", file)\n", + " with open(file, encoding='ISO-8859-1') as f:\n", + " for line in f:\n", + " # print(line)\n", + " r = parse_line(line)\n", + " if r:\n", + " d.update(r)\n", + " return d\n" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "z3_v1 = parse_file(dump_file_v1[0])\n", + "print(\"Parsed\", len(z3_v1), \"entries\")\n" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "z3_v2 = parse_file(dump_file_v2[0])\n", + "print(\"Parsed\", len(z3_v2), \"entries\")" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "# find entries in z3_v2 that are not in z3_v1\n", + "for k in z3_v2.keys():\n", + " if k not in z3_v1:\n", + " print(f\"Missing entry in {version1}: {k}\")\n", + "\n", + "# find entries in z3_v1 that are not in z3_v2\n", + "for k in z3_v1.keys():\n", + " if k not in z3_v2:\n", + " print(f\"Missing entry in {version2}: {k}\")" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "# for every entry in both dictionaries, create a new dictionary with the same key, the time fields of both dictionaries, and the difference between the times\n", + "diffs = {}\n", + "for k in z3_v1.keys():\n", + " if k in z3_v2.keys():\n", + " diffs[k] = { version1 : z3_v1[k][\"time\"], version2 : z3_v2[k][\"time\"], \"diff\" : z3_v2[k][\"time\"] - z3_v1[k][\"time\"] }\n", + "\n", + "print(f\"Found {len(diffs)} entries with both {version1} and {version2} times\")\n", + "json.dumps(diffs)" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "# sort the entries by the difference in time\n", + "sorted_diffs = sorted(diffs.items(), key=lambda x: x[1][\"diff\"], reverse=True)\n", + "\n", + "print(sorted_diffs)\n", + "#print the top 10\n", + "print(f\"Entries with the greatest speedups in {version1}:\")\n", + "for i in range(10):\n", + " print(sorted_diffs[i])\n", + "\n", + "print(f\"Entries with the greatest slowdowns in {version1}\")\n", + "# print the bottom 10\n", + "for i in range(10):\n", + " print(sorted_diffs[-(i + 1)])\n" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "# scatter plot with 485 times on x axis and 413 times on y axis\n", + "import matplotlib.pyplot as plt\n", + "import numpy as np\n", + "\n", + "# remove outliers\n", + "diffs = {k:v for k,v in sorted_diffs if abs(v[\"diff\"]) < 10000}\n", + "\n", + "x = [v[version2] for v in diffs.values()]\n", + "y = [v[version1] for v in diffs.values()]\n", + "\n", + "plt.scatter(x, y)\n", + "plt.xlabel(version2)\n", + "plt.ylabel(version1)\n", + "plt.show()\n" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "# linear regression of v1 times on v2 times\n", + "from scipy import stats\n", + "slope, intercept, r_value, p_value, std_err = stats.linregress(x, y)\n", + "print(\"slope:\", slope, \"intercept:\", intercept, \"r_value:\", r_value, \"p_value:\", p_value, \"std_err:\", std_err)\n", + "plt.plot(x, [slope * v + intercept for v in x])\n", + "plt.scatter(x, y)\n", + "plt.xlabel(version2)\n", + "plt.ylabel(version1)\n", + "plt.show()\n" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "# print all outliers\n", + "for k,v in sorted_diffs:\n", + " if abs(v[\"diff\"]) > 10000:\n", + " print(k, v)" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "# print all sorted diffs\n", + "for k,v in diffs.items():\n", + " print(k, v)" + ] + } + ], + "metadata": { + "kernelspec": { + "display_name": "Python 3", + "language": "python", + "name": "python3" + }, + "language_info": { + "codemirror_mode": { + "name": "ipython", + "version": 3 + }, + "file_extension": ".py", + "mimetype": "text/x-python", + "name": "python", + "nbconvert_exporter": "python", + "pygments_lexer": "ipython3", + "version": "3.12.3" + } + }, + "nbformat": 4, + "nbformat_minor": 2 +} diff --git a/FStar.fst.config.json b/FStar.fst.config.json index 9e7e90ab41d..6b87318bc39 100644 --- a/FStar.fst.config.json +++ b/FStar.fst.config.json @@ -2,11 +2,14 @@ "fstar_exe": "./bin/fstar.exe", "options": [ "--cache_dir", ".cache", - "--ext", "context_pruning" + "--ext", "context_pruning", + "--z3version", "4.13.3" ], "include_dirs": [ "ulib/", "ulib/experimental", - "ulib/legacy" + "ulib/legacy", + "examples/data_structures", + "examples/layeredeffects" ] } diff --git a/INSTALL.md b/INSTALL.md index e7d55c3ef92..638eb914c0f 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -28,6 +28,25 @@ using the [online F\* editor] that's part of the [F\* tutorial]. [online F\* editor]: https://www.fstar-lang.org/run.php [F\* tutorial]: https://www.fstar-lang.org/tutorial +## Runtime dependency: Particular version of Z3 ## + +F\* requires specific versions of Z3 to work correctly, +and will refuse to run if the version string does not match. +You should have `z3-4.8.5` and `z3-4.13.3` in your `$PATH`: + +``` +❯ z3-4.8.5 --version +Z3 version 4.8.5 - 64 bit + +❯ z3-4.13.3 --version +Z3 version 4.13.3 - 64 bit +``` + +On Linux you can install these two versions with the following command: +```bash +sudo ./bin/get_fstar_z3.sh /usr/local/bin +``` + ## OPAM package ## If the OCaml package manager (OPAM version 2.0 or later) is present on your platform, @@ -83,8 +102,8 @@ need to perform the following step before your first use: compiler=OCaml 4.14.0 date=yyyy-mm-ddThh:nn:ss+02:00 commit=xxxxxxxx - $ z3 --version - Z3 version 4.8.5 - 64 bit + $ z3-4.13.3 --version + Z3 version 4.13.3 - 64 bit Note: if you are using the binary package and extracted it to, say, the `/path/to/fstar` directory, then both `fstar.exe` and the right version of @@ -366,15 +385,3 @@ erase the extracted snapshot. $ make dune-extract-all -j6 ### Repeat [Step 1](#step-1-build-an-f-binary-from-ocaml-snapshot) - -## Runtime dependency: Particular version of Z3 ## - -To use F\* for verification you need a particular Z3 binary. -Our binary packages include that already in `bin`, but if you compile -F\* from sources you need to get the Z3 binary yourself and add it to -your `PATH`. We strongly recommend to use the corresponding binary here: -https://github.com/FStarLang/binaries/tree/master/z3-tested - -Other versions of Z3 may well work, but the F* tests, standard library, and -examples take a strong dependency on the particular Z3 binary above. -They will likely fail to verify with any other Z3 version. diff --git a/bin/get_fstar_z3.sh b/bin/get_fstar_z3.sh new file mode 100755 index 00000000000..acfd4b53b7f --- /dev/null +++ b/bin/get_fstar_z3.sh @@ -0,0 +1,78 @@ +#!/usr/bin/env bash +set -euo pipefail + +kernel="$(uname -s)" +case "$kernel" in + CYGWIN*) kernel=Windows ;; +esac + +arch="$(uname -m)" +case "$arch" in + arm64) arch=aarch64 ;; +esac + +declare -A release_url +release_url["Linux-x86_64-4.8.5"]="https://github.com/Z3Prover/z3/releases/download/Z3-4.8.5/z3-4.8.5-x64-ubuntu-16.04.zip" +release_url["Darwin-x86_64-4.8.5"]="https://github.com/Z3Prover/z3/releases/download/Z3-4.8.5/z3-4.8.5-x64-osx-10.14.2.zip" +release_url["Windows-x86_64-4.8.5"]="https://github.com/Z3Prover/z3/releases/download/Z3-4.8.5/z3-4.8.5-x64-win.zip" +release_url["Linux-x86_64-4.13.3"]="https://github.com/Z3Prover/z3/releases/download/z3-4.13.3/z3-4.13.3-x64-glibc-2.35.zip" +release_url["Linux-aarch64-4.13.3"]="https://github.com/Z3Prover/z3/releases/download/z3-4.13.3/z3-4.13.3-arm64-glibc-2.34.zip" +release_url["Darwin-x86_64-4.13.3"]="https://github.com/Z3Prover/z3/releases/download/z3-4.13.3/z3-4.13.3-x64-osx-13.7.zip" +release_url["Darwin-aarch64-4.13.3"]="https://github.com/Z3Prover/z3/releases/download/z3-4.13.3/z3-4.13.3-arm64-osx-13.7.zip" +release_url["Windows-x86_64-4.13.3"]="https://github.com/Z3Prover/z3/releases/download/z3-4.13.3/z3-4.13.3-x64-win.zip" + +trap "exit 1" HUP INT PIPE QUIT TERM +cleanup() { + if [ -n "${tmp_dir:-}" ]; then + rm -rf "$tmp_dir" + fi +} +trap "cleanup" EXIT + +download_z3() { + url="$1" + version="$2" + destination_file_name="$3" + + if [ -z "${tmp_dir:-}" ]; then + tmp_dir="$(mktemp -d --tmpdir get_fstar_z3.XXXXXXX)" + fi + + echo ">>> Downloading Z3 $version from $url ..." + base_name="$(basename "$url")" + + z3_path="${base_name%.zip}/bin/z3" + if [ "$kernel" = Windows ]; then z3_path="$z3_path.exe"; fi + + pushd "$tmp_dir" + curl -L "$url" -o "$base_name" + unzip "$base_name" "$z3_path" + popd + + install -m0755 "$tmp_dir/$z3_path" "$destination_file_name" + echo ">>> Installed Z3 $version to $destination_file_name" +} + +dest_dir="$1" +if [ -z "$dest_dir" ]; then + echo "Usage: get_fstar_z3.sh destination/directory/bin" + exit 1 +fi + +mkdir -p "$dest_dir" + +for z3_ver in 4.8.5 4.13.3; do + key="$kernel-$arch-$z3_ver" + url="${release_url[$key]:-}" + + destination_file_name="$dest_dir/z3-$z3_ver" + if [ "$kernel" = Windows ]; then destination_file_name="$destination_file_name.exe"; fi + + if [ -f "$destination_file_name" ]; then + echo ">>> Z3 $z3_ver already downloaded to $destination_file_name" + elif [ -z "$url" ]; then + echo ">>> Z3 $z3_ver not available for this architecture, skipping..." + else + download_z3 "$url" "$z3_ver" "$destination_file_name" + fi +done diff --git a/examples/data_structures/BinomialQueue.fst b/examples/data_structures/BinomialQueue.fst index 8d8665058e4..3268d583cb7 100644 --- a/examples/data_structures/BinomialQueue.fst +++ b/examples/data_structures/BinomialQueue.fst @@ -433,8 +433,10 @@ let rec compact_preserves_keys (q:forest) let insert_repr x q s = carry_repr 1 q (Internal Leaf x Leaf) s (ms_singleton x) +#push-options "--z3rlimit_factor 10" let merge_repr p q sp sq = join_repr 1 p q Leaf sp sq ms_empty +#pop-options /// Towards proof of delete correctness @@ -628,6 +630,7 @@ let rec find_max_is_max (d:pos) (kopt:option key_t) (q:forest) find_max_is_max (d + 1) (Some k) tl; find_max_some_is_some k tl +#push-options "--z3rlimit_factor 4" let delete_max_some_repr p pl k q ql = match find_max None p with | None -> () @@ -642,3 +645,4 @@ let delete_max_some_repr p pl k q ql = compact_preserves_keys r; assert (permutation pl (ms_append (ms_singleton k) ql)); find_max_is_max 1 None p +#pop-options \ No newline at end of file diff --git a/examples/dependencies/Makefile b/examples/dependencies/Makefile index 41f86add259..123f0c90c1b 100644 --- a/examples/dependencies/Makefile +++ b/examples/dependencies/Makefile @@ -21,7 +21,7 @@ ROOTS = Test.fst HINT_DIR = hints FSTAR_FLAGS = $(OTHERFLAGS) --cmi --odir $(OUT_DIR) --cache_dir $(CACHE_DIR) \ - --cache_checked_modules --already_cached 'Prims FStar' + --cache_checked_modules --already_cached 'Prims FStar' --z3version 4.13.3 # Run with ENABLE_HINTS= to disable ENABLE_HINTS ?= --use_hints diff --git a/examples/doublylinkedlist/DoublyLinkedList.fst b/examples/doublylinkedlist/DoublyLinkedList.fst index 55ae2f8a38b..b34fd763aeb 100644 --- a/examples/doublylinkedlist/DoublyLinkedList.fst +++ b/examples/doublylinkedlist/DoublyLinkedList.fst @@ -1905,7 +1905,7 @@ let dll_remove_node (#t:Type) (d:dll t) (e:pointer (node t)) : #reset-options -#set-options "--z3rlimit 10 --max_fuel 2 --max_ifuel 1" +#set-options "--z3rlimit 100 --max_fuel 2 --max_ifuel 1" let dll_append (#t:Type) (d1 d2:dll t) : StackInline (dll t) diff --git a/examples/doublylinkedlist/DoublyLinkedListIface.fst b/examples/doublylinkedlist/DoublyLinkedListIface.fst index 4ec0389dfad..a29d0047f76 100644 --- a/examples/doublylinkedlist/DoublyLinkedListIface.fst +++ b/examples/doublylinkedlist/DoublyLinkedListIface.fst @@ -563,8 +563,8 @@ let prev_node d n = /// code. The rest of this interface lets you talk about these /// operations easily. -#set-options "--z3rlimit 20 --max_fuel 2 --max_ifuel 1" - +#set-options "--z3rlimit 200 --max_fuel 2 --max_ifuel 1" +#restart-solver let dll_insert_at_head #t d n = let h00 = HST.get () in HST.push_frame (); @@ -580,8 +580,8 @@ let dll_insert_at_head #t d n = #reset-options -#set-options "--z3rlimit 40 --max_fuel 2 --max_ifuel 1" - +#set-options "--z3rlimit 400 --max_fuel 2 --max_ifuel 1" +#restart-solver let dll_insert_at_tail #t d n = let h00 = HST.get () in HST.push_frame (); diff --git a/examples/layeredeffects/AlgWP.fst b/examples/layeredeffects/AlgWP.fst index da85b2b1913..7c5e0862941 100644 --- a/examples/layeredeffects/AlgWP.fst +++ b/examples/layeredeffects/AlgWP.fst @@ -11,6 +11,7 @@ module FE = FStar.FunctionalExtensionality module F = FStar.FunctionalExtensionality module W = FStar.WellFounded module T = FStar.Tactics.V2 +// #show-options module ID5 = ID5 open Alg @@ -137,7 +138,7 @@ let elim_str #a (w1 w2 : st_wp a) (p : (a & state -> Type0)) (s0:state) (* Takes a while, known to fail sporadically *) #restart-solver -#push-options "--retry 10 --z3rlimit_factor 2" +#push-options "--z3rlimit_factor 4 --retry 10" let rec interp_morph #a #b #l1 #l2 (c : rwtree a l1) (f : a -> rwtree b l2) (p:_) (s0:_) : Lemma (interp_as_wp c s0 (fun (y, s1) -> interp_as_wp (f y) s1 p) == interp_as_wp (tbind #_ #_ #l1 #l2 c f) s0 p) @@ -402,4 +403,4 @@ let handle_into_ro #a (#l:rwops{~(List.Tot.memP Write l)}) #wp (f : unit -> AlgW let ignore_writes #a (#l:rwops{~(List.Tot.memP Write l)}) #pre #post (f : unit -> AlgPP a (Write::l) pre post) : AlgPP a l pre (fun h0 x h1 -> h0 == h1) - = handle_into_ro #a #l #(fun h0 p -> pre h0 /\ (forall y h1. post h0 y h1 ==> p (y, h1))) f + = handle_into_ro #a #l #(fun h0 p -> pre h0 /\ (forall y h1. post h0 y h1 ==> p (y, h1))) f \ No newline at end of file diff --git a/examples/native_tactics/Makefile b/examples/native_tactics/Makefile index 8aa9f6188f6..876708dbb90 100644 --- a/examples/native_tactics/Makefile +++ b/examples/native_tactics/Makefile @@ -5,7 +5,9 @@ # 'include test.mk'. FSTAR_HOME=../.. -FSTAR_EXE ?= $(FSTAR_HOME)/bin/fstar.exe $(OTHERFLAGS) +OTHERFLAGS += --z3version 4.13.3 +FSTAR_EXE ?= $(FSTAR_HOME)/bin/fstar.exe +MY_FSTAR_EXE=$(FSTAR_EXE) $(OTHERFLAGS) # Tests for which the native tactics used in module named Sample.Test.fst are # declared in a corresponding module named Sample.fst @@ -43,8 +45,6 @@ ALL=Apply\ Tutorial\ Unify -OTHERFLAGS += - all: $(addsuffix .sep.test, $(TAC_MODULES)) $(addsuffix .test, $(ALL)) # .depend: @@ -56,25 +56,25 @@ all: $(addsuffix .sep.test, $(TAC_MODULES)) $(addsuffix .test, $(ALL)) .PRECIOUS: %.ml %.test: %.fst %.ml - $(FSTAR_EXE) $*.fst --load $* + $(MY_FSTAR_EXE) $*.fst --load $* touch $@ %.sep.test: %.fst %.ml - $(FSTAR_EXE) $*.Test.fst --load $* + $(MY_FSTAR_EXE) $*.Test.fst --load $* touch $@ %.ml: %.fst - $(FSTAR_EXE) $*.fst --cache_checked_modules --codegen Plugin --extract $* + $(MY_FSTAR_EXE) $*.fst --cache_checked_modules --codegen Plugin --extract $* touch $@ %.clean: rm -f Registers_List.ml Registers.List.ml Registers_List.cmxs %.native: %.fst Registers.List.ml - $(FSTAR_EXE) $*.fst --load Registers.List --warn_error -266 + $(MY_FSTAR_EXE) $*.fst --load Registers.List --warn_error -266 %.interp: %.fst Registers.List.fst - $(FSTAR_EXE) $*.fst + $(MY_FSTAR_EXE) $*.fst clean: diff --git a/fstar.opam b/fstar.opam index 0f63821dfa8..9e99503d32f 100644 --- a/fstar.opam +++ b/fstar.opam @@ -21,11 +21,10 @@ depends: [ "process" "ppx_deriving" {build} "ppx_deriving_yojson" {build} - "z3" {= "4.8.5-1"} ] depexts: ["coreutils"] {os = "macos" & os-distribution = "homebrew"} build: [ - [make "PREFIX=%{prefix}%" "-j" jobs] + [make "PREFIX=%{prefix}%" "-j" jobs "ADMIT=1"] ] install: [ [make "PREFIX=%{prefix}%" "install"] diff --git a/mk/test.mk b/mk/test.mk index 0c8c8f516c7..2db05dcbb76 100644 --- a/mk/test.mk +++ b/mk/test.mk @@ -32,6 +32,7 @@ HINTS_ENABLED?=--use_hints # This warning is really useless. OTHERFLAGS += --warn_error -321 OTHERFLAGS += --ext context_pruning +OTHERFLAGS += --z3version 4.13.3 # Set ADMIT=1 to admit queries ADMIT ?= diff --git a/tests/Cfg.fst.config.json b/tests/Cfg.fst.config.json index 33824b76ec5..449ae58473d 100644 --- a/tests/Cfg.fst.config.json +++ b/tests/Cfg.fst.config.json @@ -1,7 +1,8 @@ { "fstar_exe": "../bin/fstar.exe", "options": [ - "--ext", "context_pruning" + "--ext", "context_pruning", + "--z3version", "4.13.3" ], "include_dirs": [ ] diff --git a/tests/bug-reports/closed/Bug312.fst b/tests/bug-reports/closed/Bug312.fst index 0cd3a69d76c..1c80d10f444 100644 --- a/tests/bug-reports/closed/Bug312.fst +++ b/tests/bug-reports/closed/Bug312.fst @@ -53,8 +53,7 @@ assume val sample : //#a:Type -> #b:Type irreducible val triple_a : s:double int -> Tot (r:(h:double int & shared h) {(R?.l s) - (snd(R?.l(dsnd r))) = (R?.r s) - (snd(R?.r(dsnd r)))}) - -[@@expect_failure [19]] + let triple_a s = let sample_fun = (fun x -> (x - (R?.l s)) + (R?.r s)) in cut (inverses (fun x -> x) (fun x -> x)); lemma_inverses_bij (fun x -> x) (fun x -> x); diff --git a/tests/dune_hello/Makefile b/tests/dune_hello/Makefile index 99e2277ff37..9814d8bcd8d 100644 --- a/tests/dune_hello/Makefile +++ b/tests/dune_hello/Makefile @@ -4,7 +4,7 @@ FSTAR_EXE ?= ../../bin/fstar.exe all: run Hello.ml: Hello.fst - $(FSTAR_EXE) --codegen OCaml Hello.fst --extract Hello + $(FSTAR_EXE) --codegen OCaml Hello.fst --extract Hello --z3version 4.13.3 bin/hello.exe: Hello.ml $(FSTAR_EXE) --ocamlenv dune build @install --profile=release diff --git a/tests/ide/test-incremental.py b/tests/ide/test-incremental.py index 31b6a4ea44c..7716ab92af1 100644 --- a/tests/ide/test-incremental.py +++ b/tests/ide/test-incremental.py @@ -101,6 +101,8 @@ def check_one_fragment(file_lines, json_objects, from_line): # A function to validate the response from F* interactive mode def validate_response(response, file_contents): file_lines = file_contents.splitlines() + # print(f"Validating response") + # print(f"Response: {response}") # parse the each line of the response into a JSON object # if the line is not valid JSON, print an error message and exit # store the JSON objects in a list @@ -253,7 +255,7 @@ def test_file(filepath): # print the request to the console for debugging # print(request) # Run fstar on the file with the request as stdin - p = subprocess.run([fstar, "--admit_smt_queries", "true", "--ide", file], input=request, encoding="utf-8", stdout=subprocess.PIPE, stderr=subprocess.PIPE) + p = subprocess.run([fstar, "--z3version", "4.13.3", "--admit_smt_queries", "true", "--ide", file], input=request, encoding="utf-8", stdout=subprocess.PIPE, stderr=subprocess.PIPE) # Read the response from stdout response = p.stdout # Print the response to the console for debugging diff --git a/tests/incl/Makefile b/tests/incl/Makefile index 64650b053ec..07e8d5e2aac 100644 --- a/tests/incl/Makefile +++ b/tests/incl/Makefile @@ -1,7 +1,7 @@ # Test the 'include' functionality # Do not warn about missing checked files in these tests. -OTHERFLAGS += --warn_error -241 +OTHERFLAGS += --warn_error -241 --z3version 4.13.3 POSTESTS=$(wildcard *.pos) POSTARGETS=$(addsuffix .pver,$(POSTESTS)) diff --git a/tests/micro-benchmarks/Test.Real.fst b/tests/micro-benchmarks/Test.Real.fst index 4834dbd1ffd..6ad59d281ca 100644 --- a/tests/micro-benchmarks/Test.Real.fst +++ b/tests/micro-benchmarks/Test.Real.fst @@ -37,7 +37,6 @@ let test_div_lt = assert (8.0R /. 2.0R <. 5.0R) let test_sqrt_2_mul = assert (sqrt_2 *. sqrt_2 == 2.0R) -[@@expect_failure] // should hopefully work... let test_sqrt_2_add = assert (sqrt_2 >. 1.0R) let test_sqrt_2_add_explicit = diff --git a/tests/simple_hello/Makefile b/tests/simple_hello/Makefile index 15e53f42015..a4fc6e90bd5 100644 --- a/tests/simple_hello/Makefile +++ b/tests/simple_hello/Makefile @@ -11,7 +11,7 @@ Hello.test: Hello.exe Hello.byte ./Hello.byte | grep "Hello F\*!" %.ml: %.fst - $(FSTAR) --codegen OCaml $< --extract $* + $(FSTAR) --codegen OCaml $< --extract $* --z3version 4.13.3 %.exe: %.ml $(FSTAR) --ocamlopt $< -o $@ diff --git a/tests/vale/Makefile b/tests/vale/Makefile index 42b7133b12a..e19fdb95268 100644 --- a/tests/vale/Makefile +++ b/tests/vale/Makefile @@ -2,15 +2,13 @@ FSTAR_FILES=$(wildcard *.fst) FSTAR_FILES:=$(filter-out X64.Poly1305.fst,$(FSTAR_FILES)) OTHERFLAGS += \ ---z3cliopt smt.QI.EAGER_THRESHOLD=100 \ ---z3cliopt smt.CASE_SPLIT=3 \ ---z3cliopt smt.arith.nl=false \ +--z3smtopt '(set-option :smt.qi.eager_threshold 100)' \ +--z3smtopt '(set-option :smt.arith.nl false)' \ --smtencoding.elim_box true \ --smtencoding.l_arith_repr native \ --smtencoding.nl_arith_repr wrapped\ --max_fuel 1 \ --max_ifuel 1 \ ---initial_ifuel 0 \ --warn_error -350 # ^ 350: deprecated lightweight do notation diff --git a/tests/vale/ValeTest.fst.config.json b/tests/vale/ValeTest.fst.config.json index fd4218b2d38..bcdf0260498 100644 --- a/tests/vale/ValeTest.fst.config.json +++ b/tests/vale/ValeTest.fst.config.json @@ -2,7 +2,17 @@ "fstar_exe": "fstar.exe", "options": [ "--cache_dir", ".cache", - "--ext", "context_pruning" + "--ext", "context_pruning", + "--z3version", "4.13.3", + "--z3smtopt", "(set-option :smt.qi.eager_threshold 100)", + "--z3smtopt", "(set-option :smt.arith.nl false)", + "--smtencoding.elim_box", "true", + "--smtencoding.l_arith_repr", "native", + "--smtencoding.nl_arith_repr", "wrapped", + "--max_fuel", "1", + "--max_ifuel", "1", + "--initial_ifuel", "0", + "--warn_error", "-350" ], "include_dirs": [ "../../ulib/", diff --git a/tests/vale/X64.Vale.Decls.fst b/tests/vale/X64.Vale.Decls.fst index 6fa0bc2b476..5ce333515a5 100644 --- a/tests/vale/X64.Vale.Decls.fst +++ b/tests/vale/X64.Vale.Decls.fst @@ -22,10 +22,9 @@ open FStar.UInt module S = X64.Semantics_s module P = X64.Print_s -#reset-options "--z3cliopt smt.arith.nl=true --using_facts_from Prims --using_facts_from FStar.Math" +#reset-options "--z3smtopt '(set-option :smt.arith.nl true)' --using_facts_from Prims --using_facts_from FStar.Math" let lemma_mul_nat (x:nat) (y:nat) : Lemma (ensures 0 <= (x `op_Multiply` y)) = () -#reset-options "--initial_fuel 2 --max_fuel 2" - +#reset-options "--initial_fuel 2 --max_fuel 2 --initial_ifuel 1 --z3rlimit_factor 10 --retry 5 --query_stats" let cf = Lemmas_i.cf let ins = S.ins type ocmp = S.ocmp @@ -86,7 +85,39 @@ let print_footer = P.print_footer let masm = P.masm let gcc = P.gcc -#set-options "--initial_fuel 2 --max_fuel 2 --z3rlimit 20" +let dst_of_ins (c:S.ins { not (S.Mul64? c) }) : dst_op = + let open S in + match c with + | Mov64 dst _ + | Add64 dst _ + | AddLea64 dst _ _ + | AddCarry64 dst _ + | Sub64 dst _ + | IMul64 dst _ + | Xor64 dst _ + | And64 dst _ + | Shr64 dst _ + | Shl64 dst _ -> dst + +let regs_eval_code_one (c:va_code{ Ins? c }) (dst:dst_op) (va_s0:va_state) (va_sM:va_state) +: Lemma + (requires ( + let Ins cc = c in + not (S.Mul64? cc) /\ + dst_of_ins cc == dst /\ + eval_code c va_s0 va_sM)) + (ensures ( + let Ins cc = c in + Regs_i.equal va_sM.regs (va_update_dst_operand dst va_sM va_s0).regs /\ + va_eval_dst_operand_uint64 va_sM dst == + UInt64.v (S.eval_operand dst (snd (S.eval_ins cc (state_to_S va_s0)))))) += eliminate exists fuel. + Some <| state_to_S va_sM == S.eval_code c fuel (state_to_S va_s0) + returns + Regs_i.equal va_sM.regs (va_update_dst_operand dst va_sM va_s0).regs + with _. ( + () + ) val va_transparent_code_Mov64 : dst:va_dst_operand -> src:va_operand -> Tot va_code let va_transparent_code_Mov64 dst src = @@ -107,6 +138,8 @@ irreducible let va_irreducible_lemma_Mov64 va_b0 va_s0 va_sN dst src = (va_reveal_opaque (va_transparent_code_Mov64 dst src)); let (va_old_s:va_state) = va_s0 in let (va_sM, (va_cM:va_code), va_bM) = (va_lemma_block va_b0 va_s0 va_sN) in + regs_eval_code_one (va_transparent_code_Mov64 dst src) dst va_s0 va_sM; + assert (Regs_i.equal va_sM.regs (va_update_dst_operand dst va_sM va_s0).regs); (va_bM, va_sM) let va_lemma_Mov64 = va_irreducible_lemma_Mov64 @@ -128,10 +161,12 @@ irreducible val va_irreducible_lemma_Load64 : va_b0:va_codes -> va_s0:va_state - /\ (va_get_ok va_sM) /\ (va_eval_dst_operand_uint64 va_sM dst) == (va_subscript (va_get_mem va_sM) ((va_eval_reg_operand_uint64 va_s0 src) + offset)) /\ (va_state_eq va_sM (va_update_ok va_sM (va_update_dst_operand dst va_sM va_s0)))))) + irreducible let va_irreducible_lemma_Load64 va_b0 va_s0 va_sN dst src offset = (va_reveal_opaque (va_transparent_code_Load64 dst src offset)); let (va_old_s:va_state) = va_s0 in let (va_sM, (va_cM:va_code), va_bM) = (va_lemma_block va_b0 va_s0 va_sN) in + regs_eval_code_one (va_transparent_code_Load64 dst src offset) dst va_s0 va_sM; (va_bM, va_sM) let va_lemma_Load64 = va_irreducible_lemma_Load64 @@ -166,7 +201,6 @@ let va_transparent_code_Add64 dst src = (Ins (S.Add64 dst src)) let va_code_Add64 dst src = (va_make_opaque (va_transparent_code_Add64 dst src)) - irreducible val va_irreducible_lemma_Add64 : va_b0:va_codes -> va_s0:va_state -> va_sN:va_state -> dst:va_dst_operand -> src:va_operand -> Ghost (va_codes & va_state) @@ -178,10 +212,12 @@ irreducible val va_irreducible_lemma_Add64 : va_b0:va_codes -> va_s0:va_state -> /\ (va_get_ok va_sM) /\ (eq_int (va_eval_dst_operand_uint64 va_sM dst) ((va_eval_dst_operand_uint64 va_s0 dst) + (va_eval_operand_uint64 va_s0 src))) /\ (va_state_eq va_sM (va_update_flags va_sM (va_update_ok va_sM (va_update_dst_operand dst va_sM va_s0))))))) + irreducible let va_irreducible_lemma_Add64 va_b0 va_s0 va_sN dst src = (va_reveal_opaque (va_transparent_code_Add64 dst src)); let (va_old_s:va_state) = va_s0 in let (va_sM, (va_cM:va_code), va_bM) = (va_lemma_block va_b0 va_s0 va_sN) in + regs_eval_code_one(va_transparent_code_Add64 dst src) dst va_s0 va_sM; (va_bM, va_sM) let va_lemma_Add64 = va_irreducible_lemma_Add64 @@ -192,21 +228,34 @@ let va_code_Add64Wrap dst src = (va_make_opaque (va_transparent_code_Add64Wrap dst src)) irreducible val va_irreducible_lemma_Add64Wrap : va_b0:va_codes -> va_s0:va_state -> va_sN:va_state - -> dst:va_dst_operand -> src:va_operand - -> Ghost (va_codes & va_state) + -> dst:va_dst_operand -> src:va_operand -> + Ghost (va_codes & va_state) (requires ((va_require va_b0 (va_code_Add64Wrap dst src) va_s0 va_sN) /\ (va_is_dst_dst_operand_uint64 dst va_s0) /\ (va_is_src_operand_uint64 src va_s0) /\ (va_get_ok va_s0))) - (ensures (fun ((va_bM:va_codes), (va_sM:va_state)) -> ((va_ensure va_b0 va_bM va_s0 va_sM va_sN) + (ensures (fun ((va_bM:va_codes), (va_sM:va_state)) -> + ((va_ensure va_b0 va_bM va_s0 va_sM va_sN) /\ (va_get_ok va_sM) /\ (va_eval_dst_operand_uint64 va_sM dst) == (add_wrap (va_eval_dst_operand_uint64 va_s0 dst) (va_eval_operand_uint64 va_s0 src)) /\ (cf (va_get_flags va_sM)) == ((va_eval_dst_operand_uint64 va_s0 dst) + (va_eval_operand_uint64 va_s0 src) >= nat64_max) /\ (va_state_eq va_sM (va_update_flags va_sM (va_update_ok va_sM (va_update_dst_operand dst va_sM va_s0))))))) + +let add_wrap_lemma (x y:UInt64.t) +: Lemma + (ensures add_wrap (UInt64.v x) (UInt64.v y) == UInt64.v (S.add_mod64 x y)) + [SMTPat (S.add_mod64 x y)] += () irreducible let va_irreducible_lemma_Add64Wrap va_b0 va_s0 va_sN dst src = (va_reveal_opaque (va_transparent_code_Add64Wrap dst src)); let (va_old_s:va_state) = va_s0 in let (va_sM, (va_cM:va_code), va_bM) = (va_lemma_block va_b0 va_s0 va_sN) in + regs_eval_code_one (va_transparent_code_Add64Wrap dst src) dst va_s0 va_sM; + assert (Regs_i.equal va_sM.regs (va_update_dst_operand dst va_sM va_s0).regs); + assert ( + (va_eval_dst_operand_uint64 va_sM dst) == (add_wrap + (va_eval_dst_operand_uint64 va_s0 dst) (va_eval_operand_uint64 va_s0 src)) + ); (va_bM, va_sM) let va_lemma_Add64Wrap = va_irreducible_lemma_Add64Wrap @@ -232,6 +281,8 @@ irreducible let va_irreducible_lemma_AddLea64 va_b0 va_s0 va_sN dst src1 src2 = (va_reveal_opaque (va_transparent_code_AddLea64 dst src1 src2)); let (va_old_s:va_state) = va_s0 in let (va_sM, (va_cM:va_code), va_bM) = (va_lemma_block va_b0 va_s0 va_sN) in + regs_eval_code_one (va_transparent_code_AddLea64 dst src1 src2) dst va_s0 va_sM; + assert (Regs_i.equal va_sM.regs (va_update_dst_operand dst va_sM va_s0).regs); (va_bM, va_sM) let va_lemma_AddLea64 = va_irreducible_lemma_AddLea64 @@ -254,10 +305,23 @@ irreducible val va_irreducible_lemma_Adc64Wrap : va_b0:va_codes -> va_s0:va_stat ((va_eval_dst_operand_uint64 va_s0 dst) + (va_eval_operand_uint64 va_s0 src) + (if (cf (va_get_flags va_s0)) then 1 else 0) >= nat64_max) /\ (va_state_eq va_sM (va_update_flags va_sM (va_update_ok va_sM (va_update_dst_operand dst va_sM va_s0))))))) + irreducible let va_irreducible_lemma_Adc64Wrap va_b0 va_s0 va_sN dst src = (va_reveal_opaque (va_transparent_code_Adc64Wrap dst src)); let (va_old_s:va_state) = va_s0 in let (va_sM, (va_cM:va_code), va_bM) = (va_lemma_block va_b0 va_s0 va_sN) in + regs_eval_code_one (va_transparent_code_Adc64Wrap dst src) dst va_s0 va_sM; + assert_spinoff ( + (va_eval_dst_operand_uint64 va_sM dst) == (add_wrap (add_wrap + (va_eval_dst_operand_uint64 va_s0 dst) (va_eval_operand_uint64 va_s0 src)) (if (cf + (va_get_flags va_s0)) then 1 else 0)) /\ (cf (va_get_flags va_sM)) == + ((va_eval_dst_operand_uint64 va_s0 dst) + (va_eval_operand_uint64 va_s0 src) + (if (cf + (va_get_flags va_s0)) then 1 else 0) >= nat64_max) + ); + assert_spinoff ( + (va_state_eq va_sM (va_update_flags va_sM + (va_update_ok va_sM (va_update_dst_operand dst va_sM va_s0)))) + ); (va_bM, va_sM) let va_lemma_Adc64Wrap = va_irreducible_lemma_Adc64Wrap @@ -281,6 +345,11 @@ irreducible let va_irreducible_lemma_Sub64 va_b0 va_s0 va_sN dst src = (va_reveal_opaque (va_transparent_code_Sub64 dst src)); let (va_old_s:va_state) = va_s0 in let (va_sM, (va_cM:va_code), va_bM) = (va_lemma_block va_b0 va_s0 va_sN) in + regs_eval_code_one (va_transparent_code_Sub64 dst src) dst va_s0 va_sM; + assert_spinoff ( + (eq_int (va_eval_dst_operand_uint64 va_sM dst) + ((va_eval_dst_operand_uint64 va_s0 dst) - (va_eval_operand_uint64 va_s0 src))) + ); (va_bM, va_sM) let va_lemma_Sub64 = va_irreducible_lemma_Sub64 @@ -304,6 +373,7 @@ irreducible let va_irreducible_lemma_Sub64Wrap va_b0 va_s0 va_sN dst src = (va_reveal_opaque (va_transparent_code_Sub64Wrap dst src)); let (va_old_s:va_state) = va_s0 in let (va_sM, (va_cM:va_code), va_bM) = (va_lemma_block va_b0 va_s0 va_sN) in + regs_eval_code_one (va_transparent_code_Sub64Wrap dst src) dst va_s0 va_sM; (va_bM, va_sM) let va_lemma_Sub64Wrap = va_irreducible_lemma_Sub64Wrap @@ -323,10 +393,32 @@ irreducible val va_irreducible_lemma_Mul64Wrap : va_b0:va_codes -> va_s0:va_stat == (va_get_reg Rax va_s0) `op_Multiply` (va_eval_operand_uint64 va_s0 src) /\ (va_state_eq va_sM (va_update_reg Rdx va_sM (va_update_reg Rax va_sM (va_update_flags va_sM (va_update_ok va_sM va_s0)))))))) + +let regs_eval_code_mul64 (c:va_code{ Ins? c }) (va_s0:va_state) (va_sM:va_state) +: Lemma + (requires ( + let Ins cc = c in + S.Mul64? cc /\ + eval_code c va_s0 va_sM)) + (ensures ( + Regs_i.equal va_sM.regs (va_update_reg Rdx va_sM (va_update_reg Rax va_sM va_s0)).regs)) += eliminate exists fuel. + Some <| state_to_S va_sM == S.eval_code c fuel (state_to_S va_s0) + returns + Regs_i.equal va_sM.regs (va_update_reg Rdx va_sM (va_update_reg Rax va_sM va_s0)).regs + with _. ( + () + ) + irreducible let va_irreducible_lemma_Mul64Wrap va_b0 va_s0 va_sN src = (va_reveal_opaque (va_transparent_code_Mul64Wrap src)); let (va_old_s:va_state) = va_s0 in let (va_sM, (va_cM:va_code), va_bM) = (va_lemma_block va_b0 va_s0 va_sN) in + regs_eval_code_mul64 (va_transparent_code_Mul64Wrap src) va_s0 va_sM; + assert ( + nat64_max `op_Multiply` (va_get_reg Rdx va_sM) + (va_get_reg Rax va_sM) + == (va_get_reg Rax va_s0) `op_Multiply` (va_eval_operand_uint64 va_s0 src) + ); (va_bM, va_sM) let va_lemma_Mul64Wrap = va_irreducible_lemma_Mul64Wrap @@ -348,10 +440,12 @@ irreducible val va_irreducible_lemma_IMul64 : va_b0:va_codes -> va_s0:va_state - ((va_eval_dst_operand_uint64 va_s0 dst) `op_Multiply` (va_eval_operand_uint64 va_s0 src))) /\ (va_state_eq va_sM (va_update_flags va_sM (va_update_ok va_sM (va_update_dst_operand dst va_sM va_s0))))))) +#restart-solver irreducible let va_irreducible_lemma_IMul64 va_b0 va_s0 va_sN dst src = (va_reveal_opaque (va_transparent_code_IMul64 dst src)); let (va_old_s:va_state) = va_s0 in let (va_sM, (va_cM:va_code), va_bM) = (va_lemma_block va_b0 va_s0 va_sN) in + regs_eval_code_one (va_transparent_code_IMul64 dst src) dst va_s0 va_sM; (lemma_mul_nat (va_eval_dst_operand_uint64 va_old_s dst) (va_eval_operand_uint64 va_old_s src)); (va_bM, va_sM) let va_lemma_IMul64 = va_irreducible_lemma_IMul64 @@ -376,6 +470,7 @@ irreducible let va_irreducible_lemma_Xor64 va_b0 va_s0 va_sN dst src = (va_reveal_opaque (va_transparent_code_Xor64 dst src)); let (va_old_s:va_state) = va_s0 in let (va_sM, (va_cM:va_code), va_bM) = (va_lemma_block va_b0 va_s0 va_sN) in + regs_eval_code_one (va_transparent_code_Xor64 dst src) dst va_s0 va_sM; (va_bM, va_sM) let va_lemma_Xor64 = va_irreducible_lemma_Xor64 @@ -422,6 +517,7 @@ irreducible let va_irreducible_lemma_Shl64 va_b0 va_s0 va_sN dst amt = (va_reveal_opaque (va_transparent_code_Shl64 dst amt)); let (va_old_s:va_state) = va_s0 in let (va_sM, (va_cM:va_code), va_bM) = (va_lemma_block va_b0 va_s0 va_sN) in + regs_eval_code_one (va_transparent_code_Shl64 dst amt) dst va_s0 va_sM; (va_bM, va_sM) let va_lemma_Shl64 = va_irreducible_lemma_Shl64 @@ -445,5 +541,6 @@ irreducible let va_irreducible_lemma_Shr64 va_b0 va_s0 va_sN dst amt = (va_reveal_opaque (va_transparent_code_Shr64 dst amt)); let (va_old_s:va_state) = va_s0 in let (va_sM, (va_cM:va_code), va_bM) = (va_lemma_block va_b0 va_s0 va_sN) in + regs_eval_code_one (va_transparent_code_Shr64 dst amt) dst va_s0 va_sM; (va_bM, va_sM) let va_lemma_Shr64 = va_irreducible_lemma_Shr64 diff --git a/ulib/FStar.UInt128.fst b/ulib/FStar.UInt128.fst index 444ce8b0882..c4cb549d4f0 100644 --- a/ulib/FStar.UInt128.fst +++ b/ulib/FStar.UInt128.fst @@ -588,10 +588,13 @@ val add_mod_small: n: nat -> m:nat -> k1:pos -> k2:pos -> Lemma (requires (n < k1)) (ensures (n + (k1 * m) % (k1 * k2) == (n + k1 * m) % (k1 * k2))) +#restart-solver +#push-options "--z3rlimit_factor 4" let add_mod_small n m k1 k2 = mod_spec (k1 * m) (k1 * k2); mod_spec (n + k1 * m) (k1 * k2); div_add_small n m k1 k2 +#pop-options let mod_then_mul_64 (n:nat) : Lemma (n % pow2 64 * pow2 64 == n * pow2 64 % pow2 128) = Math.pow2_plus 64 64; diff --git a/ulib/Makefile.extract b/ulib/Makefile.extract index a469d2611b6..2c7b79f7292 100644 --- a/ulib/Makefile.extract +++ b/ulib/Makefile.extract @@ -15,6 +15,8 @@ FSTAR_FILES+=$(wildcard *.fst *.fsti) FSTAR_FILES+=$(wildcard experimental/*.fst experimental/*.fsti) FSTAR_FILES:=$(filter-out $(NOEXTRACT_FILES), $(FSTAR_FILES)) +OTHERFLAGS += --z3version 4.13.3 + CODEGEN = Plugin MY_FSTAR=$(RUNLIM) $(FSTAR) $(SIL) $(OTHERFLAGS) --cache_checked_modules --odir $(OUTPUT_DIRECTORY) --cache_dir .cache --warn_error @241 EXTRACT_MODULES=--extract '* $(NOEXTRACT_MODULES)' diff --git a/ulib/Makefile.extract.fsharp b/ulib/Makefile.extract.fsharp index 8aead6591e9..ed51ebc7ee0 100644 --- a/ulib/Makefile.extract.fsharp +++ b/ulib/Makefile.extract.fsharp @@ -26,6 +26,8 @@ OUTPUT_DIRECTORY=fs/extracted CODEGEN ?= FSharp +OTHERFLAGS += --z3version 4.13.3 + MY_FSTAR=$(FSTAR) $(OTHERFLAGS) --warn_error @241 --cache_checked_modules --odir $(OUTPUT_DIRECTORY) --cache_dir .cache # And then, in a separate invocation, from each .checked file we diff --git a/ulib/Makefile.verify b/ulib/Makefile.verify index d45a978faf2..9f8c2a12667 100644 --- a/ulib/Makefile.verify +++ b/ulib/Makefile.verify @@ -34,6 +34,7 @@ WITH_CACHE_DIR=--cache_dir .cache --hint_dir .hints # 330 -> experimental feature # 247 -> did not write checked file OTHERFLAGS+=--warn_error @271-330@247 --ext context_pruning +OTHERFLAGS += --z3version 4.13.3 include $(FSTAR_HOME)/.common.mk include gmake/z3.mk diff --git a/ulib/gmake/fstar.mk b/ulib/gmake/fstar.mk index 71dc04ca735..9e167be180a 100644 --- a/ulib/gmake/fstar.mk +++ b/ulib/gmake/fstar.mk @@ -1,7 +1,7 @@ HINTS_ENABLED?=--use_hints WARN_ERROR= OTHERFLAGS+=$(WARN_ERROR) - +OTHERFLAGS+=--z3version 4.13.3 ifdef Z3 OTHERFLAGS+=--smt $(Z3) endif