# PBS Verification and Safety Checks Specification

Status: Draft v0 (Skeleton)  
Applies to: verifier-facing safety obligations, artifact validation boundaries, and the division of safety checks across compiler, loader, verifier, and runtime

## 1. Purpose

This document will define the verification and safety-check model relevant to PBS-produced artifacts.

## 2. Scope

This document is intended to define:

- which safety obligations are enforced before runtime execution,
- the division of responsibility across compiler, loader, verifier, and runtime,
- verifier-facing assumptions about already-lowered artifacts,
- safety properties that must hold for conforming PBS-produced images.

This document does not define:

- full runtime trap semantics,
- source-language typing rules already owned elsewhere,
- one verifier implementation architecture.

## 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. `6.2. Host ABI Binding and Loader Resolution Specification.md`
4. `12. IR and Lowering Specification.md`
5. `15. Bytecode and PBX Mapping Specification.md`
6. This document

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

## 4. Normative Inputs

This document depends on, at minimum:

- `6.2. Host ABI Binding and Loader Resolution Specification.md`
- `12. IR and Lowering Specification.md`
- `15. Bytecode and PBX Mapping Specification.md`

## 5. Already-Settled Inputs

The following inputs are already fixed elsewhere and must not be contradicted here:

- Loader-side ABI validation is mandatory.
- Capability gating is mandatory during load.
- The verifier runs after loader patching on the final numeric executable image.
- Loader and verifier validate different layers of the contract.

## 6. Initial Section Targets

At minimum, the completed document should contain normative sections for:

1. safety-check phase boundaries,
2. compiler-emitted safety assumptions,
3. loader-side safety checks,
4. verifier-side safety checks,
5. residual runtime safety assumptions,
6. required deterministic rejection conditions.

## 7. TODO

The following items remain to be closed in future agenda discussion.

- Exact verifier obligations beyond what is already implied by runtime/bytecode authority.
- Which safety properties must be proven before execution versus checked defensively at runtime.
- Whether PBS-level conformance includes explicit verifier test surfaces or only artifact validity outcomes.
- How source-level diagnostics relate to verifier and artifact-level safety failures.

## 8. Non-Goals

- Replacing runtime or bytecode authority.
- Duplicating the full Host ABI spec.
- Freezing one verifier implementation algorithm.

## 9. Exit Criteria

This document is ready to move beyond skeleton status only when:

1. the division of safety responsibilities is explicit,
2. verifier-facing assumptions are aligned with lowering and artifact mapping,
3. deterministic rejection surfaces are normatively described,
4. the document no longer relies on unresolved `TODO` items for ordinary v1 safety claims.