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

@@ -327,7 +327,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 
@@ -896,7 +896,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.
@@ -752,7 +752,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/ecCallbyValue.ml

@@ -323,6 +323,12 @@ and try_reduce_fixdef
     if not (st.st_ri.iota && is_fix_def st p) then
       raise Bailout;
 
+    (match st.st_ri.delta_p p with
+     | `Force -> ()
+     | _ ->
+       if EcReduction.reduction_opaque st.st_ri st.st_env p then
+         raise Bailout);
+
     let Args.{ resty = ty; stack = args; } = args in
     let op  = oget (oper st p) in
     let fix = EcDecl.operator_as_fix op in
@@ -424,7 +430,7 @@ and reduce_user_delta st f1 p tys args =
   match reduce_user_with_exn st f2 with
   | f -> f
   | exception NotReducible ->
-    let mode = st.st_ri.delta_p p in
+    let mode = EcReduction.opacity_mode st.st_ri p (st.st_ri.delta_p p) in
     let nargs = List.length args.stack in
     match mode with
     | #Op.redmode as mode -> begin

src/ecCommands.ml

@@ -665,7 +665,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;
@@ -627,16 +650,37 @@ module MC = struct
 
     | x :: qn ->
         let x = if x = EcCoreLib.i_self then EcCoreLib.i_top else x in
+        let top = MMsym.last x env.env_current.mc_components in
         let p =
-          (MMsym.last x env.env_current.mc_components) |>
+          top |>
             obind
               (fun p ->
                 match p, qn with
                 | IPIdent _, [] -> Some p
                 | IPIdent _, _  -> None
                 | IPPath  p, _  -> Some (IPPath (path_of_qn p qn)))
         in
-          p |> obind (fun p -> Mip.find_opt p env.env_comps)
+
+        match p |> obind (fun p -> Mip.find_opt p env.env_comps) with
+        | Some _ as mc -> mc
+        | None ->
+          (* A theory alias is only a component of its enclosing
+           * theory, that names the components of its target: follow
+           * the components of [qn] one by one. *)
+          let rec follow (mc : mc) (qn : symbol list) =
+            match qn with
+            | [] -> Some mc
+            | x :: qn ->
+                match MMsym.last x mc.mc_components with
+                | Some (IPPath _ as p) ->
+                    Mip.find_opt p env.env_comps
+                      |> obind (fun mc -> follow mc qn)
+                | _ -> None in
+
+          match top, qn with
+          | Some (IPPath _ as p), _ :: _ ->
+              Mip.find_opt p env.env_comps |> obind (fun mc -> follow mc qn)
+          | _ -> None
 
   (* ------------------------------------------------------------------ *)
   let lookup ?(unique = false) proj (qn, x) env =
@@ -1019,7 +1063,29 @@ module MC = struct
     { mc with mc_theories = MMsym.add x obj mc.mc_theories }
 
   let lookup_theory qnx env =
-    match lookup (fun mc -> mc.mc_theories) qnx env with
+    (* A theory alias [x = T] is a component [x] of its enclosing
+     * theory, that names [T]. *)
+    let by_alias ((qn, x) : qsymbol) =
+      match lookup_mc qn env |> obind (fun mc -> MMsym.last x mc.mc_components) with
+      | Some (IPPath p) -> begin
+          match p.EcPath.p_node with
+          | EcPath.Pqname (q, y) ->
+              Mip.find_opt (IPPath q) env.env_comps
+                |> obind (fun mc -> MMsym.last y mc.mc_theories)
+                |> obind (fun (q, th) ->
+                     match q with
+                     | IPPath q when EcPath.p_equal p q -> Some (IPPath q, ([], th))
+                     | _ -> None)
+          | _ -> None
+        end
+      | _ -> None in
+
+    let th =
+      match lookup (fun mc -> mc.mc_theories) qnx env with
+      | None -> by_alias qnx
+      | th -> th in
+
+    match th with
     | None -> lookup_error (`QSymbol qnx)
     | Some (p, (args, obj)) -> (_downpath_for_th env p args, obj)
 
@@ -1153,9 +1219,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  _
@@ -3498,18 +3592,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) =
@@ -3782,7 +3897,9 @@ module Theory = struct
       in (cleared, omap (fun item_r -> { item with ti_item = item_r; }) item_r)
 
   (* ------------------------------------------------------------------ *)
-  type clear_mode = [`Full | `ClearOnly | `No]
+  (* [`Alias] is [`Full], but also drops a theory whose items are all
+   * aliases. *)
+  type clear_mode = [`Full | `Alias | `ClearOnly | `No]
 
   let close
     ?(clears : path list = [])
@@ -3798,8 +3915,12 @@ module Theory = struct
       else snd (filter_th clears (root env) Sp.empty items) in
 
     let items =
+      let is_alias (item : theory_item) =
+        match item.ti_item with Th_alias _ -> true | _ -> false in
+
       match items, pempty with
       | None, (`No | `ClearOnly) -> Some []
+      | Some items, `Alias when List.for_all is_alias items -> None
       | _, _ -> items
     in
 

src/ecEnv.mli

@@ -321,12 +321,12 @@ module Theory : sig
 
   val close :
        ?clears:(path list)
-    -> ?pempty:[`Full | `ClearOnly | `No]
+    -> ?pempty:[`Full | `Alias | `ClearOnly | `No]
     -> EcTypes.is_local
     -> 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