Extended Testing Framework

[DavePearce]

There is currently a small testing framework in the file src/tests.rs. However, it only checks that a given set of lisp constraints can be translated into a constraint set. It doesn't actually check what they evaluate to. Some aspects of a good testing framework would be:

1. (Evaluation Tests) These are tests which evaluate a given set of constraints against a given set of tabular data. They can be run at all levels as well to help ensure correct translation and trace expansion.
2. (Translation Tests) These are tests which can make use of automation. Specifically, given a set of constraints we can fuzz them to check evaluation between lower and higher levels matches.
3. (Regression Tests) These are translation tests where the current accepted output is stored in a file for regression purposes only. That is, since we don't know a priori what the expected outcomes of a given set of constraints are for a given set of input data, then regression is the only option.
4. (Expansion Tests) These tests check that a given input trace is expanded as expected. That is, computed columns get the correct values.
5. (Model Tests) In this case, we have some kind of model (e.g. of a memory unit) with a property that, for any valid arithmetic trace, we can reconstruct a trace of the model. Using this model we can generate many random traces which should pass. We can also generate many many random traces and, for any which do pass, check they are always valid model traces.

A key question here is what format the tests should be in. Another question is, of course, what base the outcome data should be in (i.e. naturals or field elements for a given prime, etc).

[DavePearce]

In question to the test format, its worth noting there are already a number of simple lisp files in the tests/ directory. They do not have expected evaluation results, however.

[DavePearce]

For evaluation tests:

• (Pass / Fail) It makes sense to record whether a given table is expected to meet the given constraints, or not. That is because such a result is independent of the base field, etc.
• (Field Specific) For a given field then, it makes sense to consider exact input / output results. Thus, BigInt can be considered a special case.

[DavePearce]

We already have a trace format which looks like this:

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

Therefore, it would make sense for each module to list the constraints and their evaluation results.

[DavePearce]

To be honest, accept fail would be good enough as a starting point. Its only when a constraint fails that we have an output which is anything other than 0 !

[DavePearce]

Simple Permutation Model

(module test)
(defcolumns A)
(defpermutation (B) ((+ A)))
;; Enforce that B is always in consecutive order
(defconstraint consecutive ()
  (vanishes! (- B 1 (shift B -1))))

Valid Traces

A valid input is an array of n consecutive elements starting from 1 which have been randomly shuffled.

{"test": { "A": [1] } }
{"test": { "A": [1,2] } }
{"test": { "A": [2,1] } }
{"test": { "A": [1,2,3] } }
{"test": { "A": [2,1,3] } }
{"test": { "A": [1,3,2] } }
{"test": { "A": [3,2,1] } }
...
{"test": { "A": [1,2,3,4,5] } }

Invalid Traces

{"test": { "A": [2] } }
{"test": { "A": [1,3] } }
{"test": { "A": [2,3] } }
{"test": { "A": [3,3] } }
{"test": { "A": [1,2,1] } }
{"test": { "A": [1,2,2] } }
{"test": { "A": [1,2,4] } }