326953e0ac
proving/igneum-prove: core (port of igneum-exec at fb33069 as the block statement), program (SP1 v6.8.1 guest), host (execute, core, compressed; ProofSystem trait with the stub and the SP1 implementation), export (cuts a block out of igneum_exportSegments and checks every state root against the node's). Fixtures block-78-increment and block-56-transfers from the 3-node simnet. proving/windows-wsl2: SETUP-PROVER.bat, setup-wsl.sh, PROVE-BLOCK.bat, make-package.sh. docs/plans/proving-v0.md: the devnet v4 shard plan, what tonight's proof shows and does not, the morning acceptance line. Mac CPU baseline (block 78: 626 k cycles, core 22.0 s and 7.3 MB, compressed 55.7 s and 1.27 MB, both verified) appended to docs/bench-log.md, left uncommitted because that file carries another agent's pending changes. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
60 lines
3.9 KiB
PowerShell
60 lines
3.9 KiB
PowerShell
# Igneum proving v0: Windows side of the setup. Run through SETUP-PROVER.bat.
|
|
# Step A (first run): enable WSL2 and install Ubuntu 24.04. Needs a reboot.
|
|
# Step B (after the reboot): run setup-wsl.sh inside Ubuntu.
|
|
$ErrorActionPreference = 'Stop'
|
|
$here = Split-Path -Parent $MyInvocation.MyCommand.Path
|
|
$distro = 'Ubuntu-24.04'
|
|
|
|
function Is-Admin { ([Security.Principal.WindowsPrincipal][Security.Principal.WindowsIdentity]::GetCurrent()).IsInRole([Security.Principal.WindowsBuiltInRole]::Administrator) }
|
|
if (-not (Is-Admin)) {
|
|
Write-Host 'Asking for administrator rights (WSL install needs them)...'
|
|
Start-Process powershell -Verb RunAs -ArgumentList @('-NoProfile', '-ExecutionPolicy', 'Bypass', '-File', "`"$PSCommandPath`"")
|
|
exit
|
|
}
|
|
|
|
$build = [int](Get-ItemProperty 'HKLM:\SOFTWARE\Microsoft\Windows NT\CurrentVersion').CurrentBuildNumber
|
|
if ($build -lt 22000) { Write-Host "This is Windows build $build; Windows 11 (build 22000 or later) is expected. WSL2 with GPU also works on recent Windows 10 builds, continuing anyway." }
|
|
|
|
$nv = Get-Command nvidia-smi -ErrorAction SilentlyContinue
|
|
if ($nv) { Write-Host 'NVIDIA driver on Windows:'; & nvidia-smi --query-gpu=name,driver_version,memory.total --format=csv,noheader } else { Write-Host 'nvidia-smi not found: install the NVIDIA Windows driver (it includes the WSL CUDA driver; nothing is installed inside Ubuntu for the driver).' }
|
|
|
|
# Is the distro already installed?
|
|
$installed = $false
|
|
try { $list = (& wsl.exe --list --quiet 2>$null) -join "`n"; if ($list -match 'Ubuntu-24\.04') { $installed = $true } } catch {}
|
|
|
|
if (-not $installed) {
|
|
Write-Host "Step A: enabling WSL2 and installing $distro (download about 400 MB, approximate)."
|
|
Write-Host 'Command: wsl --install -d Ubuntu-24.04'
|
|
& wsl.exe --install -d $distro
|
|
Write-Host ''
|
|
Write-Host '================================================================================'
|
|
Write-Host 'REBOOT NOW. WSL2 turns on the Virtual Machine Platform, which only takes effect after a restart.'
|
|
Write-Host 'After the reboot: Ubuntu opens once by itself and asks for a username and password (pick anything,'
|
|
Write-Host 'for example igneum); close it, then double-click SETUP-PROVER.bat again for step B.'
|
|
Write-Host '================================================================================'
|
|
exit
|
|
}
|
|
|
|
# Step B: inside Ubuntu.
|
|
Write-Host "Step B: $distro is installed. Setting WSL2 as default and checking the GPU is visible inside it."
|
|
& wsl.exe --set-default-version 2 | Out-Null
|
|
& wsl.exe --update | Out-Null
|
|
$wslconfig = Join-Path $env:USERPROFILE '.wslconfig'
|
|
if (-not (Test-Path $wslconfig)) {
|
|
# SP1's CPU prover wants 16 GB or more; the GPU prover wants 4 cores and 16 GB on the host side. Give WSL most of the RAM.
|
|
$ramGb = [math]::Floor((Get-CimInstance Win32_ComputerSystem).TotalPhysicalMemory / 1GB)
|
|
$give = [math]::Max(16, [math]::Floor($ramGb * 0.75))
|
|
"[wsl2]`nmemory=${give}GB`nswap=16GB`n" | Set-Content -Path $wslconfig -Encoding ascii
|
|
Write-Host "Wrote $wslconfig (memory=${give}GB of $ramGb GB, swap=16GB). WSL restarts to apply it."
|
|
& wsl.exe --shutdown
|
|
}
|
|
$gpu = (& wsl.exe -d $distro -- bash -lc 'nvidia-smi --query-gpu=name --format=csv,noheader 2>/dev/null || ls /usr/lib/wsl/lib/libcuda.so.1 2>/dev/null') -join ' '
|
|
if ($gpu) { Write-Host "GPU visible inside WSL: $gpu" } else { Write-Host 'WARNING: no GPU visible inside WSL. Update the NVIDIA Windows driver (GeForce 470 or later) and run wsl --update.' }
|
|
|
|
# Hand over to the Linux script with the package directory mounted at /mnt/<drive>/...
|
|
$drive = $here.Substring(0,1).ToLower()
|
|
$rest = $here.Substring(2).Replace('\', '/')
|
|
$linuxDir = "/mnt/$drive$rest"
|
|
Write-Host "Running setup-wsl.sh inside $distro (package at $linuxDir). This installs about 3 to 4 GB in total (approximate) and takes 15 to 40 minutes."
|
|
& wsl.exe -d $distro -- bash "$linuxDir/setup-wsl.sh"
|
|
Write-Host 'Setup finished. Next: double-click PROVE-BLOCK.bat.'
|