Proof mode, second draft

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,30 +189,106 @@ fn run(args: impl Iterator<Item = String>) -> Result<Vec<MaybeRelocatable>, Erro
 
     let main_func = find_function(&sierra_program, "::main")?;
 
-    let initial_gas = 9999999999999_usize;
+    // println!("Main func: {:?}", main_func.entry_point);
 
     // Entry code and footer are part of the whole instructions that are
     // ran by the VM.
-    let (entry_code, builtins) = create_entry_code(
+
+    let initial_gas = 9999999999999_usize;
+
+    // This call should be removed
+    let (_, builtins) = create_entry_code(
         &sierra_program_registry,
         &casm_program,
         &type_sizes,
         main_func,
         initial_gas,
     )?;
-    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, 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)?;
 
+    println!("Compiling with proof mode and running ...");
+
+    println!("Builtins used: {:?}", 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 += 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
+        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 proof_mode_header = ctx.instructions;
+
+    let program_instructions = casm_program.instructions.iter();
+
+    // This footer is used by lib funcs
+    let libfunc_footer = create_code_footer();
+
+    // This is the program we are actually proving
+    // With embedded proof mode and the libfunc footer
     let instructions = chain!(
-        entry_code.iter(),
-        casm_program.instructions.iter(),
-        footer.iter()
+        proof_mode_header.iter(),
+        program_instructions,
+        libfunc_footer.iter()
     );
 
     let (processor_hints, program_hints) = build_hints_vec(instructions.clone());
+
     let mut hint_processor = Cairo1HintProcessor::new(&processor_hints, RunResources::default());
 
     let data: Vec<MaybeRelocatable> = instructions
@@ -222,10 +299,19 @@ fn run(args: impl Iterator<Item = String>) -> Result<Vec<MaybeRelocatable>, Erro
 
     let data_len = data.len();
 
-    let program = Program::new(
+    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,
-        Some(0),
+        starting_pc,
+        final_pc,
         program_hints,
         ReferenceManager {
             references: Vec::new(),
@@ -235,14 +321,18 @@ fn run(args: impl Iterator<Item = String>) -> Result<Vec<MaybeRelocatable>, Erro
         None,
     )?;
 
-    let mut runner = CairoRunner::new(&program, &args.layout, false)?;
+    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)?;
 
+    // Run it until the infinite loop
     runner.run_until_pc(end, &mut vm, &mut hint_processor)?;
-    runner.end_run(true, false, &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)?;
 
     // Fetch return type data
     let return_type_id = main_func