Start cleanup of ROM proofs and think more about abstractions.

proofs/DoubleROM.eca

@@ -1,6 +1,5 @@
 require import AllCore Distr List FMap PROM.
 
-
 lemma size_behead (s : 'a list) : 
   size (behead s) = if s = [] then 0 else size s - 1.
 proof. by elim: s. qed.
@@ -18,7 +17,6 @@ rewrite -(perm_cons x) => peqxc.
 rewrite (perm_eq_trans _ _ _ peqxc) perm_eq_sym perm_to_rem 1:/#.
 qed.
 
-
 lemma uniq_drop (s : 'a list) (n : int) :
   uniq s => uniq (drop n s). 
 proof. by elim: s n => // /#. qed.
@@ -2408,5 +2406,4 @@ hoare. progress. smt(pmax_ge0).
 trivial.
 qed.
 
-
-
+end section.

proofs/HashFunctionsAlt.eca

@@ -0,0 +1,55 @@
+require import AllCore Distr.
+
+type in_t.
+
+type out_t.
+
+op f : in_t -> out_t.
+
+module type Adv_CRAlt = {
+  proc find() : in_t * in_t 
+}.
+
+module CRAlt(A : Adv_CRAlt) = {
+  proc main() : bool = {
+    var x1, x2 : in_t;
+
+    (x1, x2) <@ A.find();
+
+    return f x1 = f x2;
+  }
+}.
+
+
+theory ROM.
+
+module type KHF_ROi = {
+  proc init() : unit
+  proc get(x : in_t) : out_t
+}.
+
+module type KHF_RO = {
+  include KHF_ROi [init]
+}.
+
+module type Adv_CRAlt_ROM (F_RO : KHF_RO) = {
+  include Adv_CRAlt
+}.
+
+module CRAlt_ROM (F_RO : KHF_ROi) (A : Adv_CRAlt_ROM) = { 
+  proc main() : bool = { 
+    var x1, x2 : in_t;
+    var y1, y2 : out_t;
+
+    F_RO.init();
+
+    (x1, x2) <@ A(F_RO).find();
+
+    y1 <@ F_RO.get(x1);
+    y2 <@ F_RO.get(x2);
+
+    return y1 = y2;
+  }
+}.
+
+end ROM.

proofs/HashFunctionsx2.eca

@@ -1,31 +1,71 @@
 require import AllCore.
-require HashFunctions.
 
-
-type in_t.
+type in_t1.
+type in_t2.
 type out_t.
-op f : in_t -> out_t.
 
-clone import HashFunctions as F with
-  type in_t <- in_t,
-  type out_t <- out_t,
-
-  op f <- f
-
-  proof *.
-
+op f : in_t1 -> out_t.
+op g : in_t2 -> out_t.
 
-type in_t2.
-type out_t2.
-op g : in_t2 -> out_t2.
+module type Adv_CRx2 = {
+  proc find() : in_t1 * in_t2
+}.
+
+module CRx2 (A : Adv_CRx2) = {
+  proc main() : bool = {
+    var x1 : in_t1;
+    var x2 : in_t2;
+
+    (x1, x2) <@ A.find();
+
+    return f x1 = g x2;
+  }
+}.
 
-clone import HashFunctions as G with
-  type in_t <- in_t2,
-  type out_t <- out_t2,
-
-  op f <- g
-
-  proof *.
 
+theory ROM.
 
+
+module type KHF_RO1i = {
+  proc init() : unit
+  proc get(x : in_t1) : out_t
+}.
+
+module type KHF_RO2i = {
+  proc init() : unit
+  proc get(x : in_t2) : out_t
+}.
+
+module type KHF_RO1 = {
+  include KHF_RO1i [init]
+}.
+
+module type KHF_RO2 = {
+  include KHF_RO2i [init]
+}.
+
+
+module type Adv_CRx2_ROM (F_RO : KHF_RO1) (G_RO : KHF_RO2) = {
+  include Adv_CRx2
+}.
+
+
+module CRx2_ROM (F_RO : KHF_RO1i) (G_RO : KHF_RO2i) (A : Adv_CRx2_ROM) = { 
+  proc main() : bool = { 
+    var x1 : in_t1;
+    var x2 : in_t2;
+    var y1, y2 : out_t;
+
+    F_RO.init();
+    G_RO.init();
+
+    (x1, x2) <@ A(F_RO, G_RO).find();
 
+    y1 <@ F_RO.get(x1);
+    y2 <@ G_RO.get(x2);
+
+    return y1 = y2;
+  }
+}.
+
+end ROM.

proofs/KeyedHashFunctionsAlt.eca

@@ -0,0 +1,68 @@
+require import AllCore Distr.
+require KeyedHashFunctionsx2.
+
+type key_t.
+
+type in_t.
+
+type out_t.
+
+op f : key_t -> in_t -> out_t.
+
+op dkey : key_t distr.
+
+module type Adv_CRAlt = {
+  proc find(k1 : key_t, k2 : key_t) : in_t * in_t 
+}.
+
+module CRAlt(A : Adv_CRAlt) = {
+  proc main() : bool = {
+    var k1, k2 : key_t;
+    var x1, x2 : in_t;
+
+    k1 <$ dkey;
+    k2 <$ dkey;
+
+    (x1, x2) <@ A.find(k1, k2);
+
+    return f k1 x1 = f k2 x2;
+  }
+}.
+
+
+theory ROM.
+
+module type KHF_ROi = {
+  proc init() : unit
+  proc get(kx : key_t * in_t) : out_t
+}.
+
+module type KHF_RO = {
+  include KHF_ROi [init]
+}.
+
+module type Adv_CRAlt_ROM (F_RO : KHF_RO) = {
+  include Adv_CRAlt
+}.
+
+module CRAlt_ROM (F_RO : KHF_ROi) (A : Adv_CRAlt_ROM) = { 
+  proc main() : bool = { 
+    var k1, k2 : key_t;
+    var x1, x2 : in_t;
+    var y1, y2 : out_t;
+
+    F_RO.init();
+
+    k1 <$ dkey;
+    k2 <$ dkey;
+
+    (x1, x2) <@ A(F_RO).find(k1, k2);
+
+    y1 <@ F_RO.get((k1, x1));
+    y2 <@ F_RO.get((k2, x2));
+
+    return y1 = y2;
+  }
+}.
+
+end ROM.

proofs/KeyedHashFunctionsx2.eca

@@ -0,0 +1,89 @@
+require import AllCore Distr.
+
+type key_t1.
+type key_t2.
+
+type in_t1.
+type in_t2.
+
+type out_t.
+
+op f : key_t1 -> in_t1 -> out_t.
+op g : key_t2 -> in_t2 -> out_t.
+
+op dkey1 : key_t1 distr.
+op dkey2 : key_t2 distr.
+
+
+module type Adv_CRx2 = {
+  proc find(k1 : key_t1, k2 : key_t2) : in_t1 * in_t2
+}.
+
+module CRx2 (A : Adv_CRx2) = {
+  proc main() : bool = {
+    var k1 : key_t1;
+    var k2 : key_t2;
+    var x1 : in_t1;
+    var x2 : in_t2;
+
+    k1 <$ dkey1;
+    k2 <$ dkey2;
+
+    (x1, x2) <@ A.find(k1, k2);
+
+    return f k1 x1 = g k2 x2;
+  }
+}.
+
+
+
+theory ROM.
+
+module type KHF_RO1i = {
+  proc init() : unit
+  proc get(kx : key_t1 * in_t1) : out_t
+}.
+
+module type KHF_RO2i = {
+  proc init() : unit
+  proc get(kx : key_t2 * in_t2) : out_t
+}.
+
+module type KHF_RO1 = {
+  include KHF_RO1i [init]
+}.
+
+module type KHF_RO2 = {
+  include KHF_RO2i [init]
+}.
+
+
+module type Adv_CRx2_ROM (F_RO : KHF_RO1) (G_RO : KHF_RO2) = {
+  include Adv_CRx2
+}.
+
+
+module CRx2_ROM (F_RO : KHF_RO1i) (G_RO : KHF_RO2i) (A : Adv_CRx2_ROM) = { 
+  proc main() : bool = { 
+    var k1 : key_t1;
+    var k2 : key_t2;
+    var x1 : in_t1;
+    var x2 : in_t2;
+    var y1, y2 : out_t;
+
+    F_RO.init();
+    G_RO.init();
+
+    k1 <$ dkey1;
+    k2 <$ dkey2;
+
+    (x1, x2) <@ A(F_RO, G_RO).find(k1, k2);
+
+    y1 <@ F_RO.get((k1, x1));
+    y2 <@ G_RO.get((k2, x2));
+
+    return y1 = y2;
+  }
+}.
+
+end ROM.