Update and move hasher chiplet constraints

CHANGELOG.md

@@ -8,6 +8,7 @@
 - Refactored the unrolling pass in MIR (#434).
 - Fix regressions on MIR and list_comprehensions (#449).
 - Update documentation and tests thereof (#437).
+- Create initial structure for writing Miden VM constraints (#464).
 
 ## 0.4.0 (2025-06-20)
 

Cargo.toml

@@ -8,6 +8,7 @@ members = [
     "air",
     "codegen/winterfell",
     "codegen/ace",
+    "constraints",
 ]
 resolver = "2"
 

air-script/Cargo.toml

@@ -26,6 +26,7 @@ env_logger = "0.11"
 log = { version = "0.4", default-features = false }
 miden-diagnostics = { workspace = true }
 mir = { package = "air-mir", path = "../mir", version = "0.5" }
+miden-core = { package = "miden-core", version = "0.13", default-features = false }
 
 [dev-dependencies]
 expect-test = "1.4"
@@ -35,3 +36,4 @@ winter-utils = { package = "winter-utils", version = "0.12", default-features =
 winter-prover = { package = "winter-prover", version = "0.12", default-features = false }
 winter-verifier = { package = "winter-verifier", version = "0.12", default-features = false }
 winterfell = { package = "winterfell", version = "0.12", default-features = false }
+air-codegen-ace = { path = "../codegen/ace", version = "0.5" }

constraints/Cargo.toml

@@ -0,0 +1,23 @@
+[package]
+name = "constraints"
+version = "0.1.0"
+edition = "2021"
+
+[dependencies]
+air-ir = { path = "../air", version = "0.5" }
+air-parser = { path = "../parser", version = "0.5" }
+air-pass = { path = "../pass", version = "0.5" }
+air-mir = { path = "../mir", version = "0.5" }
+air-codegen-ace = { path = "../codegen/ace", version = "0.5" }
+miden-diagnostics = { workspace = true }
+miden-core = { package = "miden-core", version = "0.13", default-features = false }
+
+winter-air = { package = "winter-air", version = "0.12", default-features = false }
+winter-math = { package = "winter-math", version = "0.12", default-features = false }
+winter-utils = { package = "winter-utils", version = "0.12", default-features = false }
+winter-prover = { package = "winter-prover", version = "0.12", default-features = false }
+winter-verifier = { package = "winter-verifier", version = "0.12", default-features = false }
+winterfell = { package = "winterfell", version = "0.12", default-features = false }
+
+[dev-dependencies]
+anyhow = "1"

constraints/bitwise.air

@@ -0,0 +1,69 @@
+##########################################################################################
+# BITWISE OPERATIONS CHIPLET
+##########################################################################################
+#
+# The Bitwise chiplet handles bitwise logical operations (AND, XOR) on 32-bit values.
+# It decomposes field elements into their binary representation and performs bit-level
+# operations efficiently using field arithmetic.
+#
+# STATUS: Not implemented
+#
+# REFERENCES:
+# - Bitwise Chiplet: https://0xmiden.github.io/miden-vm/design/chiplets/bitwise.html
+##########################################################################################
+
+mod bitwise
+
+##########################################################################################
+# BITWISE OPERATION CONSTANTS (Periodic Columns)
+##########################################################################################
+#
+# Periodic constants contain values needed to switch various constraints on or off.
+#
+periodic_columns {
+    k0: [1, 0, 0, 0, 0, 0, 0, 0],
+    k1: [1, 1, 1, 1, 1, 1, 1, 0],
+}
+
+##########################################################################################
+# BITWISE CHIPLET TRANSITION CONSTRAINTS
+##########################################################################################
+#
+# The bitwise chiplet processes 32-bit integers by decomposing them into individual
+# bits, applying bitwise operations, and recomposing the results. This approach
+# enables verification of bitwise logic within the field arithmetic constraint system.
+#
+# PLANNED CONSTRAINT EVALUATORS:
+#
+# ev bitwise_decomposition([bitwise[16]]) {
+#     
+#     # TODO
+#     
+# }
+#
+# ev bitwise_aggregation([bitwise[16]]) {
+#     
+#     # TODO
+#     
+# }
+#
+# ev bitwise_selectors([bitwise[16]]) {
+#     
+#     # TODO
+#
+# }
+#
+##########################################################################################
+# BUS CONSTRAINTS
+##########################################################################################
+#
+# The bitwise chiplet communicates with the stack component using the chiplets bus.
+#
+# MESSAGE FORMAT:
+#
+# Each bitwise operation message contains:
+# - Operation type (AND/XOR)
+# - Input operands (a, b) as 32-bit values
+# - Expected result (c)
+#
+##########################################################################################

constraints/chiplets.air

@@ -0,0 +1,110 @@
+##########################################################################################
+# CHIPLETS CONSTRAINTS MODULE
+##########################################################################################
+#
+# The Chiplets module contains specialized computation units that handle complex operations
+# like cryptographic hashing, bitwise operations, and memory access. Each chiplet uses a
+# hierarchical selector system to identify which operations are active.
+#
+# CHIPLETS COLUMN LAYOUT (20 columns):
+# ┌─────────┬──────────────────────────────────────────────────────────────────────┐
+# │ Columns │                        Purpose                                       │
+# ├─────────┼──────────────────────────────────────────────────────────────────────┤
+# │   0-4   │ s[5] - Hierarchical selector flags                                   │
+# │  5-19   │ Chiplet-specific data (hasher, bitwise ops, memory, ACE, kernel ROM) │
+# └─────────┴──────────────────────────────────────────────────────────────────────┘
+#
+# STATUS: Not fully implemented
+#
+# REFERENCES:
+# - Chiplets Design: https://0xmiden.github.io/miden-vm/design/chiplets/main.html
+##########################################################################################
+
+mod chiplets
+
+use utils::*;
+
+##########################################################################################
+# CHIPLETS CONSTRAINTS
+##########################################################################################
+
+ev chiplets_constraints([chiplets[20]]) {
+    enf chiplet_selectors([chiplets[0..5]]);
+
+    let hash_active = hasher_chiplet_flag(chiplets[0]);
+    let bitwise_active= bitwise_chiplet_flag(chiplets[0], chiplets[1]);
+    let memory_active = memory_chiplet_flag(chiplets[0], chiplets[1], chiplets[2]);
+    let ace_active = ace_chiplet_flag(chiplets[0], chiplets[1], chiplets[2], chiplets[3]);
+    let ker_rom_active = ker_rom_chiplet_flag(chiplets[0], chiplets[1], chiplets[2], chiplets[3], chiplets[4]);
+
+    enf chiplets[0] = 0;
+    #enf match {
+        #case hash_active: hash_chiplet_constraints([chiplets[1..20]]),
+        #case bitwise_active: bitwise_chiplet_constraints([chiplets[2..20]]),
+        #case memory_active: memory_chiplet_constraints([chiplets[0..18]]),
+        #case ace_active: ace_chiplet_constraints([chiplets[0], chiplets[1], chiplets[2], chiplets[3], chiplets[4..20]]),
+        #case ker_rom_active: ker_rom_chiplet_constraints([chiplets[5..20]]),
+    #};
+}
+
+##########################################################################################
+# CHIPLET SELECTOR SYSTEM
+##########################################################################################
+
+# Hierarchical chiplet selector constraints
+#
+# CONSTRAINT DEGREE: 2 (quadratic due to binary constraints)
+#
+ev chiplet_selectors([s[5]]) {
+    ####################################################################################
+    # BINARY CONSTRAINTS - Ensure all selectors are valid binary values
+    ####################################################################################
+
+    enf is_binary([s[0]]);
+
+    enf is_binary([s[1]]) when s[0];
+    enf is_binary([s[2]]) when s[0] & s[1];
+    enf is_binary([s[3]]) when s[0] & s[1] & s[2];
+    enf is_binary([s[4]]) when s[0] & s[1] & s[2] & s[3];
+
+    ####################################################################################
+    # STABILITY CONSTRAINTS - Prevent deactivation (forbids 1→0 transitions)
+    ####################################################################################
+
+    # Once a selector level becomes active (1), it must remain active
+    # This ensures chiplet operations maintain consistent state throughout execution
+    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];
+    enf s[3]' = s[3] when s[0] & s[1] & s[2] & s[3];
+    enf s[4]' = s[4] when s[0] & s[1] & s[2] & s[3] & s[4];
+}
+
+##########################################################################################
+# CHIPLET FLAG COMPUTING
+##########################################################################################
+
+# Hasher chiplet identification function
+fn hasher_chiplet_flag(s_0: felt) -> felt {
+    return !s_0;
+}
+
+# Bitwise chiplet identification function
+fn bitwise_chiplet_flag(s_0: felt, s_1: felt) -> felt {
+    return s_0 * !s_1;
+}
+
+# Memory chiplet identification function
+fn memory_chiplet_flag(s_0: felt, s_1: felt, s_2: felt) -> felt {
+    return s_0 * s_1 * !s_2;
+}
+
+# ACE chiplet identification function
+fn ace_chiplet_flag(s_0: felt, s_1: felt, s_2: felt, s_3: felt) -> felt {
+    return s_0 * s_1 * s_2 * !s_3;
+}
+
+# Kernel ROM chiplet identification function
+fn ker_rom_chiplet_flag(s_0: felt, s_1: felt, s_2: felt, s_3: felt, s_4: felt) -> felt {
+    return s_0 * s_1 * s_2 * s_3 * !s_4;
+}

constraints/decoder.air

@@ -0,0 +1,14 @@
+##########################################################################################
+# DECODER CONSTRAINTS
+##########################################################################################
+#
+# Miden VM program decoder is responsible for ensuring that a program with a given MAST
+# root is executed by the VM.
+#
+# STATUS: Not implemented
+#
+# REFERENCES:
+# - Decoder Design: https://0xmiden.github.io/miden-vm/design/decoder/main.html
+##########################################################################################
+
+mod decoder