# Vamp-IR workshop at zkSummit9

**Title**:
- LLVM for polynomial circuits (*now with benchmarks!*)

**Primary purpose**:
- Give a practical introduction to Vamp-IR

**Secondary purposes**:
- Explain what is useful about Vamp-IR
- Explain the differences between Vamp-IR and other ZK languages
- Give an update about the status of Vamp-IR
- Show where to get more information or participate

**Audience**:
- ZK developers
- likely aware of ZK languages and proving systems
- varied understanding of underlying circuits

## Format
(waiting for zkSummit team to confirm the room layout, but the following should work with any room)

- Introduction
- slides
- Main workshop
- live coding with Vamp-IR on my device
- audience members can follow along on their own devices if they wish
- slides available as a backup plan
- Conclusion
- more slides

## Outline
1. Introduction
1. My name and company
2. What is Vamp-IR?
1. slide: show vamp-ir with many-in-many-out diagram from earlier talks, updated with new targets (Noir/ACIR, ???/AirScript)
3. What makes Vamp-IR different from other ZK languages?
1. slide: (same slide as earlier?)
4. Why make Vamp-IR?
1. slide: show MASP diagram from previous talks
2. Elements of the language
1. brief primer on circuits as representations of systems of polynomials
1. slide: show circuit boards as polynomials from previous talks
2. `def`
1. slide: small example
2. mention typing: `def` can append constraints and/or return a value
3. `fresh`
1. slide: small example
2. mention dangers of `fresh` -- it does not add constraints!
3. mention possibility of removing `fresh` or separating it from the circuit
5. tuples
1. slide: small example
6. lists
1. slide: small example
7. mapping
1. slide: small example
8. folding
1. slide: small example
9. iterating
1. slide: small example
10. putting it all together
1. slide: all examples combined into one functional circuit
3. Compiling, Proving, Verifying
1. Compile (halo2)
2. Prove (halo2)
3. Verify (halo2)
4. Prove with incorrect inputs (halo2)
5. Verify showing error (halo2)
6. Briefly show Setup, Compile, Prove, Verify using plonkup
4. Status and future
1. Frontends (current and future)
1. Current
1. (Juvix -> Geb)
2. Future
1. Noir (via ACIR)
2. Zokrates
3. Circom
4. Others???
2. Backends (current and future)
1. Current
1. Halo2
2. Plonkup (zk-garage/plonk)
2. Future
1. "AirScript prover" (via AirScript) (What is the prover’s name? Winterfell?)
2. "Aztec prover" (via ACIR) (What is the prover’s name? Barrattenberg?)
3. Others???
3. Optimizations
1. Tree-matching for conversion between constraint formats
2. Assistance from SMT solvers
1. Are these circuits equivalent?
2. Is there a more efficient version of this circuit component?
3. Assistance with solving/evaluation?
4. Benchmarks
5. Thanks and closing remarks
1. Where to get more information about Vamp-IR
1. Github
2. Vamp-IR book
3. Discord
2. Thanks for coming

def bool x = {
    x^2 = x;
    x
}

// x is 2 bits
def range_2 x {
    def b0 = fresh(x%2);
    def b1 = fresh(x\2);
    bool b0;
    bool b1;
    x = b0 + 2*b1;
    x
}

def range_3 x {
    def b0 = fresh(x%2);
    bool b0;
    def rest = fresh(x\2);
    range_2 rest;
    x = b0 + 2*rest;
    x
}

def range_4 x {
    def b0 = fresh(x%2);
    bool b0;
    def rest = fresh(x\2);
    range_3 rest;
    x = b0 + 2*rest;
    x
}

range_4 y;