Bump to Z3 4.16.0

.github/workflows/ci.yml

@@ -30,6 +30,9 @@ jobs:
           path: FStar
           submodules: true
 
+      - name: Install Z3 from script
+        run: sudo ./FStar/.scripts/get_fstar_z3.sh /usr/local/bin
+
       - name: Run CI
         run: make -skj$(nproc) ci
         working-directory: FStar

.github/workflows/nightly-ci.yml

@@ -34,7 +34,7 @@ jobs:
       # don't include Z3.
       - uses: cda-tum/setup-z3@main
         with:
-          version: 4.13.3
+          version: 4.16.0
 
       - run: tar xzf fstar.tar.gz
 
@@ -59,7 +59,7 @@ jobs:
     steps:
       - uses: cda-tum/setup-z3@main
         with:
-          version: 4.13.3
+          version: 4.16.0
 
       - name: Get fstar package
         uses: actions/download-artifact@v8

.nix/z3.nix

@@ -4,6 +4,7 @@ let
   z3_4_8_5 = callPackage (import ./z3_4_8_5.nix) { };
   z3_4_13_3 = callPackage (import ./z3_4_13_3.nix) { };
   z3_4_15_3 = callPackage (import ./z3_4_15_3.nix) { };
+  z3_4_16_0 = callPackage (import ./z3_4_16_0.nix) { };
 in
 stdenv.mkDerivation {
   pname = "fstar-z3";
@@ -13,8 +14,8 @@ stdenv.mkDerivation {
 
   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
     ln -s ${z3_4_15_3}/bin/z3 $out/bin/z3-4.15.3
+    ln -s ${z3_4_16_0}/bin/z3 $out/bin/z3-4.16.0
   '';
 }

.nix/z3_4_16_0.nix

@@ -0,0 +1,11 @@
+{ fetchFromGitHub, z3 }:
+
+z3.overrideAttrs (old: rec {
+  version = "4.16.0";
+  src = fetchFromGitHub {
+    owner = "z3prover";
+    repo = "z3";
+    rev = "z3-${version}";
+    sha256 = "sha256-DnhX3kxggnFmyYwXEPBsBA1rh4oor1oIJR5TMJk/jvc=";
+  };
+})

.scripts/get_fstar_z3.sh

@@ -11,32 +11,34 @@ esac
 arch="$(uname -m)"
 case "$arch" in
   arm64) arch=aarch64 ;;
+  # ^ normalize macOS arm64 to Linux's aarch64
 esac
 
-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"
-  "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"
-  "Windows-x86_64-4.8.5":"https://github.com/Z3Prover/z3/releases/download/Z3-4.8.5/z3-4.8.5-x64-win.zip"
-  "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"
-  "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"
-  "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"
-  "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"
-  "Windows-x86_64-4.13.3":"https://github.com/Z3Prover/z3/releases/download/z3-4.13.3/z3-4.13.3-x64-win.zip"
-  "Linux-x86_64-4.15.3":"https://github.com/Z3Prover/z3/releases/download/z3-4.15.3/z3-4.15.3-x64-glibc-2.39.zip"
-  "Linux-aarch64-4.15.3":"https://github.com/Z3Prover/z3/releases/download/z3-4.15.3/z3-4.15.3-arm64-glibc-2.34.zip"
-  "Darwin-x86_64-4.15.3":"https://github.com/Z3Prover/z3/releases/download/z3-4.15.3/z3-4.15.3-x64-osx-13.7.6.zip"
-  "Darwin-aarch64-4.15.3":"https://github.com/Z3Prover/z3/releases/download/z3-4.15.3/z3-4.15.3-arm64-osx-13.7.6.zip"
-  "Windows-x86_64-4.15.3":"https://github.com/Z3Prover/z3/releases/download/z3-4.15.3/z3-4.15.3-x64-win.zip"
-)
-
 get_url() {
-  local key elem
-  key="$1"
+  local version="$1" z3_arch os_pattern
+
+  case "$arch" in
+    x86_64)  z3_arch="x64" ;;
+    aarch64) z3_arch="arm64" ;;
+    *)       z3_arch="$arch" ;;
+  esac
+
+  case "$kernel" in
+    Linux)   os_pattern="(glibc|ubuntu)" ;;
+    Darwin)  os_pattern="osx" ;;
+    Windows) os_pattern="win" ;;
+    *)       return ;;
+  esac
 
-  for elem in "${release_url[@]}"; do
-    if [ "${elem%%:*}" = "$key" ]; then
-      echo -n "${elem#*:}"
-      break
+  local tag url
+  for tag in "z3-$version" "Z3-$version"; do
+    url=$(curl -s "https://api.github.com/repos/Z3Prover/z3/releases/tags/$tag" \
+      | grep -oP '"browser_download_url":\s*"\K[^"]+' \
+      | grep -E "z3-${version}-${z3_arch}-${os_pattern}[^/]*\.zip$" \
+      | tail -1)
+    if [ -n "$url" ]; then
+      echo -n "$url"
+      return
     fi
   done
 }
@@ -146,27 +148,14 @@ fi
 
 mkdir -p "$dest_dir"
 
-for z3_ver in 4.8.5 4.13.3 4.15.3; do
+for z3_ver in 4.13.3 4.15.3 4.16.0; do
   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"
   else
-    key="$kernel-$arch-$z3_ver"
-
-    case "$key" in
-      Linux-aarch64-4.8.5)
-        echo ">>> Z3 4.8.5 is not available for aarch64, downloading x86_64 version.  You need to install qemu-user (and shared libraries) to execute it."
-        key="$kernel-x86_64-$z3_ver"
-        ;;
-      Darwin-aarch64-4.8.5)
-        echo ">>> Z3 4.8.5 is not available for aarch64, downloading x86_64 version.  You need to install Rosetta 2 to execute it."
-        key="$kernel-x86_64-$z3_ver"
-        ;;
-    esac
-
-    url="$(get_url "$key")"
+    url="$(get_url "$z3_ver")"
 
     if [ -z "$url" ]; then
       echo ">>> Z3 $z3_ver not available for this architecture, skipping..."

.scripts/package_z3.sh

@@ -19,7 +19,7 @@ inst1 () {
 	cp "$1" "$TGT"
 }
 
-for dir in z3-4.8.5 z3-4.13.3 z3-4.15.3; do
+for dir in z3-4.13.3 z3-4.15.3 z3-4.16.0; do
   inst1 ./$dir/bin/z3
   inst1 ./$dir/LICENSE.txt
   for dll in ./$dir/bin/*dll; do

INSTALL.md

@@ -28,14 +28,14 @@ using the [online F\* editor] that's part of the [F\* tutorial].
 
 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`:
+You should have `z3-4.13.3` and `z3-4.16.0` 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
+
+❯ z3-4.16.0 --version
+Z3 version 4.16.0 - 64 bit
 ```
 
 On Linux you can install these two versions with the following command:
@@ -93,8 +93,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-4.13.3 --version
-        Z3 version 4.13.3 - 64 bit
+        $ z3-4.16.0 --version
+        Z3 version 4.16.0 - 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

examples/layeredeffects/Sec2.HIFC.fst

@@ -837,8 +837,10 @@ let test8 (l:lref) (h:href)
     write l (x + 1)
 
 effect IFC (a:Type) (w r:label) (fs:flows) = HIFC a w r fs (fun _ -> True) (fun _ _ _ -> True)
+
 let test_cond (l:lref) (h:href) (b:bool)
   : IFC unit (union (single h) (single l)) (single l) [single h, single l]
+    by (Tactics.compute()) // Weird that this is now needed
   = if b then write l (read h) else write l (read l + 1)
 
 //But, using the Hoare refinements, we can recover precision and remove

fstar.opam

@@ -37,7 +37,7 @@ install: [
 post-messages: [
   """
 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
+if the version string does not match. You should have z3-4.13.3 and z3-4.16.0
 in your $PATH. For details, see
 https://github.com/FStarLang/FStar/blob/master/INSTALL.md#runtime-dependency-particular-version-of-z3.
 """ {success}

pulse/lib/core/PulseCore.IndirectionTheorySep.fst

@@ -108,9 +108,11 @@ let slprop = p:mem_pred { slprop_ok p }
 let mk_slprop (p: premem -> prop { slprop_ok' p }) : slprop =
   reveal_slprop_ok (); F.on_dom _ p
 
+#push-options "--z3rlimit 30"
 let age_to (m: mem) (n: erased nat) : mem =
   reveal_mem_le (); reveal_slprop_ok ();
   age_to_ m n
+#pop-options
 
 irreducible [@@"opaque_to_smt"]
 let reveal_mem (m: erased premem) (h: B.mem { h == timeless_heap_of m }) : m': premem { m' == reveal m } =
@@ -362,7 +364,7 @@ let star_elim (p1 p2: slprop) (w: premem { star p1 p2 w }) :
   star__elim p1 p2 w
 
 #restart-solver
-#push-options "--split_queries always"
+#push-options "--split_queries always --z3rlimit 20"
 irreducible
 let star_elim' (p1 p2: slprop) (w: mem { star p1 p2 w }) :
     GTot (w':(mem & mem) { disjoint_mem w'._1 w'._2 /\ w == join_premem w'._1 w'._2 /\ p1 w'._1 /\ p2 w'._2 }) =
@@ -1453,4 +1455,4 @@ let implies' (p q: slprop) : prop =
 let loeb (p: slprop { implies' (later p) p }) : squash (implies' emp p) =
   let rec aux (m: premem) : Lemma (ensures p m) (decreases level_ m) =
     if level_ m > 0 then aux (age1_ m) else () in
-  introduce forall m. p m with aux m
+  introduce forall m. p m with aux m

pulse/lib/pulse/lib/Pulse.Lib.Swap.Array.fst

@@ -48,7 +48,7 @@ let size_sub
 
 #restart-solver
 
-#push-options "--z3rlimit_factor 8"
+#push-options "--z3rlimit_factor 12"
 
 inline_for_extraction noextract [@@noextract_to "krml"]
 

pulse/src/checker/PulseChecker.fst.config.json

@@ -6,8 +6,6 @@
     "optimize_let_vc",
     "--ext",
     "fly_deps",
-    "--z3version",
-    "4.13.3",
     "--smtencoding.elim_box",
     "true",
     "--z3smtopt",

src/basic/FStarC.Find.Z3.fst

@@ -25,7 +25,7 @@ open FStarC.Class.Show
 
 let z3url = "https://github.com/Z3Prover/z3/releases"
 
-let packaged_z3_versions = ["4.8.5"; "4.13.3"; "4.15.3"]
+let packaged_z3_versions = ["4.13.3"; "4.15.3"; "4.16.0"]
 
 let z3_install_suggestion (v : string) : list Pprint.document =
   let open FStarC.Errors.Msg in

src/basic/FStarC.Options.fst

@@ -328,7 +328,7 @@ let defaults = [
   ("z3rlimit"                                  , Int 5);
   ("z3seed"                                    , Int 0);
   ("z3smtopt"                                  , List []);
-  ("z3version"                                 , String "4.13.3");
+  ("z3version"                                 , String "4.16.0");
 ]
 
 let init () =
@@ -1584,7 +1584,7 @@ let specs_with_types warn_unsafe : ML (list (char & string & opt_type & Pprint.d
   ( noshort,
     "z3version",
     SimpleStr "version",
-    text "Set the version of Z3 that is to be used. Default: 4.13.3");
+    text "Set the version of Z3 that is to be used. Default: 4.16.0");
 
   ( noshort,
     "__no_positivity",

ulib/FStar.BitVector.fst

@@ -122,18 +122,15 @@ let rotate_left_vec_lemma (#n: pos) (a: bv_t n) (s: nat) (i: nat{i < n})
     : Lemma (ensures index (rotate_left_vec #n a s) i = index a ((i + s) % n))
       [SMTPat (index (rotate_left_vec #n a s) i)] =
   let s' = s % n in
-  if s' = 0 then ()
-  else if i < n - s' then ()
-  else ()
+  Math.Lemmas.modulo_add n i s' s;
+  ()
 
 (** Relating the indexes of the rotated right vector to the original *)
 let rotate_right_vec_lemma (#n: pos) (a: bv_t n) (s: nat) (i: nat{i < n})
     : Lemma (ensures index (rotate_right_vec #n a s) i = index a ((i + n - (s % n)) % n))
       [SMTPat (index (rotate_right_vec #n a s) i)] =
-  let s' = s % n in
-  if s' = 0 then ()
-  else if i < s' then ()
-  else ()
+  (* Somehow trivial, unlike the above? *)
+  ()
 
 (** Rotate left by n is identity *)
 let rotate_left_vec_full_identity (#n: pos) (a: bv_t n)

ulib/FStar.UInt128.fst

@@ -181,13 +181,15 @@ let carry (a b: U64.t) : Pure U64.t
 let carry_sum_ok (a b:U64.t) :
   Lemma (U64.v (carry (U64.add_mod a b) b) == (U64.v a + U64.v b) / (pow2 64)) = ()
 
+#push-options "--z3rlimit 20"
 let add (a b: t) : Pure t
   (requires (v a + v b < pow2 128))
   (ensures (fun r -> v a + v b = v r)) =
   let l = U64.add_mod a.low b.low in
   carry_sum_ok a.low b.low;
   { low = l;
     high = U64.add (U64.add a.high b.high) (carry l b.low); }
+#pop-options
 
 let add_underspec (a b: t) =
     let l = U64.add_mod a.low b.low in