elliptic/swsep/swsepScript.sml

37 val _ = hide "regs";
588   `REGS_EQUIVALENT m registers regs =
589     (!r. ((regs ' (MREG2REG r)) = (registers (num2register (mode_reg2num m (MREG2REG r))))))`
639   (DECODE_MEXP m (MR r) regs = regs (MREG2register m r)) /\
640   (DECODE_MEXP m (MC s c) regs = ((w2w c):word32 #>> (2 * w2n s)))`
662 ``!mexp regs mode C.
663   (SND (ADDR_MODE1 regs mode C
665     ((11 >< 0) (addr_mode1_encode (MEXP2addr_model mexp)))) = DECODE_MEXP mode mexp regs)``,
716   (DECODE_SHIFT m (LSL:word4->shift r) (c:word5) (regs:register->word32) = ((regs (num2register (mode_reg2num m r))) << w2n c)) /\
717   (DECODE_SHIFT m (LSR r) c regs = ((regs (num2register (mode_reg2num m r))) >>> w2n c)) /\
718   (DECODE_SHIFT m (ASR r) c regs = ((regs (num2register (mode_reg2num m r))) >> w2n c)) /\
719   (DECODE_SHIFT m (ROR r) c regs = ((regs (num2register (mode_reg2num m r))) #>> w2n c))`;
758 ``!s c regs mode C.
760   (SND (ADDR_MODE1 regs mode C
762     ((11 >< 0) (addr_mode1_encode (Dp_shift_immediate s c)))) = DECODE_SHIFT mode s c regs)``,
789                  (REG_READ regs mode c =
790                  regs (num2register (mode_reg2num mode c)))` THEN1 (
805   ``!registers regs m mem M0.
806   REGS_EQUIVALENT m registers regs ==>
807   (read (regs,mem) (toEXP M0) = DECODE_MEXP m M0 registers)``,
819   ``!registers regs mem m M.
820     (REGS_EQUIVALENT m registers regs) ==>
821     (REG_READ registers m (MREG2REG M) = read (regs, mem) (toREG M))``,
829 ``!registers regs m m' v.
830   REGS_EQUIVALENT m (REG_WRITE registers m' 15w v) regs =
831   REGS_EQUIVALENT m registers regs``,
853 ``!registers regs m.
854   REGS_EQUIVALENT m (INC_PC registers) regs =
855   REGS_EQUIVALENT m registers regs``,
861 ``!registers regs M x.
862   REGS_EQUIVALENT m registers regs ==>
864                   (regs |+ (MREG2REG M, x))``,
1053         REGS_EQUIVALENT_MEM m (offset, length) (registers, memory) (regs, mem) =
1054         REGS_EQUIVALENT m registers regs /\
1055         (!l. (MEM l (MEMORY_SLICE ((MEM_ADDR (regs ' 13w) + offset), length)) ==>
1061 ``!m offset registers memory regs mem.
1062 REGS_EQUIVALENT_MEM m (offset, 0) (registers, memory) (regs, mem) =
1063 REGS_EQUIVALENT m registers regs``,
2008 val state2reg_fun_def = Define (`state2reg_fun (regs, memory) =
2009         (\n:word4. if (n=15w) then 0w else (regs ' n))`)
2058 ``!state regs memory. (REGS_EQUIVALENT (DECODE_MODE ((4 >< 0) (CPSR_READ state.psrs))) state.registers regs) ==>
2060                                          state2reg_fun (regs, memory))