LanglibPhase inversion for semantic protocol steps #
Every declarative action fixes the replicated phase of its old row. On a nonempty row
the phase is unique, so one ProtocolStep can be reduced to exactly the actions enabled
at the current control phase.
def
CertifiedRowSystem.Complement.ActionsAtPhase
{I : Type u_1}
{A : Type u_2}
{Q : Type u_3}
{F : Type u_4}
[Fintype A]
[Nonempty A]
[DecidableEq A]
(D : CertifiedRowSystem I A Unit Q F)
(phase : ProtocolPhase)
(old new : ProtocolRow A)
:
Actions enabled at one protocol phase.
Equations
- One or more equations did not get rendered due to their size.
- CertifiedRowSystem.Complement.ActionsAtPhase D CertifiedRowSystem.Complement.ProtocolPhase.input old new = CertifiedRowSystem.Complement.IsBoot old new
- CertifiedRowSystem.Complement.ActionsAtPhase D CertifiedRowSystem.Complement.ProtocolPhase.roundStart old new = CertifiedRowSystem.Complement.BeginRoundSpec old new
- CertifiedRowSystem.Complement.ActionsAtPhase D CertifiedRowSystem.Complement.ProtocolPhase.finishWitness old new = False
- CertifiedRowSystem.Complement.ActionsAtPhase D CertifiedRowSystem.Complement.ProtocolPhase.finishOuter old new = CertifiedRowSystem.Complement.FinishOuterSpec old new
- CertifiedRowSystem.Complement.ActionsAtPhase D CertifiedRowSystem.Complement.ProtocolPhase.finishRound old new = CertifiedRowSystem.Complement.FinishRoundSpec old new
- CertifiedRowSystem.Complement.ActionsAtPhase D CertifiedRowSystem.Complement.ProtocolPhase.finalWitness old new = False
- CertifiedRowSystem.Complement.ActionsAtPhase D CertifiedRowSystem.Complement.ProtocolPhase.finalFinish old new = CertifiedRowSystem.Complement.FinalFinishSpec old new
- CertifiedRowSystem.Complement.ActionsAtPhase D CertifiedRowSystem.Complement.ProtocolPhase.accept old new = False
Instances For
theorem
CertifiedRowSystem.Complement.protocolStep_action_of_phase
{I : Type u_1}
{A : Type u_2}
{Q : Type u_3}
{F : Type u_4}
[Fintype A]
[Nonempty A]
[DecidableEq A]
(D : CertifiedRowSystem I A Unit Q F)
{phase : ProtocolPhase}
{old new : ProtocolRow A}
(hphase : HasPhase phase old)
(hstep : ProtocolStep D old new)
:
ActionsAtPhase D phase old new
A semantic transition out of a uniformly phased nonempty row uses exactly an action enabled at that phase.