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