From e15dc7b460016a64a750eaee3beb949eea2ac464 Mon Sep 17 00:00:00 2001
From: Sebastian Ertel <sebastian.ertel@gmail.com>
Date: Mon, 6 May 2024 22:12:57 +0200
Subject: [PATCH 1/3] the functional correctness proof for signatures.

---
 theories/examples/Sig_Prot.v | 101 ++++++++++++++++++++++++++++++++---
 1 file changed, 93 insertions(+), 8 deletions(-)

diff --git a/theories/examples/Sig_Prot.v b/theories/examples/Sig_Prot.v
index 1964bcd..8a79283 100644
--- a/theories/examples/Sig_Prot.v
+++ b/theories/examples/Sig_Prot.v
@@ -65,25 +65,26 @@ Module Type SignatureProt
 
   Import π1 π2 KG Alg Prim.
 
-  Definition Sig_prot_ifce := 
-    [interface #val #[sign] : 'message → 'pubkey × ('signature × 'bool) ].
+  Definition protocol := 30.
+  Definition Sig_prot_ifce :=
+    [interface #val #[protocol] : 'message → 'pubkey × ('signature × 'bool) ].
 
   Definition Sig_prot : package Sig_locs_real Sig_ifce Sig_prot_ifce
     := [package
-      #def  #[sign] (msg : 'message) : 'pubkey × ('signature × 'bool)
+      #def  #[protocol] (msg : 'message) : 'pubkey × ('signature × 'bool)
       {
         #import {sig #[get_pk] : 'unit → 'pubkey } as get_pk ;;
         #import {sig #[sign] : 'message → 'signature  } as sign ;;
         #import {sig #[verify_sig] : ('signature × 'message) → 'bool } as verify_sig ;;
-  
+
         (* Protocol *)
         pk ← get_pk tt ;;
         sig ← sign msg ;;
         bool ← verify_sig (sig, msg) ;;
         ret (pk, ( sig, bool ))
-      } 
+      }
     ].
-  
+
 
   Equations Sig_prot_real : package Sig_locs_real [interface] Sig_prot_ifce :=
     Sig_prot_real := {package Sig_prot ∘ Sig_real_c }.
@@ -129,7 +130,7 @@ Module Type SignatureProt
     Defined.
 
   Lemma ext_unforge_sig_prot:
-  Sig_prot_real ≈₀ Sig_prot_ideal.
+    Sig_prot_real ≈₀ Sig_prot_ideal.
   Proof.
     eapply (eq_rel_perf_ind_ignore (fset [:: sign_loc])).
     - rewrite /Sig_locs_real/Sig_locs_ideal.
@@ -157,6 +158,90 @@ Module Type SignatureProt
            apply Signature_prop.
       ---- by [move: pre; rewrite /inv_conj; repeat case].
   Qed.
-      
+
+  Module Correctness.
+    Definition prot_res := 100.
+
+    Definition Prot_res_ifce :=
+      [interface #val #[prot_res] : 'message → 'unit ].
+
+
+    Equations prot_result (msg : 'message) : code Sig_locs_real Sig_prot_ifce 'bool :=
+      prot_result msg := {code
+        #import {sig #[protocol] : 'message → 'pubkey × ('signature × 'bool) } as protocol ;;
+        '(pk, t) ← protocol msg;;
+        let '(_, result) := t in
+        ret result
+    }.
+
+    (* FIXME This just cannot simplify because it is not clear what the import is! *)
+    Theorem prot_correct seed msg:
+        Run sampler (prot_result msg) seed = Some true.
+    Proof.
+      simpl.
+    Admitted.
+
+
+    Equations prot_result_pkg : package Sig_locs_real Sig_prot_ifce Prot_res_ifce
+      :=
+      prot_result_pkg := [package
+            #def  #[prot_res] (msg : 'message) : 'unit
+            {
+              #import {sig #[protocol] : 'message → 'pubkey × ('signature × 'bool) } as protocol ;;
+              '(_, t) ← protocol msg;;
+              let '(_, result) := t in
+              ret tt
+            }
+        ].
+
+    (* TODO Why do I need this cast here? *)
+    Definition tt_ : chElement 'unit := tt.
+
+    Equations prot_result_pkg' : package Sig_locs_real Sig_prot_ifce Prot_res_ifce
+      :=
+      prot_result_pkg' := [package
+        #def  #[prot_res] (msg : 'message) : 'unit
+        {
+          #import {sig #[protocol] : 'message → 'pubkey × ('signature × 'bool) } as protocol ;;
+          '(_, t) ← protocol msg;;
+          let '(_, result) := t in
+          #assert (result == true) ;;
+          ret tt_
+        }
+        ].
+
+    Equations prot_result_real : package Sig_locs_real [interface] Prot_res_ifce :=
+      prot_result_real := {package prot_result_pkg ∘ Sig_prot ∘ Sig_real_c }.
+    Next Obligation.
+      ssprove_valid.
+      all: by [apply: fsubsetxx].
+    Defined.
+
+    Equations prot_result_real' : package Sig_locs_real [interface] Prot_res_ifce :=
+      prot_result_real' := {package prot_result_pkg' ∘ Sig_prot ∘ Sig_real_c }.
+    Next Obligation.
+      ssprove_valid.
+      all: by [apply: fsubsetxx].
+    Defined.
+
+    Lemma fun_correct:
+      prot_result_real ≈₀ prot_result_real'.
+    Proof.
+      eapply eq_rel_perf_ind_eq.
+      simplify_eq_rel x.
+      all: simplify_linking; ssprove_code_simpl.
+      repeat ssprove_sync_eq.
+      move => _.
+      ssprove_sync_eq => sk.
+      ssprove_sync_eq => pk.
+      rewrite /tt_.
+      have correct_prop: forall p s m, Ver_sig p (Sign s m) m == true.
+      1: { admit.} (* FIXME specify correctness condition *)
+      rewrite (correct_prop pk sk x) /=.
+      apply r_ret => s0 s1 s0_eq_s1 //=.
+    Qed.
+
+  End Correctness.
+
 End SignatureProt.
 

From 68f2d704e51d74c6f833074b412a5e194e5b9c5a Mon Sep 17 00:00:00 2001
From: Sebastian Ertel <sebastian.ertel@gmail.com>
Date: Tue, 7 May 2024 14:57:17 +0200
Subject: [PATCH 2/3] final functional correctness property.

---
 theories/examples/Sig_Prot.v  | 5 ++---
 theories/examples/Signature.v | 3 +++
 2 files changed, 5 insertions(+), 3 deletions(-)

diff --git a/theories/examples/Sig_Prot.v b/theories/examples/Sig_Prot.v
index 8a79283..e5a7c69 100644
--- a/theories/examples/Sig_Prot.v
+++ b/theories/examples/Sig_Prot.v
@@ -160,6 +160,7 @@ Module Type SignatureProt
   Qed.
 
   Module Correctness.
+
     Definition prot_res := 100.
 
     Definition Prot_res_ifce :=
@@ -235,9 +236,7 @@ Module Type SignatureProt
       ssprove_sync_eq => sk.
       ssprove_sync_eq => pk.
       rewrite /tt_.
-      have correct_prop: forall p s m, Ver_sig p (Sign s m) m == true.
-      1: { admit.} (* FIXME specify correctness condition *)
-      rewrite (correct_prop pk sk x) /=.
+      rewrite (Signature_correct pk sk x) /=.
       apply r_ret => s0 s1 s0_eq_s1 //=.
     Qed.
 
diff --git a/theories/examples/Signature.v b/theories/examples/Signature.v
index 69c2cdc..31b4b1b 100644
--- a/theories/examples/Signature.v
+++ b/theories/examples/Signature.v
@@ -159,6 +159,9 @@ Module Type SignatureAlgorithms
       (s : Signature) (pk : PubKey) (m  : chMessage),
       Ver_sig pk s m = ((s,m) \in domm l).
 
+  (* Functional correctness property for signatures *)
+  Parameter Signature_correct: forall pk sk msg, Ver_sig pk (Sign sk msg) msg == true.
+
 End SignatureAlgorithms.
 
 Module Type SignaturePrimitives

From b573013f1c34d80519480e5fc5e0412d3618b1fa Mon Sep 17 00:00:00 2001
From: Sebastian Ertel <sebastian.ertel@gmail.com>
Date: Tue, 7 May 2024 15:03:27 +0200
Subject: [PATCH 3/3] removing checks and prints

---
 theories/examples/RA.v        |  6 ------
 theories/examples/Signature.v | 29 ++++++++++++++---------------
 2 files changed, 14 insertions(+), 21 deletions(-)

diff --git a/theories/examples/RA.v b/theories/examples/RA.v
index 68b5920..3b743ca 100644
--- a/theories/examples/RA.v
+++ b/theories/examples/RA.v
@@ -568,8 +568,6 @@ Module Type RemoteAttestationHash
       auto_in_fset.
   Qed.
 
-  (*Print extructures.ord.tag_ordType.*)
-
   Lemma INV'_full_heap_eq'_get : forall s1 s2,
       full_heap_eq' (s1, s2) ->
       ∀ l,
@@ -728,15 +726,11 @@ Module Type RemoteAttestationHash
       injective f -> (* if this is bijective then I would not end up in omap! *)
       fmap_kmap' f (setm m k v) = setm (fmap_kmap' f m) (f k) v.
   Proof.
-    Print fmap_kmap'.
     move => f k v m inj_f.
     rewrite /fmap_kmap'.
     Fail rewrite [X in _ = setm _ X]mapm2E.
     (* TODO *)
-    Check eq_fmap.
     (* rewrite -eq_fmap. *)
-    Locate "=1".
-    Print eqfun.
 
    (** * Approach 1:
 
diff --git a/theories/examples/Signature.v b/theories/examples/Signature.v
index 31b4b1b..6d628d7 100644
--- a/theories/examples/Signature.v
+++ b/theories/examples/Signature.v
@@ -75,8 +75,8 @@ End SignatureConstraints.
 (** |     KEY      |
     |  GENERATION  | **)
 
-Module Type KeyGeneration 
-    (π1 : SignatureParams) 
+Module Type KeyGeneration
+    (π1 : SignatureParams)
     (π2 : SignatureConstraints).
 
   Import π1 π2.
@@ -125,37 +125,37 @@ Module Type KeyGeneration
   Definition Key_Gen : package Key_locs [interface] KeyGen_ifce
   := [package
        #def  #[key_gen] (_ : 'unit) : ('seckey × 'pubkey)
-       { 
-         let (sk, pk) := KeyGen in 
+       {
+         let (sk, pk) := KeyGen in
          #put sk_loc := sk ;;
          #put pk_loc := pk ;;
-         
-         ret (sk, pk)      
+
+         ret (sk, pk)
        }
      ].
- 
+
 End KeyGeneration.
 
 (** |  SIGNATURE  |
     |   SCHEME    | **)
 
-Module Type SignatureAlgorithms 
-    (π1 : SignatureParams) 
-    (π2 : SignatureConstraints) 
+Module Type SignatureAlgorithms
+    (π1 : SignatureParams)
+    (π2 : SignatureConstraints)
     (π3 : KeyGeneration π1 π2).
 
   Import π1 π2 π3.
 
   Parameter Sign : ∀ (sk : SecKey) (m : chMessage), Signature.
 
-  Parameter Ver_sig : ∀ (pk :  PubKey) (sig : Signature) (m : chMessage), 
+  Parameter Ver_sig : ∀ (pk :  PubKey) (sig : Signature) (m : chMessage),
    'bool.
 
   (* TODO: fmap (Signature * A * A ) -> (Signature * A * A )  triggert endless loop  *)
 
   (* Final proposition for a signature scheme to be indistinguishable *)
   Parameter Signature_prop:
-    ∀ (l: {fmap (Signature  * chMessage ) -> 'unit}) 
+    ∀ (l: {fmap (Signature  * chMessage ) -> 'unit})
       (s : Signature) (pk : PubKey) (m  : chMessage),
       Ver_sig pk s m = ((s,m) \in domm l).
 
@@ -168,7 +168,7 @@ Module Type SignaturePrimitives
   (π1 : SignatureParams)
   (π2 : SignatureConstraints)
   (KG : KeyGeneration π1 π2)
-  (Alg : SignatureAlgorithms π1 π2 KG).  
+  (Alg : SignatureAlgorithms π1 π2 KG).
 
   Import π1 π2 KG Alg.
 
@@ -186,7 +186,7 @@ Module Type SignaturePrimitives
 
   (* The signature scheme requires a heap location to store the seen signatures. *)
   Definition Sig_locs_real := Key_locs.
-  Definition Sig_locs_ideal := Sig_locs_real :|: fset [:: sign_loc ]. 
+  Definition Sig_locs_ideal := Sig_locs_real :|: fset [:: sign_loc ].
 
   Definition Sig_ifce := [interface 
     #val #[get_pk] : 'unit → 'pubkey ;
@@ -291,7 +291,6 @@ Module Type SignaturePrimitives
   Sig_real_c ≈₀ Sig_ideal_c.
   Proof.
     eapply (eq_rel_perf_ind_ignore (fset [:: sign_loc])).
-    Check (_ :|: _).
     - rewrite /Sig_locs_real/Sig_locs_ideal/Key_locs/Sig_locs_real/Key_locs.
       apply fsubsetU.
       apply/orP; right.