Update KMIR tool application: address reviewer feedback, update to v0.4.202#5
Open
Stevengre wants to merge 2 commits intoruntimeverification:add-kmir-toolfrom
Open
Update KMIR tool application: address reviewer feedback, update to v0.4.202#5Stevengre wants to merge 2 commits intoruntimeverification:add-kmir-toolfrom
Stevengre wants to merge 2 commits intoruntimeverification:add-kmir-toolfrom
Conversation
….4.202 - Update Docker image from 0.3.152 to 0.4.202 - Add Known Limitations section addressing soundness questions - Add Artifacts & Audit Mechanisms, Versioning, CI Integration sections - Update prove-rs to prove (canonical command, prove-rs kept as alias) - Add --terminate-on-thunk flag for proof soundness - Fix --no-full-printer (removed in 0.4.x) to --statistics --leaves - Fix typos (Solitidy -> Solidity, absense -> absence, extra parenthesis) Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Reference the runtimeverification/solana-token proofs branch (50+ specs) and verification result tracking issues as a larger-scale case study of KMIR applied to real Rust programs. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
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.
Summary
0.3.152to0.4.202(latest)prove-rs→prove(canonical command;prove-rskept as backward-compatible alias)--terminate-on-thunkflag to all proof invocations for soundness--no-full-printer(removed in 0.4.x) →--statistics --leavesContext
This addresses the outstanding reviewer feedback on model-checking#310:
All 3 proofs (
unchecked_add_i32,unchecked_sub_usize,unchecked_mul_isize) verified passing with the new Docker image0.4.202.Test plan
ubuntu-jammy-0.4.202🤖 Generated with Claude Code