lospec: raw equality

Author: strub

libs/lospecs/ast.ml

@@ -70,6 +70,7 @@ type aexpr_ =
   | EOr of aword * (aexpr * aexpr)
   | EXor of aword * (aexpr * aexpr)
   | EAnd of aword * (aexpr * aexpr)
+  | EEq of aword * (aexpr * aexpr)
   | ECmp of aword * us * [`Gt | `Ge] * (aexpr * aexpr)
   | EPopCount of aword * aexpr
 [@@deriving yojson]

libs/lospecs/circuit.ml

@@ -648,6 +648,11 @@ let sle (r1 : reg) (r2 : reg) : node =
 let iszero (r : reg) : node =
   bvueq r (Array.map (fun _ -> false_) r)
 
+(* -------------------------------------------------------------------- *)
+let eq (r1 : reg) (r2 : reg) : node =
+  assert (Array.length r1 = Array.length r2);
+  bvueq r1 r2
+
 (* -------------------------------------------------------------------- *)
 let abs (a : reg) : reg =
   let msb_a, _ = split_msb a in

libs/lospecs/circuit.mli

@@ -152,6 +152,8 @@ val bvueq : reg -> reg -> node
 
 val bvseq : reg -> reg -> node
 
+val eq : reg -> reg -> node
+
 (* ==================================================================== *)
 val sat : signed:bool -> size:int -> reg -> reg
 

libs/lospecs/circuit_spec.ml

@@ -105,6 +105,11 @@ let circuit_of_specification (rs : reg list) (p : adef) : reg =
       | `US   -> Circuit.usmul e1 e2
       end
 
+    | EEq(`W _, (e1, e2)) ->
+      let e1 = of_expr env e1 in
+      let e2 = of_expr env e2 in
+      [|Circuit.eq e1 e2|]
+
     | ECmp (`W _, us, k, (e1, e2)) ->
       let e1 = of_expr env e1 in
       let e2 = of_expr env e2 in

libs/lospecs/typing.ml

@@ -155,6 +155,7 @@ module Sigs : sig
   val smullo : sig_
   val smulhi : sig_
   val usmul : sig_
+  val eq : sig_
   val sgt : sig_
   val sge : sig_
   val ugt : sig_
@@ -291,6 +292,10 @@ end = struct
   let usmul : sig_ =
     mulop ~ret:(fun n -> 2 * n) ~name:"usmul" `US
 
+  let eq : sig_ =
+    let mk = fun ws x y -> EEq (as_seq1 ws, (x, y)) in
+    binop ~ret:(fun _ -> 1) ~name:"eq" mk
+
   let sgt : sig_ =
     let mk = fun ws x y -> ECmp (as_seq1 ws, `S, `Gt, (x, y)) in
     binop ~ret:(fun _ -> 1) ~name:"sgt" mk
@@ -346,6 +351,7 @@ let sigs : sig_ list = [
   Sigs.smullo;
   Sigs.smulhi;  
   Sigs.usmul;
+  Sigs.eq;
   Sigs.sgt;
   Sigs.sge;
   Sigs.ugt;