Prover SDK tracking issue

[slumber]

The main prover functionality is gathered in nexus-prover crate, which does all sort of stuff: generate public parameters, print nice CLI output, compress proofs etc.

I propose to remove it in favor of nexus-sdk which provides abstracted interface like

pub trait Prover {
    /// Output type.
    type Proof;
    
    /// Public parameters needed for generating proofs, if any.
    type PublicParams;
    
    fn prove(&self, params: &Self::PublicParams) -> Self::Proof;
    
    /// or something like prove_step to facilitate usage of "stepped" cli output.
}

And then use it

pub struct NexusProver<P: Prover = CompressedNova> {
    /* private */
}

pub struct NexusVM { }

This SDK is then integrated into nexus-tools to be reused with CLI and pretty output.

[slumber]

@govereau @sjudson @danielmarinq

[sjudson]

You propose doing this alongside or in place of the nexus-api approach (#146) @slumber? For dev I think it'll be important to expose VM interfaces alongside the prover interface so that users can develop without needing to invoke the proof apis.

[slumber]

You propose doing this alongside or in place of the nexus-api approach (#146) @slumber? For dev I think it'll be important to expose VM interfaces alongside the prover interface so that users can develop without needing to invoke the proof apis.

nexus-api doesn't look like proper sdk and is more of a short-term solution, as it just re-exports what we currently have.
This issue is about generically wrapping the proving system and the vm into an extendable interface which we ourselves can reuse.

[sjudson]

I'm amenable to really taking the time to think through the api design in a more comprehensive way than the #146 approach, which is really an attempt to get programmatic usage "out the door" in an at least somewhat constrained and opinionated way.

I do think it makes sense though to have an independent public facing API from the prover API that is also consumed internally though.

[slumber]

I'm amenable to really taking the time to think through the api design in a more comprehensive way than the #146 approach, which is really an attempt to get programmatic usage "out the door" in an at least somewhat constrained and opinionated way.

I do think it makes sense though to have an independent public facing API from the prover API that is also consumed internally though.

This is relevant because we already have Nova(seq), Nova(pcd), Nova(pcd+spartan), HyperNova soon, maybe Jolt which is going to be different.
There's no convenient way of switching between these. We could also add things like curve choice or commitment scheme later.

[sjudson]

Here's a rough early sketch of a proposal for the overall SDK architecture. In terms of code, the idea will be to have an API that is consumed by both the SDK and CLI, providing two routes to similar functionality (albeit with the CLI being a simplified, streamlined version).

Objects

The central object of the SDK/CLI will be an engine. Each engine will correspond to an ISA + arithmetization method, which takes in a complied program using the nexus-rt and outputs a sequence of circuits to be handed to the verifier.

Each engine will be configurable with respect to its memory model and prover backend -- as checked by a compatibility layer -- and will also expose a set of properties indicating whether it supports key features (e.g., a private input tape, 32-bit vs. 64-bit architecture, various precompiles when they become available, etc.). Each engine will also be opinionated about its configuration, so that the vast majority of users should need to do no more than {NameOf}Engine::default(), while expert users have access to all possible (valid) configurations.

The prover backend will be the secondary object of the SDK/CLI. It itself will be configurable, e.g., with choice of whether to operate in sequential or PCD mode, as well as with its commitment scheme (pair) and curve (pair). Similarly, it will have compatibility checks and be opinionated about what defaults should be. Backends will also support a set of helpful property checks (e.g., whether they are recursive, Ethereum verifiable, support compression, etc.).

Interface

As for the user API exposed by the SDK, the goal is to support operation chaining using the ? operator. Ideally, we want the user to be able to write something like:

let vm = {NameOf}Engine::default()
             .load('/path/to/binary/')?
             .set_input<T>(input)
             .execute()?
             
assert!(vm.started());
assert!(vm.halted());
assert!(!vm.proven());

check(vm.output)?; // some user function returning Result<(), Error> checking that the output looks right

vm.rewind(); // do not clear loaded binary or input tape, as compared to vm.reset()

assert!(!vm.started());
assert!(!vm.halted());
 
vm.enable_prover_mode();
vm.prover.enable_sequential(); // likely to be the default
assert!(vm.is_proving());
 
vm.generate()?
  .execute()?; // alternatively, .prove()?
  .verify()?
  
assert!(vm.started());
assert!(vm.halted());
assert!(vm.proven());
assert!(vm.verified());

if vm.prover.can_compress() {
    vm.compress()?
    assert!(vm.compressed());
}

vm.proof 

I/O

For I/O (into engines that support it), we will use postcard to support serializing/deserializing arbitrary structs that implement Serde::Serialize and Serde::Deserialize. Essentially, the API (and so SDK) will support two interfaces to each of the public and private tapes:

-- set_input
-- set_input_bytes
-- set_public_input
-- set_public_input_bytes

Internal to the engines that support I/O, these are mirrored:

-- read_input
-- read_input_bytes
-- read_public_input
-- read_public_input_bytes

The bytes entries just read in and out arbitrary sequences of bytes. The non-bytes entries are generic, single-use functions, trait bound by Serde::Serialize + Serde::Deserizialize, that take care of serializing and deserializing information accordingly so that users never need to touch the raw bytes.

Compile-time Configuration

The last major piece of the early design is a compilation hook. This will be an (entirely optional) function that allows the user to trigger compilation + linkage of their program programmatically, through cargo. The main use case of this function will be to dynamically support emitting the linker, thereby enabling setting the memory limit through the SDK (per #152). The goal here will be to allow the user to provide a callback to do arbitrary compilation steps, with a default callback that just initiates the compilation, similar to: https://github.com/a16z/jolt/blob/c9bfe3226b8be6d5012495a7e2c72605980c6ae1/jolt-core/src/host/mod.rs#L93

[mx00s]

The proposed Prover trait and the sample interface code are both helping me get a taste of where we are and potential directions we can go.

Highlighting a couple points that resonate with me:

This is relevant because we already have Nova(seq), Nova(pcd), Nova(pcd+spartan), HyperNova soon, maybe Jolt which is going to be different.
There's no convenient way of switching between these.

Yes, there are so many potential configurations, both now and in the future, and it's not a simple matter to swap them in and out.

Each engine will also be opinionated about its configuration, so that the vast majority of users should need to do no more than {NameOf}Engine::default(), while expert users have access to all possible (valid) configurations.

Definitely, it makes sense that we'd want both.

General princples we seem aligned on

1. Internally, we want the flexibility to evolve implementation details to support executing multiple VM configurations with few code changes.
2. Externally, we want to expose an opinionated set of configurations that are well tested and offer a consistent and ergonomic UX.

To make that a bit more concrete, a likely implementation strategy is that (1) involves traits and generic parameters and (2) provides wrapper types that handle selecting generic type arguments and the construction of those internal values.

Additional proposed principles

1. The aformentioned compositional pattern can sensibly be used at varying layers of abstraction, not solely as part of the API/SDK distinction.
2. As much as reasonable, minimize API/SDK dependence by leaking 3rd party types, and even std, for types we consume and produce via items with pub visibility.

For example, workshopping on the I/O concept to make flexible internal abstractions:

extern crate alloc;

use alloc::vec::Vec;

enum Error {
    // TODO
}

trait RawInputTape {
    fn read_byte(&mut self) -> Option<u8>;
}

trait RawOutputTape {
    fn write_byte(&mut self, byte: u8) -> Result<(), Error>;
}

impl RawInputTape for Vec<u8> {
    fn read_byte(&mut self) -> Option<u8> {
        self.pop()
    }
}

impl RawOutputTape for Vec<u8> {
    fn write_byte(&mut self, byte: u8) -> Result<(), Error> {
        self.push(byte);
        // TODO: handle failed memory allocation
        Ok(())
    }
}

trait RawProof {}
trait RawVirtualMachine<I, O>
where
    I: RawInputTape,
    O: RawOutputTape,
{
    type Proof: RawProof;
    
    fn run(&mut self, input: I) -> Result<(O, Self::Proof), Error>;
}

This allows us to keep the engine's interfaces as minimal as possible to reduce the cost of adding more implementations.

For ergonomic conveniences like input serialization and output deserialization (which could happen outside proof machinery) we could wrap those abstractions in high-level ones. Implementations of these higher-level abstractions would automatically work with all of the engines implementing the core abstractions they consume:

trait InputValue {
    fn serialize<I: RawInputTape>(&self) -> Result<I, Error>;
}

trait OutputValue {
    fn deserialize<O: RawOutputTape>(tape: &O) -> Result<Box<Self>, Error>;
}

struct UserInput;
impl InputValue for UserInput {
    fn serialize<I: RawInputTape>(&self) -> Result<I, Error> {
        todo!();
    }
}

struct UserOutput;
impl OutputValue for UserOutput {
    fn deserialize<O: RawOutputTape>(tape: &O) -> Result<Box<Self>, Error> {
        todo!();
    }
}

trait VirtualMachine<I, O>
where
    I: InputValue,
    O: OutputValue,
{
    type Input: RawInputTape;
    type Output: RawOutputTape;
    type Proof: RawProof;
    type Core: RawVirtualMachine<Self::Input, Self::Output, Proof = Self::Proof>;
    
    fn core(&mut self) -> &mut Self::Core;
    
    fn run(&mut self, input: I) -> Result<(O, Self::Proof), Error> {
        let input: Self::Input = input.serialize()?;
        let (output, proof) = self.core().run(input)?;
        let output = O::deserialize(&output)?;
        Ok((*output, proof))
    }
}

There's a lot more we could do with traits to model valid machine state transitions through UX interactions @sjudson alludes to in their sample code and @slumber's mention of "stepped CLI output".

EDIT: I realize now, and confirmed with @sjudson, that the point of postcard is to incorporate input serialization and output deserialization in the proofs. That's likely still be possible with a trait design following the principles I suggested, but maybe it makes sense to incrementally refine the abstractions/implementations.

[sjudson]

Here is the current sketch of the basic SDK structure.

The core object of the SDK is an engine, which captures a vm + arithmetization. At time of writing, we will have two engines:

NVMEngine { ... }
JoltEngine { ... }

Each implements the Engine trait, which defines the primary API users interact with:

pub trait Engine: Default + Clone {
    /// The memory model to be used by the VM.                                                                                                                                                                        
    type Memory: Memory;

    // setup                                                                                                                                                                                                          

    /// Load the ELF file at `path` into the VM.                                                                                                                                                                      
    fn load(&mut self, path: &PathBuf) -> Result<&mut Self, NexusError>;

    /// Load the indicated test machine into the VM.                                                                                                                                                                  
    fn load_test_machine(&mut self, machine: &String) -> Result<&mut Self, NexusError>;

    // configuration                                                                                                                                                                                                  

    /// Load VM configuration from a `NexusVMConfig` object.                                                                                                                                                          
    fn from_config(&mut self, config: NexusVMConfig) -> Result<&mut Self, NexusError>;

    /// Print debugging trace of the VM execution.                                                                                                                                                                    
    fn enable_debug_execution_mode(&mut self) -> Result<&mut Self, NexusError>;

    /// When executing the VM, generate a proof.                                                                                                                                                                    
    fn enable_prover_mode(&mut self) -> Result<&mut Self, NexusError>;

    /// Set choice of prover, using its defaults.                                                                                                                                                                     
    fn set_defaulted_prover(&mut self, prover: &ProverImpl) -> Result<&mut Self, NexusError>;

    /// Set choice of prover.                                                                                                                                                                                         
    fn set_prover(&mut self, prover: &impl Prover) -> Result<&mut Self, NexusError>;

    /// Set `k` parameter that captures how many VM cycles should be proven per step.                                                                                                                                 
    fn set_k(&mut self, k: usize) -> Result<&mut Self, NexusError>;

    // input                                                                                                                                                                                                          

    /// Serialize the input of type `T` for reading as private input in the VM.                                                                                                                                       
    fn set_input<T: Serialize>(&self, input: T) -> Result<&mut Self, NexusError>;

    /// Serialize the input byte slice for reading as private input in the VM.                                                                                                                                        
    fn set_input_bytes(&self, input: &[u8]) -> Result<&mut Self, NexusError>;

    /// Serialize the input of type `T` for reading as public input in the VM.                                                                                                                                        
    fn set_public_input<T: Serialize>(&self, input: T) -> Result<&mut Self, NexusError>;

    /// Serialize the input byte slice for reading as public input in the VM.                                                                                                                                         
    fn set_public_input_bytes(&self, input: &[u8]) -> Result<&mut Self, NexusError>;

    // running

    /// Generate public parameters for proving the VM execution.                                                                                                                                                      
    fn generate(&self) -> Result<&mut Self, NexusError>;

    /// Execute the VM.                                                                                                                                                                                               
    fn execute(&self) -> Result<&mut Self, NexusError>;

    /// Execute the VM and generate a proof of its execution.                                                                                                                                                         
    fn prove(&self) -> Result<&mut Self, NexusError>;

    /// Verify a proven VM execution.                                                                                                                                                                                 
    fn verify(&self) -> Result<&mut Self, NexusError>;

    /// Rewind the VM, without clearing the loaded program or inputs.                                                                                                                                                 
    fn rewind(&self) -> Result<&mut Self, NexusError>;

    /// Reset the VM, including clearing the loaded program and inputs.                                                                                                                                               
    fn reset(&self) -> Result<&mut Self, NexusError>;

    // status                                                                                                                                                                                                         

    /// Indicates whether configured to generate a proof when executing.                                                                                                                                              
    fn proving(&self) -> bool;

    /// Indicates whether configured to print debug output for program execution.                                                                                                                                     
    fn debugging_execution(&self) -> bool;

    /// Indicates whether program execution has started.                                                                                                                                                              
    fn started(&self) -> bool;

    /// Indicates whether program execution has halted.                                                                                                                                                               
    fn halted(&self) -> bool;

    /// Indicates whether program execution has been proven.                                                                                                                                                          
    fn proven(&self) -> bool;

    /// Indicates whether proof of program execution has been verified.                                                                                                                                               
    fn verified(&self) -> bool;
}  

Note that functions which update the state of the engine return &mut Self, enabling chaining of calls:

let vm = NVMEngine::default()
             .load(PathBuf::from(r"/path/to/binary/"))?
             .set_input<T>(input)?
             .execute()?

Internally, an engine is configured with a Prover, defined by the trait:

#[derive(Default)]
enum ProverArch {
    #[default]
    Local,
}

pub trait Prover: Default + Clone {
    /// The proving architecture used to prove the trace.                                                                                                                                                             
    type Arch: ProverArch;

    /// The memory proof form used in the trace.                                                                                                                                                                      
    type MemoryProof: MemoryProof;

    /// Generate public parameters for proving.                                                                                                                                                                       
    fn generate(&self, k: usize) -> Result<(), NexusError>;

    /// Prove a VM trace.                                                                                                                                                                                             
    fn prove(&self, trace: Trace<Self::MemoryProof>) -> Result<(), NexusError>;

    /// Verify a proven VM execution.                                                                                                                                                                                 
    fn verify(&self) -> Result<(), NexusError>;
}

The ProverArch enum captures the possible backends that handle the proving, like local vs. cloud vs. network.

The set of compatible provers for a given engine is defined by an engine specific trait. For example, NVMEngine is paired with an IsNVMProver trait that NovaProver implements, while JoltEngine is paired with an IsJoltProver trait that JoltProver implements. At the moment these traits are empty, but could be used for specific engines to add particular functionalities they require from their provers.

At present there is no generic support: specific provers are concrete in both proving architectures + other proof specific generics (such as choice of curve), as is specified by the api crate (following #170).

[danielmarinq]

This looks great

[slumber]

// It shouldn't be hidden within a trait impl how to load from fs
// returns &mut Self?
fn load(&mut self, path: &PathBuf) -> Result<&mut Self, NexusError>;
// Probably should be omitted as well, or maybe autoimplemented.
fn load_test_machine(&mut self, machine: &String) -> Result<&mut Self, NexusError>;

// All these methods could go into NexusVMConfig                                                                                                                                                                
fn enable_debug_execution_mode(&mut self) -> Result<&mut Self, NexusError>;                                                                                                                                                           
fn enable_prover_mode(&mut self) -> Result<&mut Self, NexusError>;                                                                                                                                                                   
fn set_defaulted_prover(&mut self, prover: &ProverImpl) -> Result<&mut Self, NexusError>;                                                                                                                            
fn set_k(&mut self, k: usize) -> Result<&mut Self, NexusError>;

// Either of 2, otherwise this is like trying to bypass Rust rules for conflicting implementations
// because [u8] also implements Serialize.                                                                                                                              
fn set_input<T: Serialize>(&self, input: T) -> Result<&mut Self, NexusError>;                                                                                                                               
fn set_input_bytes(&self, input: &[u8]) -> Result<&mut Self, NexusError>;

// This is present in the prover trait, which one to use?
fn generate(&self) -> Result<&mut Self, NexusError>;

// Doesn't `enable_prover_mode` eliminate 1 of 2?
fn execute(&self) -> Result<&mut Self, NexusError>;                                                                                                                                                  
fn prove(&self) -> Result<&mut Self, NexusError>; 

// and so on

IMO as with the RPC pr, trying to put every possible configuration and generic into the first implementation does more bad than good. Usual software engineering practice is to build from small code, introducing such huge traits puts a maintenance burden. Like start with a single trait that only knows how to prove/verify, merge it, add some vm configurations, make it further configurable with memory layout etc.

At this point it looks like I keep blocking work on sdk, so feel free to unblock #170

[mx00s]

I broadly agree with @slumber's feedback.

Here are some additional thoughts:

1. Consider having Engine::load take a P: AsRef<Path> instead of a &PathBuf. This more flexible and align with std conventions.
2. Consider having Engine::load_test_machine take a &str instead of &String.
3. Many methods take &self instead of &mut self, yet return a Result<&mut Self, ...>. Wouldn't they need to take &mut self if they're actually mutating the provided object?
4. Is Engine::enable_prover_mode needed when there's both Engine::execute and Engine::prove?
5. Are Engine::set_prover and Engine::set_defaulted_prover needed or could their effects be coded into the various Engine impls?
6. How is the ProverImpl type defined? Should it be &impl Prover?
7. Consider changing the names of the private Engine::set_input* to clarify that they're for private inputs only.
8. Consider using "typestate" to constrain the permissible execution flows through the // running methods, e.g. Engine::generate could return a Result<Self::PublicParams, NexusError> and then both Engine::prove and Engine::verify could consume those params as an arg.
9. The // status methods like Engine::started, Engine::proven, and Engine::verified are a bit confusing. I imagine they may make sense if the // running methods could be executed concurrently, e.g. via async, but in that case the user would have freedom to decide whether/where to .await on those methods and keep track for themselves.

It may be helpful to tackle #165 and iterate on cleaning up that test until it feels both ergonomic and sufficiently configurable and extensible.

[sjudson]

Responding directly to @mx00s since they were a bit more concrete, but this also applies to some of your comments too @slumber.

Consider having Engine::load take a P: AsRef instead of a &PathBuf. This more flexible and align with std conventions.

Sure.

Consider having Engine::load_test_machine take a &str instead of &String.

Also sure.

Many methods take &self instead of &mut self, yet return a Result<&mut Self, ...>. Wouldn't they need to take &mut self if they're actually mutating the provided object?

Sorry yes, that's a typo (I accidentally reverted a search + replace before copying).

Is Engine::enable_prover_mode needed when there's both Engine::execute and Engine::prove?

I debated this. The flow I was concerned with enabling looks like:

let engine = ...;

if check_something() {
  engine.enable_prover_mode();
}

engine.execute(); // generates proof depending on what check_something() returns

Alternatively, if the user necessarily knows they will always want a proof generated, they can just do

engine.prove();

without having to think about it twice. If you are really opposed to having two ways to do the same thing like this, then I'd probably err on the side of getting rid of Engine::prove and forcing the setting of Engine::enable_prover_mode.

Are Engine::set_prover and Engine::set_defaulted_prover needed or could their effects be coded into the various Engine impls?

How is the ProverImpl type defined? Should it be &impl Prover?

These are roughly the same question: ProverImpl is used by VmConfig, and is just an enum naming the possible prover implementations. The idea here is that Engine::set_prover allows the user to manually construct Prover, while Engine::set_defaulted_prover allows the user to specify choice of Prover through just indicating the relevant enum variant, with {prover}::default() then used to construct it.

Consider changing the names of the private Engine::set_input* to clarify that they're for private inputs only.

Sure.

Consider using "typestate" to constrain the permissible execution flows through the // running methods, e.g. Engine::generate could return a Result<Self::PublicParams, NexusError> and then both Engine::prove and Engine::verify could consume those params as an arg.

This would require breaking the function call chaining paradigm (which we can, of course, do). I find the call chaining paradigm to be more misuse resistant: the user never actually has to touch, e.g., the public parameters or carry them through to the right place as an argument, but instead just needs to specify the order of operations (which they'd have to do either way).

The // status methods like Engine::started, Engine::proven, and Engine::verified are a bit confusing. I imagine they may make sense if the // running methods could be executed concurrently, e.g. via async, but in that case the user would have freedom to decide whether/where to .await on those methods and keep track for themselves.

These were formulated with the idea that an engine can be in a variety of states (has [no] program, has [no] input, has [not] generated proof, has [not] generated parameters, etc.), and we don't want to be presumptive about if and when the calling code will want to programmatically check which state it is in. The calling context being async (or, in the future, the calling context and proving architecture both being async) is certainly one possible motivation, but I'd rather provide a safe interface for directly and affirmatively checking status, than forcing the calling code to have to derive it from context.

[mx00s]

Is Engine::enable_prover_mode needed when there's both Engine::execute and Engine::prove?

I debated this. The flow I was concerned with enabling looks like:

let engine = ...;

if check_something() {
  engine.enable_prover_mode();
}

engine.execute(); // generates proof depending on what check_something() returns

I'm not sure I follow the benefit of that flow over something like this:

let engine = ...;

if check_something() {
    engine.prove();
} else {
    engine.execute();
}

The way the user inspects the state of the returned/mutated engine would also need to vary depending on the value of check_something() anyway. If and only if engine.enable_prover_mode() had been called the user would presumably want to inspect the proof.

I find the call chaining paradigm to be more misuse resistant: the user never actually has to touch, e.g., the public parameters or carry them through to the right place as an argument, but instead just needs to specify the order of operations (which they'd have to do either way).

I agree on the desire for misuse resistance.

I also find method chaining convenient, and tend to use it a lot when constructing objects with a broad spectrum of configurations. However, object construction is typically more of a concern for concrete types whereas traits (aside from Default) are relatively focused on providing an interface to support a very specific behavior across many types.

Typestate is a tactic that enforces operational constraints at compile-time and thereby improves misuse resistance. Here's an illustrative article that includes examples with method chaining.

I think is worth revisiting an important point @slumber made:

..., introducing such huge traits puts a maintenance burden. Like start with a single trait that only knows how to prove/verify, merge it, add some vm configurations, make it further configurable with memory layout etc.

Simple interfaces will lower the barrier to adding new implementations. Constraining the behaviors of those interfaces through types and generic tests will also help everyone be confident things will work when swapping one implementation for another.

I'm curious how far we could go with an interface like this, for instance:

trait Prover {
    type Program;
    type PublicInput;
    type PrivateInput;
    type Output;
    type Proof: Verifiable;
    type Error;
    
    fn prove(
        program: &Self::Program,
        public_input: &Self::PublicInput,
        private_input: &Self::PrivateInput,
    ) -> Result<(Self::Output, Self::Proof), Self::Error>;
}

trait Verifiable {
    type Error;

    fn verify(&self) -> Result<(), Self::Error>;
}

...or perhaps even this assumes to much in general, e.g. will inputs--both public and private--definitely be supported on all prover/verifier implementations we ever offer?

EDIT: Here's a Rust playground with fake implementations of those traits and a happy-path usage example. I personally find it helpful to motivate trait design by writing tests from the consumer's perspective.

[sjudson]

Resolved by #208