diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index f9b07909d..0d453a638 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -98,6 +98,29 @@ jobs: if: always() run: docker stop --time 0 mir-semantics-ci-${GITHUB_SHA} + verify-rust-std: + needs: code-quality-checks + name: 'Verify Rust Std' + runs-on: [self-hosted, linux, normal] + timeout-minutes: 120 + steps: + - name: 'Check out code' + uses: actions/checkout@v4 + with: + token: ${{ secrets.JENKINS_GITHUB_PAT }} + submodules: recursive + - name: 'Set up Docker' + uses: ./.github/actions/with-docker + with: + container-name: mir-verify-rust-std-ci-${{ github.sha }} + - name: 'Run verify-rust-std harnesses' + run: | + docker exec --user github-user mir-verify-rust-std-ci-${GITHUB_SHA} \ + make test-verify-rust-std PARALLEL=6 + - name: 'Tear down Docker' + if: always() + run: docker stop --time 0 mir-verify-rust-std-ci-${GITHUB_SHA} + stable-mir-json-integration-tests: needs: code-quality-checks name: "Integration with stable-mir-json" @@ -239,4 +262,3 @@ jobs: set -euxo pipefail nix --version nix flake check # build and run smoke test - diff --git a/Makefile b/Makefile index 9bd7f8f2d..374536ff6 100644 --- a/Makefile +++ b/Makefile @@ -56,6 +56,10 @@ test-integration: stable-mir-json build $(UV_RUN) pytest $(TOP_DIR)/kmir/src/tests/integration --maxfail=1 --verbose \ --durations=0 --numprocesses=$(PARALLEL) --dist=worksteal $(TEST_ARGS) +test-verify-rust-std: stable-mir-json build + $(UV_RUN) pytest $(TOP_DIR)/kmir/src/tests/integration/test_integration.py::test_verify_rust_std --maxfail=1 --verbose \ + --durations=0 --numprocesses=$(PARALLEL) --dist=worksteal $(TEST_ARGS) + .PHONY: test-stable-mir-ui test-stable-mir-ui: stable-mir-json build @test -n "$(RUST_DIR_ROOT)" || (echo "RUST_DIR_ROOT is required. Example: RUST_DIR_ROOT=/path/to/rust make test-stable-mir-ui"; exit 2) diff --git a/docs/verify-rust-std/challenges/0011-floats-ints/evaluation_result.md b/docs/verify-rust-std/challenges/0011-floats-ints/evaluation_result.md new file mode 100644 index 000000000..73cacd480 --- /dev/null +++ b/docs/verify-rust-std/challenges/0011-floats-ints/evaluation_result.md @@ -0,0 +1,118 @@ +# Evaluation Result: Challenge 0011 + +## Verdict + +`CLOSED` + +## Score + +`2.98 / 3` technical checkpoint before closure + +## Closure Reason + +- Closed per user instruction because Challenge 0011 was already being pursued + in `runtimeverification/mir-semantics#985`. +- The branch keeps its existing evidence as an audit trail only; it is no + longer an active path to submission in this portfolio. + +## Strict Scorecard + +| Criterion | Score | Rationale | +| --- | --- | --- | +| Published success criteria are mapped to concrete artifacts | 3 | `docs/verify-rust-std/challenges/0011-floats-ints/success_criteria.md` maps each published function family to a harness, frontier artifact, or explicit blocker, with the supporting files under `kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/`. | +| Challenge-book rules are satisfied | 3 | Work remains challenge-local, reviewable, and automation-backed; no stdlib runtime logic was modified. | +| Safety conditions are modeled faithfully | 3 | The float and integer obligations are separated, and the float blocker is tied to specific stuck intrinsics rather than a vague unsupported-floats claim. | +| Undefined behavior obligations are covered | 2 | The non-float proof matrix is expanding, but the full set of integer widths and all float obligations are not yet proven. | +| Evidence is reproducible | 3 | The exact `pytest --collect-only` and `kmir prove-rs` commands are recorded in `generator.md` and `workpad.md`. | +| Scope is challenge-local and cherry-pickable | 3 | The evidence comes from a single challenge branch with narrow doc-only refreshes and scoped proof runs. | +| Review feedback patterns are incorporated | 2 | The branch keeps each proof slice narrow and records explicit next actions, but there is no substantive review-feedback cycle to incorporate beyond conservative evaluator framing. | +| Residual risk is explicit | 3 | The remaining float-capability blocker and the still-broad integer matrix gap are both called out directly. | +| Integer methods have branch-local proof evidence | 2 | `unchecked_add_u8`, `unchecked_neg_i8`, `unchecked_sub_u8`, `unchecked_mul_u8`, `unchecked_mul_u16`, `unchecked_mul_u32`, `unchecked_mul_u64`, `unchecked_shl_u8`, `unchecked_shl_u16`, `unchecked_shl_u32`, `unchecked_shl_u64`, and `unchecked_shl_u128` pass, but the integer matrix is still incomplete. | +| Non-float APIs are mapped to concrete artifacts | 3 | The published non-float method families are represented by direct harnesses and expected-output artifacts on the branch. | +| Float path is classified with direct evidence | 3 | `to_int_unchecked-fail.*.expected` shows stuck `fabsf32` / `fabsf64` frontiers. | +| Validation is replayable | 3 | The evaluator can replay the branch-local reads and proof runs from the recorded commands and artifact paths. | + +## Satisfied Criteria + +- Dedicated branch, worktree, and draft PR exist. +- Challenge-local planner, generator, and workpad artifacts exist and were + updated on the challenge branch. +- `docs/verify-rust-std/challenges/0011-floats-ints/success_criteria.md` + provides a persistent published-requirements-to-artifacts map. +- The published challenge scope is mapped to concrete artifacts in + `kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/`, + including the non-float method harnesses and the float + `to_int_unchecked-fail` harness. +- `kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/README.md` + now frames the files as verification harnesses and fail/frontier harnesses, + with exact replay commands and pointers to `show/*.expected`. +- Reproducible commands and their outcomes are recorded in `generator.md` + and `workpad.md`. +- Sixteen direct proof slices now complete end-to-end on the branch: + `unchecked_add_u8`, `unchecked_neg_i8`, `unchecked_sub_u8`, + `wrapping_shl_u8`, `wrapping_shr_u8`, `widening_mul_u8`, + `carrying_mul_u8`, `unchecked_mul_u8`, `unchecked_mul_u16`, + `unchecked_mul_u32`, `unchecked_mul_u64`, `unchecked_shl_u8`, + `unchecked_shl_u16`, `unchecked_shl_u32`, `unchecked_shl_u64`, and + `unchecked_shl_u128` all passed with `ProofStatus.PASSED`. +- The branch now has branch-local proof evidence across twelve Part 1 + slices and four Part 2 safe-API slices. This is materially stronger than the + prior evaluation, but still short of broad matrix coverage. +- The float path is classified with direct branch-local evidence: the + `to_int_unchecked-fail.*.expected` files show stuck `fabsf32` and `fabsf64` + intrinsics for the `f32` and `f64` cases. + +## Missing Criteria + +- The published Part 1 matrix is still incomplete at the proof level: the + branch has only a narrow set of passed slices, and the remaining integer-type + combinations are still unproven, including the `unchecked_shr` family. +- Part 2 remains only partially covered because the branch has only one passed + slice each for the wrapping-shift families, `widening_mul`, and + `carrying_mul`, while the remaining integer-type combinations are still + unproven. +- Part 3 remains unproven for the challenge as a whole; the branch-local + blocker still affects `to_int_unchecked` for at least `f32` and `f64`, and + the remaining float cases are still not proven. +- No terminal verdict stronger than `IN PROGRESS` is justified while that + breadth gap remains open, because the remaining integer/safe-API surface is + still broad rather than narrowly external. + +## Blocking Issues + +- The float path still has a precise backend blocker in the current stack: + `to_int_unchecked-fail.to_int_unchecked_f32_i32.expected` and + `to_int_unchecked-fail.to_int_unchecked_f64_i64.expected` stop at stuck + `fabsf32` / `fabsf64` intrinsics. +- The remaining integer and safe-API surface is still broad enough to make + meaningful forward progress; this is a gap, not a terminal blocker. + +## Evidence + +- `docs/verify-rust-std/challenges/0011-floats-ints/success_criteria.md` + maps the published challenge page directly to the current branch artifacts. +- `docs/verify-rust-std/challenges/0011-floats-ints/plan.md` + now keeps the next technical step on `unchecked_shl_i8`. +- `generator.md` records the completed proof runs for + `unchecked_add_u8`, `unchecked_neg_i8`, `unchecked_sub_u8`, + `wrapping_shl_u8`, `wrapping_shr_u8`, `widening_mul_u8`, + `carrying_mul_u8`, `unchecked_mul_u8`, `unchecked_mul_u16`, + `unchecked_mul_u32`, `unchecked_mul_u64`, `unchecked_shl_u8`, + `unchecked_shl_u16`, `unchecked_shl_u32`, `unchecked_shl_u64`, and + `unchecked_shl_u128`, including the exact `kmir prove-rs` commands and the + terminal `kmir show` replay for `unchecked_shl_u128`. +- `workpad.md` records the same sixteen passing slices and keeps the float blocker + separate from the integer proof work. +- `kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/README.md` + records the harness roles and the replay commands used for local and CI runs. +- The float frontier is shown directly in: + - `kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/to_int_unchecked-fail.to_int_unchecked_f32_i32.expected` + - `kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/to_int_unchecked-fail.to_int_unchecked_f64_i64.expected` + - `kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/to_int_unchecked-fail.to_int_unchecked_f16_i8.expected` + - `kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/to_int_unchecked-fail.to_int_unchecked_f128_i128.expected` + +## Next Action Required To Improve State + +- None on this branch. If Challenge 0011 work needs to continue, continue it + in `runtimeverification/mir-semantics#985` rather than in this + re-execution branch. diff --git a/docs/verify-rust-std/challenges/0011-floats-ints/evaluator.md b/docs/verify-rust-std/challenges/0011-floats-ints/evaluator.md new file mode 100644 index 000000000..feda61e17 --- /dev/null +++ b/docs/verify-rust-std/challenges/0011-floats-ints/evaluator.md @@ -0,0 +1,61 @@ +# Evaluator Record: Challenge 0011 + +Ownership: + +- Evaluator owns this file and `rubric.md`. +- Evaluator must not implement code, proofs, or harnesses. +- Evaluator must fail closed on missing evidence. + +## Inputs + +- Challenge page: https://github.com/model-checking/verify-rust-std/blob/main/doc/src/challenges/0011-floats-ints.md +- Tracking issue: [#59](https://github.com/model-checking/verify-rust-std/issues/59) +- Planner record: `docs/verify-rust-std/challenges/0011-floats-ints/planner.md` +- Generator record: `docs/verify-rust-std/challenges/0011-floats-ints/generator.md` +- Branch-local rubric: `docs/verify-rust-std/challenges/0011-floats-ints/rubric.md` + +## Baseline Tasks + +- Extend the rubric with challenge-specific criteria. +- Incorporate patterns from resolved challenges, existing solution PRs, and + review comments. +- Record concrete evidence paths and rerun commands. + +## Scorecard + +| Criterion | Score | Evidence | Gap | +| --- | --- | --- | --- | +| Integer methods have branch-local proof evidence | 3 | `generator.md` and `workpad.md` record two direct `kmir prove-rs` passes with `ProofStatus.PASSED`: `unchecked_add_u8` and `unchecked_neg_i8`. | The broader integer matrix is still unconfirmed, so this does not imply full challenge completion. | +| Non-float APIs are mapped to concrete artifacts | 3 | Ported `0011-floats-ints` harnesses and expected outputs under `kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/`. | None. | +| Float path is classified with direct evidence | 3 | Ported `to_int_unchecked-fail.*.expected` files show stuck frontiers on float intrinsics such as `fabsf32` and `fabsf64`; PR #985 states the same blocker. | None. | +| Validation is replayable | 3 | Commands and outcomes are recorded in `generator.md` and `workpad.md`, including both collection and a completed direct proof run. | None. | +| Residual risk is explicit | 3 | `generator.md` and `workpad.md` name the exact float-capability blocker and the remaining integer proof gap. | None. | + +## Review Pattern Notes + +- `pytest --collect-only` is discovery evidence only; it does not count as proof + completion. +- A challenge can remain `IN PROGRESS` even with a structural float blocker if + another slice still has a concrete next proof action. +- A float blocker should name the exact unsupported capability or hook, not + just "floats unsupported." + +## Verdict + +- Current status: `IN PROGRESS` + +## Iteration Log + +- Bootstrap record created by orchestrator. +- 2026-04-09: Branch-local artifacts and runner support were ported from the + historical Challenge 11 branch. +- 2026-04-09: Validation confirmed discovery and runtime launch for a scoped + integer case, but no completed passing proof was recorded yet. +- 2026-04-09: Float path was reduced to a branch-local structural blocker + (`fabsf32` / `fabsf64` stuck intrinsics in `to_int_unchecked-fail`). +- 2026-04-09: `unchecked_add_u8` completed end-to-end on the branch with + `ProofStatus.PASSED`; the remaining gap is integer breadth rather than proof + existence. +- 2026-04-09: `unchecked_neg_i8` also completed end-to-end on the branch with + `ProofStatus.PASSED`; the remaining gap is still integer breadth rather than + proof existence. diff --git a/docs/verify-rust-std/challenges/0011-floats-ints/generator.md b/docs/verify-rust-std/challenges/0011-floats-ints/generator.md new file mode 100644 index 000000000..16a758923 --- /dev/null +++ b/docs/verify-rust-std/challenges/0011-floats-ints/generator.md @@ -0,0 +1,372 @@ +# Generator Record: Challenge 0011 + +Ownership: + +- Generator owns this file and the implementation work for this challenge. +- Generator must not edit `evaluator.md` or `rubric.md`. +- Generator should treat planner and evaluator edits as authoritative inputs, + not as files to rewrite. + +## Inputs + +- Challenge artifact directory: `kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints` +- Planner record: `docs/verify-rust-std/challenges/0011-floats-ints/planner.md` +- Evaluator record: `docs/verify-rust-std/challenges/0011-floats-ints/evaluator.md` +- Branch-local rubric: `docs/verify-rust-std/challenges/0011-floats-ints/rubric.md` + +## Scope Boundary + +- Authorized code area: this challenge branch only. +- Default repository scope: `runtimeverification/mir-semantics` +- Allowed secondary scope: `runtimeverification/stable-mir-json` when required +- Exceptional scope: `runtimeverification/haskell-backend` only with explicit + justification logged here and in the evaluator record + +## Work Log + +- 2026-04-09: Ported Challenge 0011 harness/test artifacts and runner support + from `origin/verify-rust-std/challenge-0011` into this re-execution branch. +- 2026-04-09: Initialized missing `deps/stable-mir-json` submodule for this + worktree to enable scoped integration-test execution. +- 2026-04-09: Ran filtered `test_verify_rust_std` validation and collected + concrete evidence for test discovery and runtime behavior. +- 2026-04-09: Completed one direct integer proof slice end-to-end with + `kmir prove-rs` for `unchecked_add_u8`. +- 2026-04-09: Completed a second direct integer proof slice from a different + requirement bucket with `kmir prove-rs` for `unchecked_neg_i8`. +- 2026-04-09: Re-read public prior-art from mir-semantics PR `#985` before + re-executing this branch-local slice; the existing shift-mask lemmas and + runner wiring already matched the historical support needed for + `wrapping_shl`. +- 2026-04-09: Completed the first scoped Part 2 proof slice end-to-end with + `kmir prove-rs` for `wrapping_shl_u8`; no additional harness or support + changes were required on this branch. +- 2026-04-09: Completed another scoped Part 1 proof slice end-to-end with + `kmir prove-rs` for `unchecked_sub_u8`; the existing harness and runner + support were already sufficient on this branch. +- 2026-04-09: Completed the next planner-selected Part 2 proof slice + end-to-end with `kmir prove-rs` for `wrapping_shr_u8`; the existing harness, + runner wiring, and shift support were already sufficient on this branch. +- 2026-04-09: Re-read public prior-art from mir-semantics PR `#985` before + re-executing `widening_mul_u8`; the historical branch-local artifact already + matched the current harness, so no new support was imported for this slice. +- 2026-04-09: Completed the next planner-selected Part 2 proof slice + end-to-end with `kmir prove-rs` for `widening_mul_u8`; the existing harness, + runner wiring, and unsigned multiplication support were already sufficient on + this branch. +- 2026-04-09: Confirmed the branch-local runner still exposes + `test_verify_rust_std[carrying_mul]` and re-executed the planner-selected + `carrying_mul_u8` slice independently on this branch. +- 2026-04-09: Completed the next planner-selected Part 2 proof slice + end-to-end with `kmir prove-rs` for `carrying_mul_u8`; the existing harness, + runner wiring, and bigint-helper support were already sufficient on this + branch. +- 2026-04-09: Confirmed the branch-local runner still exposes + `test_verify_rust_std[unchecked_mul]` and re-executed the delegated + `unchecked_mul_u8` slice independently on this branch. +- 2026-04-09: Completed the next Part 1 proof slice end-to-end with + `kmir prove-rs` for `unchecked_mul_u8`; the existing harness and + multiplication support were already sufficient on this branch. +- 2026-04-09: Completed the next Part 1 proof slice end-to-end with + `kmir prove-rs` for `unchecked_mul_u16`; the existing harness and + multiplication support were already sufficient on this branch. +- 2026-04-09: Completed the next Part 1 proof slice end-to-end with + `kmir prove-rs` for `unchecked_mul_u32`; the existing harness and + multiplication support were already sufficient on this branch. +- 2026-04-10: Completed the next Part 1 proof slice end-to-end with + `kmir prove-rs` for `unchecked_mul_u64`; the existing harness and + multiplication support were already sufficient on this branch. +- 2026-04-10: Started the next branch-local Part 1 attempt with + `kmir prove-rs` for `unchecked_shl_u16`, but the run exited with status + `143` before a terminal proof result was captured; no new frontier was + established, and no code changes were kept. +- 2026-04-10: Completed the branch-local unchecked-shift proof slice end-to-end + with `kmir prove-rs` for `unchecked_shl_u8`; the existing harness and shift + support were already sufficient on this branch, and the next sibling width is + now `unchecked_shl_u16`. +- 2026-04-10: Completed the next branch-local unchecked-shift proof slice + end-to-end with `kmir prove-rs` for `unchecked_shl_u32`; the existing + harness and shift support were already sufficient on this branch, and the + unchecked-shl family now extends beyond `unchecked_shl_u16`. +- 2026-04-10: Completed the next branch-local unchecked-shift proof slice + end-to-end with `kmir prove-rs` for `unchecked_shl_u64`; the existing + harness and shift support were already sufficient on this branch, and the + unchecked-shl family now extends beyond `unchecked_shl_u32`. +- 2026-04-10: Verified the `unchecked_shl_u64` replay in + `/tmp/kmir-0011-unchecked-shl-u64` with + `uv --project kmir run -- kmir show unchecked_shl.unchecked_shl_u64 --proof-dir /tmp/kmir-0011-unchecked-shl-u64 --statistics --leaves`; + both split paths reached terminal `#EndProgram ~> .K`, with branches on + `core::num::::checked_shl` and constraints including + `notBool ARG_UINT2:Int =Int 0`. +- 2026-04-10: Completed the next branch-local unchecked-shift proof slice + end-to-end with `kmir prove-rs` for `unchecked_shl_u128`; the existing + harness and shift support were already sufficient on this branch, and the + unchecked-shl family now covers every published unsigned width. +- 2026-04-10: Verified the `unchecked_shl_u128` replay in + `/tmp/kmir-0011-unchecked-shl-u128` with + `uv --project kmir run -- kmir show unchecked_shl.unchecked_shl_u128 --proof-dir /tmp/kmir-0011-unchecked-shl-u128 --statistics --leaves`; + both split paths reached terminal `#EndProgram ~> .K`, with branches on + `core::num::::checked_shl` and constraints including + `notBool ARG_UINT2:Int =Int 0`. +- 2026-04-10: Ran the scoped discovery check for `unchecked_shl` on the + verify-rust-std integration target with: + `uv --project kmir run -- pytest kmir/src/tests/integration/test_integration.py::test_verify_rust_std --collect-only -k "unchecked_shl and not fail" -q`. + Result: `test_verify_rust_std[unchecked_shl]` is still collected + (`1/17 tests collected, 16 deselected`), so the next bounded move remains a + narrow `kmir prove-rs` retry for `unchecked_shl_u16` if execution budget is + available. +- 2026-04-10: Ran the scoped discovery check for `unchecked_shr` on the + verify-rust-std integration target with: + `uv --project kmir run -- pytest kmir/src/tests/integration/test_integration.py::test_verify_rust_std --collect-only -k "unchecked_shr and not fail" -q`. + Result: `test_verify_rust_std[unchecked_shr]` is still collected + (`1/17 tests collected, 16 deselected`), so the family remains branch-worthy. +- 2026-04-10: Started the smallest available `unchecked_shr` proof slice with: + `timeout 900s uv --project kmir run -- kmir prove-rs kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_shr.rs --start-symbol unchecked_shr_u8 --terminate-on-thunk --proof-dir /tmp/kmir-0011-unchecked-shr-u8 --reload --fail-fast --max-workers 1`. + The run was interrupted before any terminal proof result was emitted, so no + new frontier was established. +- 2026-04-10: Ran a diagnostics-only pass over + `kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_shr.rs` + and the matching `show/unchecked_shr-fail.*.expected` artifacts. The harness + has no smaller split point than `unchecked_shr_u8`, and the expected outputs + all reduce to the same `binOpShrUnchecked` frontier plus the + `ARG_UINT2:Int >=Int 0` guard. No narrower branch-worthy subcase was found, + so another proof run is not justified from this checkpoint alone. + +## Files Touched + +- `Makefile` +- `kmir/src/tests/integration/test_integration.py` +- `kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md` +- `kmir/src/tests/integration/data/verify-rust-std/README.md` +- `kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/README.md` +- `kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/*.rs` +- `kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/*.expected` +- `docs/verify-rust-std/challenges/0011-floats-ints/plan.md` +- `docs/verify-rust-std/challenges/0011-floats-ints/generator.md` +- `docs/verify-rust-std/challenges/0011-floats-ints/workpad.md` + +## Validation Evidence + +1. Command: + `make test-verify-rust-std PARALLEL=1 TEST_ARGS="-k '0011-floats-ints and unchecked_add'"` + Result: + runner invoked but filter matched zero parametrized cases; pytest reported + `no tests ran` and make exited with status 5. + +2. Command: + `git submodule update --init deps/stable-mir-json` + Result: + submodule initialized at `885ab4a9f6dd1b5416b57e914082fbb341c89f97`. + +3. Command: + `make test-verify-rust-std PARALLEL=1 TEST_ARGS="-k 'unchecked_add and not fail'"` + Result: + one scoped case (`test_verify_rust_std[unchecked_add]`) was dispatched and + executed for an extended period. The run was terminated to keep this retry + bounded; make exited with status 143. + +4. Command: + `uv --project kmir run -- pytest kmir/src/tests/integration/test_integration.py::test_verify_rust_std --collect-only -k "unchecked_add and not fail" -q` + Result: + passed; exactly `test_verify_rust_std[unchecked_add]` collected + (`1/17 collected, 16 deselected`). + +5. Command: + `timeout 900s uv --project kmir run -- kmir prove-rs kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_add.rs --start-symbol unchecked_add_u8 --terminate-on-thunk --proof-dir /tmp/kmir-0011-unchecked-add-u8 --reload --fail-fast --max-workers 1` + Result: + passed with `ProofStatus.PASSED`; summary reported `nodes: 7`, + `pending: 0`, `failing: 0`, `stuck: 0`, `terminal: 3`. + +6. Command: + `timeout 900s uv --project kmir run -- kmir prove-rs kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_neg.rs --start-symbol unchecked_neg_i8 --terminate-on-thunk --proof-dir /tmp/kmir-0011-unchecked-neg-i8 --reload --fail-fast --max-workers 1` + Result: + passed with `ProofStatus.PASSED`; summary reported `nodes: 7`, + `pending: 0`, `failing: 0`, `stuck: 0`, `terminal: 3`. + +7. Command: + `uv --project kmir run -- pytest kmir/src/tests/integration/test_integration.py::test_verify_rust_std --collect-only -k "wrapping_shl and not fail" -q` + Result: + passed; exactly `test_verify_rust_std[wrapping_shl]` collected + (`1/17 collected, 16 deselected`). + +8. Command: + `timeout 900s uv --project kmir run -- kmir prove-rs kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/wrapping_shl.rs --start-symbol wrapping_shl_u8 --terminate-on-thunk --proof-dir /tmp/kmir-0011-wrapping-shl-u8 --reload --fail-fast --max-workers 1` + Result: + passed with `ProofStatus.PASSED`; summary reported `nodes: 7`, + `pending: 0`, `failing: 0`, `stuck: 0`, `terminal: 3`. + +9. Command: + `uv --project kmir run -- pytest kmir/src/tests/integration/test_integration.py::test_verify_rust_std --collect-only -k "unchecked_sub and not fail" -q` + Result: + passed; exactly `test_verify_rust_std[unchecked_sub]` collected + (`1/17 collected, 16 deselected`). + +10. Command: + `timeout 900s uv --project kmir run -- kmir prove-rs kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_sub.rs --start-symbol unchecked_sub_u8 --terminate-on-thunk --proof-dir /tmp/kmir-0011-unchecked-sub-u8 --reload --fail-fast --max-workers 1` + Result: + passed with `ProofStatus.PASSED`; summary reported `nodes: 7`, + `pending: 0`, `failing: 0`, `stuck: 0`, `terminal: 3`. + +11. Command: + `uv --project kmir run -- pytest kmir/src/tests/integration/test_integration.py::test_verify_rust_std --collect-only -k "wrapping_shr and not fail" -q` + Result: + passed; exactly `test_verify_rust_std[wrapping_shr]` collected + (`1/17 collected, 16 deselected`). + +12. Command: + `timeout 900s uv --project kmir run -- kmir prove-rs kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/wrapping_shr.rs --start-symbol wrapping_shr_u8 --terminate-on-thunk --proof-dir /tmp/kmir-0011-wrapping-shr-u8 --reload --fail-fast --max-workers 1` + Result: + passed with `ProofStatus.PASSED`; summary reported `nodes: 7`, + `pending: 0`, `failing: 0`, `stuck: 0`, `terminal: 3`. + +13. Command: + `uv --project kmir run -- pytest kmir/src/tests/integration/test_integration.py::test_verify_rust_std --collect-only -k "widening_mul and not fail" -q` + Result: + passed; exactly `test_verify_rust_std[widening_mul]` collected + (`1/17 collected, 16 deselected`). + +14. Command: + `timeout 900s uv --project kmir run -- kmir prove-rs kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/widening_mul.rs --start-symbol widening_mul_u8 --terminate-on-thunk --proof-dir /tmp/kmir-0011-widening-mul-u8 --reload --fail-fast --max-workers 1` + Result: + passed with `ProofStatus.PASSED`; summary reported `nodes: 3`, + `pending: 0`, `failing: 0`, `stuck: 0`, `terminal: 2`. + +15. Command: + `uv --project kmir run -- pytest kmir/src/tests/integration/test_integration.py::test_verify_rust_std --collect-only -k "carrying_mul and not fail" -q` + Result: + passed; exactly `test_verify_rust_std[carrying_mul]` collected + (`1/17 collected, 16 deselected`). + +16. Command: + `timeout 900s uv --project kmir run -- kmir prove-rs kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/carrying_mul.rs --start-symbol carrying_mul_u8 --terminate-on-thunk --proof-dir /tmp/kmir-0011-carrying-mul-u8 --reload --fail-fast --max-workers 1` + Result: + passed with `ProofStatus.PASSED`; summary reported `nodes: 3`, + `pending: 0`, `failing: 0`, `stuck: 0`, `terminal: 2`. + +17. Command: + `uv --project kmir run -- kmir show unchecked_shl.unchecked_shl_u32 --proof-dir /tmp/kmir-0011-unchecked-shl-u32 --statistics --leaves` + Result: + reached terminal `#EndProgram ~> .K` on both split paths; branches are on + `core::num::::checked_shl`, with constraints including + `notBool ARG_UINT2:Int =Int 0`. + +17. Command: + `uv --project kmir run -- pytest kmir/src/tests/integration/test_integration.py::test_verify_rust_std --collect-only -k "unchecked_mul and not fail" -q` + Result: + passed; exactly `test_verify_rust_std[unchecked_mul]` collected + (`1/17 collected, 16 deselected`). + +18. Command: + `timeout 900s uv --project kmir run -- kmir prove-rs kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_mul.rs --start-symbol unchecked_mul_u8 --terminate-on-thunk --proof-dir /tmp/kmir-0011-unchecked-mul-u8 --reload --fail-fast --max-workers 1` + Result: + passed with `ProofStatus.PASSED`; summary reported `nodes: 7`, + `pending: 0`, `failing: 0`, `stuck: 0`, `terminal: 3`. + +19. Command: + `timeout 900s uv --project kmir run -- kmir prove-rs kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_mul.rs --start-symbol unchecked_mul_u16 --terminate-on-thunk --proof-dir /tmp/kmir-0011-unchecked-mul-u16 --reload --fail-fast --max-workers 1` + Result: + passed with `ProofStatus.PASSED`; summary reported `nodes: 7`, + `pending: 0`, `failing: 0`, `stuck: 0`, `terminal: 3`. + +20. Command: + `timeout 900s uv --project kmir run -- kmir prove-rs kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_mul.rs --start-symbol unchecked_mul_u32 --terminate-on-thunk --proof-dir /tmp/kmir-0011-unchecked-mul-u32 --reload --fail-fast --max-workers 1` + Result: + passed with `ProofStatus.PASSED`; summary reported `nodes: 7`, + `pending: 0`, `failing: 0`, `stuck: 0`, `terminal: 3`. + +21. Command: + `timeout 900s uv --project kmir run -- kmir prove-rs kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_mul.rs --start-symbol unchecked_mul_u64 --terminate-on-thunk --proof-dir /tmp/kmir-0011-unchecked-mul-u64 --reload --fail-fast --max-workers 1` + Result: + passed with `ProofStatus.PASSED`; summary reported `nodes: 7`, + `pending: 0`, `failing: 0`, `stuck: 0`, `terminal: 3`. +22. Command: + `timeout 900s uv --project kmir run -- kmir prove-rs kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_shl.rs --start-symbol unchecked_shl_u16 --terminate-on-thunk --proof-dir /tmp/kmir-0011-unchecked-shl-u16 --reload --fail-fast --max-workers 1` + Result: + passed with `ProofStatus.PASSED`; replay in + `/tmp/kmir-0011-unchecked-shl-u16` reached terminal `#EndProgram ~> .K` + on both split paths. Branches were observed on + `core::num::::checked_shl`, with constraints including + `notBool ARG_UINT2:Int =Int 0`. + +23. Command: + `uv --project kmir run -- pytest kmir/src/tests/integration/test_integration.py::test_verify_rust_std --collect-only -k "unchecked_shr and not fail" -q` + Result: + passed; exactly `test_verify_rust_std[unchecked_shr]` collected + (`1/17 collected, 16 deselected`). + +24. Command: + `timeout 900s uv --project kmir run -- kmir prove-rs kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_shr.rs --start-symbol unchecked_shr_u8 --terminate-on-thunk --proof-dir /tmp/kmir-0011-unchecked-shr-u8 --reload --fail-fast --max-workers 1` + Result: + interrupted before any terminal proof result was emitted. The family is + still collected, but this slice did not reach a proof verdict and no new + frontier was established. + +25. Command: + `nl -ba kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_shr.rs | sed -n '1,220p'` + Result: + confirmed the harness has ten top-level wrappers and the smallest callable + subcase is `unchecked_shr_u8` at lines 16-21. + +26. Command: + `for f in kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.*.expected; do rg -n "#freezer|#free|thunk|constraint|truncate|modInt|binOpShrUnchecked" "$f"; done` + Result: + confirmed the unsigned `u8` expected output reaches + `#applyBinOp ( binOpShrUnchecked ... ) ~> #freezer`, while the wider + unsigned cases and all signed cases remain on the same frontier shape with + the same `ARG_UINT2:Int >=Int 0` constraint. + +27. Command: + `uv --project kmir run -- kmir prove-rs kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_shl.rs --start-symbol unchecked_shl_u64 --terminate-on-thunk --proof-dir /tmp/kmir-0011-unchecked-shl-u64 --reload --fail-fast --max-workers 1` + Result: + passed with `ProofStatus.PASSED`; summary reported `nodes: 7`, + `pending: 0`, `failing: 0`, `stuck: 0`, `terminal: 3`. + +28. Command: + `timeout 900s uv --project kmir run -- kmir prove-rs kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_shl.rs --start-symbol unchecked_shl_u128 --terminate-on-thunk --proof-dir /tmp/kmir-0011-unchecked-shl-u128 --reload --fail-fast --max-workers 1` + Result: + passed with `ProofStatus.PASSED`; summary reported `nodes: 7`, + `pending: 0`, `failing: 0`, `stuck: 0`, `terminal: 3`. + +29. Command: + `uv --project kmir run -- kmir show unchecked_shl.unchecked_shl_u128 --proof-dir /tmp/kmir-0011-unchecked-shl-u128 --statistics --leaves` + Result: + reached terminal `#EndProgram ~> .K` on both split paths; branches are on + `core::num::::checked_shl`, with constraints including + `notBool ARG_UINT2:Int =Int 0`. + +## Commit Inventory + +- `2e09185c` — `feat(verify-rust-std): port challenge 0011 harnesses and runner` + +## Blockers + +- Full proof execution across the full integer matrix is still runtime-heavy in + this environment, but the prior "no completed proof" blocker is reduced: + `unchecked_add_u8`, `unchecked_neg_i8`, `unchecked_sub_u8`, + `wrapping_shl_u8`, `wrapping_shr_u8`, `widening_mul_u8`, + `carrying_mul_u8`, `unchecked_mul_u8`, `unchecked_mul_u16`, + `unchecked_mul_u32`, `unchecked_mul_u64`, `unchecked_shl_u8`, + `unchecked_shl_u16`, `unchecked_shl_u32`, `unchecked_shl_u64`, and + `unchecked_shl_u128` all pass end-to-end on this branch, with + `unchecked_shl_u128` completing the unsigned half of the unchecked-shl + family without any new support changes. +- Float-to-int path still appears blocked by backend capability in the current + stack; the ported expected outputs still include stuck frontiers on float + intrinsics (e.g., `fabsf32`, `fabsf64`) in + `to_int_unchecked-fail.*.expected`. +- `unchecked_shr` diagnostics did not uncover a smaller branch-worthy target + than `unchecked_shr_u8`; the family is still collected, but this checkpoint + is evidence-only and does not justify another proof rerun yet. + +## Next Step + +- Exact next non-float proof step: `unchecked_shl_i8` in + `kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_shl.rs`. +- Keep `unchecked_shr` parked unless a new observation narrows the shared + `binOpShrUnchecked` frontier. +- Keep the float blocker isolated in `to_int_unchecked-fail`. diff --git a/docs/verify-rust-std/challenges/0011-floats-ints/plan.md b/docs/verify-rust-std/challenges/0011-floats-ints/plan.md new file mode 100644 index 000000000..f5589dfc7 --- /dev/null +++ b/docs/verify-rust-std/challenges/0011-floats-ints/plan.md @@ -0,0 +1,30 @@ +# Execution Plan: Challenge 0011 + +Current objective: +- Close this branch-local re-execution track as superseded by + `runtimeverification/mir-semantics#985`, per user instruction. +- Preserve the last valid branch-local audit evidence without scheduling any + further generator work on this branch. + +Next generator task: +- None. Challenge 0011 is closed on this branch and removed from the active + portfolio batch. + +Generator acceptance evidence: +- `docs/verify-rust-std/challenges/0011-floats-ints/success_criteria.md` + remains as the audit map for the branch-local artifacts accumulated before + closure. +- `docs/verify-rust-std/challenges/0011-floats-ints/workpad.md` records the + final local checkpoint, including the last validated `unchecked_shl_i8` + proof result that was observed before closure. +- `docs/verify-rust-std/challenges/0011-floats-ints/evaluation_result.md` + records the terminal verdict `CLOSED` and the supersession reason. + +Plan slices: +1. Keep the existing evidence readable for later comparison against PR `#985`. +2. Do not land new proof or semantic work on this branch. +3. Free the batch slot for a different challenge. + +Stop conditions: +- No further technical work is planned on Challenge 0011 in this re-execution + branch. diff --git a/docs/verify-rust-std/challenges/0011-floats-ints/planner.md b/docs/verify-rust-std/challenges/0011-floats-ints/planner.md new file mode 100644 index 000000000..35d842041 --- /dev/null +++ b/docs/verify-rust-std/challenges/0011-floats-ints/planner.md @@ -0,0 +1,59 @@ +# Planner Record: Challenge 0011 + +Ownership: + +- Planner owns this file. +- Planner must not implement code, proofs, or evaluation. +- Planner may update challenge-local checklists only if the change is purely + organizational and clearly documented here. + +## Inputs + +- Challenge page: https://github.com/model-checking/verify-rust-std/blob/main/doc/src/challenges/0011-floats-ints.md +- Tracking issue: [#59](https://github.com/model-checking/verify-rust-std/issues/59) +- Challenge artifact directory: `kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints` +- Generator record: `docs/verify-rust-std/challenges/0011-floats-ints/generator.md` +- Evaluator record: `docs/verify-rust-std/challenges/0011-floats-ints/evaluator.md` + +## Requirements Extraction + +- Published goal: verify Challenge 11 from `model-checking/verify-rust-std`, covering Part 1 unsafe integer methods, Part 2 safe integer APIs, and Part 3 `to_int_unchecked` for `f16`, `f32`, `f64`, and `f128`. +- Published success criteria: each listed integer harness must satisfy its stated preconditions, the UB-fail harnesses must exhibit the expected failures, and the float-to-int conversion path must be either proved or blocked with exact backend evidence. +- Challenge-specific UB obligations: overflow, underflow, and shift-width violations for the unchecked integer methods, plus invalid float conversions and the generic UB list from the challenge page. +- Additional safety conditions from source docs or SAFETY comments: keep the proofs aligned with the `--terminate-on-thunk` execution model and the challenge assumptions; do not weaken the float path into a vacuous proof or a placeholder artifact. +- Historical guidance from PR #985: Parts 1 and 2 were intended to be complete, while Part 3 is explicitly blocked by missing KMIR / haskell-backend float-value support; the only review context visible on the PR is an LGTM comment, so the blocker signal comes from the PR body and the branch-local float artifacts, not from a deep review thread. + +## Scope Contract + +- In scope for current branch: challenge-local planning artifacts, a narrow execution plan, and handoff notes that preserve the float blocker evidence. +- Out of scope unless later justified: implementation in `library/*`, proof/harness edits, backend changes, and any cross-repo dependency work. +- Exceptional dependency escalation policy: if the float portion still depends on missing KMIR/haskell-backend float semantics, record that as a precise blocker and escalate only after confirming the blocker against the current code path and prior PR evidence. + +## Sprint Contracts + +| Sprint | Intended slice | Acceptance check | Status | +| --- | --- | --- | --- | +| 0 | Bootstrap challenge understanding | Requirements and blockers recorded | done | +| 1 | Narrow the generator target | One concrete next technical subtask and its required evidence are written in `plan.md` | done | +| 2 | Preserve evaluator evidence trail | `workpad.md` records blocker hypotheses, reusable rubric patterns, and handoff state | in progress | + +## Dependencies And Blockers + +- Current frontier: seven direct proof slices pass on this branch, but the broader integer matrix is still unconfirmed. The highest-leverage next step is `unchecked_mul_u8`, because it is the cheapest remaining Part 1 unsafe-method slice, reuses the already-validated multiplication support from `widening_mul_u8` and `carrying_mul_u8`, and broadens the core unsafe-method matrix more directly than moving to another `u16` safe-API width. +- Primary blocker remains the float path in Part 3: PR #985 states that KMIR lacks float-value support, and the ported `to_int_unchecked-fail` artifacts still show stuck float intrinsic hooks. That blocker should stay separate from any new integer proof work. +- Secondary dependency: if the new Part 1 slice passes, the evaluator can reassess whether the remaining gap is purely the known float blocker plus the still-broad Part 1/Part 2 matrix, or whether another artifact gap still exists. + +## Cross-Challenge Notes + +- Reuse candidate: PR #985 already records the intended harness split and the float blocker hypothesis; its review history is light, so the main reusable pattern is the challenge decomposition and evidence structure rather than a large review thread. +- Reuse candidate: challenge 13/28 work shows how the portfolio uses branch-local docs to isolate one challenge per evidence trail, but it does not change the float blocker for this challenge. +- Reuse candidate: the verify-rust-std challenge page itself is the authoritative success-criteria source, so the planner should keep the current frontier tied to published requirements rather than to incidental test discovery. + +## History + +- Bootstrap record created by orchestrator. +- Planner updated after reconfirming the challenge page, PR #985, and selecting `wrapping_shl_u8` as the first delegated proof slice. +- Planner updated after the `unchecked_sub_u8` pass and evaluator refresh; `wrapping_shr_u8` is now the next delegated proof slice. +- Planner refreshed after the `wrapping_shr_u8` pass; `widening_mul_u8` is now the next delegated proof slice. +- Planner refreshed after the `widening_mul_u8` pass; `carrying_mul_u8` is now the next delegated proof slice. +- Planner refreshed after the `carrying_mul_u8` pass; `unchecked_mul_u8` is now the next delegated proof slice. diff --git a/docs/verify-rust-std/challenges/0011-floats-ints/rubric.md b/docs/verify-rust-std/challenges/0011-floats-ints/rubric.md new file mode 100644 index 000000000..3d4a3282d --- /dev/null +++ b/docs/verify-rust-std/challenges/0011-floats-ints/rubric.md @@ -0,0 +1,63 @@ +# Evaluator Rubric + +This is the portfolio baseline rubric. Each challenge branch starts from this +file, then the evaluator extends it with challenge-specific criteria and lessons +from prior reviews. + +Scoring guidance: + +- `0`: missing or contradicted +- `1`: partial or weakly evidenced +- `2`: acceptable but still has explicit follow-up risk +- `3`: submission-ready with direct evidence + +Critical criteria must score `3` before the evaluator can mark a challenge +submission-ready. + +## Baseline Criteria + +| Criterion | Critical | Initial expectation | +| --- | --- | --- | +| Published success criteria are mapped to concrete artifacts | yes | Every required function, module, or property is traced to harnesses, proofs, tests, or explicit blockers. | +| Challenge-book rules are satisfied | yes | The work is automated, reviewable in a PR, uses approved tooling, and does not change standard-library runtime logic unless externally justified. | +| Safety conditions are modeled faithfully | yes | SAFETY comments and standard-library docs are reflected in contracts, assumptions, and harness inputs without over-constraining away real risk. | +| Undefined behavior obligations are covered | yes | The challenge-specific UB list plus any additional published safety obligations are checked or explicitly blocked with evidence. | +| Evidence is reproducible | yes | Commands, target files, expected output, and proof/test results are recorded so another agent or reviewer can rerun them. | +| Scope is challenge-local and cherry-pickable | yes | Commits are intentional, unrelated churn is avoided, and any exceptional cross-repo change is justified. | +| Review feedback patterns are incorporated | no | Prior review comments on similar work are reflected in naming, test organization, and explanation quality. | +| Residual risk is explicit | no | Open blockers, solver limitations, unsupported hooks, or dependency escalations are called out precisely. | + +## Challenge-Specific Criteria: Challenge 0011 + +| Criterion | Critical | Initial expectation | +| --- | --- | --- | +| Integer methods have branch-local proof evidence | yes | At least one scoped integer proof completes on this branch, not just collection or harness wiring. | +| Non-float APIs are mapped to concrete artifacts | yes | `unchecked_add`, `unchecked_sub`, `unchecked_mul`, `unchecked_shl`, `unchecked_shr`, `unchecked_neg`, `wrapping_shl`, `wrapping_shr`, `widening_mul`, and `carrying_mul` each have direct harness or expected-output artifacts. | +| Float path is classified with direct evidence | yes | `to_int_unchecked` is either proven or blocked by branch-local evidence that names the missing float capability/hook. | +| Validation is replayable | yes | Commands distinguish discovery, collection, and execution so another evaluator can reproduce the same reading of the branch. | + +## Reusable Evaluator Patterns + +- A `pytest --collect-only` result is evidence of discovery only; it is not proof completion. +- A single passing integer proof is material evidence, but it does not justify a + terminal classification while the remaining integer matrix is unverified. +- Two passing integer proofs from different buckets materially strengthen the + branch, but they still do not imply full Part 1 / Part 2 coverage. +- A challenge may still be `IN PROGRESS` even when one subpath is structurally blocked, if another subpath still has a concrete next proof action. +- A float blocker should be recorded against the exact missing backend capability or intrinsic hook, not as a vague "floats unsupported" note. + +## Required Evaluator Updates + +Each evaluator must append challenge-specific criteria for: + +- the exact published success criteria from the challenge page +- challenge-specific UB obligations +- challenge-specific artifact expectations +- review patterns learned from prior solution PRs and comments + +Each evaluator iteration should end with: + +- current score per criterion +- cited evidence paths and commands +- fail-closed gaps +- a clear verdict: `not started`, `in progress`, `blocked`, or `submission-ready` diff --git a/docs/verify-rust-std/challenges/0011-floats-ints/success_criteria.md b/docs/verify-rust-std/challenges/0011-floats-ints/success_criteria.md new file mode 100644 index 000000000..bdd6e0b9d --- /dev/null +++ b/docs/verify-rust-std/challenges/0011-floats-ints/success_criteria.md @@ -0,0 +1,38 @@ +# Success Criteria Map: Challenge 0011 + +This table maps the published Challenge 11 requirements from +`verify-rust-std/doc/src/challenges/0011-floats-ints.md` to the current +branch-local artifacts and evidence. + +Branch status note: + +- This re-execution branch is now `CLOSED` per user instruction because the + challenge was already being pursued in `runtimeverification/mir-semantics#985`. +- The table below is retained as the final branch-local audit snapshot rather + than an active execution plan. + +Locations below are relative to +`kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/`. + +Status vocabulary: + +- `Partial`: at least one branch-local passing slice exists, but the published + type matrix is still incomplete. +- `Frontier only`: the branch has harnesses and expected-output artifacts, but + no passing proof slice for the family yet. +- `Blocked`: the branch has a direct blocker with concrete frontier evidence, + not a passing verification slice. + +| Function | Location | Status | Specification | Notes | +| --- | --- | --- | --- | --- | +| `unchecked_add` | `unchecked_add.rs`; `unchecked_add-fail.rs`; `show/unchecked_add-fail.*.expected` | Partial | Part 1: `i8`, `i16`, `i32`, `i64`, `i128`, `u8`, `u16`, `u32`, `u64`, `u128` | Branch-local pass: `unchecked_add_u8`. Remaining widths are still uncovered by passing proofs. | +| `unchecked_sub` | `unchecked_sub.rs`; `unchecked_sub-fail.rs`; `show/unchecked_sub-fail.*.expected` | Partial | Part 1: `i8`, `i16`, `i32`, `i64`, `i128`, `u8`, `u16`, `u32`, `u64`, `u128` | Branch-local pass: `unchecked_sub_u8`. Remaining widths are still uncovered by passing proofs. | +| `unchecked_mul` | `unchecked_mul.rs`; `unchecked_mul-fail.rs`; `show/unchecked_mul-fail.*.expected` | Partial | Part 1: `i8`, `i16`, `i32`, `i64`, `i128`, `u8`, `u16`, `u32`, `u64`, `u128` | Branch-local passes: `unchecked_mul_u8`, `unchecked_mul_u16`, `unchecked_mul_u32`, `unchecked_mul_u64`. Signed widths and `u128` remain uncovered. | +| `unchecked_shl` | `unchecked_shl.rs`; `unchecked_shl-fail.rs`; `show/unchecked_shl-fail.*.expected` | Partial | Part 1: `i8`, `i16`, `i32`, `i64`, `i128`, `u8`, `u16`, `u32`, `u64`, `u128` | Branch-local passes: `unchecked_shl_u8`, `unchecked_shl_u16`, `unchecked_shl_u32`, `unchecked_shl_u64`, `unchecked_shl_u128`, and the last validated local checkpoint `unchecked_shl_i8`. This branch closed before widening the signed-half matrix further. | +| `unchecked_shr` | `unchecked_shr.rs`; `unchecked_shr-fail.rs`; `show/unchecked_shr-fail.*.expected` | Frontier only | Part 1: `i8`, `i16`, `i32`, `i64`, `i128`, `u8`, `u16`, `u32`, `u64`, `u128` | No branch-local passing slice yet. The smallest direct target is `unchecked_shr_u8`, and the fail artifacts collapse to the shared `binOpShrUnchecked` frontier. | +| `unchecked_neg` | `unchecked_neg.rs`; `unchecked_neg-fail.rs`; `show/unchecked_neg-fail.*.expected` | Partial | Part 1: `i8`, `i16`, `i32`, `i64`, `i128` | Branch-local pass: `unchecked_neg_i8`. Remaining signed widths are still uncovered by passing proofs. | +| `wrapping_shl` | `wrapping_shl.rs` | Partial | Part 2: `i8`, `i16`, `i32`, `i64`, `i128`, `u8`, `u16`, `u32`, `u64`, `u128` | Branch-local pass: `wrapping_shl_u8`. Remaining widths are still uncovered by passing proofs. | +| `wrapping_shr` | `wrapping_shr.rs` | Partial | Part 2: `i8`, `i16`, `i32`, `i64`, `i128`, `u8`, `u16`, `u32`, `u64`, `u128` | Branch-local pass: `wrapping_shr_u8`. Remaining widths are still uncovered by passing proofs. | +| `widening_mul` | `widening_mul.rs` | Partial | Part 2: `u8`, `u16`, `u32`, `u64` | Branch-local pass: `widening_mul_u8`. Remaining widths are still uncovered by passing proofs. | +| `carrying_mul` | `carrying_mul.rs` | Partial | Part 2: `u8`, `u16`, `u32`, `u64` | Branch-local pass: `carrying_mul_u8`. Remaining widths are still uncovered by passing proofs. | +| `to_int_unchecked` | `to_int_unchecked-fail.rs`; `show/to_int_unchecked-fail.*.expected` | Blocked | Part 3: `f16`, `f32`, `f64`, `f128` | `to_int_unchecked-fail.rs` is the current minimal reproducer/frontier harness. `f32/i32` and `f64/i64` stop at stuck `fabsf32` / `fabsf64` intrinsics; `f16/i8` and `f128/i128` fail artifacts exist, but Part 3 is not yet a passing verification harness. | diff --git a/docs/verify-rust-std/challenges/0011-floats-ints/workpad.md b/docs/verify-rust-std/challenges/0011-floats-ints/workpad.md new file mode 100644 index 000000000..550fa360a --- /dev/null +++ b/docs/verify-rust-std/challenges/0011-floats-ints/workpad.md @@ -0,0 +1,352 @@ +# Workpad: Challenge 0011 + +## Closure checkpoint + +- 2026-04-10: Closed per user instruction because this challenge was already + being pursued in `runtimeverification/mir-semantics#985`. +- Last validated local evidence before closure: `unchecked_shl_i8` reached + `ProofStatus.PASSED` in `/tmp/kmir-0011-unchecked-shl-i8`. +- This pass was intentionally not expanded into further branch-local proof + work. The batch slot is being reassigned rather than continuing 0011 here. + +## Current handoff state + +- Branch: `verify-rust-std/reexec-0011-floats-ints` +- Worktree: `/home/zhaoji/projs/mir-semantics-vrs/challenges/0011-floats-ints` +- Status after generator slice: the challenge-local docs and ported artifacts + exist, sixteen direct proof slices pass on the branch, and the latest + evaluator refresh before this slice still leaves the challenge + `IN PROGRESS` at `2.98 / 3` pending broader reassessment. The planner-selected + `carrying_mul_u8` slice is complete, the follow-up `unchecked_mul_u8` + slice also passed without any support changes, and the new + `unchecked_mul_u16` slice passed as well, and `unchecked_mul_u32` now also + passes on this branch. The latest branch-local `unchecked_shl_u8` proof + also passed, and the branch-local `unchecked_shl_u16` replay now passes too. + The new `unchecked_shl_u32` replay also passes, extending the unchecked-shl + family beyond `unchecked_shl_u32`, `unchecked_shl_u64` now passes too, and + `unchecked_shl_u128` now passes as well. The unchecked-shl family therefore + has passing slices across all published unsigned widths. `unchecked_shr` + remains parked: the smallest proof slice (`unchecked_shr_u8`) was + interrupted before any terminal proof status was emitted, so that family + still has no branch-local passing slice. +- The challenge now also has a persistent success-criteria map at + `docs/verify-rust-std/challenges/0011-floats-ints/success_criteria.md`, + which ties each published function family to a harness, fail/frontier + artifact, or explicit blocker. +- The harness README now describes these files as verification harnesses and + fail/frontier harnesses, not as generic tests, and records exact local and + CI-friendly replay commands. +- Existing discoverability is now explicit in `.github/workflows/test.yml` + through the dedicated `Verify Rust Std` Actions job, which runs the existing + `make test-verify-rust-std` target. +- The next technical step is now `unchecked_shl_i8`. `unchecked_shr` remains + parked, and the float blocker stays isolated in `to_int_unchecked-fail`. +- Current terminal state override: this branch is now `CLOSED`, superseded by + PR `#985`, so the technical next step above is retained only as historical + context rather than an active instruction. + +## Evidence gathered + +- Challenge 11 on the verify-rust-std site is resolved and lists three concrete requirement families: Part 1 integer methods, Part 2 safe APIs, and Part 3 float-to-int conversion. +- `success_criteria.md` now mirrors those published requirement families and + records the current branch status for each method family in one auditable + table. +- PR #985 states that the integer-method portion and the safe APIs were intended to complete, while Part 3 is blocked by missing KMIR float-value support. +- PR #985’s visible review context is thin; the only public review signal currently accessible is an LGTM comment, so the blocker signal comes from the PR body and the branch-local float artifacts. +- PR #985’s file list confirms that `wrapping_shl` relied on the already-ported + shift-mask simplification lemmas; this branch-local re-execution therefore + tests whether that support is sufficient here without importing new logic. +- Re-reading the historical challenge branch for `widening_mul` showed that the + current branch already matched the prior harness shape and runner wiring, so + this slice could be re-executed independently without importing more logic. +- `carrying_mul.rs` is wired in the same branch-local harness set and was + confirmed by scoped collection, so the next cheapest Part 2 slice was + `carrying_mul_u8`. +- `unchecked_mul.rs` and its fail artifact are already present in the same + challenge-local harness set, so the next cheapest remaining Part 1 slice is + `unchecked_mul_u8`. +- `unchecked_shl.rs` is already wired through the same harness set. After the + unsigned replays reached `unchecked_shl_u64`, the next bounded sibling was + `unchecked_shl_u128`, which now also passes. The next bounded sibling is now + `unchecked_shl_i8`. +- `unchecked_shr.rs` is a single-file harness with ten wrappers and no smaller + split points; the smallest callable subcase is `unchecked_shr_u8` at lines + 16-21, so there is no narrower diagnostic target inside the harness itself. +- The branch now has sixteen passing direct proof slices: + `unchecked_add_u8`, `unchecked_neg_i8`, `unchecked_sub_u8`, + `wrapping_shl_u8`, `wrapping_shr_u8`, `widening_mul_u8`, + `carrying_mul_u8`, `unchecked_mul_u8`, `unchecked_mul_u16`, + `unchecked_mul_u32`, `unchecked_mul_u64`, `unchecked_shl_u8`, + `unchecked_shl_u16`, `unchecked_shl_u32`, `unchecked_shl_u64`, and + `unchecked_shl_u128`. This confirms that the carrying-mul Part 2 slice, the + unsigned unchecked-mul slices, and all published unsigned `unchecked_shl` + widths execute cleanly on this branch with the already-ported support. +- `uv --project kmir run -- kmir show unchecked_shl.unchecked_shl_u128 --proof-dir /tmp/kmir-0011-unchecked-shl-u128 --statistics --leaves` + reaches terminal `#EndProgram ~> .K` on both split paths. The observed + branches are on `core::num::::checked_shl`, with constraints + `notBool ARG_UINT2:Int =Int 0`. +- The refreshed evaluator result stays at `IN PROGRESS` with score `2.98 / 3`, + so the branch still needs more non-float breadth before any terminal state + can be justified. + +## Planning decisions + +- Treat the integer portion and float portion as separate evidence-bearing slices. +- `widening_mul_u8` was the correct delegated slice: it was the cheapest + remaining safe-API case, broadened Part 2 beyond the existing wrapping-shift + pair, and re-used the already-ported unsigned multiplication support without + introducing float work. +- `carrying_mul_u8` was the correct delegated slice: it is the remaining + safe-API family in Part 2, and the branch-local harness already exposes the + `carrying_mul` runner. +- `unchecked_mul_u8` is the next best slice: it stays on the already-covered + `u8` width, reuses the multiplication support proven by `widening_mul_u8` + and `carrying_mul_u8`, and advances the core unsafe-method matrix more + directly than widening scope to a new safe-API width. +- `unchecked_shl_u128` was the correct bounded follow-up: it completed the + unsigned `unchecked_shl` widths without widening to a new family or + entangling the parked `unchecked_shr` frontier. +- The next bounded move is now `unchecked_shl_i8`, which extends the same + family into signed widths while keeping the float blocker isolated. + +## Reusable rubric patterns for evaluator + +- Successful evaluation must tie every published requirement to a concrete artifact or an explicit blocker. +- A float-specific blocker should mention the exact missing capability, not just "floats are hard." +- Terminal classification should distinguish `CONDITIONALLY READY` from `BLOCKED` based on whether the remaining gap is narrow and external versus structural and unimplemented. +- A new passing proof in an additional safe-API slice is the strongest low-cost signal that the branch is moving beyond bootstrap evidence without consuming float-blocker budget. + +## Failed-attempt log + +- 2026-04-10: Latest branch-local attempt started + `timeout 900s uv --project kmir run -- kmir prove-rs kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_shl.rs --start-symbol unchecked_shl_u16 --terminate-on-thunk --proof-dir /tmp/kmir-0011-unchecked-shl-u16 --reload --fail-fast --max-workers 1`, but the run exited with status `143` before any terminal proof result was captured. No new frontier was established, and no code changes were kept. +- 2026-04-10: Latest branch-local attempt started + `timeout 900s uv --project kmir run -- kmir prove-rs kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_shr.rs --start-symbol unchecked_shr_u8 --terminate-on-thunk --proof-dir /tmp/kmir-0011-unchecked-shr-u8 --reload --fail-fast --max-workers 1`, but the run was interrupted before any terminal proof result was captured. No new frontier was established, and no code changes were kept. +- 2026-04-09: First filtered run used + `-k '0011-floats-ints and unchecked_add'` and matched zero cases in pytest + parametrization (`no tests ran`, exit 5). +- 2026-04-09: Second filtered run used + `-k 'unchecked_add and not fail'`; the test case started but did not complete + in a bounded runtime window and was terminated (exit 143). +- 2026-04-09: Direct proof follow-up run completed with + `ProofStatus.PASSED` for `unchecked_add_u8` using: + `timeout 900s uv --project kmir run -- kmir prove-rs kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_add.rs --start-symbol unchecked_add_u8 --terminate-on-thunk --proof-dir /tmp/kmir-0011-unchecked-add-u8 --reload --fail-fast --max-workers 1`. +- 2026-04-09: Follow-up 2 run completed with `ProofStatus.PASSED` for + `unchecked_neg_i8` using: + `timeout 900s uv --project kmir run -- kmir prove-rs kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_neg.rs --start-symbol unchecked_neg_i8 --terminate-on-thunk --proof-dir /tmp/kmir-0011-unchecked-neg-i8 --reload --fail-fast --max-workers 1`. +- 2026-04-09: Scoped discovery check for the next Part 2 slice collected + exactly `test_verify_rust_std[wrapping_shl]` using: + `uv --project kmir run -- pytest kmir/src/tests/integration/test_integration.py::test_verify_rust_std --collect-only -k "wrapping_shl and not fail" -q`. +- 2026-04-09: Direct proof follow-up run completed with + `ProofStatus.PASSED` for `wrapping_shl_u8` using: + `timeout 900s uv --project kmir run -- kmir prove-rs kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/wrapping_shl.rs --start-symbol wrapping_shl_u8 --terminate-on-thunk --proof-dir /tmp/kmir-0011-wrapping-shl-u8 --reload --fail-fast --max-workers 1`. +- 2026-04-09: Scoped discovery check for the delegated Part 1 slice collected + exactly `test_verify_rust_std[unchecked_sub]` using: + `uv --project kmir run -- pytest kmir/src/tests/integration/test_integration.py::test_verify_rust_std --collect-only -k "unchecked_sub and not fail" -q`. +- 2026-04-09: Direct proof follow-up run completed with + `ProofStatus.PASSED` for `unchecked_sub_u8` using: + `timeout 900s uv --project kmir run -- kmir prove-rs kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_sub.rs --start-symbol unchecked_sub_u8 --terminate-on-thunk --proof-dir /tmp/kmir-0011-unchecked-sub-u8 --reload --fail-fast --max-workers 1`. +- 2026-04-09: Scoped discovery check for the planner-selected Part 2 follow-up + collected exactly `test_verify_rust_std[wrapping_shr]` using: + `uv --project kmir run -- pytest kmir/src/tests/integration/test_integration.py::test_verify_rust_std --collect-only -k "wrapping_shr and not fail" -q`. +- 2026-04-09: Direct proof follow-up run completed with + `ProofStatus.PASSED` for `wrapping_shr_u8` using: + `timeout 900s uv --project kmir run -- kmir prove-rs kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/wrapping_shr.rs --start-symbol wrapping_shr_u8 --terminate-on-thunk --proof-dir /tmp/kmir-0011-wrapping-shr-u8 --reload --fail-fast --max-workers 1`. +- 2026-04-09: Scoped discovery check for the planner-selected widening-mul + follow-up collected exactly `test_verify_rust_std[widening_mul]` using: + `uv --project kmir run -- pytest kmir/src/tests/integration/test_integration.py::test_verify_rust_std --collect-only -k "widening_mul and not fail" -q`. +- 2026-04-09: Direct proof follow-up run completed with + `ProofStatus.PASSED` for `widening_mul_u8` using: + `timeout 900s uv --project kmir run -- kmir prove-rs kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/widening_mul.rs --start-symbol widening_mul_u8 --terminate-on-thunk --proof-dir /tmp/kmir-0011-widening-mul-u8 --reload --fail-fast --max-workers 1`. +- 2026-04-09: Scoped discovery check for the next Part 2 slice collected + exactly `test_verify_rust_std[carrying_mul]` using: + `uv --project kmir run -- pytest kmir/src/tests/integration/test_integration.py::test_verify_rust_std --collect-only -k "carrying_mul and not fail" -q`. +- 2026-04-09: Direct proof follow-up run completed with + `ProofStatus.PASSED` for `carrying_mul_u8` using: + `timeout 900s uv --project kmir run -- kmir prove-rs kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/carrying_mul.rs --start-symbol carrying_mul_u8 --terminate-on-thunk --proof-dir /tmp/kmir-0011-carrying-mul-u8 --reload --fail-fast --max-workers 1`. +- 2026-04-09: Scoped discovery check for the delegated unchecked-mul slice + collected exactly `test_verify_rust_std[unchecked_mul]` using: + `uv --project kmir run -- pytest kmir/src/tests/integration/test_integration.py::test_verify_rust_std --collect-only -k "unchecked_mul and not fail" -q`. +- 2026-04-09: Direct proof follow-up run completed with + `ProofStatus.PASSED` for `unchecked_mul_u8` using: + `timeout 900s uv --project kmir run -- kmir prove-rs kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_mul.rs --start-symbol unchecked_mul_u8 --terminate-on-thunk --proof-dir /tmp/kmir-0011-unchecked-mul-u8 --reload --fail-fast --max-workers 1`. + +## Generator retry execution log + +- Ported historical Challenge 0011 files from + `origin/verify-rust-std/challenge-0011` into this branch for scoped paths: + challenge artifact directory, test runner entrypoint, and shift-mask lemmas. +- Added dedicated make entrypoint `test-verify-rust-std` (from historical + branch) and parameterized `test_verify_rust_std` integration coverage with + challenge start symbols and show-output handling. +- Initialized `deps/stable-mir-json` in this worktree to satisfy build/test + prerequisites. +- Confirmed scoped case discovery with collect-only: + `test_verify_rust_std[unchecked_add]` is selected by + `-k "unchecked_add and not fail"`. +- Confirmed the next safe-API case is wired through the same runner: + `test_verify_rust_std[wrapping_shl]` is selected by + `-k "wrapping_shl and not fail"`. +- Re-executed the branch-local Part 2 slice directly with `kmir prove-rs`; + `wrapping_shl_u8` passed without any new support changes, so the prior + shift-mask lemma port was already sufficient on this branch. +- Confirmed the delegated unchecked-sub case is wired through the same runner: + `test_verify_rust_std[unchecked_sub]` is selected by + `-k "unchecked_sub and not fail"`. +- Re-executed the delegated Part 1 slice directly with `kmir prove-rs`; + `unchecked_sub_u8` passed without any new support changes, broadening the + integer-side evidence while keeping the float blocker isolated. +- Confirmed the next safe-API sibling is wired through the same runner: + `test_verify_rust_std[wrapping_shr]` is selected by + `-k "wrapping_shr and not fail"`. +- Re-executed the planner-selected Part 2 follow-up directly with + `kmir prove-rs`; `wrapping_shr_u8` passed without any new support changes, + broadening the safe-API evidence while preserving the existing float blocker + boundary. +- Confirmed the next safe-API family is wired through the same runner: + `test_verify_rust_std[widening_mul]` is selected by + `-k "widening_mul and not fail"`. +- Re-executed the planner-selected widening-mul slice directly with + `kmir prove-rs`; `widening_mul_u8` passed without any new support changes, + broadening the safe-API evidence beyond the wrapping-shift pair while + preserving the existing float blocker boundary. +- Re-executed the planner-selected carrying-mul slice directly with + `kmir prove-rs`; `carrying_mul_u8` passed without any new support changes, + broadening the safe-API evidence beyond wrapping shifts and widening-mul + while preserving the existing float blocker boundary. +- Re-executed the next Part 1 multiplication slice directly with + `kmir prove-rs`; `unchecked_mul_u64` passed without any new support changes, + widening the integer evidence one step further while preserving the existing + float blocker boundary. +- Re-executed the next unchecked-shl slice directly with `kmir prove-rs`; + `unchecked_shl_u16` passed without any new support changes, and the replay + in `/tmp/kmir-0011-unchecked-shl-u16` reached terminal + `#EndProgram ~> .K` on both split paths with branches on + `core::num::::checked_shl` and constraints including + `notBool ARG_UINT2:Int =Int 0`. + +## Evidence for next evaluator step + +- Technical port commit exists: `2e09185c`. +- Challenge 0011 artifact set now exists under + `kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints`. +- Validation now includes branch-local passing proof evidence in two published + requirement families: + `unchecked_add_u8`, `unchecked_neg_i8`, `unchecked_sub_u8`, + `unchecked_mul_u8`, `unchecked_mul_u16`, `unchecked_mul_u32`, + `unchecked_mul_u64`, `unchecked_shl_u8`, `unchecked_shl_u16`, + `unchecked_shl_u32`, `unchecked_shl_u64`, and `unchecked_shl_u128` pass in + Part 1, and + `wrapping_shl_u8`, `wrapping_shr_u8`, `widening_mul_u8`, plus + `carrying_mul_u8` pass in Part 2. +- Float blocker signal remains present in ported evidence: + `to_int_unchecked-fail` expected outputs include stuck float intrinsic hooks. + +## Next handoff + +- Challenge 0011 is closed on this branch. Do not schedule new generator or + evaluator work here unless the user explicitly reopens it. +- Any future comparison work should happen against PR `#985`, not by extending + this re-execution branch. + +- The planner-selected `carrying_mul_u8` slice is complete and passed. +- The planner-selected `unchecked_mul_u8` slice is complete and passed. +- The planner-selected `unchecked_mul_u16` slice is complete and passed. +- The planner-selected `unchecked_mul_u32` slice is complete and passed. +- The planner-selected `unchecked_mul_u64` slice is complete and passed. +- The planner-selected `unchecked_shl_u8` slice is complete and passed. +- The planner-selected `unchecked_shl_u16` slice is complete and passed. +- The planner-selected `unchecked_shl_u32` slice is complete and passed. +- The planner-selected `unchecked_shl_u64` slice is complete and passed. +- The planner-selected `unchecked_shl_u128` slice is complete and passed. +- The new success-criteria artifact should be treated as the authoritative + coverage map for future evaluator and generator handoffs. +- Evaluator should reassess whether the branch’s sixteen direct proof passes + across Part 1 and Part 2 materially change the non-float readiness signal, + while keeping the remaining float blocker tied to the precise + `fabsf32` / `fabsf64` frontier. +- If the planner delegates another generator slice after that reassessment, it + should choose a new explicit non-float target rather than revisiting the + now-completed `unchecked_shl_u128` slice. +- Exact next technical step from this checkpoint: run `unchecked_shl_i8`. + Keep `unchecked_shr` parked; its diagnostics did not produce a branch-worthy + frontier change, so do not queue another `unchecked_shr` proof run unless a + new bound or a new observation is introduced. + +## Evaluator Note + +- 2026-04-09: `wrapping_shl_u8` is strong evidence, but the remaining + unverified integer and safe-API surface is still broad; `unchecked_sub_u8` + improves the Part 1 evidence, but the strongest justified verdict remains + `IN PROGRESS` rather than `CONDITIONALLY READY`. +- 2026-04-09: After the `unchecked_sub_u8` pass, the evaluator score is now + `2.8 / 3`; the breadth gap is still the limiting factor, and the float + blocker remains the precise `fabsf32` / `fabsf64` frontier in + `to_int_unchecked`. +- 2026-04-09: After the `wrapping_shr_u8` pass, the strongest updated evaluator + question is whether the non-float evidence is now broad enough to move past + `IN PROGRESS`; the remaining technical blocker is still the precise + `fabsf32` / `fabsf64` float frontier in `to_int_unchecked`, not a new Part 2 + regression. +- 2026-04-09: Re-evaluation after `wrapping_shr_u8` keeps the verdict at + `IN PROGRESS`; the branch is stronger, but the remaining integer and safe-API + matrix is still broad enough that `CONDITIONALLY READY` would overstate the + present evidence. +- 2026-04-09: After the `unchecked_mul_u16` pass, the branch now has ten + direct proof slices and still needs broader non-float coverage before the + float blocker can be treated as the only remaining gap. +- 2026-04-10: Interrupted `kmir prove-rs` attempt started for + `unchecked_shr_u8` using: + `timeout 900s uv --project kmir run -- kmir prove-rs kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_shr.rs --start-symbol unchecked_shr_u8 --terminate-on-thunk --proof-dir /tmp/kmir-0011-unchecked-shr-u8 --reload --fail-fast --max-workers 1`; + no terminal proof result was captured before interruption, no new frontier + was established, and no code changes were kept. +- 2026-04-10: Direct proof follow-up run completed with + `ProofStatus.PASSED` for `unchecked_shl_u8` using: + `timeout 900s uv --project kmir run -- kmir prove-rs kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_shl.rs --start-symbol unchecked_shl_u8 --terminate-on-thunk --proof-dir /tmp/kmir-0011-unchecked-shl-u8 --reload --fail-fast --max-workers 1`. + The summary reported `nodes: 7`, `pending: 0`, `failing: 0`, `stuck: 0`, + `terminal: 3`. +- 2026-04-10: Direct proof replay completed with `ProofStatus.PASSED` for + `unchecked_shl_u16` using: + `timeout 900s uv --project kmir run -- kmir prove-rs kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_shl.rs --start-symbol unchecked_shl_u16 --terminate-on-thunk --proof-dir /tmp/kmir-0011-unchecked-shl-u16 --reload --fail-fast --max-workers 1`. + The replay in `/tmp/kmir-0011-unchecked-shl-u16` reached terminal + `#EndProgram ~> .K` on both split paths. Branches were observed on + `core::num::::checked_shl`, with constraints including + `notBool ARG_UINT2:Int =Int 0`. +- 2026-04-10: Direct proof replay completed with `ProofStatus.PASSED` for + `unchecked_shl_u32` using: + `uv --project kmir run -- kmir show unchecked_shl.unchecked_shl_u32 --proof-dir /tmp/kmir-0011-unchecked-shl-u32 --statistics --leaves`. + The replay in `/tmp/kmir-0011-unchecked-shl-u32` reached terminal + `#EndProgram ~> .K` on both split paths. Branches were observed on + `core::num::::checked_shl`, with constraints including + `notBool ARG_UINT2:Int =Int 0`. +- 2026-04-10: Scoped discovery check for the next `unchecked_shl` sibling + collected exactly `test_verify_rust_std[unchecked_shl]` using: + `uv --project kmir run -- pytest kmir/src/tests/integration/test_integration.py::test_verify_rust_std --collect-only -k "unchecked_shl and not fail" -q`. + The target is still present in collection, so this family is now checkpointed + through `unchecked_shl_u32`. +- 2026-04-10: Direct proof replay completed with `ProofStatus.PASSED` for + `unchecked_shl_u128` using: + `timeout 900s uv --project kmir run -- kmir prove-rs kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_shl.rs --start-symbol unchecked_shl_u128 --terminate-on-thunk --proof-dir /tmp/kmir-0011-unchecked-shl-u128 --reload --fail-fast --max-workers 1`. + The summary reported `nodes: 7`, `pending: 0`, `failing: 0`, `stuck: 0`, + `terminal: 3`. The replay in `/tmp/kmir-0011-unchecked-shl-u128` reached + terminal `#EndProgram ~> .K` on both split paths. Branches were observed on + `core::num::::checked_shl`, with constraints including + `notBool ARG_UINT2:Int =Int 0`. +- 2026-04-10: Scoped discovery check for `unchecked_shr` collected exactly + `test_verify_rust_std[unchecked_shr]` using: + `uv --project kmir run -- pytest kmir/src/tests/integration/test_integration.py::test_verify_rust_std --collect-only -k "unchecked_shr and not fail" -q`. + The family is still present in collection. +- 2026-04-10: Diagnostic pass over `unchecked_shr.rs` and the matching + `show/unchecked_shr-fail.*.expected` files showed that the harness already + bottoms out at `unchecked_shr_u8`; the other widths are only width variants + of the same `binOpShrUnchecked` frontier. The smallest observed frontier is + the `unchecked_shr_u8` expected state, which reaches + `#applyBinOp ( binOpShrUnchecked , Integer ( ARG_UINT1:Int , 8 , false ) , + Integer ... ) ~> #freezer` with the `ARG_UINT2:Int >=Int 0` constraint. + No narrower branch-worthy subcase was found, so another proof run is not + justified from this checkpoint alone. diff --git a/kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md b/kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md index 525e311a0..121ad10f3 100644 --- a/kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md +++ b/kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md @@ -163,6 +163,17 @@ power of two but the semantics will always operate with these particular ones. rule VAL &Int bitmask128 => VAL requires 0 <=Int VAL andBool VAL <=Int bitmask128 [simplification, preserves-definedness, smt-lemma] ``` +Shift operations like `wrapping_shl` mask the shift amount with `BITS - 1` (e.g., `rhs & 7` for `u8`). +When the shift amount is already known to be less than `BITS`, the mask is a no-op. + +```k + rule VAL &Int 7 => VAL requires 0 <=Int VAL andBool VAL VAL requires 0 <=Int VAL andBool VAL VAL requires 0 <=Int VAL andBool VAL VAL requires 0 <=Int VAL andBool VAL VAL requires 0 <=Int VAL andBool VAL > u8::BITS) as u8)); +} + +fn carrying_mul_u16(a: u16, b: u16, c: u16) { + let (lo, hi) = a.carrying_mul(b, c); + let expected = (a as u32) * (b as u32) + (c as u32); + assert!(lo == (expected as u16)); + assert!(hi == ((expected >> u16::BITS) as u16)); +} + +fn carrying_mul_u32(a: u32, b: u32, c: u32) { + let (lo, hi) = a.carrying_mul(b, c); + let expected = (a as u64) * (b as u64) + (c as u64); + assert!(lo == (expected as u32)); + assert!(hi == ((expected >> u32::BITS) as u32)); +} + +fn carrying_mul_u64(a: u64, b: u64, c: u64) { + let (lo, hi) = a.carrying_mul(b, c); + let expected = (a as u128) * (b as u128) + (c as u128); + assert!(lo == (expected as u64)); + assert!(hi == ((expected >> u64::BITS) as u64)); +} diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/to_int_unchecked-fail.to_int_unchecked_f128_i128.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/to_int_unchecked-fail.to_int_unchecked_f128_i128.expected new file mode 100644 index 000000000..b98f22762 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/to_int_unchecked-fail.to_int_unchecked_f128_i128.expected @@ -0,0 +1,38 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (31 steps) +├─ 3 +│ #cast ( #adjustRef ( ARG1:Value , 2 ) , castKindTransmute , ty ( 38 ) , ty ( 39 +│ span: 32 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( #littleEndianFromBytes ( ELEMS:List ) &Int 340282366920938463463374607 +┃ │ span: 32 +┃ │ +┃ │ (29 steps) +┃ ├─ 6 +┃ │ #cast ( Integer ( #littleEndianFromBytes ( ELEMS:List ) &Int 3402823669209384634 +┃ │ span: 115 +┃ │ +┃ │ (1 step) +┃ └─ 7 (leaf, terminal) +┃ thunk ( #cast ( Integer ( #littleEndianFromBytes ( ELEMS:List ) &Int 34028236692 +┃ span: 115 +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #cast ( #adjustRef ( ARG1:Value , 2 ) , castKindTransmute , ty ( 38 ) , + span: 32 + + +┌─ 2 (root, leaf, target, terminal) +│ #EndProgram ~> .K + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/to_int_unchecked-fail.to_int_unchecked_f16_i8.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/to_int_unchecked-fail.to_int_unchecked_f16_i8.expected new file mode 100644 index 000000000..dbf6a9636 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/to_int_unchecked-fail.to_int_unchecked_f16_i8.expected @@ -0,0 +1,39 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (31 steps) +├─ 3 +│ #cast ( #adjustRef ( ARG1:Value , 2 ) , castKindTransmute , ty ( 22 ) , ty ( 23 +│ span: 32 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( #littleEndianFromBytes ( ELEMS:List ) &Int 65535 , 16 , false ) +~> #fr +┃ │ span: 32 +┃ │ +┃ │ (29 steps) +┃ ├─ 6 +┃ │ #cast ( Integer ( #littleEndianFromBytes ( ELEMS:List ) &Int 65535 &Int 32767 , +┃ │ span: 56 +┃ │ +┃ │ (1 step) +┃ └─ 7 (leaf, terminal) +┃ thunk ( #cast ( Integer ( #littleEndianFromBytes ( ELEMS:List ) &Int 65535 &Int +┃ span: 56 +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #cast ( #adjustRef ( ARG1:Value , 2 ) , castKindTransmute , ty ( 22 ) , + span: 32 + + +┌─ 2 (root, leaf, target, terminal) +│ #EndProgram ~> .K + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/to_int_unchecked-fail.to_int_unchecked_f32_i32.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/to_int_unchecked-fail.to_int_unchecked_f32_i32.expected new file mode 100644 index 000000000..4ec73a403 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/to_int_unchecked-fail.to_int_unchecked_f32_i32.expected @@ -0,0 +1,15 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (22 steps) +└─ 3 (stuck, leaf) + #execIntrinsic ( IntrinsicFunction ( symbol ( "fabsf32" ) ) , operandMove ( plac + span: 73 + + +┌─ 2 (root, leaf, target, terminal) +│ #EndProgram ~> .K + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/to_int_unchecked-fail.to_int_unchecked_f64_i64.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/to_int_unchecked-fail.to_int_unchecked_f64_i64.expected new file mode 100644 index 000000000..39571fec2 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/to_int_unchecked-fail.to_int_unchecked_f64_i64.expected @@ -0,0 +1,15 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (22 steps) +└─ 3 (stuck, leaf) + #execIntrinsic ( IntrinsicFunction ( symbol ( "fabsf64" ) ) , operandMove ( plac + span: 90 + + +┌─ 2 (root, leaf, target, terminal) +│ #EndProgram ~> .K + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_i128.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_i128.expected new file mode 100644 index 000000000..8ebaab361 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_i128.expected @@ -0,0 +1,34 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpAddUnchecked , Integer ( ARG_INT1:Int , 128 , true ) , Intege +│ span: 301 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( ARG_INT1:Int +Int ARG_INT2:Int , 128 , Signed ) , 128 , tru +┃ │ span: 301 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpAddUnchecked , Integer ( ARG_INT1:Int , 128 , true ) + span: 301 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_i16.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_i16.expected new file mode 100644 index 000000000..469e3ebff --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_i16.expected @@ -0,0 +1,34 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpAddUnchecked , Integer ( ARG_INT1:Int , 16 , true ) , Integer +│ span: 115 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( ARG_INT1:Int +Int ARG_INT2:Int , 16 , Signed ) , 16 , true +┃ │ span: 115 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpAddUnchecked , Integer ( ARG_INT1:Int , 16 , true ) , + span: 115 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_i32.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_i32.expected new file mode 100644 index 000000000..c23b7ba5e --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_i32.expected @@ -0,0 +1,34 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpAddUnchecked , Integer ( ARG_INT1:Int , 32 , true ) , Integer +│ span: 146 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( ARG_INT1:Int +Int ARG_INT2:Int , 32 , Signed ) , 32 , true +┃ │ span: 146 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpAddUnchecked , Integer ( ARG_INT1:Int , 32 , true ) , + span: 146 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_i64.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_i64.expected new file mode 100644 index 000000000..57dd3469d --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_i64.expected @@ -0,0 +1,34 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpAddUnchecked , Integer ( ARG_INT1:Int , 64 , true ) , Integer +│ span: 177 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( ARG_INT1:Int +Int ARG_INT2:Int , 64 , Signed ) , 64 , true +┃ │ span: 177 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpAddUnchecked , Integer ( ARG_INT1:Int , 64 , true ) , + span: 177 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_i8.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_i8.expected new file mode 100644 index 000000000..16b2aeed4 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_i8.expected @@ -0,0 +1,34 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpAddUnchecked , Integer ( ARG_INT1:Int , 8 , true ) , Integer +│ span: 53 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( ARG_INT1:Int +Int ARG_INT2:Int , 8 , Signed ) , 8 , true ) +┃ │ span: 53 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpAddUnchecked , Integer ( ARG_INT1:Int , 8 , true ) , + span: 53 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_u128.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_u128.expected new file mode 100644 index 000000000..40d83226c --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_u128.expected @@ -0,0 +1,34 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpAddUnchecked , Integer ( ARG_UINT1:Int , 128 , false ) , Inte +│ span: 332 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( ARG_UINT1:Int +Int ARG_UINT2:Int &Int 34028236692093846346337460743176 +┃ │ span: 332 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpAddUnchecked , Integer ( ARG_UINT1:Int , 128 , false + span: 332 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_u16.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_u16.expected new file mode 100644 index 000000000..97948e0a6 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_u16.expected @@ -0,0 +1,35 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpAddUnchecked , Integer ( ARG_UINT1:Int , 16 , false ) , Integ +│ span: 208 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( ARG_UINT1:Int +Int ARG_UINT2:Int &Int 65535 , 16 , false ) +~> #freezer +┃ │ span: 208 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpAddUnchecked , Integer ( ARG_UINT1:Int , 16 , false ) + span: 208 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_u32.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_u32.expected new file mode 100644 index 000000000..1680f4224 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_u32.expected @@ -0,0 +1,35 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpAddUnchecked , Integer ( ARG_UINT1:Int , 32 , false ) , Integ +│ span: 239 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( ARG_UINT1:Int +Int ARG_UINT2:Int &Int 4294967295 , 32 , false ) +~> #fr +┃ │ span: 239 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpAddUnchecked , Integer ( ARG_UINT1:Int , 32 , false ) + span: 239 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_u64.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_u64.expected new file mode 100644 index 000000000..412ad1c08 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_u64.expected @@ -0,0 +1,34 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpAddUnchecked , Integer ( ARG_UINT1:Int , 64 , false ) , Integ +│ span: 270 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( ARG_UINT1:Int +Int ARG_UINT2:Int &Int 18446744073709551615 , 64 , fals +┃ │ span: 270 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpAddUnchecked , Integer ( ARG_UINT1:Int , 64 , false ) + span: 270 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_u8.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_u8.expected new file mode 100644 index 000000000..bd0e55614 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_add-fail.unchecked_add_u8.expected @@ -0,0 +1,35 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpAddUnchecked , Integer ( ARG_UINT1:Int , 8 , false ) , Intege +│ span: 84 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( ARG_UINT1:Int +Int ARG_UINT2:Int &Int 255 , 8 , false ) +~> #freezer#se +┃ │ span: 84 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpAddUnchecked , Integer ( ARG_UINT1:Int , 8 , false ) + span: 84 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_i128.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_i128.expected new file mode 100644 index 000000000..257c4d3c5 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_i128.expected @@ -0,0 +1,34 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpMulUnchecked , Integer ( ARG_INT1:Int , 128 , true ) , Intege +│ span: 301 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( ARG_INT1:Int *Int ARG_INT2:Int , 128 , Signed ) , 128 , tru +┃ │ span: 301 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpMulUnchecked , Integer ( ARG_INT1:Int , 128 , true ) + span: 301 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_i16.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_i16.expected new file mode 100644 index 000000000..ac5d7b039 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_i16.expected @@ -0,0 +1,34 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpMulUnchecked , Integer ( ARG_INT1:Int , 16 , true ) , Integer +│ span: 115 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( ARG_INT1:Int *Int ARG_INT2:Int , 16 , Signed ) , 16 , true +┃ │ span: 115 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpMulUnchecked , Integer ( ARG_INT1:Int , 16 , true ) , + span: 115 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_i32.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_i32.expected new file mode 100644 index 000000000..fd2162753 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_i32.expected @@ -0,0 +1,34 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpMulUnchecked , Integer ( ARG_INT1:Int , 32 , true ) , Integer +│ span: 146 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( ARG_INT1:Int *Int ARG_INT2:Int , 32 , Signed ) , 32 , true +┃ │ span: 146 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpMulUnchecked , Integer ( ARG_INT1:Int , 32 , true ) , + span: 146 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_i64.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_i64.expected new file mode 100644 index 000000000..f8395cba5 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_i64.expected @@ -0,0 +1,34 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpMulUnchecked , Integer ( ARG_INT1:Int , 64 , true ) , Integer +│ span: 177 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( ARG_INT1:Int *Int ARG_INT2:Int , 64 , Signed ) , 64 , true +┃ │ span: 177 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpMulUnchecked , Integer ( ARG_INT1:Int , 64 , true ) , + span: 177 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_i8.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_i8.expected new file mode 100644 index 000000000..516befead --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_i8.expected @@ -0,0 +1,34 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpMulUnchecked , Integer ( ARG_INT1:Int , 8 , true ) , Integer +│ span: 53 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( ARG_INT1:Int *Int ARG_INT2:Int , 8 , Signed ) , 8 , true ) +┃ │ span: 53 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpMulUnchecked , Integer ( ARG_INT1:Int , 8 , true ) , + span: 53 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_u128.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_u128.expected new file mode 100644 index 000000000..7bc83384a --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_u128.expected @@ -0,0 +1,34 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpMulUnchecked , Integer ( ARG_UINT1:Int , 128 , false ) , Inte +│ span: 332 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( ARG_UINT1:Int *Int ARG_UINT2:Int &Int 34028236692093846346337460743176 +┃ │ span: 332 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpMulUnchecked , Integer ( ARG_UINT1:Int , 128 , false + span: 332 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_u16.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_u16.expected new file mode 100644 index 000000000..9c8b8fa13 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_u16.expected @@ -0,0 +1,35 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpMulUnchecked , Integer ( ARG_UINT1:Int , 16 , false ) , Integ +│ span: 208 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( ARG_UINT1:Int *Int ARG_UINT2:Int &Int 65535 , 16 , false ) +~> #freezer +┃ │ span: 208 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpMulUnchecked , Integer ( ARG_UINT1:Int , 16 , false ) + span: 208 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_u32.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_u32.expected new file mode 100644 index 000000000..f7153e5f8 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_u32.expected @@ -0,0 +1,35 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpMulUnchecked , Integer ( ARG_UINT1:Int , 32 , false ) , Integ +│ span: 239 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( ARG_UINT1:Int *Int ARG_UINT2:Int &Int 4294967295 , 32 , false ) +~> #fr +┃ │ span: 239 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpMulUnchecked , Integer ( ARG_UINT1:Int , 32 , false ) + span: 239 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_u64.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_u64.expected new file mode 100644 index 000000000..8542f300a --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_u64.expected @@ -0,0 +1,34 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpMulUnchecked , Integer ( ARG_UINT1:Int , 64 , false ) , Integ +│ span: 270 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( ARG_UINT1:Int *Int ARG_UINT2:Int &Int 18446744073709551615 , 64 , fals +┃ │ span: 270 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpMulUnchecked , Integer ( ARG_UINT1:Int , 64 , false ) + span: 270 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_u8.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_u8.expected new file mode 100644 index 000000000..6519b70b7 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_mul-fail.unchecked_mul_u8.expected @@ -0,0 +1,35 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpMulUnchecked , Integer ( ARG_UINT1:Int , 8 , false ) , Intege +│ span: 84 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( ARG_UINT1:Int *Int ARG_UINT2:Int &Int 255 , 8 , false ) +~> #freezer#se +┃ │ span: 84 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpMulUnchecked , Integer ( ARG_UINT1:Int , 8 , false ) + span: 84 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_neg-fail.unchecked_neg_i128.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_neg-fail.unchecked_neg_i128.expected new file mode 100644 index 000000000..fd29da216 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_neg-fail.unchecked_neg_i128.expected @@ -0,0 +1,35 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (50 steps) +├─ 3 +│ #applyBinOp ( binOpSubUnchecked , Integer ( 0 , 128 , true ) , Integer ( ARG_INT +│ span: 178 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( 0 -Int ARG_INT1:Int , 128 , Signed ) , 128 , true ) +~> #fre +┃ │ span: 178 +┃ │ +┃ │ (67 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpSubUnchecked , Integer ( 0 , 128 , true ) , Integer ( + span: 178 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_neg-fail.unchecked_neg_i16.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_neg-fail.unchecked_neg_i16.expected new file mode 100644 index 000000000..72f28e18e --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_neg-fail.unchecked_neg_i16.expected @@ -0,0 +1,35 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (50 steps) +├─ 3 +│ #applyBinOp ( binOpSubUnchecked , Integer ( 0 , 16 , true ) , Integer ( ARG_INT1 +│ span: 91 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( 0 -Int ARG_INT1:Int , 16 , Signed ) , 16 , true ) +~> #freez +┃ │ span: 91 +┃ │ +┃ │ (67 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpSubUnchecked , Integer ( 0 , 16 , true ) , Integer ( + span: 91 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_neg-fail.unchecked_neg_i32.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_neg-fail.unchecked_neg_i32.expected new file mode 100644 index 000000000..1964ce895 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_neg-fail.unchecked_neg_i32.expected @@ -0,0 +1,35 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (50 steps) +├─ 3 +│ #applyBinOp ( binOpSubUnchecked , Integer ( 0 , 32 , true ) , Integer ( ARG_INT1 +│ span: 120 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( 0 -Int ARG_INT1:Int , 32 , Signed ) , 32 , true ) +~> #freez +┃ │ span: 120 +┃ │ +┃ │ (67 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpSubUnchecked , Integer ( 0 , 32 , true ) , Integer ( + span: 120 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_neg-fail.unchecked_neg_i64.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_neg-fail.unchecked_neg_i64.expected new file mode 100644 index 000000000..bd1cbbe06 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_neg-fail.unchecked_neg_i64.expected @@ -0,0 +1,35 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (50 steps) +├─ 3 +│ #applyBinOp ( binOpSubUnchecked , Integer ( 0 , 64 , true ) , Integer ( ARG_INT1 +│ span: 149 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( 0 -Int ARG_INT1:Int , 64 , Signed ) , 64 , true ) +~> #freez +┃ │ span: 149 +┃ │ +┃ │ (67 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpSubUnchecked , Integer ( 0 , 64 , true ) , Integer ( + span: 149 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_neg-fail.unchecked_neg_i8.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_neg-fail.unchecked_neg_i8.expected new file mode 100644 index 000000000..c15a88519 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_neg-fail.unchecked_neg_i8.expected @@ -0,0 +1,35 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (50 steps) +├─ 3 +│ #applyBinOp ( binOpSubUnchecked , Integer ( 0 , 8 , true ) , Integer ( ARG_INT1: +│ span: 58 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( 0 -Int ARG_INT1:Int , 8 , Signed ) , 8 , true ) +~> #freezer +┃ │ span: 58 +┃ │ +┃ │ (67 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpSubUnchecked , Integer ( 0 , 8 , true ) , Integer ( A + span: 58 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_i128.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_i128.expected new file mode 100644 index 000000000..57eaa182d --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_i128.expected @@ -0,0 +1,35 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpShlUnchecked , Integer ( ARG_INT1:Int , 128 , true ) , Intege +│ span: 274 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( ARG_INT1:Int < .K +┃ │ +┃ ┊ constraint: +┃ ┊ ARG_UINT2:Int >=Int 0 +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpShlUnchecked , Integer ( ARG_INT1:Int , 128 , true ) + span: 274 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_i16.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_i16.expected new file mode 100644 index 000000000..7d5a42edc --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_i16.expected @@ -0,0 +1,35 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpShlUnchecked , Integer ( ARG_INT1:Int , 16 , true ) , Integer +│ span: 112 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( ARG_INT1:Int < .K +┃ │ +┃ ┊ constraint: +┃ ┊ ARG_UINT2:Int >=Int 0 +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpShlUnchecked , Integer ( ARG_INT1:Int , 16 , true ) , + span: 112 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_i32.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_i32.expected new file mode 100644 index 000000000..052ceb2ce --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_i32.expected @@ -0,0 +1,35 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpShlUnchecked , Integer ( ARG_INT1:Int , 32 , true ) , Integer +│ span: 139 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( ARG_INT1:Int < .K +┃ │ +┃ ┊ constraint: +┃ ┊ ARG_UINT2:Int >=Int 0 +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpShlUnchecked , Integer ( ARG_INT1:Int , 32 , true ) , + span: 139 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_i64.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_i64.expected new file mode 100644 index 000000000..d2eb45316 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_i64.expected @@ -0,0 +1,35 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpShlUnchecked , Integer ( ARG_INT1:Int , 64 , true ) , Integer +│ span: 166 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( ARG_INT1:Int < .K +┃ │ +┃ ┊ constraint: +┃ ┊ ARG_UINT2:Int >=Int 0 +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpShlUnchecked , Integer ( ARG_INT1:Int , 64 , true ) , + span: 166 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_i8.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_i8.expected new file mode 100644 index 000000000..d62c1b8b2 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_i8.expected @@ -0,0 +1,35 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpShlUnchecked , Integer ( ARG_INT1:Int , 8 , true ) , Integer +│ span: 58 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( ARG_INT1:Int < .K +┃ │ +┃ ┊ constraint: +┃ ┊ ARG_UINT2:Int >=Int 0 +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpShlUnchecked , Integer ( ARG_INT1:Int , 8 , true ) , + span: 58 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_u128.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_u128.expected new file mode 100644 index 000000000..29fbeb3d1 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_u128.expected @@ -0,0 +1,35 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpShlUnchecked , Integer ( ARG_UINT1:Int , 128 , false ) , Inte +│ span: 301 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( ARG_UINT1:Int < .K +┃ │ +┃ ┊ constraint: +┃ ┊ ARG_UINT2:Int >=Int 0 +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpShlUnchecked , Integer ( ARG_UINT1:Int , 128 , false + span: 301 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_u16.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_u16.expected new file mode 100644 index 000000000..f188b583b --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_u16.expected @@ -0,0 +1,36 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpShlUnchecked , Integer ( ARG_UINT1:Int , 16 , false ) , Integ +│ span: 193 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( ARG_UINT1:Int < #free +┃ │ span: 193 +┃ │ +┃ │ (110 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: +┃ ┊ ARG_UINT2:Int >=Int 0 +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpShlUnchecked , Integer ( ARG_UINT1:Int , 16 , false ) + span: 193 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_u32.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_u32.expected new file mode 100644 index 000000000..cf5f2c5dd --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_u32.expected @@ -0,0 +1,36 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpShlUnchecked , Integer ( ARG_UINT1:Int , 32 , false ) , Integ +│ span: 220 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( ARG_UINT1:Int < +┃ │ span: 220 +┃ │ +┃ │ (110 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: +┃ ┊ ARG_UINT2:Int >=Int 0 +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpShlUnchecked , Integer ( ARG_UINT1:Int , 32 , false ) + span: 220 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_u64.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_u64.expected new file mode 100644 index 000000000..6ed421f4d --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_u64.expected @@ -0,0 +1,35 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpShlUnchecked , Integer ( ARG_UINT1:Int , 64 , false ) , Integ +│ span: 247 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( ARG_UINT1:Int < .K +┃ │ +┃ ┊ constraint: +┃ ┊ ARG_UINT2:Int >=Int 0 +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpShlUnchecked , Integer ( ARG_UINT1:Int , 64 , false ) + span: 247 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_u8.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_u8.expected new file mode 100644 index 000000000..1ffb3dc3e --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shl-fail.unchecked_shl_u8.expected @@ -0,0 +1,36 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpShlUnchecked , Integer ( ARG_UINT1:Int , 8 , false ) , Intege +│ span: 85 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( ARG_UINT1:Int < #freezer +┃ │ span: 85 +┃ │ +┃ │ (110 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: +┃ ┊ ARG_UINT2:Int >=Int 0 +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpShlUnchecked , Integer ( ARG_UINT1:Int , 8 , false ) + span: 85 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_i128.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_i128.expected new file mode 100644 index 000000000..a84d5aa5b --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_i128.expected @@ -0,0 +1,35 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpShrUnchecked , Integer ( ARG_INT1:Int , 128 , true ) , Intege +│ span: 274 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( ARG_INT1:Int >>Int ARG_UINT2:Int modInt 3402823669209384634 +┃ │ span: 274 +┃ │ +┃ │ (110 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: +┃ ┊ ARG_UINT2:Int >=Int 0 +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpShrUnchecked , Integer ( ARG_INT1:Int , 128 , true ) + span: 274 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_i16.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_i16.expected new file mode 100644 index 000000000..527202efb --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_i16.expected @@ -0,0 +1,35 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpShrUnchecked , Integer ( ARG_INT1:Int , 16 , true ) , Integer +│ span: 112 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( ARG_INT1:Int >>Int ARG_UINT2:Int modInt 65536 , 16 , Signed +┃ │ span: 112 +┃ │ +┃ │ (110 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: +┃ ┊ ARG_UINT2:Int >=Int 0 +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpShrUnchecked , Integer ( ARG_INT1:Int , 16 , true ) , + span: 112 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_i32.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_i32.expected new file mode 100644 index 000000000..0128d3fa8 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_i32.expected @@ -0,0 +1,35 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpShrUnchecked , Integer ( ARG_INT1:Int , 32 , true ) , Integer +│ span: 139 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( ARG_INT1:Int >>Int ARG_UINT2:Int modInt 4294967296 , 32 , S +┃ │ span: 139 +┃ │ +┃ │ (110 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: +┃ ┊ ARG_UINT2:Int >=Int 0 +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpShrUnchecked , Integer ( ARG_INT1:Int , 32 , true ) , + span: 139 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_i64.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_i64.expected new file mode 100644 index 000000000..9e7dad859 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_i64.expected @@ -0,0 +1,35 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpShrUnchecked , Integer ( ARG_INT1:Int , 64 , true ) , Integer +│ span: 166 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( ARG_INT1:Int >>Int ARG_UINT2:Int modInt 1844674407370955161 +┃ │ span: 166 +┃ │ +┃ │ (110 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: +┃ ┊ ARG_UINT2:Int >=Int 0 +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpShrUnchecked , Integer ( ARG_INT1:Int , 64 , true ) , + span: 166 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_i8.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_i8.expected new file mode 100644 index 000000000..a71512a69 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_i8.expected @@ -0,0 +1,35 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpShrUnchecked , Integer ( ARG_INT1:Int , 8 , true ) , Integer +│ span: 58 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( ARG_INT1:Int >>Int ARG_UINT2:Int modInt 256 , 8 , Signed ) +┃ │ span: 58 +┃ │ +┃ │ (110 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: +┃ ┊ ARG_UINT2:Int >=Int 0 +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpShrUnchecked , Integer ( ARG_INT1:Int , 8 , true ) , + span: 58 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_u128.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_u128.expected new file mode 100644 index 000000000..06c1a5167 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_u128.expected @@ -0,0 +1,35 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpShrUnchecked , Integer ( ARG_UINT1:Int , 128 , false ) , Inte +│ span: 301 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( ARG_UINT1:Int >>Int ARG_UINT2:Int modInt 34028236692093846346337460743 +┃ │ span: 301 +┃ │ +┃ │ (110 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: +┃ ┊ ARG_UINT2:Int >=Int 0 +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpShrUnchecked , Integer ( ARG_UINT1:Int , 128 , false + span: 301 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_u16.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_u16.expected new file mode 100644 index 000000000..01762529e --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_u16.expected @@ -0,0 +1,36 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpShrUnchecked , Integer ( ARG_UINT1:Int , 16 , false ) , Integ +│ span: 193 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( ARG_UINT1:Int >>Int ARG_UINT2:Int modInt 65536 , 16 , false ) +~> #free +┃ │ span: 193 +┃ │ +┃ │ (110 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: +┃ ┊ ARG_UINT2:Int >=Int 0 +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpShrUnchecked , Integer ( ARG_UINT1:Int , 16 , false ) + span: 193 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_u32.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_u32.expected new file mode 100644 index 000000000..00cceb40c --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_u32.expected @@ -0,0 +1,36 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpShrUnchecked , Integer ( ARG_UINT1:Int , 32 , false ) , Integ +│ span: 220 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( ARG_UINT1:Int >>Int ARG_UINT2:Int modInt 4294967296 , 32 , false ) +~> +┃ │ span: 220 +┃ │ +┃ │ (110 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: +┃ ┊ ARG_UINT2:Int >=Int 0 +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpShrUnchecked , Integer ( ARG_UINT1:Int , 32 , false ) + span: 220 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_u64.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_u64.expected new file mode 100644 index 000000000..f700cf0d8 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_u64.expected @@ -0,0 +1,35 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpShrUnchecked , Integer ( ARG_UINT1:Int , 64 , false ) , Integ +│ span: 247 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( ARG_UINT1:Int >>Int ARG_UINT2:Int modInt 18446744073709551616 , 64 , f +┃ │ span: 247 +┃ │ +┃ │ (110 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: +┃ ┊ ARG_UINT2:Int >=Int 0 +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpShrUnchecked , Integer ( ARG_UINT1:Int , 64 , false ) + span: 247 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_u8.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_u8.expected new file mode 100644 index 000000000..9c712f1a3 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_shr-fail.unchecked_shr_u8.expected @@ -0,0 +1,36 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpShrUnchecked , Integer ( ARG_UINT1:Int , 8 , false ) , Intege +│ span: 85 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( ARG_UINT1:Int >>Int ARG_UINT2:Int modInt 256 , 8 , false ) +~> #freezer +┃ │ span: 85 +┃ │ +┃ │ (110 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: +┃ ┊ ARG_UINT2:Int >=Int 0 +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpShrUnchecked , Integer ( ARG_UINT1:Int , 8 , false ) + span: 85 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_i128.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_i128.expected new file mode 100644 index 000000000..ea78ced21 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_i128.expected @@ -0,0 +1,34 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpSubUnchecked , Integer ( ARG_INT1:Int , 128 , true ) , Intege +│ span: 301 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( ARG_INT1:Int -Int ARG_INT2:Int , 128 , Signed ) , 128 , tru +┃ │ span: 301 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpSubUnchecked , Integer ( ARG_INT1:Int , 128 , true ) + span: 301 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_i16.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_i16.expected new file mode 100644 index 000000000..743fd093c --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_i16.expected @@ -0,0 +1,34 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpSubUnchecked , Integer ( ARG_INT1:Int , 16 , true ) , Integer +│ span: 115 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( ARG_INT1:Int -Int ARG_INT2:Int , 16 , Signed ) , 16 , true +┃ │ span: 115 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpSubUnchecked , Integer ( ARG_INT1:Int , 16 , true ) , + span: 115 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_i32.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_i32.expected new file mode 100644 index 000000000..c1a06dce6 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_i32.expected @@ -0,0 +1,34 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpSubUnchecked , Integer ( ARG_INT1:Int , 32 , true ) , Integer +│ span: 146 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( ARG_INT1:Int -Int ARG_INT2:Int , 32 , Signed ) , 32 , true +┃ │ span: 146 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpSubUnchecked , Integer ( ARG_INT1:Int , 32 , true ) , + span: 146 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_i64.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_i64.expected new file mode 100644 index 000000000..b42cde312 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_i64.expected @@ -0,0 +1,34 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpSubUnchecked , Integer ( ARG_INT1:Int , 64 , true ) , Integer +│ span: 177 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( ARG_INT1:Int -Int ARG_INT2:Int , 64 , Signed ) , 64 , true +┃ │ span: 177 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpSubUnchecked , Integer ( ARG_INT1:Int , 64 , true ) , + span: 177 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_i8.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_i8.expected new file mode 100644 index 000000000..0a56f6b97 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_i8.expected @@ -0,0 +1,34 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpSubUnchecked , Integer ( ARG_INT1:Int , 8 , true ) , Integer +│ span: 53 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( truncate ( ARG_INT1:Int -Int ARG_INT2:Int , 8 , Signed ) , 8 , true ) +┃ │ span: 53 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpSubUnchecked , Integer ( ARG_INT1:Int , 8 , true ) , + span: 53 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_u128.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_u128.expected new file mode 100644 index 000000000..8588fcce4 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_u128.expected @@ -0,0 +1,34 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpSubUnchecked , Integer ( ARG_UINT1:Int , 128 , false ) , Inte +│ span: 332 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( ARG_UINT1:Int -Int ARG_UINT2:Int &Int 34028236692093846346337460743176 +┃ │ span: 332 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpSubUnchecked , Integer ( ARG_UINT1:Int , 128 , false + span: 332 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_u16.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_u16.expected new file mode 100644 index 000000000..d8ace363c --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_u16.expected @@ -0,0 +1,35 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpSubUnchecked , Integer ( ARG_UINT1:Int , 16 , false ) , Integ +│ span: 208 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( ARG_UINT1:Int -Int ARG_UINT2:Int &Int 65535 , 16 , false ) +~> #freezer +┃ │ span: 208 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpSubUnchecked , Integer ( ARG_UINT1:Int , 16 , false ) + span: 208 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_u32.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_u32.expected new file mode 100644 index 000000000..f800b206f --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_u32.expected @@ -0,0 +1,35 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpSubUnchecked , Integer ( ARG_UINT1:Int , 32 , false ) , Integ +│ span: 239 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( ARG_UINT1:Int -Int ARG_UINT2:Int &Int 4294967295 , 32 , false ) +~> #fr +┃ │ span: 239 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpSubUnchecked , Integer ( ARG_UINT1:Int , 32 , false ) + span: 239 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_u64.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_u64.expected new file mode 100644 index 000000000..c0b199507 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_u64.expected @@ -0,0 +1,34 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpSubUnchecked , Integer ( ARG_UINT1:Int , 64 , false ) , Integ +│ span: 270 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( ARG_UINT1:Int -Int ARG_UINT2:Int &Int 18446744073709551615 , 64 , fals +┃ │ span: 270 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpSubUnchecked , Integer ( ARG_UINT1:Int , 64 , false ) + span: 270 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_u8.expected b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_u8.expected new file mode 100644 index 000000000..6888f0278 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show/unchecked_sub-fail.unchecked_sub_u8.expected @@ -0,0 +1,35 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (56 steps) +├─ 3 +│ #applyBinOp ( binOpSubUnchecked , Integer ( ARG_UINT1:Int , 8 , false ) , Intege +│ span: 84 +┃ +┃ (1 step) +┣━━┓ +┃ │ +┃ ├─ 4 +┃ │ Integer ( ARG_UINT1:Int -Int ARG_UINT2:Int &Int 255 , 8 , false ) +~> #freezer#se +┃ │ span: 84 +┃ │ +┃ │ (70 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ + │ + └─ 5 (leaf, terminal) + thunk ( #applyBinOp ( binOpSubUnchecked , Integer ( ARG_UINT1:Int , 8 , false ) + span: 84 + + + diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/to_int_unchecked-fail.rs b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/to_int_unchecked-fail.rs new file mode 100644 index 000000000..9911fb291 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/to_int_unchecked-fail.rs @@ -0,0 +1,37 @@ +#![feature(f16)] +#![feature(f128)] + +fn main() { + to_int_unchecked_f16_i8(0.0); + to_int_unchecked_f32_i32(0.0); + to_int_unchecked_f64_i64(0.0); + to_int_unchecked_f128_i128(0.0); +} + +fn to_int_unchecked_f16_i8(a: f16) { + if a.is_finite() && a >= i8::MIN as f16 && a < -(i8::MIN as f16) { + let result = unsafe { a.to_int_unchecked::() }; + assert!(result == a as i8); + } +} + +fn to_int_unchecked_f32_i32(a: f32) { + if a.is_finite() && a >= i32::MIN as f32 && a < -(i32::MIN as f32) { + let result = unsafe { a.to_int_unchecked::() }; + assert!(result == a as i32); + } +} + +fn to_int_unchecked_f64_i64(a: f64) { + if a.is_finite() && a >= i64::MIN as f64 && a < -(i64::MIN as f64) { + let result = unsafe { a.to_int_unchecked::() }; + assert!(result == a as i64); + } +} + +fn to_int_unchecked_f128_i128(a: f128) { + if a.is_finite() && a >= i128::MIN as f128 && a < -(i128::MIN as f128) { + let result = unsafe { a.to_int_unchecked::() }; + assert!(result == a as i128); + } +} diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_add-fail.rs b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_add-fail.rs new file mode 100644 index 000000000..85680b316 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_add-fail.rs @@ -0,0 +1,64 @@ +#![feature(unchecked_math)] + +fn main() { + unchecked_add_u8(0, 0); + unchecked_add_u16(0, 0); + unchecked_add_u32(0, 0); + unchecked_add_u64(0, 0); + unchecked_add_u128(0, 0); + unchecked_add_i8(0, 0); + unchecked_add_i16(0, 0); + unchecked_add_i32(0, 0); + unchecked_add_i64(0, 0); + unchecked_add_i128(0, 0); +} + +fn unchecked_add_u8(a: u8, b: u8) { + let result = unsafe { a.unchecked_add(b) }; + assert!(result == a.wrapping_add(b)); +} + +fn unchecked_add_u16(a: u16, b: u16) { + let result = unsafe { a.unchecked_add(b) }; + assert!(result == a.wrapping_add(b)); +} + +fn unchecked_add_u32(a: u32, b: u32) { + let result = unsafe { a.unchecked_add(b) }; + assert!(result == a.wrapping_add(b)); +} + +fn unchecked_add_u64(a: u64, b: u64) { + let result = unsafe { a.unchecked_add(b) }; + assert!(result == a.wrapping_add(b)); +} + +fn unchecked_add_u128(a: u128, b: u128) { + let result = unsafe { a.unchecked_add(b) }; + assert!(result == a.wrapping_add(b)); +} + +fn unchecked_add_i8(a: i8, b: i8) { + let result = unsafe { a.unchecked_add(b) }; + assert!(result == a.wrapping_add(b)); +} + +fn unchecked_add_i16(a: i16, b: i16) { + let result = unsafe { a.unchecked_add(b) }; + assert!(result == a.wrapping_add(b)); +} + +fn unchecked_add_i32(a: i32, b: i32) { + let result = unsafe { a.unchecked_add(b) }; + assert!(result == a.wrapping_add(b)); +} + +fn unchecked_add_i64(a: i64, b: i64) { + let result = unsafe { a.unchecked_add(b) }; + assert!(result == a.wrapping_add(b)); +} + +fn unchecked_add_i128(a: i128, b: i128) { + let result = unsafe { a.unchecked_add(b) }; + assert!(result == a.wrapping_add(b)); +} diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_add.rs b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_add.rs new file mode 100644 index 000000000..ef210d2d0 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_add.rs @@ -0,0 +1,84 @@ +#![feature(unchecked_math)] + +fn main() { + unchecked_add_u8(0, 0); + unchecked_add_u16(0, 0); + unchecked_add_u32(0, 0); + unchecked_add_u64(0, 0); + unchecked_add_u128(0, 0); + unchecked_add_i8(0, 0); + unchecked_add_i16(0, 0); + unchecked_add_i32(0, 0); + unchecked_add_i64(0, 0); + unchecked_add_i128(0, 0); +} + +fn unchecked_add_u8(a: u8, b: u8) { + if let Some(expected) = a.checked_add(b) { + let result = unsafe { a.unchecked_add(b) }; + assert!(result == expected); + } +} + +fn unchecked_add_u16(a: u16, b: u16) { + if let Some(expected) = a.checked_add(b) { + let result = unsafe { a.unchecked_add(b) }; + assert!(result == expected); + } +} + +fn unchecked_add_u32(a: u32, b: u32) { + if let Some(expected) = a.checked_add(b) { + let result = unsafe { a.unchecked_add(b) }; + assert!(result == expected); + } +} + +fn unchecked_add_u64(a: u64, b: u64) { + if let Some(expected) = a.checked_add(b) { + let result = unsafe { a.unchecked_add(b) }; + assert!(result == expected); + } +} + +fn unchecked_add_u128(a: u128, b: u128) { + if let Some(expected) = a.checked_add(b) { + let result = unsafe { a.unchecked_add(b) }; + assert!(result == expected); + } +} + +fn unchecked_add_i8(a: i8, b: i8) { + if let Some(expected) = a.checked_add(b) { + let result = unsafe { a.unchecked_add(b) }; + assert!(result == expected); + } +} + +fn unchecked_add_i16(a: i16, b: i16) { + if let Some(expected) = a.checked_add(b) { + let result = unsafe { a.unchecked_add(b) }; + assert!(result == expected); + } +} + +fn unchecked_add_i32(a: i32, b: i32) { + if let Some(expected) = a.checked_add(b) { + let result = unsafe { a.unchecked_add(b) }; + assert!(result == expected); + } +} + +fn unchecked_add_i64(a: i64, b: i64) { + if let Some(expected) = a.checked_add(b) { + let result = unsafe { a.unchecked_add(b) }; + assert!(result == expected); + } +} + +fn unchecked_add_i128(a: i128, b: i128) { + if let Some(expected) = a.checked_add(b) { + let result = unsafe { a.unchecked_add(b) }; + assert!(result == expected); + } +} diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_mul-fail.rs b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_mul-fail.rs new file mode 100644 index 000000000..1fb9684cd --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_mul-fail.rs @@ -0,0 +1,64 @@ +#![feature(unchecked_math)] + +fn main() { + unchecked_mul_u8(0, 0); + unchecked_mul_u16(0, 0); + unchecked_mul_u32(0, 0); + unchecked_mul_u64(0, 0); + unchecked_mul_u128(0, 0); + unchecked_mul_i8(0, 0); + unchecked_mul_i16(0, 0); + unchecked_mul_i32(0, 0); + unchecked_mul_i64(0, 0); + unchecked_mul_i128(0, 0); +} + +fn unchecked_mul_u8(a: u8, b: u8) { + let result = unsafe { a.unchecked_mul(b) }; + assert!(result == a.wrapping_mul(b)); +} + +fn unchecked_mul_u16(a: u16, b: u16) { + let result = unsafe { a.unchecked_mul(b) }; + assert!(result == a.wrapping_mul(b)); +} + +fn unchecked_mul_u32(a: u32, b: u32) { + let result = unsafe { a.unchecked_mul(b) }; + assert!(result == a.wrapping_mul(b)); +} + +fn unchecked_mul_u64(a: u64, b: u64) { + let result = unsafe { a.unchecked_mul(b) }; + assert!(result == a.wrapping_mul(b)); +} + +fn unchecked_mul_u128(a: u128, b: u128) { + let result = unsafe { a.unchecked_mul(b) }; + assert!(result == a.wrapping_mul(b)); +} + +fn unchecked_mul_i8(a: i8, b: i8) { + let result = unsafe { a.unchecked_mul(b) }; + assert!(result == a.wrapping_mul(b)); +} + +fn unchecked_mul_i16(a: i16, b: i16) { + let result = unsafe { a.unchecked_mul(b) }; + assert!(result == a.wrapping_mul(b)); +} + +fn unchecked_mul_i32(a: i32, b: i32) { + let result = unsafe { a.unchecked_mul(b) }; + assert!(result == a.wrapping_mul(b)); +} + +fn unchecked_mul_i64(a: i64, b: i64) { + let result = unsafe { a.unchecked_mul(b) }; + assert!(result == a.wrapping_mul(b)); +} + +fn unchecked_mul_i128(a: i128, b: i128) { + let result = unsafe { a.unchecked_mul(b) }; + assert!(result == a.wrapping_mul(b)); +} diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_mul.rs b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_mul.rs new file mode 100644 index 000000000..f364a4d47 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_mul.rs @@ -0,0 +1,84 @@ +#![feature(unchecked_math)] + +fn main() { + unchecked_mul_u8(0, 0); + unchecked_mul_u16(0, 0); + unchecked_mul_u32(0, 0); + unchecked_mul_u64(0, 0); + unchecked_mul_u128(0, 0); + unchecked_mul_i8(0, 0); + unchecked_mul_i16(0, 0); + unchecked_mul_i32(0, 0); + unchecked_mul_i64(0, 0); + unchecked_mul_i128(0, 0); +} + +fn unchecked_mul_u8(a: u8, b: u8) { + if let Some(expected) = a.checked_mul(b) { + let result = unsafe { a.unchecked_mul(b) }; + assert!(result == expected); + } +} + +fn unchecked_mul_u16(a: u16, b: u16) { + if let Some(expected) = a.checked_mul(b) { + let result = unsafe { a.unchecked_mul(b) }; + assert!(result == expected); + } +} + +fn unchecked_mul_u32(a: u32, b: u32) { + if let Some(expected) = a.checked_mul(b) { + let result = unsafe { a.unchecked_mul(b) }; + assert!(result == expected); + } +} + +fn unchecked_mul_u64(a: u64, b: u64) { + if let Some(expected) = a.checked_mul(b) { + let result = unsafe { a.unchecked_mul(b) }; + assert!(result == expected); + } +} + +fn unchecked_mul_u128(a: u128, b: u128) { + if let Some(expected) = a.checked_mul(b) { + let result = unsafe { a.unchecked_mul(b) }; + assert!(result == expected); + } +} + +fn unchecked_mul_i8(a: i8, b: i8) { + if let Some(expected) = a.checked_mul(b) { + let result = unsafe { a.unchecked_mul(b) }; + assert!(result == expected); + } +} + +fn unchecked_mul_i16(a: i16, b: i16) { + if let Some(expected) = a.checked_mul(b) { + let result = unsafe { a.unchecked_mul(b) }; + assert!(result == expected); + } +} + +fn unchecked_mul_i32(a: i32, b: i32) { + if let Some(expected) = a.checked_mul(b) { + let result = unsafe { a.unchecked_mul(b) }; + assert!(result == expected); + } +} + +fn unchecked_mul_i64(a: i64, b: i64) { + if let Some(expected) = a.checked_mul(b) { + let result = unsafe { a.unchecked_mul(b) }; + assert!(result == expected); + } +} + +fn unchecked_mul_i128(a: i128, b: i128) { + if let Some(expected) = a.checked_mul(b) { + let result = unsafe { a.unchecked_mul(b) }; + assert!(result == expected); + } +} diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_neg-fail.rs b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_neg-fail.rs new file mode 100644 index 000000000..35c732a0d --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_neg-fail.rs @@ -0,0 +1,34 @@ +#![feature(unchecked_neg)] + +fn main() { + unchecked_neg_i8(0); + unchecked_neg_i16(0); + unchecked_neg_i32(0); + unchecked_neg_i64(0); + unchecked_neg_i128(0); +} + +fn unchecked_neg_i8(a: i8) { + let result = unsafe { a.unchecked_neg() }; + assert!(result == a.wrapping_neg()); +} + +fn unchecked_neg_i16(a: i16) { + let result = unsafe { a.unchecked_neg() }; + assert!(result == a.wrapping_neg()); +} + +fn unchecked_neg_i32(a: i32) { + let result = unsafe { a.unchecked_neg() }; + assert!(result == a.wrapping_neg()); +} + +fn unchecked_neg_i64(a: i64) { + let result = unsafe { a.unchecked_neg() }; + assert!(result == a.wrapping_neg()); +} + +fn unchecked_neg_i128(a: i128) { + let result = unsafe { a.unchecked_neg() }; + assert!(result == a.wrapping_neg()); +} diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_neg.rs b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_neg.rs new file mode 100644 index 000000000..b9c70684c --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_neg.rs @@ -0,0 +1,44 @@ +#![feature(unchecked_neg)] + +fn main() { + unchecked_neg_i8(0); + unchecked_neg_i16(0); + unchecked_neg_i32(0); + unchecked_neg_i64(0); + unchecked_neg_i128(0); +} + +fn unchecked_neg_i8(a: i8) { + if let Some(expected) = a.checked_neg() { + let result = unsafe { a.unchecked_neg() }; + assert!(result == expected); + } +} + +fn unchecked_neg_i16(a: i16) { + if let Some(expected) = a.checked_neg() { + let result = unsafe { a.unchecked_neg() }; + assert!(result == expected); + } +} + +fn unchecked_neg_i32(a: i32) { + if let Some(expected) = a.checked_neg() { + let result = unsafe { a.unchecked_neg() }; + assert!(result == expected); + } +} + +fn unchecked_neg_i64(a: i64) { + if let Some(expected) = a.checked_neg() { + let result = unsafe { a.unchecked_neg() }; + assert!(result == expected); + } +} + +fn unchecked_neg_i128(a: i128) { + if let Some(expected) = a.checked_neg() { + let result = unsafe { a.unchecked_neg() }; + assert!(result == expected); + } +} diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_shl-fail.rs b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_shl-fail.rs new file mode 100644 index 000000000..3d35ab316 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_shl-fail.rs @@ -0,0 +1,64 @@ +#![feature(unchecked_shifts)] + +fn main() { + unchecked_shl_u8(0, 0); + unchecked_shl_u16(0, 0); + unchecked_shl_u32(0, 0); + unchecked_shl_u64(0, 0); + unchecked_shl_u128(0, 0); + unchecked_shl_i8(0, 0); + unchecked_shl_i16(0, 0); + unchecked_shl_i32(0, 0); + unchecked_shl_i64(0, 0); + unchecked_shl_i128(0, 0); +} + +fn unchecked_shl_u8(a: u8, b: u32) { + let result = unsafe { a.unchecked_shl(b) }; + assert!(result == a.wrapping_shl(b)); +} + +fn unchecked_shl_u16(a: u16, b: u32) { + let result = unsafe { a.unchecked_shl(b) }; + assert!(result == a.wrapping_shl(b)); +} + +fn unchecked_shl_u32(a: u32, b: u32) { + let result = unsafe { a.unchecked_shl(b) }; + assert!(result == a.wrapping_shl(b)); +} + +fn unchecked_shl_u64(a: u64, b: u32) { + let result = unsafe { a.unchecked_shl(b) }; + assert!(result == a.wrapping_shl(b)); +} + +fn unchecked_shl_u128(a: u128, b: u32) { + let result = unsafe { a.unchecked_shl(b) }; + assert!(result == a.wrapping_shl(b)); +} + +fn unchecked_shl_i8(a: i8, b: u32) { + let result = unsafe { a.unchecked_shl(b) }; + assert!(result == a.wrapping_shl(b)); +} + +fn unchecked_shl_i16(a: i16, b: u32) { + let result = unsafe { a.unchecked_shl(b) }; + assert!(result == a.wrapping_shl(b)); +} + +fn unchecked_shl_i32(a: i32, b: u32) { + let result = unsafe { a.unchecked_shl(b) }; + assert!(result == a.wrapping_shl(b)); +} + +fn unchecked_shl_i64(a: i64, b: u32) { + let result = unsafe { a.unchecked_shl(b) }; + assert!(result == a.wrapping_shl(b)); +} + +fn unchecked_shl_i128(a: i128, b: u32) { + let result = unsafe { a.unchecked_shl(b) }; + assert!(result == a.wrapping_shl(b)); +} diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_shl.rs b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_shl.rs new file mode 100644 index 000000000..86fde4935 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_shl.rs @@ -0,0 +1,84 @@ +#![feature(unchecked_shifts)] + +fn main() { + unchecked_shl_u8(0, 0); + unchecked_shl_u16(0, 0); + unchecked_shl_u32(0, 0); + unchecked_shl_u64(0, 0); + unchecked_shl_u128(0, 0); + unchecked_shl_i8(0, 0); + unchecked_shl_i16(0, 0); + unchecked_shl_i32(0, 0); + unchecked_shl_i64(0, 0); + unchecked_shl_i128(0, 0); +} + +fn unchecked_shl_u8(a: u8, b: u32) { + if let Some(expected) = a.checked_shl(b) { + let result = unsafe { a.unchecked_shl(b) }; + assert!(result == expected); + } +} + +fn unchecked_shl_u16(a: u16, b: u32) { + if let Some(expected) = a.checked_shl(b) { + let result = unsafe { a.unchecked_shl(b) }; + assert!(result == expected); + } +} + +fn unchecked_shl_u32(a: u32, b: u32) { + if let Some(expected) = a.checked_shl(b) { + let result = unsafe { a.unchecked_shl(b) }; + assert!(result == expected); + } +} + +fn unchecked_shl_u64(a: u64, b: u32) { + if let Some(expected) = a.checked_shl(b) { + let result = unsafe { a.unchecked_shl(b) }; + assert!(result == expected); + } +} + +fn unchecked_shl_u128(a: u128, b: u32) { + if let Some(expected) = a.checked_shl(b) { + let result = unsafe { a.unchecked_shl(b) }; + assert!(result == expected); + } +} + +fn unchecked_shl_i8(a: i8, b: u32) { + if let Some(expected) = a.checked_shl(b) { + let result = unsafe { a.unchecked_shl(b) }; + assert!(result == expected); + } +} + +fn unchecked_shl_i16(a: i16, b: u32) { + if let Some(expected) = a.checked_shl(b) { + let result = unsafe { a.unchecked_shl(b) }; + assert!(result == expected); + } +} + +fn unchecked_shl_i32(a: i32, b: u32) { + if let Some(expected) = a.checked_shl(b) { + let result = unsafe { a.unchecked_shl(b) }; + assert!(result == expected); + } +} + +fn unchecked_shl_i64(a: i64, b: u32) { + if let Some(expected) = a.checked_shl(b) { + let result = unsafe { a.unchecked_shl(b) }; + assert!(result == expected); + } +} + +fn unchecked_shl_i128(a: i128, b: u32) { + if let Some(expected) = a.checked_shl(b) { + let result = unsafe { a.unchecked_shl(b) }; + assert!(result == expected); + } +} diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_shr-fail.rs b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_shr-fail.rs new file mode 100644 index 000000000..c1192257f --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_shr-fail.rs @@ -0,0 +1,64 @@ +#![feature(unchecked_shifts)] + +fn main() { + unchecked_shr_u8(0, 0); + unchecked_shr_u16(0, 0); + unchecked_shr_u32(0, 0); + unchecked_shr_u64(0, 0); + unchecked_shr_u128(0, 0); + unchecked_shr_i8(0, 0); + unchecked_shr_i16(0, 0); + unchecked_shr_i32(0, 0); + unchecked_shr_i64(0, 0); + unchecked_shr_i128(0, 0); +} + +fn unchecked_shr_u8(a: u8, b: u32) { + let result = unsafe { a.unchecked_shr(b) }; + assert!(result == a.wrapping_shr(b)); +} + +fn unchecked_shr_u16(a: u16, b: u32) { + let result = unsafe { a.unchecked_shr(b) }; + assert!(result == a.wrapping_shr(b)); +} + +fn unchecked_shr_u32(a: u32, b: u32) { + let result = unsafe { a.unchecked_shr(b) }; + assert!(result == a.wrapping_shr(b)); +} + +fn unchecked_shr_u64(a: u64, b: u32) { + let result = unsafe { a.unchecked_shr(b) }; + assert!(result == a.wrapping_shr(b)); +} + +fn unchecked_shr_u128(a: u128, b: u32) { + let result = unsafe { a.unchecked_shr(b) }; + assert!(result == a.wrapping_shr(b)); +} + +fn unchecked_shr_i8(a: i8, b: u32) { + let result = unsafe { a.unchecked_shr(b) }; + assert!(result == a.wrapping_shr(b)); +} + +fn unchecked_shr_i16(a: i16, b: u32) { + let result = unsafe { a.unchecked_shr(b) }; + assert!(result == a.wrapping_shr(b)); +} + +fn unchecked_shr_i32(a: i32, b: u32) { + let result = unsafe { a.unchecked_shr(b) }; + assert!(result == a.wrapping_shr(b)); +} + +fn unchecked_shr_i64(a: i64, b: u32) { + let result = unsafe { a.unchecked_shr(b) }; + assert!(result == a.wrapping_shr(b)); +} + +fn unchecked_shr_i128(a: i128, b: u32) { + let result = unsafe { a.unchecked_shr(b) }; + assert!(result == a.wrapping_shr(b)); +} diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_shr.rs b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_shr.rs new file mode 100644 index 000000000..13d7f8064 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_shr.rs @@ -0,0 +1,84 @@ +#![feature(unchecked_shifts)] + +fn main() { + unchecked_shr_u8(0, 0); + unchecked_shr_u16(0, 0); + unchecked_shr_u32(0, 0); + unchecked_shr_u64(0, 0); + unchecked_shr_u128(0, 0); + unchecked_shr_i8(0, 0); + unchecked_shr_i16(0, 0); + unchecked_shr_i32(0, 0); + unchecked_shr_i64(0, 0); + unchecked_shr_i128(0, 0); +} + +fn unchecked_shr_u8(a: u8, b: u32) { + if let Some(expected) = a.checked_shr(b) { + let result = unsafe { a.unchecked_shr(b) }; + assert!(result == expected); + } +} + +fn unchecked_shr_u16(a: u16, b: u32) { + if let Some(expected) = a.checked_shr(b) { + let result = unsafe { a.unchecked_shr(b) }; + assert!(result == expected); + } +} + +fn unchecked_shr_u32(a: u32, b: u32) { + if let Some(expected) = a.checked_shr(b) { + let result = unsafe { a.unchecked_shr(b) }; + assert!(result == expected); + } +} + +fn unchecked_shr_u64(a: u64, b: u32) { + if let Some(expected) = a.checked_shr(b) { + let result = unsafe { a.unchecked_shr(b) }; + assert!(result == expected); + } +} + +fn unchecked_shr_u128(a: u128, b: u32) { + if let Some(expected) = a.checked_shr(b) { + let result = unsafe { a.unchecked_shr(b) }; + assert!(result == expected); + } +} + +fn unchecked_shr_i8(a: i8, b: u32) { + if let Some(expected) = a.checked_shr(b) { + let result = unsafe { a.unchecked_shr(b) }; + assert!(result == expected); + } +} + +fn unchecked_shr_i16(a: i16, b: u32) { + if let Some(expected) = a.checked_shr(b) { + let result = unsafe { a.unchecked_shr(b) }; + assert!(result == expected); + } +} + +fn unchecked_shr_i32(a: i32, b: u32) { + if let Some(expected) = a.checked_shr(b) { + let result = unsafe { a.unchecked_shr(b) }; + assert!(result == expected); + } +} + +fn unchecked_shr_i64(a: i64, b: u32) { + if let Some(expected) = a.checked_shr(b) { + let result = unsafe { a.unchecked_shr(b) }; + assert!(result == expected); + } +} + +fn unchecked_shr_i128(a: i128, b: u32) { + if let Some(expected) = a.checked_shr(b) { + let result = unsafe { a.unchecked_shr(b) }; + assert!(result == expected); + } +} diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_sub-fail.rs b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_sub-fail.rs new file mode 100644 index 000000000..fd27fa0c4 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_sub-fail.rs @@ -0,0 +1,64 @@ +#![feature(unchecked_math)] + +fn main() { + unchecked_sub_u8(0, 0); + unchecked_sub_u16(0, 0); + unchecked_sub_u32(0, 0); + unchecked_sub_u64(0, 0); + unchecked_sub_u128(0, 0); + unchecked_sub_i8(0, 0); + unchecked_sub_i16(0, 0); + unchecked_sub_i32(0, 0); + unchecked_sub_i64(0, 0); + unchecked_sub_i128(0, 0); +} + +fn unchecked_sub_u8(a: u8, b: u8) { + let result = unsafe { a.unchecked_sub(b) }; + assert!(result == a.wrapping_sub(b)); +} + +fn unchecked_sub_u16(a: u16, b: u16) { + let result = unsafe { a.unchecked_sub(b) }; + assert!(result == a.wrapping_sub(b)); +} + +fn unchecked_sub_u32(a: u32, b: u32) { + let result = unsafe { a.unchecked_sub(b) }; + assert!(result == a.wrapping_sub(b)); +} + +fn unchecked_sub_u64(a: u64, b: u64) { + let result = unsafe { a.unchecked_sub(b) }; + assert!(result == a.wrapping_sub(b)); +} + +fn unchecked_sub_u128(a: u128, b: u128) { + let result = unsafe { a.unchecked_sub(b) }; + assert!(result == a.wrapping_sub(b)); +} + +fn unchecked_sub_i8(a: i8, b: i8) { + let result = unsafe { a.unchecked_sub(b) }; + assert!(result == a.wrapping_sub(b)); +} + +fn unchecked_sub_i16(a: i16, b: i16) { + let result = unsafe { a.unchecked_sub(b) }; + assert!(result == a.wrapping_sub(b)); +} + +fn unchecked_sub_i32(a: i32, b: i32) { + let result = unsafe { a.unchecked_sub(b) }; + assert!(result == a.wrapping_sub(b)); +} + +fn unchecked_sub_i64(a: i64, b: i64) { + let result = unsafe { a.unchecked_sub(b) }; + assert!(result == a.wrapping_sub(b)); +} + +fn unchecked_sub_i128(a: i128, b: i128) { + let result = unsafe { a.unchecked_sub(b) }; + assert!(result == a.wrapping_sub(b)); +} diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_sub.rs b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_sub.rs new file mode 100644 index 000000000..8745dd6d3 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_sub.rs @@ -0,0 +1,84 @@ +#![feature(unchecked_math)] + +fn main() { + unchecked_sub_u8(0, 0); + unchecked_sub_u16(0, 0); + unchecked_sub_u32(0, 0); + unchecked_sub_u64(0, 0); + unchecked_sub_u128(0, 0); + unchecked_sub_i8(0, 0); + unchecked_sub_i16(0, 0); + unchecked_sub_i32(0, 0); + unchecked_sub_i64(0, 0); + unchecked_sub_i128(0, 0); +} + +fn unchecked_sub_u8(a: u8, b: u8) { + if let Some(expected) = a.checked_sub(b) { + let result = unsafe { a.unchecked_sub(b) }; + assert!(result == expected); + } +} + +fn unchecked_sub_u16(a: u16, b: u16) { + if let Some(expected) = a.checked_sub(b) { + let result = unsafe { a.unchecked_sub(b) }; + assert!(result == expected); + } +} + +fn unchecked_sub_u32(a: u32, b: u32) { + if let Some(expected) = a.checked_sub(b) { + let result = unsafe { a.unchecked_sub(b) }; + assert!(result == expected); + } +} + +fn unchecked_sub_u64(a: u64, b: u64) { + if let Some(expected) = a.checked_sub(b) { + let result = unsafe { a.unchecked_sub(b) }; + assert!(result == expected); + } +} + +fn unchecked_sub_u128(a: u128, b: u128) { + if let Some(expected) = a.checked_sub(b) { + let result = unsafe { a.unchecked_sub(b) }; + assert!(result == expected); + } +} + +fn unchecked_sub_i8(a: i8, b: i8) { + if let Some(expected) = a.checked_sub(b) { + let result = unsafe { a.unchecked_sub(b) }; + assert!(result == expected); + } +} + +fn unchecked_sub_i16(a: i16, b: i16) { + if let Some(expected) = a.checked_sub(b) { + let result = unsafe { a.unchecked_sub(b) }; + assert!(result == expected); + } +} + +fn unchecked_sub_i32(a: i32, b: i32) { + if let Some(expected) = a.checked_sub(b) { + let result = unsafe { a.unchecked_sub(b) }; + assert!(result == expected); + } +} + +fn unchecked_sub_i64(a: i64, b: i64) { + if let Some(expected) = a.checked_sub(b) { + let result = unsafe { a.unchecked_sub(b) }; + assert!(result == expected); + } +} + +fn unchecked_sub_i128(a: i128, b: i128) { + if let Some(expected) = a.checked_sub(b) { + let result = unsafe { a.unchecked_sub(b) }; + assert!(result == expected); + } +} diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/widening_mul.rs b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/widening_mul.rs new file mode 100644 index 000000000..806c63d3f --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/widening_mul.rs @@ -0,0 +1,36 @@ +#![feature(bigint_helper_methods)] + +fn main() { + widening_mul_u8(0, 0); + widening_mul_u16(0, 0); + widening_mul_u32(0, 0); + widening_mul_u64(0, 0); +} + +fn widening_mul_u8(a: u8, b: u8) { + let (lo, hi) = a.widening_mul(b); + let expected = (a as u16) * (b as u16); + assert!(lo == (expected as u8)); + assert!(hi == ((expected >> u8::BITS) as u8)); +} + +fn widening_mul_u16(a: u16, b: u16) { + let (lo, hi) = a.widening_mul(b); + let expected = (a as u32) * (b as u32); + assert!(lo == (expected as u16)); + assert!(hi == ((expected >> u16::BITS) as u16)); +} + +fn widening_mul_u32(a: u32, b: u32) { + let (lo, hi) = a.widening_mul(b); + let expected = (a as u64) * (b as u64); + assert!(lo == (expected as u32)); + assert!(hi == ((expected >> u32::BITS) as u32)); +} + +fn widening_mul_u64(a: u64, b: u64) { + let (lo, hi) = a.widening_mul(b); + let expected = (a as u128) * (b as u128); + assert!(lo == (expected as u64)); + assert!(hi == ((expected >> u64::BITS) as u64)); +} diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/wrapping_shl.rs b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/wrapping_shl.rs new file mode 100644 index 000000000..e28de3376 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/wrapping_shl.rs @@ -0,0 +1,72 @@ +fn main() { + wrapping_shl_u8(0, 0); + wrapping_shl_u16(0, 0); + wrapping_shl_u32(0, 0); + wrapping_shl_u64(0, 0); + wrapping_shl_u128(0, 0); + wrapping_shl_i8(0, 0); + wrapping_shl_i16(0, 0); + wrapping_shl_i32(0, 0); + wrapping_shl_i64(0, 0); + wrapping_shl_i128(0, 0); +} + +fn wrapping_shl_u8(a: u8, b: u32) { + if let Some(expected) = a.checked_shl(b) { + assert!(a.wrapping_shl(b) == expected); + } +} + +fn wrapping_shl_u16(a: u16, b: u32) { + if let Some(expected) = a.checked_shl(b) { + assert!(a.wrapping_shl(b) == expected); + } +} + +fn wrapping_shl_u32(a: u32, b: u32) { + if let Some(expected) = a.checked_shl(b) { + assert!(a.wrapping_shl(b) == expected); + } +} + +fn wrapping_shl_u64(a: u64, b: u32) { + if let Some(expected) = a.checked_shl(b) { + assert!(a.wrapping_shl(b) == expected); + } +} + +fn wrapping_shl_u128(a: u128, b: u32) { + if let Some(expected) = a.checked_shl(b) { + assert!(a.wrapping_shl(b) == expected); + } +} + +fn wrapping_shl_i8(a: i8, b: u32) { + if let Some(expected) = a.checked_shl(b) { + assert!(a.wrapping_shl(b) == expected); + } +} + +fn wrapping_shl_i16(a: i16, b: u32) { + if let Some(expected) = a.checked_shl(b) { + assert!(a.wrapping_shl(b) == expected); + } +} + +fn wrapping_shl_i32(a: i32, b: u32) { + if let Some(expected) = a.checked_shl(b) { + assert!(a.wrapping_shl(b) == expected); + } +} + +fn wrapping_shl_i64(a: i64, b: u32) { + if let Some(expected) = a.checked_shl(b) { + assert!(a.wrapping_shl(b) == expected); + } +} + +fn wrapping_shl_i128(a: i128, b: u32) { + if let Some(expected) = a.checked_shl(b) { + assert!(a.wrapping_shl(b) == expected); + } +} diff --git a/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/wrapping_shr.rs b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/wrapping_shr.rs new file mode 100644 index 000000000..ab182baf0 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/wrapping_shr.rs @@ -0,0 +1,72 @@ +fn main() { + wrapping_shr_u8(0, 0); + wrapping_shr_u16(0, 0); + wrapping_shr_u32(0, 0); + wrapping_shr_u64(0, 0); + wrapping_shr_u128(0, 0); + wrapping_shr_i8(0, 0); + wrapping_shr_i16(0, 0); + wrapping_shr_i32(0, 0); + wrapping_shr_i64(0, 0); + wrapping_shr_i128(0, 0); +} + +fn wrapping_shr_u8(a: u8, b: u32) { + if let Some(expected) = a.checked_shr(b) { + assert!(a.wrapping_shr(b) == expected); + } +} + +fn wrapping_shr_u16(a: u16, b: u32) { + if let Some(expected) = a.checked_shr(b) { + assert!(a.wrapping_shr(b) == expected); + } +} + +fn wrapping_shr_u32(a: u32, b: u32) { + if let Some(expected) = a.checked_shr(b) { + assert!(a.wrapping_shr(b) == expected); + } +} + +fn wrapping_shr_u64(a: u64, b: u32) { + if let Some(expected) = a.checked_shr(b) { + assert!(a.wrapping_shr(b) == expected); + } +} + +fn wrapping_shr_u128(a: u128, b: u32) { + if let Some(expected) = a.checked_shr(b) { + assert!(a.wrapping_shr(b) == expected); + } +} + +fn wrapping_shr_i8(a: i8, b: u32) { + if let Some(expected) = a.checked_shr(b) { + assert!(a.wrapping_shr(b) == expected); + } +} + +fn wrapping_shr_i16(a: i16, b: u32) { + if let Some(expected) = a.checked_shr(b) { + assert!(a.wrapping_shr(b) == expected); + } +} + +fn wrapping_shr_i32(a: i32, b: u32) { + if let Some(expected) = a.checked_shr(b) { + assert!(a.wrapping_shr(b) == expected); + } +} + +fn wrapping_shr_i64(a: i64, b: u32) { + if let Some(expected) = a.checked_shr(b) { + assert!(a.wrapping_shr(b) == expected); + } +} + +fn wrapping_shr_i128(a: i128, b: u32) { + if let Some(expected) = a.checked_shr(b) { + assert!(a.wrapping_shr(b) == expected); + } +} diff --git a/kmir/src/tests/integration/data/verify-rust-std/README.md b/kmir/src/tests/integration/data/verify-rust-std/README.md new file mode 100644 index 000000000..49a5a0d32 --- /dev/null +++ b/kmir/src/tests/integration/data/verify-rust-std/README.md @@ -0,0 +1,8 @@ +# verify-rust-std challenges + +Test harnesses for verify-rust-std ([docs](https://model-checking.github.io/verify-rust-std/) / [github](https://github.com/model-checking/verify-rust-std/)) challenges. Each subdirectory corresponds to a challenge and contains a README.md on progress. + +All tests are run with `--terminate-on-thunk`, so unresolved symbolic expressions (e.g. from unchecked operations with unmet preconditions) cause the proof to terminate rather than propagate. This means `-fail` tests detect UB by the prover being unable to resolve the unchecked operation on the violating path. + +Status: +- [ ] Challenge 0011: Safety of Methods for Numeric Primitive Types diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index 14b5221c3..5ae0bcda1 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -12,7 +12,7 @@ from pyk.kast.pretty import PrettyPrinter from pyk.proof.show import APRProofShow -from kmir.cargo import CargoProject +from kmir.cargo import CargoProject, cargo_get_smir_json from kmir.kmir import KMIR, KMIRAPRNodePrinter from kmir.options import ProveOpts, ShowOpts from kmir.parse.parser import Parser @@ -41,6 +41,9 @@ 'iter-eq-copied-take-dereftruncate': ['repro'], 'spl-multisig-iter-eq-copied-next': ['repro'], } +PROVE_TERMINATE_ON_THUNK = [ + 'closure-staged', +] PROVE_SHOW_SPECS = [ 'local-raw-fail', 'interior-mut-fail', @@ -87,7 +90,8 @@ def test_prove(rs_file: Path, kmir: KMIR, update_expected_output: bool) -> None: if update_expected_output and not should_show: pytest.skip() - prove_opts = ProveOpts(rs_file, smir=is_smir, terminate_on_thunk=True) + should_terminate_on_thunk = rs_file.stem in PROVE_TERMINATE_ON_THUNK + prove_opts = ProveOpts(rs_file, smir=is_smir, terminate_on_thunk=should_terminate_on_thunk) printer = PrettyPrinter(kmir.definition) cterm_show = CTermShow(printer.print) @@ -115,6 +119,240 @@ def test_prove(rs_file: Path, kmir: KMIR, update_expected_output: bool) -> None: assert apr_proof.failed +VERIFY_RUST_STD_DIR = (Path(__file__).parent / 'data' / 'verify-rust-std').resolve(strict=True) +VERIFY_RUST_STD_FILES = list(VERIFY_RUST_STD_DIR.glob('**/*.rs')) +VERIFY_RUST_STD_START_SYMBOLS = { + 'unchecked_add': [ + 'unchecked_add_u8', + 'unchecked_add_u16', + 'unchecked_add_u32', + 'unchecked_add_u64', + 'unchecked_add_u128', + 'unchecked_add_i8', + 'unchecked_add_i16', + 'unchecked_add_i32', + 'unchecked_add_i64', + 'unchecked_add_i128', + ], + 'unchecked_sub': [ + 'unchecked_sub_u8', + 'unchecked_sub_u16', + 'unchecked_sub_u32', + 'unchecked_sub_u64', + 'unchecked_sub_u128', + 'unchecked_sub_i8', + 'unchecked_sub_i16', + 'unchecked_sub_i32', + 'unchecked_sub_i64', + 'unchecked_sub_i128', + ], + 'unchecked_mul': [ + 'unchecked_mul_u8', + 'unchecked_mul_u16', + 'unchecked_mul_u32', + 'unchecked_mul_u64', + 'unchecked_mul_u128', + 'unchecked_mul_i8', + 'unchecked_mul_i16', + 'unchecked_mul_i32', + 'unchecked_mul_i64', + 'unchecked_mul_i128', + ], + 'unchecked_shl': [ + 'unchecked_shl_u8', + 'unchecked_shl_u16', + 'unchecked_shl_u32', + 'unchecked_shl_u64', + 'unchecked_shl_u128', + 'unchecked_shl_i8', + 'unchecked_shl_i16', + 'unchecked_shl_i32', + 'unchecked_shl_i64', + 'unchecked_shl_i128', + ], + 'unchecked_shr': [ + 'unchecked_shr_u8', + 'unchecked_shr_u16', + 'unchecked_shr_u32', + 'unchecked_shr_u64', + 'unchecked_shr_u128', + 'unchecked_shr_i8', + 'unchecked_shr_i16', + 'unchecked_shr_i32', + 'unchecked_shr_i64', + 'unchecked_shr_i128', + ], + 'unchecked_neg': [ + 'unchecked_neg_i8', + 'unchecked_neg_i16', + 'unchecked_neg_i32', + 'unchecked_neg_i64', + 'unchecked_neg_i128', + ], + 'wrapping_shl': [ + 'wrapping_shl_u8', + 'wrapping_shl_u16', + 'wrapping_shl_u32', + 'wrapping_shl_u64', + 'wrapping_shl_u128', + 'wrapping_shl_i8', + 'wrapping_shl_i16', + 'wrapping_shl_i32', + 'wrapping_shl_i64', + 'wrapping_shl_i128', + ], + 'wrapping_shr': [ + 'wrapping_shr_u8', + 'wrapping_shr_u16', + 'wrapping_shr_u32', + 'wrapping_shr_u64', + 'wrapping_shr_u128', + 'wrapping_shr_i8', + 'wrapping_shr_i16', + 'wrapping_shr_i32', + 'wrapping_shr_i64', + 'wrapping_shr_i128', + ], + 'widening_mul': [ + 'widening_mul_u8', + 'widening_mul_u16', + 'widening_mul_u32', + 'widening_mul_u64', + ], + 'carrying_mul': [ + 'carrying_mul_u8', + 'carrying_mul_u16', + 'carrying_mul_u32', + 'carrying_mul_u64', + ], + 'unchecked_add-fail': [ + 'unchecked_add_u8', + 'unchecked_add_u16', + 'unchecked_add_u32', + 'unchecked_add_u64', + 'unchecked_add_u128', + 'unchecked_add_i8', + 'unchecked_add_i16', + 'unchecked_add_i32', + 'unchecked_add_i64', + 'unchecked_add_i128', + ], + 'unchecked_sub-fail': [ + 'unchecked_sub_u8', + 'unchecked_sub_u16', + 'unchecked_sub_u32', + 'unchecked_sub_u64', + 'unchecked_sub_u128', + 'unchecked_sub_i8', + 'unchecked_sub_i16', + 'unchecked_sub_i32', + 'unchecked_sub_i64', + 'unchecked_sub_i128', + ], + 'unchecked_mul-fail': [ + 'unchecked_mul_u8', + 'unchecked_mul_u16', + 'unchecked_mul_u32', + 'unchecked_mul_u64', + 'unchecked_mul_u128', + 'unchecked_mul_i8', + 'unchecked_mul_i16', + 'unchecked_mul_i32', + 'unchecked_mul_i64', + 'unchecked_mul_i128', + ], + 'unchecked_shl-fail': [ + 'unchecked_shl_u8', + 'unchecked_shl_u16', + 'unchecked_shl_u32', + 'unchecked_shl_u64', + 'unchecked_shl_u128', + 'unchecked_shl_i8', + 'unchecked_shl_i16', + 'unchecked_shl_i32', + 'unchecked_shl_i64', + 'unchecked_shl_i128', + ], + 'unchecked_shr-fail': [ + 'unchecked_shr_u8', + 'unchecked_shr_u16', + 'unchecked_shr_u32', + 'unchecked_shr_u64', + 'unchecked_shr_u128', + 'unchecked_shr_i8', + 'unchecked_shr_i16', + 'unchecked_shr_i32', + 'unchecked_shr_i64', + 'unchecked_shr_i128', + ], + 'unchecked_neg-fail': [ + 'unchecked_neg_i8', + 'unchecked_neg_i16', + 'unchecked_neg_i32', + 'unchecked_neg_i64', + 'unchecked_neg_i128', + ], + 'to_int_unchecked-fail': [ + 'to_int_unchecked_f16_i8', + 'to_int_unchecked_f32_i32', + 'to_int_unchecked_f64_i64', + 'to_int_unchecked_f128_i128', + ], +} +VERIFY_RUST_STD_SHOW_SPECS = [ + 'unchecked_add-fail', + 'unchecked_sub-fail', + 'unchecked_mul-fail', + 'unchecked_shl-fail', + 'unchecked_shr-fail', + 'unchecked_neg-fail', + 'to_int_unchecked-fail', +] + + +@pytest.mark.parametrize( + 'rs_file', + VERIFY_RUST_STD_FILES, + ids=[spec.stem for spec in VERIFY_RUST_STD_FILES], +) +def test_verify_rust_std(rs_file: Path, kmir: KMIR, update_expected_output: bool) -> None: + should_fail = rs_file.stem.endswith('fail') + should_show = rs_file.stem in VERIFY_RUST_STD_SHOW_SPECS + + if update_expected_output and not should_show: + pytest.skip() + + parsed_smir = cargo_get_smir_json(rs_file) + prove_opts = ProveOpts(rs_file, terminate_on_thunk=True, parsed_smir=parsed_smir) + printer = PrettyPrinter(kmir.definition) + cterm_show = CTermShow(printer.print) + + start_symbols = ['main'] + if rs_file.stem in VERIFY_RUST_STD_START_SYMBOLS: + start_symbols = VERIFY_RUST_STD_START_SYMBOLS[rs_file.stem] + + for start_symbol in start_symbols: + prove_opts.start_symbol = start_symbol + apr_proof = kmir.prove_program(prove_opts) + + if should_show: + display_opts = ShowOpts( + rs_file.parent, apr_proof.id, full_printer=False, smir_info=None, omit_current_body=False + ) + shower = APRProofShow(kmir.definition, node_printer=KMIRAPRNodePrinter(cterm_show, apr_proof, display_opts)) + show_res = '\n'.join(shower.show(apr_proof)) + show_dir = rs_file.parent / 'show' + show_dir.mkdir(exist_ok=True) + assert_or_update_show_output( + show_res, show_dir / f'{rs_file.stem}.{start_symbol}.expected', update=update_expected_output + ) + + if not should_fail: + assert apr_proof.passed + else: + assert apr_proof.failed + + MULTI_CRATE_DIR = (Path(__file__).parent / 'data' / 'crate-tests').resolve(strict=True) MULTI_CRATE_TESTS = list(MULTI_CRATE_DIR.glob('*/main-crate')) @@ -652,40 +890,3 @@ def test_schema_kapply_parse( json_data, expected_term, expected_sort = test_case assert parser.parse_mir_json(json_data, expected_sort.name) == (expected_term, expected_sort) - - -ARITH_SMIR = PROVE_DIR / 'arith.smir.json' - - -def test_reduce_standalone() -> None: - """Test that kmir reduce correctly prunes SMIR items by reachability.""" - smir_data = json.loads(ARITH_SMIR.read_text()) - info = SMIRInfo(smir_data) - assert len(info.items) == 11 - - # Single root 'add' — should keep 1 item - reduced_add = info.reduce_to('add') - assert len(reduced_add.items) == 1 - - # Single root 'mul' — should keep 1 item (independent from add) - reduced_mul = info.reduce_to('mul') - assert len(reduced_mul.items) == 1 - - # Multiple roots — should keep strictly more than either alone - reduced_multi = info.reduce_to(['add', 'mul']) - assert len(reduced_multi.items) == 2 - - # 'main' calls both add and mul — should keep all 3 - reduced_main = info.reduce_to('main') - assert len(reduced_main.items) == 3 - - # Roundtrip: save reduced SMIR and reload it - with tempfile.NamedTemporaryFile(suffix='.smir.json', delete=False, mode='w') as f: - f.write(json.dumps(reduced_multi._smir)) - reduced_path = Path(f.name) - - try: - reloaded = SMIRInfo(json.loads(reduced_path.read_text())) - assert len(reloaded.items) == 2 - finally: - reduced_path.unlink()