From 400f2b68954d5f409ac3447bc79b5259b1d72820 Mon Sep 17 00:00:00 2001 From: Franklin Delehelle Date: Mon, 22 Jan 2024 11:38:38 +0100 Subject: [PATCH] refactor: homogeneize column types proving --- src/compiler/parser.rs | 10 +----- src/inspect/mod.rs | 2 +- src/transformer/inverses.rs | 3 +- src/transformer/nhood.rs | 62 ++++++++++++++++++------------------- 4 files changed, 33 insertions(+), 44 deletions(-) diff --git a/src/compiler/parser.rs b/src/compiler/parser.rs index ad39a3c6..2cc45e8e 100755 --- a/src/compiler/parser.rs +++ b/src/compiler/parser.rs @@ -712,14 +712,6 @@ fn parse_column_attributes(source: AstNode) -> Result { let must_prove = caps.name("Proven").is_some(); - if must_prove && raw_magma != RawMagma::Binary { - bail!( - "unprovable type {:?} for column {}", - raw_magma, - attributes.name.bright_white() - ); - } - attributes.must_prove = must_prove; attributes .t @@ -734,7 +726,7 @@ fn parse_column_attributes(source: AstNode) -> Result { })?; ColumnParser::Begin } else { - bail!("invalid type declaration: {}", kw) + bail!("invalid type declaration: {}", kw.red().bold()) } } } diff --git a/src/inspect/mod.rs b/src/inspect/mod.rs index 2aebaed9..c6e6190a 100644 --- a/src/inspect/mod.rs +++ b/src/inspect/mod.rs @@ -370,7 +370,7 @@ impl<'a> Inspector<'a> { self.current_module = (self.current_module + 1) % self.modules.len(); } - fn run(&mut self, terminal: &mut StdTerminal, settings: InspectorSettings) -> Result<()> { + fn run(&mut self, terminal: &mut StdTerminal, _settings: InspectorSettings) -> Result<()> { loop { terminal.draw(|term| self.render(term))?; if let Event::Key(key) = event::read()? { diff --git a/src/transformer/inverses.rs b/src/transformer/inverses.rs index 3525b82c..1f08c043 100644 --- a/src/transformer/inverses.rs +++ b/src/transformer/inverses.rs @@ -2,8 +2,7 @@ use std::collections::HashSet; use crate::{ column::{Column, Computation}, - compiler::{ColumnRef, Constraint, ConstraintSet, Expression, Intrinsic, Kind, Magma, Node}, - pretty::Base, + compiler::{ColumnRef, Constraint, ConstraintSet, Expression, Intrinsic, Kind, Node}, structs::Handle, }; use anyhow::*; diff --git a/src/transformer/nhood.rs b/src/transformer/nhood.rs index 25a65324..7645d483 100644 --- a/src/transformer/nhood.rs +++ b/src/transformer/nhood.rs @@ -1,4 +1,5 @@ -use anyhow::Result; +use anyhow::{bail, Result}; +use owo_colors::OwoColorize; use std::collections::HashMap; use crate::{ @@ -34,15 +35,14 @@ fn process_binarity(column_refs: &[ColumnRef], cs: &mut ConstraintSet) { fn process_nhood( module: &str, handles: &[ColumnRef], - n: u32, + modulo: usize, cs: &mut ConstraintSet, ) -> Result<()> { - let modulo = 2usize.pow(n); let _aux_id = cs.columns.insert_column_and_register( Column::builder() - .handle(Handle::new(module, format!("AUX_2_{}_HOOD", n))) + .handle(Handle::new(module, format!("AUX_{modulo}_HOOD"))) .kind(Kind::Phantom) - .t(Magma::integer(n as usize + 1)) + .t(Magma::native()) .build(), )?; cs.computations.insert( @@ -60,7 +60,7 @@ fn process_nhood( .collect::>(); let _intrld_aux_xs_id = cs.columns.insert_column_and_register( Column::builder() - .handle(Handle::new(module, format!("INTRLD_AUX_2_{}_HOOD", n))) + .handle(Handle::new(module, format!("INTRLD_AUX_{modulo}_HOOD"))) .kind(Kind::Phantom) .build(), )?; @@ -74,7 +74,7 @@ fn process_nhood( let srt_intrld_aux_xs_id = cs.columns.insert_column_and_register( Column::builder() - .handle(Handle::new(module, format!("SRT_INTRLD_AUX_2_{}_HOOD", n))) + .handle(Handle::new(module, format!("SRT_INTRLD_AUX_{modulo}_HOOD"))) .kind(Kind::Phantom) .build(), )?; @@ -103,13 +103,13 @@ fn process_nhood( .build(); cs.insert_constraint(Constraint::Vanishes { - handle: Handle::new(module, format!("2^{n}-hood-start")), + handle: Handle::new(module, format!("{modulo}-hood-start")), domain: Some(Domain::Set(vec![0])), expr: Box::new(srt_intrld_aux_xs_node.clone()), }); cs.insert_constraint(Constraint::Vanishes { - handle: Handle::new(module, format!("2^{n}-hood-end")), + handle: Handle::new(module, format!("{modulo}-hood-end")), domain: Some(Domain::Set(vec![-1])), expr: Box::new( Intrinsic::Sub.call(&[ @@ -118,13 +118,13 @@ fn process_nhood( .kind(Kind::Phantom) .base(Base::Dec) .build(), - Node::from_const((modulo - 1).try_into().unwrap()), + Node::from_const(modulo.try_into().unwrap()), ])?, ), }); cs.insert_constraint(Constraint::Vanishes { - handle: Handle::new(module, format!("2^{n}-hood-middle")), + handle: Handle::new(module, format!("{modulo}-hood-middle")), domain: None, expr: Box::new(Intrinsic::Mul.call(&[ // SRT_ILD_[i+1] - SRT_ILD_[i] @@ -145,41 +145,39 @@ fn process_nhood( pub fn validate_nhood(cs: &mut ConstraintSet) -> Result<()> { let mut binary_columns = Vec::new(); - let mut nibble_columns = HashMap::>::new(); - let mut byte_columns = HashMap::>::new(); + let mut constrained_columns = HashMap::>>::new(); for (h, c) in cs.columns.iter() { // only atomic columns (i.e. filled from traces) are of interest here - if c.kind == Kind::Atomic { + if c.kind == Kind::Atomic && c.must_prove { match c.t.rm() { - RawMagma::Binary => { - if c.must_prove { - binary_columns.push(h.clone()) - } - } - RawMagma::Nibble => nibble_columns + RawMagma::Binary => binary_columns.push(h.clone()), + _ => constrained_columns .entry(c.handle.module.to_owned()) .or_default() - .push(h.clone()), - RawMagma::Byte => byte_columns - .entry(c.handle.module.to_owned()) + .entry(c.t.bit_size() as u32) .or_default() .push(h.clone()), - _ => (), } } } + // Binary columns are a special case. As they only generate a single + // constraint and *do not create new columns* in their module. process_binarity(&binary_columns, cs); - for (module, handles) in nibble_columns.iter() { - process_nhood(module, handles, 4, cs)?; - cs.columns.set_min_len(module, 2usize.pow(4)); - } - - for (module, handles) in byte_columns.iter() { - process_nhood(module, handles, 8, cs)?; - cs.columns.set_min_len(module, 2usize.pow(8)); + for (module, columns) in dbg!(constrained_columns).iter() { + for (&bit_size, handles) in columns.iter() { + if bit_size > 16 { + bail!( + "do you really want to prove a {}-bits integer?", + bit_size.yellow().bold() + ); + } + let modulo = 2usize.pow(bit_size) - 1; + process_nhood(module, handles, modulo, cs)?; + cs.columns.set_min_len(module, modulo); + } } Ok(())