feat(coq): L-S43 PowerStateSafety — Wave-11b power-gate FSM off-active overlap proof

[gHashTag]

Closes #799

Summary

Formal Coq proof that the Wave-11b power-gate FSM never enters the illegal "off-active overlap" state where pwr_en=0 AND clk_en=1 simultaneously — a condition that would crash silicon.

Deliverables

docs/phd/theorems/igla/PowerStateSafety.v

• Inductive pstate: OFF | WAKE | ACTIVE | SLEEP_REQ
• Definition pwr_en: power enable signal (false only in OFF)
• Definition clk_en: clock enable signal (true only in ACTIVE)
• Definition step: deterministic FSM transition function
• Fixpoint run: trace all visited states over an input sequence

Theorem no_off_active_overlap:

forall s : pstate, pwr_en s = false -> clk_en s = false

Proved by destruct s + reflexivity/discriminate.

Lemma reachable_states_safe:

forall (init : pstate) (seq : list input) (s : pstate),
  In s (run init seq) -> pwr_en s = false -> clk_en s = false

Proved by structural induction over the input sequence.

All proofs end Qed. — zero Admitted.

docs/phd/artifacts/coq_citation_map.json

New file mapping:

• PowerStateSafety.no_off_active_overlap → power_gate_fsm.v
• PowerStateSafety.reachable_states_safe → power_gate_fsm.v

Verification

coqc 8.20.1 docs/phd/theorems/igla/PowerStateSafety.v
exit 0 ✓

Anchor

φ² + φ⁻² = 3

License

Apache-2.0

Author

Dmitrii Vasilev admin@t27.ai