Are Dafny "reals" really "real"

Could you please help answering https://stackoverflow.com/questions/77761751/are-dafny-reals-really-real ... for documentation purposes? :sweat_smile:

@RustanLeino

I'd like to ask for clarification regarding your stackoverflow comment, which unfortunately I didn't notice until today. However I expect that this would be considered "debating a controversial point", which shouldn't be done in comments according to https://stackoverflow.com/help/privileges/comment. Also I think that in this case a related github issue may be a better place to discuss this than the stackoverflow chat. I can link from stackoverflow to this issue later, if it proves interesting.

There are no compiled operations that produce irrational reals.

What about ghost operations? I can understand that irrational reals would not be very useful in compiled programs, but I don't see a reason why ghost operations should not be able to assert the existence of irrational reals without invoking unprovable(?) axioms.

Dafny's reals are indeed real numbers.

Wouldn't it be fair to say that this statement is undecidable? It seems to me that we can neither prove nor refute the statement without simply ~~relying on your word~~ accepting it axiomatically.

To make this more concrete: I could add either a completeness axiom or

lemma {:axiom} real_is_rational()
    ensures forall r: real :: exists p: nat, q: nat | q != 0 :: r == p as real / q as real

without being able to derive contradictions, right?

I added my own attempt at a partial answer to my question: https://stackoverflow.com/a/77811642/8857097 Any feedback would be appreciated.

I can say a bit about this. Dafny's real type is indeed mapped to the SMT-Lib Real theory. And, therefore, if Dafny is able to prove anything that would be inconsistent with that theory, it is a bug in either Dafny or the SMT solver. However, Dafny adds a wrinkle that often makes things harder to prove. To support quantifiers in user programs, and axiomatic definitions of some of the other data types (collection types, not real), Dafny includes quite a few quantifiers in the SMT queries it generates. In general, Z3 is less powerful in reasoning about its built-in theories when there are quantifiers around. Although Z3 is able to prove the little SMT-Lib snippet posted on StackOverflow, the equivalent generated by Dafny would be more complex, and would include more quantifiers. As a result, Z3 (which, like any SMT solver, will always be incomplete) may not be able to solve it, even if it could with a similar quantifier-free formula.

https://github.com/dafny-lang/Dafny-VMC/blob/f715055e052846157d0794c6b1a0e73484102b75/src/Math/Analysis/Reals.dfy#L6-L8:

// Fundamental properties of the real numbers.
// * States the completeness of the reals in terms of a variation of Dedekind cuts.
//     Dafny should include such an axiom, but doesn't.

Why doesn't Dafny include such an axiom? :slightly_smiling_face:

Is there hope that the issue can be solved without providing such an axiom? Hypothetically, should Dafny's designers ever see the need for completeness of the reals to be (easily, obviously, in a documented way) usable without providing a user-defined axiom, would they rather provide the Axiom (in Boogie as far as I understand) or would they try to adapt the Boogie/z3 code generation in a way that the z3 Real theory can be used more completely?

Is it maybe that the part of Dafny's design that deals with real numbers has not matured enough to provide an answer to how Dafny can avoid irrational numbers in compiled contexts while allowing them in ghost contexts? Would adding a completeness axiom just lead to more questions / problems at the moment?

Or is the common understand among Dafny's designers and expert users simply that requiring users to provide such a user-defined axiom is always going to be good enough? In that case, shouldn't this be documented? Given @RustanLeino's statement

There are no compiled operations that produce irrational reals.

Shouldn't the following part of the documentation be clarified?

Dafny supports numeric types of two kinds, integer-based, which includes the basic type int of all integers, and real-based, which includes the basic type real of all real numbers

P.S.: Maybe the axiom(s) could be provided in the new Dafny standard library?

I'd like to mention why I'm so fixated on the topic.

I'd love to use Dafny more for specifying my production code. One of the few parts where I'm not yet sure how I can best use it is in floating point computations. I want to specify that an implementation with rounding / approximation errors and other potential floating point issues satisfies some accuracy requirements. I could try to come up with my own theories that don't require completeness of the reals, but I'd rather stick to the literature. And the literature is making heavy use of analysis, which requires derivatives, limits and therefore completeness.

I'm a layman and not too comfortable with providing my own axioms about things that I don't perfectly understand. I like to get confirmation from the verifier that my lemmas are correct - without relying on my own assumptions.

Other math-focused proof assistant like Lean may be more suited for the math-heavy part of this work, but I'd love to use Dafny for it because I consider it to be better suited for the software-heavy part and I would like to stay within a single language / system / environment because things can get lost in translation. Also I think that, given time and preparation of a proof of concept from me, I could convince my colleagues (and our safety and dependability department) to use Dafny as well. But the less I can tell them that Dafny "just works", the less likely they are to take my arguments into consideration.

I have answers for only a subset of your questions, but I'll answer the ones I can here.

Is there hope that the issue can be solved without providing such an axiom? Hypothetically, should Dafny's designers ever see the need for completeness of the reals to be (easily, obviously, in a documented way) usable without providing a user-defined axiom, would they rather provide the Axiom (in Boogie as far as I understand) or would they try to adapt the Boogie/z3 code generation in a way that the z3 Real theory can be used more completely?

Adapting the Boogie/z3 code generation so that the Z3 query you mentioned would be successfully solved is a goal of mine, and one I think we're coming relatively close to achieving. So, although the encoding we currently do inhibits Z3's ability here, that may not always be true.

Is it maybe that the part of Dafny's design that deals with real numbers has not matured enough to provide an answer to how Dafny can avoid irrational numbers in compiled contexts while allowing them in ghost contexts? Would adding a completeness axiom just lead to more questions / problems at the moment?

I think the reason irrational numbers don't show up in a compiled context is that the Dafny compilers will not compile any operations that could lead to irrational numbers. As a result, the choice of using pairs of unbounded integers to represent reals is a sound choice.

There are no compiled operations that produce irrational reals.

Shouldn't the following part of the documentation be clarified?

Dafny supports numeric types of two kinds, integer-based, which includes the basic type int of all integers, and real-based, which includes the basic type real of all real numbers

In Dafny as a logic, the real type does indeed represent the mathematical reals. It's just that it's impossible to represent all real numbers in an executable program, so Dafny does the best it can and produces compiled programs that work on rationals.

I'd love to use Dafny more for specifying my production code. One of the few parts where I'm not yet sure how I can best use it is in floating point computations. I want to specify that an implementation with rounding / approximation errors and other potential floating point issues satisfies some accuracy requirements. I could try to come up with my own theories that don't require completeness of the reals, but I'd rather stick to the literature. And the literature is making heavy use of analysis, which requires derivatives, limits and therefore completeness.

This is a use case that very much interests me, as well (out of personal interest more than production need at the moment). One of the tricky things that comes up here is that you ultimately then need a way to relate real and float types, to reason about how far off the float calculations might be. Z3 does have support for both types, and so does Boogie, so it would in principle be possible to add float types to Dafny and therefore state the property that a given set of floating-point operations always yields a result within a particular delta of the associated real calculation. However, I don't know that Z3 would do very well at proving such a statement. Most of the promising work I know of for reasoning about that relationship is in the context of interactive provers (mostly Coq), though it's been a few years since I've looked at it closely.

Other math-focused proof assistant like Lean may be more suited for the math-heavy part of this work, but I'd love to use Dafny for it because I consider it to be better suited for the software-heavy part and I would like to stay within a single language / system / environment because things can get lost in translation. Also I think that, given time and preparation of a proof of concept from me, I could convince my colleagues (and our safety and dependability department) to use Dafny as well. But the less I can tell them that Dafny "just works", the less likely they are to take my arguments into consideration.

I'm hoping we can bridge the gap to get the best of both worlds before long. How exactly to do it is still an open question, but one I've been thinking about.

Okay, I take from this that neither a completeness axiom nor a documentation update are appropriate because the goal - or at least your goal - is that Dafny will be able to prove statements that require completeness of the reals (without user-defined axioms) while still prohibiting irrational numbers in compiled contexts. Maybe a note about this could be added to the "Dafny is incomplete for (at least) the following reasons" list or some other list of "errata" that is kept up-to-date, if there is one. One where it is clear that this is only a temporary issue that should be resolved in the (possible far :yum:) future.

This is a use case that very much interests me, as well (out of personal interest more than production need at the moment). One of the tricky things that comes up here is that you ultimately then need a way to relate real and float types, to reason about how far off the float calculations might be. Z3 does have support for both types, and so does Boogie, so it would in principle be possible to add float types to Dafny and therefore state the property that a given set of floating-point operations always yields a result within a particular delta of the associated real calculation. However, I don't know that Z3 would do very well at proving such a statement. Most of the promising work I know of for reasoning about that relationship is in the context of interactive provers (mostly Coq), though it's been a few years since I've looked at it closely.

Interesting. I didn't even know about the z3 FloatingPoint theory (I have only looked at z3 in the context of this issue, so this is not surprising.) and that Dafny could theoretically offer it in the future. However, I intend not to start with IEEE 754 floats but more abstractly with reals with an absolute or relative error (my choice of words may not be the best ...), as described here and here. Then I would only be dealing the reals and could avoid the IEEE 754 complication. Later I could show that IEEE 754 floats are a refinement of this abstract model. Of course non-finite IEEE 754 float values would complicate this ...

With this, I will close this issue now. Thank you for your patience :slightly_smiling_face:

dafny-lang / dafny

Are Dafny "reals" really "real" #4947