Write hasher multiset check constraints in AirScript

constraints/miden-vm/hash.air

@@ -10,51 +10,64 @@ periodic_columns:
 
 ### 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,0) on rows which are multiples of 8. This flag indicates 
+# that we are initiating computation of a single permutation, a 2-to-1 hash, or a linear hash of 
+# many elements.
+fn get_f_bp(s: vector[3]) -> scalar:
+    return cycle_row_0 & s[0] & !s[1] & !s[2]
 
 
-# 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.
+# 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]
+    return cycle_row_0 & s[0] & !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.
+# 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])
+    return cycle_row_0 & s[0] & s[1] & !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.
+# 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 (0,0,0) on rows which are 1 less than a multiple of 8. This flag
+# indicates that the result of the currently running computation is returned.
+fn get_f_hout(s: vector[3]) -> scalar:
+    return cycle_row_7 & !s[0] & !s[1] & !s[2]
+
+
+# Set to 1 when selector flags are (0,0,1) on rows which are 1 less than a multiple of 8. This flag
+# indicates that the entire hasher state is returned.
+fn get_f_sout(s: vector[3]) -> scalar:
+    return cycle_row_7 & !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])
+    return cycle_row_7 & s[0] & !s[1] & !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]
+    return cycle_row_7 & s[0] & !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])
+    return cycle_row_7 & s[0] & s[1] & !s[2]
 
 
 # Set to 1 when selector flags are (1,1,1) on rows which are 1 less than a multiple of 8. This 
@@ -65,41 +78,38 @@ 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])
-
+    return cycle_row_7 & !s[0] & !s[1]
 
-# Flag f_out_next is set to 1 when either f_hout = 1 or f_sout = 1 in the next row.
+# Flag f_out is set to 1 when either f_hout = 1 or f_sout = 1 in the next row. Notice that this 
+# function should be used only with next row values (s'),
 fn get_f_out_next(s: vector[3]) -> scalar:
-    return cycle_row_6 & binary_not(s[0]') & binary_not(s[1]')
+    return cycle_row_6 & !s[0] & !s[1]
 
 
 ### Helper evaluators #############################################################################
 
 # Enforces that column must be binary.
-ev is_binary(main: [a]):
+#
+# Constraint degree: 2
+ev is_binary([a]):
     enf a^2 = a
 
 
 # Enforces that value in column is copied over to the next row.
-ev is_unchanged(main: [column]):
+#
+# Constraint degree: 1
+ev is_unchanged([column]):
     ev column' = column
 
 
-# Enforce selector columns constraints
-ev selector_columns(main: [s[3]]):
+# Enforce selector columns constraints.
+#
+# Max constraint degree: 7
+ev selector_columns([s[3]]):
     let f_out = get_f_out(s)
-    let f_out_next = get_f_out_next(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)
@@ -110,23 +120,29 @@ ev selector_columns(main: [s[3]]):
     let f_comp = f_abp + f_mpa + f_mva + f_mua
 
     # Enforce that selector columns are binary.
+    # Constraint degree: 2
     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.
+    # Constraints degree: 7
     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.
+    # Constraint degree: 5
     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
+    # Constraint degree: 3
+    enf cycle_row_7 * !s[0] * s[1] = 0
 
 
-# Enforce node index constraints
-ev node_index(main: [s[3], i]):
+# Enforce node index constraints.
+#
+# Max constraint degree: 6
+ev node_index([s[3], i]):
     let f_out = get_f_out(s)
     let f_mp = get_f_mp(s)
     let f_mv = get_f_mv(s)
@@ -144,19 +160,24 @@ ev node_index(main: [s[3], i]):
     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.
+    # Constraint degree: 6
     enf f_an * (b^2 - b) = 0
 
     # Enforce that when a computation is finished i = 0.
+    # Constraint degree: 4
     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.
+    # Constraint degree: 5
     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]):
+#
+# Max constraint degree: 6
+ev hasher_state([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)
@@ -172,20 +193,62 @@ ev hasher_state(main: [s[3], h[12], 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.
+    # Constraint degree: 5
     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.
+    # Constraint degree: 6
     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
 
 
+# Enforce constraints for the hash chiplet sibling table, which is used to keep track of sibling 
+# nodes used during Merkle root update computations. For this computation, we need to enforce the 
+# following rules:
+# 1. When computing the old Merkle root, whenever a new sibling node is absorbed into the hasher 
+#    state (i.e., f_mv + f_mva = 1), an entry for this sibling should be included into p1.
+# 2. When computing the new Merkle root, whenever a new sibling node is absorbed into the hasher 
+#    state (i.e., f_mu + f_mua = 1), the entry for this sibling should be removed from p1.
+#
+# Max constraint degree: 7
+ev hash_sibling_table([s[3], r, h[12], i], [p1]):
+    # Compute falgs required for the sibling table constraints.
+    let f_mv = get_f_mv(s)
+    let f_mu = get_f_mu(s)
+    let f_mva = get_f_mva(s)
+    let f_mua = get_f_mua(s)
+    let f_bp = get_f_bp(s)
+    let f_mp = get_f_mp(s)
+
+    # b is the value of the bit which is discarded during shift by one bit to the right.
+    let b = i - 2 * i'
+
+    let v_b = sum([$alpha[j + 4] * h[j] for j in 4..8])
+    let v_c = sum([$alpha[j + 4] * h[j] for j in 8..12])
+
+    # v_sibling represents an entry in the sibling table.
+    let v_sibling = $alpha[0] + $alpha[3] * i + b * v_b + (1 - b) * v_c
+
+    # Enforce constraint for updating p1.
+    # Constraint degree: 7
+    enf p1' * ((f_mv + f_mva) * v_sibling + 1 - (f_mv + f_mva)) = 
+        p1 * ((f_mu + f_mua) * v_sibling + 1 - (f_mu + f_mua))
+
+    # Enforce that computation of the old Merkle root is immediately followed by the computation of 
+    # the new Merkle root.
+    # Constraint degree: 5
+    enf (f_bp + f_mp + f_mv) * (1 - p1) = 0
+
+
 ### 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]):
+#
+# Max constraint degree: 7
+ev hash_chiplet([s[3], r, h[12], i], [p1]):
     ## Row address constraint ##
     # TODO: Apply row address constraints:
     # 1. Boundary constraint `enf r.first = 1`
@@ -201,5 +264,6 @@ ev hash_chiplet(main: [s[3], r, h[12], i]):
     # TODO: apply RPO constraints to the hasher state
     enf hasher_state([s, h, i])
 
-    # Multiset check constraints
-    # TODO: Apply multiset check constraints
+    ## Multiset check constraints ##
+    # Chiplet bus constraints are implemented in the separate file.
+    enf hash_sibling_table([s, r, h, i], [p1])