feat: use assembly implementation of add module

[DavePearce]

Command to generate constraints (with nice formatting):

% go-corset debug --textwidth=80 --mir alu/add/add.zkasm

Generated constraints:

(module add)

(inputs
   (INST u8)
   (ARG_1'0 u128)
   (ARG_1'1 u128)
   (ARG_2'0 u128)
   (ARG_2'1 u128)
)

(outputs
   (RES'0 u128)
   (RES'1 u128)
)

(computed
   (c u1)
   (c$8 u1)
   (s$9 u1)
)

(compute add)
(range INST u8)
(range ARG_1'0 u128)
(range ARG_1'1 u128)
(range ARG_2'0 u128)
(range ARG_2'1 u128)
(range RES'0 u128)
(range RES'1 u128)
(range c u1)
(range c$8 u1)
(range s$9 u1)

(vanish (add:pc0)
   (if (== INST 1)
      (∧
         (== (+ RES'0 (* 2^128 c$8)) (+ ARG_2'0 ARG_1'0))
         (== (+ RES'1 (* 2^128 c)) (+ ARG_2'1 ARG_1'1 c$8)))
      (if (== INST 3)
         (∧
            (== RES'0 (+ (* ARG_2'0 -1) ARG_1'0 (* 2^128 s$9)))
            (== RES'1 (+ (* ARG_2'1 -1) ARG_1'1 (* s$9 -1) (* 2^128 c))))
         (∧ (== RES'0 0) (== RES'1 0)))))

[OlivierBBB]

Could you explain the output ? I'm confused about two things

• the meaning of (add:pc0)
• how to interpret constraints à la (vanish (bla) (if condition constraint))

[DavePearce]

@OlivierBBB No problem. The output is presented slightly differently from Corset lisp as it is the internal MIR representation. The (add:pc0) is just the handle for the constraint, where pc0 indicates its the constraint for the first instruction (i.e. at pc==0). However, since this is a one line function, there is only one instruction!

Anyway, the above is equivalent to this Corset lisp:

(module add)

(defcolumns 
   (INST :byte@prove)
   (ARG_1'0 :i128@prove)
   (ARG_1'1 :i128@prove)
   (ARG_2'0 :i128@prove)
   (ARG_2'1 :i128@prove)
   (RES'0 :i128@prove)
   (RES'1 :i128@prove)
   (c :binary@prove)
   (c$8 :binary@prove)
   (s$9 :binary@prove)
)

(defconstraint pc0 ()
   (if (== INST 1)
      (∧
         (== (+ RES'0 (* (^ 2 128) c$8)) (+ ARG_2'0 ARG_1'0))
         (== (+ RES'1 (* (^ 2 128) c)) (+ ARG_2'1 ARG_1'1 c$8)))
      (if (== INST 3)
         (∧
            (== RES'0 (+ (* ARG_2'0 -1) ARG_1'0 (* (^ 2 128) s$9)))
            (== RES'1 (+ (* ARG_2'1 -1) ARG_1'1 (* s$9 -1) (* (^ 2 128) c))))
         (∧ (== RES'0 0) (== RES'1 0)))))

If you run this file through the following command then you should get what we had originally:

> go-corset --textwidth=80 debug --mir add.lisp

If you want to see the raw constraints passed to the prover then use --air instead of --mir. You'll notice if you do this that the necessary modules for proving smallness of types are included along with their constraints and lookups.

[letypequividelespoubelles]

How is handled the padding ? I guess that now only conditional lookups will target ADD, so we don't need a row filled with 0's, that's why you can fill with any valid operation ? (I guess you fill with 0 + 0 = https://en.wikipedia.org/wiki/T%C3%AAte_%C3%A0_Toto ? )

[DavePearce]

Easy for now: add(0,0,0)=0