Langlib

Langlib.Automata.LinearBounded.CertifiedRowSystem.Complement.ProtocolStepCorrectness

Correctness interface for integrated complement-protocol steps #

The complete protocol verifier is a tagged sum of small synchronous scanners. This module hides that dispatch: a row transition whose certificate repeats one action is reduced to the corresponding scanner, then to its declarative list-level specification.

source
def CertifiedRowSystem.Complement.ProtocolActionAccepts {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] [Fintype Q] [Fintype F] (D : CertifiedRowSystem I A Unit Q F) (action : ProtocolAction) (old new : ProtocolRow A) :
Prop

Acceptance of one fixed, replicated protocol action by the integrated row verifier.

Equations
  • One or more equations did not get rendered due to their size.
Instances For

    Arbitrary-certificate normalization #

    source
    def CertifiedRowSystem.Complement.ProtocolVerifier.selectedAction {Q : Type u_3} {F : Type u_4} :
    ProtocolVerifier Q F → Option ProtocolAction

    The action selected by a live tagged verifier state.

    Equations
    Instances For
      source
      def CertifiedRowSystem.Complement.ProtocolVerifier.Live {Q : Type u_3} {F : Type u_4} :
      ProtocolVerifier Q F → Prop

      Dead verifier states are precisely the three absorbing rejecting states.

      Equations
      Instances For
        source
        theorem CertifiedRowSystem.Complement.evalProtocol_actions_eq_replicate {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] [Fintype Q] [Fintype F] (D : CertifiedRowSystem I A Unit Q F) (q out : ProtocolVerifier Q F) (expected : ProtocolAction) (old new : ProtocolRow A) (actions : List ProtocolAction) (hselected : q.selectedAction = some expected) (heval : (deterministicComplementSystem D).evalStep q old new actions = some out) (hdone : protocolStepDone D out = true) :
        actions = List.replicate (List.length old) expected

        Once an action has been selected, every certificate cell of an accepting run must repeat it.

        source
        theorem CertifiedRowSystem.Complement.deterministicComplementSystem_rowStep_iff_exists_action {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] [Fintype Q] [Fintype F] (D : CertifiedRowSystem I A Unit Q F) (old new : ProtocolRow A) :
        (deterministicComplementSystem D).RowStep old new ↔ ∃ (action : ProtocolAction), ProtocolActionAccepts D action old new

        Every accepting arbitrary certificate is equivalent to repeating its first action. This is the normalization bridge between CertifiedRowSystem.RowStep and the per-action correctness interface.

        Dispatch simulations #

        source
        theorem CertifiedRowSystem.Complement.evalProtocol_from_boot {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] [Fintype Q] [Fintype F] (D : CertifiedRowSystem I A Unit Q F) (q : BootVerifier) (old new : ProtocolRow A) (actions : List ProtocolAction) :
        (deterministicComplementSystem D).evalStep (ProtocolVerifier.boot q) old new actions = Option.map ProtocolVerifier.boot (evalBoot q old new actions)

        Once the boot scanner has been selected, the integrated verifier is its tagged map.

        source
        theorem CertifiedRowSystem.Complement.evalProtocol_from_enumeration {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] [Fintype Q] [Fintype F] (D : CertifiedRowSystem I A Unit Q F) (q : EnumerationVerifier) (old new : ProtocolRow A) (actions : List ProtocolAction) :
        (deterministicComplementSystem D).evalStep (ProtocolVerifier.enumeration q) old new actions = Option.map ProtocolVerifier.enumeration (evalEnumeration q old new actions)

        Once an enumeration scanner has been selected, the integrated verifier is its tagged map.

        source
        theorem CertifiedRowSystem.Complement.evalProtocol_from_startPath {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] [Fintype Q] [Fintype F] (D : CertifiedRowSystem I A Unit Q F) (finalScan : Bool) (q : StartPathVerifier) (old new : ProtocolRow A) :
        (deterministicComplementSystem D).evalStep (ProtocolVerifier.startPath finalScan q) old new (List.replicate (List.length old) (if finalScan = true then ProtocolAction.finalStartPath else ProtocolAction.startPath)) = Option.map (ProtocolVerifier.startPath finalScan) (evalStartPath (if finalScan = true then ProtocolPhase.finalChoose else ProtocolPhase.chooseInner) (if finalScan = true then ProtocolPhase.finalPath else ProtocolPhase.path) q old new)

        A selected path-initialization scanner remains in its tagged summand when every remaining certificate cell repeats its action.

        source
        theorem CertifiedRowSystem.Complement.evalProtocol_from_pathStep {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] [Fintype Q] [Fintype F] (D : CertifiedRowSystem I A Unit Q F) (finalScan : Bool) (q : PathStepVerifier Q) (old new : ProtocolRow A) :
        (deterministicComplementSystem D).evalStep (ProtocolVerifier.pathStep finalScan q) old new (List.replicate (List.length old) (if finalScan = true then ProtocolAction.finalPathStep else ProtocolAction.pathStep)) = Option.map (ProtocolVerifier.pathStep finalScan) (evalPathStep D (if finalScan = true then ProtocolPhase.finalPath else ProtocolPhase.path) q old new)

        A selected path-extension scanner remains in its tagged summand.

        source
        theorem CertifiedRowSystem.Complement.evalProtocol_from_finishWitness {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] [Fintype Q] [Fintype F] (D : CertifiedRowSystem I A Unit Q F) (q : FinishWitnessVerifier Q) (old new : ProtocolRow A) :
        (deterministicComplementSystem D).evalStep (ProtocolVerifier.finishWitness q) old new (List.replicate (List.length old) ProtocolAction.finishWitness) = Option.map ProtocolVerifier.finishWitness (evalFinishWitness D q old new)

        A selected counting-round witness-completion scanner remains tagged.

        source
        theorem CertifiedRowSystem.Complement.evalProtocol_from_finalWitness {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] [Fintype Q] [Fintype F] (D : CertifiedRowSystem I A Unit Q F) (q : FinalWitnessVerifier F) (old new : ProtocolRow A) :
        (deterministicComplementSystem D).evalStep (ProtocolVerifier.finalWitness q) old new (List.replicate (List.length old) ProtocolAction.finalFinishWitness) = Option.map ProtocolVerifier.finalWitness (evalFinalWitness D q old new)

        A selected final witness-completion scanner remains tagged.

        Fixed path-action correctness #

        source
        theorem CertifiedRowSystem.Complement.evalProtocolAction_boot_iff {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] [Fintype Q] [Fintype F] (D : CertifiedRowSystem I A Unit Q F) (old new : ProtocolRow A) :
        ProtocolActionAccepts D ProtocolAction.boot old new ↔ IsBoot old new

        Integrated correctness of the initialization action.

        source
        theorem CertifiedRowSystem.Complement.evalProtocolAction_beginFinal_iff {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] [Fintype Q] [Fintype F] (D : CertifiedRowSystem I A Unit Q F) (old new : ProtocolRow A) :
        ProtocolActionAccepts D ProtocolAction.beginFinal old new ↔ False

        beginFinal is intentionally not a primitive transition: the plateau branch of finishRound enters the final scan.

        source
        theorem CertifiedRowSystem.Complement.evalProtocolAction_beginRound_iff {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] [Fintype Q] [Fintype F] (D : CertifiedRowSystem I A Unit Q F) (old new : ProtocolRow A) :
        ProtocolActionAccepts D ProtocolAction.beginRound old new ↔ old ≠ [] ∧ BeginRoundSpec old new

        Integrated correctness of the transition entering an inner enumeration round.

        source
        theorem CertifiedRowSystem.Complement.evalProtocolAction_skipInner_iff {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] [Fintype Q] [Fintype F] (D : CertifiedRowSystem I A Unit Q F) (old new : ProtocolRow A) :
        ProtocolActionAccepts D ProtocolAction.skipInner old new ↔ old ≠ [] ∧ SkipInnerSpec old new

        Integrated correctness of one canonical inner-enumeration successor.

        source
        theorem CertifiedRowSystem.Complement.evalProtocolAction_finishOuter_iff {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] [Fintype Q] [Fintype F] (D : CertifiedRowSystem I A Unit Q F) (old new : ProtocolRow A) :
        ProtocolActionAccepts D ProtocolAction.finishOuter old new ↔ old ≠ [] ∧ FinishOuterSpec old new

        Integrated correctness of classifying and advancing one outer vertex.

        source
        theorem CertifiedRowSystem.Complement.evalProtocolAction_finishRound_iff {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] [Fintype Q] [Fintype F] (D : CertifiedRowSystem I A Unit Q F) (old new : ProtocolRow A) :
        ProtocolActionAccepts D ProtocolAction.finishRound old new ↔ old ≠ [] ∧ FinishRoundSpec old new

        Integrated correctness of the boundary between two counting rounds.

        source
        theorem CertifiedRowSystem.Complement.evalProtocolAction_finalSkip_iff {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] [Fintype Q] [Fintype F] (D : CertifiedRowSystem I A Unit Q F) (old new : ProtocolRow A) :
        ProtocolActionAccepts D ProtocolAction.finalSkip old new ↔ old ≠ [] ∧ FinalSkipSpec old new

        Integrated correctness of one canonical successor in the final scan.

        source
        theorem CertifiedRowSystem.Complement.evalProtocolAction_finalFinish_iff {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] [Fintype Q] [Fintype F] (D : CertifiedRowSystem I A Unit Q F) (old new : ProtocolRow A) :
        ProtocolActionAccepts D ProtocolAction.finalFinish old new ↔ old ≠ [] ∧ FinalFinishSpec old new

        Integrated correctness of the accepting final-enumeration transition.

        source
        theorem CertifiedRowSystem.Complement.evalProtocolAction_startPath_iff {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] [Fintype Q] [Fintype F] (D : CertifiedRowSystem I A Unit Q F) (old new : ProtocolRow A) :
        ProtocolActionAccepts D ProtocolAction.startPath old new ↔ old ≠ [] ∧ StartsPath ProtocolPhase.chooseInner ProtocolPhase.path old new

        Integrated correctness of the startPath action.

        source
        theorem CertifiedRowSystem.Complement.evalProtocolAction_finalStartPath_iff {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] [Fintype Q] [Fintype F] (D : CertifiedRowSystem I A Unit Q F) (old new : ProtocolRow A) :
        ProtocolActionAccepts D ProtocolAction.finalStartPath old new ↔ old ≠ [] ∧ StartsPath ProtocolPhase.finalChoose ProtocolPhase.finalPath old new

        Integrated correctness of the finalStartPath action.

        source
        theorem CertifiedRowSystem.Complement.evalProtocolAction_pathStep_iff {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] [Fintype Q] [Fintype F] (D : CertifiedRowSystem I A Unit Q F) (old new : ProtocolRow A) :
        ProtocolActionAccepts D ProtocolAction.pathStep old new ↔ IsPathStep D ProtocolPhase.path old new

        Integrated correctness of pathStep.

        source
        theorem CertifiedRowSystem.Complement.evalProtocolAction_finalPathStep_iff {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] [Fintype Q] [Fintype F] (D : CertifiedRowSystem I A Unit Q F) (old new : ProtocolRow A) :
        ProtocolActionAccepts D ProtocolAction.finalPathStep old new ↔ IsPathStep D ProtocolPhase.finalPath old new

        Integrated correctness of finalPathStep.

        source
        theorem CertifiedRowSystem.Complement.evalProtocolAction_finishWitness_iff {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] [Fintype Q] [Fintype F] (D : CertifiedRowSystem I A Unit Q F) (old new : ProtocolRow A) :
        ProtocolActionAccepts D ProtocolAction.finishWitness old new ↔ IsFinishWitness D old new

        Integrated correctness of finishWitness.

        source
        theorem CertifiedRowSystem.Complement.evalProtocolAction_finalFinishWitness_iff {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] [Fintype Q] [Fintype F] (D : CertifiedRowSystem I A Unit Q F) (old new : ProtocolRow A) :
        ProtocolActionAccepts D ProtocolAction.finalFinishWitness old new ↔ IsFinalWitness D old new

        Integrated correctness of finalFinishWitness.

        source
        theorem CertifiedRowSystem.Complement.deterministicComplementSystem_rowStep_iff {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] [Fintype Q] [Fintype F] (D : CertifiedRowSystem I A Unit Q F) (old new : ProtocolRow A) :
        (deterministicComplementSystem D).RowStep old new ↔ ProtocolStep D old new

        The compiled row checker accepts exactly the declarative protocol transition relation. In particular, this theorem covers arbitrary action certificates, not only certificates that were assumed in advance to repeat one action.