feat: make labels for signature keys more precise

fstar/symbolic/MLS.Symbolic.MyMkRand.fst

@@ -0,0 +1,88 @@
+module MLS.Symbolic.MyMkRand
+
+open DY.Core
+
+#set-options "--fuel 0 --ifuel 0"
+
+[@@ "opaque_to_smt"]
+val my_mk_rand: usg:usage -> lab:(bytes -> label) -> len:nat{len <> 0} -> traceful bytes
+let my_mk_rand usg lab len =
+  let* time = get_time in
+  let result = (Rand len time) in
+  add_event (RandGen usg (lab result) len);*
+  return result
+
+/// Generating a random bytestrings always preserve the trace invariant.
+
+#push-options "--z3rlimit 25 --fuel 1 --ifuel 1"
+val my_mk_rand_trace_invariant:
+  {|protocol_invariants|} ->
+  usg:usage -> lab:(bytes -> label) -> len:nat{len <> 0} -> tr:trace ->
+  Lemma
+  (requires trace_invariant tr)
+  (ensures (
+    let (b, tr_out) = my_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
+  ))
+  [SMTPat (my_mk_rand usg lab len tr); SMTPat (trace_invariant tr)]
+let my_mk_rand_trace_invariant #invs usg lab len tr =
+  let result = (Rand len (DY.Core.Trace.Base.length tr)) in
+  add_event_invariant (RandGen usg (lab result) len) tr;
+  reveal_opaque (`%my_mk_rand) (my_mk_rand)
+#pop-options
+
+/// Random bytestrings satisfy the bytes invariant.
+
+#push-options "--fuel 1 --ifuel 1"
+val my_mk_rand_bytes_invariant:
+  {|protocol_invariants|} ->
+  usg:usage -> lab:(bytes -> label) -> len:nat{len <> 0} -> tr:trace ->
+  Lemma
+  (ensures (
+    let (b, tr_out) = my_mk_rand usg lab len tr in
+    bytes_invariant tr_out b
+  ))
+  // We need a way for the SMT pattern to know the value of `invs`
+  // This is done using `trace_invariant`, although it is not necessary for the theorem to hold,
+  // it is certainly around in the context
+  [SMTPat (my_mk_rand usg lab len tr); SMTPat (trace_invariant tr)]
+let my_mk_rand_bytes_invariant #invs usg lab len tr =
+  reveal_opaque (`%my_mk_rand) (my_mk_rand);
+  normalize_term_spec bytes_invariant
+#pop-options
+
+/// Label of random bytestrings.
+
+#push-options "--fuel 1 --ifuel 1"
+val my_mk_rand_get_label:
+  {|protocol_invariants|} ->
+  usg:usage -> lab:(bytes -> label) -> len:nat{len <> 0} -> tr:trace ->
+  Lemma
+  (ensures (
+    let (b, tr_out) = my_mk_rand usg lab len tr in
+    get_label tr_out b == lab b
+  ))
+  [SMTPat (my_mk_rand usg lab len tr); SMTPat (trace_invariant tr)]
+let my_mk_rand_get_label #invs usg lab len tr =
+  reveal_opaque (`%my_mk_rand) (my_mk_rand);
+  normalize_term_spec get_label
+#pop-options
+
+/// Usage of random bytestrings.
+
+#push-options "--fuel 1 --ifuel 1"
+val my_mk_rand_has_usage:
+  {|protocol_invariants|} ->
+  usg:usage -> lab:(bytes -> label) -> len:nat{len <> 0} -> tr:trace ->
+  Lemma
+  (ensures (
+    let (b, tr_out) = my_mk_rand usg lab len tr in
+    b `has_usage tr_out` usg
+  ))
+  [SMTPat (my_mk_rand usg lab len tr); SMTPat (trace_invariant tr)]
+let my_mk_rand_has_usage #invs usg lab len tr =
+  normalize_term_spec my_mk_rand;
+  normalize_term_spec has_usage
+#pop-options

fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.Sessions.fst

@@ -206,109 +206,3 @@ val get_public_treesync_state_proof:
     )
   ))
 let get_public_treesync_state_proof #invs #tkt prin state_id tr = ()
-
-(*** Session predicate for private state ***)
-
-type treesync_private_state_ (bytes:Type0) {|bytes_like bytes|} = {
-  signature_key: mls_bytes bytes;
-}
-
-%splice [ps_treesync_private_state_] (gen_parser (`treesync_private_state_))
-%splice [ps_treesync_private_state__is_well_formed] (gen_is_well_formed_lemma (`treesync_private_state_))
-
-type treesync_private_state = treesync_private_state_ dy_bytes
-
-instance parseable_serializeable_treesync_private_state: parseable_serializeable dy_bytes treesync_private_state = mk_parseable_serializeable ps_treesync_private_state_
-
-instance local_state_treesync_private_state: local_state treesync_private_state =
-  mk_local_state_instance "MLS.TreeSync.PrivateState"
-
-val treesync_private_state_pred: {|crypto_invariants|} -> local_state_predicate treesync_private_state
-let treesync_private_state_pred #ci = {
-  pred = (fun tr prin state_id st ->
-    is_signature_key (mk_mls_sigkey_usage prin) (principal_label prin) tr st.signature_key
-  );
-  pred_later = (fun tr1 tr2 prin state_id st -> ());
-  pred_knowable = (fun tr prin state_id st -> ());
-}
-
-val has_treesync_private_state_invariant: {|protocol_invariants|} -> prop
-let has_treesync_private_state_invariant #invs =
-  has_local_state_predicate treesync_private_state_pred
-
-val treesync_private_state_tag_and_invariant: {|crypto_invariants|} -> dtuple2 string local_bytes_state_predicate
-let treesync_private_state_tag_and_invariant #ci = (|local_state_treesync_private_state.tag, local_state_predicate_to_local_bytes_state_predicate treesync_private_state_pred|)
-
-(*** Traceful API for private state ***)
-
-val new_private_treesync_state:
-  principal -> treesync_private_state ->
-  traceful state_id
-let new_private_treesync_state prin st =
-  let* state_id = new_session_id prin in
-  set_state prin state_id st;*
-  return state_id
-
-val new_private_treesync_state_proof:
-  {|protocol_invariants|} ->
-  prin:principal -> st:treesync_private_state ->
-  tr:trace ->
-  Lemma
-  (requires
-    is_signature_key (mk_mls_sigkey_usage prin) (principal_label prin) tr st.signature_key /\
-    trace_invariant tr /\
-    has_treesync_private_state_invariant
-  )
-  (ensures (
-    let (_, tr_out) = new_private_treesync_state prin st tr in
-    trace_invariant tr_out
-  ))
-let new_private_treesync_state_proof #invs prin st tr = ()
-
-val set_private_treesync_state:
-  principal -> state_id -> treesync_private_state ->
-  traceful unit
-let set_private_treesync_state prin state_id st =
-  set_state prin state_id st
-
-val set_private_treesync_state_proof:
-  {|protocol_invariants|} ->
-  prin:principal -> state_id:state_id -> st:treesync_private_state ->
-  tr:trace ->
-  Lemma
-  (requires
-    is_signature_key (mk_mls_sigkey_usage prin) (principal_label prin) tr st.signature_key /\
-    trace_invariant tr /\
-    has_treesync_private_state_invariant
-  )
-  (ensures (
-    let ((), tr_out) = set_private_treesync_state prin state_id st tr in
-    trace_invariant tr_out
-  ))
-let set_private_treesync_state_proof #invs prin state_id st tr = ()
-
-val get_private_treesync_state:
-  principal -> state_id ->
-  traceful (option treesync_private_state)
-let get_private_treesync_state prin state_id =
-  get_state prin state_id
-
-val get_private_treesync_state_proof:
-  {|protocol_invariants|} ->
-  prin:principal -> state_id:state_id ->
-  tr:trace ->
-  Lemma
-  (requires
-    trace_invariant tr /\
-    has_treesync_private_state_invariant
-  )
-  (ensures (
-    let (opt_result, tr_out) = get_private_treesync_state prin state_id tr in
-    tr_out == tr /\ (
-      match opt_result with
-      | None -> True
-      | Some st ->
-        is_signature_key (mk_mls_sigkey_usage prin) (principal_label prin) tr st.signature_key
-    )
-  ))
-let get_private_treesync_state_proof #invs prin state_id tr = ()