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
@[simp]
theorem Cslib.URM.Regs.write_read_self (σ : Regs) (n v : ℕ) :
(σ.write n v).read n = v
source
@[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
@[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
theorem Cslib.URM.State.ext_iff {s₁ s₂ : State} :
s₁ = s₂ ↔ s₁.pc = s₂.pc ∧ s₁.regs = s₂.regs

Instruction Lemmas #

Jump Instructions #

source
def Cslib.URM.Instr.IsJump :
Instr → Prop

An instruction is a jump instruction.

Equations
Instances For
    source
    @[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
    @[simp]
    theorem Cslib.URM.Instr.Z_nonJump (n : ℕ) :
    ¬(Z n).IsJump

    Z instruction is not a jump.

    source
    @[simp]
    theorem Cslib.URM.Instr.S_nonJump (n : ℕ) :
    ¬(S n).IsJump

    S instruction is not a jump.

    source
    @[simp]
    theorem Cslib.URM.Instr.T_nonJump (m n : ℕ) :
    ¬(T m n).IsJump

    T instruction is not a jump.

    source
    @[simp]
    theorem Cslib.URM.Instr.J_IsJump (m n q : ℕ) :
    (J m n q).IsJump

    J instruction is a jump.

    source
    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
    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
      @[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
      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
      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
      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
      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
        @[simp]
        theorem Cslib.URM.Instr.capJump_Z (len n : ℕ) :
        capJump len (Z n) = Z n
        source
        @[simp]
        theorem Cslib.URM.Instr.capJump_S (len n : ℕ) :
        capJump len (S n) = S n
        source
        @[simp]
        theorem Cslib.URM.Instr.capJump_T (len m n : ℕ) :
        capJump len (T m n) = T m n
        source
        @[simp]
        theorem Cslib.URM.Instr.capJump_J (len m n q : ℕ) :
        capJump len (J m n q) = J m n (min q len)
        source
        theorem Cslib.URM.Instr.JumpsBoundedBy.capJump (len : ℕ) (instr : Instr) :
        JumpsBoundedBy len (Instr.capJump len instr)

        capJump always produces an instruction with bounded jump.

        source
        @[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
        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.