factoring test proof made

Changes

5 changed files (+34/-7)

• factoring_test/factoring_proof.lurk
  • @@ -12,4 +12,4 @@
    !(prove-protocol the-protocol "factors-8616460799-proof" comm_a_sol comm_b_sol) ;; Inspect to make sure nothing is leaked - !(inspect "27ec4462cf3cd60f03a3c9db2b227a5fe5134226b6d4e4a5b40b55e1c0b284") + !(inspect "3e15a128f3c233ca51fe94b9bf17bbca769bc14c332fa003d7808d525d54c")
• factoring_test/factoring_protocol.lurk
  • @@ -26,8 +26,18 @@
    ( list (list 'open_a (list 'open comm_a)) (list 'open_b (list 'open comm_b)) + (list 'and (list 'lambda (list 'x 'y) (list 'if 'x (list 'if 'y t nil) nil))) + ) + (list 'and + (list 'and + (list 'and + (list '< 1 'open_a) + (list '< 'open_a 8616460799)) + (list 'and + (list '< 1 'open_b) + (list '< 'open_b 8616460799))) + (list 'eq 8616460799 (list '* 'open_a 'open_b)) ) - (list 'eq 'open_a 89681) ) ;; environment (empty-env)
  • @@ -43,12 +53,22 @@
    (eval (list 'eq (list 'open 'comm_a) 89681) (let ((comm_a comm_a_real)) (current-env))) (eval - (emit (list - 'let + (emit + (list 'let ( - list - (list 'open_a (list 'open comm_a_real)) + list (list 'open_a (list 'open comm_a_real)) + (list 'open_b (list 'open comm_b_real)) + (list 'and (list 'lambda (list 'x 'y) (list 'if 'x (list 'if 'y t nil) nil))) + ) + (list 'and + (list 'and + (list 'and + (list '< 1 'open_a) + (list '< 'open_a 8616460799)) + (list 'and + (list '< 1 'open_b) + (list '< 'open_b 8616460799))) + (list 'eq 8616460799 (list '* 'open_a 'open_b)) ) - (list 'eq 'open_a 89681) ) ) (empty-env))
• factoring_test/factoring_verification.lurk
  • @@ -1,4 +1,11 @@
    ;; Ask ryli13 if confused about this file. ;; Verify the protocol + ;; Load protocol + !(defq the-protocol !(load-expr "factors-8616460799")) + ;; Inspect to see that nothing was leaked + !(inspect "3e15a128f3c233ca51fe94b9bf17bbca769bc14c332fa003d7808d525d54c") + + ;; Now verify the proof (stored at factors-8616460799-proof) + !(verify-protocol the-protocol "factors-8616460799-proof")
• factoring_test/factors-8616460799
• factoring_test/factors-8616460799-proof