diff --git a/2024-sosp-tutorial/exercises/advanced-rust-topics/exercise_01_memoize.rs b/2024-sosp-tutorial/exercises/advanced-rust-topics/exercise_01_memoize.rs
index a9e25cc..6db45ba 100644
--- a/2024-sosp-tutorial/exercises/advanced-rust-topics/exercise_01_memoize.rs
+++ b/2024-sosp-tutorial/exercises/advanced-rust-topics/exercise_01_memoize.rs
@@ -109,7 +109,7 @@ fn todo<A>() -> A
 //
 // 1. Make `Memoizer` generic over Args, Output, and the computation.
 //
-// 2. The current locking scheme is very coarse-grained. Come up with (and implement) and more
-//    fine-grained scheme.
+// 2. The current locking scheme is very coarse-grained. Come up with (and implement) a more
+//    fine-grained locking scheme to reduce thread contention.
 
 }
diff --git a/2024-sosp-tutorial/exercises/advanced-rust-topics/solutions/solution_counting_to_2.rs b/2024-sosp-tutorial/exercises/advanced-rust-topics/solutions/solution_counting_to_2.rs
index fcf2e89..e4ec206 100644
--- a/2024-sosp-tutorial/exercises/advanced-rust-topics/solutions/solution_counting_to_2.rs
+++ b/2024-sosp-tutorial/exercises/advanced-rust-topics/solutions/solution_counting_to_2.rs
@@ -137,17 +137,17 @@ tokenized_state_machine!(
 
         #[inductive(tr_inc_a)]
         fn tr_inc_a_preserves_the_invariant(pre: Self, post: Self) {
-            /* proof here */
+            /* You can leave this empty */
         }
 
         #[inductive(tr_inc_b)]
         fn tr_inc_b_preserves_the_invariant(pre: Self, post: Self) {
-            /* proof here */
+            /* You can leave this empty */
         }
 
         #[inductive(initialize)]
         fn initial_state_satisfies_inv(post: Self) {
-            /* proof here */
+            /* You can leave this empty */
         }
     }
 );
diff --git a/2024-sosp-tutorial/exercises/advanced-rust-topics/solutions/solution_memoize.rs b/2024-sosp-tutorial/exercises/advanced-rust-topics/solutions/solution_memoize.rs
index 9be520a..60ecdcf 100644
--- a/2024-sosp-tutorial/exercises/advanced-rust-topics/solutions/solution_memoize.rs
+++ b/2024-sosp-tutorial/exercises/advanced-rust-topics/solutions/solution_memoize.rs
@@ -11,6 +11,7 @@ use vstd::rwlock::{RwLock, RwLockPredicate};
 use vstd::hash_map::HashMapWithView;
 use std::sync::Arc;
 
+#[path = "../memoization_exercise_internals.rs"]
 mod memoization_exercise_internals;
 
 verus!{
@@ -123,7 +124,7 @@ fn todo<A>() -> A
 //
 // 1. Make `Memoizer` generic over Args, Output, and the computation.
 //
-// 2. The current locking scheme is very coarse-grained. Come up with (and implement) and more
-//    fine-grained scheme.
+// 2. The current locking scheme is very coarse-grained. Come up with (and implement) a more
+//    fine-grained locking scheme to reduce thread contention.
 
 }