Consensys / corset

6 stars 12 forks source link

Invalid Lookups Not Reported #166

Open DavePearce opened 1 month ago

DavePearce commented 1 month ago

Consider this example:

(module m1)
(defcolumns X Y)
(deflookup test (m2.A m3.B) X Y)

(module m2)
(defcolumns A)

(module m3)
(defcolumns A)

And the following trace:

{ "m1": {"X": [1], "Y": [1]}, "m2": {"A": [1,2]}, "m3": {"B": [1,2,3,4]}}

Then, corset check will accept this trace as valid. However, it is not valid. Specifically, source (resp. target) columns must have the same height. In otherwords, they must always be in the same module.

DavePearce commented 1 month ago

A related example:

(deflookup test (m3.A) ((* m1.X m2.Y)))

(module m1)
(defcolumns X)

(module m2)
(defcolumns Y)

(module m3)
(defcolumns A)

And, with this trace:

{ "m1": {"X": [2,1,2]}, "m2": {"Y": [1,2,3]}, "m3": {"A": [2,6,8]}}

Then, corset actually crashes (Option::unwrap() on a None value).

delehef commented 1 month ago

You're right, a deflookup must check that all the columns in either side of the lookup stem from the same module; I guess we never hit this case before.

On top of that, as you mentioned in #161, at least one raw column should exist in the Node::leaves of at least one of the right-hand side and one of the left-hand side expressions of the lookup; otherwise we are looking up mindless functions and/or constants on each side, which does not make any sense.

delehef commented 1 month ago

I reckon the best place to implement such a check would be here; as at this point, you have two lists of nodes of the same size for the left- and right-hand criterions of the lookup; so a solution would probably be to have something like:

assert!(
  parents.iter().flat_map(|node| node.leaves()).any(|parent_leaf| parent_leaf.is_raw_column()) &&
  children.iter().flat_map(|node| node.leaves()).any(|child_leaf| child_leaf.is_raw_column()))

(pseudo-code of course, but I'm sure you get the idea)

DavePearce commented 1 month ago

Ok, interesting. I have just put together a solution. However, i did the error checking at the point where the module calculation was occurring. I will have a look at doing it earlier in the pipeline, as thinking about that does make sense!

DavePearce commented 1 month ago

Right, #167 has now put in place an error for this example which is currently triggered only when e.g. corset check -eeee is used. As such, a better error would make sense, and this issue is now focused on fixing that.