Initial SKI import.

examples/ski/.gitignore

@@ -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

examples/ski/program/Cargo.toml

@@ -0,0 +1,10 @@
+[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" }
+

examples/ski/program/src/main.rs

@@ -0,0 +1,18 @@
+//! A simple program to be proven inside the zkVM.
+
+#![no_main]
+wp1_zkvm::entrypoint!(main);
+
+use ski::{ITerm, Mem, SKI};
+
+//  INFO summary: cycles=254197, e2e=4552, khz=55.84, proofSize=1.24 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 = ITerm::try_from_ski(mem, &ski).unwrap();
+    let evaled = term.eval(mem, 0).to_ski(mem);
+
+    wp1_zkvm::io::write(&evaled);
+}

examples/ski/script/Cargo.toml

@@ -0,0 +1,12 @@
+[workspace]
+[package]
+version = "0.1.0"
+name = "ski-script"
+edition = "2021"
+
+[dependencies]
+wp1-sdk = { path = "../../../sdk" }
+ski = { path = "../ski" }
+
+[build-dependencies]
+wp1-helper = { path = "../../../helper" }

examples/ski/script/build.rs

@@ -0,0 +1,5 @@
+use wp1_helper::build_program;
+
+fn main() {
+    build_program("../program")
+}

examples/ski/script/src/main.rs

@@ -0,0 +1,35 @@
+//! 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, SP1Prover, SP1Stdin, SP1Verifier};
+
+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 mut proof = SP1Prover::prove(ELF, stdin).expect("proving failed");
+
+    // Read output.
+    let evaled = proof.stdout.read::<SKI>();
+    assert_eq!("K", evaled.to_string());
+    println!("{ski} evaled to {evaled}");
+
+    // Verify proof.
+    SP1Verifier::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!")
+}

examples/ski/ski/Cargo.toml

@@ -0,0 +1,37 @@
+[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" }
+
+[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" }

examples/ski/ski/src/air/builder.rs

@@ -0,0 +1,131 @@
+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>,
+    {
+        todo!("add cons domain");
+        self.send(AirInteraction::new(
+            chain!(a.into_exprs(), b.into_exprs(), c.into_exprs()).collect(),
+            is_cons.into(),
+            InteractionKind::MemoSet,
+        ));
+    }
+
+    /// 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>,
+    {
+        todo!("add cons domain");
+        self.receive(AirInteraction::new(
+            chain!(a.into_exprs(), b.into_exprs(), c.into_exprs()).collect(),
+            multiplicity.into(),
+            InteractionKind::MemoSet,
+        ));
+    }
+}
+
+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>,
+    {
+        todo!("add relation domain");
+        self.send(AirInteraction::new(
+            chain!(a.into_exprs(), b.into_exprs(), [tag.into()]).collect(),
+            is_real.into(),
+            InteractionKind::MemoSet,
+        ));
+    }
+
+    /// 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>,
+    {
+        todo!("add relation domain");
+        self.receive(AirInteraction::new(
+            chain!(a.into_exprs(), b.into_exprs(), [tag.into()]).collect(),
+            multiplicity.into(),
+            InteractionKind::MemoSet,
+        ));
+    }
+}

examples/ski/ski/src/air/mod.rs

@@ -0,0 +1,2 @@
+pub mod builder;
+pub mod pointer;

examples/ski/ski/src/air/pointer.rs

@@ -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()]
+    }
+}

examples/ski/ski/src/chips/mod.rs

@@ -0,0 +1,76 @@
+use p3_air::{Air, AirBuilder, BaseAir};
+use p3_field::{AbstractField, Field};
+use p3_matrix::dense::RowMajorMatrix;
+use wp1_core::stark::SP1AirBuilder;
+use wp1_derive::AlignedBorrow;
+
+use std::mem::size_of;
+
+struct EvalCols {}
+struct ApplyCols {}
+struct Eval1Cols {}
+struct SCols {}
+struct S1Cols {}
+struct S2Cols {}
+struct S3Cols {}
+struct KCols {}
+struct K1Cols {}
+struct K2Cols {}
+struct ICols {}
+struct I1Cols {}
+
+#[derive(AlignedBorrow)]
+struct CpuCols<T> {
+    x: T,
+}
+
+struct CpuChip {}
+
+const NUM_CPU_COLS: usize = size_of::<CpuCols<u8>>();
+
+impl<F: Send + Sync> BaseAir<F> for CpuChip {
+    fn width(&self) -> usize {
+        NUM_CPU_COLS
+    }
+}
+
+impl CpuChip {
+    #[allow(dead_code)]
+    fn generate_trace<F: Field>() -> RowMajorMatrix<F> {
+        todo!()
+    }
+}
+
+impl<AB: SP1AirBuilder> Air<AB> for CpuChip {
+    fn eval(&self, builder: &mut AB) {
+        todo!()
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use p3_baby_bear::BabyBear;
+    use p3_field::{AbstractField, Field};
+    use p3_matrix::dense::RowMajorMatrix;
+    use wp1_core::{
+        stark::StarkGenericConfig,
+        utils::{uni_stark_prove as prove, uni_stark_verify as verify, BabyBearPoseidon2},
+    };
+
+    use super::*;
+
+    fn prove_trace() {
+        let config = BabyBearPoseidon2::new();
+        let mut challenger = config.challenger();
+
+        let f = BabyBear::from_canonical_usize;
+
+        let trace: RowMajorMatrix<BabyBear> = CpuChip::generate_trace();
+
+        let chip = CpuChip {};
+        let proof = prove::<BabyBearPoseidon2, _>(&config, &chip, &mut challenger, trace);
+
+        let mut challenger = config.challenger();
+        verify(&config, &chip, &mut challenger, &proof).unwrap();
+    }
+}