Visualizing traces

The Inspector

The inspector tool, triggered by the inspect subcommand (e.g. corset inspect --trace <TRACEFILE> <CORSET FILES>), lets the user inspect an existing trace file (in JSON or gzipped JSON format) as seen by the given constraint files. It is expected to be mostly useful to debug the generation process of trace files, which are unwieldy to examine in their natural format.

Options

Usage: corset inspect [OPTIONS] --trace <TRACEFILE> [SOURCE]...

Arguments:
  [SOURCE]...  Either a file or a string containing the Corset code to process

Options:
  -T, --trace <TRACEFILE>  the trace to inspect
  -v, --verbose...         More output per occurrence
  -q, --quiet...           Less output per occurrence
      --debug              Compile code in debug mode
  -t, --threads <THREADS>  number of threads to use [default: 1]
  -h, --help               Print help
  -V, --version            Print version

The Inspector Interface

An example session: https://github.com/Consensys/corset/assets/1153808/0ceed937-40cc-49e7-a7e4-1df5c09c92c7

The inspector main interface is split in three parts. A bar at the top lists the different modules in the constraint system, which can be cycled through forward (TAB) and backward (S-TAB).

In the middle is presented a tabular view of the currently selected module trace. Each line represents a commitment, and each column a row in the trace. The table can be browsed forward and backward row-wise (`Right` and `Left`), 100 rows at a time (PgDown and PgUp), and a thousand rows at a time (S-PgDown and S-PgUp).

The third section of the screen displays ways to interact with the traces, as well as inputs, messages, and other interactive elements.

Interacting With Traces

Movement actions are a limited way to browse traces, especially when those can grow up to millions of lines long. To alleviate the difficulty of sipping through such quantity of data, the inspector provides commands to quickly move at the desired place.

Go to Row

Pressing the g key will open an input for a line number, that on validation will scroll the current module trace to the desired place. Position within a module trace is module-specific, and is remembered when switching between modules.

Filter Columns

Pressing the f key will open a dialog to filter the commitments to display, which is helpful when debugging large modules. The input expects a space-separated list of regular expressions. On validation of a correct input, only the commitments matching at least one of the filtering expressions will be displayed.

The current list of filters can be edited by pressing f once again, or cleared by pressing the F key.

Scanning columns

It may be useful to look for a location in the trace whose exact row is unknown, but that may be defined by a function of certain commitments. To this end, a rudimentary Forth-like, stack-based language is available. The instructions must form a program that reduces to a boolean expression.

The following stack elements are available:

Immediate values

may be expressed in decimal base, in hexadecimal base (if prefixed with 0x10, e.g. 0xDEADBEEF), in binary (if prefixed with 0b; e.g. 0b10010), or in opcodes (if prefixed with 0o; e.g. 0oCREATE2);

Commitments

any column from the current module can be accessed through its name;

Functions

functions operate on numeric values (immediate or from commitments) to produce a new numeric value, are available +, -, and *;

Conditions

conditions operate on numeric values and produce boolean values, are available >, >=, <, <=, and =;

Combinators

combinators operate on boolean values and create new boolean values, are available &, |, and !.

After a valid program has been entered, the matching rows, if any, are displayed at in the interactive zone, and the table view is shifted to the first one.

Examples

The first row where PC == 0x10

PC 0x10 =

Where ACC_1 equals 256 and PC is greater than 32

ACC_1 0xff = PC 0x20 > &

A PUSH32 where PC is between 20 and 50, and ACC_1 is greater than 128

INSTRUCTION 0oPUSH1 = PC 20 > & PC 50 < & ACC_1 128 > &