Primitive integers

This work makes it possible to take advantage of a compact
representation for integers in the entire system, as opposed to only
in some reduction machines. It is useful for heavily computational
applications, where even constructing terms is not possible without such
a representation.

Concretely, it replaces part of the retroknowledge machinery with
a primitive construction for integers in terms, and introduces a kind of
FFI which maps constants to operators (on integers). Properties of these
operators are expressed as explicit axioms, whereas they were hidden in
the retroknowledge-based approach.

This has been presented at the Coq workshop and some Coq Working Groups,
and has been used by various groups for STM trace checking,
computational analysis, etc.

Contributions by Guillaume Bertholon and Pierre Roux <Pierre.Roux@onera.fr>

Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>

8 files changed, 74 insertions, 5 deletions

diff --git a/checker/analyze.ml b/checker/analyze.ml
index 63324bff20..77e70318dd 100644
--- a/checker/analyze.ml
+++ b/checker/analyze.ml
@@ -106,6 +106,7 @@ end
 
 type repr =
 | RInt of int
+| RInt63 of Uint63.t
 | RBlock of (int * int) (* tag × len *)
 | RString of string
 | RPointer of int
@@ -119,6 +120,7 @@ type data =
 
 type obj =
 | Struct of int * data array (* tag × data *)
+| Int63 of Uint63.t (* Primitive integer *)
 | String of string
 
 module type Input =
@@ -255,6 +257,28 @@ let input_header64 chan =
   in
   (tag, len)
 
+let input_cstring chan : string =
+  let buff = Buffer.create 17 in
+  let rec loop () =
+    match input_char chan with
+    | '\o000' -> Buffer.contents buff
+    | c -> Buffer.add_char buff c |> loop
+  in loop ()
+
+let input_intL chan : int64 =
+  let i = input_byte chan in
+  let j = input_byte chan in
+  let k = input_byte chan in
+  let l = input_byte chan in
+  let m = input_byte chan in
+  let n = input_byte chan in
+  let o = input_byte chan in
+  let p = input_byte chan in
+  let ( lsl ) x y = Int64.(shift_left (of_int x) y) in
+  let ( lor ) = Int64.logor in
+  (i lsl 56) lor (j lsl 48) lor (k lsl 40) lor (l lsl 32) lor
+  (m lsl 24) lor (n lsl 16) lor (o lsl 8) lor (Int64.of_int p)
+
 let parse_object chan =
   let data = input_byte chan in
   if prefix_small_block <= data then
@@ -297,6 +321,11 @@ let parse_object chan =
     let addr = input_int32u chan in
     for _i = 0 to 15 do ignore (input_byte chan); done;
     RCode addr
+  | CODE_CUSTOM ->
+    begin match input_cstring chan with
+    | "_j" -> RInt63 (Uint63.of_int64 (input_intL chan))
+    | s -> Printf.eprintf "Unhandled custom code: %s" s; assert false
+    end
   | CODE_DOUBLE_ARRAY32_LITTLE
   | CODE_DOUBLE_BIG
   | CODE_DOUBLE_LITTLE
@@ -304,8 +333,7 @@ let parse_object chan =
   | CODE_DOUBLE_ARRAY8_LITTLE
   | CODE_DOUBLE_ARRAY32_BIG
   | CODE_INFIXPOINTER
-  | CODE_CUSTOM ->
-    Printf.eprintf "Unhandled code %04x\n%!" data; assert false
+    -> Printf.eprintf "Unhandled code %04x\n%!" data; assert false
 
 let parse chan =
   let (magic, len, _, _, size) = parse_header chan in
@@ -337,6 +365,11 @@ let parse chan =
   | RCode addr ->
     let data = Fun addr in
     data, None
+  | RInt63 i ->
+    let data = Ptr !current_object in
+    let () = LargeArray.set memory !current_object (Int63 i) in
+    let () = incr current_object in
+    data, None
   in
 
   let rec fill block off accu =
@@ -400,6 +433,7 @@ let instantiate (p, mem) =
   for i = 0 to len - 1 do
     let obj = match LargeArray.get mem i with
     | Struct (tag, blk) -> Obj.new_block tag (Array.length blk)
+    | Int63 i -> Obj.repr i
     | String str -> Obj.repr str
     in
     LargeArray.set ans i obj
@@ -418,6 +452,7 @@ let instantiate (p, mem) =
       for k = 0 to Array.length blk - 1 do
         Obj.set_field obj k (get_data blk.(k))
       done
+    | Int63 _
     | String _ -> ()
   done;
   get_data p
diff --git a/checker/analyze.mli b/checker/analyze.mli
index d7770539df..029f595959 100644
--- a/checker/analyze.mli
+++ b/checker/analyze.mli
@@ -1,3 +1,4 @@
+(** Representation of data allocated on the OCaml heap. *)
 type data =
 | Int of int
 | Ptr of int
@@ -6,6 +7,7 @@ type data =
 
 type obj =
 | Struct of int * data array (* tag × data *)
+| Int63 of Uint63.t (* Primitive integer *)
 | String of string
 
 module LargeArray :
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 086dd17e39..c33c6d5d09 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -66,6 +66,7 @@ let mk_mtb mp sign delta =
 
 let rec check_module env mp mb =
   Flags.if_verbose Feedback.msg_notice (str "  checking module: " ++ str (ModPath.to_string mp));
+  let env = Modops.add_retroknowledge mb.mod_retroknowledge env in
   let (_:module_signature) =
     check_signature env mb.mod_type mb.mod_mp mb.mod_delta
   in
diff --git a/checker/safe_checking.ml b/checker/safe_checking.ml
index 6dc2953060..4a64039e30 100644
--- a/checker/safe_checking.ml
+++ b/checker/safe_checking.ml
@@ -16,6 +16,7 @@ let import senv clib univs digest =
   let env = Safe_typing.env_of_safe_env senv in
   let env = push_context_set ~strict:true mb.mod_constraints env in
   let env = push_context_set ~strict:true univs env in
+  let env = Modops.add_retroknowledge mb.mod_retroknowledge env in
   Mod_checking.check_module env mb.mod_mp mb;
   let (_,senv) = Safe_typing.import clib univs digest senv in senv
 
diff --git a/checker/validate.ml b/checker/validate.ml
index b85944f94f..72cf38ebe6 100644
--- a/checker/validate.ml
+++ b/checker/validate.ml
@@ -86,6 +86,7 @@ let rec val_gen v ctx o = match v with
   | Annot (s,v) -> val_gen v (ctx/CtxAnnot s) o
   | Dyn -> val_dyn ctx o
   | Proxy { contents = v } -> val_gen v ctx o
+  | Uint63 -> val_uint63 ctx o
 
 (* Check that an object is a tuple (or a record). vs is an array of
    value representation for each field. Its size corresponds to the
@@ -133,6 +134,10 @@ and val_array v ctx o =
     val_gen v ctx (Obj.field o i)
   done
 
+and val_uint63 ctx o =
+  if not (Uint63.is_uint63 o) then
+    fail ctx o "not a 63-bit unsigned integer"
+
 let print_frame = function
 | CtxType t -> t
 | CtxAnnot t -> t
diff --git a/checker/values.ml b/checker/values.ml
index 1afe764ca4..7ca2dc8050 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -34,6 +34,7 @@ type value =
   | Dyn
 
   | Proxy of value ref
+  | Uint63
 
 let fix (f : value -> value) : value =
   let self = ref Any in
@@ -151,7 +152,8 @@ let rec v_constr =
     [|v_caseinfo;v_constr;v_constr;Array v_constr|]; (* Case *)
     [|v_fix|]; (* Fix *)
     [|v_cofix|]; (* CoFix *)
-    [|v_proj;v_constr|] (* Proj *)
+    [|v_proj;v_constr|]; (* Proj *)
+    [|Uint63|] (* Int *)
   |])
 
 and v_prec = Tuple ("prec_declaration",
@@ -214,9 +216,12 @@ let v_oracle =
 let v_pol_arity =
   v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ|]
 
+let v_primitive =
+  v_enum "primitive" 25
+
 let v_cst_def =
   v_sum "constant_def" 0
-    [|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]|]
+    [|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]; [|v_primitive|]|]
 
 let v_typing_flags =
   v_tuple "typing_flags" [|v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool; v_bool|]
@@ -288,6 +293,20 @@ let v_ind_pack = v_tuple "mutual_inductive_body"
     Opt v_bool;
     v_typing_flags|]
 
+let v_prim_ind = v_enum "prim_ind" 4
+
+let v_prim_type = v_enum "prim_type" 1
+
+let v_retro_action =
+  v_sum "retro_action" 0 [|
+    [|v_prim_ind; v_ind|];
+    [|v_prim_type; v_cst|];
+    [|v_cst|];
+  |]
+
+let v_retroknowledge =
+  v_sum "module_retroknowledge" 1 [|[|List v_retro_action|]|]
+
 let rec v_mae =
   Sum ("module_alg_expr",0,
   [|[|v_mp|];         (* SEBident *)
@@ -318,7 +337,7 @@ and v_impl =
 and v_noimpl = v_unit
 and v_module =
   Tuple ("module_body",
-         [|v_mp;v_impl;v_sign;Opt v_mexpr;v_context_set;v_resolver;Any|])
+         [|v_mp;v_impl;v_sign;Opt v_mexpr;v_context_set;v_resolver;v_retroknowledge|])
 and v_modtype =
   Tuple ("module_type_body",
          [|v_mp;v_noimpl;v_sign;Opt v_mexpr;v_context_set;v_resolver;v_unit|])
diff --git a/checker/values.mli b/checker/values.mli
index 616b69907f..2ab8da1928 100644
--- a/checker/values.mli
+++ b/checker/values.mli
@@ -38,6 +38,8 @@ type value =
   | Proxy of value ref
   (** Same as the inner value, used to define recursive types *)
 
+  | Uint63
+
 (** NB: List and Opt have their own constructors to make it easy to
    define eg [let rec foo = List foo]. *)
 
diff --git a/checker/votour.ml b/checker/votour.ml
index 3c088b59b5..36014cde73 100644
--- a/checker/votour.ml
+++ b/checker/votour.ml
@@ -100,6 +100,7 @@ struct
             init_size seen (fun n -> fold (succ i) (accu + 1 + n) k) os.(i)
         in
         fold 0 1 (fun size -> let () = LargeArray.set !sizes p size in k size)
+      | Int63 _ -> k 0
       | String s ->
         let size = 2 + (String.length s / ws) in
         let () = LargeArray.set !sizes p size in
@@ -116,6 +117,7 @@ struct
   | Ptr p ->
     match LargeArray.get !memory p with
     | Struct (tag, os) -> BLOCK (tag, os)
+    | Int63 _ -> OTHER (* TODO: pretty-print int63 values *)
     | String s -> STRING s
 
   let input ch =
@@ -153,6 +155,7 @@ let rec get_name ?(extra=false) = function
   |Annot (s,v) -> s^"/"^get_name ~extra v
   |Dyn -> "<dynamic>"
   | Proxy v -> get_name ~extra !v
+  | Uint63 -> "Uint63"
 
 (** For tuples, its quite handy to display the inner 1st string (if any).
     Cf. [structure_body] for instance *)
@@ -257,6 +260,7 @@ let rec get_children v o pos = match v with
     end
   |Fail s -> raise Forbidden
   | Proxy v -> get_children !v o pos
+  | Uint63 -> raise Exit
 
 let get_children v o pos =
   try get_children v o pos