Documentation

Complexitylib.Circuits.Encoding.Machine.Internal.FrontEnd

Serialized circuit-evaluator front-end correctness #

Proof internals for validating a paired machine input, rewinding it, and staging its code and data components on appendable work tapes.

source
def Complexity.CircuitCode.Machine.Internal.ValidatorPost (bits : List Bool) (inp : Tape) (work : Fin workTapeCount → Tape) (out : Tape) :
Prop

Tape contract produced by the lifted outer-pair validator before branch routing.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Complexity.CircuitCode.Machine.Internal.Routed (bits : List Bool) (verdict : Bool) (inp : Tape) (work : Fin workTapeCount → Tape) (out : Tape) :
    Prop

    Tapes after the conditional has normalized the validator output and routed to the branch for verdict.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Complexity.CircuitCode.Machine.Internal.ValidRouted (bits : List Bool) (inp : Tape) (work : Fin workTapeCount → Tape) (out : Tape) :
      Prop

      Routed tapes on the validator's accepting branch, together with validity of the serialized outer pair.

      Equations
      Instances For
        source
        def Complexity.CircuitCode.Machine.Internal.InvalidRouted (bits : List Bool) (inp : Tape) (work : Fin workTapeCount → Tape) (out : Tape) :
        Prop

        Routed tapes on the validator's rejecting branch, together with failure of the serialized outer-pair decoder.

        Equations
        Instances For
          source
          theorem Complexity.CircuitCode.Machine.Internal.validPairStageTM_hoareTime (bits : List Bool) :
          validPairStageTM.HoareTime (ValidRouted bits) (PairStagePost bits) (2 * bits.length + 7)

          The valid staging branch exposes the public pair-staging postcondition in linear time.

          source
          theorem Complexity.CircuitCode.Machine.Internal.invalidPairStageTM_hoareTime (bits : List Bool) :
          TM.rewindInputTM.HoareTime (InvalidRouted bits) (PairStagePost bits) (bits.length + 4)

          The invalid staging branch rewinds while retaining the validator's zero verdict and fresh work tapes.

          source
          theorem Complexity.CircuitCode.Machine.Internal.validator_transition_routed (bits : List Bool) (verdict : Bool) (inp : Tape) (work : Fin workTapeCount → Tape) (out : Tape) (hpost : ValidatorPost bits inp work out) (hcell : out.cells 1 = Γ.ofBool verdict) :
          Routed bits verdict (TM.transitionInput inp) (fun (i : Fin workTapeCount) => TM.transitionTape (work i)) { head := 1, cells := out.cells }

          The conditional transition turns a validator endpoint with a fixed verdict into the corresponding routed branch precondition.

          source
          theorem Complexity.CircuitCode.Machine.Internal.pairStageTM_hoareTime_internal (bits : List Bool) :
          pairStageTM.HoareTime (PairStagePre bits) (PairStagePost bits) (pairStageTime bits.length)

          Internal proof of the public total pair-staging contract.