revert: Include SMT build into CI and create container-build for smt (#17021)

Author: ludamad

barretenberg/cpp/bootstrap.sh

@@ -147,18 +147,6 @@ 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/bin
-}
-
 function build_release {
   local arch=$(arch)
   rm -rf build-release
@@ -177,7 +165,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 build_smt_verification
+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
 
 function build {
   echo_header "bb cpp build"
@@ -188,7 +176,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_smt_verification build_asan_fast)
+    builds+=(build_gcc_syntax_check_only build_fuzzing_syntax_check_only build_asan_fast)
   fi
   if [ "$CI_FULL" -eq 1 ]; then
     builds+=(build_darwin)
@@ -237,13 +225,6 @@ 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"
 }
 
@@ -275,7 +256,7 @@ function bench_cmds {
   echo "$prefix barretenberg/cpp/scripts/run_bench.sh native bb-micro-bench/native/client_ivc_verify build/bin/client_ivc_bench VerificationOnly$"
 }
 
-# Runs benchmarks sharded over mache cores.
+# Runs benchmarks sharded over machine cores.
 function bench {
   echo_header "bb bench"
   rm -rf bench-out && mkdir -p bench-out
@@ -353,7 +334,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|build_smt_verification|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|inject_version)
     $cmd "$@"
     ;;
   *)

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

@@ -5,16 +5,15 @@ 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 ${CVC5_STABLE_COMMIT}
+        GIT_TAG main
         BUILD_IN_SOURCE YES
-        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
+        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
         BUILD_COMMAND make -C build -j8
         INSTALL_COMMAND make -C build install
         UPDATE_COMMAND ""     # No update step
@@ -27,9 +26,9 @@ else()
         cvc5
         PREFIX ${CVC5_PREFIX}
         GIT_REPOSITORY "https://github.com/cvc5/cvc5.git"
-        GIT_TAG ${CVC5_STABLE_COMMIT}
+        GIT_TAG main
         BUILD_IN_SOURCE YES
-        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}
+        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}
         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().get_normalized_witness_index(), "is_inf");
+    builder.set_variable_name(p1.is_point_at_infinity().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,10 +238,6 @@ 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.