docs: remove trailing whitespaces

src/DY.Core.Bytes.fst

@@ -8,7 +8,7 @@ open DY.Core.Label
 #set-options "--fuel 1 --ifuel 1"
 
 /// This module contains functions and predicates operating on bytes.
-/// 
+///
 /// To conduct security proofs, a crucial predicate is the `bytes_invariant`,
 /// an invariant on all the bytes being used in a protocol execution.
 /// This is invariant is preserved by honest participants

src/DY.Core.Label.fst

@@ -85,7 +85,7 @@ let rec is_corrupt_later tr1 tr2 l =
     introduce is_corrupt tr1 l2 ==> is_corrupt tr2 l2 with _. is_corrupt_later tr1 tr2 l2
 
 /// A label `l1` can flow to a label `l2` when `l2` will always be more secret than `l1` in the future,
-/// or more precisely, when in the future, a corruption of `l2` implies a corruption of `l1`. 
+/// or more precisely, when in the future, a corruption of `l2` implies a corruption of `l1`.
 
 [@@"opaque_to_smt"]
 val can_flow: trace -> label -> label -> prop

src/DY.Core.Trace.Invariant.fst

@@ -12,7 +12,7 @@ open DY.Core.Label
 /// - first, we prove that all reachable traces satisfy the trace invariant,
 /// - then, we prove that traces that satisfy the trace invariant
 ///   ensure some security guarantees.
-/// 
+///
 /// Because each cryptographic protocol need a custom trace invariant to be proved secure,
 /// the trace invariant can be customised with specific state or event predicates with `trace_invariants`.
 

src/DY.Core.fst

@@ -14,7 +14,7 @@ module DY.Core
 ///
 /// Here is a high-level overview of DY.Core modules,
 /// and the DY* approach to symbolic security proofs.
-/// 
+///
 /// Participants in a cryptographic protocols can be thought as state machines,
 /// that receive some data from the network,
 /// modify their internal state,
@@ -74,7 +74,7 @@ module DY.Core
 /// we prove that every protocol function preserve the trace invariant,
 /// hence because every function used by the attacker preserve the invariants,
 /// the attacker function has no choice but to preserve the invariants.
-/// 
+///
 /// To show that every protocol function preserve the trace invariant,
 /// we will prove that every honest participant has a hygienic use of cryptography,
 /// for example they may only sign bytestrings that verify some property