a2c9486b20
Dominance said a phase cannot end unless X. A port also needs "once X holds, it must end", and that is a must-reach set: nodes from which END_PHASE is unavoidable, as a least fixpoint where n qualifies when it has successors and ALL of them qualify. The conservatism is deliberate and is the honest answer: a loop never enters the set, because a poll loop reaches its exit only if the polled predicate eventually becomes true, which is a liveness property rather than a graph one. A dominating condition is a TRIGGER when the successor it takes on being satisfied lies in that set. Over all 28 stages: 732 dominating conditions, 234 triggers (31.97%). isl_report.py phase-guards now tags every line precond / TRIGGER. The split lands where it should. Stage 02's phase-1 objective exit is six preconditions -- player alive, TCN004 destroyed, t <= 210, ADT102/ADT107/ADT113 destroyed -- and exactly ONE trigger: hp_pct_test(ADN101, 0) != 1. Destroying ADN101 is what fires the phase. That is a sentence a port can implement. Per-exit distribution over 172 reachable exits: 89 have exactly one trigger, 42 have none, 41 have several. The 42 with none are not a failure -- they are the exits no branch fires; Stage 02's 0x006260 ends on read_freg(0) < 1200, a timeout, and time passing is not a property of the graph, so declining to call it a trigger is correct. Recorded as a heuristic rather than a rule: "the first trigger is the point of no return" holds for 33 of the 41 multi-trigger exits, with 8 counterexamples where a precondition appears after a trigger. The likely cause is that the listing is ordered by file offset, which is not execution order -- coroutines and jumps let a lower offset run later. Not asserted. calls, phase-ends and conditions all regenerate byte-identical; the two phase-guards artefacts change only by gaining the tags.
186 lines
8.0 KiB
Markdown
186 lines
8.0 KiB
Markdown
# ✅ 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.
|
||
|
||
## ✅ All 28 stages — [`../data/isl-phase-guards-all.txt`](../data/isl-phase-guards-all.txt)
|
||
|
||
`isl_report.py <dir> phase-guards` runs the whole disc. **177 phase exits**, of
|
||
which only **5 (2.8 %)** are reachable from no static entry.
|
||
|
||
| | |
|
||
|---|---|
|
||
| CFG reach, best | Stage 25 — 95.8 % |
|
||
| CFG reach, worst | Stage 26 — 69.5 % |
|
||
| median conditions per exit | ~4 |
|
||
|
||
### ✅ An independent cross-check, 6 / 6
|
||
|
||
The six **tutorial** stages (S18–S23) each have exactly **one** exit with exactly
|
||
**one** dominating condition, and it is the same one every time:
|
||
|
||
```
|
||
END_PHASE <- builtin104() != 1
|
||
```
|
||
|
||
[`isl-builtins.md`](isl-builtins.md) reached built-in **104** from a completely
|
||
different direction — call-site usage — and recorded it as *"S18–S23 only …
|
||
followed by `wait_s` 39/39, preceded by `end_coroutine` 37/39 … a textbook poll
|
||
loop"*. Usage said it was the tutorial's polled test; dominance says it is the
|
||
tutorial's clear condition. **Two unrelated methods, six for six.** That the
|
||
1.0-condition uniformity turned out to be real rather than a degenerate result is
|
||
the check worth having run.
|
||
|
||
### Stage 16, the corpus outlier, also reads
|
||
|
||
`mission-script-ssb.md` flags S16 as the stage whose script may be compiled C++.
|
||
Its exits resolve anyway, and sensibly:
|
||
|
||
```
|
||
ph1 END_PHASE read_freg(0) < 600 ; player_gauge0_test(0) != 1 ; player_gauge1_test(0) != 1
|
||
ph1 FORCE_END_PHASE builtin141(TCN001, 1, 2, 0, 0, 0, 1000, 5, 100, 100) != 1 ;
|
||
builtin141(TCN001, 1, 2, 0, -4000, 0, 1000, 5, 100, 100) != 1 ; global[0] != 1
|
||
```
|
||
|
||
The two `builtin141` calls differ in one argument (`0` vs `-4000`), which is the
|
||
shape of a position or zone test — but it is unread, so it is not named.
|
||
|
||
## 🟡 Not settled
|
||
* ~~**Dominance gives necessary, not sufficient, conditions.**~~ ✅ **Done** — see
|
||
*Necessary vs sufficient* below.
|
||
* 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.
|
||
|
||
|
||
## ✅ Necessary vs sufficient — the exits now name their TRIGGER
|
||
|
||
Dominance says the exit *cannot* happen unless a condition holds. A port also
|
||
needs the other half: once it holds, does the exit *have* to happen?
|
||
|
||
That is a **must-reach** set — nodes from which an `END_PHASE` is unavoidable —
|
||
computed as a least fixpoint: `n` qualifies when it has successors and **all** of
|
||
them qualify. Deliberately conservative: a loop never enters the set, which is
|
||
the honest answer, because a poll loop reaches its exit only if the polled
|
||
predicate eventually becomes true, and that is a **liveness** property, not a
|
||
graph one.
|
||
|
||
A dominating condition is then a **TRIGGER** when the successor it branches to on
|
||
being satisfied lies in that set.
|
||
|
||
**Over all 28 stages: 732 dominating conditions, 234 of them triggers (31.97 %).**
|
||
|
||
And the split lands exactly where it should. Stage 02's phase-1 objective exit:
|
||
|
||
```
|
||
precond unit_hp_pct(TCN001, Character_Player_Test) != 0
|
||
precond hp_pct_test(TCN004, 0) != 1
|
||
precond read_freg(0) <= 210
|
||
precond hp_pct_test(ADT102, 0) != 1
|
||
precond hp_pct_test(ADT107, 0) != 1
|
||
precond hp_pct_test(ADT113, 0) != 1
|
||
TRIGGER hp_pct_test(ADN101, 0) != 1
|
||
```
|
||
|
||
Six preconditions and **one thing that actually fires it** — destroying `ADN101`.
|
||
That is a sentence a port can implement.
|
||
|
||
### Triggers per exit, 172 reachable exits
|
||
|
||
| triggers | exits |
|
||
|---|---|
|
||
| **0** | 42 |
|
||
| **1** | **89** |
|
||
| 2–4 | 35 |
|
||
| 5–13 | 6 |
|
||
|
||
**The 42 with none are not a failure** — they are the exits no branch fires. Stage
|
||
02's `0x006260` is one: its last necessary condition is `read_freg(0) < 1200`, a
|
||
timeout. Time passing is not a property of the graph, so a graph analysis
|
||
correctly declines to call it a trigger.
|
||
|
||
### 🟡 "The first trigger is the point of no return" — 33 / 41, not a rule
|
||
|
||
Where an exit has several triggers, the natural reading is that they form a
|
||
forced tail and the **first** is where the outcome is decided. Tested on the 41
|
||
multi-trigger exits: **33 hold, 8 do not** — a precondition appears after a
|
||
trigger.
|
||
|
||
The likely cause is that the listing is ordered by **file offset**, which is not
|
||
execution order: coroutines and jumps let a lower offset run later. So the
|
||
reading is a useful heuristic and **not** a property, and it is recorded that way
|
||
rather than asserted. |