Documentation

Complexitylib.Models.RandomAccessMachine.Simulation.RegisterStore.Machine.EntryCleanup.Defs

Sparse-entry miss cleanup — definitions #

The miss branch after entryMatchReadTM resets the seven decoder/result scratch tapes while preserving the consumed source cursor and query address. This restores the exact invariant needed to inspect the next encoded entry.

source
def Complexity.RAM.RegisterStore.Machine.EntryMatchTapes.cleanupIdx {n : ℕ} (tapes : EntryMatchTapes n) (i : Fin 7) :
Fin n

Embed the seven cleanup slots into the nine entry-match tapes. Slots zero through five select decoder scratch 1..6; slot six selects result tape 8, skipping the preserved query tape 7.

Equations
Instances For
    source
    theorem Complexity.RAM.RegisterStore.Machine.EntryMatchTapes.cleanupIdx_injective {n : ℕ} (tapes : EntryMatchTapes n) :
    Function.Injective tapes.cleanupIdx

    The cleanup-slot embedding is injective.

    source
    @[simp]
    theorem Complexity.RAM.RegisterStore.Machine.EntryMatchTapes.cleanupIdx_zero {n : ℕ} (tapes : EntryMatchTapes n) :
    tapes.cleanupIdx 0 = tapes.address
    source
    @[simp]
    theorem Complexity.RAM.RegisterStore.Machine.EntryMatchTapes.cleanupIdx_one {n : ℕ} (tapes : EntryMatchTapes n) :
    tapes.cleanupIdx 1 = tapes.value
    source
    @[simp]
    theorem Complexity.RAM.RegisterStore.Machine.EntryMatchTapes.cleanupIdx_two {n : ℕ} (tapes : EntryMatchTapes n) :
    tapes.cleanupIdx 2 = tapes.addressCounter
    source
    @[simp]
    theorem Complexity.RAM.RegisterStore.Machine.EntryMatchTapes.cleanupIdx_three {n : ℕ} (tapes : EntryMatchTapes n) :
    tapes.cleanupIdx 3 = tapes.addressWidth
    source
    @[simp]
    theorem Complexity.RAM.RegisterStore.Machine.EntryMatchTapes.cleanupIdx_four {n : ℕ} (tapes : EntryMatchTapes n) :
    tapes.cleanupIdx 4 = tapes.valueCounter
    source
    @[simp]
    theorem Complexity.RAM.RegisterStore.Machine.EntryMatchTapes.cleanupIdx_five {n : ℕ} (tapes : EntryMatchTapes n) :
    tapes.cleanupIdx 5 = tapes.valueWidth
    source
    @[simp]
    theorem Complexity.RAM.RegisterStore.Machine.EntryMatchTapes.cleanupIdx_six {n : ℕ} (tapes : EntryMatchTapes n) :
    tapes.cleanupIdx 6 = tapes.result
    source
    def Complexity.RAM.RegisterStore.Machine.entryMissTargets {n : ℕ} (tapes : EntryMatchTapes n) :
    List (Fin n)

    Fixed, machine-level list of the seven scratch tapes reset on a miss.

    Equations
    Instances For
      source
      def Complexity.RAM.RegisterStore.Machine.entryMissBits {n : ℕ} (tapes : EntryMatchTapes n) (entry : Entry) (queryBits : List Bool) (i : Fin n) :
      List Bool

      Canonical represented contents occupying each scratch tape at the readable match endpoint. Values away from the seven scratch tapes are irrelevant.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Complexity.RAM.RegisterStore.Machine.entryMissHeadBound {n : ℕ} (entry : Entry) (queryBits : List Bool) (initialWork : Fin n → Tape) (i : Fin n) :
        ℕ

        Per-tape cursor bound inherited from the readable match contract.

        Equations
        Instances For
          source
          def Complexity.RAM.RegisterStore.Machine.entryMissCleanupTM {n : ℕ} (tapes : EntryMatchTapes n) :
          TM n

          Rewind the preserved query, then reset all decoder/result scratch after a failed entry comparison.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Complexity.RAM.RegisterStore.Machine.entryMissCleanupTime {n : ℕ} (tapes : EntryMatchTapes n) (entry : Entry) (queryBits : List Bool) (initialWork : Fin n → Tape) :
            ℕ

            Compositional miss-cleanup bound specialized to the readable endpoint.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              structure Complexity.RAM.RegisterStore.Machine.EntryScanReady {n : ℕ} (tapes : EntryMatchTapes n) (remaining queryBits : List Bool) (initialWork finalWork : Fin n → Tape) :
              Prop

              Loop invariant restored after a failed match: the source points at the next entry, query is preserved, and all seven scratch tapes are canonical blank/zero tapes ready for another decode.

              Instances For