diff --git a/.github/workflows/generate-sail-executable-v047.yml b/.github/workflows/generate-sail-executable-v047.yml new file mode 100644 index 00000000..9e983710 --- /dev/null +++ b/.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" < 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" < 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 diff --git a/.github/workflows/package-lean-429-cutover.yml b/.github/workflows/package-lean-429-cutover.yml new file mode 100644 index 00000000..d3c3ccd7 --- /dev/null +++ b/.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 diff --git a/.github/workflows/validate-sail-cutover-v046.yml b/.github/workflows/validate-sail-cutover-v046.yml new file mode 100644 index 00000000..12553ada --- /dev/null +++ b/.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 diff --git a/ARTIFACT-RELAY-20260823.txt b/ARTIFACT-RELAY-20260823.txt new file mode 100644 index 00000000..382e2486 --- /dev/null +++ b/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.