CryptolSemantics  GaloisInc/cryptol GitHub Wiki
Denotational Semantics
We use a domain theoretic denotational semantics.
Meaning of types
Each Cryptol type is modeled as a cpo with a least element ("bottom").

Bit
Our model of type
Bit
has three values:True
,False
, andundefined
, a.k.a. "bottom". The bottom value represents a computation that either fails to terminate or quits with a runtime error. 
Tuple types
(a, b)
We model tuples as cartesian products. The pair constructor is both injective and surjective.
(undefined : a, undefined : b)
is the bottom element of type(a, b)
.The empty tuple type
()
is modeled as a singleton set. 
Record types
{x : a, y : b}
Records are modeled as cartesian products, just like tuples.

Array types
[n]a
Arrays are modeled as
n
ary cartesian products, similar to tuples. Forn = inf
, type[inf]a
consists of countably infinite sequences of elements of typea
. The bottom elementundefined : [n]a
is ann
element array whose elements are all equal toundefined : a
. 
Function types
a > b
The function type is modeled as the continuous function space from type
a
to typeb
. 
Polymorphic types
TODO
Recursive definitions
We model recursively defined values using the domain theoretic least fixed point.
Primitives

Conditionals:
if
/then
/else
The conditional is strict in the condition bit, and nonstrict in the
then
/else
branches. 
Literals and static sequences:
True
,False
, numerals,[a,b..]
,[a..b]
,[a,b..c]
,[a...]
,[a,b...]
These all produce completely defined output, with no undefined bits anywhere.

Runtime error:
error
We model the
error
function as a constant function that always returns the bottom element of the appropriate type. 
Arithmetic:
+
,
,*
,/
,%
,^^
,lg2
On bitvector types like
[n]
, these are fully strict: if any bit of the input is undefined, then all bits of the output are undefined. On higher types, a component of output is defined iff the corresponding components of both inputs are defined. 
Comparisons:
<
,>
,<=
,>=
,==
,!=
TODO On bitvector types, there are two choices that would make sense:
 Either make comparisons fully strict:
[False, undefined] < [True, undefined] = undefined
 Only force bits from the left until a difference is found:
[False, undefined] < [True, undefined] = True
On larger types, they are strict in all components to the left of where the first difference is found, and lazy afterward:
[0x02, 0x03, 0x04] == [0x02, 0x04, undefined] = False
Primitives
===
,!==
,min
, andmax
can all be defined in terms of other operations:
f === g
=\x > f x == g x

f !== g
=\x > f x != g x

min x y
=if x < y then x else y

max x y
=if x < y then y else x
 Either make comparisons fully strict:

Bitwise operators:
&&
,
,^
,~
,zero
On type
Bit
, these operations are strict in both arguments: e.g.True  undefined
=undefined  True
=undefined
. Lazier (but nonsymmetrical) versions of and/or can be defined using if/then/else. We are not going to implement parallelor.On higher types, a bit of the output is defined iff the corresponding bits of the inputs are both defined.

Shifts and rotates:
<<
,>>
,<<<
,>>>
These are all fully strict in the shift index argument. They are nonstrict in the array elements. For example:

[undefined, 0x02, 0x03] <<< 1
=[0x02, 0x03, undefined]

[undefined, undefined, 0x02] << 1
=[undefined, 0x02, 0x00]

[undefined, undefined, True] << 1
=[undefined, True, False]


Sequence operations:
#
,splitAt
,join
,split
,reverse
,transpose
These are all nonstrict in the array elements. Definedness of components is preserved.

Indexing operations:
@
,!
These are fully strict in all bits of the index, and nonstrict in the array elements.
Multiindexing operations
@@
,!!
can be derived:xs @@ js = [ xs @ j  j < js ]
xs !! js = [ xs ! j  j < js ]

Polynomial operations:
pmul
,pdiv
,pmod
We'll probably make these fully strict, like the arithmetic operators.
List comprehensions
TODO
Class constraints
TODO
Operational Semantics
TODO