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.

[jkwoods]

@alex-ozdemir I see there's a point in Codegen.C.Term where it's possible to serialize doubles/floats as bit vectors. Would this be an alright place to unhook the existing conversion to TySMT floating point and convert to TySMT bit vectors? - basically handling CDoubles and CFloats kind of like the CInts are handled - with a bit vector and width?

[kwantam]

Are we sure that we want to treat C float types as fixed-point numbers? It seems like a very reasonable alternative would be to introduce an explicit fixed-point type, no?

[jkwoods]

I think that makes sense. Pros: we leave the C --> SMT floating point intact, in case we ever want to extend that directly to R1CS; and we keep the semantic difference. But, cons: a new type that we define would not have a premade structure in the C Language AST package. It would be easy to add in on the Term level, but I'm not sure what we would have to do to allow for correct parsing (from C code)/how much manipulation that would require?

[alex-ozdemir]

But, cons: a new type that we define would not have a premade structure in the C Language AST package. It would be easy to add in on the Term level, but I'm not sure what we would have to do to allow for correct parsing (from C code)/how much manipulation that would require?

I don't think this would be too hard to hack in, since C supports typdefs. Let's say you use type names like "fixpointWIDTH_PRECISION_t". The C parser will assume that they're user-defined typedefs, and you just add some machinery to handle them differently, perhaps here.

[pcousot]

Libfixmath implements math.h for fixpoint arithmetics. Don’t know if this can help.

Patrick Cousot (from my iPhone)

On Nov 11, 2020, at 16:49, Riad S. Wahby notifications@github.com wrote:

 Are we sure that we want to treat C float types as fixed-point numbers? It seems like a very reasonable alternative would be to introduce an explicit fixed-point type, no?

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub, or unsubscribe.

[jkwoods]

Great, thanks, we'll do that then. And I think that ref will be helpful!

[jkwoods]

This is done, on the other fork.