Skip to content

Commit

Permalink
Verify all + riscof tests fixes (#165)
Browse files Browse the repository at this point in the history 
* verify_all.sh + riscof test fixes, mostly in binary SMs

---------

Co-authored-by: zkronos73 <[email protected]>
  • Loading branch information
@fractasy @zkronos73
fractasy and zkronos73 authored Nov 19, 2024
1 parent afe5934 commit 46efd80
Show file tree
Hide file tree
Showing 8 changed files with 168 additions and 59 deletions.
2 changes: 1 addition & 1 deletion core/src/zisk_inst.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ pub enum ZiskOperationType {
PubOut,
}

pub const ZISK_OPERATION_TYPE_VARIANTS: usize = 6;
pub const ZISK_OPERATION_TYPE_VARIANTS: usize = 7;

/// ZisK instruction definition
///
Expand Down
16 changes: 8 additions & 8 deletions core/src/zisk_ops.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -770,9 +770,9 @@ pub fn opc_min(ctx: &mut InstContext) {
#[inline(always)]
pub const fn op_minu_w(a: u64, b: u64) -> (u64, bool) {
if (a as u32) < (b as u32) {
(a, false)
(a as i32 as i64 as u64, false)
} else {
(b, false)
(b as i32 as i64 as u64, false)
}
}
#[inline(always)]
Expand All @@ -783,9 +783,9 @@ pub fn opc_minu_w(ctx: &mut InstContext) {
#[inline(always)]
pub const fn op_min_w(a: u64, b: u64) -> (u64, bool) {
if (a as i32) < (b as i32) {
(a, false)
(a as i32 as i64 as u64, false)
} else {
(b, false)
(b as i32 as i64 as u64, false)
}
}
#[inline(always)]
Expand Down Expand Up @@ -823,9 +823,9 @@ pub fn opc_max(ctx: &mut InstContext) {
#[inline(always)]
pub const fn op_maxu_w(a: u64, b: u64) -> (u64, bool) {
if (a as u32) > (b as u32) {
(a, false)
(a as i32 as i64 as u64, false)
} else {
(b, false)
(b as i32 as i64 as u64, false)
}
}
#[inline(always)]
Expand All @@ -836,9 +836,9 @@ pub fn opc_maxu_w(ctx: &mut InstContext) {
#[inline(always)]
pub const fn op_max_w(a: u64, b: u64) -> (u64, bool) {
if (a as i32) > (b as i32) {
(a, false)
(a as i32 as i64 as u64, false)
} else {
(b, false)
(b as i32 as i64 as u64, false)
}
}
#[inline(always)]
Expand Down
47 changes: 29 additions & 18 deletions state-machines/binary/pil/binary_table.pil
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,21 +2,21 @@ require "constants.pil";

// PIL Binary Operations Table used by Binary
// Running Total
// MINU/MINU_W (OP:0x09) * 2^16 (AxB) x 2^1 (LAST) x 2^1 (CIN) x 2^1 (RESULT_IS_A) = 2^19 | 2^19
// MIN/MIN_W (OP:0x0a) * 2^16 (AxB) x 2^1 (LAST) x 2^1 (CIN) x 2^1 (RESULT_IS_A) = 2^19 | 2^20
// MAXU/MAXU_W (OP:0x0b) * 2^16 (AxB) x 2^1 (LAST) x 2^1 (CIN) x 2^1 (RESULT_IS_A) = 2^19 | 2^20 + 2^19
// MINU/MINU_W (OP:0x09) * 2^16 (AxB) x 2^1 (LAST) x 2^1 (CIN) x 2^1 (RESULT_IS_A) = 2^19 | 2^19
// MIN/MIN_W (OP:0x0a) * 2^16 (AxB) x 2^1 (LAST) x 2^1 (CIN) x 2^1 (RESULT_IS_A) = 2^19 | 2^20
// MAXU/MAXU_W (OP:0x0b) * 2^16 (AxB) x 2^1 (LAST) x 2^1 (CIN) x 2^1 (RESULT_IS_A) = 2^19 | 2^20 + 2^19
// MAX/MAX_W (OP:0x0c) * 2^16 (AxB) x 2^1 (LAST) x 2^1 (CIN) x 2^1 (RESULT_IS_A) = 2^19 | 2^21
// LTU/LTU_W (OP:0x04) * 2^16 (AxB) x 2^1 (LAST) x 2^1 (CIN) = 2^18 | 2^21 + 2^18
// LT/LT_W (OP:0x05) * 2^16 (AxB) x 2^1 (LAST) x 2^1 (CIN) = 2^18 | 2^21 + 2^19
// LT/LT_W (OP:0x05) * 2^16 (AxB) x 2^1 (LAST) x 2^1 (CIN) = 2^18 | 2^21 + 2^19
// EQ/EQ_W (OP:0x08) * 2^16 (AxB) x 2^1 (LAST) x 2^1 (CIN) = 2^18 | 2^21 + 2^19 + 2^18
// ADD/ADD_W (OP:0x02) ** 2^16 (AxB) x 2^1 (LAST) x 2^1 (CIN) = 2^18 | 2^21 + 2^20
// SUB/SUB_W (OP:0x03) ** 2^16 (AxB) x 2^1 (LAST) x 2^1 (CIN) = 2^18 | 2^21 + 2^20 + 2^18
// LEU/LEU_W (OP:0x06) * 2^16 (AxB) x 2^1 (LAST) = 2^17 | 2^21 + 2^20 + 2^18 + 2^17
// LE/LE_W (OP:0x07) * 2^16 (AxB) x 2^1 (LAST) = 2^17 | 2^21 + 2^20 + 2^19
// LE/LE_W (OP:0x07) * 2^16 (AxB) x 2^1 (LAST) = 2^17 | 2^21 + 2^20 + 2^19
// AND/AND_W (OP:0x20) 2^16 (AxB) x 2^1 (LAST) = 2^17 | 2^21 + 2^20 + 2^19 + 2^17
// OR/OR_W (OP:0x21) 2^16 (AxB) x 2^1 (LAST) = 2^17 | 2^21 + 2^20 + 2^19 + 2^18
// XOR/XOR_W (OP:0x22) 2^16 (AxB) x 2^1 (LAST) = 2^17 | 2^21 + 2^20 + 2^19 + 2^18 + 2^17
// EXT_32 (OP:0x23) 2^16 (AxB) = 2^16 | 2^21 + 2^20 + 2^19 + 2^18 + 2^17 + 2^16 => 2^22
// EXT_32 (OP:0x23) 2^8 (A) x 2^1 (CIN) x 2^2 (FLAGS) = 2^16 | 2^21 + 2^20 + 2^19 + 2^18 + 2^17 + 2^11 => < 2^22
// --------------------------------------------------------------------------------------------------------------------------
// (*) Use carry
// (**) Do not use last indicator, but it is used for simplicity of the lookup
Expand Down Expand Up @@ -48,29 +48,30 @@ airtemplate BinaryTable(const int N = 2**22, const int disable_fixed = 0) {

col fixed A = [0..255]...; // Input A (8 bits)

col fixed B = [0:P2_8..255:P2_8]...; // Input B (8 bits)
col fixed B = [[0:P2_8..255:P2_8]:62,0:P2_11]...; // Input B (8 bits)

col fixed LAST = [[0:P2_16, 1:P2_16]:(4*4), // Indicator of the last byte (1 bit)
[0:P2_16, 1:P2_16]:(5*2),
[0:P2_16, 1:P2_16]:5,
0:P2_16]...;
0:P2_11]...;

col fixed CIN = [[0:P2_17, 1:P2_17]:(4*2), // Input carry (1 bit)
[0:P2_17, 1:P2_17]:5,
0:(P2_17*5),
0:P2_16]...;
[0:P2_8, 1:P2_8]:4]...;

col fixed OP = [0x09:P2_19, 0x0a:P2_19, 0x0b:P2_19, 0x0c:P2_19, // MINU,MIN,MAXU,MAX
0x04:P2_18, 0x05:P2_18, 0x08:P2_18, // LTU,LT,EQ
0x02:P2_18, 0x03:P2_18, // ADD,SUB
0x06:P2_17, 0x07:P2_17, // LEU,LE
0x20:P2_17, 0x21:P2_17, 0x22:P2_17, // AND,OR,XOR
0x23:P2_16]...; // EXT_32
0x23:P2_11]...; // EXT_32

// NOTE: MINU/MINU_W, MIN/MIN_W, MAXU/MAXU_W, MAX/MAX_W has double size because
// the result_is_a is 0 in the first half and 1 in the second half.

const int TABLE_SIZE = P2_19 * 4 + P2_18 * 5 + P2_17 * 5 + P2_16;
const int TABLE_SIZE = P2_19 * 4 + P2_18 * 5 + P2_17 * 6;
const int TABLE_BASE_EXT32 = P2_16 * 62;

#pragma timer t1 end
#pragma timer t2 start
Expand All @@ -91,7 +92,7 @@ airtemplate BinaryTable(const int N = 2**22, const int disable_fixed = 0) {
case 0x02: // ADD,ADD_W
c = (cin + a + b) & 0xFF;
cout = plast ? 0 : (cin + a + b) >> 8;

case 0x03: // SUB,SUB_W
sign = (a - cin) >= b ? 0 : 1;
c = 256 * sign + a - cin - b;
Expand Down Expand Up @@ -148,8 +149,10 @@ airtemplate BinaryTable(const int N = 2**22, const int disable_fixed = 0) {
c = b;
}

if (op == 0x0a && plast && (a & 0x80) != (b & 0x80)) {
cout = (a & 0x80) ? 1 : 0;
if (op == 0x0a && plast) {
if ((a & 0x80) != (b & 0x80)) {
cout = (a & 0x80) ? 1 : 0;
}
}

op_is_min_max = 1;
Expand All @@ -168,10 +171,11 @@ airtemplate BinaryTable(const int N = 2**22, const int disable_fixed = 0) {
c = b;
}

if (op == 0x0c && plast && (a & 0x80) != (b & 0x80)) {
cout = (a & 0x80) ? 0 : 1;
if (op == 0x0c && plast) {
if ((a & 0x80) != (b & 0x80)) {
cout = (a & 0x80) ? 0 : 1;
}
}

op_is_min_max = 1;

case 0x20: // AND
Expand All @@ -185,6 +189,13 @@ airtemplate BinaryTable(const int N = 2**22, const int disable_fixed = 0) {

case 0x23: // EXT_32
c = (a & 0x80) ? 0xFF : 0x00;
const int index_offset = (index - TABLE_BASE_EXT32) >> 9;
op_is_min_max = index_offset & 0x01;
if ((index_offset & 0x03) == 0x03) {
result_is_a = 1;
} else {
result_is_a = 0;
}

default:
error(`Invalid operation opcode: ${op} in row ${i}`);
Expand Down
84 changes: 67 additions & 17 deletions state-machines/binary/src/binary_basic.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -154,14 +154,14 @@ impl<F: Field> BinaryBasicSM<F> {
(c, flag) = ZiskOp::execute(operation.opcode, operation.a, operation.b);
let _flag = flag;

// Calculate result_is_a
let result_is_a: u64 = if operation.b == c { 0 } else { 1 };

// Set mode32
let opcode = ZiskOp::try_from_code(operation.opcode).expect("Invalid ZiskOp opcode");
let mode32 = Self::opcode_is_32_bits(opcode);
row.mode32 = F::from_bool(mode32);

// Set c_filtered
let c_filtered = if mode32 { c & 0xFFFFFFFF } else { c };

// Split a in bytes and store them in free_in_a
let a_bytes: [u8; 8] = operation.a.to_le_bytes();
for (i, value) in a_bytes.iter().enumerate() {
Expand Down Expand Up @@ -195,6 +195,9 @@ impl<F: Field> BinaryBasicSM<F> {
let op = ZiskOp::try_from_code(operation.opcode).unwrap();
match op {
ZiskOp::Add | ZiskOp::AddW => {
// Set opcode is min or max
row.op_is_min_max = F::zero();

// Set the binary basic table opcode
binary_basic_table_op = BinaryBasicTableOp::Add;

Expand Down Expand Up @@ -236,6 +239,9 @@ impl<F: Field> BinaryBasicSM<F> {
}
}
ZiskOp::Sub | ZiskOp::SubW => {
// Set opcode is min or max
row.op_is_min_max = F::zero();

// Set the binary basic table opcode
binary_basic_table_op = BinaryBasicTableOp::Sub;

Expand Down Expand Up @@ -276,6 +282,9 @@ impl<F: Field> BinaryBasicSM<F> {
}
}
ZiskOp::Ltu | ZiskOp::LtuW | ZiskOp::Lt | ZiskOp::LtW => {
// Set opcode is min or max
row.op_is_min_max = F::zero();

// Set the binary basic table opcode
binary_basic_table_op = if (op == ZiskOp::Ltu) || (op == ZiskOp::LtuW) {
BinaryBasicTableOp::Ltu
Expand Down Expand Up @@ -334,6 +343,9 @@ impl<F: Field> BinaryBasicSM<F> {
}
}
ZiskOp::Leu | ZiskOp::LeuW | ZiskOp::Le | ZiskOp::LeW => {
// Set opcode is min or max
row.op_is_min_max = F::zero();

// Set the binary basic table opcode
binary_basic_table_op = if (op == ZiskOp::Leu) || (op == ZiskOp::LeuW) {
BinaryBasicTableOp::Leu
Expand Down Expand Up @@ -383,6 +395,9 @@ impl<F: Field> BinaryBasicSM<F> {
}
}
ZiskOp::Eq | ZiskOp::EqW => {
// Set opcode is min or max
row.op_is_min_max = F::zero();

// Set the binary basic table opcode
binary_basic_table_op = BinaryBasicTableOp::Eq;

Expand Down Expand Up @@ -426,33 +441,46 @@ impl<F: Field> BinaryBasicSM<F> {
}
}
ZiskOp::Minu | ZiskOp::MinuW | ZiskOp::Min | ZiskOp::MinW => {
// Set opcode is min or max
row.op_is_min_max = F::one();

let result_is_a: u64 =
if (operation.a == operation.b) || (operation.b == c_filtered) { 0 } else { 1 };

// Set the binary basic table opcode
binary_basic_table_op = if (op == ZiskOp::Minu) || (op == ZiskOp::MinuW) {
BinaryBasicTableOp::Minu
} else {
BinaryBasicTableOp::Min
};

// Set use last carry to one
// Set use last carry to zero
row.use_last_carry = F::zero();

// Apply the logic to every byte
for i in 0..8 {
// Calculate carry
let previous_cin = cin;
cout = 0;
if a_bytes[i] <= b_bytes[i] {
cout = 1;
match a_bytes[i].cmp(&b_bytes[i]) {
CmpOrdering::Greater => {
cout = 0;
}
CmpOrdering::Less => {
cout = 1;
}
CmpOrdering::Equal => {
cout = cin;
}
}

// If the chunk is signed, then the result is the sign of a
if (binary_basic_table_op == BinaryBasicTableOp::Min) &&
(plast[i] == 1) &&
(a_bytes[i] & 0x80) != (b_bytes[i] & 0x80)
{
cout = if a_bytes[i] & 0x80 != 0 { 1 } else { 0 };
cout = if (a_bytes[i] & 0x80) != 0 { 1 } else { 0 };
}
if i == 7 {
if mode32 && (i >= 4) {
cout = 0;
}
cin = cout;
Expand All @@ -468,7 +496,7 @@ impl<F: Field> BinaryBasicSM<F> {
} else {
binary_basic_table_op
},
a_bytes[i] as u64,
if mode32 && (i >= 4) { c_bytes[3] as u64 } else { a_bytes[i] as u64 },
b_bytes[i] as u64,
previous_cin,
plast[i],
Expand All @@ -480,33 +508,46 @@ impl<F: Field> BinaryBasicSM<F> {
}
}
ZiskOp::Maxu | ZiskOp::MaxuW | ZiskOp::Max | ZiskOp::MaxW => {
// Set opcode is min or max
row.op_is_min_max = F::one();

let result_is_a: u64 =
if (operation.a == operation.b) || (operation.b == c_filtered) { 0 } else { 1 };

// Set the binary basic table opcode
binary_basic_table_op = if (op == ZiskOp::Maxu) || (op == ZiskOp::MaxuW) {
BinaryBasicTableOp::Maxu
} else {
BinaryBasicTableOp::Max
};

// Set use last carry to one
// Set use last carry to zero
row.use_last_carry = F::zero();

// Apply the logic to every byte
for i in 0..8 {
// Calculate carry
let previous_cin = cin;
cout = 0;
if a_bytes[i] >= b_bytes[i] {
cout = 1;
match a_bytes[i].cmp(&b_bytes[i]) {
CmpOrdering::Greater => {
cout = 1;
}
CmpOrdering::Less => {
cout = 0;
}
CmpOrdering::Equal => {
cout = cin;
}
}

// If the chunk is signed, then the result is the sign of a
if (binary_basic_table_op == BinaryBasicTableOp::Max) &&
(plast[i] == 1) &&
(a_bytes[i] & 0x80) != (b_bytes[i] & 0x80)
{
cout = if a_bytes[i] & 0x80 != 0 { 1 } else { 0 };
cout = if (a_bytes[i] & 0x80) != 0 { 0 } else { 1 };
}
if i == 7 {
if mode32 && (i >= 4) {
cout = 0;
}
cin = cout;
Expand All @@ -522,7 +563,7 @@ impl<F: Field> BinaryBasicSM<F> {
} else {
binary_basic_table_op
},
a_bytes[i] as u64,
if mode32 && (i >= 4) { c_bytes[3] as u64 } else { a_bytes[i] as u64 },
b_bytes[i] as u64,
previous_cin,
plast[i],
Expand All @@ -534,6 +575,9 @@ impl<F: Field> BinaryBasicSM<F> {
}
}
ZiskOp::And => {
// Set opcode is min or max
row.op_is_min_max = F::zero();

// Set the binary basic table opcode
binary_basic_table_op = BinaryBasicTableOp::And;

Expand Down Expand Up @@ -561,6 +605,9 @@ impl<F: Field> BinaryBasicSM<F> {
}
}
ZiskOp::Or => {
// Set opcode is min or max
row.op_is_min_max = F::zero();

// Set the binary basic table opcode
binary_basic_table_op = BinaryBasicTableOp::Or;

Expand Down Expand Up @@ -588,6 +635,9 @@ impl<F: Field> BinaryBasicSM<F> {
}
}
ZiskOp::Xor => {
// Set opcode is min or max
row.op_is_min_max = F::zero();

// Set the binary basic table opcode
binary_basic_table_op = BinaryBasicTableOp::Xor;

Expand Down
Loading

0 comments on commit 46efd80

Please sign in to comment.