search

pepper-project / pequin

A system for verifying outsourced computations, and applying SNARKs. Simplified release of the main Pepper codebase.
Other
122 stars 46 forks source link

Introducing type int128 #19

Closed fleupold closed 5 years ago

fleupold commented 5 years ago

As discussed in #18 it would be great to have support for types larger than 64 bit. This PR introduces a new type that is 128 bits wide.

I tested the change by compiling this program

struct In {unsigned int128 lhs; unsigned int128 rhs; };
struct Out { unsigned int128 result; };

void compute(struct In *input, struct Out *output) {
  output->result = input->lhs + input->rhs;
}

and making sure that I can prove and verify it with integers > 64 bit.

The generated spec_tmp file looks like this:

START_INPUT
I0 //__malloc0.lhs uint bits 128
I1 //__malloc0.rhs uint bits 128
END_INPUT

START_OUTPUT
O6 //#compute$__compute__ uint bits 1
O7 //__malloc1.result uint bits 129
END_OUTPUT

START_VARIABLES
END_VARIABLES

START_CONSTRAINTS
(  ) * (  ) + (  - O6 )
(  ) * (  ) + ( I0 + I1 - O7 )
END_CONSTRAINTS

I also ran the original example from #18 and made sure it works

maxhowald commented 5 years ago

Looks good, merged!