ci: temporary source artifact relay

.github/workflows/generate-sail-executable-v047.yml

@@ -0,0 +1,149 @@
+name: Generate official Sail executable Lean model v0.4.7
+
+on:
+  push:
+    branches: [artifact-download-relay-20260823]
+    paths:
+      - .github/workflows/generate-sail-executable-v047.yml
+  pull_request:
+    branches: [main]
+  workflow_dispatch:
+
+permissions:
+  contents: write
+
+env:
+  SAIL_RISCV_REVISION: ac2a585506aad46b088b3594e56b8c21c52e297e
+  SAIL_VERSION: 0.20.2
+  SAIL_MODULES: I;M;A;H;Zicsr_insts;Zifencei;Sstc;postlude
+
+jobs:
+  generate:
+    runs-on: ubuntu-latest
+    timeout-minutes: 120
+    steps:
+      - name: Checkout workflow repository
+        uses: actions/checkout@v5
+
+      - name: Checkout pinned official Sail RISC-V
+        uses: actions/checkout@v5
+        with:
+          repository: riscv/sail-riscv
+          ref: ${{ env.SAIL_RISCV_REVISION }}
+          path: sail-riscv
+          fetch-depth: 1
+
+      - name: Install pinned Sail toolchain
+        uses: ./sail-riscv/.github/actions/sail-setup
+        with:
+          sail-version: ${{ env.SAIL_VERSION }}
+
+      - name: Configure executable Lean backend only
+        working-directory: sail-riscv
+        shell: bash
+        run: |
+          set -euo pipefail
+          rm -rf build
+          cmake -S . -B build -G Ninja \
+            -DCMAKE_BUILD_TYPE=Release \
+            -DPRINT_EFFECTS=true \
+            -DSAIL_MODULES="$SAIL_MODULES"
+
+      - name: Generate official executable Lean definitions
+        working-directory: sail-riscv
+        shell: bash
+        run: |
+          set -euo pipefail
+          cmake --build build --target generated_lean_executable_rv64d --parallel 2
+          PKG=build/model/Lean_RV64D_executable
+          test -f "$PKG/LeanRV64D.lean"
+          test -d "$PKG/LeanRV64D"
+          du -sh "$PKG"
+          find "$PKG" -maxdepth 2 -type f -printf '%s %p\n' | sort -nr | sed -n '1,40p'
+
+      - name: Publish generated executable source checkpoint before validation
+        if: github.event_name != 'pull_request'
+        working-directory: sail-riscv
+        shell: bash
+        run: |
+          set -euo pipefail
+          PKG=build/model/Lean_RV64D_executable
+          OUT="$GITHUB_WORKSPACE/executable-source"
+          rm -rf "$OUT"
+          mkdir -p "$OUT/source"
+          cp -a "$PKG" "$OUT/source/Lean_RV64D_executable"
+          rm -rf "$OUT/source/Lean_RV64D_executable/.lake" "$OUT/source/Lean_RV64D_executable/.git"
+          cat > "$OUT/UPSTREAM-PIN.txt" <<EOF
+          sail_riscv_revision=$SAIL_RISCV_REVISION
+          sail_compiler_version=$SAIL_VERSION
+          sail_modules=$SAIL_MODULES
+          backend=generated_lean_executable_rv64d
+          validation_status=generated-not-yet-built
+          EOF
+          (cd "$OUT" && find source -type f -print0 | sort -z | xargs -0 sha256sum > SOURCE-SHA256SUMS)
+          tar --zstd -cf "$OUT/sail-riscv-H-executable-Lean-ac2a585-source.tar.zst" -C "$OUT" source UPSTREAM-PIN.txt SOURCE-SHA256SUMS
+          sha256sum "$OUT/sail-riscv-H-executable-Lean-ac2a585-source.tar.zst" > "$OUT/sail-riscv-H-executable-Lean-ac2a585-source.tar.zst.sha256"
+          ls -lh "$OUT"
+          git config user.name github-actions[bot]
+          git config user.email 41898282+github-actions[bot]@users.noreply.github.com
+          git checkout --orphan sail-v047-executable-source-20260823
+          git rm -rf .
+          cp -a "$OUT"/. .
+          git add -A
+          git commit -m 'relay: official Sail executable Lean source v0.4.7 [skip ci]'
+          git push --force origin HEAD:sail-v047-executable-source-20260823
+
+      - name: Set up generated executable-model Lean package
+        uses: leanprover/lean-action@v1
+        with:
+          auto-config: false
+          lake-package-directory: sail-riscv/build/model/Lean_RV64D_executable
+          build: false
+          test: false
+          lint: false
+          use-github-cache: false
+
+      - name: Build generated executable Lean model
+        working-directory: sail-riscv/build/model/Lean_RV64D_executable
+        shell: bash
+        run: |
+          set -euo pipefail
+          lake update
+          lake build
+          test -d .lake/packages/Sail
+
+      - name: Publish validated self-contained executable model
+        if: github.event_name != 'pull_request'
+        working-directory: sail-riscv
+        shell: bash
+        run: |
+          set -euo pipefail
+          PKG=build/model/Lean_RV64D_executable
+          OUT="$GITHUB_WORKSPACE/executable-validated"
+          rm -rf "$OUT"
+          mkdir -p "$OUT/validated/vendor"
+          cp -a "$PKG" "$OUT/validated/Lean_RV64D_executable"
+          cp -a "$PKG/.lake/packages/Sail" "$OUT/validated/vendor/LeanSailV5"
+          rm -rf "$OUT/validated/Lean_RV64D_executable/.lake" \
+            "$OUT/validated/vendor/LeanSailV5/.lake" \
+            "$OUT/validated/vendor/LeanSailV5/.git"
+          cp "$OUT/validated/Lean_RV64D_executable/lakefile.toml" "$OUT/validated/Lean_RV64D_executable/UPSTREAM-lakefile.toml"
+          perl -0pi -e 's#\[\[require\]\]\nname = "Sail"\ngit = "https://github.com/rems-project/lean-sail"\nrev = "v5"#[[require]]\nname = "Sail"\npath = "../vendor/LeanSailV5"#g' "$OUT/validated/Lean_RV64D_executable/lakefile.toml"
+          grep -F 'path = "../vendor/LeanSailV5"' "$OUT/validated/Lean_RV64D_executable/lakefile.toml"
+          cat > "$OUT/UPSTREAM-PIN.txt" <<EOF
+          sail_riscv_revision=$SAIL_RISCV_REVISION
+          sail_compiler_version=$SAIL_VERSION
+          sail_modules=$SAIL_MODULES
+          backend=generated_lean_executable_rv64d
+          validation_status=lake-build-passed
+          EOF
+          (cd "$OUT" && find validated -type f -print0 | sort -z | xargs -0 sha256sum > VALIDATED-SHA256SUMS)
+          tar --zstd -cf "$OUT/sail-riscv-H-executable-Lean-ac2a585-validated.tar.zst" -C "$OUT" validated UPSTREAM-PIN.txt VALIDATED-SHA256SUMS
+          sha256sum "$OUT/sail-riscv-H-executable-Lean-ac2a585-validated.tar.zst" > "$OUT/sail-riscv-H-executable-Lean-ac2a585-validated.tar.zst.sha256"
+          ls -lh "$OUT"
+          git checkout --orphan sail-v047-executable-validated-20260823
+          git rm -rf .
+          cp -a "$OUT"/. .
+          git add -A
+          git commit -m 'relay: validated official Sail executable Lean model v0.4.7 [skip ci]'
+          git push --force origin HEAD:sail-v047-executable-validated-20260823

.github/workflows/package-lean-429-cutover.yml

@@ -0,0 +1,84 @@
+name: Package Lean 4.29 for Sail cutover
+
+on:
+  pull_request:
+    branches: [main]
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+jobs:
+  package:
+    runs-on: ubuntu-latest
+    timeout-minutes: 45
+    steps:
+      - name: Create minimal toolchain pin
+        shell: bash
+        run: |
+          set -euo pipefail
+          mkdir -p package
+          printf '%s\n' 'leanprover/lean4:v4.29.0' > package/lean-toolchain
+          cat > package/lakefile.toml <<'EOF'
+          name = "toolchain-pin"
+          defaultTargets = []
+          EOF
+          cat > package/lake-manifest.json <<'EOF'
+          {"version":"1.2.0","packagesDir":".lake/packages","packages":[],"name":"toolchain-pin","lakeDir":".lake","fixedToolchain":false}
+          EOF
+
+      - name: Install Lean 4.29
+        uses: leanprover/lean-action@v1
+        with:
+          auto-config: false
+          lake-package-directory: package
+          build: false
+          test: false
+          lint: false
+          use-github-cache: false
+
+      - name: Package exact installed toolchain and split it
+        shell: bash
+        run: |
+          set -euo pipefail
+          LEAN_BIN=$(cd package && elan which lean)
+          TOOLCHAIN=$(dirname "$(dirname "$LEAN_BIN")")
+          test -x "$TOOLCHAIN/bin/lean"
+          "$TOOLCHAIN/bin/lean" --version
+          mkdir -p out
+          tar --sort=name --mtime='UTC 2026-08-23' --owner=0 --group=0 --numeric-owner \
+            -C "$(dirname "$TOOLCHAIN")" -cf - "$(basename "$TOOLCHAIN")" \
+            | zstd -3 -T0 -o out/lean-4.29.0-linux.tar.zst
+          sha256sum out/lean-4.29.0-linux.tar.zst > out/lean-4.29.0-linux.tar.zst.sha256
+          split -b 250M -d -a 2 out/lean-4.29.0-linux.tar.zst out/lean-4.29.0-linux.tar.zst.part-
+          rm out/lean-4.29.0-linux.tar.zst
+          ls -lh out
+
+      - name: Upload toolchain part 00
+        uses: actions/upload-artifact@v4
+        with:
+          name: lean-4.29.0-linux-cutover-part-00
+          path: out/lean-4.29.0-linux.tar.zst.part-00
+          retention-days: 1
+          compression-level: 0
+          if-no-files-found: error
+
+      - name: Upload toolchain part 01
+        uses: actions/upload-artifact@v4
+        with:
+          name: lean-4.29.0-linux-cutover-part-01
+          path: out/lean-4.29.0-linux.tar.zst.part-01
+          retention-days: 1
+          compression-level: 0
+          if-no-files-found: error
+
+      - name: Upload toolchain part 02 and checksum
+        uses: actions/upload-artifact@v4
+        with:
+          name: lean-4.29.0-linux-cutover-part-02-meta
+          path: |
+            out/lean-4.29.0-linux.tar.zst.part-02
+            out/lean-4.29.0-linux.tar.zst.sha256
+          retention-days: 1
+          compression-level: 0
+          if-no-files-found: error

.github/workflows/validate-sail-cutover-v046.yml

@@ -0,0 +1,154 @@
+name: Validate destructive official Sail cutover v0.4.6
+
+on:
+  pull_request:
+    branches: [main]
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+jobs:
+  validate:
+    runs-on: ubuntu-latest
+    timeout-minutes: 120
+    steps:
+      - name: Checkout generated official Sail Lean source checkpoint
+        uses: actions/checkout@v5
+        with:
+          repository: o8vm/bee
+          ref: sail-v044-source-fast-20260823
+          path: generated
+          fetch-depth: 1
+
+      - name: Checkout pinned lean-sail v5
+        uses: actions/checkout@v5
+        with:
+          repository: rems-project/lean-sail
+          ref: v5
+          path: cutover/vendor/LeanSailV5
+          fetch-depth: 1
+
+      - name: Assemble cutover package with no local ISA model
+        shell: bash
+        run: |
+          set -euo pipefail
+          mkdir -p cutover/vendor/OfficialSailRiscVLeanH cutover/SailAuthority
+          cp -a generated/source/Lean_RV64D/. cutover/vendor/OfficialSailRiscVLeanH/
+          rm -rf cutover/vendor/OfficialSailRiscVLeanH/.lake cutover/vendor/LeanSailV5/.git cutover/vendor/LeanSailV5/.lake
+          cat > cutover/vendor/OfficialSailRiscVLeanH/lakefile.toml <<'EOF'
+          name = "Lean_RV64D"
+          defaultTargets = ["LeanRV64D"]
+          moreLeanArgs = ["--tstack=400000"]
+          [[lean_lib]]
+          name = "LeanRV64D"
+          leanOptions.weak.linter.style.nameCheck = false
+          moreLeancArgs = ["-fbracket-depth=500"]
+          [[require]]
+          name = "Sail"
+          path = "../LeanSailV5"
+          EOF
+          cat > cutover/lean-toolchain <<'EOF'
+          leanprover/lean4:v4.29.0
+          EOF
+          cat > cutover/lakefile.toml <<'EOF'
+          name = "SailCutoverValidation"
+          defaultTargets = ["SailAuthority"]
+          moreLeanArgs = ["--tstack=400000"]
+          [[lean_lib]]
+          name = "SailAuthority"
+          leanOptions.weak.linter.style.nameCheck = false
+          [[require]]
+          name = "Sail"
+          path = "vendor/LeanSailV5"
+          [[require]]
+          name = "Lean_RV64D"
+          path = "vendor/OfficialSailRiscVLeanH"
+          EOF
+          cat > cutover/lake-manifest.json <<'EOF'
+          {"version":"1.1.0","packagesDir":".lake/packages","packages":[],"name":"SailCutoverValidation","lakeDir":".lake"}
+          EOF
+          cat > cutover/SailAuthority.lean <<'EOF'
+          import SailAuthority.KeyDecodes
+          EOF
+          cat > cutover/SailAuthority/OfficialAPI.lean <<'EOF'
+          import LeanRV64D.DecodeExt
+          import LeanRV64D.InstsEnd
+          import LeanRV64D.Model
+          import LeanRV64D.Step
+          namespace SailAuthority
+          abbrev officialDecode := LeanRV64D.Functions.ext_decode
+          abbrev officialExecute := LeanRV64D.Functions.execute
+          abbrev officialTryStep := LeanRV64D.Functions.try_step
+          abbrev officialInitModel := LeanRV64D.Functions.init_model
+          abbrev officialInitBootRequirements := LeanRV64D.Functions.init_boot_requirements
+          abbrev OfficialInstruction := LeanRV64D.instruction
+          abbrev OfficialState := Sail.ConcurrencyInterfaceV1.SequentialState LeanRV64D.RegisterType Sail.ConcurrencyInterfaceV1.trivialChoiceSource
+          end SailAuthority
+          EOF
+          cat > cutover/SailAuthority/Decode.lean <<'EOF'
+          import SailAuthority.OfficialAPI
+          namespace SailAuthority
+          def decode? (word : UInt32) : Option OfficialInstruction :=
+            let bits : BitVec 32 := BitVec.ofNat 32 word.toNat
+            match (officialDecode bits).run (default : OfficialState) with
+            | .ok instruction _ => some instruction
+            | .error _ _ => none
+          def decodesAsEcall (word : UInt32) : Bool := match decode? word with | some (.ECALL ()) => true | _ => false
+          def decodesAsMret (word : UInt32) : Bool := match decode? word with | some (.MRET ()) => true | _ => false
+          def decodesAsSret (word : UInt32) : Bool := match decode? word with | some (.SRET ()) => true | _ => false
+          def decodesAsWfi (word : UInt32) : Bool := match decode? word with | some (.WFI ()) => true | _ => false
+          def decodesAsHfenceGvma (word : UInt32) : Bool := match decode? word with | some (.HFENCE_GVMA _) => true | _ => false
+          def decodesAsHfenceVvma (word : UInt32) : Bool := match decode? word with | some (.HFENCE_VVMA _) => true | _ => false
+          end SailAuthority
+          EOF
+          cat > cutover/SailAuthority/KeyDecodes.lean <<'EOF'
+          import SailAuthority.Decode
+          set_option maxHeartbeats 1_000_000_000
+          set_option maxRecDepth 1_000_000
+          namespace SailAuthority
+          theorem ecall_decodes_officially : decodesAsEcall 0x00000073 = true := by decide +kernel
+          theorem mret_decodes_officially : decodesAsMret 0x30200073 = true := by decide +kernel
+          theorem sret_decodes_officially : decodesAsSret 0x10200073 = true := by decide +kernel
+          theorem wfi_decodes_officially : decodesAsWfi 0x10500073 = true := by decide +kernel
+          theorem hfence_gvma_decodes_officially : decodesAsHfenceGvma 0x62000073 = true := by decide +kernel
+          theorem hfence_vvma_decodes_officially : decodesAsHfenceVvma 0x22000073 = true := by decide +kernel
+          end SailAuthority
+          EOF
+          if grep -R -En 'namespace[[:space:]]+CertifiedKernel\.RV64|structure[[:space:]]+HardwareRelation|def[[:space:]]+targetMachine|customMachine_refines|CompatLayer|LegacyMachine' cutover --include='*.lean'; then
+            echo 'forbidden local ISA model or compatibility layer' >&2
+            exit 1
+          fi
+
+      - name: Install Lean 4.29
+        uses: leanprover/lean-action@v1
+        with:
+          auto-config: false
+          lake-package-directory: cutover
+          build: false
+          test: false
+          lint: false
+          use-github-cache: false
+
+      - name: Build official-Sail cutover proof root
+        working-directory: cutover
+        shell: bash
+        run: |
+          set -euo pipefail
+          lake update
+          lake build SailAuthority
+          printf 'OFFICIAL_SAIL_CUTOVER_BUILD=PASS\n' | tee build-status.env
+
+      - name: Upload validation log and source
+        uses: actions/upload-artifact@v4
+        with:
+          name: sail-cutover-v046-validation
+          path: |
+            cutover/SailAuthority.lean
+            cutover/SailAuthority
+            cutover/lakefile.toml
+            cutover/lean-toolchain
+            cutover/build-status.env
+          retention-days: 1
+          compression-level: 9
+          if-no-files-found: error

ARTIFACT-RELAY-20260823.txt

@@ -0,0 +1 @@
+Temporary pull-request trigger for downloading pinned official Sail-generated Lean sources and lean-sail v5 into the isolated build environment.