changes to compare and equality instances to make lem generate isabelle output

2 files changed, 505 insertions, 108 deletions

diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index adf46803..0fa5730b 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -82,15 +82,34 @@ type opcode = Opcode of list byte (* of length 4 *)
 
 (** typeclass instantiations *)
 
-let bitCompare (b1:bit) (b2:bit) =
+let ~{ocaml} bitCompare (b1:bit) (b2:bit) =
   match (b1,b2) with
   | (Bitc_zero, Bitc_zero) -> EQ
   | (Bitc_one, Bitc_one) -> EQ
   | (Bitc_zero, _) -> LT
   | (_,_) -> GT
   end
+let inline {ocaml} bitCompare = defaultCompare
+
+let ~{ocaml} bitLess b1 b2      = bitCompare b1 b2 =  LT
+let ~{ocaml} bitLessEq b1 b2    = bitCompare b1 b2 <> GT
+let ~{ocaml} bitGreater b1 b2   = bitCompare b1 b2 =  GT
+let ~{ocaml} bitGreaterEq b1 b2 = bitCompare b1 b2 <> LT
+
+let inline {ocaml} bitLess      = defaultLess
+let inline {ocaml} bitLessEq    = defaultLessEq
+let inline {ocaml} bitGreater   = defaultGreater
+let inline {ocaml} bitGreaterEq = defaultGreaterEq
+
+instance (Ord bit)
+  let compare = bitCompare
+  let (<)  = bitLess
+  let (<=) = bitLessEq
+  let (>)  = bitGreater
+  let (>=) = bitGreaterEq
+end
 
-let bit_liftedCompare (bl1:bit_lifted) (bl2:bit_lifted) =
+let ~{ocaml} bit_liftedCompare (bl1:bit_lifted) (bl2:bit_lifted) =
   match (bl1,bl2) with
   | (Bitl_zero, Bitl_zero) -> EQ
   | (Bitl_one, Bitl_one) -> EQ
@@ -101,62 +120,169 @@ let bit_liftedCompare (bl1:bit_lifted) (bl2:bit_lifted) =
   | (Bitl_undef, _) -> LT
   | (_,_) -> GT
   end
+let inline {ocaml} bit_liftedCompare = defaultCompare
+
+let ~{ocaml} bit_liftedLess b1 b2      = bit_liftedCompare b1 b2 =  LT
+let ~{ocaml} bit_liftedLessEq b1 b2    = bit_liftedCompare b1 b2 <> GT
+let ~{ocaml} bit_liftedGreater b1 b2   = bit_liftedCompare b1 b2 =  GT
+let ~{ocaml} bit_liftedGreaterEq b1 b2 = bit_liftedCompare b1 b2 <> LT
+
+let inline {ocaml} bit_liftedLess      = defaultLess
+let inline {ocaml} bit_liftedLessEq    = defaultLessEq
+let inline {ocaml} bit_liftedGreater   = defaultGreater
+let inline {ocaml} bit_liftedGreaterEq = defaultGreaterEq
 
 instance (Ord bit_lifted)
   let compare = bit_liftedCompare
-  let (<)  b1 b2 = (bit_liftedCompare b1 b2) = LT
-  let (<=) b1 b2 = (bit_liftedCompare b1 b2) <> GT
-  let (>)  b1 b2 = (bit_liftedCompare b1 b2) = GT
-  let (>=) b1 b2 = (bit_liftedCompare b1 b2) <> LT
- end
+  let (<)  = bit_liftedLess
+  let (<=) = bit_liftedLessEq
+  let (>)  = bit_liftedGreater
+  let (>=) = bit_liftedGreaterEq
+end
+
+let ~{ocaml} byte_liftedCompare (Byte_lifted b1) (Byte_lifted b2) = compare b1 b2
+let inline {ocaml} byte_liftedCompare = defaultCompare
+
+let ~{ocaml} byte_liftedLess b1 b2      = byte_liftedCompare b1 b2 =  LT
+let ~{ocaml} byte_liftedLessEq b1 b2    = byte_liftedCompare b1 b2 <> GT
+let ~{ocaml} byte_liftedGreater b1 b2   = byte_liftedCompare b1 b2 =  GT
+let ~{ocaml} byte_liftedGreaterEq b1 b2 = byte_liftedCompare b1 b2 <> LT
+
+let inline {ocaml} byte_liftedLess      = defaultLess
+let inline {ocaml} byte_liftedLessEq    = defaultLessEq
+let inline {ocaml} byte_liftedGreater   = defaultGreater
+let inline {ocaml} byte_liftedGreaterEq = defaultGreaterEq
 
 instance (Ord byte_lifted)
-  let compare = defaultCompare
-  let (<) = defaultLess
-  let (>) = defaultGreater
-  let (<=) = defaultLessEq
-  let (>=) = defaultGreaterEq
+  let compare = byte_liftedCompare
+  let (<)  = byte_liftedLess
+  let (<=) = byte_liftedLessEq
+  let (>)  = byte_liftedGreater
+  let (>=) = byte_liftedGreaterEq
 end
 
+let ~{ocaml} byteCompare (Byte b1) (Byte b2) = compare b1 b2
+let inline {ocaml} byteCompare = defaultCompare
+
+let ~{ocaml} byteLess b1 b2      = byteCompare b1 b2 =  LT
+let ~{ocaml} byteLessEq b1 b2    = byteCompare b1 b2 <> GT
+let ~{ocaml} byteGreater b1 b2   = byteCompare b1 b2 =  GT
+let ~{ocaml} byteGreaterEq b1 b2 = byteCompare b1 b2 <> LT
+
+let inline {ocaml} byteLess      = defaultLess
+let inline {ocaml} byteLessEq    = defaultLessEq
+let inline {ocaml} byteGreater   = defaultGreater
+let inline {ocaml} byteGreaterEq = defaultGreaterEq
+
 instance (Ord byte)
-  let compare = defaultCompare
-  let (<) = defaultLess
-  let (>) = defaultGreater
-  let (<=) = defaultLessEq
-  let (>=) = defaultGreaterEq
-end  
-
-let addressCompare (Address b1 i1) (Address b2 i2) = pairCompare compare compare (b1,i1) (b2,i2)
+  let compare = byteCompare
+  let (<)  = byteLess
+  let (<=) = byteLessEq
+  let (>)  = byteGreater
+  let (>=) = byteGreaterEq
+end
+
+let ~{ocaml} addressCompare (Address b1 i1) (Address b2 i2) = compare (b1,i1) (b2,i2)
+let inline {ocaml} addressCompare = defaultCompare
+
+let ~{ocaml} addressLess b1 b2      = addressCompare b1 b2 =  LT
+let ~{ocaml} addressLessEq b1 b2    = addressCompare b1 b2 <> GT
+let ~{ocaml} addressGreater b1 b2   = addressCompare b1 b2 =  GT
+let ~{ocaml} addressGreaterEq b1 b2 = addressCompare b1 b2 <> LT
+
+let inline {ocaml} addressLess      = defaultLess
+let inline {ocaml} addressLessEq    = defaultLessEq
+let inline {ocaml} addressGreater   = defaultGreater
+let inline {ocaml} addressGreaterEq = defaultGreaterEq
+
 instance (Ord address)
   let compare = addressCompare
-  let (<)  a1 a2 = (addressCompare a1 a2) = LT
-  let (<=) a1 a2 = (addressCompare a1 a2) <> GT
-  let (>)  a1 a2 = (addressCompare a1 a2) = GT
-  let (>=) a1 a2 = (addressCompare a1 a2) <> LT
+  let (<)  = addressLess
+  let (<=) = addressLessEq
+  let (>)  = addressGreater
+  let (>=) = addressGreaterEq
 end
 
-let addressEqual a1 a2 = (addressCompare a1 a2) = EQ
+let {coq} addressEqual a1 a2 = (addressCompare a1 a2) = EQ
+let inline ~{coq} addressEqual = unsafe_structural_equality
+
+let {coq} addressInequal a1 a2 = not (addressEqual a1 a2)
+let inline ~{coq} addressInequal = unsafe_structural_inequality
 
 instance  (Eq address)
-  let (=) = addressEqual
-  let (<>) x y = not (addressEqual x y)
+  let (=)  = addressEqual
+  let (<>) = addressInequal
+end
+
+let ~{ocaml} directionCompare d1 d2 =
+  match (d1, d2) with
+  | (D_decreasing, D_increasing) -> GT
+  | (D_increasing, D_decreasing) -> LT
+  | _ -> EQ
+  end
+let inline {ocaml} directionCompare = defaultCompare
+
+let ~{ocaml} directionLess b1 b2      = directionCompare b1 b2 =  LT
+let ~{ocaml} directionLessEq b1 b2    = directionCompare b1 b2 <> GT
+let ~{ocaml} directionGreater b1 b2   = directionCompare b1 b2 =  GT
+let ~{ocaml} directionGreaterEq b1 b2 = directionCompare b1 b2 <> LT
+
+let inline {ocaml} directionLess      = defaultLess
+let inline {ocaml} directionLessEq    = defaultLessEq
+let inline {ocaml} directionGreater   = defaultGreater
+let inline {ocaml} directionGreaterEq = defaultGreaterEq
+
+instance (Ord direction)
+  let compare = directionCompare
+  let (<)  = directionLess
+  let (<=) = directionLessEq
+  let (>)  = directionGreater
+  let (>=) = directionGreaterEq
 end
 
+let ~{ocaml} register_valueCompare rv1 rv2 =
+  compare (rv1.rv_bits, rv1.rv_dir, rv1.rv_start, rv1.rv_start_internal)
+          (rv2.rv_bits, rv2.rv_dir, rv2.rv_start, rv2.rv_start_internal)
+let inline {ocaml} register_valueCompare = defaultCompare
+
+let ~{ocaml} register_valueLess b1 b2      = register_valueCompare b1 b2 =  LT
+let ~{ocaml} register_valueLessEq b1 b2    = register_valueCompare b1 b2 <> GT
+let ~{ocaml} register_valueGreater b1 b2   = register_valueCompare b1 b2 =  GT
+let ~{ocaml} register_valueGreaterEq b1 b2 = register_valueCompare b1 b2 <> LT
+
+let inline {ocaml} register_valueLess      = defaultLess
+let inline {ocaml} register_valueLessEq    = defaultLessEq
+let inline {ocaml} register_valueGreater   = defaultGreater
+let inline {ocaml} register_valueGreaterEq = defaultGreaterEq
 
 instance (Ord register_value)
-  let compare = defaultCompare
-  let (<) = defaultLess
-  let (<=) = defaultLessEq
-  let (>) = defaultGreater
-  let (>=) = defaultGreaterEq
+  let compare = register_valueCompare
+  let (<)  = register_valueLess
+  let (<=) = register_valueLessEq
+  let (>)  = register_valueGreater
+  let (>=) = register_valueGreaterEq
 end
 
+let ~{ocaml} address_liftedCompare (Address_lifted b1 i1) (Address_lifted b2 i2) =
+  compare (b1,i1) (b2,i2)
+let inline {ocaml} address_liftedCompare = defaultCompare
+
+let ~{ocaml} address_liftedLess b1 b2      = address_liftedCompare b1 b2 =  LT
+let ~{ocaml} address_liftedLessEq b1 b2    = address_liftedCompare b1 b2 <> GT
+let ~{ocaml} address_liftedGreater b1 b2   = address_liftedCompare b1 b2 =  GT
+let ~{ocaml} address_liftedGreaterEq b1 b2 = address_liftedCompare b1 b2 <> LT
+
+let inline {ocaml} address_liftedLess      = defaultLess
+let inline {ocaml} address_liftedLessEq    = defaultLessEq
+let inline {ocaml} address_liftedGreater   = defaultGreater
+let inline {ocaml} address_liftedGreaterEq = defaultGreaterEq
+
 instance (Ord address_lifted)
-  let compare = defaultCompare
-  let (<) = defaultLess
-  let (<=) = defaultLessEq
-  let (>) = defaultGreater
-  let (>=) = defaultGreaterEq
+  let compare = address_liftedCompare
+  let (<)  = address_liftedLess
+  let (<=) = address_liftedLessEq
+  let (>)  = address_liftedGreater
+  let (>=) = address_liftedGreaterEq
 end
 
 (* Registers *)
@@ -180,58 +306,54 @@ accessed. The slice specifies where this field is in the register*)
 (* The first four components are as in Reg_field; the final slice
 specifies a part of the field, indexed w.r.t. the register as a whole *)
 
-let slice_eq (s1l,s1r) (s2l,s2r) = (s1l = s2l) && (s1r = s2r)
-
-let reg_nameEqual r1 r2 = 
-  match (r1,r2) with
-  | (Reg s1 ns1 d1 l1, Reg s2 ns2 d2 l2) -> s1=s2 && ns1 = ns2 && l1=l2 && d1=d2
-  | (Reg_slice s1 ns1 d1 sl1, Reg_slice s2 ns2 d2 sl2) -> s1=s2 && ns1=ns2 && d1=d2 && (slice_eq sl1 sl2)
-  | (Reg_field s1 ns1 d1 f1 sl1, Reg_field s2 ns2 d2 f2 sl2) -> s1=s2 && ns1=ns2 && d1=d2 && f1=f2 && (slice_eq sl1 sl2)
-  | (Reg_f_slice s1 ns1 d1 f1 sl1 sl1', Reg_f_slice s2 ns2 d2 f2 sl2 sl2') -> 
-    s1=s2 && ns1=ns2 && d1=d2 && f1=f2 && (slice_eq sl1 sl2) && (slice_eq sl1' sl2')
-  | _ -> false
-  end
-
-instance (Ord direction)
-  let compare = defaultCompare
-  let (<) = defaultLess
-  let (<=) = defaultLessEq
-  let (>) = defaultGreater
-  let (>=) = defaultGreaterEq
-end  
-
-instance  (Eq reg_name)
-  let (=) = reg_nameEqual
-  let (<>) x y = not (reg_nameEqual x y)
-end
-
-let reg_nameCompare r1 r2 = 
+let ~{ocaml} reg_nameCompare r1 r2 = 
   match (r1,r2) with
   | (Reg s1 ns1 nz1 l1, Reg s2 ns2 nz2 l2) -> 
-    quadrupleCompare compare compare compare compare (s1,ns1,nz1,l1) (s2,ns2,nz2,l2)
+     compare (s1,ns1,nz1,l1) (s2,ns2,nz2,l2)
   | (Reg_slice s1 ns1 d1 sl1, Reg_slice s2 ns2 d2 sl2) -> 
-    quadrupleCompare compare compare compare compare (s1,ns1,d1,sl1) (s2,ns2,d2,sl2)
+     compare(s1,ns1,d1,sl1) (s2,ns2,d2,sl2)
   | (Reg_field s1 ns1 d1 f1 sl1, Reg_field s2 ns2 d2 f2 sl2) -> 
-    tripleCompare (tripleCompare compare compare compare) compare compare ((s1,ns1,d2),f1,sl1) ((s2,ns2,d2),f2,sl2)
+     compare ((s1,ns1,d2),f1,sl1) ((s2,ns2,d2),f2,sl2)
   | (Reg_f_slice s1 ns1 d1 f1 sl1 sl1', Reg_f_slice s2 ns2 d2 f2 sl2 sl2') -> 
-    pairCompare (tripleCompare compare compare compare) 
-                (tripleCompare compare compare compare) ((s1,ns1,d1),(f1,sl1,sl1')) ((s2,ns2,d2),(f2,sl2,sl2'))
+     compare ((s1,ns1,d1),(f1,sl1,sl1')) ((s2,ns2,d2),(f2,sl2,sl2'))
   | (Reg _ _ _ _, _)  -> LT
   | (Reg_slice _ _ _ _, _) -> LT
   | (Reg_field _ _ _ _ _, _) -> LT
   | (_, _) -> GT
   end
+let inline {ocaml} reg_nameCompare = defaultCompare
 
-instance (SetType reg_name)
-  let setElemCompare = reg_nameCompare
-end
+let ~{ocaml} reg_nameLess b1 b2      = reg_nameCompare b1 b2 =  LT
+let ~{ocaml} reg_nameLessEq b1 b2    = reg_nameCompare b1 b2 <> GT
+let ~{ocaml} reg_nameGreater b1 b2   = reg_nameCompare b1 b2 =  GT
+let ~{ocaml} reg_nameGreaterEq b1 b2 = reg_nameCompare b1 b2 <> LT
+
+let inline {ocaml} reg_nameLess      = defaultLess
+let inline {ocaml} reg_nameLessEq    = defaultLessEq
+let inline {ocaml} reg_nameGreater   = defaultGreater
+let inline {ocaml} reg_nameGreaterEq = defaultGreaterEq
 
 instance (Ord reg_name)
   let compare = reg_nameCompare
-  let (<)  r1 r2 = (reg_nameCompare r1 r2) = LT
-  let (<=) r1 r2 = (reg_nameCompare r1 r2) <> GT
-  let (>)  r1 r2 = (reg_nameCompare r1 r2) = GT
-  let (>=) r1 r2 = (reg_nameCompare r1 r2) <> LT
+  let (<)  = reg_nameLess
+  let (<=) = reg_nameLessEq
+  let (>)  = reg_nameGreater
+  let (>=) = reg_nameGreaterEq
+end
+
+let {coq} reg_nameEqual a1 a2 = (reg_nameCompare a1 a2) = EQ
+let inline ~{coq} reg_nameEqual = unsafe_structural_equality
+
+let {coq} reg_nameInequal a1 a2 = not (reg_nameEqual a1 a2)
+let inline ~{coq} reg_nameInequal = unsafe_structural_inequality
+
+instance  (Eq reg_name)
+  let (=)  = reg_nameEqual
+  let (<>) = reg_nameInequal
+end
+
+instance (SetType reg_name)
+  let setElemCompare = reg_nameCompare
 end
 
 let direction_of_reg_name r = match r with
@@ -324,31 +446,281 @@ type event =
 | E_error of string (* Should not happen, but may if the symbolic evaluation doesn't work out*)
 
 (* more explicit type classes to work around the occurrences of big_int in reg_name ::no longer necessary?*)
+
+let ~{ocaml} read_kindCompare rk1 rk2 =
+  match (rk1, rk2) with
+  | (Read_plain, Read_plain)             -> EQ
+  | (Read_plain, Read_reserve)           -> LT
+  | (Read_plain, Read_acquire)           -> LT
+  | (Read_plain, Read_exclusive)         -> LT
+  | (Read_plain, Read_exclusive_acquire) -> LT
+  | (Read_plain, Read_stream)            -> LT
+
+  | (Read_reserve, Read_plain)             -> GT
+  | (Read_reserve, Read_reserve)           -> EQ
+  | (Read_reserve, Read_acquire)           -> LT
+  | (Read_reserve, Read_exclusive)         -> LT
+  | (Read_reserve, Read_exclusive_acquire) -> LT
+  | (Read_reserve, Read_stream)            -> LT
+
+  | (Read_acquire, Read_plain)             -> GT
+  | (Read_acquire, Read_reserve)           -> GT
+  | (Read_acquire, Read_acquire)           -> EQ
+  | (Read_acquire, Read_exclusive)         -> LT
+  | (Read_acquire, Read_exclusive_acquire) -> LT
+  | (Read_acquire, Read_stream)            -> LT
+
+  | (Read_exclusive, Read_plain)             -> GT
+  | (Read_exclusive, Read_reserve)           -> GT
+  | (Read_exclusive, Read_acquire)           -> GT
+  | (Read_exclusive, Read_exclusive)         -> EQ
+  | (Read_exclusive, Read_exclusive_acquire) -> LT
+  | (Read_exclusive, Read_stream)            -> LT
+
+  | (Read_exclusive_acquire, Read_plain)             -> GT
+  | (Read_exclusive_acquire, Read_reserve)           -> GT
+  | (Read_exclusive_acquire, Read_acquire)           -> GT
+  | (Read_exclusive_acquire, Read_exclusive)         -> GT
+  | (Read_exclusive_acquire, Read_exclusive_acquire) -> EQ
+  | (Read_exclusive_acquire, Read_stream)            -> GT
+
+  | (Read_stream, Read_plain)             -> GT
+  | (Read_stream, Read_reserve)           -> GT
+  | (Read_stream, Read_acquire)           -> GT
+  | (Read_stream, Read_exclusive)         -> GT
+  | (Read_stream, Read_exclusive_acquire) -> GT
+  | (Read_stream, Read_stream)            -> EQ
+  end
+let inline {ocaml} read_kindCompare = defaultCompare
+
+let ~{ocaml} read_kindLess b1 b2      = read_kindCompare b1 b2 =  LT
+let ~{ocaml} read_kindLessEq b1 b2    = read_kindCompare b1 b2 <> GT
+let ~{ocaml} read_kindGreater b1 b2   = read_kindCompare b1 b2 =  GT
+let ~{ocaml} read_kindGreaterEq b1 b2 = read_kindCompare b1 b2 <> LT
+
+let inline {ocaml} read_kindLess      = defaultLess
+let inline {ocaml} read_kindLessEq    = defaultLessEq
+let inline {ocaml} read_kindGreater   = defaultGreater
+let inline {ocaml} read_kindGreaterEq = defaultGreaterEq
+
 instance (Ord read_kind)
-  let compare = defaultCompare
-  let (<) = defaultLess
-  let (<=) = defaultLessEq
-  let (>) = defaultGreater
-  let (>=) = defaultGreaterEq
+  let compare = read_kindCompare
+  let (<)  = read_kindLess
+  let (<=) = read_kindLessEq
+  let (>)  = read_kindGreater
+  let (>=) = read_kindGreaterEq
 end
+
+let ~{ocaml} write_kindCompare wk1 wk2 =
+  match (wk1, wk2) with
+  | (Write_plain, Write_plain)             -> EQ
+  | (Write_plain, Write_conditional)       -> LT
+  | (Write_plain, Write_release)           -> LT
+  | (Write_plain, Write_exclusive)         -> LT
+  | (Write_plain, Write_exclusive_release) -> LT
+
+  | (Write_conditional, Write_plain)             -> GT
+  | (Write_conditional, Write_conditional)       -> EQ
+  | (Write_conditional, Write_release)           -> LT
+  | (Write_conditional, Write_exclusive)         -> LT
+  | (Write_conditional, Write_exclusive_release) -> LT
+
+  | (Write_release, Write_plain)             -> GT
+  | (Write_release, Write_conditional)       -> GT
+  | (Write_release, Write_release)           -> EQ
+  | (Write_release, Write_exclusive)         -> LT
+  | (Write_release, Write_exclusive_release) -> LT
+
+  | (Write_exclusive, Write_plain)             -> GT
+  | (Write_exclusive, Write_conditional)       -> GT
+  | (Write_exclusive, Write_release)           -> GT
+  | (Write_exclusive, Write_exclusive)         -> EQ
+  | (Write_exclusive, Write_exclusive_release) -> LT
+
+  | (Write_exclusive_release, Write_plain)             -> GT
+  | (Write_exclusive_release, Write_conditional)       -> GT
+  | (Write_exclusive_release, Write_release)           -> GT
+  | (Write_exclusive_release, Write_exclusive)         -> GT
+  | (Write_exclusive_release, Write_exclusive_release) -> EQ
+  end
+let inline {ocaml} write_kindCompare = defaultCompare
+
+let ~{ocaml} write_kindLess b1 b2      = write_kindCompare b1 b2 =  LT
+let ~{ocaml} write_kindLessEq b1 b2    = write_kindCompare b1 b2 <> GT
+let ~{ocaml} write_kindGreater b1 b2   = write_kindCompare b1 b2 =  GT
+let ~{ocaml} write_kindGreaterEq b1 b2 = write_kindCompare b1 b2 <> LT
+
+let inline {ocaml} write_kindLess      = defaultLess
+let inline {ocaml} write_kindLessEq    = defaultLessEq
+let inline {ocaml} write_kindGreater   = defaultGreater
+let inline {ocaml} write_kindGreaterEq = defaultGreaterEq
+
 instance (Ord write_kind)
-  let compare = defaultCompare
-  let (<) = defaultLess
-  let (<=) = defaultLessEq
-  let (>) = defaultGreater
-  let (>=) = defaultGreaterEq
+  let compare = write_kindCompare
+  let (<)  = write_kindLess
+  let (<=) = write_kindLessEq
+  let (>)  = write_kindGreater
+  let (>=) = write_kindGreaterEq
 end
+
+let ~{ocaml} barrier_kindCompare bk1 bk2 =
+  match (bk1, bk2) with
+  | (Sync, Sync)   -> EQ
+  | (Sync, LwSync) -> LT
+  | (Sync, Eieio)  -> LT
+  | (Sync, Isync)  -> LT
+  | (Sync, DMB)    -> LT
+  | (Sync, DMB_ST) -> LT
+  | (Sync, DMB_LD) -> LT
+  | (Sync, DSB)    -> LT
+  | (Sync, DSB_ST) -> LT
+  | (Sync, DSB_LD) -> LT
+  | (Sync, ISB)    -> LT
+
+  | (LwSync, Sync)   -> GT
+  | (LwSync, LwSync) -> EQ
+  | (LwSync, Eieio)  -> LT
+  | (LwSync, Isync)  -> LT
+  | (LwSync, DMB)    -> LT
+  | (LwSync, DMB_ST) -> LT
+  | (LwSync, DMB_LD) -> LT
+  | (LwSync, DSB)    -> LT
+  | (LwSync, DSB_ST) -> LT
+  | (LwSync, DSB_LD) -> LT
+  | (LwSync, ISB)    -> LT
+
+  | (Eieio, Sync)   -> GT
+  | (Eieio, LwSync) -> GT
+  | (Eieio, Eieio)  -> EQ
+  | (Eieio, Isync)  -> LT
+  | (Eieio, DMB)    -> LT
+  | (Eieio, DMB_ST) -> LT
+  | (Eieio, DMB_LD) -> LT
+  | (Eieio, DSB)    -> LT
+  | (Eieio, DSB_ST) -> LT
+  | (Eieio, DSB_LD) -> LT
+  | (Eieio, ISB)    -> LT
+
+  | (Isync, Sync)   -> GT
+  | (Isync, LwSync) -> GT
+  | (Isync, Eieio)  -> GT
+  | (Isync, Isync)  -> EQ
+  | (Isync, DMB)    -> LT
+  | (Isync, DMB_ST) -> LT
+  | (Isync, DMB_LD) -> LT
+  | (Isync, DSB)    -> LT
+  | (Isync, DSB_ST) -> LT
+  | (Isync, DSB_LD) -> LT
+  | (Isync, ISB)    -> LT
+
+  | (DMB, Sync)   -> GT
+  | (DMB, LwSync) -> GT
+  | (DMB, Eieio)  -> GT
+  | (DMB, ISync)  -> GT
+  | (DMB, DMB)    -> EQ
+  | (DMB, DMB_ST) -> LT
+  | (DMB, DMB_LD) -> LT
+  | (DMB, DSB)    -> LT
+  | (DMB, DSB_ST) -> LT
+  | (DMB, DSB_LD) -> LT
+  | (DMB, ISB)    -> LT
+
+  | (DMB_ST, Sync)   -> GT
+  | (DMB_ST, LwSync) -> GT
+  | (DMB_ST, Eieio)  -> GT
+  | (DMB_ST, ISync)  -> GT
+  | (DMB_ST, DMB)    -> GT
+  | (DMB_ST, DMB_ST) -> EQ
+  | (DMB_ST, DMB_LD) -> LT
+  | (DMB_ST, DSB)    -> LT
+  | (DMB_ST, DSB_ST) -> LT
+  | (DMB_ST, DSB_LD) -> LT
+  | (DMB_ST, ISB)    -> LT
+
+  | (DMB_LD, Sync)   -> GT
+  | (DMB_LD, LwSync) -> GT
+  | (DMB_LD, Eieio)  -> GT
+  | (DMB_LD, ISync)  -> GT
+  | (DMB_LD, DMB)    -> GT
+  | (DMB_LD, DMB_ST) -> GT
+  | (DMB_LD, DMB_LD) -> EQ
+  | (DMB_LD, DSB)    -> LT
+  | (DMB_LD, DSB_ST) -> LT
+  | (DMB_LD, DSB_LD) -> LT
+  | (DMB_LD, ISB)    -> LT
+
+  | (DSB, Sync)   -> GT
+  | (DSB, LwSync) -> GT
+  | (DSB, Eieio)  -> GT
+  | (DSB, ISync)  -> GT
+  | (DSB, DMB)    -> GT
+  | (DSB, DMB_ST) -> GT
+  | (DSB, DMB_LD) -> GT
+  | (DSB, DSB)    -> EQ
+  | (DSB, DSB_ST) -> LT
+  | (DSB, DSB_LD) -> LT
+  | (DSB, ISB)    -> LT
+
+  | (DSB_ST, Sync)   -> GT
+  | (DSB_ST, LwSync) -> GT
+  | (DSB_ST, Eieio)  -> GT
+  | (DSB_ST, ISync)  -> GT
+  | (DSB_ST, DMB)    -> GT
+  | (DSB_ST, DMB_ST) -> GT
+  | (DSB_ST, DMB_LD) -> GT
+  | (DSB_ST, DSB)    -> GT
+  | (DSB_ST, DSB_ST) -> EQ
+  | (DSB_ST, DSB_LD) -> LT
+  | (DSB_ST, ISB)    -> LT
+
+  | (DSB_LD, Sync)   -> GT
+  | (DSB_LD, LwSync) -> GT
+  | (DSB_LD, Eieio)  -> GT
+  | (DSB_LD, ISync)  -> GT
+  | (DSB_LD, DMB)    -> GT
+  | (DSB_LD, DMB_ST) -> GT
+  | (DSB_LD, DMB_LD) -> GT
+  | (DSB_LD, DSB)    -> GT
+  | (DSB_LD, DSB_ST) -> GT
+  | (DSB_LD, DSB_LD) -> EQ
+  | (DSB_LD, ISB)    -> LT
+                          
+  | (ISB, Sync)   -> GT
+  | (ISB, LwSync) -> GT
+  | (ISB, Eieio)  -> GT
+  | (ISB, ISync)  -> GT
+  | (ISB, DMB)    -> GT
+  | (ISB, DMB_ST) -> GT
+  | (ISB, DMB_LD) -> GT
+  | (ISB, DSB)    -> GT
+  | (ISB, DSB_ST) -> GT
+  | (ISB, DSB_LD) -> GT
+  | (ISB, ISB)    -> EQ
+  end
+let inline {ocaml} barrier_kindCompare = defaultCompare
+
+let ~{ocaml} barrier_kindLess b1 b2      = barrier_kindCompare b1 b2 =  LT
+let ~{ocaml} barrier_kindLessEq b1 b2    = barrier_kindCompare b1 b2 <> GT
+let ~{ocaml} barrier_kindGreater b1 b2   = barrier_kindCompare b1 b2 =  GT
+let ~{ocaml} barrier_kindGreaterEq b1 b2 = barrier_kindCompare b1 b2 <> LT
+
+let inline {ocaml} barrier_kindLess      = defaultLess
+let inline {ocaml} barrier_kindLessEq    = defaultLessEq
+let inline {ocaml} barrier_kindGreater   = defaultGreater
+let inline {ocaml} barrier_kindGreaterEq = defaultGreaterEq
+
 instance (Ord barrier_kind)
-  let compare = defaultCompare
-  let (<) = defaultLess
-  let (<=) = defaultLessEq
-  let (>) = defaultGreater
-  let (>=) = defaultGreaterEq
+  let compare = barrier_kindCompare
+  let (<)  = barrier_kindLess
+  let (<=) = barrier_kindLessEq
+  let (>)  = barrier_kindGreater
+  let (>=) = barrier_kindGreaterEq
 end
 
-let eventCompare e1 e2 = 
+let ~{ocaml} eventCompare e1 e2 = 
   match (e1,e2) with
-  | (E_read_mem rk1 v1 i1 tr1, E_read_mem rk2 v2 i2 tr2) -> compare (rk1, (v1,i1,tr1)) (rk2,(v2, i2, tr2)) 
+  | (E_read_mem rk1 v1 i1 tr1, E_read_mem rk2 v2 i2 tr2) ->
+     compare (rk1, (v1,i1,tr1)) (rk2,(v2, i2, tr2)) 
   | (E_write_mem wk1 v1 i1 tr1 v1' tr1', E_write_mem wk2 v2 i2 tr2 v2' tr2') -> 
     compare ((wk1,v1,i1),(tr1,v1',tr1'))  ((wk2,v2,i2),(tr2,v2',tr2')) 
   | (E_barrier bk1, E_barrier bk2) -> compare bk1 bk2
@@ -363,11 +735,28 @@ let eventCompare e1 e2 =
   | (E_write_reg _ _, _) -> LT
   | _ -> GT
   end
-
-
+let inline {ocaml} eventCompare = defaultCompare
+
+let ~{ocaml} eventLess b1 b2      = eventCompare b1 b2 =  LT
+let ~{ocaml} eventLessEq b1 b2    = eventCompare b1 b2 <> GT
+let ~{ocaml} eventGreater b1 b2   = eventCompare b1 b2 =  GT
+let ~{ocaml} eventGreaterEq b1 b2 = eventCompare b1 b2 <> LT
+
+let inline {ocaml} eventLess      = defaultLess
+let inline {ocaml} eventLessEq    = defaultLessEq
+let inline {ocaml} eventGreater   = defaultGreater
+let inline {ocaml} eventGreaterEq = defaultGreaterEq
+
+instance (Ord event)
+  let compare = eventCompare
+  let (<)  = eventLess
+  let (<=) = eventLessEq
+  let (>)  = eventGreater
+  let (>=) = eventGreaterEq
+end
 
 instance (SetType event)
-  let setElemCompare = eventCompare
+  let setElemCompare = compare
 end
 
 (* Functions to build up the initial state for interpretation *)
@@ -383,14 +772,18 @@ type instr_parm_typ =
   | Enum of string * nat (*Internally represented as either a number or constructor, externally as a bitvector*)
   | Other (*An unrepresentable type, will be represented as Unknown in instruciton form *)
 
-let instr_parm_typEqual ip1 ip2 = match (ip1,ip2) with
+let {coq} instr_parm_typEqual ip1 ip2 = match (ip1,ip2) with
   | (Bit,Bit) -> true
   | (Bvector i1,Bvector i2) -> i1 = i2
   | (Range i1,Range i2) -> i1 = i2
   | (Enum s1 i1,Enum s2 i2) -> s1 = s2 && i1 = i2
   | (Other,Other) -> true
   | _ -> false
-end 
+end
+let inline ~{coq} instr_parm_typEqual = unsafe_structural_equality
+
+let {coq} instr_parm_typInequal ip1 ip2 = not (instr_parm_typEqual ip1 ip2)
+let inline ~{coq} instr_parm_typInequal = unsafe_structural_inequality
 
 instance (Eq instr_parm_typ) 
   let (=) = instr_parm_typEqual
@@ -415,9 +808,13 @@ end
 *)
 type instruction = (string * list (string * instr_parm_typ * instruction_field_value) * list base_effect)
 
-let instructionEqual i1 i2 = match (i1,i2) with
+let {coq} instructionEqual i1 i2 = match (i1,i2) with
   | ((i1,parms1,effects1),(i2,parms2,effects2)) -> i1=i2 && parms1 = parms2 && effects1 = effects2
 end
+let inline ~{coq} instructionEqual = unsafe_structural_equality
+
+let {coq} instructionInequal i1 i2 = not (instructionEqual i1 i2)
+let inline ~{coq} instructionInequal = unsafe_structural_inequality
 
 type v_kind = Bitv | Bytev
 
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index c5c550da..3cbef5c8 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -26,16 +26,16 @@ let hardware_quot (a:integer) (b:integer) : integer =
   else a/b
 
 
-let (max_64u : integer) = Num_extra.integerOfString "18446744073709551615"
-let (max_64 : integer) = Num_extra.integerOfString  "9223372036854775807"
-let (min_64 : integer) = Num_extra.integerOfString "-9223372036854775808"
-let (max_32u : integer) = Num_extra.integerOfString "4294967295"
-let (max_32 : integer) = Num_extra.integerOfString "2147483647"
-let (min_32 : integer) = Num_extra.integerOfString "-2147483648"
-let (max_8 : integer) = (integerFromNat 127)
-let (min_8 : integer) = (integerFromNat 0) - (integerFromNat 128)
-let (max_5 : integer) = (integerFromNat 31)
-let (min_5 : integer) = (integerFromNat 0)-(integerFromNat 32)
+let (max_64u : integer) = integerFromNat ((natPow 2 64) - 1)
+let (max_64  : integer) = integerFromNat ((natPow 2 63) - 1)
+let (min_64  : integer) = integerNegate (integerFromNat (natPow 2 63))
+let (max_32u : integer) = integerFromNat 4294967295
+let (max_32  : integer) = integerFromNat 2147483647
+let (min_32  : integer) = integerNegate (integerFromNat 2147483648)
+let (max_8   : integer) = (integerFromNat 127)
+let (min_8   : integer) = (integerFromNat 0) - (integerFromNat 128)
+let (max_5   : integer) = (integerFromNat 31)
+let (min_5   : integer) = (integerFromNat 0)-(integerFromNat 32)
 
 val get_max_representable_in : signed -> nat -> integer
 let get_max_representable_in sign n =