89 lines
3.2 KiB
Markdown
89 lines
3.2 KiB
Markdown
# 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.
|