fix(clone): compare oracle-call restrictions when overriding a module type

src/ecReduction.ml

@@ -291,6 +291,16 @@ end) = struct
   and for_module_sig_body env b1 b2 =
     List.for_all2 (for_module_sig_body_item env) b1 b2
 
+  (* ------------------------------------------------------------------ *)
+  (* Allowed oracle calls are compared as sets, per procedure. *)
+  and for_oracle_infos env ~norm ois1 ois2 =
+    let allowed oi =
+      let calls = OI.allowed oi in
+      let calls = if norm then List.map (NormMp.norm_xfun env) calls else calls in
+      Sx.of_list calls in
+    EcSymbols.Msym.equal
+      (fun oi1 oi2 -> Sx.equal (allowed oi1) (allowed oi2)) ois1 ois2
+
   (* ------------------------------------------------------------------ *)
   and for_module_sig env ~norm ms1 ms2 =
     let p1 = ms1.mis_params in
@@ -300,7 +310,10 @@ end) = struct
     let env, s = add_modules env p2 p1 in
     let body1 = ms1.mis_body in
     let body2 = EcSubst.subst_modsig_body s ms2.mis_body in
-    for_module_sig_body env body1 body2
+    for_module_sig_body env body1 body2 &&
+    let ois1 = ms1.mis_oinfos in
+    let ois2 = EcSubst.subst_oracle_infos s ms2.mis_oinfos in
+    for_oracle_infos env ~norm ois1 ois2
 
   (* ------------------------------------------------------------------ *)
   let for_variable env v1 v2 =

tests/clone-modtype-oinfos.ec

@@ -0,0 +1,30 @@
+(* Regression for #1123: `clone ... with module type X <- Y` must compare the
+   oracle-call restrictions of X and Y, not only procedure names and types.
+   Lemmas proved for `A <: X` are replayed verbatim for `A <: Y`, so the
+   allowed-call sets must coincide exactly (as sets, order-insensitively). *)
+require import AllCore.
+
+theory T.
+  module type ORCL = { proc g() : unit  proc h() : unit  proc k() : unit }.
+  module type ADV (O : ORCL) = { proc f() : unit {O.g, O.h} }.
+  module type GAME (A : ADV) = { proc main() : bool }.
+end T.
+
+module type ADV_looser  (O : T.ORCL) = { proc f() : unit {O.g, O.h, O.k} }.
+module type ADV_tighter (O : T.ORCL) = { proc f() : unit {O.g} }.
+module type ADV_reorder (O : T.ORCL) = { proc f() : unit {O.h, O.g} }.
+
+fail clone T as U1 with module type ADV <- ADV_looser.
+fail clone T as U2 with module type ADV <- ADV_tighter.
+fail clone T as U3 with module type ADV =  ADV_looser.
+fail clone T as U4 with module type ADV <= ADV_tighter.
+
+clone T as U5 with module type ADV <- ADV_reorder.
+
+(* The oracle sets of functor parameters' signatures are compared too. *)
+module type GAME_looser  (A : ADV_looser)  = { proc main() : bool }.
+module type GAME_reorder (A : ADV_reorder) = { proc main() : bool }.
+
+fail clone T as U6 with module type GAME <- GAME_looser.
+
+clone T as U7 with module type GAME <- GAME_reorder.