Documentation

Complexity.Algorithms.WordRAM.FusionTree.ReadHeader

Reading a fusion-node header #

All eighteen words of an internal-node header are loaded by a fixed straight-line program. The constant offsets and their address additions are charged. Query-dependent array accesses are separate from this header load.

Main definitions #

Main results #

References #

source
@[reducible, inline]
abbrev Cslib.Algorithms.WordRAM.FusionTree.ReadHeaderProgram.pointer :
Fin 21

Base address of the record, preserved.

Instances For
    source
    @[reducible, inline]
    abbrev Cslib.Algorithms.WordRAM.FusionTree.ReadHeaderProgram.offset :
    Fin 21

    Constant-offset scratch.

    Instances For
      source
      @[reducible, inline]
      abbrev Cslib.Algorithms.WordRAM.FusionTree.ReadHeaderProgram.address :
      Fin 21

      Address scratch.

      Instances For
        source
        def Cslib.Algorithms.WordRAM.FusionTree.ReadHeaderProgram.word (i : Fin 18) :
        WordRAM.Code WordRAM.Basis.standard 21

        Load header word i into register i+1.

        Instances For
          source
          def Cslib.Algorithms.WordRAM.FusionTree.ReadHeaderProgram.code :
          WordRAM.Code WordRAM.Basis.standard 21

          All eighteen header loads, with their constant offsets and address additions.

          Instances For
            source
            def Cslib.Algorithms.WordRAM.FusionTree.ReadHeaderProgram.result (x : WordRAM.Data 21) :
            WordRAM.Data 21

            Output state after the eighteen loaded words.

            Instances For
              source
              theorem Cslib.Algorithms.WordRAM.FusionTree.ReadHeaderProgram.exec {w : ℕ} (x : WordRAM.Data 21) (ha : WordRAM.Fits w (x.regs pointer + 17)) :
              WordRAM.Exec w code x (result x) 54

              All header words are read in 54 checked standard instructions, counting constants and address additions. The address bound implies that all constant offsets fit as well.

              source
              theorem Cslib.Algorithms.WordRAM.FusionTree.ReadHeaderProgram.result_spec (x : WordRAM.Data 21) :
              (result x).regs pointer = x.regs pointer ∧ (result x).mem = x.mem ∧ ∀ (i : Fin 18), (result x).regs ⟨↑i + 1, ⋯⟩ = x.mem (x.regs pointer + ↑i)

              The record base and memory are preserved, and each output register contains its header word.