Fixed import errors updated KEM and PKE libraries.

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.

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,

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);
+      }
+    } 
+  }
+}.