# PBS Verification and Safety Checks Specification

Status: Draft v1 (Quality-Gate Baseline)  
Applies to: test-backed safety gates for backend compiler stages and integration regression safety checks against runtime

## 1. Purpose

This document defines the minimum safety/verification quality gates that must be enforced for executable backend pipelines.

Its purpose is to keep safety measurable and deterministic across:

- lowering,
- optimization,
- emission,
- and runtime integration boundaries.

## 2. Scope

This document defines:

- mandatory compiler-stage safety checks for executable pipeline stages,
- conditional integration safety regression checks against runtime line,
- and evidence requirements for safety-related support claims.

This document does not define:

- full runtime verifier algorithm internals,
- formal proof of all runtime safety properties,
- or one mandatory verifier/optimizer architecture.

## 3. Authority and Precedence

Normative precedence:

1. `docs/pbs/specs/2. Governance and Versioning.md`
2. `docs/pbs/specs/12. Diagnostics Specification.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

If a rule here conflicts with higher-precedence authorities, it is invalid.

## 4. Normative Inputs

This document depends on:

- `docs/pbs/specs/12. Diagnostics Specification.md`
- `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`

## 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.