Draft. Not linked from the writing index. Outline below, to be written.
A proof pipeline over multi-hour GPU workloads on NASA-ISRO NISAR radar data: a RISC Zero zkVM guest re-executing a Fiat-Shamir residual check, wrapped in Groth16 for on-chain verification, with Intel TDX attestation over the off-chain engine.
The Fiat-Shamir seed committed only to public inputs, which are fixed in advance. So the sampled column set is computable before choosing what to publish.
The certificate verifies. Every check passes. 999,744 of 1,000,000 output columns are wrong.
TODO: walk through construction, and state precisely what an honest verifier would have had to check to catch it.
256 samples miss a 0.1% localized corruption 77% of the time.
TODO: cross-reference the hypergeometric argument already written up in Your Spot Check Cannot See the Fault You Are Paid to Catch.
A full RISC Zero receipt ladder measured end to end: composite 1,496 B, succinct 224,090 B, Groth16 1,361 B with a 260 B seal, 5.06 ms local verify, 249,749 gas and $0.0042 to verify on chain.
Separately, a GPU probe measuring 53.44 TFLOPS fp16 at 22% of peak, and finding that the PCIe link reports Gen 3 under load on a G2 instance.
TODO: the seed has to commit to the output, not only the input. State it as the rule and show what it costs.
The SBAS design matrix turned out to be a permutation matrix, so the certified residual is identically zero for any input, and the published 2.3174e-7 is float32 cumsum-then-diff rounding noise. The proof therefore proves nothing about the physics.
TODO: say this plainly and early, not at the end.