Update feature/p-token with latest master

.github/scripts/check-cachix-pin.sh

@@ -0,0 +1,86 @@
+#!/usr/bin/env bash
+set -euo pipefail
+
+# Kup relies on cachix registry k-framework-binary.
+CACHE="k-framework-binary"
+OWNER_REPO="${OWNER_REPO:-$(git remote get-url origin | sed -E 's#(git@github.com:|https://github.com/)##; s#\.git$##')}"
+REV="${REV:-${GITHUB_SHA:-$(git rev-parse HEAD)}}"
+UNAME_S="$(uname -s)"
+UNAME_M="$(uname -m)"
+case "${UNAME_S}-${UNAME_M}" in
+  Linux-x86_64) SYSTEM="x86_64-linux" ;;
+  Linux-aarch64 | Linux-arm64) SYSTEM="aarch64-linux" ;;
+  Darwin-x86_64) SYSTEM="x86_64-darwin" ;;
+  Darwin-arm64) SYSTEM="aarch64-darwin" ;;
+  *)
+    echo "Unsupported platform: ${UNAME_S}-${UNAME_M}" >&2
+    exit 1
+    ;;
+esac
+PIN_API_URL="https://app.cachix.org/api/v1/cache/${CACHE}/pin"
+CHECK_PACKAGES=(kmir kmir.rust)
+
+SUMMARY="${GITHUB_STEP_SUMMARY:-/dev/stdout}"
+
+{
+  echo "## Cachix Publish Summary"
+  echo "CACHE: $CACHE"
+  echo "OWNER_REPO: $OWNER_REPO"
+  echo "REV: $REV"
+  echo "SYSTEM: $SYSTEM"
+  echo "PACKAGES: ${CHECK_PACKAGES[*]}"
+} >> "$SUMMARY"
+
+# Verify push + pin together for each package. Both can become visible with delay.
+PIN_VISIBILITY_TIMEOUT_SECONDS=120 # 2 minutes
+PIN_VISIBILITY_INTERVAL_SECONDS=5 # 5 seconds
+PIN_VISIBILITY_ATTEMPTS=$((PIN_VISIBILITY_TIMEOUT_SECONDS / PIN_VISIBILITY_INTERVAL_SECONDS))
+for i in $(seq 1 "$PIN_VISIBILITY_ATTEMPTS"); do
+  PIN_JSON="$(curl -fsSL "${PIN_API_URL}?q=${REV}")"
+  ALL_OK=1
+
+  for PKG in "${CHECK_PACKAGES[@]}"; do
+    KEY="github:${OWNER_REPO}/${REV}#packages.${SYSTEM}.${PKG}"
+    STORE_PATH="$(
+      echo "$PIN_JSON" \
+        | jq -r --arg k "$KEY" 'map(select(.name == $k)) | first | (.lastRevision.storePath // .storePath // .store_path // .path // "")'
+    )"
+    if [ -z "$STORE_PATH" ]; then
+      PIN_STATUS="pin-missing"
+      PUSH_STATUS="000"
+      ALL_OK=0
+      {
+        echo "key-${PKG}: ${KEY}"
+        echo "pin-status-${PKG}: ${PIN_STATUS}"
+        echo "push-http-${PKG}: ${PUSH_STATUS}"
+      }
+      continue
+    fi
+
+    PIN_STATUS="pin-ok"
+    HASH="$(basename "$STORE_PATH" | cut -d- -f1)"
+    PUSH_NARINFO_URL="https://${CACHE}.cachix.org/${HASH}.narinfo"
+    PUSH_STATUS="$(curl -sS -o /dev/null -w '%{http_code}' "$PUSH_NARINFO_URL")" || PUSH_STATUS="000"
+    if [ "$PUSH_STATUS" != "200" ]; then
+      ALL_OK=0
+    fi
+
+    {
+      echo "key-${PKG}: ${KEY}"
+      echo "store-path-${PKG}: ${STORE_PATH}"
+      echo "pin-status-${PKG}: ${PIN_STATUS}"
+      echo "push-http-${PKG}: ${PUSH_STATUS}"
+    }
+  done
+
+  if [ "$ALL_OK" = "1" ]; then
+    echo "cachix-status: push-and-pin-ok-for-all-packages" >> "$SUMMARY"
+    exit 0
+  fi
+
+  echo "cachix-check-attempt-${i}: not-ready, retrying in ${PIN_VISIBILITY_INTERVAL_SECONDS}s"
+  sleep "$PIN_VISIBILITY_INTERVAL_SECONDS"
+done
+
+echo "cachix-status: push-or-pin-missing-after-${PIN_VISIBILITY_TIMEOUT_SECONDS}s-for-at-least-one-package" >> "$SUMMARY"
+exit 1

.github/workflows/release.yml

@@ -167,12 +167,17 @@ jobs:
         env:
           CACHIX_AUTH_TOKEN: '${{ secrets.CACHIX_PRIVATE_KFB_TOKEN }}'
           GC_DONT_GC: '1'
+          OWNER_REPO: '${{ github.repository }}'
+          REV: '${{ github.sha }}'
         with:
           packages: jq
           script: |
             export PATH="$(nix build github:runtimeverification/kup --no-link --json | jq -r '.[].outputs | to_entries[].value')/bin:$PATH"
-            kup publish k-framework-binary .#kmir --keep-days 180
-            kup publish k-framework-binary .#kmir.rust --keep-days 180
+            kup publish k-framework-binary .#kmir --keep-days 180 || true
+            kup publish k-framework-binary .#kmir.rust --keep-days 180 || true
+
+            # Cachix has not been responding to 'cachix pin' requests made under the hood by kup. So we need to manually verify the push and pin.
+            .github/scripts/check-cachix-pin.sh
 
       - name: 'On failure, delete drafted release'
         if: failure()

.github/workflows/test-cachix-pin.yml

@@ -0,0 +1,28 @@
+name: 'Test Cachix Pin'
+
+on:
+  workflow_dispatch:
+    inputs:
+      ref:
+        description: 'Git ref (tag or SHA) of an existing release to verify'
+        required: true
+        type: string
+
+jobs:
+  verify-cachix-pin:
+    name: 'Verify Cachix Pin'
+    runs-on: [self-hosted, linux, normal]
+    steps:
+      - name: 'Check out code'
+        uses: actions/checkout@v4
+
+      - name: 'Verify cachix publish and pin'
+        uses: workflow/nix-shell-action@v3
+        env:
+          CACHIX_AUTH_TOKEN: '${{ secrets.CACHIX_PRIVATE_KFB_TOKEN }}'
+          GC_DONT_GC: '1'
+          OWNER_REPO: '${{ github.repository }}'
+          REV: '${{ inputs.ref }}'
+        with:
+          packages: jq
+          script: bash .github/scripts/check-cachix-pin.sh

.github/workflows/update-dependencies.yml

@@ -50,7 +50,9 @@ jobs:
           git checkout "${VERSION}"
           cd ../..
           sed -i 's!__smir_version__: Final = '"'[0-9a-f]*'"'!__smir_version__: Final = '"'${VERSION}'"'!' kmir/src/kmir/__init__.py
-          git add deps/stable-mir-json kmir/src/kmir/__init__.py
+          CHANNEL=$(grep '^channel' deps/stable-mir-json/rust-toolchain.toml | sed 's!channel = "\(.*\)"!\1!')
+          sed -i 's!^channel = ".*"!channel = "'"${CHANNEL}"'"!' rust-toolchain.toml
+          git add deps/stable-mir-json kmir/src/kmir/__init__.py rust-toolchain.toml
           git commit -m "deps/stable-mir-json: sync submodule ${VERSION}" || true
       - name: 'Update Nix flake inputs'
         run: |

Makefile

@@ -21,6 +21,7 @@ test: test-unit test-integration smir-parse-tests
 stable-mir-json: CARGO_BUILD_OPTS =
 stable-mir-json:
 	cd deps/stable-mir-json && cargo build ${CARGO_BUILD_OPTS}
+	cd deps/stable-mir-json && cargo build --release ${CARGO_BUILD_OPTS}
 	cd deps/stable-mir-json && cargo run --bin cargo_stable_mir_json -- ${TOP_DIR}/deps/stable-mir-json ${TOP_DIR}/deps
 	${TOP_DIR}/deps/.stable-mir-json/release.sh --version || ${TOP_DIR}/deps/.stable-mir-json/debug.sh --version
 

deps/stable-mir-json_release

@@ -1 +1 @@
-a5b714d89d0c12c7f4b00602a95ad2d3a34530f0
+047ca6ac01786e1b616e13a216d70268b9785e17

flake.nix

@@ -6,7 +6,7 @@
 
     flake-utils.url = "github:numtide/flake-utils";
 
-    stable-mir-json-flake.url = "github:runtimeverification/stable-mir-json/a5b714d89d0c12c7f4b00602a95ad2d3a34530f0";
+    stable-mir-json-flake.url = "github:runtimeverification/stable-mir-json/047ca6ac01786e1b616e13a216d70268b9785e17";
     stable-mir-json-flake = {
       inputs.nixpkgs.follows = "nixpkgs";
       inputs.flake-utils.follows = "flake-utils";

kmir/src/kmir/__init__.py

@@ -2,4 +2,4 @@
 from typing import Final
 
 __version__: Final = version('kmir')
-__smir_version__: Final = 'a5b714d89d0c12c7f4b00602a95ad2d3a34530f0'
+__smir_version__: Final = '047ca6ac01786e1b616e13a216d70268b9785e17'

kmir/src/kmir/__main__.py

@@ -180,7 +180,7 @@ def _kmir_show(opts: ShowOpts) -> None:
     if opts.leaves:
         if lines and lines[-1] != '':
             lines.append('')
-        lines.extend(render_leaf_k_cells(proof, node_printer.cterm_show))
+        lines.extend(render_leaf_k_cells(proof, node_printer.cterm_show, smir_info=node_printer.smir_info))
 
     # Handle --to-module output
     if opts.to_module:
@@ -410,6 +410,13 @@ def _arg_parser() -> ArgumentParser:
         action='store_true',
         help='Break on every MIR step (statements and terminators)',
     )
+    prove_args.add_argument(
+        '--break-on-function',
+        dest='break_on_function',
+        action='append',
+        default=None,
+        help='Break when calling functions / intrinsics matching this name (repeatable)',
+    )
 
     proof_args = ArgumentParser(add_help=False)
     proof_args.add_argument('id', metavar='PROOF_ID', help='The id of the proof to view')
@@ -638,6 +645,7 @@ def _parse_args(ns: Namespace) -> KMirOpts:
                 break_every_step=ns.break_every_step,
                 terminate_on_thunk=ns.terminate_on_thunk,
                 add_module=ns.add_module,
+                break_on_function=ns.break_on_function or [],
             )
         case 'link':
             return LinkOpts(

kmir/src/kmir/_prove.py

@@ -63,6 +63,7 @@ def _prove_rs(opts: ProveRSOpts, target_path: Path, label: str) -> APRProof:
             symbolic=True,
             haskell_target=opts.haskell_target,
             llvm_lib_target=opts.llvm_lib_target,
+            break_on_function=opts.break_on_function or None,
         )
     else:
         _LOGGER.info(f'Constructing initial proof: {label}')
@@ -92,6 +93,7 @@ def _prove_rs(opts: ProveRSOpts, target_path: Path, label: str) -> APRProof:
             symbolic=True,
             haskell_target=opts.haskell_target,
             llvm_lib_target=opts.llvm_lib_target,
+            break_on_function=opts.break_on_function or None,
         )
 
         proof = apr_proof_from_smir(
@@ -122,6 +124,7 @@ def _prove_rs(opts: ProveRSOpts, target_path: Path, label: str) -> APRProof:
         break_on_terminator_unreachable=opts.break_on_terminator_unreachable,
         break_every_terminator=opts.break_every_terminator,
         break_every_step=opts.break_every_step,
+        break_on_function=opts.break_on_function,
     )
 
     if opts.max_workers and opts.max_workers > 1:
@@ -251,6 +254,7 @@ def _cut_point_rules(
     break_on_terminator_unreachable: bool,
     break_every_terminator: bool,
     break_every_step: bool,
+    break_on_function: list[str] | None = None,
 ) -> list[str]:
     cut_point_rules = []
     if break_on_thunk:
@@ -291,6 +295,9 @@ def _cut_point_rules(
         or break_every_step
     ):
         cut_point_rules.append('KMIR-CONTROL-FLOW.termCallFunction')
+    if break_on_function:
+        cut_point_rules.append('KMIR-CONTROL-FLOW.termCallFunctionFilter')
+        cut_point_rules.append('KMIR-CONTROL-FLOW.termCallIntrinsicFilter')
     if break_on_terminator_assert or break_every_terminator or break_every_step:
         cut_point_rules.append('KMIR-CONTROL-FLOW.termAssert')
     if break_on_terminator_drop or break_every_terminator or break_every_step:

kmir/src/kmir/kdist/mir-semantics/intrinsics.md

@@ -23,7 +23,7 @@ its argument to the destination without modification.
 
 ```k
   // Black box intrinsic implementation - identity function
-  rule <k> #execIntrinsic(IntrinsicFunction(symbol("black_box")), ARG:Operand .Operands, DEST)
+  rule <k> #execIntrinsic(IntrinsicFunction(symbol("black_box")), ARG:Operand .Operands, DEST, _SPAN)
         => #setLocalValue(DEST, ARG)
        ... </k>
 ```
@@ -36,7 +36,7 @@ a NO OP for program semantics. `std::intrinsics::likely` and `std::intrinsics::u
 "normal" `MonoItemFn`s that call the `cold_path` intrinsic.
 
 ```k
-  rule <k> #execIntrinsic(IntrinsicFunction(symbol("cold_path")), .Operands, _DEST) => .K ... </k>
+  rule <k> #execIntrinsic(IntrinsicFunction(symbol("cold_path")), .Operands, _DEST, _SPAN) => .K ... </k>
 ```
 
 #### Prefetch (`std::intrinsics::prefetch_*`)
@@ -46,11 +46,11 @@ intrinsics in Rust are performance hints that request the CPU to load or prepare
 before it's used. They have no effect on program semantics, and are implemented as a NO OP in this semantics.
 
 ```k
-  rule <k> #execIntrinsic(IntrinsicFunction(symbol("prefetch_read_data")),  _ARG1:Operand _ARG2:Operand .Operands, _DEST) => .K ... </k>
-  rule <k> #execIntrinsic(IntrinsicFunction(symbol("prefetch_write_data")), _ARG1:Operand _ARG2:Operand .Operands, _DEST) => .K ... </k>
+  rule <k> #execIntrinsic(IntrinsicFunction(symbol("prefetch_read_data")),  _ARG1:Operand _ARG2:Operand .Operands, _DEST, _SPAN) => .K ... </k>
+  rule <k> #execIntrinsic(IntrinsicFunction(symbol("prefetch_write_data")), _ARG1:Operand _ARG2:Operand .Operands, _DEST, _SPAN) => .K ... </k>
 
-  rule <k> #execIntrinsic(IntrinsicFunction(symbol("prefetch_read_instruction")),  _ARG1:Operand _ARG2:Operand .Operands, _DEST) => .K ... </k>
-  rule <k> #execIntrinsic(IntrinsicFunction(symbol("prefetch_write_instruction")), _ARG1:Operand _ARG2:Operand .Operands, _DEST) => .K ... </k>
+  rule <k> #execIntrinsic(IntrinsicFunction(symbol("prefetch_read_instruction")),  _ARG1:Operand _ARG2:Operand .Operands, _DEST, _SPAN) => .K ... </k>
+  rule <k> #execIntrinsic(IntrinsicFunction(symbol("prefetch_write_instruction")), _ARG1:Operand _ARG2:Operand .Operands, _DEST, _SPAN) => .K ... </k>
 ```
 
 #### Assert Inhabited (`std::intrinsics::assert_inhabited`)
@@ -63,13 +63,13 @@ error with `#AssertInhabitedFailure` if we see that following the intrinsic. Oth
 
 ```k
   syntax MIRError ::= "AssertInhabitedFailure"
-  rule <k> #execIntrinsic(IntrinsicFunction(symbol("assert_inhabited")), .Operands, _DEST)
+  rule <k> #execIntrinsic(IntrinsicFunction(symbol("assert_inhabited")), .Operands, _DEST, _SPAN)
             ~> #continueAt(noBasicBlockIdx)
         => AssertInhabitedFailure
        ...
       </k>
 
-  rule <k> #execIntrinsic(IntrinsicFunction(symbol("assert_inhabited")), .Operands, _DEST)
+  rule <k> #execIntrinsic(IntrinsicFunction(symbol("assert_inhabited")), .Operands, _DEST, _SPAN)
         => .K
        ...
       </k>
@@ -88,7 +88,7 @@ Execution gets stuck (no matching rule) when operands have different types or un
 
 ```k
   // Raw eq: dereference operands, extract types, and delegate to typed comparison
-  rule <k> #execIntrinsic(IntrinsicFunction(symbol("raw_eq")), ARG1:Operand ARG2:Operand .Operands, PLACE)
+  rule <k> #execIntrinsic(IntrinsicFunction(symbol("raw_eq")), ARG1:Operand ARG2:Operand .Operands, PLACE, _SPAN)
         => #execRawEqTyped(PLACE, #withDeref(ARG1), #extractOperandType(#withDeref(ARG1), LOCALS),
                                   #withDeref(ARG2), #extractOperandType(#withDeref(ARG2), LOCALS))
        ... </k>
@@ -134,11 +134,11 @@ through a dereferenced pointer. We extract the place from the pointer operand, a
 write the value to that location.
 
 ```k
-  rule <k> #execIntrinsic(IntrinsicFunction(symbol("volatile_store")), operandCopy(place(LOCAL, PROJ)) ARG2:Operand .Operands, _DEST)
+  rule <k> #execIntrinsic(IntrinsicFunction(symbol("volatile_store")), operandCopy(place(LOCAL, PROJ)) ARG2:Operand .Operands, _DEST, _SPAN)
         => #setLocalValue(place(LOCAL, appendP(PROJ, projectionElemDeref .ProjectionElems)), ARG2)
        ... </k>
 
-  rule <k> #execIntrinsic(IntrinsicFunction(symbol("volatile_store")), operandMove(place(LOCAL, PROJ)) ARG2:Operand .Operands, _DEST)
+  rule <k> #execIntrinsic(IntrinsicFunction(symbol("volatile_store")), operandMove(place(LOCAL, PROJ)) ARG2:Operand .Operands, _DEST, _SPAN)
         => #setLocalValue(place(LOCAL, appendP(PROJ, projectionElemDeref .ProjectionElems)), ARG2)
        ... </k>
 ```
@@ -153,12 +153,12 @@ the second argument, so the returned difference is always positive.
 
 
 ```k
-  rule <k> #execIntrinsic(IntrinsicFunction(symbol("ptr_offset_from")), ARG1:Operand ARG2:Operand .Operands, DEST)
+  rule <k> #execIntrinsic(IntrinsicFunction(symbol("ptr_offset_from")), ARG1:Operand ARG2:Operand .Operands, DEST, _SPAN)
         => #ptrOffsetDiff(ARG1, ARG2, true, DEST)
         ...
        </k>
 
-  rule <k> #execIntrinsic(IntrinsicFunction(symbol("ptr_offset_from_unsigned")), ARG1:Operand ARG2:Operand .Operands, DEST)
+  rule <k> #execIntrinsic(IntrinsicFunction(symbol("ptr_offset_from_unsigned")), ARG1:Operand ARG2:Operand .Operands, DEST, _SPAN)
         => #ptrOffsetDiff(ARG1, ARG2, false, DEST)
         ...
        </k>