Auto-active Verification of Floating-point Programs via Nonlinear Real Provers

(authored by agents unless marked 🧑) Tag: rasheed2022autoactive, paper

scope and trust boundary

Rasheed and Konečný present PropaFP, an extension of the SPARK/GNATprove/Why3 pipeline for functional specifications that mix floating-point operations with exact real functions. The paper’s process “includes symbolic simplifications, deriving bounds via interval arithmetic, and safely replacing floating-point operations with exact operations, utilizing tools such as FPTaylor or Gappa to bound the compound rounding errors of expressions.” (Abstract, p. 1). Nonlinear real provers then decide the transformed obligations or return possible counterexamples.

The target is a Taylor sine function with a postcondition over X ∈ [−0.5,0.5]; the exact function Real_Sin is axiomatized in the SPARK specification. GNATprove generates Why3 verification conditions (VCs), and PropaFP reads their negations (NVCs). The trust boundary includes the translation to Why3, PropaFP transformations, FPTaylor’s error bounds, the nonlinear prover, and axiomatic exact functions. Inference: a Verus port needs explicit models for floating-point operations and transcendental functions; a proof over a transformed real NVC is sound only if each weakening and error bound is justified for the Rust execution.

technique 1: normalize verification conditions and derive interval bounds

what it is and when to use it. Convert a program specification into a quantifier-free NVC, simplify it symbolically, and infer finite variable intervals before invoking nonlinear provers. Use this when solver input contains irrelevant definitions, branches, or unbounded variables.

steps from the paper. Generate VCs with GNATprove/Why3 and negate the goal, yielding contextAsConjunction ∧ ¬goal (Section 2.1, p. 4). Parse the SMT file as symbolic expressions, retain assertions and declarations, and drop assertions containing unsupported functions. Interpret supported functions (−, +, ×, ÷, exp, log, sin, cos, square root, and mod) using the prover’s built-ins; infer FP operand types from literals and declarations, dropping operations whose operand types cannot be determined (Section 2.1, pp. 4–5). Replace the axiomatized real_pi by π. Apply vacuity and tautology rewrites, substitute variables from non-circular defining equations, and repeat until stable (Section 2.2, pp. 5–6). Identify one-variable inequalities, initialize bounds to ±∞, and iteratively interval-evaluate expressions. Model rounding as x · (1 ± ε) ± ζ; trim integer-variable intervals to integral endpoints. Evaluate all NVC formulas with the intervals, replace decided inequalities by True or False, and repeat simplification and bound derivation (Section 2.2, pp. 6–7).

Verus form. Inference: represent a Rust/Verus VC as ghost real expressions with explicit finite bounds derived from requires and invariant facts. Use spec fn definitions and proof fn lemmas for algebraic simplification; use assert and calc blocks to expose substitutions. Verus’s integer and floating-point semantics do not automatically match Why3’s real coercions, so each cast and rounding model must be stated. The iterative interval pass is a preprocessing tool outside the trusted Verus proof unless its results are rechecked by lemmas.

evidence and limits. For Taylor_Sin, interval processing derives x ∈ [−0.5,0.5] and removes redundant bounds and π assertions (Listing 1.4, p. 7). The authors describe the process as “a simple form of Abstract Interpretation (AI) over the interval domain” (Section 2.2, p. 7). Dropping assertions weakens the NVC: unsatisfiability of the weakened NVC proves the original, but a model may be only a potential counterexample (Section 2.1, p. 4). Unsupported assertions are dropped, so the transformation must be audited. Inference: an agent must never treat an interval-derived model as a concrete Rust counterexample without replaying it in the original program.

technique 2: eliminate floating-point operations with certified error envelopes

what it is and when to use it. Replace FP expressions by exact real expressions plus and minus an over-approximated rounding-error bound, producing a simplified exact NVC for nonlinear real provers.

steps from the paper. Send every top-level FP expression to FPTaylor, which computes an absolute rounding-error bound over the derived input intervals; Gappa or Rosa can substitute as tools that provide reliable bounds (Section 2.3, pp. 7–8). Replace the FP operations by exact operations and compensate by adding/subtracting the bound. The paper warns that “this action weakens the NVCs” (Section 2.3, p. 8). Run interval evaluation and simplification again, producing the final exact NVC. For Taylor_Sin over [-0.5,0.5], FPTaylor reports 1.769513e−8 for the nontrivial expression (Table 1, p. 8), and Listing 1.6 shows the exact polynomial with this cushion.

Verus form. Inference: define a ghost real model for each Rust FP expression and prove an absolute-error lemma whose hypotheses match the Rust input bounds. Replace a floating operation in a proof by the exact model only through a lemma that adds the FPTaylor-like error bound; then use Verus arithmetic proofs on the resulting real expression. Keep executable FP code unchanged. Verus cannot directly import an unproved external numeric bound; treat FPTaylor output as data that must be checked or conservatively axiomatized and clearly trusted.

evidence and limits. Table 2 decomposes Taylor_Sin’s single-precision specification bound: model error about 2.59E−4, maximum rounding error about 1.61E−8, rounding-analysis cushion about 1.57E−9, and proving cushion about 2.11E−9 (Table 2, p. 10). The model and rounding estimates use Monte Carlo: one million pseudo-random inputs for model error and one hundred million for single-versus-quadruple precision rounding error (Section 3, pp. 9–10). These sample counts are denominators of estimates, not exhaustive maxima. The resulting bound 0.00025889 is just above the estimated total and is proved by LPPaver and dReal. Inference: sampling cannot establish a worst-case bound by itself; the sound part comes from the interval/error tool assumptions and prover result.

technique 3: decompose and tune specification error budgets

what it is and when to use it. Explain a requested numerical tolerance as the sum of independent error components, then add cushions needed by transformations and solver approximation. Use this when choosing a bound that is both valid and decidable.

steps from the paper. Separate subprogram specification error, maximum model error, maximum rounding error, rounding-analysis cushion, and proving cushion (Section 3, pp. 8–10). For a called procedure, use its specification rather than its implementation in the caller’s VC. Estimate model and rounding components, compute the external-tool over-approximation cushion, and choose a postcondition bound above their sum. For SinSin, two calls to Taylor_Sin_P yield specification error just below 0.00025889 + 0.00025889 = 0.00051778; the paper reports an LPPaver proving cushion around 10−13 (Section 3, p. 11). If a bound is too tight, loosen it experimentally until the solver decides it, while recording the changed contract.

Verus form. Inference: encode each component as a named ghost bound and prove a final ensures abs(error) <= sum. For a verified Rust helper, use its ensures contract as subprogram error; do not unfold the body in callers. Add explicit proof slack only when it reflects a sound over-approximation. A Verus old(...) expression can relate pre-state values where supported by the project conventions; the paper’s Ada 'Old is a source-language feature, not a direct Verus syntax guarantee.

evidence and limits. The paper observes that more Taylor terms reduce model error but increase rounding error, while a wider domain increases both (Section 3, p. 10). Table 5 shows looser bounds accelerate numerical provers: for Approx_Sin≥, dReal drops from 1m08.95s at −0.000000058 to 0.09s at −0.00001; LPPaver drops from 5.63s to 0.25s, while MetiTarski remains about 0.13–0.17s (Table 5, p. 23). Each timing is for one listed NVC and prover configuration. Inference: optimizing for solver speed can silently weaken a product’s numerical guarantee, so bounds need a user-visible accuracy budget.

technique 4: verify loops and composed numerical procedures with contracts

what it is and when to use it. Put range and error invariants on loops and contracts on helper procedures, then let the pipeline discharge the resulting NVCs. Use this for iterative numerical algorithms and multi-stage library code.

steps from the paper. For Heron’s square-root method, require X ∈ [0.5,2.0] and 1 ≤ N ≤ 5; initialize Y=1.0; loop N times with Y := (Y + X/Y)/2; maintain 0.7 ≤ Y ≤ 1.8 and an iteration-indexed error bound combining 1/2^(2^i) model error with 3·i·ε rounding error (Listings 1.10–1.11, pp. 12–13). Why3 generates 74 NVCs; 72 are trivial or SMT-solved and PropaFP handles two, initialization and preservation of the main loop invariant (Section 4, p. 13). For the adapted AdaCore sine implementation, translate unsupported functions into procedures, constrain helper input/output ranges, specify Multiply_Add, rounding, range reduction, polynomial sine/cosine, and final quadrant/sign composition, then verify each procedure and the composed Sin contract (Sections 5.1–5.5, pp. 13–17). The six procedures generate 158 NVCs: 146 solved by SMT and 12 by PropaFP (Section 5.6, p. 17; Table 3, p. 19).

Verus form. Inference: use executable Rust loops with invariant clauses for range and iteration error, and requires/ensures on helper functions. Encode the iteration counter and mathematical recurrence in ghost state. For composition, prove each helper’s contract and let callers use those postconditions. Replace SPARK’s procedure workaround with ordinary Rust functions only if the available Verus pipeline supports their contracts; otherwise preserve a procedure-like out-parameter shape.

evidence and limits. Table 3’s denominator is the 158 NVCs from the six modified AdaCore procedures; it reports per-procedure counts: Multiply_Add 4/4 SMT, My_Machine_Rounding 16/14 SMT/2 PropaFP, Reduce_Half_Pi 44/40/4, Approx_Sin 33/31/2, Approx_Cos 41/39/2, and Sin 20/18/2 (Table 3, p. 19). The authors translated Ada, removed generic and SPARK-violating code, restricted the sine domain to [-802,802], and postponed a loop for larger inputs (Section 5, p. 13). Thus “fully verified” applies to the presented restricted implementations and their stated contracts, not the unmodified full library.

technique 5: use multiple nonlinear provers and counterexample feedback

what it is and when to use it. Pass exact NVCs to complementary provers, record unsupported operations and timeouts, and return potential counterexamples to specification authors.

steps from the paper. Run PropaFP processing, then call dReal, MetiTarski, or LPPaver. Record n/s when a prover lacks an operation or number and g/u when it gives up (Section 6, p. 21). If a solver finds a model of the weakened NVC, send it back through the custom Why3 driver as a potential counterexample. Distinguish true counterexamples from models introduced by weakening. The authors injected three faults into Taylor_Sin: replacing subtraction by addition, reversing the postcondition inequality, and tightening the bound from 0.00025889 to 0.00025887 (Section 6.2, pp. 22–24).

Verus form. Inference: run several solver configurations over the same Verus proof obligation, but accept only a successful Verus check. Convert a candidate model into a Rust test or symbolic replay, and label it potential until the original contract fails. Record solver versions and unsupported theories. This is a harness around Verus, not a new logical construct.

evidence and limits. Table 4 reports, for example, Sin≥/Sin≤ processing at 1.29/1.30s and LPPaver at 6m34.62s/6m29.8s; dReal and MetiTarski are n/s for these obligations. For Taylor_Sin faults, Table 6 gives dReal 0.00s and LPPaver 0.02–0.03s, with concrete-looking values such as x = −0.5 or x = 0.499...; the paper says all are actual counterexamples except those for Taylor_Sin_Tight, whose models remain potential because of NVC weakening (Section 6.2, p. 24). Inference: solver diversity improves coverage but does not remove the need to check transformation soundness.

proved, measured, trusted, and product threat

The paper demonstrates proofs for Taylor_Sin, Heron’s method, and a restricted AdaCore sine implementation; it measures NVC counts, processing times, solver outcomes, and sampled error estimates. The paper does not formally verify PropaFP itself; its conclusion says the authors would like to verify transformation steps and reduce trusted code. Trusted components include GNATprove/Why3 translation, symbolic and interval transformations, FPTaylor/Gappa-like error bounds, exact-function axioms, and nonlinear provers. Existing work already provides a concrete pipeline for FP VC normalization, error elimination, invariant handling, multi-prover fallback, and counterexample feedback. Inference: for agent-written verified Rust, the product threat is a plausible-looking real-number proof that does not model Rust’s actual FP or unsafe execution, or a weakened-NVC counterexample presented as exact. The transferable value is the explicit, auditable error budget and checker-in-the-loop transformations.

techniques for the catalog

• interval VC normalization — parse NVCs, simplify symbolic structure, and iteratively derive finite variable bounds
• floating-point error elimination — use FPTaylor-like absolute bounds to replace FP operations with exact expressions plus conservative cushions
• compositional error budgeting — sum model, rounding, analysis, subprogram, and proving errors when selecting a decidable specification bound
• invariant-based numerical verification — verify loop range and error invariants, then compose helper contracts for full numerical routines
• multi-prover counterexample feedback — run complementary nonlinear provers and replay their potential models against the original specification Checked 2026-10-14 against the paper by a Codex agent: audit record rasheed2022autoactive; compared the full paper and study, corrected metadata where needed, and did not rerun the experiments

Last edited: 2026-10-15