From b2838c1585dd02532d3f164fec2ee83c37ba5b49 Mon Sep 17 00:00:00 2001
From: Matthias Meijers <research@mmeijers.com>
Date: Wed, 8 Jan 2025 15:10:12 +0100
Subject: [PATCH] Fixing dependencies on old stuff.

---
 proofs/FO_T.eca                   |  6 ++----
 proofs/PublicKeyEncryptionROM.eca | 13 -------------
 2 files changed, 2 insertions(+), 17 deletions(-)

diff --git a/proofs/FO_T.eca b/proofs/FO_T.eca
index 07a77a5..3b86a17 100644
--- a/proofs/FO_T.eca
+++ b/proofs/FO_T.eca
@@ -41,13 +41,11 @@ clone import PublicKeyEncryptionROM as PKEROM with
   type ctxt_t <- ctxt_t,
   
   type in_t <- ptxt_t,
-  type out_t <- rand_t,
+  type out_t <- rand_t
 
-    op F_RO.dout <- drandm
-    
   proof *.  
   
-import PKE F_RO.
+import PKE.
 import DeltaCorrectROM DeltaCorrect.
 
 (*
diff --git a/proofs/PublicKeyEncryptionROM.eca b/proofs/PublicKeyEncryptionROM.eca
index da6c2d0..1c49e17 100644
--- a/proofs/PublicKeyEncryptionROM.eca
+++ b/proofs/PublicKeyEncryptionROM.eca
@@ -960,19 +960,6 @@ module OW_CPA_O_ROM (RO : RandomOraclei) (S : Scheme_ROM) (O : Oracles_PCi_ROM)
   }
 }.
 
-(** OW-CPA (final check performed with oracle) security game in ROM **)
-module OW_CPA_O_ROM (RO : RandomOraclei, S : Scheme_ROM, O : Oracles_PCi_ROM, A : Adv_OWCPA_ROM) = {
-  proc main() : bool = {
-    var r : bool;
-    
-    RO.init();
-    
-    r <@ OW_CPA_O(S(RO), O(RO), A(RO)).main();
-    
-    return r;    
-  }
-}.
-
 
 (* 
   One-Wayness under Plaintext-Checking Attacks (OW-PCA) in ROM