Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Linear Loop Synthesis for Quadratic Invariants

S. Hitarth, George Kenison, Laura Kovács, Anton Varonka

TL;DR

The paper tackles loop synthesis for polynomial invariants by focusing on quadratic invariants and constructing loops whose affine or linear updates preserve these invariants, making correctness by construction feasible. It develops a diagonalisation-based methodology: reduce general quadratic invariants to diagonal forms, solve the resulting equations for rational solutions, and build update matrices that preserve the invariant to yield infinite, nonrepeating state sequences. The key contributions include a decision procedure for the existence of nontrivial linear loops for a given quadratic invariant and a constructive method to synthesize affine loops for arbitrary quadratic equations, with detailed treatment of nondegenerate and degenerate cases and appendices on isotropy and synthesis procedures. This framework provides a principled, algebraic route to generate correct-by-design loop fragments that sample points on algebraic varieties, aiding formal verification and invariant-driven program synthesis with rational-valued states.

Abstract

Invariants are key to formal loop verification as they capture loop properties that are valid before and after each loop iteration. Yet, generating invariants is a notorious task already for syntactically restricted classes of loops. Rather than generating invariants for given loops, in this paper we synthesise loops that exhibit a predefined behaviour given by an invariant. From the perspective of formal loop verification, the synthesised loops are thus correct by design and no longer need to be verified. To overcome the hardness of reasoning with arbitrarily strong invariants, in this paper we construct simple (non-nested) while loops with linear updates that exhibit polynomial equality invariants. Rather than solving arbitrary polynomial equations, we consider loop properties defined by a single quadratic invariant in any number of variables. We present a procedure that, given a quadratic equation, decides whether a loop with affine updates satisfying this equation exists. Furthermore, if the answer is positive, the procedure synthesises a loop and ensures its variables achieve infinitely many different values.

Linear Loop Synthesis for Quadratic Invariants

TL;DR

The paper tackles loop synthesis for polynomial invariants by focusing on quadratic invariants and constructing loops whose affine or linear updates preserve these invariants, making correctness by construction feasible. It develops a diagonalisation-based methodology: reduce general quadratic invariants to diagonal forms, solve the resulting equations for rational solutions, and build update matrices that preserve the invariant to yield infinite, nonrepeating state sequences. The key contributions include a decision procedure for the existence of nontrivial linear loops for a given quadratic invariant and a constructive method to synthesize affine loops for arbitrary quadratic equations, with detailed treatment of nondegenerate and degenerate cases and appendices on isotropy and synthesis procedures. This framework provides a principled, algebraic route to generate correct-by-design loop fragments that sample points on algebraic varieties, aiding formal verification and invariant-driven program synthesis with rational-valued states.

Abstract

Invariants are key to formal loop verification as they capture loop properties that are valid before and after each loop iteration. Yet, generating invariants is a notorious task already for syntactically restricted classes of loops. Rather than generating invariants for given loops, in this paper we synthesise loops that exhibit a predefined behaviour given by an invariant. From the perspective of formal loop verification, the synthesised loops are thus correct by design and no longer need to be verified. To overcome the hardness of reasoning with arbitrarily strong invariants, in this paper we construct simple (non-nested) while loops with linear updates that exhibit polynomial equality invariants. Rather than solving arbitrary polynomial equations, we consider loop properties defined by a single quadratic invariant in any number of variables. We present a procedure that, given a quadratic equation, decides whether a loop with affine updates satisfying this equation exists. Furthermore, if the answer is positive, the procedure synthesises a loop and ensures its variables achieve infinitely many different values.
Paper Structure (15 sections, 10 theorems, 19 equations, 1 algorithm)

This paper contains 15 sections, 10 theorems, 19 equations, 1 algorithm.

Table of Contents

  1. Introduction
  2. Loop Synthesis.
  3. Preliminaries
  4. Linear and quadratic forms
  5. Loops and Loop Synthesis
  6. Solving Quadratic Equations
  7. Solutions of Quadratic Equations in Two Variables
  8. Solving Isotropic Quadratic Forms
  9. Finding Isotropic Vectors
  10. Quadratic Forms: Linear Loops
  11. Rational Diagonalisation
  12. Diagonal Quadratic Forms
  13. Arbitrary Quadratic Equations: Affine Loops
  14. Non-Degenerate Quadratic Forms
  15. Degenerate Quadratic Forms

Key Result

Lemma 8

For all $a,b \in \mathbb{Q}\setminus\{0\}$, Pell's equation $x^2+\frac{b}{a}y^2=1$ has a rational solution $(\alpha, \beta)$ with $\alpha \not\in \{\pm 1, \pm \frac{1}{2}, 0\}$ and $\beta \neq 0$.

Theorems & Definitions (19)

  • Definition 1: Quadratic form
  • Definition 2
  • Definition 3: Linear form
  • Definition 4: Linear loop
  • Definition 5: Affine loop
  • Remark 6: Linear and Affine Loops
  • Remark 7: Loop Synthesis and Polynomial Equation Solving
  • Lemma 8
  • Lemma 9
  • Lemma 10
  • ...and 9 more