0xMiden / 0xMiden/air-script

Miden VM Constraints Implementation in AirScript DSL

Open
#455 2 comments 2 reactions 0 assignees View on GitHub
Dominant language
Rust
Stars
96
Forks
39
PR merge metrics
No merged PRs in 30d

Description

## Overview

This issue tracks the migration and implementation of Miden VM constraints in order to use the AirScript DSL. The constraints will be organized in separate modules corresponding to different VM components, building upon previous work while addressing syntax changes and constraints updates.

## Background

Several PRs have been opened previously to implement Miden VM constraints in AirScript:
- #239
- #249
- #250
- #257
- #261
- #272

These PRs require updates due to:
- **Syntax changes** in AirScript
- **Minor constraint logic updates** in Miden VM

## Project Scope

### Module Organization

The constraints will be organized by VM components into separate AirScript modules:

1. **Decoder Module** - Instruction decoding constraints
2. **Stack Module** - Stack operation constraints
3. **Chiplets Module** - These are:
- ACE chiplet
- Hash chiplet
- Bitwise chiplet
- Memory chiplet
- Kernel ROM chiplet
4. **System Module** - Program counter and flow control constraints
5. **Range Checker Module** - Value range validation constraints

### Tasks

#### Task 1: Module Structure Definition
- [ ] #463

#### Task 2: Update Existing Constraints
- [ ] #465
- [ ] #467

#### Task 3: Update Existing PRs
- [ ] **Update PR #239**
- [ ] **Update PR #249**
- [ ] **Update PR #250**
- [ ] **Update PR #257**
- [ ] **Update PR #261**
- [ ] **Update PR #272**

#### Task 4: Implement Missing Constraints

## Implementation Guidelines

To minimize bugs and facilitate audits, all contributors should follow these principles:

### Code Organization
- **Modular structure**: Each VM component should have its own constraint module
- **Logical grouping**: Group related constraints together within modules and avoid mixing constraints from different components, when possible

### Documentation Standards
- **Comprehensive comments**: Every constraint should have clear documentation explaining its purpose and linking to the appropriate place where it is defined in the VM docs
- **Mathematical descriptions**: Include the mathematical formula and/or rationale behind mathematically-heavy constraints

### Testing Requirements
- **Constraint correctness**: Every constraint must have tests validating correct behavior
- **Edge case coverage**: Test boundary conditions and error cases

### Review Process
- **Mathematical review**: All constraint logic should be reviewed by someone familiar with the underlying mathematics, most probably from the core Miden team
- **Code review**: Standard code review for syntax, organization, and documentation, most probably from MassaLabs
- **Testing validation**: Verify that adequate test coverage exists and passes
- **Documentation check**: Ensure all constraints are properly documented

### Best Practices
- **Incremental changes**: Make small, focused changes that are easy to review

Contributor guide

Open the contributing guide

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.