remove useless asserts

REPROSEC · Oct 14, 2024 · eba7f26 · eba7f26
1 parent e83b8f5
commit eba7f26
Showing 1 changed file with 0 additions and 2 deletions.
diff --git a/examples/nsl_pk/DY.Example.NSL.Protocol.Total.Proof.fst b/examples/nsl_pk/DY.Example.NSL.Protocol.Total.Proof.fst
@@ -137,8 +137,6 @@ val compute_message2_proof:
   )
 let compute_message2_proof tr bob msg1 pk_a n_b nonce =
   let msg = Msg2 {n_a = msg1.n_a;  n_b; bob;} in
-  assert(join (nsl_nonce_label msg1.alice) (nsl_nonce_label bob) `can_flow tr` (nsl_nonce_label msg1.alice));
-  assert(join (nsl_nonce_label msg1.alice) (nsl_nonce_label bob) `can_flow tr` (nsl_nonce_label bob));
   serialize_wf_lemma message (is_knowable_by (nsl_nonce_label msg1.alice) tr) msg;
   serialize_wf_lemma message (is_knowable_by (nsl_nonce_label bob) tr) msg