Hyperreal Specifications for Continuous Sparse Data Computations
summary
A new relational separation logic called LGTM∞ specifies array-encoded geometric data as code (getter procedures) and generalises hypersafety to real-indexed hypersafety for continuous integrals, letting proofs relate uncountably many implementations to mathematical functions. The implementation embeds into lin improver and verifies kernels like CSR×dense (reported as 36 lines of proof) and bilinear interpolation; average proof-cut ratio is 2.55 and the approach yields up to a 10x reduction versus unary proofs. Continuous extensions handle integrals over real indices.
AI-written summary · about