Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

LT ABS #181

Draft
wants to merge 4 commits into
base: develop
Choose a base branch
from
Draft

LT ABS #181

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
d401515
Table augmented
hecmas Dec 3, 2024
734bdf5
New opcodes introduced to binary
hecmas Dec 4, 2024
6a27a3f
Added the arith-binary lookup
hecmas Dec 4, 2024
af3e9d8
Added the debug mode to the verify all script
hecmas Dec 4, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
68 changes: 34 additions & 34 deletions core/src/zisk_ops.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -235,32 +235,32 @@ macro_rules! define_ops {
define_ops! {
(Flag, "flag", Internal, 0, 0x00, opc_flag, op_flag),
(CopyB, "copyb", Internal, 0, 0x01, opc_copyb, op_copyb),
(SignExtendB, "signextend_b", BinaryE, 109, 0x23, opc_signextend_b, op_signextend_b),
(SignExtendH, "signextend_h", BinaryE, 109, 0x24, opc_signextend_h, op_signextend_h),
(SignExtendW, "signextend_w", BinaryE, 109, 0x25, opc_signextend_w, op_signextend_w),
(Add, "add", Binary, 77, 0x02, opc_add, op_add),
(AddW, "add_w", Binary, 77, 0x12, opc_add_w, op_add_w),
(Sub, "sub", Binary, 77, 0x03, opc_sub, op_sub),
(SubW, "sub_w", Binary, 77, 0x13, opc_sub_w, op_sub_w),
(Sll, "sll", BinaryE, 109, 0x0d, opc_sll, op_sll),
(SllW, "sll_w", BinaryE, 109, 0x1d, opc_sll_w, op_sll_w),
(Sra, "sra", BinaryE, 109, 0x0f, opc_sra, op_sra),
(Srl, "srl", BinaryE, 109, 0x0e, opc_srl, op_srl),
(SraW, "sra_w", BinaryE, 109, 0x1f, opc_sra_w, op_sra_w),
(SrlW, "srl_w", BinaryE, 109, 0x1e, opc_srl_w, op_srl_w),
(Eq, "eq", Binary, 77, 0x08, opc_eq, op_eq),
(EqW, "eq_w", Binary, 77, 0x18, opc_eq_w, op_eq_w),
(Ltu, "ltu", Binary, 77, 0x04, opc_ltu, op_ltu),
(Lt, "lt", Binary, 77, 0x05, opc_lt, op_lt),
(LtuW, "ltu_w", Binary, 77, 0x14, opc_ltu_w, op_ltu_w),
(LtW, "lt_w", Binary, 77, 0x15, opc_lt_w, op_lt_w),
(Leu, "leu", Binary, 77, 0x06, opc_leu, op_leu),
(Le, "le", Binary, 77, 0x07, opc_le, op_le),
(LeuW, "leu_w", Binary, 77, 0x16, opc_leu_w, op_leu_w),
(LeW, "le_w", Binary, 77, 0x17, opc_le_w, op_le_w),
(And, "and", Binary, 77, 0x20, opc_and, op_and),
(Or, "or", Binary, 77, 0x21, opc_or, op_or),
(Xor, "xor", Binary, 77, 0x22, opc_xor, op_xor),
(SignExtendB, "signextend_b", BinaryE, 109, 0x37, opc_signextend_b, op_signextend_b),
(SignExtendH, "signextend_h", BinaryE, 109, 0x38, opc_signextend_h, op_signextend_h),
(SignExtendW, "signextend_w", BinaryE, 109, 0x39, opc_signextend_w, op_signextend_w),
(Add, "add", Binary, 77, 0x0b, opc_add, op_add),
(AddW, "add_w", Binary, 77, 0x2b, opc_add_w, op_add_w),
(Sub, "sub", Binary, 77, 0x0c, opc_sub, op_sub),
(SubW, "sub_w", Binary, 77, 0x2c, opc_sub_w, op_sub_w),
(Sll, "sll", BinaryE, 109, 0x31, opc_sll, op_sll),
(SllW, "sll_w", BinaryE, 109, 0x34, opc_sll_w, op_sll_w),
(Sra, "sra", BinaryE, 109, 0x33, opc_sra, op_sra),
(Srl, "srl", BinaryE, 109, 0x32, opc_srl, op_srl),
(SraW, "sra_w", BinaryE, 109, 0x36, opc_sra_w, op_sra_w),
(SrlW, "srl_w", BinaryE, 109, 0x35, opc_srl_w, op_srl_w),
(Eq, "eq", Binary, 77, 0x0a, opc_eq, op_eq),
(EqW, "eq_w", Binary, 77, 0x2a, opc_eq_w, op_eq_w),
(Ltu, "ltu", Binary, 77, 0x08, opc_ltu, op_ltu),
(Lt, "lt", Binary, 77, 0x09, opc_lt, op_lt),
(LtuW, "ltu_w", Binary, 77, 0x28, opc_ltu_w, op_ltu_w),
(LtW, "lt_w", Binary, 77, 0x29, opc_lt_w, op_lt_w),
(Leu, "leu", Binary, 77, 0x0d, opc_leu, op_leu),
(Le, "le", Binary, 77, 0x0e, opc_le, op_le),
(LeuW, "leu_w", Binary, 77, 0x2d, opc_leu_w, op_leu_w),
(LeW, "le_w", Binary, 77, 0x2e, opc_le_w, op_le_w),
(And, "and", Binary, 77, 0x0f, opc_and, op_and),
(Or, "or", Binary, 77, 0x10, opc_or, op_or),
(Xor, "xor", Binary, 77, 0x11, opc_xor, op_xor),
(Mulu, "mulu", ArithAm32, 97, 0xb0, opc_mulu, op_mulu),
(Muluh, "muluh", ArithAm32, 97, 0xb1, opc_muluh, op_muluh),
(Mulsuh, "mulsuh", ArithAm32, 97, 0xb3, opc_mulsuh, op_mulsuh),
Expand All @@ -275,14 +275,14 @@ define_ops! {
(RemuW, "remu_w", ArithA32, 136, 0xbd, opc_remu_w, op_remu_w),
(DivW, "div_w", ArithA32, 136, 0xbe, opc_div_w, op_div_w),
(RemW, "rem_w", ArithA32, 136, 0xbf, opc_rem_w, op_rem_w),
(Minu, "minu", Binary, 77, 0x09, opc_minu, op_minu),
(Min, "min", Binary, 77, 0x0a, opc_min, op_min),
(MinuW, "minu_w", Binary, 77, 0x19, opc_minu_w, op_minu_w),
(MinW, "min_w", Binary, 77, 0x1a, opc_min_w, op_min_w),
(Maxu, "maxu", Binary, 77, 0x0b, opc_maxu, op_maxu),
(Max, "max", Binary, 77, 0x0c, opc_max, op_max),
(MaxuW, "maxu_w", Binary, 77, 0x1b, opc_maxu_w, op_maxu_w),
(MaxW, "max_w", Binary, 77, 0x1c, opc_max_w, op_max_w),
(Minu, "minu", Binary, 77, 0x02, opc_minu, op_minu),
(Min, "min", Binary, 77, 0x03, opc_min, op_min),
(MinuW, "minu_w", Binary, 77, 0x22, opc_minu_w, op_minu_w),
(MinW, "min_w", Binary, 77, 0x23, opc_min_w, op_min_w),
(Maxu, "maxu", Binary, 77, 0x04, opc_maxu, op_maxu),
(Max, "max", Binary, 77, 0x05, opc_max, op_max),
(MaxuW, "maxu_w", Binary, 77, 0x24, opc_maxu_w, op_maxu_w),
(MaxW, "max_w", Binary, 77, 0x25, opc_max_w, op_max_w),
(Keccak, "keccak", Keccak, 77, 0xf1, opc_keccak, op_keccak),
(PubOut, "pubout", PubOut, 77, 0x30, opc_pubout, op_pubout), // TODO: New type
}
Expand Down
2 changes: 1 addition & 1 deletion pil/src/pil_helpers/pilout.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -44,7 +44,7 @@ impl Pilout {
air_group.add_air(Some("ArithTable"), 128);
air_group.add_air(Some("ArithRangeTable"), 4194304);
air_group.add_air(Some("Binary"), 2097152);
air_group.add_air(Some("BinaryTable"), 4194304);
air_group.add_air(Some("BinaryTable"), 8388608);
air_group.add_air(Some("BinaryExtension"), 2097152);
air_group.add_air(Some("BinaryExtensionTable"), 4194304);
air_group.add_air(Some("SpecifiedRanges"), 16777216);
Expand Down
15 changes: 8 additions & 7 deletions state-machines/arith/pil/arith.pil
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,6 @@ require "arith_range_table.pil"
// full mul_64 full_32 mul_32
// TOTAL 88 77 57 44

const int OP_LT_ABS = 0x9F;

airtemplate Arith(int N = 2**18, const int operation_bus_id, const int dual_result = 0) {

const int CHUNK_SIZE = 2**16;
Expand Down Expand Up @@ -275,11 +273,14 @@ airtemplate Arith(int N = 2**18, const int operation_bus_id, const int dual_resu
bus_res0, bus_res1,
div_by_zero /*+ div_overflow*/], mul: multiplicity);

// TODO: remainder check
// lookup_assumes(operation_bus_id, [debug_main_step, signed * (OP_LT_ABS - OP_LT) + OP_LT,
// (d[0] + CHUNK_SIZE * d[1]), (d[2] + CHUNK_SIZE * d[3]) + m32 * nr * 0xFFFFFFFF,
// (b[0] + CHUNK_SIZE * b[1]), (b[2] + CHUNK_SIZE * b[3]) + m32 * nb * 0xFFFFFFFF,
// 1, 0, 1], sel: div);
// Check that remainder (d) is lower than divisor (b) when division is performed
// Specifically, we ensure that 0 <= |d| < |b|
lookup_assumes(operation_bus_id, [debug_main_step,
nr * (1 - nb) * LT_ABS_NP_OP + (1 - nr) * nb * LT_ABS_PN_OP + (nr * nb + (1 - nr) * (1 - nb)) * LT_OP,
(d[0] + CHUNK_SIZE * d[1]), (d[2] + CHUNK_SIZE * d[3]) + m32 * nr * 0xFFFFFFFF, // remainder
(b[0] + CHUNK_SIZE * b[1]), (b[2] + CHUNK_SIZE * b[3]) + m32 * nb * 0xFFFFFFFF, // divisor
1, 0,
1], sel: div);

for (int index = 0; index < length(carry); ++index) {
arith_range_table_assumes(ARITH_RANGE_CARRY, carry[index]); // TODO: review carry range
Expand Down
92 changes: 40 additions & 52 deletions state-machines/binary/pil/binary.pil
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,61 +4,49 @@ require "std_lookup.pil"

/*
List 64-bit operations:
name │ op │ m_op │ carry │ use_last_carry │ NOTES
────────┼──────────┼──────────┼───────┼────────────────┼───────────────────────────────────
ADD │ 0x02 │ 0x02 │ X │ │
SUB │ 0x03 │ 0x03 │ X │ │
LTU │ 0x04 │ 0x04 │ X │ X │
LT │ 0x05 │ 0x05 │ X │ X │
LEU │ 0x06 │ 0x06 │ X │ X │
LE │ 0x07 │ 0x07 │ X │ X │
EQ │ 0x08 │ 0x08 │ X │ X │
MINU │ 0x09 │ 0x09 │ X │ │
MIN │ 0x0a │ 0x0a │ X │ │
MAXU │ 0x0b │ 0x0b │ X │ │
MAX │ 0x0c │ 0x0c │ X │ │
AND │ 0x20 │ 0x20 │ │ │
OR │ 0x21 │ 0x21 │ │ │
XOR │ 0x22 │ 0x22 │ │ │
────────┼──────────┼──────────┼───────┼────────────────┼───────────────────────────────────
name │ op │ m_op │ carry │ use_last_carry │ ZisK OP │ Notes │
───────────┼──────────┼──────────┼───────┼────────────────┼─────────┼────────────────────────────────────────────────────┼
MINU │ 0x02 │ 0x02 │ X │ │ X │ │
MIN │ 0x03 │ 0x03 │ X │ │ X │ │
MAXU │ 0x04 │ 0x04 │ X │ │ X │ │
MAX │ 0x05 │ 0x05 │ X │ │ X │ │
LT_ABS_NP │ 0x06 │ 0x06 │ X │ X │ │ This operation is used by the arithmetic component │
LT_ABS_PN │ 0x07 │ 0x07 │ X │ X │ │ This operation is used by the arithmetic component │
LTU │ 0x08 │ 0x08 │ X │ X │ X │ │
LT │ 0x09 │ 0x09 │ X │ X │ X │ │
EQ │ 0x0a │ 0x0a │ X │ X │ X │ │
ADD │ 0x0b │ 0x0b │ X │ │ X │ │
SUB │ 0x0c │ 0x0c │ X │ │ X │ │
LEU │ 0x0d │ 0x0d │ X │ X │ X │ │
LE │ 0x0e │ 0x0e │ X │ X │ X │ │
AND │ 0x0f │ 0x0f │ │ │ X │ │
OR │ 0x10 │ 0x10 │ │ │ X │ │
XOR │ 0x11 │ 0x11 │ │ │ X │ │
───────────┼──────────┼──────────┼───────┼────────────────┼─────────┼────────────────────────────────────────────────────┼

List 32-bit operations:
name │ op │ m_op │ carry │ use_last_carry │ NOTES
────────┼──────────┼──────────┼───────┼────────────────┼───────────────────────────────────
ADD_W │ 0x12 │ 0x02 │ X │ │
SUB_W │ 0x13 │ 0x03 │ X │ │
LTU_W │ 0x14 │ 0x04 │ X │ X │
LT_W │ 0x15 │ 0x05 │ X │ X │
LEU_W │ 0x16 │ 0x06 │ X │ X │
LE_W │ 0x17 │ 0x07 │ X │ X │
EQ_W │ 0x18 │ 0x08 │ X │ X │
MINU_W │ 0x19 │ 0x09 │ X │ │
MIN_W │ 0x1a │ 0x0a │ X │ │
MAXU_W │ 0x1b │ 0x0b │ X │ │
MAX_W │ 0x1c │ 0x0c │ X │ │
────────┼──────────┼──────────┼───────┼────────────────┼───────────────────────────────────

Opcodes:
---------------------------------------
expr op = m_op + 16*mode32

mode32 64bits 32bits m_op op
0/1 ADD ADD_W 0x02 (0x02,0x12)
0/1 SUB SUB_W 0x03 (0x03,0x13)
0/1 LTU LTU_W 0x04 (0x04,0x14)
0/1 LT LT_W 0x05 (0x05,0x15)
0/1 LEU LEU_W 0x06 (0x06,0x16)
0/1 LE LE_W 0x07 (0x07,0x17)
0/1 EQ EQ_W 0x08 (0x08,0x18)
0/1 MINU MINU_W 0x09 (0x09,0x19)
0/1 MIN MIN_W 0x0a (0x0a,0x1a)
0/1 MAXU MAXU_W 0x0b (0x0b,0x1b)
0/1 MAX MAX_W 0x0c (0x0c,0x1c)
0/1 AND 0x20 0x20
0 OR 0x21 0x21
0 XOR 0x22 0x22
name │ op │ m_op │ carry │ use_last_carry │ ZisK OP │
───────────┼──────────┼──────────┼───────┼────────────────┼─────────│
MINU_W │ 0x22 │ 0x02 │ X │ │ X │
MIN_W │ 0x23 │ 0x03 │ X │ │ X │
MAXU_W │ 0x24 │ 0x04 │ X │ │ X │
MAX_W │ 0x25 │ 0x05 │ X │ │ X │
LTU_W │ 0x28 │ 0x08 │ X │ X │ X │
LT_W │ 0x29 │ 0x09 │ X │ X │ X │
EQ_W │ 0x2a │ 0x0a │ X │ X │ X │
ADD_W │ 0x2b │ 0x0b │ X │ │ X │
SUB_W │ 0x2c │ 0x0c │ X │ │ X │
LEU_W │ 0x2d │ 0x0d │ X │ X │ X │
LE_W │ 0x2e │ 0x0e │ X │ X │ X │
───────────┼──────────┼──────────┼───────┼────────────────┼─────────│

Note: op = m_op + 0x20*mode32
*/

const int LT_ABS_NP_OP = 0x06;
const int LT_ABS_PN_OP = 0x07;
const int LT_OP = 0x09;

const int BINARY_ID = 20;

airtemplate Binary(const int N = 2**21, const int operation_bus_id = BINARY_ID) {
Expand Down Expand Up @@ -160,7 +148,7 @@ airtemplate Binary(const int N = 2**21, const int operation_bus_id = BINARY_ID)
c[0] += use_last_carry * cout;
c[input_chunks - 1] -= use_last_carry * cout * factor;

expr op = m_op + 16 * mode32;
expr op = m_op + 0x20 * mode32;

col witness multiplicity;
col witness main_step;
Expand Down
18 changes: 9 additions & 9 deletions state-machines/binary/pil/binary_extension.pil
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,15 +9,15 @@ List:
┼────────┼────────┼──────────┼
│ name │ bits │ op │
┼────────┼────────┼──────────┼
│ SLL │ 64 │ 0x0d │
│ SRL │ 64 │ 0x0e │
│ SRA │ 64 │ 0x0f │
│ SLL_W │ 32 │ 0x1d │
│ SRL_W │ 32 │ 0x1e │
│ SRA_W │ 32 │ 0x1f │
│ SE_B │ 32 │ 0x23 │
│ SE_H │ 32 │ 0x24 │
│ SE_W │ 32 │ 0x25 │
│ SLL │ 64 │ 0x31 │
│ SRL │ 64 │ 0x32 │
│ SRA │ 64 │ 0x33 │
│ SLL_W │ 32 │ 0x34 │
│ SRL_W │ 32 │ 0x35 │
│ SRA_W │ 32 │ 0x36 │
│ SE_B │ 32 │ 0x37 │
│ SE_H │ 32 │ 0x38 │
│ SE_W │ 32 │ 0x39 │
┼────────┼────────┼──────────┼

Examples:
Expand Down
Loading
Loading