Basic theorems

This file contains many small lemmata about the built machine model. These lemmata help proving statements about the MRiscX language by simplifying terms. All these lemmata are added to the simp command with the @[simp]. This can shorten proofs because lean can apply these theorems with simp automatically.

@[simp]

theorem MState.incPc_increments_pc (ms : MState) : ms.incPc = { memory := ms.memory, registers := ms.registers, pc := ms.pc + 1, code := ms.code, terminated := ms.terminated }

theorem MState.setReg_incPc_symm (ms : MState) (r : Registers) : (ms.setRegister r).incPc = ms.incPc.setRegister r

theorem MState.addReg_incPc_comm (ms : MState) (r v : UInt64) : (ms.addRegister r v).incPc = ms.incPc.addRegister r v

theorem MState.addMem_incPc_comm (ms : MState) (r v : UInt64) : (ms.addMemory r v).incPc = ms.incPc.addMemory r v

theorem MState.incPc_terminated (ms : MState) : ms.incPc.terminated = ms.terminated

@[simp]

theorem MState.setPc_terminated (ms : MState) (p : UInt64) : (ms.setPc p).terminated = ms.terminated

theorem MState.addReg_terminated (ms : MState) (r v : UInt64) : (ms.addRegister r v).terminated = ms.terminated

theorem MState.addMem_terminated (ms : MState) (r v : UInt64) : (ms.addMemory r v).terminated = ms.terminated

theorem MState.addRegister_getRegister_neq (ms : MState) (r1 r2 v : UInt64) : r1 ≠ r2 → (ms.addRegister r1 v).getRegisterAt r2 = ms.getRegisterAt r2

theorem MState.addRegister_getRegister_eq (ms : MState) (r1 r2 v : UInt64) : r1 = r2 → (ms.addRegister r1 v).getRegisterAt r2 = v

theorem MState.setPc_getRegister_indep (ms : MState) (i r : UInt64) : (ms.setPc i).getRegisterAt r = ms.getRegisterAt r

theorem MState.setPc_getRegisterAt_def_indep (ms : MState) (r l : UInt64) : TMap.get ms.registers r = TMap.get (ms.setPc l).registers r

theorem MState.setPc_getMemory_indep (ms : MState) (i r : UInt64) : (ms.setPc i).getMemoryAt r = ms.getMemoryAt r

theorem MState.setPc_getMemoryAt_def_indep (ms : MState) (m l : UInt64) : TMap.get ms.memory m = TMap.get (ms.setPc l).memory m

@[simp]

theorem MState.set_pc (ms : MState) (i : UInt64) : (ms.setPc i).pc = i

theorem MState.incPc_getRegister_indep (ms : MState) (r : UInt64) : ms.incPc.getRegisterAt r = ms.getRegisterAt r

@[simp]

theorem MState.jump_set_pc (ms : MState) (s : String) (i : UInt64) : PMap.get ms.code.labels s = some i → ms.jump s = { memory := ms.memory, registers := ms.registers, pc := i, code := ms.code, terminated := ms.terminated }

@[simp]

theorem MState.currInstruction_unfold (ms : MState) : ms.currInstruction = TMap.get ms.code.instructionMap ms.pc

theorem MState.runNSteps_currInstruction (ms : MState) (n : ℕ) : (ms.runNSteps n).currInstruction = TMap.get (ms.runNSteps n).code.instructionMap (ms.runNSteps n).pc

@[simp]

theorem MState.addRegister_unfold (ms : MState) (i1 i2 : UInt64) : ms.addRegister i1 i2 = { memory := ms.memory, registers := (i1 ↦ i2; ms.registers), pc := ms.pc, code := ms.code, terminated := ms.terminated }

@[simp]

theorem MState.addMemory_unfold (ms : MState) (i1 i2 : UInt64) : ms.addMemory i1 i2 = { memory := (i1 ↦ i2; ms.memory), registers := ms.registers, pc := ms.pc, code := ms.code, terminated := ms.terminated }

@[simp]

theorem MState.run_zero_steps (ms : MState) : ms.runNSteps 0 = ms

theorem MState.run_n_run_one (ms : MState) (n : ℕ) : (ms.runNSteps n).runOneStep = ms.runNSteps (n + 1)

theorem MState.run_n_run_one_comm (ms : MState) (n : ℕ) : (ms.runNSteps n).runOneStep = ms.runOneStep.runNSteps n

@[simp]

theorem MState.run_one_step_eq_run_n_1 (ms : MState) : ms.runOneStep = ms.runNSteps 1

theorem MState.run_N_comm (ms : MState) (n m : ℕ) : (ms.runNSteps n).runNSteps m = (ms.runNSteps m).runNSteps n

@[simp]

theorem MState.run_n_m_steps_comp (ms : MState) (n m : ℕ) : (ms.runNSteps n).runNSteps m = ms.runNSteps (n + m)

theorem MState.add_reg_code_no_change (ms : MState) (r v : UInt64) : (ms.addRegister r v).code = ms.code

theorem MState.add_mem_code_no_change (ms : MState) (r v : UInt64) : (ms.addMemory r v).code = ms.code

@[simp]

theorem MState.set_pc_code_no_change (ms : MState) (v : UInt64) : (ms.setPc v).code = ms.code

@[simp]

theorem MState.set_termianted_code_no_change (ms : MState) (v : Bool) : (ms.setTerminated v).code = ms.code

@[simp]

theorem MState.jump_register_indep (ms : MState) (m : Memory) (r : Registers) (c : Code) (s : String) : ({ memory := m, registers := r, pc := ms.pc, code := c, terminated := ms.terminated }.jump s).pc = ({ memory := ms.memory, registers := ms.registers, pc := ms.pc, code := c, terminated := ms.terminated }.jump s).pc

theorem MState.get_register_only_register (m : Memory) (r : Registers) (c : Code) (terminated : Bool) (i p : UInt64) : { memory := m, registers := r, pc := p, code := c, terminated := terminated }.getRegisterAt i = TMap.get r i

theorem MState.get_register_only_register' (ms : MState) (m : Memory) (r : Registers) (c : Code) (terminated : Bool) (i p : UInt64) : { memory := m, registers := r, pc := p, code := c, terminated := terminated }.getRegisterAt i = { memory := ms.memory, registers := r, pc := ms.pc, code := ms.code, terminated := ms.terminated }.getRegisterAt i

theorem MState.get_register_only_memory (m : Memory) (r : Registers) (c : Code) (terminated : Bool) (i p : UInt64) : { memory := m, registers := r, pc := p, code := c, terminated := terminated }.getMemoryAt i = TMap.get m i

theorem MState.get_register_only_memory' (ms : MState) (m : Memory) (r : Registers) (c : Code) (terminated : Bool) (i p : UInt64) : { memory := m, registers := r, pc := p, code := c, terminated := terminated }.getMemoryAt i = { memory := m, registers := ms.registers, pc := ms.pc, code := ms.code, terminated := ms.terminated }.getMemoryAt i

@[simp]

theorem MState.get_label_from_code (ms : MState) (s : String) (l : UInt64) : (ms.getLabelAt s = some l) = (PMap.get ms.code.labels s = some l)

@[simp]

theorem MState.getRegisterAt_def (ms : MState) (l : UInt64) : ms.getRegisterAt l = TMap.get ms.registers l

@[simp]

theorem MState.getMemoryAt_def (ms : MState) (l : UInt64) : ms.getMemoryAt l = TMap.get ms.memory l

theorem MState.TMap_register_le_zero_eq_zero (ms : MState) (l : UInt64) : (TMap.get ms.registers l ≤ 0) = (TMap.get ms.registers l = 0)

theorem MState.register_le_zero_eq_zero (ms : MState) (l : UInt64) : (ms.getRegisterAt l ≤ 0) = (ms.getRegisterAt l = 0)

theorem MState.runOneSteps_code_remains (ms : MState) : ms.runOneStep.code = ms.code

@[simp]

theorem MState.runNSteps_code_remains (ms : MState) (n : ℕ) : (ms.runNSteps n).code = ms.code

theorem MState.code_remains_same (ms ms' : MState) (code : Code) (n : ℕ) : ms.code = code → ms.runNSteps n = ms' → ms'.code = code

theorem MState.runNSteps_diff (s : MState) (n : ℕ) (L1 L2 : Set UInt64) : L2 ⊆ L1 → (s.runNSteps n).pc ∉ L1 → (s.runNSteps n).pc ∉ L2

theorem MState.runNSteps_pc_in_superset (s : MState) (n : ℕ) (L1 L2 : Set UInt64) : L2 ⊆ L1 → (s.runNSteps n).pc ∈ L2 → (s.runNSteps n).pc ∈ L1

theorem MState.runNSteps_add (s s' s'' : MState) (n n' : ℕ) : s.runNSteps n = s' → s'.runNSteps n' = s'' → s.runNSteps (n + n') = s''

theorem MState.runNSteps_pc_nin (s s' s'' : MState) (n n' : ℕ) (L : Set UInt64) : s.runNSteps n = s' → s'.runNSteps n' = s'' → (s.runNSteps n).pc ∉ L → (s'.runNSteps n').pc ∉ L → (s.runNSteps (n + n')).pc ∉ L

theorem MState.runNSteps_pc_nin_extra_step (s s' : MState) (n : ℕ) (L : Set UInt64) : s.runNSteps n = s' → s'.pc ∉ L → (∀ (n' : ℕ), 0 < n' ∧ n' < n → (s.runNSteps n').pc ∉ L) → ∀ (n'' : ℕ), 0 < n'' ∧ n'' ≤ n → (s.runNSteps n'').pc ∉ L

theorem MState.run_n_plus_m_pc_not_in_set (s s' : MState) (m m' : ℕ) (set : Set UInt64) : s.runNSteps m = s' → (∀ (n : ℕ), 0 < n ∧ n ≤ m → (s.runNSteps n).pc ∉ set) → (∀ (n' : ℕ), 0 < n' ∧ n' < m' → (s'.runNSteps n').pc ∉ set) → ∀ (n'' : ℕ), 0 < n'' ∧ n'' < m + m' → (s.runNSteps n'').pc ∉ set

theorem MState.run_n_plus_m_diff_set (s s' : MState) (m m' : ℕ) (L_b L_b' : Set UInt64) : s.runNSteps m = s' → (∀ (n : ℕ), 0 < n ∧ n ≤ m → (s.runNSteps n).pc ∉ L_b) → (∀ (n' : ℕ), 0 < n' ∧ n' < m' → (s'.runNSteps n').pc ∉ L_b') → ∀ (n'' : ℕ), 0 < n'' ∧ n'' < m + m' → (s.runNSteps n'').pc ∉ L_b ∩ L_b'

theorem MState.run_n_plus_m_intersect (s s' : MState) (m m' : ℕ) (L_w L_b L_w' L_b' : Set UInt64) : L_w' ⊆ L_b ∧ L_w ∩ L_w' = ∅ → s.runNSteps m = s' → s'.pc ∈ L_w → s'.pc ∉ L_b → (∀ (n : ℕ), 0 < n ∧ n < m → (s.runNSteps n).pc ∉ L_w ∪ L_b) → (∀ (n' : ℕ), 0 < n' ∧ n' < m' → (s'.runNSteps n').pc ∉ L_w' ∪ L_b') → ∀ (n'' : ℕ), 0 < n'' ∧ n'' < m + m' → (s.runNSteps n'').pc ∉ L_w' ∪ L_b ∩ L_b'