mirror of
https://github.com/RetroPortingToolKit/psxrecomp
synced 2026-10-27 10:38:46 -04:00
Matthew Stanley
77d036bfb6
Make the repo approachable for outside contributors and an IDE integrator:
- New contributor docs:
- docs/EXECUTION_MODEL.md — semi-technical tour of the static / native-overlay
/ interpreter execution model and how coverage gaps get plugged.
- docs/ARCHITECTURE.md — component-level view (recompiler, runtime, LLE+HLE
BIOS, overlay backend static->gcc->tcc, renderers, oracle model).
- docs/BUILDING.md — accurate dependency table, per-platform prereqs, build
steps, and the submodule + local-junction framework-linking setup.
- CONTRIBUTING.md — distilled core rules, verification expectations, PR flow.
- Declutter root: move ~14 internal dev-logs into docs/internal/ (history
preserved via rename) with an index README; repoint CLAUDE.md references.
- README: correct build recipe, LLE+HLE + overlay-backend summary, links to the
new docs.
- code_provider.c: update the stale backend comment to the real static->gcc->tcc
resolution (dead SLJIT.md reference removed).
- config_schema.md: drop the obsolete "once Phase A2/A3 ships --config" note.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
290 lines
4.6 KiB
Markdown
290 lines
4.6 KiB
Markdown
This is NOT "start the runtime".
|
|
|
|
This is a **controlled proof of correctness**.
|
|
|
|
---
|
|
|
|
## Scope
|
|
|
|
### Input
|
|
- bios/SCPH1001.BIN (524288 bytes)
|
|
- Loaded at virtual address: 0xBFC00000
|
|
|
|
### Target region (STRICT)
|
|
Only recompile:
|
|
|
|
- Reset vector entry: 0xBFC00000
|
|
- Linear control flow until:
|
|
- First indirect jump (JR / JALR)
|
|
- OR first exception return (ERET)
|
|
- OR 4 KB of code max
|
|
|
|
WHICHEVER COMES FIRST.
|
|
|
|
---
|
|
|
|
## Required Outputs
|
|
|
|
### 1. Generated C file
|
|
- File: `generated/boot_slice.c`
|
|
- Must compile cleanly
|
|
- Must not be hand-edited
|
|
|
|
---
|
|
|
|
### 2. Function manifest (MANDATORY)
|
|
|
|
File: `generated/boot_slice_manifest.json`
|
|
|
|
Each entry MUST include:
|
|
|
|
```json
|
|
{
|
|
"address": "0xBFC00000",
|
|
"type": "function_entry",
|
|
"discovered_by": "reset_vector",
|
|
"instructions": 37,
|
|
"ends_at": "0xBFC00094",
|
|
"termination_reason": "jalr"
|
|
}
|
|
3. Unsupported instruction report
|
|
|
|
File: generated/unsupported_ops.json
|
|
|
|
If ANY instruction is not handled:
|
|
|
|
BUILD MUST FAIL
|
|
Entry must include:
|
|
{
|
|
"address": "0xBFC0002C",
|
|
"opcode": "COP0_MTC0",
|
|
"reason": "not implemented"
|
|
}
|
|
|
|
NO SILENT FALLBACKS.
|
|
|
|
Rules
|
|
NO interpreter
|
|
NO HLE
|
|
NO stubs
|
|
NO skipping instructions
|
|
NO "approximation"
|
|
NO partial instruction support
|
|
|
|
If something is unknown → FAIL LOUDLY
|
|
|
|
Acceptance Criteria
|
|
|
|
ALL must be true:
|
|
|
|
boot_slice.c compiles
|
|
manifest exists and is complete
|
|
unsupported_ops.json is EMPTY
|
|
Every instruction in the slice is accounted for
|
|
No TODO / FIXME in generated code
|
|
Explicit Non-Goals
|
|
No runtime
|
|
No MMIO
|
|
No GPU
|
|
No interrupts
|
|
No full BIOS walk
|
|
Failure Conditions
|
|
|
|
Immediate failure if:
|
|
|
|
Any instruction is skipped
|
|
Any fallback logic is introduced
|
|
Any "temporary" behavior appears
|
|
Manifest is incomplete or missing
|
|
Why This Exists
|
|
|
|
v3 failed because it jumped straight to "running things"
|
|
without proving the recompiler was correct.
|
|
|
|
This milestone ensures:
|
|
|
|
→ decoding is correct
|
|
→ control flow is correct
|
|
→ codegen is correct
|
|
|
|
before ANY runtime exists.
|
|
|
|
|
|
---
|
|
|
|
# 🧠 2. BOOT_RELOCATION_PLAN.md (THIS PREVENTS FUTURE FAILURE)
|
|
|
|
```md
|
|
# BOOT_RELOCATION_PLAN.md — BIOS ROM → RAM Strategy
|
|
|
|
## Problem
|
|
|
|
The PS1 BIOS copies code from ROM (0xBFCxxxxx)
|
|
into RAM (0x800xxxxx) and executes it.
|
|
|
|
Naive recompilation causes:
|
|
- duplicate functions
|
|
- broken dispatch tables
|
|
- incorrect control flow
|
|
|
|
---
|
|
|
|
## Goal
|
|
|
|
Represent ROM and RAM code as **the same logical function**
|
|
with multiple address aliases.
|
|
|
|
---
|
|
|
|
## Rules
|
|
|
|
### 1. No duplicate code generation
|
|
|
|
If ROM code at:
|
|
0xBFC01234
|
|
|
|
is copied to:
|
|
0x8001234
|
|
|
|
Then BOTH must map to:
|
|
|
|
```c
|
|
void func_001234(...)
|
|
|
|
NOT:
|
|
|
|
func_BFC01234()
|
|
func_8001234()
|
|
2. Address normalization
|
|
|
|
All functions must be identified by:
|
|
|
|
normalized_address = address & 0x1FFFFFFF
|
|
3. Manifest requirement
|
|
|
|
File: generated/address_aliases.json
|
|
|
|
{
|
|
"0xBFC01234": "0x80001234",
|
|
"0xBFC05678": "0x80005678"
|
|
}
|
|
|
|
Must be generated ONLY when proven.
|
|
|
|
4. Proof requirement
|
|
|
|
An alias may ONLY be created if:
|
|
|
|
A memcpy/move loop is identified in Ghidra
|
|
Source + destination ranges match
|
|
Verified in DuckStation memory trace
|
|
|
|
NO GUESSING.
|
|
|
|
5. Dispatch tables
|
|
|
|
When BIOS builds tables:
|
|
|
|
Entries must point to normalized functions
|
|
Not raw ROM or RAM addresses
|
|
Failure Modes (DO NOT ALLOW)
|
|
Duplicate function bodies
|
|
Diverging ROM vs RAM behavior
|
|
Table entries pointing to different implementations
|
|
"Seems equivalent" logic
|
|
Enforcement
|
|
|
|
If a function is emitted twice:
|
|
|
|
→ BUILD FAILS
|
|
|
|
Why This Matters
|
|
|
|
This is the core reason PSX recompilation fails.
|
|
|
|
If this is wrong:
|
|
|
|
→ EVERYTHING breaks later
|
|
→ bugs become untraceable
|
|
→ project becomes v3 again
|
|
|
|
|
|
---
|
|
|
|
# 🧾 3. PROOF_REQUIREMENTS.md (THIS FIXES CLAUDE'S BS)
|
|
|
|
```md
|
|
# PROOF_REQUIREMENTS.md — No More Guessing
|
|
|
|
## Rule
|
|
|
|
Any claim must produce a machine-verifiable artifact.
|
|
|
|
---
|
|
|
|
## Required Proof Types
|
|
|
|
### Function Discovery
|
|
|
|
Must output:
|
|
|
|
- address
|
|
- how discovered (linear / table / jump target)
|
|
- termination reason
|
|
|
|
---
|
|
|
|
### Indirect Calls
|
|
|
|
Must output:
|
|
|
|
- source instruction
|
|
- resolved target
|
|
- how resolved
|
|
|
|
---
|
|
|
|
### Table Builds
|
|
|
|
Must output:
|
|
|
|
- table location
|
|
- source data
|
|
- final entries
|
|
|
|
---
|
|
|
|
### Relocation
|
|
|
|
Must output:
|
|
|
|
- source ROM range
|
|
- destination RAM range
|
|
- proof (Ghidra + runtime)
|
|
|
|
---
|
|
|
|
## Forbidden
|
|
|
|
- "probably"
|
|
- "looks correct"
|
|
- "should work"
|
|
- "seems like"
|
|
- "matches expectation"
|
|
|
|
---
|
|
|
|
## Required Language
|
|
|
|
Every statement must be:
|
|
|
|
- proven
|
|
- or explicitly unknown
|
|
|
|
---
|
|
|
|
## Failure Condition
|
|
|
|
If ANY conclusion lacks proof artifact:
|
|
|
|
→ INVALID WORK |