Specification

📁 Source: MRiscX/Semantics/Specification.lean

Statistics

Metric	Count
Definitions	0
Theorems specification_AddImmediate, specification_AddRegister, specification_CopyRegister, specification_Decrement, specification_Increment, specification_Jump, specification_Jump', specification_JumpEqZero_false, specification_JumpEqZero_true, specification_JumpEq_false, specification_JumpEq_true, specification_JumpGt_false, specification_JumpGt_true, specification_JumpLe_false, specification_JumpLe_true, specification_JumpNeqZero_false, specification_JumpNeqZero_true, specification_JumpNeq_false, specification_JumpNeq_true, specification_LoadAddress, specification_LoadImmediate, specification_LoadWordImmediate, specification_LoadWordReg, specification_StoreWordImmediate, specification_SubImmediate, specification_SubRegister, specification_XOR, specification_XorImmediate	28
Total	28

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
specification_AddImmediate 📖	mathematical	—	hoare_triple_up_1 MState.addRegister MState.incPc MState.getRegisterAt MState.terminated Instr.AddImmediate	—	MState.getRegisterAt_def MState.addRegister_unfold MState.incPc_increments_pc
specification_AddRegister 📖	mathematical	—	hoare_triple_up_1 MState.addRegister MState.incPc MState.getRegisterAt MState.terminated Instr.AddRegister	—	MState.getRegisterAt_def MState.addRegister_unfold MState.incPc_increments_pc
specification_CopyRegister 📖	mathematical	—	hoare_triple_up_1 MState.addRegister MState.incPc MState.getRegisterAt MState.terminated Instr.CopyRegister	—	MState.getRegisterAt_def MState.addRegister_unfold MState.incPc_increments_pc
specification_Decrement 📖	mathematical	—	hoare_triple_up_1 MState.addRegister MState.incPc MState.getRegisterAt MState.terminated Instr.Decrement	—	MState.getRegisterAt_def MState.addRegister_unfold MState.incPc_increments_pc
specification_Increment 📖	mathematical	—	hoare_triple_up_1 MState.addRegister MState.incPc MState.getRegisterAt MState.terminated Instr.Increment	—	MState.getRegisterAt_def MState.addRegister_unfold MState.incPc_increments_pc
specification_Jump 📖	mathematical	—	hoare_triple_up_1 MState.setPc MState.getLabelAt MState.terminated Instr.Jump	—	MState.run_one_step_eq_run_n_1 MState.currInstruction_unfold MState.get_label_from_code
specification_Jump' 📖	mathematical	—	hoare_triple_up_1 MState.setPc MState.getLabelAt MState.terminated ProgramCounter MState.pc Instr.Jump	—	MState.run_one_step_eq_run_n_1 MState.currInstruction_unfold MState.get_label_from_code
specification_JumpEqZero_false 📖	mathematical	—	hoare_triple_up_1 MState.incPc MState.getRegisterAt MState.terminated Instr.JumpEqZero	—	MState.run_one_step_eq_run_n_1 MState.currInstruction_unfold MState.getRegisterAt_def MState.incPc_increments_pc
specification_JumpEqZero_true 📖	mathematical	—	hoare_triple_up_1 MState.setPc MState.getLabelAt MState.getRegisterAt MState.terminated Instr.JumpEqZero	—	MState.run_one_step_eq_run_n_1 MState.currInstruction_unfold MState.getRegisterAt_def MState.get_label_from_code
specification_JumpEq_false 📖	mathematical	—	hoare_triple_up_1 MState.incPc MState.getRegisterAt MState.terminated Instr.JumpEq	—	MState.run_one_step_eq_run_n_1 MState.currInstruction_unfold MState.getRegisterAt_def MState.incPc_increments_pc
specification_JumpEq_true 📖	mathematical	—	hoare_triple_up_1 MState.setPc MState.getLabelAt MState.getRegisterAt MState.terminated Instr.JumpEq	—	MState.run_one_step_eq_run_n_1 MState.currInstruction_unfold MState.getRegisterAt_def MState.get_label_from_code MState.runOneSteps_code_remains
specification_JumpGt_false 📖	mathematical	—	hoare_triple_up_1 MState.incPc MState.getRegisterAt MState.terminated Instr.JumpGt	—	MState.getRegisterAt_def MState.run_one_step_eq_run_n_1 MState.currInstruction_unfold MState.incPc_increments_pc
specification_JumpGt_true 📖	mathematical	—	hoare_triple_up_1 MState.setPc MState.getLabelAt MState.getRegisterAt MState.terminated Instr.JumpGt	—	MState.run_one_step_eq_run_n_1 MState.currInstruction_unfold MState.getRegisterAt_def MState.get_label_from_code MState.runOneSteps_code_remains
specification_JumpLe_false 📖	mathematical	—	hoare_triple_up_1 MState.incPc MState.getRegisterAt MState.terminated Instr.JumpLe	—	MState.run_one_step_eq_run_n_1 MState.currInstruction_unfold MState.getRegisterAt_def MState.incPc_increments_pc
specification_JumpLe_true 📖	mathematical	—	hoare_triple_up_1 MState.setPc MState.getLabelAt MState.getRegisterAt MState.terminated Instr.JumpLe	—	MState.run_one_step_eq_run_n_1 MState.currInstruction_unfold MState.getRegisterAt_def MState.get_label_from_code MState.runOneSteps_code_remains
specification_JumpNeqZero_false 📖	mathematical	—	hoare_triple_up_1 MState.incPc MState.getRegisterAt MState.terminated Instr.JumpNeqZero	—	MState.run_one_step_eq_run_n_1 MState.currInstruction_unfold MState.getRegisterAt_def MState.incPc_increments_pc
specification_JumpNeqZero_true 📖	mathematical	—	hoare_triple_up_1 MState.setPc MState.getLabelAt MState.getRegisterAt MState.terminated Instr.JumpNeqZero	—	MState.run_one_step_eq_run_n_1 MState.currInstruction_unfold MState.getRegisterAt_def MState.get_label_from_code
specification_JumpNeq_false 📖	mathematical	—	hoare_triple_up_1 MState.incPc MState.getRegisterAt MState.terminated Instr.JumpNeq	—	MState.run_one_step_eq_run_n_1 MState.currInstruction_unfold MState.getRegisterAt_def MState.incPc_increments_pc
specification_JumpNeq_true 📖	mathematical	—	hoare_triple_up_1 MState.setPc MState.getLabelAt MState.getRegisterAt MState.terminated Instr.JumpNeq	—	MState.run_one_step_eq_run_n_1 MState.currInstruction_unfold MState.getRegisterAt_def MState.get_label_from_code MState.runOneSteps_code_remains
specification_LoadAddress 📖	mathematical	—	hoare_triple_up_1 MState.addRegister MState.incPc MState.terminated Instr.LoadAddress	—	MState.addRegister_unfold MState.incPc_increments_pc
specification_LoadImmediate 📖	mathematical	—	hoare_triple_up_1 MState.addRegister MState.incPc MState.terminated Instr.LoadImmediate	—	MState.addRegister_unfold MState.incPc_increments_pc
specification_LoadWordImmediate 📖	mathematical	—	hoare_triple_up_1 MState.addRegister MState.incPc MState.getMemoryAt MState.terminated Instr.LoadWordImmediate	—	MState.getMemoryAt_def MState.addRegister_unfold MState.incPc_increments_pc
specification_LoadWordReg 📖	mathematical	—	hoare_triple_up_1 MState.addRegister MState.incPc MState.getMemoryAt MState.getRegisterAt MState.terminated Instr.LoadWordReg	—	MState.getRegisterAt_def MState.getMemoryAt_def MState.addRegister_unfold MState.incPc_increments_pc
specification_StoreWordImmediate 📖	mathematical	—	hoare_triple_up_1 MState.addMemory MState.incPc MState.getRegisterAt MState.terminated Instr.StoreWord	—	MState.getRegisterAt_def MState.addMemory_unfold MState.incPc_increments_pc
specification_SubImmediate 📖	mathematical	—	hoare_triple_up_1 MState.addRegister MState.incPc MState.getRegisterAt MState.terminated Instr.SubImmediate	—	MState.getRegisterAt_def MState.addRegister_unfold MState.incPc_increments_pc
specification_SubRegister 📖	mathematical	—	hoare_triple_up_1 MState.addRegister MState.incPc MState.getRegisterAt MState.terminated Instr.SubRegister	—	MState.getRegisterAt_def MState.addRegister_unfold MState.incPc_increments_pc
specification_XOR 📖	mathematical	—	hoare_triple_up_1 MState.addRegister MState.incPc MState.getRegisterAt MState.terminated Instr.XOR	—	MState.getRegisterAt_def MState.addRegister_unfold MState.incPc_increments_pc
specification_XorImmediate 📖	mathematical	—	hoare_triple_up_1 MState.addRegister MState.incPc MState.getRegisterAt MState.terminated Instr.XorImmediate	—	MState.getRegisterAt_def MState.addRegister_unfold MState.incPc_increments_pc

---

← Back to Index