pub fn verify(
        &self,
        proof: &SP1CoreProofData,
        vk: &SP1VerifyingKey,
    ) -> Result<(), MachineVerificationError<CoreSC>> {
        // The proof should not be empty.
        if proof.0.is_empty() {
            return Err(MachineVerificationError::EmptyProof);
        }

        // First shard has a "CPU" constraint.
        //
        // Check that the first shard has a "CPU".
        // SAFETY: The proof is already checked to not be empty.
        let first_shard = proof.0.first().unwrap();
        if !first_shard.contains_cpu() {
            return Err(MachineVerificationError::MissingCpuInFirstShard);
        }

        // CPU log degree bound constraints.
        //
        // Check that the CPU log degree does not exceed `MAX_CPU_LOG_DEGREE`. This is to ensure
        // that the lookup argument's multiplicities do not overflow.
        for shard_proof in proof.0.iter() {
            if shard_proof.contains_cpu() {
                let log_degree_cpu = shard_proof.log_degree_cpu();
                if log_degree_cpu > MAX_CPU_LOG_DEGREE {
                    return Err(MachineVerificationError::CpuLogDegreeTooLarge(log_degree_cpu));
                }
            }
        }

        // Shard constraints.
        //
        // Initialization:
        // - Shard should start at one.
        //
        // Transition:
        // - Shard should increment by one for each shard.
        let mut current_shard = BabyBear::zero();
        for shard_proof in proof.0.iter() {
            let public_values: &PublicValues<Word<_>, _> =
                shard_proof.public_values.as_slice().borrow();
            current_shard += BabyBear::one();
            if public_values.shard != current_shard {
                return Err(MachineVerificationError::InvalidPublicValues(
                    "shard index should be the previous shard index + 1 and start at 1",
                ));
            }
        }

        // Execution shard constraints.
        //
        // Initialization:
        // - Execution shard should start at one.
        //
        // Transition:
        // - Execution shard should increment by one for each shard with "CPU".
        // - Execution shard should stay the same for non-CPU shards.
        // - For the other shards, execution shard does not matter.
        let mut current_execution_shard = BabyBear::zero();
        for shard_proof in proof.0.iter() {
            let public_values: &PublicValues<Word<_>, _> =
                shard_proof.public_values.as_slice().borrow();
            if shard_proof.contains_cpu() {
                current_execution_shard += BabyBear::one();
                if public_values.execution_shard != current_execution_shard {
                    return Err(MachineVerificationError::InvalidPublicValues(
                        "execution shard index should be the previous execution shard index + 1 if cpu exists and start at 1",
                    ));
                }
            }
        }

        // Program counter constraints.
        //
        // Initialization:
        // - `start_pc` should start as `vk.start_pc`.
        //
        // Transition:
        // - `next_pc` of the previous shard should equal `start_pc`.
        // - If it's not a shard with "CPU", then `start_pc` equals `next_pc`.
        // - If it's a shard with "CPU", then `start_pc` should never equal zero.
        //
        // Finalization:
        // - `next_pc` should equal zero.
        let mut prev_next_pc = BabyBear::zero();
        for (i, shard_proof) in proof.0.iter().enumerate() {
            let public_values: &PublicValues<Word<_>, _> =
                shard_proof.public_values.as_slice().borrow();
            if i == 0 && public_values.start_pc != vk.vk.pc_start {
                return Err(MachineVerificationError::InvalidPublicValues(
                    "start_pc != vk.start_pc: program counter should start at vk.start_pc",
                ));
            } else if i != 0 && public_values.start_pc != prev_next_pc {
                return Err(MachineVerificationError::InvalidPublicValues(
                    "start_pc != next_pc_prev: start_pc should equal next_pc_prev for all shards",
                ));
            } else if !shard_proof.contains_cpu() && public_values.start_pc != public_values.next_pc
            {
                return Err(MachineVerificationError::InvalidPublicValues(
                    "start_pc != next_pc: start_pc should equal next_pc for non-cpu shards",
                ));
            } else if shard_proof.contains_cpu() && public_values.start_pc == BabyBear::zero() {
                return Err(MachineVerificationError::InvalidPublicValues(
                    "start_pc == 0: execution should never start at halted state",
                ));
            } else if i == proof.0.len() - 1 && public_values.next_pc != BabyBear::zero() {
                return Err(MachineVerificationError::InvalidPublicValues(
                    "next_pc != 0: execution should have halted",
                ));
            }
            prev_next_pc = public_values.next_pc;
        }

        // Exit code constraints.
        //
        // - In every shard, the exit code should be zero.
        for shard_proof in proof.0.iter() {
            let public_values: &PublicValues<Word<_>, _> =
                shard_proof.public_values.as_slice().borrow();
            if public_values.exit_code != BabyBear::zero() {
                return Err(MachineVerificationError::InvalidPublicValues(
                    "exit_code != 0: exit code should be zero for all shards",
                ));
            }
        }

        // Memory initialization & finalization constraints.
        //
        // Initialization:
        // - `previous_init_addr_bits` should be zero.
        // - `previous_finalize_addr_bits` should be zero.
        //
        // Transition:
        // - For all shards, `previous_init_addr_bits` should equal `last_init_addr_bits` of the
        //   previous shard.
        // - For all shards, `previous_finalize_addr_bits` should equal `last_finalize_addr_bits` of
        //   the previous shard.
        // - For shards without "MemoryInit", `previous_init_addr_bits` should equal
        //   `last_init_addr_bits`.
        // - For shards without "MemoryFinalize", `previous_finalize_addr_bits` should equal
        //   `last_finalize_addr_bits`.
        let mut last_init_addr_bits_prev = [BabyBear::zero(); 32];
        let mut last_finalize_addr_bits_prev = [BabyBear::zero(); 32];
        for shard_proof in proof.0.iter() {
            let public_values: &PublicValues<Word<_>, _> =
                shard_proof.public_values.as_slice().borrow();
            if public_values.previous_init_addr_bits != last_init_addr_bits_prev {
                return Err(MachineVerificationError::InvalidPublicValues(
                    "previous_init_addr_bits != last_init_addr_bits_prev",
                ));
            } else if public_values.previous_finalize_addr_bits != last_finalize_addr_bits_prev {
                return Err(MachineVerificationError::InvalidPublicValues(
                    "last_init_addr_bits != last_finalize_addr_bits_prev",
                ));
            } else if !shard_proof.contains_global_memory_init() &&
                public_values.previous_init_addr_bits != public_values.last_init_addr_bits
            {
                return Err(MachineVerificationError::InvalidPublicValues(
                    "previous_init_addr_bits != last_init_addr_bits",
                ));
            } else if !shard_proof.contains_global_memory_finalize() &&
                public_values.previous_finalize_addr_bits !=
                    public_values.last_finalize_addr_bits
            {
                return Err(MachineVerificationError::InvalidPublicValues(
                    "previous_finalize_addr_bits != last_finalize_addr_bits",
                ));
            }
            last_init_addr_bits_prev = public_values.last_init_addr_bits;
            last_finalize_addr_bits_prev = public_values.last_finalize_addr_bits;
        }

        // Digest constraints.
        //
        // Initialization:
        // - `committed_value_digest` should be zero.
        // - `deferred_proofs_digest` should be zero.
        //
        // Transition:
        // - If `committed_value_digest_prev` is not zero, then `committed_value_digest` should
        //   equal
        //  `committed_value_digest_prev`. Otherwise, `committed_value_digest` should equal zero.
        // - If `deferred_proofs_digest_prev` is not zero, then `deferred_proofs_digest` should
        //   equal
        //  `deferred_proofs_digest_prev`. Otherwise, `deferred_proofs_digest` should equal zero.
        // - If it's not a shard with "CPU", then `committed_value_digest` should not change from
        //   the
        //  previous shard.
        // - If it's not a shard with "CPU", then `deferred_proofs_digest` should not change from
        //   the
        //  previous shard.
        let zero_committed_value_digest =
            [Word([BabyBear::zero(); WORD_SIZE]); PV_DIGEST_NUM_WORDS];
        let zero_deferred_proofs_digest = [BabyBear::zero(); POSEIDON_NUM_WORDS];
        let mut committed_value_digest_prev = zero_committed_value_digest;
        let mut deferred_proofs_digest_prev = zero_deferred_proofs_digest;
        for shard_proof in proof.0.iter() {
            let public_values: &PublicValues<Word<_>, _> =
                shard_proof.public_values.as_slice().borrow();
            if committed_value_digest_prev != zero_committed_value_digest &&
                public_values.committed_value_digest != committed_value_digest_prev
            {
                return Err(MachineVerificationError::InvalidPublicValues(
                    "committed_value_digest != committed_value_digest_prev",
                ));
            } else if deferred_proofs_digest_prev != zero_deferred_proofs_digest &&
                public_values.deferred_proofs_digest != deferred_proofs_digest_prev
            {
                return Err(MachineVerificationError::InvalidPublicValues(
                    "deferred_proofs_digest != deferred_proofs_digest_prev",
                ));
            } else if !shard_proof.contains_cpu() &&
                public_values.committed_value_digest != committed_value_digest_prev
            {
                return Err(MachineVerificationError::InvalidPublicValues(
                    "committed_value_digest != committed_value_digest_prev",
                ));
            } else if !shard_proof.contains_cpu() &&
                public_values.deferred_proofs_digest != deferred_proofs_digest_prev
            {
                return Err(MachineVerificationError::InvalidPublicValues(
                    "deferred_proofs_digest != deferred_proofs_digest_prev",
                ));
            }
            committed_value_digest_prev = public_values.committed_value_digest;
            deferred_proofs_digest_prev = public_values.deferred_proofs_digest;
        }

        // Verify that the number of shards is not too large.
        if proof.0.len() >= 1 << 16 {
            return Err(MachineVerificationError::TooManyShards);
        }

        // Verify the shard proof.
        let mut challenger = self.core_prover.config().challenger();
        let machine_proof = MachineProof { shard_proofs: proof.0.to_vec() };
        self.core_prover.machine().verify(&vk.vk, &machine_proof, &mut challenger)?;

        Ok(())
    }
Verify a core proof by verifying the shards, verifying lookup bus, verifying that the
shards are contiguous and complete.
crates/prover/src/verify.rs