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

feat: triton-cli prove/verify, proof binary serialization #305

Open
wants to merge 27 commits into
base: master
Choose a base branch
from

Conversation

chancehudson
Copy link

@chancehudson chancehudson commented Jul 11, 2024

This PR adds a new crate triton-cli. This crate exposes a cli with two commands

  • prove: read asm from file, prove it, and write the resulting proof to file
  • verify: read a proof from file, verify it, and print details about it

Proofs are serialized in a simple binary format. This format is described in the main.rs for the cli crate.

From inside the triton-cli directory run cargo install --path . to add the triton-cli to your path.

> triton-cli prove ./simple.asm out.proof --private-inputs=12412414,9 --public-inputs 214
proving...
success!
proof written to: out.proof
>
> triton-cli verify out.proof
proof is valid!
program digest: 0xbd500d8c2bc5b683fe957fa7e2525808b1eb113ad21a99044eec82abdff548e6f27d8b1429c6eaef
=================
security level: 160 bits
FRI expansion factor: 4
trace randomizers: 166
colinearity checks: 80
codeword checks: 160
=================
public inputs:
(none)
public outputs:
(none)
>

Things to watch out for:

  • proof data is written non-atomically, halting the process can create a corrupt proof file
  • inputs are not implemented
  • the binary format describes lengths as "number of 64-bit words" instead of number of bytes

Closes #238

@aszepieniec
Copy link
Collaborator

Thanks for the contribution! And sorry for the slow follow-up. You seem to have caught @jan-ferdinand in the middle of one of his rare holidays, and he's the boss when it comes this repo.

Have you seen triton-tui? It's the debugger we use for Triton VM programs. We are not looking per se for a single tool that does everything (although that is an option), but it would be nice if the two tools had the same invocation syntax and interchangeable file formats, at least as far as programs, inputs, outputs, and nondeterminism go. If memory serves, triton-tui uses clap for command-line arguments and you can lift the format for inputs from there.

Have you considered adding a run command to produce an output? Furthermore, the ability to supply nondeterminism is certainly necessary if one wishes to make zero-knowledge proofs meaningful.

@chancehudson
Copy link
Author

Hey @aszepieniec thanks for the review. I based the cli on the feedback in #299. I wanted to see if there were any ideas on how to implement inputs (private and public). Naively i'd probably implement it as two optional flags on the prove command, each accepting a comma separated list of values. The next step from that would be passing files in some format.

@chancehudson
Copy link
Author

This PR isn't time sensitive though, i've got a local copy of the cli i'm using for debugging so there's no rush here

Copy link
Member

@jan-ferdinand jan-ferdinand left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is really shaping up! Thanks a lot for your effort with this.

I have left various questions and comments in-line. Additionally, I have the following general comments:

  • It seems like a good idea to support all 3 types of private input (collectively known as NonDeterminism):
    • individual tokens, which can be used by instruction divine – this is already supported
    • initial RAM, which can be used by any instruction accessing memory
    • non-deterministic digests, which can be accessed by instruction divine_sibling1
  • The user experience might become better if the error-propagation crate anyhow was used. By changing signature of main() to return an anyhow::Result<()>, errors can be propagated all the way to the program's entrypoint. This removes the need for many a .unwrap() or .expect().

Footnotes

  1. divine_sibling is soon to be replaced by merkle_step, but that will not change the behavior of NonDeterminism

triton-cli/src/main.rs Outdated Show resolved Hide resolved
triton-cli/src/main.rs Outdated Show resolved Hide resolved
triton-cli/src/main.rs Outdated Show resolved Hide resolved
triton-cli/src/main.rs Outdated Show resolved Hide resolved
}
}

fn digest_to_str(d: Digest) -> String {
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

In the next version of triton-vm, the method digest.to_hex() will be available. This will guarantee that hex-ified digests are consistent everywhere. 😊

triton-cli/src/main.rs Outdated Show resolved Hide resolved
triton-cli/src/main.rs Outdated Show resolved Hide resolved
triton-cli/src/main.rs Outdated Show resolved Hide resolved
Comment on lines 114 to 136
// write the proof in an arbitrary binary format
//
// version: u8
//
// security_level: u64
// fri_expansion_factor: u64
// num_trace_randomizers: u64
// num_colinearity_checks: u64
// num_combination_codeword_checks: u64
//
// digest_length: u8
// public_input_length: u64
// public_output_length: u64
// proof_length: u64
//
// program_digest: u64[digest_length]
//
// public_inputs: u64[public_input_length]
// public_outputs: u64[public_output_length]
// proof: u64[proof_length]
write_proof(data, out).expect("failed to write proof to file");
println!("proof written to: {out}");
}
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Instead of (de)serializing ad-hoc, how about using libraries built for exactly that purpose instead? In the example below, I'm using serde and bincode, but other alternatives might exist.

#[derive(Debug, Clone, Eq, PartialEq, Serialize, Deserialize)]
struct SerializableProof {
    version: u8,
    stark: Stark,
    claim: Claim,
    proof: Proof,
}

fn write_proof(proof_path: &str, (stark, claim, proof): (Stark, Claim, Proof)) -> Result<()> {
    let serializable_proof = SerializableProof {
        version: 1,
        stark,
        claim,
        proof,
    };
    let encoded = bincode::serialize(&serializable_proof)?;
    fs::write(proof_path, &encoded)?;
    Ok(())
}

fn read_proof(proof_path: &str) -> Result<(Stark, Claim, Proof)> {
    let encoded = fs::read(proof_path)?;
    let SerializableProof {
        version,
        stark,
        claim,
        proof,
    } = bincode::deserialize(&encoded)?;
    if version != 1 {
        bail!("unsupported proof version: {version}"); // uses crate `anyhow`
    }
    Ok((stark, claim, proof))
}

This is probably not the final version of the code yet: in the suggestion, the proof's version is embedded in the struct SerializableProof. However, in order to actually support different proof versions, it should probably be parsed first, and subsequent parsing should then depend on the version.

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is probably not the final version of the code yet: in the suggestion, the proof's version is embedded in the struct SerializableProof. However, in order to actually support different proof versions, it should probably be parsed first, and subsequent parsing should then depend on the version.

Yes, i really just wanted to reserve the first byte so in the future it's possible to implement versioning.

I didn't use a library because i'm not familiar with them. In the example above, will changes to the Stark, Claim, or Proof struct (or any nested structs) change the file structure? I'm not opposed to using libraries but I think it's important that the file structure is well documented/stable so others can write parsers in other languages. Explicitly writing the file byte by byte is an easy way to do that.

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I guess my question is, how do we make sure version is changed anytime the Stark/Claim/Proof struct is modified?

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I ended up making a custom struct and using serde+bincode with that.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I guess my question is, how do we make sure version is changed anytime the Stark/Claim/Proof struct is modified?

Yeah, that's a super valid question. My proposed “solution” falls short on at least two counts:

  • since the version is a field on the struct itself, making de-serialization conditional to the version doesn't work
  • it's not obvious (to me) how to ensure correct versioning if any of Stark, Claim, or Proof's format changes

A custom (de)serializer certainly allows addressing both of those shortcomings. That said, it feels as if this is a problem other people have encountered before, and have provided a general solution for. Maybe this solution is serde ∧/∨ bincode, but I'm not sure. I'll take another look. 😌

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, i really just wanted to reserve the first byte so in the future it's possible to implement versioning.

That is a super good idea as far as I can see. 👍

triton-cli/test-vectors/simple.tasm Show resolved Hide resolved
@chancehudson
Copy link
Author

@jan-ferdinand great review, thank you

initial RAM, which can be used by any instruction accessing memory

I was just about to open an issue asking about initial RAM. I'm not sure how to specify this for a program, do you have any links that could help me?

non-deterministic digests, which can be accessed by instruction divine_sibling

Also something I'm not familiar with. I've read the divine_sibling docs but I didn't fully understand how the instruction is meant to be used.

I'm kinda thinking that these additional methods of specifying inputs should be added in separate pr's.

The user experience might become better if the error-propagation crate anyhow was used. By changing signature of main() to return an anyhow::Result<()>, errors can be propagated all the way to the program's entrypoint. This removes the need for many a .unwrap() or .expect().

Looking into this rn

@chancehudson
Copy link
Author

The anyhow crate is great. I've been struggling to figure out clean error handling and this crate basically solves it

@jan-ferdinand
Copy link
Member

The anyhow crate is great. I've been struggling to figure out clean error handling and this crate basically solves it

Should you ever be looking for something similar but for a library, check out thiserror. Same author, and also super convenient to use. Both thiserror and anyhow refer to each other in their readmes, so it's easy to look up which one is better suited for which use case. 😌

@jan-ferdinand
Copy link
Member

@jan-ferdinand great review, thank you

Happy to! 😊

I'm not sure how to specify [initial RAM] for a program, do you have any links that could help me?

Yeah, the docs on this are not super great, I have to admit. 🙇 There are various answers to your question.

  • NonDeterminism has a method fn with_ram(self, ram: HashMap<BFieldElement, BFieldElement>) -> Self1 which allows to to specify the initial RAM.
  • It's not obvious how to let a user specify initial RAM as conveniently as possible. Triton TUI uses a JSON file for all three types of private input, for example like so. When starting the TUI, the path to such a JSON file can be given as one of the command line arguments. There might be better ways to go about this and I'm happy to discuss alternatives. 😌

I've read the divine_sibling docs but I didn't fully understand how the instruction is meant to be used.

Yeah, divine_sibling is a bit of a special kid. The intention is to simplify verification of inclusion of elements in a Merkle tree. Without the context of Merkle trees, the instruction probably won't make a whole lot of sense. That said, let's take the following Merkle tree:

image

The node's indices are green, the parent/child relation is marked by the black lines. The tree's root has index 1.2 Let's assume you want to walk the authentication path for node 10. In the picture, the authentication path in question is marked by red circles. To compute node 10's parent, which is node 5, you also need to know node 11. Hashing left sibling (node 10) and right sibling (node 11) gives the parent (node 5). In order to get node 5's parent, you also need node 4. Again, hashing left sibling (node 4) and right sibling (node 5), gives the parent (node 2).
Crucially, it is important that the left sibling is on the left; hashing right sibling and left sibling (concatenated in this order) gives a different result from hashing left sibling and right sibling (in this order).

Now, instruction divine_sibling takes care of a few things in order to simplify walking an authentication path. Note how sometime, the already-known-sibling is on the left, and sometimes, it is on the right.3 Instruction divine_sibling takes care that the known sibling is moved to the correct side, and that the unkown sibling is “divinely” guessed and put to the other side. Then, calling instruction hash gives the parent node. That means that moving up three layers of a Merkle tree is as easy as writing divine_sibling hash divine_sibling hash divine_sibling hash.4

Of course, this produces the correct result only if the private input for sibling digests, also known as “non-deterministic digests”, is correctly populated. Feel free to ask additional questions. 😌

I'm kinda thinking that these additional methods of specifying inputs should be added in separate pr's.

That's fine with me. 🙂👍

Footnotes

  1. the signature is slightly more general, but you get the idea

  2. For Merkle trees, 1-indexing is easier than 0-indexing, hence a break from the norm.

  3. The least significant bit of the node index is a fast way to identify which side the sibling is on.

  4. Upcoming instruction merkle_step simplifies this to merkle_step merkle_step merkle_step.

triton-cli/src/main.rs Outdated Show resolved Hide resolved
triton-cli/src/main.rs Outdated Show resolved Hide resolved
triton-cli/src/main.rs Outdated Show resolved Hide resolved
triton-cli/src/main.rs Outdated Show resolved Hide resolved
triton-cli/src/main.rs Outdated Show resolved Hide resolved
triton-cli/src/main.rs Outdated Show resolved Hide resolved
triton-cli/test-vectors/simple.tasm Outdated Show resolved Hide resolved
triton-cli/src/main.rs Outdated Show resolved Hide resolved
triton-cli/src/main.rs Outdated Show resolved Hide resolved
triton-cli/src/main.rs Outdated Show resolved Hide resolved
@chancehudson
Copy link
Author

Great explanation of divine_sibling, thanks.

Of course, this produces the correct result only if the private input for sibling digests, also known as “non-deterministic digests”, is correctly populated. Feel free to ask additional questions. 😌

The explanation makes sense, though i'll need to play with it more to understand it fully. My only question is, what motivated you to implement this at the VM level instead of the program level? Or rather, how much overhead (if any) does it add to programs that don't use the instruction? Or is it necessary for making the stark proof itself?

@jan-ferdinand
Copy link
Member

what motivated you to implement this at the VM level instead of the program level?

It's an optimization for recursive verification and not required to generate a STARK proof. An alternative to having the instruction would be something along the lines of:

; never run, never tested – likely to contain bugs
divine 5	; get the sibling digest
dup 10		; duplicate the node index
push 2
div_mod
pop 1		; least-significant bit of node index is now on top of the stack
skiz
	call swap_digests ; requires something like 15 instruction? I didn't count

When verifying a STARK, there are many Merkle tree verifications happening, each of which requires several executions of divine_sibling. If we were to replace the instruction with the program outlined above, the blow-up factor of roughly 20 would hurt a lot. In fact, the main reason for introducing merkle_step1 and removing divine_sibling is how many instructions it saves us – and that's with a reduction of 2 $\rightarrow$ 1!

You are right in assuming that there is an overhead to having this instruction around. And unfortunately, this overhead is something that everyone using Triton VM is paying, independend of them using the instruction. It is possible to design ZK-VMs that mitigate this to a certain degree, but Triton VM has not adopted any of those mitigation strategies yet; our current focus is elsewhere. 😌
Quantifying the overhead is also not easy. It is possible to get numbers, but unfortunately, that requires significant changes to the code for the time being.

Footnotes

  1. merkle_step is equivalent to divine_sibling followed by hash

@cyberbono3
Copy link

@chancehudson Good job!

triton-cli/src/main.rs Outdated Show resolved Hide resolved
triton-cli/src/main.rs Show resolved Hide resolved
Comment on lines 121 to 133
#[derive(Serialize, Deserialize, Debug, Clone)]
struct SerializedProof {
version: u8,
security_level: u64,
fri_expansion_factor: u64,
num_trace_randomizers: u64,
num_colinearity_checks: u64,
num_combination_codeword_checks: u64,
program_digest: Vec<u64>,
public_inputs: Vec<u64>,
public_outputs: Vec<u64>,
proof: Vec<u64>,
}
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Getting this right seems to be more difficult (for me) than I had anticipated. I see more or less three main ways we can go about it:

  1. Declare proof versioning out of scope for Triton CLI.
  2. Detect out-of-sync versions and report them as an error.
  3. Support as many proof versions as possible.

1 – Declare Versioning to be Out of Scope

The simplest “solution” from an implementation standpoint. If deserialization fails, the cause might be an out-of-date proof, hard disk failure, aliens, …. The user can check for an update of Triton CLI and try their luck again.

2 – Error on Out-of-Sync Proof

Requires

  • storing the proof's version alongside the proof, and
  • knowing the version of Triton VM.

3 - Support Different Proof Versions

Requires everything from (2) plus old versions of Triton VM as additional dependencies. Then, proof generation / verification can be delegated to the chosen version. This is certainly possible by renaming dependencies. The biggest downside I see are compilation times and binary size – Triton VM is not a particularly leightweight library.

Detecting Versions

Of the Proof

For strategies 2 and 3, the proof's version must be accessible whether deserialization works or not. Here are suggestions that might work:

  1. Use the file's first few bytes for the proof's version, store the serialized proof in bytes[some_index..].
  2. Declare a big enum with one struct variant per proof version. For example:
#[derive(Debug, Clone, Serialize, Deserialize)]
enum VersionedSerializableProof {
	V0_13 { stark: triton_vm_0_13::Stark, claim:  triton_vm_0_13::Claim, .. },
	V0_22 { stark: triton_vm_0_22::Stark, claim:  triton_vm_0_22::Claim, .. },
	..
}

I'm not sure this works, though: I don't think serde is able to distinguish between two different versions of same type.

Of Triton CLI / VM

With strategy (2) “Error on out-of-sync proof”, the version of Triton VM in use must be known. The ways I see to achieve this, are:

  1. Use compile-time environment variable CARGO_PKG_VERSION via the env! macro to get a &'static str to the version specifier in the Cargo.toml of Triton CLI. Only works under the assumption that Triton CLI has the same version as Triton VM. Notably, this is not currently the case.
  2. Use a build.rs build script and some parsing of the Cargo.toml to populate a compile-time environment variable with the version of Triton VM in use, which can then be read via the env! macro.
  3. Manually update some hardcoded const whenever the version of Triton VM is bumped.

I must admit, none of these approaches seem particularly resilient.

What do you think? Do these thoughts and conclusions make sense? Am I overlooking something blatantly obvious?

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

In versioning we have 2 things that can change. The first is the structure of the binary file itself. This affects how we implement encoding/decoding, but does not necessarily affect how the proof is verified. The second is the version of triton-vm that generated the proof. This is much more difficult to handle because a proof might be (de)serialized just fine and then fail verification because e.g. the merkle structure was off by 1 or the hash function changed etc.

The first case is firmly in scope for this package. Anytime we change the SerializedProof structure we should keep the old structure/implementation somewhere and match into the old structure based on the version indicator until we explicitly drop support for a version. The second case seems mostly out of scope for this package. By that i mean, we should not try and support anything but the current version. The triton-cli version number should follow triton-vm. e.g. anytime a breaking version of triton-vm is released, a breaking triton-cli version should be released as well. I would lean into the versioning system here and use the CARGO_PKG_VERSION to throw an error if a proof is verified from the wrong major version.

The tricky part here is detecting when a breaking change is made to the STARK prover/verifier logic and strictly following versioning rules. I would commit a proof to this repo from the current version of triton-vm and have the CI attempt to verify this proof on every push. This will fail anytime a breaking change is made which is an indicator to push a breaking version release (or try to undo the breaking change). Sort of a makeshift e2e test.

I think to mitigate some of the risk here we can add more variables into the serialized proof. Namely:

  • name/identifier of hash function used
  • field/field extension used

This would add slightly more flexibility on detecting implementation details.

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I would handle this versioning stuff lazily though. Let's call these things the "proof file version" and the "prover version".

We start with proof file version 1, there are no other versions to support right now. We start with prover version 0.x.x. We specify that if the prover version is not defined in the proof file it is assumed to be 0.x.x.

To pedantically support this I think we need to add the CARGO_PKG_VERSION check logic to the prover/verification and throw an error on prover version >0.x.x. It would be good to add a comment near this logic documenting this conversation/plan.

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I applied this in 553a028.

I ended up putting the version in the proof file as it seemed more self-documenting.

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

BTW i don't know how rust versioning works. I'm using the semver mental model.

Comment on lines 150 to 160
assert_eq!(
DIGEST_LENGTH,
serialized_proof.program_digest.len(),
"digest length mismatch!"
);
let digest_elements = serialized_proof
.program_digest
.iter()
.map(|v| BFieldElement::from(*v))
.collect::<Vec<BFieldElement>>();
let digest = Digest::try_from(&digest_elements[0..DIGEST_LENGTH])?;
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You don't have to do the length check yourself if you pass the entire digest_elements into the try_from:

Suggested change
assert_eq!(
DIGEST_LENGTH,
serialized_proof.program_digest.len(),
"digest length mismatch!"
);
let digest_elements = serialized_proof
.program_digest
.iter()
.map(|v| BFieldElement::from(*v))
.collect::<Vec<BFieldElement>>();
let digest = Digest::try_from(&digest_elements[0..DIGEST_LENGTH])?;
let digest_elements = serialized_proof
.program_digest
.iter()
.map(|v| BFieldElement::from(*v))
.collect::<Vec<_>>();
let digest = Digest::try_from(digest_elements)?;

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

In fact, you can remove a lot of .iter().map(…)ing by changing the types used in the SerializedProof:

#[derive(Serialize, Deserialize, Debug, Clone)]
struct SerializedProof {
	..
    program_digest: Digest,
    public_inputs: Vec<BFieldElement>,
    public_outputs: Vec<BFieldElement>,
    proof: Vec<BFieldElement>,
}

All of these types (de)serialize just fine. 🙂

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I applied the first change passing the full vector to try_from. I thought about changing the types in SerializedProof, but this makes the file structure vulnerable to change if Digest or BFieldElement changes. That's why i'm unwrapping/re-wrapping into primitive types.

@chancehudson
Copy link
Author

Hey @jan-ferdinand thinking about this more it would be very useful if the triton-vm crate provided a standard way to serialize a proof. What is your opinion of pulling the serialization logic into triton-vm itself?

@jan-ferdinand
Copy link
Member

it would be useful if Triton VM provided a standard way to serialize a proof

I think this makes sense, yes.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

add command line tool for proof generation & verification
4 participants