@@ -6,15 +6,15 @@ namespace execution;
66// Columns declared in execution.pil (see temporality groups 3 & 6):
77//
88// Inputs for read/write (retrieved through #[EXEC_SPEC_READ]):
9- // pol commit sel_mem_op_reg[6 ]; // Memory access (register is active)
10- // pol commit rw_reg[6 ]; // Read / Write (only if sel_mem_op_reg[i] = 1)
11- // pol commit sel_tag_check_reg[6 ]; // Tag check (only for read)
12- // pol commit expected_tag_reg[6 ]; // Expected tag (only if sel_tag_check_reg[i] = 1)
9+ // pol commit sel_mem_op_reg[4 ]; // Memory access (register is active)
10+ // pol commit rw_reg[4 ]; // Read / Write (only if sel_mem_op_reg[i] = 1)
11+ // pol commit sel_tag_check_reg[4 ]; // Tag check (only for read)
12+ // pol commit expected_tag_reg[4 ]; // Expected tag (only if sel_tag_check_reg[i] = 1)
1313// pol commit rop[5]; // Resolved operands (for read/write), always addresses here.
1414//
1515// Inputs for write, Outputs for read:
16- // pol commit register[6 ];
17- // pol commit mem_tag_reg[6 ];
16+ // pol commit register[4 ];
17+ // pol commit mem_tag_reg[4 ];
1818//
1919// Execution.pil temporality group selectors:
2020// pol commit sel_read_registers; // Register read
@@ -45,7 +45,7 @@ sel_read_registers = 0;
4545// (b) sel_mem_op_reg[i] is a write and we got to the write temporality group.
4646// Note that sel_mem_op_reg[i] and rw_reg[i] are defined (constrained) because
4747// they are retrieved through #[EXEC_SPEC_READ] from temporality group 2 (which happens earlier).
48- pol commit sel_op_reg_effective[6 ]; // @boolean (by definition)
48+ pol commit sel_op_reg_effective[4 ]; // @boolean (by definition)
4949#[SEL_OP_REG_EFFECTIVE_0]
5050sel_op_reg_effective[0] = sel_mem_op_reg[0] * (sel_read_registers * (1 - rw_reg[0]) + sel_write_registers * rw_reg[0]);
5151#[SEL_OP_REG_EFFECTIVE_1]
@@ -54,10 +54,6 @@ sel_op_reg_effective[1] = sel_mem_op_reg[1] * (sel_read_registers * (1 - rw_reg[
5454sel_op_reg_effective[2] = sel_mem_op_reg[2] * (sel_read_registers * (1 - rw_reg[2]) + sel_write_registers * rw_reg[2]);
5555#[SEL_OP_REG_EFFECTIVE_3]
5656sel_op_reg_effective[3] = sel_mem_op_reg[3] * (sel_read_registers * (1 - rw_reg[3]) + sel_write_registers * rw_reg[3]);
57- #[SEL_OP_REG_EFFECTIVE_4]
58- sel_op_reg_effective[4] = sel_mem_op_reg[4] * (sel_read_registers * (1 - rw_reg[4]) + sel_write_registers * rw_reg[4]);
59- #[SEL_OP_REG_EFFECTIVE_5]
60- sel_op_reg_effective[5] = sel_mem_op_reg[5] * (sel_read_registers * (1 - rw_reg[5]) + sel_write_registers * rw_reg[5]);
6157
6258// Observe that the following permutations span both temporality groups (activated at most once per instruction).
6359// That's why we have to properly activate them with the above selectors, which take into account
@@ -74,13 +70,6 @@ is memory.sel_register_op[2] { memory.clk, memory.space_id, memory.address, memo
7470#[MEM_OP_3]
7571sel_op_reg_effective[3] { clk, context_id, rop[3], register[3], mem_tag_reg[3], rw_reg[3] }
7672is memory.sel_register_op[3] { memory.clk, memory.space_id, memory.address, memory.value, memory.tag, memory.rw };
77- #[MEM_OP_4]
78- sel_op_reg_effective[4] { clk, context_id, rop[4], register[4], mem_tag_reg[4], rw_reg[4] }
79- is memory.sel_register_op[4] { memory.clk, memory.space_id, memory.address, memory.value, memory.tag, memory.rw };
80- // TODO(MW): check when reducing max registers
81- // #[MEM_OP_5]
82- // sel_op_reg_effective[5] { clk, context_id, rop[5], register[5], mem_tag_reg[5], rw_reg[5] }
83- // is memory.sel_register_op[5] { memory.clk, memory.space_id, memory.address, memory.value, memory.tag, memory.rw };
8473
8574// This error is true iff the following "batch" check failed. That is if some tag is not the expected one.
8675// Observe that we don't need to know exactly which one failed.
@@ -95,9 +84,7 @@ sel_register_read_error * (1 - sel_register_read_error) = 0;
9584pol BATCHED_TAGS_DIFF_REG = sel_tag_check_reg[0] * 2**0 * (mem_tag_reg[0] - expected_tag_reg[0])
9685 + sel_tag_check_reg[1] * 2**3 * (mem_tag_reg[1] - expected_tag_reg[1])
9786 + sel_tag_check_reg[2] * 2**6 * (mem_tag_reg[2] - expected_tag_reg[2])
98- + sel_tag_check_reg[3] * 2**9 * (mem_tag_reg[3] - expected_tag_reg[3])
99- + sel_tag_check_reg[4] * 2**12 * (mem_tag_reg[4] - expected_tag_reg[4])
100- + sel_tag_check_reg[5] * 2**15 * (mem_tag_reg[5] - expected_tag_reg[5]);
87+ + sel_tag_check_reg[3] * 2**9 * (mem_tag_reg[3] - expected_tag_reg[3]);
10188pol commit batched_tags_diff_inv_reg;
10289pol BATCHED_TAGS_DIFF_X_REG = sel_read_registers * BATCHED_TAGS_DIFF_REG; // Forces 0 if we don't read the register.
10390pol BATCHED_TAGS_DIFF_Y_REG = batched_tags_diff_inv_reg;
0 commit comments