pure/loops: skip output reordering when the ok-tuple is not a permutation of the loop outputs

.github/workflows/release.yml

@@ -40,36 +40,44 @@ jobs:
   build:
     name: Build (${{ matrix.artifact_name }})
     needs: prepare
-    runs-on: ${{ matrix.os }}
+    # The self-hosted runner only exists on aeneasverif/aeneas. On forks (and
+    # any other repo), fall back to the GitHub-hosted `matrix.os` runner.
+    runs-on: ${{ (matrix.self_hosted && github.repository == 'aeneasverif/aeneas') && fromJSON('["self-hosted","linux","nix"]') || matrix.os }}
     permissions:
       contents: write
       actions: write
+    env:
+      # True only when actually running on the self-hosted runner (which has
+      # nix pre-installed).
+      is_self_hosted: ${{ matrix.self_hosted && github.repository == 'aeneasverif/aeneas' }}
     strategy:
       fail-fast: false
       matrix:
         include:
-          - os: [self-hosted, linux, nix]
+          # On the main repo this runs on the self-hosted runner; on forks it
+          # falls back to `os` (see `runs-on` and `is_self_hosted` above).
+          - os: ubuntu-24.04
             artifact_name: aeneas-linux-x86_64
             nix_attr: aeneas-static-release
-            nix_machine: true
+            self_hosted: true
           - os: ubuntu-24.04-arm
             artifact_name: aeneas-linux-aarch64
             nix_attr: aeneas-static-release
-            nix_machine: false
+            self_hosted: false
           - os: macos-15-intel
             artifact_name: aeneas-macos-x86_64
             nix_attr: aeneas-release
-            nix_machine: false
+            self_hosted: false
           - os: macos-latest
             artifact_name: aeneas-macos-aarch64
             nix_attr: aeneas-release
-            nix_machine: false
+            self_hosted: false
 
     steps:
       - uses: actions/checkout@v4
 
       - name: Install nix
-        if: ${{ ! matrix.nix_machine }}
+        if: ${{ env.is_self_hosted != 'true' }}
         uses: nixbuild/nix-quick-install-action@v30
         with:
           nix_conf: |
@@ -79,7 +87,7 @@ jobs:
             extra-trusted-public-keys = hacl.cachix.org-1:FzsZ2xsByOwKwIWNPII7yMOelJNDZ12mDAj3d1eGX0c=
 
       - name: Restore Nix Cache
-        if: ${{ ! matrix.nix_machine }}
+        if: ${{ env.is_self_hosted != 'true' }}
         id: restore-nix-cache
         uses: nix-community/cache-nix-action/restore@v6
         with:
@@ -102,7 +110,7 @@ jobs:
           chmod -R +w dist_staging
 
       - name: Install elan (Lean toolchain manager)
-        if: ${{ ! matrix.nix_machine }}
+        if: ${{ env.is_self_hosted != 'true' }}
         run: |
           set -eo pipefail
 
@@ -123,7 +131,7 @@ jobs:
 
           script="$PWD/scripts/ci-precompile-lean.sh"
           cd dist_staging/backends/lean
-          if [[ "${{ matrix.nix_machine }}" == "true" ]]; then
+          if [[ "$is_self_hosted" == "true" ]]; then
             nix develop ../../.. --command "$script"
           else
             "$script"
@@ -171,7 +179,7 @@ jobs:
           files: ${{ matrix.artifact_name }}.tar.gz
 
       - name: Save Nix Cache
-        if: ${{ always() && ! matrix.nix_machine }}
+        if: ${{ always() && env.is_self_hosted != 'true' }}
         uses: nix-community/cache-nix-action/save@v6
         with:
           primary-key: ${{ steps.restore-nix-cache.outputs.primary-key }}

.github/workflows/select-runner.yml

@@ -16,6 +16,8 @@ jobs:
       runs_on: ${{ steps.select.outputs.runs_on }}
     steps:
       - id: select
+        env:
+          current_repository: ${{ github.repository }}
         run: |
           set -euo pipefail
 
@@ -24,6 +26,14 @@ jobs:
           github_hosted='["ubuntu-latest"]'
           max_age_seconds=$((3 * 60 * 60))
 
+          # The self-hosted runner is only available on the main Aeneas repo.
+          # On forks (and any other repo), always fall back to GitHub-hosted.
+          if [ "$current_repository" != "aeneasverif/aeneas" ]; then
+            echo "::notice title=Not on aeneasverif/aeneas::Selecting GitHub-hosted runner; current repository is ${current_repository}."
+            echo "runs_on=$github_hosted" >> "$GITHUB_OUTPUT"
+            exit 0
+          fi
+
           query_error="$(mktemp)"
           if default_branch=$(curl -fsSL "https://api.github.com/repos/${heartbeat_repository}" 2>"$query_error" | jq -r .default_branch); then
             :

backends/lean/Aeneas/Std/Array/Array.lean

@@ -116,9 +116,11 @@ theorem Array.repeat_val (n : Usize) (x : α) : (Array.repeat n x).val = List.re
   simp only [Array.repeat]
 
 @[step]
-theorem Array.index_usize_spec {α : Type u} {n : Usize} (v: Array α n) (i: Usize)
-  (hbound : i.val < v.length) :
-  (v.index_usize i) ⦃ x => x = v.val[i.val] ⦄ := by
+theorem Array.index_usize_spec {α : Type u} {n : Usize} (v: Array α n) (i: Usize) :
+    partialSpec (v.index_usize i)
+      (fun x => ∃ _ : i.val < v.length, x = v.val[i.val])
+      (fun | .arrayOutOfBounds => i.val ≥ v.length | _ => False)
+      False := by
   grind [index_usize]
 
 def Array.set {α : Type u} {n : Usize} (v: Array α n) (i: Usize) (x: α) : Array α n :=
@@ -215,26 +217,29 @@ def Array.update {α : Type u} {n : Usize} (v: Array α n) (i: Usize) (x: α) :
     ok ⟨ v.val.set i.val x, by have := v.property; simp [*] ⟩
 
 @[step]
-theorem Array.update_spec {α : Type u} {n : Usize} (v: Array α n) (i: Usize) (x : α)
-  (hbound : i.val < v.length) :
-  v.update i x ⦃ nv => nv = v.set i x ⦄
+theorem Array.update_spec {α : Type u} {n : Usize} (v: Array α n) (i: Usize) (x : α) :
+    partialSpec (v.update i x)
+      (fun nv => nv = v.set i x)
+      (fun | .arrayOutOfBounds => i.val ≥ v.length | _ => False)
+      False
   := by
-  simp only [update, set]
-  simp at *
-  split <;> simp_all
+  simp only [partialSpec, update, set]
+  cases hopt : v[i]? <;> simp_all
 
 def Array.index_mut_usize {α : Type u} {n : Usize} (v: Array α n) (i: Usize) :
   Result (α × (α -> Array α n)) := do
   let x ← index_usize v i
   ok (x, set v i)
 
 @[step]
-theorem Array.index_mut_usize_spec {α : Type u} {n : Usize} (v: Array α n) (i: Usize)
-  (hbound : i.val < v.length) :
-  v.index_mut_usize i ⦃ x back => x = v.val[i.val] ∧ back = set v i ⦄ := by
-  simp only [index_mut_usize, Bind.bind, bind]
-  have ⟨ x, h ⟩ := spec_imp_exists (index_usize_spec v i hbound)
-  simp [h]
+theorem Array.index_mut_usize_spec {α : Type u} {n : Usize} (v: Array α n) (i: Usize) :
+    partialSpec (v.index_mut_usize i)
+      (uncurry' fun x back => ∃ _ : i.val < v.length, x = v.val[i.val] ∧ back = set v i)
+      (fun | .arrayOutOfBounds => i.val ≥ v.length | _ => False)
+      False := by
+  have h := index_usize_spec v i
+  simp only [partialSpec, index_mut_usize, Bind.bind, bind, uncurry'] at h ⊢
+  cases hres : v.index_usize i <;> simp_all
 
 @[simp]
 theorem Array.set_getElem!_eq {α} {n : Usize} [Inhabited α] (x : Array α n) (i : Usize) :

backends/lean/Aeneas/Std/Array/ArraySlice.lean

@@ -54,16 +54,20 @@ def Array.subslice {α : Type u} {n : Usize} (a : Array α n) (r : Range Usize)
     fail panic
 
 @[step]
-theorem Array.subslice_spec {α : Type u} {n : Usize} [Inhabited α] (a : Array α n) (r : Range Usize)
-  (h0 : r.start.val < r.end.val) (h1 : r.end.val ≤ a.val.length) :
-  subslice a r ⦃ s =>
-  s.val = a.val.slice r.start.val r.end.val ∧
-  (∀ i, i + r.start.val < r.end.val → s.val[i]! = a.val[r.start.val + i]!) ⦄
+theorem Array.subslice_spec {α : Type u} {n : Usize} [Inhabited α] (a : Array α n) (r : Range Usize) :
+    partialSpec (subslice a r)
+      (fun s =>
+        s.val = a.val.slice r.start.val r.end.val ∧
+        (∀ i, i + r.start.val < r.end.val → s.val[i]! = a.val[r.start.val + i]!))
+      (fun | .panic => ¬ (r.start.val < r.end.val ∧ r.end.val ≤ a.val.length) | _ => False)
+      False
   := by
-  simp only [subslice, true_and, h0, h1, ↓reduceIte, spec_ok, true_and]
-  intro i _
-  have := List.getElem!_slice r.start.val r.end.val i a.val (by scalar_tac)
-  simp only [this]
+  unfold subslice
+  split <;> rename_i h <;> simp [partialSpec]
+  · intro i _
+    have := List.getElem!_slice r.start.val r.end.val i a.val (by scalar_tac)
+    simp only [this]
+  · scalar_tac
 
 
 def Array.update_subslice {α : Type u} {n : Usize} (a : Array α n) (r : Range Usize) (s : Slice α) : Result (Array α n) :=
@@ -79,17 +83,20 @@ def Array.update_subslice {α : Type u} {n : Usize} (a : Array α n) (r : Range
 -- We should introduce special symbols for the monadic arithmetic operations
 -- (the user will never write those symbols directly).
 @[step]
-theorem Array.update_subslice_spec {α : Type u} {n : Usize} [Inhabited α] (a : Array α n) (r : Range Usize) (s : Slice α)
-  (_ : r.start.val < r.end.val) (_ : r.end.val ≤ a.length) (_ : s.length = r.end.val - r.start.val) :
-  update_subslice a r s ⦃ na =>
-  (∀ i, i < r.start.val → na[i]! = a[i]!) ∧
-  (∀ i, r.start.val ≤ i → i < r.end.val → na[i]! = s[i - r.start.val]!) ∧
-  (∀ i, r.end.val ≤ i → i < n.val → na[i]! = a[i]!) ⦄ := by
-  simp [update_subslice]
-  split
-  . simp [spec_ok]
-    simp_lists
-  . scalar_tac
+theorem Array.update_subslice_spec {α : Type u} {n : Usize} [Inhabited α] (a : Array α n) (r : Range Usize) (s : Slice α) :
+    partialSpec (update_subslice a r s)
+      (fun na =>
+        (∀ i, i < r.start.val → na[i]! = a[i]!) ∧
+        (∀ i, r.start.val ≤ i → i < r.end.val → na[i]! = s[i - r.start.val]!) ∧
+        (∀ i, r.end.val ≤ i → i < n.val → na[i]! = a[i]!))
+      (fun | .panic =>
+              ¬ (r.start.val < r.end.val ∧ r.end.val ≤ a.length ∧ s.val.length = r.end.val - r.start.val)
+           | _ => False)
+      False := by
+  unfold update_subslice
+  split <;> rename_i h <;> simp [partialSpec]
+  · simp_lists
+  · scalar_tac
 
 @[rust_fun "core::array::{core::ops::index::Index<[@T; @N], @I, @O>}::index"]
 def core.array.Array.index
@@ -399,38 +406,41 @@ theorem Array.index_SliceIndexRangeUsizeSlice {T : Type} {N : Usize}
 
 @[step]
 theorem Array.index_SliceIndexRangeUsizeSlice.step {T : Type} {N : Usize} [Inhabited T]
-    (a : Array T N) (r : core.ops.range.Range Usize)
-    (h0 : r.start ≤ r.end) (h1 : r.end ≤ N) :
-    core.array.Array.index (core.ops.index.IndexSlice
-      (core.slice.index.SliceIndexRangeUsizeSlice T)) a r
-    ⦃ (s : Slice T) =>
-      s.val = a.val.slice r.start r.end ∧
-      s.length = r.end.val - r.start.val ⦄ := by
+    (a : Array T N) (r : core.ops.range.Range Usize) :
+    partialSpec
+      (core.array.Array.index (core.ops.index.IndexSlice
+        (core.slice.index.SliceIndexRangeUsizeSlice T)) a r)
+      (fun (s : Slice T) =>
+        s.val = a.val.slice r.start r.end ∧
+        s.length = r.end.val - r.start.val)
+      (fun | .panic => ¬ (r.start ≤ r.end ∧ r.end ≤ N) | _ => False)
+      False := by
   simp only [Array.index_SliceIndexRangeUsizeSlice]
   have hts : a.to_slice.length = N := by simp [Array.to_slice, Slice.length]
-  simp only [core.slice.index.SliceIndexRangeUsizeSlice.index, UScalar.le_equiv, Slice.length]
-  split
-  · simp [spec_ok, Array.to_slice]; scalar_tac
+  unfold core.slice.index.SliceIndexRangeUsizeSlice.index
+  split <;> rename_i h <;> simp [partialSpec, Array.to_slice, Slice.length]
+  · scalar_tac
   · scalar_tac
 
 @[step]
 theorem Array.index_mut_SliceIndexRangeUsizeSlice.step {T : Type} {N : Usize} [Inhabited T]
-    (a : Array T N) (r : core.ops.range.Range Usize)
-    (h0 : r.start ≤ r.end) (h1 : r.end ≤ N) :
-    core.array.Array.index_mut (core.ops.index.IndexMutSlice
-      (core.slice.index.SliceIndexRangeUsizeSlice T)) a r
-    ⦃ (s : Slice T) (back : Slice T → Array T N) =>
-      s.val = a.val.slice r.start r.end ∧
-      s.length = r.end.val - r.start.val ∧
-      ∀ s', (back s').val = a.val.setSlice! r.start.val s'.val ⦄ := by
+    (a : Array T N) (r : core.ops.range.Range Usize) :
+    partialSpec
+      (core.array.Array.index_mut (core.ops.index.IndexMutSlice
+        (core.slice.index.SliceIndexRangeUsizeSlice T)) a r)
+      (uncurry' fun (s : Slice T) (back : Slice T → Array T N) =>
+        s.val = a.val.slice r.start r.end ∧
+        s.length = r.end.val - r.start.val ∧
+        ∀ s', (back s').val = a.val.setSlice! r.start.val s'.val)
+      (fun | .panic => ¬ (r.start ≤ r.end ∧ r.end ≤ N) | _ => False)
+      False := by
   simp only [core.array.Array.index_mut, core.ops.index.IndexMutSlice,
     core.slice.index.Slice.index_mut]
   have hts : a.to_slice.length = N := by simp [Array.to_slice, Slice.length]
-  simp only [core.slice.index.SliceIndexRangeUsizeSlice.index_mut,
-    UScalar.le_equiv, Slice.length]
-  split
-  · simp [spec_ok, Array.from_slice, Array.to_slice]
-    simp_lists; scalar_tac
+  unfold core.slice.index.SliceIndexRangeUsizeSlice.index_mut
+  split <;> rename_i h <;>
+    simp [partialSpec, Array.from_slice, Array.to_slice, uncurry', Slice.length]
+  · simp_lists; scalar_tac
   · scalar_tac
 
 -- Array index/index_mut with RangeTo
@@ -444,23 +454,23 @@ theorem Array.index_SliceIndexRangeToUsizeSlice {T : Type} {N : Usize}
 
 @[step]
 theorem Array.index_mut_SliceIndexRangeToUsizeSlice {T : Type} {N : Usize}
-    (a : Array T N) (r : core.ops.range.RangeTo Usize)
-    (h : r.end ≤ N) :
-    core.array.Array.index_mut (core.ops.index.IndexMutSlice
-      (core.slice.index.SliceIndexRangeToUsizeSlice T)) a r
-    ⦃ (s : Slice T) (back : Slice T → Array T N) =>
-      s.val = a.val.slice 0 r.end ∧
-      s.length = r.end.val ∧
-      ∀ s', (back s').val = a.val.setSlice! 0 s'.val ⦄ := by
+    (a : Array T N) (r : core.ops.range.RangeTo Usize) :
+    partialSpec
+      (core.array.Array.index_mut (core.ops.index.IndexMutSlice
+        (core.slice.index.SliceIndexRangeToUsizeSlice T)) a r)
+      (uncurry' fun (s : Slice T) (back : Slice T → Array T N) =>
+        s.val = a.val.slice 0 r.end ∧
+        s.length = r.end.val ∧
+        ∀ s', (back s').val = a.val.setSlice! 0 s'.val)
+      (fun | .panic => ¬ r.end ≤ N | _ => False)
+      False := by
   simp only [core.array.Array.index_mut, core.ops.index.IndexMutSlice,
     core.slice.index.Slice.index_mut]
   have hts : a.to_slice.length = N := by simp [Array.to_slice, Slice.length]
-  simp only [core.slice.index.SliceIndexRangeToUsizeSlice.index_mut,
-    show (r.end : Usize) ≤ a.to_slice.length from by scalar_tac]
-  refine ⟨?_, ?_, ?_⟩
-  · simp [Array.to_slice]
-  · simp [Slice.length]; scalar_tac
-  · intro s'; simp [Array.from_slice, Array.to_slice]
+  unfold core.slice.index.SliceIndexRangeToUsizeSlice.index_mut
+  split <;> rename_i h <;>
+    simp [partialSpec, Array.from_slice, Array.to_slice, uncurry', Slice.length] <;>
+    scalar_tac
 
 -- Array index/index_mut with RangeFrom
 
@@ -473,24 +483,24 @@ theorem Array.index_SliceIndexRangeFromUsizeSlice {T : Type} {N : Usize}
 
 @[step]
 theorem Array.index_mut_SliceIndexRangeFromUsizeSlice {T : Type} {N : Usize}
-    (a : Array T N) (r : core.ops.range.RangeFrom Usize)
-    (h : r.start ≤ N) :
-    core.array.Array.index_mut (core.ops.index.IndexMutSlice
-      (core.slice.index.SliceIndexRangeFromUsizeSlice T)) a r
-    ⦃ (s : Slice T) (back : Slice T → Array T N) =>
-      s.val = a.val.drop r.start ∧
-      s.length = N.val - r.start.val ∧
-      ∀ s', (back s').val = a.val.setSlice! r.start.val s'.val ⦄ := by
+    (a : Array T N) (r : core.ops.range.RangeFrom Usize) :
+    partialSpec
+      (core.array.Array.index_mut (core.ops.index.IndexMutSlice
+        (core.slice.index.SliceIndexRangeFromUsizeSlice T)) a r)
+      (uncurry' fun (s : Slice T) (back : Slice T → Array T N) =>
+        s.val = a.val.drop r.start ∧
+        s.length = N.val - r.start.val ∧
+        ∀ s', (back s').val = a.val.setSlice! r.start.val s'.val)
+      (fun | .panic => ¬ r.start ≤ N | _ => False)
+      False := by
   simp only [core.array.Array.index_mut, core.ops.index.IndexMutSlice,
     core.slice.index.Slice.index_mut]
   have hts : a.to_slice.length = N := by simp [Array.to_slice, Slice.length]
-  simp only [core.slice.index.SliceIndexRangeFromUsizeSlice.index_mut,
-    Slice.drop,
-    show (r.start : Usize) ≤ a.to_slice.length from by scalar_tac]
-  refine ⟨?_, ?_, ?_⟩
-  · simp [Array.to_slice]
-  · simp [Slice.length, List.length_drop]
-  · intro s'; simp [Array.from_slice, Array.to_slice]
+  unfold core.slice.index.SliceIndexRangeFromUsizeSlice.index_mut
+  split <;> rename_i h <;>
+    simp [partialSpec, Array.from_slice, Array.to_slice, uncurry',
+          Slice.length, Slice.drop, List.length_drop];
+    scalar_tac
 
 @[reducible, rust_trait_impl "core::convert::AsRef<[@T; @N], [@T]>"]
 def Array.Insts.CoreConvertAsRefSlice (T : Type) (N : Std.Usize) :