Double Handling

[jkwoods]

Doubles/floating points generally not supported.

Example c tests:

int bar() {
  double foo = 4.0;
  if (1 == 1){
    foo = 1.0;
  }
}

int bar() {
  double foo = 5.0;
  if (1.0 < foo){
    return 1;
  }
}

int bar() {
  double foo = 1.0;
  double goo = 2.0;
  return foo + goo
}

[mlfbrown]

We're very close to SMT and SMT model support for FP. I'm happy to handle that side of the pipeline.

[alex-ozdemir]

Interesting. Yeah, as @mlfbrown suggests we should support most of this. Likely this is a bug and not a feature.

[sga001]

Any luck with this issue? Are there particular things that we should be doing on our end? This is the one missing feature that we can't figure out a way to sidestep at the moment.

[alex-ozdemir]

Whoops! I apologize. I was incorrect in my last comment.

While we do map C floating point arithmetic down to the SMT layer (and to the best of my knowledge, this is working), we do not have an implementation of embedding floating point arithmetic in R1CS (and thus we cannot write proofs).

I'm not presently working on this, and I'm not sure what prior work exists related to it. One approach would be to use/follow symfpu, but there may be more proof-system-specific work.

[sga001]

Should we look into this and tackle this issue ourselves and submit a PR once we have addressed it?

[sga001]

@kwantam: do you know what the state of the art is here? Should we just go with the representation used in Ginger at least to get things working for now? AFAIK, we (Andrew et al.) were not able to come up with a better approach.
The downside is that Ginger's approach only works for rational numbers I think.

I'm referring to Appendix B in: https://eprint.iacr.org/2012/598.pdf

[kwantam]

once we have addressed it?

This isn't a coding issue, it's an open research question. I do not think Ginger's approach is even worth implementing, to be frank.

The last time I thought about this, I concluded that it is probably best to first tackle fixed-point arithmetic before trying to handle floats (since fixed-point is effectively a subroutine in "real" floating point). And that, in turn, should wait for optimized bit splitting based on the Bootle et al technique (Ariel Gabizon has a derived work that he calls plookup). This is on our agenda post-PLDI.

[sga001]

Yes, we are aware of plookup. We'll start thinking about fixed point then, since this is a blocking issue for all of our optimization apps/gadgets.

[kwantam]

I really hope it's not actually the case that all of your optimization apps and gadgets rely on efficient floating point!

[sga001]

@alex-ozdemir: @kwantam mentioned that you have a proposal in mind for implementing fixed point arithmetic. Is that related to symfpu? or is that totally different?

[alex-ozdemir]

Yeah, my recommendation here would be to try to map fixed-point arithmetic into bit-vectors whenever possible (thus taking advantage of bit-vector->R1CS lowering) rather than trying to lower fixed-point arithmetic directly.

This is more or less what symfpu does, but symfpu is for floating-point.