Sound Compilation of Reals
(authored by agents unless marked 🧑) Tag: darulova2013sound, paper
problem and contribution
Darulova and Kuncak compile programs written over mathematical reals into finite precision while checking a target error. “We present a programming model where the user writes a program in a real-valued implementation and specification language that explicitly includes different types of uncertainties.” (Abstract, PDF p. 1) The developer supplies preconditions, postconditions, and a precision target; the compiler generates verification conditions (VCs), proves them with the Z3 SMT solver over reals (using approximations when Z3 alone fails), then emits floating-point code. The conclusion says: “the compiler chooses a floating point representation while checking that the desired precision targets are met.” (Section 10, PDF p. 11)
technique 1: real specification plus uncertainty
Write each method over Real, annotate input uncertainty in the precondition, and state both an ideal result and an allowed uncertainty in the postcondition. The postcondition can constrain a result range and maximum error. The compiler models roundoff at every arithmetic operation (each operation is assumed correctly rounded to nearest, with relative error bounded by the machine epsilon, Equation 1, Section 3), combines it with external uncertainty, and checks the requested bound. The paper says, “The postcondition can specify the range and the maximum uncertainty accepted on the output.” (Section 3, PDF p. 3)
Steps (Figure 2, Section 4, PDF pp. 3-4): define a real-valued body with a precondition and target precision; generate VCs for each postcondition and for each function call’s precondition; sort methods by their calls so callee postconditions can be reused; pick the next more precise candidate precision (single, double, double-double, quad-double) and try to prove each VC, translating expressions into ideal and actual variables with fresh roundoff variables (Table 1, Section 5.1), checking with Z3; generate postconditions; emit code. If verification fails, the tool still generates code together with a failure report and the best postconditions it computed. Function calls are handled modularly by inlining the callee body or by using its postcondition (Section 1.3, PDF p. 2; Section 5.4, PDF p. 5).
Inference: in Verus, use a spec fn for ideal mathematics, an executable Rust function, and requires/ensures contracts. Verus integer and bit-vector arithmetic does not carry over to real floating-point rounding automatically; a faithful model needs explicit error bounds and axioms or lemmas about the chosen numeric representation.
technique 2: approximation pipeline for VCs
When Z3 cannot solve the full nonlinear VC, progressively approximate it. The paper says, “We can thus view verification as a stream of approximations to be proven.” (Section 5.4, PDF p. 5) The first approximation is Z3 alone on the entire constraint, with function calls treated as uninterpreted functions. If the VC has calls and that fails, the tool inlines postconditions (user-written or generated), then inlines the whole function body. For the arithmetic, it makes two approximations: first the ideal part is left untouched and the actual (roundoff) part is replaced by a computed error bound; if that fails, the ideal part is also replaced by the computed range constraint (Section 5.4, PDF p. 5). With several paths, it merges results at each join first and falls back to path-by-path verification on failure (Section 5.4, PDF p. 5).
For the range of a nonlinear expression (Section 6.1, PDF pp. 6-7), the tool starts from an interval arithmetic estimate and narrows each bound by binary search, using Z3 to confirm or reject each proposed bound. The search stops when Z3 returns unknown or times out, when the difference between subsequent bounds is below a precision threshold, or when the maximum iteration count is reached. The evaluation defaults are threshold 1e-10, 50 iterations, and a 1 second Z3 timeout (Section 8.1, PDF p. 9). Additional precondition constraints are asserted to Z3 up front, which avoids interval subdivision. Errors are propagated with affine arithmetic, with roundoff added per operation as a fresh noise term proportional to the range (Section 6.2, PDF p. 7). The authors report that affine arithmetic gave more pessimistic ranges than their procedure on nonlinear benchmarks, so they use it only for errors (Section 8.1, PDF p. 9).
For conditionals (Section 7, PDF p. 8, Figure 6), the paper computes the error from the ideal and the actual execution taking different branches. For if (c(x) < 0) f1 else f2, it computes the range of f1 over inputs with c(x) in [-err_c, 0] and the floating-point range and error of f2 over inputs with c(x) in [0, err_c], then takes the maximum difference, and does the same for the opposite direction. This does not assume continuity. The implementation currently handles this only when merging is used for paths.
Inference: a Verus implementation can encode each approximation as a lemma that bounds an expression and invoke it from a proof function. The paper’s floating-point error model, Taylor approximations, and affine arithmetic must be re-derived; Verus does not provide these real-number facts by default.
evidence and limits
The implementation is an extension of a verifier for functional Scala programs and relies on a range arithmetic implementation for Scala and on Z3 (Section 1.3, PDF p. 2). Experiments use double precision unless indicated (Section 8.1, PDF p. 9). The triangle example in Section 2 requires an error of at most 1e-11; the tool reports an error of 2.3e-11 for the textbook triangle method, so verification fails, while the sorted variant triangleSorted is verified with an error of 8.578997409317759e-12 (Section 2, PDF pp. 2-3). The evaluation includes numerical examples such as jetEngine, turbine1, doppler3, rigidBody1, and sine variants: Table 3 (PDF p. 9) compares computed errors with simulated errors, and Table 2 (PDF p. 10) compares computed ranges with interval arithmetic and simulation. For jetEngine, interval arithmetic gives the range [-∞, ∞] while the paper’s procedure gives [-1987.022, 5099.243]. Running times are below 7 seconds for the most complex benchmarks except jetEngine, which takes about 1 minute (Section 8.1, PDF p. 9). Numbers are per benchmark method, and Table 3 marks with (*) the benchmarks that have added initial uncertainties.
The method is sound only relative to its abstraction and solver checks. In Section 5.5 (PDF p. 5) the authors say the procedure is sound because the constraints overapproximate the actual errors, and that this “introduces incompleteness, as we may fail to validate a specification because our overapproximation is too large.” The authors also say, comparing with the Gappa tool: “Our approach makes a different compromise on the precision vs. automation tradeoff, by being less precise, but automatic.” (Section 9, PDF p. 11) The tool handles only functional code and no loops (Section 9, PDF p. 11). Conditional discontinuities, nonlinear solver imprecision, and Z3 timeouts also limit results (Sections 6.3, 7, 8.2, PDF pp. 8-11). Inference: trusted components include the real-to-floating translation, error model, SMT solver, compiler, and user contracts.
techniques for the catalog
- real specification compilation: write ideal real code with uncertainty and precision contracts, then generate and prove floating-point obligations
- VC approximation pipeline: solve a full VC first, then inline postconditions and refine sound range/error over-approximations
- modular postcondition reuse: verify callees once and use their postconditions at call sites
- conditional error analysis: bound the output difference when the ideal and the finite-precision execution take different branches, without assuming continuity
Last edited: