Skip to content
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.

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

Initial SKI import. #1

Closed
wants to merge 16 commits into from
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
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
16 changes: 16 additions & 0 deletions examples/ski/.gitignore
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
# Cargo build
**/target

# Cargo config
.cargo

# Profile-guided optimization
/tmp
pgo-data.profdata

# MacOS nuisances
.DS_Store

# Proofs
**/proof-with-pis.json
**/proof-with-io.json
31 changes: 31 additions & 0 deletions examples/ski/program/Cargo.toml
Original file line number Diff line number Diff line change
@@ -0,0 +1,31 @@
[workspace]
[package]
version = "0.1.0"
name = "ski-program"
edition = "2021"

[dependencies]
wp1-zkvm = { git = "ssh://[email protected]/wormhole-foundation/wp1.git", branch = "memoset" }
ski = { path = "../ski", features = ["inzkvm"] }

[patch."https://github.com/Plonky3/Plonky3.git"]
p3-air = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
p3-field = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
p3-commit = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
p3-matrix = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
p3-baby-bear = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
p3-util = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
p3-challenger = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
p3-dft = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
p3-fri = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
p3-goldilocks = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
p3-keccak = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
p3-keccak-air = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
p3-blake3 = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
p3-mds = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
p3-merkle-tree = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
p3-poseidon2 = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
p3-symmetric = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
p3-uni-stark = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
p3-maybe-rayon = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
p3-bn254-fr = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
Binary file not shown.
18 changes: 18 additions & 0 deletions examples/ski/program/src/main.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
//! A simple program to be proven inside the zkVM.

#![no_main]
wp1_zkvm::entrypoint!(main);

use ski::{Mem, Term, SKI};

// INFO summary: cycles=204758, e2e=3709, khz=55.21, proofSize=1.16 MiB
// (S(K(SI))K)KI evaled to K
#[allow(dead_code)]
pub fn main() {
let ski = wp1_zkvm::io::read::<SKI>();
let mem = &mut Mem::new();
let term = Term::try_from_ski(mem, &ski).unwrap();
let evaled = term.eval(mem, 0).to_ski(mem);

wp1_zkvm::io::commit(&evaled);
}
36 changes: 36 additions & 0 deletions examples/ski/script/Cargo.toml
Original file line number Diff line number Diff line change
@@ -0,0 +1,36 @@
[workspace]
[package]
version = "0.1.0"
name = "ski-script"
edition = "2021"

[dependencies]
wp1-sdk = { git = "ssh://[email protected]/wormhole-foundation/wp1.git", branch = "memoset" }
ski = { path = "../ski" }

[build-dependencies]

wp1-helper = { git = "ssh://[email protected]/wormhole-foundation/wp1.git", branch = "memoset" }

[patch."https://github.com/Plonky3/Plonky3.git"]
p3-air = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
p3-field = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
p3-commit = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
p3-matrix = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
p3-baby-bear = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
p3-util = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
p3-challenger = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
p3-dft = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
p3-fri = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
p3-goldilocks = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
p3-keccak = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
p3-keccak-air = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
p3-blake3 = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
p3-mds = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
p3-merkle-tree = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
p3-poseidon2 = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
p3-symmetric = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
p3-uni-stark = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
p3-maybe-rayon = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
p3-bn254-fr = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }

5 changes: 5 additions & 0 deletions examples/ski/script/build.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
use wp1_helper::build_program;

fn main() {
build_program("../program")
}
36 changes: 36 additions & 0 deletions examples/ski/script/src/main.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,36 @@
//! A simple script to generate and verify the proof of a given program.
use std::str::FromStr;

const ELF: &[u8] = include_bytes!("../../program/elf/riscv32im-succinct-zkvm-elf");

use wp1_sdk::{utils, ProverClient, SP1Stdin};

use ski::SKI;

fn main() {
// Setup a tracer for logging.
utils::setup_logger();

// Generate proof.
let mut stdin = SP1Stdin::new();
let ski = SKI::from_str(&"(S(K(SI))K)KI").unwrap();
stdin.write(&ski);

let client = ProverClient::new();
let mut proof = client.prove(ELF, stdin).expect("proving failed");

// Read output.
let evaled = proof.public_values.read::<SKI>();
assert_eq!("K", evaled.to_string());
println!("{ski} evaled to {evaled}");

// Verify proof.
client.verify(ELF, &proof).expect("verification failed");

// Save proof.
proof
.save("proof-with-io.json")
.expect("saving proof failed");

println!("successfully generated and verified proof for the program!")
}
40 changes: 40 additions & 0 deletions examples/ski/ski/Cargo.toml
Original file line number Diff line number Diff line change
@@ -0,0 +1,40 @@
[workspace]
[package]
version = "0.1.0"
name = "ski"
edition = "2021"

[dependencies]
itertools = "0.12.0"
serde = { features = ["derive"] }
p3-air = { git = "https://github.com/Plonky3/Plonky3.git" }
p3-baby-bear = { git = "https://github.com/Plonky3/Plonky3.git" }
p3-field = { git = "https://github.com/Plonky3/Plonky3.git" }
p3-matrix = { git = "https://github.com/Plonky3/Plonky3.git" }
wp1-core = { git = "ssh://[email protected]/wormhole-foundation/wp1.git", branch = "memoset" }
wp1-derive = { git = "ssh://[email protected]/wormhole-foundation/wp1.git" }

[features]
inzkvm = ["wp1-core/inzkvm"]

[patch."https://github.com/Plonky3/Plonky3.git"]
p3-air = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
p3-field = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
p3-commit = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
p3-matrix = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
p3-baby-bear = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
p3-util = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
p3-challenger = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
p3-dft = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
p3-fri = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
#p3-goldilocks = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
p3-keccak = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
p3-keccak-air = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
p3-blake3 = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
p3-mds = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
p3-merkle-tree = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
p3-poseidon2 = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
p3-symmetric = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
p3-uni-stark = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
p3-maybe-rayon = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
#p3-bn254-fr = { git = "ssh://[email protected]/Plonky3/Plonky3.git", rev = "2871dfe257a49583c763c94a879785188716f006" }
133 changes: 133 additions & 0 deletions examples/ski/ski/src/air/builder.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,133 @@
use crate::air::pointer::Pointer;
use itertools::chain;
use wp1_core::air::{
AirInteraction, BaseAirBuilder, ByteAirBuilder, ExtensionAirBuilder, WordAirBuilder,
};
use wp1_core::lookup::InteractionKind;

/// A custom AirBuilder trait that only includes
pub trait LurkAirBuilder:
BaseAirBuilder
+ MemoSetBuilder
+ ConsBuilder
+ RelationBuilder
+ ByteAirBuilder
+ WordAirBuilder
+ ExtensionAirBuilder
{
}

pub trait MemoSetBuilder: BaseAirBuilder {
/// Make a MemoSet query
fn memoset_query(
&mut self,
tag: impl Into<Self::Expr>,
values: impl IntoIterator<Item = Self::Expr>,
is_real: impl Into<Self::Expr>,
) {
self.send(AirInteraction::new(
chain!([tag.into()], values.into_iter()).collect(),
is_real.into(),
InteractionKind::MemoSet,
));
}

/// Prove a MemoSet query (once!)
fn memoset_prove(
&mut self,
tag: impl Into<Self::Expr>,
values: impl IntoIterator<Item = Self::Expr>,
multiplicity: impl Into<Self::Expr>,
) {
self.receive(AirInteraction::new(
chain!([tag.into()], values.into_iter()).collect(),
multiplicity.into(),
InteractionKind::MemoSet,
));
}
}

//impl<AB: BaseAirBuilder> LurkAirBuilder for AB {}
impl<AB: BaseAirBuilder> MemoSetBuilder for AB {}

//pub trait LurkAirBuilder: BaseAirBuilder + ConsBuilder + RelationBuilder {}

pub trait ConsBuilder: BaseAirBuilder {
/// Sends a byte operation to be processed.
fn query_cons<E>(
&mut self,
a: Pointer<Self::Var>,
b: Pointer<Self::Var>,
c: Pointer<Self::Var>,
is_cons: E,
) where
E: Into<Self::Expr>,
{
self.send(AirInteraction::new(
chain!(a.into_exprs(), b.into_exprs(), c.into_exprs()).collect(),
is_cons.into(),
InteractionKind::MemoSet,
));

todo!("add cons domain");
}

/// Receives a byte operation to be processed.
fn prove_cons<E>(
&mut self,
a: Pointer<Self::Var>,
b: Pointer<Self::Var>,
c: Pointer<Self::Var>,
multiplicity: E,
) where
E: Into<Self::Expr>,
{
self.receive(AirInteraction::new(
chain!(a.into_exprs(), b.into_exprs(), c.into_exprs()).collect(),
multiplicity.into(),
InteractionKind::MemoSet,
));

todo!("add cons domain");
}
}

pub trait RelationBuilder: BaseAirBuilder {
/// Sends a byte operation to be processed.
fn query_relation<Etag, EReal>(
&mut self,
tag: Etag,
a: Pointer<Self::Var>,
b: Pointer<Self::Var>,
is_real: EReal,
) where
Etag: Into<Self::Expr>,
EReal: Into<Self::Expr>,
{
self.send(AirInteraction::new(
chain!(a.into_exprs(), b.into_exprs(), [tag.into()]).collect(),
is_real.into(),
InteractionKind::MemoSet,
));
todo!("add relation domain");
}

/// Receives a byte operation to be processed.
fn prove_relation<Etag, EMult>(
&mut self,
tag: Etag,
a: Pointer<Self::Var>,
b: Pointer<Self::Var>,
multiplicity: EMult,
) where
Etag: Into<Self::Expr>,
EMult: Into<Self::Expr>,
{
self.receive(AirInteraction::new(
chain!(a.into_exprs(), b.into_exprs(), [tag.into()]).collect(),
multiplicity.into(),
InteractionKind::MemoSet,
));
todo!("add relation domain");
}
}
2 changes: 2 additions & 0 deletions examples/ski/ski/src/air/mod.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
pub mod builder;
pub mod pointer;
16 changes: 16 additions & 0 deletions examples/ski/ski/src/air/pointer.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
use wp1_derive::AlignedBorrow;

#[derive(AlignedBorrow, Default, Debug, Clone, Copy)]
pub struct Pointer<T> {
pub idx: T,
pub tag: T,
}

impl<T> Pointer<T> {
pub fn into_exprs<U>(self) -> impl IntoIterator<Item = U>
where
T: Into<U>,
{
[self.tag.into(), self.idx.into()]
}
}
Loading