From 526599832d0dead79e50a5ca803057bafb7e9cc5 Mon Sep 17 00:00:00 2001
From: Eagle941 <8973725+Eagle941@users.noreply.github.com>
Date: Thu, 20 Jul 2023 20:56:13 +0100
Subject: [PATCH] feat: Added dynamic curve order in exported circuit (#16)

* Added dynamic curve order in exported circuit

* Print order as hex
---
 extractor/extractor.go   |  1 +
 extractor/lean_export.go | 14 +++++++-------
 2 files changed, 8 insertions(+), 7 deletions(-)

diff --git a/extractor/extractor.go b/extractor/extractor.go
index 036fac3..d54e040 100644
--- a/extractor/extractor.go
+++ b/extractor/extractor.go
@@ -147,6 +147,7 @@ type ExCircuit struct {
 	Inputs  []ExArg
 	Gadgets []ExGadget
 	Code    []App
+	Field   ecc.ID
 }
 
 type CodeExtractor struct {
diff --git a/extractor/lean_export.go b/extractor/lean_export.go
index 97099a9..52719a9 100644
--- a/extractor/lean_export.go
+++ b/extractor/lean_export.go
@@ -12,18 +12,17 @@ import (
 	"github.com/consensys/gnark/frontend/schema"
 )
 
-func ExportPrelude() string {
-	// Order could be extracted from circuit curve
-	s := `import ProvenZk.Gates
+func ExportPrelude(field ecc.ID) string {
+	s := fmt.Sprintf(`import ProvenZk.Gates
 import ProvenZk.VectorExtensions
 
 namespace Circuit
 
-def Order : ℕ := 21888242871839275222246405745257275088548364400416034343698204186575808495617
+def Order : ℕ := 0x%s
 variable [Fact (Nat.Prime Order)]
-abbrev F := ZMod Order`
+abbrev F := ZMod Order`, field.ScalarField().Text(16))
 
-	return fmt.Sprintf("%s", s)
+	return s
 }
 
 func ExportFooter() string {
@@ -46,7 +45,7 @@ func ExportCircuit(circuit ExCircuit) string {
 		gadgets[i] = ExportGadget(gadget)
 	}
 	circ := fmt.Sprintf("def circuit %s: Prop :=\n%s", genArgs(circuit.Inputs), genCircuitBody(circuit))
-	prelude := ExportPrelude()
+	prelude := ExportPrelude(circuit.Field)
 	footer := ExportFooter()
 	return fmt.Sprintf("%s\n\n%s\n\n%s\n\n%s", prelude, strings.Join(gadgets, "\n\n"), circ, footer)
 }
@@ -176,6 +175,7 @@ func CircuitToLean(circuit abstractor.Circuit, field ecc.ID) (string, error) {
 		Inputs:  GetExArgs(circuit, schema.Fields),
 		Gadgets: api.Gadgets,
 		Code:    api.Code,
+		Field:   api.Field,
 	}
 	out := ExportCircuit(extractorCircuit)
 	return out, nil