Skip to content
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
18 changes: 18 additions & 0 deletions constraints/ace.air
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
29 changes: 29 additions & 0 deletions constraints/hasher.air
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}

##########################################################################################
Expand Down
12 changes: 10 additions & 2 deletions constraints/utils.air
Original file line number Diff line number Diff line change
Expand Up @@ -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
Loading