WizToolKit on the Command-Line

FIREALARM (Checking and Evaluating)

FIREALARM stands for Friendly IR Evaluator And Logic Assertion and Rejection Machine, it checks and evaluates IR resources without ZK. Its intention is to be as obviously compliant with the IR Specification as possible. When given a relation, wtk-firealarm will also print gate counts before completion.

When given a single resource wtk-firealarm will checks for well-formedness. For a relation, this means that each wire is assigned before it is used, and that it is never reused ("topological ordering", and "single static assignment (SSA)"). For an instance or short witness, this simply means that each value in the stream is a field-element (e.g. does not exceed the field’s characteristic).

When given all three resources, wtk-firealarm will evaluate the relation with the instance and short witness, indicating if the proof should be valid or not (evaluation validity). It can also generate a program trace at two levels of detail.

wtk-firealarm and other WizToolKit utilities may identify resource types using the following file-suffixes. Although the IR Specification calls for all binary resources to be identified by a .sieve extension (when applicable), WizToolKit uses these suffixes instead. The IR Specification does not prescribe any file-suffixes for text resources.

`*.rel`	relation
`*.ins`	instance
`*.wit`	short witness

Command-Line Options/Flags

`-i`	Use the IRRegular text parser, instead of the ANTLR text parser.
`-f`	Use the FlatBuffer binary parser, instead of the ANTLR text parser. This option is required in order to check binary resources.
`-t`	Produces a "light" trace, showing function-boundaries, instance and witness values, and assertions. `wtk-firealarm` must be invoked with all three resources for this to take affect.
`-T`	Produces a "heavy" trace, all wire assignments, in addition to a "light" trace. `wtk-firealarm` must be invoked with all three resources for this to take affect.
`-h` or `--help`	Print the help text.
`-v` or `--version`	Print the version text.

Example Invocations

To check a relation, instance, or witness for well-formedness.

wtk-firealarm relation_file.rel
wtk-firealarm instance_file.ins
wtk-firealarm witness_file.wit

To check all three for evaluation validity.

wtk-firealarm relation_file.rel instance_file.ins witness_file.wit

To check with binary IR.

wtk-firealarm -f bin_relation_file.rel bin_instance_file.ins bin_witness_file.wit

PRESS (Format and Feature Conversion)

PRESS, as in printing-press, is short for Printing and Representation Exchange Software Suite. wtk-press is a tool for changing the format of the IR or to remove unwanted features from the IR. Press can convert between the text and binary formats of the IR, or it can replace @switch directives with a multiplexer. The multiplexer is composed with @for loops, and a @function(check_case, ….), which does have to exponentiate by p-1 when using arithmetic gates.

Command-Line Modes

wtk-press uses a <mode> <input-file> [ <output-file> ] format on its command line. Available modes are as follows. Text parsing is always done with IRRegular.

`b2b`	Binary to binary
`b2mux`	Binary to binary, with multiplex converter (if necessary)
`b2t`	Binary to text
`t2b`	Text to binary
`t2mux`	Text to text, with multiplex converter (if necessary)
`t2t`	Text to text

It also has some more testing oriented modes, which convert to nothing. Essentially they are for testing and profiling the parsers.

`a2n`	ANTLR to nothing
`b2n`	Binary to nothing
`t2n`	Text (IRRegular) to nothing

Example invocations

To convert from a text file to a binary file, or reverse.

wtk-press t2b relation_file.rel bin_relation_file.rel
wtk-press b2t bin_relation_file.rel > relation_file_copy.rel

To remove the @switch features.

wtk-press t2mux relation_file.rel relation_file_mux.rel
wtk-press b2mux bin_relation_file.rel bin_relation_file_mux.rel

Viz (Visualization)

For assistance in visualizing the IR, we came up with an IR to Graphviz converter (called wtk-viz). wtk-viz expects its input to be a relation, and produces a dot graph as output. It traverses the IR Syntax Tree, and in most cases makes a fairly naive translation into the Dot language. In the case of for-loops, wtk-viz repeats the loop scope mappings for each iteration of the loop, as it shows a better picture of the web created by repeated mappings.

Command Line Usage

wtk-viz accepts arguments in a [ options… ] <input.rel> [ <output.rel> ] form. These are the available options.

`--fg <color>`	Changes the color of nodes, edges, and text ("foreground") to the given HTML color.
`--bg <color>`	Changes the color of the background to the given HTML color.
`-f`	Use FlatBuffers to parse the binary relation (defaults to Text/IRRegular).
`-h` or --help`	Print the help text.
`-v` or --version`	Print the version information.

Example invocations

wtk-viz is invoked first to produce dot source, followed by the dot compiler to generate an image. dot invocation may take a long time for large circuits.

wtk-viz relation_file.rel relation_graph.dot
dot -Tsvg relation_graph.dot -o relation_graph.svg

BOLT (Example and Testing)

WizToolKit delivers the wtk::bolt API for implementing ZK Backends in the IR. The wtk-bolt command-line tool serves for testing this API in a non-ZK and as an example of invoking the wtk::bolt API. More information may be found in WizToolKit for Backends.

wtk::bolt implements two intepreters, BOLT for relations with heavy use of loops and PLASMASnooze for relations which are largely IR-Simple. PLASMASnooze also implements the Parser’s streaming API for additional performance when parsing IR-Simple (rather than nearly simple). Invocation is wtk-bolt [ bolt | plasmasnooze | stream ] <relation.rel> <instance.ins> <witness.wit>.