From 7b6858cac63008283fd44c82206a202ce5e9293e Mon Sep 17 00:00:00 2001
From: cwaldm <clara.waldmann@sec.uni-stuttgart.de>
Date: Tue, 22 Oct 2024 14:40:39 +0200
Subject: [PATCH] removed get_state => state_pred lemmas (since they are now
 redundant via get_state => state_was_set => state_pred

---
 src/core/DY.Core.Trace.Manipulation.fst | 21 -----------------
 src/lib/state/DY.Lib.State.Tagged.fst   | 30 -------------------------
 src/lib/state/DY.Lib.State.Typed.fst    | 24 --------------------
 3 files changed, 75 deletions(-)

diff --git a/src/core/DY.Core.Trace.Manipulation.fst b/src/core/DY.Core.Trace.Manipulation.fst
index c83ea91..547674e 100644
--- a/src/core/DY.Core.Trace.Manipulation.fst
+++ b/src/core/DY.Core.Trace.Manipulation.fst
@@ -585,27 +585,6 @@ let get_state_state_was_set prin sess_id tr =
   reveal_opaque (`%get_state) get_state;
   get_state_aux_state_was_set prin sess_id tr
 
-/// When the trace invariant holds,
-/// retrieved states satisfy the state predicate.
-
-val get_state_state_invariant:
-  {|protocol_invariants|} ->
-  prin:principal -> sess_id:state_id -> tr:trace ->
-  Lemma
-  (requires
-    trace_invariant tr
-  )
-  (ensures (
-    let (opt_content, tr_out) = get_state prin sess_id tr in
-      match opt_content with
-      | None -> True
-      | Some content -> state_pred.pred tr prin sess_id content
-  ))
-  [SMTPat (get_state prin sess_id tr); SMTPat (trace_invariant tr)]
-let get_state_state_invariant #invs prin sess_id tr =
-  normalize_term_spec get_state;
-  get_state_aux_state_invariant prin sess_id tr
-
 (*** Event triggering ***)
 
 /// Trigger a protocol event.
diff --git a/src/lib/state/DY.Lib.State.Tagged.fst b/src/lib/state/DY.Lib.State.Tagged.fst
index 1d6c329..2912c2b 100644
--- a/src/lib/state/DY.Lib.State.Tagged.fst
+++ b/src/lib/state/DY.Lib.State.Tagged.fst
@@ -335,36 +335,6 @@ let get_tagged_state_state_was_set tag prin sess_id tr =
     serialize_parse_inv_lemma #bytes tagged_state full_cont_bytes    
   )
 
-val get_tagged_state_invariant:
-  {|protocol_invariants|} ->
-  tag:string -> spred:local_bytes_state_predicate tag ->
-  prin:principal -> sess_id:state_id -> tr:trace ->
-  Lemma
-  (requires
-    trace_invariant tr /\
-    has_local_bytes_state_predicate (|tag, spred|)
-  )
-  (ensures (
-    let (opt_content, tr_out) = get_tagged_state tag prin sess_id tr in
-      match opt_content with
-      | None -> True
-      | Some content -> (
-        spred.pred tr prin sess_id content
-    )
-  ))
-  [SMTPat (get_tagged_state tag prin sess_id tr);
-   SMTPat (trace_invariant tr);
-   SMTPat (has_local_bytes_state_predicate (|tag, spred|))]
-let get_tagged_state_invariant #invs tag spred prin sess_id tr =
-  reveal_opaque (`%has_local_bytes_state_predicate) (has_local_bytes_state_predicate);
-  reveal_opaque (`%get_tagged_state) (get_tagged_state);
-  let (opt_content, tr_out) = get_tagged_state tag prin sess_id tr in
-  match opt_content with
-  | None -> ()
-  | Some content ->
-    let (Some full_content_bytes, tr) = get_state prin sess_id tr in
-    local_eq_global_lemma split_local_bytes_state_predicate_params state_pred.pred tag spred (tr, prin, sess_id, full_content_bytes) tag (tr, prin, sess_id, content)
-
 (*** Theorem ***)
 
 val tagged_state_was_set_implies_pred:
diff --git a/src/lib/state/DY.Lib.State.Typed.fst b/src/lib/state/DY.Lib.State.Typed.fst
index 65dd9e1..6b5b6eb 100644
--- a/src/lib/state/DY.Lib.State.Typed.fst
+++ b/src/lib/state/DY.Lib.State.Typed.fst
@@ -243,30 +243,6 @@ let get_state_state_was_set #a #ls prin sess_id tr =
   | (Some _, _) ->
       let (Some cont, _) = get_tagged_state ls.tag prin sess_id tr in
       serialize_parse_inv_lemma a cont
-  
-val get_state_invariant:
-  #a:Type -> {|local_state a|} ->
-  {|protocol_invariants|} ->
-  spred:local_state_predicate a ->
-  prin:principal -> sess_id:state_id -> tr:trace ->
-  Lemma
-  (requires
-    trace_invariant tr /\
-    has_local_state_predicate spred
-  )
-  (ensures (
-    let (opt_content, tr_out) = get_state prin sess_id tr in
-      match opt_content with
-      | None -> True
-      | Some content -> (
-        spred.pred tr prin sess_id content
-    )
-  ))
-  [SMTPat (get_state #a prin sess_id tr);
-   SMTPat (trace_invariant tr);
-   SMTPat (has_local_state_predicate spred)]
-let get_state_invariant #a #ls #invs spred prin sess_id tr =
-  reveal_opaque (`%get_state) (get_state #a)
 
 val state_was_set_implies_pred:
   #a:Type -> {|local_state a|} ->