Skip to content

feat: simplify lookups #2114

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

Merged
DavePearce merged 1 commit into from
Aug 7, 2026
Merged

feat: simplify lookups #2114

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
110 changes: 50 additions & 60 deletions CLAUDE.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,36 +30,35 @@ make install
### Running specific test subsets

The test targets vary widely in runtime — pick the smallest set that covers
your change to keep the iteration loop tight. The slow targets (`asm-unit`,
`asm-bench`, `corset-test`) will exceed the default 2-minute `go test`
your change to keep the iteration loop tight. The slow targets (`corset-test`,
`zkc-unit-test`, the benchmarks) will exceed the default 2-minute `go test`
timeout if invoked directly, which is why the Makefile passes `--timeout 0`.

```shell
# ZkC compiler/VM tests — Test_ZkcBench|Test_ZkcUnit|Test_ZkcInvalid (fast)
make zkc-test
# ZkC compiler/VM tests — Test_ZkcUnit|Test_ZkcMixed|Test_ZkcInvalid (slow)
make zkc-unit-test
make zkc-util-test # go test -run "Test_ZkcUtil"
make zkc-bench-test # go test -run "Test_ZkcBench"

# Cheap "everything else" — skips Asm/Bench/Corset/Zkc system tests (fast)
# Cheap "everything else" — skips Bench/Corset/Zkc system tests (fast)
make unit-test

# Corset constraint tests (valid/invalid/agnostic) — slow (minutes)
make corset-test # go test -run "Test_Agnostic|Test_Valid|Test_Invalid"

# Assembly tests — slow; Test_AsmUnit_ByteShift alone takes ~2+ min
make asm-unit # go test -run "Test_AsmInvalid|Test_AsmUnit"
make asm-util # go test -run "Test_AsmUtil"
make asm-bench # go test -run "Test_AsmBench" (slowest; -p 1)
make corset-bench # go test -run "Test_Bench" (slowest; -p 1)

# Run a single named test
go test --timeout 0 -run "Test_Valid_Basic_01" ./pkg/test/...

# Run tests with race detection
make asm-racer
make corset-racer
make zkc-racer-test
```

When iterating on ZkC changes (e.g. `pkg/zkc/...`), `make zkc-test` is the
relevant target — `make asm-unit` will not exercise ZkC code and is too slow
for a quick check. Combining `Test_ZkcUnit|Test_AsmUnit` in a single
`go test -run` invocation will time out at the default 2-minute limit.
When iterating on ZkC changes (e.g. `pkg/zkc/...`), `make zkc-unit-test` is the
relevant target — `make corset-test` will not exercise ZkC code. Note the
`zkc-*` targets depend on `zkc-lint`, which builds `bin/zkc` and checks the
formatting of the `.zkc` sources.

### CLI usage

Expand All @@ -71,12 +70,13 @@ for a quick check. Combining `Test_ZkcUnit|Test_AsmUnit` in a single
./bin/go-corset compile -o out.bin constraints.lisp

# Debug / inspect constraints
./bin/go-corset debug --stats --air constraints.lisp
./bin/go-corset debug --air constraints.lisp
./bin/go-corset debug --mir constraints.lisp

# Trace inspection / conversion
# Trace inspection / conversion (output format follows the file extension)
./bin/go-corset trace --print trace.lt
./bin/go-corset trace --out json trace.lt > trace.json
./bin/go-corset trace --stats trace.lt
./bin/go-corset trace -o trace.json trace.lt

# Interactive trace visualisation
./bin/go-corset inspect trace.lt constraints.lisp
Expand All @@ -85,7 +85,7 @@ for a quick check. Combining `Test_ZkcUnit|Test_AsmUnit` in a single
Key CLI flags (available globally):

- `--field <name>`: prime field to use (default `BLS12_377`; others: `KOALABEAR_16`, `GF_8209`, `GF_251`)
- `--air / --mir / --asm / --uasm / --nasm`: select constraint representation level
- `--air / --mir`: select constraint representation level
- `--debug`: enable debug constraints
- `-S <module.CONST=val>`: set externalised constant values
- `-O <n>`: optimisation level for MIR→AIR lowering
Expand All @@ -108,74 +108,64 @@ The central pipeline transforms `.lisp` (Corset source) into an Arithmetic Inter
```
.lisp source
→ Corset compiler (pkg/corset/)
→ MacroHirProgram (asm macro instructions + HIR modules)
→ Macro ASM → Micro ASM → Nano ASM (pkg/asm/)
→ MIR modules (pkg/ir/mir/)
→ AIR schema (pkg/ir/air/)
→ HIR schema (pkg/ir/hir/)
→ MIR modules (pkg/ir/mir/)
→ AIR schema (pkg/ir/air/)
```

Alternatively, pre-compiled `.bin` binary files can feed in at the top (read via `pkg/binfile/`).

The `SchemaStacker` in `pkg/cmd/corset/util/schema_stacker.go` orchestrates which layers are built and held in memory, controlled by the `--asm/uasm/nasm/mir/air` CLI flags.
The `SchemaStacker` in `pkg/cmd/corset/util/schema_stacker.go` orchestrates which layers are built and held in memory, controlled by the `--mir/air` CLI flags.

Layer constants (defined in `schema_stacker.go`):

- `MACRO_ASM_LAYER = 0` – highest-level; Corset output
- `MICRO_ASM_LAYER = 1` – vectorised, field-specific
- `NANO_ASM_LAYER = 2` – after register splitting
- `MIR_LAYER = 3` – true constraints, higher-level view
- `AIR_LAYER = 4` – lowest level, passed to prover
- `MIR_LAYER = 3` – true constraints, higher-level view
- `AIR_LAYER = 4` – lowest level, passed to prover

### Key packages

| Package | Role |
| ------------------------ | ---------------------------------------------------------------------------------------------------------------------------------------------- |
| `pkg/corset/` | Corset DSL compiler: parses `.lisp`, resolves symbols, type-checks, and emits a `MacroHirProgram`. Standard library embedded as `stdlib.lisp`. |
| `pkg/corset/ast/` | AST nodes for Corset: declarations, expressions, types, bindings |
| `pkg/corset/compiler/` | Compiler internals: parser, resolver, type-checker, preprocessor, translator, register allocator |
| `pkg/asm/` | Assembly layer: `MacroProgram` / `MicroProgram` types, lowering (macro→micro), vectorisation, concretisation to MIR |
| `pkg/asm/io/` | Core abstractions: `Instruction`, `Function`, `Component`, `Program`, bus interface (Map) |
| `pkg/asm/io/macro/` | Macro instruction set (high-level: assign, call, cast, divide, if/goto, …) |
| `pkg/asm/io/micro/` | Micro instruction set (low-level: polynomial, skip_if, jmp, …); includes DFA for analysis |
| `pkg/asm/assembler/` | Parser/linker for `.zkasm` assembly text format |
| `pkg/ir/hir/` | High-level IR: `LowerToMir()` — HIR modules → MIR modules |
| `pkg/ir/mir/` | Mid-level IR: `LowerToAir()` — MIR modules → AIR schema, optimiser |
| `pkg/ir/air/` | AIR schema: final vanishing polynomials + gadgets |
| `pkg/schema/` | Core schema interfaces (`Schema`, `Module`, `Assignment`, `Constraint`) parameterised over field element type `F` |
| `pkg/schema/constraint/` | Constraint types: vanishing, lookup, permutation, range |
| `pkg/trace/` | Trace representation; `json/` and `lt/` (binary) format readers/writers |
| `pkg/binfile/` | Binary `.bin` file serialisation (gob-encoded) |
| `pkg/zkc/` | ZK compiler / VM: a separate compiler+virtual machine (`pkg/zkc/vm/`) with ROM, RAM, WOM memories and a call stack |
| `pkg/util/field/` | Field element implementations: `bls12_377`, `koalabear`, `gf251`, `gf8209`, `mersenne31` |
| `pkg/util/` | General utilities: collections, iterators, source maps, math, word types |
| `cmd/go-corset/` | Main entry point |
| `pkg/cmd/corset/` | CLI commands: check, compile, debug, inspect, trace, generate |
| `pkg/cmd/zkc/` | CLI commands for the ZK compiler toolchain |
| Package | Role |
| ------------------------ | ------------------------------------------------------------------------------------------------------------------------------------------ |
| `pkg/corset/` | Corset DSL compiler: parses `.lisp`, resolves symbols, type-checks, and emits an `hir.Schema`. Standard library embedded as `stdlib.lisp`. |
| `pkg/corset/ast/` | AST nodes for Corset: declarations, expressions, types, bindings |
| `pkg/corset/compiler/` | Compiler internals: parser, resolver, type-checker, preprocessor, translator, register allocator |
| `pkg/ir/hir/` | High-level IR: `LowerToMir()` — HIR modules → MIR modules |
| `pkg/ir/mir/` | Mid-level IR: `LowerToAir()` — MIR modules → AIR schema, optimiser |
| `pkg/ir/air/` | AIR schema: final vanishing polynomials + gadgets |
| `pkg/schema/` | Core schema interfaces (`Schema`, `Module`, `Assignment`, `Constraint`) parameterised over field element type `F` |
| `pkg/schema/constraint/` | Constraint types: vanishing, lookup, range |
| `pkg/trace/` | Trace representation; `json/` and `lt/` (binary) format readers/writers |
| `pkg/binfile/` | Binary `.bin` file serialisation (gob-encoded) |
| `pkg/zkc/` | ZK compiler / VM: a separate compiler+virtual machine (`pkg/zkc/vm/`) with ROM, RAM, WOM memories and a call stack |
| `pkg/util/field/` | Field element implementations: `bls12_377`, `koalabear`, `gf251`, `gf8209`, `mersenne31` |
| `pkg/util/` | General utilities: collections, iterators, source maps, math, word types |
| `cmd/go-corset/` | Main entry point |
| `pkg/cmd/corset/` | CLI commands: check, compile, debug, inspect, trace, generate, verify |
| `pkg/cmd/zkc/` | CLI commands for the ZK compiler toolchain |

### Schema and field polymorphism

All schemas, constraints, assignments and modules are parameterised on a field element type `F` (implementing `field.Element[F]`). Most internal work uses `word.BigEndian` as the concrete field type during compilation; field-specific code lives under `pkg/util/field/<name>/`.

The `MixedProgram[F, T, M]` type in `pkg/asm/program.go` composes assembly components (parameterised on instruction type `T`) with legacy external HIR/MIR modules (type `M`), bridging the assembly and constraint worlds.

### Testing conventions

Tests live in `pkg/test/` and are named following the pattern:

- `Test_Valid_*` — traces that must be accepted by constraints
- `Test_Invalid_*` — traces that must be rejected
- `Test_Agnostic_*` — field-agnostic tests
- `Test_AsmUnit_*` — assembly unit tests
- `Test_AsmUtil_*` / `Test_AsmBench_*` — utility and benchmark tests
- `Test_Bench_*` — corset benchmark tests
- `Test_ZkcUnit_*` / `Test_ZkcMixed_*` / `Test_ZkcInvalid_*` — ZkC compiler/VM tests
- `Test_ZkcUtil_*` / `Test_ZkcBench_*` — ZkC utility and benchmark tests

Test fixtures are in `testdata/`:

- `testdata/corset/valid/`, `testdata/corset/invalid/`, `testdata/corset/agnostic/`
- `testdata/asm/unit/`, `testdata/asm/invalid/`, `testdata/asm/bench/`
- `testdata/corset/valid/`, `testdata/corset/invalid/`, `testdata/corset/agnostic/`, `testdata/corset/bench/`
- `testdata/zkc/unit/`, `testdata/zkc/invalid/`, `testdata/zkc/mixed/`, `testdata/zkc/util/`, `testdata/zkc/bench/`

Each test case consists of a `.lisp` (or `.zkasm`) source file plus `.accepts` / `.rejects` JSON trace files. Tests run against multiple fields simultaneously (e.g. `BLS12_377`, `KOALABEAR_16`, `GF_8209`).
Each test case consists of a `.lisp` (or `.zkc`) source file plus `.accepts` / `.rejects` JSON trace files. Tests run against multiple fields simultaneously (e.g. `BLS12_377`, `KOALABEAR_16`, `GF_8209`).

The `FIELD_REGEX` environment variable (in `pkg/test/util/check_valid.go`) can restrict which fields are tested — useful in CI pipelines.
The `FIELD_REGEX` environment variable (in `pkg/test/util/check_legacy.go`) can restrict which fields are tested — useful in CI pipelines.

When adding tests, always prefer end-to-end tests (a source fixture in
`testdata/` plus `.accepts` / `.rejects` trace files, registered in the
Expand Down
29 changes: 18 additions & 11 deletions pkg/cmd/corset/verify/picus/air_to_picus.go
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ import (
"github.com/LFDT-Lineth/zkc/pkg/cmd/corset/verify/picus/pcl"
"github.com/LFDT-Lineth/zkc/pkg/ir/air"
"github.com/LFDT-Lineth/zkc/pkg/schema"
"github.com/LFDT-Lineth/zkc/pkg/schema/register"
"github.com/LFDT-Lineth/zkc/pkg/util/field"
)

Expand Down Expand Up @@ -129,7 +130,7 @@ func (p *AirPicusTranslator[F]) translateLookup(v air.LookupConstraint[F], picus

source := v.Unwrap().Sources[0]
sourceModule := p.airSchema.Module(source.Module)
sourceTerm := p.lowerTerm(source.Ith(0), sourceModule)
sourceTerm := p.lowerRegister(source.Ith(0), 0, sourceModule)
upperBound := pcl.C(field.BigInt[F](*MaxValueBig(128)))
picusModule.AddLeqConstraint(sourceTerm, upperBound)
}
Expand All @@ -153,16 +154,7 @@ func (p *AirPicusTranslator[F]) lowerTerm(t air.Term[F], module schema.Module[F]
case *air.Constant[F]:
return pcl.C(e.Value)
case *air.ColumnAccess[F]:
name := module.Register(e.Register()).Name()
if strings.Contains(name, " ") {
name = fmt.Sprintf("\"%s\"", name)
}

if e.RelativeShift() != 0 {
name = fmt.Sprintf("%s_%d", name, e.RelativeShift())
}

return pcl.V[F](name)
return p.lowerRegister(e.Register(), e.RelativeShift(), module)
case *air.Mul[F]:
args := p.lowerTerms(e.Args, module)
return pcl.FoldBinaryE(pcl.Mul, args)
Expand All @@ -174,6 +166,21 @@ func (p *AirPicusTranslator[F]) lowerTerm(t air.Term[F], module schema.Module[F]
}
}

// lowerRegister converts an access of a given register (at a given relative
// shift) into a PCL variable.
func (p *AirPicusTranslator[F]) lowerRegister(rid register.Id, shift int, module schema.Module[F]) pcl.Expr[F] {
name := module.Register(rid).Name()
if strings.Contains(name, " ") {
name = fmt.Sprintf("\"%s\"", name)
}

if shift != 0 {
name = fmt.Sprintf("%s_%d", name, shift)
}

return pcl.V[F](name)
}

// lowerTerms lowers a set of zero or more AIR expressions.
func (p *AirPicusTranslator[F]) lowerTerms(exprs []air.Term[F], airModule schema.Module[F]) []pcl.Expr[F] {
nexprs := make([]pcl.Expr[F], len(exprs))
Expand Down
Loading