3 files changed, 28 insertions, 0 deletions
diff --git a/lib/generic_equality.sail b/lib/generic_equality.sail
new file mode 100644
index 00000000..22bd778e
--- /dev/null
+++ b/lib/generic_equality.sail
@@ -0,0 +1,16 @@
+$ifndef _GENERIC_EQUALITY
+$define _GENERIC_EQUALITY
+
+$include <flow.sail>
+
+val eq_anything = {ocaml: "(fun (x, y) -> x = y)", interpreter: "eq_anything", lem: "eq", coq: "generic_eq", c: "eq_anything"} : forall ('a : Type). ('a, 'a) -> bool
+
+overload operator == = {eq_anything}
+
+val neq_anything : forall ('a : Type). ('a, 'a) -> bool
+
+function neq_anything(x, y) = not_bool(eq_anything(x, y))
+
+overload operator != = {neq_anything}
+
+$endif
diff --git a/lib/sail.c b/lib/sail.c
index 94065f0a..11a6c2d8 100644
--- a/lib/sail.c
+++ b/lib/sail.c
@@ -461,6 +461,11 @@ bool EQUAL(fbits)(const fbits op1, const fbits op2)
   return op1 == op2;
 }
 
+bool EQUAL(ref_fbits)(const fbits *op1, const fbits *op2)
+{
+  return *op1 == *op2;
+}
+
 void CREATE(lbits)(lbits *rop)
 {
   rop->bits = sail_malloc(sizeof(mpz_t));
@@ -791,6 +796,11 @@ bool EQUAL(lbits)(const lbits op1, const lbits op2)
   return eq_bits(op1, op2);
 }
 
+bool EQUAL(ref_lbits)(const lbits *op1, const lbits *op2)
+{
+  return eq_bits(*op1, *op2);
+}
+
 bool neq_bits(const lbits op1, const lbits op2)
 {
   assert(op1.len == op2.len);
diff --git a/lib/sail.h b/lib/sail.h
index 0c9b18b5..6de37b0a 100644
--- a/lib/sail.h
+++ b/lib/sail.h
@@ -184,6 +184,7 @@ static inline bool bit_to_bool(const fbits a)
 }
 
 bool EQUAL(fbits)(const fbits, const fbits);
+bool EQUAL(ref_fbits)(const fbits*, const fbits*);
 
 typedef struct {
   uint64_t len;
@@ -277,6 +278,7 @@ void count_leading_zeros(sail_int *rop, const lbits op);
 
 bool eq_bits(const lbits op1, const lbits op2);
 bool EQUAL(lbits)(const lbits op1, const lbits op2);
+bool EQUAL(ref_lbits)(const lbits *op1, const lbits *op2);
 bool neq_bits(const lbits op1, const lbits op2);
 
 void vector_subrange_lbits(lbits *rop,