07 - Guard Quality Review

Verdict

CHECK_G_GUARD_QUALITY_FAIL_NEEDS_T1_FIX

The general anti-false-green rules are sound, but G-NOLEGACY is not phase-correct:

• PKG-D runs G-NOLEGACY while every legacy executable is still PUBLIC-executable.
• PKG-F requires G-NOLEGACY green as a precondition, although PKG-F is the step that revokes EXECUTE and makes its ACL clause green.
• S15 correctly lists G-NOLEGACY as proof after the step, contradicting the PKG-F precondition.

This is a deadlock or invites an implementation to weaken/skip the guard.

Required T1 fix: split the guard into phase-specific contracts without adding readiness gates, for example:

• pre-cutover structural closure/classification proof;
• in-transaction precondition proof;
• post-cutover effective-executability proof.

Each phase must have explicit expected state, non-vacuity, exact inputs, and package mapping. G-PGNATIVE must also reject the current name-pattern binding authority.