Specification

This module provides the per-instruction Hoare specifications.

theorem specification_LoadAddress (P : Assertion) (pc dst addr : UInt64) (L : Set UInt64) : L = {n : UInt64 | n ≠ pc + 1} → hoare_triple_up_1 (fun (st : MState) => P (st.incPc.addRegister dst addr) ∧ ¬st.terminated = true) (fun (st : MState) => P st ∧ ¬st.terminated = true) pc {pc + 1} L (Instr.LoadAddress dst addr)

theorem specification_LoadImmediate (P : Assertion) (pc dst val : UInt64) (L : Set UInt64) : L = {n : UInt64 | n ≠ pc + 1} → hoare_triple_up_1 (fun (st : MState) => P (st.incPc.addRegister dst val) ∧ ¬st.terminated = true) (fun (st : MState) => P st ∧ ¬st.terminated = true) pc {pc + 1} L (Instr.LoadImmediate dst val)

Specification for Instr.LoadImmediate.

For certifying the instruction, the rule of assignment (P ⟦x[dst] ← val; pc++⟧) is used. The hoare triples state that if you start in a state where the precondition P holds, and you execute the instruction, the precondition P will still hold after the execution. The precondition is applied after simulating the effects of the instruction.

theorem specification_CopyRegister (P : Assertion) (pc dst src : UInt64) (L : Set UInt64) : L = {n : UInt64 | n ≠ pc + 1} → hoare_triple_up_1 (fun (st : MState) => P (st.incPc.addRegister dst (st.getRegisterAt src)) ∧ ¬st.terminated = true) (fun (st : MState) => P st ∧ ¬st.terminated = true) pc {pc + 1} L (Instr.CopyRegister dst src)

theorem specification_AddImmediate (P : Assertion) (pc dst regAddend val : UInt64) (L : Set UInt64) : L = {n : UInt64 | n ≠ pc + 1} → hoare_triple_up_1 (fun (st : MState) => P (st.incPc.addRegister dst (st.getRegisterAt regAddend + val)) ∧ ¬st.terminated = true) (fun (st : MState) => P st ∧ ¬st.terminated = true) pc {pc + 1} L (Instr.AddImmediate dst regAddend val)

theorem specification_Increment (P : Assertion) (pc dst : UInt64) (L : Set UInt64) : L = {n : UInt64 | n ≠ pc + 1} → hoare_triple_up_1 (fun (st : MState) => P (st.incPc.addRegister dst (st.getRegisterAt dst + 1)) ∧ ¬st.terminated = true) (fun (st : MState) => P st ∧ ¬st.terminated = true) pc {pc + 1} L (Instr.Increment dst)

theorem specification_AddRegister (P : Assertion) (pc dst regAddend1 regAddend2 : UInt64) (L : Set UInt64) : L = {n : UInt64 | n ≠ pc + 1} → hoare_triple_up_1 (fun (st : MState) => P (st.incPc.addRegister dst (st.getRegisterAt regAddend1 + st.getRegisterAt regAddend2)) ∧ ¬st.terminated = true) (fun (st : MState) => P st ∧ ¬st.terminated = true) pc {pc + 1} L (Instr.AddRegister dst regAddend1 regAddend2)

theorem specification_SubImmediate (P : Assertion) (pc dst regMinuend subtrahend : UInt64) (L : Set UInt64) : L = {n : UInt64 | n ≠ pc + 1} → hoare_triple_up_1 (fun (st : MState) => P (st.incPc.addRegister dst (st.getRegisterAt regMinuend - subtrahend)) ∧ ¬st.terminated = true) (fun (st : MState) => P st ∧ ¬st.terminated = true) pc {pc + 1} L (Instr.SubImmediate dst regMinuend subtrahend)

theorem specification_Decrement (P : Assertion) (pc dst : UInt64) (L : Set UInt64) : L = {n : UInt64 | n ≠ pc + 1} → hoare_triple_up_1 (fun (st : MState) => P (st.incPc.addRegister dst (st.getRegisterAt dst - 1)) ∧ ¬st.terminated = true) (fun (st : MState) => P st ∧ ¬st.terminated = true) pc {pc + 1} L (Instr.Decrement dst)

theorem specification_SubRegister (P : Assertion) (pc dst regMinuend regSubtrahend : UInt64) (L : Set UInt64) : L = {n : UInt64 | n ≠ pc + 1} → hoare_triple_up_1 (fun (st : MState) => P (st.incPc.addRegister dst (st.getRegisterAt regMinuend - st.getRegisterAt regSubtrahend)) ∧ ¬st.terminated = true) (fun (st : MState) => P st ∧ ¬st.terminated = true) pc {pc + 1} L (Instr.SubRegister dst regMinuend regSubtrahend)

theorem specification_XorImmediate (P : Assertion) (pc dst reg val : UInt64) (L : Set UInt64) : L = {n : UInt64 | n ≠ pc + 1} → hoare_triple_up_1 (fun (st : MState) => P (st.incPc.addRegister dst (st.getRegisterAt reg ^^^ val)) ∧ ¬st.terminated = true) (fun (st : MState) => P st ∧ ¬st.terminated = true) pc {pc + 1} L (Instr.XorImmediate dst reg val)

theorem specification_XOR (P : Assertion) (pc dst reg1 reg2 : UInt64) (L : Set UInt64) : L = {n : UInt64 | n ≠ pc + 1} → hoare_triple_up_1 (fun (st : MState) => P (st.incPc.addRegister dst (st.getRegisterAt reg1 ^^^ st.getRegisterAt reg2)) ∧ ¬st.terminated = true) (fun (st : MState) => P st ∧ ¬st.terminated = true) pc {pc + 1} L (Instr.XOR dst reg1 reg2)

theorem specification_LoadWordImmediate (P : Assertion) (pc dst addr : UInt64) (L : Set UInt64) : L = {n : UInt64 | n ≠ pc + 1} → hoare_triple_up_1 (fun (st : MState) => P (st.incPc.addRegister dst (st.getMemoryAt addr)) ∧ ¬st.terminated = true) (fun (st : MState) => P st ∧ ¬st.terminated = true) pc {pc + 1} L (Instr.LoadWordImmediate dst addr)

theorem specification_LoadWordReg (P : Assertion) (pc dst regWithAddr : UInt64) (L : Set UInt64) : L = {n : UInt64 | n ≠ pc + 1} → hoare_triple_up_1 (fun (st : MState) => P (st.incPc.addRegister dst (st.getMemoryAt (st.getRegisterAt regWithAddr))) ∧ ¬st.terminated = true) (fun (st : MState) => P st ∧ ¬st.terminated = true) pc {pc + 1} L (Instr.LoadWordReg dst regWithAddr)

theorem specification_StoreWordImmediate (P : Assertion) (pc regWithAddr regWithValue : UInt64) (L : Set UInt64) : L = {n : UInt64 | n ≠ pc + 1} → hoare_triple_up_1 (fun (st : MState) => P (st.incPc.addMemory (st.getRegisterAt regWithAddr) (st.getRegisterAt regWithValue)) ∧ ¬st.terminated = true) (fun (st : MState) => P st ∧ ¬st.terminated = true) pc {pc + 1} L (Instr.StoreWord regWithValue regWithAddr)

theorem specification_Jump (P : Assertion) (pc newPc : UInt64) (label : String) (L : Set UInt64) : L = {n : UInt64 | n ≠ newPc} → hoare_triple_up_1 (fun (st : MState) => P (st.setPc newPc) ∧ st.getLabelAt label = some newPc ∧ ¬st.terminated = true) (fun (st : MState) => P st ∧ ¬st.terminated = true) pc {newPc} L (Instr.Jump label)

theorem specification_Jump' (P : Assertion) (pc newPc : UInt64) (label : String) (L : Set UInt64) : L = {n : UInt64 | n ≠ newPc} → hoare_triple_up_1 (fun (st : MState) => P (st.setPc newPc) ∧ st.getLabelAt label = some newPc ∧ ¬st.terminated = true) (fun (st : MState) => P st ∧ ¬st.terminated = true ∧ st.pc = newPc) pc {newPc} L (Instr.Jump label)

theorem specification_JumpEq_true (P : Assertion) (pc newPc reg1 reg2 : UInt64) (s : String) (L : Set UInt64) : L = {n : UInt64 | n ≠ newPc} → hoare_triple_up_1 (fun (st : MState) => P (st.setPc newPc) ∧ st.getLabelAt s = some newPc ∧ st.getRegisterAt reg1 = st.getRegisterAt reg2 ∧ ¬st.terminated = true) (fun (st : MState) => P st ∧ st.getLabelAt s = some newPc ∧ ¬st.terminated = true) pc {newPc} L (Instr.JumpEq reg1 reg2 s)

theorem specification_JumpEq_false (P : Assertion) (pc reg1 reg2 : UInt64) (s : String) (L : Set UInt64) : L = {n : UInt64 | n ≠ pc + 1} → hoare_triple_up_1 (fun (st : MState) => P st.incPc ∧ st.getRegisterAt reg1 ≠ st.getRegisterAt reg2 ∧ ¬st.terminated = true) (fun (st : MState) => P st ∧ ¬st.terminated = true) pc {pc + 1} L (Instr.JumpEq reg1 reg2 s)

theorem specification_JumpNeq_true (P : Assertion) (pc newPc reg1 reg2 : UInt64) (s : String) (L : Set UInt64) : L = {n : UInt64 | n ≠ newPc} → hoare_triple_up_1 (fun (st : MState) => P (st.setPc newPc) ∧ st.getLabelAt s = some newPc ∧ st.getRegisterAt reg1 ≠ st.getRegisterAt reg2 ∧ ¬st.terminated = true) (fun (st : MState) => P st ∧ st.getLabelAt s = some newPc ∧ ¬st.terminated = true) pc {newPc} L (Instr.JumpNeq reg1 reg2 s)

theorem specification_JumpNeq_false (P : Assertion) (pc reg1 reg2 : UInt64) (s : String) (L : Set UInt64) : L = {n : UInt64 | n ≠ pc + 1} → hoare_triple_up_1 (fun (st : MState) => P st.incPc ∧ st.getRegisterAt reg1 = st.getRegisterAt reg2 ∧ ¬st.terminated = true) (fun (st : MState) => P st ∧ ¬st.terminated = true) pc {pc + 1} L (Instr.JumpNeq reg1 reg2 s)

theorem specification_JumpGt_true (P : Assertion) (pc newPc reg1 reg2 : UInt64) (s : String) (L : Set UInt64) : L = {n : UInt64 | n ≠ newPc} → hoare_triple_up_1 (fun (st : MState) => P (st.setPc newPc) ∧ st.getLabelAt s = some newPc ∧ st.getRegisterAt reg1 > st.getRegisterAt reg2 ∧ ¬st.terminated = true) (fun (st : MState) => P st ∧ st.getLabelAt s = some newPc ∧ ¬st.terminated = true) pc {newPc} L (Instr.JumpGt reg1 reg2 s)

theorem specification_JumpGt_false (P : Assertion) (pc reg1 reg2 : UInt64) (s : String) (L : Set UInt64) : L = {n : UInt64 | n ≠ pc + 1} → hoare_triple_up_1 (fun (st : MState) => P st.incPc ∧ st.getRegisterAt reg1 ≤ st.getRegisterAt reg2 ∧ ¬st.terminated = true) (fun (st : MState) => P st ∧ ¬st.terminated = true) pc {pc + 1} L (Instr.JumpGt reg1 reg2 s)

theorem specification_JumpLe_true (P : Assertion) (pc newPc reg1 reg2 : UInt64) (s : String) (L : Set UInt64) : L = {n : UInt64 | n ≠ newPc} → hoare_triple_up_1 (fun (st : MState) => P (st.setPc newPc) ∧ st.getLabelAt s = some newPc ∧ st.getRegisterAt reg1 ≤ st.getRegisterAt reg2 ∧ ¬st.terminated = true) (fun (st : MState) => P st ∧ st.getLabelAt s = some newPc ∧ ¬st.terminated = true) pc {newPc} L (Instr.JumpLe reg1 reg2 s)

theorem specification_JumpLe_false (P : Assertion) (pc reg1 reg2 : UInt64) (s : String) (L : Set UInt64) : L = {n : UInt64 | n ≠ pc + 1} → hoare_triple_up_1 (fun (st : MState) => P st.incPc ∧ st.getRegisterAt reg1 > st.getRegisterAt reg2 ∧ ¬st.terminated = true) (fun (st : MState) => P st ∧ ¬st.terminated = true) pc {pc + 1} L (Instr.JumpLe reg1 reg2 s)

theorem specification_JumpEqZero_true (P : Assertion) (pc newPc reg : UInt64) (label : String) (L : Set UInt64) : L = {n : UInt64 | n ≠ newPc} → hoare_triple_up_1 (fun (st : MState) => P (st.setPc newPc) ∧ st.getLabelAt label = some newPc ∧ st.getRegisterAt reg = 0 ∧ ¬st.terminated = true) (fun (st : MState) => P st ∧ ¬st.terminated = true) pc {newPc} L (Instr.JumpEqZero reg label)

theorem specification_JumpEqZero_false (P : Assertion) (pc reg : UInt64) (label : String) (L : Set UInt64) : L = {n : UInt64 | n ≠ pc + 1} → hoare_triple_up_1 (fun (st : MState) => P st.incPc ∧ st.getRegisterAt reg ≠ 0 ∧ ¬st.terminated = true) (fun (st : MState) => P st ∧ ¬st.terminated = true) pc {pc + 1} L (Instr.JumpEqZero reg label)

theorem specification_JumpNeqZero_true (P : Assertion) (pc newPc reg : UInt64) (s : String) (L : Set UInt64) : L = {n : UInt64 | n ≠ newPc} → hoare_triple_up_1 (fun (st : MState) => P (st.setPc newPc) ∧ st.getLabelAt s = some newPc ∧ st.getRegisterAt reg ≠ 0 ∧ ¬st.terminated = true) (fun (st : MState) => P st) pc {newPc} L (Instr.JumpNeqZero reg s)

theorem specification_JumpNeqZero_false (P : Assertion) (pc reg : UInt64) (s : String) (L : Set UInt64) : L = {n : UInt64 | n ≠ pc + 1} → hoare_triple_up_1 (fun (st : MState) => P st.incPc ∧ st.getRegisterAt reg = 0 ∧ ¬st.terminated = true) (fun (st : MState) => P st ∧ ¬st.terminated = true) pc {pc + 1} L (Instr.JumpNeqZero reg s)