allow ommiting latch if no operations and operation_id if <= 1 operat…

…ions

airgen/src/lib.rs

@@ -74,8 +74,8 @@ pub fn compile<T: FieldElement>(input: AnalysisASMFile<T>) -> PILGraph<T> {
     PILGraph {
         main: ast::object::Machine {
             location: main_location,
-            latch: main_ty.latch.clone().unwrap(),
-            operation_id: main_ty.operation_id.clone().unwrap(),
+            latch: main_ty.latch.clone(),
+            operation_id: main_ty.operation_id.clone(),
         },
         entry_points: main_ty
             .operations()
@@ -129,8 +129,6 @@ impl<'a, T: FieldElement> ASMPILConverter<'a, T> {
 
         // machines should only have constraints, operations and links at this point
         assert!(input.instructions.is_empty());
-        assert!(input.latch.is_some());
-        assert!(input.operation_id.is_some());
         assert!(input.registers.is_empty());
         assert!(input.callable.is_only_operations());
 
@@ -186,8 +184,8 @@ impl<'a, T: FieldElement> ASMPILConverter<'a, T> {
                 .map(|d| LinkTo {
                     machine: ast::object::Machine {
                         location: instance_location,
-                        latch: instance_ty.latch.clone().unwrap(),
-                        operation_id: instance_ty.operation_id.clone().unwrap(),
+                        latch: instance_ty.latch.clone(),
+                        operation_id: instance_ty.operation_id.clone(),
                     },
                     operation: Operation {
                         name: d.name.to_string(),

analysis/src/block_enforcer.rs

@@ -7,27 +7,28 @@ use crate::utils::parse_pil_statement;
 
 pub fn enforce<T: FieldElement>(mut file: AnalysisASMFile<T>) -> AnalysisASMFile<T> {
     for machine in file.machines.values_mut() {
-        let operation_id = machine.operation_id.as_ref().unwrap();
-        let latch = machine.latch.as_ref().unwrap();
-        let last_step = "_block_enforcer_last_step";
-        let operation_id_no_change = "_operation_id_no_change";
+        if let Some(operation_id) = machine.operation_id.as_ref() {
+            let latch = machine.latch.as_ref().unwrap();
+            let last_step = "_block_enforcer_last_step";
+            let operation_id_no_change = "_operation_id_no_change";
 
-        // add the necessary embedded constraints which apply to both static and dynamic machines
-        let embedded_constraints = [
-            // inject last step
-            parse_pil_statement(&format!("col constant {last_step} = [0]* + [1]")),
-            // the operation id must be constant within a block.
-            // TODO: use an intermediate polynomial, currently it yields an error later in `analyzed`
-            parse_pil_statement(&format!("col witness {operation_id_no_change}")),
-            parse_pil_statement(&format!(
-                "{operation_id_no_change} = (1 - {last_step}) * (1 - {latch})"
-            )),
-            parse_pil_statement(&format!(
-                "{operation_id_no_change} * ({operation_id}' - {operation_id}) = 0"
-            )),
-        ];
+            // add the necessary embedded constraints which apply to both static and dynamic machines
+            let embedded_constraints = [
+                // inject last step
+                parse_pil_statement(&format!("col constant {last_step} = [0]* + [1]")),
+                // the operation id must be constant within a block.
+                // TODO: use an intermediate polynomial, currently it yields an error later in `analyzed`
+                parse_pil_statement(&format!("col witness {operation_id_no_change}")),
+                parse_pil_statement(&format!(
+                    "{operation_id_no_change} = (1 - {last_step}) * (1 - {latch})"
+                )),
+                parse_pil_statement(&format!(
+                    "{operation_id_no_change} * ({operation_id}' - {operation_id}) = 0"
+                )),
+            ];
 
-        machine.pil.extend(embedded_constraints);
+            machine.pil.extend(embedded_constraints);
+        }
     }
     file
 }

asm_to_pil/src/romgen.rs

@@ -200,7 +200,9 @@ pub fn generate_machine_rom<T: FieldElement>(
             // replace the function by an operation
             *callable.symbol = OperationSymbol {
                 start: 0,
-                id: OperationId { id: operation_id },
+                id: OperationId {
+                    id: Some(operation_id),
+                },
                 params: Params {
                     inputs: operation_inputs,
                     outputs: operation_outputs,

ast/src/object/display.rs

@@ -59,7 +59,7 @@ impl Display for Machine {
     fn fmt(&self, f: &mut Formatter<'_>) -> Result {
         write!(
             f,
-            "object at location \"{}\" with latch \"{}\" and operation_id \"{}\"",
+            "object at location \"{}\" with latch \"{:?}\" and operation_id \"{:?}\"",
             self.location, self.latch, self.operation_id
         )
     }
@@ -69,8 +69,10 @@ impl<T: Display> Display for Operation<T> {
     fn fmt(&self, f: &mut Formatter<'_>) -> Result {
         write!(
             f,
-            "operation \"{}\" with id {} with params {}",
-            self.name, self.id, self.params,
+            "operation \"{}\" with id {:?} with params {}",
+            self.name,
+            self.id.as_ref().map(|id| id.to_string()),
+            self.params,
         )
     }
 }

ast/src/object/mod.rs

@@ -72,17 +72,17 @@ pub struct Machine {
     /// the location of this instance
     pub location: Location,
     /// its latch
-    pub latch: String,
+    pub latch: Option<String>,
     /// its operation id
-    pub operation_id: String,
+    pub operation_id: Option<String>,
 }
 
 #[derive(Clone)]
 pub struct Operation<T> {
     /// the name of the operation
     pub name: String,
     /// the value of the operation id of this machine which activates this operation
-    pub id: T,
+    pub id: Option<T>,
     /// the parameters
     pub params: Params,
 }

ast/src/parsed/asm.rs

@@ -251,7 +251,7 @@ impl Params {
 #[derive(Debug, PartialEq, Eq, PartialOrd, Ord, Clone)]
 /// the operation id necessary to call this function from the outside
 pub struct OperationId<T> {
-    pub id: T,
+    pub id: Option<T>,
 }
 
 #[derive(Debug, PartialEq, Eq, Clone, PartialOrd, Ord)]

ast/src/parsed/display.rs

@@ -171,7 +171,10 @@ impl<T: Display> Display for MachineStatement<T> {
 
 impl<T: Display> Display for OperationId<T> {
     fn fmt(&self, f: &mut Formatter<'_>) -> Result {
-        write!(f, "<{}>", self.id)
+        match &self.id {
+            Some(id) => write!(f, "<{id}>"),
+            None => write!(f, ""),
+        }
     }
 }
 

backend/src/pilstark/estark.rs

@@ -113,7 +113,6 @@ impl<F: FieldElement> BackendImpl<F> for EStark {
             &setup.program,
             &pil,
             &self.params,
-            &"".to_string(),
         )
         .unwrap();
 

book/src/asm/machines.md

@@ -25,8 +25,8 @@ Constrained machines are a lower-level type of machine. They do not have registe
 They are defined by:
 - a degree, indicating the number of execution steps
 - a set of [operations](./operations.md)
-- an `operation_identifier` column, used to make constraints conditional over which function is called
-- a `latch` column, used to identify rows at which the machine can be accessed from the outside (where the inputs and outputs are passed)
+- an `operation_identifier` column, used to make constraints conditional over which function is called. It can be omitted with `_` if the machine has at most one operation.
+- a `latch` column, used to identify rows at which the machine can be accessed from the outside (where the inputs and outputs are passed). It can be omitted if the machine has no operations.
 - a set of submachines
 - a set of [links](links.md)
 

compiler/tests/asm.rs

@@ -99,6 +99,25 @@ fn single_function_vm() {
 }
 
 #[test]
+fn empty() {
+    let f = "empty.asm";
+    let i = [];
+    verify_asm::<GoldilocksField>(f, slice_to_vec(&i));
+    gen_halo2_proof(f, slice_to_vec(&i));
+    gen_estark_proof(f, slice_to_vec(&i));
+}
+
+#[test]
+fn single_operation() {
+    let f = "single_operation.asm";
+    let i = [];
+    verify_asm::<GoldilocksField>(f, slice_to_vec(&i));
+    gen_halo2_proof(f, slice_to_vec(&i));
+    gen_estark_proof(f, slice_to_vec(&i));
+}
+
+#[test]
+#[should_panic = "Witness generation failed."]
 fn empty_vm() {
     let f = "empty_vm.asm";
     let i = [];

linker/src/lib.rs

@@ -1,7 +1,5 @@
 #![deny(clippy::print_stdout)]
 
-use std::iter::once;
-
 use analysis::utils::parse_pil_statement;
 use ast::{
     object::{Location, PILGraph},
@@ -59,7 +57,7 @@ pub fn link<T: FieldElement>(graph: PILGraph<T>) -> Result<PILFile<T>, Vec<Strin
                 // the lhs is `instr_flag { inputs, outputs }`
                 let lhs = SelectedExpressions {
                     selector: Some(from.flag),
-                    expressions: once(Expression::Number(to.operation.id))
+                    expressions: to.operation.id.map(Expression::Number).into_iter()
                         .chain(
                             from.params
                                 .inputs
@@ -87,11 +85,11 @@ pub fn link<T: FieldElement>(graph: PILGraph<T>) -> Result<PILFile<T>, Vec<Strin
                 let to_namespace = to.machine.location.clone().to_string();
 
                 let rhs = SelectedExpressions {
-                    selector: Some(namespaced_reference(to_namespace.clone(), to.machine.latch)),
-                    expressions: once(namespaced_reference(
+                    selector: Some(namespaced_reference(to_namespace.clone(), to.machine.latch.unwrap())),
+                    expressions: to.machine.operation_id.map(|operation_id| namespaced_reference(
                         to_namespace.clone(),
-                        to.machine.operation_id,
-                    ))
+                        operation_id,
+                    )).into_iter()
                     .chain(
                         params
                             .inputs
@@ -115,14 +113,20 @@ pub fn link<T: FieldElement>(graph: PILGraph<T>) -> Result<PILFile<T>, Vec<Strin
                 {
                     let main_operation_id = main_operation.id;
                     let operation_id = main_machine.operation_id.clone();
-                    // call the main operation by initialising `operation_id` to that of the main operation
-                    let linker_first_step = "_linker_first_step";
-                    pil.extend([
-                        parse_pil_statement(&format!("col fixed {linker_first_step} = [1] + [0]*")),
-                        parse_pil_statement(&format!(
-                            "{linker_first_step} * ({operation_id} - {main_operation_id}) = 0"
-                        )),
-                    ]);
+                    match (operation_id, main_operation_id) {
+                        (Some(operation_id), Some(main_operation_id)) => {
+                            // call the main operation by initialising `operation_id` to that of the main operation
+                            let linker_first_step = "_linker_first_step";
+                            pil.extend([
+                                parse_pil_statement(&format!("col fixed {linker_first_step} = [1] + [0]*")),
+                                parse_pil_statement(&format!(
+                                    "{linker_first_step} * ({operation_id} - {main_operation_id}) = 0"
+                                )),
+                            ]);
+                        }
+                        (None, None) => {}
+                        _ => unreachable!()
+                    }
                 }
             }
 
@@ -166,8 +170,8 @@ mod test {
         let test_graph = |main_degree, foo_degree| PILGraph {
             main: ast::object::Machine {
                 location: Location::main(),
-                operation_id: "operation_id".into(),
-                latch: "latch".into(),
+                operation_id: Some("operation_id".into()),
+                latch: Some("latch".into()),
             },
             entry_points: vec![],
             objects: [

parser/src/powdr.lalrpop

@@ -284,7 +284,8 @@ OperationDeclaration: MachineStatement<T> = {
 }
 
 OperationId: OperationId<T> = {
-    "<" <id:FieldElement> ">" => OperationId { id },
+    "<" <id:FieldElement> ">" => OperationId { id: Some(id) },
+    => OperationId { id: None }
 }
 
 pub FunctionStatement: FunctionStatement<T> = {

test_data/asm/empty.asm

@@ -0,0 +1,7 @@
+// this cannot quite be empty yet, as we rely on fixed columns to determine the degree. TODO: change this because it's odd
+// also, for halo2 to generate a proof, we need at least one constraint.
+machine Empty {
+    col fixed A(i) { i };
+    col witness w;
+    w = w * w;
+}

test_data/asm/full_pil_constant.asm

@@ -1,8 +1,6 @@
-machine FullConstant(latch, operation_id) {
+machine FullConstant {
 	degree 2;
 
-	pol constant operation_id = [0]*;
-	pol constant latch = [1]*;
 	pol constant C = [0, 1]*;
 	col commit w;
 	w = C;

test_data/asm/single_operation.asm

@@ -0,0 +1,18 @@
+// we don't need to specify an operation_id if we have a single operation
+machine SingleOperation(latch, _) {
+    operation nothing;
+
+    // added for the same reason as in `empty.asm`
+    col fixed A(i) { i };
+    col fixed latch = [1]*;
+    col witness w;
+    w = w * w;
+}
+
+machine Main {
+    SingleOperation m;
+
+    col fixed A(i) { i };
+
+    link 1 = m.nothing;
+}

type_check/src/lib.rs

@@ -175,15 +175,16 @@ impl<T: FieldElement> TypeChecker<T> {
         let operation_id = machine.arguments.operation_id;
 
         if !registers.iter().any(|r| r.ty.is_pc()) {
-            if latch.is_none() {
+            let operation_count = callable.operation_definitions().count();
+            if operation_count > 0 && latch.is_none() {
                 errors.push(format!(
-                    "Machine {} should have a latch column as it does not have a pc",
+                    "Machine {} should have a latch column as it does not have a pc and has operations",
                     ctx
                 ));
             }
-            if operation_id.is_none() {
+            if operation_count > 1 && operation_id.is_none() {
                 errors.push(format!(
-                    "Machine {} should have an operation id column as it does not have a pc",
+                    "Machine {} should have an operation id column as it does not have a pc and has more than one operation",
                     ctx
                 ));
             }