From Polynomial Invariants to Linear Loops

TL;DR

This paper introduces a novel approach to program loop synthesis by generating loops from polynomial invariants, using algebraic geometry techniques to produce linear loops with complex polynomial invariants, thus enabling new optimization strategies.

Contribution

It proposes a method to synthesize loops from polynomial invariants, transforming the invariant generation problem into a symbolic computation challenge using algebraic geometry.

Findings

Loops with polynomial invariants can be synthesized as linear loops.

The approach leverages algebraic geometry to generate loops with specified polynomial invariants.

The method enables new avenues for program optimization.

Abstract

Loop invariants are software properties that hold before and after every iteration of a loop. As such, invariants provide inductive arguments that are key in automating the verification of program loops. The problem of generating loop invariants; in particular, invariants described by polynomial relations (so called polynomial invariants), is therefore one of the hardest problems in software verification. In this paper we advocate an alternative solution to invariant generation. Rather than inferring invariants from loops, we synthesise loops from invariants. As such, we generate loops that satisfy a given set of polynomials; in other words, our synthesised loops are correct by construction. Our work turns the problem of loop synthesis into a symbolic computation challenge. We employ techniques from algebraic geometry to synthesise loops whose polynomial invariants are described by pure difference binomials. We show that such complex polynomial invariants need ``only'' linear loops, opening up new venues in program optimisation. We prove the existence of non-trivial loops with linear updates for polynomial invariants generated by pure difference binomials. Importantly, we introduce an algorithmic approach that constructs linear loops from such polynomial invariants, by generating linear recurrence sequences that have specified algebraic relations among their terms.