feat: KZG on BN254

.cargo/config.toml

@@ -1,2 +1,9 @@
 [build]
-rustflags = ["-Ctarget-cpu=native"]
+rustflags = ["-Ctarget-cpu=native"]
+
+# Lean's bundled toolchain links against glibc stubs older than 2.38, whose
+# headers in C23 mode, the default of recent GCC, redirect `strtol` and its
+# relatives to `__isoc23_*` symbols the stubs lack. C17 keeps symbols the link
+# can resolve.
+[env]
+CFLAGS = "-std=gnu17"

.github/workflows/ci.yml

@@ -142,9 +142,8 @@ jobs:
       image: nvidia/cuda:13.3.1-devel-ubuntu26.04
     env:
       # This job validates feature plumbing and the Rust-staticlib-to-Lean
-      # link without paying for a GPU runner. Multi-stark CI compiles the
-      # complete supported cubin set; one representative architecture is
-      # sufficient for this downstream integration gate.
+      # link without paying for a GPU runner. One explicit architecture
+      # is sufficient for this downstream integration gate.
       MULTI_STARK_CUDA_ARCHS: "80"
     steps:
       # No sccache here yet. Once the GPU benchmark lands after #644, wire
@@ -177,9 +176,10 @@ jobs:
           auto-config: false
           use-github-cache: false
       - name: Compile CUDA Rust targets
-        run: cargo check --release --locked --workspace --all-targets --features ix-ffi/parallel,ix-ffi/cuda
-      - name: Link a CUDA-enabled Lean executable
-        run: IX_CUDA=1 lake build bench-typecheck
+        run: |
+          cargo check --release --locked --workspace --all-targets --features ix-ffi/parallel,ix-ffi/cuda,ix-proof-compression/cuda
+      - name: Link CUDA-enabled Lean executables
+        run: IX_CUDA=1 lake build ix bench-typecheck
 
   lints:
     name: Lint workflows

Benchmarks/Typecheck.lean

@@ -430,7 +430,7 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do
     IO.eprintln "error: --join requires singleton CheckEnv shards; drop --skip-deps"
     return Ix.Benchmark.Results.exitUsage
   -- Off by default; CI passes --texray explicitly.
-  let useTexray := p.hasFlag "texray"
+  let useTexray ← TracingTexray.enabled (p.hasFlag "texray")
   let useInterp := p.hasFlag "interp"
   if join && useInterp then
     IO.eprintln "error: --join requires the native singleton-shard prover; drop --interp"