Add formal terminal control models

.gitignore

@@ -41,6 +41,9 @@ cover.html
 cover.out
 cover_funcs.txt
 
+# TLA+ model checker artifacts
+**/states/
+
 # REDOGI
 doc/all
 doc/build/**/*.html

CHANGELOG.md

@@ -266,6 +266,8 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ### Fixed
 
+- Attempted to formally improve the semantics of job control and terminal control on both Linux and Windows.
+  Should fix potential bugs when running TUI programs from within mshell scripts.
 - On Windows, a command name containing a forward slash (e.g. `./script.msh`)
   is now treated as a file reference instead of being searched for on `PATH`,
   matching the behavior on Linux/macOS. Previously only backslashes were

ai/terminal-control/ASSUMPTIONS.md

@@ -0,0 +1,82 @@
+# Trusted platform contracts
+
+Checked against primary documentation on 2026-08-09.  These are assumptions at
+the formal model boundary and must be revisited when supported Go or operating
+system versions change.
+
+## POSIX Issue 8
+
+- A controlling terminal records one foreground process-group ID.  Terminal
+  access by background process groups is governed by the terminal driver and can
+  stop readers with `SIGTTIN` (and writers with `SIGTTOU` when `TOSTOP` applies).
+- `tcsetpgrp()` requires a terminal associated with the caller's session and a
+  process group in that session.  It can fail, including when the caller is a
+  background group and does not appropriately block or ignore `SIGTTOU`.
+- Each job is placed in its own process group.  The POSIX rationale recommends
+  calling `setpgid()` in both child and parent to close the fork/exec race.
+- A shell foregrounds a job with `tcsetpgrp()`, observes stopped children with
+  `waitpid(..., WUNTRACED)`, reclaims the terminal, and foregrounds a stopped job
+  before sending `SIGCONT`.
+
+Sources:
+
+- https://pubs.opengroup.org/onlinepubs/9799919799/utilities/V3_chap02.html#tag_19_11
+- https://pubs.opengroup.org/onlinepubs/9699919799/functions/tcsetpgrp.html
+- https://pubs.opengroup.org/onlinepubs/009604599/xrat/xbd_chap03.html
+- https://pubs.opengroup.org/onlinepubs/9799919799/basedefs/V1_chap03.html
+
+## Windows console
+
+- Any number of processes can share one console and its queued input buffer.
+  Windows has no POSIX-equivalent kernel foreground process group that gates
+  reads.  Therefore mshell must make its own reader quiescent before allowing a
+  foreground child to read the shared queue.
+- `CREATE_NEW_PROCESS_GROUP` creates a control-event group, not an input-owner
+  group.  It disables Ctrl+C in the new group.  `CTRL_BREAK_EVENT` can target the
+  group; `CTRL_C_EVENT` cannot be limited to a nonzero group.
+- the SetConsoleCtrlHandler Ctrl+C-ignore attribute is inherited.  Handler tables
+  are reset by `AttachConsole`, `AllocConsole`, and `FreeConsole`.
+- Console modes belong to console buffers, so processes sharing a buffer observe
+  changes to that shared state.  Mode changes need owner-scoped save/restore.
+- A ConPTY uses synchronous input and output channels.  Microsoft recommends a
+  separate servicing thread for each direction to avoid deadlock.  The host must
+  close its copies of handles given to the pseudoconsole after child creation so
+  broken-channel/EOF detection works.  Teardown output must continue to be
+  drained while closing the pseudoconsole.
+- Windows handle inheritance requires both an inheritable handle and inheritance
+  at `CreateProcess`; `PROC_THREAD_ATTRIBUTE_HANDLE_LIST` restricts the exact
+  inherited set.  Inherited handles refer to the same underlying objects.
+
+Sources:
+
+- https://learn.microsoft.com/en-us/windows/console/consoles
+- https://learn.microsoft.com/en-us/windows/console/console-input-buffer
+- https://learn.microsoft.com/en-us/windows/win32/procthread/process-creation-flags
+- https://learn.microsoft.com/en-us/windows/console/generateconsolectrlevent
+- https://learn.microsoft.com/en-us/windows/console/setconsolectrlhandler
+- https://learn.microsoft.com/en-us/windows/console/creating-a-pseudoconsole-session
+- https://learn.microsoft.com/en-us/windows/win32/procthread/inheritance
+
+## Go process creation
+
+The current development toolchain reports Go 1.26.5.  Its local source is the
+authoritative implementation reference for this checkout.
+
+- `exec.Cmd` copies non-`*os.File` stdin/stdout/stderr through goroutines; `Wait`
+  also waits for those copy goroutines under the documented rules.
+- On Unix, `syscall.SysProcAttr` exposes `Setpgid`, `Pgid`, and `Foreground`.
+  `Foreground` performs foreground placement in the child-side creation path and
+  requires a parent controlling-terminal descriptor in `Ctty`.
+- On Windows, `syscall.SysProcAttr` exposes `CreationFlags`,
+  `AdditionalInheritedHandles`, and `NoInheritHandles`; Go uses an extended
+  startup-info handle list for the selected inherited handles.
+- `os.Process.Signal(os.Interrupt)` is not implemented on Windows.  Windows
+  control events require platform-specific code and the limitations above.
+
+Sources:
+
+- https://pkg.go.dev/os/exec
+- https://pkg.go.dev/syscall#SysProcAttr
+- `/usr/lib/go/src/os/exec/exec.go`
+- `/usr/lib/go/src/syscall/exec_linux.go`
+- `/usr/lib/go/src/syscall/exec_windows.go`

ai/terminal-control/IMPLEMENTATION.md

@@ -0,0 +1,159 @@
+# Implementation blueprint
+
+## Current failure
+
+The current execution path resolves a child `cmd.Stdin`, but foreground control
+later tests and operates on `os.Stdin`.  This fails when mshell is reading a pipe
+and a child receives an explicitly opened terminal, as in `brename`:
+
+1. the editor receives a terminal handle as its effective stdin;
+2. mshell sees that its own inherited stdin is not a terminal and skips the
+   foreground transfer;
+3. the editor emits a terminal query (the observed OSC color sequence is an
+   example) and exits or fails to consume the response correctly;
+4. the response remains in the terminal input queue; and
+5. mshell resumes its interactive parser and treats response bytes such as `;r`
+   as user input, invoking the file-manager binding.
+
+The escape parser is not the correct primary fix.  While an editor owns the
+terminal, mshell must not read or interpret its input.  Parser hardening remains
+defense in depth for input received while mshell genuinely owns the terminal.
+
+The current code also discards errors from foreground transfer and restoration.
+That makes recovery unverifiable: the in-memory control flow can claim a handoff
+that the kernel rejected.
+
+## Proposed architecture
+
+Introduce one serialized `JobController`; do not spread process creation,
+terminal modes, input reading, waiting, and recovery across `RunProcess`,
+`RunPipeline`, the prompt, and platform helpers.
+
+```text
+resolved command and endpoints
+            |
+            v
+       JobController
+       /     |      \
+ reader gate   process launcher   terminal backend
+       |             |             /            \
+ prompt lexer    process/job table       POSIX       Windows
+```
+
+Core types should make the proof state visible:
+
+- `ResolvedEndpoint`: stream direction, concrete reader/writer, optional terminal
+  identity, ownership/lifetime, and child inheritance information.
+- `ResolvedStdio`: three endpoints plus aliases used by stream merging.
+- `Job`: stable ID, process records, pipeline topology, state, placement,
+  platform group/isolation identity, saved terminal mode, and completion state.
+- `ControlTransaction`: the one job currently acquiring or releasing terminal
+  control.  TLC found that this serialization cannot safely be implicit.
+- `InputGate`: starts, quiesces, and resumes the shell input reader and confirms
+  quiescence before a job is activated.
+- `TerminalBackend`: transactional acquire/reclaim/save/restore operations with
+  typed errors.  A failed acquire must run an explicit rollback.
+
+Every transition should return an error that identifies both the failed action
+and the recovery result.  No terminal-control error should be discarded.
+
+## Endpoint resolution
+
+Resolve all three child streams before process creation.  Terminal control is
+based on the resolved controlling-terminal identity, not on file-descriptor
+number 0 and not just on `os.Stdin`.
+
+For the original case, an `*os.File` opened from `/dev/tty` is both the child's
+stdin endpoint and a candidate controlling-terminal descriptor for
+`tcgetpgrp`/`tcsetpgrp`.  If the child has terminal output but redirected input,
+the job can still require foreground control for signals and output policy, so
+the decision is a job property rather than a single `stdinIsTerminal` test.
+
+Abstract `io.Reader`/`io.Writer` values without a descriptor are never guessed to
+be terminals.  Wrappers that intentionally preserve terminal identity should
+implement a private endpoint interface instead of relying on incidental Go type
+assertions throughout the evaluator.
+
+## POSIX backend
+
+1. Establish whether mshell has a controlling terminal independently from its
+   standard streams.  Interactive job control also requires mshell to be in its
+   own process group and in the terminal foreground before reading a prompt.
+2. Quiesce the shell reader and restore the shell's cooked baseline.
+3. Create one process group per job.  Use child-side `Setpgid` before exec and a
+   parent-side `setpgid`/verification where useful to close the documented race.
+4. Launch all pipeline members into that group.  Track start failure per member;
+   do not destroy the group when its leader exits early.
+5. Save shell modes, call `tcsetpgrp` with a descriptor for the controlling
+   terminal, check the result, restore the job's saved modes when continuing, and
+   send `SIGCONT` only after foregrounding a stopped job.
+6. Wait with stopped/continued status enabled and aggregate process state into
+   job state.
+7. On stop, exit, or error: save the job's modes if applicable, reclaim the
+   foreground group, restore shell modes, then resume the shell reader.
+
+Signal disposition must follow shell rules: the shell protects itself while it
+manipulates the terminal, children receive default job-control dispositions, and
+the protection is scoped and restored.
+
+## Windows backends
+
+Windows needs two explicit profiles because documented APIs cannot make a shared
+console enforce exclusive input access for background jobs.
+
+### Direct attached-console compatibility profile
+
+- Quiesce the shell reader before process creation/activation and do not resume
+  it until the child has stopped or exited.
+- Save and restore console input/output modes because they are shared buffer
+  state.
+- Treat `CREATE_NEW_PROCESS_GROUP` only as a control-event routing mechanism.
+  It is not terminal ownership, and it disables Ctrl+C for the created group.
+- Document Ctrl+C versus Ctrl+Break behavior exactly; targeted Ctrl+C via
+  `GenerateConsoleCtrlEvent` is not available.
+- Do not claim enforceable background-input isolation.  A background process
+  retaining the shared console input handle can consume the queue.
+
+This profile can correctly fix the foreground editor handoff, but it is not the
+foundation for full Windows job control.
+
+### Isolated ConPTY job-control profile
+
+- Give every terminal-using job its own ConPTY.  The child reads only its ConPTY
+  input; mshell is the sole reader of the real console and forwards input only to
+  the foreground job.
+- Service ConPTY input and output on independent workers with bounded queues and
+  cancellation.  Continue draining output through teardown as Microsoft
+  requires.
+- Restrict inherited handles with the extended startup handle list.  Close host
+  copies of child-only channel ends immediately after creation on success and on
+  every rollback path.
+- Combine the ConPTY with a Windows Job Object for process-tree accounting and
+  cleanup.  A Job Object is not the same concept as a shell job, so wrap it behind
+  the platform backend.
+- Define stop/continue semantics explicitly.  Windows exposes no documented
+  equivalent of POSIX `SIGTSTP`/`SIGCONT` for arbitrary console trees; the first
+  implementation may need to report stop/continue as unsupported rather than use
+  undocumented process-suspension APIs and falsely promise correctness.
+
+ConPTY changes presentation: mshell becomes a terminal relay and must forward
+virtual-terminal bytes transparently.  It should recognize only the terminal
+queries that mshell itself must answer as host; it must not reinterpret child
+output as shell input.
+
+## Testing strategy
+
+- Unit-test every controller transition and injected backend failure.
+- Generate transition traces from the TLA+ state graph and replay them against a
+  fake backend.
+- On POSIX, use a fresh session and pseudo-terminal for integration tests.  Cover
+  piped shell stdin plus `/dev/tty`, early pipeline-leader exit, stop/continue,
+  nested shells, terminal loss, and failed `tcsetpgrp`/mode restoration.
+- On Windows, test both classic Console Host and Windows Terminal, redirected
+  handles, Ctrl+C/Ctrl+Break, ConPTY resize, EOF, child-created descendants, and
+  teardown with a full output buffer.
+- Every interactive test must have a deadline and retain process/job handles so a
+  hung tree can be terminated and diagnosed.  Never rely only on killing the
+  immediate child.
+- Add a byte-stream corpus for parser defense in depth, but keep it separate from
+  ownership tests.  Escape-sequence coverage cannot prove terminal handoff.

ai/terminal-control/IMPLEMENTATION_STATUS.md

@@ -0,0 +1,70 @@
+# Implementation status
+
+Last updated: 2026-08-09.
+
+## Implemented
+
+- Resolved stdin/stdout/stderr metadata remains attached to the `exec.Cmd`
+  streams after redirects and merges are applied.
+- Terminal selection distinguishes an arbitrary TTY from the session's
+  controlling terminal and prefers resolved stdin, then stdout and stderr.
+- One serialized foreground transaction spans acquisition, `SIGCONT`, wait, and
+  reclamation, corresponding to the model's `controlJob` reservation.
+- Terminal/console modes are captured before transfer and restored only after
+  ownership is reclaimed.  Shell input remains blocked if either restoration
+  step fails.
+- The shell input gate rejects a foreground acquisition while an input read is
+  outstanding and rejects shell reads while a foreground job owns input.
+- POSIX single commands and pipelines use the resolved controlling-terminal
+  descriptor rather than `os.Stdin`.
+- A process group that may have stopped on `SIGTTIN` between `Start` and
+  `tcsetpgrp` receives `SIGCONT` only after it is foreground.
+- Pipeline stages retain a duplicated terminal handle through reclamation.  The
+  full test suite exposed the original borrowed-handle version closing too early;
+  the retained-handle implementation fixes that counterexample.
+- Acquisition failure kills and reaps the immediate child or pipeline processes
+  instead of waiting forever on a stopped terminal reader.
+- Windows direct-console control-handler installation errors are reported, and
+  the same serialized input gate prevents mshell from competing with a
+  foreground child for the shared console queue.
+- Windows and POSIX restore the exact previous foreground marker/process group
+  recorded during acquisition.
+- Foreground Windows commands inherit their resolved console and standard
+  handles directly.  The surrounding console host remains responsible for
+  keyboard input, output, escape sequences, Unicode, and resize events while
+  mshell stops reading and waits.
+- A nested foreground ConPTY was implemented and then removed because it made
+  mshell an unnecessary terminal proxy.  ConPTY remains a possible future
+  isolation mechanism for interactive background jobs, not the foreground
+  handoff mechanism.
+
+## Verification currently passing
+
+- Controller unit tests inject mode capture, acquisition, continue, rollback,
+  ownership restoration, and mode restoration failures and check operation order
+  and input-gate state.
+- A deadline-protected PTY test runs msh logic with piped shell stdin while the
+  child reads `/dev/tty`.  It kills the entire test session on timeout.
+- A second PTY test covers an interactive pipeline stage and terminal-handle
+  lifetime through pipeline completion.
+- Linux package tests pass.
+- Windows amd64 and macOS amd64 test binaries cross-compile.
+- All five bounded TLC configurations pass after the implementation changes.
+  `StreamLifecycle` was strengthened with the retained-terminal-handle invariant
+  discovered during implementation.
+
+## Not yet implemented
+
+- Durable job objects and user-facing `jobs`, `fg`, and `bg` operations.
+- Stopped/continued process aggregation and terminal-mode snapshots per stopped
+  job.
+- Asynchronous reaping for background jobs.
+- Per-job Windows ConPTY isolation, relay workers, resizing, and Job Object
+  cleanup.  These are future background-job facilities; foreground jobs should
+  continue to use direct console inheritance.
+- Mechanical trace replay or refinement checking between Go and TLA+.
+- Conditional liveness checks and unbounded TLAPS proofs.
+
+These remaining items are the future full-job-control program.  The current
+milestone fixes synchronous foreground handoff without pretending that the full
+program is complete.

ai/terminal-control/MODEL_RESULTS.md

@@ -0,0 +1,59 @@
+# TLC results
+
+Tool: TLA+ tools 1.7.4, TLC 2.19 (`5a47802`), Java 17.
+
+Last complete run: 2026-08-09.
+
+| Model | Configured size | Distinct states | Result |
+| --- | ---: | ---: | --- |
+| `TerminalControl` | 2 jobs | 204 | all configured invariants hold |
+| `POSIXTerminalControl` | 2 processes; shell stdin non-TTY, child stdin TTY | 58 | all configured invariants hold |
+| `POSIXTerminalControl` | 2 processes; child stdin non-TTY | 2 | all configured invariants hold |
+| `WindowsTerminalControl` | one foreground job | 11 | all configured invariants hold |
+| `StreamLifecycle` | 2 processes, 5 stream handles, retained terminal | 36 | all configured invariants hold |
+
+`check.sh` uses `-deadlock` because terminal `done` and explicitly failed states
+are expected to have no enabled action.  Invariant checking still explores their
+complete reachable state graph.
+
+## Counterexample found during modeling
+
+The first `TerminalControl` version did not serialize acquisition transactions.
+TLC found this trace:
+
+1. job 1 begins a foreground launch;
+2. job 2 begins in the background and requests `fg`;
+3. job 2 pauses the shell;
+4. job 1 fails and enters recovery;
+5. job 2 acquires the terminal, stops, reclaims it, and resumes the shell; and
+6. job 1 remains forever in a recovery state that can no longer satisfy its
+   preconditions.
+
+The model now has a single `controlJob` reservation spanning resolution through
+recovery.  This is a design requirement for the future Go controller, not merely
+a modeling convenience.
+
+## Boundaries and unfinished proof work
+
+- These are exhaustive finite-state safety checks, not unbounded TLAPS proofs.
+- The current platform modules are contract models, not yet mechanically checked
+  refinement mappings to `TerminalControl`.
+- Progress requirements are documented but not checked yet.  Fairness must be
+  stated carefully because children are allowed to run forever or retain handles.
+- The Windows model covers reader quiescence in a shared console.  A separate,
+  larger ConPTY relay model is required before claiming full Windows isolation.
+- Terminal resize, nested shells, signal masks, per-process stopped/continued
+  aggregation, mode-snapshot failure, and shutdown policy need additional state.
+- The Go controller and failure-injection tests mirror the principal ownership
+  transitions, but no refinement checker has mechanically proved that every Go
+  execution implements the TLA+ specification.  Generated trace replay remains
+  a next conformance step.
+
+The stream model now also requires a duplicated controlling-terminal handle to
+remain live from endpoint resolution through job completion and to be closed in
+terminal states.  This invariant was added after the Go integration tests found
+that retaining only a borrowed pipeline descriptor allowed a stage to close it
+before terminal reclamation.
+
+Accordingly, the present result should be described as a checked formal design
+foundation, not as “mshell terminal handling is formally verified.”