new-cs.lisp 712 B

123456789101112131415161718192021222324252627282930313233343536
  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. (
  10. (enforce
  11. (scalar::one x)
  12. (scalar::one x)
  13. (scalar::one x2)
  14. )
  15. (enforce
  16. (scalar::one x2)
  17. (scalar::one x)
  18. (scalar::one x3)
  19. )
  20. (enforce
  21. (scalar::one input)
  22. (scalar::one cs::one)
  23. (scalar::one x3)
  24. )
  25. ;; (enforce
  26. ;; (scalar::one tmp)
  27. ;; ((scalar::one left_i) (mimc_constant cs::one))
  28. ;; ((scalar::one left_i_1) ((neg scalar::one) right))
  29. ;; )
  30. )
  31. ))
  32. (prove))
  33. ;; (println 'verify (MyCircuit (scalar 27)))