diff --git a/arithmetization/src/main/java/net/consensys/linea/corset/AbstractExecutable.java b/arithmetization/src/main/java/net/consensys/linea/corset/AbstractExecutable.java new file mode 100644 index 0000000000..c478b78ce1 --- /dev/null +++ b/arithmetization/src/main/java/net/consensys/linea/corset/AbstractExecutable.java @@ -0,0 +1,92 @@ +/* + * Copyright Consensys Software Inc. + * + * Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with + * the License. You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on + * an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the + * specific language governing permissions and limitations under the License. + * + * SPDX-License-Identifier: Apache-2.0 + */ +package net.consensys.linea.corset; + +import java.io.IOException; +import java.nio.charset.Charset; +import java.util.List; +import java.util.concurrent.TimeUnit; + +import org.apache.commons.io.IOUtils; + +public class AbstractExecutable { + protected record Outcome(int exitcode, String output, boolean timeout) {} + + /** + * Execute a system command using a given command-line, producing an exitc-code and the sysout and + * syserr streams. This operation can also timeout. + * + * @param timeout The timeout to use (in seconds). + * @param commands The command-line to use for execution. + * @return An outcome holding all the key information. + * @throws IOException If an IO error of some kind arises. + * @throws InterruptedException If the process is interrupted somehow. + */ + protected Outcome exec(int timeout, List commands) + throws IOException, InterruptedException { + return exec(timeout, commands.toArray(new String[commands.size()])); + } + + /** + * Execute a system command using a given command-line, producing an exitc-code and the sysout and + * syserr streams. This operation can also timeout. + * + * @param timeout The timeout to use (in seconds). + * @param commands The command-line to use for execution. + * @return An outcome holding all the key information. + * @throws IOException If an IO error of some kind arises. + * @throws InterruptedException If the process is interrupted somehow. + */ + protected Outcome exec(int timeout, String... commands) throws IOException, InterruptedException { + // =================================================== + // Construct the process + // =================================================== + ProcessBuilder builder = + new ProcessBuilder(commands) + .redirectInput(ProcessBuilder.Redirect.INHERIT) + .redirectErrorStream(true); + Process child = builder.start(); + try { + // Read output from child process. Note that this will include both the STDOUT and STDERR + // since (for + // simplicity) the latter is redirected above. + String output = IOUtils.toString(child.getInputStream(), Charset.defaultCharset()); + // Second, read the result whilst checking for a timeout + boolean success = child.waitFor(timeout, TimeUnit.SECONDS); + // Report everything back + return new Outcome(child.exitValue(), output, !success); + } finally { + // make sure child process is destroyed. + child.destroy(); + } + } + + /** + * Attempt to run an executable. This basically just checks it executes as expected and produces + * some output. + * + * @param binary Binary executable to try + * @return Flag indicating whether executing the given binary was successful or not. + */ + protected boolean isExecutable(String... commands) { + try { + Outcome outcome = exec(5, commands); + // Check process executed correctly, and produced some output. + return outcome.exitcode() == 0 && !outcome.output().isEmpty(); + } catch (Throwable e) { + return false; + } + } +} diff --git a/arithmetization/src/main/java/net/consensys/linea/corset/CorsetValidator.java b/arithmetization/src/main/java/net/consensys/linea/corset/CorsetValidator.java index 2d56bb824e..aa3596e7ad 100644 --- a/arithmetization/src/main/java/net/consensys/linea/corset/CorsetValidator.java +++ b/arithmetization/src/main/java/net/consensys/linea/corset/CorsetValidator.java @@ -17,18 +17,9 @@ import java.io.File; import java.io.IOException; -import java.nio.charset.Charset; -import java.nio.file.Files; import java.nio.file.Path; -import java.util.ArrayList; -import java.util.List; -import java.util.Optional; -import java.util.concurrent.TimeUnit; -import lombok.Getter; -import lombok.Setter; import lombok.extern.slf4j.Slf4j; -import org.apache.commons.io.IOUtils; /** * Responsible for running the command-line corset tool to check that a given trace is @@ -52,172 +43,67 @@ public class CorsetValidator { public record Result(boolean isValid, File traceFile, String corsetOutput) {} + /** */ private static final String ZK_EVM_RELATIVE_PATH = "/zkevm-constraints/zkevm.bin"; /** Specifies the default zkEVM.bin file to use (including its path). */ private String defaultZkEvm = null; - /** Specifies the Corset binary to use (including its path). */ - private String corsetBin; + /** Interface to existing Rust corset tool. */ + private final RustCorsetValidator rustCorset; - /** - * Specifies whether field arithmetic should be used. To best reflect the prover, this should be - * enabled. - */ - @Getter @Setter private boolean fieldArithmetic = true; - - /** - * Specifies how much expansion should be applied to constraints (max is 4). For example, - * normalisation expressions are expanded into columns containing the multiplicative inverse, etc. - * To best reflect the prover, this should be enabled. Also, the effect of this option is limited - * unless field arithmetic is also enabled. - */ - @Getter @Setter private int expansion = 4; - - /** - * Specifies whether expansion of "auto constraints" should be performed. This is the final step - * of expansion taking us to the lowest level. To best reflect the prover, this should be enabled. - * However, it is not enabled by default because this imposes a high performance overhead. - */ - @Getter @Setter private boolean autoConstraints = false; + /** Interface to Go corset tool. */ + private final GoCorsetValidator goCorset; public CorsetValidator() { - initCorset(); - configCorset(); + // Construct and initialise Rust corset. + this.rustCorset = new RustCorsetValidator(); + // Construct and initialise Go corset. + this.goCorset = new GoCorsetValidator(); + // Configure default path to the zkevm.bin file. initDefaultZkEvm(); } - public Result validate(final Path filename) throws RuntimeException { + /** + * Attempt to validate a given tracefile against a given set of zkEVM constraints. A default + * location for the zkevm.bin file is used. + * + * @param traceFile The tracefile being validated. + * @return A result which tells us whether or not the trace file was accepted, and provides + * additional information for debugging purposes. + */ + public Result validate(final Path traceFile) throws RuntimeException { if (defaultZkEvm == null) { throw new IllegalArgumentException("Default zkevm.bin not set."); } - return validate(filename, defaultZkEvm); - } - - public Result validate(final Path filename, final String zkEvmBin) throws RuntimeException { - final Process corsetValidationProcess; - try { - List options = buildOptions(filename, zkEvmBin); - corsetValidationProcess = - new ProcessBuilder(options) - .redirectInput(ProcessBuilder.Redirect.INHERIT) - .redirectErrorStream(true) - .start(); - } catch (IOException e) { - log.error("Corset validation has thrown an exception: %s".formatted(e.getMessage())); - throw new RuntimeException(e); - } - - final String corsetOutput; - try { - corsetOutput = - IOUtils.toString(corsetValidationProcess.getInputStream(), Charset.defaultCharset()); - } catch (IOException e) { - log.error( - "Error while catching output corsetValidationProcess: %s".formatted(e.getMessage())); - throw new RuntimeException(e); - } - - try { - corsetValidationProcess.waitFor(5, TimeUnit.SECONDS); - } catch (InterruptedException e) { - log.error("Timeout while validating trace file: %s".formatted(e.getMessage())); - throw new RuntimeException(e); - } - - if (corsetValidationProcess.exitValue() != 0) { - log.error("Validation failed: %s".formatted(corsetOutput)); - return new Result(false, filename.toFile(), corsetOutput); - } - - return new Result(true, filename.toFile(), corsetOutput); - } - - private void initCorset() { - final Process whichCorsetProcess; - - try { - whichCorsetProcess = Runtime.getRuntime().exec(new String[] {"which", "corset"}); - } catch (IOException e) { - log.error("Error while searching for corset: %s".formatted(e.getMessage())); - throw new RuntimeException(e); - } - - final String whichCorsetProcessOutput; - try { - whichCorsetProcessOutput = - IOUtils.toString(whichCorsetProcess.getInputStream(), Charset.defaultCharset()); - } catch (IOException e) { - log.error("Error while catching output whichCorsetProcess: %s".formatted(e.getMessage())); - throw new RuntimeException(e); - } - - try { - whichCorsetProcess.waitFor(5, TimeUnit.SECONDS); - } catch (InterruptedException e) { - log.error("Timeout while searching for corset: %s".formatted(e.getMessage())); - throw new RuntimeException(e); - } - - if (whichCorsetProcess.exitValue() == 0) { - corsetBin = whichCorsetProcessOutput.trim(); - return; - } - - log.warn("Could not find corset executable: %s".formatted(whichCorsetProcessOutput)); - - final String homePath = System.getenv("HOME"); - corsetBin = homePath + "/.cargo/bin/corset"; - log.warn("Trying to use default corset path: %s".formatted(corsetBin)); - - if (!Files.isExecutable(Path.of(corsetBin))) { - throw new RuntimeException("Corset is not executable: %s".formatted(corsetBin)); - } + return validate(traceFile, defaultZkEvm); } /** - * Configure corset from the CORSET_FLAGS environment variable (if set). If the - * environment variable is not set, the default configuration is retained. If the environment - * variable is set, but its value is malformed then an exception is raised. + * Attempt to validate a given tracefile against a given set of zkEVM constraints. + * + * @param traceFile The tracefile being validated. + * @param zkEvmBin The zkEVM constraints file (compiled using corset). + * @return A result which tells us whether or not the trace file was accepted, and provides + * additional information for debugging purposes. */ - private void configCorset() { - String flags = System.getenv().get("CORSET_FLAGS"); - if (flags != null) { - log.info( - "Configuring corset from CORSET_FLAGS environment variable: \"%s\"".formatted(flags)); - // Reset default configuration - this.fieldArithmetic = false; - this.expansion = 0; - this.autoConstraints = false; - // Check for default case (empty string) - if (!flags.isEmpty()) { - // split flags by separator - String[] splitFlags = flags.split(","); - // Build configuration based on flags - for (String flag : splitFlags) { - switch (flag) { - case "fields": - this.fieldArithmetic = true; - break; - case "expand": - if (expansion >= 4) { - throw new RuntimeException( - ("Malformed Corset configuration flags (expansion " - + "beyond four meaningless): %s") - .formatted(flags)); - } - this.expansion++; - break; - case "auto": - this.autoConstraints = true; - break; - default: - // Error - throw new RuntimeException("Unknown Corset configuration flag: %s".formatted(flag)); - } - } + public Result validate(final Path traceFile, final String zkEvmBin) { + // Sanity check at least one validator is active + if (!rustCorset.isActive() && !goCorset.isActive()) { + throw new RuntimeException("Neither corset nor go-corset are available"); + } + // First, generate "official" result from Rust tool + Result rr = rustCorset.validate(traceFile, zkEvmBin); + Result rg = goCorset.validate(traceFile, zkEvmBin); + // Second, validate this against Go tool + if (rg != null && rg.isValid() != rr.isValid()) { + log.info("Output from Rust and Go tools differs ({} v {})", rr.isValid(), rg.isValid()); + if (!rg.isValid()) { + return rg; } } + // + return rr; } private void initDefaultZkEvm() { @@ -244,59 +130,4 @@ private void initDefaultZkEvm() { log.warn("Could not find default path for zkevm.bin"); } - - /** - * Construct the list of options to be used when running Corset. - * - * @return - */ - private List buildOptions(Path filename, String zkEvmBin) { - ArrayList options = new ArrayList<>(); - // Specify corset binary - options.add(corsetBin); - // Specify corset "check" command. - options.add("check"); - // Specify corset trace file to use - options.add("-T"); - options.add(filename.toAbsolutePath().toString()); - // Specify reporting options where: - // - // -q Decrease logging verbosity - // -r detail failing constraint - // -d dim unimportant expressions for failing constraints - // -s display original source along with compiled form - options.add("-qrds"); - // Enable field arithmetic (if applicable) - if (fieldArithmetic) { - options.add("-N"); - } - // Enable expansion (if applicable) - if (expansion != 0) { - String es = "e".repeat(expansion); - options.add("-" + es); - } - // Enable auto constraints (if applicable) - if (autoConstraints) { - options.add("--auto-constraints"); - options.add("nhood,sorts"); - } - // Specify number of threads to use. - options.add("-t"); - options.add(determineNumberOfThreads()); - // Specify the zkevm.bin file. - options.add(zkEvmBin); - log.info("Corset options: " + options); - // Done - return options; - } - - /** - * Determine the number of threads to use when checking constraints. The default is "2", but this - * can be overriden using an environment variable CORSET_THREADS. - * - * @return - */ - private String determineNumberOfThreads() { - return Optional.ofNullable(System.getenv("CORSET_THREADS")).orElse("2"); - } } diff --git a/arithmetization/src/main/java/net/consensys/linea/corset/GoCorsetValidator.java b/arithmetization/src/main/java/net/consensys/linea/corset/GoCorsetValidator.java new file mode 100644 index 0000000000..8132a33556 --- /dev/null +++ b/arithmetization/src/main/java/net/consensys/linea/corset/GoCorsetValidator.java @@ -0,0 +1,111 @@ +/* + * Copyright Consensys Software Inc. + * + * Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with + * the License. You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on + * an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the + * specific language governing permissions and limitations under the License. + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package net.consensys.linea.corset; + +import java.nio.file.Path; +import java.util.ArrayList; +import java.util.List; + +import lombok.Getter; +import lombok.extern.slf4j.Slf4j; +import net.consensys.linea.corset.CorsetValidator.Result; + +/** + * Responsible for running the command-line go-corset tool to check that a given trace + * is accepted by the zkevm constraints. The corset tool has three IR levels at which + * it can do this (HIR/MIR/AIR). The lowest level (AIR) provides the most accurate results (i.e. + * most comparable with prover). + * + *

The configuration can be set using the environment variable GO_CORSET_FLAGS. If + * this is not set, then this validator will not be activated. . + */ +@Slf4j +public class GoCorsetValidator extends AbstractExecutable { + /** Indicates whether or not this validator is active (i.e. we located the go-corset binary). */ + @Getter private boolean active = false; + + public GoCorsetValidator() { + configGoCorset(); + } + + /** + * Attempt to validate a given trace against a given zkEvmBin file. + * + * @param traceFile Path to the trace file being validated. + * @param zkEvmBin Path to the zkEvmBin file being validated. + * @return A result which tells us whether or not the trace file was accepted, and provides + * additional information for debugging purposes. + */ + public Result validate(final Path traceFile, final String zkEvmBin) { + if (active) { + Outcome outcome; + try { + List commands = buildCommandLine(traceFile, zkEvmBin); + log.debug("{}", commands); + // Execute corset with a 5s timeout. + outcome = super.exec(5, commands); + } catch (Throwable e) { + log.error("Corset validation has thrown an exception: %s".formatted(e.getMessage())); + throw new RuntimeException(e); + } + // Check for success or failure + if (outcome.exitcode() != 0) { + log.error("Validation failed: %s".formatted(outcome.output())); + return new Result(false, traceFile.toFile(), outcome.output()); + } + // success! + return new Result(true, traceFile.toFile(), outcome.output()); + } + // Tool is not active + log.debug("(inactive)"); + return null; + } + + /** + * Configure corset from the CORSET_FLAGS environment variable (if set). If the + * environment variable is not set, the default configuration is retained. If the environment + * variable is set, but its value is malformed then an exception is raised. + */ + private void configGoCorset() { + // If we can execute go-corset then use it! + this.active = super.isExecutable("go-corset", "--help"); + } + + /** + * Construct the command-line to use for running corset to check a given trace file is accepted + * (or not) by a given bin file. Amongst other things, this will configure the command-line flags + * as dictated by the CORSET_FLAGS environment variable. + * + * @return + */ + private List buildCommandLine(Path traceFile, String zkEvmBin) { + ArrayList options = new ArrayList<>(); + // Specify corset binary + options.add("go-corset"); + // Specify corset "check" command. + options.add("check"); + // -w Report non-critical errors as warnings. + options.add("-w"); + // Perform validation at AIR level only. + options.add("--air"); + // Specify trace file to use + options.add(traceFile.toAbsolutePath().toString()); + // Specify the zkevm.bin file. + options.add(zkEvmBin); + // Done + return options; + } +} diff --git a/arithmetization/src/main/java/net/consensys/linea/corset/RustCorsetValidator.java b/arithmetization/src/main/java/net/consensys/linea/corset/RustCorsetValidator.java new file mode 100644 index 0000000000..8efe2d1ca9 --- /dev/null +++ b/arithmetization/src/main/java/net/consensys/linea/corset/RustCorsetValidator.java @@ -0,0 +1,228 @@ +/* + * Copyright Consensys Software Inc. + * + * Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with + * the License. You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on + * an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the + * specific language governing permissions and limitations under the License. + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package net.consensys.linea.corset; + +import java.nio.file.Path; +import java.util.ArrayList; +import java.util.List; +import java.util.Optional; + +import lombok.Getter; +import lombok.Setter; +import lombok.extern.slf4j.Slf4j; +import net.consensys.linea.corset.CorsetValidator.Result; + +/** + * Responsible for running the command-line corset tool to check that a given trace is + * accepted by the zkevm constraints. The corset tool has variables levels of + * "expansion" which it can apply before performing the check. Greater levels of expansion imply + * more accurate checks (i.e. more realistic compared to the prover). Furthermore, corset + * can be configured to use field arithmetic or simply big integers (with the latter option + * intended to offer faster but much less precise checking). The default configuration is set to + * give good accuracy, but without significant overhead. A greater level can be configured by + * enabling the autoConstraints. + * + *

The configuration can be set using the environment variable CORSET_FLAGS. Example + * values for this environment variable include fields,expand (sets + * fieldArithmetic=true and expansion=0) and fields,expand,expand, + * auto (enables fieldArithmetic and autoConstraints and sets + * expansion=2). Note, it doesn't make sense to have expand without + * fields. Likewise, it doesn't make sense to have auto without expand + * . + */ +@Slf4j +public class RustCorsetValidator extends AbstractExecutable { + /** Specifies the Corset binary to use (including its path). */ + private String corsetBin; + + /** + * Specifies whether field arithmetic should be used. To best reflect the prover, this should be + * enabled. + */ + @Getter @Setter private boolean fieldArithmetic = true; + + /** + * Specifies how much expansion should be applied to constraints (max is 4). For example, + * normalisation expressions are expanded into columns containing the multiplicative inverse, etc. + * To best reflect the prover, this should be enabled. Also, the effect of this option is limited + * unless field arithmetic is also enabled. + */ + @Getter @Setter private int expansion = 4; + + /** + * Specifies whether expansion of "auto constraints" should be performed. This is the final step + * of expansion taking us to the lowest level. To best reflect the prover, this should be enabled. + * However, it is not enabled by default because this imposes a high performance overhead. + */ + @Getter @Setter private boolean autoConstraints = false; + + /** Indicates whether or not this validator is active (i.e. we located the corset binary). */ + @Getter private boolean active = false; + + public RustCorsetValidator() { + initCorset(); + configCorset(); + } + + /** + * Attempt to validate a given trace against a given zkEvmBin file. + * + * @param traceFile Path to the trace file being validated. + * @param zkEvmBin Path to the zkEvmBin file being validated. + * @return A result which tells us whether or not the trace file was accepted, and provides + * additional information for debugging purposes. + */ + public Result validate(final Path traceFile, final String zkEvmBin) { + Outcome outcome; + try { + List commands = buildCommandLine(traceFile, zkEvmBin); + log.debug("{}", commands); + // Execute corset with a 5s timeout. + outcome = super.exec(5, commands); + } catch (Throwable e) { + log.error("Corset validation has thrown an exception: %s".formatted(e.getMessage())); + throw new RuntimeException(e); + } + // Check for success or failure + if (outcome.exitcode() != 0) { + log.error("Validation failed: %s".formatted(outcome.output())); + return new Result(false, traceFile.toFile(), outcome.output()); + } + // success! + return new Result(true, traceFile.toFile(), outcome.output()); + } + + /** + * Attempt to locate the corset executable. Ideally, this is on the PATH and works out-of-the-box. + * However, this will fall back to a default location (based on where Cargo normally places + * binaries) if that is not the case. + */ + private void initCorset() { + // Try default + if (isExecutable("corset", "--version")) { + corsetBin = "corset"; + active = true; + } else { + // Try fall back + final String homePath = System.getenv("HOME"); + corsetBin = homePath + "/.cargo/bin/corset"; + log.warn("Trying to use default corset path: %s".formatted(corsetBin)); + // Sanity check we can execute it + active = isExecutable(corsetBin, "--version"); + } + } + + /** + * Configure corset from the CORSET_FLAGS environment variable (if set). If the + * environment variable is not set, the default configuration is retained. If the environment + * variable is set, but its value is malformed then an exception is raised. + */ + private void configCorset() { + String flags = System.getenv().get("CORSET_FLAGS"); + if (flags != null) { + log.info( + "Configuring corset from CORSET_FLAGS environment variable: \"%s\"".formatted(flags)); + // Reset default configuration + this.fieldArithmetic = false; + this.expansion = 0; + this.autoConstraints = false; + // Check for default case (empty string) + if (!flags.isEmpty()) { + // split flags by separator + String[] splitFlags = flags.split(","); + // Build configuration based on flags + for (String flag : splitFlags) { + switch (flag) { + case "fields": + this.fieldArithmetic = true; + break; + case "expand": + if (expansion >= 4) { + throw new RuntimeException( + ("Malformed Corset configuration flags (expansion " + + "beyond four meaningless): %s") + .formatted(flags)); + } + this.expansion++; + break; + case "auto": + this.autoConstraints = true; + break; + default: + // Error + throw new RuntimeException("Unknown Corset configuration flag: %s".formatted(flag)); + } + } + } + } + } + + /** + * Construct the command-line to use for running corset to check a given trace file is accepted + * (or not) by a given bin file. Amongst other things, this will configure the command-line flags + * as dictated by the CORSET_FLAGS environment variable. + * + * @return + */ + private List buildCommandLine(Path traceFile, String zkEvmBin) { + List options = new ArrayList<>(); + // Specify corset binary + options.add(corsetBin); + // Specify corset "check" command. + options.add("check"); + // Specify corset trace file to use + options.add("-T"); + options.add(traceFile.toAbsolutePath().toString()); + // Specify reporting options where: + // + // -q Decrease logging verbosity + // -r detail failing constraint + // -d dim unimportant expressions for failing constraints + // -s display original source along with compiled form + options.add("-qrds"); + // Enable field arithmetic (if applicable) + if (fieldArithmetic) { + options.add("-N"); + } + // Enable expansion (if applicable) + if (expansion != 0) { + String es = "e".repeat(expansion); + options.add("-" + es); + } + // Enable auto constraints (if applicable) + if (autoConstraints) { + options.add("--auto-constraints"); + options.add("nhood,sorts"); + } + // Specify number of threads to use. + options.add("-t"); + options.add(determineNumberOfThreads()); + // Specify the zkevm.bin file. + options.add(zkEvmBin); + // Done + return options; + } + + /** + * Determine the number of threads to use when checking constraints. The default is "2", but this + * can be overriden using an environment variable CORSET_THREADS. + * + * @return + */ + private String determineNumberOfThreads() { + return Optional.ofNullable(System.getenv("CORSET_THREADS")).orElse("2"); + } +}