diff --git a/constraints/ace.air b/constraints/ace.air index f822adbb3..0f1fb3026 100644 --- a/constraints/ace.air +++ b/constraints/ace.air @@ -75,7 +75,11 @@ ev ace_chiplet_constraints_all_rows([s3, ace[16]]) { let flag_ace_next = flag_ace_current_and_next(s3'); let flag_ace_last = flag_ace_last(s3'); - + + #################################################################################### + # TRANSITION CONSTRAINTS + #################################################################################### + # Section and block flags constraints enf section_block_flags_constraints([s3, sstart, sstart', sblock, id0, n_eval]); @@ -91,10 +95,33 @@ ev ace_chiplet_constraints_all_rows([s3, ace[16]]) { # Finalization constraints let f_end = binary_or(binary_and(flag_ace_next, sstart'), flag_ace_last); enf finalization_constraints([id0, v0_0, v0_1]) when f_end; + + #################################################################################### + # BUS RESPONSE - ACE INITIALIZATION + #################################################################################### + # The ACE chiplet provides a response to the decoder's ACE_INIT request via the + # chiplets bus. The response is sent when a new section starts (sstart = 1). + # + # Message format: (ACE_INIT, ctx, ptr, clk, nread, neval) + # where: + # - ctx, clk: Memory access context and clock cycle + # - ptr: Word-aligned pointer to first input variable + # - nread: Total count of input and constant elements (computed as id0 + 1 - neval) + # - neval: Total number of arithmetic operations + # + # Note: Since id0 = nread + neval - 1 in the first row, we have nread = id0 - neval + 1 + #################################################################################### + + # Compute nread from id0 and n_eval + # Since id0 = nread + neval - 1 in first row, then: nread = id0 - neval + 1 + let nread = id0 + 1 - n_eval; + + # Remove ACE INIT response when a section starts + bus_6_chiplets_bus.remove(ACEINIT, ctx, ptr, clk, nread, n_eval) when sstart; } # Enforces that on the first row of ACE chiplet we should have sstart' = 1 -ev ace_chiplet_constraints_first_row([ace[16]]) { +ev ace_chiplet_constraints_first_row([s3, ace[16]]) { let sstart = ace[0]; # Section start flag enf sstart' = 1; @@ -145,10 +172,7 @@ ev section_block_flags_constraints([s3, sstart, sstart_next, sblock, id0, n_eval # Sections must end with EVAL blocks (not READ) enf f_read = 0 when f_end; - # In a READ block, n_eval stays constant. - # When transitioning to an EVAL block, the next id0 must equal n_eval - 1. - # This ensures proper sequencing: READ loads nodes with IDs, EVAL starts processing - # from the highest loaded node ID (n_eval - 1). + # READ→EVAL transition occurs when n_eval matches id0+1 enf select(f_read_next, n_eval', id0' + 1) = n_eval when f_read; } @@ -167,9 +191,6 @@ ev enforce_binary_columns([sstart, sblock]) { # - Context (ctx) and clock (clk) remain constant within a section # - Memory pointer (ptr) increments with fixed increments: +4 in READ, +1 in EVAL # - Node identifiers (id0) decrement with fixed decrements: -2 in READ, -1 in EVAL -# -# Note: These constraints are active when the next row is NOT the start of a new section, -# i.e., all but the last rows of the section (intra-section transitions only). ev section_constraints([sstart, sblock, ctx, ptr, clk, id0]) { let flag_within_section = binary_not(sstart'); let flag_read = !sblock; @@ -181,10 +202,10 @@ ev section_constraints([sstart, sblock, ctx, ptr, clk, id0]) { # Clock consistency within a section enf clk' = clk when flag_within_section; - # Memory pointer increases by 4 in READ blocks and by 1 in EVAL blocks + # Memory pointer must decrease by 4 in READ blocks and by 1 in EVAL blocks enf ptr' = ptr + 4 * flag_read + flag_eval when flag_within_section; - # Node identifiers decrease by 2 in READ blocks and by 1 in EVAL blocks + # Node identifiers decreases by 2 in READ blocks and by 1 in EVAL blocks enf id0 = id0' + 2 * flag_read + flag_eval when flag_within_section; } @@ -310,4 +331,4 @@ fn block_flags(s_block: felt) -> felt[2] { let f_eval = s_block; return [f_read, f_eval]; -} \ No newline at end of file +} diff --git a/constraints/bitwise.air b/constraints/bitwise.air index 78efb50a6..ce4db600e 100644 --- a/constraints/bitwise.air +++ b/constraints/bitwise.air @@ -8,7 +8,7 @@ # # Each bitwise operation spans exactly 8 rows, with limbs processed in little-endian order. # -# STATUS: Partially implemented (missing bus constraints) +# STATUS: Fully implemented (core constraints + bus responses complete) # # REFERENCES: # - Bitwise Chiplet: https://0xmiden.github.io/miden-vm/design/chiplets/bitwise.html @@ -41,9 +41,38 @@ periodic_columns { # # Max constraint degree: 4 ev bitwise_chiplet_constraints([op_flag, a, b, a_limb[4], b_limb[4], zp, z]) { + #################################################################################### + # TRANSITION CONSTRAINTS + #################################################################################### + enf bitwise_op_flag([op_flag]); enf input_decomposition([a, b, a_limb, b_limb]); enf output_aggregation([op_flag, a, b, a_limb, b_limb, zp, z]); + + #################################################################################### + # BUS OPERATIONS - CHIPLETS COMMUNICATION + #################################################################################### + # The bitwise chiplet provides responses to bitwise operation requests via the + # chiplets bus. Each operation spans 8 rows, and the response is removed on the + # LAST row of the cycle (when k_transition = 0). + # + # OPERATIONS: + # - BITWISEAND (label = 2): AND operation (op_flag = 0) + # - BITWISEXOR (label = 6): XOR operation (op_flag = 1) + # + # Response format: (operation_label, a, b, z) + # where a, b are 32-bit operands and z is the result. + #################################################################################### + + # Compute operation flags + let is_and = binary_not(op_flag); + let is_xor = op_flag; + + # Remove bus responses on the last row of the 8-row cycle + let is_last_row = binary_not(k_transition); + + bus_6_chiplets_bus.remove(BITWISEAND, a, b, z) when (is_and * is_last_row); + bus_6_chiplets_bus.remove(BITWISEXOR, a, b, z) when (is_xor * is_last_row); } ########################################################################################## diff --git a/constraints/chiplets.air b/constraints/chiplets.air index 37d6a6b9b..7de790cda 100644 --- a/constraints/chiplets.air +++ b/constraints/chiplets.air @@ -44,7 +44,7 @@ use utils::*; # CHIPLETS CONSTRAINTS ########################################################################################## -ev chiplets_constraints([chiplets[20]]) { +ev chiplets_constraints([chiplets[20], system_clk]) { # Chiplets' flag constraints let s0 = chiplets[0]; let s1 = chiplets[1]; @@ -68,7 +68,7 @@ ev chiplets_constraints([chiplets[20]]) { # Apply chiplet-specific constraints based on hierarchical selector state. enf match { - case hash_active: hash_chiplet([chiplets[1..17]]), + case hash_active: hash_chiplet([chiplets[0..16], system_clk]), case bitwise_active: bitwise_chiplet_constraints([chiplets[2..15]]), case memory_active: memory_chiplet_constraints_all_rows([chiplets[3..18]]), case ace_active: ace_chiplet_constraints_all_rows([chiplets[3..20]]), @@ -96,7 +96,7 @@ ev chiplets_constraints([chiplets[20]]) { ### Apply ACE chiplet initialization constraints at the transition point let next_row_first_ace = binary_and(memory_active, s2'); # Transitioning into ACE chiplet - enf ace_chiplet_constraints_first_row([chiplets[4..20]]) when next_row_first_ace; + enf ace_chiplet_constraints_first_row([chiplets[3..20]]) when next_row_first_ace; ## KERNEL ROM diff --git a/constraints/decoder.air b/constraints/decoder.air index 66a237c3d..85fdf5e07 100644 --- a/constraints/decoder.air +++ b/constraints/decoder.air @@ -40,9 +40,11 @@ use utils::*; ########################################################################################## # Main decoder constraint evaluator -# Note: Decoder needs access to stack top (s0) for general constraints -ev decoder([addr, b0, b1, b2, b3, b4, b5, b6, h0, h1, h2, h3, h4, h5, h6, h7, sp, gc, ox, c0, c1, c2, e0, e1, s0]) { - # DECODING +# Note: Decoder needs access to stack top (s0-s2) for operation constraints and general constraints, and system clk/ctx for bus operations +ev decoder([addr, b0, b1, b2, b3, b4, b5, b6, h0, h1, h2, h3, h4, h5, h6, h7, sp, gc, ox, c0, c1, c2, e0, e1, s0, s1, s2, system_clk, system_ctx]) { + #################################################################################### + # TRANSITION CONSTRAINTS + #################################################################################### # GENERAL DECODER CONSTRAINTS enf general_constraints([b0, b1, b2, b3, b4, b5, b6, e0, e1, h0, h1, h2, h3, h4, h5, h6, h7, addr, sp, s0]); @@ -53,19 +55,63 @@ ev decoder([addr, b0, b1, b2, b3, b4, b5, b6, h0, h1, h2, h3, h4, h5, h6, h7, sp # OPERATION BATCH FLAGS CONSTRAINTS enf op_batch_flags_constraints([b0, b1, b2, b3, b4, b5, b6, e0, e1, h0, h1, h2, h3, h4, h5, h6, h7, c0, c1, c2]); - # OP FLAGS BITS - - # U32 OPERATIONS BIT CONSTRAINTS - # Force b0 = 0 for all u32 operations (100_xxx0 pattern) + # OP FLAGS BITS CONSTRAINTS enf u32_bit_constraints([b0, b1, b2, b3, b4, b5, b6]); - - # HIGH-DEGREE OPERATIONS BIT CONSTRAINTS - # Define degree reduction: e0 = b6 * (1-b5) * b4 for 101-prefix group enf high_degree_bit_constraints([b0, b1, b2, b3, b4, b5, b6, e0]); - - # VERY HIGH-DEGREE OPERATIONS BIT CONSTRAINTS - # Define degree reduction and force last 2 bits to be 0 for 11-prefix groups enf very_high_degree_bit_constraints([b0, b1, b2, b3, b4, b5, b6, e1]); + + #################################################################################### + # BUS OPERATIONS - CHIPLETS COMMUNICATION + #################################################################################### + + # Compute operation flags once for all bus operations + let fdyn = flag_dyn([b0, b1, b2, b3, b4, b5, b6], e0); + let fdyncall = flag_dyncall([b0, b1, b2, b3, b4, b5, b6], e0); + let fsyscall = flag_syscall([b0, b1, b2, b3, b4, b5, b6], e1); + let fevalcircuit = flag_evalcircuit([b0, b1, b2, b3, b4, b5, b6], e0); + let fspan = flag_span([b0, b1, b2, b3, b4, b5, b6], e0); + let frespan = flag_respan([b0, b1, b2, b3, b4, b5, b6], e1); + let fend = flag_end([b0, b1, b2, b3, b4, b5, b6], e1); + let fjoin = flag_join([b0, b1, b2, b3, b4, b5, b6], e0); + let fsplit = flag_split([b0, b1, b2, b3, b4, b5, b6], e0); + let floop = flag_loop([b0, b1, b2, b3, b4, b5, b6], e0); + let fcall = flag_call([b0, b1, b2, b3, b4, b5, b6], e1); + + # Opcode value for domain separation: d = Σ(bi·2^i) + let opcode = b0 + 2 * b1 + 4 * b2 + 8 * b3 + 16 * b4 + 32 * b5 + 64 * b6; + + # Memory operations: DYN/DYNCALL read target hash from memory + # The callee hash is read into h0'-h3' for bookkeeping, but the hash computation + # itself operates on [ZERO; 8] to compute the block hash + bus_6_chiplets_bus.insert(MEMREADWORD, system_ctx, s0, system_clk, h0', h1', h2', h3') when (fdyn + fdyncall); + bus_6_chiplets_bus.insert(HASHERLINEARHASH, addr', 0, 0, 0, 0, 0, 0, 0, 0) when (fdyn + fdyncall); + + # Kernel ROM: SYSCALL validates kernel procedure and computes block hash + # SYSCALL hashes: hash_control_block(kernel_proc_hash, EMPTY_WORD, domain, digest) + # The kernel procedure hash is in h0-h3, second child is zeros (no second child) + bus_6_chiplets_bus.insert(KERNELPROCCALL, h0, h1, h2, h3) when fsyscall; + bus_6_chiplets_bus.insert(HASHERLINEARHASH, addr', h0, h1, h2, h3, 0, 0, 0, 0, opcode) when fsyscall; + + # ACE chiplet: EVALCIRCUIT initializes arithmetic circuit evaluation + # Stack layout for EVALCIRCUIT: [ptr, nread, neval, ...] + # Message format: (ACE_INIT, ctx, ptr, clk, nread, neval) + let ace_ptr = s0; # Memory pointer to first input variable (word-aligned) + let ace_nread = s1; # Number of input and constant elements + let ace_neval = s2; # Number of arithmetic operations + bus_6_chiplets_bus.insert(ACEINIT, system_ctx, ace_ptr, system_clk, ace_nread, ace_neval) when fevalcircuit; + + # Basic block hashing: SPAN/RESPAN/END operations + bus_6_chiplets_bus.insert(HASHERLINEARHASH, addr', h0, h1, h2, h3, h4, h5, h6, h7) when fspan; + bus_6_chiplets_bus.insert(HASHERLINEARHASH, addr', h0, h1, h2, h3, h4, h5, h6, h7) when frespan; + bus_6_chiplets_bus.insert(HASHERRETURNHASH, addr + 7, h0', h1', h2', h3') when fend; + + # Control flow with opcode domain separation: JOIN/SPLIT/LOOP/CALL + # JOIN/SPLIT hash two children: hash_control_block(child1, child2, domain, digest) + bus_6_chiplets_bus.insert(HASHERLINEARHASH, addr', h0, h1, h2, h3, h4, h5, h6, h7, opcode) when fjoin; + bus_6_chiplets_bus.insert(HASHERLINEARHASH, addr', h0, h1, h2, h3, h4, h5, h6, h7, opcode) when fsplit; + # LOOP/CALL hash one child + zeros: hash_control_block(child, EMPTY_WORD, domain, digest) + bus_6_chiplets_bus.insert(HASHERLINEARHASH, addr', h0, h1, h2, h3, 0, 0, 0, 0, opcode) when floop; + bus_6_chiplets_bus.insert(HASHERLINEARHASH, addr', h0, h1, h2, h3, 0, 0, 0, 0, opcode) when fcall; } ########################################################################################## diff --git a/constraints/hasher.air b/constraints/hasher.air index 5d92137f4..11272b1a2 100644 --- a/constraints/hasher.air +++ b/constraints/hasher.air @@ -10,7 +10,7 @@ # 4. Merkle path verification. # 5. Merkle root update. # -# STATUS: Partially implemented (missing bus interactions) +# STATUS: Fully implemented (includes bus interactions) # # REFERENCES: # - Hasher chiplet design: https://0xmiden.github.io/miden-vm/design/chiplets/hasher.html @@ -26,7 +26,15 @@ use rpo::enforce_rpo_round; ########################################################################################## # Enforces the constraints on the hash chiplet given its columns. -ev hash_chiplet([s[3], h[12], i]) { +# +# NOTE: system_clk parameter is required for proper bus message timing. +# The hasher chiplet needs the system clock to construct bus messages that match +# the requests from the decoder/stack components. +ev hash_chiplet([s[3], h[12], i, system_clk]) { + #################################################################################### + # TRANSITION CONSTRAINTS + #################################################################################### + # Selector columns constraints enf selector_columns([s]); @@ -35,6 +43,110 @@ ev hash_chiplet([s[3], h[12], i]) { # Hasher state constraints enf hasher_state([s, h, i]); + + #################################################################################### + # BUS OPERATIONS + #################################################################################### + # The hasher chiplet provides responses to hash operation requests via the chiplets + # bus. All bus messages are sent on row 7 of the 8-row cycle (cycle_row_7 = 1). + # + # OPERATIONS: + # - HASHERLINEARHASH (label = 3): BP/ABP operations + # * BP: Begin permutation (cycle_row_0, sends all 12 state elements) + # * ABP: Absorb for linear hash (cycle_row_7, sends 8 newly absorbed elements in overwrite-mode) + # - HASHERRETURNHASH (label = 1): Hash output (4-element digest) + # - HASHERRETURNSTATE (label = 9): State output (all 12 elements) + # - HASHERMPVERIFY (label = 11): Merkle path verification + # - HASHERMRUPDATEOLD (label = 7): Merkle root update (old path) + # - HASHERMRUPDATENEW (label = 15): Merkle root update (new path) + # + # Note: MPA/MVA/MUA (Merkle absorb) operations do not send bus messages + #################################################################################### + + # Destructure hasher state array into individual elements due to some limitations in bus syntax + let h0 = h[0]; + let h1 = h[1]; + let h2 = h[2]; + let h3 = h[3]; + let h4 = h[4]; + let h5 = h[5]; + let h6 = h[6]; + let h7 = h[7]; + let h8 = h[8]; + let h9 = h[9]; + let h10 = h[10]; + let h11 = h[11]; + + # BP: Begin Permutation operation + # Initiates single permutation, 2-to-1 hash, or linear hash computation + # Flag: f_bp = (1,0,0) on cycle_row_0 + # Message format: (operation_label, clk+1, node_index, h0, h1, h2, h3, h4, h5, h6, h7, h8, h9, h10, h11) + # Sends the entire hasher state (all 12 elements) + let f_bp = get_f_bp(s, cycle_row_0); + bus_6_chiplets_bus.remove(HASHERLINEARHASH, system_clk + 1, i, h0, h1, h2, h3, h4, h5, h6, h7, h8, h9, h10, h11) when f_bp; + + # ABP: Absorb for linear hash operation + # Absorbs new elements into hasher state during linear hash computation + # Flag: f_abp = (1,0,0) on cycle_row_7 + # Message format: (operation_label, clk+1, node_index, 0,0,0,0, h4', h5', h6', h7', h8', h9', h10', h11') + # Sends the newly absorbed 8 elements (overwrite-mode, not add-mode) + # The capacity portion (h[0..4]) is preserved unchanged via transition constraints + let f_abp = get_f_abp(s, cycle_row_7); + bus_6_chiplets_bus.remove(HASHERLINEARHASH, system_clk + 1, i, 0, 0, 0, 0, h4', h5', h6', h7', h8', h9', h10', h11') when f_abp; + + # HOUT: Hash Output operation + # Returns the 4-element hash result (h4, h5, h6, h7) + # Flag: f_hout = (0,0,0) on cycle_row_7 + # Message format: (operation_label, clk+1, node_index, 0,0,0,0, h4, h5, h6, h7, 0,0,0,0) + let f_hout = get_f_hout(s, cycle_row_7); + bus_6_chiplets_bus.remove(HASHERRETURNHASH, system_clk + 1, i, 0, 0, 0, 0, h4, h5, h6, h7, 0, 0, 0, 0) when f_hout; + + # SOUT: State Output operation + # Returns the entire 12-element hasher state + # Flag: f_sout = (0,0,1) on cycle_row_7 + # Message format: (operation_label, clk+1, node_index, h0, h1, h2, h3, h4, h5, h6, h7, h8, h9, h10, h11) + let f_sout = get_f_sout(s, cycle_row_7); + bus_6_chiplets_bus.remove(HASHERRETURNSTATE, system_clk + 1, i, h0, h1, h2, h3, h4, h5, h6, h7, h8, h9, h10, h11) when f_sout; + + # MP, MV, MU: Merkle Path verification operations + # These operations return the leaf value selected based on bit b (LSB of node index). + # The leaf is either from h[4..8] (when b=0) or h[8..12] (when b=1). + # + # Message format per documentation: vleaf = vh + (1-b)·vb + b·vd + # where: + # vh = header with (operation_label, row_addr, node_index) + # vb = (h4, h5, h6, h7) - second word of hasher state + # vd = (h8, h9, h10, h11) - third word (using same alphas as vb) + # + # Flags: f_mp = (1,0,1), f_mv = (1,1,0), f_mu = (1,1,1) on cycle_row_0 + # + # Reference: https://0xmiden.github.io/miden-vm/design/chiplets/hasher.html#chiplets-bus-constraints + + let f_mp = get_f_mp(s, cycle_row_0); + let f_mv = get_f_mv(s, cycle_row_0); + let f_mu = get_f_mu(s, cycle_row_0); + + # Compute bit b (LSB of node index) = i - 2*i' + # This is the bit shifted out when dividing node index by 2 + let b = i - 2 * i'; + + # Selector flags for leaf position + let is_b_zero = binary_not(b); # When b=0, leaf is in h[4..8] + let is_b_one = b; # When b=1, leaf is in h[8..12] + + # MP: Merkle Path verification - send leaf value based on bit b + # When b=0: send (clk+1, node_index, 0,0,0,0, h4,h5,h6,h7, 0,0,0,0) + # When b=1: send (clk+1, node_index, 0,0,0,0, 0,0,0,0, h8,h9,h10,h11) + bus_6_chiplets_bus.remove(HASHERMPVERIFY, system_clk + 1, i, 0, 0, 0, 0, h4, h5, h6, h7, 0, 0, 0, 0) when f_mp * is_b_zero; + bus_6_chiplets_bus.remove(HASHERMPVERIFY, system_clk + 1, i, 0, 0, 0, 0, 0, 0, 0, 0, h8, h9, h10, h11) when f_mp * is_b_one; + + # MV: Merkle root update (old path) - send leaf value based on bit b + bus_6_chiplets_bus.remove(HASHERMRUPDATEOLD, system_clk + 1, i, 0, 0, 0, 0, h4, h5, h6, h7, 0, 0, 0, 0) when f_mv * is_b_zero; + bus_6_chiplets_bus.remove(HASHERMRUPDATEOLD, system_clk + 1, i, 0, 0, 0, 0, 0, 0, 0, 0, h8, h9, h10, h11) when f_mv * is_b_one; + + # 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; } ########################################################################################## @@ -114,27 +226,31 @@ ev hasher_state([s[3], h[12], i]) { enf enforce_rpo_round([h]) when !cycle_row_7; # Compute relevant flags (passing periodic column values as parameters) - let f_mp = get_f_mp(s, cycle_row_0); - let f_mv = get_f_mv(s, cycle_row_0); - let f_mu = get_f_mu(s, cycle_row_0); + let f_mpa = get_f_mpa(s, cycle_row_7); + let f_mva = get_f_mva(s, cycle_row_7); + let f_mua = get_f_mua(s, cycle_row_7); let f_abp = get_f_abp(s, cycle_row_7); - # Flag that is true when the performed operation includes absorbing the next node during Merkle - # path computation. - let f_absorb_node = f_mp + f_mv + f_mu; + # Flag that is true when absorbing the next node during Merkle path computation on cycle_row_7. + # NOTE: We use f_mpa/f_mva/f_mua (absorption flags) NOT f_mp/f_mv/f_mu (initialization flags) + # because these constraints apply on the last row of the cycle (cycle_row_7). + let f_absorb_node = f_mpa + f_mva + f_mua; # b is the value of the bit which is discarded during shift by one bit to the right. let b = i - 2 * i'; - # Enforce that when absorbing the next set of elements into the state during linear hash - # computation (i.e. f_abp = 1) the first 4 elements (the capacity portion) are carried over to - # the next row. - enf f_abp * (h' - h) = 0 for h in h; + # Enforce that when absorbing the next set of elements during linear hash computation on cycle_row_7 + # (i.e. f_abp = 1), the first 4 elements (the capacity portion) are carried over to the next row. + # This implements overwrite-mode where only the rate portion (h[4..12]) is overwritten. + enf h[0]' - h[0] = 0 when f_abp; + enf h[1]' - h[1] = 0 when f_abp; + enf h[2]' - h[2] = 0 when f_abp; + enf h[3]' - h[3] = 0 when f_abp; - # TODO: Double check the following and fix both docs and VM if there is a typo + # FIXED: Changed from f_mp/f_mv/f_mu to f_mpa/f_mva/f_mua (correct absorption flags) # - # Enforce that when absorbing the next node during Merkle path computation - # (i.e. f_mp + f_mv + f_mu = 1), the result of the previous hash (h[4], ..., h[7]) are copied + # Enforce that when absorbing the next node during Merkle path computation on cycle_row_7 + # (i.e. f_mpa + f_mva + f_mua = 1), the result of the previous hash (h[4], ..., h[7]) are copied # over either to (h[4]', ..., h[7]') or to (h[8]', ..., h[11]') depending on the value of b. # # TODO: uncomment when computed indices are supported @@ -183,6 +299,12 @@ ev hasher_state([s[3], h[12], i]) { # ########################################################################################## +# f_bp: Begin Permutation flag (1,0,0) on cycle_row_0 +# Initiates single permutation, 2-to-1 hash, or linear hash computation. +fn get_f_bp(s: felt[3], row0: felt) -> felt { + return row0 & s[0] & binary_not(s[1]) & binary_not(s[2]); +} + # f_mp: Merkle Path verification flag (1,0,1) on cycle_row_0 # Initiates standard Merkle path verification computation. fn get_f_mp(s: felt[3], row0: felt) -> felt { @@ -244,6 +366,18 @@ fn get_f_out_next(s: felt[3], row6: felt, s0_next: felt, s1_next: felt) -> felt return row6 & binary_not(s0_next) & binary_not(s1_next); } +# f_hout: Hash Output flag (0,0,0) on cycle_row_7 +# Returns the 4-element hash result (h4-h7) +fn get_f_hout(s: felt[3], row7: felt) -> felt { + return row7 & binary_not(s[0]) & binary_not(s[1]) & binary_not(s[2]); +} + +# f_sout: State Output flag (0,0,1) on cycle_row_7 +# Returns the entire 12-element hasher state +fn get_f_sout(s: felt[3], row7: felt) -> felt { + return row7 & binary_not(s[0]) & binary_not(s[1]) & s[2]; +} + ########################################################################################## # PERIODIC COLUMNS ########################################################################################## diff --git a/constraints/kernel_rom.air b/constraints/kernel_rom.air index 49b83f463..b1275ee11 100644 --- a/constraints/kernel_rom.air +++ b/constraints/kernel_rom.air @@ -9,7 +9,7 @@ # The chiplet contains digest values for all kernel procedures and enforces contiguity # constraints to ensure proper execution tracking. # -# STATUS: Core constraints implemented, bus constraints not implemented +# STATUS: Fully implemented (core constraints + bus responses complete) # # REFERENCES: # - Kernel ROM Chiplet: https://0xmiden.github.io/miden-vm/design/chiplets/kernel_rom.html @@ -25,15 +25,44 @@ use utils::*; # Enforces the constraints on the kernel ROM chiplet given its columns. # -# Parameters: -# - s4: Chiplet selector flag -# - sfirst: Section first flag (1 = start of new digest block, 0 = continuation of a given block) -# - r[4]: Kernel procedure root/digest (4 field elements) -# # Max constraint degree: 3 ev ker_rom_chiplet_constraints([s4, sfirst, r[4]]) { + #################################################################################### + # TRANSITION CONSTRAINTS + #################################################################################### + enf kernel_rom_selector([sfirst]); enf kernel_rom_digest_contiguity([s4, sfirst, r]); + + #################################################################################### + # BUS OPERATIONS - CHIPLETS COMMUNICATION + #################################################################################### + # The kernel ROM chiplet provides responses to kernel procedure requests via the + # chiplets bus. + # + # OPERATIONS: + # - KERNELPROCINIT (label = 48): Initialization from verifier (sfirst = 1) + # Responds to public input kernel digests on first row of digest block + # + # - KERNELPROCCALL (label = 16): Procedure call from decoder (sfirst = 0) + # Responds to SYSCALL operations on subsequent rows + # + # Response format: (operation_label, r0, r1, r2, r3) + # where r0-r3 form the 4-element kernel procedure digest. + #################################################################################### + + # Extract digest elements + let r0 = r[0]; + let r1 = r[1]; + let r2 = r[2]; + let r3 = r[3]; + + # Compute operation flags + let is_init = sfirst; # 1 when sfirst = 1 (initialization) + let is_call = binary_not(sfirst); # 1 when sfirst = 0 (procedure call) + + bus_6_chiplets_bus.remove(KERNELPROCINIT, r0, r1, r2, r3) when is_init; + bus_6_chiplets_bus.remove(KERNELPROCCALL, r0, r1, r2, r3) when is_call; } # Enforces initialization constraints for the first row of kernel ROM chiplet execution. @@ -54,24 +83,32 @@ ev kernel_rom_chiplet_constraints_first_row([s4, sfirst, r[4]]) { # HELPERS ########################################################################################## +### Helper evaluators ############################################################################# + # Enforces that the kernel ROM selector is valid. # # Max constraint degree: 2 ev kernel_rom_selector([sfirst]) { - # Enforce that sfirst is binary (0 or 1) + # Enforce that sfirst is binary (0 or 1). + # Constraint degree: 2 enf is_binary([sfirst]); + + # First row initialization constraint + # This is part of the ACE chiplet constraints } # Enforces digest contiguity constraints for the kernel ROM. # -# When sfirst' = 0 (not starting a new digest block), the digest values must remain -# unchanged from the current row to the next row. This ensures contiguous blocks of -# identical digest values for proper tracking of kernel procedure executions. +# When sfirst' = 0, consecutive rows must contain identical digest values to ensure +# proper tracking of kernel procedure executions. # # Max constraint degree: 3 ev kernel_rom_digest_contiguity([s4, sfirst, r[4]]) { - # Constraint is active when: - # - sfirst' = 0 (next row is not the start of a new digest block) - # - s4' = 0 (next row is still within the kernel ROM chiplet) - enf is_unchanged([r_i]) for r_i in r when binary_and(binary_not(s4'), binary_not(sfirst')); + # Enforce that when sfirst = 0 (not the start of a new digest block), + # the digest values in the current row must be identical to the next row. + # This ensures contiguous blocks of identical digest values. + # + # Note: This constraint is disabled when the current row is the last row of the kernel ROM chiplet + # which is indicated by s4' being set to 1 + enf is_unchanged([r]) for r in r when binary_and(binary_not(s4'), binary_not(sfirst')); } diff --git a/constraints/memory.air b/constraints/memory.air index efb9579d4..2df2b58c5 100644 --- a/constraints/memory.air +++ b/constraints/memory.air @@ -7,22 +7,22 @@ # element access and optimized word-aligned batch operations (4 elements per word). # # MEMORY TABLE LAYOUT: -# ┌─────────────────┬────────────────────────────────────────────────────────────────┐ -# │ Column │ Purpose │ -# ├─────────────────┼────────────────────────────────────────────────────────────────┤ -# │ is_read │ Read/write selector: 1=read, 0=write │ -# │ is_word_access │ Element/word access selector: 0=element, 1=word │ -# │ ctx │ Context ID for execution context separation │ -# │ addr │ Memory address (word-aligned for word access) │ -# │ idx0/1 │ Element index within word [0,3] - binary decomposition │ -# │ clk │ Clock cycle when operation occurred │ -# │ v0-v3 │ Four field elements stored in memory word │ -# │ d0/d1 │ Delta tracking columns for monotonicity verification │ -# │ d_inv │ Inverse delta column for consecutive transitions │ -# │ f_scw │ Same context/word flag for sequential access optimization │ -# └─────────────────┴────────────────────────────────────────────────────────────────┘ +# ┌─────────┬──────────────────────────────────────────────────────────────────────────┐ +# │ Column │ Purpose │ +# ├─────────┼──────────────────────────────────────────────────────────────────────────┤ +# │ rw │ Read/write selector: 1=read, 0=write │ +# │ ew │ Element/word access selector: 0=element, 1=word │ +# │ ctx │ Context ID for execution context separation │ +# │ w_addr │ Word address (must be divisible by 4 for aligned access) │ +# │ idx0/1 │ Element index within word [0,3] - binary decomposition of low 2 bits │ +# │ clk │ Clock cycle when operation occurred │ +# │ v0-v3 │ Four field elements stored in memory word │ +# │ d0/d1 │ Delta tracking columns for monotonicity verification │ +# │ d_inv │ Inverse delta column for consecutive transitions │ +# │ f_scw │ Same context/word address flag for sequential access optimization │ +# └─────────┴──────────────────────────────────────────────────────────────────────────┘ # -# STATUS: Partially implemented (missing bus integration) +# STATUS: Fully implemented with chiplets bus integration # # REFERENCES: # - Memory Design: https://0xmiden.github.io/miden-vm/design/chiplets/memory.html @@ -33,7 +33,7 @@ mod memory use utils::*; ########################################################################################## -# MEMORY CHIPLET CONSTRAINTS +# MEMORY CHIPLET TRANSITION CONSTRAINTS ########################################################################################## # Enforces proper memory initialization when entering memory chiplet @@ -49,13 +49,31 @@ ev memory_chiplet_constraints_first_row([memory[15]]) { let v2 = memory[9]; # Memory value 2 let v3 = memory[10]; # Memory value 3 - let is_constrained_value = compute_element_access_flags(idx0', idx1', is_read', is_word_access'); + # Element selection flags: f[i] = 1 when element index (2*idx1 + idx0) equals i + let f0 = binary_not(idx1') * binary_not(idx0'); + let f1 = binary_not(idx1') * idx0'; + let f2 = idx1' * binary_not(idx0'); + let f3 = idx1' * idx0'; + + # c_i is set to 1 when `v'[i]` is not written to, and 0 otherwise. + # + # In other words, c_i is set to 1 when `v'[i]` needs to be constrained (to either 0 or `v[i]`). + # + # Note that `c_i` only uses values in the "next" row. This is because it must be used to + # constrain the first row of the memory chiplet, where that row sits in the "next" position of + # the frame, and the "current" row belongs to the previous chiplet (and hence the "current" row + # must not be accessed). + # + # As a result, `c_i` does not include the constraint of being in the memory chiplet, or in the + # same context and word - these must be enforced separately. + let f = [f0, f1, f2, f3]; + let c = [compute_c_i(f_i, is_read', is_word_access') for f_i in f]; # Enforce that when v'[i] is not written to, then v'[i] must be 0. - enf v0' = 0 when is_constrained_value[0]; - enf v1' = 0 when is_constrained_value[1]; - enf v2' = 0 when is_constrained_value[2]; - enf v3' = 0 when is_constrained_value[3]; + enf v0' = 0 when c[0]; + enf v1' = 0 when c[1]; + enf v2' = 0 when c[2]; + enf v3' = 0 when c[3]; } # Enforces constraints that apply to every row in the memory chiplet @@ -66,21 +84,12 @@ ev memory_chiplet_constraints_all_rows([memory[15]]) { let idx0 = memory[4]; # Element index bit 0 let idx1 = memory[5]; # Element index bit 1 - # Read/write selector must be binary - enf is_binary([is_read]); - - # Element/word access selector must be binary - enf is_binary([is_word_access]); - - # Index bit 0 must be binary - enf is_binary([idx0]); - - # Index bit 1 must be binary - enf is_binary([idx1]); + # Binary column constraints + enf enforce_binary_columns([is_read, is_word_access, idx0, idx1]); } # Enforces memory state transition constraints for all rows except the final row -# Includes monotonicity, value consistency, and proper read/write semantics +# Includes monotonicity, value consistency, proper read/write semantics, and bus interactions ev memory_chiplet_constraints_all_rows_except_last([memory[15]]) { let is_read = memory[0]; # Read(1)/Write(0) selector let is_word_access = memory[1]; # Element(0)/Word(1) access selector @@ -112,30 +121,79 @@ ev memory_chiplet_constraints_all_rows_except_last([memory[15]]) { # Memory value constraints enf enforce_values_consistency([is_read, is_word_access, idx0, idx1, v0, v1, v2, v3, f_scw]); + + #################################################################################### + # BUS OPERATIONS + #################################################################################### + # The memory chiplet provides responses to memory operation requests via the + # chiplets bus. + # + # OPERATIONS: + # - MEMREADWORD (label = 28): Read 4-element word from memory + # - MEMWRITEWORD (label = 20): Write 4-element word to memory + # - MEMREADELEMENT (label = 12): Read single element from memory + # - MEMWRITEELEMENT (label = 4): Write single element to memory + # + # All operations include context, address, and clock cycle + #################################################################################### + + # Compute operation flags + let is_word_read = is_read * is_word_access; + let is_word_write = binary_not(is_read) * is_word_access; + let is_element_read = is_read * binary_not(is_word_access); + let is_element_write = binary_not(is_read) * binary_not(is_word_access); + + # For element operations, compute which element is being accessed + let f0_bus = binary_not(idx1) * binary_not(idx0); + let f1_bus = binary_not(idx1) * idx0; + let f2_bus = idx1 * binary_not(idx0); + let f3_bus = idx1 * idx0; + let element_value = f0_bus * v0 + f1_bus * v1 + f2_bus * v2 + f3_bus * v3; + + # Remove responses from bus when operations occur + bus_6_chiplets_bus.remove(MEMREADWORD, ctx, addr, clk, v0, v1, v2, v3) when is_word_read; + bus_6_chiplets_bus.remove(MEMWRITEWORD, ctx, addr, clk, v0, v1, v2, v3) when is_word_write; + bus_6_chiplets_bus.remove(MEMREADELEMENT, ctx, addr, clk, element_value) when is_element_read; + bus_6_chiplets_bus.remove(MEMWRITEELEMENT, ctx, addr, clk, element_value) when is_element_write; } ########################################################################################## # HELPER EVALUATORS ########################################################################################## +# Constrains binary columns for selectors and indices +ev enforce_binary_columns([is_read, is_word_access, idx0, idx1]) { + # Read/write selector must be binary + enf is_binary([is_read]); + + # Element/word access selector must be binary + enf is_binary([is_word_access]); + + # Index bit 0 must be binary + enf is_binary([idx0]); + + # Index bit 1 must be binary + enf is_binary([idx1]); +} + # Constrains the delta inverse column ev enforce_d_inv([ctx, addr, clk, d0, d1, d_inv]) { let ctx_delta = ctx' - ctx; let addr_delta = addr' - addr; - let is_ctx_changed = ctx_delta * d_inv'; - let is_addr_changed = addr_delta * d_inv'; + let n0 = ctx_delta * d_inv'; + let n1 = addr_delta * d_inv'; - # is_ctx_changed is binary - enf binary_constraint(is_ctx_changed) = 0; + # n0 is binary + enf binary_constraint(n0) = 0; - # When context changes, is_ctx_changed must be 1 - enf ctx_delta = 0 when !is_ctx_changed; + # When context changes, n0 must be 1 + enf ctx_delta = 0 when binary_not(n0); - # When is_ctx_changed is 0 then is_addr_changed is binary - enf binary_constraint(is_addr_changed) = 0 when !is_ctx_changed; + # When n0 is 0 then n1 is binary + enf binary_constraint(n1) = 0 when binary_not(n0); - # When is_ctx_changed and is_addr_changed are both 0, then address must not change - enf addr_delta = 0 when binary_not(is_ctx_changed) * binary_not(is_addr_changed); + # When n0 and n1 are both 0, then address must not change + enf addr_delta = 0 when binary_not(n0) * binary_not(n1); } # Enforces monotonicity constraints for context, address, and clock transitions @@ -144,20 +202,20 @@ ev enforce_delta([ctx, addr, clk, d0, d1, d_inv]) { let addr_delta = addr' - addr; let clk_delta = clk' - clk; let delta_next = d1' * 2^16 + d0'; - let is_ctx_changed = ctx_delta * d_inv'; - let is_addr_changed = addr_delta * d_inv'; + let n0 = ctx_delta * d_inv'; + let n1 = addr_delta * d_inv'; - enf is_ctx_changed * ctx_delta + binary_not(is_ctx_changed) * (is_addr_changed * addr_delta + binary_not(is_addr_changed) * clk_delta) = delta_next; + enf n0 * ctx_delta + binary_not(n0) * (n1 * addr_delta + binary_not(n1) * clk_delta) = delta_next; } # Enforces correct f_scw flag computation ev enforce_flag_same_context_and_word([ctx, addr, d_inv, f_scw]) { let ctx_delta = ctx' - ctx; let addr_delta = addr' - addr; - let is_ctx_changed = ctx_delta * d_inv'; - let is_addr_changed = addr_delta * d_inv'; + let n0 = ctx_delta * d_inv'; + let n1 = addr_delta * d_inv'; - enf f_scw' = binary_not(is_ctx_changed) * binary_not(is_addr_changed); + enf f_scw' = binary_not(n0) * binary_not(n1); } # Enforces that accesses to same context, word address, and clock must be reads @@ -165,20 +223,38 @@ ev enforce_same_context_word_addr_and_clock([is_read, clk, f_scw, d_inv]) { let clk_delta = clk' - clk; let clk_no_change = binary_not(clk_delta * d_inv'); - enf f_scw' * clk_no_change * binary_not(is_read) * binary_not(is_read') = 0; + enf binary_not(is_read) * binary_not(is_read') = 0 when clk_no_change * f_scw'; } # Enforces memory value consistency, and proper read/write semantics ev enforce_values_consistency([is_read, is_word_access, idx0, idx1, v0, v1, v2, v3, f_scw]) { - let is_constrained_value = compute_element_access_flags(idx0', idx1', is_read', is_word_access'); + # Element selection flags: f[i] = 1 when element index (2*idx1 + idx0) equals i + let f0 = binary_not(idx1') * binary_not(idx0'); + let f1 = binary_not(idx1') * idx0'; + let f2 = idx1' * binary_not(idx0'); + let f3 = idx1' * idx0'; + + # c_i is set to 1 when `v'[i]` is not written to, and 0 otherwise. + # + # In other words, c_i is set to 1 when `v'[i]` needs to be constrained (to either 0 or `v[i]`). + # + # Note that `c_i` only uses values in the "next" row. This is because it must be used to + # constrain the first row of the memory chiplet, where that row sits in the "next" position of + # the frame, and the "current" row belongs to the previous chiplet (and hence the "current" row + # must not be accessed). + # + # As a result, `c_i` does not include the constraint of being in the memory chiplet, or in the + # same context and word - these must be enforced separately. + let f = [f0, f1, f2, f3]; + let c = [compute_c_i(f_i, is_read', is_word_access') for f_i in f]; # Non-first row constraints: if v[i]' is not written to and, # - (f_scw' = 1) then its value needs to be copied over from the previous row, # - (f_scw' = 0) then its value needs to be set to 0. - enf f_scw' * (v0' - v0) + binary_not(f_scw') * v0' = 0 when is_constrained_value[0]; - enf f_scw' * (v1' - v1) + binary_not(f_scw') * v1' = 0 when is_constrained_value[1]; - enf f_scw' * (v2' - v2) + binary_not(f_scw') * v2' = 0 when is_constrained_value[2]; - enf f_scw' * (v3' - v3) + binary_not(f_scw') * v3' = 0 when is_constrained_value[3]; + enf f_scw' * (v0' - v0) + binary_not(f_scw') * v0' = 0 when c[0]; + enf f_scw' * (v1' - v1) + binary_not(f_scw') * v1' = 0 when c[1]; + enf f_scw' * (v2' - v2) + binary_not(f_scw') * v2' = 0 when c[2]; + enf f_scw' * (v3' - v3) + binary_not(f_scw') * v3' = 0 when c[3]; } ########################################################################################## @@ -206,32 +282,8 @@ fn flag_next_row_first_row_memory(s0: felt, s1: felt, s2: felt) -> felt { } # Computes constraint flag: 1 if value needs to be constrained, 0 otherwise -fn compute_constrained_values(is_accessed_i: felt, is_read_next: felt, is_word_access_next: felt) -> felt { - let z_i = binary_not(is_word_access_next) * binary_not(is_accessed_i); +fn compute_c_i(f_i: felt, is_read_next: felt, is_word_access_next: felt) -> felt { + let z_i = binary_not(is_word_access_next) * binary_not(f_i); return is_read_next + binary_not(is_read_next) * z_i; } -# Computes which memory elements need to be constrained based on access pattern -# Returns array of 4 flags indicating whether each element (v0-v3) needs constraining -# -# is_constrainted_value_i is set to 1 when `v'[i]` is not written to, and 0 otherwise. -# -# In other words, is_constrainted_value_i is set to 1 when `v'[i]` needs to be constrained (to either 0 or `v[i]`). -# -# Note that `is_constrainted_value_i` only uses values in the "next" row. This is because it must be used to -# constrain the first row of the memory chiplet, where that row sits in the "next" position of -# the frame, and the "current" row belongs to the previous chiplet (and hence the "current" row -# must not be accessed). -# -# As a result, `is_constrainted_value_i` does not include the constraint of being in the memory chiplet, or in the -# same context and word - these must be enforced separately. -fn compute_element_access_flags(idx0_next: felt, idx1_next: felt, is_read_next: felt, is_word_access_next: felt) -> felt[4] { - # Element selection flags: is_accessed[i] = 1 when element index (2*idx1 + idx0) equals i - let is_accessed_0 = binary_not(idx1_next) * binary_not(idx0_next); - let is_accessed_1 = binary_not(idx1_next) * idx0_next; - let is_accessed_2 = idx1_next * binary_not(idx0_next); - let is_accessed_3 = idx1_next * idx0_next; - - let is_accessed = [is_accessed_0, is_accessed_1, is_accessed_2, is_accessed_3]; - return [compute_constrained_values(is_accessed_i, is_read_next, is_word_access_next) for is_accessed_i in is_accessed]; -} diff --git a/constraints/miden-vm/bitwise.air b/constraints/miden-vm/bitwise.air deleted file mode 100644 index 8c186367f..000000000 --- a/constraints/miden-vm/bitwise.air +++ /dev/null @@ -1,114 +0,0 @@ -mod BitwiseAir - -### Constants and periodic columns ################################################################ - -periodic_columns { - k0: [1, 0, 0, 0, 0, 0, 0, 0] - k1: [1, 1, 1, 1, 1, 1, 1, 0] -} - - -### Helper functions ############################################################################## - -# Returns value aggregated from limbs. -fn aggregate(limb: vector[4]) -> scalar: - return sum([2^i * a for (i, a) in (0..4, limb)]) - - -### Helper evaluators ############################################################################# - -# Enforces that column must be binary. -# -# Constraint degree: 2 -ev is_binary([a]) { - enf a^2 = a -} - - -# Enforces that the bitwise selector is valid. -# -# Max constraint degree: 2 -ev bitwise_selector([s]) { - # Enforce that selector must be binary. - # Constraint degree: 2 - enf is_binary([s]) - - # Enforce that selector should stay the same throughout the cycle. - # Constraint degree: 2 - enf s' = s when k1 -} - - -# Enforces that the input to the bitwise chiplet is decomposed into limbs correctly. -# -# Max constraint degree: 2 -ev input_decomposition([a, b, a_limb[4], b_limb[4]]) { - # Enforce that the input is decomposed into valid bits. - # Constraints degree: 2 - enf is_binary([a]) for a in a_limb - enf is_binary([b]) for b in b_limb - - # Enforce that the value in the first row of column `a` of the current 8-row cycle should be - # the aggregation of the decomposed bit columns `a_limb`. - let a_aggr = aggregate(a_limb) - # Constraint degree: 2 - enf a = a_aggr when k0 - - # Enforce that the value in the first row of column `b` of the current 8-row cycle should be - # the aggregation of the decomposed bit columns `b_limb`. - let b_aggr = aggregate(b_limb) - # Constraint degree: 2 - enf b = b_aggr when k0 - - # Enforce that for all rows in an 8-row cycle, except for the last one, the values in a and b - # columns are increased by the values contained in the individual bit columns a_limb and - # b_limb. - # Constraints degree: 2 - enf a' = a * 16 + a_aggr when k1 - enf b' = b * 16 + b_aggr when k1 -} - - -# Enforces that the output of the bitwise operation is aggregated correctly from the decomposed -# limbs. -# -# Max constraint degree: 3 -ev output_aggregation([s, a, b, a_limb[4], b_limb[4], zp, z]) { - # Enforce that in the first row, the aggregated output value of the previous row should be 0. - # Constraint degree: 2 - enf zp = 0 when k0 - - # Enforce that for each row except the last, the aggregated output value must equal the - # previous aggregated output value in the next row. - # Constraint degree: 2 - enf zp' = z when k1 - - # Enforce that for all rows the value in the z column is computed by multiplying the previous - # output value (from the zp column in the current row) by 16 and then adding it to the bitwise - # operation applied to the row's set of bits of a_limb and b_limb. The entire constraint must - # also be multiplied by the operation selector flag to ensure it is only applied for the - # appropriate operation. The constraint for AND is enforced when s = 0 and the constraint for - # XOR is enforced when s = 1. Because the selectors for the AND and XOR operations are mutually - # exclusive, the constraints for different operations can be aggregated into the same result - # indices. - # Constraints degree: 3 - let a_and_b = sum([2^i * a * b for (i, a, b) in (0..4, a_limb, b_limb)]) - let a_xor_b = sum([2^i * (a + b - 2 * a * b) for (i, a, b) in (0..4, a_limb, b_limb)]) - match enf: - z = zp * 16 + a_xor_b when s - z = zp * 16 + a_and_b when !s -} - - -### Bitwise Chiplet Air Constraints ############################################################### - -# Enforces the constraints on the bitwise chiplet, given the columns of the bitwise execution -# trace. -# -# Max constraint degree: 4 -ev bitwise_chiplet([s, a, b, a_limb[4], b_limb[4], zp, z]) { - enf bitwise_selector([s]) - enf input_decomposition([a, b, a_limb, b_limb]) - enf output_aggregation([s, a, b, a_limb, b_limb, zp, z]) - # Bus constraint is implemented in a separate file -} diff --git a/constraints/miden-vm/chiplets.air b/constraints/miden-vm/chiplets.air deleted file mode 100644 index 2cc397ed2..000000000 --- a/constraints/miden-vm/chiplets.air +++ /dev/null @@ -1,38 +0,0 @@ -mod ChipletsConstraintsAir - -use bitwise::bitwise_chiplet -use hash::hash_chiplet -use memory::memory_chiplet - -### Helper evaluators ############################################################################# - -# Enforces that the provided columns must be binary. -ev is_binary([a]) { - enf a^2 = a -} - -# Enforces that the chiplet selector columns are set correctly. -ev chiplet_selectors([s[3]]) { - # Enforce that selectors are binary. - enf is_binary([s[0]]) - enf is_binary([s[1]]) when s[0] - enf is_binary([s[2]]) when s[0] & s[1] - - # Enforce that the chiplets are stacked correctly by restricting selector values so they can - # only change from 0 to 1. - enf s[0]' = s[0] when s[0] - enf s[1]' = s[1] when s[0] & s[1] - enf s[2]' = s[2] when s[0] & s[1] & s[2] -} - -### Chiplets Constraints ########################################################################## - -# Enforce the constraints on the hash, bitwise or memory chiplet, given the columns of the chiplet -# module trace. -ev chiplets([s[3], chiplet_columns[15]]) { - enf chiplet_selectors([s]) - match enf: - hash_chiplet([s[1], s[2], chiplet_columns]) when !s[0] - bitwise_chiplet([s[2], chiplet_columns]) when s[0] & !s[1] - memory_chiplet([chiplet_columns]) when s[0] & s[1] & !s[2]' -} \ No newline at end of file diff --git a/constraints/miden-vm/decoder.air b/constraints/miden-vm/decoder.air deleted file mode 100644 index cdab70682..000000000 --- a/constraints/miden-vm/decoder.air +++ /dev/null @@ -1,654 +0,0 @@ -mod DecoderAir - -### Constants and periodic columns ################################################################ - -const HASHER_LINEAR_HASH = 3 -const HASHER_RETURN_HASH = 1 - -periodic_columns { - cycle_row_0: [1, 0, 0, 0, 0, 0, 0, 0] - cycle_row_7: [0, 0, 0, 0, 0, 0, 0, 1] -} - -### Helper functions ############################################################################## - -# Returns the f_join operation flag which is set when JOIN control operation is executed. -# -# Flag degree: 6 -fn get_f_join(b: vector[7]) -> scalar: - return b[6] & !b[5] & b[4] & b[3] & !b[2] & b[1] - - -# Returns the f_split operation flag which is set when SPLIT control operation is executed. -# -# Flag degree: 6 -fn get_f_split(b: vector[7]) -> scalar: - return b[6] & !b[5] & b[4] & b[3] & b[2] & !b[1] - - -# Returns the f_loop operation flag which is set when LOOP control operation is executed. -# -# Flag degree: 6 -fn get_f_loop(b: vector[7]) -> scalar: - return b[6] & !b[5] & b[4] & b[3] & b[2] & b[1] - - -# Returns the f_repeat operation flag which is set when REPEAT operation is executed. -# -# Flag degree: 4 -fn get_f_repeat(b: vector[7], extra: scalar) -> scalar: - return extra & b[4] & !b[3] & b[2] - - -# Returns the f_span operation flag which is set when SPAN operation is executed. -# -# Flag degree: 6 -fn get_f_span(b: vector[7]) -> scalar: - return b[6] & !b[5] & b[4] & b[3] & !b[2] & !b[1] - - -# Returns the f_respan operation flag which is set when RESPAN operation is executed. -# -# Flag degree: 4 -fn get_f_respan(b: vector[7], extra: scalar) -> scalar: - return extra & b[4] & b[3] & !b[2] - - -# Returns the f_call operation flag which is set when CALL control operation is executed. -# -# Flag degree: 4 -fn get_f_call(b: vector[7], extra: scalar) -> scalar: - return extra & !b[4] & b[3] & b[2] - - -# Returns the f_syscall operation flag which is set when SYSCALL control operation is executed. -# -# Flag degree: 4 -fn get_f_syscall(b: vector[7], extra: scalar) -> scalar: - return extra & !b[4] & b[3] & !b[2] - - -# Returns the f_end operation flag which is set when END operation is executed. -# -# Flag degree: 4 -fn get_f_end(b: vector[7], extra: scalar) -> scalar: - return extra & b[4] & !b[3] & !b[2] - - -# Returns the f_halt operation flag which is set when HALT operation is executed. -# -# Flag degree: 4 -fn get_f_halt(b: vector[7], extra: scalar) -> scalar: - return extra & b[4] & b[3] & b[2] - - -# Returns the f_push operation flag which is set when PUSH operation is executed. -# -# Flag degree: 4 -fn get_f_push(b: vector[7], extra: scalar) -> scalar: - return extra & !b[4] & !b[3] & b[2] - - -# Returns the f_ctrl flag which is set when any one of the control flow operations (JOIN, SPLIT, -# LOOP, REPEAT, SPAN, RESPAN, CALL, SYSCALL, END, HALT) is being executed. -# -# Flag degree: 4 -fn get_f_ctrl(b: vector[7], extra: scalar) -> scalar: - # flag for SPAN, JOIN, SPLIT, LOOP - let f_sjsl = b[6] & !b[5] & b[4] & b[3] - - # flag for END, REPEAT, RESPAN, HALT - let f_errh = b[6] & b[5] & b[4] - - return f_sjsl + f_errh + get_f_call(b, extra) + get_f_syscall(b, extra) - - -# Returns f_ctrli flag which is set to 1 when a control flow operation that signifies the -# initialization of a control block (JOIN, SPLIT, LOOP, CALL, SYSCALL) is being executed on the VM. -# -# Flag degree: 6 -fn get_f_ctrli(b: vector[7], extra: scalar) -> scalar: - return get_f_join(b) + get_f_split(b) + get_f_loop(b) + get_f_call(b, extra) + get_f_syscall(b, extra) - - -# Returns transition label, composed of the operation label and the periodic columns that uniquely -# identify each transition function. -fn get_transition_label(op_label: scalar) -> scalar: - return op_label + 2^4 * cycle_row_7 + 2^5 * cycle_row_0 - - -# Returns f_g8 flag which is set to 1 if there are 8 operation groups in the batch. -fn get_f_g8(op_batch_flags: vector[3]) -> scalar: - return op_batch_flags[0] - - -# Returns f_g4 flag which is set to 1 if there are 4 operation groups in the batch. -fn get_f_g4(op_batch_flags: vector[3]) -> scalar: - return !op_batch_flags[0] & op_batch_flags[1] & op_batch_flags[2] - - -# Returns f_g2 flag which is set to 1 if there are 2 operation groups in the batch. -fn get_f_g2(op_batch_flags: vector[3]) -> scalar: - return !op_batch_flags[0] & !op_batch_flags[1] & op_batch_flags[2] - - -# Returns f_g1 flag which is set to 1 if there are 1 operation groups in the batch. -fn get_f_g1(op_batch_flags: vector[3]) -> scalar: - return !op_batch_flags[0] & op_batch_flags[1] & !op_batch_flags[2] - - -### Helper evaluators ############################################################################# - -# Enforces that column must be binary. -# Constraint degree: 2 -ev is_binary([a]) { - enf a^2 = a -} - - -# Enforces that value in column is copied over to the next row. -# Constraint degree: 1 -ev is_unchanged([column]) { - enf column' = column -} - - -# Enforces decoder general constraints. -# -# Max constraint degree: 9 -ev general([addr, op_bits[7], hasher[8], in_span, s0, extra]) { - # Get flags required for the general constraints - let f_repeat = get_f_repeat(op_bits, extra) - let f_end = get_f_end(op_bits, extra) - let f_halt = get_f_halt(op_bits, extra) - - # Enforce that `extra` column is set to 1 when op_bits[6] = 1 and op_bits[5] = 1 - # Constraint degree: 3 - enf extra = 1 when op_bits[6] & op_bits[5] - - # Enforce that when SPLIT or LOOP operation is executed, the top of the operand stack must - # contain a binary value. - # Constraint degree: 8 - enf is_binary([s0]) when get_f_split(op_bits) | get_f_loop(op_bits) - - # Enforce that When REPEAT operation is executed, the value at the top of the operand stack - # must be 1. - # Constraint degree: 5 - enf s0 = 1 when f_repeat - - # Enforce that when REPEAT operation is executed, the value in hasher[4] column (the - # is_loop_body flag), must be set to 1. This ensures that REPEAT operation can be executed only - # inside a loop. - # Constraint degree: 5 - enf hasher[4] = 1 when f_repeat - - # Enforce that when RESPAN operation is executed, we need to make sure that the block ID is - # incremented by 8. - # Constraint degree: 5 - enf addr' = addr + 8 when f_respan(op_bits, extra) - - # Enforce that when END operation is executed and we are exiting a loop block (i.e., is_loop, - # value which is stored in hasher[5], is 1), the value at the top of the operand stack must be - # 0. - # Constraint degree: 6 - enf s0 = 0 when f_end & hasher[5] - - # Enforce that when END operation is executed and the next operation is REPEAT, values in - # hasher[0], ..., hasher[4] (the hash of the current block and the is_loop_body flag) must be - # copied to the next row. - # Constraint degree: 9 - enf is_unchanged([hasher[i]]) for i in 0..5 when f_end & get_f_repeat(op_bits', extra') - - # Enforce that a HALT instruction can be followed only by another HALT instruction. - # Constraint degree: 8 - enf f_halt * !get_f_halt(op_bits', extra') = 0 - - # Enforce that when a HALT operation is executed, block address column (addr) must be 0. - # Constraint degree: 5 - enf addr = 0 when f_halt - - # Enforce that values in op_bits columns must be binary. - # Constraint degree: 2 - enf is_binary([b]) for b in op_bits - - # Enforce that when the value in in_span column is set to 1, control flow operations cannot be - # executed on the VM, but when in_span flag is 0, only control flow operations can be executed - # on the VM. - # Constraint degree: 4 - enf 1 - in_span - get_f_ctrl(op_bits, extra) = 0 -} - - -# Enforces the constraint for computing block hashes. -# -# Max constraint degree: 8 -ev block_hash_computation([addr, op_bits[7], hasher[8], extra], [p[4]]) { - # Get flags required for the block hash computation constraint - let f_ctrli = get_f_ctrli(op_bits, extra) - let f_span = get_f_span(op_bits) - let f_respan = get_f_respan(op_bits, extra) - let f_end = get_f_end(op_bits, extra) - - # Label specifying that we are starting a new hash computation. - let m_bp = get_transition_label(HASHER_LINEAR_HASH) - - # Label specifying that we are absorbing the next sequence of 8 elements into an ongoing hash - # computation. - let m_abp = get_transition_label(HASHER_LINEAR_HASH) - - # Label specifying that we are reading the result of a hash computation. - let m_hout = get_transition_label(HASHER_RETURN_HASH) - - # `alpha` is the global random values array. - let rate_sum = sum([$alpha[i + 8] * hasher[i] for i in 0..8]) - let digest_sum = sum([$alpha[i + 8] * hasher[i] for i in 0..4]) - - # Variable for initiating a hasher with address addr' and absorbing 8 elements from the hasher - # state (hasher[0], ..., hasher[7]) into it. - let h_init = $alpha[0] + $alpha[1] * m_bp + $alpha[2] * addr' + rate_sum - - # Variable for the absorption. - let h_abp = $alpha[0] + $alpha[1] * m_abp + $alpha[2] * addr' + rate_sum - - # Variable for the result. - let h_res = $alpha[0] + $alpha[1] * m_hout + $alpha[2] * (addr + 7) + digest_sum - - # Opcode value of the opcode being executed on the virtual machine. - let opcode_value = sum([op_bits[i] * 2^i for i in 0..7]) - - # When a control block initializer operation (JOIN, SPLIT, LOOP, CALL, SYSCALL) is executed, a - # new hasher is initialized and the contents of hasher[0], ..., hasher[7] are absorbed into the - # hasher. - # - # Value degree: 7 - let u_ctrli = f_ctrli * (h_init + $alpha[5] * opcode_value) - - # When SPAN operation is executed, a new hasher is initialized and contents of - # hasher[0], ..., hasher[7] are absorbed into the hasher. - # - # Value degree: 7 - let u_span = f_span * h_init - - # When RESPAN operation is executed, contents of hasher[0], ..., hasher[7] (which contain the - # new operation batch) are absorbed into the hasher. - # - # Value degree: 5 - let u_respan = f_respan * h_abp - - # When END operation is executed, the hash result is copied into registers - # hasher[0], ..., hasher[3]. - # - # Value degree: 5 - let u_end = f_end * h_res - - # Enforce the block hash computation constraint. We need to add 1 and subtract the sum of the - # relevant operation flags to ensure that when none of the flags is set to 1, the above - # constraint reduces to p[0]' = p[0]. - # Constraint degree: 8 - enf p[0]' * (u_ctrli + u_span + u_respan + u_end + 1 - - (f_ctrli + f_span + f_respan + f_end)) = p[0] -} - - -# Enforces the constraint for updating the block stack table. -# -# Max constraint degree: 8 -ev block_stack_table([addr, op_bits[7], hasher[8], s0, extra], [p[4]]) { - # Get flags required for the block stack table constraint - let f_join = get_f_join(op_bits) - let f_split = get_f_split(op_bits) - let f_loop = get_f_loop(op_bits) - let f_span = get_f_span(op_bits) - let f_respan = get_f_respan(op_bits, extra) - let f_end = get_f_end(op_bits, extra) - - # When JOIN operation is executed, row (addr', addr, 0) is added to the block stack table. - # Value degree: 7 - let v_join = f_join * ($alpha[0] + $alpha[1] * addr' + $alpha[2] * addr) - - # When SPLIT operation is executed, row (addr', addr, 0) added to the block stack table. - # Value degree: 7 - let v_split = f_split * ($alpha[0] + $alpha[1] * addr' + $alpha[2] * addr) - - # When LOOP operation is executed, row (addr', addr, 1) is added to the block stack table if - # the value at the top of the operand stack is 1, and row (addr', addr, 0) is added to the - # block stack table if the value at the top of the operand stack is 0. - # Value degree: 7 - let v_loop = f_loop * ($alpha[0] + $alpha[1] * addr' + $alpha[2] * addr + $alpha[3] * s0) - - # When SPAN operation is executed, row (addr', addr, 0) is added to the block stack table. - # Value degree: 7 - let v_span = f_span * ($alpha[0] + $alpha[1] * addr' + $alpha[2] * addr) - - # When RESPAN operation is executed, row (addr, hasher[1]', 0) is removed from the block stack - # table, and row (addr', hasher[1]', 0) is added to the table. The prover sets the value of - # register hasher[1] at the next row to the ID of the parent block. - # Value degree: 5 - let u_respan = f_respan * ($alpha[0] + $alpha[1] * addr + $alpha[2] * hasher[1]') - # Value degree: 5 - let v_respan = f_respan * ($alpha[0] + $alpha[1] * addr' + $alpha[2] * hasher[1]') - - # When END operation is executed, row (addr, addr', hasher[5]) is removed from the block span - # table. Register hasher[5] contains the is_loop flag. - # Value degree: 5 - let u_end = f_end * - ($alpha[0] + $alpha[1] * addr + $alpha[2] * addr' + $alpha[3] * hasher[5]) - - # Enforce the block stack table constraint. We need to add 1 and subtract the sum of the - # relevant operation flags from each side to ensure that when none of the flags is set to 1, - # the above constraint reduces to p[1]' = p[1] - # Constraint degree: 8 - enf p[1]' * (u_end + u_respan + 1 - (f_end + f_respan)) = - p[1] * (v_join + v_split + v_loop + v_span + v_respan + 1 - - (f_join + f_split + f_loop + f_span + f_respan)) -} - - -# Enforces the constraint for updating the block hash table. -# -# Max constraint degree: 9 -ev block_hash_table([addr, op_bits[7], hasher[8], s0, extra], [p[4]]) { - # Get flags required for the block hash table constraint - let f_join = get_f_join(op_bits) - let f_split = get_f_split(op_bits) - let f_loop = get_f_loop(op_bits) - let f_end = get_f_end(op_bits, extra) - let f_repeat = get_f_repeat(op_bits, extra) - - # Values representing left and right children of a block. - # Value degree: 1 - let ch1 = $alpha[0] + $alpha[1] * addr' + sum([$alpha[i + 2] * hasher[i] for i in 0..4]) - # Value degree: 1 - let ch2 = $alpha[0] + $alpha[1] * addr' + sum([$alpha[i + 2] * hasher[i + 4] for i in 0..4]) - - # Value representing the result of hash computation. - # Value degree: 1 - let bh = $alpha[0] + $alpha[1] * addr + sum([$alpha[i + 2] * hasher[i]]) + $alpha[7] * hasher[4] - - # When JOIN operation is executed, hashes of both child nodes are added to the block hash - # table. We add alpha[6] term to the first child value to differentiate it from the second - # child (i.e., this sets is_first_child to 1). - # Value degree: 8 - let v_join = f_join * (ch1 + $alpha[6]) * ch2 - - # When SPLIT operation is executed and the top of the stack is 1, hash of the true branch is - # added to the block hash table, but when the top of the stack is 0, hash of the false branch - # is added to the block hash table. - # Value degree: 8 - let v_split = f_split * (s0 * ch1 + (1 - s0) * ch2) - - # When LOOP operation is executed and the top of the stack is 1, hash of loop body is added to - # the block hash table. We add alpha[7] term to indicate that the child is a body of a loop. - # The below also means that if the top of the stack is 0, nothing is added to the block hash - # table as the expression evaluates to 0. - # Value degree: 8 - let v_loop = f_loop * s0 * (ch1 + $alpha[7]) - - # When REPEAT operation is executed, hash of loop body is added to the block hash table. We add - # alpha[7] term to indicate that the child is a body of a loop. - # Value degree: 5 - let v_repeat = f_repeat * (ch1 + $alpha[7]) - - # When END operation is executed, hash of the completed block is removed from the block hash - # table. However, we also need to differentiate between removing the first and the second child - # of a join block. We do this by looking at the next operation. Specifically, if the next - # operation is neither END nor REPEAT we know that another block is about to be executed, and - # thus, we have just finished executing the first child of a join block. Thus, if the next - # operation is neither END nor REPEAT we need to set the term for alpha[6] coefficient to 1 as - # shown below. - # Value degree: 8 - let u_end = f_end * - (bh + $alpha[6] * (1 - (get_f_end(op_bits', extra') + get_f_repeat(op_bits', extra')))) - - # Enforce the block hash table constraint. We need to add 1 and subtract the sum of the - # relevant operation flags from each side to ensure that when none of the flags is set to 1, - # the above constraint reduces to p[2]' = p[2] - # Constraint degree: 9 - enf p[2]' * (u_end + 1 - f_end) = - p[2] * (v_join + v_split + v_loop + v_repeat + 1 - (f_join + f_split + f_loop + f_repeat)) - - # TODO: add boundary constraints to the p[2] column: - # 1. The first value in the column represents a row for the entire program. Specifically, the - # row tuple would be (0, program_hash, 0, 0). This row should be removed from the table - # when the last END operation is executed. - # 2. The last value in the column is 1 - i.e., the block hash table is empty. -} - - -# Enforce that values in in_span column, which is used to identify rows which execute non-control -# flow operations, are set correctly. -# -# Constraint degree: 7 -ev in_span_column([op_bits[7], in_span, extra]) { - # Get flags required for the inspan column constraint - let f_span = get_f_span(op_bits) - let f_respan = get_f_respan(op_bits, extra) - let f_respan_next = get_f_respan(op_bits', extra') - let f_end_next = get_f_end(op_bits', extra') - - # Enforce that when executing SPAN or RESPAN operation, the next value in in_span column must - # be set to 1. - # Constraint degree: 7 - enf in_span' = 1 when f_span | f_respan - - # Enforce that when the next operation is END or RESPAN, the next value in in_span column must - # be set to 0. - # Constraint degree: 5 - enf in_span' = 0 when f_end_next | f_respan_next - - # Enforce that in all other cases, the value in in_span column must be copied over to the next - # row. - # Constraint degree: 7 - enf is_unchanged(in_span) when !f_span & !f_respan & !f_end_next & !f_respan_next - - # TODO: add boundary constraint for in_span column: in_span.first = 0 -} - -# Enforce that when we are inside a span block, values in the block address column (denoted as addr) -# must remain the same. -# -# Constraint degree: 2 -ev block_address([addr, in_span]) { - enf is_unchanged(addr) when in_span -} - -# Enforce that values in group_count column, which is used to keep track of the number of operation -# groups which remains to be executed in a span block, are set correctly. -# -# Max constraint degree: 7 -ev group_count([op_bits[7], hasher[8], in_span, group_count, extra]) { - # Get value of the f_push flag - let f_push = get_f_push(op_bits, extra) - - # Enforce that inside a span block, group count can either stay the same or decrease by one. - # Constraint degree: 3 - enf (group_count' - group_count) * (group_count' - group_count - 1) = 0 when in_span - - # Enforce that when group count is decremented inside a span block, either hasher[0] must be 0 - # (we consumed all operations in a group) or we must be executing PUSH operation. - # Constraint degree: 7 - enf (1 - f_push) * hasher[0] = 0 when in_span & (group_count' - group_count) - - # Enforce that when executing a SPAN, a RESPAN, or a PUSH operation, group count must be - # decremented by 1. - # Constraint degree: 7 - enf group_count' - group_count = 1 when f_span(op_bits) | get_f_respan(op_bits, extra) | f_push - - # Enforce that if the next operation is either an END or a RESPAN, group count must remain the - # same. - # Constraint degree: 5 - enf is_unchanged(group_count) when get_f_end(op_bits', extra') | get_f_respan(op_bits', extra') - - # Enforce that when an END operation is executed, group count must be 0. - # Constraint degree: 5 - enf group_count = 0 when get_f_end(op_bits, extra) -} - -# Enforce that register hasher[0], which is used to keep track of operations to be executed in the -# current operation group, is set correctly. -# -# Max constraint degree: 7 -ev op_group_decoding([op_bits[7], in_span, group_count, extra]) { - # opcode value for the next row. - let op_next = sum([op_bits[i]' * 2^i for i in 0..7]) - - # Flag which is set to 1 when the group count within a span block does not change. We multiply - # it by sp' to make sure the flag is 0 when we are about to end decoding of an operation batch. - let f_sgc = in_span * in_span' * (1 - group_count' + group_count) - - # Enforce that when a SPAN, a RESPAN, or a PUSH operation is executed or when the group count - # does not change, the value in hasher[0] should be decremented by the value of the opcode in - # the next row. - # Constraint degree: 7 - enf hasher[0] - hasher[0]' * 2^7 - op_next = 0 - when f_span(op_bits) | get_f_respan(op_bits, extra) | get_f_push(op_bits, extra) | f_sgc - - # Enforce that when we are in a span block and the next operation is END or RESPAN, the current - # value in hasher[0] column must be 0. - # Constraint degree: 6 - enf (get_f_end(op_bits', extra') + get_f_respan(op_bits', extra')) * hasher[0] = 0 when in_span -} - -# Enforce that the values in op_index column, which tracks index of an operation within its -# operation group, are set correctly. -# -# Max constraint degree: 9 -ev op_index([op_bits[7], in_span, group_count, op_index, extra]) { - # ng is set to 1 when we are about to start executing a new operation group (i.e., group count - # is decremented but we did not execute a PUSH operation). - let ng = group_count' - group_count - get_f_push(op_bits, extra) - - # Enforce that when executing SPAN or RESPAN operations the next value of op_index must be set - # to 0. - # Constraint degree: 7 - enf op_index' = 0 when f_span(op_bits) | get_f_respan(op_bits, extra) - - # Enforce that when starting a new operation group inside a span block, the next value of - # op_index must be set to 0. - # Constraint degree: 6 - enf op_index' = 0 when in_span & ng - - # Enforce that when inside a span block but not starting a new operation group, op_index must - # be incremented by 1. - # Constraint degree: 7 - enf op_index' - op_index = 1 when in_span & in_span' & !ng - - # Enforce that values of op_index must be in the range [0, 8]. - # Constraint degree: 9 - enf prod([op_index - i for i in 0..9]) = 0 -} - -# Enforce that values in operation batch flag columns (denoted op_batch_flags[]), which are used to -# specify how many operation groups are present in an operation batch, are set correctly. -# -# Max constraint degree: 6 -ev op_batch_flags([op_bits[7], hasher[8], op_batch_flags[3], extra]) { - # Get flags required for the op batch flag constraints - let f_g1 = get_f_g1(op_batch_flags) - let f_g2 = get_f_g2(op_batch_flags) - let f_g4 = get_f_g4(op_batch_flags) - let f_g8 = get_f_g8(op_batch_flags) - - # Enforce that all batch flags are binary. - # Constraint degree: 2 - enf is_binary(bc) for bc in op_batch_flags - - # Enforce that when SPAN or RESPAN operations is executed, one of the batch flags must be set - # to 1. - # Constraint degree: 6 - enf f_g1 + f_g2 + f_g4 + f_g8 = 1 when f_span(op_bits) | get_f_respan(op_bits, extra) - - # Enforce that when we have at most 4 groups in a batch, registers h[4], ..., h[7] should be - # set to 0's. - # Constraint degree: 4 - enf hasher[i] = 0 for i in 4..8 when f_g1 | f_g2 | f_g4 - - # Enforce that When we have at most 2 groups in a batch, registers h[2] and h[3] should also be - # set to 0's. - # Constraint degree: 4 - enf hasher[i] = 0 for i in 2..4 when f_g1 | f_g2 - - # Enforce that when we have at most 1 group in a batch, register h[1] should also be set to 0. - # Constraint degree: 4 - enf hasher[1] = 0 when f_g1 -} - -# Enforce that all operation groups in a given batch are consumed before a new batch is started -# (i.e., via a RESPAN operation) or the execution of a span block is complete (i.e., via an END -# operation). -# -# Max constraint degree: 9 -ev op_group_table([addr, op_bits[7], hasher[8], in_span, group_count, op_index, op_batch_flags[3], s0, extra], [p[4]]) { - # Get value of the f_push flag - let f_push = get_f_push(op_bits, extra) - - # opcode value for the next row. - let op_next = sum([op_bits[i]' * 2^i for i in 0..7]) - - # Row value for group in hasher[1] to be added to the op group table when a SPAN or a RESPAN - # operation is executed. - # Value degree: 1 - let v_1 = $alpha[0] + $alpha[1] * addr' + $alpha[2] * (group_count - 1) + $alpha[3] * hasher[1] - - # Value degree: 1 - let prod_v_3 = prod([$alpha[0] + - $alpha[1] * addr' + - $alpha[2] * (group_count - i) + - $alpha[3] * hasher[i] for i in 1..4]) - - # Value degree: 1 - let prod_v_7 = prod([$alpha[0] + - $alpha[1] * addr' + - $alpha[2] * (group_count - i) + - $alpha[3] * hasher[i] for i in 1..8]) - - # The value of the row to be removed from the op group table. - # Value degree: 5 - let u = $alpha[0] + $alpha[1] * addr + $alpha[2] * group_count + $alpha[3] * - ((hasher[0]' * 2^7 + op_next) * (1 - f_push) + s0' * f_push) = 0 - - # A flag which is set to 1 when a group needs to be removed from the op group table. - let f_dg = in_span * (group_count' - group_count) - - # Enforce the constraint for updating op group table. The constraint specifies that when SPAN - # or RESPAN operations are executed, we add between 1 and 7 groups to the op group table, and - # when group count is decremented inside a span block, we remove a group from the op group - # table. - # Constraint degree: 9 - enf p[3]' * (f_dg * u + 1 - f_dg) = p[3] * (get_f_g2(op_batch_flags) * v_1 + - get_f_g4(op_batch_flags) * prod_v_3 + - get_f_g8(op_batch_flags) * prod_v_7 - 1 + - (f_span(op_bits) + get_f_respan(op_bits, extra))) -} - -# Enforce proper decoding of span blocks. -# -# Max constraint degree: 9 -ev span_block([addr, op_bits[7], hasher[8], in_span, group_count, op_index, op_batch_flags[3], s0, extra], [p[4]]) { - enf in_span_column([op_bits, in_span, extra]) - enf block_address([addr, in_span]) - enf group_count([op_bits, hasher, in_span, group_count, extra]) - enf op_group_decoding([op_bits, in_span, group_count, extra]) - enf op_index([op_bits, in_span, group_count, op_index, extra]) - enf op_batch_flags([op_bits, hasher, op_batch_flags, extra]) - enf op_group_table([addr, op_bits, hasher, in_span, group_count, op_index, op_batch_flags, s0, extra], [p]) -} - -### Decoder Air Constraints ####################################################################### - -# Enforces the constraints on the decoder. The register `s0` denotes the value at the top of the -# stack. `extra` denotes the register for degree reduction during flag computations, and p[4] -# columns denote multiset check columns. -# -# Max constraint degree: 9 -ev decoder_constraints([addr, op_bits[7], hasher[8], in_span, group_count, op_index, op_batch_flags[3], s0, extra], [p[4]]) { - enf general([addr, op_bits[7], hasher[8], in_span, s0, extra]) - - enf block_hash_computation([addr, op_bits[7], hasher[8], extra], [p[4]]) - - enf block_stack_table([addr, op_bits[7], hasher[8], s0, extra], [p[4]]) - - enf block_hash_table([addr, op_bits, hasher, s0, extra], [p[4]]) - - enf span_block([addr, op_bits[7], hasher[8], in_span, group_count, op_index, op_batch_flags[3], s0, extra], [p[4]]) -} \ No newline at end of file diff --git a/constraints/miden-vm/hash.air b/constraints/miden-vm/hash.air deleted file mode 100644 index 55165cd19..000000000 --- a/constraints/miden-vm/hash.air +++ /dev/null @@ -1,208 +0,0 @@ -mod HashChipletAir - -### Constants and periodic columns ################################################################ - -periodic_columns { - cycle_row_0: [1, 0, 0, 0, 0, 0, 0, 0] - cycle_row_6: [0, 0, 0, 0, 0, 0, 1, 0] - cycle_row_7: [0, 0, 0, 0, 0, 0, 0, 1] -} - -### Helper functions ############################################################################## - -# Returns binary negation of the value. -fn binary_not(value: scalar) -> scalar: - return 1 - value - - -# Set to 1 when selector flags are (1,0,1) on rows which are multiples of 8. This is flag of -# the instruction that initiates Merkle path verification computation. -fn get_f_mp(s: vector[3]) -> scalar: - return cycle_row_0 & s[0] & binary_not(s[1]) & s[2] - - -# Set to 1 when selector flags are (1,1,0) on rows which are multiples of 8. This is flag of -# the instruction that initiates Merkle path verification for the "old" node value during -# Merkle root update computation. -fn get_f_mv(s: vector[3]) -> scalar: - return cycle_row_0 & s[0] & s[1] & binary_not(s[2]) - - -# Set to 1 when selector flags are (1,1,1) on rows which are multiples of 8. This is flag of -# the instruction that initiates Merkle path verification for the "new" node value during -# Merkle root update computation. -fn get_f_mu(s: vector[3]) -> scalar: - return cycle_row_0 & s[0] & s[1] & s[2] - - -# Set to 1 when selector flags are (1,0,0) on rows which are 1 less than a multiple of 8. This -# is flag of the instruction that absorbs a new set of elements into the hasher state when -# computing a linear hash of many elements. -fn get_f_abp(s: vector[3]) -> scalar: - return cycle_row_7 & s[0] & binary_not(s[1]) & binary_not(s[2]) - - -# Set to 1 when selector flags are (1,0,1) on rows which are 1 less than a multiple of 8. This -# is flag of the instruction that absorbs the next Merkle path node into the hasher state -# during Merkle path verification computation. -fn get_f_mpa(s: vector[3]) -> scalar: - return cycle_row_7 & s[0] & binary_not(s[1]) & s[2] - - -# Set to 1 when selector flags are (1,1,0) on rows which are 1 less than a multiple of 8. This -# is flag of the instruction that absorbs the next Merkle path node into the hasher state -# during Merkle path verification for the "old" node value during Merkle root update -# computation. -fn get_f_mva(s: vector[3]) -> scalar: - return cycle_row_7 & s[0] & s[1] & binary_not(s[2]) - - -# Set to 1 when selector flags are (1,1,1) on rows which are 1 less than a multiple of 8. This -# is flag of the instruction that absorbs the next Merkle path node into the hasher state -# during Merkle path verification for the "new" node value during Merkle root update -# computation. -fn get_f_mua(s: vector[3]) -> scalar: - return cycle_row_7 & s[0] & s[1] & s[2] - - -# We can define two flags: -# 1. Flag f_hout = cycle_row_7 & binary_not(s[0]) & binary_not(s[1]) & binary_not(s[2]), -# which is set to 1 when selector flags are (0,0,0) on rows which are 1 less than a multiple -# of 8. This is flag of the instruction that returns the result of the currently running -# computation. -# 2. Flag f_sout = cycle_row_7 & binary_not(s[0]) & binary_not(s[1]) & s[2], which is set to 1 -# when selector flags are (0,0,1) on rows which are 1 less than a multiple of 8. This is flag -# of the instruction that returns the whole hasher state. -# -# Flag f_out is set to 1 when either f_hout = 1 or f_sout = 1 in the current row. -fn get_f_out(s: vector[3]) -> scalar: - return cycle_row_7 & binary_not(s[0]) & binary_not(s[1]) - - -# Flag f_out_next is set to 1 when either f_hout = 1 or f_sout = 1 in the next row. -fn get_f_out_next(s: vector[3]) -> scalar: - return cycle_row_6 & binary_not(s[0]') & binary_not(s[1]') - - -### Helper evaluators ############################################################################# - -# Enforces that column must be binary. -ev is_binary(main: [a]) { - enf a^2 = a -} - - -# Enforces that value in column is copied over to the next row. -ev is_unchanged(main: [column]) { - ev column' = column -} - - -# Enforce selector columns constraints -ev selector_columns(main: [s[3]]) { - let f_out = get_f_out(s) - let f_out_next = get_f_out_next(s) - let f_abp = get_f_abp(s) - let f_mpa = get_f_mpa(s) - let f_mva = get_f_mva(s) - let f_mua = get_f_mua(s) - - # Flag that is true when the performed operation is one of the represented by flags f_abp, - # f_mpa, f_mva or f_mua - let f_comp = f_abp + f_mpa + f_mva + f_mua - - # Enforce that selector columns are binary. - enf is_binary([selector]) for selector in s - - # Enforce that unless f_out = 1 or f_out' = 1, the values in columns s[1] and s[2] are copied - # over to the nex row. - enf is_unchanged([s[1]]) when !f_out & !f_out_next - enf is_unchanged([s[2]]) when !f_out & !f_out_next - - # Enforce that if any of f_abp, f_mpa, f_mva, f_mua flags is set to 1, the next value of s[0] - # is 0. - enf s[0]' * f_comp = 0 - - # Enforce that no invalid combinations of flags are allowed. - enf cycle_row_7 * binary_not(s[0]) * s[1] = 0 -} - -# Enforce node index constraints -ev node_index(main: [s[3], i]) { - let f_out = get_f_out(s) - let f_mp = get_f_mp(s) - let f_mv = get_f_mv(s) - let f_mu = get_f_mu(s) - let f_mpa = get_f_mpa(s) - let f_mva = get_f_mva(s) - let f_mua = get_f_mua(s) - - # b is the value of the bit which is discarded during shift by one bit to the right. - let b = i - 2 * i' - - # Flag that allows to enforce constraint that b is binary only when a new node is absorbed into - # the hasher state (when the hash operation is one of Merkle path verification operations or - # next Merkle path node absorption operations) - let f_an = f_mp + f_mv + f_mu + f_mpa + f_mva + f_mua - - # Enforce that b is binary only when a new node is absorbed into the hasher state. - enf f_an * (b^2 - b) = 0 - - # Enforce that when a computation is finished i = 0. - enf f_out * i = 0 - - # Enforce that the value in i is copied over to the next row unless we are absorbing a new row - # or the computation is finished. - let absorbing_or_comp_finished = 1 - f_an - f_out - enf is_unchanged([i]) when absorbing_or_comp_finished -} - -# Enforce hasher state constraints -ev hasher_state(main: [s[3], h[12], i]) { - let f_mp = get_f_mp(s) - let f_mv = get_f_mv(s) - let f_mu = get_f_mu(s) - let f_abp = get_f_abp(s) - - # Flag that is true when the performed operation includes absorbing the next node during Merkle - # path computation. - let f_absorb_node = f_mp + f_mv + f_mu - - # b is the value of the bit which is discarded during shift by one bit to the right. - let b = i - 2 * i' - - # Enforce that when absorbing the next set of elements into the state during linear hash - # computation (i.e. f_abp = 1) the first 4 elements (the capacity portion) are carried over to - # the next row. - enf f_abp * (h[j]' - h[j]) = 0 for j in 0..4 - - # Enforce that when absorbing the next node during Merkle path computation - # (i.e. f_mp + f_mv + f_mu = 1), the result of the previous hash (h[4], ..., h[7]) are copied - # over either to (h[4]', ..., h[7]') or to (h[8]', ..., h[11]') depending on the value of b. - match enf: - is_unchanged(h[j + 4]) for j in 0..4 when !b & f_absorb_node - h[j + 8]' = h[j + 4] for j in 0..4 when b & f_absorb_node -} - -### Hash Chiplet Air Constraints ################################################################## - -# Enforces the constraints on the hash chiplet, given the columns of the hash execution trace. -ev hash_chiplet(main: [s[3], r, h[12], i]) { - ## Row address constraint ## - # TODO: Apply row address constraints: - # 1. Boundary constraint `enf r.first = 1` - # 2. Transition constraint. It requires chiplets module's selector flag s0. - - ## Selector columns constraints ## - enf selector_columns([s]) - - ## Node index constraints ## - enf node_index([s, i]) - - ## Hasher state constraints ## - # TODO: apply RPO constraints to the hasher state - enf hasher_state([s, h, i]) - - # Multiset check constraints - # TODO: Apply multiset check constraints -} \ No newline at end of file diff --git a/constraints/miden-vm/memory.air b/constraints/miden-vm/memory.air deleted file mode 100644 index 17da938a5..000000000 --- a/constraints/miden-vm/memory.air +++ /dev/null @@ -1,120 +0,0 @@ -mod MemoryChipletAir - -### Helper functions ############################################################################## - -# Returns the n0 flag which is set to 1 when context changes and 0 otherwise. -fn get_n0(ctx: scalar, ctx_next: scalar, t_next: scalar) -> scalar: - return (ctx_next - ctx) * t_next - - -# Returns the n1 flag. If context remains the same, n1 = 1 when address changes and 0 otherwise. -fn get_n1(addr: scalar, addr_next: scalar, t_next: scalar) -> scalar: - return (addr_next - addr) * t_next - - -### Helper evaluators ############################################################################# - -# Enforces that column must be binary. -# Constraint degree: 2 -ev is_binary([a]) { - enf a^2 = a -} - - -# Enforces that value in column is copied over to the next row. -# Constraint degree: 1 -ev is_unchanged([column]) { - enf column' = column -} - - -# Enforces that the provided columns must be zero. -ev is_zero([column]) { - enf column = 0 -} - - -# Enforces that created flags have valid values during the program execution. -ev flags_validity([ctx, addr, t]) { - # n0 = 1 when context changes and 0 otherwise. - let n0 = get_n0(ctx, ctx', t') - - # if context remains the same, n1 = 1 when address changes and 0 otherwise. - let n1 = get_n1(addr, addr', t') - - # Enforce that n0 must be binary. - enf n0^2 = n0 - - # Enforce that when context changes, n0 = 1 (or when n0 = 0, context remains the same). - enf ctx' = ctx when !n0 - - # Enforce that n1 must be binary. An additional condition ensures that the check of n1 - # occurs only if the context does not change (n0 = 0). - enf n1^2 = n1 when !n0 - - # Enforce that if context remains the same, n1 = 1 when address changes and 0 otherwise. - enf addr' = addr when !n0 & !n1 -} - -# Enforces that selectors take the correct values under certain conditions. -ev enforce_selectors([s[2], ctx, addr, t]) { - # Enforce that values in the selectior columns must be binary. - # s[0] is set to 0 for write operations and to 1 for read operations. - enf is_binary([selector]) for selector in s - - # n0 = 1 when context changes and 0 otherwise. - let n0 = get_n0(ctx, ctx', t') - - # if context remains the same, n1 = 1 when address changes and 0 otherwise. - let n1 = get_n1(addr, addr', t') - - # Enforce that s[1]' = 1 when the operation is a read and `ctx` and `addr` columns are both - # unchanged. - enf s[1]' = 1 when !n0 & !n1 & s[0]' - - # Enforce that s[1]' = 0 when either the context changed, the address changed, or the operation - # is a write. - enf s[1]' = 0 when n0 | n1 | !s[0]' -} - -# Enforces that the delta between two consecutive contexts, addresses, or clock cycles is updated -# and decomposed into the `d1` and `d0` columns correctly. -ev enforce_delta([ctx, addr, clk, d[2], t]) { - # n0 = 1 when context changes and 0 otherwise. - let n0 = get_n0(ctx, ctx', t') - - # if context remains the same, n1 = 1 when address changes and 0 otherwise. - let n1 = get_n1(addr, addr', t') - - let d_next_agg = 2^16 * d[1]' + d[0]' - - # Enforce that values of context (`ctx`), address (`addr`), and clock cycle (`clk`) grow - # monotonically - match enf: - d_next_agg = ctx' - ctx when n0 - d_next_agg = addr' - addr when !n0 & n1 - d_next_agg = clk' - clk - 1 when !n0 & !n1 -} - -# Enforces that memory is initialized to zero when it is read before being written and that when -# existing memory values are read they remain unchanged. -ev enforce_values([s[2], v[4]]) { - # Enforce that values at a given memory address are always initialized to 0. - enf is_zero([v_i]) for v_i in v when s[0] & !s[1] - - # Enforce that for the same context/address combination, the v columns of the current row are - # equal to the corresponding v columns of the next row - enf is_unchanged([v_i]) for v_i in v when s[1] -} - -### Memory Chiplet Air Constraints ################################################################ - -# Enforces the constraints on the memory chiplet, given the columns of the memory execution trace. -ev memory_chiplet([s[2], ctx, addr, clk, v[4], d[2], t]) { - enf flags_validity([ctx, addr, t]) - enf enforce_selectors([s, ctx, addr, t]) - enf enforce_delta([ctx, addr, clk, d, t]) - # TODO: perform range checks for values in columns d[0] and d[1] - enf enforce_values([s, v]) - # Bus constraint is implemented in a separate file -} \ No newline at end of file diff --git a/constraints/miden-vm/range_checker.air b/constraints/miden-vm/range_checker.air deleted file mode 100644 index f3581de8c..000000000 --- a/constraints/miden-vm/range_checker.air +++ /dev/null @@ -1,62 +0,0 @@ -mod RangeCheckerAir - -### Helper functions ############################################################################## - -# Returns array of mutually exclusive multiplicity flags. -# f[0] set to 1 when we don't include the value into the running product. -# f[1] set to 1 when we include the value into the running product. -# f[2] set to 1 when we include two copies of the value into the running product. -# f[3] set to 1 when we include four copies of the value into the running product. -fn get_multiplicity_flags(s0: scalar, s1: scalar) -> vector[4]: - return [!s0 & !s1, s0 & !s1, !s0 & s1, s0 & s1] - - -### Helper evaluators ############################################################################# - -# Enforces that column must be binary. -ev is_binary([v]) { - enf v^2 = v -} - -# Enforces correct transition from 8-bit to 16-bit section of the table. -ev transition_8_to_16_bit([t, v]) { - # Ensure that values in column t can flip from 0 to 1 only once - enf t * !t' = 0 - - # Ensure that when column t flips, column v must equal 255 - enf v = 255 when t' & !t - - # Ensure that when column t flips, v' must be reset to 0 - enf v' = 0 when t' & !t -} - -# The virtual table enforces an 8-bit range check for each row transition in the 16-bit section of -# the range checker, which enforces its internal correctness. -ev virtual_table([t, s0, s1, v], [p0]) { - let val = $alpha[0] + v - let f = get_multiplicity_flags(s0, s1) - - # z represents how a row in the execution trace is reduced to a single value. - let z = val^4 * f[3] + val^2 * f[2] + val * f[1] + f[0] - enf p0' * (($alpha[0] + v' - v) * t - t + 1) = p0 * (z - z * t + t) - - # TODO: add boundary constraints p0.first = 1 and p0.last = 1 -} - -### Range checker Air Constraints ################################################################# - -ev range_checker([t, s0, s1, v], [p0]) { - # Check selector flags are binary. - let selectors = [t, s0, s1] - enf is_binary([s]) for s in selectors - - # Constrain the row transitions in the 8-bit section of the table so that as we move from one - # row to the next the value either stays the same or increases by 1. - enf (v' - v) * (v' - v - 1) = 0 when !t' - - # Constrain the transition from 8-bit to 16-bit section of the table. - enf transition_8_to_16_bit([t, v]) - - # Constrain the row transitions in the 16-bit section of the table. - enf virtual_table([t, s0, s1, v], [p0]) -} \ No newline at end of file diff --git a/constraints/miden_vm.air b/constraints/miden_vm.air index 38d0ebee0..0d50d44bf 100644 --- a/constraints/miden_vm.air +++ b/constraints/miden_vm.air @@ -176,14 +176,14 @@ integrity_constraints { # System state transitions (needs decoder columns for operation flags) enf system_transition([system[0..8], decoder[0..24]]); - # Decoder constraints - Program execution and operation decoding (needs stack top s0) - enf decoder([decoder, stack[0]]); + # Decoder constraints - Program execution and operation decoding (needs stack top s0-s2, system clk and ctx) + enf decoder([decoder, stack[0], stack[1], stack[2], system[0], system[2]]); # Stack constraints - Operand stack operations and overflow handling - enf stack([stack[0..19], decoder[0..24], system[0], system[1]]); # Pass decoder columns, system clock, and fmp for flag computation + enf stack([stack[0..19], decoder[0..24], system[0], system[1], system[2], system[4], system[5], system[6], system[7]]); # Chiplet constraints - Hash, bitwise, ACE, memory operations, and kernel ROM - enf chiplets_constraints([chiplets[0..20]]); + enf chiplets_constraints([chiplets[0..20], system[0]]); #################################################################################### # BUS CONSTRAINTS diff --git a/constraints/stack.air b/constraints/stack.air index 1af364b42..d751ea09d 100644 --- a/constraints/stack.air +++ b/constraints/stack.air @@ -29,7 +29,7 @@ ev stack([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, decoder_addr, decoder_b0, decoder_b1, decoder_b2, decoder_b3, decoder_b4, decoder_b5, decoder_b6, decoder_h0, decoder_h1, decoder_h2, decoder_h3, decoder_h4, decoder_h5, decoder_h6, decoder_h7, decoder_sp, decoder_gc, decoder_ox, decoder_c0, decoder_c1, decoder_c2, decoder_e0, decoder_e1, - system_clk, system_fmp]) { + system_clk, system_fmp, system_ctx, system_fn_hash_0, system_fn_hash_1, system_fn_hash_2, system_fn_hash_3]) { # Stack element columns (always visible top 16 elements) # s0-s15 are the top 16 stack elements (s0 = top of stack) # b0 = stack depth (≥ 16) @@ -48,9 +48,10 @@ ev stack([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, #################################################################################### enf stack_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, - b0, decoder_b0, decoder_b1, decoder_b2, decoder_b3, decoder_b4, decoder_b5, decoder_b6, + b0, b1, decoder_b0, decoder_b1, decoder_b2, decoder_b3, decoder_b4, decoder_b5, decoder_b6, decoder_h0, decoder_h1, decoder_h2, decoder_h3, decoder_h4, decoder_h5, - decoder_e0, decoder_e1, system_clk, system_fmp]); + decoder_e0, decoder_e1, system_clk, system_fmp, system_ctx, + system_fn_hash_0, system_fn_hash_1, system_fn_hash_2, system_fn_hash_3]); } @@ -154,10 +155,11 @@ ev right_shift_b1_constraint([b1, decoder_b0, decoder_b1, decoder_b2, decoder_b3 # Applies the appropriate operation-specific constraints based on active operation flags ev stack_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, - stack_b0, decoder_b0, decoder_b1, decoder_b2, decoder_b3, decoder_b4, decoder_b5, decoder_b6, + stack_b0, stack_b1, decoder_b0, decoder_b1, decoder_b2, decoder_b3, decoder_b4, decoder_b5, decoder_b6, decoder_h0, decoder_h1, decoder_h2, decoder_h3, decoder_h4, decoder_h5, decoder_e0, decoder_e1, - system_clk, system_fmp + system_clk, system_fmp, system_ctx, + system_fn_hash_0, system_fn_hash_1, system_fn_hash_2, system_fn_hash_3 ]) { @@ -255,13 +257,17 @@ ev stack_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11 let is_mstream = flag_mstream(op_bits, decoder_e0); # Opcode 83 (101_0011) let is_split = flag_split(op_bits, decoder_e0); # Opcode 84 (101_0100) let is_loop = flag_loop(op_bits, decoder_e0); # Opcode 85 (101_0101) + let is_dyn = flag_dyn(op_bits, decoder_e0); # Opcode 88 (101_1000) let is_hornerext = flag_hornerext(op_bits, decoder_e0); # Opcode 89 (101_1001) let is_push = flag_push(op_bits, decoder_e0); # Opcode 91 (101_1011) + let is_dyncall = flag_dyncall(op_bits, decoder_e0); # Opcode 92 (101_1100) let is_evalcircuit = flag_evalcircuit(op_bits, decoder_e0); # Opcode 93 (101_1101) # Group 5: Very high-degree operations (110 group) - requires e1 for degree reduction let is_mrupdate = flag_mrupdate(op_bits, decoder_e1); # Opcode 96 (110_0000) let is_hornerbase = flag_hornerbase(op_bits, decoder_e1); # Opcode 100 (110_0100) + let is_syscall = flag_syscall(op_bits, decoder_e1); # Opcode 104 (110_1000) + let is_call = flag_call(op_bits, decoder_e1); # Opcode 108 (110_1100) enf match { # No stack shift operations - ordered by Miden VM specification (opcodes 0-31) @@ -272,9 +278,9 @@ ev stack_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11 case is_incr: incr_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15]), # 4 case is_not: not_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15]), # 5 case is_fmpadd: fmpadd_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, system_fmp]), # 6 - case is_mload: mload_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15]), # 7 + case is_mload: mload_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, system_ctx, system_clk]), # 7 case is_swap: swap_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15]), # 8 - case is_caller: caller_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15]), # 9 + case is_caller: caller_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, system_fn_hash_0, system_fn_hash_1, system_fn_hash_2, system_fn_hash_3]), # 9 case is_movup2: movup2_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15]), # 10 case is_movdn2: movdn2_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15]), # 11 case is_movup3: movup3_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15]), # 12 @@ -311,9 +317,9 @@ ev stack_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11 case is_drop: drop_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15]), # 41 case is_cswap: cswap_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15]), # 42 case is_cswapw: cswapw_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15]), # 43 - case is_mloadw: mloadw_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15]), # 44 - case is_mstore: mstore_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15]), # 45 - case is_mstorew: mstorew_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15]), # 46 + case is_mloadw: mloadw_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, system_ctx, system_clk]), # 44 + case is_mstore: mstore_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, system_ctx, system_clk]), # 45 + case is_mstorew: mstorew_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, system_ctx, system_clk]), # 46 case is_fmpupdate: fmpupdate_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, system_fmp]), # 47 # Right stack shift operations - ordered by Miden VM specification (opcodes 48-63) @@ -351,13 +357,17 @@ ev stack_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11 case is_mstream: mstream_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15]), # 83 case is_split: split_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15]), # 84 case is_loop: loop_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15]), # 85 + case is_dyn: dyn_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15]), # 88 case is_hornerext: hornerext_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, decoder_h0, decoder_h1, decoder_h2, decoder_h3, decoder_h4, decoder_h5]), # 89 case is_push: push_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15]), # 91 + case is_dyncall: dyncall_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, stack_b0, stack_b1]), # 92 case is_evalcircuit: evalcircuit_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15]), # 93 # Very high-degree operations (110 group) case is_mrupdate: mrupdate_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15]), # 96 case is_hornerbase: hornerbase_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, decoder_h0, decoder_h1, decoder_h2, decoder_h3, decoder_h4, decoder_h5]), # 100 + case is_syscall: syscall_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, stack_b0, stack_b1]), # 104 + case is_call: call_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, stack_b0, stack_b1]), # 108 }; } @@ -414,6 +424,9 @@ ev add_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, # Applies Rescue Prime Optimized permutation to top 12 elements (8 rate + 4 capacity) ev hperm_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15]) { # Positions 0-11: Transformed by RPO permutation (unconstrained, validated by hash chiplet) + # Request full state from hasher chiplet (SOUT returns all 12 elements) + bus_6_chiplets_bus.insert(HASHERRETURNSTATE, s0', s1', s2', s3', s4', s5', s6', s7', s8', s9', s10', s11') when 1; + # Positions 12-15: Unchanged enf s12' = s12; enf s13' = s13; enf s14' = s14; enf s15' = s15; } @@ -422,6 +435,11 @@ ev hperm_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11 # Stack behavior: [V0, V1, V2, V3, d, i, R0, R1, R2, R3, ...] -> [V0, V1, V2, V3, d, i, R0, R1, R2, R3, ...] # Verifies Merkle path from node value V to root R at depth d and index i ev mpverify_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15]) { + # Request Merkle path verification from hasher chiplet + # The hasher verifies that the path from leaf V (s0-s3) at index i (s5) and depth d (s4) + # results in root R (s6-s9). The result (should equal R) is returned in the response. + bus_6_chiplets_bus.insert(HASHERMPVERIFY, s6, s7, s8, s9) when 1; + # Positions 0-9: Unchanged (node value, depth, index, root all stay on stack) enf s0' = s0; enf s1' = s1; enf s2' = s2; enf s3' = s3; enf s4' = s4; enf s5' = s5; enf s6' = s6; enf s7' = s7; enf s8' = s8; enf s9' = s9; @@ -472,6 +490,14 @@ ev push_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, # Stack behavior: [V0, V1, V2, V3, d, i, R0, R1, R2, R3, NV0, NV1, NV2, NV3, ...] -> [NR0, NR1, NR2, NR3, d, i, R0, R1, R2, R3, NV0, NV1, NV2, NV3, ...] # Updates node from old value V to new value NV, replaces top with new root NR ev mrupdate_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15]) { + # Request Merkle root update from hasher chiplet + # This involves two verifications: + # 1. MV (old path): Verify path from old value V (s0-s3) results in old root R (s6-s9) + # 2. MU (new path): Verify path from new value NV (s10-s13) results in new root NR (s0'-s3') + # The hasher computes the new root and returns it. + bus_6_chiplets_bus.insert(HASHERMRUPDATEOLD, s6, s7, s8, s9) when 1; + bus_6_chiplets_bus.insert(HASHERMRUPDATENEW, s0', s1', s2', s3') when 1; + # Positions 0-3: Overwritten by new root (unconstrained, validated by hash chiplet) # Positions 4-15: Unchanged (depth, index, old root, new value all stay) enf s4' = s4; enf s5' = s5; enf s6' = s6; enf s7' = s7; enf s8' = s8; enf s9' = s9; enf s10' = s10; enf s11' = s11; @@ -1223,6 +1249,11 @@ ev u32and_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s1 enf s1' = s2; enf s2' = s3; enf s3' = s4; enf s4' = s5; enf s5' = s6; enf s6' = s7; enf s7' = s8; enf s8' = s9; enf s9' = s10; enf s10' = s11; enf s11' = s12; enf s12' = s13; enf s13' = s14; enf s14' = s15; # s15' comes from overflow table or is 0 (handled by left_shift_zero_insertion) + + # Insert bitwise AND request to chiplets bus + # Operands: s0 (top of stack), s1 (second element) + # Result: s0' (will contain the AND result) + bus_6_chiplets_bus.insert(BITWISEAND, s0, s1, s0') when 1; } # U32XOR operation: Bitwise XOR of two u32 values @@ -1233,33 +1264,51 @@ ev u32xor_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s1 enf s1' = s2; enf s2' = s3; enf s3' = s4; enf s4' = s5; enf s5' = s6; enf s6' = s7; enf s7' = s8; enf s8' = s9; enf s9' = s10; enf s10' = s11; enf s11' = s12; enf s12' = s13; enf s13' = s14; enf s14' = s15; # s15' comes from overflow table or is 0 (handled by left_shift_zero_insertion) + + # Insert bitwise XOR request to chiplets bus + # Operands: s0 (top of stack), s1 (second element) + # Result: s0' (will contain the XOR result) + bus_6_chiplets_bus.insert(BITWISEXOR, s0, s1, s0') when 1; } # MLOADW operation: Load word from memory at address s4 # Stack behavior: [a, b, c, d, addr, ...] -> [v3, v2, v1, v0, ...] -ev mloadw_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15]) { +ev mloadw_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, system_ctx, system_clk]) { # Positions 0-3: Overwritten by memory word (unconstrained) # Positions 4-14: Left shift enf s4' = s5; enf s5' = s6; enf s6' = s7; enf s7' = s8; enf s8' = s9; enf s9' = s10; enf s10' = s11; enf s11' = s12; enf s12' = s13; enf s13' = s14; enf s14' = s15; + + # Insert memory read word request to chiplets bus + # MLOADW reads a 4-element word from memory address s0 (must be word-aligned) + # The word will be placed in s0', s1', s2', s3' (unconstrained here, but constrained by memory chiplet response) + bus_6_chiplets_bus.insert(MEMREADWORD, system_ctx, s0, system_clk, s0', s1', s2', s3') when 1; } # MSTORE operation: Store element to memory at address s0 # Stack behavior: [addr, value, ...] -> [value, ...] -ev mstore_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15]) { +ev mstore_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, system_ctx, system_clk]) { # Positions 0-14: Left shift by 1 (address consumed, value stays) enf s0' = s1; enf s1' = s2; enf s2' = s3; enf s3' = s4; enf s4' = s5; enf s5' = s6; enf s6' = s7; enf s7' = s8; enf s8' = s9; enf s9' = s10; enf s10' = s11; enf s11' = s12; enf s12' = s13; enf s13' = s14; enf s14' = s15; + + # Insert memory write element request to chiplets bus + # MSTORE writes a single element (s1) to memory address s0 in the current execution context + bus_6_chiplets_bus.insert(MEMWRITEELEMENT, system_ctx, s0, system_clk, s1) when 1; } # MSTOREW operation: Store word to memory at address s0 # Stack behavior: [addr, v0, v1, v2, v3, ...] -> [v0, v1, v2, v3, ...] -ev mstorew_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15]) { +ev mstorew_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, system_ctx, system_clk]) { # Positions 0-14: Left shift by 1 (address consumed, word stays) enf s0' = s1; enf s1' = s2; enf s2' = s3; enf s3' = s4; enf s4' = s5; enf s5' = s6; enf s6' = s7; enf s7' = s8; enf s8' = s9; enf s9' = s10; enf s10' = s11; enf s11' = s12; enf s12' = s13; enf s13' = s14; enf s14' = s15; + + # Insert memory write word request to chiplets bus + # MSTOREW writes a 4-element word (s1, s2, s3, s4) to memory address s0 (must be word-aligned) + bus_6_chiplets_bus.insert(MEMWRITEWORD, system_ctx, s0, system_clk, s1, s2, s3, s4) when 1; } # FRIE2F4 operation: TODO @@ -1310,6 +1359,14 @@ ev loop_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, # s15' comes from overflow table or is 0 (handled by left_shift_zero_insertion) } +# DYN operation: Execute code block dynamically without context switch +ev dyn_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15]) { + # Stack LEFT SHIFT: all elements shift up one position + enf s0' = s1; enf s1' = s2; enf s2' = s3; enf s3' = s4; enf s4' = s5; enf s5' = s6; enf s6' = s7; enf s7' = s8; + enf s8' = s9; enf s9' = s10; enf s10' = s11; enf s11' = s12; enf s12' = s13; enf s13' = s14; enf s14' = s15; + # s15' from overflow table or 0 (handled by left_shift_zero_insertion) +} + ########################################################################################## # NO STACK SHIFT OPERATION CONSTRAINTS (MOVUP/MOVDN) ########################################################################################## @@ -1731,14 +1788,20 @@ ev expacc_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s1 enf s9' = s9; enf s10' = s10; enf s11' = s11; enf s12' = s12; enf s13' = s13; enf s14' = s14; enf s15' = s15; } -# CALLER operation: Get ID of the calling context (no stack depth change) -# Stack behavior: [...] -> [caller_id, ...] (no depth change) -ev caller_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15]) { - # Position 0: Gets caller context ID from system state - # TODO: Integrate with system context columns to get actual caller ID - enf s0' = 0; # Placeholder - needs system context integration - # Positions 1-15: Unchanged (all other elements stay in place) - enf s1' = s1; enf s2' = s2; enf s3' = s3; enf s4' = s4; enf s5' = s5; enf s6' = s6; enf s7' = s7; enf s8' = s8; +# CALLER operation: Get hash of the calling function (no stack depth change) +# Stack behavior: [...] -> [fn_hash[0], fn_hash[1], fn_hash[2], fn_hash[3], ...] (no depth change) +# Loads the function hash (4 elements) from system state onto top of stack +# Note: CALLER can only be executed within a SYSCALL; constraints enforced in system.air +ev caller_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, + fn_hash_0, fn_hash_1, fn_hash_2, fn_hash_3]) { + # Positions 0-3: Load function hash word from system state + enf s0' = fn_hash_0; + enf s1' = fn_hash_1; + enf s2' = fn_hash_2; + enf s3' = fn_hash_3; + + # Positions 4-15: Unchanged (all other elements stay in place) + enf s4' = s4; enf s5' = s5; enf s6' = s6; enf s7' = s7; enf s8' = s8; enf s9' = s9; enf s10' = s10; enf s11' = s11; enf s12' = s12; enf s13' = s13; enf s14' = s14; enf s15' = s15; } @@ -1751,11 +1814,16 @@ ev emit_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, # MLOAD operation: Load word from memory (no stack depth change) # Stack behavior: [addr, ...] -> [mem[addr], ...] (no depth change) -ev mload_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15]) { +ev mload_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, system_ctx, system_clk]) { # Position 0: Overwritten by memory value (unconstrained) # Positions 1-15: Unchanged enf s1' = s1; enf s2' = s2; enf s3' = s3; enf s4' = s4; enf s5' = s5; enf s6' = s6; enf s7' = s7; enf s8' = s8; enf s9' = s9; enf s10' = s10; enf s11' = s11; enf s12' = s12; enf s13' = s13; enf s14' = s14; enf s15' = s15; + + # Insert memory read element request to chiplets bus + # MLOAD reads a single element from memory address s0 in the current execution context + # The value read will be placed in s0' (which is unconstrained here, but constrained by memory chiplet response) + bus_6_chiplets_bus.insert(MEMREADELEMENT, system_ctx, s0, system_clk, s0') when 1; } # ADVPOPW operation: Pop word from advice stack (no stack depth change) @@ -1845,3 +1913,37 @@ ev ext2mul_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s enf s4' = s4; enf s5' = s5; enf s6' = s6; enf s7' = s7; enf s8' = s8; enf s9' = s9; enf s10' = s10; enf s11' = s11; enf s12' = s12; enf s13' = s13; enf s14' = s14; enf s15' = s15; } + +########################################################################################## +# CONTEXT SWITCHING OPERATIONS +########################################################################################## + +# CALL operation: Call a function and start a new execution context +ev call_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, b0, b1]) { + # Stack elements s0-s15 remain unchanged (no shift) + + # Reset stack depth and overflow address for new context + enf b0' = 16; + enf b1' = 0; +} + +# SYSCALL operation: Call kernel function in root context +ev syscall_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, b0, b1]) { + # Stack elements s0-s15 remain unchanged (no shift) + + # Reset stack depth and overflow address for root context + enf b0' = 16; + enf b1' = 0; +} + +# DYNCALL operation: Call function dynamically with hash from memory +ev dyncall_operation_constraints([s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, b0, b1]) { + # Stack LEFT SHIFT: all elements shift up one position + enf s0' = s1; enf s1' = s2; enf s2' = s3; enf s3' = s4; enf s4' = s5; enf s5' = s6; enf s6' = s7; enf s7' = s8; + enf s8' = s9; enf s9' = s10; enf s10' = s11; enf s11' = s12; enf s12' = s13; enf s13' = s14; enf s14' = s15; + # s15' from overflow table or 0 (handled by left_shift_zero_insertion) + + # Reset stack depth and overflow address for new context + enf b0' = 16; + enf b1' = 0; +} diff --git a/constraints/utils.air b/constraints/utils.air index 5af593a2c..4ca9df3e8 100644 --- a/constraints/utils.air +++ b/constraints/utils.air @@ -140,3 +140,36 @@ fn binary_xor(a: felt, b: felt) -> felt { fn select(condition: felt, if_true: felt, if_false: felt) -> felt { return condition * (if_true - if_false) + if_false; } + +########################################################################################## +# OPERATION LABELS +########################################################################################## + +# Operation labels for bus communication +# +########################################################################################## + +# Hasher Chiplet Operation Labels +const HASHERLINEARHASH = 3; # Linear hash of n elements +const HASHERMPVERIFY = 11; # Merkle path verification +const HASHERMRUPDATEOLD = 7; # Merkle root update (old path) +const HASHERMRUPDATENEW = 15; # Merkle root update (new path) +const HASHERRETURNHASH = 1; # Return hash result (positions 4-7) +const HASHERRETURNSTATE = 9; # Return full state (all 12 elements) + +# Bitwise Chiplet Operation Labels +const BITWISEAND = 2; # Bitwise AND of two u32 values +const BITWISEXOR = 6; # Bitwise XOR of two u32 values + +# Memory Chiplet Operation Labels +const MEMWRITEELEMENT = 4; # Element write operation (1 element) +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 + +# Kernel ROM Chiplet Operation Labels +const KERNELPROCCALL = 16; # Kernel procedure call +const KERNELPROCINIT = 48; # Kernel procedure initialization