anoma / alucard

A common lisp DSL for writing zero knowledge circuits
https://anoma.github.io/alucard
18 stars 1 forks source link

Remove binders to void #26

Open mariari opened 2 years ago

mariari commented 2 years ago

With the last commit, explciit voids can be generated from standalone with-constraint.

This means that the code currently generates out a void with the following code

(defcircuit range-check ((private input int)
                         (output void))
  (with-constraint (b1 b0)
    (with-constraint (b2 b3)
      (= input (+ b1 b2)))))

ALU-TEST> (pipeline:pipeline (storage:lookup-function :range-check))
def range_check input {
  g71716 = b1 + b2
  input = g71716
  g71717 = input
  vg71718 = void
}

It would be good if we removed the void as it would be an improper binding.

This task should be simple, since we generate out a typing map, in the past we had

;; Update logic so that we can get inference on this.
(-> remove-void-bindings (ir:fully-expanded-list) ir:fully-expanded-list)
(defun remove-void-bindings (terms)

which would scan the syntax manually for applications to remove the bindings.

Thus this should be updated to use the typing map to check if a value is void and do the transformations then.

mariari commented 2 years ago

Edit:

With the following change

@@ -216,7 +216,8 @@ of the user program is preserved."
                                     (list (ir:var term))))
                         (ir:make-multiple-bind :var nil :val (ir:value term)))
                        ((and (typep value 'ir:reference)
-                             (sycamore:tree-set-find set (ir:name value)))
+                             (or (alu.spec.term-op:void-reference? value)
+                                 (sycamore:tree-set-find set (ir:name value))))
                         (sycamore:tree-set-insertf set (ir:var term))
                         nil)

in remove-void-bindings the void is gone, however the shift to using the typing map should happen here, as more primitives should trigger this issue