gstew5 / snarkl Goto Github PK

View Code? Open in Web Editor NEW

59.0 59.0 9.0 936 KB

License: BSD 3-Clause "New" or "Revised" License

Haskell 89.02% Makefile 1.47% C++ 5.14% Shell 3.06% Python 0.15% Gnuplot 1.16%

snarkl's People

Contributors

Stargazers

Watchers

Forkers

dantengsky christomoore rahulmutt 3for blockchainchaos sellout ksuenaga

snarkl's Issues

Optimize vars.

The simplifier removes redundant clauses but doesn't yet remove the redundant variables. Not difficult except that: must be careful to communicate to the rest of the compiler the renaming table for pinned vars (inputs/outputs).

R1CS generator is not field-agnostic

The encoding of x*x=z relies on a field element one+one != zero, with the appropriate semantics (e.g., as in ZmodP for large P). File: https://github.com/gstew5/snarkl/blob/master/src/constraints.hs.

Is this library expected to work against libsnark master?

I've been packaging snarkl for nixpkgs and am running it against libsnark master, and a lot of the tests (but not all) seem to fail for reasons I don't understand.

For example, in the first test (if-then-else):

Generating Keys
(enter) Call to r1cs_ppzksnark_generator   	[             ]	(1133431.1352s x1339.09 from start)
  (enter) Call to r1cs_constraint_system::swap_AB_if_beneficial	[             ]	(1133431.1359s x1339.09 from start)
    (enter) Estimate densities                 	[             ]	(1133431.1360s x1339.09 from start)
      * Non-zero A-count (estimate): 7
      * Non-zero B-count (estimate): 9
    (leave) Estimate densities                 	[0.0000s x1.25]	(1133431.1360s x1339.09 from start)
    (enter) Perform the swap                   	[             ]	(1133431.1360s x1339.09 from start)
    (leave) Perform the swap                   	[0.0000s x1.02]	(1133431.1360s x1339.09 from start)
  (leave) Call to r1cs_constraint_system::swap_AB_if_beneficial	[0.0001s x0.93]	(1133431.1360s x1339.09 from start)
  (enter) Call to r1cs_to_qap_instance_map_with_evaluation	[             ]	(1133431.1361s x1339.09 from start)
Key-generation Failed!

I can't tell what actually went wrong with that invocation, but all the failures look like that. They enter r1cs_to_qap_instance_map_with_evaluation but never leave it. Given that there are other blocks entered fairly early in that function, it seems like there's a small number of places that could be failing, but I haven't looked more carefully.

Here's the full list of passes and fails:

Field Tests
  if-then-else
    1-1 FAILED [1]
  bigsum
    2-1 FAILED [2]
    2-2 FAILED [3]
    2-3 FAILED [4]
    2-4 FAILED [5]
  arrays
    3-1
    3-2
    3-3
    3-4
    4-1
    4-2
    4-3
    4-4
    5-1 FAILED [6]
    5-2 FAILED [7]
    5-3 FAILED [8]
    5-4 FAILED [9]
  times
    6-1 FAILED [10]
  forall
    7-1
  forall2
    8-1
  unused inputs
    11-1
  multiplicative identity
    13-1 FAILED [11]
  opt: 0x * 3y = out ~~> out=0
    14-1
  exp_binop smart constructor: 3 - (2 - 1) = 2
    15-1
  lists
    26-1
    27-1
    28-1
    29-1 FAILED [12]
    30-1
    37-1 FAILED [13]
  div
    31-1
    31-1
    31-1
    31-1
  beta
    34-1 FAILED [14]
  trees
    35-1
Boolean Tests
  and
    9-1 FAILED [15]
    9-2 FAILED [16]
    9-3 FAILED [17]
    9-4 FAILED [18]
  xor
    10-1 FAILED [19]
    10-2 FAILED [20]
    10-3 FAILED [21]
    10-4 FAILED [22]
  boolean eq
    12-1 FAILED [23]
    12-2 FAILED [24]
    12-3 FAILED [25]
    12-4 FAILED [26]
  bool inputs
    16-1 FAILED [27]
  array
    17-1
  input array
    18-1 FAILED [28]
  products
    19-1 FAILED [29]
    20-1 FAILED [30]
    21-1 FAILED [31]
  products
    22-1 FAILED [32]
    23-1 FAILED [33]
  peano
    24-1
  lam
    25-1
  zeq
    32-1 FAILED [34]
    32-2 FAILED [35]
    32-3 FAILED [36]
  eq
    33-1
    33-2
    33-3
    33-3
    33-3
    33-3
  sum
    36-1 FAILED [37]
    36-2 FAILED [38]
Keccak Tests
  keccak
    keccak-2 FAILED [39]
    keccak-2 FAILED [40]

It's unclear to me whether it's an issue with my packaging or whether stuff has just changed in libsnark in the couple of years since the @jkroll fork snarkl is using.

cc @gstew5

'case_sum' breaks compile-time invariants

Case analysis returns a variable x bound to a conditional expression:

case_sum :: ...
         => (TExp ty1 Rational -> Comp ty)
         -> (TExp ty2 Rational -> Comp ty)
         -> TExp (TSum ty1 ty2) Rational
         -> Comp ty
case_sum f1 f2 e
  = do { p <- get_addr (var_of_texp e,0)
       ; ...
       ; x <- var
       ; ret $ te_seq (TEUpdate x (if b then re else le)) x
       }

When the return type ty is nonscalar, e.g., TProd ty1 ty2, other shallowly-embedded operations such as fst_pair will fail when run on x. The problem: while both re and le are registered in the compile-time env as values of type ty, x is totally unknown to the compiler. It's only resolved at "runtime" (i.e., in the generated constraint system).

One possible solution: Since re and le have the same type, and we expand values of recursive type to a fixed depth, we should be able to fold the conditional if ... then ... else to the "leaves" of the two expressions, giving a single expression e of type ty. This folding might be a useful optimization wrt. encoding size as well.

Wasteful encodings

Expressions such as x \/ y = z ~~> x+y - z = x*y, with x and y boolean encode to more variables/R1Cs than strictly necessary. The simplifier helps a bit, but usually by no more than a factor of 50% in the current small experiments.

One fix: in the intermediate constraint language, support arbitrary linear combinations of terms, as in

data Constraint a =
  CBinop COp ([Term a],Term a) -- fold op xs unit = z
  deriving (Eq,Ord)

instead of the current

...
  CBinop COp (Term a,Term a,Term a) -- x `op` y = z
...

The change will primarily affect:

the simplifier
translation phase: intermediate constraint sets -> R1CS

Update to work with libsnark:master

Snarkl was developed against a fork of libsnark at https://github.com/jkroll/libsnark (it's this libsnark that's built by ./prepare-depends.sh). It should be ported to work with the master branch of https://github.com/scipr-lab/libsnark. Cf. #11 for a description of issues that may arise during this port.

`Op` datatype in `src/common.hs` should not be shared

The expression language supports more binary operations than the intermediate constraint language. We should make this fact explicit in the types.

Missing run-proofgen.sh?

From https://github.com/gstew5/snarkl/blob/master/src/Toplevel.hs#L266-L271 it sounds like there's supposed to be another shell script called run-proofgen.sh, but I don't see it in the repo. Is it dead code?

Pinned Variables

In order to optimize the IL constraint systems generated for nontrivial programs (even at b=25, the Keccak round function encodes to vars = 1405, constraints = 1426), we need to distinguish "pinned" variables (those that cannot be optimized away, e.g., inputs and outputs) from variables that were introduced as temporaries.

Temporaries should be optimized as aggressively as possible, as long as the optimized constraint set remains equisatisfiable with the initial one.

Witness-generation failure

The program

p3 :: Comp 'TField
p3 = do
  b1 <- fresh_input
  r1 <- inl 1.0
  r2 <- inr 2.0
  x <- if b1 then r1 else r2
  case_sum (\n -> return $ n + 1.0) (\m -> return $ m + 2.0) x

fails at witness generation

λ> snarkify_comp "test" p3 [1]

with error:

*** Exception: unassigned variables,                                                                                                                                         
  [1,2,4,9,14,23],                                                                                                                                                           
in assignment context                                                                                                                                                        
  fromList [(0,1 % 1),(3,1 % 1),(5,0 % 1),(6,2 % 1),(7,0 % 1),(8,0 % 1),(10,0 % 1),(11,0 % 1),(12,0 % 1),(13,0 % 1),(15,0 % 1),(16,0 % 1),(17,2 % 1),(18,1 % 1),(19,2 % 1),(\
20,0 % 1),(21,0 % 1),(22,1 % 1)],                                                                                                                                            
in pinned-variable context                                                                                                                                                   
  [0,6],                                                                                                                                                                     
in optimized-constraint context                                                                                                                                              
  ConstraintSystem {cs_constraints = fromList [(-2) % 1 + 1 % 1x6 == 0,(-1) % 1 + 1 % 1x0 == 0,2 % 1 + (-1) % 1x23 + 1 % 1x1 == 0], cs_num_vars = 24, cs_in_vars = [0], cs_o\
ut_vars = [6]},                                                                                                                                                              
in constraint context                                                                                                                                                        
  ConstraintSystem {cs_constraints = fromList [0 % 1 + (-1) % 1x3 + 1 % 1x0 + 1 % 1x7 == 0,0 % 1 + (-1) % 1x3 + 1 % 1x0 + 1 % 1x12 == 0,0 % 1 + (-1) % 1x4 + 1 % 1x9 + 1 % 1\
x10 == 0,0 % 1 + (-1) % 1x4 + 1 % 1x14 + 1 % 1x15 == 0,0 % 1 + (-1) % 1x6 + 1 % 1x17 + 1 % 1x20 == 0,0 % 1 + (-1) % 1x10 + 2 % 1x11 == 0,0 % 1 + (-1) % 1x15 + 2 % 1x16 == 0\
,1 % 1 + (-1) % 1x0 + (-1) % 1x5 == 0,1 % 1 + (-1) % 1x0 + (-1) % 1x8 == 0,1 % 1 + (-1) % 1x0 + (-1) % 1x11 == 0,1 % 1 + (-1) % 1x0 + (-1) % 1x13 == 0,1 % 1 + (-1) % 1x0 + \
(-1) % 1x16 == 0,1 % 1 + (-1) % 1x5 + (-1) % 1x18 == 0,1 % 1 + (-1) % 1x5 + (-1) % 1x22 == 0,1 % 1 + (-1) % 1x19 + 1 % 1x3 == 0,1 % 1 + (-1) % 1x22 + (-1) % 1x21 == 0,2 % 1\
 + (-1) % 1x23 + 1 % 1x4 == 0,1 % 1x0 * 1 % 1x0 == 1 % 1x0,1 % 1x0 * 1 % 1x1 == 1 % 1x9,1 % 1x0 * 1 % 1x1 == 1 % 1x14,1 % 1x8 * 1 % 1x2 == 1 % 1x7,1 % 1x13 * 1 % 1x2 == 1 %\
 1x12,1 % 1x18 * 1 % 1x19 == 1 % 1x17,1 % 1x21 * 1 % 1x23 == 1 % 1x20], cs_num_vars = 24, cs_in_vars = [0], cs_out_vars = [6]}

This is a note to myself so I don't forget to fix this.

starkl?

With the release of the new ZK-STARK paper, it might be interesting to see how snarkl needs to change to accommodate it: https://eprint.iacr.org/2018/046.pdf

Clarify support for zero-knowledge

I read the paper and it makes it clear that zero-knowledge is supported but not the primary driver. At the same time, a lot of the interest in this field is around the zero-knowledge aspect, since as the paper explains, it's not yet practical to just hand off full-knowledge computation to someone else and expect a proof back that it's correct (or at least, there's no computational benefit to doing so at this point). As such, it seems like one of the primary selling points is the ZKP community, which often wants something like snarkl, except with some sort of commitment/revealing aspect to operating it. So for example, in Bitcoin's zero-knowledge contingent payments, one might agree to pay money for a Sudoku solution (or more realistically, the preimage to some hash function, or a discrete logarithm, or something of the sort), as verified by a ZKP. Typically the proofs here involve not only convincing the counterparty that you have a valid solution to their problem, but also revealing something to them that (in the right conditions) gives away the actual solution, typically alongside a payment.

I'm wondering if you could write a bit about what that sort of use case would look like with this library. The circuit compilation stuff all looks great but I'm not super clear on how to plug it into an actual zero-knowledge use case.