smt check for ci + container-build

Pinning cvc5 to stable commit. Resolve building errors. Update boostrap
Add Required packages to ci environment

Author: Sarkoxed

barretenberg/cpp/bootstrap.sh

@@ -147,6 +147,19 @@ function build_fuzzing_syntax_check_only {
   cache_upload barretenberg-fuzzing-$hash.zst build-fuzzing/syntax-check-success.flag
 }
 
+# Do basic tests that the smt preset still compiles and runs
+function build_smt_verification {
+  set -eu
+  if cache_download barretenberg-smt-$hash.zst; then
+    return
+  fi
+
+  sudo apt update && sudo apt install -y python3-pip python3-venv m4
+  cmake --preset smt-verification
+  cmake --build build-smt --target smt_verification_tests
+  cache_upload barretenberg-smt-$hash.zst build-smt
+}
+
 function build_release {
   local arch=$(arch)
   rm -rf build-release
@@ -165,7 +178,7 @@ function build_release {
   fi
 }
 
-export -f build_preset build_native build_asan_fast build_darwin build_nodejs_module build_wasm build_wasm_threads build_gcc_syntax_check_only build_fuzzing_syntax_check_only
+export -f build_preset build_native build_asan_fast build_darwin build_nodejs_module build_wasm build_wasm_threads build_gcc_syntax_check_only build_fuzzing_syntax_check_only build_smt_verification
 
 function build {
   echo_header "bb cpp build"
@@ -176,7 +189,7 @@ function build {
     build_wasm_threads
   )
   if [ "$(arch)" == "amd64" ] && [ "$CI" -eq 1 ]; then
-    builds+=(build_gcc_syntax_check_only build_fuzzing_syntax_check_only build_asan_fast)
+    builds+=(build_gcc_syntax_check_only build_fuzzing_syntax_check_only build_asan_fast build_smt_verification)
   fi
   if [ "$CI_FULL" -eq 1 ]; then
     builds+=(build_darwin)
@@ -225,6 +238,13 @@ function test_cmds {
       echo -e "$prefix barretenberg/cpp/build-asan-fast/bin/$bin_name --gtest_filter=$filter"
     done
   fi
+
+  # Run the SMT compatibility tests
+  if [ "$(arch)" == "amd64" ] &&  [ "$CI" -eq 1 ]; then
+    local prefix="$hash:CPUS=4:MEM=8g"
+    echo -e "$prefix barretenberg/cpp/build-smt/bin/smt_verification_tests"
+  fi
+
   echo "$hash barretenberg/cpp/scripts/test_civc_standalone_vks_havent_changed.sh"
 }
 
@@ -334,7 +354,7 @@ case "$cmd" in
   "hash")
     echo $hash
     ;;
-  test|test_cmds|bench|bench_cmds|build_bench|release|build_native|build_nodejs_module|build_asan_fast|build_wasm|build_wasm_threads|build_gcc_syntax_check_only|build_fuzzing_syntax_check_only|build_darwin|build_release|inject_version)
+  test|test_cmds|bench|bench_cmds|build_bench|release|build_native|build_nodejs_module|build_asan_fast|build_wasm|build_wasm_threads|build_gcc_syntax_check_only|build_fuzzing_syntax_check_only|build_darwin|build_release|build_smt_verification|inject_version)
     $cmd "$@"
     ;;
   *)

barretenberg/cpp/src/barretenberg/smt_verification/CMakeLists.txt

@@ -5,15 +5,16 @@ set(CVC5_PREFIX "${CMAKE_BINARY_DIR}/_deps/cvc5")
 set(CVC5_BUILD "${CVC5_PREFIX}/src/cvc5-build")
 set(CVC5_LIB "${CVC5_BUILD}/lib/libcvc5.so")
 set(CVC5_INCLUDE "${CVC5_BUILD}/include")
+set(CVC5_STABLE_COMMIT "5fcdb48eb26dee9385e0d0e6377fcc7e4afee85a")
 
 if(ENABLE_ASAN)
     ExternalProject_Add(
         cvc5
         PREFIX ${CVC5_PREFIX}
         GIT_REPOSITORY "https://github.com/cvc5/cvc5.git"
-        GIT_TAG main
+        GIT_TAG ${CVC5_STABLE_COMMIT}
         BUILD_IN_SOURCE YES
-        CONFIGURE_COMMAND ${SHELL} ./configure.sh debug --gpl --auto-download --cocoa --cryptominisat --kissat -DCMAKE_C_COMPILER=/usr/bin/clang -DCMAKE_CXX_COMPILER=/usr/bin/clang++ --prefix=${CVC5_BUILD} --asan
+        CONFIGURE_COMMAND ${SHELL} ./configure.sh debug --gpl --auto-download --cocoa --cryptominisat --kissat -DCMAKE_C_COMPILER=${CMAKE_C_COMPILER} -DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER} --prefix=${CVC5_BUILD} --asan
         BUILD_COMMAND make -C build -j8
         INSTALL_COMMAND make -C build install
         UPDATE_COMMAND ""     # No update step
@@ -26,9 +27,9 @@ else()
         cvc5
         PREFIX ${CVC5_PREFIX}
         GIT_REPOSITORY "https://github.com/cvc5/cvc5.git"
-        GIT_TAG main
+        GIT_TAG ${CVC5_STABLE_COMMIT}
         BUILD_IN_SOURCE YES
-        CONFIGURE_COMMAND ${SHELL} ./configure.sh production --gpl --auto-download --cocoa --cryptominisat --kissat -DCMAKE_C_COMPILER=/usr/bin/clang -DCMAKE_CXX_COMPILER=/usr/bin/clang++ --prefix=${CVC5_BUILD}
+        CONFIGURE_COMMAND ${SHELL} ./configure.sh production --gpl --auto-download --cocoa --cryptominisat --kissat -DCMAKE_C_COMPILER=${CMAKE_C_COMPILER} -DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER} --prefix=${CVC5_BUILD}
         BUILD_COMMAND make -C build -j8
         INSTALL_COMMAND make -C build install
         UPDATE_COMMAND ""     # No update step

barretenberg/cpp/src/barretenberg/smt_verification/circuit/ultra_circuit.test.cpp

@@ -160,7 +160,7 @@ TEST(UltraCircuitSMT, EllipticRelationDBL)
     builder.set_variable_name(p2.x.get_witness_index(), "x2");
     builder.set_variable_name(p1.y.get_witness_index(), "y1");
     builder.set_variable_name(p2.y.get_witness_index(), "y2");
-    builder.set_variable_name(p1.is_point_at_infinity().witness_index, "is_inf");
+    builder.set_variable_name(p1.is_point_at_infinity().get_normalized_witness_index(), "is_inf");
 
     auto circuit_info = unpack_from_buffer(builder.export_circuit());
     Solver s(circuit_info.modulus, ultra_solver_config);

build-images/src/Dockerfile

@@ -238,6 +238,10 @@ RUN apt update && \
         inotify-tools \
         # Annoyingly unminimize upgrades nodejs.
         nodejs=22.16.0-1nodesource1 \
+        # smt_verification dependencies
+        python3-venv \
+        python3-pip \
+        m4 \
     && rm -rf /var/lib/apt/lists/* /tmp/* /var/tmp/*
 
 # Install osxcross. Requires developer to mount SDK from their mac host.

container-builds/smt-container/build.sh

@@ -0,0 +1,5 @@
+#!/usr/bin/env bash
+
+image_name="smt-build-static"
+COMMIT="f3ff6161155ba5e07d14ea1c52a218494eb8bb96"
+docker build -t "$image_name" --target reuse --build-arg COMMIT="$COMMIT" src

container-builds/smt-container/src/Dockerfile

@@ -0,0 +1,30 @@
+FROM ubuntu:noble as base
+
+RUN apt-get update && \
+    apt-get install -y build-essential python3 wget unzip git cmake clang ninja-build curl python3-venv python3-pip m4 && \
+    apt-get -y autoremove && \
+    apt-get clean && \
+    rm -rf /var/lib/apt/lists/* /tmp/* /var/tmp/*
+RUN useradd -m smt -G sudo
+WORKDIR /home/smt
+
+FROM base AS cvc5
+RUN git clone https://github.com/AztecProtocol/aztec-packages.git
+WORKDIR /home/smt/aztec-packages/barretenberg/cpp
+RUN cmake -DCMAKE_C_COMPILER=clang-18 -DCMAKE_CXX_COMPILER=clang++-18 --preset smt-verification
+RUN cmake --build ./build-smt --target cvc5
+
+FROM base AS reuse
+
+ARG COMMIT=latest
+RUN git clone https://github.com/AztecProtocol/aztec-packages.git && \
+    cd aztec-packages &&                                             \
+    if [ "$COMMIT" != "latest" ]; then                               \
+        git checkout $COMMIT || exit 1;                              \
+    fi
+
+WORKDIR /home/smt/aztec-packages/barretenberg/cpp
+RUN cmake -DCMAKE_C_COMPILER=clang-18 -DCMAKE_CXX_COMPILER=clang++-18 --preset smt-verification
+RUN rm -rf ./build-smt/_deps/cvc5
+COPY --from=cvc5 /home/smt/aztec-packages/barretenberg/cpp/build-smt/_deps/cvc5 ./build-smt/_deps/cvc5
+RUN cmake --build ./build-smt --target smt_verification_tests