From eba7f2665a8a8683aa019b9fdfa357071d3d8bdc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9ophile=20Wallez?= Date: Mon, 14 Oct 2024 14:24:40 +0200 Subject: [PATCH] remove useless asserts --- examples/nsl_pk/DY.Example.NSL.Protocol.Total.Proof.fst | 2 -- 1 file changed, 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 index 133f0fd..0a21428 100644 --- 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