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

Division does not divide #69

Open jsalzbergedu opened 2 years ago

jsalzbergedu commented 2 years ago

Hello Pequin Project Maintainers,

In trying to make an example with data-dependent access to memory, I'm having some trouble with division in pequin. Here's my example. I replace the code of mergesort_merkle with the following:

#include <stdint.h>
#include <db.h>

#include "mergesort_merkle.h"

void compute(struct In *input, struct Out *output) {
  uint32_t i;
  uint32_t loop_max;
  int character;
  character = 64;
  loop_max = 0;
  ramput(0, &loop_max);
  printf("Input 0 is: %u", loop_max);
  loop_max = loop_max / 10000000;
  printf("Will iterate: %u times", loop_max);
  for (i = 0; i < loop_max; i++) {
    printf("Reached the loop (?)\n");
    character += 1;
    ramput(i + 1, &character);
  }

  for (i = 0; i < loop_max; i++) {
    ramget(&(output->output[i]), i + 1);
  }
}

Then I run the commands 

./pepper_compile_and_setup_V.sh mergesort_merkle mergesort_merkle.vkey mergesort_merkle.pkey
./pepper_compile_and_setup_P.sh mergesort_merkle
bin/pepper_verifier_mergesort_merkle gen_input mergesort_merkle.inputs
bin/pepper_prover_mergesort_merkle prove mergesort_merkle.pkey mergesort_merkle.inputs mergesort_merkle.outputs mergesort_merkle.proof

Which results in the following output from the prover:

PRINTF in computation_p 1:
"Input 0 is: 3179900336"
PRINTF in computation_p 1:
"Will iterate: 3179900336 times"
reading proving key from file...
Reset time counters for profiling
(enter) Call to r1cs_gg_ppzksnark_prover    [             ] (0.0000s x0.00 from start)
  (enter) Compute the polynomial H              [             ] (0.0000s x0.00 from start)
    (enter) Call to r1cs_to_qap_witness_map     [             ] (0.0000s x0.00 from start)
      (enter) Compute evaluation of polynomials A, B on set S   [             ] (0.4120s x1.00 from start)
      (leave) Compute evaluation of polynomials A, B on set S   [0.0568s x0.99] (0.4688s x1.00 from start)
      (enter) Compute coefficients of polynomial A  [             ] (0.4688s x1.00 from start)
      (leave) Compute coefficients of polynomial A  [0.1602s x1.00] (0.6291s x1.00 from start)
      (enter) Compute coefficients of polynomial B  [             ] (0.6291s x1.00 from start)
      (leave) Compute coefficients of polynomial B  [0.1560s x1.00] (0.7851s x1.00 from start)
      (enter) Compute ZK-patch                      [             ] (0.7851s x1.00 from start)
      (leave) Compute ZK-patch                      [0.0182s x1.10] (0.8033s x1.00 from start)
      (enter) Compute evaluation of polynomial A on set T   [             ] (0.8033s x1.00 from start)
      (leave) Compute evaluation of polynomial A on set T   [0.1575s x0.99] (0.9608s x1.00 from start)
      (enter) Compute evaluation of polynomial B on set T   [             ] (0.9608s x1.00 from start)
      (leave) Compute evaluation of polynomial B on set T   [0.1532s x1.02] (1.1140s x1.00 from start)
      (enter) Compute evaluation of polynomial H on set T   [             ] (1.1140s x1.00 from start)
        (enter) Compute evaluation of polynomial C on set S [             ] (1.1228s x1.00 from start)
        (leave) Compute evaluation of polynomial C on set S [0.3540s x0.99] (1.4768s x1.00 from start)
        (enter) Compute coefficients of polynomial C    [             ] (1.4768s x1.00 from start)
        (leave) Compute coefficients of polynomial C    [0.1588s x1.01] (1.6356s x1.00 from start)
        (enter) Compute evaluation of polynomial C on set T [             ] (1.6357s x1.00 from start)
        (leave) Compute evaluation of polynomial C on set T [0.1530s x0.99] (1.7887s x1.00 from start)
        (enter) Divide by Z on set T                [             ] (1.7954s x1.00 from start)
        (leave) Divide by Z on set T                [0.0666s x1.02] (1.8621s x1.00 from start)
      (leave) Compute evaluation of polynomial H on set T   [0.7481s x1.00] (1.8621s x1.00 from start)
      (enter) Compute coefficients of polynomial H  [             ] (1.8621s x1.00 from start)
      (leave) Compute coefficients of polynomial H  [0.1703s x0.99] (2.0324s x1.00 from start)
      (enter) Compute sum of H and ZK-patch         [             ] (2.0325s x1.00 from start)
      (leave) Compute sum of H and ZK-patch         [0.0046s x0.87] (2.0370s x1.00 from start)
    (leave) Call to r1cs_to_qap_witness_map     [2.0370s x1.00] (2.0370s x1.00 from start)
  (leave) Compute the polynomial H              [2.0446s x1.00] (2.0446s x1.00 from start)
  (enter) Compute the proof                     [             ] (2.0447s x1.00 from start)
    (enter) Compute evaluation to A-query       [             ] (2.0447s x1.00 from start)
    (enter) Process scalar vector               [             ] (2.0526s x1.00 from start)
      * Elements of w skipped: 52549 (49.64%)
      * Elements of w processed with special addition: 51824 (48.96%)
      * Elements of w remaining: 1486 (1.40%)
    (leave) Process scalar vector               [0.0199s x1.01] (2.0724s x1.00 from start)
    (leave) Compute evaluation to A-query       [0.0330s x1.09] (2.0777s x1.00 from start)
    (enter) Compute evaluation to B-query       [             ] (2.0777s x1.00 from start)
    (enter) Process scalar vector               [             ] (2.0777s x1.00 from start)
      * Elements of w skipped: 22009 (50.56%)
      * Elements of w processed with special addition: 21522 (49.44%)
      * Elements of w remaining: 0 (0.00%)
    (leave) Process scalar vector               [0.0353s x0.91] (2.1129s x1.00 from start)
    (leave) Compute evaluation to B-query       [0.0353s x0.91] (2.1129s x1.00 from start)
    (enter) Compute evaluation to H-query       [             ] (2.1129s x1.00 from start)
    (leave) Compute evaluation to H-query       [1.4565s x1.00] (3.5695s x1.00 from start)
    (enter) Compute evaluation to L-query       [             ] (3.5695s x1.00 from start)
    (enter) Process scalar vector               [             ] (3.5695s x1.00 from start)
      * Elements of w skipped: 52546 (49.65%)
      * Elements of w processed with special addition: 51823 (48.97%)
      * Elements of w remaining: 1465 (1.38%)
    (leave) Process scalar vector               [0.0285s x0.98] (3.5980s x1.00 from start)
    (leave) Compute evaluation to L-query       [0.0356s x0.90] (3.6051s x1.00 from start)
  (leave) Compute the proof                     [1.5611s x1.00] (3.6057s x1.00 from start)
(leave) Call to r1cs_gg_ppzksnark_prover    [3.6057s x1.00] (3.6058s x1.00 from start)
* G1 elements in proof: 2
* G2 elements in proof: 1
* Proof size in bits: 1019
Done proving

I don't think this issue is particularly important. Just a funny little problem :)

jsalzbergedu commented 2 years ago

Okay I understand now that this is a bit of a spurious example because I'm using data dependent loops and maybe somehow it is impossible to flatten them.