require "std_constants.pil"
require "std_lookup.pil"
require "operations.pil"
require "opids.pil"
/* PIL Binary Operations Table used by Binary Extension
The shift/rotate/single-bit family only depends on the low 6 bits of B (the shift amount is
masked with LS_6_BITS for 64-bit ops and LS_5_BITS for the *_W variants), so B is enumerated
over 2^6 (0..63) instead of 2^8. This shrinks every B-using block from 2^19 to 2^17.
Accumulated rows
SLL 2^8 (A) * 2^3 (OFFSET) * 2^6 (B) = 2^17 | 131,072
SRL 2^8 (A) * 2^3 (OFFSET) * 2^6 (B) = 2^17 | 262,144
SRA 2^8 (A) * 2^3 (OFFSET) * 2^6 (B) = 2^17 | 393,216
SLL_W 2^8 (A) * 2^3 (OFFSET) * 2^6 (B) = 2^17 | 524,288
SRL_W 2^8 (A) * 2^3 (OFFSET) * 2^6 (B) = 2^17 | 655,360
SRA_W 2^8 (A) * 2^3 (OFFSET) * 2^6 (B) = 2^17 | 786,432
SEXT_B 2^8 (A) * 2^3 (OFFSET) = 2^11 | 788,480
SEXT_H 2^8 (A) * 2^3 (OFFSET) = 2^11 | 790,528
SEXT_W 2^8 (A) * 2^3 (OFFSET) = 2^11 | 792,576
REV8 2^8 (A) * 2^3 (OFFSET) = 2^11 | 794,624
ORCB 2^8 (A) * 2^3 (OFFSET) = 2^11 | 796,672
ROL 2^8 (A) * 2^3 (OFFSET) * 2^6 (B) = 2^17 | 927,744
ROL_W 2^8 (A) * 2^3 (OFFSET) * 2^6 (B) = 2^17 | 1,058,816
ROR 2^8 (A) * 2^3 (OFFSET) * 2^6 (B) = 2^17 | 1,189,888
ROR_W 2^8 (A) * 2^3 (OFFSET) * 2^6 (B) = 2^17 | 1,320,960
CPOP 2^8 (A) * 2^3 (OFFSET) = 2^11 | 1,323,008
CPOP_W 2^8 (A) * 2^3 (OFFSET) = 2^11 | 1,325,056
CTZ 2^6 (ACC) * 2^3 (OFFSET) * 2^8 (A) = 2^17 | 1,456,128
CTZ_W 2^6 (ACC) * 2^3 (OFFSET) * 2^8 (A) = 2^17 | 1,587,200
CLZ 2^6 (ACC) * 2^3 (OFFSET) * 2^8 (A) = 2^17 | 1,718,272
CLZ_W 2^6 (ACC) * 2^3 (OFFSET) * 2^8 (A) = 2^17 | 1,849,344
PACK 2^8 (A) * 2^3 (OFFSET) = 2^11 | 1,851,392
PACK_H 2^8 (A) * 2^3 (OFFSET) = 2^11 | 1,853,440
PACK_W 2^8 (A) * 2^3 (OFFSET) = 2^11 | 1,855,488
BCLR 2^8 (A) * 2^3 (OFFSET) * 2^6 (B) = 2^17 | 1,986,560
BEXT 2^8 (A) * 2^3 (OFFSET) * 2^6 (B) = 2^17 | 2,117,632
BINV 2^8 (A) * 2^3 (OFFSET) * 2^6 (B) = 2^17 | 2,248,704
BSET 2^8 (A) * 2^3 (OFFSET) * 2^6 (B) = 2^17 | 2,379,776 => BINARY_EXTENSION_TABLE_SIZE
Total N = 2,379,776 rows, with 2^21 (2,097,152) < N < 2^22 (4,194,304)
*/
const int BINARY_EXTENSION_TABLE_SIZE = 2_379_776;
const int BINARY_EXTENSION_TABLE_SIZE_P2 = 2**22;
// Row where the byte-chain blocks (CTZ, CTZ_W, CLZ, CLZ_W) start. Each chain op enumerates its
// acc_in input (0..63, the "outer" dimension, stride P2_11) instead of the B operand, so each
// block is 2^6 (acc_in) * 2^3 (offset) * 2^8 (byte) = P2_17 rows.
const int CTZ_TABLE_OFFSET = 1_325_056;
const int CTZ_W_TABLE_OFFSET = CTZ_TABLE_OFFSET + P2_17;
const int CLZ_TABLE_OFFSET = CTZ_TABLE_OFFSET + P2_17 * 2;
const int CLZ_W_TABLE_OFFSET = CTZ_TABLE_OFFSET + P2_17 * 3;
airtemplate BinaryExtensionTable(int N = 0) {
if (N == 0) {
N = VIRTUAL ? BINARY_EXTENSION_TABLE_SIZE : BINARY_EXTENSION_TABLE_SIZE_P2;
} else if (N < BINARY_EXTENSION_TABLE_SIZE) {
error(`N must be at least ${BINARY_EXTENSION_TABLE_SIZE}, but N=${N} was provided`);
}
const int SE_MASK_32 = 0xFF_FF_FF_FF_00_00_00_00;
const int SE_MASK_16 = 0xFF_FF_FF_FF_FF_FF_00_00;
const int SE_MASK_8 = 0xFF_FF_FF_FF_FF_FF_FF_00;
const int SIGN_32_BIT = 0x80_00_00_00;
const int SIGN_BYTE = 0x80;
const int LS_5_BITS = 0x1F;
const int LS_6_BITS = 0x3F;
// Number of bytes of the 64-bit word (must match BYTES in binary_extension.pil).
const int BYTES = 8;
// Input A (8 bits)
col fixed A = [0..255]...;
// Input B (6 bits: only the low 6 bits of the shift amount / bit index are relevant)
col fixed B = [[0:P2_11..63:P2_11]:3, // SLL, SRL, SRA
[0:P2_11..63:P2_11]:3, // SLL_W, SRL_W, SRA_W
0:(P2_11*5), // SEXT_B, SEXT_H, SEXT_W, REV8, ORCB
[0:P2_11..63:P2_11]:4, // ROL, ROL_W, ROR, ROR_W (use B)
0:(P2_11*2), // CPOP, CPOP_W (single input, B unused)
0:(P2_17*4), // CTZ, CTZ_W, CLZ, CLZ_W (single input, B unused; acc_in in C1)
0:(P2_11*3), // PACK, PACK_H, PACK_W (two inputs interleaved in free_in_a; B unused)
[0:P2_11..63:P2_11]:4]...; // BCLR, BEXT, BINV, BSET (shift family: B = bit index)
// Operation opcode
col fixed OP = [ OP_SLL:P2_17, OP_SRL:P2_17, OP_SRA:P2_17, // SLL, SRL, SRA
OP_SLL_W:P2_17, OP_SRL_W:P2_17, OP_SRA_W:P2_17, // SLL_W, SRL_W, SRA_W
OP_SEXT_B:P2_11, OP_SEXT_H:P2_11, OP_SEXT_W:P2_11, // SEXT_B, SEXT_H, SEXT_W
OP_REV8:P2_11, OP_ORCB:P2_11, // REV8, ORCB
OP_ROL:P2_17, OP_ROL_W:P2_17, // ROL, ROL_W
OP_ROR:P2_17, OP_ROR_W:P2_17, // ROR, ROR_W
OP_CPOP:P2_11, OP_CPOP_W:P2_11, // CPOP, CPOP_W
OP_CTZ:P2_17, OP_CTZ_W:P2_17, // CTZ, CTZ_W
OP_CLZ:P2_17, OP_CLZ_W:P2_17, // CLZ, CLZ_W
OP_PACK:P2_11, OP_PACK_H:P2_11, OP_PACK_W:P2_11, // PACK, PACK_H, PACK_W
OP_BCLR:P2_17, OP_BEXT:P2_17, // BCLR, BEXT
OP_BINV:P2_17, OP_BSET:P2_17]...; // BINV, BSET
col fixed C0; // Output C0 (32 bits)
col fixed C1; // Output C1 (32 bits)
// Offset and flags column: encodes both the byte offset and the operation flags in a single
// fixed column, OFFSET_AND_FLAGS = offset + BYTES * (op_is_shift + 2 * op_is_chain
// + 4 * op_is_chain_rev + 8 * op_is_combine). This lets the caller send one combined value
// (j + BYTES * flags) instead of a separate offset plus four flag columns, saving fixed
// columns. flags is 0 (single-input), 1 (shift), 2 (chain), 4 (chain_rev) or 8 (combine);
// never more than one.
col fixed OFFSET_AND_FLAGS;
#pragma transpile
for (int i = 0; i < N; i++) {
// offset is the middle dimension (stride P2_8, cycles 0..7); derived from the row index
// so no dedicated OFFSET column is needed.
const int offset = (i / P2_8) % BYTES;
int [op, a, b] = [OP[i], A[i], B[i]];
int out = 0;
int op_is_shift = 0;
int op_is_chain = 0;
int op_is_chain_rev = 0;
int op_is_combine = 0;
const int a_pos = a << (8*offset);
switch (op) {
case OP_SLL: // SLL: Shift Left Logical
// Shifts value left by B positions
// Example: SLL(0x12, offset=0, B=4) = 0x120
// Example: SLL(0x80, offset=1, B=1) = 0x10000 (0x8000 << 1)
out = a_pos << (b & LS_6_BITS);
op_is_shift = 1;
case OP_SRL: // SRL: Shift Right Logical
// Shifts value right by B positions
// Example: SRL(0x80, offset=0, B=4) = 0x8
// Example: SRL(0xFF, offset=2, B=8) = 0xFF00 (0xFF0000 >> 8)
out = a_pos >> (b & LS_6_BITS);
op_is_shift = 1;
case OP_SRA: // SRA: Shift Right Arithmetic
// Shifts value right by B positions, preserves sign bit
// Example: SRA(0x80, offset=7, B=8) = 0xFF80000000000000 (sign extends)
// Example: SRA(0x7F, offset=7, B=1) = 0x3F80000000000000 (no sign extend)
const int _b = b & LS_6_BITS;
out = a_pos >> _b;
if (offset == 7) {
// most significant bit of most significant byte define if negative or not
// if negative then add b bits one on the left
if (a & SIGN_BYTE) {
out = out | (MASK_64 << (64 - _b));
}
}
op_is_shift = 1;
case OP_SLL_W: // SLL_W: Shift Left Logical Word
// Shifts value left by B positions, sign extends the rest
// Example: SLL_W(0x12, offset=0, B=4) = 0x120
// Example: SLL_W(0x01, offset=3, B=7) = 0xFFFFFFFF80000000
if (offset >= 4) {
// last most significant bytes are ignored because it's 32-bit operation
out = 0;
} else {
out = (a_pos << (b & LS_5_BITS)) & MASK_32;
if (out & SIGN_32_BIT) {
out = out | SE_MASK_32;
}
}
op_is_shift = 1;
case OP_SRL_W: // SRL_W: Shift Right Logical Word
// Shifts value right by B positions, sign extends the rest
// Example: SRL_W(0x80, offset=0, B=4) = 0x8
// Example: SRL_W(0xFF, offset=3, B=1) = 0x7F800000
if (offset >= 4) {
// last most significant bytes are ignored because it's 32-bit operation
out = 0;
} else {
out = (a_pos >> (b & LS_5_BITS)) & MASK_32;
if (out & SIGN_32_BIT) {
out = out | SE_MASK_32;
}
}
op_is_shift = 1;
case OP_SRA_W: // SRA_W: Shift Right Arithmetic Word
// Shifts value right by B positions, preserves sign
// Example: SRA_W(0x80, offset=3, B=1) = 0xFFFFFFFF40000000
// Example: SRA_W(0x7F, offset=3, B=1) = 0x3F800000
if (offset >= 4) {
// last most significant bytes are ignored because it's 32-bit operation
out = 0;
} else {
const int _b = b & LS_5_BITS;
out = a_pos >> _b;
if (offset == 3) {
// most significant bit of most significant byte define if negative or not
// if negative then add b bits one on the left
if (a & SIGN_BYTE) {
out = out | (MASK_64 << (32 - _b));
}
}
}
op_is_shift = 1;
case OP_SEXT_B: // SEXT_B: Sign Extend Byte (8-bit to 64-bit)
// Sign extends an 8-bit value to 64-bit
// Example: SEXT_B(0x7F, offset=0) = 0x7F (positive byte)
// Example: SEXT_B(0x80, offset=0) = 0xFFFFFFFFFFFFFF80 (negative byte)
// Example: SEXT_B(0x42, offset=1) = 0x0 (ignored, only offset 0 matters)
if (offset == 0) {
// the most significant bit of first byte determines the sign extend
out = (a & SIGN_BYTE) ? a | SE_MASK_8 : a
} else {
// the rest of the bytes are ignored
out = 0;
}
case OP_SEXT_H: // SEXT_H: Sign Extend Halfword (16-bit to 64-bit)
// Sign extends a 16-bit value to 64-bit
// Example: SEXT_H with offset=0,A=0x34 and offset=1,A=0x12 = 0x1234 (positive)
// Example: SEXT_H with offset=0,A=0x34 and offset=1,A=0x80 = 0xFFFFFFFFFFFF8034 (negative)
if (offset == 0) {
// fist byte not define the sign extend, but participate of result
out = a;
} else if (offset == 1) {
// the most significant bit of second byte determines the sign extend
out = (a & SIGN_BYTE) ? a_pos | SE_MASK_16 : a_pos
} else {
// the rest of the bytes are ignored
out = 0;
}
case OP_SEXT_W: // SEXT_W: Sign Extend Word (32-bit to 64-bit)
// Sign extends a 32-bit value to 64-bit
// Example: SEXT_W with bytes forming 0x12345678 = 0x12345678 (positive)
// Example: SEXT_W with bytes forming 0x80000000 = 0xFFFFFFFF80000000 (negative)
if (offset <= 3) {
out = a_pos;
if (offset == 3) {
if (a & SIGN_BYTE) {
// the most significant bit of fourth byte determines the sign extend
out = out | SE_MASK_32
}
}
}
case OP_REV8: // REV8: reverse the byte order of the 64-bit value
// Byte at position `offset` moves to position 7 - offset.
// Example: REV8(0x11, offset=0) contributes 0x1100000000000000
out = a << (8 * (7 - offset));
// op_is_shift stays 0 (single input, like SEXT)
case OP_ORCB: // ORC.B: OR-combine bits within each byte, in place
// Output byte is 0xFF if the input byte has any bit set, else 0x00.
out = ((a != 0) ? 0xFF : 0x00) << (8 * offset);
// op_is_shift stays 0 (single input, per-byte, like SEXT)
case OP_ROL: // ROL: rotate left the full 64-bit value by B (mod 64)
const int rol_s = b & LS_6_BITS;
out = (rol_s == 0) ? a_pos : (((a_pos << rol_s) | (a_pos >> (64 - rol_s))) & MASK_64);
op_is_shift = 1;
case OP_ROR: // ROR: rotate right the full 64-bit value by B (mod 64)
const int ror_s = b & LS_6_BITS;
out = (ror_s == 0) ? a_pos : (((a_pos >> ror_s) | (a_pos << (64 - ror_s))) & MASK_64);
op_is_shift = 1;
case OP_ROL_W: // ROL_W: rotate left low 32 bits by B (mod 32), sign-extend
if (offset >= 4) {
out = 0;
} else {
const int rolw_s = b & LS_5_BITS;
const int rolw_lo = a_pos & MASK_32;
out = (rolw_s == 0) ? rolw_lo : (((rolw_lo << rolw_s) | (rolw_lo >> (32 - rolw_s))) & MASK_32);
if (out & SIGN_32_BIT) {
out = out | SE_MASK_32;
}
}
op_is_shift = 1;
case OP_ROR_W: // ROR_W: rotate right low 32 bits by B (mod 32), sign-extend
if (offset >= 4) {
out = 0;
} else {
const int rorw_s = b & LS_5_BITS;
const int rorw_lo = a_pos & MASK_32;
out = (rorw_s == 0) ? rorw_lo : (((rorw_lo >> rorw_s) | (rorw_lo << (32 - rorw_s))) & MASK_32);
if (out & SIGN_32_BIT) {
out = out | SE_MASK_32;
}
}
op_is_shift = 1;
case OP_CPOP: // CPOP: population count (number of set bits), summed per byte
// Each byte contributes the count of its set bits (0..8), position-independent.
// The 8 per-byte contributions sum to the full 64-bit popcount (0..64).
out = 0;
for (int k = 0; k < 8; k++) {
out = out + ((a >> k) & 0x01);
}
// op_is_shift stays 0 (single input, like SEXT)
case OP_CPOP_W: // CPOP_W: population count of the low 32 bits
// Only the low 4 bytes contribute; higher bytes are ignored.
if (offset >= 4) {
out = 0;
} else {
out = 0;
for (int k = 0; k < 8; k++) {
out = out + ((a >> k) & 0x01);
}
}
// op_is_shift stays 0 (single input, per-byte, like SEXT)
case OP_CTZ: // CTZ: count trailing zeros of the 64-bit value
// Byte-chain op. acc_in is the running count entering this byte, enumerated as
// the outer dimension (0..63) and carried in C1. The byte is "still counting"
// (all lower bytes were zero) iff acc_in == 8*offset. In that case it adds its
// own trailing-zero count (8 if the byte is zero, else 0..7); otherwise it is
// already past the first set bit and adds 0. Increments telescope to ctz.
const int ctz_acc_in = (i - CTZ_TABLE_OFFSET) / P2_11;
int ctz_tz = 0;
for (int k = 0; k < 8; k++) {
if (ctz_tz == k && ((a >> k) & 0x01) == 0) {
ctz_tz = ctz_tz + 1;
}
}
int ctz_incr = (ctz_acc_in == 8 * offset) ? ctz_tz : 0;
// C0 = increment, C1 = acc_in
out = ctz_incr + (ctz_acc_in << 32);
op_is_chain = 1;
case OP_CTZ_W: // CTZ_W: count trailing zeros of the low 32 bits
// Same chain as CTZ but only the low 4 bytes participate; bytes at offset >= 4
// add nothing. If all 4 low bytes are zero the increments reach 32.
const int ctzw_acc_in = (i - CTZ_W_TABLE_OFFSET) / P2_11;
int ctzw_tz = 0;
for (int k = 0; k < 8; k++) {
if (ctzw_tz == k && ((a >> k) & 0x01) == 0) {
ctzw_tz = ctzw_tz + 1;
}
}
int ctzw_incr = 0;
if (offset < 4) {
ctzw_incr = (ctzw_acc_in == 8 * offset) ? ctzw_tz : 0;
}
out = ctzw_incr + (ctzw_acc_in << 32);
op_is_chain = 1;
case OP_CLZ: // CLZ: count leading zeros of the 64-bit value
// Reverse byte-chain op (scanned MSB -> LSB). The position threshold is measured
// from the top: the byte is "still counting" (all higher bytes were zero) iff
// acc_in == 8*(BYTES-1-offset). In that case it adds its own leading-zero count
// (8 if the byte is zero, else 0..7); otherwise it adds 0. Increments telescope
// to clz. acc_in is enumerated (0..63) as the outer dimension and carried in C1.
const int clz_acc_in = (i - CLZ_TABLE_OFFSET) / P2_11;
int clz_lz = 0;
for (int k = 0; k < 8; k++) {
if (clz_lz == k && ((a >> (7 - k)) & 0x01) == 0) {
clz_lz = clz_lz + 1;
}
}
int clz_incr = (clz_acc_in == 8 * (BYTES - 1 - offset)) ? clz_lz : 0;
out = clz_incr + (clz_acc_in << 32);
op_is_chain_rev = 1;
case OP_CLZ_W: // CLZ_W: count leading zeros of the low 32 bits
// Same reverse chain as CLZ but over the low 4 bytes only; the top of the 32-bit
// word is byte offset 3. Bytes at offset >= 4 add nothing. If all 4 low bytes are
// zero the increments reach 32.
const int clzw_acc_in = (i - CLZ_W_TABLE_OFFSET) / P2_11;
int clzw_lz = 0;
for (int k = 0; k < 8; k++) {
if (clzw_lz == k && ((a >> (7 - k)) & 0x01) == 0) {
clzw_lz = clzw_lz + 1;
}
}
int clzw_incr = 0;
if (offset < 4) {
clzw_incr = (clzw_acc_in == 8 * (3 - offset)) ? clzw_lz : 0;
}
out = clzw_incr + (clzw_acc_in << 32);
op_is_chain_rev = 1;
case OP_PACK: // PACK: rd = rs1[31:0] | (rs2[31:0] << 32)
// Two-input op. free_in_a holds rs1[31:0] in its low 4 bytes and rs2[31:0] in its
// high 4 bytes, so each byte just lands at its own position (identity placement).
out = a_pos;
op_is_combine = 1;
case OP_PACK_H: // PACK_H: rd = rs1[7:0] | (rs2[7:0] << 8)
// Only byte 0 (rs1[7:0]) and byte 4 (rs2[7:0]) contribute; the latter moves to
// result byte 1. All other bytes are ignored.
if (offset == 0) {
out = a; // rs1[7:0] at byte 0
} else if (offset == 4) {
out = a << 8; // rs2[7:0] at byte 1
} else {
out = 0;
}
op_is_combine = 1;
case OP_PACK_W: // PACK_W: rd = sext32(rs1[15:0] | (rs2[15:0] << 16))
// Bytes 0,1 (rs1[15:0]) land at result bytes 0,1; bytes 4,5 (rs2[15:0]) land at
// result bytes 2,3. The result is a 32-bit value sign-extended to 64 bits; the
// sign bit is bit 7 of byte 5 (bit 31 of the result).
if (offset == 0) {
out = a; // rs1[7:0] at byte 0
} else if (offset == 1) {
out = a << 8; // rs1[15:8] at byte 1
} else if (offset == 4) {
out = a << 16; // rs2[7:0] at byte 2
} else if (offset == 5) {
out = a << 24; // rs2[15:8] at byte 3
if (a & SIGN_BYTE) {
out = out | SE_MASK_32;
}
} else {
out = 0;
}
op_is_combine = 1;
case OP_BCLR: // BCLR: rd = a & ~(1 << (b & 63)) (shift family: b is the bit index)
// Clearing bit `pos` only affects the byte that contains it; a_pos has no bits at
// `pos` for the other bytes, so masking is a no-op there (branch-free).
const int bclr_pos = b & LS_6_BITS;
out = a_pos & (MASK_64 ^ (1 << bclr_pos));
op_is_shift = 1;
case OP_BEXT: // BEXT: rd = (a >> (b & 63)) & 1 (result bit lands at position 0)
const int bext_pos = b & LS_6_BITS;
out = (offset == (bext_pos >> 3)) ? ((a >> (bext_pos & 0x07)) & 0x01) : 0;
op_is_shift = 1;
case OP_BINV: // BINV: rd = a ^ (1 << (b & 63)) (only the byte holding `pos` flips)
const int binv_pos = b & LS_6_BITS;
out = a_pos ^ ((offset == (binv_pos >> 3)) ? (1 << binv_pos) : 0);
op_is_shift = 1;
case OP_BSET: // BSET: rd = a | (1 << (b & 63)) (only the byte holding `pos` sets it)
const int bset_pos = b & LS_6_BITS;
out = a_pos | ((offset == (bset_pos >> 3)) ? (1 << bset_pos) : 0);
op_is_shift = 1;
default:
error(`Invalid operation opcode: ${op} at row ${i}`);
}
const int c0 = out & MASK_32;
const int c1 = (out >> 32) & MASK_32;
C0[i] = c0;
C1[i] = c1;
const int offset_and_flags = offset + BYTES * (op_is_shift + 2 * op_is_chain + 4 * op_is_chain_rev + 8 * op_is_combine);
OFFSET_AND_FLAGS[i] = offset_and_flags;
log(`T[${i}] = [${op}, ${offset_and_flags}, ${a}, ${b}, ${c0}, ${c1}]`);
}
col witness multiplicity;
lookup_proves(BINARY_EXTENSION_TABLE_ID, [OP, OFFSET_AND_FLAGS, A, B, C0, C1], multiplicity);
}