```
FORP(1)                                                   FORP(1)

NAME
forp - formula prover

SYNOPSIS
forp [ -m ] [ file ]

DESCRIPTION
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 semi-
colons and comments using C syntax (using // or /* */ syn-
tax).  Valid statements are

Variable definitions, roughly: type var ;
Expressions (including assignments): expr ;
Assertions: obviously expr ;
Assumptions: assume expr ;

Assertions are formulae to be proved.  If multiple asser-
tions are given, they are effectively "and"-ed together.
Each input file must have at least one assertion to be
valid.  Assumptions are formulae that are assumed, i.e.
counterexamples that would violate assumptions are never
considered.  Exercise care with them, as contradictory
assumptions will lead to any formula being true (the
logician's principle of explosion).

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,

bit a, b, c;
signed bit d;
signed e;

is a set of valid declarations.

Page 1                       Plan 9             (printed 4/22/21)

FORP(1)                                                   FORP(1)

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 assign-
ments 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 independently.

[]            Array indexing. The syntax is var[a:b], with a
denoting the MSB and b denoting the LSB.
Omiting :b addresses a single bit.  The result
is always treated as unsigned.

!, ~, +, -    (Unary operators) Logical and bitwise "not",
unary plus (no-op), arithmetic negation.
Because of promotion, ~ and - operate beyond
the width of variables.

*, /, %       Multiplication, division, modulo.  Division
and modulo add an assumption that the divisor
is non-zero.

+, -          Addition, subtraction.

<<, >>        Left shift, arithmetic right shift. Because of
promotion, this is effectively a logical right
shift on unsigned variables.

<, <=, >, >=  Less than, less than or equal to, greater
than, greather than or equal to.

==, !=        Equal to, not equal to.

&             Bitwise "and".

^             Bitwise "xor".

|             Bitwise "or".

&&            Logical "and"

||            Logical "or".

<=>, =>       Logical equivalence and logical implication
(equivalent to (a != 0) == (b != 0) and !a ||
b, respectively).

Page 2                       Plan 9             (printed 4/22/21)

FORP(1)                                                   FORP(1)

?:            Ternary operator (a?b:c equals b if a is true
and c otherwise).

=             Assignment.

One subtle point concerning assignments is that they forci-
bly 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 assignment.

EXAMPLES
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

bit a, b;
obviously a + b >= a;

Forp will report "Proved", since it cannot find a counterex-
ample for which this is not true.  In C, on the other hand,
we know that this is not necessarily true.  The reason is
that, depending on the types involved, results are trun-
cated.  We can emulate this by writing

bit a, b, c;
c = a + b;
obviously c >= a;

Given this, forp will now report it as incorrect by provid-
ing a counterexample, for example

a = 10000000000000000000000000000000
b = 10000000000000000000000000000000
c = 00000000000000000000000000000000

Can we use c < a to check for overflow?  We can ask forp to
confirm this using

bit a, b, c;
c = a + b;
obviously c < a <=> c != a+b;

Here the statement to be proved is "c is less than a if and
only if c does not equal the mathematical sum a + b (i.e.
overflow has occured)".

SOURCE
/sys/src/cmd/forp

SEE ALSO
spin(1)

Page 3                       Plan 9             (printed 4/22/21)

FORP(1)                                                   FORP(1)

BUGS
Any proof is only as good as the assumptions made, in par-
ticular care has to be taken with respect to truncation of
intermediate results.

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.

HISTORY
Forp first appeared in 9front in March, 2018.

Page 4                       Plan 9             (printed 4/22/21)

```