Skip to content

Commit

Permalink
Pil for two buses
Browse files Browse the repository at this point in the history
  • Loading branch information
hecmas committed Dec 16, 2024
1 parent 3fc9061 commit 6319349
Show file tree
Hide file tree
Showing 5 changed files with 18 additions and 18 deletions.
12 changes: 6 additions & 6 deletions state-machines/arith/pil/arith_table.pil
Original file line number Diff line number Diff line change
Expand Up @@ -266,7 +266,7 @@ airtemplate ArithTable(int N = 2**7, int generate_table = 0) {
}
col witness multiplicity;

lookup_proves(ARITH_TABLE_ID, mul: multiplicity, cols: [OP, FLAGS, RANGE_AB, RANGE_CD]);
lookup_proves(ARITH_TABLE_ID, mul: multiplicity, expressions: [OP, FLAGS, RANGE_AB, RANGE_CD]);
}

function arith_table_assumes( const expr op, const expr flag_m32, const expr flag_div, const expr flag_na,
Expand All @@ -275,9 +275,9 @@ function arith_table_assumes( const expr op, const expr flag_m32, const expr fla
const expr flag_main_mul, const expr flag_main_div, const expr flag_signed,
const expr range_ab, const expr range_cd) {

lookup_assumes(ARITH_TABLE_ID, cols: [ op, flag_m32 + 2 * flag_div + 4 * flag_na + 8 * flag_nb +
16 * flag_np + 32 * flag_nr + 64 * flag_sext +
128 * flag_div_by_zero + 256 * flag_div_overflow +
512 * flag_main_mul + 1024 * flag_main_div + 2048 * flag_signed,
range_ab, range_cd]);
lookup_assumes(ARITH_TABLE_ID, expressions: [ op, flag_m32 + 2 * flag_div + 4 * flag_na + 8 * flag_nb +
16 * flag_np + 32 * flag_nr + 64 * flag_sext +
128 * flag_div_by_zero + 256 * flag_div_overflow +
512 * flag_main_mul + 1024 * flag_main_div + 2048 * flag_signed,
range_ab, range_cd]);
}
2 changes: 1 addition & 1 deletion state-machines/binary/pil/binary_extension.pil
Original file line number Diff line number Diff line change
Expand Up @@ -104,5 +104,5 @@ airtemplate BinaryExtension(const int N = 2**18, const int operation_bus_id) {
multiplicity
);

range_check(colu: in2[0], min: 0, max: 2**24-1, sel: op_is_shift);
range_check(expression: in2[0], min: 0, max: 2**24-1, sel: op_is_shift);
}
12 changes: 6 additions & 6 deletions state-machines/main/pil/main.pil
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
require "std_lookup.pil"
require "std_permutation.pil"
require "std_common.pil"
require "std_direct.pil"

const int BOOT_ADDR = 0x1000;
const int END_PC_ADDR = 0x2000;
Expand Down Expand Up @@ -163,7 +163,7 @@ airtemplate Main(int N = 2**21, int RC = 2, int stack_enabled = 0, const int ope
// Operation.assume => how organize software
col witness __debug_operation_bus_enabled;

lookup_assumes(operation_bus_id, [STEP, op, a[0], (1 - m32) * a[1], b[0], (1 - m32) * b[1], ...c, flag], sel: is_external_op * __debug_operation_bus_enabled, name: PIOP_NAME_ISOLATED);
lookup_assumes(operation_bus_id, [STEP, op, a[0], (1 - m32) * a[1], b[0], (1 - m32) * b[1], ...c, flag], sel: is_external_op * __debug_operation_bus_enabled);

const expr a_src_c;
const expr b_src_c;
Expand Down Expand Up @@ -241,8 +241,8 @@ airtemplate Main(int N = 2**21, int RC = 2, int stack_enabled = 0, const int ope
//

const expr bus_main_segment = main_segment - SEGMENT_LAST * (main_segment * main_last_segment - 1 + main_last_segment);
permutation (MAIN_CONTINUATION_ID, cols: [bus_main_segment, is_last_continuation, pc, c[0], c[1], set_pc, jmp_offset1, flag * SEGMENT_LAST * (jmp_offset1 - jmp_offset2) + jmp_offset2],
sel: SEGMENT_LAST - SEGMENT_L1, name: PIOP_NAME_ISOLATED, bus_type: PIOP_BUS_SUM);
permutation (MAIN_CONTINUATION_ID, expressions: [bus_main_segment, is_last_continuation, pc, c[0], c[1], set_pc, jmp_offset1, flag * SEGMENT_LAST * (jmp_offset1 - jmp_offset2) + jmp_offset2],
sel: SEGMENT_LAST - SEGMENT_L1, bus_type: PIOP_BUS_PROD);

flag * (1 - flag) === 0;

Expand Down Expand Up @@ -271,6 +271,6 @@ airtemplate Main(int N = 2**21, int RC = 2, int stack_enabled = 0, const int ope
lookup_assumes(ROM_BUS_ID, [pc, a_offset_imm0, a_imm1, b_offset_imm0, b_imm1, ind_width,
op, store_offset, jmp_offset1, jmp_offset2, rom_flags], sel: 1 - SEGMENT_L1);

direct_global_update_proves(MAIN_CONTINUATION_ID, cols: [0, 0, 4096, 0, 0, 0, 0, 0], bus_type: PIOP_BUS_SUM);
direct_global_update_assumes(MAIN_CONTINUATION_ID, cols: [0, 1, 0x1000_0000, 0, 0, 0, 0, 0], bus_type: PIOP_BUS_SUM);
direct_global_update_proves(MAIN_CONTINUATION_ID, expressions: [0, 0, 4096, 0, 0, 0, 0, 0], bus_type: PIOP_BUS_PROD);
direct_global_update_assumes(MAIN_CONTINUATION_ID, expressions: [0, 1, 0x1000_0000, 0, 0, 0, 0, 0], bus_type: PIOP_BUS_PROD);
}
8 changes: 4 additions & 4 deletions state-machines/mem/pil/mem.pil
Original file line number Diff line number Diff line change
Expand Up @@ -153,10 +153,10 @@ airtemplate Mem(const int N = 2**21, const int id = MEMORY_ID, const int RC = 2,
direct_global_update_proves(MEMORY_CONT_ID, [ base_address, 0, internal_base_address, 0, ...zeros], sel: enable_flag);

// for security check that first address has correct value, to avoid add huge quantity of instances to "overflow" prime field.
range_check(colu: previous_segment_addr - internal_base_address + 1, min: 1, max: MEMORY_MAX_DIFF);
range_check(expression: previous_segment_addr - internal_base_address + 1, min: 1, max: MEMORY_MAX_DIFF);

// control final of memory
range_check(colu: internal_end_address - segment_last_addr + 1, min: 1, max: MEMORY_MAX_DIFF);
range_check(expression: internal_end_address - segment_last_addr + 1, min: 1, max: MEMORY_MAX_DIFF);


// check increment of memory
Expand All @@ -181,7 +181,7 @@ airtemplate Mem(const int N = 2**21, const int id = MEMORY_ID, const int RC = 2,

is_first_segment * SEGMENT_L1 * (1 - addr_changes) === 0;

range_check(colu: increment, min: 1, max: MEMORY_MAX_DIFF);
range_check(expression: increment, min: 1, max: MEMORY_MAX_DIFF);
}

(1 - addr_changes) * (addr - previous_addr) === 0;
Expand Down Expand Up @@ -218,7 +218,7 @@ airtemplate Mem(const int N = 2**21, const int id = MEMORY_ID, const int RC = 2,
// These are handled with the Memory Align component

const expr mem_op = wr * (MEMORY_STORE_OP - MEMORY_LOAD_OP) + MEMORY_LOAD_OP;
permutation_proves(MEMORY_ID, cols: [mem_op, addr * mem_bytes, step, mem_bytes, ...value], sel: sel);
permutation_proves(MEMORY_ID, expressions: [mem_op, addr * mem_bytes, step, mem_bytes, ...value], sel: sel);
}

function mem_load(int id = MEMORY_ID, expr addr, expr step, expr step_offset = 0, expr bytes = 8, expr value[], expr sel = 1) {
Expand Down
2 changes: 1 addition & 1 deletion state-machines/mem/pil/mem_align.pil
Original file line number Diff line number Diff line change
Expand Up @@ -184,5 +184,5 @@ airtemplate MemAlign(const int N = 2**10, const int RC = 2, const int CHUNK_NUM
for (int i = 0; i < RC; i++) {
value[i] === sel_prove * prove_val[i] + sel_assume * assume_val[i];
}
permutation(MEMORY_ID, cols: [wr * (MEMORY_STORE_OP - MEMORY_LOAD_OP) + MEMORY_LOAD_OP, addr * CHUNK_NUM + offset, step, width, ...value], sel: sel_prove - sel_assume);
permutation(MEMORY_ID, expressions: [wr * (MEMORY_STORE_OP - MEMORY_LOAD_OP) + MEMORY_LOAD_OP, addr * CHUNK_NUM + offset, step, width, ...value], sel: sel_prove - sel_assume, bus_type: PIOP_BUS_PROD);
}

0 comments on commit 6319349

Please sign in to comment.