A research project by Requant Network.
Status: the bounded SM120 port study is complete. Five new GPU proofs across three randomized commitments and two policies pass the original CPU verifier. See results, methods and final conclusions.
This study ports a pinned inference prover to the RTX 5060 Ti 16 GB and investigates whether exact fused arithmetic can fit consumer Blackwell's shared-memory budget. The question is concrete: can the original commitment, model execution, proof and CPU verification run while retaining all arithmetic and acceptance checks?
| Experiment | Coverage and result |
|---|---|
| Unmodified native CPU verifier | Stored synthetic proof accepted, exit 0, last line YES |
| Negative CPU controls | Incorrect ID, altered request/output/proof, and truncated proof are rejected |
| Compact fused routed experts | 384 cases per input seed, two seeds, 3,258,112 exact integer outputs in total |
| Expert shared memory | Maximum 82,944 bytes (81 KiB), within the measured device limit of 101,376 bytes (99 KiB) |
| Compact histogram kernels | 114 cases per seed, two seeds, 12,500,052 exact output counters in total |
| Histogram shared memory | At most 65,536 bytes (64 KiB), including the full 16-bit key range through public bin windows |
| First architecture/cuBLAS fallback | Full run fails at an unconditional 128 KiB histogram opt-in; retained as an unsuccessful baseline |
| Complete corrected GPU proof | Accepted on RTX 5060 Ti 16 GB, native CPU verifier exit 0 and YES; 4,160,364-byte proof retained publicly |
| Replication and independent requests | Three commitments, exact-match/clipped-gap configurations and two new next-token-only prompts; all five proofs accept |
| Altered public artifacts | Five honest whole native calls accept; all 35 ID/request/response/proof/key/leaf controls reject |
These correctness probes ran while other CPU compilation could be active. Their incidental times do not establish a speedup. The pinned source, patch, executed script and native binary hashes are retained in results.
The Hopper expert kernel has two A buffers and three B buffers. Its larger configurations exceed the SM120 per-block budget. The compact path keeps the original 128-row by 256-input arithmetic tile and WMMA operations, uses a single shared tile per operand, and synchronizes before reuse. It caps token tiles at sixteen slots.
The memory calculation also includes the WMMA output overlay. An early input-only estimate missed that overlay and produced an illegal-address failure for a larger token tile. The corrected allocation is the maximum of input and output footprints. This failed draft is documented because apparently rejected designs can fail through implementation mistakes, rather than an invalid mathematical idea.
Two independent input cohorts cover Q4/Q5 decoding, one through four signed-byte activation limbs, ragged routing, 1/17/33/65 tokens, 128/256 output rows, 256/1024 input coordinates, zero/max/min/random activations, absent and power-of-two gains, and fractional gains in eighths. The independent CPU decoder uses integer arithmetic and rational ties-to-even rounding. Every output is checked exactly, with no floating tolerance. Coverage is bounded to those scales and shapes; it is not a proof for arbitrary model weights.
Range and lookup histograms use public windows over the output bins. A 16-bit key histogram scans four 16,384-bin windows rather than two 32,768-bin halves, reducing its allocation from 128 to 64 KiB. Counters are merged to the same global positions. Large range-table histograms are tiled without rejecting the originally supported 15-bit tables.
The generic tiled matrix engine uses two pipeline stages, reducing its footprint from 108 to 72 KiB while leaving its arithmetic tile and output overlay intact. Byte-fold combination selects a 96 KiB public resource cap and retains the existing exact fallback for larger shapes. Packed immutable lookup tables can remain in GPU memory rather than a 128 KiB shared copy. Occupancy selection uses the runtime's actual kernel resources for SM120.
Some separate lookup-forest fusion kernels still assume Hopper-sized buffers. The port selects their existing exact generic paths. The compact expert kernel remains fused. Further forest fusion is an optimization question, and its speed is not inferred from the expert experiment.
The first memory-corrected complete run passed the old histogram fault but failed because the engine reserves 24 GiB of VRAM even for a small model. The consumer-card layer reserves 4 GiB, retains the separate 2 GiB driver allowance and all allocation checks, and reports the actual native pool peak. The complete small-model run passes with this budget; its key-generation engine-pool peak is 603,979,776 bytes. No universal model-fit claim is made. The packed-table accessors pass 1,179,648 exact entry checks in two cohorts, separately from the complete field/proof computation.
FlashProve is pinned at 9e2bdd8ff5bf9c62f18263d7dac189b0400b260c. Patches retain Anthropic's Apache-2.0 attribution. Run as an ordinary Linux user, with newly created private work directories under ancestors that other accounts cannot modify. Preserve the upstream compiler probe, secure-path checks and verifier rules.
python prepare_consumer.py build/FlashProve
cd build/FlashProve
verifier/build.sh
FLASH_GPU_ARCH=sm_120a prover/build.sh
cd ../..
python cpu_study.py build/FlashProveThe measured compiler is CUDA 13.3.73. Upstream's supported version is CUDA 13.2.86. The build retains the warning and compiler arithmetic sample; this deviation must accompany all results. A correct build is required before the full cycle below. The work directory must be new, and its parent must already be private:
python flash_cycle.py build/FlashProve /absolute/private/new-runflash_cycle.py runs the original target-example script. Small research wrappers time the unchanged native commit/prove/verify programs separately. Only an accepted response permits exporting public configuration, verification key, request, answer and proof. Private proving keys and rejected responses are not published. Exact exit codes, verdict lines, commitment ID, coverage, commitment assumptions, proof-of-work line and result-v1 are retained.
The isolated expert bridge can be built with:
nvcc -O3 -std=c++17 -arch=sm_120a -DFLASH_EXPERT_COMPACT=1 -shared -Xcompiler=-fPIC \
-Ibuild/FlashProve/prover native/expert_bridge.cu -o build/libexpert.so
python expert_validation.py
python expert_validation.py --seed 20261209 --output results/expert-replication.json
python memory_validation.py build/FlashProve
python memory_validation.py build/FlashProve --seed 20261209 --output results/memory-replication.json
python verify_records.pyGPU checks use NumPy 2.2.6 and CuPy 13.6.0. patches/README.md distinguishes the fallback, compact expert, general memory and packed-table layers.
The accepted stored proof uses commitment ID 79a5a2bc7a469b40df73dedf40abeb740671e8ae8077738bd3743897aeb22183, with r=60, e=64, tokens 61..63 and y=yes; it does not establish a new GPU inference result. Its complete coverage and accounting statements are retained in the CPU record. Reported accounting bits are not interpreted as an independently established security level.
The C++/CUDA implementation is not formally verified by the Lean development. Native acceptance does not establish weight hiding or remove the verifier's stated external assumptions. All weights in these experiments are synthetic. There is no throughput, energy, production-model or mining-income claim yet.
The first accepted GPU cycle is retained as a complete record, with public proof artifacts. Its commitment is 4f351f1f2123409da095d4df1140fcd39a06719d9061163cb62c6719ad2f1943. Standalone process times are 36.33 s for commitment, 3.04 s for proving and 1.14 s for CPU verification; these are one observation, not a throughput distribution. Complete native coverage and assumptions accompany every proof. The full phase table includes all three commitments and the two added prompts. The synthetic weight construction is controlled; independent commitment randomness is not a population of independently trained models.
The final report maps every protocol gate to retained evidence and prioritizes larger-memory qualification, compact forest fusion and declared service-batching workloads as follow-up work. CPU CI builds the pinned verifier and checks stored fixtures and all five retained public GPU proofs; it cannot rerun SM120 kernels. Original research scripts are MIT licensed; patch modifications retain Apache-2.0 terms. See the full research protocol and related work.
The follow-up report records the disposition of the concrete next steps: new experiments, negative findings and measured resource limits. The earlier completed campaign remains available for historical comparison. Run python verify_followups.py for the added evidence checks.