add rigor to the prelude

[kiniry]

Include formal specifications for built-ins and verify that they conform to them.

[kiniry]

I do not have the time to work on this for the 2.1 release, so I'm pushing.

[brianhuffman]

I did some work on this a while back, and started a Cryptol module stating characteristic properties of a bunch of primitives. Maybe we should finish it.

/*

This module contains logical specifications of all of Cryptol's
primitives, written as checkable properties in Cryptol. Overloaded
primitives are specified for each base instance of the class: For
example, the Arith primitives are specified for bitvectors and integer
types.

Each primitive is specified in terms of earlier ones. We take True,
False, and logical complement as our base primitives, which are left
unspecified.

*/

module PrimSpec where

cons : {n, a} a -> [n]a -> [1+n]a
cons x xs = [x] # xs

/* Logic Bit, Cmp Bit */

infix 5 <==>
(<==>) : Bit -> Bit -> Bit
x <==> y = x == y

property not_Bit_1 = ~ False
property not_Bit_2 = ~ (~ True)

property eq_Bit_1 = True == True
property eq_Bit_2 = ~ (True == False)
property eq_Bit_3 = ~ (False == True)
property eq_Bit_4 = False == False

property ite_Bit_1 x y = (if True then x else y) <==> x
property ite_Bit_2 x y = (if False then x else y) <==> y

property conj_Bit x y = (x && y) <==> (if x then y else False)
property disj_Bit x y = (x || y) <==> (if x then True else y)
property xor_Bit x y = (x ^ y) <==> (if x then ~ y else y)
property zero_Bit = zero <==> False

property le_Bit x y = (x <= y) <==> (if x then y else True)
property lt_Bit x y = (x < y) <==> (if x then False else y)
property ge_Bit x y = (x >= y) <==> (if y then x else True)
property gt_Bit x y = (x > y) <==> (if y then False else x)
property ne_Bit x y = (x != y) <==> ~ (x == (y : Bit))

/* Cmp [n]a */

eq_nil : {a} (Cmp a) => Bit
eq_nil = [] == ([] : [0]a)

eq_cons : {n, a} (Cmp a, fin n) => a -> [n]a -> a -> [n]a -> Bit
eq_cons x xs y ys = (cons x xs == cons y ys) <==> (x == y /\ xs == ys)

le_nil : {a} (Cmp a) => Bit
le_nil = [] <= ([] : [0]a)

le_cons : {n, a} (Cmp a, fin n) => a -> [n]a -> a -> [n]a -> Bit
le_cons x xs y ys = (cons x xs <= cons y ys) <==> (x <= y) /\ (x == y ==> xs <= ys)

/* Arith [n] */

//primitive (+) : {a} (Arith a) => a -> a -> a
//primitive (-) : {a} (Arith a) => a -> a -> a
//primitive (*) : {a} (Arith a) => a -> a -> a
//primitive (/) : {a} (Arith a) => a -> a -> a
//primitive (%) : {a} (Arith a) => a -> a -> a
//primitive (^^) : {a} (Arith a) => a -> a -> a
//primitive lg2 : {a} (Arith a) => a -> a
//primitive negate : {a} (Arith a) => a -> a

inc : {n} (fin n) => [n] -> [n]
inc xs = reverse [ x ^ c | x <- reverse xs | c <- cs ]
  where cs = [True] # [ x && c | x <- reverse xs | c <- cs ]

inc_spec : {n} (fin n, n >= 1) => [n] -> Bit
inc_spec x = inc x == x + 1

add_0 : {a} (Arith a, Cmp a, Literal 0 a) => a -> Bit
add_0 x = 0 + x == x

add_S : {a} (Arith a, Cmp a, Literal 1 a) => a -> a -> Bit
add_S x y = (x + 1) + y == (x + y) + 1

mul_0 : {a} (Arith a, Cmp a, Literal 0 a) => a -> Bit
mul_0 x = 0 * x == 0

mul_S : {a} (Arith a, Cmp a, Literal 1 a) => a -> a -> Bit
mul_S x y = (x + 1) * y == x + x * y

sub_spec x y = x - y == x + negate y

/* Sequence primitives */

//primitive (#) : {front, back, a} (fin front) => [front]a -> [back]a -> [front + back] a

append_nil xs = [] # xs == xs

append_cons x xs ys = cons x xs # ys == cons x (xs # ys)

//primitive splitAt : {front, back, a} (fin front) => [front + back]a -> ([front]a, [back]a)

splitAt_nil : {back, a} (fin back, Cmp a) => [back]a -> Bit
splitAt_nil xs = splitAt`{0, back} xs == ([], xs)

splitAt_cons : {front, back, a} (fin front, fin back, Cmp a) => a -> [front + back]a -> Bit
splitAt_cons x xs = splitAt`{1+front, back} (cons x xs) == (cons x xs1, xs2)
  where (xs1, xs2) = splitAt`{front, back} xs

//primitive join : {parts, each, a} (fin each) => [parts][each]a
//                                             -> [parts * each]a

join_nil : {each, a} (fin each, Cmp a) => Bit
join_nil = join ([] : [0][each]a) == []

join_cons :
  {parts, each, a} (fin parts, fin each, Cmp a) =>
  [each]a -> [parts][each]a -> Bit
join_cons xs xss = join (cons xs xss) == xs # join xss

//primitive split : {parts, each, a} (fin each) => [parts * each]a
//                                              -> [parts][each]a

split_nil : {each, a} (fin each, Cmp a) => Bit
split_nil = split`{0} [] == ([] : [0][each]a)

split_cons : {parts, each, a} (fin parts, fin each, Cmp a) => [(1 + parts) * each]a -> Bit
split_cons xs = split`{1+parts} xs == cons xs1 (split xs2)
  where (xs1, xs2) = splitAt`{each, parts * each} xs

//primitive reverse : {n, a} (fin n) => [n]a -> [n]a

reverse_nil : {a} (Cmp a) => Bit
reverse_nil = reverse [] == ([] : [0]a)

reverse_cons : {n, a} (fin n, Cmp a) => a -> [n]a -> Bit
reverse_cons x xs = reverse (cons x xs) == reverse xs # [x]

//primitive transpose : {rows, cols, a} [rows][cols]a -> [cols][rows]a

transpose_cons xs xss = transpose (cons xs xss) == [ cons y ys | y <- xs | ys <- xss ]

[atomb]

Let's add the Cryptol file quoted above to the repo, and continue to add to it.

[brianhuffman]

Todo: Put the cryptol file with specs for primitives in the lib directory, alongside Cryptol.cry. This would let cryptol users (or saw users) to import and refer to the properties in the file.

We should also strive to keep the file up to date whenever we add new primitive functions to cryptol.

Todo: Also add a test to the test suite that runs :check and :prove on all the properties in this file at several common bit-widths.