Support lazy vals under separation checking

Initializers are be treated as read-only methods
and thus are forbidden from invoking update
methods.

Author: bracevac

compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala

@@ -746,6 +746,15 @@ class CheckCaptures extends Recheck, SymTransformer:
         checkUpdate(qualType, tree.srcPos):
           i"Cannot call update ${tree.symbol} of ${qualType.showRef}"
 
+        // Additionally, lazy val initializers should not call update methods
+        if curEnv.owner.is(Lazy) then
+          qualType.captureSet.elems.foreach: elem =>
+            if elem.isExclusive then
+              report.error(
+                em"""Lazy val initializer calls update method on exclusive capability $elem;
+                    |lazy val initializers should only access capabilities in a read-only fashion.""",
+                tree.srcPos)
+
       // If selecting a lazy val member, charge the qualifier since accessing
       // the lazy val can trigger initialization that uses the qualifier's capabilities
       if tree.symbol.is(Lazy) then

tests/neg-custom-args/captures/lazyvals-sep.scala

@@ -0,0 +1,100 @@
+import language.experimental.captureChecking
+import language.experimental.separationChecking
+import caps.*
+
+class Ref(x: Int) extends Mutable:
+  private var value: Int = x
+  def get(): Int = value
+  update def set(newValue: Int): Unit = value = newValue
+
+// For testing types other than functions
+class Wrapper(val ref: Ref^) extends Mutable:
+  def compute(): Int = ref.get()
+  update def mutate(x: Int): Unit = ref.set(x)
+
+class WrapperRd(val ref: Ref^{cap.rd}):
+  def compute(): Int = ref.get()
+
+@main def run =
+  val r: Ref^ = Ref(0)
+  val r2: Ref^ = Ref(42)
+
+  // Test case 1: Read-only access in initializer - should be OK
+  lazy val lazyVal: () ->{r.rd} Int =
+    val current = r2.get()
+    () => r.get() + current
+
+  // Test case 2: Exclusive access in initializer - should error
+  lazy val lazyVal2: () ->{r.rd} Int =
+    val current = r2.get()
+    r.set(current * 100)  // error - exclusive access in initializer
+    () => r.get()
+
+  // Test case 3: Exclusive access in returned closure - should be OK
+  lazy val lazyVal3: () ->{r} Int =
+    val current = r2.get()
+    () => r.set(current); r.get()  // exclusive access in closure, not initializer
+
+  // Test case 4: Multiple nested blocks with exclusive access - should error
+  lazy val lazyVal4: () ->{r.rd} Int =
+    val x = {
+      val y = {
+        r.set(100)  // error
+        r.get()
+      }
+      y + 1
+    }
+    () => r.get() + x
+
+  // Test case 5: Multiple nested blocks with only read access - should be OK
+  lazy val lazyVal5: () ->{r.rd} Int =
+    val x = {
+      val y = {
+        r.get()  // only read access in nested blocks
+      }
+      y + 1
+    }
+    () => r.get() + x
+
+  // Test case 6: WrapperRd type - exclusive access in initializer - should error
+  lazy val lazyVal6: WrapperRd^{r} =
+    r.set(200)  // error
+    WrapperRd(r)
+
+  // Test case 7: WrapperRd type - non-exclusive access in initializer - should be ok
+  lazy val lazyVal7: WrapperRd^{r} =
+    r.get()
+    WrapperRd(r)
+
+  // Test case 8: Wrapper type - exclusive access in initializer - should error
+  lazy val lazyVal8: Wrapper^{cap, r} =
+    r.set(200)  // error
+    Wrapper(r)
+
+  // Test case 9: Wrapper type - non-exclusive access in initializer - should be ok
+  lazy val lazyVal9: Wrapper^{cap, r} =
+    r.get()
+    Wrapper(r)
+
+  // Test case 10: Conditional with exclusive access - should error
+  lazy val lazyVal10: WrapperRd^{r} =
+    val x = if r.get() > 0 then
+      r.set(0)  // error exclusive access in conditional
+      1
+    else 2
+    WrapperRd(r)
+
+  // Test case 11: Try-catch with exclusive access - should error
+  lazy val lazyVal11: () ->{r.rd} Int =
+    val x = try
+      r.set(42)  // error
+      r.get()
+    catch
+      case _: Exception => 0
+    () => r.get() + x
+
+  // // Test case 12: Local exclusive access - should be OK
+  // lazy val lazyVal12: () => Int =
+  //   val r3: Ref^ = Ref(10)
+  //   r3.set(100) FIXME should work
+  //   () => r3.get()