triton_vm/
lib.rs

1//! Triton Virtual Machine is a Zero-Knowledge Proof System (ZKPS) for proving
2//! correct execution of programs written in Triton assembly. The proof system
3//! is a [zk-STARK](Stark), which is a state-of-the-art ZKPS.
4//!
5//! Generally, all arithmetic performed by Triton VM happens in the prime field with
6//! 2^64 - 2^32 + 1 elements. Instructions for u32 operations are provided.
7//!
8//! For a full overview over all available instructions and their effects, see the
9//! [specification](https://triton-vm.org/spec/instructions.html).
10//!
11//! [Triton VM's STARK](Stark) is parametric, but it is highly recommended to
12//! use the provided [default](Stark::default). Furthermore, certain runtime
13//! characteristics are [configurable](config), and usually don't need changing.
14//!
15//! # Non-Determinism
16//!
17//! Triton VM is a non-deterministic machine. That is,
18//! 1. Triton VM's random access memory can be initialized arbitrarily, and
19//! 1. for a select few instructions (namely `divine` and `merkle_step`),
20//!    correct state transition is not fully determined by the current state and
21//!    Triton VM's public input.
22//!
23//! The input for those non-deterministic instructions use dedicated input
24//! streams. Those, together with the initial RAM, are collectively called
25//! [`NonDeterminism`].
26//!
27//! # Examples
28//!
29//! Below are a few examples on how to use Triton VM. They show the instruction
30//! set architecture in action and highlight the core methods required to
31//! generate & verify a proof of correct execution. Some of these are
32//! convenience function [`prove_program()`] as well as the [`prove()`] and
33//! [`verify()`] methods.
34//!
35//! ## Factorial
36//!
37//! Compute the factorial of the given public input.
38//!
39//! The execution of the factorial program is already fully determined by the public input.
40//! Hence, in this case, there is no need for specifying non-determinism.
41//! Keep reading for an example that does use non-determinism.
42//!
43//! The [`triton_program!`] macro is used to conveniently write Triton assembly. In below example,
44//! the state of the operational stack is shown as a comment after most instructions.
45//!
46//! ```
47//! # use triton_vm::prelude::*;
48//! let factorial_program = triton_program!(
49//!     read_io 1           // n
50//!     push 1              // n 1
51//!     call factorial      // 0 n!
52//!     write_io 1          // 0
53//!     halt
54//!
55//!     factorial:          // n acc
56//!         // if n == 0: return
57//!         dup 1           // n acc n
58//!         push 0 eq       // n acc n==0
59//!         skiz            // n acc
60//!             return      // 0 acc
61//!         // else: multiply accumulator with n and recurse
62//!         dup 1           // n acc n
63//!         mul             // n acc·n
64//!         swap 1          // acc·n n
65//!         push -1 add     // acc·n n-1
66//!         swap 1          // n-1 acc·n
67//!         recurse
68//! );
69//! let public_input = PublicInput::new(bfe_vec![10]);
70//! let non_determinism = NonDeterminism::default();
71//!
72//! let (stark, claim, proof) =
73//!     triton_vm::prove_program(factorial_program, public_input, non_determinism).unwrap();
74//!
75//! let verdict = triton_vm::verify(stark, &claim, &proof);
76//! assert!(verdict);
77//!
78//! assert_eq!(1, claim.output.len());
79//! assert_eq!(3_628_800, claim.output[0].value());
80//! ```
81//!
82//! ## Non-Determinism
83//!
84//! In the following example, a public field elements equality to the sum of some squared secret
85//! elements is proven. For demonstration purposes, some of the secret elements come from secret in,
86//! and some are read from RAM, which can be initialized arbitrarily.
87//!
88//! Note that the non-determinism is not required for proof verification, and does not appear in
89//! the claim or the proof. It is only used for proof generation. This way, the verifier can be
90//! convinced that the prover did indeed know some input that satisfies the claim, but learns
91//! nothing beyond that fact.
92//!
93//! The third potential source of non-determinism is intended for verifying Merkle authentication
94//! paths. It is not used in this example. See [`NonDeterminism`] for more information.
95//!
96//! ```
97//! # use triton_vm::prelude::*;
98//! let sum_of_squares_program = triton_program!(
99//!     read_io 1                       // n
100//!     call sum_of_squares_secret_in   // n sum_1
101//!     call sum_of_squares_ram         // n sum_1 sum_2
102//!     add                             // n sum_1+sum_2
103//!     eq                              // n==(sum_1+sum_2)
104//!     assert                          // abort the VM if n!=(sum_1+sum_2)
105//!     halt
106//!
107//!     sum_of_squares_secret_in:
108//!         divine 1 dup 0 mul          // s₁²
109//!         divine 1 dup 0 mul add      // s₁²+s₂²
110//!         divine 1 dup 0 mul add      // s₁²+s₂²+s₃²
111//!         return
112//!
113//!     sum_of_squares_ram:
114//!         push 17                     // 18
115//!         read_mem 1                  // s₄ 17
116//!         pop 1                       // s₄
117//!         dup 0 mul                   // s₄²
118//!         push 42                     // s₄² 43
119//!         read_mem 1                  // s₄² s₅ 42
120//!         pop 1                       // s₄² s₅
121//!         dup 0 mul                   // s₄² s₅²
122//!         add                         // s₄²+s₅²
123//!         return
124//! );
125//! let public_input = PublicInput::from([bfe!(597)]);
126//! let secret_input = [5, 9, 11].map(|v| bfe!(v));
127//! let initial_ram = [(17, 3), (42, 19)].map(|(address, v)| (bfe!(address), bfe!(v)));
128//! let non_determinism = NonDeterminism::from(secret_input).with_ram(initial_ram);
129//!
130//! let (stark, claim, proof) =
131//!    triton_vm::prove_program(sum_of_squares_program, public_input, non_determinism).unwrap();
132//!
133//! let verdict = triton_vm::verify(stark, &claim, &proof);
134//! assert!(verdict);
135//! ```
136//!
137//! ## Crashing Triton VM
138//!
139//! Successful termination of a program is not guaranteed. For example, a program must execute
140//! `halt` as its last instruction. Certain instructions, such as `assert`, `invert`, or the u32
141//! instructions, can also cause the VM to crash. Upon crashing Triton VM, methods like
142//! [`run`](VM::run) and [`trace_execution`](VM::trace_execution) will return a
143//! [`VMError`]. This can be helpful for debugging.
144//!
145//! ```
146//! # use triton_vm::prelude::*;
147//! let crashing_program = triton_program!(push 2 assert error_id 42 halt);
148//! let vm_error = VM::run(crashing_program, [].into(), [].into()).unwrap_err();
149//! let InstructionError::AssertionFailed(ref assertion_error) = vm_error.source else {
150//!     unreachable!();
151//! };
152//!
153//! assert_eq!(Some(42), assertion_error.id);
154//! eprintln!("{vm_error}"); // inspect the VM state
155//! ```
156
157#![recursion_limit = "4096"]
158
159pub use air;
160pub use isa;
161pub use twenty_first;
162
163use isa::program::Program;
164
165use crate::error::ProvingError;
166use crate::prelude::*;
167
168pub mod aet;
169pub mod arithmetic_domain;
170pub mod challenges;
171pub mod config;
172pub mod constraints;
173pub mod error;
174pub mod example_programs;
175pub mod execution_trace_profiler;
176pub mod fri;
177pub mod memory_layout;
178mod ndarray_helper;
179pub mod prelude;
180pub mod profiler;
181pub mod proof;
182pub mod proof_item;
183pub mod proof_stream;
184pub mod stark;
185pub mod table;
186pub mod vm;
187
188#[cfg(test)]
189mod shared_tests;
190
191/// Prove correct execution of a program written in Triton assembly.
192/// This is a convenience function, abstracting away the details of the STARK construction.
193/// If you want to have more control over the STARK construction, this method can serve as a
194/// reference for how to use Triton VM.
195///
196/// Note that all arithmetic is in the prime field with 2^64 - 2^32 + 1 elements. If the
197/// provided public input or secret input contains elements larger than this, proof generation
198/// will be aborted.
199///
200/// The program executed by Triton VM must terminate gracefully, i.e., with instruction `halt`.
201/// If the program crashes, _e.g._, due to an out-of-bounds instruction pointer or a failing
202/// `assert` instruction, proof generation will fail.
203///
204/// The default STARK parameters used by Triton VM give a (conjectured) security level of 160 bits.
205pub fn prove_program(
206    program: Program,
207    public_input: PublicInput,
208    non_determinism: NonDeterminism,
209) -> Result<(Stark, Claim, Proof), ProvingError> {
210    // Set up the claim that is to be proven. The claim contains all public information. The
211    // proof is zero-knowledge with respect to everything else.
212    //
213    // While it is more convenient to construct a `Claim::about_program(&program)`, this API is
214    // purposefully not used here to highlight that only a program's hash digest, not the full
215    // program, is part of the claim.
216    let claim = Claim::new(program.hash()).with_input(public_input.clone());
217
218    // Generate
219    // - the witness required for proof generation, i.e., the Algebraic Execution Trace (AET), and
220    // - the (public) output of the program.
221    //
222    // Crashes in the VM can occur for many reasons. For example:
223    // - due to failing `assert` instructions,
224    // - due to an out-of-bounds instruction pointer,
225    // - if the program does not terminate gracefully, _i.e._, with instruction `halt`,
226    // - if any of the two inputs does not conform to the program,
227    // - because of a bug in the program, among other things.
228    // If the VM crashes, proof generation will fail.
229    let (aet, public_output) = VM::trace_execution(program, public_input, non_determinism)?;
230
231    // Now that the public output is computed, populate the claim accordingly.
232    let claim = claim.with_output(public_output);
233
234    // The default parameters give a (conjectured) security level of 160 bits.
235    let stark = Stark::default();
236
237    // Generate the proof.
238    let proof = stark.prove(&claim, &aet)?;
239
240    Ok((stark, claim, proof))
241}
242
243/// A convenience function for proving a [`Claim`] and the program that claim corresponds to.
244/// Method [`prove_program`] gives a simpler interface with less control.
245pub fn prove(
246    stark: Stark,
247    claim: &Claim,
248    program: Program,
249    non_determinism: NonDeterminism,
250) -> Result<Proof, ProvingError> {
251    let program_digest = program.hash();
252    if program_digest != claim.program_digest {
253        return Err(ProvingError::ProgramDigestMismatch);
254    }
255    let (aet, public_output) =
256        VM::trace_execution(program, (&claim.input).into(), non_determinism)?;
257    if public_output != claim.output {
258        return Err(ProvingError::PublicOutputMismatch);
259    }
260
261    stark.prove(claim, &aet)
262}
263
264/// Verify a proof generated by [`prove`] or [`prove_program`].
265///
266/// Use [`Stark::verify`] for more verbose verification failures.
267#[must_use]
268pub fn verify(stark: Stark, claim: &Claim, proof: &Proof) -> bool {
269    stark.verify(claim, proof).is_ok()
270}
271
272#[cfg(test)]
273mod tests {
274    use assert2::assert;
275    use assert2::let_assert;
276    use isa::instruction::LabelledInstruction;
277    use isa::instruction::TypeHint;
278    use proptest::prelude::*;
279    use proptest_arbitrary_interop::arb;
280    use test_strategy::proptest;
281    use twenty_first::prelude::*;
282
283    use crate::prelude::*;
284
285    use super::*;
286
287    /// The compiler automatically adds any applicable auto trait (all of which are
288    /// marker traits) to self-defined types. This implies that these trait bounds
289    /// might vanish if the necessary pre-conditions are no longer met. That'd be a
290    /// breaking API change!
291    ///
292    /// To prevent _accidental_ removal of auto trait implementations, this method
293    /// tests for their presence. If you are re-designing any of the types below
294    /// and a test fails as a result, that might be fine. You are now definitely
295    /// aware of a consequence you might not have known about otherwise. (If you
296    /// were already aware you know how subtle this stuff can be and are hopefully
297    /// fine with reading this comment.)
298    ///
299    /// Inspired by “Rust for Rustaceans” by Jon Gjengset.
300    fn implements_auto_traits<T: Sized + Send + Sync + Unpin>() {}
301
302    #[test]
303    fn public_types_implement_usual_auto_traits() {
304        // re-exports
305        implements_auto_traits::<BFieldElement>();
306        implements_auto_traits::<Digest>();
307        implements_auto_traits::<Tip5>();
308        implements_auto_traits::<XFieldElement>();
309
310        // prelude
311        implements_auto_traits::<LabelledInstruction>();
312        implements_auto_traits::<NonDeterminism>();
313        implements_auto_traits::<Program>();
314        implements_auto_traits::<PublicInput>();
315        implements_auto_traits::<Claim>();
316        implements_auto_traits::<Proof>();
317        implements_auto_traits::<Prover>();
318        implements_auto_traits::<Stark>();
319        implements_auto_traits::<Verifier>();
320        implements_auto_traits::<VM>();
321        implements_auto_traits::<VMState>();
322
323        // errors
324        implements_auto_traits::<error::VMError>();
325        implements_auto_traits::<error::ArithmeticDomainError>();
326        implements_auto_traits::<error::ProofStreamError>();
327        implements_auto_traits::<error::FriSetupError>();
328        implements_auto_traits::<error::FriProvingError>();
329        implements_auto_traits::<error::FriValidationError>();
330        implements_auto_traits::<error::ProvingError>();
331        implements_auto_traits::<error::VerificationError>();
332
333        // table things
334        implements_auto_traits::<challenges::Challenges>();
335        implements_auto_traits::<table::degree_lowering::DegreeLoweringMainColumn>();
336        implements_auto_traits::<table::degree_lowering::DegreeLoweringAuxColumn>();
337        implements_auto_traits::<table::degree_lowering::DegreeLoweringTable>();
338        implements_auto_traits::<table::master_table::MasterMainTable>();
339        implements_auto_traits::<table::master_table::MasterAuxTable>();
340        implements_auto_traits::<table::op_stack::OpStackTableEntry>();
341        implements_auto_traits::<table::ram::RamTableCall>();
342        implements_auto_traits::<table::u32::U32TableEntry>();
343
344        // other
345        implements_auto_traits::<aet::AlgebraicExecutionTrace>();
346        implements_auto_traits::<aet::TableHeight>();
347        implements_auto_traits::<arithmetic_domain::ArithmeticDomain>();
348        implements_auto_traits::<execution_trace_profiler::ExecutionTraceProfile>();
349        implements_auto_traits::<execution_trace_profiler::ProfileLine>();
350        implements_auto_traits::<execution_trace_profiler::VMTableHeights>();
351        implements_auto_traits::<fri::Fri>();
352        implements_auto_traits::<memory_layout::DynamicTasmConstraintEvaluationMemoryLayout>();
353        implements_auto_traits::<memory_layout::MemoryRegion>();
354        implements_auto_traits::<memory_layout::StaticTasmConstraintEvaluationMemoryLayout>();
355        implements_auto_traits::<profiler::VMPerformanceProfile>();
356        implements_auto_traits::<proof_item::FriResponse>();
357        implements_auto_traits::<proof_item::ProofItem>();
358        implements_auto_traits::<proof_stream::ProofStream>();
359        implements_auto_traits::<TypeHint>();
360        implements_auto_traits::<vm::CoProcessorCall>();
361    }
362
363    #[proptest]
364    fn prove_verify_knowledge_of_hash_preimage(
365        #[strategy(arb())] hash_preimage: Digest,
366        #[strategy(arb())] some_tie_to_an_outer_context: Digest,
367    ) {
368        let hash_digest = Tip5::hash_pair(hash_preimage, Digest::default()).values();
369
370        let program = triton_program! {
371            divine 5
372            hash
373            push {hash_digest[4]}
374            push {hash_digest[3]}
375            push {hash_digest[2]}
376            push {hash_digest[1]}
377            push {hash_digest[0]}
378            assert_vector
379            read_io 5
380            halt
381        };
382
383        let public_input = PublicInput::from(some_tie_to_an_outer_context.reversed().values());
384        let non_determinism = NonDeterminism::new(hash_preimage.reversed().values());
385        let maybe_proof = prove_program(program.clone(), public_input.clone(), non_determinism);
386        let (stark, claim, proof) =
387            maybe_proof.map_err(|err| TestCaseError::Fail(err.to_string().into()))?;
388        prop_assert_eq!(Stark::default(), stark);
389
390        let verdict = verify(stark, &claim, &proof);
391        prop_assert!(verdict);
392
393        prop_assert!(claim.output.is_empty());
394        let expected_program_digest = program.hash();
395        prop_assert_eq!(expected_program_digest, claim.program_digest);
396        prop_assert_eq!(public_input.individual_tokens, claim.input);
397    }
398
399    #[test]
400    fn lib_use_initial_ram() {
401        let program = triton_program!(
402            push 51 read_mem 1 pop 1
403            push 42 read_mem 1 pop 1
404            mul
405            write_io 1 halt
406        );
407
408        let public_input = PublicInput::default();
409        let initial_ram = [(42, 17), (51, 13)].map(|(address, v)| (bfe!(address), bfe!(v)));
410        let non_determinism = NonDeterminism::default().with_ram(initial_ram);
411        let (stark, claim, proof) = prove_program(program, public_input, non_determinism).unwrap();
412        assert!(13 * 17 == claim.output[0].value());
413
414        let verdict = verify(stark, &claim, &proof);
415        assert!(verdict);
416    }
417
418    #[test]
419    fn lib_prove_verify() {
420        let program = triton_program!(push 1 assert halt);
421        let claim = Claim::about_program(&program);
422
423        let stark = Stark::default();
424        let proof = prove(stark, &claim, program, [].into()).unwrap();
425        let verdict = verify(stark, &claim, &proof);
426        assert!(verdict);
427    }
428
429    #[test]
430    fn prove_then_verify_concurrently() {
431        let program = crate::example_programs::FIBONACCI_SEQUENCE.clone();
432        let input = PublicInput::from(bfe_array![100]);
433
434        let (stark, claim, proof) =
435            prove_program(program, input, NonDeterminism::default()).unwrap();
436
437        let verify = || assert!(stark.verify(&claim, &proof).is_ok());
438        rayon::join(verify, verify);
439    }
440
441    #[test]
442    fn lib_prove_with_incorrect_program_digest_gives_appropriate_error() {
443        let program = triton_program!(push 1 assert halt);
444        let other_program = triton_program!(push 2 assert halt);
445        let claim = Claim::about_program(&other_program);
446
447        let stark = Stark::default();
448        let_assert!(Err(err) = prove(stark, &claim, program, [].into()));
449        assert!(let ProvingError::ProgramDigestMismatch = err);
450    }
451
452    #[test]
453    fn lib_prove_with_incorrect_public_output_gives_appropriate_error() {
454        let program = triton_program! { read_io 1 push 2 mul write_io 1 halt };
455        let claim = Claim::about_program(&program)
456            .with_input(bfe_vec![2])
457            .with_output(bfe_vec![5]);
458
459        let stark = Stark::default();
460        let_assert!(Err(err) = prove(stark, &claim, program, [].into()));
461        assert!(let ProvingError::PublicOutputMismatch = err);
462    }
463
464    #[test]
465    fn nested_triton_asm_interpolation() {
466        let double_write = triton_asm![write_io 1; 2];
467        let quadruple_write = triton_asm!({&double_write} write_io 2);
468        let snippet_0 = triton_asm!(push 7 nop call my_label);
469        let snippet_1 = triton_asm!(pop 2 halt my_label: push 8 push 9 {&quadruple_write});
470        let source_code = triton_asm!(push 6 {&snippet_0} {&snippet_1} halt);
471
472        let program = triton_program!({ &source_code });
473        let public_output = VM::run(program, [].into(), [].into()).unwrap();
474
475        let expected_output = bfe_vec![9, 8, 7, 6];
476        assert_eq!(expected_output, public_output);
477    }
478
479    #[test]
480    fn triton_asm_interpolation_of_many_pops() {
481        let push_25 = triton_asm![push 0; 25];
482        let pop_25 = triton_asm![pop 5; 5];
483        let program = triton_program! { push 1 { &push_25 } { &pop_25 } assert halt };
484        VM::run(program, [].into(), [].into()).unwrap();
485    }
486
487    #[test]
488    #[should_panic(expected = "IndexOutOfBounds(0)")]
489    fn parsing_pop_with_illegal_argument_fails() {
490        triton_instr!(pop 0);
491    }
492
493    #[test]
494    fn triton_asm_macro_can_parse_type_hints() {
495        let instructions = triton_asm!(
496            hint name_0: Type0  = stack[0..8]
497            hint name_1         = stack[1..9]
498            hint name_2: Type2  = stack[2]
499            hint name_3         = stack[3]
500        );
501
502        assert!(4 == instructions.len());
503        let_assert!(LabelledInstruction::TypeHint(type_hint_0) = instructions[0].clone());
504        let_assert!(LabelledInstruction::TypeHint(type_hint_1) = instructions[1].clone());
505        let_assert!(LabelledInstruction::TypeHint(type_hint_2) = instructions[2].clone());
506        let_assert!(LabelledInstruction::TypeHint(type_hint_3) = instructions[3].clone());
507
508        let expected_type_hint_0 = TypeHint {
509            starting_index: 0,
510            length: 8,
511            type_name: Some("Type0".to_string()),
512            variable_name: "name_0".to_string(),
513        };
514        let expected_type_hint_1 = TypeHint {
515            starting_index: 1,
516            length: 8,
517            type_name: None,
518            variable_name: "name_1".to_string(),
519        };
520        let expected_type_hint_2 = TypeHint {
521            starting_index: 2,
522            length: 1,
523            type_name: Some("Type2".to_string()),
524            variable_name: "name_2".to_string(),
525        };
526        let expected_type_hint_3 = TypeHint {
527            starting_index: 3,
528            length: 1,
529            type_name: None,
530            variable_name: "name_3".to_string(),
531        };
532
533        assert!(expected_type_hint_0 == type_hint_0);
534        assert!(expected_type_hint_1 == type_hint_1);
535        assert!(expected_type_hint_2 == type_hint_2);
536        assert!(expected_type_hint_3 == type_hint_3);
537    }
538
539    #[test]
540    fn triton_program_macro_can_parse_type_hints() {
541        let program = triton_program! {
542            push 3 hint loop_counter = stack[0]
543            call my_loop
544            pop 1
545            halt
546
547            my_loop:
548                dup 0 push 0 eq
549                hint return_condition: bool = stack[0]
550                skiz return
551                divine 3
552                swap 3
553                hint magic_number: XFE = stack[1..4]
554                hint fizzled_magic = stack[5..8]
555                recurse
556        };
557
558        let expected_type_hint_address_02 = TypeHint {
559            starting_index: 0,
560            length: 1,
561            type_name: None,
562            variable_name: "loop_counter".to_string(),
563        };
564        let expected_type_hint_address_12 = TypeHint {
565            starting_index: 0,
566            length: 1,
567            type_name: Some("bool".to_string()),
568            variable_name: "return_condition".to_string(),
569        };
570        let expected_type_hint_address_18_0 = TypeHint {
571            starting_index: 1,
572            length: 3,
573            type_name: Some("XFE".to_string()),
574            variable_name: "magic_number".to_string(),
575        };
576        let expected_type_hint_address_18_1 = TypeHint {
577            starting_index: 5,
578            length: 3,
579            type_name: None,
580            variable_name: "fizzled_magic".to_string(),
581        };
582
583        assert!(vec![expected_type_hint_address_02] == program.type_hints_at(2));
584
585        assert!(vec![expected_type_hint_address_12] == program.type_hints_at(12));
586
587        let expected_type_hints_address_18 = vec![
588            expected_type_hint_address_18_0,
589            expected_type_hint_address_18_1,
590        ];
591        assert!(expected_type_hints_address_18 == program.type_hints_at(18));
592    }
593}