fabi/Syplheed-Reborn
Archived
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

re: the per-phase clear conditions, by dominance over the ISL CFG

Browse Source 
Closes the backlog's "which condition guards each END_PHASE".  With the CFG from the
previous commit this is a graph query, not new machinery.

The obvious query is WRONG for this language, and I implemented it first: "one
successor reaches END_PHASE and the other does not" finds 1/62/1 guards across Stage
02's three phases, and the 1s are both the same read_freg(0) < 1200 timeout -- every
objective test missed.  The cause is the dominant idiom: a POLL LOOP's loop-back
branch also reaches the exit, one iteration later, so neither successor discriminates.
The asymmetric 1/62/1 is what exposed it; a uniform number would have read as
plausible.

Dominance has no such blind spot: a condition dominates an exit when every path from
an entry passes through it, so it is NECESSARY for the phase to end that way, and a
poll loop's test dominates its own exit by construction.  Iterative dominators
converge in 3 passes over 15670/18739 instructions (83.6%).

Result for Stage 02 -- every exit in all three phases is dominated by
unit_hp_pct(TCN001, Character_Player_Test) != 0, the player's ship being alive, which
falls out rather than being assumed.  Beyond that, phase 1's objective exit requires
hp_pct_test on ADT102, ADT107 and ADT113; phase 3's requires ADT301 and ADT302;
read_freg(0) gates at 210 / 300 and times out at 1200; random(3) and random(5)
dominate only the exits that pick one of several closing lines.

Two of the 15 exits are reachable from NO static entry, both FORCE_END_PHASE.  That
agrees with the independently measured 389 unreachable routines: they are started from
the trigger queue at phase+272, by data rather than code.

Practical note recorded: the first dominator run was OOM-killed -- 6743 nodes each
holding a Python set of up to 6743 elements.  Integer bitmasks run in seconds.

Not settled, and said so: dominance gives necessary, not sufficient, conditions; only
Stage 02's artefact is committed; one listed condition is still an unresolved
<unknown>; read_freg's units are inferred from the gate values, not read.

calls, phase-ends and conditions all regenerate byte-identical.
This commit is contained in:
Sylpheed RE agent
2026-08-27 06:12:41 +00:00
parent 5ea9e38b35
commit 4f95b98813
6 changed files with 387 additions and 3 deletions
Download Patch File Download Diff File Expand all files Collapse all files

88
docs/re/structures/isl-phase-guards.md Normal file
View File

@@ -0,0 +1,88 @@
# ✅ What each phase exit requires — the per-phase clear conditions
This is what the ISL thread was for. `BACKLOG.md` framed it as *"which condition
guards each `END_PHASE`"*, and with the CFG from
[isl-conditions](isl-conditions.md) it is a graph query rather than new
machinery. Artefact:
[`../data/isl-stage02-phase-guards.txt`](../data/isl-stage02-phase-guards.txt),
generator `isl_report.py phase-guards`.
## 🔴 The obvious query is WRONG here — tried first, and it fails quietly
The natural definition of a guard is *one successor reaches `END_PHASE` and the
other does not*. I implemented that first. It reports, for Stage 02:
| phase | 1 | 2 | 3 |
|---|---|---|---|
| "guards" found | **1** | 62 | **1** |
and the single condition it finds in phases 1 and 3 is the same one —
`read_freg(0) < 1200`, a timeout. Every objective test is missed.
**The reason is the shape of the language.** The dominant idiom here is a **poll
loop**: `if still-alive: jump back`. The loop-back branch reaches the exit too —
one iteration later — so *neither* successor discriminates and the clear
condition is invisible to a reachability test. The asymmetric 1 / 62 / 1 is what
exposed it; a uniform number would have looked plausible and been wrong.
## ✅ Dominance has no such blind spot
A condition **dominates** an exit when *every* path from an entry to that
`END_PHASE` passes through it — so it is a **necessary** condition for the phase
to end that way. A poll loop's test dominates its own exit, so the idiom that
defeats reachability is handled by construction.
Iterative dominators over the CFG, converging in **3 passes**, reaching
**15 670 of 18 739** instructions (83.6 %).
> Practical note: the first run was **OOM-killed**. 6 743 reachable nodes each
> carrying a Python `set` of up to 6 743 elements is ~45 M objects. Integer
> bitmasks fit in seconds.
## ✅ What Stage 02 actually requires
**Every exit in all three phases** is dominated by
```
unit_hp_pct(TCN001, Character_Player_Test) != 0
```
— the player's own ship being alive. That is the universal precondition, and it
falls out of the analysis rather than being assumed.
Then, per phase:
| phase | exit at | necessary conditions beyond the player being alive |
|---|---|---|
| 1 | `0x0051E4` | `random(3) == 0` |
| 1 | `0x005828` | `hp_pct_test(TCN004, 0) != 1`, `random(5) == 0` |
| 1 | `0x006010` | `hp_pct_test(TCN004…)`, `read_freg(0) <= 210`, **`hp_pct_test(ADT102, 0) != 1`**, **`ADT107`**, **`ADT113`** |
| 1 | `0x006260` | `hp_pct_test(TCN004…)`, `read_freg(0) <= 210`, `read_freg(0) < 1200` |
| 2 | `0x019934` | `hp_pct_test(TCT206, 0) != 1` |
| 2 | `0x01AC44` | `TCT206`, `builtin7(TCT206, 1, Route_TCT206_p2S, …, 500) == 1`, `global[4] == 0`, `global[4] != 1` |
| 2 | `0x0249F0` | `hp_pct_test(ADN202, 0) != 1`, `unit_state(TCT206) != 1` |
| 3 | `0x02C1E0` | `hp_pct_test(TCN004…)`, `global[112] < 4` |
| 3 | `0x02CF74` | + `read_freg(0) <= 300`, **`hp_pct_test(ADT301, 0) != 1`**, **`ADT302`** |
| 3 | `0x02D1DC` | + `read_freg(0) < 1200` |
The `hp_pct_test(ADTnnn, 0) != 1` chains are the objective kills; `read_freg(0)`
is a phase clock (`<= 210`, `<= 300` gates, `< 1200` the timeout); `random(3)`
and `random(5)` dominate only the exits that pick one of several closing lines.
## 🟡 Two exits are unreachable, and that is informative
`0x01482C` and `0x034A10` — both `FORCE_END_PHASE` — are reachable from **no
static entry**. That agrees with the independently measured 389 unreachable
routines: they are started from the **trigger queue at `phase+272`**, by data
rather than code. So a purely static reading cannot say what forces those exits.
## 🟡 Not settled
* **Only Stage 02 is committed.** The other 27 generate from the same command.
* **Dominance gives necessary, not sufficient, conditions.** A dominator set does
not say the phase ends *when* they all hold, only that it cannot end unless
they do. Turning these into a simulator's exit test needs the sufficient side.
* One condition in the phase-2 list still prints `<unknown> <= 240` — one of the
402 sites the CFG cannot resolve.
* `builtin7` and `read_freg`'s units are unread; `read_freg(0)` behaves like
seconds against the 210 / 300 / 1200 gates but that is not established.