bryan-minimal · Nov 6, 2026 · Sep 24, 2026 · Oct 15, 2026 · Oct 23, 2026 · Oct 23, 2026
@@ -113,9 +113,10 @@ let aeneas_sha = "ab34bd28458a08c150b7cbf1873e59af74588138" in
     # bundles it; our from-source lean does not).
     toolchain,
     leangz,
-    # `bv_decide` (exercised by Bvify's own `#guard_msgs` examples during the
-    # library build) shells out to `cadical`; lean releases bundle it, ours
-    # doesn't.
+    # `bv_decide` shells out to `cadical`; lean releases bundle it, ours
+    # doesn't. The library build runs 60 solver call sites (Bvify's
+    # `bv_decide` examples, and BvTac's `bv_tac` examples, Tests and simp
+    # lemmas), so this build is the real-goal test of a cadical bump.
     cadical,
     curl,
     git,

@@ -5,8 +5,23 @@ let make = import "../make/build.ncl" in
 let gcc = import "../gcc/build.ncl" in
 let glibc = import "../glibc/build.ncl" in
 
-# The release Lean 4.33 bundles as `bin/cadical` (lean4 CMake INSTALL_CADICAL).
-let version = "2.1.3" in
+# The latest upstream release, deliberately NOT the one Lean bundles (lean4
+# 4.35's CMakeLists.txt pins rel-2.1.2): we run current versions and fix what
+# breaks. A newer solver cannot make Lean accept a false goal, because
+# `bv_decide` checks the solver's LRAT certificate in Lean's own verified
+# checker. A solver change can only make a proof fail: a rejected
+# certificate, a timeout, or a changed message. Two places would show that:
+#   - lean's `bv_decide` standalone test is a smoke test. It checks that
+#     cadical is found and that lean accepts the certificates it writes for
+#     four goals. Three goals are small and one is Aeneas's ML-KEM
+#     conditional-subtraction goal, restated on plain `BitVec 32`. It also
+#     checks that a false goal is refuted with a counterexample.
+#   - aeneas-latest's library build covers real goals. `lake build Aeneas`
+#     runs 60 solver call sites: 9 `bv_decide` (Bvify) and 51 `bv_tac`, which
+#     ends in `bv_decide` (BvTac's examples, its Tests and 30 simp lemmas).
+#     The goals are 8- to 128-bit scalar goals. Any failure fails that build,
+#     and a cadical change re-keys it, so the build-bot rebuilds it.
+let version = "3.0.1" in
 {
   name = "cadical",
   # CaDiCaL, the SAT solver behind Lean's `bv_decide`. Official Lean releases
@@ -17,7 +32,7 @@ let version = "2.1.3" in
     { file = "build.sh" } | Local,
     {
       url = "https://github.com/arminbiere/cadical/archive/refs/tags/rel-%{version}.tar.gz",
-      sha256 = "abfe890aa4ccda7b8449c7ad41acb113cfb8e7e8fbf5e49369075f9b00d70465",
+      sha256 = "0a8ea563b5a25f5aa064634814edab45cc0e45111ea0f5d412a565f806fd7e11",
       extract = true,
       strip_prefix = "cadical-rel-%{version}",
     } | Source,

@@ -2,8 +2,41 @@
 set -ex
 export CXX=g++
 export CXXFLAGS="-O2 -ffile-prefix-map=$(pwd)=/builddir -gno-record-gcc-switches"
+# 3.x also compiles one C file (src/kitten.c) with CC/CFLAGS (CC defaults to
+# gcc for CXX=g++), so it gets the same reproducibility flags.
+export CFLAGS="$CXXFLAGS"
 export LDFLAGS="-Wl,--build-id=none"
+
+# Reproducibility: scripts/make-build-header.sh writes build.hpp's DATE macro,
+# which lands in .rodata. Since 3.0.0 it takes the date from SOURCE_DATE_EPOCH
+# (set by the sandbox, AGENTS.md), but it still appends `uname -srmn`: the
+# host's hostname and kernel release. Its other inputs are already
+# deterministic here: the git id is empty (no .git in the tarball), COMPILER
+# is `g++ --version`, FLAGS are the CXXFLAGS above.
+# Rather than edit the upstream script, give the make step a pinned `uname`
+# on PATH (kernel name and machine only, no hostname, no kernel release) and
+# TZ=UTC so the epoch renders the same everywhere.
+: "${SOURCE_DATE_EPOCH:?SOURCE_DATE_EPOCH unset}"
+real_uname="$(command -v uname)"
+shims="$(mktemp -d)"
+cat > "$shims/uname" <<SHIM
+#!/bin/sh
+echo "\$("$real_uname" -s) \$("$real_uname" -m)"
+SHIM
+chmod 755 "$shims/uname"
+
 ./configure
-make -j"$(nproc)" cadical
+PATH="$shims:$PATH" TZ=UTC make -j"$(nproc)" cadical
+
+# Fail closed if the header carries anything but the pinned value: a future
+# script change (dropping SOURCE_DATE_EPOCH, or no longer reading `uname` from
+# PATH) would otherwise silently put host data back into the binary.
+pinned="$(echo "$(LC_TIME=C TZ=UTC date -d "@$SOURCE_DATE_EPOCH") $("$shims/uname")" | sed -e 's,  *, ,g')"
+grep -qxF "#define DATE \"$pinned\"" build/build.hpp || {
+  echo "ERROR: build/build.hpp DATE is not the pinned value:" >&2
+  grep '^#define DATE' build/build.hpp >&2 || true
+  exit 1
+}
+
 mkdir -p "$OUTPUT_DIR/usr/bin"
 cp build/cadical "$OUTPUT_DIR/usr/bin/cadical"
@@ -38,7 +38,11 @@ let version = "4.35.0" in
     # `bv_decide` shells out to the `cadical` SAT solver by name on PATH. An
     # official Lean release bundles it in `bin/`; built from source we don't
     # get one, and `bv_decide` fails with "could not execute external process
-    # 'cadical'" (found building aeneas-latest). Same release Lean pins.
+    # 'cadical'" (found building aeneas-latest). Our cadical is the latest
+    # release, not the older one Lean's CMake bundles: `bv_decide` verifies
+    # the solver's LRAT certificate, so a newer solver cannot make lean accept
+    # a false goal. The `bv_decide` test below is a smoke test of the pair.
+    # aeneas-latest's build is the real-goal coverage (see cadical/build.ncl).
     cadical,
     # `lean` and `libleanshared.so` link libssl.so.3 / libcrypto.so.3 (lake's
     # HTTP client). Without this the binary does not START in a closure that
@@ -115,6 +119,26 @@ let version = "4.35.0" in
           ["/bin/bash", "-c", "mkdir -p /tmp/lk && cd /tmp/lk && printf 'import Lake\\nopen Lake DSL\\npackage t\\n@[default_target] lean_lib T\\n' > lakefile.lean && mkdir -p T && printf 'def hello := 42\\n' > T.lean && LAKE_NO_CACHE=1 HOME=/tmp/lk lake build"],
         ],
       } | Test,
+    # `bv_decide` end to end, against the `cadical` runtime dep. Lean bit-blasts
+    # each goal to CNF, runs cadical (`--lrat --binary=true --quiet ...`), and
+    # replays the LRAT certificate in its own checker, so this proves both that
+    # cadical is found and that lean accepts the proofs this cadical writes.
+    # Each goal reaches the SAT solver (none is closed by bv_decide's
+    # preprocessing): with a fake `cadical` that prints garbage, every one of
+    # them fails. `csub` is a realistic query: Aeneas's ML-KEM conditional
+    # subtraction (aeneas-latest's Bvify.lean), restated on plain BitVec 32
+    # so it needs no Aeneas import. It takes under a second. The second
+    # command takes the SAT path: a false goal must be refuted with a
+    # counterexample, not proved and not errored.
+    bv_decide =
+      {
+        class = 'Standalone,
+        test_deps = [base],
+        cmds = [
+          ["/bin/bash", "-c", "cd /tmp && printf '%s\\n' 'import Std.Tactic.BVDecide' 'theorem mul3 (x : BitVec 32) : x * 3 = x + x + x := by bv_decide' 'theorem andor (x y : BitVec 32) : (x &&& y) + (x ||| y) = x + y := by bv_decide' 'theorem mulcomm (x y : BitVec 8) : x * y = y * x := by bv_decide (config := { solverMode := .proof })' 'theorem csub (a b c2 c5 : BitVec 32) (ha : a < 3329#32) (hb : b < 3329#32) (hc2 : c2 = a + b - 3329#32) (hc5 : c5 = c2 + (3329#32 &&& (c2 >>> 16))) : c5 % 3329#32 = (a + b) % 3329#32 ∧ c5 < 3329#32 := by bv_decide' > bv.lean && lean bv.lean"],
+          ["/bin/bash", "-c", "cd /tmp && printf '%s\\n' 'import Std.Tactic.BVDecide' 'theorem bad (x : BitVec 8) : x < x + 1 := by bv_decide' > cex.lean; out=\"$(lean cex.lean 2>&1)\"; echo \"$out\"; echo \"$out\" | grep -q 'The prover found a counterexample'"],
+        ],
+      } | Test,
   },
   attrs =
     {