Re-execution: Challenge 11: Safety of Methods for Numeric Primitive Types

.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
-

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)

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.

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.