Merge pull request #41 from reilabs/circuit-extractor

feat: full circuit extraction to Lean

.github/workflows/test.yml

@@ -28,9 +28,10 @@ jobs:
     - name: Test
       run: go test
     - name: Export circuit
-      run: ./gnark-mbu extract-circuit --output=formal-verification/FormalVerification.lean --tree-depth 30
+      run: ./gnark-mbu extract-circuit --output=formal-verification/FormalVerification.lean --tree-depth 30 --batch-size 4
     - name: Build lean project
       run: |
         cd formal-verification
+        ulimit -s 65520
         ~/.elan/bin/lake exe cache get
         ~/.elan/bin/lake build

README.md

@@ -56,8 +56,9 @@ This part explains the existing cli commands.
         3. batch-size *n* - Batch size for Merkle tree updates
 8. extract-circuit - Transpiles the circuit from gnark to Lean
     Flags:  
-        1. output *file path* - File to be written to
-        2. tree-depth *n* - Merkle tree depth
+        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
 
 ## Benchmarks
 

formal-verification/FormalVerification/Poseidon/Correctness.lean

@@ -92,27 +92,18 @@ lemma full_round_3_uncps (S C: Vector F 3) (k : Vector F 3 -> Prop):
   SemaphoreMTB.fullRound_3_3 S C k = k (full_round Constants.x5_254_3 S C) := by
   unfold SemaphoreMTB.fullRound_3_3
   unfold Gates.add
-  simp [Gates.add, sbox_uncps, mds_3_uncps, full_round]
-  apply iff_to_eq
-  have : ∀ {α} {v : Vector α 3}, vec![v[0], v[1], v[2]] = v := by
-    intro α v
-    conv => rhs; rw [←Vector.ofFn_get v]
-  rw [this]
-  congr
-  conv => rhs ; rw [←Vector.ofFn_get S]
+  simp [mds_3_uncps, sbox_uncps, full_round]
+  rw [←Vector.ofFn_get S]
+  rfl
+
 
 lemma half_round_3_uncps (S C: Vector F 3) (k : Vector F 3 -> Prop):
   SemaphoreMTB.halfRound_3_3 S C k = k (partial_round Constants.x5_254_3 S C) := by
   unfold SemaphoreMTB.halfRound_3_3
   unfold Gates.add
-  simp [Gates.add, sbox_uncps, mds_3_uncps, partial_round]
-  apply iff_to_eq
-  have : ∀ {α} {v : Vector α 3}, vec![v[0], v[1], v[2]] = v := by
-    intro α v
-    conv => rhs; rw [←Vector.ofFn_get v]
-  rw [this]
-  congr
-  conv => rhs ; rw [←Vector.ofFn_get S]
+  simp [sbox_uncps, mds_3_uncps, partial_round]
+  rw [←Vector.ofFn_get S]
+  rfl
 
 lemma partial_rounds_uncps
   {cfg : Constants}
@@ -196,24 +187,18 @@ lemma full_rounds_3_uncps
   apply full_rounds_uncps
   apply full_round_3_uncps
 
-lemma fold_vec_2 {v : Vector F 2}: vec![v[0], v[1]] = v := by
-    conv => rhs; rw [←Vector.ofFn_get v]
-
 def looped_poseidon_3 (inp : Vector F 3) (k: Vector F 3 -> Prop): Prop :=
     full_rounds_cps Constants.x5_254_3 SemaphoreMTB.fullRound_3_3 inp 0 4 fun state =>
     half_rounds_cps Constants.x5_254_3 SemaphoreMTB.halfRound_3_3 state 12 57  fun state' =>
     full_rounds_cps Constants.x5_254_3 SemaphoreMTB.fullRound_3_3 state' 183 4 k
 
-lemma fold_vec_3 {v : Vector F 3}: vec![v[0], v[1], v[2]] = v := by
-    conv => rhs; rw [←Vector.ofFn_get v]
-
 set_option maxRecDepth 2048
 
 theorem looped_poseidon_3_go (inp : Vector F 3) (k : Vector F 3 -> Prop):
     SemaphoreMTB.poseidon_3 inp k = looped_poseidon_3 inp k := by
     unfold looped_poseidon_3
     unfold SemaphoreMTB.poseidon_3
-    simp [full_rounds_cps, half_rounds_cps, getElem!, fold_vec_3, Vector.ofFn]
+    simp [full_rounds_cps, half_rounds_cps, getElem!, Vector.ofFn]
     rfl
 
 set_option maxRecDepth 512
@@ -305,4 +290,4 @@ theorem poseidon_3_correct (inp : Vector F 3) (k : Vector F 3 -> Prop):
     perm_folded_go,
     perm_folded
   ]
-  rfl
+  rfl

formal-verification/FormalVerification/SemanticEquivalence.lean

@@ -10,14 +10,20 @@ open SemaphoreMTB (F Order)
 
 variable [Fact (Nat.Prime Order)]
 
-abbrev D := 30
+abbrev D := 30 -- Tree depth
+abbrev B := 4 -- Batch sizes
+abbrev gVerifyProof := SemaphoreMTB.VerifyProof_31_30
 
 def poseidon₂ : Hash F 2 := fun a => (Poseidon.perm Constants.x5_254_3 vec![0, a.get 0, a.get 1]).get 0
 
 lemma Poseidon2_uncps (a b : F) (k : F -> Prop) : SemaphoreMTB.Poseidon2 a b k ↔ k (poseidon₂ vec![a, b]) := by
     simp [SemaphoreMTB.Poseidon2, poseidon₂, poseidon_3_correct, getElem]
     rfl
 
+/-!
+`ProofRound_uncps` proves that `SemaphoreMTB.ProofRound` is equivalent to a
+single iteration of `MerkleTree.recover_tail`
+-/
 lemma ProofRound_uncps {direction: F} {hash: F} {sibling: F} {k: F -> Prop} : 
     SemaphoreMTB.ProofRound direction hash sibling k ↔
     is_bit direction ∧ k (match Dir.nat_to_dir direction.val with
@@ -31,12 +37,18 @@ lemma ProofRound_uncps {direction: F} {hash: F} {sibling: F} {k: F -> Prop} :
         rw [Poseidon2_uncps]
     }
 
+/-!
+`proof_rounds` rewrites `SemaphoreMTB.VerifyProof_31_30` with recursion using `proof_rounds`
+-/
 def proof_rounds (Siblings : Vector F (n+1)) (PathIndices : Vector F n) (k : F -> Prop) : Prop :=
   match n with
   | Nat.zero => k Siblings.head
   | Nat.succ _ => SemaphoreMTB.ProofRound PathIndices.head Siblings.tail.head Siblings.head fun next =>
     proof_rounds (next ::ᵥ Siblings.tail.tail) PathIndices.tail k
 
+/-!
+`proof_rounds_uncps` rewrites `proof_rounds` using the corresponding operations of `MerkleTree` library
+-/
 lemma proof_rounds_uncps
   {Leaf : F}
   {Siblings : Vector F n}
@@ -54,16 +66,22 @@ lemma proof_rounds_uncps
     intros
     rfl
 
+/-!
+`VerifyProof_looped` proves that `SemaphoreMTB.VerifyProof_31_30` is identical to `proof_rounds`
+-/
 lemma VerifyProof_looped (PathIndices: Vector F D) (Siblings: Vector F (D+1)) (k: F -> Prop):
-    SemaphoreMTB.VerifyProof_31_30 Siblings PathIndices k =
+    gVerifyProof Siblings PathIndices k =
       proof_rounds Siblings PathIndices k := by
-    unfold SemaphoreMTB.VerifyProof_31_30
+    unfold gVerifyProof
     simp [proof_rounds]
     rw [←Vector.ofFn_get (v := PathIndices)]
     rw [←Vector.ofFn_get (v := Siblings)]
     rfl
 
-lemma VerifyProof_31_30_uncps {PathIndices: Vector F D} {Siblings: Vector F (D+1)} {k : F -> Prop}:
-    SemaphoreMTB.VerifyProof_31_30 (Siblings.head ::ᵥ Siblings.tail) PathIndices k ↔
+/-!
+`VerifyProof_uncps` proves that `SemaphoreMTB.VerifyProof_31_30` is identical to `MerkleTree.recover_tail`
+-/
+lemma VerifyProof_uncps {PathIndices: Vector F D} {Siblings: Vector F (D+1)} {k : F -> Prop}:
+    gVerifyProof (Siblings.head ::ᵥ Siblings.tail) PathIndices k ↔
     is_vector_binary PathIndices ∧ k (MerkleTree.recover_tail poseidon₂ (Dir.create_dir_vec PathIndices) Siblings.tail Siblings.head) := by
-    simp only [VerifyProof_looped, proof_rounds_uncps]
+    simp only [VerifyProof_looped, proof_rounds_uncps]

formal-verification/Main.lean

@@ -2,4 +2,13 @@ import ProvenZk.Binary
 import ProvenZk.Hash
 import ProvenZk.Merkle
 
+import FormalVerification
+import FormalVerification.Poseidon.Spec
+import FormalVerification.Poseidon.Correctness
+import FormalVerification.SemanticEquivalence
+
+open SemaphoreMTB (F Order)
+
+variable [Fact (Nat.Prime Order)]
+
 def main : IO Unit := pure ()

formal-verification/lakefile.lean

@@ -12,11 +12,11 @@ require ProvenZK from git
   "https://github.com/reilabs/proven-zk.git"@"v1.0.0"
 
 lean_lib FormalVerification {
+  moreLeanArgs := #["--tstack=65520", "-DmaxRecDepth=10000", "-DmaxHeartbeats=200000000"]
   -- add library configuration options here
 }
 
 @[default_target]
 lean_exe «formal-verification» {
-  moreLeanArgs := #["--tstack=1000000"]
   root := `Main
 }

go.mod

@@ -6,7 +6,7 @@ require (
 	github.com/consensys/gnark v0.8.0
 	github.com/iden3/go-iden3-crypto v0.0.13
 	github.com/prometheus/client_golang v1.14.0
-	github.com/reilabs/gnark-lean-extractor v1.1.1-0.20230905143002-6e277112c0df
+	github.com/reilabs/gnark-lean-extractor/v2 v2.1.0
 	github.com/urfave/cli/v2 v2.10.2
 )
 
@@ -21,11 +21,15 @@ require (
 	github.com/mattn/go-colorable v0.1.13 // indirect
 	github.com/mattn/go-isatty v0.0.16 // indirect
 	github.com/matttproud/golang_protobuf_extensions v1.0.1 // indirect
+	github.com/mitchellh/copystructure v1.2.0 // indirect
+	github.com/mitchellh/reflectwalk v1.0.2 // indirect
 	github.com/prometheus/client_model v0.3.0 // indirect
 	github.com/prometheus/common v0.37.0 // indirect
 	github.com/prometheus/procfs v0.8.0 // indirect
+	github.com/rogpeppe/go-internal v1.11.0 // indirect
 	github.com/russross/blackfriday/v2 v2.1.0 // indirect
 	github.com/xrash/smetrics v0.0.0-20201216005158-039620a65673 // indirect
+	golang.org/x/exp v0.0.0-20230905200255-921286631fa9 // indirect
 	google.golang.org/protobuf v1.28.1 // indirect
 	rsc.io/tmplfunc v0.0.3 // indirect
 )
@@ -40,6 +44,6 @@ require (
 	github.com/stretchr/testify v1.8.2 // indirect
 	github.com/x448/float16 v0.8.4 // indirect
 	golang.org/x/crypto v0.10.0 // indirect
-	golang.org/x/sys v0.9.0 // indirect
+	golang.org/x/sys v0.12.0 // indirect
 	gopkg.in/yaml.v3 v3.0.1 // indirect
 )

go.sum

@@ -175,6 +175,10 @@ github.com/mattn/go-isatty v0.0.16 h1:bq3VjFmv/sOjHtdEhmkEV4x1AJtvUvOJ2PFAZ5+peK
 github.com/mattn/go-isatty v0.0.16/go.mod h1:kYGgaQfpe5nmfYZH+SKPsOc2e4SrIfOl2e/yFXSvRLM=
 github.com/matttproud/golang_protobuf_extensions v1.0.1 h1:4hp9jkHxhMHkqkrB3Ix0jegS5sx/RkqARlsWZ6pIwiU=
 github.com/matttproud/golang_protobuf_extensions v1.0.1/go.mod h1:D8He9yQNgCq6Z5Ld7szi9bcBfOoFv/3dc6xSMkL2PC0=
+github.com/mitchellh/copystructure v1.2.0 h1:vpKXTN4ewci03Vljg/q9QvCGUDttBOGBIa15WveJJGw=
+github.com/mitchellh/copystructure v1.2.0/go.mod h1:qLl+cE2AmVv+CoeAwDPye/v+N2HKCj9FbZEVFJRxO9s=
+github.com/mitchellh/reflectwalk v1.0.2 h1:G2LzWKi524PWgd3mLHV8Y5k7s6XUvT0Gef6zxSIeXaQ=
+github.com/mitchellh/reflectwalk v1.0.2/go.mod h1:mSTlrgnPZtwu0c4WaC2kGObEpuNDbx0jmZXqmk4esnw=
 github.com/mmcloughlin/addchain v0.4.0 h1:SobOdjm2xLj1KkXN5/n0xTIWyZA2+s99UCY1iPfkHRY=
 github.com/mmcloughlin/addchain v0.4.0/go.mod h1:A86O+tHqZLMNO4w6ZZ4FlVQEadcoqkyU72HC5wJ4RlU=
 github.com/mmcloughlin/profile v0.1.1/go.mod h1:IhHD7q1ooxgwTgjxQYkACGA77oFTDdFVejUS1/tS/qU=
@@ -216,10 +220,11 @@ github.com/prometheus/procfs v0.6.0/go.mod h1:cz+aTbrPOrUb4q7XlbU9ygM+/jj0fzG6c1
 github.com/prometheus/procfs v0.7.3/go.mod h1:cz+aTbrPOrUb4q7XlbU9ygM+/jj0fzG6c1xBZuNvfVA=
 github.com/prometheus/procfs v0.8.0 h1:ODq8ZFEaYeCaZOJlZZdJA2AbQR98dSHSM1KW/You5mo=
 github.com/prometheus/procfs v0.8.0/go.mod h1:z7EfXMXOkbkqb9IINtpCn86r/to3BnA0uaxHdg830/4=
-github.com/reilabs/gnark-lean-extractor v1.1.1-0.20230905143002-6e277112c0df h1:aCdrzgCm8Xkxz+I35qE0vDU7AtUP9EZkmEKx4eLCuGU=
-github.com/reilabs/gnark-lean-extractor v1.1.1-0.20230905143002-6e277112c0df/go.mod h1:FuCRQ2kdpdImOzmzFUqMoCMQxn+Nol+AmzPDWlBZLA8=
+github.com/reilabs/gnark-lean-extractor/v2 v2.1.0 h1:3W+JidULH2KlJU6i3kypv8owIDN9thOBxv7upY8264o=
+github.com/reilabs/gnark-lean-extractor/v2 v2.1.0/go.mod h1:kSqrDOzPVw4WJdWBoiPlHbyuVDx39p6ksejwHydRDLY=
 github.com/rogpeppe/go-internal v1.3.0/go.mod h1:M8bDsm7K2OlrFYOpmOWEs/qY81heoFRclV5y23lUDJ4=
-github.com/rogpeppe/go-internal v1.10.0 h1:TMyTOH3F/DB16zRVcYyreMH6GnZZrwQVAoYjRBZyWFQ=
+github.com/rogpeppe/go-internal v1.11.0 h1:cWPaGQEPrBb5/AsnsZesgZZ9yb1OQ+GOISoDNXVBh4M=
+github.com/rogpeppe/go-internal v1.11.0/go.mod h1:ddIwULY96R17DhadqLgMfk9H9tvdUzkipdSkR5nkCZA=
 github.com/rs/xid v1.4.0/go.mod h1:trrq9SKmegXys3aeAKXMUTdJsYXVwGY3RLcfgqegfbg=
 github.com/rs/zerolog v1.29.0 h1:Zes4hju04hjbvkVkOhdl2HpZa+0PmVwigmo8XoORE5w=
 github.com/rs/zerolog v1.29.0/go.mod h1:NILgTygv/Uej1ra5XxGf82ZFSLk58MFGAUS2o6usyD0=
@@ -273,6 +278,8 @@ golang.org/x/exp v0.0.0-20191227195350-da58074b4299/go.mod h1:2RIsYlXP63K8oxa1u0
 golang.org/x/exp v0.0.0-20200119233911-0405dc783f0a/go.mod h1:2RIsYlXP63K8oxa1u096TMicItID8zy7Y6sNkU49FU4=
 golang.org/x/exp v0.0.0-20200207192155-f17229e696bd/go.mod h1:J/WKrq2StrnmMY6+EHIKF9dgMWnmCNThgcyBT1FY9mM=
 golang.org/x/exp v0.0.0-20200224162631-6cc2880d07d6/go.mod h1:3jZMyOhIsHpP37uCMkUooju7aAi5cS1Q23tOzKc+0MU=
+golang.org/x/exp v0.0.0-20230905200255-921286631fa9 h1:GoHiUyI/Tp2nVkLI2mCxVkOjsbSXD66ic0XW0js0R9g=
+golang.org/x/exp v0.0.0-20230905200255-921286631fa9/go.mod h1:S2oDrQGGwySpoQPVqRShND87VCbxmc6bL1Yd2oYrm6k=
 golang.org/x/image v0.0.0-20190227222117-0694c2d4d067/go.mod h1:kZ7UVZpmo3dzQBMxlp+ypCbDeSB+sBbTgSJuh5dn5js=
 golang.org/x/image v0.0.0-20190802002840-cff245a6509b/go.mod h1:FeLwcggjj3mMvU+oOTbSwawSJRM1uh48EjtB4UJZlP0=
 golang.org/x/lint v0.0.0-20181026193005-c67002cb31c3/go.mod h1:UVdnD1Gm6xHRNCYTkRU2/jEulfH38KcIWyp/GAMgvoE=
@@ -382,8 +389,8 @@ golang.org/x/sys v0.0.0-20210927094055-39ccf1dd6fa6/go.mod h1:oPkhp1MJrh7nUepCBc
 golang.org/x/sys v0.0.0-20211216021012-1d35b9e2eb4e/go.mod h1:oPkhp1MJrh7nUepCBck5+mAzfO9JrbApNNgaTdGDITg=
 golang.org/x/sys v0.0.0-20220114195835-da31bd327af9/go.mod h1:oPkhp1MJrh7nUepCBck5+mAzfO9JrbApNNgaTdGDITg=
 golang.org/x/sys v0.0.0-20220811171246-fbc7d0a398ab/go.mod h1:oPkhp1MJrh7nUepCBck5+mAzfO9JrbApNNgaTdGDITg=
-golang.org/x/sys v0.9.0 h1:KS/R3tvhPqvJvwcKfnBHJwwthS11LRhmM5D59eEXa0s=
-golang.org/x/sys v0.9.0/go.mod h1:oPkhp1MJrh7nUepCBck5+mAzfO9JrbApNNgaTdGDITg=
+golang.org/x/sys v0.12.0 h1:CM0HF96J0hcLAwsHPJZjfdNzs0gftsLfgKt57wWHJ0o=
+golang.org/x/sys v0.12.0/go.mod h1:oPkhp1MJrh7nUepCBck5+mAzfO9JrbApNNgaTdGDITg=
 golang.org/x/term v0.0.0-20201126162022-7de9c90e9dd1/go.mod h1:bj7SfCRtBDWHUb9snDiAeCFNEtKQo2Wmx5Cou7ajbmo=
 golang.org/x/term v0.0.0-20210927222741-03fcf44c2211/go.mod h1:jbD1KX2456YbFQfuXm/mYQcufACuNUgVhRMnK/tPxf8=
 golang.org/x/text v0.0.0-20170915032832-14c0d48ead0c/go.mod h1:NqM8EUOU14njkJ3fqMW+pc6Ldnwhi/IjpwHt7yyuwOQ=

main.go

@@ -340,12 +340,14 @@ func main() {
 				Flags: []cli.Flag{
 					&cli.StringFlag{Name: "output", Usage: "Output file", Required: true},
 					&cli.UintFlag{Name: "tree-depth", Usage: "Merkle tree depth", Required: true},
+					&cli.UintFlag{Name: "batch-size", Usage: "Batch size", Required: true},
 				},
 				Action: func(context *cli.Context) error {
 					path := context.String("output")
 					treeDepth := uint32(context.Uint("tree-depth"))
+					batchSize := uint32(context.Uint("batch-size"))
 					logging.Logger().Info().Msg("Extracting gnark circuit to Lean")
-					circuit_string, err := prover.ExtractLean(treeDepth)
+					circuit_string, err := prover.ExtractLean(treeDepth, batchSize)
 					if err != nil {
 						return err
 					}