Skip to content

Commit

Permalink
Merge pull request #74 from 0xPolygonHermez/feature/pil-binary-update
Browse files Browse the repository at this point in the history 
feature/pil binary update
  • Loading branch information
@zkronos73
zkronos73 authored Sep 5, 2024
2 parents c5ac96f + 651a134 commit cc5b925
Show file tree
Hide file tree
Showing 5 changed files with 165 additions and 131 deletions.
Binary file modified pil/fork_0/pil/zisk.pilout
View file
Binary file not shown.
124 changes: 73 additions & 51 deletions state-machines/binary/pil/binary.pil
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,39 +4,59 @@ require "std_lookup.pil"

/*
List 64-bit operations:
name │ opcode │ mOpcode │ carry │ use_last_carry │ NOTES
────────┼──────────┼──────────┼───────┼──────────────┼───────────────────────────────────
ADD │ 0x10 │ 0x00 │ X │ │
SUB │ 0x20 │ 0x01 │ X │ │
LTU │ 0x60 │ 0x02 │ X │ X │
LT │ 0x61 │ 0x03 │ X │ X │
LEU │ 0x70 │ 0x04 │ X │ X │
LE │ 0x71 │ 0x05 │ X │ X │
EQ │ 0x50 │ 0x06 │ X │ X │
MINU │ 0xd0 │ 0x07 │ X │ X │
MIN │ 0xd1 │ 0x08 │ X │ X │
MAXU │ 0xe0 │ 0x09 │ X │ X │
MAX │ 0xe1 │ 0x10 │ X │ X │
AND │ 0x80 │ 0x11 │ │ │
OR │ 0x90 │ 0x12 │ │ │
XOR │ 0xa0 │ 0x13 │ │ │
────────┼──────────┼──────────┼───────┼──────────────┼───────────────────────────────────
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 │ X │
MIN │ 0x0a │ 0x0a │ X │ X │
MAXU │ 0x0b │ 0x0b │ X │ X │
MAX │ 0x0c │ 0x0c │ X │ X │
AND │ 0x20 │ 0x20 │ │ │
OR │ 0x21 │ 0x21 │ │ │
XOR │ 0x22 │ 0x22 │ │ │
────────┼──────────┼──────────┼───────┼────────────────┼───────────────────────────────────

List 32-bit operations:
name │ opcode │ mOpcode │ carry │ use_last_carry │ NOTES
────────┼──────────┼──────────┼───────┼──────────┼───────────────────────────────────
ADD_W │ 0x14 │ 0x00 │ X │ │
SUB_W │ 0x24 │ 0x01 │ X │ │
LTU_W │ 0x64 │ 0x02 │ X │ X │
LT_W │ 0x65 │ 0x03 │ X │ X │
LEU_W │ 0x74 │ 0x04 │ X │ X │
LE_W │ 0x75 │ 0x05 │ X │ X │
EQ_W │ 0x54 │ 0x06 │ X │ X │
MINU_W │ 0xd4 │ 0x07 │ X │ X │
MIN_W │ 0xd5 │ 0x08 │ X │ X │
MAXU_W │ 0xe4 │ 0x09 │ X │ X │
MAX_W │ 0xe5 │ 0x10 │ X │ X │
────────┼──────────┼──────────┼───────┼──────────┼───────────────────────────────────
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 │ X │
MIN_W │ 0x1a │ 0x0a │ X │ X │
MAXU_W │ 0x1b │ 0x0b │ X │ X │
MAX_W │ 0x1c │ 0x0c │ X │ 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
*/

const int BINARY_ID = 20;
Expand All @@ -51,12 +71,12 @@ airtemplate Binary(const int N = 2**21, const int operation_bus_id = BINARY_ID)
const int input_chunk_bytes = bytes / input_chunks;

// Primary columns
col witness op; // operation code (e.g. add)
col witness mode32; // 1 if the operation is 32 bits, 0 otherwise
col witness m_op; // micro operation code of the binary table (e.g. add)
col witness mode32; // 1 if the operation is 32 bits, 0 otherwise
col witness free_in_a[bytes]; // input1
col witness free_in_b[bytes]; // input2
col witness free_in_c[bytes]; // output
col witness carry[bytes+1]; // bytes + 1 chunks carries [cin:0,cout:1],[cin:1,cout:2],...,[cin:bytes-1,cout:bytes]
col witness carry[bytes+1]; // bytes + 1 chunks carries [cin:0,cout:1],[cin:1,cout:2],...,[cin:bytes-1,cout:bytes]

// Secondary columns
col witness use_last_carry; // flag indicating whether the operation uses the last carry as its result
Expand All @@ -71,33 +91,33 @@ airtemplate Binary(const int N = 2**21, const int operation_bus_id = BINARY_ID)

// Constraints to check the correctness of each binary operation
/*
opid last a b c cin cout
─────────────────────────────────────────────────────────────
op 0 a0 b0 c0 0 carry0
op 0 a1 b1 c1 carry0 carry1
op 0 a2 b2 c2 carry1 carry2
op 0 a3 b3 c3 carry2 carry3 + 2*use_last_carry
op|EXT_32 0 a4|c3 b4|0 c4 carry3 carry4
op|EXT_32 0 a5|c3 b5|0 c5 carry4 carry5
op|EXT_32 0 a6|c3 b6|0 c6 carry5 carry6
op|EXT_32 1 a7|c3 b7|0 c7 carry6 carry7 + 2*use_last_carry
opid last a b c cin cout
───────────────────────────────────────────────────────────────
m_op 0 a0 b0 c0 0 carry0
m_op 0 a1 b1 c1 carry0 carry1
m_op 0 a2 b2 c2 carry1 carry2
m_op 0 a3 b3 c3 carry2 carry3 + 2*use_last_carry
m_op|EXT_32 0 a4|c3 b4|0 c4 carry3 carry4
m_op|EXT_32 0 a5|c3 b5|0 c5 carry4 carry5
m_op|EXT_32 0 a6|c3 b6|0 c6 carry5 carry6
m_op|EXT_32 1 a7|c3 b7|0 c7 carry6 carry7 + 2*use_last_carry
*/

lookup_assumes(BINARY_TABLE_ID, cols: [0, op, free_in_a[0], free_in_b[0], 0, free_in_c[0], carry[1]]);
lookup_assumes(BINARY_TABLE_ID, [0, m_op, free_in_a[0], free_in_b[0], 0, free_in_c[0], carry[1]]);

expr _op = (1-mode32) * (op - EXT_32_OP) + EXT_32_OP;
expr _m_op = (1-mode32) * (m_op - EXT_32_OP) + EXT_32_OP;
for (int i = 1; i < bytes; i++) {
expr _freeInA = (1-mode32) * (free_in_a[i] - free_in_c[bytes/2-1]) + free_in_c[bytes/2-1];
expr _free_in_b = (1-mode32) * free_in_b[i];

if (i < bytes/2 - 1) {
lookup_assumes(BINARY_TABLE_ID, cols: [0, op, free_in_a[i], free_in_b[i], carry[i], free_in_c[i], carry[i+1]]);
lookup_assumes(BINARY_TABLE_ID, [0, m_op, free_in_a[i], free_in_b[i], carry[i], free_in_c[i], carry[i+1]]);
} else if (i == bytes/2 - 1) {
lookup_assumes(BINARY_TABLE_ID, cols: [mode32, op, free_in_a[i], free_in_b[i], carry[i], free_in_c[i], cout32 + 2 * use_last_carry * mode32]);
lookup_assumes(BINARY_TABLE_ID, [mode32, m_op, free_in_a[i], free_in_b[i], carry[i], free_in_c[i], cout32 + 2 * use_last_carry * mode32]);
} else if (i < bytes - 1) {
lookup_assumes(BINARY_TABLE_ID, cols: [0, _op, _freeInA, _free_in_b, carry[i], free_in_c[i], carry[i+1]]);
lookup_assumes(BINARY_TABLE_ID, [0, _m_op, _freeInA, _free_in_b, carry[i], free_in_c[i], carry[i+1]]);
} else {
lookup_assumes(BINARY_TABLE_ID, cols: [1-mode32, _op, _freeInA, _free_in_b, carry[i], free_in_c[i], cout64 + 2 * use_last_carry * (1-mode32)]);
lookup_assumes(BINARY_TABLE_ID, [1-mode32, _m_op, _freeInA, _free_in_b, carry[i], free_in_c[i], cout64 + 2 * use_last_carry * (1-mode32)]);
}
}

Expand Down Expand Up @@ -132,7 +152,9 @@ airtemplate Binary(const int N = 2**21, const int operation_bus_id = BINARY_ID)
expr cout = (1-mode32) * (cout64 - cout32) + cout32;
c[0] += use_last_carry * cout;
c[input_chunks - 1] -= use_last_carry * cout;

expr op = m_op + 16 * mode32;

col witness multiplicity;
lookup_proves(operation_bus_id, mul: multiplicity, cols: [op, ...a, ...b, ...c, cout]);
lookup_proves(operation_bus_id, [m_op, ...a, ...b, ...c, cout], multiplicity);
}
76 changes: 44 additions & 32 deletions state-machines/binary/pil/binary_extension.pil
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,19 +7,31 @@ require "std_range_check.pil"
/*
List:
┼────────┼────────┼──────────┼──────────┼
│ name │ bits │ opcode │ mOpcode │
│ name │ bits │ op │ m_op │
┼────────┼────────┼──────────┼──────────┼
│ SLL │ 64 │ 0x30 │ 0x00 │
│ SRL │ 64 │ 0x41 │ 0x01 │
│ SRA │ 64 │ 0x40 │ 0x02 │
│ SLL_W │ 32 │ 0x34 │ 0x00 │
│ SRL_W │ 32 │ 0x45 │ 0x01 │
│ SRA_W │ 32 │ 0x44 │ 0x02 │
│ SE_B │ 32 │ 0x02 │ 0x03 │
│ SE_H │ 32 │ 0x03 │ 0x04 │
│ SE_W │ 32 │ 0x04 │ 0x05 │
│ SLL │ 64 │ 0x0d │ 0x0d │
│ SRL │ 64 │ 0x0e │ 0x0e │
│ SRA │ 64 │ 0x0f │ 0x0f │
│ SLL_W │ 32 │ 0x1d │ 0x0d │
│ SRL_W │ 32 │ 0x1e │ 0x0e │
│ SRA_W │ 32 │ 0x1f │ 0x0f │
│ SE_B │ 32 │ 0x24 │ 0x24 │
│ SE_H │ 32 │ 0x25 │ 0x25 │
│ SE_W │ 32 │ 0x26 │ 0x26 │
┼────────┼────────┼──────────┼──────────┼

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

mode32 64bits 32bits m_op op
0/1 SLL SLL_W 0x0d (0x0d,0x1d)
0/1 SRL SRL_W 0x0e (0x0e,0x1e)
0/1 SRA SRA_W 0x0f (0x0f,0x1f)
0 SE_B 0x24 0x24
0 SE_H 0x25 0x25
0 SE_W 0x26 0x26

Examples:
=======================================

Expand Down Expand Up @@ -72,7 +84,7 @@ airtemplate BinaryExtension(const int N = 2**18, const int operation_bus_id = BI
const int bits = 64;
const int bytes = bits / 8;

col witness op;
col witness m_op;
col witness mode8;
col witness mode16;
col witness mode32; // if mode32, in2_low∊[0,2^5-1], else in2_low∊[0,2^6-1]
Expand All @@ -86,26 +98,26 @@ airtemplate BinaryExtension(const int N = 2**18, const int operation_bus_id = BI
(mode8 + mode16 + mode32) * (mode8 + mode16 + mode32 - 1) === 0;

// Associate the mode with its possible operations
mode8 * (0x02 - op) === 0;
mode16 * (0x03 - op) === 0;
mode32 * (0x34 - op) * (0x45 - op) * (0x44 - op) * (0x04 - op) === 0;
mode8 * (0x02 - m_op) === 0;
mode16 * (0x03 - m_op) === 0;
mode32 * (0x34 - m_op) * (0x45 - m_op) * (0x44 - m_op) * (0x04 - m_op) === 0;

/*
opid j in1 in2 out0 out1
─────────────────────────────────────────────────────────────
op 0 in1_0 in2 out0_0 out1_0
op 1 in1_1|out0_0 in2|0 out0_1 out1_1
op 2 in1_2|out0_(0/1) in2|0 out0_2 out1_2
op 3 in1_3|out0_(0/1) in2|0 out0_3 out1_3
op|EXT 4 in1_4|out0_(0/1/3) in2|0 out0_4 out1_4
op|EXT 5 in1_5|out0_(0/1/3) in2|0 out0_5 out1_5
op|EXT 6 in1_6|out0_(0/1/3) in2|0 out0_6 out1_6
op|EXT 7 in1_7|out0_(0/1/3) in2|0 out0_7 out1_7
opid j in1 in2 out0 out1
───────────────────────────────────────────────────────────────
m_op 0 in1_0 in2 out0_0 out1_0
m_op 1 in1_1|out0_0 in2|0 out0_1 out1_1
m_op 2 in1_2|out0_(0/1) in2|0 out0_2 out1_2
m_op 3 in1_3|out0_(0/1) in2|0 out0_3 out1_3
m_op|EXT 4 in1_4|out0_(0/1/3) in2|0 out0_4 out1_4
m_op|EXT 5 in1_5|out0_(0/1/3) in2|0 out0_5 out1_5
m_op|EXT 6 in1_6|out0_(0/1/3) in2|0 out0_6 out1_6
m_op|EXT 7 in1_7|out0_(0/1/3) in2|0 out0_7 out1_7
*/

lookup_assumes(BINARY_EXTENSION_TABLE_ID, cols: [op, 0, in1[0], in2_low, out[0][0], out[0][1]]);
lookup_assumes(BINARY_EXTENSION_TABLE_ID, [m_op, 0, in1[0], in2_low, out[0][0], out[0][1]]);
for (int j = 1; j < bytes; j++) {
expr _op = op;
expr _m_op = m_op;
expr _in1 = 0;
expr _in2 = 0;
if (j == 1)
Expand All @@ -120,12 +132,12 @@ airtemplate BinaryExtension(const int N = 2**18, const int operation_bus_id = BI
}
else
{
_op = (1-mode32) * (op - EXT_OP) + EXT_OP;
_m_op = (1-mode32) * (m_op - EXT_OP) + EXT_OP;
_in1 = mode8*out[0][0] + mode16*out[1][0] + mode32*(out[bytes/2-1][0]) + (1-mode8)*(1-mode16)*(1-mode32)*in1[j];
_in2 = (1-mode8)*(1-mode16)*(1-mode32)*in2_low;
}

lookup_assumes(BINARY_EXTENSION_TABLE_ID, cols: [_op, j, _in1, _in2, out[j][0], out[j][1]]);
lookup_assumes(BINARY_EXTENSION_TABLE_ID, [_m_op, j, _in1, _in2, out[j][0], out[j][1]]);
}

// Relation with main
Expand All @@ -143,12 +155,11 @@ airtemplate BinaryExtension(const int N = 2**18, const int operation_bus_id = BI
range_check(colu: free_in2[2], min: 0, max: 2**16-1);
range_check(colu: free_in2[3], min: 0, max: 2**16-1);

expr op = m_op + 16 * mode32;
col witness multiplicity;

lookup_proves(
opid: operation_bus_id,
mul: multiplicity,
cols:
operation_bus_id,
[
op, // TODO: use correct opcode
in1[0] + in1[1]*2**8 + in1[2]*2**16 + in1[3]*2**24,
Expand All @@ -158,6 +169,7 @@ airtemplate BinaryExtension(const int N = 2**18, const int operation_bus_id = BI
out[0][0] + out[1][0] + out[2][0] + out[3][0] + out[4][0] + out[5][0] + out[6][0] + out[7][0],
out[0][1] + out[1][1] + out[2][1] + out[3][1] + out[4][1] + out[5][1] + out[6][1] + out[7][1],
0
]
],
multiplicity
)
}
Loading

0 comments on commit cc5b925

Please sign in to comment.