From 21fbec833b0969d66c90688cf9a2228aa7e76da2 Mon Sep 17 00:00:00 2001 From: Leo Alt Date: Fri, 9 Aug 2024 14:46:13 +0200 Subject: [PATCH 1/4] baby bear --- cli/src/main.rs | 4 +- cli/src/util.rs | 1 + number/Cargo.toml | 14 +- number/src/baby_bear.rs | 467 ++++++++++++++++++++++++++++++++++++++++ number/src/lib.rs | 2 + number/src/traits.rs | 1 + riscv/src/code_gen.rs | 1 + 7 files changed, 485 insertions(+), 5 deletions(-) create mode 100644 number/src/baby_bear.rs diff --git a/cli/src/main.rs b/cli/src/main.rs index 1215844b2..455a870e8 100644 --- a/cli/src/main.rs +++ b/cli/src/main.rs @@ -8,7 +8,7 @@ use env_logger::{Builder, Target}; use log::LevelFilter; use powdr_backend::BackendType; use powdr_number::{buffered_write_file, read_polys_csv_file, CsvRenderMode}; -use powdr_number::{BigUint, Bn254Field, FieldElement, GoldilocksField}; +use powdr_number::{BabyBearField, BigUint, Bn254Field, FieldElement, GoldilocksField}; use powdr_pipeline::Pipeline; use std::io; use std::path::PathBuf; @@ -56,6 +56,8 @@ fn bind_cli_args( #[derive(Clone, EnumString, EnumVariantNames, Display)] pub enum FieldArgument { + #[strum(serialize = "bb")] + Bb, #[strum(serialize = "gl")] Gl, #[strum(serialize = "bn254")] diff --git a/cli/src/util.rs b/cli/src/util.rs index 701c033d8..9a33f0bd0 100644 --- a/cli/src/util.rs +++ b/cli/src/util.rs @@ -13,6 +13,7 @@ macro_rules! clap_enum_variants { macro_rules! call_with_field { ($function:ident::<$field:ident>($($args:expr),*) ) => { match $field { + FieldArgument::Bb => $function::($($args),*), FieldArgument::Gl => $function::($($args),*), FieldArgument::Bn254 => $function::($($args),*), } diff --git a/number/Cargo.toml b/number/Cargo.toml index 989adac51..cc73cdd29 100644 --- a/number/Cargo.toml +++ b/number/Cargo.toml @@ -9,17 +9,23 @@ repository = { workspace = true } [dependencies] ark-bn254 = { version = "0.4.0", default-features = false, features = [ - "scalar_field", + "scalar_field", ] } ark-ff = "0.4.2" ark-serialize = "0.4.2" +p3-baby-bear = "0.1.0" +p3-field = "0.1.0" num-bigint = { version = "0.4.3", features = ["serde"] } num-traits = "0.2.15" csv = "1.3" -serde = { version = "1.0", default-features = false, features = ["alloc", "derive", "rc"] } +serde = { version = "1.0", default-features = false, features = [ + "alloc", + "derive", + "rc", +] } serde_with = "3.6.1" -schemars = { version = "0.8.16", features = ["preserve_order"]} -ibig = { version = "0.3.6", features = ["serde"]} +schemars = { version = "0.8.16", features = ["preserve_order"] } +ibig = { version = "0.3.6", features = ["serde"] } serde_cbor = "0.11.2" derive_more = "0.99.17" diff --git a/number/src/baby_bear.rs b/number/src/baby_bear.rs new file mode 100644 index 000000000..aac294551 --- /dev/null +++ b/number/src/baby_bear.rs @@ -0,0 +1,467 @@ +use p3_baby_bear::BabyBear; +use schemars::{ + schema::{Schema, SchemaObject}, + JsonSchema, +}; +use serde::{Deserialize, Serialize}; + +use num_traits::{ConstOne, ConstZero}; +use std::ops::{Add, AddAssign, Div, Mul, MulAssign, Neg, Not, Sub, SubAssign}; +use std::str::FromStr; +use std::{collections::BTreeSet, fmt::LowerHex}; + +use crate::{BigUint, FieldElement, KnownField, LargeInt}; +use ark_ff::{One, Zero}; + +use core::fmt::{self, Debug, Formatter}; +use core::hash::Hash; + +use p3_field::{AbstractField, Field, PrimeField32}; + +#[derive( + Debug, + Copy, + Clone, + Default, + Eq, + Hash, + PartialEq, + Ord, + PartialOrd, + Serialize, + Deserialize, + derive_more::Display, +)] +pub struct BabyBearField(pub BabyBear); + +const P: u32 = 0x78000001; +const MONTY_BITS: u32 = 32; +const MONTY_ZERO: u32 = to_monty(0); +const MONTY_ONE: u32 = to_monty(1); + +const fn to_monty(x: u32) -> u32 { + (((x as u64) << MONTY_BITS) % P as u64) as u32 +} + +impl BabyBearField { + const ORDER: u32 = P; + + #[inline(always)] + fn from_canonical_u32(n: u32) -> Self { + Self(BabyBear::from_canonical_u32(n)) + } + + #[inline] + fn to_canonical_u32(self) -> u32 { + self.0.as_canonical_u32() + } +} + +impl FieldElement for BabyBearField { + type Integer = BBLargeInt; + + const BITS: u32 = 31; + + fn to_degree(&self) -> crate::DegreeType { + self.to_canonical_u32() as u64 + } + + fn to_integer(&self) -> Self::Integer { + self.to_canonical_u32().into() + } + + #[inline] + fn modulus() -> Self::Integer { + Self::ORDER.into() + } + + fn pow(self, exp: Self::Integer) -> Self { + Self(BabyBear::exp_u64_generic( + self.0, + exp.try_into_u64().unwrap(), + )) + } + + fn to_bytes_le(&self) -> Vec { + self.to_canonical_u32().to_le_bytes().to_vec() + } + + fn from_bytes_le(bytes: &[u8]) -> Self { + let u = u32::from_le_bytes(bytes.try_into().unwrap()); + Self::from_canonical_u32(u) + } + + fn from_str_radix(s: &str, radix: u32) -> Result { + u32::from_str_radix(s, radix) + .map(Self::from_canonical_u32) + .map_err(|e| e.to_string()) + } + + fn checked_from(value: ibig::UBig) -> Option { + if value < Self::modulus().to_arbitrary_integer() { + Some(u32::try_from(value).unwrap().into()) + } else { + None + } + } + + fn is_in_lower_half(&self) -> bool { + self.to_canonical_u32() <= (Self::ORDER - 1) / 2 + } + + fn known_field() -> Option { + Some(KnownField::BabyBearField) + } + + fn try_into_i32(&self) -> Option { + Some(self.to_canonical_u32() as i32) + } +} + +impl LowerHex for BabyBearField { + fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result { + LowerHex::fmt(&self.to_canonical_u32(), f) + } +} + +impl From for BabyBearField { + fn from(b: bool) -> Self { + Self(BabyBear::from_bool(b)) + } +} + +impl From for BabyBearField { + fn from(n: i64) -> Self { + From::::from(n as u64) + } +} + +impl From for BabyBearField { + fn from(n: i32) -> Self { + From::::from(n as i64) + } +} + +impl From for BabyBearField { + fn from(n: u32) -> Self { + Self(BabyBear::from_wrapped_u32(n)) + } +} + +impl From for BabyBearField { + #[inline] + fn from(n: u64) -> Self { + Self(BabyBear::from_wrapped_u64(n)) + } +} + +impl From for BabyBearField { + fn from(n: crate::BigUint) -> Self { + u64::try_from(n).unwrap().into() + } +} + +impl From for BabyBearField { + #[inline] + fn from(n: BBLargeInt) -> Self { + n.0.into() + } +} + +impl ConstZero for BabyBearField { + // TODO This is a hack because BabyBear::new() is private. + const ZERO: Self = unsafe { Self(std::mem::transmute(MONTY_ZERO)) }; +} + +impl Zero for BabyBearField { + fn zero() -> Self { + Self(BabyBear::zero()) + } + + fn is_zero(&self) -> bool { + self.0.is_zero() + } +} + +impl ConstOne for BabyBearField { + // TODO This is a hack because BabyBear::new() is private. + const ONE: Self = unsafe { Self(std::mem::transmute(MONTY_ONE)) }; +} + +impl One for BabyBearField { + fn one() -> Self { + Self(BabyBear::one()) + } + + fn is_one(&self) -> bool { + self.to_canonical_u32() == 1 + } +} + +impl FromStr for BabyBearField { + type Err = String; + fn from_str(s: &str) -> Result { + let n = BigUint::from_str(s).map_err(|e| e.to_string())?; + let modulus = Self::modulus(); + if n >= modulus.to_arbitrary_integer() { + Err(format!("Decimal number \"{s}\" too large for field.")) + } else { + Ok(n.into()) + } + } +} + +impl Neg for BabyBearField { + type Output = Self; + + #[inline] + fn neg(self) -> Self { + Self(self.0.neg()) + } +} + +impl Add for BabyBearField { + type Output = Self; + + #[inline] + fn add(self, rhs: Self) -> Self { + Self(self.0.add(rhs.0)) + } +} + +impl AddAssign for BabyBearField { + #[inline] + fn add_assign(&mut self, rhs: Self) { + self.0.add_assign(rhs.0) + } +} + +impl Sub for BabyBearField { + type Output = Self; + + #[inline] + fn sub(self, rhs: Self) -> Self { + Self(self.0.sub(rhs.0)) + } +} + +impl SubAssign for BabyBearField { + #[inline] + fn sub_assign(&mut self, rhs: Self) { + self.0.sub_assign(rhs.0) + } +} + +impl Mul for BabyBearField { + type Output = Self; + + fn mul(self, rhs: Self) -> Self { + Self(self.0.mul(rhs.0)) + } +} + +impl MulAssign for BabyBearField { + fn mul_assign(&mut self, rhs: Self) { + self.0.mul_assign(rhs.0) + } +} + +impl Div for BabyBearField { + type Output = Self; + + fn div(self, rhs: Self) -> Self::Output { + Self(self.0.div(rhs.0)) + } +} + +impl JsonSchema for BabyBearField { + fn schema_name() -> String { + "BabyBearField".to_string() + } + + fn json_schema(gen: &mut schemars::gen::SchemaGenerator) -> Schema { + // Since BabyBear is just a wrapper around u32, use the schema for u32 + let u32_schema = gen.subschema_for::(); + + SchemaObject { + // Define the schema for BabyBearField, where field is of type BabyBear (which is u32) + instance_type: Some(schemars::schema::InstanceType::Object.into()), + object: Some(Box::new(schemars::schema::ObjectValidation { + properties: vec![("field".to_string(), u32_schema)] + .into_iter() + .collect(), + required: BTreeSet::from(["field".to_string()]), // Convert Vec to BTreeSet + ..Default::default() + })), + ..Default::default() + } + .into() + } +} + +#[derive( + Clone, + Copy, + PartialEq, + Eq, + Debug, + Default, + PartialOrd, + Ord, + Hash, + derive_more::Display, + Serialize, + Deserialize, + JsonSchema, + derive_more::Mul, + derive_more::Add, + derive_more::Sub, + derive_more::AddAssign, + derive_more::SubAssign, + derive_more::MulAssign, + derive_more::Shr, + derive_more::Shl, + derive_more::BitAnd, + derive_more::BitOr, + derive_more::BitXor, + derive_more::BitAndAssign, + derive_more::BitOrAssign, + derive_more::BitXorAssign, +)] +pub struct BBLargeInt(u32); + +impl LargeInt for BBLargeInt { + const NUM_BITS: usize = 32; + + fn to_arbitrary_integer(self) -> ibig::UBig { + self.0.into() + } + + fn num_bits(&self) -> usize { + Self::NUM_BITS - self.0.leading_zeros() as usize + } + + fn one() -> Self { + Self(1) + } + + fn is_one(&self) -> bool { + self.0 == 1 + } + + fn try_into_u64(&self) -> Option { + Some(self.0 as u64) + } + + fn try_into_u32(&self) -> Option { + Some(self.0) + } + + fn from_hex(s: &str) -> Self { + Self(u32::from_str_radix(s, 16).unwrap()) + } +} + +impl From for BBLargeInt { + fn from(value: u32) -> Self { + Self(value) + } +} + +impl From for BBLargeInt { + fn from(value: u64) -> Self { + Self(value as u32) + } +} + +impl Zero for BBLargeInt { + fn zero() -> Self { + Self(0) + } + + fn is_zero(&self) -> bool { + self.0 == 0 + } +} + +impl ConstZero for BBLargeInt { + const ZERO: Self = Self(0); +} + +impl LowerHex for BBLargeInt { + fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result { + LowerHex::fmt(&self.0, f) + } +} + +impl Not for BBLargeInt { + type Output = Self; + + fn not(self) -> Self::Output { + Self(!self.0) + } +} + +#[cfg(test)] +mod test { + use crate::traits::int_from_hex_str; + use test_log::test; + + use super::*; + + #[test] + fn bitwise() { + let n = int_from_hex_str::("00ff00ff"); + let p = int_from_hex_str::("f00ff00f"); + let not_n = int_from_hex_str::("ff00ff00"); + let n_shr_4 = int_from_hex_str::("000ff00f"); + let n_shl_4 = int_from_hex_str::("0ff00ff0"); + let n_or_p = int_from_hex_str::("f0fff0ff"); + let n_and_p = int_from_hex_str::("000f000f"); + let n_xor_p = int_from_hex_str::("f0f0f0f0"); + + assert_eq!(n.not().not(), n); + assert_eq!(n.not(), not_n); + assert_eq!(n >> 4, n_shr_4); + assert_eq!(n << 4, n_shl_4); + assert_eq!(n & p, n_and_p); + assert_eq!(n | p, n_or_p); + assert_eq!(n ^ p, n_xor_p); + } + + #[test] + fn zero_one() { + let x = BabyBearField::ZERO; + assert_eq!(x, BabyBearField::zero()); + assert_eq!(x.to_canonical_u32(), 0); + let y = BabyBearField::ONE; + assert_eq!(y, BabyBearField::one()); + assert_eq!(y.to_canonical_u32(), 1); + let z = x + y + y; + assert_eq!(z.to_canonical_u32(), 2); + } + + #[test] + fn lower_half() { + let x = BabyBearField::from(0); + assert!(x.is_in_lower_half()); + assert!(!(x - 1.into()).is_in_lower_half()); + + let y = BabyBearField::from_str_radix("3c000000", 16).unwrap(); + assert!(y.is_in_lower_half()); + assert!(!(y + 1.into()).is_in_lower_half()); + } + + #[test] + #[should_panic] + fn integer_div_by_zero() { + let _ = BabyBearField::from(1).to_arbitrary_integer() + / BabyBearField::from(0).to_arbitrary_integer(); + } + + #[test] + #[should_panic] + fn div_by_zero() { + let _ = BabyBearField::from(1) / BabyBearField::from(0); + } +} diff --git a/number/src/lib.rs b/number/src/lib.rs index 8842281c6..5634ed9c7 100644 --- a/number/src/lib.rs +++ b/number/src/lib.rs @@ -4,6 +4,7 @@ #[macro_use] mod macros; +mod baby_bear; mod bn254; mod goldilocks; mod serialize; @@ -12,6 +13,7 @@ pub use serialize::{ buffered_write_file, read_polys_csv_file, write_polys_csv_file, CsvRenderMode, ReadWrite, }; +pub use baby_bear::BabyBearField; pub use bn254::Bn254Field; pub use goldilocks::GoldilocksField; pub use traits::KnownField; diff --git a/number/src/traits.rs b/number/src/traits.rs index 34eca3071..9e894ed6a 100644 --- a/number/src/traits.rs +++ b/number/src/traits.rs @@ -64,6 +64,7 @@ pub trait LargeInt: #[derive(Debug, PartialEq, Serialize, Deserialize)] pub enum KnownField { + BabyBearField, GoldilocksField, Bn254Field, } diff --git a/riscv/src/code_gen.rs b/riscv/src/code_gen.rs index ce26ad3df..c5929a69d 100644 --- a/riscv/src/code_gen.rs +++ b/riscv/src/code_gen.rs @@ -683,6 +683,7 @@ fn mul_instruction(runtime: &Runtime) -> &'static str { link ~> regs.mstore(W, STEP + 3, tmp4_col); "# } + KnownField::BabyBearField => todo!(), } } From 9072b3e35550b8a2eceadf2c7dddab2f2b58f3e0 Mon Sep 17 00:00:00 2001 From: Leo Alt Date: Fri, 16 Aug 2024 15:05:44 +0200 Subject: [PATCH 2/4] review --- number/src/baby_bear.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/number/src/baby_bear.rs b/number/src/baby_bear.rs index aac294551..94a75d017 100644 --- a/number/src/baby_bear.rs +++ b/number/src/baby_bear.rs @@ -32,7 +32,7 @@ use p3_field::{AbstractField, Field, PrimeField32}; Deserialize, derive_more::Display, )] -pub struct BabyBearField(pub BabyBear); +pub struct BabyBearField(BabyBear); const P: u32 = 0x78000001; const MONTY_BITS: u32 = 32; From c8a658a60b02a9bef513e5343a4c9149b7f301c0 Mon Sep 17 00:00:00 2001 From: Leo Alt Date: Fri, 9 Aug 2024 14:46:13 +0200 Subject: [PATCH 3/4] baby bear test --- pipeline/src/test_util.rs | 25 ++++++++- pipeline/tests/asm.rs | 21 ++++---- pipeline/tests/powdr_std.rs | 16 +++++- std/machines/binary_bb.asm | 65 ++++++++++++++++++++++ std/machines/mod.asm | 3 +- test_data/std/binary_bb_test_16.asm | 73 +++++++++++++++++++++++++ test_data/std/binary_bb_test_8.asm | 83 +++++++++++++++++++++++++++++ 7 files changed, 272 insertions(+), 14 deletions(-) create mode 100644 std/machines/binary_bb.asm create mode 100644 test_data/std/binary_bb_test_16.asm create mode 100644 test_data/std/binary_bb_test_8.asm diff --git a/pipeline/src/test_util.rs b/pipeline/src/test_util.rs index f0f1818cd..90aa523ef 100644 --- a/pipeline/src/test_util.rs +++ b/pipeline/src/test_util.rs @@ -1,6 +1,8 @@ use powdr_ast::analyzed::Analyzed; use powdr_backend::BackendType; -use powdr_number::{buffered_write_file, BigInt, Bn254Field, FieldElement, GoldilocksField}; +use powdr_number::{ + buffered_write_file, BabyBearField, BigInt, Bn254Field, FieldElement, GoldilocksField, +}; use powdr_pil_analyzer::evaluator::{self, SymbolLookup}; use std::path::PathBuf; use std::{env, fs}; @@ -69,6 +71,27 @@ pub fn regular_test(file_name: &str, inputs: &[i32]) { let inputs_bn = inputs.iter().map(|x| Bn254Field::from(*x)).collect(); let pipeline_bn = make_prepared_pipeline(file_name, inputs_bn, vec![]); test_halo2(pipeline_bn); + + let inputs_bb = inputs.iter().map(|x| BabyBearField::from(*x)).collect(); + let mut pipeline_bb = make_prepared_pipeline(file_name, inputs_bb, vec![]); + pipeline_bb.compute_witness().unwrap(); +} + +pub fn regular_test_only_babybear(file_name: &str, inputs: &[i32]) { + let inputs_bb = inputs.iter().map(|x| BabyBearField::from(*x)).collect(); + let mut pipeline_bb = make_prepared_pipeline(file_name, inputs_bb, vec![]); + pipeline_bb.compute_witness().unwrap(); +} + +pub fn regular_test_without_babybear(file_name: &str, inputs: &[i32]) { + let inputs_gl = inputs.iter().map(|x| GoldilocksField::from(*x)).collect(); + let pipeline_gl = make_prepared_pipeline(file_name, inputs_gl, vec![]); + test_pilcom(pipeline_gl.clone()); + gen_estark_proof(pipeline_gl); + + let inputs_bn = inputs.iter().map(|x| Bn254Field::from(*x)).collect(); + let pipeline_bn = make_prepared_pipeline(file_name, inputs_bn, vec![]); + test_halo2(pipeline_bn); } pub fn test_pilcom(pipeline: Pipeline) { diff --git a/pipeline/tests/asm.rs b/pipeline/tests/asm.rs index 906290d28..7e29229be 100644 --- a/pipeline/tests/asm.rs +++ b/pipeline/tests/asm.rs @@ -6,9 +6,10 @@ use powdr_number::{Bn254Field, FieldElement, GoldilocksField}; use powdr_pipeline::{ test_util::{ asm_string_to_pil, gen_estark_proof_with_backend_variant, make_prepared_pipeline, - make_simple_prepared_pipeline, regular_test, resolve_test_file, - run_pilcom_with_backend_variant, test_halo2, test_halo2_with_backend_variant, test_pilcom, - test_plonky3_with_backend_variant, BackendVariant, + make_simple_prepared_pipeline, regular_test, regular_test_without_babybear, + resolve_test_file, run_pilcom_with_backend_variant, test_halo2, + test_halo2_with_backend_variant, test_pilcom, test_plonky3_with_backend_variant, + BackendVariant, }, util::{FixedPolySet, PolySet, WitnessPolySet}, Pipeline, @@ -292,7 +293,7 @@ fn multi_return_wrong_assignment_register_length() { fn bit_access() { let f = "asm/bit_access.asm"; let i = [20]; - regular_test(f, &i); + regular_test_without_babybear(f, &i); } #[test] @@ -305,7 +306,7 @@ fn sqrt() { fn functional_instructions() { let f = "asm/functional_instructions.asm"; let i = [20]; - regular_test(f, &i); + regular_test_without_babybear(f, &i); } #[test] @@ -387,13 +388,13 @@ fn multiple_signatures() { #[test] fn permutation_simple() { let f = "asm/permutations/simple.asm"; - regular_test(f, Default::default()); + regular_test_without_babybear(f, Default::default()); } #[test] fn permutation_to_block() { let f = "asm/permutations/vm_to_block.asm"; - regular_test(f, Default::default()); + regular_test_without_babybear(f, Default::default()); } #[test] @@ -407,7 +408,7 @@ fn permutation_to_vm() { #[test] fn permutation_to_block_to_block() { let f = "asm/permutations/block_to_block.asm"; - regular_test(f, Default::default()); + regular_test_without_babybear(f, Default::default()); } #[test] @@ -420,14 +421,14 @@ fn permutation_incoming_needs_selector() { #[test] fn call_selectors_with_no_permutation() { let f = "asm/permutations/call_selectors_with_no_permutation.asm"; - regular_test(f, Default::default()); + regular_test_without_babybear(f, Default::default()); } #[test] #[ignore = "Too slow"] fn vm_args() { let f = "asm/vm_args.asm"; - regular_test(f, Default::default()); + regular_test_without_babybear(f, Default::default()); } #[test] diff --git a/pipeline/tests/powdr_std.rs b/pipeline/tests/powdr_std.rs index 71a617582..f46f0d972 100644 --- a/pipeline/tests/powdr_std.rs +++ b/pipeline/tests/powdr_std.rs @@ -6,8 +6,8 @@ use powdr_pil_analyzer::evaluator::Value; use powdr_pipeline::{ test_util::{ evaluate_function, evaluate_integer_function, execute_test_file, gen_estark_proof, - gen_halo2_proof, make_simple_prepared_pipeline, regular_test, std_analyzed, test_halo2, - test_pilcom, BackendVariant, + gen_halo2_proof, make_simple_prepared_pipeline, regular_test, regular_test_only_babybear, + std_analyzed, test_halo2, test_pilcom, BackendVariant, }, Pipeline, }; @@ -182,6 +182,18 @@ fn binary_test() { test_halo2(make_simple_prepared_pipeline(f)); } +#[test] +fn binary_bb_8_test() { + let f = "std/binary_bb_test_8.asm"; + regular_test_only_babybear(f, &[]); +} + +#[test] +fn binary_bb_16_test() { + let f = "std/binary_bb_test_16.asm"; + regular_test_only_babybear(f, &[]); +} + #[test] #[ignore = "Too slow"] fn shift_test() { diff --git a/std/machines/binary_bb.asm b/std/machines/binary_bb.asm new file mode 100644 index 000000000..ec2ff4274 --- /dev/null +++ b/std/machines/binary_bb.asm @@ -0,0 +1,65 @@ +use std::convert::int; +use std::utils::cross_product; +use std::utils::unchanged_until; +use std::machines::binary::ByteBinary; + +// Computes bitwise operations on two 32-bit numbers +// decomposed into 4 bytes each. +machine Binary8(byte_binary: ByteBinary) with + latch: latch, + operation_id: operation_id, + // Allow this machine to be connected via a permutation + call_selectors: sel, +{ + operation and<0> A1, A2, A3, A4, B1, B2, B3, B4 -> C1, C2, C3, C4; + + operation or<1> A1, A2, A3, A4, B1, B2, B3, B4 -> C1, C2, C3, C4; + + operation xor<2> A1, A2, A3, A4, B1, B2, B3, B4 -> C1, C2, C3, C4; + + col witness operation_id; + + col fixed latch(i) { 1 }; + + col witness A1, A2, A3, A4; + col witness B1, B2, B3, B4; + col witness C1, C2, C3, C4; + + link => C1 = byte_binary.run(operation_id, A1, B1); + link => C2 = byte_binary.run(operation_id, A2, B2); + link => C3 = byte_binary.run(operation_id, A3, B3); + link => C4 = byte_binary.run(operation_id, A4, B4); +} + +// Computes bitwise operations on two 32-bit numbers +// decomposed into two 16-bit limbs each. +machine Binary16(byte_binary: ByteBinary) with + latch: latch, + operation_id: operation_id, + // Allow this machine to be connected via a permutation + call_selectors: sel, +{ + operation and<0> I1, I2, I3, I4 -> O1, O2; + operation or<1> I1, I2, I3, I4 -> O1, O2; + operation xor<2> I1, I2, I3, I4 -> O1, O2; + + col witness operation_id; + + col fixed latch(i) { 1 }; + + let I1: inter = A1 + 256 * A2; + let I2: inter = A3 + 256 * A4; + let I3: inter = B1 + 256 * B2; + let I4: inter = B3 + 256 * B4; + let O1: inter = C1 + 256 * C2; + let O2: inter = C3 + 256 * C4; + + col witness A1, A2, A3, A4; + col witness B1, B2, B3, B4; + col witness C1, C2, C3, C4; + + link => C1 = byte_binary.run(operation_id, A1, B1); + link => C2 = byte_binary.run(operation_id, A2, B2); + link => C3 = byte_binary.run(operation_id, A3, B3); + link => C4 = byte_binary.run(operation_id, A4, B4); +} diff --git a/std/machines/mod.asm b/std/machines/mod.asm index 5e0306287..d059419c1 100644 --- a/std/machines/mod.asm +++ b/std/machines/mod.asm @@ -1,9 +1,10 @@ mod arith; mod binary; +mod binary_bb; mod range; mod hash; mod memory; mod memory_with_bootloader_write; mod shift; mod split; -mod write_once_memory; \ No newline at end of file +mod write_once_memory; diff --git a/test_data/std/binary_bb_test_16.asm b/test_data/std/binary_bb_test_16.asm new file mode 100644 index 000000000..a2c2035de --- /dev/null +++ b/test_data/std/binary_bb_test_16.asm @@ -0,0 +1,73 @@ +use std::machines::binary::ByteBinary; +use std::machines::binary_bb::Binary16; + +machine Main { + reg pc[@pc]; + reg X0_1[<=]; + reg X0_2[<=]; + reg X1_1[<=]; + reg X1_2[<=]; + reg X2_1[<=]; + reg X2_2[<=]; + reg A1; + reg A2; + + ByteBinary byte_binary; + Binary16 binary(byte_binary); + + instr and X0_1, X0_2, X1_1, X1_2 -> X2_1, X2_2 link ~> (X2_1, X2_2) = binary.and(X0_1, X0_2, X1_1, X1_2); + instr or X0_1, X0_2, X1_1, X1_2 -> X2_1, X2_2 link ~> (X2_1, X2_2) = binary.or(X0_1, X0_2, X1_1, X1_2); + instr xor X0_1, X0_2, X1_1, X1_2 -> X2_1, X2_2 link ~> (X2_1, X2_2) = binary.xor(X0_1, X0_2, X1_1, X1_2); + + instr assert_eq X0_1, X0_2, X1_1, X1_2 { + X0_1 = X1_1, + X0_2 = X1_2 + } + + function main { + + // AND + A1, A2 <== and(0, 0, 0, 0); + assert_eq A1, A2, 0, 0; + A1, A2 <== and(0xffff, 0xffff, 0xffff, 0xffff); + assert_eq A1, A2, 0xffff, 0xffff; + A1, A2 <== and(0xffff, 0xffff, 0xabcd, 0xef01); + assert_eq A1, A2, 0xabcd, 0xef01; + A1, A2 <== and(0xabcd, 0xef01, 0xffff, 0xffff); + assert_eq A1, A2, 0xabcd, 0xef01; + A1, A2 <== and(0, 0, 0xabcd, 0xef01); + assert_eq A1, A2, 0, 0; + A1, A2 <== and(0xabcd, 0xef01, 0, 0); + assert_eq A1, A2, 0, 0; + + // OR + A1, A2 <== or(0, 0, 0, 0); + assert_eq A1, A2, 0, 0; + A1, A2 <== or(0xffff, 0xffff, 0xffff, 0xffff); + assert_eq A1, A2, 0xffff, 0xffff; + A1, A2 <== or(0xffff, 0xffff, 0xabcd, 0xef01); + assert_eq A1, A2, 0xffff, 0xffff; + A1, A2 <== or(0xabcd, 0xef01, 0xffff, 0xffff); + assert_eq A1, A2, 0xffff, 0xffff; + A1, A2 <== or(0, 0, 0xabcd, 0xef01); + assert_eq A1, A2, 0xabcd, 0xef01; + A1, A2 <== or(0xabcd, 0xef01, 0, 0); + assert_eq A1, A2, 0xabcd, 0xef01; + + // XOR + A1, A2 <== xor(0, 0, 0, 0); + assert_eq A1, A2, 0, 0; + A1, A2 <== xor(0xffff, 0xffff, 0xffff, 0xffff); + assert_eq A1, A2, 0, 0; + A1, A2 <== xor(0xffff, 0xffff, 0xabcd, 0xef01); + assert_eq A1, A2, 0x5432, 0x10fe; + A1, A2 <== xor(0xabcd, 0xef01, 0xffff, 0xffff); + assert_eq A1, A2, 0x5432, 0x10fe; + A1, A2 <== xor(0, 0, 0xabcd, 0xef01); + assert_eq A1, A2, 0xabcd, 0xef01; + A1, A2 <== xor(0xabcd, 0xef01, 0, 0); + assert_eq A1, A2, 0xabcd, 0xef01; + + return; + } +} diff --git a/test_data/std/binary_bb_test_8.asm b/test_data/std/binary_bb_test_8.asm new file mode 100644 index 000000000..5203d1177 --- /dev/null +++ b/test_data/std/binary_bb_test_8.asm @@ -0,0 +1,83 @@ +use std::machines::binary::ByteBinary; +use std::machines::binary_bb::Binary8; + +machine Main { + reg pc[@pc]; + reg X0_1[<=]; + reg X0_2[<=]; + reg X0_3[<=]; + reg X0_4[<=]; + reg X1_1[<=]; + reg X1_2[<=]; + reg X1_3[<=]; + reg X1_4[<=]; + reg X2_1[<=]; + reg X2_2[<=]; + reg X2_3[<=]; + reg X2_4[<=]; + reg A1; + reg A2; + reg A3; + reg A4; + + ByteBinary byte_binary; + Binary8 binary(byte_binary); + + instr and X0_1, X0_2, X0_3, X0_4, X1_1, X1_2, X1_3, X1_4 -> X2_1, X2_2, X2_3, X2_4 link ~> (X2_1, X2_2, X2_3, X2_4) = binary.and(X0_1, X0_2, X0_3, X0_4, X1_1, X1_2, X1_3, X1_4); + instr or X0_1, X0_2, X0_3, X0_4, X1_1, X1_2, X1_3, X1_4 -> X2_1, X2_2, X2_3, X2_4 link ~> (X2_1, X2_2, X2_3, X2_4) = binary.or(X0_1, X0_2, X0_3, X0_4, X1_1, X1_2, X1_3, X1_4); + instr xor X0_1, X0_2, X0_3, X0_4, X1_1, X1_2, X1_3, X1_4 -> X2_1, X2_2, X2_3, X2_4 link ~> (X2_1, X2_2, X2_3, X2_4) = binary.xor(X0_1, X0_2, X0_3, X0_4, X1_1, X1_2, X1_3, X1_4); + + instr assert_eq X0_1, X0_2, X0_3, X0_4, X1_1, X1_2, X1_3, X1_4 { + X0_1 = X1_1, + X0_2 = X1_2, + X0_3 = X1_3, + X0_4 = X1_4 + } + + function main { + + // AND + A1, A2, A3, A4 <== and(0, 0, 0, 0, 0, 0, 0, 0); + assert_eq A1, A2, A3, A4, 0, 0, 0, 0; + A1, A2, A3, A4 <== and(0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff); + assert_eq A1, A2, A3, A4, 0xff, 0xff, 0xff, 0xff; + A1, A2, A3, A4 <== and(0xff, 0xff, 0xff, 0xff, 0xab, 0xcd, 0xef, 0x01); + assert_eq A1, A2, A3, A4, 0xab, 0xcd, 0xef, 0x01; + A1, A2, A3, A4 <== and(0xab, 0xcd, 0xef, 0x01, 0xff, 0xff, 0xff, 0xff); + assert_eq A1, A2, A3, A4, 0xab, 0xcd, 0xef, 0x01; + A1, A2, A3, A4 <== and(0, 0, 0, 0, 0xab, 0xcd, 0xef, 0x01); + assert_eq A1, A2, A3, A4, 0, 0, 0, 0; + A1, A2, A3, A4 <== and(0xab, 0xcd, 0xef, 0x01, 0, 0, 0, 0); + assert_eq A1, A2, A3, A4, 0, 0, 0, 0; + + // OR + A1, A2, A3, A4 <== or(0, 0, 0, 0, 0, 0, 0, 0); + assert_eq A1, A2, A3, A4, 0, 0, 0, 0; + A1, A2, A3, A4 <== or(0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff); + assert_eq A1, A2, A3, A4, 0xff, 0xff, 0xff, 0xff; + A1, A2, A3, A4 <== or(0xff, 0xff, 0xff, 0xff, 0xab, 0xcd, 0xef, 0x01); + assert_eq A1, A2, A3, A4, 0xff, 0xff, 0xff, 0xff; + A1, A2, A3, A4 <== or(0xab, 0xcd, 0xef, 0x01, 0xff, 0xff, 0xff, 0xff); + assert_eq A1, A2, A3, A4, 0xff, 0xff, 0xff, 0xff; + A1, A2, A3, A4 <== or(0, 0, 0, 0, 0xab, 0xcd, 0xef, 0x01); + assert_eq A1, A2, A3, A4, 0xab, 0xcd, 0xef, 0x01; + A1, A2, A3, A4 <== or(0xab, 0xcd, 0xef, 0x01, 0, 0, 0, 0); + assert_eq A1, A2, A3, A4, 0xab, 0xcd, 0xef, 0x01; + + // XOR + A1, A2, A3, A4 <== xor(0, 0, 0, 0, 0, 0, 0, 0); + assert_eq A1, A2, A3, A4, 0, 0, 0, 0; + A1, A2, A3, A4 <== xor(0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff); + assert_eq A1, A2, A3, A4, 0, 0, 0, 0; + A1, A2, A3, A4 <== xor(0xff, 0xff, 0xff, 0xff, 0xab, 0xcd, 0xef, 0x01); + assert_eq A1, A2, A3, A4, 0x54, 0x32, 0x10, 0xfe; + A1, A2, A3, A4 <== xor(0xab, 0xcd, 0xef, 0x01, 0xff, 0xff, 0xff, 0xff); + assert_eq A1, A2, A3, A4, 0x54, 0x32, 0x10, 0xfe; + A1, A2, A3, A4 <== xor(0, 0, 0, 0, 0xab, 0xcd, 0xef, 0x01); + assert_eq A1, A2, A3, A4, 0xab, 0xcd, 0xef, 0x01; + A1, A2, A3, A4 <== xor(0xab, 0xcd, 0xef, 0x01, 0, 0, 0, 0); + assert_eq A1, A2, A3, A4, 0xab, 0xcd, 0xef, 0x01; + + return; + } +} From 240bd0af4fe4e55394e1917ac11902b58d561424 Mon Sep 17 00:00:00 2001 From: Leo Alt Date: Mon, 12 Aug 2024 16:49:40 +0200 Subject: [PATCH 4/4] memory with baby bear --- .../machines/double_sorted_witness_machine.rs | 153 +++++++--- std/machines/memory_bb.asm | 283 ++++++++++++++++++ std/machines/mod.asm | 1 + test_data/std/memory_bb_test.asm | 65 ++++ 4 files changed, 454 insertions(+), 48 deletions(-) create mode 100644 std/machines/memory_bb.asm create mode 100644 test_data/std/memory_bb_test.asm diff --git a/executor/src/witgen/machines/double_sorted_witness_machine.rs b/executor/src/witgen/machines/double_sorted_witness_machine.rs index 1f98e896d..f5dfb8bff 100644 --- a/executor/src/witgen/machines/double_sorted_witness_machine.rs +++ b/executor/src/witgen/machines/double_sorted_witness_machine.rs @@ -10,16 +10,18 @@ use crate::witgen::util::try_to_simple_poly; use crate::witgen::{EvalError, EvalResult, FixedData, MutableState, QueryCallback}; use crate::witgen::{EvalValue, IncompleteCause}; use crate::Identity; -use powdr_number::{DegreeType, FieldElement}; +use powdr_number::{DegreeType, FieldElement, LargeInt}; use powdr_ast::analyzed::{IdentityKind, PolyID}; /// If all witnesses of a machine have a name in this list (disregarding the namespace), /// we'll consider it to be a double-sorted machine. /// This does not include the selectors, which are dynamically added to this list. -const ALLOWED_WITNESSES: [&str; 8] = [ - "m_value", - "m_addr", +const ALLOWED_WITNESSES: [&str; 10] = [ + "m_value1", + "m_value2", + "m_addr1", + "m_addr2", "m_step", "m_change", "m_is_write", @@ -51,10 +53,9 @@ pub struct DoubleSortedWitnesses<'a, T: FieldElement> { /// Position of the witness columns in the data. /// The key column has a position of usize::max //witness_positions: HashMap, - /// (addr, step) -> value - trace: BTreeMap<(T, T), Operation>, - /// A map addr -> value, the current content of the memory. - data: BTreeMap, + /// (addr1, addr2, step) -> (value1, value2) + trace: BTreeMap<(T, T, T), Operation>, + data: BTreeMap, is_initialized: BTreeMap, namespace: String, name: String, @@ -73,7 +74,8 @@ pub struct DoubleSortedWitnesses<'a, T: FieldElement> { struct Operation { pub is_normal_write: bool, pub is_bootloader_write: bool, - pub value: T, + pub value1: T, + pub value2: T, pub selector_id: PolyID, } @@ -213,9 +215,11 @@ impl<'a, T: FieldElement> Machine<'a, T> for DoubleSortedWitnesses<'a, T> { &mut self, _mutable_state: &'b mut MutableState<'a, 'b, T, Q>, ) -> HashMap> { - let mut addr = vec![]; + let mut addr1 = vec![]; + let mut addr2 = vec![]; let mut step = vec![]; - let mut value = vec![]; + let mut value1 = vec![]; + let mut value2 = vec![]; let mut is_normal_write = vec![]; let mut is_bootloader_write = vec![]; let mut diff = vec![]; @@ -234,17 +238,17 @@ impl<'a, T: FieldElement> Machine<'a, T> for DoubleSortedWitnesses<'a, T> { } }; - for ((a, s), o) in std::mem::take(&mut self.trace) { - if let Some(prev_address) = addr.last() { - assert!(a >= *prev_address, "Expected addresses to be sorted"); + for ((a1, a2, s), o) in std::mem::take(&mut self.trace) { + if let Some(prev_address) = addr1.last() { + assert!(a1 >= *prev_address, "Expected addresses to be sorted"); if self.diff_columns_base.is_none() - && (a - *prev_address).to_degree() >= self.degree + && (a1 - *prev_address).to_degree() >= self.degree { - log::error!("Jump in memory accesses between {prev_address:x} and {a:x} is larger than or equal to the degree {}! This will violate the constraints.", self.degree); + log::error!("Jump in memory accesses between {prev_address:x} and {a1:x} is larger than or equal to the degree {}! This will violate the constraints.", self.degree); } - let current_diff = if a != *prev_address { - a - *prev_address + let current_diff = if a1 != *prev_address { + a1 - *prev_address } else { s - *step.last().unwrap() }; @@ -252,19 +256,23 @@ impl<'a, T: FieldElement> Machine<'a, T> for DoubleSortedWitnesses<'a, T> { diff.push(current_diff.to_degree() - 1); } - addr.push(a); + addr1.push(a1); + addr2.push(a2); step.push(s); - value.push(o.value); + value1.push(o.value1); + value2.push(o.value2); is_normal_write.push(o.is_normal_write.into()); is_bootloader_write.push(o.is_bootloader_write.into()); set_selector(Some(o.selector_id)); } - if addr.is_empty() { + if addr1.is_empty() { // No memory access at all - fill a first row with something. - addr.push(-T::one()); + addr1.push(-T::one()); + addr2.push(-T::one()); step.push(0.into()); - value.push(0.into()); + value1.push(0.into()); + value2.push(0.into()); is_normal_write.push(0.into()); is_bootloader_write.push(0.into()); set_selector(None); @@ -285,11 +293,13 @@ impl<'a, T: FieldElement> Machine<'a, T> for DoubleSortedWitnesses<'a, T> { self.degree = new_size; } - while addr.len() < self.degree as usize { - addr.push(*addr.last().unwrap()); + while addr1.len() < self.degree as usize { + addr1.push(*addr1.last().unwrap()); + addr2.push(*addr2.last().unwrap()); step.push(*step.last().unwrap() + T::from(1)); diff.push(0); - value.push(*value.last().unwrap()); + value1.push(*value1.last().unwrap()); + value2.push(*value2.last().unwrap()); is_normal_write.push(0.into()); is_bootloader_write.push(0.into()); set_selector(None); @@ -300,19 +310,19 @@ impl<'a, T: FieldElement> Machine<'a, T> for DoubleSortedWitnesses<'a, T> { diff.push(0); let last_row_change_value = match self.has_bootloader_write_column { - true => (&addr[0] != addr.last().unwrap()).into(), + true => (&addr1[0] != addr1.last().unwrap()).into(), // In the machine without the bootloader write column, m_change is constrained // to be 1 in the last row. false => 1.into(), }; - let change = addr + let change = addr1 .iter() .tuple_windows() .map(|(a, a_next)| if a == a_next { 0.into() } else { 1.into() }) .chain(once(last_row_change_value)) .collect::>(); - assert_eq!(change.len(), addr.len()); + assert_eq!(change.len(), addr1.len()); let diff_columns = if let Some(diff_columns_base) = self.diff_columns_base { let diff_upper = diff @@ -346,8 +356,10 @@ impl<'a, T: FieldElement> Machine<'a, T> for DoubleSortedWitnesses<'a, T> { .collect::>(); [ - (self.namespaced("m_value"), value), - (self.namespaced("m_addr"), addr), + (self.namespaced("m_value1"), value1), + (self.namespaced("m_value2"), value2), + (self.namespaced("m_addr1"), addr1), + (self.namespaced("m_addr2"), addr2), (self.namespaced("m_step"), step), (self.namespaced("m_change"), change), (self.namespaced("m_is_write"), is_normal_write.clone()), @@ -394,47 +406,80 @@ impl<'a, T: FieldElement> DoubleSortedWitnesses<'a, T> { let is_normal_write = operation_id == T::from(OPERATION_ID_WRITE); let is_bootloader_write = operation_id == T::from(OPERATION_ID_BOOTLOADER_WRITE); let is_write = is_bootloader_write || is_normal_write; - let addr = match args[1].constant_value() { + let addr1 = match args[1].constant_value() { Some(v) => v, None => { return Ok(EvalValue::incomplete( - IncompleteCause::NonConstantRequiredArgument("m_addr"), + IncompleteCause::NonConstantRequiredArgument("m_addr1"), )) } }; + let addr2 = match args[2].constant_value() { + Some(v) => v, + None => { + return Ok(EvalValue::incomplete( + IncompleteCause::NonConstantRequiredArgument("m_addr2"), + )) + } + }; + + let addr1_int = addr1.to_integer().try_into_u64().unwrap(); + let addr2_int = addr2.to_integer().try_into_u64().unwrap(); + let addr = addr1_int + (addr2_int << 16); if self.has_bootloader_write_column { - let is_initialized = self.is_initialized.get(&addr).cloned().unwrap_or_default(); + let is_initialized = self + .is_initialized + .get(&addr.into()) + .cloned() + .unwrap_or_default(); if !is_initialized && !is_bootloader_write { panic!("Memory address {addr:x} must be initialized with a bootloader write",); } - self.is_initialized.insert(addr, true); + self.is_initialized.insert(addr.into(), true); } - let step = args[2] + let step = args[3] .constant_value() - .ok_or_else(|| format!("Step must be known but is: {}", args[2]))?; + .ok_or_else(|| format!("Step must be known but is: {}", args[3]))?; - let value_expr = &args[3]; + let value1_expr = &args[4]; + let value2_expr = &args[5]; log::trace!( "Query addr={:x}, step={step}, write: {is_write}, value: {}", - addr.to_arbitrary_integer(), - value_expr + addr, + value1_expr ); // TODO this does not check any of the failure modes let mut assignments = EvalValue::complete(vec![]); let has_side_effect = if is_write { - let value = match value_expr.constant_value() { + let value1 = match value1_expr.constant_value() { + Some(v) => v, + None => { + return Ok(EvalValue::incomplete( + IncompleteCause::NonConstantRequiredArgument("m_value1"), + )) + } + }; + + let value2 = match value2_expr.constant_value() { Some(v) => v, None => { return Ok(EvalValue::incomplete( - IncompleteCause::NonConstantRequiredArgument("m_value"), + IncompleteCause::NonConstantRequiredArgument("m_value2"), )) } }; + let value1_int = value1.to_integer().try_into_u64().unwrap(); + let value2_int = value2.to_integer().try_into_u64().unwrap(); + let value = value1_int + (value2_int << 16); + + assert!(value1_int < 0x10000); + assert!(value2_int < 0x10000); + log::trace!( "Memory write: addr={:x}, step={step}, value={:x}", addr, @@ -443,11 +488,12 @@ impl<'a, T: FieldElement> DoubleSortedWitnesses<'a, T> { self.data.insert(addr, value); self.trace .insert( - (addr, step), + (addr1, addr2, step), Operation { is_normal_write, is_bootloader_write, - value, + value1, + value2, selector_id, }, ) @@ -459,16 +505,27 @@ impl<'a, T: FieldElement> DoubleSortedWitnesses<'a, T> { addr, value ); - let ass = - (value_expr.clone() - (*value).into()).solve_with_range_constraints(caller_rows)?; + + let value_int: u64 = *value; + let value1_int = value_int & 0xffff; + let value2_int = value_int >> 16; + let value1_fe: T = value1_int.into(); + let value2_fe: T = value2_int.into(); + + let ass = (value1_expr.clone() - value1_fe.into()) + .solve_with_range_constraints(caller_rows)?; assignments.combine(ass); + let ass2 = (value2_expr.clone() - value2_fe.into()) + .solve_with_range_constraints(caller_rows)?; + assignments.combine(ass2); self.trace .insert( - (addr, step), + (addr1, addr2, step), Operation { is_normal_write, is_bootloader_write, - value: *value, + value1: value1_fe, + value2: value2_fe, selector_id, }, ) diff --git a/std/machines/memory_bb.asm b/std/machines/memory_bb.asm new file mode 100644 index 000000000..440b8f752 --- /dev/null +++ b/std/machines/memory_bb.asm @@ -0,0 +1,283 @@ +use std::array; +use std::machines::range::Byte2; + +// A read/write memory, similar to that of Polygon: +// https://github.com/0xPolygonHermez/zkevm-proverjs/blob/main/pil/mem.pil +machine Memory(byte2: Byte2) with + latch: LATCH, + operation_id: m_is_write, + call_selectors: selectors, +{ + // lower bound degree is 65536 + + operation mload<0> m_addr1, m_addr2, m_step -> m_value1, m_value2; + operation mstore<1> m_addr1, m_addr2, m_step, m_value1, m_value2 ->; + + let LATCH = 1; + + // =============== read-write memory ======================= + // Read-write memory. Columns are sorted by addr and + // then by step. change is 1 if and only if addr changes + // in the next row. + // Note that these column names are used by witgen to detect + // this machine... + col witness m_addr1, m_addr2; + col witness m_step; + col witness m_change; + col witness m_value1, m_value2; + + link => byte2.check(m_addr1); + link => byte2.check(m_addr2); + link => byte2.check(m_value1); + link => byte2.check(m_value2); + + // Memory operation flags + col witness m_is_write; + std::utils::force_bool(m_is_write); + + // is_write can only be 1 if a selector is active + let is_mem_op = array::sum(selectors); + std::utils::force_bool(is_mem_op); + (1 - is_mem_op) * m_is_write = 0; + + // If the next line is a not a write and we have an address change, + // then the value is zero. + (1 - m_is_write') * m_change * m_value1' = 0; + (1 - m_is_write') * m_change * m_value2' = 0; + + // change has to be 1 in the last row, so that a first read on row zero is constrained to return 0 + (1 - m_change) * LAST = 0; + + // If the next line is a read and we stay at the same address, then the + // value cannot change. + (1 - m_is_write') * (1 - m_change) * (m_value1' - m_value1) = 0; + (1 - m_is_write') * (1 - m_change) * (m_value2' - m_value2) = 0; + + col witness m_diff_lower; + col witness m_diff_upper; + + col fixed FIRST = [1] + [0]*; + let LAST = FIRST'; + + link => byte2.check(m_diff_lower); + link => byte2.check(m_diff_upper); + + std::utils::force_bool(m_change); + + // if change is zero, addr has to stay the same. + (m_addr1' - m_addr1) * (1 - m_change) = 0; + (m_addr2' - m_addr2) * (1 - m_change) = 0; + + // Except for the last row, if change is 1, then addr has to increase, + // if it is zero, step has to increase. + // `m_diff_upper * 2**16 + m_diff_lower` has to be equal to the difference **minus one**. + // Since we know that both addr and step can only be 32-Bit, this enforces that + // the values are strictly increasing. + // TODO check this + col diff = (m_change * ((m_addr1' - m_addr1) + (m_addr2' - m_addr2) * 2**16) + (1 - m_change) * (m_step' - m_step)); + (1 - LAST) * (diff - 1 - m_diff_upper * 2**16 - m_diff_lower) = 0; +} + +// TODO Remove when https://github.com/powdr-labs/powdr/issues/1572 is done +machine Memory_20(byte2: Byte2) with + degree: 2**20, + latch: LATCH, + operation_id: m_is_write, + call_selectors: selectors, +{ + operation mload<0> m_addr, m_step -> m_value; + operation mstore<1> m_addr, m_step, m_value ->; + + let LATCH = 1; + + // =============== read-write memory ======================= + // Read-write memory. Columns are sorted by addr and + // then by step. change is 1 if and only if addr changes + // in the next row. + // Note that these column names are used by witgen to detect + // this machine... + col witness m_addr; + col witness m_step; + col witness m_change; + col witness m_value; + + // Memory operation flags + col witness m_is_write; + std::utils::force_bool(m_is_write); + + // is_write can only be 1 if a selector is active + let is_mem_op = array::sum(selectors); + std::utils::force_bool(is_mem_op); + (1 - is_mem_op) * m_is_write = 0; + + // If the next line is a not a write and we have an address change, + // then the value is zero. + (1 - m_is_write') * m_change * m_value' = 0; + + // change has to be 1 in the last row, so that a first read on row zero is constrained to return 0 + (1 - m_change) * LAST = 0; + + // If the next line is a read and we stay at the same address, then the + // value cannot change. + (1 - m_is_write') * (1 - m_change) * (m_value' - m_value) = 0; + + col witness m_diff_lower; + col witness m_diff_upper; + + col fixed FIRST = [1] + [0]*; + let LAST = FIRST'; + col fixed STEP(i) { i }; + col fixed BIT16(i) { i & 0xffff }; + + link => byte2.check(m_diff_lower); + link => byte2.check(m_diff_upper); + + std::utils::force_bool(m_change); + + // if change is zero, addr has to stay the same. + (m_addr' - m_addr) * (1 - m_change) = 0; + + // Except for the last row, if change is 1, then addr has to increase, + // if it is zero, step has to increase. + // `m_diff_upper * 2**16 + m_diff_lower` has to be equal to the difference **minus one**. + // Since we know that both addr and step can only be 32-Bit, this enforces that + // the values are strictly increasing. + col diff = (m_change * (m_addr' - m_addr) + (1 - m_change) * (m_step' - m_step)); + (1 - LAST) * (diff - 1 - m_diff_upper * 2**16 - m_diff_lower) = 0; +} + +// TODO Remove when https://github.com/powdr-labs/powdr/issues/1572 is done +machine Memory_21(byte2: Byte2) with + degree: 2**21, + latch: LATCH, + operation_id: m_is_write, + call_selectors: selectors, +{ + operation mload<0> m_addr, m_step -> m_value; + operation mstore<1> m_addr, m_step, m_value ->; + + let LATCH = 1; + + // =============== read-write memory ======================= + // Read-write memory. Columns are sorted by addr and + // then by step. change is 1 if and only if addr changes + // in the next row. + // Note that these column names are used by witgen to detect + // this machine... + col witness m_addr; + col witness m_step; + col witness m_change; + col witness m_value; + + // Memory operation flags + col witness m_is_write; + std::utils::force_bool(m_is_write); + + // is_write can only be 1 if a selector is active + let is_mem_op = array::sum(selectors); + std::utils::force_bool(is_mem_op); + (1 - is_mem_op) * m_is_write = 0; + + // If the next line is a not a write and we have an address change, + // then the value is zero. + (1 - m_is_write') * m_change * m_value' = 0; + + // change has to be 1 in the last row, so that a first read on row zero is constrained to return 0 + (1 - m_change) * LAST = 0; + + // If the next line is a read and we stay at the same address, then the + // value cannot change. + (1 - m_is_write') * (1 - m_change) * (m_value' - m_value) = 0; + + col witness m_diff_lower; + col witness m_diff_upper; + + col fixed FIRST = [1] + [0]*; + let LAST = FIRST'; + col fixed STEP(i) { i }; + col fixed BIT16(i) { i & 0xffff }; + + link => byte2.check(m_diff_lower); + link => byte2.check(m_diff_upper); + + std::utils::force_bool(m_change); + + // if change is zero, addr has to stay the same. + (m_addr' - m_addr) * (1 - m_change) = 0; + + // Except for the last row, if change is 1, then addr has to increase, + // if it is zero, step has to increase. + // `m_diff_upper * 2**16 + m_diff_lower` has to be equal to the difference **minus one**. + // Since we know that both addr and step can only be 32-Bit, this enforces that + // the values are strictly increasing. + col diff = (m_change * (m_addr' - m_addr) + (1 - m_change) * (m_step' - m_step)); + (1 - LAST) * (diff - 1 - m_diff_upper * 2**16 - m_diff_lower) = 0; +} + +// TODO Remove when https://github.com/powdr-labs/powdr/issues/1572 is done +machine Memory_22(byte2: Byte2) with + degree: 2**22, + latch: LATCH, + operation_id: m_is_write, + call_selectors: selectors, +{ + operation mload<0> m_addr, m_step -> m_value; + operation mstore<1> m_addr, m_step, m_value ->; + + let LATCH = 1; + + // =============== read-write memory ======================= + // Read-write memory. Columns are sorted by addr and + // then by step. change is 1 if and only if addr changes + // in the next row. + // Note that these column names are used by witgen to detect + // this machine... + col witness m_addr; + col witness m_step; + col witness m_change; + col witness m_value; + + // Memory operation flags + col witness m_is_write; + std::utils::force_bool(m_is_write); + + // is_write can only be 1 if a selector is active + let is_mem_op = array::sum(selectors); + std::utils::force_bool(is_mem_op); + (1 - is_mem_op) * m_is_write = 0; + + // If the next line is a not a write and we have an address change, + // then the value is zero. + (1 - m_is_write') * m_change * m_value' = 0; + + // change has to be 1 in the last row, so that a first read on row zero is constrained to return 0 + (1 - m_change) * LAST = 0; + + // If the next line is a read and we stay at the same address, then the + // value cannot change. + (1 - m_is_write') * (1 - m_change) * (m_value' - m_value) = 0; + + col witness m_diff_lower; + col witness m_diff_upper; + + col fixed FIRST = [1] + [0]*; + let LAST = FIRST'; + col fixed STEP(i) { i }; + col fixed BIT16(i) { i & 0xffff }; + + link => byte2.check(m_diff_lower); + link => byte2.check(m_diff_upper); + + std::utils::force_bool(m_change); + + // if change is zero, addr has to stay the same. + (m_addr' - m_addr) * (1 - m_change) = 0; + + // Except for the last row, if change is 1, then addr has to increase, + // if it is zero, step has to increase. + // `m_diff_upper * 2**16 + m_diff_lower` has to be equal to the difference **minus one**. + // Since we know that both addr and step can only be 32-Bit, this enforces that + // the values are strictly increasing. + col diff = (m_change * (m_addr' - m_addr) + (1 - m_change) * (m_step' - m_step)); + (1 - LAST) * (diff - 1 - m_diff_upper * 2**16 - m_diff_lower) = 0; +} diff --git a/std/machines/mod.asm b/std/machines/mod.asm index d059419c1..b04e243c4 100644 --- a/std/machines/mod.asm +++ b/std/machines/mod.asm @@ -4,6 +4,7 @@ mod binary_bb; mod range; mod hash; mod memory; +mod memory_bb; mod memory_with_bootloader_write; mod shift; mod split; diff --git a/test_data/std/memory_bb_test.asm b/test_data/std/memory_bb_test.asm new file mode 100644 index 000000000..409fc2caf --- /dev/null +++ b/test_data/std/memory_bb_test.asm @@ -0,0 +1,65 @@ +use std::machines::range::Byte2; +use std::machines::memory_bb::Memory; + +machine Main with degree: 65536 { + reg pc[@pc]; + reg X1[<=]; + reg X2[<=]; + reg Y1[<=]; + reg Y2[<=]; + reg A1; + reg A2; + + col fixed STEP(i) { i }; + Byte2 byte2; + Memory memory(byte2); + + instr mload X1, X2 -> Y1, Y2 link ~> (Y1, Y2) = memory.mload(X1, X2, STEP); + instr mstore X1, X2, Y1, Y2 -> link ~> memory.mstore(X1, X2, STEP, Y1, Y2); + + instr assert_eq X1, X2, Y1, Y2 { + X1 = Y1, + X2 = Y2 + } + + function main { + + // Store 4 + mstore 100, 0, 4, 0; + + // Read uninitialized memory + A1, A2 <== mload(104, 0); + assert_eq A1, A2, 0, 0; + + // Read previously stored value + A1, A2 <== mload(100, 0); + assert_eq A1, A2, 4, 0; + + // Update previously stored value + mstore 100, 0, 7, 0; + mstore 100, 0, 8, 0; + + // Read updated values (twice) + A1, A2 <== mload(100, 0); + assert_eq A1, A2, 8, 0; + A1, A2 <== mload(100, 0); + assert_eq A1, A2, 8, 0; + + // Write to previously uninitialized memory cell + mstore 104, 0, 1234, 0; + A1, A2 <== mload(104, 0); + assert_eq A1, A2, 1234, 0; + + // Write max value + mstore 200, 0, 0xffff, 0xffff; + A1, A2 <== mload(200, 0); + assert_eq A1, A2, 0xffff, 0xffff; + + // Store at maximal address + mstore 0xffff, 0xfffc, 1, 0; + A1, A2 <== mload(0xffff, 0xfffc); + assert_eq A1, A2, 1, 0; + + return; + } +}