Langlib

Langlib.Automata.LinearBounded.CertifiedRowSystem.Complement.Construction

Certified-row complement protocol construction #

This module implements the synchronous scanners and row actions of the inductive-counting complement protocol.

Boot action #

source
inductive CertifiedRowSystem.Complement.BootVerifier :
Type

State of the first, initialization scan.

Instances For
    source
    def CertifiedRowSystem.Complement.instDecidableEqBootVerifier.decEq (x✝ x✝¹ : BootVerifier) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      source
      instance CertifiedRowSystem.Complement.instDecidableEqBootVerifier :
      DecidableEq BootVerifier
      Equations
      source
      instance CertifiedRowSystem.Complement.instReprBootVerifier :
      Repr BootVerifier
      Equations
      source
      def CertifiedRowSystem.Complement.instReprBootVerifier.repr :
      BootVerifier → ℕ → Std.Format
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable instance CertifiedRowSystem.Complement.BootVerifier.instFintype :
        Fintype BootVerifier
        Equations
        • One or more equations did not get rendered due to their size.
        source
        noncomputable def CertifiedRowSystem.Complement.bootLocalOK {A : Type u_1} [Fintype A] [Nonempty A] [DecidableEq A] (old new : ProtocolCell A) :
        Bool

        Cell-local conditions of the boot transition, apart from the LSD-first one check on the new oldCount track.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem CertifiedRowSystem.Complement.bootLocalOK_eq_true_iff {A : Type u_1} [Fintype A] [Nonempty A] [DecidableEq A] {old new : ProtocolCell A} :
          bootLocalOK old new = true ↔ old.phase = ProtocolPhase.input ∧ new.phase = ProtocolPhase.roundStart ∧ old.vertex.source = new.vertex.source ∧ old.vertex.depth = (vertexCodec A).zero ∧ new.vertex.depth = (vertexCodec A).zero ∧ old.vertex.outer = (vertexCodec A).zero ∧ new.vertex.outer = (vertexCodec A).zero ∧ old.vertex.inner = (vertexCodec A).zero ∧ new.vertex.inner = (vertexCodec A).zero ∧ old.vertex.path = (vertexCodec A).zero ∧ new.vertex.path = (vertexCodec A).zero ∧ old.vertex.fuel = (vertexCodec A).zero ∧ new.vertex.fuel = (vertexCodec A).zero ∧ old.counter.oldCount = (countCodec A).zero ∧ old.counter.newCount = (countCodec A).zero ∧ new.counter.newCount = (countCodec A).zero ∧ old.counter.seenCount = (countCodec A).zero ∧ new.counter.seenCount = (countCodec A).zero ∧ old.found = false ∧ new.found = false
          source
          noncomputable def CertifiedRowSystem.Complement.bootStepCell {A : Type u_1} [Fintype A] [Nonempty A] [DecidableEq A] :
          BootVerifier → ProtocolCell A → ProtocolCell A → ProtocolAction → BootVerifier

          One cell of the initialization scan. The certificate must request boot in every cell; OneState.first makes the first count digit one and every later digit zero.

          Equations
          Instances For
            source
            def CertifiedRowSystem.Complement.bootDone :
            BootVerifier → Bool

            Successful terminal state of the initialization scan.

            Equations
            Instances For
              source
              noncomputable def CertifiedRowSystem.Complement.evalBoot {A : Type u_1} [Fintype A] [Nonempty A] [DecidableEq A] :
              BootVerifier → ProtocolRow A → ProtocolRow A → List ProtocolAction → Option BootVerifier

              Run only the boot verifier across aligned rows.

              Equations
              Instances For
                source
                theorem CertifiedRowSystem.Complement.evalBoot_eq_evalStep {A : Type u_1} [Fintype A] [Nonempty A] [DecidableEq A] (q : BootVerifier) (old new : ProtocolRow A) (actions : List ProtocolAction) :
                evalBoot q old new actions = { inputCell := fun (cell : ProtocolCell A) => cell, stepStart := BootVerifier.start, stepCell := bootStepCell, stepDone := bootDone, finalStart := true, finalCell := fun (ok : Bool) (x : ProtocolCell A) => ok, finalDone := id }.evalStep q old new actions

                evalBoot is the ordinary certified-row evaluator for bootStepCell.

                source
                noncomputable def CertifiedRowSystem.Complement.bootSystem {I : Type u_1} {A : Type u_2} [Fintype A] [Nonempty A] [DecidableEq A] (sourceCell : I → A) :
                CertifiedRowSystem I (ProtocolCell A) ProtocolAction BootVerifier Bool

                A certified row system exposing the initialization action. It is also the prefix of the complete protocol system: subsequent actions extend BootVerifier with the counting scanners while leaving this transition unchanged.

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

                  Integrated protocol system #

                  source
                  inductive CertifiedRowSystem.Complement.ProtocolVerifier (Q : Type u_1) (F : Type u_2) :
                  Type (max u_1 u_2)

                  Finite verifier state of the complete protocol. The outer constructor records which small synchronous scanner was selected by the repeated action certificate.

                  Instances For
                    source
                    def CertifiedRowSystem.Complement.instDecidableEqProtocolVerifier.decEq {Q✝ : Type u_1} {F✝ : Type u_2} [DecidableEq Q✝] [DecidableEq F✝] (x✝ x✝¹ : ProtocolVerifier Q✝ F✝) :
                    Decidable (x✝ = x✝¹)
                    Equations
                    Instances For
                      source
                      instance CertifiedRowSystem.Complement.instDecidableEqProtocolVerifier {Q✝ : Type u_1} {F✝ : Type u_2} [DecidableEq Q✝] [DecidableEq F✝] :
                      DecidableEq (ProtocolVerifier Q✝ F✝)
                      Equations
                      source
                      noncomputable instance CertifiedRowSystem.Complement.ProtocolVerifier.instFintype {Q : Type u_1} {F : Type u_2} [Fintype Q] [Fintype F] :
                      Fintype (ProtocolVerifier Q F)
                      Equations
                      • One or more equations did not get rendered due to their size.
                      source
                      noncomputable def CertifiedRowSystem.Complement.startProtocolAction {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) (old new : ProtocolCell A) :
                      ProtocolAction → ProtocolVerifier Q F

                      Select and run the first cell of the scanner named by an action.

                      Equations
                      Instances For
                        source
                        noncomputable def CertifiedRowSystem.Complement.protocolStepCell {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) :
                        ProtocolVerifier Q F → ProtocolCell A → ProtocolCell A → ProtocolAction → ProtocolVerifier Q F

                        One cell of the complete complement-protocol verifier.

                        Equations
                        Instances For
                          source
                          def CertifiedRowSystem.Complement.protocolStepDone {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} (D : CertifiedRowSystem I A Unit Q F) :
                          ProtocolVerifier Q F → Bool

                          Terminal predicate of the integrated scanner.

                          Equations
                          Instances For
                            source
                            noncomputable def CertifiedRowSystem.Complement.deterministicComplementSystem {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) :
                            CertifiedRowSystem I (ProtocolCell A) ProtocolAction (ProtocolVerifier Q F) Bool

                            The full inductive-counting row system for a source system whose edge verifier is deterministic (Unit-certified).

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              source
                              @[simp]
                              theorem CertifiedRowSystem.Complement.final_deterministicComplementSystem_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) (row : ProtocolRow A) :
                              (deterministicComplementSystem D).Final row ↔ HasPhase ProtocolPhase.accept row

                              A protocol row is final exactly when every cell carries the accepting phase.

                              source
                              noncomputable def CertifiedRowSystem.Complement.complementSystem {I : Type u_1} {A : Type u_2} {C : Type u_3} {Q : Type u_4} {F : Type u_5} [Fintype A] [Nonempty A] [DecidableEq A] [Fintype C] [Fintype Q] [DecidableEq Q] [Fintype F] (S : CertifiedRowSystem I A C Q F) :
                              CertifiedRowSystem I (ProtocolCell A) ProtocolAction (ProtocolVerifier (Finset Q) F) Bool

                              Machine-independent Immerman--Szelepcsényi construction for an arbitrary finite certified row system. The source edge verifier is determinized before the counting protocol is installed.

                              Equations
                              Instances For

                                Machine-independent protocol relation #

                                source
                                def CertifiedRowSystem.Complement.IsBoot {A : Type u_1} [Fintype A] [Nonempty A] [DecidableEq A] (old new : ProtocolRow A) :
                                Prop

                                List-level initialization action implemented by the boot scanner.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  source
                                  theorem CertifiedRowSystem.Complement.isBoot_input_initialized {I : Type u_1} {A : Type u_2} [Fintype A] [Nonempty A] [DecidableEq A] (sourceCell : I → A) {input : List I} (hne : input ≠ []) :
                                  IsBoot (List.map (inputProtocolCell sourceCell) input) (initializedProtocolRow (List.map sourceCell input))

                                  Every nonempty input row performs the canonical boot action.

                                  source
                                  def CertifiedRowSystem.Complement.ProtocolStep {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) (old new : ProtocolRow A) :
                                  Prop

                                  The union of all semantic actions in one complement-protocol step.

                                  This relation is independent of the compiler to an LBA. Its source parameter is already deterministic, so both D.RowStep and its negation are certified synchronously.

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