Skip to content

feat(air): add commitment-aware AIR parser, IR types, and validation suite#8

Merged
hooftly merged 10 commits intomainfrom
air
Oct 27, 2025
Merged

feat(air): add commitment-aware AIR parser, IR types, and validation suite#8
hooftly merged 10 commits intomainfrom
air

Conversation

@hooftly
Copy link
Member

@hooftly hooftly commented Oct 27, 2025

Summary

Introduces a full commitment-aware AIR parsing pipeline, including typed public
inputs, normalized commitment bindings, and validation logic for use across the
CLI, SDK, and backend interfaces.

Changes

  • Added air/parser.rs: unified TOML/YAML parser that produces a validated
    AirIr structure, running commitment binding checks before returning.
  • Added air/types.rs: defines AirIr, PublicTy, CommitmentKind, and
    CommitmentBinding enums/structs to represent the backend-neutral AIR IR.
  • Added air/validate.rs: validator enforcing curve requirements, disallowing
    duplicate or unknown public-input bindings, and normalizing commitment kinds.
  • Extended air.rs:
    • integrated parse_air_file, parse_air_str, and new IR modules
    • added commitment deserialization support for legacy, table, and list forms
    • added AirPublicInput and AirCommitments helpers
  • Registered new parser and degree invariance tests in corelib/Cargo.toml.
  • Added examples/air/commit_demo.air with Pedersen, Poseidon, and Keccak
    bindings.
  • Expanded documentation (INTERFACES.md) to reference the new parser DSL.
  • Added integration tests:
    • air_ir_parser.rs — validates parsing, error messages, and binding rules
    • air_ir_degree.rs — ensures commitment bindings preserve degree metrics

Motivation

Unifies AIR DSL parsing under a typed, backend-agnostic IR, enabling validation
of commitments and public inputs prior to proof generation. This ensures
deterministic validation surfaces across SDKs and CLI tooling.

Testing

  • cargo test -p zkprov-corelib
  • Integration tests: air_ir_parser, air_ir_degree
  • Verified example AIR files parse and validate deterministically

Checklist

  • Tests added and passing
  • Docs updated (INTERFACES.md)
  • Lint checks pass
  • Ready for review

- Exposed `parser` and `types` modules from the AIR crate so downstream
  code can access AIR IR interfaces directly
- Added parsing entry points to load `.air` sources into the new `AirIr`
  via the existing `AirProgram` validation path
- Defined `AirIr` structure, `CommitmentBinding` enum, and conversion
  from `AirProgram` to `AirIr`
- Scaffolded ignored integration tests to exercise upcoming parser and
  degree checks
- Extend AirIr with degree hint, typed commitment bindings, and public input metadata
- Introduce CommitmentKind, CommitmentBinding, and PublicInput structures
- Update AirProgram conversion to populate the new commitment binding representation
- Preserve existing degree hint handling during conversion
- Improve type safety and clarity of commitment and public input metadata
Extend AIR parser to deserialize commitment bindings from both table and list
forms while preserving legacy hints and normalizing public-input declarations
for each binding kind (Pedersen(curve), PoseidonCommit, KeccakCommit).

Add lowering to IR with the new bindings and normalized public inputs, and run
parser-level validation to surface missing curves, unknown public inputs, or
duplicate bindings before returning the AIR.

Add regression coverage for the new syntax and validation rules, plus a sample
AIR showcasing Pedersen, Poseidon, and Keccak commitment bindings.

Affects: parser, IR, validation, tests, fixtures
Require Pedersen bindings to specify a curve; flag unknown public inputs; and
prevent duplicate commitments per (kind, name) pair. Keep error strings exact
for stable downstream matching.

Tests: expand parser coverage to include whitespace-only curve values and
duplicate references within a single commitment entry, alongside existing
error scenarios.

Affects: parser validation, tests
Added a regression test that ensures keccak commitment bindings reject curve hints and surface `CommitmentBindingUnexpectedCurve`.
…-end

Add `PublicTy` enum and update `PublicInput` so AIR IR always carries typed
public inputs converted from the manifest.

Parser:
- Preserve public-input types during deserialization and lowering.
- Refresh demo AIR manifest to annotate each input with its declared type.

Tests:
- Expand AIR parser tests to assert the typed public-input surface.
- Add negative cases for invalid public-input type declarations.

Affects: air/ir, air/parser, manifests, tests
…ndings

Add regression test comparing AIR degree metrics between equivalent programs
with and without commitment bindings to ensure invariance of:
- trace length / register count
- constraint counts (transition and boundary)

Guards against accidental degree changes introduced by binding handling.

Affects: tests/air_degree
…izer; tighten validation

- Standardize AIR commitment parsing errors so both inline and list forms return
  actionable curve guidance.
- Add custom public-input type deserializer to ensure robust, typed PI handling.
- Tighten validator messages for missing curves, unknown public inputs, and
  duplicate (kind,name) bindings with exact, stable error text.

Tests:
- Expand parser tests with shared helpers to snapshot every validation failure
  and assert exact error strings.

Affects: air/parser, validation, tests
…nvariance; add cross-links

- Add commitment-aware AIR parser docs with a full TOML example.
- Clarify that commitment bindings do not alter `degree_hint`.
- Expand AIR IR type documentation to illustrate DSL → struct materialization,
  reiterating that commitment wiring does not affect degree accounting.
- Link the interface guide directly from the parser docs for easy access to the DSL walkthrough.

Affects: docs/air/parser.md, docs/air/ir-types.md, docs/interfaces.md
…e doctest and guidance

- Update AIR parser docs to show `[[commitments]]` declared before other table
  headers, with guidance to keep the array at the root scope.
- Align `AirIr` doctest with the root-level commitments layout and document why
  commitments must precede table sections.

Affects: docs/air/parser.md, crates/air_ir/src/lib.rs (doctest)
@hooftly hooftly merged commit 82f42bd into main Oct 27, 2025
36 checks passed
@hooftly hooftly deleted the air branch October 27, 2025 16:51
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant