From fc60d665f910ac4e49f24463967e467da1980819 Mon Sep 17 00:00:00 2001
From: Alex Kuzmin <alex.kuzmin@proton.me>
Date: Tue, 6 Aug 2024 18:03:34 +0800
Subject: [PATCH 1/2] Restore halo2 frontend compilation test

---
 src/interpreter/mod.rs       | 78 ++++++++++++++++++++++++++++++++++--
 src/parser/ast/mod.rs        | 10 ++++-
 src/plonkish/compiler/mod.rs |  4 +-
 3 files changed, 87 insertions(+), 5 deletions(-)

diff --git a/src/interpreter/mod.rs b/src/interpreter/mod.rs
index 0643c941..e6177239 100644
--- a/src/interpreter/mod.rs
+++ b/src/interpreter/mod.rs
@@ -326,8 +326,11 @@ fn get_block_stmts(stmt: &Statement<BigInt, Identifier>) -> Vec<Statement<BigInt
 
 #[cfg(test)]
 mod test {
-    use crate::plonkish::backend::halo2::Halo2Provable;
-    use halo2_proofs::halo2curves::bn256::Fr;
+    use crate::plonkish::backend::{
+        halo2::Halo2Provable,
+        halo2_legacy::{chiquito2Halo2, ChiquitoHalo2Circuit},
+    };
+    use halo2_proofs::{dev::MockProver, halo2curves::bn256::Fr};
     use std::collections::HashMap;
 
     use crate::{
@@ -404,7 +407,76 @@ mod test {
     }
 
     #[test]
-    fn test_run_halo2_prover() {
+    fn test_run_halo2_mock_prover() {
+        let code = "
+        machine fibo(signal n) (signal b: field) {
+            // n and be are created automatically as shared
+            // signals
+            signal a: field, i;
+
+            // there is always a state called initial
+            // input signals get bound to the signal
+            // in the initial state (first instance)
+            state initial {
+             signal c;
+
+             i, a, b, c <== 1, 1, 1, 2;
+
+             -> middle {
+              i', a', b', n' <== i + 1, b, c, n;
+             }
+            }
+
+            state middle {
+             signal c;
+
+             c <== a + b;
+
+             if i + 1 == n {
+              -> final {
+               i', b', n' <== i + 1, c, n;
+              }
+             } else {
+              -> middle {
+               i', a', b', n' <== i + 1, b, c, n;
+              }
+             }
+            }
+
+            // There is always a state called final.
+            // Output signals get automatically bound to the signals
+            // with the same name in the final step (last instance).
+            // This state can be implicit if there are no constraints in it.
+           }
+        ";
+
+        let chiquito =
+            compile_legacy::<Fr>(code, Config::default(), &DebugSymRefFactory::new("", code))
+                .unwrap();
+
+        let plonkish = chiquito.plonkish(config(
+            SingleRowCellManager {},
+            SimpleStepSelectorBuilder {},
+        ));
+
+        let compiled = chiquito2Halo2(plonkish.circuit);
+
+        let circuit = ChiquitoHalo2Circuit::new(
+            compiled,
+            plonkish
+                .assignment_generator
+                .map(|g| g.generate(HashMap::from([("n".to_string(), Fr::from(12))]))),
+        );
+
+        let prover = MockProver::<Fr>::run(10, &circuit, circuit.instance()).unwrap();
+
+        let result = prover.verify();
+
+        assert!(result.is_ok());
+    }
+
+    #[test]
+    fn test_run_halo2_middleware_prover() {
         let code = "
         machine fibo(signal n) (signal b: field) {
             // n and be are created automatically as shared
diff --git a/src/parser/ast/mod.rs b/src/parser/ast/mod.rs
index 9a855436..c64e2665 100644
--- a/src/parser/ast/mod.rs
+++ b/src/parser/ast/mod.rs
@@ -142,7 +142,14 @@ impl PartialEq for DebugSymRef {
 }
 
 #[derive(Clone, PartialEq, Eq)]
-pub struct Identifier(pub String, pub i32, pub DebugSymRef);
+pub struct Identifier(
+    /// Name
+    pub String,
+    /// Rotation
+    pub i32,
+    /// Debug symbol reference
+    pub DebugSymRef,
+);
 impl Identifier {
     pub(crate) fn new<S: AsRef<str>>(value: S, dsym: DebugSymRef) -> Self {
         let value_str = value.as_ref();
@@ -153,6 +160,7 @@ impl Identifier {
         self.2.clone()
     }
 
+    /// Increase the rotation by one
     pub(crate) fn next(&self) -> Self {
         Self(self.0.clone(), self.1 + 1, self.2.clone())
     }
diff --git a/src/plonkish/compiler/mod.rs b/src/plonkish/compiler/mod.rs
index 5646728f..2e062764 100644
--- a/src/plonkish/compiler/mod.rs
+++ b/src/plonkish/compiler/mod.rs
@@ -5,7 +5,9 @@ use crate::{
         Circuit, Column, Poly, PolyExpr, PolyLookup,
     },
     poly::Expr,
-    sbpir::{query::Queriable, ExposeOffset, StepType, StepTypeUUID, PIR, SBPIRLegacy as astCircuit},
+    sbpir::{
+        query::Queriable, ExposeOffset, SBPIRLegacy as astCircuit, StepType, StepTypeUUID, PIR,
+    },
     wit_gen::{AutoTraceGenerator, FixedAssignment, TraceGenerator},
 };
 use std::hash::Hash;

From 83abc0572f2deba9e2145a70ebc08ce7ec429a4b Mon Sep 17 00:00:00 2001
From: Alex Kuzmin <alex.kuzmin@proton.me>
Date: Tue, 6 Aug 2024 18:29:05 +0800
Subject: [PATCH 2/2] Fix formatting

---
 src/frontend/dsl/mod.rs       | 2 +-
 src/plonkish/compiler/unit.rs | 4 ++--
 src/wit_gen.rs                | 2 +-
 3 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/frontend/dsl/mod.rs b/src/frontend/dsl/mod.rs
index acd888b2..6710b114 100644
--- a/src/frontend/dsl/mod.rs
+++ b/src/frontend/dsl/mod.rs
@@ -1,6 +1,6 @@
 use crate::{
     field::Field,
-    sbpir::{query::Queriable, ExposeOffset, StepType, StepTypeUUID, PIR, SBPIRLegacy},
+    sbpir::{query::Queriable, ExposeOffset, SBPIRLegacy, StepType, StepTypeUUID, PIR},
     util::{uuid, UUID},
     wit_gen::{FixedGenContext, StepInstance, TraceGenerator},
 };
diff --git a/src/plonkish/compiler/unit.rs b/src/plonkish/compiler/unit.rs
index f74dbf84..49f4cae8 100644
--- a/src/plonkish/compiler/unit.rs
+++ b/src/plonkish/compiler/unit.rs
@@ -6,8 +6,8 @@ use halo2_proofs::plonk::{Advice, Column as Halo2Column};
 use crate::{
     plonkish::ir::{assignments::Assignments, Circuit, Column, ColumnType, Poly, PolyLookup},
     sbpir::{
-        FixedSignal, ForwardSignal, ImportedHalo2Advice, ImportedHalo2Fixed, SharedSignal,
-        StepType, StepTypeUUID, SBPIRLegacy as astCircuit,
+        FixedSignal, ForwardSignal, ImportedHalo2Advice, ImportedHalo2Fixed,
+        SBPIRLegacy as astCircuit, SharedSignal, StepType, StepTypeUUID,
     },
     util::{uuid, UUID},
     wit_gen::TraceGenerator,
diff --git a/src/wit_gen.rs b/src/wit_gen.rs
index 36d0d1ef..6e1cd107 100644
--- a/src/wit_gen.rs
+++ b/src/wit_gen.rs
@@ -4,7 +4,7 @@ use crate::{
     field::Field,
     frontend::dsl::StepTypeHandler,
     poly::Expr,
-    sbpir::{query::Queriable, ForwardSignal, InternalSignal, StepTypeUUID, PIR, SBPIRLegacy},
+    sbpir::{query::Queriable, ForwardSignal, InternalSignal, SBPIRLegacy, StepTypeUUID, PIR},
     util::UUID,
 };