Wrong Evaluation of Constraint Expressions using Expansion

[LukiMueller]

I have found vanishing constraint instances that show a different behavior depending on providing the expansion flag -e or not.

Following instances behave the same regardless of the trace:

test.lisp

(defcolumns X)

(defconstraint constraint-1 () (is-not-zero! (if (is-zero 1) 1 1)))
(defconstraint constraint-2 () (eq! (is-not-zero! (if (is-zero X) 1 X)) 0))
(defconstraint constraint-3 () (eq! (~and! (is-not-zero! (if (is-zero 0) 1 0)) 0) 0))
(defconstraint constraint-4 () (is-not-zero! (if (is-zero 0) 1 0)))
(defconstraint constraint-5 () (is-not-zero! (if (is-zero X) 1 X)))

but currently the output differs depending on the -e flag

> corset check test.lisp -N --trace trace.json

> corset check test.lisp -Ne --trace trace.json
Error: while checking trace.json

Caused by:
    constraints failed: constraint-3, constraint-5, constraint-2, constraint-1, constraint-4

I also have two examples where the trace makes a difference:

test.lisp

(defcolumns X ST)

(defconstraint constraint-6 () (if-not-zero ST (neq! 1 (if (is-zero 0) X X))))
(defconstraint constraint-7 () (if-not-zero ST (neq! 0 (if (is-zero X) X X))))

trace1.json

{
    "<prelude>": { "ST": [ 1 ], "X": [ 1 ] }
}

trace2.json

{
    "<prelude>": { "ST": [ 1 ], "X": [ 0 ] }
}

> corset check test.lisp -N --trace trace1.json
Error: while checking trace.json

Caused by:
    constraints failed: constraint-6

> corset check test.lisp -Ne --trace trace1.json
Error: while checking trace.json

Caused by:
    constraints failed: constraint-6, constraint-7

> corset check test.lisp -N --trace trace2.json
Error: while checking trace.json

Caused by:
    constraints failed: constraint-7

> corset check test.lisp -Ne --trace trace2.json
Error: while checking trace.json

Caused by:
    constraints failed: constraint-6, constraint-7

The last examples are slightly different than the first, as the present rather than the absence of -e triggers the constraints.
They all seem related to if, is-zero and if-not-zero.
I am using corset version corset 9.7.13 b573a83.

[OlivierBBB]

I may be getting confused with Boolean/loobean values but shouldn't

(defconstraint constraint-1 () (is-not-zero! (if (is-zero 1) 1 1)))

Always evaluate to 0 and thus be satisfied as a constraint ?

[LukiMueller]

(is-not-zero! 1)
(- 1 (is-not-zero 1))
(- 1 (~ 1))
(- 1 1)
0

@OlivierBBB , you are absolutely right, I got the values mixed up! I update the issue from "[...] should always fail [...]" to something like "[...] shows the same behavior [...]".

Moreover, it seems that in this case (is-not-zero! (if (is-zero 1) 1 1) evaluates to a non-zero value if the -e-flag is present, because the constraint fails.

[DavePearce]

Hey Christoph,

Yes, there is a problem with the handling of if conditions when they are nested within certain expressions (e.g. (- 1 (if (is-zero 1) ...)).

[DavePearce]

Ok, I believe that is fixed now. Let me know if any more failing tests surface.

[LukiMueller]

I am sorry to report that this issue is not resolved yet:

test-1.lisp

(module module-0)
(defcolumns in0 ST)
(defconstraint constraint-0 () (if-not-zero ST (vanishes! (if (is-zero (if (is-zero 1) 0 0)) (if (is-zero in0) in0 0) (~and! 1 1)))))
(defconstraint constraint-1 () (if-not-zero ST (vanishes! (if (is-zero (~or! (if (is-zero 1) 0 0) (if (is-zero 1) 0 0))) (if (is-zero in0) in0 0) (~and! 1 1)))))
(defconstraint constraint-2 () (if-not-zero ST (vanishes! (is-not-zero! (is-not-zero! (if (is-zero (if (is-zero 1) 0 0)) (if (is-zero in0) in0 0) (~and! 1 1)))))))
(defconstraint constraint-3 () (if-not-zero ST (vanishes! (~or! (if (is-zero (if (is-zero 1) 0 0)) (if (is-zero in0) in0 0) (~and! 1 1)) 1))))
(defconstraint constraint-4 () (if-not-zero ST (vanishes! (if (is-zero (if (is-zero 1) 0 0)) (if (is-zero in0) in0 0) 1))))
(defconstraint constraint-5 () (if-not-zero ST (vanishes! (~and! (if (is-zero (if (is-zero 1) 0 0)) (if (is-zero in0) in0 0) (~and! 1 1)) (if (is-zero (if (is-zero 1) 0 0)) (if (is-zero in0) in0 0) (~and! 1 1))))))

(module module-1)
(defcolumns in0 ST)
(defconstraint constraint-0 () (if-not-zero ST (vanishes! (if (is-zero (if (is-zero 1) 0 0)) (if (is-zero in0) in0 0) (~and! 1 1)))))
(defconstraint constraint-1 () (if-not-zero ST (vanishes! (if (is-zero (~or! (if (is-zero 1) 0 0) (if (is-zero 1) 0 0))) (if (is-zero in0) in0 0) (~and! 1 1)))))
(defconstraint constraint-2 () (if-not-zero ST (vanishes! (is-not-zero! (is-not-zero! (if (is-zero (if (is-zero 1) 0 0)) (if (is-zero in0) in0 0) (~and! 1 1)))))))
(defconstraint constraint-3 () (if-not-zero ST (vanishes! (~or! (if (is-zero (if (is-zero 1) 0 0)) (if (is-zero in0) in0 0) (~and! 1 1)) 1))))
(defconstraint constraint-4 () (if-not-zero ST (vanishes! (if (is-zero (if (is-zero 1) 0 0)) (if (is-zero in0) in0 0) 1))))
(defconstraint constraint-5 () (if-not-zero ST (vanishes! (~and! (if (is-zero (if (is-zero 1) 0 0)) (if (is-zero in0) in0 0) (~and! 1 1)) (if (is-zero (if (is-zero 1) 0 0)) (if (is-zero in0) in0 0) (~and! 1 1))))))

trace.json

{
    "module-0": {
        "in0": [
            0
        ],
        "ST": [
            1
        ]
    },
    "module-1": {
        "in0": [
            1
        ],
        "ST": [
            1
        ]
    }
}

These constraints together with the provided trace pass for corset check test-1.lisp --trace trace.json -N but fail for corset check test-1.lisp --trace trace.json -Ne

---

I also picked out one of those instances and experimented with it and found following behavior (given the same trace):

(module module-0)
(defcolumns in0 ST)

;; fails for the flags "-Ne" but not "-N"
(defconstraint constraint-0 () (if-not-zero ST (vanishes! (if (is-zero (if (is-zero 1) 0 0)) in0 (~and! 1 1)))))

;; does not fail anymore
(defconstraint constraint-1 () (if-not-zero ST (vanishes! (if (is-zero                 0           ) in0 (~and! 1 1)))))

;; does not fail anymore
(defconstraint constraint-1 () (if-not-zero ST (vanishes!                                in0                                         ))

(module module-1)
(defcolumns in0 ST)

;; fails for the flags "-N" and "-Ne"
(defconstraint constraint-0 () (if-not-zero ST (vanishes! (if (is-zero (if (is-zero 1) 0 0)) in0 (~and! 1 1)))))

;; fails for the flags "-N" and "-Ne"
(defconstraint constraint-1 () (if-not-zero ST (vanishes! (if (is-zero                 0           ) in0 (~and! 1 1)))))

;; fails for the flags "-N" and "-Ne"
(defconstraint constraint-1 () (if-not-zero ST (vanishes!                                in0                                         ))

It seems that for all the provided instances (if (is-zero 1) 0 0) makes some troubles.

---

I also found this interesting behavior (which might be unrelated):

;; fails for "-Neeee" but not for "-Neee"
(module module-0)
(defcolumns ST)
(defconstraint constraint-0 () (is-not-zero! (~and! (if (is-zero 1) 1 1) (if (is-zero 1) 1 1))))

;; no longer fails
(module module-0)
;; (defcolumns ST) ;; <-- commented out
(defconstraint constraint-0 () (is-not-zero! (~and! (if (is-zero 1) 1 1) (if (is-zero 1) 1 1))))

---

> corset --version
corset 9.7.13 e50d554 SIMD JSON parsing unavailable

[DavePearce]

Ok, so the related issue is in the same file as the original problem, but a different method. However, overall, this particular file has caused considerable problems thus far. Therefore, I am going to rework it from scratch.