Experimenting with different adder implementations

.github/workflows/algebraic-checks.yaml

@@ -0,0 +1,67 @@
+name: Algebraic solver checks
+
+# Lightweight guards for the algebraic pre-solver:
+#  1. proof-traceability lint (no build) — every PROOF: reference resolves
+#     and every UNSAT conclusion in try_algebraic_solve is annotated;
+#  2. a soundness smoke test that runs the algebraic regression queries and
+#     cross-checks each verdict against z3 (the wrong-verdict guard that the
+#     standard output-matching regression harness does not provide).
+
+on:
+  pull_request:
+    branches:
+      - '**'
+    paths:
+      - 'src/solvers/algebraic/**'
+      - 'src/solvers/flattening/boolbv*'
+      - 'src/solvers/flattening/bv_utils*'
+      - 'src/solvers/smt2/**'
+      - 'formal-proofs/**'
+      - 'regression/smt2_solver/**'
+      - 'scripts/check_proof_traceability.py'
+      - 'scripts/algebraic_soundness_smoke.sh'
+      - '.github/workflows/algebraic-checks.yaml'
+  push:
+    branches:
+      - main
+      - develop
+
+jobs:
+  proof-traceability:
+    name: Proof-traceability lint
+    runs-on: ubuntu-24.04
+    steps:
+      - uses: actions/checkout@v6
+      - name: Run proof-traceability check
+        run: python3 scripts/check_proof_traceability.py
+
+  soundness-smoke:
+    name: Algebraic soundness smoke (vs z3)
+    runs-on: ubuntu-24.04
+    timeout-minutes: 40
+    steps:
+      - uses: actions/checkout@v6
+        with:
+          submodules: true
+      - name: Install dependencies
+        run: |
+          export DEBIAN_FRONTEND=noninteractive
+          sudo apt-get update
+          sudo apt-get install --no-install-recommends -y \
+            clang-19 clang++-19 flex bison cmake ninja-build ccache z3
+      - name: Prepare ccache
+        uses: actions/cache@v5
+        with:
+          path: .ccache
+          key: ${{ runner.os }}-algcheck-${{ github.sha }}
+          restore-keys: ${{ runner.os }}-algcheck-
+      - name: ccache environment
+        run: echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
+      - name: Build smt2_solver
+        run: |
+          cmake -S . -Bbuild -GNinja -DCMAKE_BUILD_TYPE=Release \
+            -DCMAKE_CXX_COMPILER=clang++-19 \
+            -DCMAKE_CXX_COMPILER_LAUNCHER=ccache -DWITH_JBMC=OFF
+          cmake --build build --target smt2_solver -- -j4
+      - name: Run soundness smoke test
+        run: scripts/algebraic_soundness_smoke.sh build/bin/smt2_solver

.github/workflows/lean-proofs.yaml

@@ -0,0 +1,132 @@
+name: Lean formal proofs
+
+on:
+  pull_request:
+    branches:
+      - '**'
+    paths:
+      - 'formal-proofs/**'
+      - '.github/workflows/lean-proofs.yaml'
+  push:
+    branches:
+      - main
+      - develop
+    paths:
+      - 'formal-proofs/**'
+      - '.github/workflows/lean-proofs.yaml'
+
+jobs:
+  lean-build:
+    name: Build and verify Lean proofs
+    runs-on: ubuntu-24.04
+    timeout-minutes: 60
+    defaults:
+      run:
+        working-directory: formal-proofs
+    steps:
+      - uses: actions/checkout@v6
+
+      - name: Install elan (Lean version manager)
+        run: |
+          set -o pipefail
+          curl -sSfL https://raw.githubusercontent.com/leanprover/elan/v4.0.1/elan-init.sh | sh -s -- -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+
+      - name: Show Lean toolchain
+        run: |
+          cat lean-toolchain
+          lean --version
+          lake --version
+
+      - name: Cache .lake (mathlib + build artifacts)
+        id: lake-cache
+        uses: actions/cache@v5
+        with:
+          path: formal-proofs/.lake
+          # Key on the lakefile + manifest + toolchain so that any
+          # dependency change invalidates the cache.
+          key: lake-${{ runner.os }}-${{ hashFiles('formal-proofs/lakefile.toml', 'formal-proofs/lake-manifest.json', 'formal-proofs/lean-toolchain') }}
+          restore-keys: |
+            lake-${{ runner.os }}-
+
+      - name: Fetch mathlib oleans from cache (if not in lake cache already)
+        run: |
+          # `lake exe cache get` downloads prebuilt mathlib oleans.
+          # This is much faster than building mathlib from source.
+          # Skip if the .lake cache already covers it.
+          if [ ! -f .lake/packages/mathlib/.lake/build/lib/lean/Mathlib.olean ]; then
+            lake exe cache get || true  # tolerated: failure means we will build from source
+          fi
+
+      - name: Build all modules
+        run: lake build
+
+      - name: Verify zero sorry across project modules
+        run: |
+          set -e
+          fail=0
+          for f in *.lean; do
+            if [ "$f" = "Main.lean" ]; then continue; fi
+            count=$(grep -E "^[[:space:]]*sorry[[:space:]]*$" "$f" | wc -l)
+            if [ "$count" -gt 0 ]; then
+              echo "::error file=formal-proofs/$f::contains $count sorry"
+              fail=1
+            fi
+          done
+          if [ "$fail" -eq 1 ]; then
+            echo "Sorry-check failed."
+            exit 1
+          fi
+          echo "Sorry-check passed: zero sorry across all project modules."
+
+      - name: Verify project axioms are only the documented ones
+        run: |
+          set -e
+          # All project-internal axioms have been mechanised. Any
+          # module that introduces axioms requires explicit review.
+          fail=0
+          for f in *.lean; do
+            if [ "$f" = "Main.lean" ]; then continue; fi
+            count=$(grep -cE "^axiom " "$f" || true)
+            if [ "$count" -gt 0 ]; then
+              echo "::error file=formal-proofs/$f::introduces $count undocumented axioms"
+              fail=1
+            fi
+          done
+          if [ "$fail" -eq 1 ]; then
+            echo "Axiom check failed."
+            exit 1
+          fi
+          echo "Axiom check passed: zero project-internal axioms across all modules."
+
+      - name: Verify forward traceability (PROOF: refs resolve)
+        working-directory: .
+        run: |
+          set -e
+          fail=0
+          # Every PROOF: formal-proofs/<File>::<theorem> reference in src/
+          # must resolve to an existing theorem/lemma/instance in <File>.
+          grep -rh "PROOF: formal-proofs" src/ 2>/dev/null | sort -u | while read ref; do
+            file=$(echo "$ref" | sed "s|.*formal-proofs/\([^:]*\)::.*|\1|")
+            thm=$(echo "$ref" | sed "s|.*::\([a-zA-Z_][a-zA-Z0-9_'.]*\).*|\1|")
+            if [ -z "$thm" ] || [ "$thm" = "$ref" ]; then continue; fi
+            if [ ! -f "formal-proofs/$file" ]; then
+              echo "::error::missing file formal-proofs/$file (referenced as ::$thm)"
+              echo "fail" > /tmp/trace_fail
+              continue
+            fi
+            short=$(echo "$thm" | rev | cut -d. -f1 | rev)
+            if grep -qE "^(theorem|lemma|def|axiom|instance) +${thm}( |\$)" "formal-proofs/$file" 2>/dev/null; then
+              :
+            elif grep -qE "^(theorem|lemma|def|axiom|instance) +${short}( |\$)" "formal-proofs/$file" 2>/dev/null; then
+              :
+            else
+              echo "::error::unresolved PROOF: ref formal-proofs/$file::$thm"
+              echo "fail" > /tmp/trace_fail
+            fi
+          done
+          if [ -f /tmp/trace_fail ]; then
+            echo "Forward traceability check failed."
+            exit 1
+          fi
+          echo "Forward traceability check passed."

.github/workflows/pull-request-checks.yaml

@@ -234,7 +234,7 @@ jobs:
         env:
           # This is needed in addition to -yq to prevent apt-get from asking for
           # user input
-          DEBIAN_FRONTEND: noninteractive
+          DEBIAN_FRONTEND: nonint eractive
         run: |
           sudo apt-get update
           sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc gdb g++ maven flex bison libxml2-utils dpkg-dev ccache doxygen graphviz z3
@@ -301,6 +301,62 @@ jobs:
         with:
           path: .ccache
           key: ${{ steps.restore-ccache.outputs.cache-primary-key }}
+
+  # This job takes approximately 29 to 42 minutes
+  check-ubuntu-24_04-cmake-gcc-mergesat:
+    runs-on: ubuntu-24.04
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          submodules: recursive
+      - name: Fetch dependencies
+        env:
+          # This is needed in addition to -yq to prevent apt-get from asking for
+          # user input
+          DEBIAN_FRONTEND: noninteractive
+        run: |
+          sudo apt-get update
+          sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc gdb g++ maven flex bison libxml2-utils dpkg-dev ccache doxygen z3
+      - name: Confirm z3 solver is available and log the version installed
+        run: z3 --version
+      - name: Download cvc-5 from the releases page and make sure it can be deployed
+        run: |
+          wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-x86_64-static.zip
+          unzip -j -d /usr/local/bin cvc5-Linux-x86_64-static.zip cvc5-Linux-x86_64-static/bin/cvc5
+          rm cvc5-Linux-x86_64-static.zip
+          cvc5 --version
+      - name: Prepare ccache
+        uses: actions/cache@v4
+        with:
+          path: .ccache
+          key: ${{ runner.os }}-24.04-Release-mergesat-${{ github.ref }}-${{ github.sha }}-PR
+          restore-keys: |
+            ${{ runner.os }}-24.04-Release-mergesat-${{ github.ref }}
+            ${{ runner.os }}-24.04-Release-mergesat
+      - name: ccache environment
+        run: |
+          echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
+          echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
+      - name: Configure using CMake
+        run: cmake -S . -B build -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ -Dsat_impl="mergesat;cadical"
+      - name: Check that doc task works
+        run: ninja -C build doc
+      - name: Zero ccache stats and limit in size
+        run: ccache -z --max-size=500M
+      - name: Build with Ninja
+        run: ninja -C build -j${{env.linux-vcpus}}
+      - name: Print ccache stats
+        run: ccache -s
+      - name: Checking completeness of help output
+        run: scripts/check_help.sh /usr/bin/g++ build/bin
+      - name: Check if package building works
+        run: |
+          cd build
+          ninja package
+          ls *.deb
+      - name: Run tests
+        run: cd build; ctest . -V -L CORE -j${{env.linux-vcpus}}
+
   # This job takes approximately 20 to 38 minutes
   check-ubuntu-22_04-make-clang:
     runs-on: ubuntu-22.04

.gitignore

@@ -166,3 +166,11 @@ dist/
 
 # auto generated documentation
 doc/html/
+scripts/adder-research/benchmarks/
+
+# Stray artifacts that were accidentally committed in the past
+# (build trees, coverage output, patch backups). See REPRODUCE.md.
+build-*/
+*.gcov
+*.gcno
+*.orig

bench-multiplication/ablation-audit/ablation-cbmc.sh

@@ -0,0 +1,32 @@
+#!/bin/bash
+# cbmc ablation: ON vs DISABLE_ALGEBRAIC=1.  result via VERIFICATION (SUCCESSFUL/FAILED)
+# Usage: ablation-cbmc.sh <timeout> <out-tsv> -- "<label> <cbmc-args...>" ...
+set -u
+CBMC=/home/ubuntu/cbmc-github.git/build/bin/cbmc
+TO="$1"; OUT="$2"; shift 2; shift   # drop the --
+: > "$OUT"
+runv() { # $1=label-args
+  local args="$1" label v
+  label="${args%% *}"; local rest="${args#* }"
+  local s e ton toff von voff
+  s=$(date +%s.%N)
+  von=$( ulimit -v 12000000 2>/dev/null; timeout "$TO" $CBMC $rest --no-standard-checks 2>/dev/null \
+         | grep -aoE "VERIFICATION (SUCCESSFUL|FAILED)" | head -1)
+  e=$(date +%s.%N); ton=$(echo "$e-$s"|bc)
+  s=$(date +%s.%N)
+  voff=$( ulimit -v 12000000 2>/dev/null; DISABLE_ALGEBRAIC=1 timeout "$TO" $CBMC $rest --no-standard-checks 2>/dev/null \
+         | grep -aoE "VERIFICATION (SUCCESSFUL|FAILED)" | head -1)
+  e=$(date +%s.%N); toff=$(echo "$e-$s"|bc)
+  [ -z "$von" ] && von=TO; [ -z "$voff" ] && voff=TO
+  local sol_on=0 sol_off=0
+  [ "$von" = "VERIFICATION SUCCESSFUL" ] && sol_on=1
+  [ "$voff" = "VERIFICATION SUCCESSFUL" ] && sol_off=1
+  local cls
+  if [ $sol_on = 1 ] && [ $sol_off = 0 ]; then cls=NEEDS_ALGEBRA
+  elif [ $sol_on = 0 ] && [ $sol_off = 1 ]; then cls=ONLY_OFF
+  elif [ $sol_on = 0 ] && [ $sol_off = 0 ]; then cls=BOTH_TO
+  elif awk "BEGIN{exit !($toff>=3*$ton && $toff-$ton>=5)}"; then cls=ALGEBRA_FASTER
+  else cls=ARTIFACT; fi
+  printf '%s\t%s\t%.2f\t%s\t%.2f\t%s\n' "$label" "$von" "$ton" "$voff" "$toff" "$cls" | tee -a "$OUT"
+}
+for spec in "$@"; do runv "$spec"; done

bench-multiplication/ablation-audit/ablation.sh

@@ -0,0 +1,38 @@
+#!/bin/bash
+# Ablation audit: for each benchmark run algebra-ON vs DISABLE_ALGEBRAIC=1.
+# Usage: ablation.sh <list-of-abs-paths> <timeout> <jobs> <out-tsv>
+# Output columns: path  v_on  t_on  v_off  t_off  class
+#   class: NEEDS_ALGEBRA (on solves, off TO)
+#          ALGEBRA_FASTER (both solve, on >=3x faster AND saves >=5s)
+#          ARTIFACT       (both solve, comparable)
+#          BOTH_TO        (neither solves)
+#          ONLY_OFF       (off solves, on doesn't -- algebra harmful)
+set -u
+LIST="$1"; TO="$2"; JOBS="$3"; OUT="$4"
+SOLVER=/home/ubuntu/cbmc-github.git/build/bin/smt2_solver
+
+one() {
+  local f="$1" to="$2" von toff voff ton s e
+  s=$(date +%s.%N)
+  von=$( ulimit -v 8000000 2>/dev/null; timeout "$to" "$SOLVER" < "$f" 2>/dev/null | grep -aE '^(sat|unsat|unknown)$' | head -1 )
+  e=$(date +%s.%N); ton=$(echo "$e-$s"|bc)
+  s=$(date +%s.%N)
+  voff=$( ulimit -v 8000000 2>/dev/null; DISABLE_ALGEBRAIC=1 timeout "$to" "$SOLVER" < "$f" 2>/dev/null | grep -aE '^(sat|unsat|unknown)$' | head -1 )
+  e=$(date +%s.%N); toff=$(echo "$e-$s"|bc)
+  [ -z "$von" ] && von=TO; [ -z "$voff" ] && voff=TO
+  local cls
+  sol() { [ "$1" = sat ] || [ "$1" = unsat ]; }
+  if sol "$von" && ! sol "$voff"; then cls=NEEDS_ALGEBRA
+  elif ! sol "$von" && sol "$voff"; then cls=ONLY_OFF
+  elif ! sol "$von" && ! sol "$voff"; then cls=BOTH_TO
+  else
+    # both solve
+    if awk "BEGIN{exit !($toff>=3*$ton && $toff-$ton>=5)}"; then cls=ALGEBRA_FASTER
+    else cls=ARTIFACT; fi
+  fi
+  printf '%s\t%s\t%.2f\t%s\t%.2f\t%s\n' "$f" "$von" "$ton" "$voff" "$toff" "$cls"
+}
+export -f one; export SOLVER
+: > "$OUT"
+cat "$LIST" | xargs -P "$JOBS" -I {} bash -c 'one "$@"' _ {} "$TO" >> "$OUT"
+echo "Done: $(wc -l <"$OUT") in $OUT"

bench-multiplication/ablation-audit/brain-wins.tsv

@@ -0,0 +1,4 @@
+/tmp/martin-bench/seed-23/bitwidth-16-degree-13-seed-23-multiplication-reduced-native-encoding.smt2	unsat	0.26	TO	60.01	NEEDS_ALGEBRA
+/tmp/martin-bench/seed-23/bitwidth-16-degree-23-seed-23-correctness-original-native-encoding-vs-reduced-native-encoding.smt2	unsat	0.34	TO	60.01	NEEDS_ALGEBRA
+/tmp/martin-bench/seed-23/bitwidth-32-degree-27-seed-23-correctness-original-native-encoding-vs-reduced-native-encoding.smt2	unsat	2.53	TO	60.06	NEEDS_ALGEBRA
+/tmp/martin-bench/seed-23/bitwidth-32-degree-19-seed-23-multiplication-reduced-native-encoding.smt2	unsat	3.10	TO	60.07	NEEDS_ALGEBRA

bench-multiplication/ablation-audit/custom-c.tsv

@@ -0,0 +1,8 @@
+mac_equiv	VERIFICATION SUCCESSFUL	0.14	VERIFICATION SUCCESSFUL	45.80	ALGEBRA_FASTER
+div_roundtrip	VERIFICATION SUCCESSFUL	0.04	VERIFICATION SUCCESSFUL	0.91	ARTIFACT
+comm_64	VERIFICATION SUCCESSFUL	0.03	TO	90.01	NEEDS_ALGEBRA
+assoc	VERIFICATION SUCCESSFUL	0.03	VERIFICATION FAILED	0.05	NEEDS_ALGEBRA
+distrib	VERIFICATION SUCCESSFUL	0.03	VERIFICATION SUCCESSFUL	0.03	ARTIFACT
+mul_overflow	VERIFICATION SUCCESSFUL	0.03	TO	90.01	NEEDS_ALGEBRA
+matrix_mul	VERIFICATION SUCCESSFUL	0.04	TO	90.01	NEEDS_ALGEBRA
+hash_mul	VERIFICATION SUCCESSFUL	0.05	TO	90.01	NEEDS_ALGEBRA