[WIP] crypto examples

[veorq]

No description provided.

[porcuquine]

Neat. Note that GCD only makes sense if you view a and b as natural numbers. (As field elements, you could kind of argue that every value is divided by <whichever value you consider 'greatest'>). If that's how you mean it, then it's important to specify (or check) that a and b are in range. I think if either one is negative, then your > check won't give the right results. We spent some time thinking about this example (GCD — not your code) recently, but I still might have gotten a detail wrong in my quick summary. cc: @emmorais @differentialderek @weissjeffm

[porcuquine]

Consider adding a comment to clarify, so people studying this code don't get confused or misled.

[dhsorens]

This is sleek—the nice thing about it is that it doesn't require values greater than a and b so from the "field-elements-as-integers" perspective this is simulates normal gcd for positives (as long as you start with positives, you don't run the risk of getting so positive that you go negative).

I have a much more clunky version here: #32 lol, probably should throw that one away now

[dhsorens]

Note that this recurses infinitely if a or b is negative, which can be solved by adding something like

(if (< a 0) 
    (gcd -a b) 
    (if (< b 0)
        (gcd a -b)
        (...)))

or failing if (< a 0) or (< b 0)

[dhsorens]

Because of the field arithmetic there is some ambiguity on what < means too -- not sure if that's a problem here @emmorais? I think if you start from the position of (< 0 a) and (< 0 b), this simulates gcd on natural numbers

[porcuquine]

Cool. Obviously in this case, it would be cheaper just to expand by hand. I like the explanatory library function, just thought I would mention it as an aside.

[porcuquine]

I like this a lot as an example. One nice thing about Lurk is that if you replace hash2 with cons, you'll get real Poseidon hashing much more efficiently. But your proof will still make sense. In that case, you will be able to avoid hashing all the leaves because the destructuring/opening operators (car and cdr) have access to the non-deterministic information in the store — so they wouldn't have to be supplied. In that way, the prover's knowledge is encapsulated in the store.

Put differently, Lurk makes obvious that merkle proofs are exactly membership tests. In this case, the 'container' is an 8-leaf binary tree. So if we were to hard-code the leaf in question like your example, we could just write:

(lambda (root x)
  (eq x (cdr (cdr (cdr root)))))

Of course that requires that root be a cons. However, you can still use a cons (an opaque one) as a structured commitment. Just discard the type tag and use the value.

Since we have primitives for commitments and get some useful properties from them, you could also use commit/hide (at the cost of one extra hash).

Then you would have

> (let ((tree8 (lambda (a b c d e f g h)
                 (hide 12345 (cons (cons (cons a b)
                                         (cons c d))
                                   (cons (cons e f)
                                         (cons g h))))))) 
  (tree8 1 2 3 4 5 6 7 8))
[100 iterations] => (comm 0x14e93dde5d0dbbdcccbebda5e91708f13d3e1fd846dc7b3a4ddf14d0ae1e012d)
> (let ((treeproof8 (lambda (root x)
                      (eq x (cdr (cdr (cdr (open root))))))))
    (treeproof8 0x14e93dde5d0dbbdcccbebda5e91708f13d3e1fd846dc7b3a4ddf14d0ae1e012d 8))
[24 iterations] => T

open in treeproof8 works for the same reason car and cdr does; the prover must know the opening and also the secret (in this case 12345). In the case of an explicit commitment however, the apparent value returned to the user is evidently opaque, without extra error-prone manipulation of the cons.

---

I know these examples don't replace what you were trying to do here. I just wrote them out in case they help you get a better picture of why some Lurk features are as they are, and what they enable.