Integers as default

.github/workflows/proof.yml

@@ -94,10 +94,11 @@ jobs:
         opam install --yes cn
 
     - name: Checkout cn-tutorial
-      uses: actions/checkout@v6
+      uses: actions/checkout@v7
       with:
         repository: rems-project/cn-tutorial
         path: cn-tutorial
+	ref: fix-integers       # remove once the PR is ready
 
     - name: Run CN tests
       run: |

bin/verify.ml

@@ -43,6 +43,7 @@ let verify
       allow_split_magic_comments
       disable_derived_lc1
       try_hard
+      always_interp
       disable_unfold_multiclause_preds
       check_consistency (* integermode *)
   =
@@ -67,6 +68,7 @@ let verify
   Solver.solver_type := solver_type;
   Solver.solver_flags := solver_flags;
   Solver.try_hard := try_hard;
+  Solver.always_interp := always_interp;
   Solver.inc_enabled := solver_inc_enabled;
   Solver.inc_timeout := solver_inc_timeout;
   Solver.hybrid := solver_hybrid;
@@ -99,13 +101,13 @@ let verify
     ~skip_label_inlining:false
     ~handle_error:(Common.handle_type_error ~json ?output_dir ~serialize_json:json_trace)
     ~f:(fun ~cabs_tunit:_ ~prog5:_ ~ail_prog:_ ~statement_locs:_ ~paused ->
-      let check (functions, global_var_constraints, lemmas) =
+      let check (functions, constraints_to_add, lemmas) =
         let open Typing in
         let@ errors =
           Check.time_check_c_functions
             (skip, only)
             check_consistency
-            (global_var_constraints, functions)
+            (constraints_to_add, functions)
         in
         if not quiet then
           List.iter
@@ -203,6 +205,11 @@ module Flags = struct
     Arg.(value & flag & info ~docs:s_verification [ "try-hard" ] ~doc)
 
 
+  let always_interp =
+    let doc = "Always use interpreted functions, even for NIA." in
+    Arg.(value & flag & info ~docs:s_verification [ "always-interp" ] ~doc)
+
+
   let only =
     let doc = "Only type-check this function (or comma-separated names)" in
     Arg.(value & opt (list string) [] & info ~docs:s_verification [ "only" ] ~doc)
@@ -350,6 +357,7 @@ let verify_t : unit Term.t =
   $ Common.Flags.allow_split_magic_comments
   $ Flags.disable_derived_lc1
   $ Flags.try_hard
+  $ Flags.always_interp
   $ Flags.disable_unfold_multiclause_preds
   $ Flags.check_consistency
 

coq/Cn/Terms.v

@@ -29,6 +29,7 @@ Inductive const : Type :=
 
 (* Unary operators *)
 Inductive unop : Type :=
+  | Abs : unop
   | Not : unop
   | Negate : unop
   | BW_CLZ : unop

lib/baseTypes.ml

@@ -1,4 +1,4 @@
-let cnBV = ref true
+let cnBV = ref false
 
 type sign =
   | Signed

lib/builtins.ml

@@ -80,7 +80,8 @@ let min_bits_def (sign, n) =
     | Signed -> (Z.(neg @@ shift_left one (Int.sub n 1)), "i")
   in
   let name = "MIN" ^ letter ^ Int.to_string n in
-  MT.num_lit_ num (BT.Bits (sign, n)) loc |> mk_builtin_arg0 name
+  let bt = if !BT.cnBV then BT.Bits (sign, n) else Integer in
+  MT.num_lit_ num bt loc |> mk_builtin_arg0 name
 
 
 let max_bits_def (sign, n) =
@@ -90,7 +91,8 @@ let max_bits_def (sign, n) =
     | Signed -> (Z.(shift_left one (Int.sub n 1) - one), "i")
   in
   let name = "MAX" ^ letter ^ Int.to_string n in
-  MT.num_lit_ num (BT.Bits (sign, n)) loc |> mk_builtin_arg0 name
+  let bt = if !BT.cnBV then BT.Bits (sign, n) else Integer in
+  MT.num_lit_ num bt loc |> mk_builtin_arg0 name
 
 
 let max_min_bits =
@@ -176,6 +178,8 @@ let power_def =
     mk_arg2 (fun (it, it') loc -> MT.binop Exp (it, it') loc (Terms.get_bt it)) )
 
 
+let abs_def = ("abs", Sym.fresh "abs", mk_arg1 (fun it loc -> MT.arith_unop Abs it loc))
+
 let rem_def =
   ( "rem",
     Sym.fresh "rem",
@@ -209,6 +213,7 @@ let builtin_funs
     shift_left_def;
     shift_right_def;
     power_def;
+    abs_def;
     rem_def;
     mod_def;
     has_alloc_id_def;

lib/cLogicalFuns.ml

@@ -789,8 +789,19 @@ let add_logical_funs_from_c call_funinfo funs_to_convert funs =
   let@ conv_defs =
     ListM.mapM
       (fun Mu.{ c_fun_sym; loc; l_fun_sym } ->
-         if not !BT.cnBV then
-           failwith "todo: deriving CN function from C function in integer-mode";
+         let@ () =
+           if !BT.cnBV then
+             return ()
+           else
+             fail_n
+               { loc;
+                 msg =
+                   Generic
+                     !^"Deriving CN functions from C functions not yet supported in \
+                        integer-mode."
+                   [@alert "-deprecated"]
+               }
+         in
          let@ def = Global.get_logical_function_def loc l_fun_sym in
          let@ fbody =
            match Pmap.lookup c_fun_sym funs with