release: Ix v0.1, Archimedes

[johnchandlerburnham]

Ix v0.1: Lean -> Binius end-to-end

Compress typechecking and reduction of Lean programs into Binius zero-knowledge proofs

Ix Compiler

Goal: Compile Lean libraries to a content-addressed binary representation that can be ingested by the IxVM

Tasks:

• Blake3 Lean bindings and FFI chore: use Blake3.lean dependency #14 feat: Blake3 + LSpec #6 chore: fix blake3 dependencies #36
• Define Ixon binary serialization format Ixon Serialization and Ix Canonicalization #13
• Define Ix IR based on [Yatima IR] (https://github.com/argumentcomputer/yatima/tree/main/Yatima/Datatypes) and the Lean kernel which separates alpha-invariant computational content from noncomputational metadata Ixon Serialization and Ix Canonicalization #13
• Transporter: convert Ix IR into Ixon wire-format to "beam" it from one context to another Ixon Serialization and Ix Canonicalization #13
  • Dematerialize Ix IR into Ixon content and Ixon metadata serializations
  • Rematerialize Ixon content and metadata serializations into Ix IR
• Canonicalize Lean Environment into Ix IR Ixon Serialization and Ix Canonicalization #13
• Persistent filemapped Ix store Ixon Serialization and Ix Canonicalization #13
• Ix kernel reference implementation in Lean
• CLI for running a Lean library through Ix (ported from Yatima)
• Lean metaprogramming integration
• Define proof and claim format

Aiur

Goal: write a zkDSL in Lean that can generate corresponding circuits and witness for them, ultimately producing a zk proof and being able to quickly verify it.

• Archon as an interface to Binius core (in Rust)
  • Design and implementation of self-contained "circuit modules"
  • Design and implementation of self-contained "witness modules"
  • Algorithm for automatic population of witness modules
  • Compilation of multiple circuit modules into a Binius' ConstraintSystem
  • Compilation of multiple witness modules into an Archon witness
  • Wrappers around Binius' witness validation, proof generation and proof verification
• Lean bindings to Archon
• Aiur frontend (datatypes + Lean DSL)
• Aiur Bytecode datatypes
• Simplification + typechecking + compilation of Aiur frontend datatypes to Bytecode
• Execution of Aiur Bytecode to generate a QueryRecord
• Circuit generation
• Witness generation
• Pipelines for proof generation and verification
• Aiur API for external gadgets
• Benchmarks for Aiur

IxVM

Goal: write an Aiur Toplevel that can handle Ix claims by processing Ixon data.

• Blake3 gadget in Archon
• Main function that can deal with different kinds of Ix claims
• Ingress function (turn serialized Ixon data into Aiur datatypes)
• Egress function (turn Aiur datatypes into serialized Ixon data)
• Reduction algorithm
• Typechecking algorithm
• Plug Ix frontend (Lean constants -> Ixon) to the IxVM
• Benchmarks for the IxVM

Infrastructure

• nix devshell Ixon Serialization and Ix Canonicalization #13 19 chore: Bump Nix flake to Lean v4.17.0 #40 fix: change nixpkgs channel back to unstable #41
• nix build feat: Add Nix flake #44
• cachix caching of nix build feat: Add Nix flake #44

[storojs72]

I would extend the "Blake3 precompile work" from "Binius integration" section to a bit more details:

• Blake3 precompile work
  • Initial Binius circuit for Blake3 compression function: feat: Blake3 G function gadget IrreducibleOSS/binius#16, feat: Blake3 compression IrreducibleOSS/binius#38, chore: Blake3 circuit usage example IrreducibleOSS/binius#56;
  • Create example of Binius circuit for proving correctness of some arbitrary memory (ReadOnlyMemory): example;
  • Create example of Binius circuit for proving integrity of program's memory based on existing Keccak circuit (IntegrityCheckGadget): example;
  • Optimised circuit (with "horizontal" witness population) for Blake3 compression function: example, [circuits] Optimised Blake3 compression IrreducibleOSS/binius#222;
  • Create example of IntegrityCheckGadget based on Blake3 hashing;
  • Porting Blake3-based IntegrityCheckGadget to Archon-style circuit - this is what we actually treat as a Blake3 precompile usable by Ix: feat: Some improvements for Rust Blake3 compression #111, feat: Blake3 compression circuit as isolated modules #108, feat: Initial Blake3 compression in Archon #105;
  • Integrating Blake3 precompile into Aiur

[storojs72]

In terms of Blake3 work, we currently are progressing with porting Archon modules from Rust to Lean (in context of integrating the Blake3 precompile into Aiur). Once we have them in Lean we can proceed with memory integrity checking based on Blake3 hashing already on Lean side