Add adder Test(s)

[DavePearce]

Here is my code:

(defcolumns
  (X3 :i16@prove) (X2 :i16@prove) (X1 :i16@prove) (X0 :i16@prove)
  (Y3 :i16@prove) (Y2 :i16@prove) (Y1 :i16@prove) (Y0 :i16@prove)
  (C3 :i1@prove)  (C2 :i1@prove)  (C1 :i1@prove)  (C0 :i1@prove)
  (Z3 :i16)       (Z2 :i16)       (Z1 :i16)       (Z0 :i16))

(defconst OVERFLOW 65536)

(defpurefun (ADDER cin arg1 arg2 out cout)
  (eq! (+ out (* cout OVERFLOW)) (+ arg1 arg2 cin)))

(defconstraint X_Y_Z ()
  (begin
   (ADDER 0 X0 Y0 Z0 C0)
   (ADDER C0 X1 Y1 Z1 C1)
   (ADDER C1 X2 Y2 Z2 C2)
   (ADDER C2 X3 Y3 Z3 C3)))

And an example trace:

{ "<prelude>": {
    "X3": [0], "X2": [0], "X1": [0], "X0": [33000],
    "Y3": [0], "Y2": [0], "Y1": [0], "Y0": [33001],
    "C3": [0], "C2": [0], "C1": [0], "C0": [1],        
    "Z3": [0], "Z2": [0], "Z1": [1], "Z0": [465]
}}

What we could do is actually enumerate all input / output values and check it really works. We could repeat this for other operators related to field agnosticity.

[DavePearce]

(defcolumns
  (X3 :i16@prove) (X2 :i16@prove) (X1 :i16@prove) (X0 :i16@prove)
  (RES :binary@prove)
)

(defpurefun ((IS-ZERO :binary@loob :force) w3 w2 w1 w0) (+ w3 w2 w1 w0))

(defconstraint c1 ()
  (if (IS-ZERO X3 X2 X1 X0)
      (vanishes! RES) (eq! RES 1)))

And an example trace:

{ "<prelude>": {
    "X3": [0], "X2": [0], "X1": [0], "X0": [0],
    "RES": [0]
}}

[DavePearce]

Another example (bit shift):

(module m1)

(defcolumns
  X Y
  ;; X bits
  (x1 :binary@prove)
  (x2 :binary@prove)
  (x3 :binary@prove)
  (x4 :binary@prove)
  ;; Y bits
  (y1 :binary@prove)
  (y2 :binary@prove)
  (y3 :binary@prove)
  (y4 :binary@prove))

;; Combine bits into a nibble
(defpurefun (bits a1 a2 a3 a4)
  (+ (* 1 a1)
     (* 2 a2)
     (* 4 a3)
     (* 8 a4)))

;; For X
(defconstraint X_bits () (eq! X (bits x1 x2 x3 x4)))
;; For Y
(defconstraint Y_bits () (eq! Y (bits y1 y2 y3 y4)))
;; Relating X and Y
(defconstraint X_Y_bits ()
  (begin
   (eq!  0 y1)   
   (eq! x1 y2)
   (eq! x2 y3)
   (eq! x3 y4)))

Which accepts this trace:

{ "m1": {
    "X": [0,1,14],
    "Y": [0,2,12],
    
    "x1": [0,1,0],
    "x2": [0,0,1],
    "x3": [0,0,1],
    "x4": [0,0,1],
    
    "y1": [0,0,0],
    "y2": [0,1,0],
    "y3": [0,0,1],
    "y4": [0,0,1]
   }
}

[DavePearce]

Another one for comparison:

(module m1)

(defcolumns
  ARG1
  ARG2
  WIT
  (RES :binary@prove)
  (ARG1_b1 :byte@prove)
  (ARG1_b2 :byte@prove)
  (ARG2_b1 :byte@prove)
  (ARG2_b2 :byte@prove)
  (WIT_b1 :byte@prove)
  (WIT_b2 :byte@prove)  
  )

;; Enforce that a column is a U16
(defpurefun (IS_U16 c b1 b2)
  (eq! c (+ b1 (* 256 b2))))

;; Enforce ARG1,ARG2,WIT are u16
(defconstraint types () (begin
			  (IS_U16 ARG1 ARG1_b1 ARG1_b2)
			  (IS_U16 ARG2 ARG2_b1 ARG2_b2)
			  (IS_U16 WIT WIT_b1 WIT_b2)))

(defconstraint res ()
  (if-zero RES
	   ;; if RES==0 then ARG1==ARG2+WIT
	   (eq! ARG1 (+ ARG2 WIT))
	   ;; if RES==1 then ARG2==ARG1+WIT
	   (eq! (+ ARG1 WIT) ARG2)))

;; Witness cannot be zero when RES==0
(defconstraint wit ()
  (if-not-zero RES
	   (is-not-zero! WIT)))

With this trace:

{ "m1": {
    "ARG1": [0,2,5,4834], "ARG1_b1": [0,2,5,226], "ARG1_b2": [0,0,0,18],
    "ARG2": [0,3,2,258],  "ARG2_b1": [0,3,2,2],   "ARG2_b2": [0,0,0,1],
    "WIT":  [0,1,3,4576], "WIT_b1":  [0,1,3,224], "WIT_b2":  [0,0,0,17],
    "RES":  [0,1,0,0]
}}

[DavePearce]

(module m1)

(defcolumns
  STAMP
  CT
  ARG_1
  ARG_2
  WIT
  (RES :binary@prove)
  ACC_1
  ACC_2
  ACC_3
  (BYTE_1 :byte@prove)  
  (BYTE_2 :byte@prove)
  (BYTE_3 :byte@prove))

;; ===================================================================
;; Heartbeat constraints
;; ===================================================================

;; In the first row, STAMP is always zero.  This allows for an
;; arbitrary amount of padding at the beginning which has no function.
(defconstraint first-row (:domain {0})
  (vanishes! STAMP))

;; The stamp either remains constant between rows, or can increase by
;; at most 1.
(defconstraint stamp-increments ()
  (any! (will-remain-constant! STAMP) (will-inc! STAMP 1)))

;; Whenever the stamp changes, the counter resets to 0.
(defconstraint counter-reset ()
  (if-not-zero (will-remain-constant! STAMP)
               (vanishes! (next CT))))

;; Whenever the counter reaches 3, then the stamp will increase by
;; one.  Otherwise, the counter increases by 1.
(defconstraint heartbeat (:guard STAMP)
  (if-eq-else CT 3 (will-inc! STAMP 1) (will-inc! CT 1)))

;; ===================================================================
;; Counter Constant
;; ===================================================================

;; From the standard library
(defpurefun ((counter-constancy :@loob) ct X)
  (if-not-zero ct
               (remained-constant! X)))

;; These columns cannot change between frames.
(defconstraint counter-constancies ()
  (begin (counter-constancy CT ARG_1)
         (counter-constancy CT ARG_2)
         (counter-constancy CT RES)
         (counter-constancy CT WIT)))

;; ===================================================================
;; Byte decomposition
;; ===================================================================

;; Similar to what is found in the standard library
(defpurefun (byte-decomposition ct acc digits)
  (if-zero ct
           (eq! acc digits)
           (eq! acc (+ (* 256 (prev acc)) digits))))

;; ACC_1 accumulates bytes from BYTE_1, etc.
(defconstraint byte_decompositions ()
  (begin (byte-decomposition CT ACC_1 BYTE_1)
         (byte-decomposition CT ACC_2 BYTE_2)
         (byte-decomposition CT ACC_3 BYTE_3)))

;; ===================================================================
;; Target Constraints
;; ===================================================================

;; Connect columns with accumulators.  For example, this ensures that
;; the final accumulated value for ARG_1 does indeed match ARG_1.
(defconstraint target-constraints (:guard STAMP)
  ;; Target constraints hold on last line of frame.
  (if-eq CT 3
	 (begin
	  (eq! ARG_1 ACC_1)
	  (eq! ARG_2 ACC_2)
	  (eq! WIT ACC_3))))

;; ===================================================================
;; Result Constraints
;; ===================================================================

(defconstraint res (:guard STAMP)
  ;; Target constraints hold on last line of frame.
  (if-eq CT 3
	 ;; 
	 (if-zero RES
	   ;; if RES==0 then ARG_1==ARG_2+WIT
	   (eq! ARG_1 (+ ARG_2 WIT))
	   ;; if RES==1 then ARG_2==ARG_1+WIT
	   (eq! (+ ARG_1 WIT) ARG_2))))

(defconstraint wit (:guard STAMP)
  ;; Target constraints hold on last line of frame.
  (if-eq CT 3
	 ;; Witness must be zero when RES==0	 
	 (if-not-zero RES
	      (is-not-zero! WIT))))

{ "m1": {
    "ARG_1":  [0,0,0,0,    288,  288,  288,  288],
    "ARG_2":  [0,0,0,0,  70123,70123,70123,70123],
    "RES":    [0,0,0,0,      1,    1,    1,    1],
    "WIT":    [0,0,0,0,  69835,69835,69835,69835],
    
    "STAMP":  [1,1,1,1,      2,    2,    2,    2],
    "CT":     [0,1,2,3,      0,    1,    2,    3],
    "ACC_1":  [0,0,0,0,      0,    0,    1,  288],
    "ACC_2":  [0,0,0,0,      0,    1,  273,70123],
    "ACC_3":  [0,0,0,0,      0,    1,  272,69835],   
    "BYTE_1": [0,0,0,0,      0,    0,    1,   32],
    "BYTE_2": [0,0,0,0,      0,    1,   17,  235],
    "BYTE_3": [0,0,0,0,      0,    1,   16,  203]
   }
}