Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[WIP] crypto examples #31

Open
wants to merge 9 commits into
base: master
Choose a base branch
from
Open

[WIP] crypto examples #31

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
b6a69ab
crypto
veorq Nov 18, 2022
091ef49
fastexp
veorq Nov 18, 2022
8e744dc
cryptotests
veorq Nov 18, 2022
fc1e10c
better hash
veorq Nov 18, 2022
c5d326e
fix tests
veorq Nov 23, 2022
c6512f9
draft
veorq Nov 24, 2022
5b1a240
testsfix
veorq Nov 25, 2022
4e5e3da
trees
veorq Nov 29, 2022
5b6856a
64
veorq Dec 12, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
34 changes: 34 additions & 0 deletions crypto/crypto-tests.lurk
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,34 @@
; crypto-tests.lurk
;
; tests for crypto.lurk
;
; run in repl as:
; > :run "crypto-tests.lurk"

!(:load "crypto.lurk")

!(:assert-eq (odd 0) NIL)
!(:assert-eq (odd 121) T)
!(:assert-eq (odd (/ 2 3)) T)

!(:assert-eq (even 0) T)
!(:assert-eq (even 121) NIL)
!(:assert-eq (even (/ 2 3)) NIL)

!(:assert-eq (fastexp 129 13) 2739468013418114691600975489)
!(:assert-eq (fastexp 129 921) 0x188bc6b313e74bcf3c8f8ddb1311c5e892b271c636866b64930d3357600c7f3f)

!(:assert-eq (gcd 11856 25883) 13)

!(:assert-eq (hash1 3) 0x12c26d76c2dff4b314388dc4ed60788206d921608575f77b1b9340e17a41b015)
!(:assert-eq (hashn '(1 2 3 4 5)) 0x0c46596ba7b418cdea2764e0c8f48d48c418ab1b7e141981aaddfb70d439666c)

!(:assert-eq (hashn '(1 2)) (hash2 1 2))

!(assert-eq (tree8 1 2 3 4 5 6 7 8)
0x02fdb269fa0d532c68afb6120682cb0453255d71cdb09ac6323ef13a4dcada0e)





104 changes: 104 additions & 0 deletions crypto/crypto.lurk
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,104 @@
; crypto.lurk
;
; simple crypto-related functions
;
; load in repl as:
; > :load "crypto.lurk"


(letrec (

; parity tests
(odd (lambda (a) (< (/ a 2) 0)))
(even (lambda (a) (eq NIL (odd a))))

; square & multiply exponentiation
(fastexp (lambda (b e)
(if (= e 0) 1
(if (even e) (fastexp (* b b) (/ e 2))
(* b (fastexp (* b b) (/ (- e 1) 2)))))))

(odd64 (lambda (a) (eq 1u64 (% (u64 a) 2u64))))
(even64 (lambda (a) (eq NIL (odd64 a))))

(fastexp64 (lambda (b e)
(if (= e 0) 1
(if (even e) (fastexp64 (* (u64 b) (u64 b)) (/ e 2))
(* (u64 b) (fastexp64 (* (u64 b) (u64 b)) (/ (- e 1) 2)))))))

; GCD
(gcd (lambda (a b)
(if (= a b) a
(if (> a b) (gcd (- a b) b)
(gcd (- b a) a)))))
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link

@dhsorens dhsorens Dec 2, 2022 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link

@dhsorens dhsorens Dec 2, 2022 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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)

Copy link

@dhsorens dhsorens Dec 2, 2022 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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


; hash function, poseidon-like
; 2-element permutation used by the hash
; NOT cryptographically safe
(permute (lambda (a b)
(letrec (
(rnd (lambda (i a b) (let (
(mat1 (lambda (a b) (+ (/ a 3) (* b 5))))
(mat2 (lambda (a b) (+ (/ a 7) (* b 9))))
(sbox (lambda (a) (fastexp a 5)))
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

(add1 (lambda (a) (+ a (/ 2 3))))
(add2 (lambda (a) (+ a (/ 3 2))))
)
(cons
(+ i (add1 (sbox (mat1 a b))))
(add2 (sbox (mat2 a b)))))))
(iter (lambda (i a b)
(if (= i 4) ; 4 rounds
(cons a b)
(let (
(res (rnd i a b))
(a (car res))
(b (cdr res))
)
(iter (+ i 1) a b))))))
(iter 0 a b))))

; initial state of the hash will be (0 iv)
(iv (/ 5 2))

; hash 1 element
(hash1 (lambda (a) (car (permute a iv))))

; hash 2 elements
(hash2 (lambda (a b)
(let (
(res1 (permute a iv))
(res2 (permute (+ b (car res1)) (cdr res1)))
)
(car res2))))

; hash a list of elements
; such that (hashn '(a b)) = (hash2 a b)
(hashn (lambda (alist)
(if (eq alist nil) nil
(let (
(res0 (permute (car alist) iv))
)
(letrec (
(iter (lambda (blist a b)
(if (eq blist nil) a
(let (
(res (permute (+ (car blist) a) b))
)
(iter (cdr blist) (car res) (cdr res))))))
)
(iter (cdr alist) (car res0) (cdr res0)))))))

; basic 8-leaf tree
(tree8 (lambda (a b c d e f g h)
(hash2
(hash2 (hash2 a b) (hash2 c d))
(hash2 (hash2 e f) (hash2 g h)))))

; proof of membership check
(treeproof8 (lambda (root x h1 h2 h3)
(eq root (hash2 h1 (hash2 h2 (hash2 h3 x))))))
Copy link
Contributor

@porcuquine porcuquine Dec 2, 2022 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.


)
(current-env))

0 example/test.lurk → example/lib-tests.lurk
View file
Open in desktop
File renamed without changes.