Prover floor patch v2: every trace buffer sized to its padded need (setup keys and shards), the sweep-2 points

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
2026-10-05 22:41:37 +00:00 · 2026-10-05 22:41:37 +00:00 · 830efc63e1
commit 830efc63e1
parent 393a8f831f
4 changed files with 148 additions and 13 deletions
--- a/proving/prover-floor/sp1-gpu-6.8.1-floor.patch
+++ b/proving/prover-floor/sp1-gpu-6.8.1-floor.patch
@ -1,8 +1,42 @@
 diff --git a/sp1-gpu/crates/jagged_tracegen/src/lib.rs b/sp1-gpu/crates/jagged_tracegen/src/lib.rs
-index 579f70a..88bfc79 100644
+index 579f70a..09e73e8 100644
 --- a/sp1-gpu/crates/jagged_tracegen/src/lib.rs
 +++ b/sp1-gpu/crates/jagged_tracegen/src/lib.rs
-@@ -494,6 +494,11 @@ async fn allocate_and_initialize_traces(
+@@ -481,6 +481,33 @@ async fn device_preprocessed_tracegen<A: CudaTracegenAir<Felt>>(
+     named_traces
+ }
+ 
+/// Igneum prover-floor patch: the dense elements a set of traces will occupy once `generate_jagged_traces`
+/// has laid them out, that is the sum of their buffers padded to the next multiple of 2^log_stacking_height
+/// (the "final padding" step below). Each phase (preprocessed, then main) is padded on its own.
+pub fn padded_trace_elements(
+    traces: &BTreeMap<String, Trace<TaskScope>>,
+    log_stacking_height: u32,
+) -> usize {
+    let total: usize = traces
+        .values()
+        .map(|t| match t {
+            Trace::Real(trace) => trace.guts().as_buffer().len(),
+            Trace::Padding(_) => 0,
+        })
+        .sum();
+    total.next_multiple_of(1 << log_stacking_height)
+}
+
+/// Igneum prover-floor patch: the capacity to allocate for a trace set: the exact padded size plus one
+/// stacking height of slack, never more than the prover's `max_trace_size`. `SP1_GPU_FLOOR_EXACT=0` restores
+/// upstream's full-capacity allocation.
+fn floor_capacity(max_trace_size: usize, needed: usize, log_stacking_height: u32) -> usize {
+    if std::env::var("SP1_GPU_FLOOR_EXACT").map(|v| v == "0").unwrap_or(false) {
+        return max_trace_size;
+    }
+    max_trace_size.min(needed + (1 << log_stacking_height))
+}
+
+ async fn allocate_and_initialize_traces(
+     preprocessed_traces: BTreeMap<String, Trace<TaskScope>>,
+     max_trace_size: usize,
+@@ -494,6 +521,11 @@ async fn allocate_and_initialize_traces(
 
     let total_gb = total_bytes as f64 / (1 << 30) as f64;
     tracing::debug!("Allocating {:?} GB of traces", total_gb);
@ -14,7 +48,40 @@ index 579f70a..88bfc79 100644
     let mut dense_data: Buffer<Felt, TaskScope> =
         Buffer::with_capacity_in(max_trace_size, backend.clone());
     let mut col_index: Buffer<u32, TaskScope> =
-@@ -1002,6 +1007,18 @@ pub async fn full_tracegen<A: CudaTracegenAir<Felt>>(
+@@ -677,9 +709,14 @@ pub async fn setup_tracegen<A: CudaTracegenAir<Felt>>(
+     let preprocessed_traces =
+         device_preprocessed_tracegen(program, host_phase_tracegen, backend).await;
+ 
+    let capacity = floor_capacity(
+        max_trace_size,
+        padded_trace_elements(&preprocessed_traces, log_stacking_height),
+        log_stacking_height,
+    );
+     let jagged_traces = allocate_and_initialize_traces(
+         preprocessed_traces,
+-        max_trace_size,
+        capacity,
+         log_stacking_height,
+         max_log_row_count,
+         backend,
+@@ -984,9 +1021,15 @@ pub async fn full_tracegen<A: CudaTracegenAir<Felt>>(
+ 
+     log_chip_stats(machine, &chip_set, &main_traces);
+ 
+    let capacity = floor_capacity(
+        max_trace_size,
+        padded_trace_elements(&preprocessed_traces, log_stacking_height)
+            + padded_trace_elements(&main_traces, log_stacking_height),
+        log_stacking_height,
+    );
+     let mut jagged_mle = allocate_and_initialize_traces(
+         preprocessed_traces,
+-        max_trace_size,
+        capacity,
+         log_stacking_height,
+         max_log_row_count,
+         backend,
+@@ -1002,6 +1045,18 @@ pub async fn full_tracegen<A: CudaTracegenAir<Felt>>(
     )
     .await;
 
@ -22,7 +89,7 @@ index 579f70a..88bfc79 100644
 +        let dense = jagged_mle.dense();
 +        let (free, total) = sp1_gpu_cudart::cuda_memory_info().unwrap_or((0, 0));
 +        eprintln!(
-+            "FLOOR tracegen used preprocessed_elements={} main_elements={} dense_len={} capacity_elements={max_trace_size} device_used_mib={}",
+            "FLOOR tracegen used preprocessed_elements={} main_elements={} dense_len={} capacity_elements={capacity} max_trace_size={max_trace_size} device_used_mib={}",
 +            dense.preprocessed_offset,
 +            dense.main_size(),
 +            dense.dense.len(),
--- a/tools/prover-floor/pc2-build-server.ps1
+++ b/tools/prover-floor/pc2-build-server.ps1
--- a/tools/prover-floor/pc2-floor-sweep2.ps1
+++ b/tools/prover-floor/pc2-floor-sweep2.ps1
@ -0,0 +1,65 @@
+# Prover floor (5 October 2026): the peak GPU memory and the time of one compressed shard proof through the PATCHED
+# sp1-gpu-server (/opt/igneum-floor/home/.sp1/bin, reached by HOME=/opt/igneum-floor/home: the SDK spawns the
+# server it finds under $HOME/.sp1/bin, sp1-cuda-6.8.1/src/server.rs) on PC 2's RTX 5090, the miners STOPPED by the
+# job (--stop-miners) and the live prover switched off for the run (its server would otherwise own the socket).
+# Every point: every server killed and its socket unlinked, a 1-s nvidia-smi sampler, one `--mode compressed
+# --shard 0` of the pv1 host (/opt/igneum-pv1, the UNPATCHED SDK and verifier: its VERIFIED is the unpatched
+# verifier's word on the patched server's proof), the peak, the time, the FLOOR lines the server prints.
+# The point list comes from the FLOOR_POINTS environment the job carries, else the default sweep below.
+$ErrorActionPreference = 'Continue'
+$urlFile = if ($env:IGNEUM_APP_DIR) { Join-Path $env:IGNEUM_APP_DIR 'app.url' } else { Join-Path $env:LOCALAPPDATA 'igneum\app\app.url' }
+if (-not (Test-Path $urlFile)) { $urlFile = Join-Path $env:LOCALAPPDATA 'igneum\app\app.url' }
+$base = (Get-Content $urlFile -Raw).Trim().TrimEnd('/')
+function Stamp { (Get-Date).ToUniversalTime().ToString('yyyy-MM-ddTHH:mm:ssZ') }
+function Prove($on) { try { (Invoke-RestMethod -Method Post -Uri "$base/api/prove" -ContentType 'application/json' -Body (@{on=$on} | ConvertTo-Json -Compress) -TimeoutSec 10) | ConvertTo-Json -Compress } catch { "error: $_" } }
+"RESULT start $(Stamp) prover off for the run: $(Prove $false)"
+Start-Sleep -Seconds 45
+"RESULT gpus $(Stamp) $((& nvidia-smi --query-gpu=index,name,memory.used,memory.total,utilization.gpu,power.draw --format=csv,noheader,nounits 2>$null) -join ' | ')"
+$job = $env:IGNEUM_JOB_DIR; if (-not $job) { $job = Join-Path $env:TEMP 'igneum-floor-measure' }; New-Item -ItemType Directory -Force -Path $job | Out-Null
+function WslPath($p) { $w = (& wsl.exe -d Ubuntu-24.04 -u root -- wslpath -a ($p -replace '\\', '/') 2>$null); if ($w) { ($w -replace "`0", '').Trim() } else { '/mnt/c' + ($p.Substring(2) -replace '\\', '/') } }
+$jobW = WslPath $job
+$emptyW = WslPath (Join-Path $env:LOCALAPPDATA 'igneum\app\jobs\chain-pc2-pv1c\block-83616.json')
+$points = if ($env:FLOOR_POINTS) { $env:FLOOR_POINTS } else { 'run x12 "$EMPTY" SP1_GPU_MEMORY_BUDGET_GB=12;run x12 "$V1" SP1_GPU_MEMORY_BUDGET_GB=12;run x12 "$ONE" SP1_GPU_MEMORY_BUDGET_GB=12;run x12 "$FULL" SP1_GPU_MEMORY_BUDGET_GB=12;run xe26 "$V1" SP1_GPU_ELEMENT_THRESHOLD=67108864;run xe26 "$EMPTY" SP1_GPU_ELEMENT_THRESHOLD=67108864;run x16 "$V1" SP1_GPU_MEMORY_BUDGET_GB=16;run x32 "$V1" SP1_GPU_MEMORY_BUDGET_GB=32;run x12r "$V1" SP1_GPU_MEMORY_BUDGET_GB=12 SP1_GPU_RECURSION_TRACE_ALLOCATION=100663296' }
+$bash = @'
+set -uo pipefail
+export PATH="$HOME/.cargo/bin:$PATH"
+CUDA_DIR="$(ls -d /usr/local/cuda-12.* 2>/dev/null | sort -V | tail -1 || true)"; [ -n "$CUDA_DIR" ] && export PATH="$CUDA_DIR/bin:$PATH" && export LD_LIBRARY_PATH="$CUDA_DIR/lib64:/usr/lib/wsl/lib:${LD_LIBRARY_PATH:-}"
+stamp() { date -u +%Y-%m-%dT%H:%M:%SZ; }
+JOB='JOBW_PLACEHOLDER'; H=/opt/igneum-pv1/igneum-prove-host; FX="/root/igneum-prove-pv1/proving/fixtures"
+FLOORHOME=/opt/igneum-floor/home; SRV=$FLOORHOME/.sp1/bin/sp1-gpu-server
+EMPTY='EMPTY_PLACEHOLDER'; V1="$FX/fees-v1-shards2.json"; FULL="$FX/block-338-shard1.json"; ONE="$FX/block-56-transfers.json"
+[ -x "$SRV" ] || { echo "RESULT measure_failed no patched server at $SRV"; exit 2; }
+[ -x "$H" ] || { echo "RESULT measure_failed no pv1 host at $H"; exit 2; }
+echo "RESULT patched_server sha256=$(sha256sum $SRV | cut -c1-64) version=$($SRV --version 2>/dev/null) host=$(sha256sum $H | cut -c1-16)"
+echo "RESULT live_server sha256=$(sha256sum /root/.sp1/bin/sp1-gpu-server | cut -c1-16) untouched"
+pkill -f sp1-gpu-server 2>/dev/null; sleep 2; rm -f /tmp/sp1-cuda-*.sock
+echo "RESULT idle_mib $(nvidia-smi --query-gpu=memory.used --format=csv,noheader,nounits | head -1)"
+run() { # name fixture env...
+  local name="$1" fx="$2"; shift 2
+  local tag="$name-$(basename $fx .json)"
+  pkill -f sp1-gpu-server 2>/dev/null; sleep 2; rm -f /tmp/sp1-cuda-*.sock
+  local csv="$JOB/smi-$tag.csv" log="$JOB/log-$tag.txt"
+  nvidia-smi --query-gpu=timestamp,memory.used,utilization.gpu --format=csv,noheader,nounits -l 1 > "$csv" 2>/dev/null &
+  local SMI=$!
+  local t0=$(date +%s)
+  env HOME=$FLOORHOME SP1_PROVER=cuda RUST_LOG=off SP1_GPU_FLOOR_LOG=1 "$@" $H "$fx" --mode compressed --shard 0 --out "$JOB/res-$tag.json" > "$log" 2>&1
+  local rc=$?
+  local wall=$(( $(date +%s) - t0 ))
+  pkill -f sp1-gpu-server 2>/dev/null; sleep 1; kill $SMI 2>/dev/null; sleep 1; rm -f /tmp/sp1-cuda-*.sock
+  local peak=$(awk -F', *' '{ if ($2+0 > m) m=$2+0 } END { print m+0 }' "$csv")
+  local n=$(wc -l < "$csv")
+  local line=$(grep -E "^RESULT compressed shard" "$log" | tail -1 | sed -E 's/.*prove ([0-9.]+) s, proof ([0-9]+) bytes, verify ([0-9.]+) s, ([A-Z ]+);.*/prove_s=\1 bytes=\2 verify_s=\3 \4/')
+  local cyc=$(grep -E "^RESULT execute shard" "$log" | tail -1 | sed -E 's/.*: ([0-9]+) cycles.*/\1/')
+  local err=$(grep -iE "error|panick|out of memory|OOM|unsupported" "$log" | grep -v "^FLOOR" | head -1 | cut -c1-200)
+  echo "RESULT floor cfg=$name fixture=$(basename $fx .json) peak_mib=$peak samples=$n wall_s=$wall cycles=${cyc:-na} ${line:-no_result} exit=$rc env='$*' ${err:+err=$err}"
+  grep -E "^FLOOR" "$log" | sed "s/^/RESULT floorline cfg=$name fixture=$(basename $fx .json) /" | head -40
+}
+POINTS_PLACEHOLDER_BASH
+pkill -f sp1-gpu-server 2>/dev/null; sleep 1; rm -f /tmp/sp1-cuda-*.sock
+echo "RESULT measure_end $(stamp)"
+'@
+$bash = $bash.Replace('JOBW_PLACEHOLDER', $jobW).Replace('EMPTY_PLACEHOLDER', $emptyW).Replace('POINTS_PLACEHOLDER_BASH', ($points -replace ';', "`n"))
+$bashFile = Join-Path $job 'measure.sh'
+[IO.File]::WriteAllText($bashFile, ($bash -replace "`r`n", "`n"), (New-Object System.Text.UTF8Encoding $false))
+& wsl.exe -d Ubuntu-24.04 -u root -- bash (WslPath $bashFile) 2>&1 | ForEach-Object { ($_ -replace "`0", '') }
+"RESULT end $(Stamp) prover back on: $(Prove $true)"
--- a/tools/prover-floor/points-sweep2.txt
+++ b/tools/prover-floor/points-sweep2.txt
@ -1,6 +1,9 @@
-run r26b12 "$EMPTY" SP1_GPU_MEMORY_BUDGET_GB=12 SP1_GPU_RECURSION_TRACE_ALLOCATION=67108864
-run r26b12 "$V1" SP1_GPU_MEMORY_BUDGET_GB=12 SP1_GPU_RECURSION_TRACE_ALLOCATION=67108864
-run r25b12 "$V1" SP1_GPU_MEMORY_BUDGET_GB=12 SP1_GPU_RECURSION_TRACE_ALLOCATION=33554432
-run r26e26 "$V1" SP1_GPU_ELEMENT_THRESHOLD=67108864 SP1_GPU_RECURSION_TRACE_ALLOCATION=67108864
-run r26e26 "$ONE" SP1_GPU_ELEMENT_THRESHOLD=67108864 SP1_GPU_RECURSION_TRACE_ALLOCATION=67108864
-run r26e26 "$FULL" SP1_GPU_ELEMENT_THRESHOLD=67108864 SP1_GPU_RECURSION_TRACE_ALLOCATION=67108864
+run x12 "$EMPTY" SP1_GPU_MEMORY_BUDGET_GB=12
+run x12 "$V1" SP1_GPU_MEMORY_BUDGET_GB=12
+run x12 "$ONE" SP1_GPU_MEMORY_BUDGET_GB=12
+run x12 "$FULL" SP1_GPU_MEMORY_BUDGET_GB=12
+run xe26 "$V1" SP1_GPU_ELEMENT_THRESHOLD=67108864
+run xe26 "$EMPTY" SP1_GPU_ELEMENT_THRESHOLD=67108864
+run x16 "$V1" SP1_GPU_MEMORY_BUDGET_GB=16
+run x32 "$V1" SP1_GPU_MEMORY_BUDGET_GB=32
+run x12r "$V1" SP1_GPU_MEMORY_BUDGET_GB=12 SP1_GPU_RECURSION_TRACE_ALLOCATION=100663296