From b2fcc8e8dc4b5b17b00116acc7d2112d5bce863d Mon Sep 17 00:00:00 2001
From: Matthias Meijers <research@mmeijers.com>
Date: Thu, 2 Jan 2025 19:50:12 +0100
Subject: [PATCH] Fixed import errors updated KEM and PKE libraries.

---
 proofs/FO_KEM.eca     |  3 ---
 proofs/KEM_KDF_PP.eca | 25 ++++++++++++++++++++++---
 tmp/testpp.eca        | 36 ++++++++++++++++++++++++++++++++++++
 3 files changed, 58 insertions(+), 6 deletions(-)
 create mode 100644 tmp/testpp.eca

diff --git a/proofs/FO_KEM.eca b/proofs/FO_KEM.eca
index 83e5ee3..c6bf74b 100644
--- a/proofs/FO_KEM.eca
+++ b/proofs/FO_KEM.eca
@@ -34,6 +34,3 @@ clone import PublicKeyEncryptionROM as PKEROM with
   
   type in_t <- ptxt_t,
   type out_t <- rand_t.
-
-import PKE F_RO.
-import DeltaCorrectROM.
diff --git a/proofs/KEM_KDF_PP.eca b/proofs/KEM_KDF_PP.eca
index fa2b2c7..2faad05 100644
--- a/proofs/KEM_KDF_PP.eca
+++ b/proofs/KEM_KDF_PP.eca
@@ -1,4 +1,4 @@
-require import AllCore Distr.
+require import AllCore Distr PROM.
 require KeyEncapsulationMechanismsROM.
 
 
@@ -26,6 +26,13 @@ type rand_t.
 **)
 theory PPKDFKCT.
 (* Clones and imports *)
+clone import FullRO as F_RO with
+  type in_t <- key_t * ctxt_t,
+  type out_t <- key_t
+  
+  proof *.
+
+  
 (* Definitions for KEMs in ROM *)
 clone import KeyEncapsulationMechanismsROM as KEMsROM with
   type pk_t <- pk_t,
@@ -42,7 +49,7 @@ clone import KeyEncapsulationMechanismsROM as KEMsROM with
 clone import MALBINDROM with
   type rand_t <- rand_t.
 
-import MALBIND KEMs F_RO.
+import MALBIND KEMs.
 
 
 (* Properties (other) *)
@@ -242,6 +249,12 @@ end PPKDFKCT.
 **)
 theory PPKDFKPK.
 (* Clones and imports *)
+clone import FullRO as F_RO with
+  type in_t <- key_t * pk_t,
+  type out_t <- key_t
+  
+  proof *.
+  
 (* Definitions for KEMs in ROM *)
 clone import KeyEncapsulationMechanismsROM as KEMsROM with
   type pk_t <- pk_t,
@@ -258,7 +271,7 @@ clone import KeyEncapsulationMechanismsROM as KEMsROM with
 clone import MALBINDROM with
   type rand_t <- rand_t.
 
-import MALBIND KEMs F_RO.
+import MALBIND KEMs.
 
 
 (* Properties (other) *)
@@ -459,6 +472,12 @@ end PPKDFKPK.
 **)
 theory PPKDFKCTPK.
 (* Clones and imports *)
+clone import FullRO as F_RO with
+  type in_t <- key_t * ctxt_t * pk_t,
+  type out_t <- key_t
+  
+  proof *.
+  
 (* Definitions for KEMs in ROM *)
 clone import KeyEncapsulationMechanismsROM as KEMsROM with
   type pk_t <- pk_t,
diff --git a/tmp/testpp.eca b/tmp/testpp.eca
new file mode 100644
index 0000000..918cd33
--- /dev/null
+++ b/tmp/testpp.eca
@@ -0,0 +1,36 @@
+require KeyEncapsulationMechanisms.
+
+clone import KeyEncapsulationMechanisms as KEMs.
+
+print HON_BIND.
+
+
+module T = {
+  proc main(bc : bindconf) : unit = {
+    var pk0 : pk_t;
+    var pk1 : pk_t;
+    var sk0 : sk_t;
+    var sk1 : sk_t;
+    var b : bool;
+    var c0 : ctxt_t;
+    var c1 : ctxt_t;
+    var k0 : key_t option;
+    var k1 : key_t option;
+    var no_fail : bool;
+    
+    
+    if (is_pkbsc bc) 
+      (pk1, sk1) <- (pk0, sk0);
+    else {
+      if (is_pkbtc bc) 
+        (pk1, sk1) <- witness;
+      else {
+        b <- false ;
+        if (b) 
+          (pk1, sk1) <- witness;
+        else 
+          (pk1, sk1) <- (pk0, sk0);
+      }
+    } 
+  }
+}.