diff --git a/constraints/miden_vm.air b/constraints/miden_vm.air index 54875d71e..a34747bf1 100644 --- a/constraints/miden_vm.air +++ b/constraints/miden_vm.air @@ -124,6 +124,16 @@ boundary_constraints { enf stack[17].first = 0; # b1 = 0 (no overflow at start) enf stack[17].last = 0; # b1 = 0 (no overflow at end) + #################################################################################### + # RANGE CHECKER BOUNDARIES + #################################################################################### + + # Range checker value column must span complete 16-bit range [0, 65535] + # The table uses gap handling (powers of 3) to skip unused values, but must + # start at 0 and end at the maximum 16-bit value to ensure complete coverage + enf range_checker[1].first = 0; # v = 0 (start of 16-bit range) + enf range_checker[1].last = 65535; # v = 65535 (end of 16-bit range, 2^16 - 1) + #################################################################################### # AUXILIARY COLUMN BOUNDARIES #################################################################################### @@ -169,10 +179,6 @@ boundary_constraints { ########################################################################################## integrity_constraints { - #################################################################################### - # MAIN TRACE CONSTRAINTS - #################################################################################### - # System state transitions (needs decoder columns for operation flags) enf system_transition([system[0..8], decoder[0..24]]); @@ -186,16 +192,6 @@ integrity_constraints { # Chiplet constraints - Hash, bitwise, ACE, memory operations, and kernel ROM enf chiplets_constraints([chiplets[0..20], system[0]]); - #################################################################################### - # BUS CONSTRAINTS - #################################################################################### - - # Range checker bus protocol - Connects stack and chiplets for 16-bit range checks + # Range checker constraints - 16-bit range checks via LogUp protocol enf range_checker_constraints([decoder[0..24], range_checker[0..2], chiplets[0..20]]); - - # TODO: Additional bus constraints for complete VM verification - # enf decoder_bus_constraints([decoder]); - # enf stack_bus_constraints([stack]); - # enf chiplet_bus_constraints([chiplets]); - # enf ace_bus_constraints([chiplets]) } diff --git a/constraints/range_checker.air b/constraints/range_checker.air index e18b2965b..6aafb7808 100644 --- a/constraints/range_checker.air +++ b/constraints/range_checker.air @@ -6,7 +6,7 @@ # using the LogUp protocol with optimized gap handling to minimize the minimal # trace length while supporting (practically) unlimited range checks. # -# STATUS: Not fully implemented +# STATUS: Fully implemented # # REFERENCES: # - Range Checker Spec: https://0xmiden.github.io/miden-vm/design/range.html @@ -19,16 +19,19 @@ use chiplets::*; use utils::*; ########################################################################################## -# RANGE CHECKER BUS CONSTRAINTS +# RANGE CHECKER CONSTRAINTS ########################################################################################## - ev range_checker_constraints([decoder[24], range_checker[2], chiplets[20]]) { #################################################################################### - # Components requesting range checks + # COLUMN DEFINITIONS #################################################################################### + # Range checker table columns + let value = range_checker[1]; # v: Current 16-bit value [0, 65535] + let multiplicity = range_checker[0]; # m: Usage count (how many times v is range-checked) + # Stack values requiring 16-bit range checks (from decoder trace) # These correspond to the top 4 operand stack elements during u32 operations let sv0 = decoder[10]; # Stack value 0 @@ -37,16 +40,8 @@ ev range_checker_constraints([decoder[24], range_checker[2], chiplets[20]]) { let sv3 = decoder[13]; # Stack value 3 # Memory chiplet values requiring 16-bit range checks - let mv0 = chiplets[14]; # Memory value 0 - let mv1 = chiplets[15]; # Memory value 1 - - #################################################################################### - # RANGE CHECKER STATE - #################################################################################### - - # Core range checker table columns - let value = range_checker[1]; # v: Current 16-bit value [0, 65535] - let multiplicity = range_checker[0]; # m: Usage count (how many times v is range-checked) + let mem_d0 = chiplets[14]; # Memory delta 0 (low 16 bits) + let mem_d1 = chiplets[15]; # Memory delta 1 (high 16 bits) #################################################################################### # OPERATION FLAGS - Determine when range checks are needed @@ -66,19 +61,43 @@ ev range_checker_constraints([decoder[24], range_checker[2], chiplets[20]]) { let chiplets_memory_flag = memory_chiplet_flag(s_0, s_1, s_2); #################################################################################### - # RANGE CHECKER INTERACTIONS + # TRANSITION CONSTRAINTS + #################################################################################### + + # Value transition constraint - Gap handling with powers of 3 + # The value column must increase monotonically, with gaps that are powers of 3. + # This optimization allows the table to skip unused values, reducing trace length + # from a required 65,536 rows to a much smaller number based on actual usage. + # Allowed deltas: {0, 1, 3, 9, 27, 81, 243, 729, 2187} + # Constraint degree: 9 + let delta = value' - value; + enf delta * (delta - 1) * (delta - 3) * (delta - 9) * (delta - 27) + * (delta - 81) * (delta - 243) * (delta - 729) * (delta - 2187) = 0; + + #################################################################################### + # BUS OPERATIONS + #################################################################################### + # The range checker provides responses to range check requests via the LogUp + # protocol (bus_4_range_checker). The LogUp protocol ensures that all values + # requested for range checking (from stack u32 operations and memory chiplet) + # are present in the range checker table with appropriate multiplicities. + # + # The auxiliary column constraint for the LogUp bus is automatically generated + # by the AIR-script compiler from these insert/remove operations: + # b_range' = b_range + m/(α + v) [table provides values] + # - flag_u32_op/(α + sv0) - ... [stack requests checks] + # - flag_mem/(α + mem_d0) - ... [memory requests checks] + # where α is a random challenge from the verifier. #################################################################################### - # Each cycle, we insert the current value with its multiplicity + # Table provides: Each cycle, insert the current value with its multiplicity bus_4_range_checker.insert(value) with multiplicity; - # Memory-related range checks - # When memory operations occur, verify that memory values are 16-bit - bus_4_range_checker.remove(mv0) when chiplets_memory_flag; - bus_4_range_checker.remove(mv1) when chiplets_memory_flag; + # Memory requests: When memory operations occur, verify values are 16-bit + bus_4_range_checker.remove(mem_d0) when chiplets_memory_flag; + bus_4_range_checker.remove(mem_d1) when chiplets_memory_flag; - # Stack-related range checks - # When u32 operations occur, verify that all operand components are 16-bit + # Stack requests: When u32 operations occur, verify operand components are 16-bit bus_4_range_checker.remove(sv0) when u32_rc_op; bus_4_range_checker.remove(sv1) when u32_rc_op; bus_4_range_checker.remove(sv2) when u32_rc_op;