sys/man/1/forp

   1 .TH FORP 1
   2 .SH NAME
   3 forp \- formula prover
   4 .SH SYNOPSIS
   5 .B forp
   6 [
   7 .B -m
   8 ]
   9 [
  10 .I file
  11 ]
  12 .SH DESCRIPTION
  13 .I Forp
  14 is a tool for proving formulae involving finite-precision arithmetic.
  15 Given a formula it will attempt to find a counterexample; if it can't find one the formula has been proven correct.
  16 .PP
  17 .I Forp
  18 is invoked on an input file with the syntax as defined below.
  19 If no input file is provided, standard input is used instead.
  20 The
  21 .B -m
  22 flag instructs
  23 .I forp
  24 to produce a table of all counterexamples rather than report just one.
  25 Note that counterexamples may report bits as
  26 .BR ? ,
  27 meaning that either value will lead to a counterexample.
  28 .PP
  29 The input file consists of statements terminated by semicolons and comments using C syntax (using
  30 .B //
  31 or
  32 .B "/* */"
  33 syntax).
  34 Valid statements are
  35 .IP
  36 Variable definitions, roughly:
  37 .I type
  38 .I var
  39 .B ;
  40 .br
  41 Expressions (including assignments):
  42 .I expr
  43 .B ;
  44 .br
  45 Assertions:
  46 .B obviously
  47 .I expr
  48 .B ;
  49 .br
  50 Assumptions:
  51 .B assume
  52 .I expr
  53 .B ;
  54 .PP
  55 Assertions are formulae to be proved.
  56 If multiple assertions are given, they are effectively "and"-ed together.
  57 Each input file must have at least one assertion to be valid.
  58 Assumptions are formulae that are assumed, i.e. counterexamples that would violate assumptions are never considered.
  59 Exercise care with them, as contradictory assumptions will lead to any formula being true (the logician's principle of explosion).
  60 .PP
  61 Variables can be defined with C notation, but the only types supported are
  62 .B bit
  63 and 1D arrays of
  64 .B bit
  65 (corresponding to machine integers of the specified size).
  66 Signed integers are indicated with the keyword
  67 .BR signed .
  68 Like
  69 .B int
  70 in C, the
  71 .B bit
  72 keyword can be omitted in the presence of
  73 .BR signed .
  74 For example,
  75 .PP
  76 .EX
  77         bit a, b[4], c[8];
  78         signed bit d[3];
  79         signed e[16];
  80 .EE
  81 .PP
  82 is a set of valid declarations.
  83 .PP
  84 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.
  85 .I Forp
  86 tries to find assignments for all input variables that render the assertions invalid.
  87 .PP
  88 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.
  89 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.
  90 .TP "\w'\fL<\fR, \fL<=\fR, \fL>\fR, \fL>=\fR  'u"
  91 \fL[]\fR
  92 Array indexing. The syntax is \fIvar\fL[\fIa\fL:\fIb\fR], with \fIa\fR denoting the MSB and \fIb\fR denoting the LSB.
  93 Omiting \fL:\fIb\fR addresses a single bit.
  94 The result is always treated as unsigned.
  95 .TP
  96 \fL!\fR, \fL~\fR, \fL+\fR, \fL-\fR
  97 (Unary operators) Logical and bitwise "not", unary plus (no-op), arithmetic negation. Because of promotion, \fL~\fR and \fL-\fR operate beyond the width of variables.
  98 .TP
  99 \fL*\fR, \fL/\fR, \fL%\fR
 100 Multiplication, division, modulo.
 101 Division and modulo add an assumption that the divisor is non-zero.
 102 .TP
 103 \fL+\fR, \fL-\fR
 104 Addition, subtraction.
 105 .TP
 106 \fL<<\fR, \fL>>\fR
 107 Left shift, arithmetic right shift. Because of promotion, this is effectively a logical right shift on unsigned variables.
 108 .TP
 109 \fL<\fR, \fL<=\fR, \fL>\fR, \fL>=\fR
 110 Less than, less than or equal to, greater than, greather than or equal to.
 111 .TP
 112 \fL==\fR, \fL!=\fR
 113 Equal to, not equal to.
 114 .TP
 115 \fL&\fR
 116 Bitwise "and".
 117 .TP
 118 \fL^\fR
 119 Bitwise "xor".
 120 .TP
 121 \fL|\fR
 122 Bitwise "or".
 123 .TP
 124 \fL&&\fR
 125 Logical "and"
 126 .TP
 127 \fL||\fR
 128 Logical "or".
 129 .TP
 130 \fL<=>\fR, \fL=>\fR
 131 Logical equivalence and logical implication (equivalent to
 132 .B "(a != 0) == (b != 0)"
 133 and
 134 .BR "!a || b" ,
 135 respectively).
 136 .TP
 137 \fL?:\fR
 138 Ternary operator (\fLa?b:c\fR equals \fLb\fR if \fLa\fR is true and \fLc\fR otherwise).
 139 .TP
 140 \fL=\fR
 141 Assignment.
 142 .PP
 143 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.
 144 Note that the values reported as the counterexample are always the values given by the last assignment.
 145 .SH EXAMPLES
 146 We know that, mathematically, \fIa\fR + \fIb\fR ≥ \fIa\fR if \fIb\fR ≥ 0 (which is always true for an unsigned number).
 147 We can ask
 148 .I forp
 149 to prove this using
 150 .PP
 151 .EX
 152         bit a[32], b[32];
 153         obviously a + b >= a;
 154 .EE
 155 .PP
 156 .I Forp
 157 will report "Proved", since it cannot find a counterexample for which this is not true.
 158 In C, on the other hand, we know that this is not necessarily true.
 159 The reason is that, depending on the types involved, results are truncated.
 160 We can emulate this by writing
 161 .PP
 162 .EX
 163         bit a[32], b[32], c[32];
 164         c = a + b;
 165         obviously c >= a;
 166 .EE
 167 .PP
 168 Given this,
 169 .I forp
 170 will now report it as incorrect by providing a counterexample, for example
 171 .PP
 172 .EX
 173         a = 10000000000000000000000000000000
 174         b = 10000000000000000000000000000000
 175         c = 00000000000000000000000000000000
 176 .EE
 177 .PP
 178 Can we use \fIc\fR < \fIa\fR to check for overflow?
 179 We can ask
 180 .I forp
 181 to confirm this using
 182 .PP
 183 .EX
 184         bit a[32], b[32], c[32];
 185         c = a + b;
 186         obviously c < a <=> c != a+b;
 187 .EE
 188 .PP
 189 Here the statement to be proved is "\fIc\fR is less than \fIa\fR if and only if \fIc\fR does not equal the mathematical sum \fIa\fR + \fIb\fR (i.e. overflow has occured)".
 190 .SH SOURCE
 191 .B /sys/src/cmd/forp
 192 .SH "SEE ALSO"
 193 .IR spin (1)
 194 .SH BUGS
 195 Any proof is only as good as the assumptions made, in particular care has to be taken with respect to truncation of intermediate results.
 196 .PP
 197 Array indices must be constants.
 198 .PP
 199 Left shifting can produce a huge number of intermediate bits.
 200 .I Forp
 201 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.
 202 .SH HISTORY
 203 .I Forp
 204 first appeared in 9front in March, 2018.