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