fix merge conflict

.github/workflows/test.yml

@@ -3,13 +3,33 @@ on: push
 jobs:
  build-and-test:
  runs-on: ubuntu-latest
+ timeout-minutes: 600
  steps:
- - uses: actions/checkout@v2
- - name: Set up Go
- uses: actions/setup-go@v2
- with:
- go-version: 1.20.3
- - name: Build
- run: go build
- - name: Test
- run: go test
+ - name: Checkout repo
+ uses: actions/checkout@v3
+ with:
+ fetch-depth: 0
+ - name: Install Elan
+ run: |
+ curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y -v --default-toolchain leanprover/lean4:nightly-2023-07-12
+ echo "LAKE_VERSION=$(~/.elan/bin/lake --version)" >> $GITHUB_ENV
+ - name: Cache dependencies
+ uses: actions/cache@v3
+ with:
+ path: formal-verification/lake-packages
+ key: "${{ env.LAKE_VERSION }}"
+ - name: Set up Go
+ uses: actions/setup-go@v4
+ with:
+ go-version-file: './go.mod'
+ - name: Build
+ run: go build
+ - name: Test
+ run: go test
+ - name: Export circuit
+ run: ./gnark-mbu extract-circuit --output=formal-verification/FormalVerification.lean
+ - name: Build lean project
+ run: |
+ cd formal-verification
+ ~/.elan/bin/lake exe cache get
+ ~/.elan/bin/lake build

.gitignore

@@ -1,3 +1,10 @@
 .idea
 out
 gnark-mbu
+gnark-mbu.exe
+
+formal-verification/build
+formal-verification/.cache
+formal-verification/lean-packages/*
+formal-verification/lake-packages/*
+!formal-verification/lake-manifest.json

README.md

@@ -54,6 +54,9 @@ This part explains the existing cli commands.
  1. output *file path* - File to be writen to 
  2. tree-depth *n* - Depth of a tree 
  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 writen to
 
 ## Benchmarks
 

formal-verification/Main.lean

@@ -0,0 +1,5 @@
+import ProvenZk.Binary
+import ProvenZk.Hash
+import ProvenZk.Merkle
+
+def main : IO Unit := pure ()

formal-verification/lake-manifest.json

@@ -0,0 +1,45 @@
+{"version": 4,
+ "packagesDir": "lake-packages",
+ "packages":
+ [{"git":
+ {"url": "https://github.com/EdAyers/ProofWidgets4",
+ "subDir?": null,
+ "rev": "c43db94a8f495dad37829e9d7ad65483d68c86b8",
+ "name": "proofwidgets",
+ "inputRev?": "v0.0.11"}},
+ {"git":
+ {"url": "https://github.com/mhuisi/lean4-cli.git",
+ "subDir?": null,
+ "rev": "5a858c32963b6b19be0d477a30a1f4b6c120be7e",
+ "name": "Cli",
+ "inputRev?": "nightly"}},
+ {"git":
+ {"url": "https://github.com/reilabs/proven-zk.git",
+ "subDir?": null,
+ "rev": "08431b93eeef80f6acbf3d6a6401c02d849f6864",
+ "name": "ProvenZK",
+ "inputRev?": "v1.0.0"}},
+ {"git":
+ {"url": "https://github.com/leanprover-community/mathlib4.git",
+ "subDir?": null,
+ "rev": "ea67efc21e4e1496f0a1d954cd0c0a952523133a",
+ "name": "mathlib",
+ "inputRev?": "ea67efc21e4e1496f0a1d954cd0c0a952523133a"}},
+ {"git":
+ {"url": "https://github.com/gebner/quote4",
+ "subDir?": null,
+ "rev": "c0d9516f44d07feee01c1103c8f2f7c24a822b55",
+ "name": "Qq",
+ "inputRev?": "master"}},
+ {"git":
+ {"url": "https://github.com/JLimperg/aesop",
+ "subDir?": null,
+ "rev": "f04538ab6ad07642368cf11d2702acc0a9b4bcee",
+ "name": "aesop",
+ "inputRev?": "master"}},
+ {"git":
+ {"url": "https://github.com/leanprover/std4",
+ "subDir?": null,
+ "rev": "dff883c55395438ae2a5c65ad5ddba084b600feb",
+ "name": "std",
+ "inputRev?": "main"}}]}

formal-verification/lakefile.lean

@@ -0,0 +1,22 @@
+import Lake
+open Lake DSL
+
+package «formal-verification» {
+ -- add package configuration options here
+}
+
+require mathlib from git
+ "https://github.com/leanprover-community/mathlib4.git"@"ea67efc21e4e1496f0a1d954cd0c0a952523133a"
+
+require ProvenZK from git
+ "https://github.com/reilabs/proven-zk.git"@"v1.0.0"
+
+lean_lib FormalVerification {
+ -- add library configuration options here
+}
+
+@[default_target]
+lean_exe «formal-verification» {
+ moreLeanArgs := #["--tstack=1000000"]
+ root := `Main
+}

formal-verification/lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:nightly-2023-07-12

main.go

@@ -335,6 +335,32 @@ func main() {
  return nil
  },
  },
+ {
+ Name: "extract-circuit",
+ Flags: []cli.Flag{
+ &cli.StringFlag{Name: "output", Usage: "Output file", Required: true},
+ },
+ Action: func(context *cli.Context) error {
+ path := context.String("output")
+ logging.Logger().Info().Msg("Extracting gnark circuit to Lean")
+ circuit_string, err := prover.ExtractLean()
+ if err != nil {
+ return err
+ }
+ file, err := os.Create(path)
+ defer file.Close()
+ if err != nil {
+ return err
+ }
+ written, err := file.WriteString(circuit_string)
+ if err != nil {
+ return err
+ }
+ logging.Logger().Info().Int("bytesWritten", written).Msg("Lean circuit written to file")
+
+ return nil
+ },
+ },
  },
  }
 

prover/insertion_proving_system.go

@@ -93,6 +93,10 @@ func SetupInsertion(treeDepth uint32, batchSize uint32) (*ProvingSystem, error)
  return &ProvingSystem{treeDepth, batchSize, pk, vk, ccs}, nil
 }
 
+func ExtractLean() (string, error) {
+ return "", nil
+}
+
 func (ps *ProvingSystem) ProveInsertion(params *InsertionParameters) (*Proof, error) {
  if err := params.ValidateShape(ps.TreeDepth, ps.BatchSize); err != nil {
  return nil, err