The termination check is under-constrained due to incomplete check of "public_values.next_pc == 0".

[Koukyosyumei]

The verifier determines whether execution properly invoked the halt syscall by checking if public_values.next_pc == 0, as implemented here:

sphinx/prover/src/verify.rs

Lines 54 to 94 in 8a39b95

	for (i, shard_proof) in proof.0.iter().enumerate() {
	let public_values = PublicValues::from_vec(&shard_proof.public_values);
	// Verify shard transitions
	if i == 0 {
	// If it's the first shard, index should be 1.
	if public_values.shard != BabyBear::one() {
	return Err(MachineVerificationError::InvalidPublicValues(
	"first shard not 1",
	));
	}
	if public_values.start_pc != vk.vk.pc_start {
	return Err(MachineVerificationError::InvalidPublicValues(
	"wrong pc_start",
	));
	}
	} else {
	let prev_shard_proof = &proof.0[i - 1];
	let prev_public_values = PublicValues::from_vec(&prev_shard_proof.public_values);
	// For non-first shards, the index should be the previous index + 1.
	if public_values.shard != prev_public_values.shard + BabyBear::one() {
	return Err(MachineVerificationError::InvalidPublicValues(
	"non incremental shard index",
	));
	}
	// Start pc should be what the next pc declared in the previous shard was.
	if public_values.start_pc != prev_public_values.next_pc {
	return Err(MachineVerificationError::InvalidPublicValues("pc mismatch"));
	}
	// Digests and exit code should be the same in all shards.
	if public_values.committed_value_digest != prev_public_values.committed_value_digest
	|| public_values.deferred_proofs_digest
	!= prev_public_values.deferred_proofs_digest
	|| public_values.exit_code != prev_public_values.exit_code
	{
	return Err(MachineVerificationError::InvalidPublicValues(
	"digest or exit code mismatch",
	));
	}
	// The last shard should be halted. Halt is signaled with next_pc == 0.
	if i == proof.0.len() - 1 && public_values.next_pc != BabyBear::zero() {
	return Err(MachineVerificationError::InvalidPublicValues(

However, this check is located inside the else branch for i = 0, and is therefore skipped entirely when the proof contains only one shard.

This issue is disclosed with the permission of @johnchandlerburnham.