an extended polynomial identity language (PIL) in rust

Related tags

Cryptography powdr
Overview

powdr

an extended polynomial identity language (PIL) in rust

Ideas

This is a random list of ideas that help designing the language. Most if this is heavily inspired by zkASM / PIL of the polygon/hermez team.

Main goal: Everything is written in the same language, if possible not even spread across multiple files.

Constant Definitions

Define constants directly in the pil file:

pol constant BYTE = |i| i % 0xff;

Constants can also depend on each other:

pol constant A = |i| i & 0xffff;
pol constant B = |i| (i / 0x10000) & 0xffff;
pol constant SUM = |i| (A[i] + B[i]) & 0xffff;
pol constant OVERFLOW = |i| (A[i] + B[i]) >> 16;

By just declaring A and B to be of type u16, it might not be needed to define them? There should be a way to create a "cross product" of constants somehow, so that the definition of A and B above is trivial. This could also help to combine two lookps into one.

Types

Polynomials are typed (which adds a constraint automatically unless it can be proven that it is not needed due to a lookup):

pol commit isJump: bool; // creates constraint "isJump * (1-isJump) = 0;"

There can be user-defined types for enums or bitfields.

Templates

The language should have as few built-in as possible. There should be ways to define functions or templates, for example the following:

fun<T> ite(c: bool, a: T, b: T) -> T = c * (a - b) + b;

There should be ways to handle complex types like arrays and structs efficiently.

Instruction / Assembly language

The second layer of this langauge is to define an assembly-like language that helps in defining complex constants.

The zkASM language of polygon/hermez can be used as a basis, but with the following changes:

  • The number of registers needs to be user-defined
  • The way instructions are mapped to constraints has to be user-defined (i.e. the instructions themselves are user-defined)
  • The execution process and the constraints generated from an instruction have to be defined at the same place.
  • The correspondence between assembly identifiers and polynomials has to be direct.

Example from polygon-hermez zkASM:

$               :ADD, MSTORE(SP++), JMP(readCode)

The $ means that the "input" is computed depending on the instruction on the right hand side. To understand the data flow, the implicit inputs and outputs of the instructions must be known:

  • ADD reads from registers A and B and outputs in the implicit default register. It also invokes a state machine.
  • MSTORE writes to memory and reads from the implicit default register
  • JMP only handles control-flow, but we could also have JMPN here which would read from the implicit default register

Combining these is fine as long as for every register, there is only one writing to that register.

It might be better to make the order of the instructions explicit (i.e. put them in separate statements) and rely on an optimizer to combine instructions into a single step if they are not conflicting.

A better notation might be:

X := ADD(A, B);
MSTORE(SP++, X);
JMP(readCode);

If we assume we have an optimizer that combines instructions, we could also think about an optimizer that performs automatic register compression, so that we could use an arbitrary number of registers in the source code, but specify a certain (smaller) number of registers for the target architecture. It would not be possible to move registers to memory in that case, but the optimizer would just report an error if the number of used registers is too large.

High-level language

The third layer is a high-level language that has all the usual features of a regular programming language like loops, functions and local variables. How to map it to a user-defined instruction set is not clear yet, but it would be nice to at least relieve the user from having to assign registers, jump labels and so on.

It might be possible to define interlieve assembly code like we do with Solidity/Yul and then provide a set of simplification rules specific to an instruction set.

You might also like...
Zero-Knowledge Assembly language and compiler

zkAsm A Zero-Knowledge circuit assembly language, designed to represent Zero-Knowledge circuits in a compressed format, to be stored on blockchains. I

Noir is a domain specific language for zero knowledge proofs

The Noir Programming Language Noir is a Domain Specific Language for SNARK proving systems. It has been designed to use any ACIR compatible proving sy

Encrypt your files in cow language 🐄
Encrypt your files in cow language 🐄

Cow-encryptor Encrypt your files in cow language 🐮 Installation 📦 Arch Linux 🐧 cow-encryptor is in the AUR yay -S cow-encryptor Other 🪟 🐧 With ma

STARK - SNARK recursive zero knowledge proofs, combinaison of the Winterfell library and the Circom language

STARK - SNARK recursive proofs The point of this library is to combine the SNARK and STARK computation arguments of knowledge, namely the Winterfell l

Validity is a next-generation, deduction-based language for formally verified, context-aware, autonomous & reactive smart contracts.
Validity is a next-generation, deduction-based language for formally verified, context-aware, autonomous & reactive smart contracts.

Validity Language Validity is a next-generation, deduction-based language for formally verified, context-aware, autonomous & reactive smart contracts.

An EVM low-level language that gives full control over the control flow of the smart contract.

Meplang - An EVM low-level language Meplang is a low-level programming language that produces EVM bytecode. It is designed for developers who need ful

An extensible and practical demonstration of constructing evm-based sandwich attacks built with ethers-rs and Huff language.
An extensible and practical demonstration of constructing evm-based sandwich attacks built with ethers-rs and Huff language.

subway-rs • Construct evm-based sandwich attacks using Rust and Huff. Getting Started subway-rs is a port of libevm's original subway, implemented wit

A fast zero-knowledge proof friendly Move language runtime environment.
A fast zero-knowledge proof friendly Move language runtime environment.

zkMove Lite zkMove Lite is a lightweight zero-knowledge proof friendly Move language virtual machine. Move bytecode is automatically "compiled" into c

Package used by the cosmos-rust-interface. Makes direct use of cosmos-rust.

Package used by the cosmos-rust-interface. Makes direct use of cosmos-rust (cosmos‑sdk‑proto, osmosis-proto, cosmrs).

Owner
null
A prototype implementation of the Host Identity Protocol v2 for bare-metal systems, written in pure-rust.

Host Identity Protocol for bare-metal systems, using Rust I've been evaluating TLS replacements in constrained environments for a while now. Embedded

null 31 Dec 12, 2022
Alternative Free Identity System

Alfis Alternative Free Identity System This project represents a minimal blockchain without cryptocurrency, capable of sustaining any number of domain

Revertron 207 Jan 5, 2023
As part of the IOP Stack™ Morpheus is a toolset to have gatekeeper-free identity management and verifiable claims as a 2nd layer on top of a blockchain

Internet of People Internet of People (IoP) is a software project creating a decentralized software stack that provides the building blocks and tools

We are building a complete decentralized ecosystem with the IOP Stack™ 9 Nov 4, 2022
An open source Rust high performance cryptocurrency trading API with support for multiple exchanges and language wrappers. written in rust(🦀) with ❤️

Les.rs - Rust Cryptocurrency Exchange Library An open source Rust high performance cryptocurrency trading API with support for multiple exchanges and

Crabby AI 4 Jan 9, 2023
Aya is an eBPF library for the Rust programming language, built with a focus on developer experience and operability.

Aya API docs | Chat | Aya-Related Projects Overview eBPF is a technology that allows running user-supplied programs inside the Linux kernel. For more

null 1.5k Jan 6, 2023
Prost is a Protocol Buffers implementation for the Rust Language.

PROST! prost is a Protocol Buffers implementation for the Rust Language. prost generates simple, idiomatic Rust code from proto2 and proto3 files. Com

Tokio 2.5k Jan 8, 2023
A low-level assembly language for the Ethereum Virtual Machine built in blazing-fast pure rust.

huff-rs • huff-rs is a Huff compiler built in rust. What is a Huff? Huff is a low-level programming language designed for developing highly optimized

Huff 276 Dec 31, 2022
`llm-chain` is a powerful rust crate for building chains in large language models allowing you to summarise text and complete complex tasks

llm-chain ?? llm-chain is a collection of Rust crates designed to help you work with Large Language Models (LLMs) more effectively. Our primary focus

Sobel IO 36 Apr 6, 2023
A bitcoin vanity address generator written with the Rust programming language.

btc-vanity A bitcoin vanity address generator written with the Rust programming language. With btc-vanity you can create a private key which has a com

Emirhan TALA 22 Aug 7, 2023
Emerging smart contract language for the Ethereum blockchain.

Emerging smart contract language for the Ethereum blockchain.

null 1.4k Jan 9, 2023