∀x x^{2}+x+1 = yvariable x is bound and y is free.
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))))This one proves. Now we return to:
(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").
(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))) <= thisACL2 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 thisThe 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.
{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:
--------------------- {Q[E/x]} x := E; {Q}Example:
{P} C1 {R}, {R} C2 {Q} ---------------------- {P} C1; C2 {Q}Example:
{A ∧ B} C1 {Q}, {¬A ∧ B} C2 {Q} ------------------------------- {B} if A then C1 else C2 {Q}Example:
P' → P, {P} C {Q}, Q' → Q ------------------------- {P'} C {Q'}Example:
{Q ∧ A} C {Q} ------------------------- {Q} while A do C {¬A ∧ Q}Example:
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:
{(n ≥ 0)} i := 0; s := 0; while i != n do i := i+1; s := s + (2*i - 1); end {(s == n*n)} P_{0} = ((i == n) ∧ (s == n∗n)) P_{1} = ((i == n−1) ∧ (s == i∗i)) P_{2} = ((i == n-2) ∧ (s == i∗i)) ... P_{j} = ((i == n−j) ∧ (s == i∗i) ... wp(while..., (s == n∗n)) = ((i ≤ n) ∧ (s == i∗i)
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. |
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).
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.
(φ_{11}(...) ⊕ φ_{12}(...)) ∨ (φ_{21}(...) ⊕ φ_{22}(...)) ∨ ... ∨ (φ_{21}(...) ⊕ φ_{22}(...)) |
Example: click this link
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 };