JSON Traces Involving Perspectives

[DavePearce]

(@delehef following on our discussion from #128)

I am trying to check a trace involving a perspective. Here is my test:

(module test)
(defcolumns A B)
(defperspective A_B A (B))
(defconstraint B-zero (:perspective A_B) (vanishes! B))

Here is my example trace:

{ "test": {
        "A": [0,1,2],
        "B": [1,0,0],
        "B/A_B": [0,0,0]
        }
}

This currently reports the following:

[ERROR] test.B%A_B not found in the given trace
[ERROR] all columns in (* test.A test.A_B/B) are not of the same length:
        test.A: 4
        test.A_B/B: nil
Error: while checking issue128.trace

Its strange because the following variation behaves differently:

{ "test": {
        ...
        "B%A_B": [0,0,0]
        }
}

This just gives the following error:

[ERROR] test.B%A_B not found in the given trace

So it feels like, in the first trace, column A_B/B is being recognised in someway but then we encounter a bug?

[DavePearce]

Ok, finally figured it out. With these constraints:

(module test)
(defcolumns A B)
(defperspective A_B A (C))
(defconstraint C-zero (:perspective A_B) (vanishes! C))

This trace is accepted:

{ "test": {
        "A": [0,1,2],
        "B": [1,0,0],
        "C": [1,1,0]
        }
}

[DavePearce]

So, interesting that this is not rejected:

(defcolumns A B)
(defperspective A_B A (B))

Surely this is a conflicting definition? It does appear to allocate different columns:

  ID                                                                            Name  Type   ×                                              Reg.
   1                                                                          test.A     𝔽   1                                       r0/test.Aι1
   0                                                                          test.B     𝔽   1                                       r1/test.Bι1
   2                                                                      test.A_B/B     𝔽   1

However, that then brings into question how a trace is interpreted in this case.

[DavePearce]

Next issue:

(module test)
(defcolumns A B)
;; First perspective
(defperspective A_C A (C))
(defconstraint C-zero (:perspective A_C) (vanishes! C))
;; Second perspective
(defperspective B_D B (D))
(defconstraint D-one (:perspective B_D) (eq! 1 D))

Now, I can't seem to write a trace which is accepted here. For example:

{ "test": {
        "A": [0,1,2],
        "B": [1,0,0],
        "C": [1,0,0],
        "D": [1,1,1]
        }
}

Is rejected with this error:

[ERROR] test.C%A_C not found in the given trace
[ERROR] test.D%B_D not found in the given trace

However, if I e.g. comment out the two lines related to perspective A_C then the trace is accepted.

[DavePearce]

Ok, after some digging through the code, I found that it is indeed possible:

{ "test": {
        "A": [0,1,2],
        "B": [1,0,0],
        "C_xor_D": [0,0,0]
        }
}

Not sure what I think about the syntax here ... but I get the idea :)

[DavePearce]

Ok, and finally, I can run test which sent me on this goose chase:

(module test)
(defcolumns A B)
;; First perspective
(defperspective A_C A (C))
(defconstraint C-not-one (:perspective A_C) (vanishes! (eq 1 C)))
;; Second perspective
(defperspective B_D B (D))
(defconstraint D-not-twp (:perspective B_D) (vanishes! (eq 2 D)))

{ "test": {
        "A": [0,1,2],
        "B": [1,0,0],
        "C_xor_D": [0,0,0]
        }
}

This trace is accepted without any warnings or errors:

[INFO] Parsing Corset source files...
[INFO] Parsing stdlib
[INFO] Parsing issue128.lisp
[INFO] Parsing trace from JSON file with SIMD, Elapsed=817.725µs
[INFO] Computing expanded columns, Elapsed=2.64µs
[INFO] test.C-not-one validated
[INFO] test.D-not-twp validated
[INFO] Validation successful
[INFO] issue128.trace: SUCCESS

@letypequividelespoubelles You have your answer here. Corset does not report any errors or warnings when two perspectives are enabled at the same time. I guess the assumption is that (as in this case) its possible for that to make sense? If there should indeed be an invariant that no two perspectives should be enabled at the same time then we need to fix this.