Merging latest master into feature/p-token#994
Closed
mariaKt wants to merge 6 commits intofeature/p-tokenfrom
Closed
Merging latest master into feature/p-token#994mariaKt wants to merge 6 commits intofeature/p-tokenfrom
mariaKt wants to merge 6 commits intofeature/p-tokenfrom
Conversation
Collaborator
mariaKt
commented
Mar 18, 2026
mariaKt
commented
- Update dependency: deps/stable-mir-json_release 966
- docs: streamline README and improve CLI --help descriptions 979
- fix(kmir.md): handle projected operandMove callees 983
- Collapse prove-rs into prove 986
- Added volatile_load intrinsic 987
- test(stable-mir-ui): add external UI test harness with skip management 968
Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: github-actions[bot] <github-actions[bot]@users.noreply.github.com> Co-authored-by: Daniel Cumming <124537596+dkcumming@users.noreply.github.com>
## Summary **README.md:** - Consolidate repeated setup instructions (rustup, git clone, submodule init) into a single Quick Start section - Replace verbose per-command CLI documentation with a command table — detailed options available via `--help` - Add "Typical proof workflow" section showing the prove → show → inspect cycle - Add "Debugging a stuck or failing proof" section covering `--break-on-*` flags, `section-edge`, `prune`, and module export/import - Reduce README from ~245 lines to ~163 lines with no information loss **CLI `--help` improvements (`__main__.py`):** - `run`: clarify `--bin` (cargo target) vs `--file` (SMIR JSON) mutual exclusivity; `--depth` → "execution steps" - `prove-rs`: `--max-depth` explains KCFG edge semantics; `--reload` warns about discarding progress; `--break-on-function` clarifies substring matching - `show`: `--full-printer` notes default is compact; `--minimize-proof` notes dependency on `--to-module`; `--rules` describes Markdown link output; `--node-deltas-pro` documents auto-printing rules - `prune`: `NODE` explains subtree removal - `section-edge`: clearer edge format description - `info --types`: documents output format and behavior when omitted - `link --output-file`: shows default value ## Test plan - [x] Verify `--help` output renders correctly for all subcommands - [x] README renders correctly on GitHub
## Summary Fix call dispatch for projected `operandMove` callees. When the callee is reached through `projectionElemDeref`, `kmir` was not computing the effective callee correctly, which left the proof stuck. This PR adds a regression for that case and updates call dispatch to use the projected place type, allowing the repro to run through to `#EndProgram`. ## Testing Validated as a `red -> partial green -> green` series with: ```bash make test-integration TEST_ARGS="-k spl-multisig-iter-eq-copied-next-fail" ``` Each commit in the final branch passes that scoped command on the remote validation workspace: - `86074df5` `test(integration): add spl-multisig iter-eq copied next repro` - `f04e1656` `fix(call): match projected operandMove callees` - `ceb4a2a0` `fix(call): compute projected callee types through to EndProgram` --------- Co-authored-by: automergerpr-permission-manager[bot] <190534181+automergerpr-permission-manager[bot]@users.noreply.github.com>
Collapse `prove-rs` into `prove`: - ProveRSOpts merged into ProveOpts - `kmir prove` is the primary command (`prove-rs` kept as alias for backwards compatibility) - adds `parsed_smir` option for programmatic use (useful for tests with many start symbols like #985)
This PR adds the [volatile_load](https://doc.rust-lang.org/std/intrinsics/fn.volatile_load.html) intrinsic. For this semantics, memory being "volatile" is meaningless as the we are not compiling any further, and aren't modeling any compiler optimisations that could occur if we were to. Therefore this is implemented as a simple dereference of the pointer and read of the value at the location into the destination.
#968) ## Summary - Add parametrized pytest harness running `kmir prove-rs` against every entry in `stable-mir-json`'s `passing.tsv` - Ship `skip.txt` (2859 entries) for known-failing cases, with `--update-skip` mode to shrink it by re-proving skipped cases - 300s per-test timeout via `pytest-timeout`; proof show output saved to `tmp_path` on failure ## Usage ```bash # Normal run (skipped cases are skipped) RUST_DIR_ROOT=/path/to/rust make test-stable-mir-ui # Shrink skip.txt by re-proving skipped cases RUST_DIR_ROOT=/path/to/rust make test-stable-mir-ui TEST_ARGS="--update-skip" ``` ## Test plan - [x] `make check` passes (B011 lint fixed) - [x] Single squashed commit, rebased on `origin/master` --------- Co-authored-by: Daniel Cumming <124537596+dkcumming@users.noreply.github.com> Co-authored-by: dkcumming <daniel.cumming@runtimeverification.com>
Collaborator
Author
|
Closed in favor of #996 |
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
4 participants
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.