CryptolSemantics

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, and undefined, a.k.a. "bottom". The bottom value represents a computation that either fails to terminate or quits with a run-time 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. For n = inf, type [inf]a consists of countably infinite sequences of elements of type a. The bottom element undefined : [n]a is an n-element array whose elements are all equal to undefined : a.

• Function types a -> b

  The function type is modeled as the continuous function space from type a to type b.

• 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 non-strict 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.

• Run-time 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:

  1. Either make comparisons fully strict: [False, undefined] < [True, undefined] = undefined
  2. 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, and max 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

• Bitwise operators: &&, ||, ^, ~, zero

  On type Bit, these operations are strict in both arguments: e.g. True || undefined = undefined || True = undefined. Lazier (but non-symmetrical) versions of and/or can be defined using if/then/else. We are not going to implement parallel-or.

  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 non-strict 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 non-strict in the array elements. Definedness of components is preserved.

• Indexing operations: @, !

  These are fully strict in all bits of the index, and non-strict in the array elements.

  Multi-indexing 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