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

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. A Ver

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 A Ver items for ordinary v1 safety claims.