Machine integers

F* machine integers

Common representation

F* machine integers are all implemented in modules called FStar.IntN for signed integers, and FStar.UIntN for unsigned integers, where N is the number of bits the integer is encoded on.

F* currently offers support for:

• char and unsigned char (FStar.Int8 and FStar.UInt8)
• short and unsigned short (FStar.Int16 and FStar.UInt16)
• int31 and unsigned int31, which are the OCaml native integers on 32-bit platforms (FStar.Int31 and FStar.UInt31)
• int32 and unsigned int32 (FStar.Int32 and FStar.UInt32)
• int63 and unsigned int63, which are the OCaml native integers on 64-bit platforms (FStar.Int63 and FStar.UInt63)
• int64 and unsigned int64 (FStar.Int64 and FStar.UInt64)
• int128 and unsigned int128 which are non-standard but supported by certain C compilers (FStar.Int128 and FStar.UInt128)

All those modules have similar structures and expose the same operators:

• a type t, which is the type of the machine integers of that module. E.g. the type of int64 is FStar.UInt64.t.
• a function val v: t -> Tot int which returns the integer value of a machine integer.
• the n constant defines the number of bits the machine integer is encoded on.
• a size predicate which specifies the range of mathematical integer values that can be encoded on the machine integer.
• a val (u)int_to_t: x:t{size x n} -> Tot t function that converts a mathematical integer to a machine integer encoding that value.
• the max_int n and min_int n values define the maximum and minimum values that can be represented by the machine integers of the given module. (e.g. -128 and 127 for shorts).
• [add|sub|mul] operators are strictly non-overflowing addition, subtraction and multiplication, which means that the proof system checks the absence of overflows before typechecking.
• [add|sub|mul]_mod are addition, subtraction and multiplication with wrapping semantics.
• [add|sub|mul]_underspec are underspecified non-overflowing addition, subtraction and multiplication, which means that if the proof system cannot assert the absence of overflows, the result of the operation will be undefined.
• div and rem are the division and the remainder. For signed integers, those are the flooring division and the signed remainder and NOT the respective euclidian versions.
• shift_left and shift_right are the shift operators. The right operand must be smaller that the number of bits the integer represents (e.g. for an int32, the right operand has to be less than or equal to 31).
• logand, logor, logxor and lognot are bitwise operators to compute &, |, ^ and ~.
• eq, gte, gt, lte, lt are boolean comparison that compute 'equals', 'greater than or equal', 'greater than', 'lower than or equal', 'lower than'.
• of_string and to_string allow to use of constants in the code. However as the format of the string is not currently checked to be proper, the use of the of_string function is unsound and should be avoided. Machine integer constants should be used instead (see section below).

For convenience, those modules also define infix operators for most of those functions, which is the usual infix operator post-fixed by the ^ symbol:

• [add|sub|mul] ==> [+|-|*]^
• [add|sub|mul]_mod ==> [+|-|*]%^
• [add|sub|mul]_underspec ==> [+|-|*]?^
• div ==> /^
• rem ==> %^
• shift_left ==> <<^
• shift_right ==> >>^
• logand, logor, logxor ==> &^, |^, ^^

Machine integer constants

F* uses the following syntax for machine integer values:

• constants can be written in decimal, binary, octal or hexadecimal form:
  • 0b10 stands for 2
  • 0o10 stands for 8
  • 10 stands for 10
  • 0x10 stands for 16
• suffixes allow the parser to pick the right size and sign:
  • 1y and 1uy for FStar.Int8 and FStar.UInt8
  • 1s and 1us for FStar.Int16 and FStar.UInt16
  • 1l and 1ul for FStar.Int32 and FStar.UInt32
  • 1L and 1uL for FStar.Int64 and FStar.UInt64

Those prefixes and suffixes can be freely combined. E.g. 0x10ul is the FStar.UInt32.t value encoding 16.

Namespace scopes

F* does not support overloading. The infix operators will be those of the last opened FStar.(U)IntN module.

The F* parser supports namespace scoping to help manipulating values of different machine integer types. For instance one can write:

let word = let open FStar.Int32 in 0l +^ 1l in
let word' = let open FStar.Int64 in 0L +^ 0L in
...

Or, alternatively:

let word = FStar.Int32.( 0l +^ 1l ) in
let word' = FStar.Int64.( 0L +^ 0L ) in
...

Realization

Those modules have OCaml (all modules) and C ((U)Int[8|16|32|64|128], via KreMLin) realization. The OCaml realized modules link to:

• native OCaml integers for (U)Int8,16,31,32,63, assuming a 64-bit platform. That implies that concretely, all machine integers smaller than 63 bits will be encoded as 63 bits integers, for performance.
• Boxed integers from the Stdint OCaml library. E.g. FStar.Int64 goes to Stdint.Int64 in OCaml.

Remarks

It is assumed that the default type for machine integers in F* is FStar.UInt32.t. Hence indexes, lengths or counters should be of that type.

Some modules define additional type and operators:

• FStar.UInt8 defines the type byte (unsigned char)
• the unsigned FStar.UIntN modules define two masking operators:
  • eq_mask which compares two operands and returns 0xff...ff if they are equal, 0x0..0 otherwise
  • gte_mask which compares two operands and returns 0xff...ff if the first one is greater than or equal to the other, 0x0..0 otherwise
• the FStar.(u)Int128 modules define a mul_wide operator which takes two FStar.(U)Int64.t integers and return a FStar.(U)Int128.t result.