Skip to content

Commit

Permalink
feat: initial Integration of Go Corset (#907)
Browse files Browse the repository at this point in the history
This integrates `go-corset` and (when installed) runs it side-by-side
the existing Rust tool.  However, if the `go-corset` binary cannot be
found then it is simply ignored.

At this stage, `go-corset` is not enabled in the CI pipeline.  This is
because it is consuming too much memory on the test `leoFailingRange`.

Signed-off-by: David Pearce <[email protected]>
  • Loading branch information
DavePearce authored Aug 14, 2024
1 parent 973f18d commit 44e2bd3
Show file tree
Hide file tree
Showing 4 changed files with 472 additions and 210 deletions.
Original file line number Diff line number Diff line change
@@ -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<String> 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;
}
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -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 <code>corset</code> tool to check that a given trace is
Expand All @@ -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<String> 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 <code>CORSET_FLAGS</code> 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() {
Expand All @@ -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<String> buildOptions(Path filename, String zkEvmBin) {
ArrayList<String> 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 <code>CORSET_THREADS</code>.
*
* @return
*/
private String determineNumberOfThreads() {
return Optional.ofNullable(System.getenv("CORSET_THREADS")).orElse("2");
}
}
Loading

0 comments on commit 44e2bd3

Please sign in to comment.