# VM Architecture

This document defines the VM architecture, scheduling semantics, and concurrency envelope used by Rust runtime targets and Lean conformance surfaces.

## Architecture Overview

The canonical semantic authority is `VMKernel`. The cooperative `VM` and threaded `ThreadedVM` are execution adapters that call kernel-owned step entrypoints. Both implement the `KernelMachine` trait, which provides `kernel_step_round` for executing scheduler rounds.

The runtime keeps a single state model across targets. Core state includes coroutines, sessions, scheduler queues, observable trace, effect trace, and failure-topology snapshot fields.

The canonical round model is one semantic step when concurrency is nonzero. Threaded execution is admitted as an extension only when the wave certificate gate is satisfied.

## Engine Roles

| Engine | Role | Contract Surface |
|---|---|---|
| `VM` | Canonical cooperative runtime | Exact reference for parity at concurrency `1` |
| `ThreadedVM` | Parallel wave executor | Certified-wave execution with fallback to canonical one-step |
| WASM runtime | Single-thread deployment | Cooperative schedule only |

## Scheduler Semantics

Canonical scheduling is one semantic step when concurrency is nonzero. `VMKernel` owns the selection and step contract. For cooperative execution, this gives exact behavior for deterministic replay and baseline parity.

The canonical Lean runner is `runScheduled` in `Runtime/VM/Runtime/Runner.lean`. For nonzero concurrency, canonical round semantics normalize to one scheduler step. This model is the semantic reference for parity at concurrency `1`.

## Scheduler Policies

Scheduler policy controls selection order. Policy does not change instruction semantics.

| Policy | Primary Runtime Use |
|---|---|
| `Cooperative` | Canonical single-step execution and WASM deployment |
| `RoundRobin` | Fair queue progression in native runs |
| `Priority` | Explicit priority maps or token weighting |
| `ProgressAware` | Token-biased pick behavior |

## Threaded Wave Execution

Threaded execution selects compatible picks per wave. Compatibility is lane-disjoint, session-disjoint, and footprint-disjoint for picks in the same wave.

The threaded extension is defined in `Runtime/VM/Runtime/ThreadedRunner.lean`. Concurrency `n = 1` is theorem-equal to canonical execution. For `n > 1`, execution is admitted through certified waves. Invalid certificates degrade to canonical one-step behavior.

Each wave is checked against a `WaveCertificate`. If certificate validation fails, the runtime degrades to canonical one-step behavior for that round.

## Refinement Envelope

| Concurrency Regime | Required Contract | Enforcement Lane |
|---|---|---|
| `n = 1` | Exact canonical parity | `threaded_equivalence.rs` |
| `n > 1` | Envelope-bounded parity with declared `EnvelopeDiff` | `parity_fixtures_v2.rs` |
| Invalid wave certificate | Mandatory fallback to canonical one-step | `threaded_lane_runtime.rs` |
| Undocumented deviation | Active deviation coverage required | `just check-parity --types` |

The regression lane validates both regimes. The test `canonical_parity_is_exact_at_concurrency_one` enforces exact equality. The test `envelope_bounded_parity_holds_for_n_gt_1` enforces envelope-bounded behavior.

## Runtime Gates

Runtime mode admission and profile selection are capability gated.

| Gate | Runtime Surface | Current Rust Path |
|---|---|---|
| Advanced mode admission | `requires_vm_runtime_contracts` and `admit_vm_runtime` | `rust/vm/src/runtime_contracts.rs`, `rust/vm/src/composition.rs` |
| Determinism profile validation | `request_determinism_profile` | `rust/vm/src/runtime_contracts.rs`, `rust/vm/src/composition.rs` |
| Threaded certified-wave fallback | `WaveCertificate` check with one-step degrade | `rust/vm/src/threaded.rs` |
| Deviation registry enforcement | Undocumented parity drift rejection | `just check-parity --types` |

## Runtime Hardening Contracts

The VM adapters now enforce explicit runtime hardening at load and startup boundaries.

- `ThreadedVM` provides both `with_workers` (panic-on-invalid initialization compatibility path) and `try_with_workers` (fallible initialization with `VMError`).
- Cooperative and threaded `load_choreography` paths validate trusted `CodeImage` runtime shape before session allocation.
- Register-bound violations are fail-closed through `Fault::OutOfRegisters` rather than unchecked index panic in executable instruction paths.

## Capability Gate Architecture

| Capability Gate | Lean Surface | Rust Surface |
|---|---|---|
| Advanced mode admission | `requiresVMRuntimeContracts`, `admitVMRuntime` | `requires_vm_runtime_contracts`, `admit_vm_runtime` |
| Live migration switch | `requestLiveMigration` | Runtime contracts capability booleans in composition admission |
| Autoscale/repartition switch | `requestAutoscaleOrRepartition` | Runtime contracts capability booleans in composition admission |
| Placement refinement switch | `requestPlacementRefinement` | Runtime contracts capability booleans in composition admission |
| Relaxed reordering switch | `requestRelaxedReordering` | Runtime contracts capability booleans in composition admission |

## Determinism Profiles

`VMConfig.determinism_mode` includes `Full`, `ModuloEffects`, `ModuloCommutativity`, and `Replay`.

| Profile | Lean Profile | Rust Profile | Gate Requirement |
|---|---|---|---|
| Full | `full` | `DeterminismMode::Full` | Profile artifact support |
| Modulo effect trace | `moduloEffectTrace` | `DeterminismMode::ModuloEffects` | Mixed-profile capability plus artifact support |
| Modulo commutativity | `moduloCommutativity` | `DeterminismMode::ModuloCommutativity` | Mixed-profile capability plus artifact support |
| Replay | `replay` | `DeterminismMode::Replay` | Mixed-profile capability plus artifact support |

## Communication Consumption Identity

Communication replay-consumption uses one canonical identity schema across send and receive checks.

Canonical identity fields:

- Domain tag: `telltale.comm.identity.v1`
- Session id: `sid`
- Directed edge endpoints: `sender`, `receiver`
- Protocol step context: `step_kind` (`send`, `recv`, `offer`, `choose`) and local label context
- Message label: `label`
- Payload digest: domain-separated digest of serialized payload bytes
- Sequence number: `seq_no` (used by `sequence` mode, carried for all modes)

Replay semantics by mode:

- `off`: no replay-consumption checks are enforced.
- `sequence`: receive must consume exactly the expected next `seq_no` per `(sid, sender, receiver)`.
- `nullifier`: receive computes a nullifier over the canonical identity and rejects already-consumed identities.

Replay outcomes:

- Duplicate delivery: reject in `sequence` and `nullifier`, accept in `off`.
- Reordered delivery: reject in `sequence`, accepted when unseen in `nullifier`, accept in `off`.
- Cross-session reuse: reject in `sequence` and `nullifier` because `sid` is part of canonical identity.

## Proved Theorem Surfaces

| Area | Lean Surface | Status |
|---|---|---|
| Canonical round normalization | `Runtime/Proofs/Concurrency.lean` | Proved |
| Threaded equality at `n = 1` | `schedRoundThreaded_one_eq_schedRound_one`, `runScheduledThreaded_one_eq_runScheduled` | Proved |
| Per-session trace equality at `n = 1` | `per_session_trace_threaded_one_eq_canonical` | Proved |
| Scheduler theorem exports | `Runtime/Proofs/VM/Scheduler.lean` | Proved |

## Premise-Scoped Interface Surfaces

| Area | Lean Surface | Interface Type |
|---|---|---|
| Threaded `n > 1` refinement | `ThreadedRoundRefinementPremises` | Premise-scoped |
| Runtime admission/profile gates | `Runtime/Proofs/Contracts/RuntimeContracts.lean` | Interface consumed by runtime |
| Theorem-pack capability inventory APIs | `Runtime/Proofs/TheoremPack/API.lean` | Interface consumed by runtime |

These interfaces are intentionally explicit. They are not claimed as unconditional global theorems. Canonical one-step normalization and `n = 1` refinement are theorem-backed in Lean. Higher-concurrency threaded refinement is modeled as a certified interface with premise-scoped refinement obligations. Rust uses executable certificate checking and parity fixtures as release guards.

## Release and CI Conformance

Release conformance surfaces are exported through theorem-pack APIs and enforced by `just check-release-conformance`. Parity and drift governance are enforced by `just check-parity --all`.

## Related Docs

- [Bytecode Instructions](13_bytecode_instructions.md)
- [Session Lifecycle](14_session_lifecycle.md)
- [VM Simulation](15_vm_simulation_overview.md)
- [Rust-Lean Parity](19_rust_lean_parity.md)
- [Effect Handlers and Session Types](11_effect_session_bridge.md)
- [Lean Verification](23_lean_verification.md)
- [Capability and Admission](25_capability_admission.md)
