From 2abeecee1902aaa396ef932cd3ee83fb591ab45e Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@amazon.com>
Date: Mon, 14 Feb 2022 10:07:27 -0800
Subject: [PATCH 1/2] docs: Document :termination attribute

---
 Source/Dafny/DafnyOptions.cs | 15 ++++++++++++++-
 1 file changed, 14 insertions(+), 1 deletion(-)

diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs
index 0d7075ccc9d..b61bf3b2ba3 100644
--- a/Source/Dafny/DafnyOptions.cs
+++ b/Source/Dafny/DafnyOptions.cs
@@ -692,7 +692,20 @@ that the method/function is compiled and tail recursive. If it
       is not, an error is given.
 
     {:termination}
-      TODO
+      Dafny currently lacks the features needed to specify usable termination
+      metrics for trait methods that are dynamically dispatched to method
+      implementations given in other modules. This issue and a sketch of a
+      solution are described in https://github.com/dafny-lang/dafny/issues/1588.
+      Until such features are added to the language, a type `C` that extends a
+      trait `T` must be declared in the same module as `T`.
+      There is, however, an available loophole: if a programmer is willing to
+      take the responsibility that all calls to methods in a trait `T`
+      that dynamically dispatch to implementations in other modules terminate,
+      then the trait `T` can be marked with `{:termination false}`. This will
+      allow `T` to be extended by types declared in modules outside `T`'s module.
+      Caution: This loophole is unsound; that is, if a cross-module dynamic
+      dispatch fails to terminate, then this and other errors in the program
+      may have been overlooked by the verifier.       
 
     {:warnShadowing}
       TODO

From bd35d681c71fb84d9c5634da8b12e0a23e2ec6a6 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@amazon.com>
Date: Tue, 15 Feb 2022 09:15:09 -0800
Subject: [PATCH 2/2] Added two clarifications, per PR comments

---
 Source/Dafny/DafnyOptions.cs | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs
index b61bf3b2ba3..d878acb28e7 100644
--- a/Source/Dafny/DafnyOptions.cs
+++ b/Source/Dafny/DafnyOptions.cs
@@ -703,10 +703,30 @@ take the responsibility that all calls to methods in a trait `T`
       that dynamically dispatch to implementations in other modules terminate,
       then the trait `T` can be marked with `{:termination false}`. This will
       allow `T` to be extended by types declared in modules outside `T`'s module.
+
       Caution: This loophole is unsound; that is, if a cross-module dynamic
       dispatch fails to terminate, then this and other errors in the program
       may have been overlooked by the verifier.       
 
+      The meaning of `{:termination false}` is defined only on trait declarations.
+      It has no meaning if applied to other declarations.
+
+      Applying `{:termination false}` to a trait is similar to the
+      effect of declaring each of its methods with `decreases *`, but
+      there are several differences.  The biggest difference is that
+      `decreases *` is sound, whereas the attribute is not. As such,
+      `decreases *` cannot be used with functions, lemmas, or ghost
+      methods, and callers of a `decreases *` method must themselves
+      be declared with `decreases *`. In contrast, `{:termination false}`
+      applies to all functions, lemmas, and methods of the trait, and
+      callers do not have to indicate that they are using such a
+      trait. Another difference is that `{:termination false}` does
+      not change checking for intra-module calls. That is, even if a
+      trait is declared with `{:termination false}`, calls to its
+      functions, lemmas, and methods from within the module where the
+      trait is declared are checked for termination in the usual
+      manner.
+
     {:warnShadowing}
       TODO