[Submitted on 15 Sep 2026 (v1), last revised 15 Sep 2026 (this version, v4)]
Title:A Verified WebAssembly Solver for a Two-Dimensional Euler Riemann Problem
Abstract: A LeanExe-compiled WebAssembly solver has kernel-checked proofs of complete execution, bounded memory, and numerical invariants for a two-dimensional Euler Riemann problem on grids from 2 by 2 through 800 by 800. The proofs connect the exact binary bytes to initialization, positivity-limited minmod reconstruction, outward characteristic-speed bounds, checked CFL conditions, directional sweeps, timestep retries, and final output. Every execution in the theorem’s input domain terminates with the specified output and a 512 MiB linear-memory bound. Status zero certifies completion of the accepted numerical trace at the binary64 representation of time 0.8. Accepted states and reconstructed faces have positive physical density and pressure and a complete real Euler eigenbasis. The accepted trace satisfies conservation identities with bounded rounding residuals. The same binary completed 192 by 192 and 800 by 800 calculations in 176.7 seconds and 3 hours 58 minutes, respectively. Checked counterexamples exhibit a negative-pressure reconstructed face and a characteristic-speed underestimate in the preceding nearest-rounded helper. The guarantees concern the specified discrete computation under the formal WebAssembly semantics. Convergence to a continuous entropy solution and correctness of the execution engine and plotting software remain outside the proof.
| Comments: | 15 pages, 2 figures |
| Subjects: | Logic in Computer Science (cs.LO); Programming Languages (cs.PL) |
| Cite as: | marXiv:2609.00006 [cs.LO] (or marXiv:2609.00006v4 [cs.LO] for this version) |
Submission history
[v1] Tue, 15 Sep 2026 22:59:51 UTC (1,087 KB)
[v2] Tue, 15 Sep 2026 23:12:01 UTC (1,112 KB)
[v3] Tue, 15 Sep 2026 23:57:04 UTC (1,112 KB)
[v4] Wed, 16 Sep 2026 00:02:49 UTC (1,113 KB)