Skip to content

Fix explicit proof version zero resolution - #1164

Open
DicksonWu654 wants to merge 1 commit into
runtimeverification:masterfrom
DicksonWu654:fix/explicit-version-zero
Open

Fix explicit proof version zero resolution#1164
DicksonWu654 wants to merge 1 commit into
runtimeverification:masterfrom
DicksonWu654:fix/explicit-version-zero

Conversation

@DicksonWu654

@DicksonWu654 DicksonWu654 commented Sep 1, 2026

Copy link
Copy Markdown

Summary

  • Preserve explicitly requested proof version 0 in Foundry.resolve_proof_version.
  • Distinguish an omitted version from any explicit integer value, leaving latest-version selection only for omission.
  • Add a focused unit regression over the ordinary multi-version proof inventory for explicit zero, explicit nonzero, and omitted versions.

Problem

The resolver used a truthiness check for user_specified_version. Because the parser represents version 0 as integer 0, an explicit request for version 0 skipped the user-specified branch and fell through to latest-version selection. With later proof versions present, Kontrol could therefore select a different proof than requested.

Fix

Use an explicit None check so version 0 follows the same validation and selection path as every other requested version. Existing latest-version behavior remains unchanged when no version is supplied.

Regression test

The unit test covers:

  • explicit version 0 returns 0
  • explicit nonzero version 2 returns 2
  • omitted version returns latest version 3

Validation

Tests were not run locally under the review constraint, which prohibits executing repository code and tests. Static review of the complete diff and git diff --check completed successfully.

@DicksonWu654
DicksonWu654 marked this pull request as ready for review September 1, 2026 02:47
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant