new-cs.lisp 704 B

1234567891011121314151617181920212223242526272829303132333435
  1. (println "new-cs.lisp")
  2. (setup
  3. (let* [aux (scalar 3)
  4. x (alloc "x" aux)
  5. x2 (alloc "x2" (* aux aux))
  6. x3 (alloc "x3" (* aux (* aux aux)))
  7. input (alloc-input "input variable" aux)]
  8. ;; (enforce left right output)
  9. (enforce
  10. (scalar::one x)
  11. (scalar::one x)
  12. (scalar::one x2)
  13. )
  14. (enforce
  15. (scalar::one x2)
  16. (scalar::one x)
  17. (scalar::one x3)
  18. )
  19. (enforce
  20. (scalar::one input)
  21. (scalar::one cs::one)
  22. (scalar::one x3)
  23. )
  24. ;; (enforce
  25. ;; (scalar::one tmp)
  26. ;; ((scalar::one left_i) (mimc_constant cs::one))
  27. ;; ((scalar::one left_i_1) ((neg scalar::one) right))
  28. ;; )
  29. ))
  30. (prove))
  31. ;; (println 'verify (MyCircuit (scalar 27)))