Realizing IEEE 754-compliant floating point numbers in CirC

[lorenzorota]

Hi @alex-ozdemir,

In the CirC paper you stated that the R1CS backend does not support IEEE 754 floats. I came across https://eprint.iacr.org/2024/1842 (published in IEEE S&P 2025), which claims to have constructed fully IEEE 754-compliant arithmetization-agnostic circuits for floating point arithmetic. I have a feeling that this could fill the gap for floats in CirC. From what I read, they provide the following constructions:

• Unary ops: initializing, rounding, sqrt
• Binary ops: addition, multiplication, division, comparison, min, max

Do you think these constructions are applicable in the R1CS lowering pass?

[alex-ozdemir]

Yes, it would make sense to add the construction around there. The construction uses lookups, so you might want to add the construction just before the R1CS lowering pass and build on our RAM/lookup machinery here. You would implement the paper's constructions in a compiler pass that add RAM accesses or lookups, then run the existing pass that translate those operations into interactive proofs, and then run the R1CS lowering pass to flatten everything down into (Interactive) R1CS that you can feed into some ZKP.

[lorenzorota]

Sounds good. I worked on the IR to make sure floats are fully represented, could you see in the PR draft if there's anything missing or that should be modified/removed?

I also had a couple of questions:

• Since these constructions are handled at compile-time, do the lookups pertain to volatile RAM?
• In the Z# RAM tests I noticed that the volatile RAM programs using groth16 require additional options to be passed (waksman permutation, etc.). Do you think additional steps are needed for constructing floats based on the proof system or is there a standard way to handle lookups?

[alex-ozdemir]

Hi Lorenzo,

Mostly so far, so good. I had just one comment.

Re: lookups: yes, they are similar to volatile RAM. A bit easier though. Happy to discuss synchronously, somtime.

Re: waksman/.... If you want to resolve the lookups with a deterministic circuit that is fed into Groth16, then yes, you need a permutation network like Waksman. If you're OK with a randomized circuit that is fed into Mirage (a slight generalization of Groth16 that we support), then you don't need Waksman.