Documentation: Layout of BMC section.

Author: johanneskloos

doc/architectural/background-concepts.md

@@ -778,54 +778,58 @@ unsigned long fac = 1;
 Now, from the C standard and the most common C ABIs, we know that internally,
 `fac` will be represented as a binary number with 64 bits. So, if we wish to
 reason about the contents of the variable `fac`, we might as well represent it
-as a vector of 64 propositional variables, say `fac_0` to `fac_{63}`, where
-`fac = 2^{63} fac_{63} + ... + 2^0 fac_0`. We can then assert that `fac=1` using
+as a vector of 64 propositional variables, say `fac`<sub>0</sub> to
+`fac`<sub>63</sub>, where
+`fac` = 2<sup>63</sup> `fac`<sub>63</sub> + ... + 2<sup>0</sup> `fac`<sub>0</sub>.
+We can then assert that `fac`=1 using
 the propsitional formula
-`fac_{63} = 0 and ... and fac_1 = 0 and fac_0 = 1`, where we define the formula
-`A = B` as `(A and B) or ((not A) and (not B))`.
+`fac`<sub>63</sub> = 0 and ... and `fac`<sub>1</sub> = 0 and `fac`<sub>0</sub> = 1,
+where we define the formula A = B as ''(A and B) or ((not A) and (not B))''.
 
 We call this a *bit vector* representation. Compare the Wikipedia page on
 [Binary numbers](https://en.wikipedia.org/wiki/Binary_number).
 
 Bit vector representations can also be used to describe operations on binary
-numbers. For instance, suppose we have two four-bit numbers `A_3, ... A_0`
-(representing a number `A`) and `B_3, ..., B_0` (representing a number `b`)
+numbers. For instance, suppose we have two four-bit numbers A_3, ... A_0
+(representing a number A) and B_3, ..., B_0 (representing a number b)
 and wish to add them. As detailed on the page on
 [Binary adders](https://en.wikipedia.org/wiki/Adder_(electronics)),
-we define three additional bit vectors, the *carries* `C_0, ..., C_3`,
-the *partial sum* `P_0, ..., P_4` and
-the *sum* `S_0, ..., S_4` , representing a number `S` such that `S=A+B`.
+we define three additional bit vectors, the *carries* C<sub>0</sub>, ..., C<sub>3</sub>,
+the *partial sum* P<sub>0</sub>, ..., P<sub>4</sub> and
+the *sum* S<sub>0</sub>, ..., S<sub>4</sub> , representing a number S such that
+S=A+B.
 Note that the sum vector has one bit more - why? How
 is this related to arithmetic overflow in C?
 
 For convenience, we first define the *half-adder*. This is given as two
-formulas, `HA_S(A,B) = (A and not B) or (B and not A)`, which gives the
-sum of the bits `A` and `B`, and `HA_C(A,B) = A and B`, which indicates
+formulas, HA_S(A,B) = (A and not B) or (B and not A), which gives the
+sum of the bits A and B, and HA_C(A,B) = A and B, which indicates
 whether the result of the sum was too big to fit into one bit (so we carry
 a one to the next bit).
 
 Using the half-adder formulas, we can define the *full adder*, again given as
 two formulas, one for sum and the other for carry. We have
-`FA_S(A,B,C_in) = HA(HA(A,B),C_in)`, giving the sum of `A`, `B` and `C_in`,
-and `FA_C(A,B,C_in) = HA_C(A,B) or (C_in and HA_S(A,B))`, which states
+FA_S(A,B,C_in) = HA(HA(A,B),C_in), giving the sum of A, B and C_in,
+and FA_C(A,B,C_in) = HA_C(A,B) or (C_in and HA_S(A,B)), which states
 whether the result is too big to fit into a bit. Not that the full adder
 has an additional input for carries; in the following step, we will use it
 to chain the full adders together to compute the actual sum.
 
 Using the helper variables we have above, we can give the sum of the four-bit
-numbers as `C_0 = FA_C(A_0,B_0,0) and C_1 = FA_C(A_1,B_1,C_0) and
-C_2 = FA_C(A_2,B_2,C_1) and C_3 = FA_C(A_3,B_3,C_2) and
-S_0 = FA_S(A_0,B_0,0) and S_1 = FA_S(A_1,B_1,C_0) and
-and S_2 = FA_S(A_2,B_2,C_1) and S_3 = FA_S(A_3,B_3,C_2)
-and S_3 = FA_S(0,0,C_3)`.
+numbers as
+> C_0 = FA_C(A_0,B_0,0) and C_1 = FA_C(A_1,B_1,C_0) and
+> C_2 = FA_C(A_2,B_2,C_1) and C_3 = FA_C(A_3,B_3,C_2) and
+> S_0 = FA_S(A_0,B_0,0) and S_1 = FA_S(A_1,B_1,C_0) and
+> and S_2 = FA_S(A_2,B_2,C_1) and S_3 = FA_S(A_3,B_3,C_2)
+> and S_3 = FA_S(0,0,C_3).
 
 Other arithmetic operations on binary number can be expressed using propositional
 logic as well; the details can be found in the linked articles, as well
 as [Two's complement](https://en.wikipedia.org/wiki/Two%27s_complement) for
 handling signed integers and [IEEE 754](https://en.wikipedia.org/wiki/IEEE_754)
 for floating point numbers.
 
-In the following, we will simply write formulas such as `S=A+B`, with the
+In the following, we will simply write formulas such as S=A+B, with the
 understanding that this is internally represented using the appropriate bit
 vectors.
 
@@ -842,14 +846,14 @@ int sum(int a, int b)
 }
 ```
 To describe the behavior of this program, we introduce the appropriately-sized
-bit vectors `A` and `B`, and an additional helper vector `return`. The `A` and
-`B` bit vectors reflect the values of the parameters `a` and `b`, while
-`return` contains the return value of the function. As we have seen above, we
-can describe the value of `a+b` as `A+B` -- remember that this is an
+bit vectors A and B, and an additional helper vector return. The A and
+B bit vectors reflect the values of the parameters `a` and `b`, while
+return contains the return value of the function. As we have seen above, we
+can describe the value of `a+b` as A+B -- remember that this is an
 abbreviation for a moderately complex formula on bit vectors!
 
 From the semantics of the `return` instruction, we know that this program will
-return the value `a+b`, so we can describe its behavior as `return = A+B`.
+return the value `a+b`, so we can describe its behavior as return = A+B.
 
 Let us consider a slighly more complex program.
 ```C
@@ -861,7 +865,7 @@ int calculate(int x)
 }
 ```
 We again introduce several bit vectors. For the parameter `x`, we introduce a
-bit vector `X`, and for the return value, `return`. But we also have to deal
+bit vector X, and for the return value, return. But we also have to deal
 with the (local) variable `y`, which gets two assignments. Furthermore, we
 now have a program with three instructions.
 
@@ -882,15 +886,15 @@ int calculate(int x.1)
 ```
 In this form, we know that each variable is assigned to at most once.
 To capture the behavior of this program, we translate it statement-by-statement
-into a propositional formula. We introduce two bit vectors `Y1` and `Y2` to
-stand for `y.1` and `y.2` (we map `X` to `x.1` and `return` to the return
-value). `int y.1 = x.1 * x.1` becomes `Y1 = X * X`, `y.2 = y.1 + x.1` becomes
-`Y2 = Y1 + X` and `return y.2` becomes `return = Y2`.
+into a propositional formula. We introduce two bit vectors Y1 and Y2 to
+stand for `y.1` and `y.2` (we map X to `x.1` and return to the return
+value). `int y.1 = x.1 * x.1` becomes Y1 = X * X, `y.2 = y.1 + x.1` becomes
+Y2 = Y1 + X and `return y.2` becomes return = Y2.
 
 To tie the three formulas together into a description of the while program,
 we note that the three instructions form a single basic block, so we know they
 are always executed as a unit. In this case, it is sufficient to simple connect
-them with `and`: `Y1 = X * X and Y2 = Y1 + X and return = Y2`. Note that this
+them with ''and'': Y1 = X * X and Y2 = Y1 + X and return = Y2. Note that this
 propositional formula does not actually describe the order of execution of the
 statements, but simply summarizes their outcomes! Once we have non-trivial
 control flow, we have to do some extra work in this model.
@@ -908,7 +912,7 @@ int max(int a, int b)
   return result;
 }
 ```
-Bringing this into SSA form, we have the following program:
+Bringing this into SSA form, we have the following program (we write `Phi` for &Phi;):
 ```C
 int max(int a, int b)
 {
@@ -917,19 +921,19 @@ int max(int a, int b)
     result.1 = b;
   else
     result.2 = a;
-  return &Phi;(result.1,result.2);
+  return Phi(result.1,result.2);
 }
 ```
-We again introduce bit vectors `A` (for parameter `a`), `B` (for parameters `b`),
-`R1` (for `result.1`), `R2` (for `result.2`) and
-`return` (for the return value). The interesting question in this case is
+We again introduce bit vectors A (for parameter `a`), B (for parameters `b`),
+R1 (for `result.1`), R2 (for `result.2`) and
+return (for the return value). The interesting question in this case is
 how we can handle the &Phi; node: so far, it is a ''magic'' operator that selects
 the correct value.
 
 As a first step, we modify the SSA form slightly by introducing an additional
-propositional variable `C` that tracks which branch of the `if` was taken.
+propositional variable C that tracks which branch of the `if` was taken.
 We call this variabel the *code guard variable*, or *guard* for short.
-Additionally, we add `C` to the &Phi; node as a new first parameter, describing
+Additionally, we add C to the &Phi; node as a new first parameter, describing
 which input to use as a result.
 The corresponding program looks something like this:
 ```C
@@ -942,39 +946,39 @@ int max(int a, int b)
     result.1 = b;
   else
     result.2 = a;
-  return &Phi;(C,result.1,result.2);
+  return Phi(C,result.1,result.2);
 }
 ```
 For the encoding of the program, we introduce a new propositional junctor,
-&Rarr;, where `A &Rarr; B` is equivalent to `(not A) or B`. It can be understood
-as ''if `A` holds, `B` must hold as well''.
+&rArr;, where ''A &rArr; B'' is equivalent to ''(not A) or B''.
+It can be understood as ''if A holds, B must hold as well''.
 
 With these ingredients, we can encode the program. First of all, we translate
 the basic statements of the program:
-- `C = a<b` maps to `C = A<B`, for an appropriate formula `A<B`.
-- `result.1 = b` becomes `R1 = B`, and `result.2 = a` becomes `R2 = A`.
+- `C = a<b` maps to C = A&lt;B, for an appropriate formula A&lt;B.
+- `result.1 = b` becomes R1 = B, and `result.2 = a` becomes R2 = A.
 
 To handle the `if` statement, we simply make the execution of each branch
-conditional on `C` using the &Rarr; junctor:
+conditional on C using the &rArr; junctor:
 ```C
   if (C)
     result.1 = b;
   else
     result.2 = a;
 ```
-becomes `(C &Rarr; R1 = B) and ((not C) &Rarr; R2 = A)`, stating that
-the equation for the first assignment holds when `C` is true, and that for
-the second assignment holds when `C` is false.
+becomes (C &rArr; R1 = B) and ((not C) &rArr; R2 = A), stating that
+the equation for the first assignment holds when C is true, and that for
+the second assignment holds when C is false.
 
-Finally, the &Phi; node is again resolved using the &Rarr; junctor: we
+Finally, the &Phi; node is again resolved using the &rArr; junctor: we
 can encode the `return` statement as
-`(C &Rarr; return = R1) and ((not C) &Rarr; return = R2)`.
+(C &rArr; return = R1) and ((not C) &rArr; return = R2).
 
 At this point, it remains to tie the statements together; we find that we can
 again simply connect them with ''and'', since the statements are always executed
 in sequence. We get:
-`C = a<b and (C &Rarr; R1 = B) and (C &Rarr; return = R1) and
-((not C) &Rarr; R2 = A) and ((not C) &Rarr; return = R2)`.
+> C = a&lt;b and (C &rArr; R1 = B) and (C &rArr; return = R1) and
+> ((not C) &rArr; R2 = A) and ((not C) &rArr; return = R2).
 
 We can extend this approach quite straightforwardly to other constructs, but
 one obvious problem remains: We have not described how to handle loops. This
@@ -1079,48 +1083,48 @@ unsigned long factorial(unsigned n) {
         }
     }
   }
-  return &Phi(C1, &Phi(C2, &Phi(C3, fac.4, fac.3), fac.2), fac.1);
+  return Phi(C1, Phi(C2, Phi(C3, fac.4, fac.3), fac.2), fac.1);
 }
 ```
-We translate `IGNORE` into the formula `false` - this will later allow
+We translate `IGNORE` into the formula **false** - this will later allow
 us to rule out all paths that reach this point.
 
 The corresponding propositional formula can then be written as (check
 that this is equivalent to the formula you would be getting by following
 the translation procedure described above):
-```
-fac.1 = 1 and i.1 = 1 and C1 = i.1 <= n and
-((not C1) &Rarr; return = fac.1) and
-C1 &Rarr; (
-  fac.2 = fac.1 * i.1 and i.2 = i.1 + 1 and C2 = i.2 <= n and
-  ((not C2) &Rarr; return = fac.2) and
-  C2 &Rarr; (
-    fac.3 = fac.2 * i.2 and i.3 = i.2 + 1 and C3 = i.3 <= n and
-    ((not C3) &Rarr; return = fac.3) and
-    C3 &Rarr; (
-      fac.4 = fac.3 * i.3 and i.4 = i.3 + 1 and C4 = i.4 <= n and
-      ((not C4) &Rarr; return = fac.4) and
-      (C4 &Rarr; false)
-    )
-  )
-)
-```
-In the following, we reference this formula as `FA(n, result)`.
+
+> fac.1 = 1 and i.1 = 1 and C1 = i.1 &lt;= n and
+> ((not C1) &rArr; return = fac.1) and
+> C1 &rArr; (
+>>   fac.2 = fac.1 * i.1 and i.2 = i.1 + 1 and C2 = i.2 &lt;= n and
+>>   ((not C2) &rArr; return = fac.2) and
+>>   C2 &rArr; (
+>>>     fac.3 = fac.2 * i.2 and i.3 = i.2 + 1 and C3 = i.3 &lt;= n and
+>>>     ((not C3) &rArr; return = fac.3) and
+>>>     C3 &rArr; (
+>>>>       fac.4 = fac.3 * i.3 and i.4 = i.3 + 1 and C4 = i.4 &lt;= n and
+>>>>       ((not C4) &rArr; return = fac.4) and
+>>>>       (C4 &rArr; false)
+>>>     )
+>>>   )
+>> )
+
+In the following, we reference this formula as FA(n, result).
 
 At this point, we know how to encode programs as propositional formulas.
 Our goal was to reason about programs, and in particular, to check whether
 a certain property holds. Suppose, for example, that we want to check if there
 is a way that the `factorial` function returns `6`. One way to do this is to
-look at the following propositional formula: `FA(n, result) and result = 6`.
+look at the following propositional formula: FA(n, result) and result = 6.
 If this formula has a model (i.e., if we can find a satisfying assignment to
-all variables, and in particular, to `n`), we can extract the required value
+all variables, and in particular, to n), we can extract the required value
 for the parameter `n` from that model. As we have discussed above, this can
 be done using a SAT solver: If you run, say, MiniSAT on this formula, you will
-get a model involving `n=3`.
+get a model involving n=3.
 
 Be aware that this method has very clear limits: We know that the factorial of
 `5` is `120`, but with the formula above, evaluating
-`FA(n, result) and result=120` would yield ''unsatisfiable''! This is because
+''FA(n, result) and result=120'' would yield ''unsatisfiable''! This is because
 we limited the number of loop iterations, and to reach 120, we have to execute
 the loop more than three times.
 That being said, for typical CPROVER use cases, we can often make do with a