stdlib: basic commutative algebra

examples/SchnorrPK.ec

@@ -15,7 +15,7 @@ clone G.PowZMod as GP with
 
 clone GP.FDistr as FD.
 
-clone GP.ZModE.ZModpField as ZPF.
+clone GP.ZModE.ZModpFieldBd as ZPF.
 
 import G GP GP.ZModE FD.
 
@@ -145,7 +145,7 @@ section SchnorrPKSecurity.
     auto; rewrite /R /R_DL /oget => &hr /> hne 2!-> /=.
     rewrite expM !expB accepting_transcript_1 accepting_transcript_2.
     rewrite invM (mulcC m{hr}) -mulcA (mulcA m{hr}) mulcV mulcA mulc1 -expB -expM.
-    by rewrite ZPF.divrr ?ZPF.subr_eq0 // exp1.
+    by rewrite ZPF.F.divff ?ZPF.R.subr_eq0 // exp1.
   qed.
 
   (* Special honest verifier zero knowledge *)

examples/UC/dh_enc.ec

@@ -328,7 +328,7 @@ require DiffieHellman.
 clone DiffieHellman as DH.
 import DH.DDH DH.G DH.GP DH.FD DH.GP.ZModE.
 
-clone DH.GP.ZModE.ZModpField as ZPF.
+clone DH.GP.ZModE.ZModpFieldBd as ZPF.
 
 (*  Such statements make no sense when we don't restrict to a
     complexity class 
@@ -897,7 +897,7 @@ wp;call (_: ={glob HybFChan.F2Auth.F2Auth,
 ); last first.
 
 (* Init *)
-by auto => /> &2; rewrite expM /= -expM ZPF.mulrC expM.
+by auto => /> &2; rewrite expM /= -expM ZPF.R.mulrC expM.
 (* Now the call *)
 + by proc;inline *; auto => /> /#.
 + by sim />.

examples/cramer-shoup/cramer_shoup.ec

@@ -9,7 +9,7 @@ require DiffieHellman.
 clone DiffieHellman as DH.
 import DH.DDH DH.G DH.GP DH.FD DH.GP.ZModE.
 
-clone DH.GP.ZModE.ZModpField as ZPF.
+clone DH.GP.ZModE.ZModpFieldBd as ZPF.
 
 lemma gt1_q : 1 < order by smt(ge2_p).
 
@@ -576,7 +576,7 @@ section Security_Aux.
     move=> kL _ xL _ x2L _ yL _ y2L _ zL _ resu bL _.
     have H1 : (-uL) * wL + u'L * wL = wL * (u'L - uL) by ring.
     have H2 : (-uL) * wL + u'L * wL <> zero.
-    + rewrite H1 ZPF.mulf_eq0 negb_or HwL /=.
+    + rewrite H1 ZPF.F.mulf_eq0 negb_or HwL /=.
       by move: Hu'L;apply: contra => H;ring H.
     split => [? _ | _ ]; 1: by field.
     move=> z2L _; split => [ | _]; 1: by field.
@@ -605,7 +605,7 @@ section Security_Aux.
     move=> kL _ yL _ y2L _ zL _ r'L _ xL _.
     have H1 : (-uL) * wL + u'L * wL = wL * (u'L - uL) by ring.
     have H2 : (-uL) * wL + u'L * wL <> zero.
-    + rewrite H1 ZPF.mulf_eq0 negb_or HwL /=.
+    + rewrite H1 ZPF.F.mulf_eq0 negb_or HwL /=.
       by move: Hu'L;apply: contra => H;ring H.
     split => [? _ | _ ]; 1: by field.
     move=> z2L _; split => [ | _]; 1: by field.
@@ -751,7 +751,7 @@ section Security_Aux.
     move=> yL _ y2L _ zL _ r'L _ xL _ rL _.
     have H1 : (-uL) * wL + u'L * wL = wL * (u'L - uL) by ring.
     have H2 : (-uL) * wL + u'L * wL <> zero.
-    + rewrite H1 ZPF.mulf_eq0 negb_or HwL0 /=.
+    + rewrite H1 ZPF.F.mulf_eq0 negb_or HwL0 /=.
       by move: HuL;apply: contra => H;ring H.
     split => [ | _ /#].
     rewrite log_bij !(logg1, logrzM, logDr); field.

examples/elgamal.ec

@@ -11,7 +11,7 @@ pragma +implicits.
 clone DiffieHellman as DH.
 import DH.DDH DH.G DH.GP DH.FD DH.GP.ZModE.
 
-clone DH.GP.ZModE.ZModpField as ZPF.
+clone DH.GP.ZModE.ZModpFieldBd as ZPF.
 
 (** Construction: a PKE **)
 type pkey = group.
@@ -107,8 +107,8 @@ section Security.
       (fun z, z - loge (if b then m1 else m0){2}).
   auto; call (_:true).
   auto; progress.
-  - by rewrite ZPF.addrAC -ZPF.addrA ZPF.subrr ZPF.addr0.
-  - by rewrite  -ZPF.addrA ZPF.subrr ZPF.addr0.
+  - by rewrite ZPF.R.addrAC -ZPF.R.addrA ZPF.R.subrr ZPF.R.addr0.
+  - by rewrite  -ZPF.R.addrA ZPF.R.subrr ZPF.R.addr0.
   - by rewrite expD expgK.
   qed.
 

src/ecCommands.ml

@@ -662,7 +662,7 @@ and process_th_clone (scope : EcScope.scope) thcl =
   EcScope.Cloning.clone scope (Pragma.get ()).pm_check thcl
 
 (* -------------------------------------------------------------------- *)
-and process_th_alias (scope : EcScope.scope) (thcl : psymbol * pqsymbol) =
+and process_th_alias (scope : EcScope.scope) (thcl : psymbol * pqsymbol list) =
   EcScope.check_state `InTop "theory alias" scope;
   EcScope.Theory.alias scope thcl
 

src/ecEnv.ml

@@ -312,6 +312,29 @@ let empty_mc params = {
   mc_components = MMsym.empty;
 }
 
+(* -------------------------------------------------------------------- *)
+(* Merge the members of [mc2] into [mc1].  Entries keep their original
+ * paths; bindings of [mc2] shadow same-named bindings of [mc1] (the
+ * most recently merged component wins, as with imports). *)
+let mc_merge (mc1 : mc) (mc2 : mc) =
+  let merge m1 m2 =
+    MMsym.fold
+      (fun x vs acc -> List.fold_right (fun v acc -> MMsym.add x v acc) vs acc)
+      m2 m1 in
+
+  { mc_parameters = mc1.mc_parameters;
+    mc_modules    = merge mc1.mc_modules     mc2.mc_modules;
+    mc_modsigs    = merge mc1.mc_modsigs     mc2.mc_modsigs;
+    mc_tydecls    = merge mc1.mc_tydecls     mc2.mc_tydecls;
+    mc_operators  = merge mc1.mc_operators   mc2.mc_operators;
+    mc_axioms     = merge mc1.mc_axioms      mc2.mc_axioms;
+    mc_theories   = merge mc1.mc_theories    mc2.mc_theories;
+    mc_variables  = merge mc1.mc_variables   mc2.mc_variables;
+    mc_functions  = merge mc1.mc_functions   mc2.mc_functions;
+    mc_typeclasses= merge mc1.mc_typeclasses mc2.mc_typeclasses;
+    mc_rwbase     = merge mc1.mc_rwbase      mc2.mc_rwbase;
+    mc_components = merge mc1.mc_components  mc2.mc_components; }
+
 (* -------------------------------------------------------------------- *)
 let empty_norm_cache =
   { norm_mp   = Mm.empty;
@@ -1153,9 +1176,37 @@ module MC = struct
       | Th_baserw (x, _) ->
           (add2mc _up_rwbase x (expath x) mc, None)
 
-      | Th_alias _ ->
-          (* FIXME:ALIAS *)
-          (mc, None)
+      | Th_alias (name, targets) -> begin
+          (* Alias entries resolve to their targets.  A single-target
+           * alias is a pure component redirection; a packed alias
+           * (several targets) gets a merged component built from the
+           * sibling targets (enforced in [EcScope.Theory.alias]),
+           * whose entries keep the targets' paths. *)
+          match targets with
+          | [target] ->
+              (_up_mc ~name false mc (IPPath target), None)
+
+          | targets ->
+              let mc_of_target (target : path) =
+                let tname = EcPath.basename target in
+                let tcth  =
+                  List.find_map_opt
+                    (fun item ->
+                      match item.ti_item with
+                      | Th_theory (x, tcth) when x = tname -> Some tcth
+                      | _ -> None)
+                    cth.cth_items in
+                (* enforced by [EcScope.Theory.alias] *)
+                let tcth = oget tcth in
+                let ((_, tmc), _) = mc_of_theory_r subscope (tname, tcth) in
+                tmc in
+
+              let merged =
+                List.fold_left mc_merge (empty_mc None)
+                  (List.map mc_of_target targets) in
+              let mc = _up_mc false mc (IPPath (expath name)) in
+              (mc, Some ((name, merged), []))
+        end
       | Th_export    _
       | Th_addrw     _
       | Th_instance  _
@@ -3512,18 +3563,39 @@ module Theory = struct
       Option.get (Mp.find_opt p env.env_thenvs)
 
 (* ------------------------------------------------------------------ *)
-  let rebind_alias (name : symbol) (path : path) (env : env) =
-    let th = by_path path env in
-    let src = EcPath.pqname (root env) name in
-    let env = MC.import_theory ~name path th env in
-    let env = MC.import_mc ~name (IPPath path) env in
-    let env = { env with env_albase = Mp.add path src env.env_albase } in
-    env
+  let rebind_alias (name : symbol) (paths : path list) (env : env) =
+    match paths with
+    | [path] ->
+        let th = by_path path env in
+        let src = EcPath.pqname (root env) name in
+        let env = MC.import_theory ~name path th env in
+        let env = MC.import_mc ~name (IPPath path) env in
+        let env = { env with env_albase = Mp.add path src env.env_albase } in
+        env
+
+    | paths ->
+        (* Packed alias: merge the targets' components under the alias
+         * name.  Entries keep their original paths, so resolution
+         * always yields the aliased objects -- no copies.  Contrary to
+         * [MC.bind_mc], rebinding must be idempotent: the alias is
+         * rebound on every import of the enclosing theory. *)
+        let mc_of (p : path) =
+          oget (Mip.find_opt (IPPath p) env.env_comps) in
+        let merged =
+          List.fold_left mc_merge (empty_mc None) (List.map mc_of paths) in
+        let apath = IPPath (EcPath.pqname (root env) name) in
+        { env with
+            env_current = MC._up_mc true env.env_current apath;
+            env_comps =
+              Mip.change
+                (fun mc -> Some (MC._up_mc true (oget mc) apath))
+                (IPPath (root env))
+                (Mip.add apath merged env.env_comps); }
 
   (* ------------------------------------------------------------------ *)
-  let alias ?(import = true) (name : symbol) (path : path) (env : env) =
-    let env = if import then rebind_alias name path env else env in
-    { env with env_item = mkitem ~import (Th_alias (name, path)) :: env.env_item }
+  let alias ?(import = true) (name : symbol) (paths : path list) (env : env) =
+    let env = if import then rebind_alias name paths env else env in
+    { env with env_item = mkitem ~import (Th_alias (name, paths)) :: env.env_item }
 
   (* ------------------------------------------------------------------ *)
   let aliases (env : env) =

src/ecEnv.mli

@@ -326,7 +326,7 @@ module Theory : sig
     -> EcTheory.thmode
     -> env -> compiled_theory option
 
-  val alias : ?import:bool -> symbol -> path -> env -> env
+  val alias : ?import:bool -> symbol -> path list -> env -> env
   val aliases : env -> path Mp.t
 end
 

src/ecParser.mly

@@ -3938,7 +3938,7 @@ realize:
 (* Theory aliasing                                                      *)
 
 theory_alias: (* FIXME: THEORY ALIAS -> S/R conflict *)
-| THEORY name=uident EQ target=uqident { (name, target) }
+| THEORY name=uident EQ targets=plist1(uqident, PLUS) { (name, targets) }
 
 (* -------------------------------------------------------------------- *)
 (* Printing                                                             *)

src/ecParsetree.ml

@@ -1501,7 +1501,7 @@ type global_action =
   | GthImport    of pqsymbol list
   | GthExport    of pqsymbol list
   | GthClone     of theory_cloning
-  | GthAlias     of (psymbol * pqsymbol)
+  | GthAlias     of (psymbol * pqsymbol list)
   | GModImport   of pmsymbol located list
   | GsctOpen     of osymbol_r
   | GsctClose    of osymbol_r

src/ecPrinting.ml

@@ -3953,8 +3953,9 @@ let rec pp_theory ppe (fmt : Format.formatter) (path, cth) =
       Format.fprintf fmt "%abind circuit %a \"%s\"."
         pp_locality lc (pp_opname ppe) cr.operator cr.name
   end
-  | EcTheory.Th_alias (name, target) ->
-      Format.fprintf fmt "theory %s = %a." name (pp_thname ~alias:false ppe) target
+  | EcTheory.Th_alias (name, targets) ->
+      Format.fprintf fmt "theory %s = %a." name
+        (pp_list " +@ " (pp_thname ~alias:false ppe)) targets
 
 (* -------------------------------------------------------------------- *)
 and pp_th_item ppe p fmt item =

src/ecScope.ml

@@ -2065,12 +2065,31 @@ module Theory = struct
   let required scope = scope.sc_required
 
   (* -------------------------------------------------------------------- *)
-  let alias (scope : scope) ((name, target) : psymbol * pqsymbol) =
-    let thpath = EcEnv.Theory.lookup_opt (unloc target) (env scope) in
-    let thpath, _ = ofdfl (fun () ->
-      hierror ~loc:(loc target) "unknown theory: %a" pp_qsymbol (unloc target)
-    ) thpath in
-    let item = EcTheory.mkitem ~import:true (Th_alias (unloc name, thpath)) in
+  let alias (scope : scope) ((name, targets) : psymbol * pqsymbol list) =
+    let resolve (target : pqsymbol) =
+      let thpath = EcEnv.Theory.lookup_opt (unloc target) (env scope) in
+      let thpath, _ = ofdfl (fun () ->
+        hierror ~loc:(loc target) "unknown theory: %a" pp_qsymbol (unloc target)
+      ) thpath in
+      thpath in
+
+    let thpaths = List.map resolve targets in
+
+    (* Packed aliases (more than one target) merge the targets' members
+     * under one name.  Restrict the targets to sibling sub-theories of
+     * the current scope, so that the components of the alias can be
+     * reconstructed purely from the enclosing theory (see
+     * [EcEnv.MC.mc_of_theory_r]). *)
+    if List.length thpaths > 1 then begin
+      let root = EcEnv.root (env scope) in
+      List.iter2 (fun target thpath ->
+        if EcPath.prefix thpath <> Some root then
+          hierror ~loc:(loc target)
+            "packed theory aliases must reference sibling theories")
+        targets thpaths
+    end;
+
+    let item = EcTheory.mkitem ~import:true (Th_alias (unloc name, thpaths)) in
 
     { scope with sc_env = EcSection.add_item item scope.sc_env }
 end

src/ecScope.mli

@@ -219,7 +219,7 @@ module Theory : sig
 
   (* [alias scope (name, thname)] create a theory alias [name] to
    * [thname] *)
-  val alias : scope -> psymbol * pqsymbol -> scope
+  val alias : scope -> psymbol * pqsymbol list -> scope
 end
 
 (* -------------------------------------------------------------------- *)

src/ecSubst.ml

@@ -1201,7 +1201,7 @@ let rec subst_theory_item_r (s : subst) (item : theory_item_r) =
       Th_crbinding (subst_crbinding s bd, lc)
 
   | Th_alias (name, target) ->
-      Th_alias (name, subst_path s target)
+      Th_alias (name, List.map (subst_path s) target)
 
 (* -------------------------------------------------------------------- *)
 and subst_theory (s : subst) (items : theory) =

src/ecTheory.ml

@@ -32,7 +32,7 @@ and theory_item_r =
   | Th_reduction of reduction_rule
   | Th_crbinding of crbinding * is_local
   | Th_auto      of auto_rule
-  | Th_alias     of (symbol * path) (* FIXME: currently, only theories *)
+  | Th_alias     of (symbol * path list) (* FIXME: currently, only theories *)
 
 and thsource = {
   ths_base : EcPath.path;

src/ecTheory.mli

@@ -29,7 +29,7 @@ and theory_item_r =
   | Th_reduction of reduction_rule
   | Th_crbinding of crbinding * is_local
   | Th_auto      of auto_rule
-  | Th_alias     of (symbol * path)
+  | Th_alias     of (symbol * path list)
 
 and thsource = {
   ths_base : EcPath.path;

src/ecTheoryReplay.ml

@@ -1265,16 +1265,19 @@ and replay_crbinding (ove : _ ovrenv) (subst, ops, proofs, scope) (import, bindi
 
 (* -------------------------------------------------------------------- *)
 and replay_alias
-  (ove : _ ovrenv) (subst, ops, proofs, scope) (import, name, target)
+  (ove : _ ovrenv) (subst, ops, proofs, scope) (import, name, targets)
 =
   let scenv = ove.ovre_hooks.henv scope in
   let env = EcSection.env scenv in
-  let p = EcSubst.subst_path subst target in
+  let targets = List.map (EcSubst.subst_path subst) targets in
+  let subst, name = rename ove subst (`Theory, name) in
 
-  if is_none (EcEnv.Theory.by_path_opt p env) then
+  if List.for_all
+       (fun p -> is_some (EcEnv.Theory.by_path_opt p env)) targets
+  then
+    let scope = ove.ovre_hooks.hadd_item scope ~import (Th_alias (name, targets)) in
     (subst, ops, proofs, scope)
   else
-    let scope = ove.ovre_hooks.hadd_item scope ~import (Th_alias (name, target)) in
     (subst, ops, proofs, scope)
 
 (* -------------------------------------------------------------------- *)
@@ -1328,8 +1331,8 @@ and replay1 (ove : _ ovrenv) (subst, ops, proofs, scope) (hidden, item) =
   | Th_instance _ ->
     (subst, ops, proofs, scope)
 
-  | Th_alias (name, target) ->
-     replay_alias ove (subst, ops, proofs, scope) (item.ti_import, name, target)
+  | Th_alias (name, targets) ->
+     replay_alias ove (subst, ops, proofs, scope) (item.ti_import, name, targets)
 
   | Th_crbinding (binding, lc) when not hidden ->
      replay_crbinding ove (subst, ops, proofs, scope) (item.ti_import, binding, lc)