Certification of bounds on expressions involving rounded operators

1. INTRODUCTION

• Gappa bounds arithmetic expressions over real and rational numbers and their computer evaluations, including ranges that prevent exceptional behavior and absolute or relative error bounds.It handles fixed- and floating-point formats.Source: §1 · p. 1
• Gappa can certify bounds for programs using advanced numerical techniques such as error compensation and iterative refinement.Source: §1 · p. 2
• Gappa generates formal certificates for users who need not write proofs in a formal system, and simplifies valid proofs to reduce certification time.A companion theorem library lets proof assistants check the certificates; the paper reports Coq use and ongoing work toward HOL Light.Source: §1 · p. 2
• Gappa combines interval arithmetic, dyadic fractions, and rewriting rules, exhaustively searches its built-in facts and techniques, and follows user hints to incorporate additional techniques.Source: §1 · p. 2
• Gappa’s stated goal is to support numerical applications using floating- and fixed-point arithmetic that must meet Common Criteria Evaluation Assurance Level 7.Source: §1 · p. 2

2. DESCRIPTION OF THE INPUT LANGUA GE OF GAPP A

• The computed expression y uses rounded operators and constants, while ideal value Y replaces them with exact operators and constants and restores terms optimized out of the implementation.The distinction supports reasoning about the computed value and its error relative to the ideal value.Source: §2 · p. 3
• To certify code correctness, one may need an interval containing all possible y values to guarantee no overflow or invalid value, or an interval for y − Y or (y − Y)/Y to guarantee y is accurate and close to Y.Source: §2 · p. 3
• An input file comprises aliases, the proposition, and hints; when successful, Gappa produces a proof file checkable by Coq or HOL Light.Coq checks it using the companion library, while HOL Light uses a set of axioms until a companion library becomes available.Source: §2 · p. 3

2.1 F o rmalizing the p rop osition (PROP) that Gappa p roves

• A proposition may combine enclosures using conjunction, disjunction, implication, or negation; enclosures state inequalities or bounded ranges over expressions.Range endpoints and inequality bounds are numerical constants, and ranges may be left unspecified with question marks.Source: §2.1 · p. 3
• Expressions can use constants, identifiers, user-defined or built-in rounding operators, and arithmetic operators including fused multiply-add.The listed arithmetic operators include addition, subtraction, multiplication, division, absolute value, square root, and negation.Source: §2.1 · p. 3
• When an enclosure uses question marks, Gappa suggests intervals that make the proposition provable; in the example, it gives x + y ∈ [3, 5], the tightest such interval.Question marks are disallowed if, after Section 3.1 transformations, they would imply unspecified hypotheses.Source: §2.1 · p. 3

2 PROP: REAL LE SNUMBER

• The proposition grammar includes the form REAL IN '?'.Source: §2 · p. 4
• The proposition grammar includes the form REAL GE SNUMBER.Source: §2 · p. 4
• PROP AND PROP is a listed proposition form.Source: §2 · p. 4
• PROP OR PROP is a listed proposition form.Source: §2 · p. 4
• PROP IMPL PROP is a listed proposition form.Source: §2 · p. 4
• NOT PROP is a listed proposition form.Source: §2 · p. 4
• Parentheses can enclose a proposition as '(' PROP ')'.Source: §2 · p. 4

16 FUNCTION_PARAMS_AUX: FUNCTION_PARAM

• FUNCTION_PARAMS_AUX is followed by a comma and FUNCTION_PARAM in the supplied production fragment.The fragment is labeled “17” and names FUNCTION_PARAMS_AUX.Source: §16 · p. 4

18 FUNCTION_PARAMS: /* empty */

• The passage specifies the FUNCTION_PARAMS form as '<' FUNCTION_PARAMS_AUX '>', placing literal opening and closing angle-bracket tokens around FUNCTION_PARAMS_AUX.Source: §18 · p. 4

20 FUNCTION: IDENT FUNCTION_PARAMS

• An empty production is permitted for PROG.The passage lists PROG with an empty body.Source: §20 · p. 4
• A PROG may consist of IDENT EQUAL REAL followed by a semicolon.This production defines an identifier assignment to a real value.Source: §20 · p. 4

Interval limitations

• Gappa’s dyadic endpoints can make a requested interval too tight to represent, causing the goal to be replaced by an empty interval.For example, it cannot prove 13/10 in [1.3,1.3], because the empty set is the largest representable subset of {1.3}.Source: §26 · p. 5
• Although bounds are numerical constants, users can express linear dependencies by transforming expressions, such as bounding (y − Y)/i rather than y − Y in an interval scaled by i.The enclosure y − Y ∈ [−i × 10^-6, i × 10^-6] is disallowed, while (y − Y)/i ∈ [−10^-6, 10^-6] is allowed.Source: §26 · p. 5

2.2 Definitions of aliases to describe program behavior (PROG)

• Aliases let users name expressions for later definitions, propositions, and hints, avoiding unwieldy expressions in software-generated proof obligations.An identifier can be aliased only once and cannot be aliased after use as an unbound variable.Source: §26 · p. 5

Rounding operators

• Rounding operators model numerical operations as real functions that produce values rounded to a target format and predefined rounding mode.For truncated hardware or compound operators that cannot be modeled as exact computation followed by rounding, Gappa uses underspecified functions with a known relative-error bound; a supplied minimum exponent limits which error assumptions apply.Source: §26 · pp. 5–6

2.3 Rewriting expressions to suppress some dependency effects

• Correlated expressions can make naively computed error intervals useless, so Gappa rewrites error expressions to suppress dependencies.For y = rnd(a + b) and Y = A + B, it separates the rounding error from the input error, then rewrites (a + b) − (A + B) as (a − A) + (b − B).Source: §26 · pp. 6–7
• Gappa’s built-in rewriting rules and approximation heuristics verify many properties in common numerical applications, but the tool is not a complete decision procedure.Users can add approximation hints or direct rewriting rules when automatic proof fails; Gappa warns when an approximation hint is unnecessary because it inferred the property itself.Source: §26 · p. 8

• User-defined rewriting rules generate hypotheses that must be proved independently; Gappa checks whether a primary expression equals its secondary form and warns when it does not.A primary-to-secondary rule is valid only if every primary value is contained in the computed enclosure of the secondary expression.Source: §26 · p. 8
• Equivalent expressions can yield different interval bounds whose intersection tightens known bounds, and Gappa explores their directed quantity graph breadth-first until the goal is reached or bounds stop evolving.Tightening one quantity can lead to tighter bounds on other quantities.Source: §26 · pp. 8–9

2.4 Sub-paving the range of some quantities by bisection (second use of HINT)

• Range paving lets Gappa prove separate tiles when rewriting cannot provide the different proof structures needed across a range.In the example, Gappa notices that rnd(y) − y is zero in a region only when the final line is supplied.Source: §26 · p. 9
• Bisection hints can evenly split a range, divide it at user-specified points, or use dichotomy to find a paving satisfying a goal; multiple hints can be sequenced, but higher-dimensional paving risks combinatorial explosion.Source: §26 · p. 9

3.1 Work on the logical proposition (PROP)

• Gappa decomposes propositions into implications with enclosure conjunctions on the left and conjunctions or disjunctions on the right; unspecified ranges are allowed only on the right.Left-side inequalities are used only when Gappa can enclose them by other means; for a right-side disjunction, Gappa searches for a sub-term that always holds and fails if it cannot find one.Source: §3 · p. 10

3.2 Structure of the generated proof

• Gappa’s internal BND, ABS, FIX, and FLT predicates describe enclosure, absolute-value bounds, and fixed- or floating-point representability; FIX and FLT help detect exact rounded operations.FIX and FLT capture that computer numbers form discrete subsets of the reals, unlike the connected sets represented by intervals.Source: §3 · p. 10
• Gappa’s companion library uses computable Boolean expressions in theorem hypotheses, formally proving that when they evaluate to true, the standard hypotheses hold and the theorem applies.This simpler form of reflection is used in Coq; the PVS interval-arithmetic library shows interval-computation proofs are also attainable in other proof assistants.Source: §3 · p. 13

3.3 Widening intervals to speed up proof certification

• Dyadic-fraction interval bounds make Boolean proof conditions computable, and the checker only verifies those conditions, so any sufficiently wide valid interval can be used.The checker need not compute dyadic numbers or require the sharpest enclosing interval.Source: §3 · p. 13
• Gappa finds a correct proof path, then greedily works backward from the last proved results, widening intervals to simplify dyadic numbers and speed proof checking.Simplified numbers can considerably speed verification in Coq, which is slower than a specialized mathematical library; the time spent searching for a better sub-paving is negligible by comparison.Source: §3 · pp. 13–14

Future development

• The work already enables guarantees for many useful functions, and the authors plan to extend Gappa if continued use reveals practices it cannot handle appropriately.The software, user guide, and project details are available online.Source: §4 · p. 14

Applications

• Gappa certifies CRlibm’s elementary functions with correct rounding in all four IEEE-754 modes and performance comparable to standard mathematical libraries, and supports CGAL filters and delayed linear algebra over finite fields.The passage also describes a single-precision exponential example and cites an earlier HOL Light validation and an almost correctly rounded function.Source: §4 · p. 14, Figure 2 · p. 15

Proof generation and checking

• Gappa precomputes intervals and generates proofs for external checkers that need only integer addition, multiplication, and comparison, not rational or real arithmetic or complex Coq tactics.The authors aim to generate proofs for checkers beyond Coq.Source: §4 · p. 14

Program control flow

• Branches and loops are outside this work’s scope; the authors instead propose combining Gappa with Why, which handles branches and supports verification of larger software.Why certifies memory allocation and usage in hierarchically structured code with functions and assertions; a floating-point formalism designed with Gappa was added to Why.Source: §4 · pp. 14–15
• Fluctuat handles loops by computing invariants; given those invariants, Gappa can certify numerical code and can reject erroneous Fluctuat results.Fluctuat’s results serve as oracles that Gappa verifies.Source: §4 · p. 15