Tracking issue: write Miden VM constraints in AirScript

[grjte]

Goal(s)

• write a core subset of Miden VM constraints in AirScript

Details

While we don't expect to be able to define all Miden VM constraints in AirScript by the 2023/03/28 milestone, we want to support a core subset of them so that the full recursive verification pipeline is in place.

The constraints are all described in the Miden VM docs, and some of them are also implemented in Rust.

The first thing we need to do is identify which constraints we will aim to write in AirScript for this milestone.

### Must have
- [x] Choose which MidenVM constraints should be written as "must haves" for this target
- [ ] https://github.com/0xPolygonMiden/air-script/issues/176
- [ ] https://github.com/0xPolygonMiden/air-script/issues/178
- [ ] https://github.com/0xPolygonMiden/air-script/issues/182
- [ ] https://github.com/0xPolygonMiden/air-script/issues/201
- [ ] https://github.com/0xPolygonMiden/air-script/issues/202
- [ ] https://github.com/0xPolygonMiden/air-script/issues/205
- [ ] https://github.com/0xPolygonMiden/air-script/issues/206
- [ ] https://github.com/0xPolygonMiden/air-script/issues/207
- [ ] https://github.com/0xPolygonMiden/air-script/issues/208
- [ ] https://github.com/0xPolygonMiden/air-script/issues/209
- [ ] https://github.com/0xPolygonMiden/air-script/issues/212

### Nice to have
  - [ ] stack: crypto ops
  - [ ] stack: field ops
  - [ ] stack: io ops
  - [ ] stack: stack manipulation
  - [ ] stack: system ops
  - [ ] https://github.com/0xPolygonMiden/air-script/issues/199
  - [ ] decoder: block hash computation constraints
  - [ ] decoder: block hash table constraints (includes multiset checks for virtual table)
  - [ ] decoder: span block constraints (includes multiset checks for virtual table)
- [ ] https://github.com/0xPolygonMiden/air-script/issues/203
- [ ] https://github.com/0xPolygonMiden/air-script/issues/204
- [ ] https://github.com/0xPolygonMiden/air-script/issues/200
- [ ] https://github.com/0xPolygonMiden/air-script/issues/209
- [ ] https://github.com/0xPolygonMiden/air-script/issues/209
- [ ] https://github.com/0xPolygonMiden/air-script/issues/211
- [ ] https://github.com/0xPolygonMiden/air-script/issues/211

Working group:

@Al-Kindi-0, @grjte, @Overcastan, @tohrnii

Workflow

- Discussion should happen here or in the related sub-issues. - PRs should only be merged by the coordinator, to ensure everyone is able to review. - Aim to complete reviews within 24 hours. - When a related sub-issue is opened: - add it to the list of sub-issues in this tracking issue - When opening a related PR: - request review from everyone in this working group - When a sub-issue is completed: - close the related issue with a comment that links to the PR where the work was completed

Coordinator: @tohrnii

The working group coordinator ensures scope & progress tracking are transparent and accurate. They will: - Merge approved PRs after all working group members have completed their reviews. - add the PR # to the relevant section of the current tracking PR. - close any completed sub-issue(s) with a comment that links to the PR where the work was completed - Monitor workflow items and complete anything that slips through the cracks. - Monitor scope to see if anything is untracked or unclear. Create missing sub-issues or initiate discussion as required. - Monitor progress to see if there's anything which isn't moving forward. Initiate discussion as required. - Identify PRs with especially significant changes and add @grjte and @bobbinth for review.

[grjte]

1. Which of the sets of constraints do we want to move to the "must have" section for this target?
2. Do we want to break any of these down further into smaller issues?

Once we've decided on (2) we can turn each of these items into an issue.

[grjte]

My general opinion is that it makes sense to write the constraints that we have already written in Rust in the VM, since this gives us a point of comparison for correctness, and we also already have some integration tests in the VM for those constraints.

That would include the following:

• chiplets: module (skip multiset checks)
  • chiplets: bitwise
  • chiplets: hasher (skip multiset checks)
  • chiplets: memory
• range checker (includes multiset checks for bus and for virtual table)
• stack: top level + op flag handling
  • stack: field ops
  • stack: io ops
  • stack: overflow (skip multiset checks)
  • stack: stack manipulation
  • stack: system ops
  • stack: u32 ops

We may want to reduce the number of stack constraints that we try to do, and we may want to consider including some of the multiset checks that weren't implemented in Rust yet. However, the multiset checks could be done subsequently as separate tasks.