prometeu-studio/docs/specs/compiler/19. Verification and Safety Checks Specification.md

# Compiler Verification and Safety Checks Specification

Status: Draft v1 (Quality-Gate Baseline)  
Applies to: test-backed safety gates for common compiler stages, validation ownership across executable frontends, and integration regression safety checks against runtime

## 1. Purpose

This document defines the minimum safety/verification quality gates that must be enforced for executable compiler pipelines, and the ownership rule that separates language validation from platform validation.

Its purpose is to keep safety measurable and deterministic across:

- lowering,
- optimization,
- emission,
- runtime integration boundaries,
- and the classification of diagnostics that every executable frontend must obey.

PBS is the current executable frontend. It is an example, not the owner of this specification.

## 2. Scope

This document defines:

- mandatory compiler-stage safety checks for executable pipeline stages,
- conditional integration safety regression checks against runtime line,
- evidence requirements for safety-related support claims,
- and validation-ownership rules that apply to all executable frontends.

This document does not define:

- full runtime verifier algorithm internals,
- formal proof of all runtime safety properties,
- one mandatory verifier/optimizer architecture,
- PBS syntax or static-semantics catalogs,
- or a generic validator-core package.

## 3. Authority and Precedence

Normative precedence:

1. Runtime authority (`docs/specs/hardware/topics/chapter-2.md`, `chapter-3.md`, `chapter-9.md`, `chapter-12.md`, `chapter-16.md`)
2. Bytecode authority (`docs/specs/bytecode/ISA_CORE.md`)
3. `20. IRBackend to IRVM Lowering Specification.md`
4. `21. IRVM Optimization Pipeline Specification.md`
5. `15. Bytecode and PBX Mapping Specification.md`
6. `13. Conformance Test Specification.md`
7. This document
8. Frontend diagnostics specifications, including `docs/specs/compiler-languages/pbs/12. Diagnostics Specification.md`, for language-owned coverage only

If a rule here conflicts with a higher-precedence authority, it is invalid. Frontend diagnostics documents MUST NOT redefine compiler-general safety gates or platform validation ownership.

## 4. Normative Inputs

This document depends on:

- `13. Conformance Test Specification.md`
- `15. Bytecode and PBX Mapping Specification.md`
- `20. IRBackend to IRVM Lowering Specification.md`
- `21. IRVM Optimization Pipeline Specification.md`
- `docs/specs/compiler-languages/pbs/12. Diagnostics Specification.md` as the current frontend diagnostics catalog, not as the owner of this specification

## 5. Safety Gate Model

### 5.1 Gate S-U: Compiler-Stage Safety Unit Tests (Required)

For executable pipelines, S-U must cover stage-level safety checks at minimum:

1. `LowerToVM` safety checks:
   - deterministic control-flow lowering checks,
   - deterministic function-id assignment checks,
   - mandatory slot/return shape checks,
   - mandatory callsite form checks.
2. `OptimizeIRVM` safety checks:
   - semantic-preservation regression checks,
   - deterministic output checks for same input graph,
   - profile-compatibility checks (`vm_profile`).
3. `EmitBytecode` safety checks:
   - deterministic function/code layout checks,
   - host-backed pre-load form checks (`HOSTCALL`, `SYSC`),
   - deterministic rejection for malformed emission candidates,
   - minimum debug-attribution output checks.
4. deterministic diagnostics identity for required rejection surfaces (`code`, `severity`, primary attribution when applicable).

This gate is mandatory regardless of backend maturity stage.

### 5.2 Gate S-I: Integration Safety Regression With Runtime (Required for Executable Backends)

For backends that emit executable artifacts, S-I must cover integration safety at minimum:

1. valid pre-load host path that loader patches and runtime executes,
2. rejection of out-of-bounds `HOSTCALL` index,
3. rejection of unused `SYSC` declarations,
4. rejection of raw `SYSCALL` in pre-load artifact,
5. rejection of host ABI mismatch (`arg_slots`/`ret_slots`),
6. rejection of missing capability at load-time,
7. valid VM-owned intrinsic path,
8. repeatability across declared runtime line.

When executable artifact emission is not present, S-I may be explicitly `deferred`.

## 6. Evidence Requirements

Safety claims must map to gate evidence:

1. S-U evidence is required for baseline safety posture,
2. S-I evidence is required for integration-ready safety claims,
3. and published safety-related support claims must remain evidence-backed and current.

For executable backends, evidence should include deterministic regression fixtures that prove pipeline order and stage-boundary safety behavior.

## 7. Deterministic Failure Taxonomy Expectations

Backend safety checks should expose stable rejection families at minimum:

1. `MARSHAL_FORMAT_*`,
2. `MARSHAL_LINKAGE_*`,
3. `MARSHAL_VERIFY_PRECHECK_*`.

This taxonomy complements existing diagnostics contracts and does not replace runtime loader/verifier error surfaces.

## 8. Explicit Deferrals

The following are intentionally deferred:

- full formal verifier obligation catalog,
- formal proof frameworks for optimizer equivalence,
- and richer standardized source-map formats beyond v1 minimum hooks.

## 9. Non-Goals

- Replacing runtime or bytecode authority.
- Freezing optimizer/verifier internal architecture prematurely.
- Defining performance tooling in a safety specification.

## 10. Exit Criteria

This document is healthy when:

1. required stage-level safety checks are test-backed,
2. executable backends have explicit S-I status (`pass`/`fail`/`deferred`),
3. integration safety regressions are preserved in tests,
4. and safety-related support claims remain evidence-backed.

## 11. Validation Ownership

A validation MUST live at the lowest layer that understands the failure without knowing the source language.

- A check is language-owned if it needs AST, tokens, a language marker, a barrel, or another source-language rule.
- A check is platform-owned if it can be performed on `IRBackend`, `IRLifecycleDeclaration`, IRVM, PBX, host/capability tables, or ids.

Adding a validation MUST record:

1. the input artifact the check reads;
2. whether that artifact is language source/AST/marker or a common contract;
3. the matrix owner;
4. the code family (`E_PARSE_*` / `E_SEM_*` / `E_LINK_*` / `E_HOST_*` versus `COMMON_*` / `LOWER_IRVM_*` / `MARSHAL_*`);
5. whether the span comes from a common-contract origin or from language tokens/AST.

If item 2 is both, the implementation MUST emit two diagnostics with distinct identities, not one hybrid.

### 11.1 Diagnostic identity and span

Platform diagnostics MUST use `COMMON_*`, `LOWER_IRVM_*`, or `MARSHAL_*` codes and the phase of the pipeline stage that reports them.

PBS MUST keep its current `E_PARSE_*`, `E_SEM_*`, `E_LINK_*`, and `E_HOST_*` codes.

This specification MUST NOT rewrite diagnostic messages or renumber existing codes.

Common code MUST copy origin/span when the declaration, instruction, or metadata carries one. A missing origin MUST be a structural error. Implementations MUST NOT invent a span.

The same fact MAY exist on both sides. PBS explains the language rule; the common layer rejects an invalid handoff even when the frontend has no PBS markers. The two errors MUST keep distinct identities. Example: `E_SEM_MISSING_PROJECT_FRAME` and a missing frame root on an executable `IRLifecycleDeclaration`.

### 11.2 Initial ownership matrix

| Family | Owner | Status | Notes |
| --- | --- | --- | --- |
| Parse / syntax (`ParseErrors`) | `compiler/pbs` | language | remains |
| Type, flow, declaration, const, and source-form global semantics | `compiler/pbs` | language | remains |
| Markers `[Init]`, `[Frame]`, `InitAllowed`, signature, colocation | `compiler/pbs` | language | already split by lifecycle assembly |
| `host call not allowed during init` | `compiler/pbs` | language | marker/source rule |
| PBS linking (`PbsLinkErrors`, barrel, import, visibility) | `compiler/pbs` | language | do not extract |
| Source shape of `[Host]` / `[Capability]` | `compiler/pbs` | language | host-admission split |
| Canonical host-binding identity and capability over `IRReservedMetadata` | `compiler/general` | platform | classified; validator remains in the PBS package until a later plan |
| Lifecycle assembler | `compiler/general` | platform | already implemented |
| IRVM preconditions for wrapper, boot guard, origin | `compiler/general` | platform | already implemented |
| `IRVMValidator`, lowering, marshal/bytecode | `compiler/general` | platform | already implemented |
| `Addressable` / asset path | `compiler/general` | platform | classified; no extra migration in this specification |
| Gates S-U/S-I | `compiler/general` | platform | this document |

### 11.3 Host admission, assets, and linking

Host admission is split:

- language owns the source shape of `[Host]` and `[Capability]`;
- platform owns canonical binding identity `(module, name, version)`, unknown capability, undeclared capability, and inconsistent binding once those facts exist on `IRReservedMetadata`.

`PbsHostAdmissionValidator` MAY remain in the PBS package until a later plan. `E_HOST_*` MUST NOT be treated as eternal PBS semantics.

`Addressable` / asset-path resolution is platform-owned. This specification classifies it and MUST NOT move additional asset code.

PBS linking, barrel files, and `PbsLinkErrors` remain language-owned. `ResolveDeps` does not authorize extracting them.

### 11.4 What this section does not authorize

This specification MUST NOT be read as authorizing:

- a generic validator-core package;
- moving `PbsHostAdmissionValidator` into a common package;
- moving asset-resolution production code;
- extracting PBS linking;
- or reopening lifecycle-assembly ownership.

Platform validators MUST NOT depend on types from the PBS frontend module (`prometeu-frontend-pbs`). The package `p.studio.compiler.pbs` is not the complete boundary; facades shipped by that module remain PBS-owned. Platform validators MUST NOT discover roles from `__pbs.` prefixes.