202 lines
8.9 KiB
Markdown
202 lines
8.9 KiB
Markdown
# Phase 0.9A installation transaction design
|
|
|
|
Status: **DESIGN_ONLY — NOT INSTALLATION READY**.
|
|
|
|
This document defines a future evidence and state contract. It contains no
|
|
PS5 path, install command, device write implementation, lifecycle transition,
|
|
autoload, retry, graphics code or RetroArch transition. All approval values
|
|
remain false.
|
|
|
|
## Anti-brick invariants
|
|
|
|
| ID | Mandatory invariant |
|
|
|---|---|
|
|
| AB-001 | Never write without exact stable path, mount ID, object ID, type, size and pre-image SHA-256. |
|
|
| AB-002 | A stock hash remains `reference_only` until observed on one stable on-device object. |
|
|
| AB-003 | Hash match without object identity is insufficient. |
|
|
| AB-004 | Object identity without hash match is insufficient. |
|
|
| AB-005 | Before staging, a separate backup survives close, reopen, identity, size and hash verification. |
|
|
| AB-006 | Backup and recovery do not depend on the candidate or replaced component. |
|
|
| AB-007 | Never overwrite a live executable in place. |
|
|
| AB-008 | Stage under a separate inactive identity. |
|
|
| AB-009 | Reopen and hash the candidate before activation; bytes equal the approved artifact. |
|
|
| AB-010 | No autoload, retry, service restart or boot starts the candidate. |
|
|
| AB-011 | Switch only with a separately proven transactional or atomic primitive. |
|
|
| AB-012 | Unproven atomicity or durability blocks installation. |
|
|
| AB-013 | Verify the new live identity; execution is a later approval. |
|
|
| AB-014 | At most one manual execution and zero automatic retries. |
|
|
| AB-015 | Failed post-switch verification enters `ROLLBACK_REQUIRED`, never execution. |
|
|
| AB-016 | Rollback uses only the verified backup and exact target mapping. |
|
|
| AB-017 | After rollback, re-establish size, hash, object identity and metadata. |
|
|
| AB-018 | elfldr and Payload Manager are never replaced in one uninterrupted transaction. |
|
|
| AB-019 | The lifecycle probe is not an installation candidate. |
|
|
| AB-020 | No later phase begins without separate human permission. |
|
|
|
|
## State machine
|
|
|
|
The complete ordered state set is:
|
|
|
|
```text
|
|
OFFLINE_ONLY
|
|
-> OBSERVATION_NOT_AUTHORIZED
|
|
-> OBSERVATION_AUTHORIZED
|
|
-> DEVICE_IDENTITY_OBSERVED
|
|
-> LIVE_OBJECTS_VERIFIED
|
|
-> BACKUP_NOT_PRESENT
|
|
-> BACKUP_CREATION_NOT_AUTHORIZED
|
|
-> BACKUP_CREATION_AUTHORIZED
|
|
-> BACKUP_CREATED
|
|
-> BACKUP_REOPENED_AND_VERIFIED
|
|
-> RECOVERY_PATH_VERIFIED
|
|
-> CANDIDATE_NOT_AUTHORIZED
|
|
-> CANDIDATE_APPROVED_OFFLINE
|
|
-> STAGING_NOT_AUTHORIZED
|
|
-> STAGING_AUTHORIZED
|
|
-> CANDIDATE_STAGED
|
|
-> CANDIDATE_REOPENED_AND_VERIFIED
|
|
-> TARGET_NOT_QUIESCENT
|
|
-> TARGET_QUIESCENT
|
|
-> SWITCH_NOT_AUTHORIZED
|
|
-> SWITCH_AUTHORIZED
|
|
-> SWITCH_IN_PROGRESS
|
|
-> POST_SWITCH_VERIFY
|
|
-> MANUAL_EXECUTION_NOT_AUTHORIZED
|
|
-> MANUAL_EXECUTION_AUTHORIZED
|
|
-> ONE_SHOT_EXECUTION
|
|
-> ACCEPTED
|
|
```
|
|
|
|
The only recovery branch is:
|
|
|
|
```text
|
|
POST_SWITCH_VERIFY
|
|
-> ROLLBACK_REQUIRED
|
|
-> ROLLBACK_AUTHORIZED
|
|
-> ROLLBACK_IN_PROGRESS
|
|
-> ROLLBACK_VERIFIED
|
|
```
|
|
|
|
Any error, mismatch, timeout, unknown or object change goes to `BLOCKED`.
|
|
No state automatically crosses an authorization state. There is no automatic
|
|
retry, autoload, lifecycle, graphics or RetroArch transition. A general READY
|
|
value cannot bypass a specific gate.
|
|
|
|
The current real state is `OFFLINE_ONLY`; the repository templates do not move
|
|
it.
|
|
|
|
## Approval separation
|
|
|
|
Observation, backup creation, staging, switch, one-shot execution and rollback
|
|
each require a different active-task authorization. An authorization must bind
|
|
one component, device, exact firmware, live pre-image, candidate hash and
|
|
size, action count, runtime, expiration and stop conditions. Reuse for another
|
|
hash, action or component fails.
|
|
|
|
Phase 0.9A grants none of these authorizations. The simulator uses explicitly
|
|
labelled synthetic authorization objects only to test state-machine logic.
|
|
Those objects always report `installation_authorized=false` and
|
|
`execution_authorized=false`.
|
|
|
|
## Component-separated models
|
|
|
|
### Hardened elfldr
|
|
|
|
- stock reference: 397000 bytes,
|
|
`092d16ee0ede0c494947efd38d1a17bbd7cc4b022d3858ea898833c188c703e8`;
|
|
- candidate reference: 397000 bytes,
|
|
`63e810982471eb40cae3a20aa9df9a0a02892f420e429874fae4e99aa400b561`;
|
|
- live path, mount, object ID and current hash: `UNPROVEN`;
|
|
- separate on-device backup: `UNPROVEN`;
|
|
- process, service, listener, autoload and quiescence: `UNPROVEN`;
|
|
- target mapping, recovery independence and switch primitive: `UNPROVEN`;
|
|
- approval, staging, switch, execution, acceptance and rollback: not
|
|
authorized or performed.
|
|
|
|
### Controlled Payload Manager
|
|
|
|
- stock reference: 2050320 bytes,
|
|
`518740adbacccb9094fadb07dd424c53ee290f38306449ccc9d6957fdf813c0b`;
|
|
- candidate reference: 99560 bytes,
|
|
`8fecf8241a46246eddbd21e8bb4d875f5d76f1f4f4c6a11384df1f131aa5e5b1`;
|
|
- live path, mount, object ID and current hash: `UNPROVEN`;
|
|
- byte-exact, separate, reopened on-device backup: **HARD_BLOCKER**;
|
|
- process, service, listener, autoload and quiescence: `UNPROVEN`;
|
|
- target mapping, recovery independence and switch primitive: `UNPROVEN`;
|
|
- approval, staging, switch, execution, acceptance and rollback: not
|
|
authorized or performed.
|
|
|
|
There is no “install all” operation and no shared approval. Component B may be
|
|
considered only after component A is separately accepted or fully rolled back,
|
|
but Phase 0.9A does not infer which component is A. Order requires proven
|
|
dependency and recovery evidence. The lifecycle probe belongs to neither
|
|
model.
|
|
|
|
## Switch contract
|
|
|
|
Design preference, without assuming platform support:
|
|
|
|
1. side-by-side or dual-slot activation without deleting stock;
|
|
2. proven atomic exchange;
|
|
3. proven transactional snapshot;
|
|
4. another method only after separate evidence.
|
|
|
|
An in-place copy-overwrite is always forbidden. The sequence `rename live ->
|
|
backup; rename candidate -> live` is forbidden while a power-loss interval can
|
|
leave the live name absent.
|
|
|
|
Before a future switch, evidence must establish:
|
|
|
|
- filesystem type, mount identity and read/write state;
|
|
- atomic rename or exchange behavior and replacement semantics;
|
|
- file-flush and directory-flush durability;
|
|
- interruption and power-loss behavior;
|
|
- no-follow behavior and stable open-object identity;
|
|
- ownership, mode and metadata preservation;
|
|
- capacity, metadata reserve and maximum file size;
|
|
- behavior while the target executable is open.
|
|
|
|
None is proven for the PS5 in this phase.
|
|
|
|
**BLOCKER: NO PROVEN POWER-LOSS-SAFE SWITCH.**
|
|
|
|
## Power-loss boundary table
|
|
|
|
All results are `UNPROVEN` for PS5. The host simulator can prove only its own
|
|
virtual atomic primitive.
|
|
|
|
| # | Boundary | Possible state | Live visibility | Backup | Auto-start | Recovery | Result |
|
|
|---:|---|---|---|---|---:|---|---|
|
|
| 1 | before backup write | old live only | old | absent | no | no mutation yet | UNPROVEN |
|
|
| 2 | during backup write | old plus partial backup | old | invalid partial | no | old must remain | UNPROVEN |
|
|
| 3 | after backup write before flush | volatile backup | old | not durable | no | old must remain | UNPROVEN |
|
|
| 4 | after flush before reopen/hash | unverified backup | old | not reverified | no | old must remain | UNPROVEN |
|
|
| 5 | during candidate staging | partial candidate | old | verified if contract holds | no | independent | UNPROVEN |
|
|
| 6 | after staging before verification | unverified candidate | old | verified if contract holds | no | independent | UNPROVEN |
|
|
| 7 | immediately before switch | three verified logical objects | old | verified | no | independent | UNPROVEN |
|
|
| 8 | during switch | must be complete old or complete new | unknown | must remain verified | no | independent | UNPROVEN |
|
|
| 9 | immediately after switch | namespace/durability uncertain | unknown | must remain verified | no | independent | UNPROVEN |
|
|
| 10 | after switch before live hash | nominal new live unverified | unverified | verified | no | independent | UNPROVEN |
|
|
| 11 | after live hash before execution | nominal verified new | new | verified | no | independent | UNPROVEN |
|
|
| 12 | during first manual execution | new plus backup | new | verified | no automatic start | must work without new component | UNPROVEN |
|
|
| 13 | during rollback | must be complete new or complete old | unknown | must remain verified | no | independent | UNPROVEN |
|
|
| 14 | after rollback before verification | nominal restored old | unverified old | verified | no | independent | UNPROVEN |
|
|
|
|
Because at least one boundary is `UNPROVEN`, the model is not
|
|
installation-suitable. Here all fourteen are `UNPROVEN`.
|
|
|
|
## Host simulator
|
|
|
|
`tools/simulate_phase09_transaction.py` models logical objects, identities,
|
|
hashes, mounts, approvals, transitions, failures and all fourteen power-loss
|
|
boundaries in memory. It has no device path, network operation, cross-compiler
|
|
call, target artifact open, production installer or output-file option.
|
|
|
|
The default scenario stops at
|
|
`NO_PROVEN_POWER_LOSS_SAFE_SWITCH`. A special in-memory primitive can be
|
|
treated as atomic for fault-testing, but every report marks it
|
|
`host_simulation_only=true` and `hardware_evidence=false`. Even that synthetic
|
|
happy path stops at `MANUAL_EXECUTION_NOT_AUTHORIZED`.
|
|
|
|
The machine-readable contract is
|
|
`manifests/runtime/phase-0.9-anti-brick-design.json`.
|