From 3a1b94cd9e49b26342eeb6c60ce6ce220515e9e1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Dupressoir?= <fdupress@gmail.com>
Date: Wed, 3 Jun 2026 15:30:49 +0100
Subject: [PATCH] [cryptolib] generalize PRF definitions, PRP<->PRF

---
 theories/crypto/PRF.eca                  | 27 +++++++++---------------
 theories/crypto/prp_prf/Strong_RP_RF.eca |  1 -
 2 files changed, 10 insertions(+), 18 deletions(-)

diff --git a/theories/crypto/PRF.eca b/theories/crypto/PRF.eca
index 8725b35214..4de755096e 100644
--- a/theories/crypto/PRF.eca
+++ b/theories/crypto/PRF.eca
@@ -57,30 +57,23 @@ end RF.
 abstract theory PseudoRF.
 type K.
 
-op dK: { K distr | is_lossless dK } as dK_ll.
-
-op F : K -> D -> R.
-
 module type PseudoRF = {
   proc keygen(): K
-  proc f(_ : K * D): R
+  proc f(_: K * D): R
 }.
 
-module PseudoRF = {
-  proc keygen() = {
-    var k;
+module PRF (P : PseudoRF) = {
+  var k : K
 
-    k <$ dK;
-    return k;
+  proc init() = {
+    k <@ P.keygen();
   }
 
-  proc f(k, x) = { return F k x; }
-}.
-
-module PRF = {
-  var k : K
+  proc f(x: D) = {
+    var r;
 
-  proc init() = { k <$ dK; }
-  proc f(x: D) = { return F k x; }
+    r <@ P.f(k, x);
+    return r;
+  }
 }.
 end PseudoRF.
diff --git a/theories/crypto/prp_prf/Strong_RP_RF.eca b/theories/crypto/prp_prf/Strong_RP_RF.eca
index 435ecbadcf..785a6773ce 100644
--- a/theories/crypto/prp_prf/Strong_RP_RF.eca
+++ b/theories/crypto/prp_prf/Strong_RP_RF.eca
@@ -12,7 +12,6 @@ op uD: { D distr | is_uniform uD /\ is_lossless uD /\ is_full uD } as uD_uf_fu.
 
 (** and a type K equipped with a lossless distribution **)
 type K.
-op dK: { K distr | is_lossless dK } as dK_ll.
 
 clone import PRP as PRPt with
   type D  <- D.