mirror of https://github.com/RetroPortingToolKit/psxrecomp synced 2026-10-26 02:11:36 -04:00

Files

T

Matthew Stanley 7c40d33db3 Phase 1 complete: recompiler proven correct on SCPH1001.BIN

Phase 1a (boot slice): 30 instructions at 0xBFC00000, compiles clean.
Phase 1b (instruction coverage): 54 opcodes implemented in strict_translator,
  44,629 walker-reachable instructions covered, 0 missing.
Phase 1c (function discovery): 76 functions from 2 seeds, 2,988 instructions,
  199 call edges, 27 indirect jumps. All validated through StrictTranslator.
Phase 1d (indirect control flow): 27 sites classified — 21 A0/B0/C0 dispatch
  stubs, 4 computed calls, 2 computed tail calls. Ghidra cross-referenced
  with 0 disagreements.
Phase 1e (relocation): ROM-to-RAM copy at FUN_bfc00420 proven with both
  Ghidra (static) and DuckStation (runtime). 69 address aliases, 68/69
  function entries match byte-for-byte in RAM. Normalization rule documented.

Includes PRINCIPLES.md and DEBUG.md adapted from recomp-template.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

2026-04-11 21:26:04 -07:00

3.0 KiB

Raw Blame History

Address Normalization Rule — Phase 1e

Rule

A function's identity is its canonical physical address, computed in two steps:

Step 1: KSEG strip

physical = virtual_address & 0x1FFFFFFF

This removes the MIPS KSEG segment prefix. All four segments map to the same physical address space:

Segment	Virtual range	Physical range
KUSEG	0x00000000-0x7FFFFFFF	0x00000000-0x1FFFFFFF
KSEG0	0x80000000-0x9FFFFFFF	0x00000000-0x1FFFFFFF
KSEG1	0xA0000000-0xBFFFFFFF	0x00000000-0x1FFFFFFF
KSEG2	0xC0000000-0xFFFFFFFF	(memory-mapped I/O)

Step 2: ROM-to-RAM copy offset

If the physical address falls within the BIOS ROM copy source range, map it to the RAM destination:

if 0x1FC10000 <= physical <= 0x1FC18BEF:
    physical = physical - 0x1FC10000 + 0x00000500

This accounts for the single proven ROM-to-RAM copy performed by FUN_bfc00420 during BIOS init:

Property	Value
Source	ROM 0xBFC10000 (physical 0x1FC10000)
Dest	RAM 0xA0000500 (physical 0x00000500)
Length	0x8BF0 bytes (35,824 bytes)
Proof	generated/relocation_proofs/primary_copy/proof.json

Combined formula

normalize(addr):
    phys = addr & 0x1FFFFFFF
    if 0x1FC10000 <= phys <= 0x1FC18BEF:
        phys = phys - 0x1FC10000 + 0x00000500
    return phys

Examples

Input address	After KSEG strip	After ROM-to-RAM	Canonical
0xBFC10C74	0x1FC10C74	0x00001174	0x00001174
0x80001174	0x00001174	(not in ROM range)	0x00001174
0xA0001174	0x00001174	(not in ROM range)	0x00001174
0xBFC00420	0x1FC00420	(not in copy range)	0x1FC00420
0xBFC06EC4	0x1FC06EC4	(not in copy range)	0x1FC06EC4

Evidence

The copy parameters (source, destination, length) are all immediate constants in the BIOS code. No runtime computation is involved.
Ghidra decompilation confirms the loop structure and parameters.
69 Ghidra-known functions fall within the copy source range.
The normalization formula maps all 69 ROM-source functions to their RAM-destination equivalents, producing 69 alias pairs.
No alias was added without tracing back to the proof artifact at generated/relocation_proofs/primary_copy/proof.json.

Scope limitation

This rule covers only the single ROM-to-RAM copy identified in Phase 1e. If additional copies are discovered in later phases (e.g., from RAM-side code that runs after the initial copy), the rule must be extended with new proof artifacts.

The exception vector trampoline at 0x80000080 is installed by intra-RAM code at ROM 0xBFC109B0 (RAM 0x80000EB0) which copies 16 bytes from RAM 0x00000F0C to RAM 0x80000080. This is an intra-RAM copy (not ROM-to-RAM) and does not require a normalization entry because both addresses are already in RAM physical space.

3.0 KiB Raw Blame History