Primitive objects¶
Primitive Integers¶
The language of terms features 63-bit machine integers as values. The type of
such a value is axiomatized; it is declared through the following sentence
(excerpt from the PrimInt63
module):
This type can be understood as representing either unsigned or signed integers,
depending on which module is imported or, more generally, which scope is open.
Uint63
and uint63_scope
refer to the unsigned version, while Sint63
and sint63_scope
refer to the signed one.
The PrimInt63
module declares the available operators for this type.
For instance, equality of two unsigned primitive integers can be determined using
the Uint63.eqb
function, declared and specified as follows:
The complete set of such operators can be found in the PrimInt63
module.
The specifications and notations are in the Uint63
and Sint63
modules.
These primitive declarations are regular axioms. As such, they must be trusted and are listed by the
Print Assumptions
command, as in the following example.
- From Stdlib Require Import Uint63.
- [Loading ML file ring_plugin.cmxs (using legacy method) ... done] [Loading ML file zify_plugin.cmxs (using legacy method) ... done] [Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done] [Loading ML file micromega_plugin.cmxs (using legacy method) ... done] [Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
- Lemma one_minus_one_is_zero : (1 - 1 = 0)%uint63.
- 1 goal ============================ (1 - 1)%uint63 = 0%uint63
- Proof. apply eqb_correct; vm_compute; reflexivity. Qed.
- No more goals.
- Print Assumptions one_minus_one_is_zero.
- Axioms: sub : int -> int -> int eqb_correct : forall i j : int, (i =? j)%uint63 = true -> i = j eqb : int -> int -> bool
The reduction machines implement dedicated, efficient rules to reduce the applications of these primitive operations.
The extraction of these primitives can be customized similarly to the extraction
of regular axioms (see Program extraction). Nonetheless, the ExtrOCamlInt63
module can be used when extracting to OCaml: it maps the Rocq primitives to types
and functions of a Uint63
module (including signed functions for
Sint63
despite the name). That OCaml module is not produced by extraction.
Instead, it has to be provided by the user (if they want to compile or execute
the extracted code). For instance, an implementation of this module can be taken
from the kernel of Rocq.
Literal values (at type Uint63.int
) are extracted to literal OCaml values
wrapped into the Uint63.of_int
(resp. Uint63.of_int64
) constructor on
64-bit (resp. 32-bit) platforms. Currently, this cannot be customized (see the
function Uint63.compile
from the kernel).
Primitive Floats¶
The language of terms features Binary64 floating-point numbers as values.
The type of such a value is axiomatized; it is declared through the
following sentence (excerpt from the PrimFloat
module):
This type is equipped with a few operators, that must be similarly declared.
For instance, the product of two primitive floats can be computed using the
PrimFloat.mul
function, declared and specified as follows:
where Prim2SF
is defined in the FloatOps
module.
The set of such operators is described in section Floats library.
These primitive declarations are regular axioms. As such, they must be trusted, and are listed by the
Print Assumptions
command.
The reduction machines (vm_compute
, native_compute
) implement
dedicated, efficient rules to reduce the applications of these primitive
operations, using the floating-point processor operators that are assumed
to comply with the IEEE 754 standard for floating-point arithmetic.
The extraction of these primitives can be customized similarly to the extraction
of regular axioms (see Program extraction). Nonetheless, the ExtrOCamlFloats
module can be used when extracting to OCaml: it maps the Rocq primitives to types
and functions of a Float64
module. Said OCaml module is not produced by
extraction. Instead, it has to be provided by the user (if they want to compile
or execute the extracted code). For instance, an implementation of this module
can be taken from the kernel of Rocq.
Literal values (of type Float64.t
) are extracted to literal OCaml
values (of type float
) written in hexadecimal notation and
wrapped into the Float64.of_float
constructor, e.g.:
Float64.of_float (0x1p+0)
.
Primitive Arrays¶
The language of terms features persistent arrays as values. The type of
such a value is axiomatized; it is declared through the following sentence
(excerpt from the PArray
module):
This type is equipped with a few operators, that must be similarly declared.
For instance, elements in an array can be accessed and updated using the
PArray.get
and PArray.set
functions, declared and specified as
follows:
The rest of these operators can be found in the PArray
module.
These primitive declarations are regular axioms. As such, they must be trusted and are listed by the
Print Assumptions
command.
The reduction machines (vm_compute
, native_compute
) implement
dedicated, efficient rules to reduce the applications of these primitive
operations.
The extraction of these primitives can be customized similarly to the extraction
of regular axioms (see Program extraction). Nonetheless, the ExtrOCamlPArray
module can be used when extracting to OCaml: it maps the Rocq primitives to types
and functions of a Parray
module. Said OCaml module is not produced by
extraction. Instead, it has to be provided by the user (if they want to compile
or execute the extracted code). For instance, an implementation of this module
can be taken from the kernel of Rocq (see kernel/parray.ml
).
Rocq's primitive arrays are persistent data structures. Semantically, a set operation
t.[i <- a]
represents a new array that has the same values as t
, except
at position i
where its value is a
. The array t
still exists, can
still be used and its values were not modified. Operationally, the implementation
of Rocq's primitive arrays is optimized so that the new array t.[i <- a]
does not
copy all of t
. The details are in section 2.3 of [CF07].
In short, the implementation keeps one version of t
as an OCaml native array and
other versions as lists of modifications to t
. Accesses to the native array
version are constant time operations. However, accesses to versions where all the cells of
the array are modified have O(n) access time, the same as a list. The version that is kept as the native array
changes dynamically upon each get and set call: the current list of modifications
is applied to the native array and the lists of modifications of the other versions
are updated so that they still represent the same values.
Primitive (Byte-Based) Strings¶
The language of terms supports immutable strings as values. Primitive strings
are axiomatized. The type is declared through the following sentence (excerpt
from the PrimString
module):
This type is equipped with functions that must be similarly declared. For example,
the length of a string can be computed with PrimString.length
, and the character
(i.e., byte) at a given position can be obtained with PrimString.get
. These
functions are defined as follows:
The remaining primitives can be found in the PrimString
module.
These primitive declarations are regular axioms. As such, they must be trusted and
are listed by the Print Assumptions
command.
The reduction machines (vm_compute
, native_compute
) implement
dedicated, efficient rules to reduce the applications of these primitive
operations.
The extraction of these primitives can be customized similarly to the extraction
of regular axioms (see Program extraction). Nonetheless, the ExtrOCamlPString
module can be used when extracting to OCaml: it maps the Rocq primitives to types
and functions of a Pstring
module. Said OCaml module is not produced by
extraction. Instead, it has to be provided by the user (if they want to compile
or execute the extracted code). For instance, an implementation of this module
can be taken from the kernel of Rocq (see kernel/pstring.ml
).
Literal values (of type Pstring.t
, or equivalently string
) are extracted
to literal OCaml values (of type string
).