ci(kani): pin Kani 0.68.0 in every tier; record the accepted add_64/sub_64 gap (#169) - #220
Merged
Merged
Conversation
…ub_64 gap (#169) - kani-github-action used `kani-version: latest`, which queries crates.io. A failed lookup failed wide-tier and_32 in 19 s (run 36821560393: "Could not determine the latest Kani version"). Pinned to 0.68.0 in all three uses; this is the same unpinned-tool class as #189. - add_64/sub_64 stay unscheduled. The self-hosted rust-cpu pool was tried: one run timed out at 90 min and the other ran about 3 h until the runner dropped, with no log either time. The maintainer accepted the gap. These rules are proven at every width in Lean (BlasterArith.lean), and since #192 phase 2 those proofs cover the code that runs. The tier script records the reason. Implements: TR-046 Refs: #169 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01EBJ6kdJ16E3hnsBbq9Lwf1
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.
Two changes for #169.
kani-version: latest, which looks up the newest Kani on crates.io before every run. That lookup failed in run 36821560393 and took down the wide-tierand_32job in 19 s. This is the same unpinned-tool problem as Release supply chain: unpinned tools (cross at git HEAD), no macOS CI, caret dep on the trusted checker, wasm not published with a digest #189.add_64/sub_64gap is accepted and recorded (your decision). The org self-hostedrust-cpurunner was tried twice. Run 36813381641 timed out at 90 min, and run 36821560393 ran about 3 h until the runner itself dropped. Neither left a log. These two rules are proven at every width in Lean (BlasterArith.lean), and since Research: close the query→CNF gap — end-to-end verified encoder or a proven re-encoder beside the checker (structural fix for the #182 class) #192 phase 2 those proofs cover the code that actually runs. They are also tested exhaustively at width 8 and randomized at 32/64.The self-hosted job branch is not merged and is being deleted. actionlint is clean, and
kani_tiers.sh checkpasses.🤖 Generated with Claude Code
https://claude.ai/code/session_01EBJ6kdJ16E3hnsBbq9Lwf1