MAN.9FRONT.ORG RTFM


     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[4], c[8];
               signed bit d[3];
               signed e[16];

          is a set of valid declarations.

     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.
                        Omitting :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, greater 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).

     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[32], b[32];
               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[32], b[32], c[32];
               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[32], b[32], c[32];
               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 occurred)".

     SOURCE
          /sys/src/cmd/forp

     SEE ALSO
          spin(1)

     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.