[Pitch] Safely sending non-`Sendable` values across isolation domains

If a variable passed to a Task is accessed after it's passed,
it will cause problems due to simultaneous access.
However, if the variable is accessed after Task.value has been await-ed, as in the code below,
I believe there would be no problem as there's no risk of simultaneous access.
Am I correct?

// not Sendable
class NS {}

func main() async {
    var x = NS()
    let task = Task<Void, Never> { () async -> Void in
        print("use x in task: \(x))")
    }
    await task.value
    print("use x outside task: \(x)")
}

Would the proposed analysis method be able to handle such a pattern?

In my thoughts, the analyzer would require information that the closure passed to Task.init has already ended after task.value.
However, this information cannot be obtained from just the method signature, so it seems hard.

In fact, I have encountered a similar pattern with NIO's EventLoop.
I believe that the following pattern with EventLoop, similar to the Task pattern above, is also safe.

func main(eventLoop: any EventLoop) async {
    var x = NS()

    let promise = eventLoop.makePromise(of: Void.self)
    promise.completeWithTask {
        print("use x in task: \(x)")
    }

    await promise.futureResult.get()
    print("use x outside task: \(x)")
}

Is this a correct assumption?
Unfortunately, it seems quite challenging for static analysis in this case, as it requires knowledge about EventLoop.makePromise, EventLoopPromise.completeWithTask, EventLoopPromise.futureResult, and EventLoopFuture.get.