fix: preserve wrapper session safety invariants

Beam/Broker/Protocol.lean

@@ -446,16 +446,15 @@ The generic `Request` remains the internal broker protocol used by maintenance t
 -/
 structure ProjectRequest where
   private request : Request
-  private requestId : String
 
 private def projectRequestForbiddenFields : Array String :=
   #["workspaceId", "workspaceMode", "daemonCapability", "root", "leanCmd", "leanPlugin", "rocqCmd"]
 
 private def ProjectRequest.supportedOp : Op → Bool
-  | .ensure | .openDocs | .cancel | .updateFile | .syncFile | .refreshFile | .close | .runAt
+  | .openDocs | .cancel | .updateFile | .syncFile | .refreshFile | .close | .runAt
   | .hover | .signatureHelp | .definition | .references | .documentSymbols | .workspaceSymbols
   | .codeActionResolve | .saveOlean | .goals | .todo | .runWith | .release | .stats => true
-  | .initWorkspace | .listWorkspaces | .dropWorkspace | .resetStats | .shutdown => false
+  | .ensure | .initWorkspace | .listWorkspaces | .dropWorkspace | .resetStats | .shutdown => false
 
 def ProjectRequest.ofRequest (request : Request) : Except String ProjectRequest := do
   unless ProjectRequest.supportedOp request.op do
@@ -469,7 +468,7 @@ def ProjectRequest.ofRequest (request : Request) : Except String ProjectRequest
   if clientRequestId.isEmpty then
     throw "project requests require a non-empty clientRequestId"
   request.validateFields
-  pure { request, requestId := clientRequestId }
+  pure { request }
 
 instance : FromJson ProjectRequest where
   fromJson? json := do
@@ -484,9 +483,6 @@ instance : FromJson ProjectRequest where
 def ProjectRequest.op (request : ProjectRequest) : Op :=
   request.request.op
 
-def ProjectRequest.clientRequestId (request : ProjectRequest) : String :=
-  request.requestId
-
 /-- Attach one semantic request to a selected, authenticated workspace session. -/
 def ProjectRequest.attach
     (request : ProjectRequest)

Beam/BrokerClient.lean

@@ -23,7 +23,7 @@ private def usage : String :=
     "usage: beam-client [--port N] request <json|-> | request-stream <json|->",
     "",
     "beam-client is raw port-oriented maintainer/debug tooling.",
-    "For wrapper sessions, use: lean-beam --root PATH [--control-dir DIR] request-stream <json|->",
+    "For wrapper sessions, use: lean-beam --root PATH [--session-dir DIR] request-stream <json|->",
     "That supported machine interface selects the session descriptor and injects routing/authentication.",
     "",
     "request prints the final response on stdout and formats streamed diagnostics for humans on stderr.",

Beam/Cli/Args.lean

@@ -22,7 +22,7 @@ structure CliOptions where
   args : List String := []
 
 structure ParsedTextArg where
-  text? : Option String := none
+  text : String
   source : String := "argv"
 
 def parseNatArg (name value : String) : IO Nat := do
@@ -39,7 +39,7 @@ def hasSubstring (text needle : String) : Bool :=
   | _ => true
 
 def textArgUsage (cmdHead : String) : String :=
-  s!"usage: beam [--root PATH] {cmdHead} [--stdin | --text-file <path> | -- <text...> | <text...>]"
+  s!"usage: beam [--root PATH] {cmdHead} (--stdin | --text-file <path> | -- <text...> | <text...>)"
 
 def textArgReadsStdin (args : List String) : Bool :=
   match args with
@@ -48,19 +48,23 @@ def textArgReadsStdin (args : List String) : Bool :=
 
 def parseTextArg (cmdHead : String) (args : List String) : IO ParsedTextArg := do
   match args with
-  | [] => pure {}
+  | [] => throw <| IO.userError (textArgUsage cmdHead)
   | ["--stdin"] =>
-      pure { text? := some (← (← IO.getStdin).readToEnd), source := "stdin" }
+      pure { text := ← (← IO.getStdin).readToEnd, source := "stdin" }
   | ["--text-file", path] =>
-      pure { text? := some (← IO.FS.readFile (System.FilePath.mk path)), source := s!"text-file:{path}" }
-  | "--" :: rest =>
-      pure { text? := joinTextArgs rest, source := "argv" }
+      pure { text := ← IO.FS.readFile (System.FilePath.mk path), source := s!"text-file:{path}" }
+  | "--" :: rest => do
+      let some text := joinTextArgs rest
+        | throw <| IO.userError (textArgUsage cmdHead)
+      pure { text, source := "argv" }
   | "--stdin" :: _ =>
       throw <| IO.userError (textArgUsage cmdHead)
   | "--text-file" :: _ =>
       throw <| IO.userError (textArgUsage cmdHead)
-  | _ =>
-      pure { text? := joinTextArgs args, source := "argv" }
+  | _ => do
+      let some text := joinTextArgs args
+        | throw <| IO.userError (textArgUsage cmdHead)
+      pure { text, source := "argv" }
 
 def parseJsonText (label text : String) : IO Json := do
   match Json.parse text with
@@ -194,6 +198,29 @@ def parseLeanTodoArgs (args : List String) :
 def shellQuote (text : String) : String :=
   "'" ++ text.replace "'" "'\\''" ++ "'"
 
+inductive WrapperSessionCommand where
+  | serve (backend : Backend)
+  | status
+  | stop
+  | recoverGeneration (generation : String)
+  | recoverForce
+
+private def WrapperSessionCommand.text : WrapperSessionCommand → String
+  | .serve .lean => "serve"
+  | .serve .rocq => "serve rocq"
+  | .status => "status"
+  | .stop => "stop"
+  | .recoverGeneration generation =>
+      s!"recover --generation {shellQuote generation}"
+  | .recoverForce => "recover --force"
+
+/-- Render one exact public wrapper-session command selector. -/
+def wrapperSessionCommand
+    (root sessionDir : System.FilePath)
+    (command : WrapperSessionCommand) : String :=
+  s!"lean-beam --root {shellQuote root.toString} " ++
+    s!"--session-dir {shellQuote sessionDir.toString} {command.text}"
+
 def parseEnvFlag (raw : String) : Bool :=
   let normalized := raw.trimAscii.toString.toLower
   !(normalized.isEmpty || normalized == "0" || normalized == "false" || normalized == "no")
@@ -209,22 +236,29 @@ private def resolveExplicitRootArg (root : String) : IO System.FilePath := do
   catch err =>
     throw <| IO.userError s!"workspace root does not resolve: {err.toString}"
 
-private def resolveControlDirArg (dir : String) : IO System.FilePath := do
+private def resolveSessionDirArg (dir : String) : IO System.FilePath := do
   let path := System.FilePath.mk dir
-  if ← path.pathExists then
-    Beam.resolveExistingPath path
-  else
-    let cwd ← IO.currentDir
-    let absolute := if path.isAbsolute then path else cwd / path
-    pure absolute.normalize
+  unless path.isAbsolute do
+    throw <| IO.userError s!"--session-dir requires an absolute path, got '{path}'"
+  try
+    let metadata ← path.symlinkMetadata
+    match metadata.type with
+    | .symlink =>
+        throw <| IO.userError <|
+          s!"--session-dir does not accept a symbolic-link leaf: '{path}'"
+    | .dir | .file | .other =>
+        Beam.resolveExistingPath path
+  catch
+  | .noFileOrDirectory .. => Beam.resolvePathForCreation path
+  | err => throw err
 
 partial def parseCliOptions (opts : CliOptions) : List String → IO CliOptions
   | [] => pure opts
   | "--root" :: root :: rest => do
       let root ← resolveExplicitRootArg root
       parseCliOptions { opts with explicitRoot? := some root } rest
-  | "--control-dir" :: dir :: rest => do
-      let dir ← resolveControlDirArg dir
+  | "--session-dir" :: dir :: rest => do
+      let dir ← resolveSessionDirArg dir
       parseCliOptions { opts with explicitControlDir? := some dir } rest
   | "--port" :: port :: rest => do
       let port ← IO.ofExcept <| parsePortText "port" port