Merge pull request #119 from aqjune-aws/zarith

Update Codebuild to switch to Zarith, use num instead of Int

arm/proofs/bignum_copy_row_from_table_16_neon.ml

@@ -95,7 +95,7 @@ let ABBREV_TABLE_READ_128BITS_TAC name st ofs =
     else
       let templ0 = `read (memory :> bytes128 (word_add table (word (8 * 16 * i + ofs)):int64)) s0`
  in
-      let newofs = mk_numeral (Int ofs) in
+      let newofs = mk_numeral (num ofs) in
       subst [(newofs,`ofs:num`)] templ0 in
   let rhs = subst [(mk_var(st,`:armstate`),`st0:armstate`)] templ in
   ABBREV_TAC (mk_eq (v,rhs));;

arm/proofs/bignum_copy_row_from_table_32_neon.ml

@@ -119,7 +119,7 @@ let ABBREV_TABLE_READ_128BITS_TAC name st ofs =
     else
       let templ0 = `read (memory :> bytes128 (word_add table (word (8 * 32 * i + ofs)):int64)) s0`
  in
-      let newofs = mk_numeral (Int ofs) in
+      let newofs = mk_numeral (num ofs) in
       subst [(newofs,`ofs:num`)] templ0 in
   let rhs = subst [(mk_var(st,`:armstate`),`st0:armstate`)] templ in
   ABBREV_TAC (mk_eq (v,rhs));;

arm/proofs/bignum_copy_row_from_table_8n_neon.ml

@@ -217,7 +217,7 @@ let ABBREV_Z_READ_128BITS_TAC name stname ofs =
       `read (memory :> bytes128 (word_add z (word (8 * (val (width:int64) - 8 * (i' + 1)))):int64)) s0`
     else
       let templ0 = `read (memory :> bytes128 (word_add z (word (8 * (val (width:int64) - 8 * (i' + 1)) + ofs)):int64)) s0` in
-      let newofs = mk_numeral (Int ofs) in
+      let newofs = mk_numeral (num ofs) in
       subst [(newofs,`ofs:num`)] templ0 in
   let rhs = subst [(mk_var(stname, `:armstate`),`st0:armstate`)] templ in
   ABBREV_TAC (mk_eq (v,rhs));;
@@ -231,7 +231,7 @@ let ABBREV_TABLE_READ_128BITS_TAC name stname ofs =
     else
       let templ0 = `read (memory :> bytes128 (word_add table
             (word (8 * (i * val (width:int64) + val (width:int64) - 8 * (i' + 1)) + ofs)):int64)) s0` in
-      let newofs = mk_numeral (Int ofs) in
+      let newofs = mk_numeral (num ofs) in
       subst [(newofs,`ofs:num`)] templ0 in
   let rhs = subst [(mk_var(stname, `:armstate`),`st0:armstate`)] templ in
   ABBREV_TAC (mk_eq (v,rhs));;

arm/proofs/bignum_mul_8_16_neon.ml

@@ -831,16 +831,16 @@ let BIGNUM_MUL_8_16_NEON_CORRECT = prove(
       CONV_TAC (ONCE_DEPTH_CONV (NUM_MULT_CONV ORELSEC NUM_ADD_CONV)) THEN
     MAP_EVERY (fun t -> ASSUME_TAC (SPEC t VAL_BOUND_64)) [`x:int64`;`y:int64`;`z:int64`] THEN
     MAP_EVERY (fun (v:term) ->
-        ASM_CASES_TAC (mk_binary "<" (v,mk_numeral (Num.Int 1984))) THEN
-        ASM_CASES_TAC (mk_binary "<" (v,mk_numeral (Num.Int (2*1984)))) THEN
-        ASM_CASES_TAC (mk_binary "<" (v,mk_numeral (Num.Int (3*1984)))))
+        ASM_CASES_TAC (mk_binary "<" (v,mk_numeral (num 1984))) THEN
+        ASM_CASES_TAC (mk_binary "<" (v,mk_numeral (num (2*1984)))) THEN
+        ASM_CASES_TAC (mk_binary "<" (v,mk_numeral (num (3*1984)))))
         [`val (x:int64)`;`val (y:int64)`;`val (z:int64)`] THEN
       RULE_ASSUM_TAC (REWRITE_RULE [ARITH_RULE`!x k. ~(x < k) <=> k <= x`]) THEN
       TRY ASM_ARITH_TAC (* Remove invalid layouts *) THEN
-      TRY_CONST_PC_TAC (mk_numeral (Num.Int (3 * 1984 + 128))) THEN
-      TRY_CONST_PC_TAC (mk_numeral (Num.Int (2 * 1984 + 128))) THEN
-      TRY_CONST_PC_TAC (mk_numeral (Num.Int (1 * 1984 + 128))) THEN
-      TRY_CONST_PC_TAC (mk_numeral (Num.Int (0 * 1984 + 128)));
+      TRY_CONST_PC_TAC (mk_numeral (num (3 * 1984 + 128))) THEN
+      TRY_CONST_PC_TAC (mk_numeral (num (2 * 1984 + 128))) THEN
+      TRY_CONST_PC_TAC (mk_numeral (num (1 * 1984 + 128))) THEN
+      TRY_CONST_PC_TAC (mk_numeral (num (0 * 1984 + 128)));
 
     (** SUBGOAL 2 **)
     ALL_TAC

arm/proofs/bignum_sqr_8_16_neon.ml

@@ -808,14 +808,14 @@ let BIGNUM_SQR_8_16_NEON_CORRECT = prove(
       CONV_TAC (ONCE_DEPTH_CONV (NUM_MULT_CONV ORELSEC NUM_ADD_CONV)) THEN
     MAP_EVERY (fun t -> ASSUME_TAC (SPEC t VAL_BOUND_64)) [`x:int64`;`z:int64`] THEN
     MAP_EVERY (fun (v:term) ->
-        ASM_CASES_TAC (mk_binary "<" (v,mk_numeral (Num.Int 1984))) THEN
-        ASM_CASES_TAC (mk_binary "<" (v,mk_numeral (Num.Int (2*1984)))))
+        ASM_CASES_TAC (mk_binary "<" (v,mk_numeral (num 1984))) THEN
+        ASM_CASES_TAC (mk_binary "<" (v,mk_numeral (num (2*1984)))))
         [`val (x:int64)`;`val (z:int64)`] THEN
       RULE_ASSUM_TAC (REWRITE_RULE [ARITH_RULE`!x k. ~(x < k) <=> k <= x`]) THEN
       TRY ASM_ARITH_TAC (* Remove invalid layouts *) THEN
-      TRY_CONST_PC_TAC (mk_numeral (Num.Int (2 * 1984 + 128))) THEN
-      TRY_CONST_PC_TAC (mk_numeral (Num.Int (1 * 1984 + 128))) THEN
-      TRY_CONST_PC_TAC (mk_numeral (Num.Int (0 * 1984 + 128)));
+      TRY_CONST_PC_TAC (mk_numeral (num (2 * 1984 + 128))) THEN
+      TRY_CONST_PC_TAC (mk_numeral (num (1 * 1984 + 128))) THEN
+      TRY_CONST_PC_TAC (mk_numeral (num (0 * 1984 + 128)));
 
     (** SUBGOAL 2 **)
     ALL_TAC

arm/proofs/decode.ml

@@ -617,13 +617,13 @@ let REG_CONV =
     let wsp = REWRITE_RULE [GSYM WREG_SP; sp] WSP in
     let F spth regth A = Array.mapi (fun i th ->
       if i = 31 then SYM spth else
-      let th' = INST [mk_numeral (Int i),`n:num`] regth in
+      let th' = INST [mk_numeral (num i),`n:num`] regth in
       TRANS (PROVE_HYP (EQT_ELIM (NUM_RED_CONV (hd (hyp th')))) th') th) A in
     F sp xth xs, F wsp wth ws in
   let xs',ws',qs',ds' =
     let F th' A = Array.mapi (fun i ->
       TRANS (CONV_RULE (RAND_CONV (RAND_CONV WORD_RED_CONV))
-        (SPEC (mk_comb (`word:num->5 word`, mk_numeral (Int i))) th'))) A in
+        (SPEC (mk_comb (`word:num->5 word`, mk_numeral (num i))) th'))) A in
     F XREG' xs, F WREG' ws, F QREG' qs,F DREG' ds in
   function
   | Comb(Const("XREG",_),n) -> xs.(Num.int_of_num (dest_numeral n))
@@ -696,7 +696,7 @@ let BINARY_NSUM_CONV =
     let rec go n =
       if n = 0 then PART_MATCH lhs pth0 else
       PART_MATCH lhs (MATCH_MP pthS
-        (NUM_SUC_CONV (mk_comb (`SUC`, mk_numeral (Int (n-1)))))) THENC
+        (NUM_SUC_CONV (mk_comb (`SUC`, mk_numeral (num (n-1)))))) THENC
       COMB2_CONV
         (RATOR_CONV (LAND_CONV (TRY_CONV BETA_CONV THENC conv)) THENC REWRITE_CONV [])
         (go (n-1)) THENC zero_conv in
@@ -708,8 +708,8 @@ let BINARY_NSUM_CONV =
 let DECODE_BITMASK_CONV =
   let pths = split_32_64 (fun ty -> bool_split (fun n ->
     Array.init 64 (fun r -> Array.init 64 (fun s -> lazy (
-      let r = mk_comb (`word:num->6 word`, mk_numeral (Int r))
-      and s = mk_comb (`word:num->6 word`, mk_numeral (Int s)) in
+      let r = mk_comb (`word:num->6 word`, mk_numeral (num r))
+      and s = mk_comb (`word:num->6 word`, mk_numeral (num s)) in
       CONV_RULE (WORD_REDUCE_CONV THENC
         NUM_REDUCE_CONV THENC ONCE_DEPTH_CONV let_CONV THENC
         NUM_REDUCE_CONV THENC ONCE_DEPTH_CONV let_CONV THENC
@@ -1160,7 +1160,7 @@ let rec decode_all = function
 
 let dest_cons4 =
   let assert_byte n = function
-  | Comb(Const("word",_),a) -> dest_numeral a = Int n
+  | Comb(Const("word",_),a) -> dest_numeral a = num n
   | _ -> false in
   fun n t -> match t with
   | Comb(Comb(Const("CONS",_),a1), Comb(Comb(Const("CONS",_),a2),
@@ -1206,7 +1206,7 @@ let assert_relocs =
   let rec consume_reloc_BL sym = function
     | pc, Comb(Comb(Const("APPEND",_),v),tm)
       when v = vsubst [mk_var(sym,`:num`),`v:num`;
-        mk_numeral (Int pc),`i:num`] ptm -> (pc+4,tm)
+        mk_numeral (num pc),`i:num`] ptm -> (pc+4,tm)
     | _ -> failwith "assert_relocs" in
   fun (args,tm) F ->
     if type_of tm = `:byte list` then
@@ -1417,7 +1417,7 @@ let bignum_madd_mc = define_word_list "bignum_madd_mc"
 let term_of_relocs_arm =
   let reloc_BL = `APPEND (bytelist_of_num 4 (encode_BL (&v - &(pc + i))))` in
   let append_reloc_BL sym add = curry mk_comb (vsubst
-      [sym,`v:num`; mk_numeral (Int add),`i:num`] reloc_BL) in
+      [sym,`v:num`; mk_numeral (num add),`i:num`] reloc_BL) in
   term_of_relocs (fun bs,ty,off,sym,add -> 4,
     match ty, get_int_le bs off 4, add with
     | Arm_call26, 0x94000000, 0 -> append_reloc_BL sym off

arm/proofs/equiv.ml

@@ -496,7 +496,7 @@ let EVENTUALLY_TAKE_STEP_RIGHT_FORALL_TAC
     (exec_decode:thm) (init_st_var:term) (pc_init_ofs:int) (k:int) (n:int):tactic =
   let exec_decode_len,exec_decode_th = CONJ_PAIR exec_decode and
       k4::k4p4::n4::nmk4::nmk::nmkmone4::nmkmone::kpcofs4::k4p4pcofs4::npcofs4::[] =
-    List.map (fun n -> mk_numeral (Int n))
+    List.map (fun n -> mk_numeral (num n))
        [k*4; (k+1)*4; n*4; (n-k)*4; n-k; (n-k-1)*4; n-k-1;
         pc_init_ofs+k*4;pc_init_ofs+(k+1)*4;pc_init_ofs+n*4] in
   let nmk_th = ARITH_RULE
@@ -557,7 +557,7 @@ let EVENTUALLY_STEPS_EXISTS_STEP_TAC (exec_decode:thm) (k:int) (next_pc_ofs:int)
     let pcname = find_pc_varname asl ("s" ^ (string_of_int k)) in
 
     ((if is_numeral nterm then
-      let nminus1 = (dest_numeral nterm) -/ (Num.Int 1) in
+      let nminus1 = (dest_numeral nterm) -/ (num 1) in
       GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [
         ARITH_RULE
         (mk_eq (nterm, mk_binary "+" (`1`, mk_numeral (nminus1))))]
@@ -569,7 +569,7 @@ let EVENTUALLY_STEPS_EXISTS_STEP_TAC (exec_decode:thm) (k:int) (next_pc_ofs:int)
           LABEL_TAC "HARM" th_arm THEN
           MP_TAC th_steps)) THEN
      EXPAND_ARM_AND_UPDATE_BYTES_LOADED_TAC "HARM" exec_decode_th exec_decode_len THEN
-     UPDATE_PC_TAC pcname snextname (mk_numeral (Num.Int next_pc_ofs)) THEN
+     UPDATE_PC_TAC pcname snextname (mk_numeral (num next_pc_ofs)) THEN
      DISCARD_OLDSTATE_TAC snextname
     )
     (asl,g);;
@@ -598,7 +598,7 @@ let ARM_BASIC_STEP'_TAC2 =
     let atm = mk_comb(mk_comb(arm_tm,sv),sv') in
     let eth = ARM_CONV execth2 (map snd asl) atm in
     let stepn = dest_numeral(rand(rator(rator w))) in
-    let stepn_decr = stepn -/ Int 1 in
+    let stepn_decr = stepn -/ num 1 in
     (* stepn = 1+{stepn-1}*)
     let stepn_thm = ARITH_RULE(
       mk_eq(mk_numeral(stepn), mk_binary "+" (`1:num`,mk_numeral(stepn_decr)))) in

arm/proofs/simulator.ml

@@ -58,7 +58,7 @@ let random64() = randomnd 64 (Random.int 65);;
 let random_regstate () =
   let d = Random.int 65 in
   map (fun _ -> randomnd 64 d) (0--30) @
-  [mod_num (random64()) (Int 16)] @
+  [mod_num (random64()) (num 16)] @
   map (fun _ -> randomnd 128 d) (0--31);;
 
 (* ------------------------------------------------------------------------- *)
@@ -73,7 +73,7 @@ let classbit s =
 
 let random_iclass s =
   if String.length s <> 32 then failwith "random_iclass: malformed string"
-  else itlist (fun c n -> classbit c +/ Int 2 */ n) (rev(explode s)) num_0;;
+  else itlist (fun c n -> classbit c +/ num 2 */ n) (rev(explode s)) num_0;;
 
 let random_instruction iclasses =
   let iclass = el (Random.int (length iclasses)) iclasses in
@@ -351,10 +351,10 @@ let run_random_simulation () =
   let _ = printf "random inst: decode %d\n" (Num.int_of_num icode) in
 
   let ibytes =
-    [mod_num icode (Int 256);
-     mod_num (quo_num icode (Int 256)) (Int 256);
-     mod_num (quo_num icode (Int 65536)) (Int 256);
-     quo_num icode (Int 16777216)] in
+    [mod_num icode (num 256);
+     mod_num (quo_num icode (num 256)) (num 256);
+     mod_num (quo_num icode (num 65536)) (num 256);
+     quo_num icode (num 16777216)] in
 
   let ibyteterm =
     mk_flist(map (curry mk_comb `word:num->byte` o mk_numeral) ibytes) in

codebuild/proofs.yml

@@ -5,7 +5,7 @@ phases:
       - curl -sS https://dl.yarnpkg.com/debian/pubkey.gpg | sudo apt-key add -
       - wget -q -O - https://dl.google.com/linux/linux_signing_key.pub | sudo apt-key add - # To resolve apt update GPG error about https://dl.google.com/linux/chrome/deb
       - apt-get update
-      - apt-get -y install ocaml binutils-aarch64-linux-gnu binutils-aarch64-linux-gnu binutils-x86-64-linux-gnu libstring-shellquote-perl
+      - apt-get -y install ocaml binutils-aarch64-linux-gnu binutils-aarch64-linux-gnu binutils-x86-64-linux-gnu libstring-shellquote-perl libgmp-dev
       # Install OPAM
       - wget https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh
       - chmod +x install.sh
@@ -15,7 +15,7 @@ phases:
       - eval $(opam env --switch=4.14.0)
       - echo $(ocamlc -version)
       - opam pin -y add camlp5 8.00.03
-      - opam install -y num
+      - opam install -y zarith
       - echo $(camlp5 -v)
       # Build s2n-bignum
       - cd ${CODEBUILD_SRC_DIR_hol_light}

codebuild/sematests.yml

@@ -4,7 +4,7 @@ phases:
     commands:
       - yum -y install ocaml
       # Perl dependencies for OPAM
-      - yum -y install perl-CPAN
+      - yum -y install perl-CPAN gmp gmp-devel
       - SHELL=/bin/sh perl -MCPAN -e'install "IPC::System::Simple"'
       - SHELL=/bin/sh perl -MCPAN -e'install "String::ShellQuote"'
       # Install OPAM
@@ -16,7 +16,7 @@ phases:
       - eval $(opam env --switch=4.14.0)
       - echo $(ocamlc -version)
       - opam pin -y add camlp5 8.00.03
-      - opam install -y num
+      - opam install -y zarith
       - echo $(camlp5 -v)
       # Build s2n-bignum
       - cd ${CODEBUILD_SRC_DIR_hol_light}

common/components.ml

@@ -2757,7 +2757,7 @@ let (NONOVERLAPPING_TAC:tactic) =
         (BINOP_CONV (mk_theorem n) THENC
           PART_MATCH lhs (SYM (SPEC_ALL LEFT_ADD_DISTRIB))) t
       | Comb(Comb(Const("*",_),t1),t2) as t ->
-        if try dest_numeral t1 = Int n with _ -> false then REFL t else
+        if try dest_numeral t1 = num n with _ -> false then REFL t else
         let n1 = gcd n (factor t1) in let n2 = n / n1 in
         (BINOP2_CONV (mk_theorem n1) (mk_theorem n2) THENC
           PART_MATCH lhs MULT_ASSOC4 THENC LAND_CONV NUM_MULT_CONV) t

common/elf.ml

@@ -102,7 +102,7 @@ let term_of_list_int,app_term_of_int_fun,term_of_int_fun =
   and nil = `NIL:byte list`
   and cons = `CONS:byte->byte list->byte list` in
   let cons_word n e =
-    mk_comb (mk_comb (cons, mk_comb (word, mk_numeral (Int n))), e) in
+    mk_comb (mk_comb (cons, mk_comb (word, mk_numeral (num n))), e) in
   let app_term_of_int_fun f start end_ =
     let rec go n e =
       if n = start then e else

common/words2.ml

@@ -392,10 +392,10 @@ let READ_WORD_CONV =
 
   let nsa0 = Array.init 256 (fun i ->
     NUM_SHIFT_ADD_CONV (mk_comb (mk_comb (mk_comb (`num_shift_add`,
-      mk_numeral (Int i)), `0`), `8`)))
+      mk_numeral (num i)), `0`), `8`)))
   and nsaS = Array.init 256 (fun i ->
     NUM_SHIFT_ADD_CONV (mk_comb (mk_comb (mk_comb (`num_shift_add`,
-      mk_numeral (Int i)), `NUMERAL r`), `8`))) in
+      mk_numeral (num i)), `NUMERAL r`), `8`))) in
   let num_shift_add_conv a' r' = match rand r' with
   | Const("_0",_) -> nsa0.(Num.int_of_num (dest_numeral a'))
   | r' -> INST [r',er] nsaS.(Num.int_of_num (dest_numeral a')) in

tests/known_value_testgen.ml

@@ -13,9 +13,9 @@ let print_num n = print_string(string_of_num n);;
 (* Misc convenient functions.                                                *)
 (* ------------------------------------------------------------------------- *)
 
-let num_0 = Int 0 and num_1 = Int 1 and num_2 = Int 2;;
+let num_0 = num 0 and num_1 = num 1 and num_2 = num 2;;
 
-let pow2 n = power_num num_2 (Int n);;
+let pow2 n = power_num num_2 (num n);;
 
 let ( ** ) = fun f g x -> f(g x);;
 
@@ -74,8 +74,8 @@ let rec allpairs f l1 l2 =
 (* ------------------------------------------------------------------------- *)
 
 let rec random_num k =
-  if k <=/ pow2 29 then Int(Random.int(int_of_num(floor_num k)))
-  else Int(Random.int(1 lsl 29)) +/ pow2 29 */ random_num (k // pow2 29);;
+  if k <=/ pow2 29 then num(Random.int(int_of_num(floor_num k)))
+  else num(Random.int(1 lsl 29)) +/ pow2 29 */ random_num (k // pow2 29);;
 
 (* ------------------------------------------------------------------------- *)
 (* The key numbers p and n, some extra mathematical functions.               *)
@@ -119,7 +119,7 @@ let string_of_num_nary =
     and n1 = quo_num n ten in
     let d0 = ell n0 digits in
     if n1 =/ num_0 then d0 else (string_of_num ten n1)^d0 in
-  fun b n -> string_of_num (Int b) n;;
+  fun b n -> string_of_num (num b) n;;
 
 let string_of_padded_hex k n =
   let s = string_of_num_nary 16 (abs_num n) in
@@ -281,7 +281,7 @@ let alltests = (end_itlist (^) ** end_itlist (@))
    (fun x -> mod_num (pow2 384 */ x) p);
 
   unary_tests 100 full "bignum_triple_p384"
-   (fun x -> mod_num (Int 3 */ x) p);
+   (fun x -> mod_num (num 3 */ x) p);
 
 (*** These two are endian-specific. All s2n-bignum numbers are
  *** stored with the words in little-endian order, but the byte