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

Open
#205 0 comments 0 reactions 0 assignees View on GitHub

Nobody has claimed this yet.

Assessment

Difficulty
3/5
Estimated time
1-2 days
Newbie friendliness
72/100
Issue type
Bug
Clarity
Clearly specified
Activity status
Quiet
Tech stack
rust
Domain
security

Research direction

Read prover/src/verify.rs around lines 54-94, starting at the termination check for public_values.next_pc == 0. Compare verifier behavior for proofs with one shard and multiple shards, then inspect nearby verification tests or entry points. Done means the single-shard path enforces the same halt-syscall termination condition as the other paths.

Written by the indexing model from the issue text.

Description

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

https://github.com/argumentcomputer/sphinx/blob/8a39b951e3ea520e295b693ad38bff6b43a2630c/prover/src/verify.rs#L54-L94

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.

Dominant language
Rust
Stars
80
Forks
8
No merged PRs in 30d

Contributor guide

Open the contributing guide

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

More from argumentcomputer/sphinx

All issues in argumentcomputer/sphinx

Similar issues

More Rust issues

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.