Skip to content

Complete range checker #499

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
Al-Kindi-0 wants to merge 1 commit into
base: al-decoder-virtual-tables-v2
Choose a base branch
from
Open

Complete range checker #499

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
26 changes: 11 additions & 15 deletions constraints/miden_vm.air
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
####################################################################################
Expand Down Expand Up @@ -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]]);

Expand All @@ -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])
}
63 changes: 41 additions & 22 deletions constraints/range_checker.air
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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;
Expand Down