Update CC language reference with lazy vals

Author: bracevac

docs/_docs/reference/experimental/capture-checking/basics.md

@@ -172,6 +172,63 @@ def f(x: ->{c} Int): Int
 ```
 Here, the actual argument to `f` is allowed to use the `c` capability but no others.
 
+## Lazy Vals
+
+Lazy vals receive special treatment under capture checking, similar to parameterless methods. A lazy val has two distinct capture sets:
+
+1. **The initializer's capture set**: What capabilities the initialization code uses
+2. **The result's capture set**: What capabilities the lazy val's value captures
+
+### Initializer Captures
+
+When a lazy val is declared, its initializer is checked in its own environment (like a method body). The initializer can capture capabilities, and these are tracked separately:
+
+```scala
+def example(console: Console^) =
+  lazy val x: () -> String =
+    console.println("Computing x")  // console captured by initializer
+    () => "Hello, World!"           // result doesn't capture console
+
+  val fun: () ->{console} String = () => x()   // ok: accessing x uses console
+  val fun2: () -> String = () => x()           // error: x captures console
+```
+
+Here, the initializer of `x` uses `console` (to print a message), so accessing `x` for the first time will use the `console` capability. However, the **result** of `x` is a pure function `() -> String` that doesn't capture any capabilities.
+
+The type system tracks that accessing `x` requires the `console` capability, even though the resulting value doesn't. This is reflected in the function types: `fun` must declare `{console}` in its capture set because it accesses `x`.
+
+### Lazy Val Member Selection
+
+When accessing a lazy val member through a qualifier, the qualifier is charged to the current capture set, just like calling a parameterless method:
+
+```scala
+trait Container:
+  lazy val lazyMember: String
+
+def client(c: Container^): Unit =
+  val f1: () -> String = () => c.lazyMember        // error
+  val f2: () ->{c} String = () => c.lazyMember     // ok
+```
+
+Accessing `c.lazyMember` can trigger initialization, which may use capabilities from `c`. Therefore, the capture set must include `c`.
+
+### Equivalence with Methods
+
+For capture checking purposes, lazy vals behave identically to parameterless methods:
+
+```scala
+trait T:
+  def methodMember(): String
+  lazy val lazyMember: String
+
+def test(t: T^): Unit =
+  // Both require {t} in the capture set
+  val m: () ->{t} String = () => t.methodMember()
+  val l: () ->{t} String = () => t.lazyMember
+```
+
+This equivalence reflects that both can trigger computation using capabilities from their enclosing object.
+
 ## Subtyping and Subcapturing
 
 Capturing influences subtyping. As usual we write `T₁ <: T₂` to express that the type

docs/_docs/reference/experimental/capture-checking/mutability.md

@@ -215,6 +215,67 @@ val b1: Ref^{a.rd} = a
 val b2: Ref^{cap.rd} = a
 ```
 
+## Lazy Vals and Read-Only Restrictions
+
+Lazy val initializers are subject to read-only restrictions similar to those for normal methods in `Mutable` classes. Specifically, a lazy val initializer cannot call update methods on non-local exclusive capabilities—capabilities defined outside the lazy val's scope.
+
+### Read-Only Initialization
+
+When a lazy val is declared, its initializer may use capabilities from the surrounding environment. However, it can only access non-local exclusive capabilities in a read-only fashion:
+
+```scala
+def example(r: Ref^) =
+  lazy val badInit: () ->{r.rd} Int =
+    r.set(100)      // error: cannot call update method
+    () => r.get()
+
+  lazy val goodInit: () ->{r.rd} Int =
+    val i = r.get() // ok: read-only access
+    () => r.get() + i
+```
+
+The initializer of `badInit` attempts to call `r.set(100)`, an update method on the non-local exclusive capability `r`. This is rejected because initializers should not perform mutations on external state.
+
+### Local Capabilities
+
+The restriction applies only to **non-local** capabilities. A lazy val can freely call update methods on capabilities it creates locally within its initializer:
+
+```scala
+def example =
+  lazy val localMutation: () => Int =
+    val local: Ref^ = Ref(10)  // created in initializer
+    local.set(100)              // ok: local capability
+    () => local.get()
+```
+
+Here, `local` is created within the lazy val's initializer, so it counts as a local capability. The initializer can call update methods on it.
+
+### Closures vs. Initializer Code
+
+The read-only restriction applies to code that runs during initialization, not to closures created by the initializer:
+
+```scala
+def example(r: Ref^) =
+  lazy val closure: () ->{r} Int =
+    val i = r.get()
+    () => r.set(i); r.get()  // ok: closure runs later, not during init
+```
+
+Closures (like `() => ...`) run at a later time than the initializer, so their update method calls are permitted.
+
+### Rationale
+
+Since lazy val initialization happens unpredictably (on first access), allowing initializers to mutate non-local state could cause subtle bugs. The read-only restriction ensures:
+
+1. **Predictable initialization**: Accessing a lazy val for the first time doesn't have surprising side effects on external mutable state
+2. **Thread safety**: Lazy vals can be safely used in concurrent contexts without worrying about initialization side effects
+3. **Referential transparency**: The timing of first access doesn't affect program correctness
+
+This makes lazy vals behave like normal methods in `Mutable` classes: they can read from their environment but cannot update it unless explicitly marked.
+There's currently no `update` modifier for lazy vals, so their initialization is always read-only with respect to non-local capabilities. A future version of capture checking might
+support `update lazy val` if there are compelling use cases and there is sufficient
+community demand.
+
 ## Update Restrictions
 
 If a capability `r` is a read-only access, then one cannot use `r` to call an update method of `r` or to assign to a field of `r`. E.g. `r.set(22)` and `r.current = 22` are both disallowed.