re: the sufficient side -- each phase exit now names the condition that FIRES it
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.
This commit is contained in:
@@ -119,10 +119,68 @@ 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.** 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.
|
||||
* ~~**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.
|
||||
Reference in New Issue
Block a user