1#![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
191pub fn prove_program(
206 program: Program,
207 public_input: PublicInput,
208 non_determinism: NonDeterminism,
209) -> Result<(Stark, Claim, Proof), ProvingError> {
210 let claim = Claim::new(program.hash()).with_input(public_input.clone());
217
218 let (aet, public_output) = VM::trace_execution(program, public_input, non_determinism)?;
230
231 let claim = claim.with_output(public_output);
233
234 let stark = Stark::default();
236
237 let proof = stark.prove(&claim, &aet)?;
239
240 Ok((stark, claim, proof))
241}
242
243pub 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#[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 fn implements_auto_traits<T: Sized + Send + Sync + Unpin>() {}
301
302 #[test]
303 fn public_types_implement_usual_auto_traits() {
304 implements_auto_traits::<BFieldElement>();
306 implements_auto_traits::<Digest>();
307 implements_auto_traits::<Tip5>();
308 implements_auto_traits::<XFieldElement>();
309
310 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 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 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 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}