apollo_starknet_os_program,starknet_os: verify the processed proof in the aggregator

crates/apollo_starknet_os_program/src/cairo/starkware/starknet/core/aggregator/main.cairo

@@ -4,6 +4,9 @@ from starkware.cairo.common.alloc import alloc
 from starkware.cairo.common.bool import FALSE
 from starkware.cairo.common.cairo_builtins import EcOpBuiltin, HashBuiltin, PoseidonBuiltin
 from starkware.starknet.core.aggregator.combine_blocks import combine_blocks
+from starkware.starknet.core.aggregator.verify_processed_proof import (
+    verify_aggregated_processed_proof,
+)
 from starkware.starknet.core.os.os_config.os_config import (
     StarknetOsConfig,
     get_public_keys_hash,
@@ -53,6 +56,9 @@ func main{
         full_output=full_output,
     );
 
+    // Verify the processed proof of the aggregated blocks' transaction with proof facts, if any.
+    verify_aggregated_processed_proof(header=combined_output.header);
+
     // Output the bootloader output of the inner OsOutput instances.
     // This represents the "input" of the aggregator, whose correctness is later verified
     // by the bootloader by running the Cairo verifier.

crates/apollo_starknet_os_program/src/cairo/starkware/starknet/core/aggregator/verify_processed_proof.cairo

@@ -11,6 +11,7 @@ from starkware.cairo.common.cairo_builtins import (
     PoseidonBuiltin,
     SignatureBuiltin,
 )
+from starkware.starknet.core.os.output import OsOutputHeader
 from starkware.starknet.core.os.proof_fact_fold import (
     BLAKE2S_DIGEST_N_WORDS,
     compute_verification_digest,
@@ -27,6 +28,26 @@ const CIRCUIT_VERIFIER_PROGRAM_HASH = (
 // The output of a simple bootloader task: its size and program hash and verifier output digest.
 const VERIFIER_TASK_OUTPUT_SIZE = 2 + BLAKE2S_DIGEST_N_WORDS;
 
+// Verifies the processed proof of the aggregated blocks' transaction with proof facts, if they have
+// one, against the output digest in their combined header.
+func verify_aggregated_processed_proof{
+    pedersen_ptr: HashBuiltin*,
+    range_check_ptr,
+    ec_op_ptr: EcOpBuiltin*,
+    poseidon_ptr: PoseidonBuiltin*,
+}(header: OsOutputHeader*) {
+    if (header.n_proof_facts_transactions == 0) {
+        return ();
+    }
+    %{ EnterCircuitVerifierTaskScope %}
+    verify_processed_proof(
+        processed_proof_output_low=header.processed_proof_output_low,
+        processed_proof_output_high=header.processed_proof_output_high,
+    );
+    %{ vm_exit_scope() %}
+    return ();
+}
+
 // Runs the circuit verifier on a processed proof as a simple bootloader task.
 func verify_processed_proof{
     pedersen_ptr: HashBuiltin*,

crates/apollo_starknet_os_program/src/program_hash.json

@@ -1,6 +1,6 @@
 {
   "os": "0x5dfdb7dab2180055f967f6f94c3431f0add9dbed61c509a867027738f792305",
   "virtual_os": "0x6f51d5c22ea301edd0544e40c92e01ac04c63db0772d9a9c349f36009d22bfa",
-  "aggregator": "0x7a7382c43d4dabb0c454bb8679018cc6f784e70c63b80031d771159c9fc18e0",
-  "aggregator_with_prefix": "0x6fd55f06de3b556bbd36e6d25b5af222dc56d8d7e634f9b780f3affd84fea78"
+  "aggregator": "0x6fb86d1e2f0d5995e125e9babb9b46ad342e5066e49f98d5adfeb0a430a486a",
+  "aggregator_with_prefix": "0x76b561abc01b17595fab39c6460e8d610e88d5a388b7c26a46e284a09a74bc8"
 }

crates/starknet_os/resources/hint_coverage/test_aggregator_verifies_the_processed_proof.json

@@ -0,0 +1,56 @@
+[
+  {
+    "StatelessHint": "SelectedBuiltins"
+  },
+  {
+    "StatelessHint": "SelectBuiltin"
+  },
+  {
+    "StatelessHint": "SetStateUpdatesStart"
+  },
+  {
+    "StatelessHint": "AllocateSegmentsForMessages"
+  },
+  {
+    "CommonHint": "SetProofFactTopology"
+  },
+  {
+    "CommonHint": "LoadStoragePtrAndPrevState"
+  },
+  {
+    "CommonHint": "UpdateClassesPtr"
+  },
+  {
+    "CommonHint": "GuessClassesPtr"
+  },
+  {
+    "CommonHint": "UpdateContractAddrToStoragePtr"
+  },
+  {
+    "CommonHint": "SetStateUpdatePointersToNone"
+  },
+  {
+    "CommonHint": "GetPublicKeys"
+  },
+  {
+    "AggregatorHint": "DisableDaPageCreation"
+  },
+  {
+    "AggregatorHint": "EnterCircuitVerifierTaskScope"
+  },
+  {
+    "AggregatorHint": "GetOsOuputForInnerBlocks"
+  },
+  {
+    "AggregatorHint": "GetAggregatorOutput"
+  },
+  {
+    "AggregatorHint": "WriteDaSegment"
+  },
+  {
+    "AggregatorHint": "GetUseKzgDaAndFullOutputFromInput"
+  },
+  {
+    "AggregatorHint": "GetChainIdAndFeeTokenAddressFromInput"
+  }
+]

crates/starknet_os/src/hint_processor/aggregator_hint_processor.rs

@@ -52,6 +52,9 @@ pub struct AggregatorInput {
     pub fee_token_address: Felt,
     pub chain_id: Felt,
     pub public_keys: Option<Vec<Felt>>,
+    // The circuit verifier task on the processed proof of the aggregated blocks' transaction with
+    // proof facts. Required only if there is such a transaction.
+    pub circuit_verifier_task: Option<CircuitVerifierTaskInput>,
 }
 
 impl AggregatorInput {

crates/starknet_os/src/hints/enum_definition.rs

@@ -12,6 +12,7 @@ use crate::hints::error::{OsHintError, OsHintExtensionResult, OsHintResult};
 use crate::hints::hint_implementation::aggregator::implementation::{
     allocate_segments_for_messages,
     disable_da_page_creation,
+    enter_circuit_verifier_task_scope,
     get_aggregator_output,
     get_chain_id_and_fee_token_address_from_input,
     get_os_output_for_inner_blocks,
@@ -568,6 +569,7 @@ define_hint_enum!(
     AggregatorHint,
     AggregatorHintProcessor<'_>,
     (DisableDaPageCreation, disable_da_page_creation),
+    (EnterCircuitVerifierTaskScope, enter_circuit_verifier_task_scope),
     (GetOsOuputForInnerBlocks, get_os_output_for_inner_blocks),
     (GetAggregatorOutput, get_aggregator_output),
     (WriteDaSegment, write_da_segment),

crates/starknet_os/src/hints/enum_definition_test.rs

@@ -63,11 +63,22 @@ impl TryFrom<DeprecatedSyscallSelector> for DeprecatedSyscallHint {
     }
 }
 
+/// The module of the copied simple bootloader code, whose hints the bootloader hint processor of
+/// `cairo_program_runner_lib` runs, rather than the OS or aggregator hint processor.
+const SIMPLE_BOOTLOADER_MODULE: &str = "starkware.cairo.bootloaders.simple_bootloader.";
+
+/// The hints of the program, except the simple bootloader code's.
 fn program_hints(program: &Program) -> HashSet<String> {
     program
         .shared_program_data
         .hints_collection
         .iter_hints()
+        .filter(|hint| {
+            !hint
+                .accessible_scopes
+                .last()
+                .is_some_and(|scope| scope.starts_with(SIMPLE_BOOTLOADER_MODULE))
+        })
         .map(|hint| hint.code.clone())
         .collect()
 }

crates/starknet_os/src/hints/error.rs

@@ -1,6 +1,7 @@
 use blockifier::execution::deprecated_syscalls::deprecated_syscall_executor::DeprecatedSyscallExecutorBaseError;
 use blockifier::execution::deprecated_syscalls::hint_processor::DeprecatedSyscallExecutionError;
 use blockifier::state::errors::StateError;
+use cairo_program_runner_lib::tasks::BootloaderTaskError;
 use cairo_vm::hint_processor::hint_processor_definition::HintExtension;
 use cairo_vm::types::errors::math_errors::MathError;
 use cairo_vm::types::errors::program_errors::ProgramError;
@@ -46,6 +47,8 @@ pub enum OsHintError {
     BlockNumberTooSmall { stored_block_hash_buffer: Felt },
     #[error("{id:?} value {felt} is not a boolean.")]
     BooleanIdExpected { id: Ids, felt: Felt },
+    #[error("Failed to build the circuit verifier task: {0}")]
+    CircuitVerifierTask(#[from] BootloaderTaskError),
     #[error("Failed to convert {variant:?} felt value {felt:?} to type {ty}: {reason:?}.")]
     ConstConversion { variant: Const, felt: Felt, ty: String, reason: String },
     #[error(transparent)]
@@ -95,6 +98,11 @@ pub enum OsHintError {
     Memory(#[from] MemoryError),
     #[error("No bytecode segment structure for class hash: {0:?}.")]
     MissingBytecodeSegmentStructure(CompiledClassHash),
+    #[error(
+        "The aggregated blocks contain a transaction with proof facts, but the aggregator input \
+         has no circuit verifier task."
+    )]
+    MissingCircuitVerifierTask,
     #[error("Hint {hint:?} has no nondet offset.")]
     MissingOffsetForHint { hint: AllHints },
     #[error("No component hashes for class hash {0:?}.")]

crates/starknet_os/src/hints/hint_implementation/aggregator/implementation.rs

@@ -1,3 +1,7 @@
+use std::any::Any;
+use std::collections::HashMap;
+
+use cairo_program_runner_lib::SIMPLE_BOOTLOADER_INPUT;
 use starknet_types_core::felt::Felt;
 
 use crate::hint_processor::aggregator_hint_processor::{AggregatorHintProcessor, DataAvailability};
@@ -29,6 +33,27 @@ pub(crate) fn disable_da_page_creation(
     Ok(())
 }
 
+/// Enters a scope holding the simple bootloader input that runs the circuit verifier on the
+/// processed proof of the aggregated blocks' transaction with proof facts.
+pub(crate) fn enter_circuit_verifier_task_scope(
+    hint_processor: &mut AggregatorHintProcessor<'_>,
+    ctx: HintContext<'_>,
+) -> OsHintResult {
+    let simple_bootloader_input: Box<dyn Any> = Box::new(
+        hint_processor
+            .input
+            .circuit_verifier_task
+            .as_ref()
+            .ok_or(OsHintError::MissingCircuitVerifierTask)?
+            .simple_bootloader_input()?,
+    );
+    ctx.exec_scopes.enter_scope(HashMap::from([(
+        SIMPLE_BOOTLOADER_INPUT.to_string(),
+        simple_bootloader_input,
+    )]));
+    Ok(())
+}
+
 pub(crate) fn get_os_output_for_inner_blocks(
     hint_processor: &mut AggregatorHintProcessor<'_>,
     mut ctx: HintContext<'_>,