programs: fix Float specs referencing removed wp_call_of_terminates - #146
Merged
Conversation
`main` fails `Build & verify proofs`: the Float{Trunc,Round,Reinterpret}
specs call `wp_call_of_terminates`, which no longer exists.
PR #113 dropped that alias in favour of the byte-identical `wp_call_tw`
and repointed its call sites, but the Float Programs PR (#132) branched
beforehand and reintroduced the dead name, so the two merged into a
red main.
`wp_call_of_terminates` was defined as `wp_call_tw hRun hPost` with an
identical signature, so this is a pure rename of all 22 call sites
(2 + 6 + 14). Verified locally: all three `Project.Float*.Spec` targets
build.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Contributor
|
Verifier report preview: https://talos-verifier-report-pr-146.vercel.app (This URL is stable for this PR — it always points to the latest build of f6e92d0.) |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Problem
mainis red — the Build & verify proofs CI job fails becauseProject.FloatTrunc.Spec,Project.FloatRound.Spec, andProject.FloatReinterpret.Speccallwp_call_of_terminates, which no longer exists:Root cause
A merge-order collision between two already-merged PRs:
wp_call_of_terminatesalias in favour of the byte-identicalwp_call_twand repointed its call sites.wp_call_of_terminatesin the new Float specs.Both merged, leaving
mainreferencing a deleted lemma. This blocks CI on every open PR (it's how I noticed — it surfaced on an unrelated docstring PR).Fix
wp_call_of_terminateswas defined as:— same signature and argument order as
wp_call_tw, so this is a pure rename of all 22 call sites (2 in FloatTrunc, 6 in FloatRound, 14 in FloatReinterpret). No proof restructuring.Verification
Built locally against the pinned v4.32.0 toolchain:
🤖 Generated with Claude Code