Problem with Sum in Constraint

[DavePearce]

The following expression is not behaving as expected:

(eq! DATA_HI
              (+ (for i
                      [0 : LLARGEMO]
                      (* (^ 256 (- LLARGEMO i))
                         [BYTE_HI i]))))

This is suppose to reconstruct the value of a byte decomposition.

@letypequividelespoubelles Feel free to add any further comments

[DavePearce]

@letypequividelespoubelles One thing I can say immediately is that the expression is not formulated correctly. This is because arrays are indexed from 1 in Corset, not 0. Therefore, I think you can rewrite the above like so:

(eq! DATA_HI
              (+ (for i
                      [1 : LLARGE]
                      (* (^ 256 (- LLARGE i))
                         [BYTE_HI i]))))

Notice: [0 : LLARGEMO] becomes [1 : LLARGE] and likewise (^ 256 LLARGEMO) becomes (^ 256 LLARGE)

[DavePearce]

Ok, so there is an issue here. Here's my minimal test case:

(module test)

(defconst WIDTH 2)

(defcolumns
    WORD
    (BYTE :byte@prove :array[WIDTH]))

(defconstraint test1 () (eq! WORD
              (+ (for i [1:WIDTH]
                      (* (^ 256 (- WIDTH i)) [BYTE i])))))

(defconstraint test2 () (eq! WORD
              (+ (* 256 [BYTE 1]) [BYTE 2])))

Here, test1 and test2 are supposed to be equivalent. The output from corset debug -ceeee is:

test.test1 :=
WORD .- {
 256 * BYTE_1
 1 * BYTE_2
}

test.test2 :=
WORD .- (256 * BYTE_1 + BYTE_2)

Also, here's is a trace which is (unexpectedly) rejected by constraint test1 above (but not test2):

{ "test": {"WORD": [0,1,255,256,257], "BYTE_1": [0,0,0,1,1], "BYTE_2": [0,1,255,0,1] } }

Specifically, the last row of the trace where WORD=257, BYTE_1=1 and BYTE_2=1 is the problem.

[DavePearce]

I think the issue is related to how the for loops are being expanded. I guess that it is being expanded as this:

(defconstraint test2 ()
  (eq! WORD
       (+ (begin
           (* 256 [BYTE 1])
           [BYTE 2]))))

Yes, that's it.

@letypequividelespoubelles I'm not sure you can use a for loop in this way unfortunately. Its intended for generating multiple distinct constraints, rather than generating multiple expressions.

@delehef Any comments?

[delehef]

Yep, one should use reduce; as in (reduce + (for i [1:5] (* 3 i))) == $\sum_{i=1..5} 3 \times i$

There is a bug however; test1 should not compile, as + should refuse non-scalar arguments, such as the list generated by a for. Ideally, this should be fixed in the type validation for Intrinsic::Add.

[DavePearce]

Ah ha, thanks --- I've upgraded this to have bug status!

[letypequividelespoubelles]

@letypequividelespoubelles One thing I can say immediately is that the expression is not formulated correctly. This is because arrays are indexed from 1 in Corset, not 0. Therefore, I think you can rewrite the above like so:

Yes but in the columns.go, I specifically define the columns array to start at 0 : (BYTE_HI :array [0 : LLARGEMO] :byte@prove)

Yep, one should use reduce

I tried with reduce too but it was the exact same output

[DavePearce]

Yes but in the columns.go, I specifically define the columns array to start at 0

Ah, ok, I see. I will try to get reduce to work.

[DavePearce]

Can confirm this:

(module test)

(defconst WIDTH 2)

(defcolumns
    WORD
    (BYTE :byte@prove :array[WIDTH]))

(defconstraint test1 () (eq! WORD
              (reduce + (for i [1:WIDTH]
                      (* (^ 256 (- WIDTH i)) [BYTE i])))))

Accepts this trace:

{ "test": {"WORD": [0,1,255,256,257], "BYTE_1": [0,0,0,1,1], "BYTE_2": [0,1,255,0,1] } }

[DavePearce]

And, can also confirm this:

(module test)

(defconst
    WIDTH 2
    WIDTHMO (- WIDTH 1)
  )

(defcolumns
    WORD
    (BYTE :byte@prove :array[0:WIDTHMO]))

(defconstraint test1 () (eq! WORD
              (reduce + (for i [0:WIDTHMO]
                      (* (^ 256 (- WIDTHMO i)) [BYTE i])))))

accepts the following trace:

{ "test": {"WORD": [0,1,255,256,257], "BYTE_0": [0,0,0,1,1], "BYTE_1": [0,1,255,0,1] } }

@letypequividelespoubelles I think we need some more info on how its failing for you with reduce ?