feat: Update `CorsetValidator` to use `-eeeeN` by Default

[DavePearce]

After investigating #158, I noticed that the CorsetValidator is not using the prime field for validation. Rather, its using big integers instead. I'm happy to be corrected, but that doesn't sound ideal to me. Specifically, you can see here in the file src/main/java/net/consensys/linea/corset/CorsetValidator.java:

public Result validate(final Path filename, final String zkEvmBin) throws Ru\
ntimeException {
    final Process corsetValidationProcess;
    try {
      corsetValidationProcess =
          new ProcessBuilder(
                  corsetBin,
                  "check",
                  "-T",
                  filename.toAbsolutePath().toString(),
                  "-q",
                  "-r",
                  "-d",
                  "-s",
                  "-t",
                  Optional.ofNullable(System.getenv("CORSET_THREADS")).orElse(\
"2"),
                  zkEvmBin)
              .redirectInput(ProcessBuilder.Redirect.INHERIT)
              .redirectErrorStream(true)
              .start();
    } catch (IOException e) {
      log.error("Corset validation has thrown an exception: %s".formatted(e.ge\
tMessage()));
      throw new RuntimeException(e);
    }

This is missing the switch -N which tells corset to use the prime field.

[DavePearce]

Just to be absolutely clear what this means. Consider this example:

(module test)
(defcolumns X)
(defconstraint notone () (vanishes! (if-eq X 1 1)))

This constraint says that X cannot be 1. Then, consider this test.trace file:

{ "test": {"X": [8444461749428370424248824938781546531375899335154063827935233455917409239042]}}

Here, the value for X should wrap around in the prime field to 1. We can see the difference between running with and without the -N switch here:

$ corset check --trace test.trace test.lisp

This passes, whilst this does not:

$ corset check -N --trace test.trace test.lisp
Error: while checking test.trace

Caused by:
    constraints failed: test.notone

Therefore, to get the most accurate validation corset should always be run with the -N switch.

[DavePearce]

I should warn, however, that we shouldn't enable validation with -N until #158 is resolved. Otherwise, stuff will definitely break!

[DavePearce]

I want to add two specific comments about this:

• We should also be using the -eeee switches and possibly also --auto-constraints nhood,sorts. These ensure the constraints are fully expanded before being checked. That gets them as close as possible to what the prover sees.
• I have now witnessed a trace generated by @ivokub that passed without the -N switch but which failed with -eeeeN. That means this problem is not theoretical.

@powerslider FYI

[DavePearce]

Some data now on test failures. Note, with the default configuration all tests pass (for the commit I was working on) in 4mins 30sec.

• -N / -eN / -eeN --- these all fail because of known bug #163.
• -eeeN --- 332 / 332 pass (in 5mins)
• -eeee --- 332 / 332 pass (in 6mins)
• -eeeeN --- 14 / 332 pass (in 6mins)
• -eeeeN --auto-constraints nhood,sorts --- 14 / 332 passed (in 21mins)

[powerslider]

Maybe we could consider adding separate testing phases corresponding to running the tests with the different expansion levels, but we need to probably migrate to bigger CI instances in order to get a reasonably fast feedback loop.