From 15cf5d1f1bcb16c5b05a33834db292891a75afed Mon Sep 17 00:00:00 2001
From: Giuseppe <8973725+Eagle941@users.noreply.github.com>
Date: Sat, 29 Jul 2023 14:44:17 +0100
Subject: [PATCH] New readme

---
 extractor/extractor_test.go | 26 ++++++++++++++++++++
 readme.md                   | 48 ++++++++++++++++++++++++++++++++++---
 2 files changed, 71 insertions(+), 3 deletions(-)

diff --git a/extractor/extractor_test.go b/extractor/extractor_test.go
index b101b24..ad55f24 100644
--- a/extractor/extractor_test.go
+++ b/extractor/extractor_test.go
@@ -12,6 +12,32 @@ import (
 	"github.com/stretchr/testify/assert"
 )
 
+// Example: readme circuit
+type DummyCircuit struct {
+	In_1 frontend.Variable
+	In_2 frontend.Variable
+	Out  frontend.Variable
+}
+
+func (circuit *DummyCircuit) AbsDefine(api abstractor.API) error {
+	sum := api.Add(circuit.In_1, circuit.In_2)
+	api.AssertIsEqual(sum, circuit.Out)
+	return nil
+}
+
+func (circuit DummyCircuit) Define(api frontend.API) error {
+	return abstractor.Concretize(api, &circuit)
+}
+
+func TestDummyCircuit(t *testing.T) {
+	assignment := DummyCircuit{}
+	out, err := CircuitToLean(&assignment, ecc.BN254)
+	if err != nil {
+		log.Fatal(err)
+	}
+	fmt.Println(out)
+}
+
 // Example: circuit with constant parameter
 type SliceGadget struct {
 	In_1 []frontend.Variable
diff --git a/readme.md b/readme.md
index 15469ca..a72638d 100644
--- a/readme.md
+++ b/readme.md
@@ -1,7 +1,48 @@
 # `gnark-lean-extractor` library
 
+This is a transpiler from `Go` to `Lean` for arithmetic circuits. You can design your circuit in `Go` and export it to `Lean`.
+The benefit of this library is the ability to prototype circuits in a high level language and perform formal verification using `Lean`.
+
+## Example
+Here is how a simple circuit is designed using the `gnark-lean-extractor` library:
+
+```go
+type DummyCircuit struct {
+    In_1 frontend.Variable
+    In_2 frontend.Variable
+    Out  frontend.Variable
+}
+
+func (circuit *DummyCircuit) AbsDefine(api abstractor.API) error {
+    sum := api.Add(circuit.In_1, circuit.In_2)
+    api.AssertIsEqual(sum, circuit.Out)
+    return nil
+}
+```
+
+Here is how it looks like exported for `Lean`:
+
+```lean
+namespace DummyCircuit
+
+def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
+variable [Fact (Nat.Prime Order)]
+abbrev F := ZMod Order
+
+def circuit (In_1: F) (In_2: F) (Out: F): Prop :=
+    ∃gate_0, gate_0 = Gates.add In_1 In_2 ∧
+    Gates.eq gate_0 Out ∧
+    True
+
+end DummyCircuit
+```
+
+Further examples are available in `extractor/extractor_test.go` with various levels of complexity.
+
 ## How to use
-Implement the methods `AbsDefine` and `Define` for `MyCircuit` struct. Choose a curve to test the circuit on, then call the Lean extractor the following way:
+The circuit API is based on the `consensys/gnark` library with the addition of Gadgets: this makes for easy integration of existing circuits. 
+To integrate your own circuit, implement the methods `AbsDefine` and `Define` for `MyCircuit` struct. Choose a circuit curve, then call the extractor with the function `CircuitToLean`:
+
 ```go
 assignment := MyCircuit{}
 out, err := CircuitToLean(&assignment, ecc.BN254)
@@ -10,10 +51,11 @@ if err != nil {
 }
 fmt.Println(out)
 ```
+
 The curves supported match the curves present in the library `consensys/gnark`.
 
-`CircuitToLean` prints in the `stdout` the circuit to be imported in Lean4 for verification. The Lean code depends on library `proven-zk` for the representation of Gates.
+`CircuitToLean` returns a string which contains the circuit in a format readable by `Lean`. The `Lean` code depends on the library `proven-zk` for the representation of Gates, Vectors and other useful circuit verification utilities.
 
-## Windows
+## Notes
 If using Powershell, change font to `NSimSun` for correct view of all characters:
 [check this answer](https://stackoverflow.com/a/48029600)
\ No newline at end of file