104 lines
6.6 KiB
Markdown
104 lines
6.6 KiB
Markdown
# Phase 0.9C capability closure
|
|
|
|
Status: **NO TARGET CAPABILITY CLOSED**.
|
|
|
|
“Host evidence” below means a deterministic model or source validator. It is
|
|
not PS5 evidence. `implementation allowed` and `execution allowed` are false
|
|
for every capability because the startup/exit, output, firmware-source, and
|
|
side-effect gates fail before target implementation.
|
|
|
|
## Closure matrix
|
|
|
|
| Capability | Source evidence | Host evidence | Target evidence | Implement allowed | Execute allowed | Remaining blocker |
|
|
|---|---|---|---|---:|---:|---|
|
|
| runtime self-identity | future protocol binds observer version and artifact SHA-256 | framing validates both | absent | false | false | no target artifact or runtime self-binding |
|
|
| firmware source 1 | SDK `kernel_get_fw_version`, `crt/kernel.c:148-170` | protocol binds raw value | absent | false | false | depends on prohibited runtime and is not independent system identity |
|
|
| firmware source 2 | export-stub name only, no accepted signature/semantics | missing/conflict tests fail closed | absent | false | false | independent accepted source absent |
|
|
| mount query | SDK `samples/mntinfo` and libc wrapper | unsupported can be represented | absent | false | false | ABI, completeness, runtime behavior and effects unproven |
|
|
| metadata | controlled manager no-follow pattern | result framing can represent error | absent | false | false | target metadata/no-follow semantics and effects unproven |
|
|
| object ID | manager compares `st_dev/st_ino` | completeness rules modeled | absent | false | false | stable target identity and race contract unproven |
|
|
| size | manager compares exact `st_size` | checked result length modeled | absent | false | false | current object and stable-read evidence absent |
|
|
| SHA-256 | bounded same-FD manager implementation | checksum corruption is rejected | absent | false | false | target read effects, current paths and stable object absent |
|
|
| processes | SDK `samples/ps` partial snapshot | unsupported result modeled | absent | false | false | complete ABI, bounds and semantics absent |
|
|
| services | no complete source/API mapping | unsupported result modeled | absent | false | false | service inventory and ownership semantics absent |
|
|
| listeners | no accepted snapshot/owner API | unsupported result modeled | absent | false | false | listener API, ownership and side effects absent |
|
|
| autoload/startup/retry | stock manager readers/HTTP are incomplete or side-effecting | missing source remains blocked | absent | false | false | complete authoritative sources and safe collector absent |
|
|
| rollback objects | Phase 0.8R/0.9A evidence contract only | no false promotion in validators | absent | false | false | current exact backups absent; manager backup is hard blocker |
|
|
| monotonic time | hardened loader uses `CLOCK_MONOTONIC` | deadline expiry is rejected | absent in observer ABI | false | false | loader exposes no clock callback; freestanding callable ABI absent |
|
|
| startup | SDK and hardened loader callgraphs | startup classifications validated | absent | false | false | normal CRT writes; freestanding dependency closure incomplete |
|
|
| output | current route proven send-only; D1 host contract defined | 4096-byte framing and negative tests | absent | false | false | no caller-owned target buffer/copy-out/manager delivery |
|
|
| normal exit | loader has wait/reap; status discarded | no safe exit terminal modeled | absent | false | false | return/exit semantics and teardown unproven |
|
|
| error exit | CRT error/longjmp/trap and loader reap reviewed | observer error cannot equal empty success | absent | false | false | partial unwind, status and cleanup unproven |
|
|
| timeout | loader SIGTERM/SIGKILL watchdog reviewed | timeout record is rejected | absent | false | false | kill/timeout is not an admissible safe exit |
|
|
| cleanup | pre-detach cleanup state exists; post-detach relies on process lifetime | failed/incomplete cleanup rejected | absent | false | false | mappings, FDs, buffers, loader and manager cleanup not jointly proven |
|
|
| recovery independence | Phase 0.9A contract | blocker preserved | absent | false | false | recovery executor and exact rollback objects unproven |
|
|
|
|
## Firmware-source closure
|
|
|
|
Current source 1 reads a process-parameter field associated with
|
|
`libSceLibcInternal`; its own comment says it is chosen because some payloads
|
|
modify the kernel-reported value. That makes it useful source evidence, but
|
|
not an independent second current device identity.
|
|
|
|
The SDK stubs contain
|
|
`sceKernelGetProsperoSystemSwVersion`, but a stub exports only a name/NID
|
|
surface. The repository has no reviewed public prototype, result layout,
|
|
return semantics, side-effect contract, or firmware-9.60 observation. It is
|
|
not callable evidence and is not source 2.
|
|
|
|
A future source 2 must:
|
|
|
|
1. be official/reproducible public platform evidence or a separately reviewed
|
|
locally obtained runtime value;
|
|
2. have exact function/data ABI and side-effect evidence;
|
|
3. identify the current system, not the observer's compiled SDK requirement;
|
|
4. produce an exact raw value under the same deadline;
|
|
5. be independent of source 1's data origin;
|
|
6. bind source identity, raw result, nonce, request ID, observer artifact hash
|
|
and deadline into the result record; and
|
|
7. fail closed if absent, ambiguous, stale, or conflicting.
|
|
|
|
The host protocol returns
|
|
`BLOCKED_FIRMWARE_SOURCE_2_ABSENT` for absence and
|
|
`BLOCKED_FIRMWARE_CONFLICT` for disagreement. It never normalizes a conflict
|
|
away or prefers one source.
|
|
|
|
## Cross-gate closure
|
|
|
|
The following dependencies form one conjunctive gate:
|
|
|
|
```text
|
|
kernelwrite-free usable startup
|
|
+ proven stack/relocation/BSS/TLS closure
|
|
+ callable bounded observation primitives
|
|
+ two bound firmware sources
|
|
+ bounded transient output
|
|
+ normal/error/deadline exit without kill
|
|
+ complete cleanup and unambiguous status
|
|
+ bounded accepted observation effects
|
|
= target implementation may be reconsidered
|
|
```
|
|
|
|
Every term is required. A passing host protocol cannot compensate for a
|
|
missing exit ABI. A proven read algorithm cannot compensate for an absent
|
|
output channel. Two firmware strings cannot compensate for an unreviewed ABI
|
|
or stale execution binding.
|
|
|
|
## Decision
|
|
|
|
Closed for host design:
|
|
|
|
- startup graph classifications are explicit;
|
|
- the freestanding missing dependencies are explicit;
|
|
- D1 framing is fixed at 4096 bytes and fails closed;
|
|
- stale, duplicate, incomplete, corrupt, timed-out and conflicting records
|
|
are rejected; and
|
|
- every capability has an explicit blocker.
|
|
|
|
Not closed for target implementation:
|
|
|
|
- all 21 capabilities in the matrix.
|
|
|
|
The capability result contributes to
|
|
`BLOCKED_MULTIPLE_FOUNDATIONAL_CONTRACTS`.
|