From 7b598ac778e94119a372886c7896c635321b712c Mon Sep 17 00:00:00 2001 From: Maddiaa0 <47148561+Maddiaa0@users.noreply.github.com> Date: Wed, 4 Oct 2023 16:01:27 +0000 Subject: [PATCH 01/75] temp: brillig impl 1 --- aztec/Cargo.toml | 16 ++ aztec/README.md | 38 +++++ aztec/brillig.asm | 124 ++++++++++++++ aztec/brillig_out.asm | 139 ++++++++++++++++ aztec/bytecode.acir | 1 + aztec/node_modules/.yarn-integrity | 10 ++ aztec/src/main.rs | 250 +++++++++++++++++++++++++++++ aztec/tut/hello.asm | 39 +++++ 8 files changed, 617 insertions(+) create mode 100644 aztec/Cargo.toml create mode 100644 aztec/README.md create mode 100644 aztec/brillig.asm create mode 100644 aztec/brillig_out.asm create mode 100644 aztec/bytecode.acir create mode 100644 aztec/node_modules/.yarn-integrity create mode 100644 aztec/src/main.rs create mode 100644 aztec/tut/hello.asm diff --git a/aztec/Cargo.toml b/aztec/Cargo.toml new file mode 100644 index 0000000000..fcfa733296 --- /dev/null +++ b/aztec/Cargo.toml @@ -0,0 +1,16 @@ +[package] +name = "aztec" +version = "0.1.0" +authors = ["Maddiaa"] +edition = "2021" + +[dependencies] +asm_utils = { path = "../asm_utils" } + +# TODO: we probably want to pull in the local version of nargo while i am working on it here + +# Include acvm brillig module such that we can serialise and deserialise them +acvm = { git = "https://github.com/noir-lang/noir", directory = "acvm-repo/acvm" } +base64 = "*" +rand = "0.8.4" + diff --git a/aztec/README.md b/aztec/README.md new file mode 100644 index 0000000000..6c5fc9d169 --- /dev/null +++ b/aztec/README.md @@ -0,0 +1,38 @@ +## Operations + +Field Ops { + Add, + Sub, + Mul, + Div, + Equals +} + +Int ops { + Add, + sub, + mul, + div, + equals, + lt, + lte, + and, + or, + xor, + shl, + shr +} + +jumpin // Surely this can just be removed, and allow for negative conditions +jumpi +jump +call +const <- really just push for a field elem +return +foregincall // do we need +mov +load +store +blackbox <- cant really use in a vm +trap <- failure +stop <- complete diff --git a/aztec/brillig.asm b/aztec/brillig.asm new file mode 100644 index 0000000000..88f054de7d --- /dev/null +++ b/aztec/brillig.asm @@ -0,0 +1,124 @@ + + degree 256; + + reg pc[@pc]; + reg X[<=]; + reg Y[<=]; + reg Z[<=]; + + reg jump_ptr; // Store the location of a call + reg addr; // used for memory operations + reg tmp; // used for temporary storage + reg r0; // 12 registers for now + reg r1; + reg r2; + reg r3; + reg r4; + reg r5; + reg r6; + reg r7; + reg r8; + reg r9; + reg r10; + reg r11; + + constraints { + // ============== iszero check for X ======================= + col witness XInv; + col witness XIsZero; + XIsZero = 1 - X * XInv; + XIsZero * X = 0; + XIsZero * (1 - XIsZero) = 0; + + + // =============== read-write memory ======================= + // Read-write memory. Columns are sorted by m_addr and + // then by m_step. m_change is 1 if and only if m_addr changes + // in the next row. + col witness m_addr; + col witness m_step; + col witness m_change; + col witness m_value; + // If we have an operation at all (needed because this needs to be a permutation) + col witness m_op; + // If the operation is a write operation. + col witness m_is_write; + col witness m_is_read; + + // positive numbers (assumed to be much smaller than the field order) + col fixed POSITIVE(i) { i + 1 }; + col fixed FIRST = [1] + [0]*; + col fixed LAST(i) { FIRST(i + 1) }; + col fixed STEP(i) { i }; + + m_change * (1 - m_change) = 0; + + // if m_change is zero, m_addr has to stay the same. + (m_addr' - m_addr) * (1 - m_change) = 0; + + // Except for the last row, if m_change is 1, then m_addr has to increase, + // if it is zero, m_step has to increase. + (1 - LAST) { m_change * (m_addr' - m_addr) + (1 - m_change) * (m_step' - m_step) } in POSITIVE; + + m_op * (1 - m_op) = 0; + m_is_write * (1 - m_is_write) = 0; + m_is_read * (1 - m_is_read) = 0; + // m_is_write can only be 1 if m_op is 1. + m_is_write * (1 - m_op) = 0; + m_is_read * (1 - m_op) = 0; + m_is_read * m_is_write = 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; + + // If the next line is a read and we have an address change, + // then the value is zero. + (1 - m_is_write') * m_change * m_value' = 0; + } + + + // ============== memory instructions ============== + instr store X { { addr, STEP, X } is m_is_write { m_addr, m_step, m_value } } + instr load -> X { { addr, STEP, X } is m_is_read { m_addr, m_step, m_value } } + + + + /// Add + /// Take in two input registers, send the result into the output register + instr add Y, Z -> X { + X = Y + Z + } + + /// Sub + instr sub Y, Z -> X { + X = Y - Z + } + + /// Is the value equal to 0 - uses only assignment registers + instr eq X -> Y { Y = XIsZero } + + /// Mul + instr mul Y, Z -> X { + X = Y * Z + } + + /// move + // TODO: move should zero out the sending register? + instr mov Y -> X { + X = Y + } + + // When we get a call, we want + instr call l: label { pc' = l, jump_ptr' = pc + 1 } + instr ret { pc' = jump_ptr } + + /// Jumps + instr jump l: label { pc' = l } + instr jumpi X, l: label { pc' = (1 - XIsZero) * l + XIsZero * (pc + 1) } + instr jumpni X, l: label { pc' = XIsZero * l + (1 - XIsZero) * (pc + 1) } + diff --git a/aztec/brillig_out.asm b/aztec/brillig_out.asm new file mode 100644 index 0000000000..5eeca24475 --- /dev/null +++ b/aztec/brillig_out.asm @@ -0,0 +1,139 @@ + +machine Main { + + + degree 256; + + reg pc[@pc]; + reg X[<=]; + reg Y[<=]; + reg Z[<=]; + + reg jump_ptr; // Store the location of a call + reg addr; // used for memory operations + reg tmp; // used for temporary storage + reg r0; // 12 registers for now + reg r1; + reg r2; + reg r3; + reg r4; + reg r5; + reg r6; + reg r7; + reg r8; + reg r9; + reg r10; + reg r11; + + constraints { + // ============== iszero check for X ======================= + col witness XInv; + col witness XIsZero; + XIsZero = 1 - X * XInv; + XIsZero * X = 0; + XIsZero * (1 - XIsZero) = 0; + + + // =============== read-write memory ======================= + // Read-write memory. Columns are sorted by m_addr and + // then by m_step. m_change is 1 if and only if m_addr changes + // in the next row. + col witness m_addr; + col witness m_step; + col witness m_change; + col witness m_value; + // If we have an operation at all (needed because this needs to be a permutation) + col witness m_op; + // If the operation is a write operation. + col witness m_is_write; + col witness m_is_read; + + // positive numbers (assumed to be much smaller than the field order) + col fixed POSITIVE(i) { i + 1 }; + col fixed FIRST = [1] + [0]*; + col fixed LAST(i) { FIRST(i + 1) }; + col fixed STEP(i) { i }; + + m_change * (1 - m_change) = 0; + + // if m_change is zero, m_addr has to stay the same. + (m_addr' - m_addr) * (1 - m_change) = 0; + + // Except for the last row, if m_change is 1, then m_addr has to increase, + // if it is zero, m_step has to increase. + (1 - LAST) { m_change * (m_addr' - m_addr) + (1 - m_change) * (m_step' - m_step) } in POSITIVE; + + m_op * (1 - m_op) = 0; + m_is_write * (1 - m_is_write) = 0; + m_is_read * (1 - m_is_read) = 0; + // m_is_write can only be 1 if m_op is 1. + m_is_write * (1 - m_op) = 0; + m_is_read * (1 - m_op) = 0; + m_is_read * m_is_write = 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; + + // If the next line is a read and we have an address change, + // then the value is zero. + (1 - m_is_write') * m_change * m_value' = 0; + } + + + // ============== memory instructions ============== + instr store X { { addr, STEP, X } is m_is_write { m_addr, m_step, m_value } } + instr load -> X { { addr, STEP, X } is m_is_read { m_addr, m_step, m_value } } + + + + /// Add + /// Take in two input registers, send the result into the output register + instr add Y, Z -> X { + X = Y + Z + } + + /// Sub + instr sub Y, Z -> X { + X = Y - Z + } + + /// Is the value equal to 0 - uses only assignment registers + instr eq X -> Y { Y = XIsZero } + + /// Mul + instr mul Y, Z -> X { + X = Y * Z + } + + /// move + // TODO: move should zero out the sending register? + instr mov Y -> X { + X = Y + } + + // When we get a call, we want + instr call l: label { pc' = l, jump_ptr' = pc + 1 } + instr ret { pc' = jump_ptr } + + /// Jumps + instr jump l: label { pc' = l } + instr jumpi X, l: label { pc' = (1 - XIsZero) * l + XIsZero * (pc + 1) } + instr jumpni X, l: label { pc' = XIsZero * l + (1 - XIsZero) * (pc + 1) } + + + + function main { + r0 <=X= 0; + r1 <=X= 0; + call dafe; + return; + dafe:: + r3 <=X= 3; + ret; + } +} diff --git a/aztec/bytecode.acir b/aztec/bytecode.acir new file mode 100644 index 0000000000..b4019fc537 --- /dev/null +++ b/aztec/bytecode.acir @@ -0,0 +1 @@ +H4sIAAAAAAAA/61SQQrAMAjTuXV0h73Fsg/0/68aMoVQvM1cDApJGipExPRBgCNiN33qPwyu01LMuwG/fPZlb2jAZ1GOVt+THpC1J++8/S61vo957a4lSY9xOyn5L0UhRgijAS8FGF5CSMECwQIAAA== \ No newline at end of file diff --git a/aztec/node_modules/.yarn-integrity b/aztec/node_modules/.yarn-integrity new file mode 100644 index 0000000000..ae931097fe --- /dev/null +++ b/aztec/node_modules/.yarn-integrity @@ -0,0 +1,10 @@ +{ + "systemParams": "linux-x64-108", + "modulesFolders": [], + "flags": [], + "linkedModules": [], + "topLevelPatterns": [], + "lockfileEntries": {}, + "files": [], + "artifacts": {} +} \ No newline at end of file diff --git a/aztec/src/main.rs b/aztec/src/main.rs new file mode 100644 index 0000000000..f298702ace --- /dev/null +++ b/aztec/src/main.rs @@ -0,0 +1,250 @@ +use acvm::acir::brillig::Opcode as BrilligOpcode; +use acvm::acir::circuit::Circuit; +use acvm::acir::circuit::Opcode; +use acvm::brillig_vm::brillig::BinaryFieldOp; +use acvm::brillig_vm::brillig::Label; +use acvm::brillig_vm::brillig::RegisterIndex; +use rand::distributions::Alphanumeric; +use rand::Rng; +use std::fs; +use std::io::Write; +use std::iter; + +use std::collections::HashMap; + +/// Module to convert brillig assmebly into powdr assembly + +// struct BrilligArchitecture {} + +// impl Architecture for BrilligArchitecture { +// fn instruction_ends_control_flow(instr: &str) -> bool { +// match instr { +// "li" | "lui" | "la" | "mv" | "add" | "addi" | "sub" | "neg" | "mul" | "mulhu" +// | "divu" | "xor" | "xori" | "and" | "andi" | "or" | "ori" | "not" | "slli" | "sll" +// | "srli" | "srl" | "srai" | "seqz" | "snez" | "slt" | "slti" | "sltu" | "sltiu" +// | "sgtz" | "beq" | "beqz" | "bgeu" | "bltu" | "blt" | "bge" | "bltz" | "blez" +// | "bgtz" | "bgez" | "bne" | "bnez" | "jal" | "jalr" | "call" | "ecall" | "ebreak" +// | "lw" | "lb" | "lbu" | "lh" | "lhu" | "sw" | "sh" | "sb" | "nop" | "fence" +// | "fence.i" | "amoadd.w.rl" | "amoadd.w" => false, +// "j" | "jr" | "tail" | "ret" | "trap" => true, +// _ => { +// panic!("Unknown instruction: {instr}"); +// } +// } +// } + +// fn get_references<'a, R: asm_utils::ast::Register, F: asm_utils::ast::FunctionOpKind>( +// instr: &str, +// args: &'a [asm_utils::ast::Argument], +// ) -> Vec<&'a str> { +// // fence arguments are not symbols, they are like reserved +// // keywords affecting the instruction behavior +// if instr.starts_with("fence") { +// Vec::new() +// } else { +// symbols_in_args(args) +// } +// } +// } + +fn main() { + // Read in file called bytecode.acir + let bytecode = fs::read("bytecode.acir").expect("Unable to read file"); + // Convert the read-in base64 file into Vec + let decoded = base64::decode(&bytecode).expect("Failed to decode base64"); + let bytecode = Vec::from(decoded); + + // Create a new circuit from the bytecode instance + let circuit: Circuit = Circuit::read(&*bytecode).expect("Failed to deserialize circuit"); + + println!("circuit: {:?}", circuit); + + // Get the brillig opcodes + let brillig = extract_brillig(circuit.opcodes); + print!("{:?}", brillig); + + let preamble = get_preamble(); + let program = construct_main(brillig); + let powdr = brillig_machine(&preamble, program); + + println!("powdr: {:?}", powdr); + + // temp write the output to a file + let mut file = fs::File::create("brillig_out.asm").expect("Could not create file"); + file.write_all(powdr.as_bytes()) + .expect("Could not write to file"); +} + +fn brillig_machine( + // machines: &[&str], + preamble: &str, + // submachines: &[(&str, &str)], + program: Vec, +) -> String { + format!( + r#" +machine Main {{ + +{} + + function main {{ +{} + }} +}} +"#, + preamble, + program + .into_iter() + .map(|line| format!("\t\t{line}")) + .collect::>() + .join("\n") + ) +} + +// Output the powdr assembly with the given circuit +fn construct_main(program: Opcode) -> Vec { + let mut main_asm: Vec = Vec::new(); + + // For each instruction in brillig, we want o + let trace = match program { + Opcode::Brillig(brillig) => brillig.bytecode, + _ => { + panic!("Opcode is not of type brillig"); + } + }; + + println!(""); + println!(""); + trace.iter().for_each(|i| println!("{:?}", i)); + println!(""); + println!(""); + + // Label of [index], String, where index is the generated name of the jump, we will place a jump label there when + // we encounter it to prove + let mut index = 0; + let mut labels: HashMap = HashMap::new(); + + for instr in trace { + println!("{:?}", instr); + println!(""); + println!(""); + println!(""); + // powdr_asm.push_str(&instr.to_string()); + + // If we require a label to be placed at the jump location then we add it + if let Some(jump) = labels.get(&index) { + main_asm.push(format!("{}::", jump)); + } + + match instr { + BrilligOpcode::Const { destination, value } => { + let number = value.to_usize().to_string(); + main_asm.push(format!("{} <=X= {};", print_register(destination), number)); + } + BrilligOpcode::Stop => { + main_asm.push("return;".to_owned()); + } + BrilligOpcode::Return => { + main_asm.push("ret;".to_owned()); + } + // Calls -> look more into how this is performed internally + // For calls we want to store the current pc in a holding register such that we can return to it + // We then want to jump to that location in the bytecode + BrilligOpcode::Call { location } => { + // Generate a label for the location we are going to + let label = gen_label(); + labels.insert(location, label.clone()); // This label will be inserted later on! + + main_asm.push(format!("call {};", label)); + } + BrilligOpcode::BinaryFieldOp { + destination, + op, + lhs, + rhs, + } => { + // Match the given operation + match op { + BinaryFieldOp::Add => { + main_asm.push(format!( + "{} <== add({}, {});", + print_register(destination), + print_register(lhs), + print_register(rhs) + )); + } + BinaryFieldOp::Sub => { + main_asm.push(format!( + "{} <== sub({}, {});", + print_register(destination), + print_register(lhs), + print_register(rhs) + )); + } + // Equals is currently a mix of the equals instruction and the using the X is 0 witness column + BinaryFieldOp::Equals => { + main_asm.push(format!( + "tmp <== sub({}, {});", + print_register(lhs), + print_register(rhs) + )); + main_asm.push(format!("{} <== eq(tmp);", print_register(destination),)); + } + BinaryFieldOp::Mul => { + main_asm.push(format!( + "{} <== mul({}, {});", + print_register(destination), + print_register(lhs), + print_register(rhs) + )); + } + // TODO: div + _ => println!("not implemented"), + } + } + _ => println!("not implemented"), + } + + // Increment the index in the instruction array + index += 1; + } + + println!("main_asm: {:?}", main_asm); + + main_asm +} + +fn gen_label() -> String { + let mut rng = rand::thread_rng(); + let hex_chars: Vec = "abcdef".chars().collect(); + // Lmao chat gpt fix + let label: String = iter::repeat(()) + .map(|()| rng.gen_range(0..hex_chars.len())) + .map(|i| hex_chars[i]) + .take(4) + .collect(); + + label +} + +fn print_register(r_index: RegisterIndex) -> String { + let num = r_index.to_usize(); + format!("r{}", num.to_string()).to_owned() +} + +// Read the preamble from the brillig.asm machine +fn get_preamble() -> String { + let preamble = fs::read_to_string("brillig.asm").expect("Unable to read file"); + preamble +} + +fn extract_brillig(opcodes: Vec) -> Opcode { + if opcodes.len() != 1 { + panic!("There should only be one brillig opcode"); + } + let opcode = &opcodes[0]; + if opcode.name() != "brillig" { + panic!("Opcode is not of type brillig"); + } + opcode.clone() +} diff --git a/aztec/tut/hello.asm b/aztec/tut/hello.asm new file mode 100644 index 0000000000..e3974219a2 --- /dev/null +++ b/aztec/tut/hello.asm @@ -0,0 +1,39 @@ +machine HelloWorld { + + degree 8; + + reg pc[@pc]; + reg X[<=]; // assignment registers + reg Y[<=]; + reg A; // floating registers + + instr incr X -> Y { + Y = X + 1 + } + + instr decr X -> Y { + Y = X -1 + } + + // How do we stop this from being an assignment + // rather than a comparison, as the instruction looks the same + instr assert_zero X { + X = 0 + } + + // ============== memory instructions ============== + instr mstore X { { addr, STEP, X } is m_is_write { m_addr, m_step, m_value } } + instr mload -> X { { addr, STEP, X } is m_is_read { m_addr, m_step, m_value } } + + constraints { + + } + + function main { + A <=X= ${ ("input", 0)}; // This is a built in function to take args from the command line + A <== incr(A); + A <== decr(A); + assert_zero A; + return; + } +} \ No newline at end of file From 5be067339cbbf2159abd0037726f70bb5f327378 Mon Sep 17 00:00:00 2001 From: Maddiaa0 <47148561+Maddiaa0@users.noreply.github.com> Date: Tue, 10 Oct 2023 10:24:36 +0000 Subject: [PATCH 02/75] temp --- Cargo.toml | 1 + 1 file changed, 1 insertion(+) diff --git a/Cargo.toml b/Cargo.toml index f7c5862b4c..523d267f20 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -15,6 +15,7 @@ members = [ "asm_to_pil", "halo2", "backend", + "aztec", "ast", "analysis", "linker", From e7c4a7d7213044fe5299706b3901758c8c24bed4 Mon Sep 17 00:00:00 2001 From: Maddiaa0 <47148561+Maddiaa0@users.noreply.github.com> Date: Tue, 10 Oct 2023 10:29:06 +0000 Subject: [PATCH 03/75] rm starky param --- backend/src/pilstark/estark.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/backend/src/pilstark/estark.rs b/backend/src/pilstark/estark.rs index f423b9b74a..d9646b0534 100644 --- a/backend/src/pilstark/estark.rs +++ b/backend/src/pilstark/estark.rs @@ -113,7 +113,7 @@ impl BackendImpl for EStark { &setup.program, &pil, &self.params, - &"".to_string(), + // &"".to_string(), ) .unwrap(); From 8eca3e7b962b21eff9eaa693014b61a417754c47 Mon Sep 17 00:00:00 2001 From: Maddiaa0 <47148561+Maddiaa0@users.noreply.github.com> Date: Thu, 12 Oct 2023 15:42:20 +0000 Subject: [PATCH 04/75] temp --- Cargo.toml | 2 +- ast/src/analyzed/mod.rs | 10 +- aztec/Cargo.toml | 16 - aztec/brillig.asm | 124 ----- aztec/brillig_out.asm | 139 ------ backend/Cargo.toml | 4 + ...BBergCodegen::assert_field_is_compatible:: | 0 backend/src/bberg_impl.rs | 66 +++ backend/src/halo2_impl.rs | 2 +- backend/src/lib.rs | 8 + bberg/Cargo.toml | 36 ++ {aztec => bberg}/README.md | 0 bberg/brillig.asm | 122 +++++ bberg/brillig_out.asm | 137 ++++++ {aztec => bberg}/bytecode.acir | 0 {aztec => bberg}/node_modules/.yarn-integrity | 0 bberg/src/bberg_codegen.rs | 48 ++ bberg/src/circuit_builder.rs | 453 ++++++++++++++++++ bberg/src/lib.rs | 2 + {aztec => bberg}/src/main.rs | 3 + {aztec => bberg}/tut/hello.asm | 0 brillig.pil | 333 +++++++++++++ brillig_opt.pil | 121 +++++ brillig_out.pil | 333 +++++++++++++ brillig_out_opt.pil | 116 +++++ commits.bin | Bin 0 -> 1024 bytes constants.bin | Bin 0 -> 512 bytes constraints.json | 1 + fibonacci_opt.pil | 10 + halo2/src/circuit_builder.rs | 3 + hello.pil | 69 +++ hello_opt.pil | 54 +++ number/src/serialize.rs | 2 + proof.bin | Bin 0 -> 5248 bytes 34 files changed, 1930 insertions(+), 284 deletions(-) delete mode 100644 aztec/Cargo.toml delete mode 100644 aztec/brillig.asm delete mode 100644 aztec/brillig_out.asm create mode 100644 backend/src/BBergCodegen::assert_field_is_compatible:: create mode 100644 backend/src/bberg_impl.rs create mode 100644 bberg/Cargo.toml rename {aztec => bberg}/README.md (100%) create mode 100644 bberg/brillig.asm create mode 100644 bberg/brillig_out.asm rename {aztec => bberg}/bytecode.acir (100%) rename {aztec => bberg}/node_modules/.yarn-integrity (100%) create mode 100644 bberg/src/bberg_codegen.rs create mode 100644 bberg/src/circuit_builder.rs create mode 100644 bberg/src/lib.rs rename {aztec => bberg}/src/main.rs (99%) rename {aztec => bberg}/tut/hello.asm (100%) create mode 100644 brillig.pil create mode 100644 brillig_opt.pil create mode 100644 brillig_out.pil create mode 100644 brillig_out_opt.pil create mode 100644 commits.bin create mode 100644 constants.bin create mode 100644 constraints.json create mode 100644 fibonacci_opt.pil create mode 100644 hello.pil create mode 100644 hello_opt.pil create mode 100644 proof.bin diff --git a/Cargo.toml b/Cargo.toml index 523d267f20..b4753c51bf 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -15,7 +15,7 @@ members = [ "asm_to_pil", "halo2", "backend", - "aztec", + "bberg", "ast", "analysis", "linker", diff --git a/ast/src/analyzed/mod.rs b/ast/src/analyzed/mod.rs index 20376db860..a35b1d4402 100644 --- a/ast/src/analyzed/mod.rs +++ b/ast/src/analyzed/mod.rs @@ -315,8 +315,12 @@ pub struct Identity { pub source: SourceRef, /// For a simple polynomial identity, the selector contains /// the actual expression (see expression_for_poly_id). - pub left: SelectedExpressions, - pub right: SelectedExpressions, + // + // + // NTS(Md) Both left and right are only used in the case of perm / plookup + // + pub left: SelectedExpressions, // left is selector expressions - for an arithmetic gate, the entire relation is in SL + pub right: SelectedExpressions, // right is the overall expressions } impl Identity { @@ -336,7 +340,7 @@ pub enum IdentityKind { Polynomial, Plookup, Permutation, - Connect, + Connect, // not used } pub type SelectedExpressions = parsed::SelectedExpressions; diff --git a/aztec/Cargo.toml b/aztec/Cargo.toml deleted file mode 100644 index fcfa733296..0000000000 --- a/aztec/Cargo.toml +++ /dev/null @@ -1,16 +0,0 @@ -[package] -name = "aztec" -version = "0.1.0" -authors = ["Maddiaa"] -edition = "2021" - -[dependencies] -asm_utils = { path = "../asm_utils" } - -# TODO: we probably want to pull in the local version of nargo while i am working on it here - -# Include acvm brillig module such that we can serialise and deserialise them -acvm = { git = "https://github.com/noir-lang/noir", directory = "acvm-repo/acvm" } -base64 = "*" -rand = "0.8.4" - diff --git a/aztec/brillig.asm b/aztec/brillig.asm deleted file mode 100644 index 88f054de7d..0000000000 --- a/aztec/brillig.asm +++ /dev/null @@ -1,124 +0,0 @@ - - degree 256; - - reg pc[@pc]; - reg X[<=]; - reg Y[<=]; - reg Z[<=]; - - reg jump_ptr; // Store the location of a call - reg addr; // used for memory operations - reg tmp; // used for temporary storage - reg r0; // 12 registers for now - reg r1; - reg r2; - reg r3; - reg r4; - reg r5; - reg r6; - reg r7; - reg r8; - reg r9; - reg r10; - reg r11; - - constraints { - // ============== iszero check for X ======================= - col witness XInv; - col witness XIsZero; - XIsZero = 1 - X * XInv; - XIsZero * X = 0; - XIsZero * (1 - XIsZero) = 0; - - - // =============== read-write memory ======================= - // Read-write memory. Columns are sorted by m_addr and - // then by m_step. m_change is 1 if and only if m_addr changes - // in the next row. - col witness m_addr; - col witness m_step; - col witness m_change; - col witness m_value; - // If we have an operation at all (needed because this needs to be a permutation) - col witness m_op; - // If the operation is a write operation. - col witness m_is_write; - col witness m_is_read; - - // positive numbers (assumed to be much smaller than the field order) - col fixed POSITIVE(i) { i + 1 }; - col fixed FIRST = [1] + [0]*; - col fixed LAST(i) { FIRST(i + 1) }; - col fixed STEP(i) { i }; - - m_change * (1 - m_change) = 0; - - // if m_change is zero, m_addr has to stay the same. - (m_addr' - m_addr) * (1 - m_change) = 0; - - // Except for the last row, if m_change is 1, then m_addr has to increase, - // if it is zero, m_step has to increase. - (1 - LAST) { m_change * (m_addr' - m_addr) + (1 - m_change) * (m_step' - m_step) } in POSITIVE; - - m_op * (1 - m_op) = 0; - m_is_write * (1 - m_is_write) = 0; - m_is_read * (1 - m_is_read) = 0; - // m_is_write can only be 1 if m_op is 1. - m_is_write * (1 - m_op) = 0; - m_is_read * (1 - m_op) = 0; - m_is_read * m_is_write = 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; - - // If the next line is a read and we have an address change, - // then the value is zero. - (1 - m_is_write') * m_change * m_value' = 0; - } - - - // ============== memory instructions ============== - instr store X { { addr, STEP, X } is m_is_write { m_addr, m_step, m_value } } - instr load -> X { { addr, STEP, X } is m_is_read { m_addr, m_step, m_value } } - - - - /// Add - /// Take in two input registers, send the result into the output register - instr add Y, Z -> X { - X = Y + Z - } - - /// Sub - instr sub Y, Z -> X { - X = Y - Z - } - - /// Is the value equal to 0 - uses only assignment registers - instr eq X -> Y { Y = XIsZero } - - /// Mul - instr mul Y, Z -> X { - X = Y * Z - } - - /// move - // TODO: move should zero out the sending register? - instr mov Y -> X { - X = Y - } - - // When we get a call, we want - instr call l: label { pc' = l, jump_ptr' = pc + 1 } - instr ret { pc' = jump_ptr } - - /// Jumps - instr jump l: label { pc' = l } - instr jumpi X, l: label { pc' = (1 - XIsZero) * l + XIsZero * (pc + 1) } - instr jumpni X, l: label { pc' = XIsZero * l + (1 - XIsZero) * (pc + 1) } - diff --git a/aztec/brillig_out.asm b/aztec/brillig_out.asm deleted file mode 100644 index 5eeca24475..0000000000 --- a/aztec/brillig_out.asm +++ /dev/null @@ -1,139 +0,0 @@ - -machine Main { - - - degree 256; - - reg pc[@pc]; - reg X[<=]; - reg Y[<=]; - reg Z[<=]; - - reg jump_ptr; // Store the location of a call - reg addr; // used for memory operations - reg tmp; // used for temporary storage - reg r0; // 12 registers for now - reg r1; - reg r2; - reg r3; - reg r4; - reg r5; - reg r6; - reg r7; - reg r8; - reg r9; - reg r10; - reg r11; - - constraints { - // ============== iszero check for X ======================= - col witness XInv; - col witness XIsZero; - XIsZero = 1 - X * XInv; - XIsZero * X = 0; - XIsZero * (1 - XIsZero) = 0; - - - // =============== read-write memory ======================= - // Read-write memory. Columns are sorted by m_addr and - // then by m_step. m_change is 1 if and only if m_addr changes - // in the next row. - col witness m_addr; - col witness m_step; - col witness m_change; - col witness m_value; - // If we have an operation at all (needed because this needs to be a permutation) - col witness m_op; - // If the operation is a write operation. - col witness m_is_write; - col witness m_is_read; - - // positive numbers (assumed to be much smaller than the field order) - col fixed POSITIVE(i) { i + 1 }; - col fixed FIRST = [1] + [0]*; - col fixed LAST(i) { FIRST(i + 1) }; - col fixed STEP(i) { i }; - - m_change * (1 - m_change) = 0; - - // if m_change is zero, m_addr has to stay the same. - (m_addr' - m_addr) * (1 - m_change) = 0; - - // Except for the last row, if m_change is 1, then m_addr has to increase, - // if it is zero, m_step has to increase. - (1 - LAST) { m_change * (m_addr' - m_addr) + (1 - m_change) * (m_step' - m_step) } in POSITIVE; - - m_op * (1 - m_op) = 0; - m_is_write * (1 - m_is_write) = 0; - m_is_read * (1 - m_is_read) = 0; - // m_is_write can only be 1 if m_op is 1. - m_is_write * (1 - m_op) = 0; - m_is_read * (1 - m_op) = 0; - m_is_read * m_is_write = 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; - - // If the next line is a read and we have an address change, - // then the value is zero. - (1 - m_is_write') * m_change * m_value' = 0; - } - - - // ============== memory instructions ============== - instr store X { { addr, STEP, X } is m_is_write { m_addr, m_step, m_value } } - instr load -> X { { addr, STEP, X } is m_is_read { m_addr, m_step, m_value } } - - - - /// Add - /// Take in two input registers, send the result into the output register - instr add Y, Z -> X { - X = Y + Z - } - - /// Sub - instr sub Y, Z -> X { - X = Y - Z - } - - /// Is the value equal to 0 - uses only assignment registers - instr eq X -> Y { Y = XIsZero } - - /// Mul - instr mul Y, Z -> X { - X = Y * Z - } - - /// move - // TODO: move should zero out the sending register? - instr mov Y -> X { - X = Y - } - - // When we get a call, we want - instr call l: label { pc' = l, jump_ptr' = pc + 1 } - instr ret { pc' = jump_ptr } - - /// Jumps - instr jump l: label { pc' = l } - instr jumpi X, l: label { pc' = (1 - XIsZero) * l + XIsZero * (pc + 1) } - instr jumpni X, l: label { pc' = XIsZero * l + (1 - XIsZero) * (pc + 1) } - - - - function main { - r0 <=X= 0; - r1 <=X= 0; - call dafe; - return; - dafe:: - r3 <=X= 3; - ret; - } -} diff --git a/backend/Cargo.toml b/backend/Cargo.toml index d9f10651ed..cddf02f783 100644 --- a/backend/Cargo.toml +++ b/backend/Cargo.toml @@ -5,9 +5,13 @@ edition = "2021" [features] halo2 = ["dep:halo2"] +# TODO: enable feature flag for bberg backend +# bberg = ["dep:bberg"] [dependencies] halo2 = { path = "../halo2", optional = true } +bberg = { path = "../bberg"} + pil_analyzer = { path = "../pil_analyzer" } number = { path = "../number" } strum = { version = "0.24.1", features = ["derive"] } diff --git a/backend/src/BBergCodegen::assert_field_is_compatible:: b/backend/src/BBergCodegen::assert_field_is_compatible:: new file mode 100644 index 0000000000..e69de29bb2 diff --git a/backend/src/bberg_impl.rs b/backend/src/bberg_impl.rs new file mode 100644 index 0000000000..98e6129f1d --- /dev/null +++ b/backend/src/bberg_impl.rs @@ -0,0 +1,66 @@ +use std::io::{self}; + +use crate::{BackendImpl, BackendImplWithSetup, Proof}; +use ast::analyzed::Analyzed; + +// We do not directly have a bberg prover at the moment +// however we can just perform codegen +use bberg::bberg_codegen::BBergCodegen; +use number::{DegreeType, FieldElement}; + +impl BackendImpl for BBergCodegen { + fn new(degree: DegreeType) -> Self { + BBergCodegen::assert_field_is_compatible::(); + BBergCodegen::new(degree) + } + + fn prove( + &self, + pil: &Analyzed, + fixed: &[(&str, Vec)], + witness: &[(&str, Vec)], + _prev_proof: Option, + ) -> (Option, Option) { + self.build_ast(pil, fixed, witness); + + // Note(md): In the current bberg impl we do not produce proofs here + // as we do cpp code generation, and then create proofs with bberg + // This may change in the future when the library matures to be more pluggable + (None, None) + } +} + +impl BackendImplWithSetup for BBergCodegen { + fn new_from_setup(mut input: &mut dyn io::Read) -> Result { + BBergCodegen::assert_field_is_compatible::(); + BBergCodegen::new_from_setup(&mut input) + } + + // TODO: implement this + fn write_setup(&self, mut output: &mut dyn io::Write) -> Result<(), io::Error> { + Ok(()) + // self.write_setup(&mut output) + } +} + +pub struct BBergMock; +impl BackendImpl for BBergMock { + fn new(_degree: DegreeType) -> Self { + Self + } + + fn prove( + &self, + pil: &Analyzed, + fixed: &[(&str, Vec)], + witness: &[(&str, Vec)], + prev_proof: Option, + ) -> (Option, Option) { + if prev_proof.is_some() { + unimplemented!("BBergMock backend does not support aggregation"); + } + + // TODO: mock prover + unimplemented!("BBergMock backend is not implemented"); + } +} diff --git a/backend/src/halo2_impl.rs b/backend/src/halo2_impl.rs index fb39b14a5a..aec908f014 100644 --- a/backend/src/halo2_impl.rs +++ b/backend/src/halo2_impl.rs @@ -27,7 +27,7 @@ impl BackendImpl for Halo2Prover { } } -impl BackendImplWithSetup for halo2::Halo2Prover { +impl BackendImplWithSetup for Halo2Prover { fn new_from_setup(mut input: &mut dyn io::Read) -> Result { Halo2Prover::assert_field_is_compatible::(); Halo2Prover::new_from_setup(&mut input) diff --git a/backend/src/lib.rs b/backend/src/lib.rs index deb22929db..36a4724ed4 100644 --- a/backend/src/lib.rs +++ b/backend/src/lib.rs @@ -1,5 +1,7 @@ #![deny(clippy::print_stdout)] +// #[cfg(feature = "bberg")] +mod bberg_impl; #[cfg(feature = "halo2")] mod halo2_impl; mod pilstark; @@ -11,6 +13,9 @@ use strum::{Display, EnumString, EnumVariantNames}; #[derive(Clone, EnumString, EnumVariantNames, Display)] pub enum BackendType { + // #[cfg(feature = "bberg")] + #[strum(serialize = "bberg")] + BBerg, #[cfg(feature = "halo2")] #[strum(serialize = "halo2")] Halo2, @@ -34,6 +39,8 @@ impl BackendType { WithoutSetupFactory(PhantomData); const PIL_STARK_CLI_FACTORY: WithoutSetupFactory = WithoutSetupFactory(PhantomData); + const BBERG_FACTORY: WithoutSetupFactory = + WithoutSetupFactory(PhantomData); match self { #[cfg(feature = "halo2")] @@ -42,6 +49,7 @@ impl BackendType { BackendType::Halo2Mock => &HALO2_MOCK_FACTORY, BackendType::PilStarkCli => &PIL_STARK_CLI_FACTORY, BackendType::EStark => &ESTARK_FACTORY, + BackendType::BBerg => &BBERG_FACTORY, } } } diff --git a/bberg/Cargo.toml b/bberg/Cargo.toml new file mode 100644 index 0000000000..a5ed90bc53 --- /dev/null +++ b/bberg/Cargo.toml @@ -0,0 +1,36 @@ +[package] +name = "bberg" +version = "0.1.0" +authors = ["Maddiaa"] +edition = "2021" + +[dependencies] +asm_utils = { path = "../asm_utils" } +num-bigint = "0.4.3" + +number = { path = "../number" } +pil_analyzer = { path = "../pil_analyzer" } +num-traits = "0.2.15" +num-integer = "0.1.45" +itertools = "^0.10" +log = "0.4.17" +rand = "0.8.5" +ast = { version = "0.1.0", path = "../ast" } + + +# TODO: we probably want to pull in the local version of nargo while i am working on it here + +# Include acvm brillig module such that we can serialise and deserialise them +acvm = { git = "https://github.com/noir-lang/noir", directory = "acvm-repo/acvm" } +base64 = "*" + +[dev-dependencies] +importer = { path = "../importer" } +analysis = { path = "../analysis" } +executor = { path = "../executor" } +parser = { path = "../parser" } +test-log = "0.2.12" +env_logger = "0.10.0" +linker = { path = "../linker" } + + diff --git a/aztec/README.md b/bberg/README.md similarity index 100% rename from aztec/README.md rename to bberg/README.md diff --git a/bberg/brillig.asm b/bberg/brillig.asm new file mode 100644 index 0000000000..317f34d740 --- /dev/null +++ b/bberg/brillig.asm @@ -0,0 +1,122 @@ + + degree 256; + + reg pc[@pc]; + reg X[<=]; + reg Y[<=]; + reg Z[<=]; + + reg jump_ptr; // Store the location of a call + reg addr; // used for memory operations + reg tmp; // used for temporary storage + reg r0; // 12 registers for now + reg r1; + reg r2; + reg r3; + reg r4; + reg r5; + reg r6; + reg r7; + reg r8; + reg r9; + reg r10; + reg r11; + + // ============== iszero check for X ======================= + col witness XInv; + col witness XIsZero; + XIsZero = 1 - X * XInv; + XIsZero * X = 0; + XIsZero * (1 - XIsZero) = 0; + + + // =============== read-write memory ======================= + // Read-write memory. Columns are sorted by m_addr and + // then by m_step. m_change is 1 if and only if m_addr changes + // in the next row. + col witness m_addr; + col witness m_step; + col witness m_change; + col witness m_value; + // If we have an operation at all (needed because this needs to be a permutation) + col witness m_op; + // If the operation is a write operation. + col witness m_is_write; + col witness m_is_read; + + // positive numbers (assumed to be much smaller than the field order) + col fixed POSITIVE(i) { i + 1 }; + col fixed FIRST = [1] + [0]*; + col fixed LAST(i) { FIRST(i + 1) }; + col fixed STEP(i) { i }; + + m_change * (1 - m_change) = 0; + + // if m_change is zero, m_addr has to stay the same. + (m_addr' - m_addr) * (1 - m_change) = 0; + + // Except for the last row, if m_change is 1, then m_addr has to increase, + // if it is zero, m_step has to increase. + (1 - LAST) { m_change * (m_addr' - m_addr) + (1 - m_change) * (m_step' - m_step) } in POSITIVE; + + m_op * (1 - m_op) = 0; + m_is_write * (1 - m_is_write) = 0; + m_is_read * (1 - m_is_read) = 0; + // m_is_write can only be 1 if m_op is 1. + m_is_write * (1 - m_op) = 0; + m_is_read * (1 - m_op) = 0; + m_is_read * m_is_write = 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; + + // If the next line is a read and we have an address change, + // then the value is zero. + (1 - m_is_write') * m_change * m_value' = 0; + + + // ============== memory instructions ============== + instr store X { { addr, STEP, X } is m_is_write { m_addr, m_step, m_value } } + instr load -> X { { addr, STEP, X } is m_is_read { m_addr, m_step, m_value } } + + + + /// Add + /// Take in two input registers, send the result into the output register + instr add Y, Z -> X { + X = Y + Z + } + + /// Sub + instr sub Y, Z -> X { + X = Y - Z + } + + /// Is the value equal to 0 - uses only assignment registers + instr eq X -> Y { Y = XIsZero } + + /// Mul + instr mul Y, Z -> X { + X = Y * Z + } + + /// move + // TODO: move should zero out the sending register? + instr mov Y -> X { + X = Y + } + + // When we get a call, we want + instr call l: label { pc' = l, jump_ptr' = pc + 1 } + instr ret { pc' = jump_ptr } + + /// Jumps + instr jump l: label { pc' = l } + instr jumpi X, l: label { pc' = (1 - XIsZero) * l + XIsZero * (pc + 1) } + instr jumpni X, l: label { pc' = XIsZero * l + (1 - XIsZero) * (pc + 1) } + diff --git a/bberg/brillig_out.asm b/bberg/brillig_out.asm new file mode 100644 index 0000000000..3af9de9ff1 --- /dev/null +++ b/bberg/brillig_out.asm @@ -0,0 +1,137 @@ + +machine Main { + + + degree 256; + + reg pc[@pc]; + reg X[<=]; + reg Y[<=]; + reg Z[<=]; + + reg jump_ptr; // Store the location of a call + reg addr; // used for memory operations + reg tmp; // used for temporary storage + reg r0; // 12 registers for now + reg r1; + reg r2; + reg r3; + reg r4; + reg r5; + reg r6; + reg r7; + reg r8; + reg r9; + reg r10; + reg r11; + + // ============== iszero check for X ======================= + col witness XInv; + col witness XIsZero; + XIsZero = 1 - X * XInv; + XIsZero * X = 0; + XIsZero * (1 - XIsZero) = 0; + + + // =============== read-write memory ======================= + // Read-write memory. Columns are sorted by m_addr and + // then by m_step. m_change is 1 if and only if m_addr changes + // in the next row. + col witness m_addr; + col witness m_step; + col witness m_change; + col witness m_value; + // If we have an operation at all (needed because this needs to be a permutation) + col witness m_op; + // If the operation is a write operation. + col witness m_is_write; + col witness m_is_read; + + // positive numbers (assumed to be much smaller than the field order) + col fixed POSITIVE(i) { i + 1 }; + col fixed FIRST = [1] + [0]*; + col fixed LAST(i) { FIRST(i + 1) }; + col fixed STEP(i) { i }; + + m_change * (1 - m_change) = 0; + + // if m_change is zero, m_addr has to stay the same. + (m_addr' - m_addr) * (1 - m_change) = 0; + + // Except for the last row, if m_change is 1, then m_addr has to increase, + // if it is zero, m_step has to increase. + (1 - LAST) { m_change * (m_addr' - m_addr) + (1 - m_change) * (m_step' - m_step) } in POSITIVE; + + m_op * (1 - m_op) = 0; + m_is_write * (1 - m_is_write) = 0; + m_is_read * (1 - m_is_read) = 0; + // m_is_write can only be 1 if m_op is 1. + m_is_write * (1 - m_op) = 0; + m_is_read * (1 - m_op) = 0; + m_is_read * m_is_write = 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; + + // If the next line is a read and we have an address change, + // then the value is zero. + (1 - m_is_write') * m_change * m_value' = 0; + + + // ============== memory instructions ============== + instr store X { { addr, STEP, X } is m_is_write { m_addr, m_step, m_value } } + instr load -> X { { addr, STEP, X } is m_is_read { m_addr, m_step, m_value } } + + + + /// Add + /// Take in two input registers, send the result into the output register + instr add Y, Z -> X { + X = Y + Z + } + + /// Sub + instr sub Y, Z -> X { + X = Y - Z + } + + /// Is the value equal to 0 - uses only assignment registers + instr eq X -> Y { Y = XIsZero } + + /// Mul + instr mul Y, Z -> X { + X = Y * Z + } + + /// move + // TODO: move should zero out the sending register? + instr mov Y -> X { + X = Y + } + + // When we get a call, we want + instr call l: label { pc' = l, jump_ptr' = pc + 1 } + instr ret { pc' = jump_ptr } + + /// Jumps + instr jump l: label { pc' = l } + instr jumpi X, l: label { pc' = (1 - XIsZero) * l + XIsZero * (pc + 1) } + instr jumpni X, l: label { pc' = XIsZero * l + (1 - XIsZero) * (pc + 1) } + + + + function main { + r0 <=X= 0; + r1 <=X= 0; + call bbdf; + return; + bbdf:: + r3 <=X= 3; + ret; + } +} diff --git a/aztec/bytecode.acir b/bberg/bytecode.acir similarity index 100% rename from aztec/bytecode.acir rename to bberg/bytecode.acir diff --git a/aztec/node_modules/.yarn-integrity b/bberg/node_modules/.yarn-integrity similarity index 100% rename from aztec/node_modules/.yarn-integrity rename to bberg/node_modules/.yarn-integrity diff --git a/bberg/src/bberg_codegen.rs b/bberg/src/bberg_codegen.rs new file mode 100644 index 0000000000..0eeeae68d0 --- /dev/null +++ b/bberg/src/bberg_codegen.rs @@ -0,0 +1,48 @@ +use ast::analyzed::Analyzed; +use std::{io, str::FromStr}; + +use number::{BigInt, Bn254Field, DegreeType, FieldElement}; + +use crate::circuit_builder::analyzed_to_cpp; + +/// Barretenberg codegen +/// +/// This module will take pil compiler output and make it generate relation header files that can be compiled into bberg + +pub struct BBergCodegen { + // Note: Im not sure we need to know the degree ahead of time + // degree: DegreeType, +} + +impl BBergCodegen { + pub fn new(_degree: DegreeType) -> Self { + Self {} + } + + pub fn new_from_setup(input: &mut impl io::Read) -> Result { + println!("warning bberg: new_from_setup not implemented"); + Ok(Self {}) + } + + // Note: only returns vec to keep with the interface + pub fn build_ast( + &self, + pil: &Analyzed, + fixed: &[(&str, Vec)], + witness: &[(&str, Vec)], + ) -> Vec { + let circuit = analyzed_to_cpp(pil, fixed, witness); + + Vec::new() + } + + pub fn assert_field_is_compatible() { + if Bn254Field::modulus().to_arbitrary_integer() != F::modulus().to_arbitrary_integer() { + panic!("powdr modulus doesn't match halo2 modulus. Make sure you are using Bn254"); + } + } +} + +// static str& template = r#" + +// "#; diff --git a/bberg/src/circuit_builder.rs b/bberg/src/circuit_builder.rs new file mode 100644 index 0000000000..f0063b9eeb --- /dev/null +++ b/bberg/src/circuit_builder.rs @@ -0,0 +1,453 @@ +use std::{fmt::Display, process::id}; + +use ast::{analyzed::Identity, parsed::BinaryOperator}; +use itertools::Itertools; +use num_bigint::BigUint; + +use ast::analyzed::{Analyzed, Expression, IdentityKind, Reference, SelectedExpressions}; +use num_traits::{identities, One}; +use number::{BigInt, FieldElement}; + +// use super::circuit_data::CircuitData; + +use pil_analyzer::pil_analyzer::inline_intermediate_polynomials; + +pub(crate) fn analyzed_to_cpp( + analyzed: &Analyzed, + fixed: &[(&str, Vec)], + witness: &[(&str, Vec)], +) -> String { + let all_rows = get_all_row_names(fixed, witness); + + let row_type = create_row_type(&all_rows); + + let identities = create_identities(&analyzed.identities, &all_rows); + + // These are all of the exotic ish data structures we will need + // let mut lookups = vec![]; + // let mut perms = vec![]; + // let mut polys = vec![]; + + // // From all of the fixed and witness columns we have, we want to create the row object for bb + + // // Note: we do not have lookups yet + // assert!(lookups.len() == 0, "lookups not implemented"); + + "ye-haw".to_owned() +} + +// As all of our rows are annotated, we should be able to create +// the row type by hand here +// The row type is a combination of the fixed and witness columns + +// The include statements required for a new relation file +fn relation_includes() -> &'static str { + r#" +#pragma once +#include "../relation_parameters.hpp" +#include "../relation_types.hpp" +"# +} + +// Yucky that everything is allocated into vecs here +fn create_row_type_items(names: &Vec) -> Vec { + names + .iter() + .map(|name| format!(" FF {};", name)) + .collect::>() +} + +fn get_all_row_names( + fixed: &[(&str, Vec)], + witness: &[(&str, Vec)], +) -> Vec { + let fixed_names: Vec = fixed.iter().map(|(name, _)| (*name).to_owned()).collect(); + let witness_names: Vec = witness.iter().map(|(name, _)| (*name).to_owned()).collect(); + + let shift_names: Vec = witness + .iter() + .map(|(name, _)| format!("{}_shift", *name)) + .collect(); + + // h/t kev + [fixed_names, witness_names, shift_names] + .into_iter() + .flatten() + .collect() +} + +// Each vm will need to have a row which is a combination of all of the witness columns +fn create_row_type(all_rows: &Vec) -> String { + let all_annotated = create_row_type_items(all_rows); + + let row_type = format!( + "template struct Row {{ \n{}\n }}", + all_annotated.join("\n"), + ); + + println!("{}", row_type); + row_type +} + +// Get the boiler plate to access rows +fn get_cols_in_identity(row_index: usize, all_rows: &Vec) -> String { + let template = format!("\nusing View = typename std::tuple_element<{}, typename AccumulatorTypes::AccumulatorViews>::type;\n", row_index); + let col_accesses: Vec = all_rows + .iter() + .map(|col_name| format!("auto {} = View(new_term.{});\n", col_name, col_name)) + .collect(); + + return template + &col_accesses.join("\n"); +} + +fn create_identity( + row_index: usize, + expression: SelectedExpressions, + all_rows: &Vec, +) -> String { + // We want to read the types of operators and then create the appropiate code + + "output".to_owned() +} + +/// Todo, eventually these will need to be siloed based on the file name they are in +fn create_identities( + identities: &Vec>, + all_rows: &Vec, +) -> String { + // We only want the expressions for now + // When we have a poly type, we only need the left side of it + let expressions = identities + .iter() + .filter_map(|identity| { + if identity.kind == IdentityKind::Polynomial { + Some(identity.left.clone()) + } else { + None + } + }) + .collect::>(); + + for expression in expressions { + dbg!(&expression); + } + + "The output".to_owned() +} + +// /// &_analyzed.identities = [ +// Identity { +// id: 0, +// kind: Polynomial, +// source: SourceRef { +// file: "fibonacci.pil", +// line: 12, +// }, +// left: SelectedExpressions { +// selector: Some( +// BinaryOperation( +// Reference( +// Poly( +// PolynomialReference { +// name: "Fibonacci.ISLAST", +// poly_id: Some( +// PolyID { +// id: 0, +// ptype: Constant, +// }, +// ), +// index: None, +// next: false, +// }, +// ), +// ), +// Mul, +// BinaryOperation( +// Reference( +// Poly( +// PolynomialReference { +// name: "Fibonacci.y", +// poly_id: Some( +// PolyID { +// id: 1, +// ptype: Committed, +// }, +// ), +// index: None, +// next: true, +// }, +// ), +// ), +// Sub, +// Number( +// Bn254Field { +// value: BigInt( +// [ +// 1, +// 0, +// 0, +// 0, +// ], +// ), +// }, +// ), +// ), +// ), +// ), +// expressions: [], +// }, +// right: SelectedExpressions { +// selector: None, +// expressions: [], +// }, +// }, +// Identity { +// id: 1, +// kind: Polynomial, +// source: SourceRef { +// file: "fibonacci.pil", +// line: 13, +// }, +// left: SelectedExpressions { +// selector: Some( +// BinaryOperation( +// Reference( +// Poly( +// PolynomialReference { +// name: "Fibonacci.ISLAST", +// poly_id: Some( +// PolyID { +// id: 0, +// ptype: Constant, +// }, +// ), +// index: None, +// next: false, +// }, +// ), +// ), +// Mul, +// BinaryOperation( +// Reference( +// Poly( +// PolynomialReference { +// name: "Fibonacci.x", +// poly_id: Some( +// PolyID { +// id: 0, +// ptype: Committed, +// }, +// ), +// index: None, +// next: true, +// }, +// ), +// ), +// Sub, +// Number( +// Bn254Field { +// value: BigInt( +// [ +// 1, +// 0, +// 0, +// 0, +// ], +// ), +// }, +// ), +// ), +// ), +// ), +// expressions: [], +// }, +// right: SelectedExpressions { +// selector: None, +// expressions: [], +// }, +// }, +// Identity { +// id: 2, +// kind: Polynomial, +// source: SourceRef { +// file: "fibonacci.pil", +// line: 15, +// }, +// left: SelectedExpressions { +// selector: Some( +// BinaryOperation( +// BinaryOperation( +// Number( +// Bn254Field { +// value: BigInt( +// [ +// 1, +// 0, +// 0, +// 0, +// ], +// ), +// }, +// ), +// Sub, +// Reference( +// Poly( +// PolynomialReference { +// name: "Fibonacci.ISLAST", +// poly_id: Some( +// PolyID { +// id: 0, +// ptype: Constant, +// }, +// ), +// index: None, +// next: false, +// }, +// ), +// ), +// ), +// Mul, +// BinaryOperation( +// Reference( +// Poly( +// PolynomialReference { +// name: "Fibonacci.x", +// poly_id: Some( +// PolyID { +// id: 0, +// ptype: Committed, +// }, +// ), +// index: None, +// next: true, +// }, +// ), +// ), +// Sub, +// Reference( +// Poly( +// PolynomialReference { +// name: "Fibonacci.y", +// poly_id: Some( +// PolyID { +// id: 1, +// ptype: Committed, +// }, +// ), +// index: None, +// next: false, +// }, +// ), +// ), +// ), +// ), +// ), +// expressions: [], +// }, +// right: SelectedExpressions { +// selector: None, +// expressions: [], +// }, +// }, +// Identity { +// id: 3, +// kind: Polynomial, +// source: SourceRef { +// file: "fibonacci.pil", +// line: 16, +// }, +// left: SelectedExpressions { +// selector: Some( +// BinaryOperation( +// BinaryOperation( +// Number( +// Bn254Field { +// value: BigInt( +// [ +// 1, +// 0, +// 0, +// 0, +// ], +// ), +// }, +// ), +// Sub, +// Reference( +// Poly( +// PolynomialReference { +// name: "Fibonacci.ISLAST", +// poly_id: Some( +// PolyID { +// id: 0, +// ptype: Constant, +// }, +// ), +// index: None, +// next: false, +// }, +// ), +// ), +// ), +// Mul, +// BinaryOperation( +// Reference( +// Poly( +// PolynomialReference { +// name: "Fibonacci.y", +// poly_id: Some( +// PolyID { +// id: 1, +// ptype: Committed, +// }, +// ), +// index: None, +// next: true, +// }, +// ), +// ), +// Sub, +// BinaryOperation( +// Reference( +// Poly( +// PolynomialReference { +// name: "Fibonacci.x", +// poly_id: Some( +// PolyID { +// id: 0, +// ptype: Committed, +// }, +// ), +// index: None, +// next: false, +// }, +// ), +// ), +// Add, +// Reference( +// Poly( +// PolynomialReference { +// name: "Fibonacci.y", +// poly_id: Some( +// PolyID { +// id: 1, +// ptype: Committed, +// }, +// ), +// index: None, +// next: false, +// }, +// ), +// ), +// ), +// ), +// ), +// ), +// expressions: [], +// }, +// right: SelectedExpressions { +// selector: None, +// expressions: [], +// }, +// }, +// ] diff --git a/bberg/src/lib.rs b/bberg/src/lib.rs new file mode 100644 index 0000000000..1c67d60210 --- /dev/null +++ b/bberg/src/lib.rs @@ -0,0 +1,2 @@ +pub mod bberg_codegen; +pub mod circuit_builder; diff --git a/aztec/src/main.rs b/bberg/src/main.rs similarity index 99% rename from aztec/src/main.rs rename to bberg/src/main.rs index f298702ace..277902b220 100644 --- a/aztec/src/main.rs +++ b/bberg/src/main.rs @@ -12,6 +12,9 @@ use std::iter; use std::collections::HashMap; + + + /// Module to convert brillig assmebly into powdr assembly // struct BrilligArchitecture {} diff --git a/aztec/tut/hello.asm b/bberg/tut/hello.asm similarity index 100% rename from aztec/tut/hello.asm rename to bberg/tut/hello.asm diff --git a/brillig.pil b/brillig.pil new file mode 100644 index 0000000000..cea4a71d14 --- /dev/null +++ b/brillig.pil @@ -0,0 +1,333 @@ +namespace main(256); +pol commit XInv; +pol commit XIsZero; +XIsZero = (1 - (X * XInv)); +(XIsZero * X) = 0; +(XIsZero * (1 - XIsZero)) = 0; +pol commit m_addr; +pol commit m_step; +pol commit m_change; +pol commit m_value; +pol commit m_op; +pol commit m_is_write; +pol commit m_is_read; +pol constant POSITIVE(i) { (i + 1) }; +pol constant FIRST = [1] + [0]*; +pol constant LAST(i) { FIRST((i + 1)) }; +pol constant STEP(i) { i }; +(m_change * (1 - m_change)) = 0; +((m_addr' - m_addr) * (1 - m_change)) = 0; +(1 - LAST) { ((m_change * (m_addr' - m_addr)) + ((1 - m_change) * (m_step' - m_step))) } in { POSITIVE }; +(m_op * (1 - m_op)) = 0; +(m_is_write * (1 - m_is_write)) = 0; +(m_is_read * (1 - m_is_read)) = 0; +(m_is_write * (1 - m_op)) = 0; +(m_is_read * (1 - m_op)) = 0; +(m_is_read * m_is_write) = 0; +(((1 - m_is_write') * (1 - m_change)) * (m_value' - m_value)) = 0; +(((1 - m_is_write') * m_change) * m_value') = 0; +pol commit _operation_id; +pol commit _sigma; +pol constant _romgen_first_step = [1] + [0]*; +_sigma' = ((1 - _romgen_first_step') * (_sigma + instr_return)); +(_sigma * (_operation_id - 8)) = 0; +pol commit pc; +pol commit X; +pol commit Y; +pol commit Z; +pol commit reg_write_X_jump_ptr; +pol commit reg_write_Y_jump_ptr; +pol commit reg_write_Z_jump_ptr; +pol commit jump_ptr; +pol commit reg_write_X_addr; +pol commit reg_write_Y_addr; +pol commit reg_write_Z_addr; +pol commit addr; +pol commit reg_write_X_tmp; +pol commit reg_write_Y_tmp; +pol commit reg_write_Z_tmp; +pol commit tmp; +pol commit reg_write_X_r0; +pol commit reg_write_Y_r0; +pol commit reg_write_Z_r0; +pol commit r0; +pol commit reg_write_X_r1; +pol commit reg_write_Y_r1; +pol commit reg_write_Z_r1; +pol commit r1; +pol commit reg_write_X_r2; +pol commit reg_write_Y_r2; +pol commit reg_write_Z_r2; +pol commit r2; +pol commit reg_write_X_r3; +pol commit reg_write_Y_r3; +pol commit reg_write_Z_r3; +pol commit r3; +pol commit reg_write_X_r4; +pol commit reg_write_Y_r4; +pol commit reg_write_Z_r4; +pol commit r4; +pol commit reg_write_X_r5; +pol commit reg_write_Y_r5; +pol commit reg_write_Z_r5; +pol commit r5; +pol commit reg_write_X_r6; +pol commit reg_write_Y_r6; +pol commit reg_write_Z_r6; +pol commit r6; +pol commit reg_write_X_r7; +pol commit reg_write_Y_r7; +pol commit reg_write_Z_r7; +pol commit r7; +pol commit reg_write_X_r8; +pol commit reg_write_Y_r8; +pol commit reg_write_Z_r8; +pol commit r8; +pol commit reg_write_X_r9; +pol commit reg_write_Y_r9; +pol commit reg_write_Z_r9; +pol commit r9; +pol commit reg_write_X_r10; +pol commit reg_write_Y_r10; +pol commit reg_write_Z_r10; +pol commit r10; +pol commit reg_write_X_r11; +pol commit reg_write_Y_r11; +pol commit reg_write_Z_r11; +pol commit r11; +pol commit instr_store; +instr_store { addr, STEP, X } is m_is_write { m_addr, m_step, m_value }; +pol commit instr_load; +instr_load { addr, STEP, X } is m_is_read { m_addr, m_step, m_value }; +pol commit instr_add; +(instr_add * (X - (Y + Z))) = 0; +pol commit instr_sub; +(instr_sub * (X - (Y - Z))) = 0; +pol commit instr_eq; +(instr_eq * (Y - XIsZero)) = 0; +pol commit instr_mul; +(instr_mul * (X - (Y * Z))) = 0; +pol commit instr_mov; +(instr_mov * (X - Y)) = 0; +pol commit instr_call; +pol commit instr_call_param_l; +pol commit instr_ret; +pol commit instr_jump; +pol commit instr_jump_param_l; +pol commit instr_jumpi; +pol commit instr_jumpi_param_l; +pol instr_jumpi_pc_update = ((1 - XIsZero) * instr_jumpi_param_l); +pol instr_jumpi_pc_update_1 = (XIsZero * (pc + 1)); +pol commit instr_jumpni; +pol commit instr_jumpni_param_l; +pol instr_jumpni_pc_update = (XIsZero * instr_jumpni_param_l); +pol instr_jumpni_pc_update_1 = ((1 - XIsZero) * (pc + 1)); +pol commit instr__jump_to_operation; +pol commit instr__reset; +pol commit instr__loop; +pol commit instr_return; +pol commit X_const; +pol commit X_read_free; +pol commit read_X_addr; +pol commit read_X_jump_ptr; +pol commit read_X_r0; +pol commit read_X_r1; +pol commit read_X_r10; +pol commit read_X_r11; +pol commit read_X_r2; +pol commit read_X_r3; +pol commit read_X_r4; +pol commit read_X_r5; +pol commit read_X_r6; +pol commit read_X_r7; +pol commit read_X_r8; +pol commit read_X_r9; +pol commit read_X_tmp; +pol commit read_X_pc; +X = ((((((((((((((((((read_X_addr * addr) + (read_X_jump_ptr * jump_ptr)) + (read_X_r0 * r0)) + (read_X_r1 * r1)) + (read_X_r10 * r10)) + (read_X_r11 * r11)) + (read_X_r2 * r2)) + (read_X_r3 * r3)) + (read_X_r4 * r4)) + (read_X_r5 * r5)) + (read_X_r6 * r6)) + (read_X_r7 * r7)) + (read_X_r8 * r8)) + (read_X_r9 * r9)) + (read_X_tmp * tmp)) + (read_X_pc * pc)) + X_const) + (X_read_free * X_free_value)); +pol commit Y_const; +pol commit Y_read_free; +pol commit read_Y_addr; +pol commit read_Y_jump_ptr; +pol commit read_Y_r0; +pol commit read_Y_r1; +pol commit read_Y_r10; +pol commit read_Y_r11; +pol commit read_Y_r2; +pol commit read_Y_r3; +pol commit read_Y_r4; +pol commit read_Y_r5; +pol commit read_Y_r6; +pol commit read_Y_r7; +pol commit read_Y_r8; +pol commit read_Y_r9; +pol commit read_Y_tmp; +pol commit read_Y_pc; +Y = ((((((((((((((((((read_Y_addr * addr) + (read_Y_jump_ptr * jump_ptr)) + (read_Y_r0 * r0)) + (read_Y_r1 * r1)) + (read_Y_r10 * r10)) + (read_Y_r11 * r11)) + (read_Y_r2 * r2)) + (read_Y_r3 * r3)) + (read_Y_r4 * r4)) + (read_Y_r5 * r5)) + (read_Y_r6 * r6)) + (read_Y_r7 * r7)) + (read_Y_r8 * r8)) + (read_Y_r9 * r9)) + (read_Y_tmp * tmp)) + (read_Y_pc * pc)) + Y_const) + (Y_read_free * Y_free_value)); +pol commit Z_const; +pol commit Z_read_free; +pol commit read_Z_addr; +pol commit read_Z_jump_ptr; +pol commit read_Z_r0; +pol commit read_Z_r1; +pol commit read_Z_r10; +pol commit read_Z_r11; +pol commit read_Z_r2; +pol commit read_Z_r3; +pol commit read_Z_r4; +pol commit read_Z_r5; +pol commit read_Z_r6; +pol commit read_Z_r7; +pol commit read_Z_r8; +pol commit read_Z_r9; +pol commit read_Z_tmp; +pol commit read_Z_pc; +Z = ((((((((((((((((((read_Z_addr * addr) + (read_Z_jump_ptr * jump_ptr)) + (read_Z_r0 * r0)) + (read_Z_r1 * r1)) + (read_Z_r10 * r10)) + (read_Z_r11 * r11)) + (read_Z_r2 * r2)) + (read_Z_r3 * r3)) + (read_Z_r4 * r4)) + (read_Z_r5 * r5)) + (read_Z_r6 * r6)) + (read_Z_r7 * r7)) + (read_Z_r8 * r8)) + (read_Z_r9 * r9)) + (read_Z_tmp * tmp)) + (read_Z_pc * pc)) + Z_const) + (Z_read_free * Z_free_value)); +pol constant first_step = [1] + [0]*; +addr' = (((((reg_write_X_addr * X) + (reg_write_Y_addr * Y)) + (reg_write_Z_addr * Z)) + (instr__reset * 0)) + ((1 - (((reg_write_X_addr + reg_write_Y_addr) + reg_write_Z_addr) + instr__reset)) * addr)); +jump_ptr' = ((((((reg_write_X_jump_ptr * X) + (reg_write_Y_jump_ptr * Y)) + (reg_write_Z_jump_ptr * Z)) + (instr_call * (pc + 1))) + (instr__reset * 0)) + ((1 - ((((reg_write_X_jump_ptr + reg_write_Y_jump_ptr) + reg_write_Z_jump_ptr) + instr_call) + instr__reset)) * jump_ptr)); +pol pc_update = (((((((((instr_call * instr_call_param_l) + (instr_ret * jump_ptr)) + (instr_jump * instr_jump_param_l)) + (instr_jumpi * (instr_jumpi_pc_update + instr_jumpi_pc_update_1))) + (instr_jumpni * (instr_jumpni_pc_update + instr_jumpni_pc_update_1))) + (instr__jump_to_operation * _operation_id)) + (instr__loop * pc)) + (instr_return * 0)) + ((1 - (((((((instr_call + instr_ret) + instr_jump) + instr_jumpi) + instr_jumpni) + instr__jump_to_operation) + instr__loop) + instr_return)) * (pc + 1))); +pc' = ((1 - first_step') * pc_update); +r0' = (((((reg_write_X_r0 * X) + (reg_write_Y_r0 * Y)) + (reg_write_Z_r0 * Z)) + (instr__reset * 0)) + ((1 - (((reg_write_X_r0 + reg_write_Y_r0) + reg_write_Z_r0) + instr__reset)) * r0)); +r1' = (((((reg_write_X_r1 * X) + (reg_write_Y_r1 * Y)) + (reg_write_Z_r1 * Z)) + (instr__reset * 0)) + ((1 - (((reg_write_X_r1 + reg_write_Y_r1) + reg_write_Z_r1) + instr__reset)) * r1)); +r10' = (((((reg_write_X_r10 * X) + (reg_write_Y_r10 * Y)) + (reg_write_Z_r10 * Z)) + (instr__reset * 0)) + ((1 - (((reg_write_X_r10 + reg_write_Y_r10) + reg_write_Z_r10) + instr__reset)) * r10)); +r11' = (((((reg_write_X_r11 * X) + (reg_write_Y_r11 * Y)) + (reg_write_Z_r11 * Z)) + (instr__reset * 0)) + ((1 - (((reg_write_X_r11 + reg_write_Y_r11) + reg_write_Z_r11) + instr__reset)) * r11)); +r2' = (((((reg_write_X_r2 * X) + (reg_write_Y_r2 * Y)) + (reg_write_Z_r2 * Z)) + (instr__reset * 0)) + ((1 - (((reg_write_X_r2 + reg_write_Y_r2) + reg_write_Z_r2) + instr__reset)) * r2)); +r3' = (((((reg_write_X_r3 * X) + (reg_write_Y_r3 * Y)) + (reg_write_Z_r3 * Z)) + (instr__reset * 0)) + ((1 - (((reg_write_X_r3 + reg_write_Y_r3) + reg_write_Z_r3) + instr__reset)) * r3)); +r4' = (((((reg_write_X_r4 * X) + (reg_write_Y_r4 * Y)) + (reg_write_Z_r4 * Z)) + (instr__reset * 0)) + ((1 - (((reg_write_X_r4 + reg_write_Y_r4) + reg_write_Z_r4) + instr__reset)) * r4)); +r5' = (((((reg_write_X_r5 * X) + (reg_write_Y_r5 * Y)) + (reg_write_Z_r5 * Z)) + (instr__reset * 0)) + ((1 - (((reg_write_X_r5 + reg_write_Y_r5) + reg_write_Z_r5) + instr__reset)) * r5)); +r6' = (((((reg_write_X_r6 * X) + (reg_write_Y_r6 * Y)) + (reg_write_Z_r6 * Z)) + (instr__reset * 0)) + ((1 - (((reg_write_X_r6 + reg_write_Y_r6) + reg_write_Z_r6) + instr__reset)) * r6)); +r7' = (((((reg_write_X_r7 * X) + (reg_write_Y_r7 * Y)) + (reg_write_Z_r7 * Z)) + (instr__reset * 0)) + ((1 - (((reg_write_X_r7 + reg_write_Y_r7) + reg_write_Z_r7) + instr__reset)) * r7)); +r8' = (((((reg_write_X_r8 * X) + (reg_write_Y_r8 * Y)) + (reg_write_Z_r8 * Z)) + (instr__reset * 0)) + ((1 - (((reg_write_X_r8 + reg_write_Y_r8) + reg_write_Z_r8) + instr__reset)) * r8)); +r9' = (((((reg_write_X_r9 * X) + (reg_write_Y_r9 * Y)) + (reg_write_Z_r9 * Z)) + (instr__reset * 0)) + ((1 - (((reg_write_X_r9 + reg_write_Y_r9) + reg_write_Z_r9) + instr__reset)) * r9)); +tmp' = (((((reg_write_X_tmp * X) + (reg_write_Y_tmp * Y)) + (reg_write_Z_tmp * Z)) + (instr__reset * 0)) + ((1 - (((reg_write_X_tmp + reg_write_Y_tmp) + reg_write_Z_tmp) + instr__reset)) * tmp)); +pol constant p_line = [0, 1, 2, 3, 4, 5, 6, 7, 8] + [8]*; +pol commit X_free_value(i) query match pc { }; +pol commit Y_free_value(i) query match pc { }; +pol commit Z_free_value(i) query match pc { }; +pol constant p_X_const = [0, 0, 0, 3, 0, 0, 0, 0, 0] + [0]*; +pol constant p_X_read_free = [0, 0, 0, 0, 1, 1, 0, 0, 0] + [0]*; +pol constant p_Y_const = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_Y_read_free = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_Z_const = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_Z_read_free = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_instr__jump_to_operation = [0, 1, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_instr__loop = [0, 0, 0, 0, 0, 0, 0, 0, 1] + [1]*; +pol constant p_instr__reset = [1, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_instr_add = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_instr_call = [0, 0, 1, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_instr_call_param_l = [0, 0, 3, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_instr_eq = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_instr_jump = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_instr_jump_param_l = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_instr_jumpi = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_instr_jumpi_param_l = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_instr_jumpni = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_instr_jumpni_param_l = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_instr_load = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_instr_mov = [0, 0, 0, 0, 1, 1, 0, 0, 0] + [0]*; +pol constant p_instr_mul = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_instr_ret = [0, 0, 0, 0, 0, 0, 1, 0, 0] + [0]*; +pol constant p_instr_return = [0, 0, 0, 0, 0, 0, 0, 1, 0] + [0]*; +pol constant p_instr_store = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_instr_sub = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_X_addr = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_X_jump_ptr = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_X_pc = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_X_r0 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_X_r1 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_X_r10 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_X_r11 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_X_r2 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_X_r3 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_X_r4 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_X_r5 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_X_r6 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_X_r7 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_X_r8 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_X_r9 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_X_tmp = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Y_addr = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Y_jump_ptr = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Y_pc = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Y_r0 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Y_r1 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Y_r10 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Y_r11 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Y_r2 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Y_r3 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Y_r4 = [0, 0, 0, 0, 1, 1, 0, 0, 0] + [0]*; +pol constant p_read_Y_r5 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Y_r6 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Y_r7 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Y_r8 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Y_r9 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Y_tmp = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Z_addr = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Z_jump_ptr = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Z_pc = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Z_r0 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Z_r1 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Z_r10 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Z_r11 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Z_r2 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Z_r3 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Z_r4 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Z_r5 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Z_r6 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Z_r7 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Z_r8 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Z_r9 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Z_tmp = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_X_addr = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_X_jump_ptr = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_X_r0 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_X_r1 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_X_r10 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_X_r11 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_X_r2 = [0, 0, 0, 0, 0, 1, 0, 0, 0] + [0]*; +pol constant p_reg_write_X_r3 = [0, 0, 0, 1, 1, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_X_r4 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_X_r5 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_X_r6 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_X_r7 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_X_r8 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_X_r9 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_X_tmp = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Y_addr = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Y_jump_ptr = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Y_r0 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Y_r1 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Y_r10 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Y_r11 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Y_r2 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Y_r3 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Y_r4 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Y_r5 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Y_r6 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Y_r7 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Y_r8 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Y_r9 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Y_tmp = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Z_addr = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Z_jump_ptr = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Z_r0 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Z_r1 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Z_r10 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Z_r11 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Z_r2 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Z_r3 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Z_r4 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Z_r5 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Z_r6 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Z_r7 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Z_r8 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Z_r9 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Z_tmp = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +{ pc, reg_write_X_jump_ptr, reg_write_Y_jump_ptr, reg_write_Z_jump_ptr, reg_write_X_addr, reg_write_Y_addr, reg_write_Z_addr, reg_write_X_tmp, reg_write_Y_tmp, reg_write_Z_tmp, reg_write_X_r0, reg_write_Y_r0, reg_write_Z_r0, reg_write_X_r1, reg_write_Y_r1, reg_write_Z_r1, reg_write_X_r2, reg_write_Y_r2, reg_write_Z_r2, reg_write_X_r3, reg_write_Y_r3, reg_write_Z_r3, reg_write_X_r4, reg_write_Y_r4, reg_write_Z_r4, reg_write_X_r5, reg_write_Y_r5, reg_write_Z_r5, reg_write_X_r6, reg_write_Y_r6, reg_write_Z_r6, reg_write_X_r7, reg_write_Y_r7, reg_write_Z_r7, reg_write_X_r8, reg_write_Y_r8, reg_write_Z_r8, reg_write_X_r9, reg_write_Y_r9, reg_write_Z_r9, reg_write_X_r10, reg_write_Y_r10, reg_write_Z_r10, reg_write_X_r11, reg_write_Y_r11, reg_write_Z_r11, instr_store, instr_load, instr_add, instr_sub, instr_eq, instr_mul, instr_mov, instr_call, instr_call_param_l, instr_ret, instr_jump, instr_jump_param_l, instr_jumpi, instr_jumpi_param_l, instr_jumpni, instr_jumpni_param_l, instr__jump_to_operation, instr__reset, instr__loop, instr_return, X_const, X_read_free, read_X_addr, read_X_jump_ptr, read_X_r0, read_X_r1, read_X_r10, read_X_r11, read_X_r2, read_X_r3, read_X_r4, read_X_r5, read_X_r6, read_X_r7, read_X_r8, read_X_r9, read_X_tmp, read_X_pc, Y_const, Y_read_free, read_Y_addr, read_Y_jump_ptr, read_Y_r0, read_Y_r1, read_Y_r10, read_Y_r11, read_Y_r2, read_Y_r3, read_Y_r4, read_Y_r5, read_Y_r6, read_Y_r7, read_Y_r8, read_Y_r9, read_Y_tmp, read_Y_pc, Z_const, Z_read_free, read_Z_addr, read_Z_jump_ptr, read_Z_r0, read_Z_r1, read_Z_r10, read_Z_r11, read_Z_r2, read_Z_r3, read_Z_r4, read_Z_r5, read_Z_r6, read_Z_r7, read_Z_r8, read_Z_r9, read_Z_tmp, read_Z_pc } in { p_line, p_reg_write_X_jump_ptr, p_reg_write_Y_jump_ptr, p_reg_write_Z_jump_ptr, p_reg_write_X_addr, p_reg_write_Y_addr, p_reg_write_Z_addr, p_reg_write_X_tmp, p_reg_write_Y_tmp, p_reg_write_Z_tmp, p_reg_write_X_r0, p_reg_write_Y_r0, p_reg_write_Z_r0, p_reg_write_X_r1, p_reg_write_Y_r1, p_reg_write_Z_r1, p_reg_write_X_r2, p_reg_write_Y_r2, p_reg_write_Z_r2, p_reg_write_X_r3, p_reg_write_Y_r3, p_reg_write_Z_r3, p_reg_write_X_r4, p_reg_write_Y_r4, p_reg_write_Z_r4, p_reg_write_X_r5, p_reg_write_Y_r5, p_reg_write_Z_r5, p_reg_write_X_r6, p_reg_write_Y_r6, p_reg_write_Z_r6, p_reg_write_X_r7, p_reg_write_Y_r7, p_reg_write_Z_r7, p_reg_write_X_r8, p_reg_write_Y_r8, p_reg_write_Z_r8, p_reg_write_X_r9, p_reg_write_Y_r9, p_reg_write_Z_r9, p_reg_write_X_r10, p_reg_write_Y_r10, p_reg_write_Z_r10, p_reg_write_X_r11, p_reg_write_Y_r11, p_reg_write_Z_r11, p_instr_store, p_instr_load, p_instr_add, p_instr_sub, p_instr_eq, p_instr_mul, p_instr_mov, p_instr_call, p_instr_call_param_l, p_instr_ret, p_instr_jump, p_instr_jump_param_l, p_instr_jumpi, p_instr_jumpi_param_l, p_instr_jumpni, p_instr_jumpni_param_l, p_instr__jump_to_operation, p_instr__reset, p_instr__loop, p_instr_return, p_X_const, p_X_read_free, p_read_X_addr, p_read_X_jump_ptr, p_read_X_r0, p_read_X_r1, p_read_X_r10, p_read_X_r11, p_read_X_r2, p_read_X_r3, p_read_X_r4, p_read_X_r5, p_read_X_r6, p_read_X_r7, p_read_X_r8, p_read_X_r9, p_read_X_tmp, p_read_X_pc, p_Y_const, p_Y_read_free, p_read_Y_addr, p_read_Y_jump_ptr, p_read_Y_r0, p_read_Y_r1, p_read_Y_r10, p_read_Y_r11, p_read_Y_r2, p_read_Y_r3, p_read_Y_r4, p_read_Y_r5, p_read_Y_r6, p_read_Y_r7, p_read_Y_r8, p_read_Y_r9, p_read_Y_tmp, p_read_Y_pc, p_Z_const, p_Z_read_free, p_read_Z_addr, p_read_Z_jump_ptr, p_read_Z_r0, p_read_Z_r1, p_read_Z_r10, p_read_Z_r11, p_read_Z_r2, p_read_Z_r3, p_read_Z_r4, p_read_Z_r5, p_read_Z_r6, p_read_Z_r7, p_read_Z_r8, p_read_Z_r9, p_read_Z_tmp, p_read_Z_pc }; +pol constant _block_enforcer_last_step = [0]* + [1]; +pol commit _operation_id_no_change; +_operation_id_no_change = ((1 - _block_enforcer_last_step) * (1 - instr_return)); +(_operation_id_no_change * (_operation_id' - _operation_id)) = 0; +pol constant _linker_first_step = [1] + [0]*; +(_linker_first_step * (_operation_id - 2)) = 0; diff --git a/brillig_opt.pil b/brillig_opt.pil new file mode 100644 index 0000000000..fce18d8624 --- /dev/null +++ b/brillig_opt.pil @@ -0,0 +1,121 @@ +namespace main(256); + col witness XInv; + col witness XIsZero; + main.XIsZero = (1 - (main.X * main.XInv)); + (main.XIsZero * main.X) = 0; + (main.XIsZero * (1 - main.XIsZero)) = 0; + col witness m_addr; + col witness m_step; + col witness m_change; + col witness m_value; + col witness m_op; + col witness m_is_write; + col witness m_is_read; + col fixed POSITIVE(i) { (i + 1) }; + col fixed FIRST = [1] + [0]*; + col fixed LAST(i) { main.FIRST((i + 1)) }; + col fixed STEP(i) { i }; + (main.m_change * (1 - main.m_change)) = 0; + ((main.m_addr' - main.m_addr) * (1 - main.m_change)) = 0; + (1 - main.LAST) { ((main.m_change * (main.m_addr' - main.m_addr)) + ((1 - main.m_change) * (main.m_step' - main.m_step))) } in { main.POSITIVE }; + (main.m_op * (1 - main.m_op)) = 0; + (main.m_is_write * (1 - main.m_is_write)) = 0; + (main.m_is_read * (1 - main.m_is_read)) = 0; + (main.m_is_write * (1 - main.m_op)) = 0; + (main.m_is_read * (1 - main.m_op)) = 0; + (main.m_is_read * main.m_is_write) = 0; + (((1 - main.m_is_write') * (1 - main.m_change)) * (main.m_value' - main.m_value)) = 0; + (((1 - main.m_is_write') * main.m_change) * main.m_value') = 0; + col witness _operation_id; + col witness _sigma; + col fixed _romgen_first_step = [1] + [0]*; + main._sigma' = ((1 - main._romgen_first_step') * (main._sigma + main.instr_return)); + (main._sigma * (main._operation_id - 8)) = 0; + col witness pc; + col witness X; + col witness Y; + col witness Z; + col witness jump_ptr; + col witness addr; + col witness tmp; + col witness r0; + col witness r1; + col witness reg_write_X_r2; + col witness r2; + col witness reg_write_X_r3; + col witness r3; + col witness r4; + col witness r5; + col witness r6; + col witness r7; + col witness r8; + col witness r9; + col witness r10; + col witness r11; + 0 { main.addr, main.STEP, main.X } is main.m_is_write { main.m_addr, main.m_step, main.m_value }; + 0 { main.addr, main.STEP, main.X } is main.m_is_read { main.m_addr, main.m_step, main.m_value }; + col witness instr_mov; + (main.instr_mov * (main.X - main.Y)) = 0; + col witness instr_call; + col witness instr_call_param_l; + col witness instr_ret; + col instr_jumpi_pc_update = 0; + col instr_jumpi_pc_update_1 = (main.XIsZero * (main.pc + 1)); + col instr_jumpni_pc_update = 0; + col instr_jumpni_pc_update_1 = ((1 - main.XIsZero) * (main.pc + 1)); + col witness instr__jump_to_operation; + col witness instr__reset; + col witness instr__loop; + col witness instr_return; + col witness X_const; + col witness X_read_free; + main.X = (main.X_const + (main.X_read_free * main.X_free_value)); + col witness read_Y_r4; + main.Y = (main.read_Y_r4 * main.r4); + main.Z = 0; + col fixed first_step = [1] + [0]*; + main.addr' = ((1 - main.instr__reset) * main.addr); + main.jump_ptr' = ((main.instr_call * (main.pc + 1)) + ((1 - (main.instr_call + main.instr__reset)) * main.jump_ptr)); + col pc_update = (((((main.instr_call * main.instr_call_param_l) + (main.instr_ret * main.jump_ptr)) + (main.instr__jump_to_operation * main._operation_id)) + (main.instr__loop * main.pc)) + ((1 - ((((main.instr_call + main.instr_ret) + main.instr__jump_to_operation) + main.instr__loop) + main.instr_return)) * (main.pc + 1))); + main.pc' = ((1 - main.first_step') * main.pc_update); + main.r0' = ((1 - main.instr__reset) * main.r0); + main.r1' = ((1 - main.instr__reset) * main.r1); + main.r10' = ((1 - main.instr__reset) * main.r10); + main.r11' = ((1 - main.instr__reset) * main.r11); + main.r2' = ((main.reg_write_X_r2 * main.X) + ((1 - (main.reg_write_X_r2 + main.instr__reset)) * main.r2)); + main.r3' = ((main.reg_write_X_r3 * main.X) + ((1 - (main.reg_write_X_r3 + main.instr__reset)) * main.r3)); + main.r4' = ((1 - main.instr__reset) * main.r4); + main.r5' = ((1 - main.instr__reset) * main.r5); + main.r6' = ((1 - main.instr__reset) * main.r6); + main.r7' = ((1 - main.instr__reset) * main.r7); + main.r8' = ((1 - main.instr__reset) * main.r8); + main.r9' = ((1 - main.instr__reset) * main.r9); + main.tmp' = ((1 - main.instr__reset) * main.tmp); + col fixed p_line = [0, 1, 2, 3, 4, 5, 6, 7, 8] + [8]*; + col witness X_free_value(i) query match main.pc { }; + col witness Y_free_value(i) query match main.pc { }; + col witness Z_free_value(i) query match main.pc { }; + col fixed p_X_const = [0, 0, 0, 3, 0, 0, 0, 0, 0] + [0]*; + col fixed p_X_read_free = [0, 0, 0, 0, 1, 1, 0, 0, 0] + [0]*; + col fixed p_instr__jump_to_operation = [0, 1, 0, 0, 0, 0, 0, 0, 0] + [0]*; + col fixed p_instr__loop = [0, 0, 0, 0, 0, 0, 0, 0, 1] + [1]*; + col fixed p_instr__reset = [1, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; + col fixed p_instr_call = [0, 0, 1, 0, 0, 0, 0, 0, 0] + [0]*; + col fixed p_instr_call_param_l = [0, 0, 3, 0, 0, 0, 0, 0, 0] + [0]*; + col fixed p_instr_mov = [0, 0, 0, 0, 1, 1, 0, 0, 0] + [0]*; + col fixed p_instr_ret = [0, 0, 0, 0, 0, 0, 1, 0, 0] + [0]*; + col fixed p_instr_return = [0, 0, 0, 0, 0, 0, 0, 1, 0] + [0]*; + col fixed p_read_Y_r4 = [0, 0, 0, 0, 1, 1, 0, 0, 0] + [0]*; + col fixed p_reg_write_X_r2 = [0, 0, 0, 0, 0, 1, 0, 0, 0] + [0]*; + col fixed p_reg_write_X_r3 = [0, 0, 0, 1, 1, 0, 0, 0, 0] + [0]*; + { main.pc, main.reg_write_X_r2, main.reg_write_X_r3, main.instr_mov, main.instr_call, main.instr_call_param_l, main.instr_ret, main.instr__jump_to_operation, main.instr__reset, main.instr__loop, main.instr_return, main.X_const, main.X_read_free, main.read_Y_r4 } in { main.p_line, main.p_reg_write_X_r2, main.p_reg_write_X_r3, main.p_instr_mov, main.p_instr_call, main.p_instr_call_param_l, main.p_instr_ret, main.p_instr__jump_to_operation, main.p_instr__reset, main.p_instr__loop, main.p_instr_return, main.p_X_const, main.p_X_read_free, main.p_read_Y_r4 }; + col fixed _block_enforcer_last_step = [0]* + [1]; + col witness _operation_id_no_change; + main._operation_id_no_change = ((1 - main._block_enforcer_last_step) * (1 - main.instr_return)); + (main._operation_id_no_change * (main._operation_id' - main._operation_id)) = 0; + col fixed _linker_first_step = [1] + [0]*; + (main._linker_first_step * (main._operation_id - 2)) = 0; + { main.pc, main.reg_write_X_r2, main.reg_write_X_r3, main.instr_mov, main.instr_call, main.instr_call_param_l, main.instr_ret, main.instr__jump_to_operation, main.instr__reset, main.instr__loop, main.instr_return, main.X_const, main.X_read_free, main.read_Y_r4 } in { main.p_line, main.p_reg_write_X_r2, main.p_reg_write_X_r3, main.p_instr_mov, main.p_instr_call, main.p_instr_call_param_l, main.p_instr_ret, main.p_instr__jump_to_operation, main.p_instr__reset, main.p_instr__loop, main.p_instr_return, main.p_X_const, main.p_X_read_free, main.p_read_Y_r4 }; + main._operation_id_no_change = ((1 - main._block_enforcer_last_step) * (1 - main.instr_return)); + (main._operation_id_no_change * (main._operation_id' - main._operation_id)) = 0; + (main._linker_first_step * (main._operation_id - 2)) = 0; diff --git a/brillig_out.pil b/brillig_out.pil new file mode 100644 index 0000000000..cddde76885 --- /dev/null +++ b/brillig_out.pil @@ -0,0 +1,333 @@ +namespace main(256); +pol commit XInv; +pol commit XIsZero; +XIsZero = (1 - (X * XInv)); +(XIsZero * X) = 0; +(XIsZero * (1 - XIsZero)) = 0; +pol commit m_addr; +pol commit m_step; +pol commit m_change; +pol commit m_value; +pol commit m_op; +pol commit m_is_write; +pol commit m_is_read; +pol constant POSITIVE(i) { (i + 1) }; +pol constant FIRST = [1] + [0]*; +pol constant LAST(i) { FIRST((i + 1)) }; +pol constant STEP(i) { i }; +(m_change * (1 - m_change)) = 0; +((m_addr' - m_addr) * (1 - m_change)) = 0; +(1 - LAST) { ((m_change * (m_addr' - m_addr)) + ((1 - m_change) * (m_step' - m_step))) } in { POSITIVE }; +(m_op * (1 - m_op)) = 0; +(m_is_write * (1 - m_is_write)) = 0; +(m_is_read * (1 - m_is_read)) = 0; +(m_is_write * (1 - m_op)) = 0; +(m_is_read * (1 - m_op)) = 0; +(m_is_read * m_is_write) = 0; +(((1 - m_is_write') * (1 - m_change)) * (m_value' - m_value)) = 0; +(((1 - m_is_write') * m_change) * m_value') = 0; +pol commit _operation_id; +pol commit _sigma; +pol constant _romgen_first_step = [1] + [0]*; +_sigma' = ((1 - _romgen_first_step') * (_sigma + instr_return)); +(_sigma * (_operation_id - 8)) = 0; +pol commit pc; +pol commit X; +pol commit Y; +pol commit Z; +pol commit reg_write_X_jump_ptr; +pol commit reg_write_Y_jump_ptr; +pol commit reg_write_Z_jump_ptr; +pol commit jump_ptr; +pol commit reg_write_X_addr; +pol commit reg_write_Y_addr; +pol commit reg_write_Z_addr; +pol commit addr; +pol commit reg_write_X_tmp; +pol commit reg_write_Y_tmp; +pol commit reg_write_Z_tmp; +pol commit tmp; +pol commit reg_write_X_r0; +pol commit reg_write_Y_r0; +pol commit reg_write_Z_r0; +pol commit r0; +pol commit reg_write_X_r1; +pol commit reg_write_Y_r1; +pol commit reg_write_Z_r1; +pol commit r1; +pol commit reg_write_X_r2; +pol commit reg_write_Y_r2; +pol commit reg_write_Z_r2; +pol commit r2; +pol commit reg_write_X_r3; +pol commit reg_write_Y_r3; +pol commit reg_write_Z_r3; +pol commit r3; +pol commit reg_write_X_r4; +pol commit reg_write_Y_r4; +pol commit reg_write_Z_r4; +pol commit r4; +pol commit reg_write_X_r5; +pol commit reg_write_Y_r5; +pol commit reg_write_Z_r5; +pol commit r5; +pol commit reg_write_X_r6; +pol commit reg_write_Y_r6; +pol commit reg_write_Z_r6; +pol commit r6; +pol commit reg_write_X_r7; +pol commit reg_write_Y_r7; +pol commit reg_write_Z_r7; +pol commit r7; +pol commit reg_write_X_r8; +pol commit reg_write_Y_r8; +pol commit reg_write_Z_r8; +pol commit r8; +pol commit reg_write_X_r9; +pol commit reg_write_Y_r9; +pol commit reg_write_Z_r9; +pol commit r9; +pol commit reg_write_X_r10; +pol commit reg_write_Y_r10; +pol commit reg_write_Z_r10; +pol commit r10; +pol commit reg_write_X_r11; +pol commit reg_write_Y_r11; +pol commit reg_write_Z_r11; +pol commit r11; +pol commit instr_store; +instr_store { addr, STEP, X } is m_is_write { m_addr, m_step, m_value }; +pol commit instr_load; +instr_load { addr, STEP, X } is m_is_read { m_addr, m_step, m_value }; +pol commit instr_add; +(instr_add * (X - (Y + Z))) = 0; +pol commit instr_sub; +(instr_sub * (X - (Y - Z))) = 0; +pol commit instr_eq; +(instr_eq * (Y - XIsZero)) = 0; +pol commit instr_mul; +(instr_mul * (X - (Y * Z))) = 0; +pol commit instr_mov; +(instr_mov * (X - Y)) = 0; +pol commit instr_call; +pol commit instr_call_param_l; +pol commit instr_ret; +pol commit instr_jump; +pol commit instr_jump_param_l; +pol commit instr_jumpi; +pol commit instr_jumpi_param_l; +pol instr_jumpi_pc_update = ((1 - XIsZero) * instr_jumpi_param_l); +pol instr_jumpi_pc_update_1 = (XIsZero * (pc + 1)); +pol commit instr_jumpni; +pol commit instr_jumpni_param_l; +pol instr_jumpni_pc_update = (XIsZero * instr_jumpni_param_l); +pol instr_jumpni_pc_update_1 = ((1 - XIsZero) * (pc + 1)); +pol commit instr__jump_to_operation; +pol commit instr__reset; +pol commit instr__loop; +pol commit instr_return; +pol commit X_const; +pol commit X_read_free; +pol commit read_X_addr; +pol commit read_X_jump_ptr; +pol commit read_X_r0; +pol commit read_X_r1; +pol commit read_X_r10; +pol commit read_X_r11; +pol commit read_X_r2; +pol commit read_X_r3; +pol commit read_X_r4; +pol commit read_X_r5; +pol commit read_X_r6; +pol commit read_X_r7; +pol commit read_X_r8; +pol commit read_X_r9; +pol commit read_X_tmp; +pol commit read_X_pc; +X = ((((((((((((((((((read_X_addr * addr) + (read_X_jump_ptr * jump_ptr)) + (read_X_r0 * r0)) + (read_X_r1 * r1)) + (read_X_r10 * r10)) + (read_X_r11 * r11)) + (read_X_r2 * r2)) + (read_X_r3 * r3)) + (read_X_r4 * r4)) + (read_X_r5 * r5)) + (read_X_r6 * r6)) + (read_X_r7 * r7)) + (read_X_r8 * r8)) + (read_X_r9 * r9)) + (read_X_tmp * tmp)) + (read_X_pc * pc)) + X_const) + (X_read_free * X_free_value)); +pol commit Y_const; +pol commit Y_read_free; +pol commit read_Y_addr; +pol commit read_Y_jump_ptr; +pol commit read_Y_r0; +pol commit read_Y_r1; +pol commit read_Y_r10; +pol commit read_Y_r11; +pol commit read_Y_r2; +pol commit read_Y_r3; +pol commit read_Y_r4; +pol commit read_Y_r5; +pol commit read_Y_r6; +pol commit read_Y_r7; +pol commit read_Y_r8; +pol commit read_Y_r9; +pol commit read_Y_tmp; +pol commit read_Y_pc; +Y = ((((((((((((((((((read_Y_addr * addr) + (read_Y_jump_ptr * jump_ptr)) + (read_Y_r0 * r0)) + (read_Y_r1 * r1)) + (read_Y_r10 * r10)) + (read_Y_r11 * r11)) + (read_Y_r2 * r2)) + (read_Y_r3 * r3)) + (read_Y_r4 * r4)) + (read_Y_r5 * r5)) + (read_Y_r6 * r6)) + (read_Y_r7 * r7)) + (read_Y_r8 * r8)) + (read_Y_r9 * r9)) + (read_Y_tmp * tmp)) + (read_Y_pc * pc)) + Y_const) + (Y_read_free * Y_free_value)); +pol commit Z_const; +pol commit Z_read_free; +pol commit read_Z_addr; +pol commit read_Z_jump_ptr; +pol commit read_Z_r0; +pol commit read_Z_r1; +pol commit read_Z_r10; +pol commit read_Z_r11; +pol commit read_Z_r2; +pol commit read_Z_r3; +pol commit read_Z_r4; +pol commit read_Z_r5; +pol commit read_Z_r6; +pol commit read_Z_r7; +pol commit read_Z_r8; +pol commit read_Z_r9; +pol commit read_Z_tmp; +pol commit read_Z_pc; +Z = ((((((((((((((((((read_Z_addr * addr) + (read_Z_jump_ptr * jump_ptr)) + (read_Z_r0 * r0)) + (read_Z_r1 * r1)) + (read_Z_r10 * r10)) + (read_Z_r11 * r11)) + (read_Z_r2 * r2)) + (read_Z_r3 * r3)) + (read_Z_r4 * r4)) + (read_Z_r5 * r5)) + (read_Z_r6 * r6)) + (read_Z_r7 * r7)) + (read_Z_r8 * r8)) + (read_Z_r9 * r9)) + (read_Z_tmp * tmp)) + (read_Z_pc * pc)) + Z_const) + (Z_read_free * Z_free_value)); +pol constant first_step = [1] + [0]*; +addr' = (((((reg_write_X_addr * X) + (reg_write_Y_addr * Y)) + (reg_write_Z_addr * Z)) + (instr__reset * 0)) + ((1 - (((reg_write_X_addr + reg_write_Y_addr) + reg_write_Z_addr) + instr__reset)) * addr)); +jump_ptr' = ((((((reg_write_X_jump_ptr * X) + (reg_write_Y_jump_ptr * Y)) + (reg_write_Z_jump_ptr * Z)) + (instr_call * (pc + 1))) + (instr__reset * 0)) + ((1 - ((((reg_write_X_jump_ptr + reg_write_Y_jump_ptr) + reg_write_Z_jump_ptr) + instr_call) + instr__reset)) * jump_ptr)); +pol pc_update = (((((((((instr_call * instr_call_param_l) + (instr_ret * jump_ptr)) + (instr_jump * instr_jump_param_l)) + (instr_jumpi * (instr_jumpi_pc_update + instr_jumpi_pc_update_1))) + (instr_jumpni * (instr_jumpni_pc_update + instr_jumpni_pc_update_1))) + (instr__jump_to_operation * _operation_id)) + (instr__loop * pc)) + (instr_return * 0)) + ((1 - (((((((instr_call + instr_ret) + instr_jump) + instr_jumpi) + instr_jumpni) + instr__jump_to_operation) + instr__loop) + instr_return)) * (pc + 1))); +pc' = ((1 - first_step') * pc_update); +r0' = (((((reg_write_X_r0 * X) + (reg_write_Y_r0 * Y)) + (reg_write_Z_r0 * Z)) + (instr__reset * 0)) + ((1 - (((reg_write_X_r0 + reg_write_Y_r0) + reg_write_Z_r0) + instr__reset)) * r0)); +r1' = (((((reg_write_X_r1 * X) + (reg_write_Y_r1 * Y)) + (reg_write_Z_r1 * Z)) + (instr__reset * 0)) + ((1 - (((reg_write_X_r1 + reg_write_Y_r1) + reg_write_Z_r1) + instr__reset)) * r1)); +r10' = (((((reg_write_X_r10 * X) + (reg_write_Y_r10 * Y)) + (reg_write_Z_r10 * Z)) + (instr__reset * 0)) + ((1 - (((reg_write_X_r10 + reg_write_Y_r10) + reg_write_Z_r10) + instr__reset)) * r10)); +r11' = (((((reg_write_X_r11 * X) + (reg_write_Y_r11 * Y)) + (reg_write_Z_r11 * Z)) + (instr__reset * 0)) + ((1 - (((reg_write_X_r11 + reg_write_Y_r11) + reg_write_Z_r11) + instr__reset)) * r11)); +r2' = (((((reg_write_X_r2 * X) + (reg_write_Y_r2 * Y)) + (reg_write_Z_r2 * Z)) + (instr__reset * 0)) + ((1 - (((reg_write_X_r2 + reg_write_Y_r2) + reg_write_Z_r2) + instr__reset)) * r2)); +r3' = (((((reg_write_X_r3 * X) + (reg_write_Y_r3 * Y)) + (reg_write_Z_r3 * Z)) + (instr__reset * 0)) + ((1 - (((reg_write_X_r3 + reg_write_Y_r3) + reg_write_Z_r3) + instr__reset)) * r3)); +r4' = (((((reg_write_X_r4 * X) + (reg_write_Y_r4 * Y)) + (reg_write_Z_r4 * Z)) + (instr__reset * 0)) + ((1 - (((reg_write_X_r4 + reg_write_Y_r4) + reg_write_Z_r4) + instr__reset)) * r4)); +r5' = (((((reg_write_X_r5 * X) + (reg_write_Y_r5 * Y)) + (reg_write_Z_r5 * Z)) + (instr__reset * 0)) + ((1 - (((reg_write_X_r5 + reg_write_Y_r5) + reg_write_Z_r5) + instr__reset)) * r5)); +r6' = (((((reg_write_X_r6 * X) + (reg_write_Y_r6 * Y)) + (reg_write_Z_r6 * Z)) + (instr__reset * 0)) + ((1 - (((reg_write_X_r6 + reg_write_Y_r6) + reg_write_Z_r6) + instr__reset)) * r6)); +r7' = (((((reg_write_X_r7 * X) + (reg_write_Y_r7 * Y)) + (reg_write_Z_r7 * Z)) + (instr__reset * 0)) + ((1 - (((reg_write_X_r7 + reg_write_Y_r7) + reg_write_Z_r7) + instr__reset)) * r7)); +r8' = (((((reg_write_X_r8 * X) + (reg_write_Y_r8 * Y)) + (reg_write_Z_r8 * Z)) + (instr__reset * 0)) + ((1 - (((reg_write_X_r8 + reg_write_Y_r8) + reg_write_Z_r8) + instr__reset)) * r8)); +r9' = (((((reg_write_X_r9 * X) + (reg_write_Y_r9 * Y)) + (reg_write_Z_r9 * Z)) + (instr__reset * 0)) + ((1 - (((reg_write_X_r9 + reg_write_Y_r9) + reg_write_Z_r9) + instr__reset)) * r9)); +tmp' = (((((reg_write_X_tmp * X) + (reg_write_Y_tmp * Y)) + (reg_write_Z_tmp * Z)) + (instr__reset * 0)) + ((1 - (((reg_write_X_tmp + reg_write_Y_tmp) + reg_write_Z_tmp) + instr__reset)) * tmp)); +pol constant p_line = [0, 1, 2, 3, 4, 5, 6, 7, 8] + [8]*; +pol commit X_free_value(i) query match pc { }; +pol commit Y_free_value(i) query match pc { }; +pol commit Z_free_value(i) query match pc { }; +pol constant p_X_const = [0, 0, 0, 0, 0, 0, 3, 0, 0] + [0]*; +pol constant p_X_read_free = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_Y_const = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_Y_read_free = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_Z_const = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_Z_read_free = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_instr__jump_to_operation = [0, 1, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_instr__loop = [0, 0, 0, 0, 0, 0, 0, 0, 1] + [1]*; +pol constant p_instr__reset = [1, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_instr_add = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_instr_call = [0, 0, 0, 0, 1, 0, 0, 0, 0] + [0]*; +pol constant p_instr_call_param_l = [0, 0, 0, 0, 6, 0, 0, 0, 0] + [0]*; +pol constant p_instr_eq = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_instr_jump = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_instr_jump_param_l = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_instr_jumpi = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_instr_jumpi_param_l = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_instr_jumpni = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_instr_jumpni_param_l = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_instr_load = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_instr_mov = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_instr_mul = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_instr_ret = [0, 0, 0, 0, 0, 0, 0, 1, 0] + [0]*; +pol constant p_instr_return = [0, 0, 0, 0, 0, 1, 0, 0, 0] + [0]*; +pol constant p_instr_store = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_instr_sub = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_X_addr = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_X_jump_ptr = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_X_pc = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_X_r0 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_X_r1 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_X_r10 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_X_r11 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_X_r2 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_X_r3 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_X_r4 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_X_r5 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_X_r6 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_X_r7 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_X_r8 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_X_r9 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_X_tmp = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Y_addr = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Y_jump_ptr = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Y_pc = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Y_r0 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Y_r1 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Y_r10 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Y_r11 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Y_r2 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Y_r3 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Y_r4 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Y_r5 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Y_r6 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Y_r7 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Y_r8 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Y_r9 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Y_tmp = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Z_addr = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Z_jump_ptr = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Z_pc = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Z_r0 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Z_r1 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Z_r10 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Z_r11 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Z_r2 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Z_r3 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Z_r4 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Z_r5 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Z_r6 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Z_r7 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Z_r8 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Z_r9 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Z_tmp = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_X_addr = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_X_jump_ptr = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_X_r0 = [0, 0, 1, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_X_r1 = [0, 0, 0, 1, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_X_r10 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_X_r11 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_X_r2 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_X_r3 = [0, 0, 0, 0, 0, 0, 1, 0, 0] + [0]*; +pol constant p_reg_write_X_r4 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_X_r5 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_X_r6 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_X_r7 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_X_r8 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_X_r9 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_X_tmp = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Y_addr = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Y_jump_ptr = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Y_r0 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Y_r1 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Y_r10 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Y_r11 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Y_r2 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Y_r3 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Y_r4 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Y_r5 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Y_r6 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Y_r7 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Y_r8 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Y_r9 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Y_tmp = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Z_addr = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Z_jump_ptr = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Z_r0 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Z_r1 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Z_r10 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Z_r11 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Z_r2 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Z_r3 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Z_r4 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Z_r5 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Z_r6 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Z_r7 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Z_r8 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Z_r9 = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Z_tmp = [0, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +{ pc, reg_write_X_jump_ptr, reg_write_Y_jump_ptr, reg_write_Z_jump_ptr, reg_write_X_addr, reg_write_Y_addr, reg_write_Z_addr, reg_write_X_tmp, reg_write_Y_tmp, reg_write_Z_tmp, reg_write_X_r0, reg_write_Y_r0, reg_write_Z_r0, reg_write_X_r1, reg_write_Y_r1, reg_write_Z_r1, reg_write_X_r2, reg_write_Y_r2, reg_write_Z_r2, reg_write_X_r3, reg_write_Y_r3, reg_write_Z_r3, reg_write_X_r4, reg_write_Y_r4, reg_write_Z_r4, reg_write_X_r5, reg_write_Y_r5, reg_write_Z_r5, reg_write_X_r6, reg_write_Y_r6, reg_write_Z_r6, reg_write_X_r7, reg_write_Y_r7, reg_write_Z_r7, reg_write_X_r8, reg_write_Y_r8, reg_write_Z_r8, reg_write_X_r9, reg_write_Y_r9, reg_write_Z_r9, reg_write_X_r10, reg_write_Y_r10, reg_write_Z_r10, reg_write_X_r11, reg_write_Y_r11, reg_write_Z_r11, instr_store, instr_load, instr_add, instr_sub, instr_eq, instr_mul, instr_mov, instr_call, instr_call_param_l, instr_ret, instr_jump, instr_jump_param_l, instr_jumpi, instr_jumpi_param_l, instr_jumpni, instr_jumpni_param_l, instr__jump_to_operation, instr__reset, instr__loop, instr_return, X_const, X_read_free, read_X_addr, read_X_jump_ptr, read_X_r0, read_X_r1, read_X_r10, read_X_r11, read_X_r2, read_X_r3, read_X_r4, read_X_r5, read_X_r6, read_X_r7, read_X_r8, read_X_r9, read_X_tmp, read_X_pc, Y_const, Y_read_free, read_Y_addr, read_Y_jump_ptr, read_Y_r0, read_Y_r1, read_Y_r10, read_Y_r11, read_Y_r2, read_Y_r3, read_Y_r4, read_Y_r5, read_Y_r6, read_Y_r7, read_Y_r8, read_Y_r9, read_Y_tmp, read_Y_pc, Z_const, Z_read_free, read_Z_addr, read_Z_jump_ptr, read_Z_r0, read_Z_r1, read_Z_r10, read_Z_r11, read_Z_r2, read_Z_r3, read_Z_r4, read_Z_r5, read_Z_r6, read_Z_r7, read_Z_r8, read_Z_r9, read_Z_tmp, read_Z_pc } in { p_line, p_reg_write_X_jump_ptr, p_reg_write_Y_jump_ptr, p_reg_write_Z_jump_ptr, p_reg_write_X_addr, p_reg_write_Y_addr, p_reg_write_Z_addr, p_reg_write_X_tmp, p_reg_write_Y_tmp, p_reg_write_Z_tmp, p_reg_write_X_r0, p_reg_write_Y_r0, p_reg_write_Z_r0, p_reg_write_X_r1, p_reg_write_Y_r1, p_reg_write_Z_r1, p_reg_write_X_r2, p_reg_write_Y_r2, p_reg_write_Z_r2, p_reg_write_X_r3, p_reg_write_Y_r3, p_reg_write_Z_r3, p_reg_write_X_r4, p_reg_write_Y_r4, p_reg_write_Z_r4, p_reg_write_X_r5, p_reg_write_Y_r5, p_reg_write_Z_r5, p_reg_write_X_r6, p_reg_write_Y_r6, p_reg_write_Z_r6, p_reg_write_X_r7, p_reg_write_Y_r7, p_reg_write_Z_r7, p_reg_write_X_r8, p_reg_write_Y_r8, p_reg_write_Z_r8, p_reg_write_X_r9, p_reg_write_Y_r9, p_reg_write_Z_r9, p_reg_write_X_r10, p_reg_write_Y_r10, p_reg_write_Z_r10, p_reg_write_X_r11, p_reg_write_Y_r11, p_reg_write_Z_r11, p_instr_store, p_instr_load, p_instr_add, p_instr_sub, p_instr_eq, p_instr_mul, p_instr_mov, p_instr_call, p_instr_call_param_l, p_instr_ret, p_instr_jump, p_instr_jump_param_l, p_instr_jumpi, p_instr_jumpi_param_l, p_instr_jumpni, p_instr_jumpni_param_l, p_instr__jump_to_operation, p_instr__reset, p_instr__loop, p_instr_return, p_X_const, p_X_read_free, p_read_X_addr, p_read_X_jump_ptr, p_read_X_r0, p_read_X_r1, p_read_X_r10, p_read_X_r11, p_read_X_r2, p_read_X_r3, p_read_X_r4, p_read_X_r5, p_read_X_r6, p_read_X_r7, p_read_X_r8, p_read_X_r9, p_read_X_tmp, p_read_X_pc, p_Y_const, p_Y_read_free, p_read_Y_addr, p_read_Y_jump_ptr, p_read_Y_r0, p_read_Y_r1, p_read_Y_r10, p_read_Y_r11, p_read_Y_r2, p_read_Y_r3, p_read_Y_r4, p_read_Y_r5, p_read_Y_r6, p_read_Y_r7, p_read_Y_r8, p_read_Y_r9, p_read_Y_tmp, p_read_Y_pc, p_Z_const, p_Z_read_free, p_read_Z_addr, p_read_Z_jump_ptr, p_read_Z_r0, p_read_Z_r1, p_read_Z_r10, p_read_Z_r11, p_read_Z_r2, p_read_Z_r3, p_read_Z_r4, p_read_Z_r5, p_read_Z_r6, p_read_Z_r7, p_read_Z_r8, p_read_Z_r9, p_read_Z_tmp, p_read_Z_pc }; +pol constant _block_enforcer_last_step = [0]* + [1]; +pol commit _operation_id_no_change; +_operation_id_no_change = ((1 - _block_enforcer_last_step) * (1 - instr_return)); +(_operation_id_no_change * (_operation_id' - _operation_id)) = 0; +pol constant _linker_first_step = [1] + [0]*; +(_linker_first_step * (_operation_id - 2)) = 0; diff --git a/brillig_out_opt.pil b/brillig_out_opt.pil new file mode 100644 index 0000000000..f958a18614 --- /dev/null +++ b/brillig_out_opt.pil @@ -0,0 +1,116 @@ +namespace main(256); + col witness XInv; + col witness XIsZero; + main.XIsZero = (1 - (main.X * main.XInv)); + (main.XIsZero * main.X) = 0; + (main.XIsZero * (1 - main.XIsZero)) = 0; + col witness m_addr; + col witness m_step; + col witness m_change; + col witness m_value; + col witness m_op; + col witness m_is_write; + col witness m_is_read; + col fixed POSITIVE(i) { (i + 1) }; + col fixed FIRST = [1] + [0]*; + col fixed LAST(i) { main.FIRST((i + 1)) }; + col fixed STEP(i) { i }; + (main.m_change * (1 - main.m_change)) = 0; + ((main.m_addr' - main.m_addr) * (1 - main.m_change)) = 0; + (1 - main.LAST) { ((main.m_change * (main.m_addr' - main.m_addr)) + ((1 - main.m_change) * (main.m_step' - main.m_step))) } in { main.POSITIVE }; + (main.m_op * (1 - main.m_op)) = 0; + (main.m_is_write * (1 - main.m_is_write)) = 0; + (main.m_is_read * (1 - main.m_is_read)) = 0; + (main.m_is_write * (1 - main.m_op)) = 0; + (main.m_is_read * (1 - main.m_op)) = 0; + (main.m_is_read * main.m_is_write) = 0; + (((1 - main.m_is_write') * (1 - main.m_change)) * (main.m_value' - main.m_value)) = 0; + (((1 - main.m_is_write') * main.m_change) * main.m_value') = 0; + col witness _operation_id; + col witness _sigma; + col fixed _romgen_first_step = [1] + [0]*; + main._sigma' = ((1 - main._romgen_first_step') * (main._sigma + main.instr_return)); + (main._sigma * (main._operation_id - 8)) = 0; + col witness pc; + col witness X; + col witness Y; + col witness Z; + col witness jump_ptr; + col witness addr; + col witness tmp; + col witness reg_write_X_r0; + col witness r0; + col witness reg_write_X_r1; + col witness r1; + col witness r2; + col witness reg_write_X_r3; + col witness r3; + col witness r4; + col witness r5; + col witness r6; + col witness r7; + col witness r8; + col witness r9; + col witness r10; + col witness r11; + 0 { main.addr, main.STEP, main.X } is main.m_is_write { main.m_addr, main.m_step, main.m_value }; + 0 { main.addr, main.STEP, main.X } is main.m_is_read { main.m_addr, main.m_step, main.m_value }; + col witness instr_call; + col witness instr_call_param_l; + col witness instr_ret; + col instr_jumpi_pc_update = 0; + col instr_jumpi_pc_update_1 = (main.XIsZero * (main.pc + 1)); + col instr_jumpni_pc_update = 0; + col instr_jumpni_pc_update_1 = ((1 - main.XIsZero) * (main.pc + 1)); + col witness instr__jump_to_operation; + col witness instr__reset; + col witness instr__loop; + col witness instr_return; + col witness X_const; + main.X = main.X_const; + main.Y = 0; + main.Z = 0; + col fixed first_step = [1] + [0]*; + main.addr' = ((1 - main.instr__reset) * main.addr); + main.jump_ptr' = ((main.instr_call * (main.pc + 1)) + ((1 - (main.instr_call + main.instr__reset)) * main.jump_ptr)); + col pc_update = (((((main.instr_call * main.instr_call_param_l) + (main.instr_ret * main.jump_ptr)) + (main.instr__jump_to_operation * main._operation_id)) + (main.instr__loop * main.pc)) + ((1 - ((((main.instr_call + main.instr_ret) + main.instr__jump_to_operation) + main.instr__loop) + main.instr_return)) * (main.pc + 1))); + main.pc' = ((1 - main.first_step') * main.pc_update); + main.r0' = ((main.reg_write_X_r0 * main.X) + ((1 - (main.reg_write_X_r0 + main.instr__reset)) * main.r0)); + main.r1' = ((main.reg_write_X_r1 * main.X) + ((1 - (main.reg_write_X_r1 + main.instr__reset)) * main.r1)); + main.r10' = ((1 - main.instr__reset) * main.r10); + main.r11' = ((1 - main.instr__reset) * main.r11); + main.r2' = ((1 - main.instr__reset) * main.r2); + main.r3' = ((main.reg_write_X_r3 * main.X) + ((1 - (main.reg_write_X_r3 + main.instr__reset)) * main.r3)); + main.r4' = ((1 - main.instr__reset) * main.r4); + main.r5' = ((1 - main.instr__reset) * main.r5); + main.r6' = ((1 - main.instr__reset) * main.r6); + main.r7' = ((1 - main.instr__reset) * main.r7); + main.r8' = ((1 - main.instr__reset) * main.r8); + main.r9' = ((1 - main.instr__reset) * main.r9); + main.tmp' = ((1 - main.instr__reset) * main.tmp); + col fixed p_line = [0, 1, 2, 3, 4, 5, 6, 7, 8] + [8]*; + col witness X_free_value(i) query match main.pc { }; + col witness Y_free_value(i) query match main.pc { }; + col witness Z_free_value(i) query match main.pc { }; + col fixed p_X_const = [0, 0, 0, 0, 0, 0, 3, 0, 0] + [0]*; + col fixed p_instr__jump_to_operation = [0, 1, 0, 0, 0, 0, 0, 0, 0] + [0]*; + col fixed p_instr__loop = [0, 0, 0, 0, 0, 0, 0, 0, 1] + [1]*; + col fixed p_instr__reset = [1, 0, 0, 0, 0, 0, 0, 0, 0] + [0]*; + col fixed p_instr_call = [0, 0, 0, 0, 1, 0, 0, 0, 0] + [0]*; + col fixed p_instr_call_param_l = [0, 0, 0, 0, 6, 0, 0, 0, 0] + [0]*; + col fixed p_instr_ret = [0, 0, 0, 0, 0, 0, 0, 1, 0] + [0]*; + col fixed p_instr_return = [0, 0, 0, 0, 0, 1, 0, 0, 0] + [0]*; + col fixed p_reg_write_X_r0 = [0, 0, 1, 0, 0, 0, 0, 0, 0] + [0]*; + col fixed p_reg_write_X_r1 = [0, 0, 0, 1, 0, 0, 0, 0, 0] + [0]*; + col fixed p_reg_write_X_r3 = [0, 0, 0, 0, 0, 0, 1, 0, 0] + [0]*; + { main.pc, main.reg_write_X_r0, main.reg_write_X_r1, main.reg_write_X_r3, main.instr_call, main.instr_call_param_l, main.instr_ret, main.instr__jump_to_operation, main.instr__reset, main.instr__loop, main.instr_return, main.X_const } in { main.p_line, main.p_reg_write_X_r0, main.p_reg_write_X_r1, main.p_reg_write_X_r3, main.p_instr_call, main.p_instr_call_param_l, main.p_instr_ret, main.p_instr__jump_to_operation, main.p_instr__reset, main.p_instr__loop, main.p_instr_return, main.p_X_const }; + col fixed _block_enforcer_last_step = [0]* + [1]; + col witness _operation_id_no_change; + main._operation_id_no_change = ((1 - main._block_enforcer_last_step) * (1 - main.instr_return)); + (main._operation_id_no_change * (main._operation_id' - main._operation_id)) = 0; + col fixed _linker_first_step = [1] + [0]*; + (main._linker_first_step * (main._operation_id - 2)) = 0; + { main.pc, main.reg_write_X_r0, main.reg_write_X_r1, main.reg_write_X_r3, main.instr_call, main.instr_call_param_l, main.instr_ret, main.instr__jump_to_operation, main.instr__reset, main.instr__loop, main.instr_return, main.X_const } in { main.p_line, main.p_reg_write_X_r0, main.p_reg_write_X_r1, main.p_reg_write_X_r3, main.p_instr_call, main.p_instr_call_param_l, main.p_instr_ret, main.p_instr__jump_to_operation, main.p_instr__reset, main.p_instr__loop, main.p_instr_return, main.p_X_const }; + main._operation_id_no_change = ((1 - main._block_enforcer_last_step) * (1 - main.instr_return)); + (main._operation_id_no_change * (main._operation_id' - main._operation_id)) = 0; + (main._linker_first_step * (main._operation_id - 2)) = 0; diff --git a/commits.bin b/commits.bin new file mode 100644 index 0000000000000000000000000000000000000000..ebff482de6432da86a83f4398852f43dc6f59bd6 GIT binary patch literal 1024 zcmajdF%f_;5Jka+Oc 1, _ => 0, } }; + col witness x; + col witness y; + (Fibonacci.ISLAST * (Fibonacci.y' - 1)) = 0; + (Fibonacci.ISLAST * (Fibonacci.x' - 1)) = 0; + ((1 - Fibonacci.ISLAST) * (Fibonacci.x' - Fibonacci.y)) = 0; + ((1 - Fibonacci.ISLAST) * (Fibonacci.y' - (Fibonacci.x + Fibonacci.y))) = 0; + public out = Fibonacci.y(15); diff --git a/halo2/src/circuit_builder.rs b/halo2/src/circuit_builder.rs index b1c12c4ef8..9025283c4c 100644 --- a/halo2/src/circuit_builder.rs +++ b/halo2/src/circuit_builder.rs @@ -115,8 +115,11 @@ pub(crate) fn analyzed_to_circuit( }; let identities = inline_intermediate_polynomials(analyzed); + + // NTS(md): this is traversing all of the identities and building the polys. for id in &identities { match id.kind { + // for the case of normal poly everything is in the left IdentityKind::Polynomial => { // polynomial identities. diff --git a/hello.pil b/hello.pil new file mode 100644 index 0000000000..9b731f7393 --- /dev/null +++ b/hello.pil @@ -0,0 +1,69 @@ +namespace main(8); +pol commit _operation_id; +pol commit _sigma; +pol constant _romgen_first_step = [1] + [0]*; +_sigma' = ((1 - _romgen_first_step') * (_sigma + instr_return)); +(_sigma * (_operation_id - 7)) = 0; +pol commit pc; +pol commit X; +pol commit Y; +pol commit reg_write_X_A; +pol commit reg_write_Y_A; +pol commit A; +pol commit instr_incr; +(instr_incr * (Y - (X + 1))) = 0; +pol commit instr_decr; +(instr_decr * (Y - (X - 1))) = 0; +pol commit instr_assert_zero; +(instr_assert_zero * (X - 0)) = 0; +pol commit instr_mstore; +instr_mstore { addr, STEP, X } is m_is_write { m_addr, m_step, m_value }; +pol commit instr_mload; +instr_mload { addr, STEP, X } is m_is_read { m_addr, m_step, m_value }; +pol commit instr__jump_to_operation; +pol commit instr__reset; +pol commit instr__loop; +pol commit instr_return; +pol commit X_const; +pol commit X_read_free; +pol commit read_X_A; +pol commit read_X_pc; +X = ((((read_X_A * A) + (read_X_pc * pc)) + X_const) + (X_read_free * X_free_value)); +pol commit Y_const; +pol commit Y_read_free; +pol commit read_Y_A; +pol commit read_Y_pc; +Y = ((((read_Y_A * A) + (read_Y_pc * pc)) + Y_const) + (Y_read_free * Y_free_value)); +pol constant first_step = [1] + [0]*; +A' = ((((reg_write_X_A * X) + (reg_write_Y_A * Y)) + (instr__reset * 0)) + ((1 - ((reg_write_X_A + reg_write_Y_A) + instr__reset)) * A)); +pol pc_update = ((((instr__jump_to_operation * _operation_id) + (instr__loop * pc)) + (instr_return * 0)) + ((1 - ((instr__jump_to_operation + instr__loop) + instr_return)) * (pc + 1))); +pc' = ((1 - first_step') * pc_update); +pol constant p_line = [0, 1, 2, 3, 4, 5, 6, 7] + [7]*; +pol commit X_free_value(i) query match pc { 2 => ("input", 0), }; +pol commit Y_free_value(i) query match pc { }; +pol constant p_X_const = [0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_X_read_free = [0, 0, 1, 0, 0, 0, 0, 0] + [0]*; +pol constant p_Y_const = [0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_Y_read_free = [0, 0, 0, 1, 1, 0, 0, 0] + [0]*; +pol constant p_instr__jump_to_operation = [0, 1, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_instr__loop = [0, 0, 0, 0, 0, 0, 0, 1] + [1]*; +pol constant p_instr__reset = [1, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_instr_assert_zero = [0, 0, 0, 0, 0, 1, 0, 0] + [0]*; +pol constant p_instr_decr = [0, 0, 0, 0, 1, 0, 0, 0] + [0]*; +pol constant p_instr_incr = [0, 0, 0, 1, 0, 0, 0, 0] + [0]*; +pol constant p_instr_mload = [0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_instr_mstore = [0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_instr_return = [0, 0, 0, 0, 0, 0, 1, 0] + [0]*; +pol constant p_read_X_A = [0, 0, 0, 1, 1, 1, 0, 0] + [0]*; +pol constant p_read_X_pc = [0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Y_A = [0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_read_Y_pc = [0, 0, 0, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_X_A = [0, 0, 1, 0, 0, 0, 0, 0] + [0]*; +pol constant p_reg_write_Y_A = [0, 0, 0, 1, 1, 0, 0, 0] + [0]*; +{ pc, reg_write_X_A, reg_write_Y_A, instr_incr, instr_decr, instr_assert_zero, instr_mstore, instr_mload, instr__jump_to_operation, instr__reset, instr__loop, instr_return, X_const, X_read_free, read_X_A, read_X_pc, Y_const, Y_read_free, read_Y_A, read_Y_pc } in { p_line, p_reg_write_X_A, p_reg_write_Y_A, p_instr_incr, p_instr_decr, p_instr_assert_zero, p_instr_mstore, p_instr_mload, p_instr__jump_to_operation, p_instr__reset, p_instr__loop, p_instr_return, p_X_const, p_X_read_free, p_read_X_A, p_read_X_pc, p_Y_const, p_Y_read_free, p_read_Y_A, p_read_Y_pc }; +pol constant _block_enforcer_last_step = [0]* + [1]; +pol commit _operation_id_no_change; +_operation_id_no_change = ((1 - _block_enforcer_last_step) * (1 - instr_return)); +(_operation_id_no_change * (_operation_id' - _operation_id)) = 0; +pol constant _linker_first_step = [1] + [0]*; +(_linker_first_step * (_operation_id - 2)) = 0; diff --git a/hello_opt.pil b/hello_opt.pil new file mode 100644 index 0000000000..8eeacd9f39 --- /dev/null +++ b/hello_opt.pil @@ -0,0 +1,54 @@ +namespace main(8); + col witness _operation_id; + col witness _sigma; + col fixed _romgen_first_step = [1] + [0]*; + main._sigma' = ((1 - main._romgen_first_step') * (main._sigma + main.instr_return)); + (main._sigma * (main._operation_id - 7)) = 0; + col witness pc; + col witness X; + col witness Y; + col witness reg_write_X_A; + col witness reg_write_Y_A; + col witness A; + col witness instr_incr; + (main.instr_incr * (main.Y - (main.X + 1))) = 0; + col witness instr_decr; + (main.instr_decr * (main.Y - (main.X - 1))) = 0; + col witness instr_assert_zero; + (main.instr_assert_zero * main.X) = 0; + col witness instr__jump_to_operation; + col witness instr__reset; + col witness instr__loop; + col witness instr_return; + col witness X_read_free; + col witness read_X_A; + main.X = ((main.read_X_A * main.A) + (main.X_read_free * main.X_free_value)); + col witness Y_read_free; + main.Y = (main.Y_read_free * main.Y_free_value); + col fixed first_step = [1] + [0]*; + main.A' = (((main.reg_write_X_A * main.X) + (main.reg_write_Y_A * main.Y)) + ((1 - ((main.reg_write_X_A + main.reg_write_Y_A) + main.instr__reset)) * main.A)); + col pc_update = (((main.instr__jump_to_operation * main._operation_id) + (main.instr__loop * main.pc)) + ((1 - ((main.instr__jump_to_operation + main.instr__loop) + main.instr_return)) * (main.pc + 1))); + main.pc' = ((1 - main.first_step') * main.pc_update); + col fixed p_line = [0, 1, 2, 3, 4, 5, 6, 7]; + col witness X_free_value(i) query match main.pc { 2 => ("input", 0), }; + col witness Y_free_value(i) query match main.pc { }; + col fixed p_X_read_free = [0, 0, 1, 0, 0, 0, 0, 0]; + col fixed p_Y_read_free = [0, 0, 0, 1, 1, 0, 0, 0]; + col fixed p_instr__jump_to_operation = [0, 1, 0, 0, 0, 0, 0, 0]; + col fixed p_instr__loop = [0, 0, 0, 0, 0, 0, 0, 1]; + col fixed p_instr__reset = [1, 0, 0, 0, 0, 0, 0, 0]; + col fixed p_instr_assert_zero = [0, 0, 0, 0, 0, 1, 0, 0]; + col fixed p_instr_decr = [0, 0, 0, 0, 1, 0, 0, 0]; + col fixed p_instr_incr = [0, 0, 0, 1, 0, 0, 0, 0]; + col fixed p_instr_return = [0, 0, 0, 0, 0, 0, 1, 0]; + col fixed p_read_X_A = [0, 0, 0, 1, 1, 1, 0, 0]; + col fixed p_reg_write_X_A = [0, 0, 1, 0, 0, 0, 0, 0]; + col fixed p_reg_write_Y_A = [0, 0, 0, 1, 1, 0, 0, 0]; + { main.pc, main.reg_write_X_A, main.reg_write_Y_A, main.instr_incr, main.instr_decr, main.instr_assert_zero, main.instr__jump_to_operation, main.instr__reset, main.instr__loop, main.instr_return, main.X_read_free, main.read_X_A, main.Y_read_free } in { main.p_line, main.p_reg_write_X_A, main.p_reg_write_Y_A, main.p_instr_incr, main.p_instr_decr, main.p_instr_assert_zero, main.p_instr__jump_to_operation, main.p_instr__reset, main.p_instr__loop, main.p_instr_return, main.p_X_read_free, main.p_read_X_A, main.p_Y_read_free }; + col fixed _block_enforcer_last_step = [0]* + [1]; + col witness _operation_id_no_change; + main._operation_id_no_change = ((1 - main._block_enforcer_last_step) * (1 - main.instr_return)); + (main._operation_id_no_change * (main._operation_id' - main._operation_id)) = 0; + col fixed _linker_first_step = [1] + [0]*; + (main._linker_first_step * (main._operation_id - 2)) = 0; + (main._linker_first_step * (main._operation_id - 2)) = 0; diff --git a/number/src/serialize.rs b/number/src/serialize.rs index ab5344cc78..1f3bf65739 100644 --- a/number/src/serialize.rs +++ b/number/src/serialize.rs @@ -13,6 +13,8 @@ pub fn write_polys_file( ) { let width = ceil_div(T::BITS as usize, 64) * 8; + // TODO: maybe i need to prefix this at the beginning + for i in 0..degree as usize { for (_name, constant) in polys { let bytes = constant[i].to_bytes_le(); diff --git a/proof.bin b/proof.bin new file mode 100644 index 0000000000000000000000000000000000000000..0736dde6f28c1101d22391f5d7cd0de300822470 GIT binary patch literal 5248 zcmai%Ra+Ab13)QZ^cX#Ibf?nY-Ha9xknR?wyOETZlI}*jL3(t^=niSA@B0Vu^?AN{yMZO}7^X5|R7FKnuc1=a6agf|b1}s7PqUpd-P8(V^ zLpn2NUPs+U6_Bt+DQ!tx&$EPaGl3(8n^lgSvZ3c@E|)AYu3W|tQdZ^)afx3(uH_JN zSgX*#uJxYoFAxU71|xV#e+3|2SE`g^>YB6e3hG3l%XHjh$PgX4et?+C39secE>Xst!`R0H~Cw%4HmFh+6G7W7mCX1q>qRm#wNfecmYcov-#H!#|XWiV+l03Dbv_{G}j#He*ss`l(^@RHZLI zn8gYOV=sRH5q2mvf4-hlE#YNl04E8x!qQf(cNojRVoo;#`RkI`S8rdngLfu^M9e67 z96F?TSw0+Wg6KnR_!Yyc-t4MHvop?IF6U4l z&5+g}Cn7g(l~jVyI*~%4$ zKD#ScYqAEdAz5}jF081@Y7}*T9^3!s`Z=_z_p2h?!xlZ4Vy(g9B4xX!yWqreF4K1yd`b$6i{DK}CPyW8E zNOZcW{Zk47A4<#D=4ts+PiynxUV^L3Ml4Soyns=@57<7P1QOvk(w#a~ZNII*Oq$FR zkt*;RkE?h~x&F9l9-UFPP~hCrU(7JSu61uu)Qcw?Rm;Y4$+QY=iFJWoUBOPTEN^lP zD^9ppaIZU{2@{F2jW(MU03K!7x?VKU{&t|0QwsW;?f7J2HRi|{!=_|uchOD#hu3-_cnwvHIe{!iXQ zd|lIp_AV~R79Ve|%V<2`yohd+VmSC>2F^EYu5}Zy%wvqm(@kG4e$iKK6F7&gA;4}q zJ%hi6VZW)}{NkUX=NmU>&nGGS=^*pzN|W!Ke=Eh{6D+zy2``$J(Bh1o3vv@(XO(}F z=SZ!fc5`Mn#h?1f4)Ci0H~Qt!O4C*V={* z{=nS;$AlDB?i-g}3TVxtr^p0G0!f2CBl%zuDg!3`& z-55_al+FugPku%XP1( zh5AM^-+o9N>H3l?pe~+;7ekRqlkYANq|VI;=L0%YD8y7uUZldV9PzZ1LTo>B@GF*B zswZ3Rt32#<+l;ZoIk;$ZZ??1#m4nV+q1DL|-{6K0m~JcI0<1-zhQ*36a2x(cwECAM znxLH<1qF1d@sU2_TnDdsYBGvG4DNo$B3AFY=}UPZsUgs%m=5?7qxI)VO2n@TTGGxE zgLQ`jC?_!`{J1`MiIFA1C6TO6O-MWAhCs41kWu<3;nBEv)-pH z9+*H+jO)(s>SkHaNk;djYZf_cm_crWn{jFX2H~x>2|>*JS<73KHz>cCS(pt+VZW=$ zscDwUelw7CKs|LIVY;S3f67&kpbskI2vO&mus6(niSS1?3wN+C#O)fbHNnYPVB>^i zxZ4x4+;<90BQ(sQoEaQzC&as=Vi=CfDpVAW>A#p>9qt26E0u#@joF~~tqS+N9dXQ| zB=Z$bXJ5wwdZRuV-{2nU|G+qF>E@#;IUYz7{%-+t1Wt>OZ}Blw2ZRRlT;9y10Zv$v zT3f2R&vv4_s(6{%*pr*1C5nyxs0*$52q)g*A6RAb7cU=Ps2x}Vx5t)H`gVIUO#KZrO&bYK zAC(Oj5M}%I>n1@1i%Googvvkd`I8|tiT}tK7TqA z)n8P{&AerKqaix{=c_dX_9)2nprtF4QnG5R_^rBgTnp1iDI?#uBkLmIIxYAdv*KZ4 zN>6TVl>P1dAO>O+q+Ak$V)0YBHVej(U?HlBS#1V+0pIJE}7Lcmtz21n4G%obw^^QgS0(o7Zbqpi3NW_^=vFET^MnT%nU{SpTgUwBwq)iWOsZcNmMZ;ZAV^ za}Y6W?vN7=rR9w3UeU;A!iG16Z^CQ`p)VY9w?-NkqKA6Fy*K6v8IPnYEr55$gMM@% zOYGCHxm^l~ zQK_$A+%x`S?Q{e3E?eX|Cx6R#7OdWm-Q~VkscaZEfa4Rzo!Q2p4p4rEFV*_MZ(!wW zV}tE?yMo6-vfT+tcOuRy;RmuUYH;|hTd0h)U68{u{cf`PKb#I9x@K_}t?-Y&ziqr! zpGsAI7aPGi_osAB?LJ=1i4WdmqTHuM!84AA`|OV`R@A`*mT|S2+(6Ycd_?4w&D+hK zQiQ)aXf?(j%VRA&;-+q;wRpYq_^2(Xx&Hm|IqyqOGdJo?I&8MCpARMX3JVM|yV=gak9cyO$q=MYpQZ9<|<1_||<;b@?8Kvt9 zy9LR_pwulCYq@=827+}e@*dK@np;q%&4@J))LdV-`b7Q7C8CPs9}^xZfBN9gs`z2z zO+8og^?Bs~e_@tRLlCC2by3gqbmmZ4v1Dg9WW>*qcu|P?w(ZV+7Mh-Pr{?%~DN2hX z!ui#vLL{oJ&`tfS*TCN->d-wdG+cIVApdpSF-MK!8|C0J%_B!vqnllAS?+ayZ?7JK ztvImNgQ7DQU8I__S=2@LEFcREh|MFKjgr+-$L(S^+}UweuCIk$IekPJIC^V$$tz6) z>TpB~fguros+|vE5sr6AF||ozaTjdxAr(4Nu@&qk@2B``ukSZYM{OzX@#*^wEIIp!3 zGI_eC(7)vEG|X)s=X~}GSD6>j(OpQ4KD8~Nm3@Mjqx|UDWxHPi=gY1I=`dNLkSa4P z7C3l;+T7Vgoa&@gkQrsa!L8T~u~tP8NXao5PlNnxpFu^)He!NrmCQ!|^vx(P#H~K*7XF~OuHz%g? zbBFTd0$WN2aUmBsPj=GvgFB^)MkVDvq5REmz=*)Uaby&oy{K~hKzQnXY*SdjtpWu) z(_!f6^Gdi(xJFN?lb6yUVROA>Z$!|368jC$;xM>{A3p{feZrOPW;svLU1~cWywudU zRzC{H?|nQoEyU9}<~y&^h^{lj4N4!hm4B0&F$EX9JTgFF&-N=vzc52u|B#5Y#icS& zp{%{2UKl?so;B`$uD19NX4!~lWXI-CXrh-B&G%!mp?6g1X7)kr5r zuL-D+aV;Dk%T8E{u=>#%!+c{P@{F#TM0-NRE=Tlcj zqoY-nupNVw^#zo}*3W8?mN?FtF;Fzaks<(4Hyd&jhcBx>fQIy`#f*41SlP+k5)*ey z>I+Pi(@t#QbFzTu2+9CKKYAy-1M4Jw=32Qf?tSubX_y)K-G6Z|@lA4-a2z;=#C~p& z!(I6c;Y#!qAgGnoWEAQhzZc_#soRZ-tI^yM1~4*duI(H*(H_2( zkFhdb=Jq&;ugk&7#jfNrrFF2@^Vl#*6j}srMrJ1*Msb;qDsYgr5og92d1c*Pv+?*l zPQw$bv!=BS6lsX*jHOo@>%hs&QxR9J8vDhl*ctvg^3V>8VlETK##*7(?vZ3d2!A(m(9DRLk$GRo_61F=n27>~!3E(gu zBJDe?2Zv=0dN6s9|A3@oC-KiKLdD2?jiFD3|J650W$a51(qH6>Lu=28Z`nRI3NC&o z;%c(poC~lrSPS83HjUR(Ny{hjD?vyyUxPO#2LkH;=Y;o%(|O#EQ(dU%4d=XXEA_dm zgnO6R)!0WFg73TL|DaBDa?i$MYT9uiTkD{B$ajl+e?i~3r_cMcj4&k2pk}pl*3QHN z7d!%J+f(f~-4FRyBk;J*=IvCh&#_)qInBqw*6nw+IY)sm0^Hn1A7vkN*@YcODt;i_ zm9Onf7!@k1LCVbTFc{EVi*VB`Wyjj;XcjGP1~61k&bGgHpXjfRMFREld*Lh`{hm7W z>+w4%DB-5YnR}nx`~_dWKAn?~UoJoEN;lG{5#JNM|LGwnhnrPD;%xjk=-hdec3|OXQuO=nA@GMm82POOhAV`kri@U`Rc(gNt;fLca8! z^6Mb__^SBc4~3W9`7~d3oa?7;nOzB@X{IZqJX;~LZa_{+&CcJtWL29;o>gXrRYLTskWQ=)I(LieXwR=+YY06$sA#pk;qTk@W+xE6O zQ~%|YVwwq))HR~_{Ms;32}kN(a-Ru+HjP;F9i3jzxDi)-Mpk6u=wrl1KS#9A!Hnp} Lj9xx$$(8+ojAInp literal 0 HcmV?d00001 From 188596e446de75b2d9e08dd6361ed996fa645338 Mon Sep 17 00:00:00 2001 From: Maddiaa0 <47148561+Maddiaa0@users.noreply.github.com> Date: Fri, 13 Oct 2023 16:23:13 +0000 Subject: [PATCH 05/75] codegen --- ExampleRelation.hpp | 98 +++++++++ ExampleRelation_arith.hpp | 8 + ExampleRelation_flavor.hpp | 260 ++++++++++++++++++++++++ ExampleRelation_trace.hpp | 67 +++++++ bberg/src/bberg_codegen.rs | 5 +- bberg/src/circuit_builder.rs | 293 ++++++++++++++++++++++++--- bberg/src/flavor_builder.rs | 378 +++++++++++++++++++++++++++++++++++ bberg/src/lib.rs | 2 + bberg/src/trace_builder.rs | 106 ++++++++++ example.hpp | 90 +++++++++ node_modules/.yarn-integrity | 10 + yarn.lock | 4 + 12 files changed, 1297 insertions(+), 24 deletions(-) create mode 100644 ExampleRelation.hpp create mode 100644 ExampleRelation_arith.hpp create mode 100644 ExampleRelation_flavor.hpp create mode 100644 ExampleRelation_trace.hpp create mode 100644 bberg/src/flavor_builder.rs create mode 100644 bberg/src/trace_builder.rs create mode 100644 example.hpp create mode 100644 node_modules/.yarn-integrity create mode 100644 yarn.lock diff --git a/ExampleRelation.hpp b/ExampleRelation.hpp new file mode 100644 index 0000000000..973c221af3 --- /dev/null +++ b/ExampleRelation.hpp @@ -0,0 +1,98 @@ + +#pragma once +#include "../relation_parameters.hpp" +#include "../relation_types.hpp" + +namespace proof_system::ExampleRelation_vm { + +template struct Row { + FF Fibonacci_ISLAST; + FF Fibonacci_x; + FF Fibonacci_y; + FF Fibonacci_x_shift; + FF Fibonacci_y_shift; + }; + +template class ExampleRelationImpl { + public: + + static constexpr size_t RELATION_LENGTH = 3; + static constexpr size_t DEGREE_0 = 3; + static constexpr size_t DEGREE_1 = 3; + static constexpr size_t DEGREE_2 = 3; + static constexpr size_t DEGREE_3 = 3; +template