Skip to content

Commit

Permalink
WIP
Browse files Browse the repository at this point in the history
  • Loading branch information
hecmas committed Nov 29, 2024
1 parent 5211645 commit f8baaad
Show file tree
Hide file tree
Showing 3 changed files with 81 additions and 39 deletions.
13 changes: 8 additions & 5 deletions state-machines/arith/pil/arith.pil
Original file line number Diff line number Diff line change
Expand Up @@ -275,11 +275,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);
// TODO: 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,
// signed * (OP_LT_ABS - OP_LT) + OP_LT,
// (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
69 changes: 36 additions & 33 deletions state-machines/binary/pil/binary.pil
Original file line number Diff line number Diff line change
Expand Up @@ -4,43 +4,45 @@ 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 │ 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 │ │
LT_ABS │ 0x0d │ 0x0d │ X │ ? │
AND │ 0x20 │ 0x20 │ │ │
OR │ 0x21 │ 0x21 │ │ │
XOR │ 0x22 │ 0x22 │ │ │
──────────┼──────────┼──────────┼───────┼────────────────┼───────────────────────────────────

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 │ │
────────┼──────────┼──────────┼───────┼────────────────┼───────────────────────────────────
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 │ │
LT_ABS_W │ 0x1d │ 0x0d │ X │ ? │
──────────┼──────────┼──────────┼───────┼────────────────┼───────────────────────────────────

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

mode32 64bits 32bits m_op op
0/1 ADD ADD_W 0x02 (0x02,0x12)
Expand All @@ -54,7 +56,8 @@ require "std_lookup.pil"
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/1 LT_ABS LT_ABS_W 0x0d (0x0d,0x1d)
0 AND 0x20 0x20
0 OR 0x21 0x21
0 XOR 0x22 0x22
*/
Expand Down
38 changes: 37 additions & 1 deletion state-machines/binary/pil/binary_table.pil
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ require "constants.pil";
// 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^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
// 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 @@ -178,6 +178,42 @@ airtemplate BinaryTable(const int N = 2**22, const int disable_fixed = 0) {
}
op_is_min_max = 1;

case 0x0d: // LT_ABS,LT_ABS_W

// LT_NP, LT_PN

// state {lt, cin_a, cin_b, na, nb}

// cin_a[0] = na; // flag
// cin_b[0] = nb;

// _a = na ? a[i] ^ 0xFF + cin_a[i] : a[i];
// _b = nb ? b[i] ^ 0xFF + cin_b[i] : b[i];

// cout_a = _a >> 8;
// cout_b = _b >> 8;

// lt_out = cmp(_a & 0xFF, _b & 0xFF, lt_in);

if (a < b) {
cout = 1;
c = plast;
} else if (a == b) {
cout = cin;
c = plast * cin;
}

// If the last chunk is signed, then the result is the sign of a
if (plast && (a & 0x80) != (b & 0x80)) {
c = (a & 0x80) ? 1 : 0;
cout = c;
}

use_last_carry = plast;

c = (a & 0x80) ? 1 : 0;
if (plast) c = 1 - c;

case 0x20: // AND
c = a & b;

Expand Down

0 comments on commit f8baaad

Please sign in to comment.