From 985482062e517305a6aa110303a105baf1b3f707 Mon Sep 17 00:00:00 2001 From: chriseth Date: Tue, 30 May 2023 20:53:36 +0200 Subject: [PATCH 1/2] Allow literal numbers as instruction parameters. --- pilgen/src/lib.rs | 113 ++++++++++++++++++++++++++++++++++++++++------ 1 file changed, 98 insertions(+), 15 deletions(-) diff --git a/pilgen/src/lib.rs b/pilgen/src/lib.rs index 02f867042..03663a085 100644 --- a/pilgen/src/lib.rs +++ b/pilgen/src/lib.rs @@ -235,7 +235,13 @@ impl ASMPILConverter { .params .into_iter() .map(|param| match param.ty { - Some(ty) if ty == "label" => Input::Label(param.name), + Some(ty) if ty == "label" => Input::Literal(param.name, LiteralKind::Label), + Some(ty) if ty == "signed" => { + Input::Literal(param.name, LiteralKind::SignedConstant) + } + Some(ty) if ty == "unsigned" => { + Input::Literal(param.name, LiteralKind::UnsignedConstant) + } None => Input::Register(param.name), Some(ty) => panic!("param type must be nothing or label, found `{ty}`"), }) @@ -258,12 +264,11 @@ impl ASMPILConverter { let instr = Instruction { inputs, outputs }; let substitutions = instr - .labels() - .map(|label| { - // label - let param_col_name = format!("instr_{name}_param_{label}"); + .literal_arg_names() + .map(|arg_name| { + let param_col_name = format!("instr_{name}_param_{arg_name}"); self.create_witness_fixed_pair(start, ¶m_col_name); - (label.clone(), param_col_name) + (arg_name.clone(), param_col_name) }) .collect(); @@ -366,9 +371,34 @@ impl ASMPILConverter { assert!(!value.contains_key(reg)); value.insert(reg.clone(), self.process_assignment_value(a)); } - Input::Label(_) => { + Input::Literal(_, LiteralKind::Label) => { if let Expression::PolynomialReference(r) = a { - instruction_literal_arg.push(r.name); + instruction_literal_arg + .push(InstructionLiteralArg::LabelRef(r.name)); + } else { + panic!(); + } + } + Input::Literal(_, LiteralKind::UnsignedConstant) => { + // TODO evaluate expression + if let Expression::Number(n) = a { + // TODO check that it is not too large. + instruction_literal_arg.push(InstructionLiteralArg::Number(n)); + } else { + panic!(); + } + } + Input::Literal(_, LiteralKind::SignedConstant) => { + // TODO evaluate expression + if let Expression::Number(n) = a { + instruction_literal_arg.push(InstructionLiteralArg::Number(n)); + } else if let Expression::UnaryOperation(UnaryOperator::Minus, expr) = a + { + if let Expression::Number(n) = *expr { + instruction_literal_arg.push(InstructionLiteralArg::Number(-n)); + } else { + panic!(); + } } else { panic!(); } @@ -623,11 +653,16 @@ impl ASMPILConverter { for (arg, param) in line .instruction_literal_args .iter() - .zip(self.instructions[instr].labels()) + .zip(self.instructions[instr].literal_arg_names()) { program_constants .get_mut(&format!("p_instr_{instr}_param_{}", param.clone())) - .unwrap()[i] = (label_positions[arg] as u64).into(); + .unwrap()[i] = match arg { + InstructionLiteralArg::LabelRef(name) => { + (label_positions[name] as u64).into() + } + InstructionLiteralArg::Number(n) => *n, + }; } } else { assert!(line.instruction_literal_args.is_empty()); @@ -743,7 +778,13 @@ impl Register { enum Input { Register(String), - Label(String), + Literal(String, LiteralKind), +} + +enum LiteralKind { + Label, + SignedConstant, + UnsignedConstant, } struct Instruction { @@ -752,9 +793,9 @@ struct Instruction { } impl Instruction { - fn labels(&self) -> impl Iterator { + fn literal_arg_names(&self) -> impl Iterator { self.inputs.iter().filter_map(|input| match input { - Input::Label(label) => Some(label), + Input::Literal(name, _) => Some(name), _ => None, }) } @@ -771,8 +812,7 @@ struct CodeLine { value: BTreeMap)>>, label: Option, instruction: Option, - // TODO we only support labels for now. - instruction_literal_args: Vec, + instruction_literal_args: Vec>, } enum AffineExpressionComponent { @@ -781,6 +821,11 @@ enum AffineExpressionComponent { FreeInput(Expression), } +enum InstructionLiteralArg { + LabelRef(String), + Number(T), +} + fn witness_column, T>( start: usize, name: S, @@ -999,4 +1044,42 @@ pol constant p_reg_write_X_CNT = [1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; let pil = compile::(Some(file_name), &contents).unwrap(); assert_eq!(format!("{pil}").trim(), expectation.trim()); } + + #[test] + pub fn compile_literal_number_args() { + let source = r#" +reg pc[@pc]; +reg fp; + +instr inc_fp amount: unsigned { fp' = fp + amount } +instr adjust_fp amount: signed, t: label { fp' = fp + amount, pc' = label } + +inc_fp 7; +loop:: +adjust_fp -2, loop; +"#; + let expectation = r#" +namespace Assembly(1024); +pol constant first_step = [1] + [0]*; +pol commit pc; +(first_step * fp) = 0; +pol commit fp; +pol commit instr_inc_fp; +pol commit instr_inc_fp_param_amount; +pol commit instr_adjust_fp; +pol commit instr_adjust_fp_param_amount; +pol commit instr_adjust_fp_param_t; +fp' = ((((first_step' * 0) + (instr_inc_fp * (fp + instr_inc_fp_param_amount))) + (instr_adjust_fp * (fp + instr_adjust_fp_param_amount))) + ((1 - ((first_step' + instr_inc_fp) + instr_adjust_fp)) * fp)); +pc' = ((1 - first_step') * ((instr_adjust_fp * label) + ((1 - instr_adjust_fp) * (pc + 1)))); +pol constant p_line = [0, 1, 2] + [2]*; +pol constant p_instr_adjust_fp = [0, 0, 1] + [1]*; +pol constant p_instr_adjust_fp_param_amount = [0, 0, -2] + [-2]*; +pol constant p_instr_adjust_fp_param_t = [0, 0, 1] + [1]*; +pol constant p_instr_inc_fp = [1, 0, 0] + [0]*; +pol constant p_instr_inc_fp_param_amount = [7, 0, 0] + [0]*; +{ pc, instr_inc_fp, instr_inc_fp_param_amount, instr_adjust_fp, instr_adjust_fp_param_amount, instr_adjust_fp_param_t } in { p_line, p_instr_inc_fp, p_instr_inc_fp_param_amount, p_instr_adjust_fp, p_instr_adjust_fp_param_amount, p_instr_adjust_fp_param_t }; +"#; + let pil = compile::(None, source).unwrap(); + assert_eq!(format!("{pil}").trim(), expectation.trim()); + } } From ff827b0985c4e0d856d4b0fca4577e951c260154 Mon Sep 17 00:00:00 2001 From: chriseth Date: Tue, 30 May 2023 21:49:30 +0200 Subject: [PATCH 2/2] Test for negative. --- number/src/goldilocks.rs | 11 +++++++++++ number/src/macros.rs | 10 +++++++--- number/src/traits.rs | 4 ++++ pilgen/src/lib.rs | 16 +++++++++++++++- 4 files changed, 37 insertions(+), 4 deletions(-) diff --git a/number/src/goldilocks.rs b/number/src/goldilocks.rs index 76ab65f2c..6ecfc72c5 100644 --- a/number/src/goldilocks.rs +++ b/number/src/goldilocks.rs @@ -34,6 +34,17 @@ mod test { assert_eq!(n ^ p, n_xor_p); } + #[test] + fn lower_half() { + let x = GoldilocksField::from(0); + assert!(x.is_in_lower_half()); + assert!(!(x - 1.into()).is_in_lower_half()); + + let y = GoldilocksField::from_str_radix("7fffffff80000000", 16).unwrap(); + assert!(y.is_in_lower_half()); + assert!(!(y + 1.into()).is_in_lower_half()); + } + #[test] #[should_panic] fn integer_div_by_zero() { diff --git a/number/src/macros.rs b/number/src/macros.rs index 78e888502..e3489bb78 100644 --- a/number/src/macros.rs +++ b/number/src/macros.rs @@ -285,6 +285,10 @@ macro_rules! powdr_field { .into(), } } + + fn is_in_lower_half(&self) -> bool { + self.to_integer().value <= <$ark_type>::MODULUS_MINUS_ONE_DIV_TWO + } } impl From<$ark_type> for $name { @@ -351,12 +355,12 @@ macro_rules! powdr_field { impl fmt::Display for $name { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { let value = self.to_integer().value; - if value > <$ark_type>::MODULUS_MINUS_ONE_DIV_TWO { + if self.is_in_lower_half() { + write!(f, "{value}") + } else { let mut res = Self::modulus(); assert!(!res.value.sub_with_borrow(&value)); write!(f, "-{}", res) - } else { - write!(f, "{value}") } } } diff --git a/number/src/traits.rs b/number/src/traits.rs index 323c39faa..1b49749f4 100644 --- a/number/src/traits.rs +++ b/number/src/traits.rs @@ -80,6 +80,10 @@ pub trait FieldElement: fn from_str(s: &str) -> Self; fn from_str_radix(s: &str, radix: u32) -> Result; + + /// Returns true if the value is in the "lower half" of the field, + /// i.e. the value <= (modulus() - 1) / 2 + fn is_in_lower_half(&self) -> bool; } #[cfg(test)] diff --git a/pilgen/src/lib.rs b/pilgen/src/lib.rs index 03663a085..9ec7607d4 100644 --- a/pilgen/src/lib.rs +++ b/pilgen/src/lib.rs @@ -382,7 +382,7 @@ impl ASMPILConverter { Input::Literal(_, LiteralKind::UnsignedConstant) => { // TODO evaluate expression if let Expression::Number(n) = a { - // TODO check that it is not too large. + assert!(n.is_in_lower_half(), "Number passed to unsigned parameter is negative or too large: {n}"); instruction_literal_arg.push(InstructionLiteralArg::Number(n)); } else { panic!(); @@ -1082,4 +1082,18 @@ pol constant p_instr_inc_fp_param_amount = [7, 0, 0] + [0]*; let pil = compile::(None, source).unwrap(); assert_eq!(format!("{pil}").trim(), expectation.trim()); } + + #[test] + #[should_panic] + pub fn negative_for_unsigned() { + let source = r#" +reg pc[@pc]; +reg fp; + +instr instro x: unsigned { pc' = pc + x } + +instro 9223372034707292161; +"#; + compile::(None, source).unwrap(); + } }