From 69a50fc7dc2774706dd3379d6e703dcf355dc390 Mon Sep 17 00:00:00 2001
From: Jost Berthold <jost.berthold@gmail.com>
Date: Mon, 13 Oct 2025 08:30:36 +1100
Subject: [PATCH 01/15] Tweak proof-running workflow

* add some proofs with runtime < 1h as defaults
* use self-hosted linux runners (normal)
* always store artefacts after running
* use timeout 2h for running the proof, ~3h for the daemon
---
 .github/workflows/rv-run-proofs.yaml | 15 ++++++++-------
 1 file changed, 8 insertions(+), 7 deletions(-)

diff --git a/.github/workflows/rv-run-proofs.yaml b/.github/workflows/rv-run-proofs.yaml
index 43580310..1876a8c6 100644
--- a/.github/workflows/rv-run-proofs.yaml
+++ b/.github/workflows/rv-run-proofs.yaml
@@ -7,7 +7,7 @@ on:
         description: Start symbols for proofs to run
         required: true
         type: string
-        default: "['test_ptoken_domain_data', 'this_will_fail']"
+        default: "['test_ptoken_domain_data', test_process_approve, test_process_get_account_data_size, test_process_initialize_immutable_owner]"
       kmir:
         description: KMIR to work with (must exist as a docker image tag, optional)
         required: false
@@ -44,7 +44,7 @@ jobs:
         with:
           flakes: github:runtimeverification/stable-mir-json/${{ inputs.smir }}
 
-      - name: "Build with stable_mir_json"      
+      - name: "Build with stable_mir_json"
         run: |
           cd p-token
           RUSTC=stable_mir_json cargo build --features runtime-verification
@@ -71,10 +71,10 @@ jobs:
 
   run_proof:
     name: "Link SMIR and Run Proofs"
-    needs: 
+    needs:
       - compile
       - prepare_matrix
-    runs-on: ubuntu-latest
+    runs-on: [self-hosted, linux, normal]
     # container:
     #   image: runtimeverificationinc/kmir:${{ inputs.kmir }}
     strategy:
@@ -96,7 +96,7 @@ jobs:
             -v $PWD:/workdir --workdir /workdir \
             --name "${KMIR_CONTAINER_NAME}" \
             runtimeverificationinc/kmir:${{ inputs.kmir }} \
-            sleep 3600
+            sleep 10000
           sleep 10
 
       - name: "Get SMIR Files"
@@ -112,7 +112,7 @@ jobs:
 
       - name: "Run Proof ${{ matrix.proof }} and store resulting tree"
         run: |
-          timeout 3600 \
+          timeout 7200 \
             docker exec --workdir /workdir "${KMIR_CONTAINER_NAME}" \
               kmir prove-rs --smir artefacts/p-token.smir.json \
               --start-symbol 'pinocchio_token_program::entrypoint::${{ matrix.proof }}' \
@@ -120,11 +120,12 @@ jobs:
               --max-iterations 100 \
               --proof-dir artefacts/proof
           docker exec --workdir /workdir "${KMIR_CONTAINER_NAME}" \
-            kmir show --full-printer --proof-dir artefacts/proof \
+            kmir show --statistics --leaves --proof-dir artefacts/proof \
             'p-token.smir.pinocchio_token_program::entrypoint::${{ matrix.proof }}' \
             > artefacts/proof/${{ matrix.proof }}-full.txt
 
       - name: "Save proof tree and smir"
+        if: always()
         uses: actions/upload-artifact@v4
         with:
           name: $artefacts-{{ matrix.proof }}

From 382bd60091b50085cdb24b44fa6e2e6a9453590e Mon Sep 17 00:00:00 2001
From: Jost Berthold <jost.berthold@gmail.com>
Date: Mon, 13 Oct 2025 08:33:17 +1100
Subject: [PATCH 02/15] better quote the proofs in the list

---
 .github/workflows/rv-run-proofs.yaml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/rv-run-proofs.yaml b/.github/workflows/rv-run-proofs.yaml
index 1876a8c6..c7d4465f 100644
--- a/.github/workflows/rv-run-proofs.yaml
+++ b/.github/workflows/rv-run-proofs.yaml
@@ -7,7 +7,7 @@ on:
         description: Start symbols for proofs to run
         required: true
         type: string
-        default: "['test_ptoken_domain_data', test_process_approve, test_process_get_account_data_size, test_process_initialize_immutable_owner]"
+        default: "['test_ptoken_domain_data', 'test_process_approve', 'test_process_get_account_data_size', 'test_process_initialize_immutable_owner']"
       kmir:
         description: KMIR to work with (must exist as a docker image tag, optional)
         required: false

From 6ba670a22f1b2f1c8be58212bd21bc09a8c80ca6 Mon Sep 17 00:00:00 2001
From: Jost Berthold <jost.berthold@gmail.com>
Date: Mon, 13 Oct 2025 09:04:24 +1100
Subject: [PATCH 03/15] update default KMIR image tag

---
 .github/workflows/rv-run-proofs.yaml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/rv-run-proofs.yaml b/.github/workflows/rv-run-proofs.yaml
index c7d4465f..9158eb49 100644
--- a/.github/workflows/rv-run-proofs.yaml
+++ b/.github/workflows/rv-run-proofs.yaml
@@ -12,7 +12,7 @@ on:
         description: KMIR to work with (must exist as a docker image tag, optional)
         required: false
         type: string
-        default: p-token-f8c403f # hard-wired now, retrieve from submodule later
+        default: p-token-024f2d3 # hard-wired now, retrieve from submodule later
       smir:
         description: Stable MIR JSON to work with (commit hash, optional)
         required: false

From d2fa77359abf05b0cefd79a6e782540350463e93 Mon Sep 17 00:00:00 2001
From: Jost Berthold <jost.berthold@gmail.com>
Date: Mon, 13 Oct 2025 09:50:05 +1100
Subject: [PATCH 04/15] limit depth to 500

---
 .github/workflows/rv-run-proofs.yaml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.github/workflows/rv-run-proofs.yaml b/.github/workflows/rv-run-proofs.yaml
index 9158eb49..fe843964 100644
--- a/.github/workflows/rv-run-proofs.yaml
+++ b/.github/workflows/rv-run-proofs.yaml
@@ -117,6 +117,7 @@ jobs:
               kmir prove-rs --smir artefacts/p-token.smir.json \
               --start-symbol 'pinocchio_token_program::entrypoint::${{ matrix.proof }}' \
               --verbose \
+              --max-depth 500 \
               --max-iterations 100 \
               --proof-dir artefacts/proof
           docker exec --workdir /workdir "${KMIR_CONTAINER_NAME}" \

From 4e38d17331c7b1b3fc65f563778b362a0e3843bd Mon Sep 17 00:00:00 2001
From: Jost Berthold <jost.berthold@gmail.com>
Date: Mon, 13 Oct 2025 10:08:14 +1100
Subject: [PATCH 05/15] debug: try creating proof directory beforehand. Correct
 artefact name

---
 .github/workflows/rv-run-proofs.yaml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/rv-run-proofs.yaml b/.github/workflows/rv-run-proofs.yaml
index fe843964..66a3cb57 100644
--- a/.github/workflows/rv-run-proofs.yaml
+++ b/.github/workflows/rv-run-proofs.yaml
@@ -112,6 +112,8 @@ jobs:
 
       - name: "Run Proof ${{ matrix.proof }} and store resulting tree"
         run: |
+          docker exec --workdir /workdir "${KMIR_CONTAINER_NAME}" \
+            bash -c "ls -la artefacts; mkdir -p artefacts/proof; ls -la artefacts"
           timeout 7200 \
             docker exec --workdir /workdir "${KMIR_CONTAINER_NAME}" \
               kmir prove-rs --smir artefacts/p-token.smir.json \
@@ -129,7 +131,7 @@ jobs:
         if: always()
         uses: actions/upload-artifact@v4
         with:
-          name: $artefacts-{{ matrix.proof }}
+          name: $artefacts-${{ matrix.proof }}
           path: |
             artefacts/p-token.smir.json
             artefacts/proof/*-full.txt

From 4701385a70a3bd0863bd977358befa8fbd678636 Mon Sep 17 00:00:00 2001
From: Jost Berthold <jost.berthold@gmail.com>
Date: Mon, 13 Oct 2025 11:15:46 +1100
Subject: [PATCH 06/15] DEBUG logging for kore-rpc-booster to determine crash
 reason

---
 .github/workflows/rv-run-proofs.yaml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/rv-run-proofs.yaml b/.github/workflows/rv-run-proofs.yaml
index 66a3cb57..9ae85c92 100644
--- a/.github/workflows/rv-run-proofs.yaml
+++ b/.github/workflows/rv-run-proofs.yaml
@@ -115,7 +115,9 @@ jobs:
           docker exec --workdir /workdir "${KMIR_CONTAINER_NAME}" \
             bash -c "ls -la artefacts; mkdir -p artefacts/proof; ls -la artefacts"
           timeout 7200 \
-            docker exec --workdir /workdir "${KMIR_CONTAINER_NAME}" \
+            docker exec \
+              --env KORE_RPC_OPTS="--log-context *>depth. --log-context *>proxy" \
+              --workdir /workdir "${KMIR_CONTAINER_NAME}" \
               kmir prove-rs --smir artefacts/p-token.smir.json \
               --start-symbol 'pinocchio_token_program::entrypoint::${{ matrix.proof }}' \
               --verbose \
@@ -131,7 +133,7 @@ jobs:
         if: always()
         uses: actions/upload-artifact@v4
         with:
-          name: $artefacts-${{ matrix.proof }}
+          name: artefacts-${{ matrix.proof }}
           path: |
             artefacts/p-token.smir.json
             artefacts/proof/*-full.txt

From 5b1caa7e2123f81be7327b10ccc42edca20f8ceb Mon Sep 17 00:00:00 2001
From: Jost Berthold <jost.berthold@gmail.com>
Date: Mon, 13 Oct 2025 11:59:58 +1100
Subject: [PATCH 07/15] DEBUG wipe artefacts directory before starting docker
 container

---
 .github/workflows/rv-run-proofs.yaml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.github/workflows/rv-run-proofs.yaml b/.github/workflows/rv-run-proofs.yaml
index 9ae85c92..2bb4164e 100644
--- a/.github/workflows/rv-run-proofs.yaml
+++ b/.github/workflows/rv-run-proofs.yaml
@@ -91,6 +91,7 @@ jobs:
       - name: "Set up Docker Host"
         run: |
           mkdir -p $PWD/artefacts
+          ls -l $PWD/artefacts && rm -rf $PWD/artefacts/*
           chmod a+rwx $PWD/artefacts
           docker run --rm --detach \
             -v $PWD:/workdir --workdir /workdir \

From 1621c46d7afe3832b20a0ad6b4d3b011f3ada851 Mon Sep 17 00:00:00 2001
From: Jost Berthold <jost.berthold@gmail.com>
Date: Mon, 13 Oct 2025 19:31:46 +1100
Subject: [PATCH 08/15] DEBUG log LLVM interactions of the server

---
 .github/workflows/rv-run-proofs.yaml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/rv-run-proofs.yaml b/.github/workflows/rv-run-proofs.yaml
index 2bb4164e..cc8860b8 100644
--- a/.github/workflows/rv-run-proofs.yaml
+++ b/.github/workflows/rv-run-proofs.yaml
@@ -117,12 +117,12 @@ jobs:
             bash -c "ls -la artefacts; mkdir -p artefacts/proof; ls -la artefacts"
           timeout 7200 \
             docker exec \
-              --env KORE_RPC_OPTS="--log-context *>depth. --log-context *>proxy" \
+              --env KORE_RPC_OPTS="--log-context *>depth. --log-context *>proxy --log-context *>llvm" \
               --workdir /workdir "${KMIR_CONTAINER_NAME}" \
               kmir prove-rs --smir artefacts/p-token.smir.json \
               --start-symbol 'pinocchio_token_program::entrypoint::${{ matrix.proof }}' \
               --verbose \
-              --max-depth 500 \
+              --max-depth 10 \
               --max-iterations 100 \
               --proof-dir artefacts/proof
           docker exec --workdir /workdir "${KMIR_CONTAINER_NAME}" \

From 83ce4c5343f1207377e7e8a03dd31b890283a80e Mon Sep 17 00:00:00 2001
From: Jost Berthold <jost.berthold@gmail.com>
Date: Mon, 13 Oct 2025 20:06:39 +1100
Subject: [PATCH 09/15] DEBUG make work directory world-writeable to appease
 LLVM backend

---
 .github/workflows/rv-run-proofs.yaml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/rv-run-proofs.yaml b/.github/workflows/rv-run-proofs.yaml
index cc8860b8..d3c54d3f 100644
--- a/.github/workflows/rv-run-proofs.yaml
+++ b/.github/workflows/rv-run-proofs.yaml
@@ -92,7 +92,7 @@ jobs:
         run: |
           mkdir -p $PWD/artefacts
           ls -l $PWD/artefacts && rm -rf $PWD/artefacts/*
-          chmod a+rwx $PWD/artefacts
+          chmod a+rwx $PWD/artefacts $PWD
           docker run --rm --detach \
             -v $PWD:/workdir --workdir /workdir \
             --name "${KMIR_CONTAINER_NAME}" \
@@ -117,7 +117,7 @@ jobs:
             bash -c "ls -la artefacts; mkdir -p artefacts/proof; ls -la artefacts"
           timeout 7200 \
             docker exec \
-              --env KORE_RPC_OPTS="--log-context *>depth. --log-context *>proxy --log-context *>llvm" \
+              --env KORE_RPC_OPTS="--log-context *>depth. --log-context *>proxy " \
               --workdir /workdir "${KMIR_CONTAINER_NAME}" \
               kmir prove-rs --smir artefacts/p-token.smir.json \
               --start-symbol 'pinocchio_token_program::entrypoint::${{ matrix.proof }}' \

From 28f1bee8334bfcafdf1931ed66bdd3ccb99a4093 Mon Sep 17 00:00:00 2001
From: Jost Berthold <jost.berthold@gmail.com>
Date: Mon, 13 Oct 2025 20:12:06 +1100
Subject: [PATCH 10/15] remove server debug logging

---
 .github/workflows/rv-run-proofs.yaml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/.github/workflows/rv-run-proofs.yaml b/.github/workflows/rv-run-proofs.yaml
index d3c54d3f..a93d1b86 100644
--- a/.github/workflows/rv-run-proofs.yaml
+++ b/.github/workflows/rv-run-proofs.yaml
@@ -117,12 +117,11 @@ jobs:
             bash -c "ls -la artefacts; mkdir -p artefacts/proof; ls -la artefacts"
           timeout 7200 \
             docker exec \
-              --env KORE_RPC_OPTS="--log-context *>depth. --log-context *>proxy " \
               --workdir /workdir "${KMIR_CONTAINER_NAME}" \
               kmir prove-rs --smir artefacts/p-token.smir.json \
               --start-symbol 'pinocchio_token_program::entrypoint::${{ matrix.proof }}' \
               --verbose \
-              --max-depth 10 \
+              --max-depth 500 \
               --max-iterations 100 \
               --proof-dir artefacts/proof
           docker exec --workdir /workdir "${KMIR_CONTAINER_NAME}" \

From 6b6b451a5375384f1899299cbd65513f038e02a7 Mon Sep 17 00:00:00 2001
From: Jost Berthold <jost.berthold@gmail.com>
Date: Wed, 15 Oct 2025 11:38:43 +1100
Subject: [PATCH 11/15] Tweak workflow: updated kmir image, timeout, use user,
 tolerate failing proofs, clean up artefacts

---
 .github/workflows/rv-run-proofs.yaml | 21 +++++++++++++++++----
 1 file changed, 17 insertions(+), 4 deletions(-)

diff --git a/.github/workflows/rv-run-proofs.yaml b/.github/workflows/rv-run-proofs.yaml
index a93d1b86..b017e5c0 100644
--- a/.github/workflows/rv-run-proofs.yaml
+++ b/.github/workflows/rv-run-proofs.yaml
@@ -12,12 +12,17 @@ on:
         description: KMIR to work with (must exist as a docker image tag, optional)
         required: false
         type: string
-        default: p-token-024f2d3 # hard-wired now, retrieve from submodule later
+        default: p-token-3bd9b7c # empty = retrieve from submodule (later)
       smir:
         description: Stable MIR JSON to work with (commit hash, optional)
         required: false
         type: string
         default:  # empty = master
+      timeout:
+        description: Timeout for running the proofs
+        required: false
+        type: string
+        default: 7200 # 2h
 concurrency:
   group: ${{ github.workflow }}-${{ github.ref }}
   cancel-in-progress: true
@@ -94,10 +99,11 @@ jobs:
           ls -l $PWD/artefacts && rm -rf $PWD/artefacts/*
           chmod a+rwx $PWD/artefacts $PWD
           docker run --rm --detach \
+            -u $(id -u):$(id -g) \
             -v $PWD:/workdir --workdir /workdir \
             --name "${KMIR_CONTAINER_NAME}" \
             runtimeverificationinc/kmir:${{ inputs.kmir }} \
-            sleep 10000
+            bash -c 'while true; do sleep 600; done'
           sleep 10
 
       - name: "Get SMIR Files"
@@ -115,7 +121,7 @@ jobs:
         run: |
           docker exec --workdir /workdir "${KMIR_CONTAINER_NAME}" \
             bash -c "ls -la artefacts; mkdir -p artefacts/proof; ls -la artefacts"
-          timeout 7200 \
+          timeout ${{ inputs.timeout }} \
             docker exec \
               --workdir /workdir "${KMIR_CONTAINER_NAME}" \
               kmir prove-rs --smir artefacts/p-token.smir.json \
@@ -123,7 +129,9 @@ jobs:
               --verbose \
               --max-depth 500 \
               --max-iterations 100 \
-              --proof-dir artefacts/proof
+              --proof-dir artefacts/proof \
+            || echo "Runner signals proof failure"
+
           docker exec --workdir /workdir "${KMIR_CONTAINER_NAME}" \
             kmir show --statistics --leaves --proof-dir artefacts/proof \
             'p-token.smir.pinocchio_token_program::entrypoint::${{ matrix.proof }}' \
@@ -144,3 +152,8 @@ jobs:
           docker stop ${KMIR_CONTAINER_NAME}
           sleep 5
           docker rm -f ${KMIR_CONTAINER_NAME}
+
+      - name: "Clean up artefacts directory"
+        if: always()
+        run: |
+          rm -rf $PWD/artefacts

From 687c3283c3ef6e1ffffd3e8caaf4d229591bb7f3 Mon Sep 17 00:00:00 2001
From: Jost Berthold <jost.berthold@gmail.com>
Date: Wed, 15 Oct 2025 15:04:27 +1100
Subject: [PATCH 12/15] select KMIR version from submodule if not provided

---
 .github/workflows/rv-run-proofs.yaml  | 20 +++++++++++++++++---
 p-token/test-properties/mir-semantics |  2 +-
 2 files changed, 18 insertions(+), 4 deletions(-)

diff --git a/.github/workflows/rv-run-proofs.yaml b/.github/workflows/rv-run-proofs.yaml
index b017e5c0..8cd3b4a3 100644
--- a/.github/workflows/rv-run-proofs.yaml
+++ b/.github/workflows/rv-run-proofs.yaml
@@ -67,12 +67,26 @@ jobs:
     runs-on: ubuntu-latest
     outputs:
       proofs: ${{ steps.split.outputs.matrix }}
+      kmir: ${{ steps.kmir.outputs.kmir }}
     steps:
+      - name: "Git Checkout"
+        uses: actions/checkout@v4
+
       - name: "Create Proof Array"
         id: split
         run: |
           echo "proofs = '${{ inputs.proofs }}'"
           echo "matrix=${{ inputs.proofs }}" >> $GITHUB_OUTPUT
+      - name: "Set KMIR version"
+        id: kmir
+        run: |
+          if [ ! -z "${{ inputs.kmir }}" ]; then
+              echo "KMIR version set to ${{ inputs.kmir }}"
+              kmir=${{ inputs.kmir }}
+          else
+              kmir=p-token-$(git rev-parse --short $(git ls-tree HEAD mir-semantics/ | awk '{print $3}'))
+          fi
+          echo "kmir=$kmir" >> $GITHUB_OUTPUT
 
   run_proof:
     name: "Link SMIR and Run Proofs"
@@ -81,7 +95,7 @@ jobs:
       - prepare_matrix
     runs-on: [self-hosted, linux, normal]
     # container:
-    #   image: runtimeverificationinc/kmir:${{ inputs.kmir }}
+    #   image: runtimeverificationinc/kmir:${{ needs.prepare_matrix.outputs.kmir }}
     strategy:
       matrix:
         proof: ${{ fromJSON(needs.prepare_matrix.outputs.proofs) }}
@@ -91,7 +105,7 @@ jobs:
       - name: debug matrix and docker image
         run: |
           echo "This is proof ${{ matrix.proof }}"
-          echo "Running with $KMIR_CONTAINER_NAME, docker image runtimeverificationinc/kmir:${{ inputs.kmir }}"
+          echo "Running with $KMIR_CONTAINER_NAME, docker image runtimeverificationinc/kmir:${{ needs.prepare_matrix.outputs.kmir }}"
 
       - name: "Set up Docker Host"
         run: |
@@ -102,7 +116,7 @@ jobs:
             -u $(id -u):$(id -g) \
             -v $PWD:/workdir --workdir /workdir \
             --name "${KMIR_CONTAINER_NAME}" \
-            runtimeverificationinc/kmir:${{ inputs.kmir }} \
+            runtimeverificationinc/kmir:${{ needs.prepare_matrix.outputs.kmir }} \
             bash -c 'while true; do sleep 600; done'
           sleep 10
 
diff --git a/p-token/test-properties/mir-semantics b/p-token/test-properties/mir-semantics
index 3bd9b7c3..6b3b8bd2 160000
--- a/p-token/test-properties/mir-semantics
+++ b/p-token/test-properties/mir-semantics
@@ -1 +1 @@
-Subproject commit 3bd9b7c390eacf2db7932eacb09ca6c534fdd6df
+Subproject commit 6b3b8bd23aee3988c9a2002a0f224e61356a724d

From 2c187dfeda545c64736fac84bcdd8e1b99606209 Mon Sep 17 00:00:00 2001
From: Jost Berthold <jost.berthold@gmail.com>
Date: Wed, 15 Oct 2025 15:09:17 +1100
Subject: [PATCH 13/15] explicitly empty input parameter kmir

---
 .github/workflows/rv-run-proofs.yaml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/rv-run-proofs.yaml b/.github/workflows/rv-run-proofs.yaml
index 8cd3b4a3..41f9d4ed 100644
--- a/.github/workflows/rv-run-proofs.yaml
+++ b/.github/workflows/rv-run-proofs.yaml
@@ -12,7 +12,7 @@ on:
         description: KMIR to work with (must exist as a docker image tag, optional)
         required: false
         type: string
-        default: p-token-3bd9b7c # empty = retrieve from submodule (later)
+        default: # empty = retrieve from submodule (later)
       smir:
         description: Stable MIR JSON to work with (commit hash, optional)
         required: false

From 9a76a7b1d669ac69d491ddbd662ee541e7c0bb67 Mon Sep 17 00:00:00 2001
From: Jost Berthold <jost.berthold@gmail.com>
Date: Wed, 15 Oct 2025 15:11:05 +1100
Subject: [PATCH 14/15] use correct path for submodule

---
 .github/workflows/rv-run-proofs.yaml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/rv-run-proofs.yaml b/.github/workflows/rv-run-proofs.yaml
index 41f9d4ed..01ee57bd 100644
--- a/.github/workflows/rv-run-proofs.yaml
+++ b/.github/workflows/rv-run-proofs.yaml
@@ -84,7 +84,7 @@ jobs:
               echo "KMIR version set to ${{ inputs.kmir }}"
               kmir=${{ inputs.kmir }}
           else
-              kmir=p-token-$(git rev-parse --short $(git ls-tree HEAD mir-semantics/ | awk '{print $3}'))
+              kmir=p-token-$(git rev-parse --short $(git ls-tree HEAD p-token/test-properties/mir-semantics/ | awk '{print $3}'))
           fi
           echo "kmir=$kmir" >> $GITHUB_OUTPUT
 

From 0a34390bb76ec4eb4198e74a9f1061ca96c7480c Mon Sep 17 00:00:00 2001
From: Jost Berthold <jost.berthold@gmail.com>
Date: Wed, 15 Oct 2025 15:16:36 +1100
Subject: [PATCH 15/15] reset submodule to proofs branch version

---
 p-token/test-properties/mir-semantics | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/p-token/test-properties/mir-semantics b/p-token/test-properties/mir-semantics
index 6b3b8bd2..3bd9b7c3 160000
--- a/p-token/test-properties/mir-semantics
+++ b/p-token/test-properties/mir-semantics
@@ -1 +1 @@
-Subproject commit 6b3b8bd23aee3988c9a2002a0f224e61356a724d
+Subproject commit 3bd9b7c390eacf2db7932eacb09ca6c534fdd6df