significant partial working progress towards creating a hiding protocol

Changes

8 changed files (+118/-0)

• factoring_test/factoring_proof.lurk (new)
  • @@ -0,0 +1,15 @@
    + ;; Ask ryli13 if confused about this file. + ;; Proves the protocol by giving working a and b. + + ;; Load the protocol + !(defq the-protocol !(load-expr "factors-8616460799")) + + ;; Find a solution + !(def comm_a_sol (hide #0x9040959483 89681)) + !(def comm_b_sol (hide #0x0984564598 96079)) + + ;; Prove the protocol with working a and b + !(prove-protocol the-protocol "factors-8616460799-proof" comm_a_sol comm_b_sol) + + ;; Inspect to make sure nothing is leaked + !(inspect "27ec4462cf3cd60f03a3c9db2b227a5fe5134226b6d4e4a5b40b55e1c0b284")
• factoring_test/factoring_protocol.lurk (new)
  • @@ -0,0 +1,54 @@
    + ;; Ask ryli13 if confused about this file. + ;; Define and dump a protocol to demonstrate knowledge of factoring 8616460799 = 89681 x 96079 + + ;; Making sure code works + !(def and (lambda (x y) (if x (if y t nil) nil))) + !(def a 89681) + !(def b 96079) + !(def comm_a_real (hide #0x8239548349 a)) + !(def comm_b_real (hide #0x3895383045 b)) + (let ((open_a (open comm_a_real)) + (open_b (open comm_b_real))) + (and (and (and (< 1 open_a) (< open_a 8616460799)) + (and (< 1 open_b) (< open_b 8616460799))) + (eq 8616460799 (* open_a open_b)) + ) + ) + + ;; Defining the actual protocol + !(defprotocol factors_found (comm_a comm_b) + (cons + ;; claim definition + (cons (cons + ;; expression + ;; needs to be a quoted syntax tree + (list 'let + ( + list (list 'open_a (list 'open comm_a)) + (list 'open_b (list 'open comm_b)) + ) + (list 'eq 'open_a 89681) + ) + ;; environment + (empty-env) + ) + ;; expected output + t ) + ;; post-verification predicate + nil) + :description "proof that one knows two non-one factors that multiply to 8616460799") + + !(dump-expr factors_found "factors-8616460799") + + (eval (list 'eq (list 'open 'comm_a) 89681) (let ((comm_a comm_a_real)) (current-env))) + + (eval + (emit (list + 'let + ( + list + (list 'open_a (list 'open comm_a_real)) + ) + (list 'eq 'open_a 89681) + ) + ) (empty-env))
• factoring_test/factoring_verification.lurk (new)
  • @@ -0,0 +1,4 @@
    + ;; Ask ryli13 if confused about this file. + ;; Verify the protocol + + ;; Inspect to see that nothing was leaked
• factoring_test/factors-8616460799 (new)
• factoring_test/factors-8616460799-proof (new)
• factoring_test/protocol-proof (new)
• factoring_test/protocol_examples.lurk (new)
  • @@ -0,0 +1,45 @@
    + ;; Define simple test protocol + !(defprotocol simple-protocol (n) + (cons + ;; claim definition + (cons (cons (list '= n n) (empty-env)) + t) + ;; post-verification predicate is not provided + nil) + :description "(= n n) reduces to t") + !(dump-expr simple-protocol "simple-protocol-file") + !(defq simple-protocol !(load-expr "simple-protocol-file")) + !(prove-protocol simple-protocol "protocol-proof" 3) + !(inspect "56b674aa77c68bdc916a01c122da092f7a5fdc9fd0b13646382f80bebcbe99") + !(verify-protocol simple-protocol "protocol-proof") + + ;; THE BELOW HAS BEEN BUTCHERED SO I CAN FIGURE STUFF OUT + ;; A protocol that requires knowledge of a hash that opens to a pair such that + ;; its components add up to 30. If the proof is accepted, further require that + ;; the first component of the pair be greater than 10. + !(defprotocol my-protocol (hash pair) + (cons + ;; claim definition + (cons (cons + ;; expression + (list 'open hash) + ;; environment + (empty-env)) + ;; expected output + pair) + nil) + :description "hash opens to a pair (a, b) s.t. a+b=30 and a>10") + + ;; This is the prover's pair, whose hash is + ;; #c0x955f855f302a30ed988cc48685c442ebd98c8711e989fc64df8f27f52e1350 + (commit '(13 . 17)) + + ;; Let's prove it and write the proof to the file protocol-proof + !(prove-protocol my-protocol + "protocol-proof" + #c0x955f855f302a30ed988cc48685c442ebd98c8711e989fc64df8f27f52e1350 + '(13 . 17)) + + ;; Now it can be verified + !(inspect "4dadc3bcba8e53c412002249f43cb23965f3808c4a2d458920dff3ff7f997f") + !(verify-protocol my-protocol "protocol-proof")
• factoring_test/simple-protocol-file (new)