Add formal verification tests using Halmos

.github/workflows/ci.yml

@@ -98,38 +98,6 @@ jobs:
       - name: Check unused imports
         run: python3 script/utils/fix_imports.py --check-unused
 
-  # halmos:
-  #   runs-on: ubuntu-latest
-
-  #   steps:
-  #     - name: Checkout
-  #       uses: actions/checkout@v4
-  #       with:
-  #         submodules: recursive
-
-  #     - name: Setup Python
-  #       uses: actions/setup-python@v5
-  #       with:
-  #         python-version: 3.13
-  #         architecture: x64
-
-  #     - name: Install Foundry
-  #       uses: foundry-rs/foundry-toolchain@v1
-  #       with:
-  #         version: nightly
-
-  #     - name: Install `setuptools`
-  #       run: pip install setuptools
-
-  #     - name: Install Halmos
-  #       run: pip install git+https://github.com/a16z/halmos.git@main
-
-  #     - name: Show the Halmos version
-  #       run: halmos --version
-
-  #     - name: Run Halmos symbolic tests
-  #       run: halmos --contract TestMessageLibIdentities --function test
-
   anvil-deploy:
     runs-on: ubuntu-latest
     permissions:

script/fv.yml

@@ -0,0 +1,43 @@
+name: "FV"
+
+on:
+  push:
+    paths:
+      - src/misc/libraries/**
+      - test/misc/unit/libraries/**
+
+env:
+  FOUNDRY_PROFILE: ci
+
+jobs:
+  halmos:
+    runs-on: ubuntu-latest
+
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+        with:
+          submodules: recursive
+
+      - name: Setup Python
+        uses: actions/setup-python@v5
+        with:
+          python-version: 3.13
+          architecture: x64
+
+      - name: Install Foundry
+        uses: foundry-rs/foundry-toolchain@v1
+        with:
+          version: nightly
+
+      - name: Install `setuptools`
+        run: pip install setuptools
+
+      - name: Install Halmos
+        run: pip install git+https://github.com/a16z/halmos.git@main
+
+      - name: Show the Halmos version
+        run: halmos --version
+
+      - name: Run Halmos symbolic tests
+        run: halmos --match-test '^symbolic|^testSymbolic' -vv