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.