Merge pull request tonk-labs#24 from matthieuauger/dex

feat: Add DEX implementation code

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,82 @@ 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;
+    } else {
+        status.Z = 0;
     }
+
     if (number as u8 > 127) {
-        status.N = 1;
+        status.N = 128;
         // bits = bits & 128;
+    } else {
+        status.N = 0;
     }
     // bits
     status
 }
 
+#[test]
+fn test_compute_sn_empty_status() {
+    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);
+}
+
+#[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)
 }
@@ -79,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],

circuits/instr/dex/Nargo.toml

@@ -5,4 +5,5 @@ authors = [""]
 compiler_version = ">=0.10.5"
 
 [dependencies]
+constants = { path = "../../constants" }
 helpers = { path = "../../helpers" }

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
     )
-}
+}
+
+#[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]
+    )
+}