Pin F* release v2026.04.17 in setup.sh and CI

- setup.sh: default 'binary' mode now installs pinned release (v2026.04.17)
  instead of latest nightly. Supports: './setup.sh binary' (pinned),
  './setup.sh binary nightly', './setup.sh binary VERSION'.
- CI: uses pinned release for reproducible builds.
- Nightly workflow: explicitly passes 'nightly' to track master.
- Pulse mk files are now fetched from the matching release tag.
- Ch15 MatrixChain: bump rlimit 10→20 for one query that became
  marginal in the new release (was using exactly 10.0/10.0).

Full clean build passes with -j$(nproc) on v2026.04.17.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Author: nikswamy

.github/workflows/ci.yml

@@ -16,7 +16,7 @@ jobs:
       - name: Checkout
         uses: actions/checkout@v4
 
-      - name: Install F* (nightly binary)
+      - name: Install F* (pinned release)
         run: ./setup.sh binary
 
       - name: Show F* version

.github/workflows/nightly.yml

@@ -15,7 +15,7 @@ jobs:
         uses: actions/checkout@v4
 
       - name: Install F* (latest nightly)
-        run: ./setup.sh binary
+        run: ./setup.sh binary nightly
 
       - name: Show F* version
         run: ./fstar/bin/fstar.exe --version

autoclrs/ch15-dynamic-programming/CLRS.Ch15.MatrixChain.Impl.fst

@@ -83,6 +83,7 @@ let mc_result_eq_mc_cost (dims: Seq.seq int) (n: nat)
 
 open Pulse.Lib.BoundedIntegers
 
+#push-options "--z3rlimit 20"
 //SNIPPET_START: mc_sig
 fn matrix_chain_order
   (#p: perm)
@@ -287,3 +288,4 @@ fn matrix_chain_order
 
   result
 }
+#pop-options

setup.sh

@@ -4,7 +4,9 @@
 # Two modes:
 #
 #   1. Binary install (recommended for most users):
-#      ./setup.sh binary          # install latest nightly F* binary
+#      ./setup.sh binary          # install pinned release (v2026.04.17)
+#      ./setup.sh binary nightly  # install latest nightly build
+#      ./setup.sh binary v2026.04.17  # install a specific release
 #
 #   2. Source build (for F* developers):
 #      ./setup.sh                 # build F* stage3 + KaRaMeL from submodule
@@ -27,6 +29,9 @@ NPROC=$(nproc 2>/dev/null || sysctl -n hw.ncpu 2>/dev/null || echo 4)
 # Binary install destination
 FSTAR_BIN_DIR="$SCRIPT_DIR/fstar"
 
+# Pinned F* release version (update when a new release is validated)
+FSTAR_RELEASE_VERSION="v2026.04.17"
+
 red()   { printf '\033[1;31m%s\033[0m\n' "$*"; }
 green() { printf '\033[1;32m%s\033[0m\n' "$*"; }
 info()  { printf '\033[1;34m=> %s\033[0m\n' "$*"; }
@@ -123,9 +128,22 @@ build_karamel() {
 # ---- Binary install ----
 
 install_binary() {
-  info "Installing F* nightly binary to $FSTAR_BIN_DIR ..."
+  local version_arg="${1:-}"
+  local install_flags=()
+
+  if [ "$version_arg" = "nightly" ]; then
+    info "Installing F* latest nightly binary to $FSTAR_BIN_DIR ..."
+    install_flags=(--nightly)
+  elif [ -n "$version_arg" ]; then
+    info "Installing F* $version_arg binary to $FSTAR_BIN_DIR ..."
+    install_flags=(--release --version "$version_arg")
+  else
+    info "Installing F* $FSTAR_RELEASE_VERSION binary to $FSTAR_BIN_DIR ..."
+    install_flags=(--release --version "$FSTAR_RELEASE_VERSION")
+  fi
+
   curl -fsSL https://aka.ms/install-fstar | bash -s -- \
-    --nightly \
+    "${install_flags[@]}" \
     --dest "$FSTAR_BIN_DIR" \
     --no-link
 
@@ -150,9 +168,11 @@ install_binary() {
 # These are small build-infrastructure files not included in binary packages.
 install_pulse_mk() {
   local mk_dir="$FSTAR_BIN_DIR/pulse/mk"
-  local base_url="https://raw.githubusercontent.com/FStarLang/FStar/master/pulse/mk"
+  # Use the pinned release tag for mk files so they match the installed binary
+  local tag="${FSTAR_RELEASE_VERSION}"
+  local base_url="https://raw.githubusercontent.com/FStarLang/FStar/${tag}/pulse/mk"
 
-  info "Downloading Pulse build infrastructure (mk files)..."
+  info "Downloading Pulse build infrastructure (mk files from ${tag})..."
   mkdir -p "$mk_dir"
   for f in common.mk locate.mk test.mk krmlheader; do
     curl -fsSL "$base_url/$f" -o "$mk_dir/$f"
@@ -182,7 +202,7 @@ setup_karamel_compat() {
 case "${1:-all}" in
   binary)
     check_prereqs_binary
-    install_binary
+    install_binary "${2:-}"
     ;;
   fstar)
     check_prereqs
@@ -203,12 +223,14 @@ case "${1:-all}" in
     green "Setup complete. Run 'make' to verify all chapters."
     ;;
   *)
-    echo "Usage: $0 [binary|fstar|karamel|all]"
+    echo "Usage: $0 [binary [nightly|VERSION]|fstar|karamel|all]"
     echo
-    echo "  binary    Install F* from a pre-built nightly binary (fast)"
-    echo "  fstar     Build F* stage3 from source (requires OCaml)"
-    echo "  karamel   Build KaRaMeL from source (requires F* already built)"
-    echo "  all       Build F* + KaRaMeL from source (default)"
+    echo "  binary              Install pinned F* release ($FSTAR_RELEASE_VERSION)"
+    echo "  binary nightly      Install latest nightly F* build"
+    echo "  binary VERSION      Install a specific release (e.g. v2026.04.17)"
+    echo "  fstar               Build F* stage3 from source (requires OCaml)"
+    echo "  karamel             Build KaRaMeL from source (requires F* already built)"
+    echo "  all                 Build F* + KaRaMeL from source (default)"
     exit 1
     ;;
 esac