Contents

Cryptol 2 Language Primitives Comparisons and Ordering Arithmetic Boolean Sequences Shift And Rotate Random Values Debugging Hints for Hardware Generation? Closing Remarks
Cryptol 2 Language Primitives
Cryptol 2 has a number of built-in primitive functions. Herein we summaries them.

Comparisons and Ordering
` `( == ) : { a } ( Cmp a ) => a -> a -> Bit
( != ) : { a } ( Cmp a ) => a -> a -> Bit
( === ) : { a , b } ( Cmp b ) => ( a -> b ) -> ( a -> b ) -> a -> Bit
( !== ) : { a , b } ( Cmp b ) => ( a -> b ) -> ( a -> b ) -> a -> Bit
( < ) : { a } ( Cmp a ) => a -> a -> Bit
( > ) : { a } ( Cmp a ) => a -> a -> Bit
( <= ) : { a } ( Cmp a ) => a -> a -> Bit
( >= ) : { a } ( Cmp a ) => a -> a -> Bit
min : { a } ( Cmp a ) => a -> a -> a
max : { a } ( Cmp a ) => a -> a -> a
instance Cmp Bit
// No instance for functions .
instance ( Cmp a , fin n ) => Cmp [ n ] a
instance ( Cmp a , Cmp b ) => Cmp ( a , b )
instance ( Cmp a , Cmp b ) => Cmp { x : a , y : b }

Arithmetic
` `negate : { a } ( Arith a ) => a -> a
( + ) : { a } ( Arith a ) => a -> a -> a
( - ) : { a } ( Arith a ) => a -> a -> a
( * ) : { a } ( Arith a ) => a -> a -> a
( / ) : { a } ( Arith a ) => a -> a -> a
( % ) : { a } ( Arith a ) => a -> a -> a
( ^^ ) : { a } ( Arith a ) => a -> a -> a
// No instance for ` Bit ` .
instance ( fin n ) => Arith ( [ n ] Bit )
instance ( Arith a ) => Arith ( [ n ] a )
instance ( Arith b ) => Arith ( a -> b )
instance ( Arith a , Arith b ) => Arith ( a , b )
instance ( Arith a , Arith b ) => Arith { x : a , y : b }

Note that because there is no instances for `Arith Bit`

the top two instances do not actually overlap.

A corner case: unlike the old system, we’d also have to define `negate`

at type `0`

. This makes sense, there is only one element of type `[0]`

, so it is naturally its own inverse, thus `negate`

should behave as the identity function.

Boolean
` `False : Bit
True : Bit
zero : ( Logic a ) => a
( && ) : ( Logic a ) => a -> a -> a
( || ) : ( Logic a ) => a -> a -> a
( ^ ) : ( Logic a ) => a -> a -> a
( ~ ) : ( Logic a ) => a -> a
// There are instances for all types ,
// so we could potentially omit the constraints .
instance Logic Bit
instance Logic a => Logic ([ n ] a )
instance Logic b => Logic ( a -> b )
instance ( Logic a , Logic b ) => Logic ( a , b )
instance ( Logic a , Logic b ) => Logic { x : a , y : b }

Sequences
` `length : { n , a , m } ( m >= width n ) => [ n ] a -> [ m ]
join : { parts , ench , a } ( fin each ) => [ parts ][ each ] a -> [ parts * each ] a
split : { parts , each , a } ( fin each ) => [ parts * each ] a -> [ parts ][ each ] a
( # ) : { front , back , a } ( fin front ) => [ front ] a -> [ back ] a -> [ front + back ] a
splitAt : { front , back , a } ( fin front ) => [ from + back ] a -> ([ front ] a , [ back ] a )
reverse : { n , a } ( fin n ) => [ n ] a -> [ n ] a
transpose : { n , m , a } [ n ][ m ] a -> [ m ][ n ] a
( @ ) : { n a m } [ n ] a -> [ m ] -> a
( @@ ) : { n a m i } [ n ] a -> [ m ][ i ] -> [ m ] a
( ! ) : { n a m } ( fin n ) => [ n ] a -> [ m ] -> a
( !! ) : { n a m i } ( fin n ) => [ n ] a -> [ m ][ i ] -> [ m ] a
// Abbreviations
splitBy n = split `{ parts = n }
groupBy n = split `{ each = n }
tail n = splitAt `{ front = 1 } . 2
take n = splitAt `{ front = n } . 1
drop n = splitAt `{ front = n } . 2
/* Also , ` length ` is not really needed :
length : { n , a , m } ( m >= width n ) => [ n ] a -> [ m ]
length _ = ` n
*/

Shift And Rotate
` `( << ) : { n , a , m } ( fin n , Logic a ) => [ n ] a -> [ m ] -> [ n ] a
( >> ) : { n , a , m } ( fin n , Logic a ) => [ n ] a -> [ m ] -> [ n ] a
( <<< ) : { n , a , m } ( fin n , Logic a ) => [ n ] a -> [ m ] -> [ n ] a
( >>> ) : { n , a , m } ( fin n , Logic a ) => [ n ] a -> [ m ] -> [ n ] a

Random Values
New types:

` `random : { a } => [ 32 ] -> a

Debugging
` `ASSERT : { n a } ( Bit ,[ n ][ 8 ], a ) -> a
undefined : { a } a
error : { n a } [ n ][ 8 ] -> a
trace : { n a j } ([ n ][ 8 ], a , j ) -> j

Hints for Hardware Generation?
` `pipeline_stop : { a } a -> a
pipeline : { n a } ( fin n ) => ([ n ], a ) -> a
seq : { n a } [ n ] a -> [ n ] a
par : { n a } [ n ] a -> [ n ] a
reg : { a } a -> a
const : { a } a -> a

Remark : If you have ever used Cryptol 1 you will notice there are some differences in the type-signatures.