From 179a06cef9954726645e561c81d648dc961b09dd Mon Sep 17 00:00:00 2001 From: Sergey Timoshin Date: Thu, 5 Jun 2025 17:50:15 +0100 Subject: [PATCH 1/2] Enable Lean formal verification steps in CI --- .github/workflows/prover-test.yml | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/.github/workflows/prover-test.yml b/.github/workflows/prover-test.yml index 1c2cab91a1..504038432e 100644 --- a/.github/workflows/prover-test.yml +++ b/.github/workflows/prover-test.yml @@ -80,13 +80,13 @@ jobs: cd prover/server go test -run TestFull -timeout 120m - # - name: Extract circuit to Lean - # run: | - # cd prover/server - # ./light-prover extract-circuit --output formal-verification/FormalVerification/Circuit.lean --tree-height=26 --compressed-accounts=8 + - name: Extract circuit to Lean + run: | + cd prover/server + ./light-prover extract-circuit --output formal-verification/FormalVerification/Circuit.lean --tree-height=26 --compressed-accounts=8 - # - name: Build lean project - # run: | - # cd prover/server/formal-verification - # ~/.elan/bin/lake exe cache get - # ~/.elan/bin/lake build + - name: Build lean project + run: | + cd prover/server/formal-verification + ~/.elan/bin/lake exe cache get + ~/.elan/bin/lake build From d9e209fa2f0319995c2192b03510cd4e53c453fa Mon Sep 17 00:00:00 2001 From: Sergey Timoshin Date: Thu, 5 Jun 2025 22:16:41 +0100 Subject: [PATCH 2/2] Update circuit extraction parameters --- .github/workflows/prover-test.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/prover-test.yml b/.github/workflows/prover-test.yml index 504038432e..3a95f6e0e7 100644 --- a/.github/workflows/prover-test.yml +++ b/.github/workflows/prover-test.yml @@ -83,7 +83,7 @@ jobs: - name: Extract circuit to Lean run: | cd prover/server - ./light-prover extract-circuit --output formal-verification/FormalVerification/Circuit.lean --tree-height=26 --compressed-accounts=8 + ./light-prover extract-circuit --output formal-verification/FormalVerification/Circuit.lean --address-tree-height 40 --compressed-accounts 8 --state-tree-height 32 - name: Build lean project run: |