diff --git a/airgen/src/lib.rs b/airgen/src/lib.rs index 19bd7b65f7..9532291e4e 100644 --- a/airgen/src/lib.rs +++ b/airgen/src/lib.rs @@ -74,8 +74,8 @@ pub fn compile(input: AnalysisASMFile) -> PILGraph { 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(), diff --git a/analysis/src/block_enforcer.rs b/analysis/src/block_enforcer.rs index b86fc20cb5..4598740aab 100644 --- a/analysis/src/block_enforcer.rs +++ b/analysis/src/block_enforcer.rs @@ -7,27 +7,28 @@ use crate::utils::parse_pil_statement; pub fn enforce(mut file: AnalysisASMFile) -> AnalysisASMFile { 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 } diff --git a/asm_to_pil/src/romgen.rs b/asm_to_pil/src/romgen.rs index 02d2b38ac5..2b673420f1 100644 --- a/asm_to_pil/src/romgen.rs +++ b/asm_to_pil/src/romgen.rs @@ -200,7 +200,9 @@ pub fn generate_machine_rom( // 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, diff --git a/ast/src/object/display.rs b/ast/src/object/display.rs index 0b114e76e3..5b920fe67c 100644 --- a/ast/src/object/display.rs +++ b/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 Display for Operation { 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, ) } } diff --git a/ast/src/object/mod.rs b/ast/src/object/mod.rs index c4447927ed..c5d537e5e0 100644 --- a/ast/src/object/mod.rs +++ b/ast/src/object/mod.rs @@ -72,9 +72,9 @@ pub struct Machine { /// the location of this instance pub location: Location, /// its latch - pub latch: String, + pub latch: Option, /// its operation id - pub operation_id: String, + pub operation_id: Option, } #[derive(Clone)] @@ -82,7 +82,7 @@ pub struct Operation { /// 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, /// the parameters pub params: Params, } diff --git a/ast/src/parsed/asm.rs b/ast/src/parsed/asm.rs index 7420d7a536..ab92e06b12 100644 --- a/ast/src/parsed/asm.rs +++ b/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 { - pub id: T, + pub id: Option, } #[derive(Debug, PartialEq, Eq, Clone, PartialOrd, Ord)] diff --git a/ast/src/parsed/display.rs b/ast/src/parsed/display.rs index e4cf0706d5..a5b1fb3b26 100644 --- a/ast/src/parsed/display.rs +++ b/ast/src/parsed/display.rs @@ -171,7 +171,10 @@ impl Display for MachineStatement { impl Display for OperationId { fn fmt(&self, f: &mut Formatter<'_>) -> Result { - write!(f, "<{}>", self.id) + match &self.id { + Some(id) => write!(f, "<{id}>"), + None => write!(f, ""), + } } } diff --git a/book/src/asm/machines.md b/book/src/asm/machines.md index a97dc66f55..891cbe133e 100644 --- a/book/src/asm/machines.md +++ b/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) diff --git a/compiler/tests/asm.rs b/compiler/tests/asm.rs index 1263ce632a..a97ad36076 100644 --- a/compiler/tests/asm.rs +++ b/compiler/tests/asm.rs @@ -98,6 +98,24 @@ fn single_function_vm() { gen_estark_proof(f, slice_to_vec(&i)); } +#[test] +fn empty() { + let f = "empty.asm"; + let i = []; + verify_asm::(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::(f, slice_to_vec(&i)); + gen_halo2_proof(f, slice_to_vec(&i)); + gen_estark_proof(f, slice_to_vec(&i)); +} + #[test] fn empty_vm() { let f = "empty_vm.asm"; diff --git a/linker/src/lib.rs b/linker/src/lib.rs index dd04e720d8..3964995c4e 100644 --- a/linker/src/lib.rs +++ b/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(graph: PILGraph) -> Result, Vec(graph: PILGraph) -> Result, Vec(graph: PILGraph) -> Result, Vec { + // 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: [ diff --git a/parser/src/powdr.lalrpop b/parser/src/powdr.lalrpop index d96319a8d4..72ce5c1818 100644 --- a/parser/src/powdr.lalrpop +++ b/parser/src/powdr.lalrpop @@ -284,7 +284,8 @@ OperationDeclaration: MachineStatement = { } OperationId: OperationId = { - "<" ">" => OperationId { id }, + "<" ">" => OperationId { id: Some(id) }, + => OperationId { id: None } } pub FunctionStatement: FunctionStatement = { diff --git a/test_data/asm/empty.asm b/test_data/asm/empty.asm new file mode 100644 index 0000000000..f98bc1085b --- /dev/null +++ b/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; +} \ No newline at end of file diff --git a/test_data/asm/full_pil_constant.asm b/test_data/asm/full_pil_constant.asm index d8b8031e90..5c2891829c 100644 --- a/test_data/asm/full_pil_constant.asm +++ b/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; diff --git a/test_data/asm/single_operation.asm b/test_data/asm/single_operation.asm new file mode 100644 index 0000000000..0f859f3198 --- /dev/null +++ b/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; +} \ No newline at end of file diff --git a/type_check/src/lib.rs b/type_check/src/lib.rs index 81e810e3e8..0616f93627 100644 --- a/type_check/src/lib.rs +++ b/type_check/src/lib.rs @@ -175,15 +175,16 @@ impl TypeChecker { 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 )); }