design: define os Environment and argv contract

[vycdev2]

Summary

Define the canonical Environment/argv effect contract before changing the current hardcoded os.env and os.args behavior, and establish the intended boundary between public compiler-shipped .jett declarations and private host-access runtime kernels.

Source documentation

• docs/progress.md — Phase K os status
• docs/design.md — Rule Set 16: Capability-Based I/O
• docs/architecture.md — Phase 6 capability types
• docs/architecture.md — Phase K standard library

Current state

• The typechecker exposes capability-free os.env(string) -> optional[string] and os.args() -> list[string] signatures.
• The interpreter calls std::env::var and std::env::args directly. The environment lookup collapses missing variables and non-Unicode values to none, while std::env::args includes the program name.
• These public os.* calls are not classified as impure and can currently run in verify blocks.
• Rule Set 16 instead says OS reads require explicit capability values, documents Environment.get(view env, ...), and specifies Environment.args(view env) with the program name excluded.
• A partial hardcoded Environment.args checker entry exists, but there is no corresponding public stdlib declaration or interpreter implementation.
• There is no stdlib/os.jett; the public signatures and behavior remain compiler/Rust-owned rather than source-owned with private runtime kernels.

Scope

This issue should decide:

• whether the canonical public API remains under os.*, becomes capability-shaped Environment operations, or uses a compatibility transition between them;
• whether environment and argv reads require view Environment, how impurity propagates, and whether these reads are available during verify or comptime execution;
• whether argv includes the executable/program name;
• how missing and invalid/non-Unicode environment values are represented;
• which public declarations and compositional behavior live in compiler-shipped .jett source, with host access retained only behind private interpreter/runtime kernels;
• how the current os.env, os.args, and partial Environment.args paths migrate without leaving duplicate public contracts.

It does not include process spawning/lifecycle APIs, new filesystem APIs, HIR/MIR/native lowering, the general runtime ABI, or the module/import/trusted-origin work tracked by #3.

Acceptance criteria

• The canonical Environment/argv API and compatibility treatment for os.env, os.args, and Environment.args are documented.
• Capability requirements, impurity propagation, and verify/comptime behavior are explicit and consistent with Rule Set 16.
• Program-name inclusion or exclusion is specified and covered by a focused argv test.
• Missing and invalid/non-Unicode environment-value behavior is specified and covered.
• Public os declarations are owned by compiler-shipped .jett source; Rust/interpreter/runtime code retains only private host-access kernels.
• Focused compile-pass and compile-fail tests pin the selected effect behavior and public signatures.
• docs/progress.md, docs/design.md, and docs/architecture.md reflect the decision.
• Process management and filesystem work remain explicitly out of scope.

Dependencies / open questions

Issue #3 owns module imports and trusted stdlib origins. Process management should receive separate tracking only after its public capability and lifecycle requirements are bounded; it is intentionally not folded into this Environment/argv issue.

This was generated by an AI agent (vycdev2). Please verify any changes before merging or applying.