diff --git a/constraints/ace.air b/constraints/ace.air index 0f1fb3026..eaaf466a9 100644 --- a/constraints/ace.air +++ b/constraints/ace.air @@ -118,6 +118,24 @@ ev ace_chiplet_constraints_all_rows([s3, ace[16]]) { # Remove ACE INIT response when a section starts bus_6_chiplets_bus.remove(ACEINIT, ctx, ptr, clk, nread, n_eval) when sstart; + + #################################################################################### + # BUS REQUESTS - ACE MEMORY ACCESS + #################################################################################### + # ACE requests memory via virtual table (memory responds via bus_6_chiplets_bus). + # + # READ: word-aligned read (MEMREADWORD, ctx, ptr, clk, v0_0, v0_1, v1_0, v1_1) + # EVAL: encoded instruction (MEMREADELEMENT, ctx, ptr, clk, instruction) + # where instruction = id1 + id2 * 2^30 + (op + 1) * 2^60 + #################################################################################### + + let is_read_block = binary_not(sblock); + let is_eval_block = sblock; + + bus_5_v_table.remove(MEMREADWORD, ctx, ptr, clk, v0_0, v0_1, v1_0, v1_1) when is_read_block; + + let instruction = id1 + id2 * ACEINSTRUCTIONIDONEOFFSET + (op + 1) * ACEINSTRUCTIONIDTWOOFFSET; + bus_5_v_table.remove(MEMREADELEMENT, ctx, ptr, clk, instruction) when is_eval_block; } # Enforces that on the first row of ACE chiplet we should have sstart' = 1 diff --git a/constraints/hasher.air b/constraints/hasher.air index 2406ff66a..aaf364438 100644 --- a/constraints/hasher.air +++ b/constraints/hasher.air @@ -147,6 +147,35 @@ ev hash_chiplet([s[3], h[12], i, system_clk]) { # MU: Merkle root update (new path) - send leaf value based on bit b bus_6_chiplets_bus.remove(HASHERMRUPDATENEW, system_clk + 1, i, 0, 0, 0, 0, h4, h5, h6, h7, 0, 0, 0, 0) when f_mu * is_b_zero; bus_6_chiplets_bus.remove(HASHERMRUPDATENEW, system_clk + 1, i, 0, 0, 0, 0, 0, 0, 0, 0, h8, h9, h10, h11) when f_mu * is_b_one; + + #################################################################################### + # VIRTUAL TABLE SIBLING SHARING + #################################################################################### + # The virtual table ensures identical sibling nodes are used when verifying both + # old and new Merkle paths during root updates: + # - MV (old path): INSERT siblings into virtual table + # - MU (new path): REMOVE siblings from virtual table (must match insertions) + # + # Sibling location based on LSB of node index (bit b): + # - b=0: sibling in h[8..11] | b=1: sibling in h[4..7] + # + # Message format: (node_index, sibling[0..3]) + #################################################################################### + + let f_mva = get_f_mva(s); + let f_mua = get_f_mua(s); + + # MV: INSERT siblings during OLD path verification (cycle_row_0 and cycle_row_7) + bus_5_v_table.insert(i, h8, h9, h10, h11) when f_mv * is_b_zero; + bus_5_v_table.insert(i, h4, h5, h6, h7) when f_mv * is_b_one; + bus_5_v_table.insert(i, h8', h9', h10', h11') when f_mva * is_b_zero; + bus_5_v_table.insert(i, h4', h5', h6', h7') when f_mva * is_b_one; + + # MU: REMOVE siblings during NEW path verification (cycle_row_0 and cycle_row_7) + bus_5_v_table.remove(i, h8, h9, h10, h11) when f_mu * is_b_zero; + bus_5_v_table.remove(i, h4, h5, h6, h7) when f_mu * is_b_one; + bus_5_v_table.remove(i, h8', h9', h10', h11') when f_mua * is_b_zero; + bus_5_v_table.remove(i, h4', h5', h6', h7') when f_mua * is_b_one; } ########################################################################################## diff --git a/constraints/utils.air b/constraints/utils.air index 4ca9df3e8..79be1121f 100644 --- a/constraints/utils.air +++ b/constraints/utils.air @@ -167,9 +167,17 @@ const MEMREADELEMENT = 12; # Element read operation (1 element) const MEMWRITEWORD = 20; # Word write operation (4 elements) const MEMREADWORD = 28; # Word read operation (4 elements) -# ACE Chiplet Operation Labels (uses bus_7_wiring_bus, not bus_6_chiplets_bus) -const ACEINIT = 8; # ACE circuit initialization +# ACE Chiplet Operation Labels +const ACEINIT = 8; # ACE circuit initialization (uses bus_6_chiplets_bus) # Kernel ROM Chiplet Operation Labels const KERNELPROCCALL = 16; # Kernel procedure call const KERNELPROCINIT = 48; # Kernel procedure initialization + +########################################################################################## +# GENERAL CONSTANTS +########################################################################################## + +# ACE instruction encoding offsets +const ACEINSTRUCTIONIDONEOFFSET = 1073741824; # 2^30 +const ACEINSTRUCTIONIDTWOOFFSET = 1152921504606846976; # 2^60