chore: sync feature/p-token with master#1007
Open
Stevengre wants to merge 7 commits intofeature/p-tokenfrom
Open
chore: sync feature/p-token with master#1007Stevengre wants to merge 7 commits intofeature/p-tokenfrom
Stevengre wants to merge 7 commits intofeature/p-tokenfrom
Conversation
…ng wrappers. (#989) This is a bit of everything in one go, but what I was trying to do was isolate the case seen in [this Kompass test](https://github.com/runtimeverification/kompass/blob/master/src/tests/integration/data/token/spl-token/show/spl_token_domain_data-fail.main.expected) that was discussed in #987. The `volatile_load` is coming from `Box::new` which we are not supporting right now as that does heap allocation. This PR: - Adds failing tests for statics (not decoding properly) - Adds a failing test for `Box::new` - Supports sound transmutation between transparent wrappers (in `#[repr(rust)]` case and their wrapped type. Seen as a `thunk` earlier in the `Box::new` proof and I thought I would solve it now. There are tests for this changed from failing passing in the commit history. So the `volatile_load` is expected to fail until we figure out some support for the things that these tests fail on. This is not blocking any work now so I think it is fine just to add the failing tests --------- Co-authored-by: automergerpr-permission-manager[bot] <190534181+automergerpr-permission-manager[bot]@users.noreply.github.com>
## Summary - Skip LLVM backend `test_exec_smir` tests in CI — keep Haskell only, since it's the backend used for proving and bugs there have higher impact - Skip `test_prove_termination` in CI — the same 19 programs are already executed via `test_exec_smir[*-haskell]` This is done via a pytest `-k` filter in the CI workflow only — **no test code is modified**, so all tests remain available for local development. **Deselected: 58 of 247 tests** (39 LLVM exec_smir + 19 prove_termination) ## Risk Analysis - LLVM backend regression will be missed in the previous test, which should be handled by future test framework refactoring. But if we don't add new `exec_smir` test or add new `exec_smir` test with llvm to update expected files, the result is the same as we run CI before. - `test_prove_termination` just uses `prove-rs` to validate the termination, which is the same as the comparison with the current expected files. I believe that there is no risk to remove them in this way. ## Expected CI time reduction ~2h37m → ~1h20m (based on [this run](https://github.com/runtimeverification/mir-semantics/actions/runs/22658250856/job/65672639933?pr=957)) ## Test plan - [x] Integration tests pass with the `-k` filter applied - [x] Verify CI time improvement Resolves #971 (Phase 1) --------- Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com> Co-authored-by: dkcumming <daniel.cumming@runtimeverification.com>
This PR adds basic support for [IEEE 754 Floating Point Numbers](https://en.wikipedia.org/wiki/IEEE_754), specifically `f16`, `f32`, `f64`, `f128`. These are already supported in K through builtins (see [domains.md](https://github.com/runtimeverification/k/blob/master/k-distribution/include/kframework/builtin/domains.md#ieee-754-floating-point-numbers)). This work is derivative of the implementation in the c-semantics (see ieee754.k in that repository). In particular: - 6 tests are added that tests each type for equality, negation, comparison, casting, arithmetic, and special values (NaN and Infinity) - Documentation and helpers for floats are added to numbers.md - Decoding is added for floats from bytes in numbers.md (see note on haskell backend below) - Semantic rules for arithmetic are extended for floats in data.md ### Haskell Backend The haskell backend has no `Float` builtins (no Float.hs in [kore/src/Kore/Builtin/](https://github.com/runtimeverification/haskell-backend/tree/master/kore/src/Kore/Builtin)). This means `kore-exec` crashes with "missing hook FLOAT.int2float" when attempting to evaluate a float. The booster avoids this by delegating Float evaluation to the LLVM shared library via `simplifyTerm` in [booster/library/Booster/LLVM.hs](https://github.com/runtimeverification/haskell-backend/blob/master/booster/library/Booster/LLVM.hs). Prior to being able to decode floats, they were left as `UnableToDecode` which did not throw and error in the exec-smir test suite for `--haskell-backend`. Now that they are able to be decoded, the haskell backend throws on these decoded values. So I am now skipping any tests with decoded floats for exec-smir with haskell backend.
## Summary - remove the redundant `#forceSetLocal` helper now that `#setLocalValue` no longer guards on mutability - route moved-writeback and zero-sized-local initialization through `#setLocalValue` - drop the obsolete interior-mutability fast-path introduced by the old branch state ## Why After rebasing onto current `origin/master`, the original interior-mutability writeback fast-path became obsolete: `#setLocalValue` already permits writes to immutable locals, so the extra helper and its special-case callsites no longer buy any behavior. This PR turns the branch into the cleanup that current master actually needs. ## Validation - `make build` - `cd kmir && uv run pytest src/tests/integration/test_integration.py -v --timeout=600 -k "interior-mut or transmute-maybe-uninit-fail" -x` - 4 passed, 261 deselected - started `make test-integration`; no early failures before stopping due runtime
…pping strategy (#988) ## Summary - Fixes stuck execution caused by incorrect projection chains from `#pointeeProjection` - Root cause: non-deterministic overlap between struct and array rules — when source is a struct and target is an array (or vice versa), both rules match and the LLVM backend's choice determines correctness - Commit history shows why `[priority(45)]` alone doesn't work (it fixes one case but regresses the other) - Fix: always unwrap the source type first; target-side unwrapping deferred to `#pointeeProjectionTarget` - Reproducer from @dkcumming's review comment (minimal `Wrapper([u8; 2])` cast) ## Test plan - [x] `ptr-cast-wrapper-to-array` passes (new reproducer) - [x] `iter_next_2` still passes (regression test for opposite overlap: `[Thing;3] → Thing`) - [x] Full integration test suite passes --------- Co-authored-by: Daniel Cumming <124537596+dkcumming@users.noreply.github.com> Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…on (#813) ## Summary Fix two issues preventing correct handling of zero-sized function item types (e.g., non-capturing closures): 1. **`#zeroSizedType` did not recognize `typeInfoFunType`** (`types.md`) — Function items are inherently zero-sized (`#elemSize` already returns 0), but `#zeroSizedType` returned `false`, preventing `rvalueRef` from materializing uninitialized closure locals. 2. **`#decodeConstant` had no rule for `typeInfoFunType`** (`data.md`) — Zero-sized function constants fell through to the `thunk` wrapper instead of decoding to `Aggregate(variantIdx(0), .List)`. ## Evidence `closure-staged.rs` with `terminate-on-thunk`: | | Steps | Result | |---|---|---| | Before | 44 | `thunk(#decodeConstant(constantKindZeroSized, _, typeInfoFunType(_)))` | | After | 266 | `#EndProgram` | --------- Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com> Co-authored-by: Daniel Cumming <124537596+dkcumming@users.noreply.github.com>
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: aa05ac9e19
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
Comment on lines
+1642
to
+1647
| rule <k> #cast(VAL:Value, castKindTransmute, TY_SOURCE, TY_TARGET) | ||
| => | ||
| Aggregate(variantIdx(0), ListItem(VAL)) | ||
| ... | ||
| </k> | ||
| requires #transparentFieldTy(lookupTy(TY_TARGET)) ==K TY_SOURCE |
There was a problem hiding this comment.
This transmute rule assumes the target is a single-field wrapper, but the guard only checks #transparentFieldTy(...) == TY_SOURCE; #transparentFieldTy matches any zero-offset struct with at least one field, not exactly one field. That allows T -> Struct(T, Zst...) casts to pass and constructs Aggregate(..., ListItem(VAL)) with one element, so reading additional fields later can get stuck or observe malformed values. Please add an explicit one-field check (or materialize all fields) before applying this rewrite.
Useful? React with 👍 / 👎.
Stevengre
added a commit
that referenced
this pull request
Mar 31, 2026
Haskell Proofs hit the 60-minute timeout at ~63% completion in PR #1007, and LLVM Concrete Tests barely exceeded 20 minutes. Increase timeouts to absorb runner variability without masking real regressions. - LLVM Concrete Tests: 20 → 30 minutes - Haskell Proofs: 60 → 120 minutes Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
2 tasks
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
2 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.
Summary
feature/p-tokenwith currentmasterso the symbolic SPL work carries the latest runtime, type, and test updates#forceSetLocalusage exposed by the merge with current masterUpstream commits included
fix(rt): handle zero-sized function types in decode and ZST recognition(fix(rt): handle zero-sized function types in decode and ZST recognition #813)fix(types): make #pointeeProjection confluent with source-first unwrapping strategy(fix(types): make #pointeeProjection confluent with source-first unwrapping strategy #988)cleanup(rt): remove redundant #forceSetLocal(cleanup(rt): remove redundant #forceSetLocal #810)Basic support for floats(Basic support for floats (f16,f32,f64,f128) #995)perf(test): remove redundant integration test executions(ci: split integration tests into parallel LLVM and Haskell jobs with shared build #972)volatile_{load,store}with statics, heap-allocation repros, and transparent-wrapper transmute coverage (volatile_{load,store}with statics. Heap allocations. And transmuting wrappers. #989)Why a replacement PR
feature/p-tokenis a protected branch, so the originalmaster -> feature/p-tokensync PR cannot be repaired by directly updating the base branch. This replacement PR carries the resolved merge result onsync-pr1006instead.Supersedes #1006.
Validation
make buildmake checkmake test-unit PARALLEL=12make smir-parse-testsprove-rs/showexpectations via scoped--update-expected-outputmake test-integration PARALLEL=6was started and the first failure was resolved; remaining suite execution should continue in GitHub CI