Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Error when Missing Reduce #191

Closed
DavePearce opened this issue Jun 11, 2024 · 6 comments · Fixed by #194
Closed

Error when Missing Reduce #191

DavePearce opened this issue Jun 11, 2024 · 6 comments · Fixed by #194
Labels
bug Something isn't working

Comments

@DavePearce
Copy link
Collaborator

The following examples should generate a corset error, but currently do not:

(module test)
(defcolumns X (BYTE :array[0:2]))
(defconstraint test ()
  (vanishes! (+ (for k [0:2] [BYTE k]))))
(module test)
(defcolumns X (BYTE :array[0:2]))
(defconstraint test
  (:guard (+ (for k [0:2] [BYTE k])))
    (vanishes! X))

The problem is that we're missing reduce. For example, a corrected version for the first example above is:

(module test)
(defcolumns X (BYTE :array[0:2]))
(defconstraint test ()
  (vanishes! (reduce + (for k [0:2] [BYTE k]))))
@DavePearce DavePearce added the bug Something isn't working label Jun 11, 2024
@DavePearce
Copy link
Collaborator Author

@delehef (migrated from #176)

This should fail at the verification of the arguments to +, that accepts multiple arguments, but not an argument that is a list.

This is a problem because you can't easily distinguish cases where an expression represents a "unit" or not. Examples:

(defconstraint test ()
  (vanishes! (+ X (begin 1 2))
(defconstraint test ()
  (vanishes! (+ (if X 1 0))))

These are all valid in some sense, even if they're a bit non-sensical. It seems like we could outlaw situations like this ... but that could prevent existing code from compiling? In the case of a guard, well it makes sense there at least.

@DavePearce
Copy link
Collaborator Author

DavePearce commented Jun 12, 2024

Right, so I have a partial fix for this which catches occurrences in :guards. These are easier since we expect guards to be "atomic". That is, to be expressions which will not expand into multiple expressions. So, guards like this don't make sense:

(module test)
(defcolumns (P :binary@bool) X)
(defun (wierd) (if P (eq X 1) (eq X 2)))
(defconstraint test (:guard (wierd)) (vanishes! X))

This previously compiled, though I don't think it really makes sense? The generated constraints are:

test.test :=
{
 P * (1 - NORM(X .- 1))
 (1 - NORM(P)) * (1 - NORM(X .- 2))
} * X

@DavePearce
Copy link
Collaborator Author

The challenge is that its not clear to me how to fix the general problem. Some points:

  • Checking the parameters for + are atomic is quite restrictive. If we apply this uniformly to e.g. + / * / - then the existing constraints fail to compile as, internally, corset uses multiplication to generate expressions like (* (begin ... )).
  • Perhaps for + alone it might work, but that doesn't seem very consistent.

One possibility might be to make the internal uses of * explicit by having another Intrinsic (e.g. Intrinsic::Select) or perhaps a flag indicating a "relaxed" intrinsic.

@DavePearce
Copy link
Collaborator Author

Ok, have resolved that in two ways: firstly, only checking arguments explicitly for lists; secondly, managing the one internal call (related to perspective selectors) by disabling validation for that call.

@DavePearce DavePearce linked a pull request Jun 12, 2024 that will close this issue
@delehef
Copy link
Contributor

delehef commented Jun 12, 2024

(defconstraint test ()
  (vanishes! (+ X (begin 1 2))

This one should be refused because (i) vanishes! should only accept columns or scalars, not list, (ii) same for +.

(defconstraint test ()
  (vanishes! (+ (if X 1 0))))

This one is acceptable I believe (although I reckon it's just a convoluted way of writing (vanishes! X)): + with a single argument is the identity, and the if will return a column-scaled value.

@DavePearce
Copy link
Collaborator Author

This one should be refused because (i) vanishes! should only accept columns or scalars

Did you have any specific mechanism for detecting whether a Node returns a column or scalar? I added two methods for this (one is recursive, the other is not): Node::is_atomic and Node::is_list. I didn't see any existing mechanism for this, but if there is then it'd be better to use that!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants