elliptic/swsep/swsepScript.sml

120   (IS_MEMORY_DOPER (MLDR dst src) = T) /\
121   (IS_MEMORY_DOPER (MSTR src dst) = T) /\
122   (IS_MEMORY_DOPER (MPUSH dst' srcL) = T) /\
123   (IS_MEMORY_DOPER (MPOP dst' srcL) = T) /\
127   (IS_WELL_FORMED_DOPER (MMUL dst src1 src2) = ~(dst = src1)) /\
195          (STACK_SIZE_DOPER (MMOV dst e) = (0, 0, ~(dst = R13))) /\
196          (STACK_SIZE_DOPER (MADD dst reg1 e) = (0, 0, ~(dst = R13))) /\
197          (STACK_SIZE_DOPER (MSUB dst reg1 e) = (0, 0, ~(dst = R13))) /\
198          (STACK_SIZE_DOPER (MRSB dst reg1 e) = (0, 0, ~(dst = R13))) /\
199          (STACK_SIZE_DOPER (MMUL dst reg1 reg2) = (0, 0, ~(dst = R13) /\
200                 ~(dst = reg1))) /\
201          (STACK_SIZE_DOPER (MAND dst reg1 e) = (0, 0, ~(dst = R13))) /\
202          (STACK_SIZE_DOPER (MORR dst reg1 e) = (0, 0, ~(dst = R13))) /\
203          (STACK_SIZE_DOPER (MEOR dst reg1 e) = (0, 0, ~(dst = R13))) /\
204          (STACK_SIZE_DOPER (MLSL dst reg1 s) = (0, 0, ~(dst = R13))) /\
205          (STACK_SIZE_DOPER (MLSR dst reg1 s) = (0, 0, ~(dst = R13))) /\
206          (STACK_SIZE_DOPER (MASR dst reg1 s) = (0, 0, ~(dst = R13))) /\
207          (STACK_SIZE_DOPER (MROR dst reg1 s) = (0, 0, ~(dst = R13))) /\
542   (DOPER2INSTRUCTION (MMOV dst src) =
543       MOV AL F (MREG2REG dst) (MEXP2addr_model src)) /\
544   (DOPER2INSTRUCTION (MADD dst src1 src2) =
545       ADD AL F (MREG2REG dst) (MREG2REG src1) (MEXP2addr_model src2)) /\
546   (DOPER2INSTRUCTION (MSUB dst src1 src2) =
547       SUB AL F (MREG2REG dst) (MREG2REG src1) (MEXP2addr_model src2)) /\
548   (DOPER2INSTRUCTION (MRSB dst src1 src2) =
549       RSB AL F (MREG2REG dst) (MREG2REG src1) (MEXP2addr_model src2)) /\
550   (DOPER2INSTRUCTION (MMUL dst src1 src2_reg) =
551       MUL AL F (MREG2REG dst) (MREG2REG src1) (MREG2REG src2_reg)) /\
552   (DOPER2INSTRUCTION (MAND dst src1 src2) =
553       AND AL F (MREG2REG dst) (MREG2REG src1) (MEXP2addr_model src2)) /\
554   (DOPER2INSTRUCTION (MORR dst src1 src2) =
555       ORR AL F (MREG2REG dst) (MREG2REG src1) (MEXP2addr_model src2)) /\
556   (DOPER2INSTRUCTION (MEOR dst src1 src2) =
557       EOR AL F (MREG2REG dst) (MREG2REG src1) (MEXP2addr_model src2)) /\
558   (DOPER2INSTRUCTION (MLSL dst src2_reg src2_num) =
559       MOV AL F (MREG2REG dst) (Dp_shift_immediate (LSL (MREG2REG src2_reg)) src2_num)) /\
560   (DOPER2INSTRUCTION (MLSR dst src2_reg src2_num) =
563         MOV AL F (MREG2REG dst) (Dp_shift_immediate (LSL (MREG2REG src2_reg)) src2_num)
565         MOV AL F (MREG2REG dst) (Dp_shift_immediate (LSR (MREG2REG src2_reg)) src2_num)) /\
566   (DOPER2INSTRUCTION (MASR dst src2_reg src2_num) =
569         MOV AL F (MREG2REG dst) (Dp_shift_immediate (LSL (MREG2REG src2_reg)) src2_num)
571         MOV AL F (MREG2REG dst) (Dp_shift_immediate (ASR (MREG2REG src2_reg)) src2_num)) /\
572   (DOPER2INSTRUCTION (MROR dst src2_reg src2_num) =
575         MOV AL F (MREG2REG dst) (Dp_shift_immediate (LSL (MREG2REG src2_reg)) src2_num)
577         MOV AL F (MREG2REG dst) (Dp_shift_immediate (ROR (MREG2REG src2_reg)) src2_num))