Important Aspects of C626
(preparation for final exam)

• In all important computer protocols, software, systems, and so on, execution entails a trajectory through a state-space: a current state represents the history of execution from an initial state up to the current state; the next state in the execution is a function of the current state and the values of any input variables that may be a part of the definition of the system, and the collection of all reachable states from a given initial state is the state-space.

• State is embodied as the values of a collection of variables and data structures.

• A free variable is a variable that has no binding to a quantifier. In the following:
```      ∀x x2+x+1 = y
```
variable x is bound and y is free.

• ACL2 is an interactive, first order logic theorem prover. ACL2 is much more powerful than Satisfiability methods discussed elsewhere because it employs induction and rewrite rules in addition to BDD and SAT theorem proving methods. Induction allows ACL2 to prove theorems on structures of any size. However, it is frequently the case that a more general theorem must be proved first, then strengthened to get the desired theorem. Knowing what generalizations to prove is a difficult task that requires significant expertise.

For example, consider the pigeon-hole problem (which is difficult for bare-bones resolution-based theorem provers:

Given: n pigeon holes and n+1 pigeons,
Prove: it is not possible to put pigeons in holes so that every hole has at most one pigeon.

By the way, pigeon holes do not have anything to do with pigeons, except maybe carrier pigeons - how this problem came to be thought of as placing birds in holes is a mystery to me.

Start with a representation of the problem that is easy to work with. Lists are easy to work with in ACL2 so we choose to use a list of dimension n where each element represents a hole and contains a non-negative integer which expresses the number of pigeons assigned to that hole. Call the list lst. The total number of holes is (len lst). The total number of pigeons is the sum of all elements in lst. This can be calculated with a defun such as the following:

```   (defun sum-list (l)
(if (endp l)
0
(+ (car l) (sum-list (cdr l)))))
```
We can relate (sum-list lst) to (len lst) but to completely answer the question at hand we need to ensure that no hole has more than one pigeon. This can be done with the following procedure that returns T if and only if this condition is satisfied:
```   (defun posn-one-listp (l)
(if (endp l)
t
(if (or (equal 0 (car l)) (equal (car l) 1))
(posn-one-listp (cdr l))
nil)))
```
The following theorems prove that posn-one-listp does what it is supposed to do:
```   (thm (implies (and (posn-one-listp l) (member x l)) (< x 2)))
(thm (implies (and (posn-one-listp l) (member x l)) (natp x)))
(thm (implies (and (posn-one-listp l) (member x l)) (<= 0 x)))
```
We are ready to prove the pigeon-hole principle:
```   (defthm attempted-pigeon-hole-violation
(implies
(and (< 0 n) (equal (len l) n) (equal (+ n 1) (sum-list l)))
(not (posn-one-listp l))))
```
But this does not prove. So we generalize:
```   (defthm pigeon-hole-violation-proved
(implies
(and (< 0 (len l)) (< (len l) (sum-list l)))
(not (posn-one-listp l))))
```
```   (defthm attempted-pigeon-hole-violation-now-proves
(implies
(and (< 0 n) (equal (len l) n) (equal (+ n 1) (sum-list l)))
(not (posn-one-listp l))))
```
which now proves. Observe that generalization was necessary to get the weakest precondition at the entry point of Legato's multiplier to prove in ACL2 (check the notes - "proof that Mostek code multiplies").

• ACL2 provides copious feedback to help the user develop lemmas which will eventually allow the theorems of interest to prove. We the example of checking whether two lists are permutations to illustrate. The following is code for this problem - it returns T if and only if the two inputs lists are permutations:
```   (defun perm (x y)
(if (endp x)
(endp y)
(if (member (car x) y)
(perm (cdr x) (remove1 (car x) y))
nil)))
```
We want to prove the following theorem:
```   (defthm perm-transitive
(implies (and (perm x y) (perm y z)) (perm x z)))
```
but the proof fails at two points, one of which generates the following:
```   (IMPLIES (AND (CONSP X)
(NOT (MEMBER (CAR X) Z))              <- These two are
(MEMBER (CAR X) Y)                    <- enough to prove
(PERM (CDR X) (REMOVE1 (CAR X) Y)))
(NOT (PERM Y Z)))                          <= this
```
ACL2 is telling us that it could not prove the above. A user might notice that only part of the hypothesis is needed to imply the conclusion - in this case the part of the hypothesis needed consists of the 2nd and 3rd lines. So the user may attempt to prove an auxilliary theorem such as the following:
```   (defthm perm-member
(implies (and (perm x z) (member e x)) (member e z)))
```
Observe that this is looking at the contrapositive: if the conclusion is false and one of the two hypothesis lines is true, then the other hypothesis line, and therefore the entire hypothesis, must be false. But this fails with this:
```   (IMPLIES (AND (CONSP X)
(NOT (EQUAL E (CAR X)))              <- as long as this holds
(MEMBER E (REMOVE1 (CAR X) Z))       <= this is equivalent
(MEMBER (CAR X) Z)
(PERM (CDR X) (REMOVE1 (CAR X) Z))
(MEMBER E (CDR X)))
(MEMBER E Z))                             <= to this
```
The user may notice that as long as line 2 holds, then lines 3 and 7 are equivalent. Hence the following theorem is tried:
```   (defthm member-remove1
(implies (not (equal e d))
(iff (member e (remove1 d z)) (member e z))))
```
This proves. Retrying, perm-member also proves. Retrying, perm-transitive fails at only one point - which is displayed as this:
```   (IMPLIES (AND (CONSP X)
(NOT (PERM (REMOVE1 (CAR X) Y)       <= imply this is false
(REMOVE1 (CAR X) Z)))
(MEMBER (CAR X) Y)
<- this and two down
(PERM (CDR X) (REMOVE1 (CAR X) Y))
(PERM Y Z))                          <- here
(PERM (CDR X) (REMOVE1 (CAR X) Z)))
```
The user discovers that the hypothesis is always false because lines 4 and 6 imply lines 2/3 is false. A theorem to show this is as follows:
```   (defthm perm-remove1-remove1
(implies (and (member e y) (perm y z))
(perm (remove1 e y) (remove1 e z))))
```
But this fails with the following:
```   (IMPLIES (AND (CONSP Y)
(PERM (REMOVE1 E (CDR Y))
(REMOVE1 E (REMOVE1 (CAR Y) Z)))
(MEMBER E (CDR Y))
(MEMBER (CAR Y) Z)
(PERM (CDR Y) (REMOVE1 (CAR Y) Z))
(NOT (EQUAL E (CAR Y))))
(PERM (REMOVE1 E (CDR Y))
(REMOVE1 (CAR Y) (REMOVE1 E Z))))
```
Lines 3 and 9 should be equal because the order of removal should not matter. This is expressed as the following:
```   (defthm remove1-remove1
(equal (remove1 e (remove1 d x))
(remove1 d (remove1 e x))))
```
which proves. Retrying, perm-remove1-remove1 proves. Retyring, perm-transitive proves and this is what was desired in the first place.

• Floyd-Hoare logic is a formal system for proving correctness of protocols, software, or any other computer system that manipulates state. With respect to software, execution of instructions results in state changes. Hoare logic follows state changes through triples:
```      {P} C {Q}
```
where P is an assertion about the state before the execution of line or code segment C and Q is an assertion about the state after execution of C. We call P a precondition for C and it is consistent with the postcondition Q and the semantics of C.

Examples:

```      {P} nop {P}
{a == 1, a != b} b := 2 {a == 1, a != b}
{b == 20} a := b+1 {a > 1}
{b > 10} a := b+1 {a > 1}
{b > 0} a := b+1 {a > 1}
```
The last one is the weakest precondition for a := b+1; that is consistent with the postcondition a > 1. Formally,

 The weakest precondition for code segment C with respect to postcondition Q is a predicate that is true for precisely those initial states in which C must terminate and produce a state satisfying Q.

More Examples:

```      {b > 10} a := b+1 {a > 0}
{b > 10} a := b+1 {a > 11}
```
The last one is the strongest postcondition for a := b+1 that is consistent with the precondition b > 10. Formally,

 The strongest postcondition for code segment C with respect to precondition P is a predicate that is implied by P when acted upon by C.

Note: There is a peculiar asymmetry in the above definitions - we require termination for weakest preconditions but not for strongest postconditions.

Another Example:

```      {x < 10 ∧ x ≤ 10} while (x < 10) x := x+1 {¬(x < 10) ∧ x ≤ 10}
```
This demonstates a loop invariant. Formally,

 A loop invariant for a loop C is a collection of assertions on state entering C and guaranteed to be true at every iteration of the loop. The invariant is the postcondition for C on exit from C.

The loop invariant for the loop above could be written x < 10 but the reason for using x < 10 ∧ x ≤ 10 will be made clear later.

Basic rules of Floyd-Hoare logic:

• In the following [E/x] means substitute the expression E for free variable x.

• Assignment:
```      ---------------------
{Q[E/x]} x := E; {Q}
```
Example:
In {y == 10} x := y+1; {x == 11}
Q = {x == 11}
[E/x] = [(y + 1)/x] = {y+1}
Q[E/x] = {y+1 == 11} = {y == 10}

• Composition:
```      {P} C1 {R}, {R} C2 {Q}
----------------------
{P} C1; C2 {Q}
```
Example:
Given
{y == 10} x := y+1 {x == 11} and
{x == 11} z := x+1 {z == 12}
We can substitute
{y == 10} x := y+1; z := x+1 {z == 12}

• Condition:
```      {A ∧ B} C1 {Q}, {¬A ∧ B} C2 {Q}
-------------------------------
{B} if A then C1 else C2 {Q}
```
Example:
Given
{a==T ∧ b==6 ∧ c==10} x := b; {(x==6 ∧ a==T) ∨ (x==10 ∧ a==F)} and
{a==F ∧ b==6 ∧ c==10} x := c; {(x==6 ∧ a==T) ∨ (x==10 ∧ a==F)}
We can substitute
{(b==6 ∧ c==10)} if a==T then x := b; else x := c; {(x==6 ∧ a==T) ∨ (x==10 ∧ a==F)}

• Consequence:
```      P' → P, {P} C {Q}, Q' → Q
-------------------------
{P'} C {Q'}
```
Example:
Starting with:
{P} = {x+1==10} y := x+1; {y==10} = {Q}
and
P' = (x==9 → x+1==10),
Q' = (x==9 ∧ y==10 → y==10),
We can substitute
{x==9} y := x+1; {x==9 ∧ y==10}

• While:
```            {Q ∧ A} C {Q}
-------------------------
{Q} while A do C {¬A ∧ Q}
```
Example:
Starting with:
{x < 10 ∧ x ≤ 10} x = x+1; {x ≤ 10}
After application of the while rule:
{x ≤ 10} while(x < 10) x = x+1; {¬(x < 10) ∧ x ≤ 10}
After application of the cconsequence rule:
{x ≤ 10} while(x < 10) x = x+1; {x==10}

• Weakest Preconditions - a predicate transformer.

Important: By definition, if Q is a predicate that expresses a query about some property a program has at some point, a weakest precondition P at the entry point of the program expresses all initial conditions that may lead to satisfying Q through some execution path through the state-space of the program. If a weakest precondition exists at the entry point, the Q can be satisfied. If one can show that another predicate P' implies P, then P' also implies Q for some execution path to Q.

Notation: wp(C,Q) - the weakest precondition for code segment C with respect to postcondition predicate Q.

Example:
wp(a := b+1, a > 11) = b > 10

Reason for weakest preconditions: supports the implementation of an effective process for transforming Floyd-Hoare logic to predicate logic. In that context, one can employ ACL2 to prove properties about code.

Weakest precondition rules:

• NOP:
wp(NOP,Q) = Q
• Abort:
wp(Abort,Q) = False
• Assignment:
wp(x := E;, Q) = Q[E/x]
ex:  wp(x := x+1, x > 10) = x+1 > 10 ⇔ x > 9
• Composition:
wp(C1; C2,Q) = wp(C1, wp(C2,Q))
ex:     wp(x := x+2; y := y−2, x+y == 0)
= wp(x := x+2, wp(y := y−2, x+y == 0))
= wp(x := x+2, x+(y−2) == 0)
= (x+2 + (y−2)) == 0
= x+y == 0
• Condition:
wp(if E then C1 else C2, Q) = (E → wp(C1, Q)) ∧ (¬E → wp(C2, Q)))
ex:     wp(if x > 2 then y := 1 else y := −1, (y > 0))
= ((x > 2) → wp(y := 1, (y > 0))) ∧ (¬(x > 2) → wp(y := −1, (y > 0)))
= ((x > 2) → (1 > 0)) ∧ (¬(x > 2) → (−1 > 0))
= ((x > 2) → T) ∧ (¬(x > 2) → F))
= ((x > 2) → T) ∧ ((x > 2) ∨ F))
= (x > 2)
• While:
wp(while E do C, Q) = ∃k. (k ≥ 0) ∧ Pk where
P0 = ¬E ∧ Q and
Pk+1 = E ∧ wp(C, Pk)
ex:   wp(while n > 0 do n := n − 1, n == 0)
P0 = ¬(n > 0) ∧ (n == 0) = (n == 0)
P1 = (n > 0) ∧ wp(n := n−1, (n == 0)) = (n == 1)
P2 = (n > 0) ∧ wp(n := n−1, (n == 1)) = (n == 2)
∃k. (k ≥ 0) ∧ Pk = (n >= 0)
ex:
```      {(n ≥ 0)}
i := 0;
s := 0;
while i != n do
i := i+1;
s := s + (2*i - 1);
end
{(s == n*n)}

P0 = ((i == n) ∧ (s == n∗n))
P1 = ((i == n−1) ∧ (s == i∗i))
P2 = ((i == n-2) ∧ (s == i∗i))
...
Pj = ((i == n−j) ∧ (s == i∗i)
...
wp(while..., (s == n∗n)) = ((i ≤ n) ∧ (s == i∗i)
```
Useful special cases:
• wp(C, Q) = T   C terminates with Q from any initial state
• wp(C, T) = T   C terminates from any initial state
• wp(C, T) = F   C does not terminate from any initial state

Example: Legato's Mostek 6502 8-bit multiplier.
 See last two pages of homework 4 for an example See for all the weakest preconditions at important points of the code The theorem to prove is the following:

```      (defthm legatoIsCorrect
(implies (and (equal f1save f1)
(natp f2)
(< f2 256)
(natp f1)
(< f1 256)
(natp low)
(< low 256)
(natp c))
(wp-1 f2 f1 c low f1save)))
```
 But this won't prove (easily) unless a more general version of the weakest preconditions are supplied and proved. Details are here.

• A Formal Model is a logic expression that describes in whole or in part the behavior of some aspect of the operation of a protocol, software, circuit, or system. That is, a legal state transition or series of transitions will cause the expression to have value True and forbidden transitions will cause it to have value False. A predicate may be added to a formal model to determine the validity of some query that might be made about the system under study. Also, the functional equivalence of two formal models may be checked to prove, for example, that an implementation (one formal model) matches a specification (the other formal model).

Before the midterm exam we used CNF formulas and even first order logic structures as formal models. In the second half of the course we have used and-inverter graphs (AIG).

• An And-Inverter Graph is a canonical representation of a Boolean function as a graphical abstraction of a circuit consisting only of 2-input 'and' gates and inverters. In this abstraction vertices represent the 'and' gates. The edges may be directed, in which case outgoing edges represent signal flow out of a gate and incoming edges represent inputs to a gate. There can only be at most 2 incoming edges to a vertex but there can be many outgoing edges. A white circle may be place over any edge to represent an inverter- then the signal at the incoming end is opposite in value to the signal at the outgoing end.

AIGs may be used to define specifications and implementations as formal models.

There is no problem representing a logical entity with no state as an AIG. If the entity has state, some unrolling of possible execution cycles may be needed to build the appropriate AIG.

• A Mitre Circuit is used to check the functional equivalence of two formal models. Let φ1(x,y,...) and φ2(x,y,...) be two Boolean functions with the same arguments. The mitre circuit φ1(x,y,...) ⊕ φ2(x,y,...) is False for all inputs if and only if both functions are equivalent. For a collection φ1,1(...), φ1,2(...), φ2,1(...), ... , φk,1(...), φk,2(...) of Boolean functions, φi,1(...) is equivalent to φi,2(...) for all 1≤i≤k if and only if the mitre  (φ11(...) ⊕ φ12(...)) ∨ (φ21(...) ⊕ φ22(...)) ∨ ... ∨ (φ21(...) ⊕ φ22(...))
is unsatisfiable.

• A theorem may be proved by checking the equivalence of the formal model that corresponds to the theorem against the formal model that corresponds to True.

• One way to perform an equivalence check is to apply a SAT solver directly.

• But, it is often better to apply a SAT solver incrementally. This is accomplished as follows, given two AIGs, alternately run some random truth assignments on both circuits and collect statistics showing possible vertex equivalences (that is, the value at a vertex in one AIG matched the value at a vertex in the other AIG for all random inputs). Then use a SAT solver to prove the vertices represent equivalent functions and, if so, collapse the two graphs at that vertex. This process proceeds from input to output - that is, the candidates for equivalence that are closest to the inputs are given highest priority for the equivalence check.

• Cryptol is a language for writing specifications and building formal models for equivalence checking. Cryptol has a built-in equivalence checker called jaig but better results are typically obtained using abc outside of cryptol where abc is applied to the formal models produced in cryptol. The language is versatile and can be used to model code at the bit level - as long as a bit-level semantics can be defined for instructions. On applications where loops run for a fixed number of iterations and there are relatively few case splits, cryptol seems to be a good formal verification tool, even for bit widths up to 32 and 64 bits.

The main construct for manipulating state in cryptol is the list comprehension. Here are a few examples:

```      ex0 = [| f(x,y)
|| x <- [..list of x elems..], y <- [..list of y elems..] |];
```
create a list of elements, each having value f(x,y) for every pair of values in [..list of x elems..] and [..list of y elems..]. Size of ex0 is the product of the sizes of both lists.
```      ex1 = [| f(x,y,z)
|| x <- [..list of x elems..], y <- [..list of y elems..]
|| z <- [..list of z elems..] |];
```
try to create a list of elements, each having value f(x,y,z) for every pair of values in [..list of x elems..] and [..list of y elems..] and for each of those pairs, a single value from [..list of z elems..]. Size of ex1 is the minimum of the product of the sizes of the x and y lists and the size of the z list.
```      ex2 = [| f(x,y,z)
|| x <- [1 2], y <- [3 4], z <- [5 6] |];
```
create a list of elements, each having value f(x,y,z) for every triple of values in [..list of x elems..]. [..list of y elems..] and [..list of z elems..]. Size of ex2 is the product of the sizes of the x, y, and z lists.
```      ex3 = [| f(x,y)
|| x <- [..list of x elems..]
|| y <- [..list of y elems..] |];
```
create a list of elements, each having value f(x,y) for every pair where x is indexed in [..list of x elems..] at the same point that y is indexed in [..list of y elems..]. Size of ex3 is the minimum of the size of [..list of x elems..] and [..list of y elems..].
```      ex4 = s
where {
s = [..init..]#[| f(x,y)
|| y <- [..list of y elems..]
|| x <- s |];
};
```
This is the most useful of all types of list comprehensions. Think of output list s as a sequence of states and [..list of y elems..] as a sequence of input values. The single element list [..init..] is the initial state. The function f(x,y) is just a state transition function - it maps an input and a current state to a new state. If one is interested in just the last state in the sequence, change the top line to ex4 = s@(width(s)-1)

Example: The pigeon-hole principle.

The procedures sum-list and posn-one-listp in ACL2 have the following counterparts in cryptol:

```      sum_list : {a} ([a][32] -> [32]);
sum_list l = s@(width(s)-1)
where {
s = [0]#[| x+y
|| x <- l
|| y <- s |];
};

posn_one_listp l = s@(width(s)-1)
where {
s = [True]#[| if ((x>1) | (x<0)) then False else y
|| x <- l
|| y <- s |];
};
```
The theorem to prove is the following, for 100 holes:
```      theorem thm1: {l}.
~(sum_list(l:[100][32]) > width(l)) | ~posn_one_listp(l);
```
which does prove after a little time using abc.

Example: Legato's multiplier

```      /* Here is Legato's algorithm, as coded in Mostek assembly

step1 :       LDX #8         ; load X immediate with the integer 8
step2 :       LDA #0         ; load A immediate with the integer 0
step3 :       CLC            ; set C to 0
step4 : LOOP  ROR F1         ; rotate F1 right circular through C
step5 :       BCC ZCOEF      ; branch to ZCOEF if C = 0
step6 :       CLC            ; set C to 0
step7 :       ADC F2         ; set A to A+F2+C and C to the carry
step8 : ZCOEF ROR A          ; rotate A right circular through C
step9 :       ROR LOW        ; rotate LOW right circular through C
step10:       DEX            ; set X to X-1
step11:       BNE LOOP       ; branch to LOOP if Z = 0
*/

// An abstraction of the Mostek state;
type Mostek = ( [8] // F1
, [8] // F2
, [8] // A
, [8] // X
, [8] // LOW
, Bit // C (Carry)
, Bit // Z (Zero)
);

// Each line in the program becomes a state transformer,
// captured by the Instruction type below
type Instruction = Mostek -> Mostek;

// Each line modifies the state and passes the control
// to the next.

// step1: LDX #8; load X immediate with the integer 8
step1 : Instruction;
step1 (f1, f2, a, _, l, c, z) = step2 (f1, f2, a, 8, l, c, z);

// step2: LDA #0; load A immediate with the integer 0
step2 : Instruction;
step2 (f1, f2, _, x, l, c, z) = step3 (f1, f2, 0, x, l, c, z);

// step3: CLC; set C to 0
step3 : Instruction;
step3 (f1, f2, a, x, l, _, z) = step4 (f1, f2, a, x, l, False, z);

// step4: LOOP  ROR F1; rotate F1 right circular through C
step4 : Instruction;
step4 (f1, f2, a, x, l, c, z) = step5 (f1', f2, a, x, l, b0, z)
where {
[b0 b1 b2 b3 b4 b5 b6 b7] = f1; // NB: Little-endian!
f1' = [b1 b2 b3 b4 b5 b6 b7 c]; // ROR; little-endian; so go left
};

// step5 : BCC ZCOEF; branch to ZCOEF if C = 0
// ZCOEF is step8 in our encoding
step5 (f1, f2, a, x, l, c, z)
= if c then step6 (f1, f2, a, x, l, c, z)
else step8 (f1, f2, a, x, l, c, z);

// step6: CLC; set C to 0
step6 (f1, f2, a, x, l, _, z) = step7 (f1, f2, a, x, l, False, z);

// step7: ADC F2; set A to A+F2+C and C to the carry
step7 (f1, f2, a, x, l, c, z) = step8 (f1, f2, a', x, l, c', z')
where {
a' = a + f2 + (if c then (1:[8]) else (0:[8]));
a'Large : [9];  // for the carry - need one more bit
a'Large = (a # zero) + (f2 # zero) + (if c then (1:[9]) else (0:[9]));
c' = a'Large > (255:[9]);
z' = a' == 0;
};

// step8 : ZCOEF ROR A; rotate A right circular through C
step8 : Instruction;
step8 (f1, f2, a, x, l, c, z) = step9 (f1, f2, a', x, l, a0, z)
where {
[a0 a1 a2 a3 a4 a5 a6 a7] = a; // NB: Little-endian!
a' = [a1 a2 a3 a4 a5 a6 a7 c]; // ROR; little-endian; so go left
};

// step9 : ROR LOW; rotate LOW right circular through C
step9 : Instruction;
step9 (f1, f2, a, x, l, c, z) = step10 (f1, f2, a, x, l', l0, z)
where {
[l0 l1 l2 l3 l4 l5 l6 l7] = l; // NB: Little-endian!
l' = [l1 l2 l3 l4 l5 l6 l7 c]; // ROR; little-endian; so go left
};

// step10: DEX; set X to X-1
step10 : Instruction;
step10 (f1, f2, a, x, l, c, z) = step11 (f1, f2, a, x', l, c, x'==0)
where x' = x-1;

// step11: BNE LOOP; branch to LOOP if Z = 0
// LOOP is step4 in our encoding
step11 : Instruction;
step11 (f1, f2, a, x, l, c, z)
= if z
then (f1, f2, a, x, l, c, z)        // done!
else step4 (f1, f2, a, x, l, c, z);

// legato: given two 8 bit arguments f1 and f2, return 8 bit
// results hi and lo, s.t. f1 * f2 = hi * 256 + lo
legato : ([8], [8], Mostek) -> ([8], [8]);
legato (f1, f2, st) = (hi, lo)
where {
// get the relevant parts to construct the starting state
(_, _, A, X, LOW, C, Z) = st;
// Run legato multiplier; final A is hi; and final LOW is low
(_, _, hi, _, lo, _, _) = step1 (f1, f2, A, X, LOW, C, Z);
};

// State the correctness of the algorithm
theorem legatoIsCorrect: {x y st}. x' * y' == 256 * hi' + lo'
where { (hi, lo) = legato (x, y, st);
hi', lo', x', y' : [16];
hi' = hi # zero;
lo' = lo # zero;
x'  = x  # zero;
y'  = y  # zero
};
```