cleanup: split _invariant lemmas (#81)

src/core/DY.Core.Trace.Base.fst

@@ -254,6 +254,20 @@ val event_at_grows:
   [SMTPat (event_at tr1 i e); SMTPat (tr1 <$ tr2)]
 let event_at_grows #label_t tr1 tr2 i e = ()
 
+val last_entry_exists:
+  #label_t:Type ->
+  tr:trace_ label_t ->
+  Lemma
+    (requires Snoc? tr )
+    (ensures (
+       let Snoc _ last = tr in
+       event_exists tr last
+    ))
+    [SMTPat (Snoc? tr)]
+let last_entry_exists tr = 
+  let Snoc _ last = tr in
+  assert(event_at tr (DY.Core.Trace.Base.length tr - 1) last)
+
 /// Shorthand predicates.
 
 /// Has a message been sent on the network?

src/core/DY.Core.Trace.Manipulation.fst

@@ -115,6 +115,15 @@ let add_event e tr =
   norm_spec [zeta; delta_only [`%prefix]] (prefix #label);
   ((), Snoc tr e)
 
+val add_event_event_exists:
+  e:trace_event -> tr:trace ->
+  Lemma
+  (ensures (
+    let ((), tr_out) = add_event e tr in
+    event_exists tr_out e
+  ))
+let add_event_event_exists e tr = ()
+
 /// Adding a trace event preserves the trace invariant
 /// when the trace event satisfy the invariant.
 
@@ -128,8 +137,7 @@ val add_event_invariant:
   )
   (ensures (
     let ((), tr_out) = add_event e tr in
-    trace_invariant tr_out /\
-    event_exists tr_out e
+    trace_invariant tr_out
   ))
 let add_event_invariant #invs e tr =
   norm_spec [zeta; delta_only [`%trace_invariant]] (trace_invariant)
@@ -152,6 +160,18 @@ let send_msg msg =
   add_event (MsgSent msg);*
   return time
 
+val send_msg_msg_event:
+  msg:bytes -> tr:trace ->
+  Lemma
+  (ensures (
+    let (i, tr_out) = send_msg msg tr in
+    event_at tr_out i (MsgSent msg)
+  ))
+ [SMTPat (send_msg msg tr);]
+let send_msg_msg_event msg tr =
+ reveal_opaque (`%send_msg) (send_msg)
+
+
 /// Sending a message on the network preserves the trace invariant
 /// when the message is publishable.
 
@@ -165,8 +185,7 @@ val send_msg_invariant:
   )
   (ensures (
     let (i, tr_out) = send_msg msg tr in
-    trace_invariant tr_out /\
-    event_at tr_out i (MsgSent msg)
+    trace_invariant tr_out
   ))
   [SMTPat (send_msg msg tr); SMTPat (trace_invariant tr)]
 let send_msg_invariant #invs msg tr =
@@ -186,6 +205,18 @@ let recv_msg i =
   else
     return None
 
+
+val recv_msg_same_trace:
+  i:timestamp -> tr:trace ->
+  Lemma
+  (ensures (
+    let (opt_msg, tr_out) = recv_msg i tr in
+    tr_out == tr
+  ))
+  [SMTPat (recv_msg i tr);]
+let recv_msg_same_trace i tr =
+  reveal_opaque (`%recv_msg) recv_msg
+
 /// When the trace invariant holds,
 /// received messages are publishable.
 
@@ -196,11 +227,9 @@ val recv_msg_invariant:
   (requires trace_invariant tr)
   (ensures (
     let (opt_msg, tr_out) = recv_msg i tr in
-    tr_out == tr /\ (
       match opt_msg with
       | None -> True
       | Some msg -> is_publishable tr msg
-    )
   ))
   [SMTPat (recv_msg i tr);
    SMTPat (trace_invariant tr)
@@ -252,25 +281,35 @@ let mk_rand usg lab len =
   add_event (RandGen usg lab len);*
   return (Rand len time)
 
+
+val mk_rand_rand_gen_at_end:
+  usg:usage -> lab:label -> len:nat{len <> 0} -> tr:trace ->
+  Lemma
+  (ensures (
+    let (b, tr_out) = mk_rand usg lab len tr in
+    1 <= DY.Core.Trace.Base.length tr_out /\
+    rand_generated_at tr_out (DY.Core.Trace.Base.length tr_out - 1) b
+  ))
+  [SMTPat (mk_rand usg lab len tr);]
+let mk_rand_rand_gen_at_end usg lab len tr =
+  reveal_opaque (`%mk_rand) (mk_rand)
+
+
 /// Generating a random bytestrings always preserve the trace invariant.
 
-#push-options "--z3rlimit 25"
 val mk_rand_trace_invariant:
   {|protocol_invariants|} ->
   usg:usage -> lab:label -> len:nat{len <> 0} -> tr:trace ->
   Lemma
   (requires trace_invariant tr)
   (ensures (
     let (b, tr_out) = mk_rand usg lab len tr in
-    trace_invariant tr_out /\
-    1 <= DY.Core.Trace.Base.length tr_out /\
-    rand_generated_at tr_out (DY.Core.Trace.Base.length tr_out - 1) b
+    trace_invariant tr_out
   ))
   [SMTPat (mk_rand usg lab len tr); SMTPat (trace_invariant tr)]
 let mk_rand_trace_invariant #invs usg lab len tr =
   add_event_invariant (RandGen usg lab len) tr;
   reveal_opaque (`%mk_rand) (mk_rand)
-#pop-options
 
 /// Random bytestrings satisfy the bytes invariant.
 
@@ -418,21 +457,33 @@ let get_state prin sess_id =
 
 /// Obtaining a new state identifier do not change the trace.
 
-val new_session_id_invariant:
+val new_session_id_same_trace:
   prin:principal -> tr:trace ->
   Lemma
   (ensures (
     let (_, tr_out) = new_session_id prin tr in
     tr == tr_out
   ))
   [SMTPat (new_session_id prin tr)]
-let new_session_id_invariant prin tr =
+let new_session_id_same_trace prin tr =
   normalize_term_spec new_session_id
 
+
+val set_state_state_was_set:
+  prin:principal -> sess_id:state_id -> content:bytes -> tr:trace ->
+  Lemma
+  (ensures (
+    let ((), tr_out) = set_state prin sess_id content tr in
+    state_was_set tr_out prin sess_id content
+  ))
+  [SMTPat (set_state prin sess_id content tr);]
+let set_state_state_was_set prin sess_id content tr =
+  normalize_term_spec set_state
+
+
 /// Storing a state preserves the trace invariant
 /// when the state satisfy the state predicate.
 
-#push-options "--z3rlimit 15"
 val set_state_invariant:
   {|protocol_invariants|} ->
   prin:principal -> sess_id:state_id -> content:bytes -> tr:trace ->
@@ -443,71 +494,59 @@ val set_state_invariant:
   )
   (ensures (
     let ((), tr_out) = set_state prin sess_id content tr in
-    trace_invariant tr_out /\
-    state_was_set tr_out prin sess_id content
+    trace_invariant tr_out
   ))
   [SMTPat (set_state prin sess_id content tr); SMTPat (trace_invariant tr)]
 let set_state_invariant #invs prin sess_id content tr =
   add_event_invariant (SetState prin sess_id content) tr;
   normalize_term_spec set_state
-#pop-options
 
-val get_state_aux_state_invariant:
-  {|protocol_invariants|} ->
+val get_state_same_trace:
+  prin:principal -> sess_id:state_id -> tr:trace ->
+  Lemma
+  (ensures (
+    let (opt_content, tr_out) = get_state prin sess_id tr in
+    tr == tr_out
+  ))
+  [SMTPat (get_state prin sess_id tr);]
+let get_state_same_trace prin sess_id tr =
+  reveal_opaque (`%get_state) get_state
+
+
+val get_state_aux_state_was_set:
   prin:principal -> sess_id:state_id -> tr:trace ->
   Lemma
-  (requires
-    trace_invariant tr
-  )
   (ensures (
     match get_state_aux prin sess_id tr with
     | None -> True
-    | Some content -> state_pred.pred tr prin sess_id content
+    | Some content -> 
+        state_was_set tr prin sess_id content
   ))
-let rec get_state_aux_state_invariant #invs prin sess_id tr =
-  reveal_opaque (`%grows) (grows #label);
-  norm_spec [zeta; delta_only [`%trace_invariant]] (trace_invariant);
-  norm_spec [zeta; delta_only [`%prefix]] (prefix #label);
-  match tr with
+let rec get_state_aux_state_was_set prin sess_id tr =
+   match tr with
   | Nil -> ()
   | Snoc tr_init (SetState prin' sess_id' content) -> (
-    if prin = prin' && sess_id = sess_id' then (
-      state_pred.pred_later tr_init tr prin sess_id content
-    ) else (
-      get_state_aux_state_invariant prin sess_id tr_init;
-      match get_state_aux prin sess_id tr_init with
-      | None -> ()
-      | Some content -> state_pred.pred_later tr_init tr prin sess_id content
-    )
+    if prin = prin' && sess_id = sess_id' 
+    then ()
+    else get_state_aux_state_was_set prin sess_id tr_init
   )
   | Snoc tr_init _ ->
-    get_state_aux_state_invariant prin sess_id tr_init;
-    match get_state_aux prin sess_id tr_init with
-    | None -> ()
-    | Some content -> state_pred.pred_later tr_init tr prin sess_id content
-
-/// When the trace invariant holds,
-/// retrieved states satisfy the state predicate.
+         get_state_aux_state_was_set prin sess_id tr_init
 
-val get_state_state_invariant:
-  {|protocol_invariants|} ->
+val get_state_state_was_set:
   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
-    tr == tr_out /\ (
-      match opt_content with
-      | None -> True
-      | Some content -> state_pred.pred tr prin sess_id content
-    )
+    match opt_content with
+    | None -> True
+    | Some content ->
+        state_was_set 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
+  [SMTPat (get_state prin sess_id tr)]
+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
 
 (*** Event triggering ***)
 
@@ -518,6 +557,17 @@ val trigger_event: principal -> string -> bytes -> traceful unit
 let trigger_event prin tag content =
   add_event (Event prin tag content)
 
+val trigger_event_event_triggered:
+  prin:principal -> tag:string -> content:bytes -> tr:trace ->
+  Lemma
+  (ensures (
+    let ((), tr_out) = trigger_event prin tag content tr in
+    event_triggered tr_out prin tag content
+  ))
+  [SMTPat (trigger_event prin tag content tr);]
+let trigger_event_event_triggered prin tag content tr =
+  reveal_opaque (`%trigger_event) trigger_event
+
 /// Triggering a protocol event preserves the trace invariant
 /// when the protocol event satisfy the event predicate.
 
@@ -531,8 +581,7 @@ val trigger_event_trace_invariant:
   )
   (ensures (
     let ((), tr_out) = trigger_event prin tag content tr in
-    trace_invariant tr_out /\
-    event_triggered tr_out prin tag content
+    trace_invariant tr_out
   ))
   [SMTPat (trigger_event prin tag content tr); SMTPat (trace_invariant tr)]
 let trigger_event_trace_invariant #invs prin tag content tr =

src/lib/event/DY.Lib.Event.Typed.fst

@@ -137,6 +137,19 @@ val event_triggered:
 let event_triggered #a #ev tr prin e =
   exists i. event_triggered_at tr i prin e
 
+val trigger_event_event_triggered:
+  #a:Type -> {|ev:event a|} ->
+  prin:principal -> e:a -> tr:trace ->
+  Lemma
+  (ensures (
+    let ((), tr_out) = trigger_event prin e tr in
+    event_triggered tr_out prin e
+  ))
+  [SMTPat (trigger_event #a #ev prin e tr);]
+let trigger_event_event_triggered #a #ev prin e tr =
+  reveal_opaque (`%trigger_event) (trigger_event #a);
+  reveal_opaque (`%event_triggered_at) (event_triggered_at #a)
+
 val trigger_event_trace_invariant:
   {|protocol_invariants|} ->
   #a:Type -> {|ev:event a|} ->
@@ -150,18 +163,30 @@ val trigger_event_trace_invariant:
   )
   (ensures (
     let ((), tr_out) = trigger_event prin e tr in
-    trace_invariant tr_out /\
-    event_triggered tr_out prin e
+    trace_invariant tr_out
   ))
   [SMTPat (trigger_event prin e tr);
    SMTPat (has_event_pred epred);
    SMTPat (trace_invariant tr)]
 let trigger_event_trace_invariant #invs #a #ev epred prin e tr =
   reveal_opaque (`%has_compiled_event_pred) (has_compiled_event_pred);
   reveal_opaque (`%trigger_event) (trigger_event #a);
-  reveal_opaque (`%event_triggered_at) (event_triggered_at #a);
   local_eq_global_lemma split_event_pred_params event_pred ev.tag (compile_event_pred epred) (tr, prin, ev.tag, serialize _ e) ev.tag (tr, prin, serialize _ e)
 
+
+val event_triggered_at_on_trace:
+  #a:Type -> {|ev:event a|} ->
+  tr:trace ->
+  i:timestamp -> prin:principal -> e:a ->
+  Lemma
+  (requires
+    event_triggered_at tr i prin e
+  )
+  (ensures i < DY.Core.Trace.Base.length tr)
+  [SMTPat (event_triggered_at #a #ev tr i prin e)]
+let event_triggered_at_on_trace #a #ev  tr i prin e =
+  reveal_opaque (`%event_triggered_at) (event_triggered_at #a)
+
 val event_triggered_at_implies_pred:
   {|protocol_invariants|} ->
   #a:Type -> {|ev:event a|} ->
@@ -173,7 +198,7 @@ val event_triggered_at_implies_pred:
     has_event_pred epred /\
     trace_invariant tr
   )
-  (ensures i <= DY.Core.Trace.Base.length tr /\ epred (prefix tr i) prin e)
+  (ensures epred (prefix tr i) prin e)
   [SMTPat (event_triggered_at tr i prin e);
    SMTPat (has_event_pred epred);
    SMTPat (trace_invariant tr);
@@ -201,7 +226,6 @@ val event_triggered_at_implies_trace_event_at:
   Lemma
   (requires event_triggered_at tr i prin e)
   (ensures
-    i < DY.Core.Trace.Base.length tr /\
     get_event_at tr i == Event prin ev.tag (serialize a e) /\
     parse #bytes a (serialize a e) == Some e
   )