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.
@@ -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/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;
@@ -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  _
@@ -3498,18 +3549,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/ecHiGoal.ml

@@ -89,6 +89,21 @@ let process_change fp (tc : tcenv1) =
   let fp = TTC.tc1_process_formula tc fp in
   t_change fp tc
 
+(* -------------------------------------------------------------------- *)
+(* Resolve the [-delta ops] / [+delta ops] items of a hint clause and
+   record them as reduction-opacity overrides in the simplify context. *)
+let apply_hint_opacity tc env (specs : (bool * pqsymbol list) list) simpl =
+  List.fold_left (fun simpl (opq, ops) ->
+    let ops =
+      List.map (fun ps ->
+        match EcEnv.Op.lookup_opt (unloc ps) env with
+        | None   -> tc_lookup_error !!tc ~loc:ps.pl_loc `Operator (unloc ps)
+        | Some p -> fst p) ops
+    in
+    EcEnv.SimplifyContext.set_opacity
+      (List.map (fun p -> (p, opq)) ops) simpl)
+    simpl specs
+
 (* -------------------------------------------------------------------- *)
 let process_local_hint (hint : plocalhint) (tc : tcenv1) =
   let env = FApi.tc1_env tc in
@@ -137,8 +152,13 @@ let process_local_hint (hint : plocalhint) (tc : tcenv1) =
             in
             (mode, List.rev ops))
         in
-        hd |> Option.fold ~none:simpl ~some:(fun hd ->
-          EcEnv.SimplifyContext.set_default_hd (Some hd) simpl)
+        let simpl =
+          hd |> Option.fold ~none:simpl ~some:(fun hd ->
+            EcEnv.SimplifyContext.set_default_hd (Some hd) simpl)
+        in
+
+        (* reduction-opacity overrides ([-delta ops] / [+delta ops]) *)
+        apply_hint_opacity tc env h.ph_opacity simpl
 
     | PLHClear base ->
         EcEnv.SimplifyContext.clear ?base simpl
@@ -205,6 +225,9 @@ let process_simplify_info ri (tc : tcenv1) =
     ) simpl hint.ph_lemmas
   in
 
+  (* Per-call reduction-opacity overrides ([-delta ops] / [+delta ops]). *)
+  let simpl = apply_hint_opacity tc env hint.ph_opacity simpl in
+
   (* Database list consulted by this call: the unsigned selection if any
      (else the proof-local default / active set), with the signed
      activate / deactivate deltas applied in order. [None] when no [hint]

src/ecLowGoal.ml

@@ -423,6 +423,13 @@ let rec t_lazy_match ?(reduce = `Full) ?(texn = fun _ -> raise InvalidGoalShape)
       | `None    -> raise InvalidGoalShape
       | `Full    -> EcReduction.full_red
       | `NoDelta -> EcReduction.nodelta in
+    (* honor proof-local [-delta op] opacity overrides without changing
+       which simplify databases the strategy consults *)
+    let strategy =
+      { strategy with
+          EcReduction.user_local =
+            EcEnv.SimplifyContext.opacity_only
+              (FApi.tc1_simplify_context tc) } in
     FApi.t_seq (FApi.t_or (t_hred_with_info strategy) texn) (t_lazy_match ~reduce tx) tc
 
 (* -------------------------------------------------------------------- *)
@@ -2542,7 +2549,12 @@ let t_crush ?(delta = true) ?tsolve (tc : tcenv1) =
     { cs_undosubst = Sid.empty (*Sid.of_list (List.map fst (LDecl.tohyps (FApi.tc1_hyps tc)).h_local)*) ;
       cs_sbeq = (* Sid.of_list (List.map fst (LDecl.tohyps (FApi.tc1_hyps tc)).h_local)*) Sid.empty;
     } in
-  FApi.t_seq (entry state) (t_simplify_with_info EcReduction.nodelta) tc
+  let final =
+    { EcReduction.nodelta with
+        EcReduction.user_local =
+          EcEnv.SimplifyContext.opacity_only
+            (FApi.tc1_simplify_context tc) } in
+  FApi.t_seq (entry state) (t_simplify_with_info final) tc
 
 
 (* -------------------------------------------------------------------- *)
@@ -2914,6 +2926,11 @@ let t_crush_fwd ?(delta = true) nb_intros (tc : tcenv1) =
     | _ -> t_fail tc
   in
 
+  let final =
+    { EcReduction.nodelta with
+        EcReduction.user_local =
+          EcEnv.SimplifyContext.opacity_only
+            (FApi.tc1_simplify_context tc) } in
   FApi.t_seq
     (aux0 nb_intros)
-    (t_simplify_with_info EcReduction.nodelta) tc
+    (t_simplify_with_info final) tc

src/ecParser.mly

@@ -2551,6 +2551,7 @@ simplify_hint_item:
 | m=pmode x=lident             { `Db    (m = `Plus, unloc x) }
 | m=pmode l=bracket(qoident+)  { `Hd    (m, l) }
 | l=brace(qident+)             { `Lemma l }
+| m=pmode DELTA l=qoident+     { `Opacity (m = `Minus, l) }
 
 (* The body of a [hint] clause: an unsigned base database selection
    followed by items. A clause may not both select databases (unsigned
@@ -2568,6 +2569,7 @@ simplify_hint_body:
             let m = match m with `Plus -> `Include | `Minus -> `Exclude in
             { h with ph_hd = Some (m, l) }
         | `Lemma l -> { h with ph_lemmas = h.ph_lemmas @ l }
+        | `Opacity (b, l) -> { h with ph_opacity = h.ph_opacity @ [(b, l)] }
       in
       let h =
         List.fold_left doit
@@ -3948,7 +3950,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

@@ -575,14 +575,16 @@ type pmpred_args = (osymbol * pformula) list
    [ph_lemmas] are lemmas added to the default DB for this call (lemma
    sets are add-only -- the head filter restricts which rules apply). *)
 type psimplify_hint = {
-  ph_select : symbol list;
-  ph_dbs    : (bool * symbol) list;
-  ph_hd     : ([`Include | `Exclude] * pqsymbol list) option;
-  ph_lemmas : pqsymbol list;
+  ph_select  : symbol list;
+  ph_dbs     : (bool * symbol) list;
+  ph_hd      : ([`Include | `Exclude] * pqsymbol list) option;
+  ph_lemmas  : pqsymbol list;
+  (* [-delta ops] / [+delta ops]: true = make reduction-opaque *)
+  ph_opacity : (bool * pqsymbol list) list;
 }
 
 let empty_simplify_hint = {
-  ph_select = []; ph_dbs = []; ph_hd = None; ph_lemmas = [];
+  ph_select = []; ph_dbs = []; ph_hd = None; ph_lemmas = []; ph_opacity = [];
 }
 
 (* -------------------------------------------------------------------- *)
@@ -1509,7 +1511,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