From 4be23ec8eef0b3eafe86cad63907e0dbb019fb32 Mon Sep 17 00:00:00 2001 From: MauroFab Date: Sun, 19 Nov 2023 11:20:41 -0300 Subject: [PATCH 1/6] proof mode for add u8 --- cairo1-run/src/main.rs | 76 +++++++++++++++++++++++++++++++++++++----- 1 file changed, 68 insertions(+), 8 deletions(-) diff --git a/cairo1-run/src/main.rs b/cairo1-run/src/main.rs index ce711ca554..5af8f65052 100644 --- a/cairo1-run/src/main.rs +++ b/cairo1-run/src/main.rs @@ -40,6 +40,7 @@ use cairo_vm::serde::deserialize_program::BuiltinName; use cairo_vm::serde::deserialize_program::{ApTracking, FlowTrackingData, HintParams}; use cairo_vm::types::errors::program_errors::ProgramError; use cairo_vm::types::relocatable::Relocatable; +use cairo_vm::vm::decoding::decoder::decode_instruction; use cairo_vm::vm::errors::cairo_run_errors::CairoRunError; use cairo_vm::vm::errors::memory_errors::MemoryError; use cairo_vm::vm::errors::runner_errors::RunnerError; @@ -188,11 +189,16 @@ fn run(args: impl Iterator) -> Result, Erro let main_func = find_function(&sierra_program, "::main")?; + println!("Main func: {:?}", main_func.entry_point); + let initial_gas = 9999999999999_usize; // Entry code and footer are part of the whole instructions that are // ran by the VM. - let (entry_code, builtins) = create_entry_code( + + // We are replacing the entry with a proof mode like code + + let (_, builtins) = create_entry_code( &sierra_program_registry, &casm_program, &type_sizes, @@ -201,17 +207,45 @@ fn run(args: impl Iterator) -> Result, Erro )?; let footer = create_code_footer(); - let check_gas_usage = true; + // We don't want additional data regarding gas for offchain programs + let check_gas_usage = false; + + // ap_change_info maybe useful ? let metadata = calc_metadata(&sierra_program, Default::default(), false)?; let casm_program = compile(&sierra_program, &metadata, check_gas_usage)?; + + // Error: VirtualMachine(DiffAssertValues((RelocatableValue(Relocatable { segment_index: 4, offset: 0 }), RelocatableValue(Relocatable { segment_index: 4, offset: 8 })))) + + // Error: VirtualMachine(DiffAssertValues((RelocatableValue(Relocatable { segment_index: 4, offset: 0 }), RelocatableValue(Relocatable { segment_index: 4, offset: 1 })))) + + // + let mut ctx = casm! {}; + casm_extend! {ctx, + ap += 1; + call rel 4; + jmp rel 0; + }; + + // ap += main.Args.SIZE + main.ImplicitArgs.SIZE; + + // println!("Main {:?}", main_func); + + + let program_instructions = casm_program.instructions.iter(); + + let proof_mode_header = ctx.instructions; + let instructions = chain!( - entry_code.iter(), - casm_program.instructions.iter(), - footer.iter() + proof_mode_header.iter(), + program_instructions ); + // println!("Instructions: {:?}", instructions); + // println!("Builtins: {:?}", builtins); + let (processor_hints, program_hints) = build_hints_vec(instructions.clone()); + let mut hint_processor = Cairo1HintProcessor::new(&processor_hints, RunResources::default()); let data: Vec = instructions @@ -222,10 +256,11 @@ fn run(args: impl Iterator) -> Result, Erro let data_len = data.len(); - let program = Program::new( + let program = Program::new_for_proof( builtins, data, - Some(0), + 0, + 4, program_hints, ReferenceManager { references: Vec::new(), @@ -235,14 +270,39 @@ fn run(args: impl Iterator) -> Result, Erro None, )?; - let mut runner = CairoRunner::new(&program, &args.layout, false)?; + /* let program = Program::new( + builtins, + data, + Some(0), + program_hints, + ReferenceManager { + references: Vec::new(), + }, + HashMap::new(), + vec![], + None, + )?; */ + + let mut runner = CairoRunner::new(&program, &args.layout, true)?; + let mut vm = VirtualMachine::new(args.trace_file.is_some()); let end = runner.initialize(&mut vm)?; additional_initialization(&mut vm, data_len)?; runner.run_until_pc(end, &mut vm, &mut hint_processor)?; + /* + runner + .run_for_steps(50, &mut vm, &mut hint_processor) + .unwrap(); runner.end_run(true, false, &mut vm, &mut hint_processor)?; + */ + /* + output: true, + pedersen: Some(PedersenInstanceDef::default()), + range_check: Some(RangeCheckInstanceDef::default()), + ecdsa: Some(EcdsaInstanceDef::default()), + */ // Fetch return type data let return_type_id = main_func From ff104eb3df73c18ff4783fe3c029f0cafebc737b Mon Sep 17 00:00:00 2001 From: MauroFab Date: Sun, 19 Nov 2023 11:45:10 -0300 Subject: [PATCH 2/6] proof mode 2 --- cairo1-run/src/main.rs | 15 ++------------- 1 file changed, 2 insertions(+), 13 deletions(-) diff --git a/cairo1-run/src/main.rs b/cairo1-run/src/main.rs index 5af8f65052..1c06663ae3 100644 --- a/cairo1-run/src/main.rs +++ b/cairo1-run/src/main.rs @@ -270,19 +270,6 @@ fn run(args: impl Iterator) -> Result, Erro None, )?; - /* let program = Program::new( - builtins, - data, - Some(0), - program_hints, - ReferenceManager { - references: Vec::new(), - }, - HashMap::new(), - vec![], - None, - )?; */ - let mut runner = CairoRunner::new(&program, &args.layout, true)?; let mut vm = VirtualMachine::new(args.trace_file.is_some()); @@ -291,6 +278,8 @@ fn run(args: impl Iterator) -> Result, Erro additional_initialization(&mut vm, data_len)?; runner.run_until_pc(end, &mut vm, &mut hint_processor)?; + + runner.run_until_next_power_of_2(&mut vm, &mut hint_processor)?; /* runner .run_for_steps(50, &mut vm, &mut hint_processor) From cfb5e0a3df587d96091d145f11635653c337dc74 Mon Sep 17 00:00:00 2001 From: MauroFab Date: Sun, 19 Nov 2023 16:06:36 -0300 Subject: [PATCH 3/6] Improved code readability, upper bounded ap --- cairo1-run/src/main.rs | 46 +++++++++++------------------------------- 1 file changed, 12 insertions(+), 34 deletions(-) diff --git a/cairo1-run/src/main.rs b/cairo1-run/src/main.rs index 1c06663ae3..39d7451be7 100644 --- a/cairo1-run/src/main.rs +++ b/cairo1-run/src/main.rs @@ -196,7 +196,7 @@ fn run(args: impl Iterator) -> Result, Erro // Entry code and footer are part of the whole instructions that are // ran by the VM. - // We are replacing the entry with a proof mode like code + // We are replacing the entry with a proof mode like code, so this is unused let (_, builtins) = create_entry_code( &sierra_program_registry, @@ -205,47 +205,35 @@ fn run(args: impl Iterator) -> Result, Erro main_func, initial_gas, )?; - let footer = create_code_footer(); - // We don't want additional data regarding gas for offchain programs + // We don't want additional data regarding gas for offchain programs let check_gas_usage = false; - // ap_change_info maybe useful ? + // ap_change_info maybe useful, we can also count builtins from sierra let metadata = calc_metadata(&sierra_program, Default::default(), false)?; let casm_program = compile(&sierra_program, &metadata, check_gas_usage)?; - - // Error: VirtualMachine(DiffAssertValues((RelocatableValue(Relocatable { segment_index: 4, offset: 0 }), RelocatableValue(Relocatable { segment_index: 4, offset: 8 })))) - - // Error: VirtualMachine(DiffAssertValues((RelocatableValue(Relocatable { segment_index: 4, offset: 0 }), RelocatableValue(Relocatable { segment_index: 4, offset: 1 })))) - - // let mut ctx = casm! {}; casm_extend! {ctx, - ap += 1; + // ap += #builtin pointers + main args + // Setting it to a high number should work for all cases, but it's allocating more memory than needing + // CairoZero: ap += main.Args.SIZE + main.ImplicitArgs.SIZE; + ap += 16; call rel 4; jmp rel 0; }; - // ap += main.Args.SIZE + main.ImplicitArgs.SIZE; - - // println!("Main {:?}", main_func); - - let program_instructions = casm_program.instructions.iter(); let proof_mode_header = ctx.instructions; - let instructions = chain!( - proof_mode_header.iter(), - program_instructions - ); + let instructions = chain!(proof_mode_header.iter(), program_instructions); // println!("Instructions: {:?}", instructions); // println!("Builtins: {:?}", builtins); - + let (processor_hints, program_hints) = build_hints_vec(instructions.clone()); - + let mut hint_processor = Cairo1HintProcessor::new(&processor_hints, RunResources::default()); let data: Vec = instructions @@ -277,21 +265,11 @@ fn run(args: impl Iterator) -> Result, Erro additional_initialization(&mut vm, data_len)?; + // Run it until the infinite loop runner.run_until_pc(end, &mut vm, &mut hint_processor)?; + // Then pad it to the power of 2 runner.run_until_next_power_of_2(&mut vm, &mut hint_processor)?; - /* - runner - .run_for_steps(50, &mut vm, &mut hint_processor) - .unwrap(); - runner.end_run(true, false, &mut vm, &mut hint_processor)?; - */ - /* - output: true, - pedersen: Some(PedersenInstanceDef::default()), - range_check: Some(RangeCheckInstanceDef::default()), - ecdsa: Some(EcdsaInstanceDef::default()), - */ // Fetch return type data let return_type_id = main_func From 95c32a7b6643db89f8acc9e98bc24be98eb8926d Mon Sep 17 00:00:00 2001 From: MauroFab Date: Sun, 19 Nov 2023 16:12:01 -0300 Subject: [PATCH 4/6] Dynamic builtins --- cairo1-run/src/main.rs | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/cairo1-run/src/main.rs b/cairo1-run/src/main.rs index 39d7451be7..f12d87aede 100644 --- a/cairo1-run/src/main.rs +++ b/cairo1-run/src/main.rs @@ -213,12 +213,13 @@ fn run(args: impl Iterator) -> Result, Erro let metadata = calc_metadata(&sierra_program, Default::default(), false)?; let casm_program = compile(&sierra_program, &metadata, check_gas_usage)?; + let n = builtins.len(); + let mut ctx = casm! {}; casm_extend! {ctx, // ap += #builtin pointers + main args - // Setting it to a high number should work for all cases, but it's allocating more memory than needing // CairoZero: ap += main.Args.SIZE + main.ImplicitArgs.SIZE; - ap += 16; + ap += n; call rel 4; jmp rel 0; }; From ee577ff16ef3b472d997f73af699c6c0d012a390 Mon Sep 17 00:00:00 2001 From: MauroFab Date: Wed, 22 Nov 2023 14:26:42 -0300 Subject: [PATCH 5/6] Generalized the code to work with and without gas builtins --- cairo1-run/src/main.rs | 85 ++++++++++++++++++++++++++++++++++++------ 1 file changed, 74 insertions(+), 11 deletions(-) diff --git a/cairo1-run/src/main.rs b/cairo1-run/src/main.rs index f12d87aede..2a800ca2e8 100644 --- a/cairo1-run/src/main.rs +++ b/cairo1-run/src/main.rs @@ -178,6 +178,8 @@ fn run(args: impl Iterator) -> Result, Erro .map_err(|err| Error::SierraCompilation(err.to_string()))?) .clone(); + println!("Sierra: {}", sierra_program); + let metadata_config = Some(Default::default()); let gas_usage_check = metadata_config.is_some(); let metadata = create_metadata(&sierra_program, metadata_config)?; @@ -191,13 +193,13 @@ fn run(args: impl Iterator) -> Result, Erro println!("Main func: {:?}", main_func.entry_point); - let initial_gas = 9999999999999_usize; - // Entry code and footer are part of the whole instructions that are // ran by the VM. // We are replacing the entry with a proof mode like code, so this is unused + let initial_gas = 9999999999999_usize; + // This call should be removed let (_, builtins) = create_entry_code( &sierra_program_registry, &casm_program, @@ -210,28 +212,81 @@ fn run(args: impl Iterator) -> Result, Erro let check_gas_usage = false; // ap_change_info maybe useful, we can also count builtins from sierra + println!("Ap change info: {:?}", metadata.ap_change_info); let metadata = calc_metadata(&sierra_program, Default::default(), false)?; let casm_program = compile(&sierra_program, &metadata, check_gas_usage)?; - let n = builtins.len(); + println!("Builtins: {:?}", builtins); + + println!(" Main signs: {:?}", main_func.signature.param_types); + + // Each params needs the AP to be updated for them to work + let amount_of_main_args = main_func.signature.param_types.len(); + + // Additionally, some params need extra logic + // We look for a gas builtin, since it needs us to set the implicit param in the header of the initial amount of gas. + // Adittionally : + // - SegmentArena additional segments should be handled here too. + // - Array arguments should be tested in the future too + // - Syscalls don't apply to programs + // - Other params shouldn't need an explicit handling, they just need the ap to be handled + + let mut has_gas_builtin = false; + for ty in main_func.signature.param_types.iter() { + let info = get_info(&sierra_program_registry, ty) + .ok_or_else(|| Error::NoInfoForType(ty.clone()))?; + let generic_ty = &info.long_id.generic_id; + if generic_ty == &GasBuiltinType::ID { + has_gas_builtin = true; + } + } + + let mut ap_offset = amount_of_main_args; let mut ctx = casm! {}; + + // Gas builtin requires saving the max amount of gas in a header, and increasing the ap manually. So we will remove it from the base ap offset + if has_gas_builtin { + ap_offset -= 1; + } + + // Here we prepare the header + // AP needs to be updated. Each argument moves the ap by one casm_extend! {ctx, // ap += #builtin pointers + main args // CairoZero: ap += main.Args.SIZE + main.ImplicitArgs.SIZE; - ap += n; + ap += ap_offset; + }; + + if has_gas_builtin { + // If there's a gas builtin, we need to set the initial gas to a high number. It shouldn't be needed, but cairo sierra compiler will add the "gas builtin" for programs with explicit recursion + // ap needs to be increased at this moment, and not with the usual ap offset + println!("Appending gas builtin code"); + casm_extend! {ctx, + [ap + 0] = initial_gas, ap++; + } + } + + // Then goes the main proof mode code. Notice we expect main to be at the beggining of the casm code, that's why call rel is 4. + casm_extend! {ctx, call rel 4; jmp rel 0; }; - let program_instructions = casm_program.instructions.iter(); - let proof_mode_header = ctx.instructions; - let instructions = chain!(proof_mode_header.iter(), program_instructions); + let program_instructions = casm_program.instructions.iter(); + + // This footer is used by lib funcs + let libfunc_footer = create_code_footer(); - // println!("Instructions: {:?}", instructions); - // println!("Builtins: {:?}", builtins); + // This is the program we are actually proving + // With embedded proof mode and the libfunc footer + let instructions = chain!( + proof_mode_header.iter(), + program_instructions, + libfunc_footer.iter() + ); let (processor_hints, program_hints) = build_hints_vec(instructions.clone()); @@ -245,11 +300,19 @@ fn run(args: impl Iterator) -> Result, Erro let data_len = data.len(); + let starting_pc = 0; + let mut final_pc = 4; + + // Notice we added an additional instruction with the initial gas when gas builtin was activated, so the infinite loop has moved + if has_gas_builtin { + final_pc += 2; + } + let program = Program::new_for_proof( builtins, data, - 0, - 4, + starting_pc, + final_pc, program_hints, ReferenceManager { references: Vec::new(), From c4fe8828eb0027bc365911951020e67afa5755d7 Mon Sep 17 00:00:00 2001 From: MauroFab Date: Thu, 23 Nov 2023 15:41:53 -0300 Subject: [PATCH 6/6] Fix comments --- cairo1-run/src/main.rs | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) diff --git a/cairo1-run/src/main.rs b/cairo1-run/src/main.rs index 2a800ca2e8..d3c35ff474 100644 --- a/cairo1-run/src/main.rs +++ b/cairo1-run/src/main.rs @@ -178,8 +178,6 @@ fn run(args: impl Iterator) -> Result, Erro .map_err(|err| Error::SierraCompilation(err.to_string()))?) .clone(); - println!("Sierra: {}", sierra_program); - let metadata_config = Some(Default::default()); let gas_usage_check = metadata_config.is_some(); let metadata = create_metadata(&sierra_program, metadata_config)?; @@ -191,12 +189,11 @@ fn run(args: impl Iterator) -> Result, Erro let main_func = find_function(&sierra_program, "::main")?; - println!("Main func: {:?}", main_func.entry_point); + // println!("Main func: {:?}", main_func.entry_point); // Entry code and footer are part of the whole instructions that are // ran by the VM. - // We are replacing the entry with a proof mode like code, so this is unused let initial_gas = 9999999999999_usize; // This call should be removed @@ -212,13 +209,16 @@ fn run(args: impl Iterator) -> Result, Erro let check_gas_usage = false; // ap_change_info maybe useful, we can also count builtins from sierra - println!("Ap change info: {:?}", metadata.ap_change_info); let metadata = calc_metadata(&sierra_program, Default::default(), false)?; let casm_program = compile(&sierra_program, &metadata, check_gas_usage)?; - println!("Builtins: {:?}", builtins); + println!("Compiling with proof mode and running ..."); + + println!("Builtins used: {:?}", builtins); + + // println!(" Main signs: {:?}", main_func.signature.param_types); + - println!(" Main signs: {:?}", main_func.signature.param_types); // Each params needs the AP to be updated for them to work let amount_of_main_args = main_func.signature.param_types.len(); @@ -261,7 +261,6 @@ fn run(args: impl Iterator) -> Result, Erro if has_gas_builtin { // If there's a gas builtin, we need to set the initial gas to a high number. It shouldn't be needed, but cairo sierra compiler will add the "gas builtin" for programs with explicit recursion // ap needs to be increased at this moment, and not with the usual ap offset - println!("Appending gas builtin code"); casm_extend! {ctx, [ap + 0] = initial_gas, ap++; }