From 7ebcbd9bf5cf62b0de42ac0c1c1c9121eaf04888 Mon Sep 17 00:00:00 2001 From: Matthieu Auger Date: Fri, 22 Mar 2024 23:34:43 +0100 Subject: [PATCH 1/3] add tests and fix compute_zn_status() --- circuits/helpers/src/lib.nr | 57 +++++++++++++++++++++++++++++++++++-- 1 file changed, 55 insertions(+), 2 deletions(-) diff --git a/circuits/helpers/src/lib.nr b/circuits/helpers/src/lib.nr index 062487d..8e26f2e 100644 --- a/circuits/helpers/src/lib.nr +++ b/circuits/helpers/src/lib.nr @@ -27,6 +27,21 @@ unconstrained pub fn convert_to_status(n: Field) -> Status { status } +#[test] +fn test_convert_to_status() { + let sr = 0x26; // 0 0 1 0 0 1 1 0 -> 0 1 1 0 0 1 0 0 reversed + + let status = convert_to_status(sr); + assert(status.C == 0); + assert(status.Z == 2); + assert(status.I == 4); + assert(status.D == 0); + assert(status.B == 0); + assert(status.U == 32); + assert(status.V == 0); + assert(status.N == 0); +} + unconstrained pub fn status_to_num(status: Status) -> Field { let mut number = 0 as u32; number = number | status.C & 1; @@ -40,20 +55,58 @@ unconstrained pub fn status_to_num(status: Status) -> Field { number as Field } +#[test] +fn test_status_to_num() { + let status = Status { + C: 0, + Z: 2, + I: 4, + D: 0, + B: 0, + U: 32, + V: 0, + N: 128 + }; + let num = status_to_num(status); + + assert(num == 0xa6); // 1 0 1 0 0 1 1 0 -> 0 1 1 0 0 1 0 1 reversed +} + pub fn compute_zn_status(number: Field, mut status: Status) -> Status { // let mut bits = 0 as u8; if (number == 0) { - status.Z = 1; + status.Z = 2; // bits = bits & 2; } if (number as u8 > 127) { - status.N = 1; + status.N = 128; // bits = bits & 128; } // bits status } +#[test] +fn test_compute_sn_status_0() { + let status = Status { + C: 0, + Z: 0, + I: 0, + D: 0, + B: 0, + U: 0, + V: 0, + N: 0 + }; + + let computed_status = compute_zn_status(0, status); + assert(computed_status.Z == 2); + + let computed_status = compute_zn_status(200, status); + assert(computed_status.N == 128); +} + + pub fn wrapping_add_u16(a: Field, b: Field) -> Field { addressing::wrapping_add_u16(a, b) } From 671376f1bf8282fdc07127b746c0b59c2817708a Mon Sep 17 00:00:00 2001 From: Matthieu Auger Date: Fri, 22 Mar 2024 23:55:21 +0100 Subject: [PATCH 2/3] Z and N should be reversed if existing --- circuits/helpers/src/lib.nr | 26 +++++++++++++++++++++++++- 1 file changed, 25 insertions(+), 1 deletion(-) diff --git a/circuits/helpers/src/lib.nr b/circuits/helpers/src/lib.nr index 8e26f2e..f4d0387 100644 --- a/circuits/helpers/src/lib.nr +++ b/circuits/helpers/src/lib.nr @@ -77,17 +77,22 @@ pub fn compute_zn_status(number: Field, mut status: Status) -> Status { if (number == 0) { status.Z = 2; // bits = bits & 2; + } else { + status.Z = 0; } + if (number as u8 > 127) { status.N = 128; // bits = bits & 128; + } else { + status.N = 0; } // bits status } #[test] -fn test_compute_sn_status_0() { +fn test_compute_sn_empty_status() { let status = Status { C: 0, Z: 0, @@ -106,6 +111,25 @@ fn test_compute_sn_status_0() { assert(computed_status.N == 128); } +#[test] +fn test_compute_sn_non_empty_status() { + let status = Status { + C: 1, + Z: 2, + I: 4, + D: 8, + B: 16, + U: 32, + V: 64, + N: 128 + }; + + // should reverse Z + let computed_status = compute_zn_status(1, status); + assert(computed_status.Z == 0); + assert(computed_status.N == 0); +} + pub fn wrapping_add_u16(a: Field, b: Field) -> Field { addressing::wrapping_add_u16(a, b) From f09b79c59f1a1447647e2095e2de63d3f6892af1 Mon Sep 17 00:00:00 2001 From: Matthieu Auger Date: Fri, 22 Mar 2024 23:56:01 +0100 Subject: [PATCH 3/3] implement dex --- circuits/helpers/src/lib.nr | 17 ++++ circuits/instr/dex/Nargo.toml | 1 + circuits/instr/dex/src/main.nr | 148 ++++++++++++++++++++++++++------- 3 files changed, 134 insertions(+), 32 deletions(-) diff --git a/circuits/helpers/src/lib.nr b/circuits/helpers/src/lib.nr index f4d0387..11db345 100644 --- a/circuits/helpers/src/lib.nr +++ b/circuits/helpers/src/lib.nr @@ -156,6 +156,23 @@ pub fn wrapping_add_u8(a: Field, b: Field) -> WrapResult { } } +pub fn wrapping_dec_u8(a: Field, b: Field) -> WrapResult { + let result = a - b; + + if (result as i32 < 0) { + WrapResult { + value: 255, + wrapped: true, + } + } else { + WrapResult { + value: result, + wrapped: false, + } + } +} + + pub fn acc( op_sorted_addr: [Field; 1], op_sorted_val: [Field; 1], diff --git a/circuits/instr/dex/Nargo.toml b/circuits/instr/dex/Nargo.toml index d484aa9..3064bae 100644 --- a/circuits/instr/dex/Nargo.toml +++ b/circuits/instr/dex/Nargo.toml @@ -5,4 +5,5 @@ authors = [""] compiler_version = ">=0.10.5" [dependencies] +constants = { path = "../../constants" } helpers = { path = "../../helpers" } diff --git a/circuits/instr/dex/src/main.nr b/circuits/instr/dex/src/main.nr index 7d341a4..5aef51f 100644 --- a/circuits/instr/dex/src/main.nr +++ b/circuits/instr/dex/src/main.nr @@ -1,46 +1,130 @@ +use dep::constants::{PC_ADDR, A_ADDR, X_ADDR, Y_ADDR, SR_ADDR}; use dep::helpers; +use dep::std; -fn check_op( +pub fn OPCODE_VALUE() -> Field { + 202 +} + +fn main( r: Field, - op_sorted_step: [Field; 21], - op_sorted_addr: [Field; 21], - op_sorted_val: [Field; 21], - op_sorted_op_rw: [Field; 21] -) -> Field { - // TODO: implemented mode retrieval here for the opcode read - // we don't generalize this because each opcode will only have a few modes - // and we want to keep the total constraints down rather than needlessly - // checking for other opcodes every time - - let mode: Field = 0; //stubbed for now, we assume the mode is retreived in logic above - let mut sub_arr_step: [Field; 7] = [0,0,0,0,0,0,0]; - let mut sub_arr_addr: [Field; 7] = [0,0,0,0,0,0,0]; - let mut sub_arr_val: [Field; 7] = [0,0,0,0,0,0,0]; - let mut sub_arr_op_rw: [Field; 7] = [0,0,0,0,0,0,0]; - for i in 0..7 { - sub_arr_step[i] = op_sorted_step[i]; - sub_arr_addr[i] = op_sorted_addr[i]; - sub_arr_val[i] = op_sorted_val[i]; - sub_arr_op_rw[i] = op_sorted_op_rw[i]; + op_sorted_step: [Field; 9], + op_sorted_addr: [Field; 9], + op_sorted_val: [Field; 9], + op_sorted_op_rw: [Field; 9] +) -> pub Field { + assert(op_sorted_addr[0] == PC_ADDR()); + assert(op_sorted_op_rw[0] == 0); + let pc = op_sorted_val[0]; + + // this the address read value should be the opcode + assert(op_sorted_val[1] == OPCODE_VALUE()); + assert(op_sorted_op_rw[1] == 0); + + //next update the PC + assert(op_sorted_addr[2] == PC_ADDR()); + assert(op_sorted_op_rw[2] == 1); + assert(op_sorted_val[2] == pc + 1); + + let mut sub_arr_addr: [Field; 2] = [0, 0]; + let mut sub_arr_val: [Field; 2] = [0, 0]; + let mut sub_arr_op_rw: [Field; 2] = [0, 0]; + let offset = 3; + for i in 0..2 { + sub_arr_addr[i] = op_sorted_addr[offset + i]; + sub_arr_val[i] = op_sorted_val[offset + i]; + sub_arr_op_rw[i] = op_sorted_op_rw[offset + i]; } - let address_and_value: [Field; 2] = helpers::get_addressing( - mode, - sub_arr_step, - sub_arr_addr, - sub_arr_val, - sub_arr_op_rw - ); - // TODO: implement the rest of the op code checks here + helpers::imp(sub_arr_addr, sub_arr_val, sub_arr_op_rw); + + // we perform a read of x + assert(op_sorted_addr[5] == X_ADDR()); + assert(op_sorted_op_rw[5] == 0); + let value = op_sorted_val[5]; + + // we then perform a write of x - 1 + assert(op_sorted_addr[6] == X_ADDR()); + assert(op_sorted_op_rw[6] == 1); + + let wdec = helpers::wrapping_dec_u8(value, 1); + assert(op_sorted_val[6] == wdec.value); + + // we then set a new status into the status register + + // first there is a read from the status register + assert(op_sorted_addr[7] == SR_ADDR()); + assert(op_sorted_op_rw[7] == 0); + let sr = op_sorted_val[7]; - // TODO: handle case of padding + let mut status = helpers::convert_to_status(sr); + + // next there is a write to the status register + // we need to compute the zero and negative flag + status = helpers::compute_zn_status(wdec.value, status); + let comp_status = helpers::status_to_num(status); // 0x26 + + assert(op_sorted_addr[8] == SR_ADDR()); + assert(op_sorted_op_rw[8] == 1); + assert(op_sorted_val[8] == comp_status); // Compute permutation and return it - helpers::compute_permutation( + helpers::compute_permutation_9( r, op_sorted_step, op_sorted_addr, op_sorted_val, op_sorted_op_rw ) -} \ No newline at end of file +} + +#[test] +fn test_0() -> Field { + main( + 1, + [212536, 212537, 212538, 212539, 212540, 212541, 212542, 212543, 212544], + [PC_ADDR(), 55, PC_ADDR(), PC_ADDR(), 56, X_ADDR(), X_ADDR(), SR_ADDR(), SR_ADDR()], + [49207, OPCODE_VALUE(), 49208, 49208, 208, 0, 255, 38, 164], + [0, 0, 1, 0, 0, 0, 1, 0, 1] + ) +} +#[test] +fn test_1() -> Field { + main( + 1, + [212570, 212571, 212572, 212573, 212574, 212575, 212576, 212577, 212578], + [PC_ADDR(), 55, PC_ADDR(), PC_ADDR(), 56, X_ADDR(), X_ADDR(), SR_ADDR(), SR_ADDR()], + [49207, 202, 49208, 49208, 208, 255, 254, 164, 164], + [0, 0, 1, 0, 0, 0, 1, 0, 1] + ) +} +#[test] +fn test_2() -> Field { + main( + 1, + [212604, 212605, 212606, 212607, 212608, 212609, 212610, 212611, 212612], + [PC_ADDR(), 55, PC_ADDR(), PC_ADDR(), 56, X_ADDR(), X_ADDR(), SR_ADDR(), SR_ADDR()], + [49207, 202, 49208, 49208, 208, 254, 253, 164, 164], + [0, 0, 1, 0, 0, 0, 1, 0, 1] + ) +} +#[test] +fn test_3() -> Field { + main( + 1, + [212638, 212639, 212640, 212641, 212642, 212643, 212644, 212645, 212646], + [PC_ADDR(), 55, PC_ADDR(), PC_ADDR(), 56, X_ADDR(), X_ADDR(), SR_ADDR(), SR_ADDR()], + [49207, 202, 49208, 49208, 208, 253, 252, 164, 164], + [0, 0, 1, 0, 0, 0, 1, 0, 1] + ) +} +#[test] +fn test_4() -> Field { + main( + 1, + [212672, 212673, 212674, 212675, 212676, 212677, 212678, 212679, 212680], + [PC_ADDR(), 55, PC_ADDR(), PC_ADDR(), 56, X_ADDR(), X_ADDR(), SR_ADDR(), SR_ADDR()], + [49207, 202, 49208, 49208, 208, 252, 251, 164, 164], + [0, 0, 1, 0, 0, 0, 1, 0, 1] + ) +}