heterogeneous bv operators

EasyCrypt · Oct 11, 2024 · 9b02e43 · 9b02e43
1 parent 4411b4c
commit 9b02e43
Show file tree

Hide file tree

Showing 13 changed files with 295 additions and 147 deletions.
diff --git a/src/ecCommands.ml b/src/ecCommands.ml
@@ -708,10 +708,10 @@ and process_dump scope (source, tc) =
 (* -------------------------------------------------------------------- *)
 and process_crbind (scope : EcScope.scope) (binding : pcrbinding) =
   match binding.binding with
-  | CRB_Bitstring  bs -> EcScope.Circuit.add_bitstring scope binding.locality bs
-  | CRB_Array      ba -> EcScope.Circuit.add_bsarray   scope binding.locality ba
-  | CRB_BvOperator op -> EcScope.Circuit.add_qfabvop   scope binding.locality op
-  | CRB_Circuit    cr -> EcScope.Circuit.add_circuit   scope binding.locality cr
+  | CRB_Bitstring  bs -> EcScope.Circuit.add_bitstring  scope binding.locality bs
+  | CRB_Array      ba -> EcScope.Circuit.add_array      scope binding.locality ba
+  | CRB_BvOperator op -> EcScope.Circuit.add_bvoperator scope binding.locality op
+  | CRB_Circuit    cr -> EcScope.Circuit.add_circuit    scope binding.locality cr
 
 (* -------------------------------------------------------------------- *)
 and process (ld : Loader.loader) (scope : EcScope.scope) g =

diff --git a/src/ecDecl.ml b/src/ecDecl.ml
@@ -16,10 +16,11 @@ type ty_params = ty_param list
 type ty_pctor  = [ `Int of int | `Named of ty_params ]
 
 type tydecl = {
-  tyd_params  : ty_params;
-  tyd_type    : ty_body;
-  tyd_loca    : locality;
-  tyd_resolve : bool;
+  tyd_params   : ty_params;
+  tyd_type     : ty_body;
+  tyd_loca     : locality;
+  tyd_resolve  : bool;
+  tyd_clinline : bool;
 }
 
 and ty_body = [
@@ -60,7 +61,11 @@ let abs_tydecl ?(resolve = true) ?(tc = Sp.empty) ?(params = `Int 0) lc =
           (EcUid.NameGen.bulk ~fmt n)
   in
 
-  { tyd_params = params; tyd_type = `Abstract tc; tyd_resolve = resolve; tyd_loca = lc; }
+  { tyd_params   = params
+  ; tyd_type     = `Abstract tc
+  ; tyd_resolve  = resolve
+  ; tyd_loca     = lc
+  ; tyd_clinline = false }
 
 (* -------------------------------------------------------------------- *)
 let ty_instanciate (params : ty_params) (args : ty list) (ty : ty) =
@@ -361,21 +366,23 @@ type crb_array =
   ; size   : int }
 
 type bv_opkind = [
-  | `Add  of int
-  | `Sub  of int
-  | `Mul  of int
-  | `UDiv of int
-  | `URem of int
-  | `Shl  of int
-  | `Shr  of int
-  | `And  of int
-  | `Or   of int
-  | `Not  of int
+  | `Add      of int
+  | `Sub      of int
+  | `Mul      of int
+  | `UDiv     of int
+  | `URem     of int
+  | `Shl      of int
+  | `Shr      of int
+  | `And      of int
+  | `Or       of int
+  | `Not      of int
+  | `ZExtend  of int * int
+  | `Truncate of int * int
 ]
 
 type crb_bvoperator =
   { kind     : bv_opkind
-  ; type_    : EcPath.path
+  ; types    : EcPath.path list
   ; operator : EcPath.path
   ; theory   : EcPath.path }
 

diff --git a/src/ecDecl.mli b/src/ecDecl.mli
@@ -12,10 +12,11 @@ type ty_params = ty_param list
 type ty_pctor  = [ `Int of int | `Named of ty_params ]
 
 type tydecl = {
-  tyd_params  : ty_params;
-  tyd_type    : ty_body;
-  tyd_loca    : locality;
-  tyd_resolve : bool;
+  tyd_params   : ty_params;
+  tyd_type     : ty_body;
+  tyd_loca     : locality;
+  tyd_resolve  : bool;
+  tyd_clinline : bool;
 }
 
 and ty_body = [
@@ -211,21 +212,23 @@ type crb_array =
   ; size   : int }
 
 type bv_opkind = [
-  | `Add  of int
-  | `Sub  of int
-  | `Mul  of int
-  | `UDiv of int
-  | `URem of int
-  | `Shl  of int
-  | `Shr  of int
-  | `And  of int
-  | `Or   of int
-  | `Not  of int
+  | `Add      of int
+  | `Sub      of int
+  | `Mul      of int
+  | `UDiv     of int
+  | `URem     of int
+  | `Shl      of int
+  | `Shr      of int
+  | `And      of int
+  | `Or       of int
+  | `Not      of int
+  | `ZExtend  of int * int
+  | `Truncate of int * int
 ]
 
 type crb_bvoperator =
   { kind     : bv_opkind
-  ; type_    : EcPath.path
+  ; types    : EcPath.path list
   ; operator : EcPath.path
   ; theory   : EcPath.path }
 

diff --git a/src/ecHiInductive.ml b/src/ecHiInductive.ml
@@ -83,10 +83,11 @@ let trans_datatype (env : EcEnv.env) (name : ptydname) (dt : pdatatype) =
   let tpath = EcPath.pqname (EcEnv.root env) (unloc name) in
   let env0  =
     let myself = {
-      tyd_params  = EcUnify.UniEnv.tparams ue;
-      tyd_type    = `Abstract EcPath.Sp.empty;
-      tyd_loca    = lc;
-      tyd_resolve = true;
+      tyd_params   = EcUnify.UniEnv.tparams ue;
+      tyd_type     = `Abstract EcPath.Sp.empty;
+      tyd_loca     = lc;
+      tyd_resolve  = true;
+      tyd_clinline = false;
     } in
       EcEnv.Ty.bind (unloc name) myself env
   in

diff --git a/src/ecParser.mly b/src/ecParser.mly
@@ -3898,7 +3898,10 @@ cr_binding_r:
   { CRB_Array { get; set; tolist; type_; size; } }
 
 | BIND OP type_=loc(simpl_type_exp) operator=qoident name=loc(STRING)
-  { CRB_BvOperator { type_; operator; name; } }
+  { CRB_BvOperator { types = [type_]; operator; name; } }
+
+| BIND OP types=bracket(plist1(loc(simpl_type_exp), AMP)) operator=qoident name=loc(STRING)
+  { CRB_BvOperator { types; operator; name; } }
 
 | BIND CIRCUIT operator=qoident circuit=loc(STRING)
   { CRB_Circuit { operator; circuit; } }

diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml
@@ -1286,7 +1286,7 @@ type pbind_array =
 (* -------------------------------------------------------------------- *)
 type pbind_bvoperator =
   { name     : string located
-  ; type_    : pty
+  ; types    : pty list
   ; operator : pqsymbol }
 
 (* -------------------------------------------------------------------- *)

diff --git a/src/ecPrinting.ml b/src/ecPrinting.ml
@@ -3393,20 +3393,22 @@ let rec pp_theory ppe (fmt : Format.formatter) (path, cth) =
     | CRB_BvOperator op ->
       let kind =
         match op.kind with
-        | `Add   _ -> "add"
-        | `Sub   _ -> "sub"
-        | `Mul   _ -> "mul"
-        | `UDiv  _ -> "udiv"
-        | `URem  _ -> "urem"
-        | `Shl   _ -> "shl"
-        | `Shr   _ -> "shr"
-        | `Not   _ -> "not"
-        | `And   _ -> "and"
-        | `Or    _ -> "or"
+        | `Add      _ -> "add"
+        | `Sub      _ -> "sub"
+        | `Mul      _ -> "mul"
+        | `UDiv     _ -> "udiv"
+        | `URem     _ -> "urem"
+        | `Shl      _ -> "shl"
+        | `Shr      _ -> "shr"
+        | `Not      _ -> "not"
+        | `And      _ -> "and"
+        | `Or       _ -> "or"
+        | `ZExtend  _ -> "zextend"
+        | `Truncate _ -> "truncate"
       in
-      Format.fprintf fmt "%abind op %a %a \"%s\""
+      Format.fprintf fmt "%abind op [%a] %a \"%s\"."
         pp_locality lc
-        (pp_tyname ppe) op.type_
+        (pp_list " & " (pp_tyname ppe)) op.types
         (pp_opname ppe) op.operator
         kind