forp – formula prover|
forp [ –m ] [ file ]|
Forp is a tool for proving formulae involving finite–precision
arithmetic. Given a formula it will attempt to find a counterexample;
if it can't find one the formula has been proven correct. |
Forp is invoked on an input file with the syntax as defined below. If no input file is provided, standard input is used instead. The –m flag instructs forp to produce a table of all counterexamples rather than report just one. Note that counterexamples may report bits as ?, meaning that either value will lead to a counterexample.
The input file consists of statements terminated by semicolons
and comments using C syntax (using // or /* */ syntax). Valid
Variables can be defined with C notation, but the only types supported are bit and 1D arrays of bit (corresponding to machine integers of the specified size). Signed integers are indicated with the keyword signed. Like int in C, the bit keyword can be omitted in the presence of signed. For example,
Unlike a programming language, it is perfectly legitimate to use a variable before it is assigned value; this means the variable is an "input" variable. Forp tries to find assignments for all input variables that render the assertions invalid.
Expressions can be formed just as in C, however when used in an
expression, all variables are automatically promoted to an infinite
size signed type. The valid operators are listed below, in decreasing
precedence. Note that logical operations treat all non–zero values
as 1, whereas bitwise operators operate on all bits
One subtle point concerning assignments is that they forcibly
override any previous values, i.e. expressions use the value of
the latest assignments preceding them. Note that the values reported
as the counterexample are always the values given by the last
We know that, mathematically, a + b ≥ a if b ≥ 0 (which is always
true for an unsigned number). We can ask forp to prove this using
Any proof is only as good as the assumptions made, in particular
care has to be taken with respect to truncation of intermediate
Array indices must be constants.
Left shifting can produce a huge number of intermediate bits.
Forp will try to identify the minimum needed number but it may
be a good idea to help it by assigning the result of a left shift
to a variable.
Forp first appeared in 9front in March, 2018.|