summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/lem_interp/interp_lib.lem30
-rw-r--r--src/type_internal.ml96
2 files changed, 100 insertions, 26 deletions
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index f7b29a33..95fc323d 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -338,6 +338,22 @@ let eq v = match v with
| _ -> Assert_extra.failwith ("eq not given tuple of length 2 " ^ (string_of_value v))
end
+let eq_vec v =
+ let eq_vec_help v1 v2 = match (v1,v2) with
+ | ((V_vector _ _ c1s),(V_vector _ _ c2s)) ->
+ if (List.length c1s = List.length c2s) &&
+ List.listEqualBy
+ (fun v1 v2 -> match eq (V_tuple [v1; v2]) with V_lit (L_aux L_one _) -> true | _ -> false end) c1s c2s then
+ V_lit (L_aux L_one Unknown)
+ else V_lit (L_aux L_zero Unknown)
+ | (V_unknown, _) -> V_unknown
+ | (_, V_unknown) -> V_unknown
+ | _ -> Assert_extra.failwith ("eq_vec not given two vectors, given instead " ^ (string_of_value v)) end in
+ match v with
+ | (V_tuple [v1; v2]) -> binary_taint eq_vec_help v1 v2
+ | _ -> Assert_extra.failwith ("eq_vec not given tuple of length 2 " ^ (string_of_value v))
+end
+
let eq_vec_range v = match v with
| (V_tuple [v; r]) -> eq (V_tuple [to_num Unsigned v; r])
| _ -> Assert_extra.failwith ("eq_vec_range not given tuple of length 2 " ^ (string_of_value v))
@@ -346,10 +362,10 @@ let eq_range_vec v = match v with
| (V_tuple [r; v]) -> eq (V_tuple [r; to_num Unsigned v])
| _ -> Assert_extra.failwith ("eq_range_vec not given tuple of length 2 " ^ (string_of_value v))
end
-let eq_vec_vec v = match v with
+(*let eq_vec_vec v = match v with
| (V_tuple [v;v2]) -> eq (V_tuple [to_num Signed v; to_num Signed v2])
| _ -> Assert_extra.failwith ("eq_vec_vec not given tuple of length 2 " ^ (string_of_value v))
-end
+end*)
let rec neg v = retaint v (match detaint v with
| V_lit (L_aux arg la) ->
@@ -364,7 +380,7 @@ end)
let neq = compose neg eq ;;
-let neq_vec = compose neg eq_vec_vec
+let neq_vec = compose neg eq_vec
let arith_op op v =
let fail () = Assert_extra.failwith ("arith_op given unexpected " ^ (string_of_value v)) in
@@ -918,9 +934,17 @@ let library_functions direction = [
("quot_overflow_vec_signed", arith_op_overflow_vec_no0 hardware_quot "quot" Signed 1);
("power", arith_op power);
("eq", eq);
+ ("eq_vec", eq_vec);
("eq_vec_range", eq_vec_range);
("eq_range_vec", eq_range_vec);
+ ("eq_bit", eq);
+ ("eq_range", eq);
("neq", neq);
+ ("neq_vec", neq_vec);
+ ("neq_vec_range", neq);
+ ("neq_range_vec", neq);
+ ("neq_bit", neq);
+ ("neq_range", neq);
("vec_concat", vec_concat);
("is_one", is_one);
("to_num", to_num Unsigned);
diff --git a/src/type_internal.ml b/src/type_internal.ml
index b9cde124..a5c7e1c2 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -2357,32 +2357,82 @@ let initial_typ_env =
(*Correct types again*)
("==",
Overload(
- Base((mk_typ_params ["a";"b"],(mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]) bit_t)),
- (External (Some "eq")),[],pure_e,pure_e,nob),
+ (lib_tannot (mk_typ_params ["a";"b"],(mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]) bit_t))
+ (Some "eq") []),
false,
- [Base((mk_nat_params["n";"m";],
- mk_pure_fun (mk_tup [mk_atom (mk_nv "n") ;mk_atom (mk_nv "m")]) bit_t),
- (External (Some "eq")),
- [Predicate(Specc(Parse_ast.Int("==",None)),
- Eq(Specc(Parse_ast.Int("==",None)), mk_nv "n", mk_nv "m"),
- NtEq(Specc(Parse_ast.Int("==",None)), mk_nv "n", mk_nv "m"))],
- pure_e,pure_e,nob);
+ [(*== : 'a['m] * 'a['m] -> bit_t *)
+ lib_tannot ((mk_nat_params["n";"m";"o"]@mk_typ_params["a"]@mk_ord_params["ord"]),
+ (mk_pure_fun (mk_tup [mk_vector {t=Tvar "a"} (mk_ovar "ord") (mk_nv "n") (mk_nv "m");
+ mk_vector {t=Tvar "a"} (mk_ovar "ord") (mk_nv "o") (mk_nv "m")])
+ bit_t))
+ (Some "eq_vec")
+ [];
(* == : bit['n] * [:'o:] -> bit_t *)
- Base(((mk_nat_params ["n";"m";"o"])@(mk_ord_params ["ord"]),
- (mk_pure_fun (mk_tup [mk_atom (mk_nv "o");
- mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m")])
- bit_t)),
- (External (Some "eq_range_vec")),[],pure_e,pure_e,nob);
+ lib_tannot ((mk_nat_params ["n";"m";"o"])@(mk_ord_params ["ord"]),
+ (mk_pure_fun (mk_tup [mk_atom (mk_nv "o");
+ mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m")])
+ bit_t))
+ (Some "eq_range_vec")
+ [];
(* == : [:'o:] * bit['n] -> bit_t *)
- Base(((mk_nat_params ["n";"m";"o"])@(mk_ord_params ["ord"]),
- (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m");
- mk_atom (mk_nv "o")])
- bit_t)),
- (External (Some "eq_vec_range")),[],pure_e,pure_e,nob);
- Base((["a",{k=K_Typ}],(mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "a"}]) bit_t)),
- (External (Some "eq")),[],pure_e,pure_e,nob)]));
- ("!=",Base((["a",{k=K_Typ}; "b",{k=K_Typ}], (mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]) bit_t)),
- (External (Some "neq")),[],pure_e,pure_e,nob));
+ lib_tannot ((mk_nat_params ["n";"m";"o"])@(mk_ord_params ["ord"]),
+ (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m");
+ mk_atom (mk_nv "o")])
+ bit_t))
+ (Some "eq_vec_range")
+ [];
+ (* == : [:'n:] * [:'m:] -> bit_t *)
+ lib_tannot ((mk_nat_params["n";"m";],
+ mk_pure_fun (mk_tup [mk_atom (mk_nv "n") ;mk_atom (mk_nv "m")]) bit_t))
+ (Some "eq_range")
+ [Predicate(Specc(Parse_ast.Int("==",None)),
+ Eq(Specc(Parse_ast.Int("==",None)), mk_nv "n", mk_nv "m"),
+ NtEq(Specc(Parse_ast.Int("==",None)), mk_nv "n", mk_nv "m"))];
+ (* == : (bit_t,bit_t) -> bit_t *)
+ lib_tannot ([], mk_pure_fun (mk_tup [bit_t;bit_t]) bit_t)
+ (Some "eq_bit")
+ [];
+ lib_tannot (["a",{k=K_Typ}],(mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "a"}]) bit_t))
+ (Some "eq") []]));
+ ("!=",
+ Overload(
+ lib_tannot ((mk_typ_params ["a";"b"]),(mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]) bit_t))
+ (Some "neq") [],
+ false,
+ [(*!= : 'a['m] * 'a['m] -> bit_t *)
+ lib_tannot ((mk_nat_params["n";"m";"o"]@mk_typ_params["a"]@mk_ord_params["ord"]),
+ (mk_pure_fun (mk_tup [mk_vector {t=Tvar "a"} (mk_ovar "ord") (mk_nv "n") (mk_nv "m");
+ mk_vector {t=Tvar "a"} (mk_ovar "ord") (mk_nv "o") (mk_nv "m")])
+ bit_t))
+ (Some "neq_vec")
+ [];
+ (* != : bit['n] * [:'o:] -> bit_t *)
+ lib_tannot ((mk_nat_params ["n";"m";"o"])@(mk_ord_params ["ord"]),
+ (mk_pure_fun (mk_tup [mk_atom (mk_nv "o");
+ mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m")])
+ bit_t))
+ (Some "neq_range_vec")
+ [];
+ (* != : [:'o:] * bit['n] -> bit_t *)
+ lib_tannot ((mk_nat_params ["n";"m";"o"])@(mk_ord_params ["ord"]),
+ (mk_pure_fun (mk_tup [mk_vector bit_t (mk_ovar "ord") (mk_nv "n") (mk_nv "m");
+ mk_atom (mk_nv "o")])
+ bit_t))
+ (Some "neq_vec_range")
+ [];
+ (* != : [:'n:] * [:'m:] -> bit_t *)
+ lib_tannot ((mk_nat_params["n";"m";],
+ mk_pure_fun (mk_tup [mk_atom (mk_nv "n") ;mk_atom (mk_nv "m")]) bit_t))
+ (Some "neq_range")
+ [Predicate(Specc(Parse_ast.Int("!=",None)),
+ Eq(Specc(Parse_ast.Int("!=",None)), mk_nv "n", mk_nv "m"),
+ NtEq(Specc(Parse_ast.Int("!=",None)), mk_nv "n", mk_nv "m"))];
+ (* != : (bit_t,bit_t) -> bit_t *)
+ lib_tannot ([], mk_pure_fun (mk_tup [bit_t;bit_t]) bit_t)
+ (Some "neq_bit")
+ [];
+ lib_tannot (["a",{k=K_Typ}],(mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "a"}]) bit_t))
+ (Some "neq") []]));
("<",
Overload(
Base((["a",{k=K_Typ};"b",{k=K_Typ}],(mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]) bit_t)),
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 08:42:26 +0000