search

Consensys / corset

4 stars 12 forks source link

Incorrect typing of `eq!` #140

Closed delehef closed 1 month ago

delehef commented 1 month ago

The following patch must be applied to the standard library:

-(defpurefun ((eq! :binary@loob :force) x y) (~>> (-. x y)))
+(defpurefun ((eq! :@loob :force) x y) (~>> (-. x y)))

~>> is a no-op in the current state of affairs, and will always be for single-field-element values.

DavePearce commented 1 month ago

@delehef Is this a fix for #138, or just something you have noticed ?

DavePearce commented 1 month ago

Test case:

(defcolumns (A :binary) B)
(defconstraint test1 () (vanishes! (eq (eq! A B) 1)))

This originally generated:

test1 :=
   (A .- B - 1)^2

And now generates:

=== Constraints ===

test1 :=
1 - (A .- B .- 1) * C/INV[(.- (.- A B) 1)]

NORM[(.- (.- A B) 1)] :=
|(.- (.- A B) 1)| == (.- (.- A B) 1) × C/INV[(.- (.- A B) 1)]
(.- (.- A B) 1)×(1 - (.- (.- A B) 1)×C/INV[(.- (.- A B) 1)]) = 0
C/INV[(.- (.- A B) 1)]×(1 - (.- (.- A B) 1)×C/INV[(.- (.- A B) 1)]) = 0

=== Computations ===
C/INV[(.- (.- A B) 1)] = (inv (.- (.- A B) 1))
DavePearce commented 1 month ago

Have also recompiled the zkevm.bin and that appears to have gone through.

delehef commented 1 month ago

Just something I noticed while crafting an example for #139 ;)