136 lines
4.7 KiB
Markdown
136 lines
4.7 KiB
Markdown
# 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.
|