Documentation

Cslib.Computability.URM.Basic

URM Basic Lemmas #

This file contains basic lemmas and helper operations for URM types.

Main definitions #

Main results #

Register Lemmas #

source
šŸ“ coverage
@[simp]
theorem Cslib.URM.Regs.write_read_self (Ļƒ : Regs) (n v : ā„•) :
(Ļƒ.write n v).read n = v
source
šŸ“ coverage
@[simp]
theorem Cslib.URM.Regs.write_read_of_ne (Ļƒ : Regs) (m n v : ā„•) (h : m ā‰  n) :
(Ļƒ.write n v).read m = Ļƒ.read m

State Lemmas #

source
šŸ“ coverage
@[simp]
theorem Cslib.URM.State.isHalted_iff (s : State) (p : Program) :
s.isHalted p ā†” List.length p ā‰¤ s.pc
source
theorem Cslib.URM.State.ext {sā‚ sā‚‚ : State} (hpc : sā‚.pc = sā‚‚.pc) (hregs : sā‚.regs = sā‚‚.regs) :
sā‚ = sā‚‚

Extensionality for State: two states are equal iff their components are equal.

source
šŸ“ coverage
theorem Cslib.URM.State.ext_iff {sā‚ sā‚‚ : State} :
sā‚ = sā‚‚ ā†” sā‚.pc = sā‚‚.pc āˆ§ sā‚.regs = sā‚‚.regs

Instruction Lemmas #

Jump Instructions #

source
šŸ”¹ coverage
def Cslib.URM.Instr.IsJump :
Instr ā†’ Prop

An instruction is a jump instruction.

Equations
Instances For
    source
    šŸ”ø coverage
    @[implicit_reducible]
    instance Cslib.URM.Instr.instDecidableIsJump (instr : Instr) :
    Decidable instr.IsJump
    Equations
    • One or more equations did not get rendered due to their size.
    source
    šŸ“ coverage
    @[simp]
    theorem Cslib.URM.Instr.Z_nonJump (n : ā„•) :
    Ā¬(Z n).IsJump

    Z instruction is not a jump.

    source
    šŸ“ coverage
    @[simp]
    theorem Cslib.URM.Instr.S_nonJump (n : ā„•) :
    Ā¬(S n).IsJump

    S instruction is not a jump.

    source
    šŸ“ coverage
    @[simp]
    theorem Cslib.URM.Instr.T_nonJump (m n : ā„•) :
    Ā¬(T m n).IsJump

    T instruction is not a jump.

    source
    šŸ“ coverage
    @[simp]
    theorem Cslib.URM.Instr.J_IsJump (m n q : ā„•) :
    (J m n q).IsJump

    J instruction is a jump.

    source
    šŸ“ coverage
    theorem Cslib.URM.Instr.shiftJumps_of_nonJump {instr : Instr} (h : Ā¬instr.IsJump) (offset : ā„•) :
    shiftJumps offset instr = instr

    shiftJumps is identity for non-jumping instructions.

    Bounded Jump Targets #

    source
    šŸ”¹ coverage
    def Cslib.URM.Instr.JumpsBoundedBy (len : ā„•) :
    Instr ā†’ Prop

    An instruction's jump target is bounded by a given length. Non-jump instructions trivially satisfy this.

    Equations
    Instances For
      source
      šŸ”ø coverage
      @[implicit_reducible]
      instance Cslib.URM.Instr.instDecidableJumpsBoundedBy (len : ā„•) (instr : Instr) :
      Decidable (JumpsBoundedBy len instr)
      Equations
      • One or more equations did not get rendered due to their size.
      source
      šŸ“ coverage
      theorem Cslib.URM.Instr.jumpsBoundedBy_of_nonJump {instr : Instr} (h : Ā¬instr.IsJump) (len : ā„•) :
      JumpsBoundedBy len instr

      Non-jumping instructions have bounded jumps for any length.

      source
      šŸ“ coverage
      theorem Cslib.URM.Instr.JumpsBoundedBy.mono {instr : Instr} {len1 len2 : ā„•} (h : JumpsBoundedBy len1 instr) (hle : len1 ā‰¤ len2) :
      JumpsBoundedBy len2 instr

      JumpsBoundedBy is monotonic: if bounded for len1, then bounded for any len2 ā‰„ len1.

      source
      šŸ“ coverage
      theorem Cslib.URM.Instr.JumpsBoundedBy.shiftJumps {instr : Instr} {len offset : ā„•} (h : JumpsBoundedBy len instr) :
      JumpsBoundedBy (offset + len) (Instr.shiftJumps offset instr)

      shiftJumps preserves bounded jumps with adjusted bound.

      Jump Target Capping #

      source
      šŸ”ø coverage
      def Cslib.URM.Instr.capJump (len : ā„•) :
      Instr ā†’ Instr

      Cap a jump target to be at most len. Non-jump instructions are unchanged.

      Equations
      Instances For
        source
        šŸ“ coverage
        @[simp]
        theorem Cslib.URM.Instr.capJump_Z (len n : ā„•) :
        capJump len (Z n) = Z n
        source
        šŸ“ coverage
        @[simp]
        theorem Cslib.URM.Instr.capJump_S (len n : ā„•) :
        capJump len (S n) = S n
        source
        šŸ“ coverage
        @[simp]
        theorem Cslib.URM.Instr.capJump_T (len m n : ā„•) :
        capJump len (T m n) = T m n
        source
        šŸ“ coverage
        @[simp]
        theorem Cslib.URM.Instr.capJump_J (len m n q : ā„•) :
        capJump len (J m n q) = J m n (min q len)
        source
        šŸ“ coverage
        theorem Cslib.URM.Instr.JumpsBoundedBy.capJump (len : ā„•) (instr : Instr) :
        JumpsBoundedBy len (Instr.capJump len instr)

        capJump always produces an instruction with bounded jump.

        source
        šŸ“ coverage
        @[simp]
        theorem Cslib.URM.Instr.capJump_idempotent (len : ā„•) (instr : Instr) :
        capJump len (capJump len instr) = capJump len instr

        capJump is idempotent: capping twice is the same as capping once.

        source
        šŸ“ coverage
        theorem Cslib.URM.Program.mem_maxRegister {p : Program} {instr : Instr} (h : instr āˆˆ p) :
        instr.maxRegister ā‰¤ p.maxRegister

        Any instruction in a program has maxRegister at most the program's maxRegister.