Checked Linux paths

Std.Path represents a path as a list of byte segments and an absolute flag. stdPathToLinuxBytes is the explicit checked boundary:

StdPath -> StdResult StdPathError Bytes

The first bad segment, and then the first bad byte in that segment, determines its error. StdPathEmptySegment rejects empty segments, StdPathNulByte rejects byte zero, and StdPathSeparatorByte rejects a slash within a segment. Every other byte is retained, including invalid UTF-8. Names are not decoded, normalized, resolved, or looked up in the filesystem.

stdPathJoin left right returns an absolute right operand unchanged. A relative right operand appends its segments and keeps the left absolute flag. Dot and dot-dot segments remain literal. Valid segments render with exactly one slash between them and, for an absolute path, one leading slash. No trailing slash is inserted. A path with no segments renders as empty when relative and / when absolute. The empty relative name is passed to the OS, whose open operation fails; it is not silently interpreted as the current directory.

Std.System/stdSystemReadPath and stdSystemWritePath construct File effects through this boundary. Their results are StdResult StdPathError Bytes and StdResult StdPathError Nat, respectively. A rejected path returns a typed error without constructing a read or write. OS failures preserve the underlying File operation's hard failure behavior; they are not converted into successful empty bytes or a zero byte count.

Text output uses stdTextBytes explicitly before stdSystemWritePath. The checked boundary does not infer an encoding from file contents.

The generic native write-file operation retries every positive short write until the payload is complete and returns the total byte count. A zero result, an OS error (including EINTR), or a result larger than the remaining length is a hard write failure (native evaluator exit 131). This is distinct from the durable-checkpoint writer's bounded EINTR retry policy. The generic operation writes a temporary file before verified publication: these failure cases retain the previous destination, and may leave a partial .alpha-tmp file. A successful three-byte Text output returns 3, even if three one-byte syscalls were needed.

stdPathToBytes remains a lexical renderer. The historical Std.Effect path helpers use that renderer; callers requiring typed validation use the checked Std.System entry points. Raw read-file and write-file still accept Bytes. This change adds no source syntax, core constructor, or binary format.

Evidence and remaining qualification

tests/language/path/PathLaws.alpha checks boundary and join laws, plus rejected read/write computations. NativePath.alpha uses Alpha assertions over observed native output and exit status: byte output, explicit Text output, rejected paths, missing-file failure, read-after-write, and an invalid-UTF-8 filename. The separate false-control-tests manifest must fail with ALPHA-TEST-BYTES.

WriteModel.alpha supplies a typed, ordered syscall-outcome provider for an independent Model-lane write contract: 15 laws cover completion, partial writes, zero progress, oversized results, OS errors, provider exhaustion, and ignored outcomes after completion. It is test code, and does not implement File effects. The shared L25 lifecycle provider remains separate work.

Run ALPHA=/absolute/path/to/alpha python3 debug/short-write-check.py --output /new/evidence/directory on Linux x86-64. It compiles fresh native fixtures, limits actual kernel writes with ptrace, injects failure outcomes, and passes captured counts and bytes to ShortWriteObservations.alpha. Three altered observations must be rejected. Positive short writes really write bytes; they are not simulated by merely replacing the syscall return value.

These fixtures use the default native evaluator lane. They do not establish direct lowering for every dynamic path shape or qualify all L25 OS lifecycles. Builder native-copy accounting remains open under TXT-006.