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

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.