Package m0-model: M0 model
Information
| name | m0-model |
| version | 1.0 |
| description | M0 model |
| author | HOL OpenTheory Packager <opentheory-packager@hol-theorem-prover.org> |
| license | MIT |
| checksum | b0f8e11bf1ea11b8133b9f5375fd2f48dbd4676c |
| requires | base hol-base hol-words hol-string hol-integer hol-monad hol-floating-point |
| show | Data.Bool Data.List Data.Option Data.Pair Data.Unit Function HOL4 Number.Natural Relation |
Files
- Package tarball m0-model-1.0.tgz
- Theory source file m0-model.thy (included in the package tarball)
Defined Type Operators
- HOL4
- m0
- m0.exception
- m0.instruction
- m0.m0_state
- m0.offset
- m0.AIRCR
- m0.ARM_Exception
- m0.Branch
- m0.CCR
- m0.CONTROL
- m0.Data
- m0.Hint
- m0.IPR
- m0.Load
- m0.MachineCode
- m0.Media
- m0.Mode
- m0.Multiply
- m0.PRIMASK
- m0.PSR
- m0.RName
- m0.SHPR2
- m0.SHPR3
- m0.SRType
- m0.Store
- m0.System
- m0
Defined Constants
- HOL4
- m0
- m0.bitify16
- m0.bitify4
- m0.boolify16
- m0.boolify4
- m0.dfn'ArithLogicImmediate
- m0.dfn'BranchExchange
- m0.dfn'BranchLinkExchangeRegister
- m0.dfn'BranchLinkImmediate
- m0.dfn'BranchTarget
- m0.dfn'Breakpoint
- m0.dfn'ByteReverse
- m0.dfn'ByteReversePackedHalfword
- m0.dfn'ByteReverseSignedHalfword
- m0.dfn'ChangeProcessorState
- m0.dfn'CompareImmediate
- m0.dfn'DataMemoryBarrier
- m0.dfn'DataSynchronizationBarrier
- m0.dfn'ExtendByte
- m0.dfn'ExtendHalfword
- m0.dfn'InstructionSynchronizationBarrier
- m0.dfn'LoadByte
- m0.dfn'LoadHalf
- m0.dfn'LoadLiteral
- m0.dfn'LoadMultiple
- m0.dfn'LoadWord
- m0.dfn'Move
- m0.dfn'MoveToRegisterFromSpecial
- m0.dfn'MoveToSpecialRegister
- m0.dfn'Multiply32
- m0.dfn'NoOperation
- m0.dfn'Push
- m0.dfn'Register
- m0.dfn'SendEvent
- m0.dfn'ShiftImmediate
- m0.dfn'ShiftRegister
- m0.dfn'StoreByte
- m0.dfn'StoreHalf
- m0.dfn'StoreMultiple
- m0.dfn'StoreWord
- m0.dfn'SupervisorCall
- m0.dfn'TestCompareRegister
- m0.dfn'Undefined
- m0.dfn'WaitForEvent
- m0.dfn'WaitForInterrupt
- m0.dfn'Yield
- m0.doRegister
- m0.exception_CASE
- m0.exception_size
- m0.immediate_form
- m0.instruction_CASE
- m0.instruction_size
- m0.m0_state_AIRCR
- m0.m0_state_AIRCR_fupd
- m0.m0_state_CASE
- m0.m0_state_CCR
- m0.m0_state_CCR_fupd
- m0.m0_state_CONTROL
- m0.m0_state_CONTROL_fupd
- m0.m0_state_CurrentMode
- m0.m0_state_CurrentMode_fupd
- m0.m0_state_ExceptionActive
- m0.m0_state_ExceptionActive_fupd
- m0.m0_state_MEM
- m0.m0_state_MEM_fupd
- m0.m0_state_NVIC_IPR
- m0.m0_state_NVIC_IPR_fupd
- m0.m0_state_PRIMASK
- m0.m0_state_PRIMASK_fupd
- m0.m0_state_PSR
- m0.m0_state_PSR_fupd
- m0.m0_state_REG
- m0.m0_state_REG_fupd
- m0.m0_state_SHPR2
- m0.m0_state_SHPR2_fupd
- m0.m0_state_SHPR3
- m0.m0_state_SHPR3_fupd
- m0.m0_state_VTOR
- m0.m0_state_VTOR_fupd
- m0.m0_state_count
- m0.m0_state_count_fupd
- m0.m0_state_exception
- m0.m0_state_exception_fupd
- m0.m0_state_pcinc
- m0.m0_state_pcinc_fupd
- m0.m0_state_pending
- m0.m0_state_pending_fupd
- m0.m0_state_size
- m0.mem
- m0.mem1
- m0.num2Mode
- m0.num2RName
- m0.num2SRType
- m0.offset_CASE
- m0.offset_size
- m0.raise'exception
- m0.rec'AIRCR
- m0.rec'CCR
- m0.rec'CONTROL
- m0.rec'IPR
- m0.rec'PRIMASK
- m0.rec'PSR
- m0.rec'SHPR2
- m0.rec'SHPR3
- m0.recordtype.AIRCR
- m0.recordtype.CCR
- m0.recordtype.CONTROL
- m0.recordtype.IPR
- m0.recordtype.PRIMASK
- m0.recordtype.PSR
- m0.recordtype.SHPR2
- m0.recordtype.SHPR3
- m0.recordtype.m0_state
- m0.reg'AIRCR
- m0.reg'CCR
- m0.reg'CONTROL
- m0.reg'IPR
- m0.reg'PRIMASK
- m0.reg'PSR
- m0.reg'SHPR2
- m0.reg'SHPR3
- m0.register_form
- m0.write'LR
- m0.write'MemA
- m0.write'MemU
- m0.write'PC
- m0.write'R
- m0.write'SP
- m0.write'SP_main
- m0.write'SP_process
- m0.write'mem
- m0.write'rec'AIRCR
- m0.write'rec'CCR
- m0.write'rec'CONTROL
- m0.write'rec'IPR
- m0.write'rec'PRIMASK
- m0.write'rec'PSR
- m0.write'rec'SHPR2
- m0.write'rec'SHPR3
- m0.write'reg'AIRCR
- m0.write'reg'CCR
- m0.write'reg'CONTROL
- m0.write'reg'IPR
- m0.write'reg'PRIMASK
- m0.write'reg'PSR
- m0.write'reg'SHPR2
- m0.write'reg'SHPR3
- m0.AIRCR_CASE
- m0.AIRCR_ENDIANNESS
- m0.AIRCR_ENDIANNESS_fupd
- m0.AIRCR_SYSRESETREQ
- m0.AIRCR_SYSRESETREQ_fupd
- m0.AIRCR_VECTCLRACTIVE
- m0.AIRCR_VECTCLRACTIVE_fupd
- m0.AIRCR_VECTKEY
- m0.AIRCR_VECTKEY_fupd
- m0.AIRCR_aircr'rst
- m0.AIRCR_aircr'rst_fupd
- m0.AIRCR_size
- m0.ALUWritePC
- m0.ARM_Exception_CASE
- m0.ARM_Exception_size
- m0.ASR
- m0.ASR_C
- m0.ASSERT
- m0.AddWithCarry
- m0.Align
- m0.Aligned
- m0.ArithLogicImmediate
- m0.ArithmeticOpcode
- m0.BLXWritePC
- m0.BXWritePC
- m0.BigEndianReverse
- m0.BitCount
- m0.Branch
- m0.BranchExchange
- m0.BranchLinkExchangeRegister
- m0.BranchLinkImmediate
- m0.BranchTarget
- m0.BranchTo
- m0.BranchWritePC
- m0.Branch_CASE
- m0.Branch_size
- m0.Breakpoint
- m0.ByteReverse
- m0.ByteReversePackedHalfword
- m0.ByteReverseSignedHalfword
- m0.CCR_CASE
- m0.CCR_STKALIGN
- m0.CCR_STKALIGN_fupd
- m0.CCR_UNALIGN_TRP
- m0.CCR_UNALIGN_TRP_fupd
- m0.CCR_ccr'rst
- m0.CCR_ccr'rst_fupd
- m0.CCR_size
- m0.CONTROL_CASE
- m0.CONTROL_SPSEL
- m0.CONTROL_SPSEL_fupd
- m0.CONTROL_control'rst
- m0.CONTROL_control'rst_fupd
- m0.CONTROL_nPRIV
- m0.CONTROL_nPRIV_fupd
- m0.CONTROL_size
- m0.CallSupervisor
- m0.ChangeProcessorState
- m0.CompareImmediate
- m0.ConditionPassed
- m0.CountLeadingZeroBits
- m0.CurrentModeIsPrivileged
- m0.DECODE_UNPREDICTABLE
- m0.Data
- m0.DataMemoryBarrier
- m0.DataProcessing
- m0.DataProcessingALU
- m0.DataProcessingPC
- m0.DataSynchronizationBarrier
- m0.Data_CASE
- m0.Data_size
- m0.DeActivate
- m0.Decode
- m0.DecodeImmShift
- m0.DecodeRegShift
- m0.DecodeThumb
- m0.DecodeThumb2
- m0.ExcNumber
- m0.ExceptionActiveBitCount
- m0.ExceptionEntry
- m0.ExceptionPriority
- m0.ExceptionReturn
- m0.ExceptionTaken
- m0.ExecutionPriority
- m0.Extend
- m0.ExtendByte
- m0.ExtendHalfword
- m0.ExternalInterrupt
- m0.Fetch
- m0.HardFault
- m0.HighestSetBit
- m0.Hint
- m0.Hint_CASE
- m0.Hint_size
- m0.IPR_CASE
- m0.IPR_PRI_N0
- m0.IPR_PRI_N0_fupd
- m0.IPR_PRI_N1
- m0.IPR_PRI_N1_fupd
- m0.IPR_PRI_N2
- m0.IPR_PRI_N2_fupd
- m0.IPR_PRI_N3
- m0.IPR_PRI_N3_fupd
- m0.IPR_ipr'rst
- m0.IPR_ipr'rst_fupd
- m0.IPR_size
- m0.IncPC
- m0.InstructionSynchronizationBarrier
- m0.IsOnes
- m0.LR
- m0.LSL
- m0.LSL_C
- m0.LSR
- m0.LSR_C
- m0.Load
- m0.LoadByte
- m0.LoadHalf
- m0.LoadLiteral
- m0.LoadMultiple
- m0.LoadWord
- m0.LoadWritePC
- m0.Load_CASE
- m0.Load_size
- m0.LookUpSP
- m0.LowestSetBit
- m0.MachineCode_CASE
- m0.MachineCode_size
- m0.Media
- m0.Media_CASE
- m0.Media_size
- m0.MemA
- m0.MemU
- m0.Mode2num
- m0.Mode_CASE
- m0.Mode_Handler
- m0.Mode_Thread
- m0.Mode_size
- m0.Move
- m0.MoveToRegisterFromSpecial
- m0.MoveToSpecialRegister
- m0.Multiply
- m0.Multiply32
- m0.Multiply_CASE
- m0.Multiply_size
- m0.NMI
- m0.Next
- m0.NoException
- m0.NoOperation
- m0.PC
- m0.PRIMASK_CASE
- m0.PRIMASK_PM
- m0.PRIMASK_PM_fupd
- m0.PRIMASK_primask'rst
- m0.PRIMASK_primask'rst_fupd
- m0.PRIMASK_size
- m0.PSR_C
- m0.PSR_CASE
- m0.PSR_C_fupd
- m0.PSR_ExceptionNumber
- m0.PSR_ExceptionNumber_fupd
- m0.PSR_N
- m0.PSR_N_fupd
- m0.PSR_T
- m0.PSR_T_fupd
- m0.PSR_V
- m0.PSR_V_fupd
- m0.PSR_Z
- m0.PSR_Z_fupd
- m0.PSR_psr'rst
- m0.PSR_psr'rst_fupd
- m0.PSR_size
- m0.PendSV
- m0.PopStack
- m0.ProcessorID
- m0.Push
- m0.PushStack
- m0.R
- m0.RName2num
- m0.RName_0
- m0.RName_1
- m0.RName_10
- m0.RName_11
- m0.RName_12
- m0.RName_2
- m0.RName_3
- m0.RName_4
- m0.RName_5
- m0.RName_6
- m0.RName_7
- m0.RName_8
- m0.RName_9
- m0.RName_CASE
- m0.RName_LR
- m0.RName_PC
- m0.RName_SP_main
- m0.RName_SP_process
- m0.RName_size
- m0.ROR
- m0.ROR_C
- m0.RRX
- m0.RRX_C
- m0.Raise
- m0.Register
- m0.Reset
- m0.ReturnAddress
- m0.Run
- m0.SHPR2_CASE
- m0.SHPR2_PRI_11
- m0.SHPR2_PRI_11_fupd
- m0.SHPR2_shpr2'rst
- m0.SHPR2_shpr2'rst_fupd
- m0.SHPR2_size
- m0.SHPR3_CASE
- m0.SHPR3_PRI_14
- m0.SHPR3_PRI_14_fupd
- m0.SHPR3_PRI_15
- m0.SHPR3_PRI_15_fupd
- m0.SHPR3_shpr3'rst
- m0.SHPR3_shpr3'rst_fupd
- m0.SHPR3_size
- m0.SP
- m0.SP_main
- m0.SP_process
- m0.SRType2num
- m0.SRType_ASR
- m0.SRType_CASE
- m0.SRType_LSL
- m0.SRType_LSR
- m0.SRType_ROR
- m0.SRType_RRX
- m0.SRType_size
- m0.SVCall
- m0.SendEvent
- m0.Shift
- m0.ShiftImmediate
- m0.ShiftRegister
- m0.Shift_C
- m0.SignExtendFrom
- m0.Store
- m0.StoreByte
- m0.StoreHalf
- m0.StoreMultiple
- m0.StoreWord
- m0.Store_CASE
- m0.Store_size
- m0.SupervisorCall
- m0.SysTick
- m0.System
- m0.System_CASE
- m0.System_size
- m0.TakeReset
- m0.TestCompareRegister
- m0.Thumb
- m0.Thumb2
- m0.UInt
- m0.UNPREDICTABLE
- m0.Undefined
- m0.WaitForEvent
- m0.WaitForInterrupt
- m0.Yield
- m0
Theorems
⊦ ¬(m0.Mode_Thread = m0.Mode_Handler)
⊦ m0.Mode_Thread = m0.num2Mode 0
⊦ m0.RName_0 = m0.num2RName 0
⊦ m0.SRType_LSL = m0.num2SRType 0
⊦ m0.Mode_Handler = m0.num2Mode 1
⊦ m0.RName_1 = m0.num2RName 1
⊦ m0.RName_2 = m0.num2RName (arithmetic.BIT2 0)
⊦ m0.SRType_ASR = m0.num2SRType (arithmetic.BIT2 0)
⊦ m0.SRType_LSR = m0.num2SRType 1
⊦ ∀x. m0.Mode_size x = 0
⊦ ∀x. m0.RName_size x = 0
⊦ ∀x. m0.SRType_size x = 0
⊦ m0.RName_3 = m0.num2RName 3
⊦ m0.RName_4 = m0.num2RName (arithmetic.BIT2 1)
⊦ m0.RName_5 = m0.num2RName (bit1 (arithmetic.BIT2 0))
⊦ m0.RName_6 = m0.num2RName (arithmetic.BIT2 (arithmetic.BIT2 0))
⊦ m0.SRType_ROR = m0.num2SRType 3
⊦ m0.SRType_RRX = m0.num2SRType (arithmetic.BIT2 1)
⊦ ∀_. m0.ProcessorID _ = integer.int_of_num 0
⊦ ∀a. m0.num2Mode (m0.Mode2num a) = a
⊦ ∀a. m0.num2RName (m0.RName2num a) = a
⊦ ∀a. m0.num2SRType (m0.SRType2num a) = a
⊦ ∀w. m0.bitify4 (m0.boolify4 w) = w
⊦ ∀x. m0.boolify4 (m0.bitify4 x) = x
⊦ ∀w. m0.bitify16 (m0.boolify16 w) = w
⊦ ∀x. m0.boolify16 (m0.bitify16 x) = x
⊦ ∀_. m0.ReturnAddress _ = λstate. m0.PC state
⊦ ∀x. ∃p. x = m0.Multiply32 p
⊦ m0.RName_10 = m0.num2RName (arithmetic.BIT2 (arithmetic.BIT2 1))
⊦ m0.RName_11 = m0.num2RName (bit1 (bit1 (arithmetic.BIT2 0)))
⊦ m0.RName_12 = m0.num2RName (arithmetic.BIT2 (bit1 (arithmetic.BIT2 0)))
⊦ m0.RName_7 = m0.num2RName 7
⊦ m0.RName_8 = m0.num2RName (arithmetic.BIT2 3)
⊦ m0.RName_9 = m0.num2RName (bit1 (arithmetic.BIT2 1))
⊦ m0.RName_SP_main =
m0.num2RName (bit1 (arithmetic.BIT2 (arithmetic.BIT2 0)))
⊦ m0.RName_SP_process =
m0.num2RName (arithmetic.BIT2 (arithmetic.BIT2 (arithmetic.BIT2 0)))
⊦ ∀state. m0.SP_main state = m0.m0_state_REG state m0.RName_SP_main
⊦ ∀state. m0.SP_process state = m0.m0_state_REG state m0.RName_SP_process
⊦ ∀w. m0.UInt w = integer.int_of_num (words.w2n w)
⊦ ∀w. m0.LowestSetBit w = m0.CountLeadingZeroBits (words.word_reverse w)
⊦ ∀_. m0.CallSupervisor _ = λstate. m0.Raise m0.SVCall state
⊦ ∀imm32. m0.dfn'Undefined imm32 = λstate. m0.Raise m0.HardFault state
⊦ ∀address. m0.ALUWritePC address = λstate. m0.BranchWritePC address state
⊦ ∀address. m0.BranchTo address = λstate. m0.write'PC address state
⊦ ∀address. m0.LoadWritePC address = λstate. m0.BXWritePC address state
⊦ m0.RName_LR = m0.num2RName 15
⊦ m0.RName_PC = m0.num2RName (arithmetic.BIT2 7)
⊦ ∀a. a = m0.Mode_Thread ∨ a = m0.Mode_Handler
⊦ ∀b c. m0.PRIMASK_PM (m0.recordtype.PRIMASK b c) ⇔ b
⊦ ∀b c. m0.PRIMASK_primask'rst (m0.recordtype.PRIMASK b c) = c
⊦ ∀c c0. m0.SHPR2_PRI_11 (m0.recordtype.SHPR2 c c0) = c
⊦ ∀c c0. m0.SHPR2_shpr2'rst (m0.recordtype.SHPR2 c c0) = c0
⊦ ∀a' a. ¬(m0.immediate_form a = m0.register_form a')
⊦ ∀address.
m0.mem1 address = λstate. bitstring.w2v (m0.m0_state_MEM state address)
⊦ ∀a' a. ¬(m0.Thumb a = m0.Thumb2 a')
⊦ ∀x. ∃b c. x = m0.recordtype.PRIMASK b c
⊦ ∀x. ∃c c0. x = m0.recordtype.SHPR2 c c0
⊦ ∀_ x. m0.write'reg'AIRCR (_, x) = m0.rec'AIRCR x
⊦ ∀e. m0.Raise e = λstate. m0.m0_state_pending_fupd (const (some e)) state
⊦ ∀_ x. m0.write'reg'CCR (_, x) = m0.rec'CCR x
⊦ ∀_ x. m0.write'reg'CONTROL (_, x) = m0.rec'CONTROL x
⊦ ∀_ x. m0.write'reg'IPR (_, x) = m0.rec'IPR x
⊦ ∀_ x. m0.write'reg'PRIMASK (_, x) = m0.rec'PRIMASK x
⊦ ∀_ x. m0.write'reg'PSR (_, x) = m0.rec'PSR x
⊦ ∀_ x. m0.write'reg'SHPR2 (_, x) = m0.rec'SHPR2 x
⊦ ∀_ x. m0.write'reg'SHPR3 (_, x) = m0.rec'SHPR3 x
⊦ ∀a0 a1. m0.SHPR2_size (m0.recordtype.SHPR2 a0 a1) = 1
⊦ ∀_ x. m0.write'rec'CONTROL (_, x) = m0.reg'CONTROL x
⊦ ∀_ x. m0.write'rec'AIRCR (_, x) = m0.reg'AIRCR x
⊦ ∀_ x. m0.write'rec'CCR (_, x) = m0.reg'CCR x
⊦ ∀_ x. m0.write'rec'IPR (_, x) = m0.reg'IPR x
⊦ ∀_ x. m0.write'rec'PRIMASK (_, x) = m0.reg'PRIMASK x
⊦ ∀_ x. m0.write'rec'PSR (_, x) = m0.reg'PSR x
⊦ ∀_ x. m0.write'rec'SHPR2 (_, x) = m0.reg'SHPR2 x
⊦ ∀_ x. m0.write'rec'SHPR3 (_, x) = m0.reg'SHPR3 x
⊦ ∀a f. m0.Multiply_CASE (m0.Multiply32 a) f = f a
⊦ m0.num2Mode 0 = m0.Mode_Thread ∧ m0.num2Mode 1 = m0.Mode_Handler
⊦ m0.Mode2num m0.Mode_Thread = 0 ∧ m0.Mode2num m0.Mode_Handler = 1
⊦ ∀x.
m0.reg'SHPR2 x =
m0.SHPR2_CASE x (λPRI_11 shpr2'rst. words.word_concat PRI_11 shpr2'rst)
⊦ ∀P. (∀a. P (m0.Multiply32 a)) ⇒ ∀x. P x
⊦ ∀w. m0.IsOnes w ⇔ w = words.word_2comp (words.n2w 1)
⊦ ∀f. ∃fn. ∀a. fn (m0.Multiply32 a) = f a
⊦ ∀_.
m0.LookUpSP _ =
λstate.
if m0.CONTROL_SPSEL (m0.m0_state_CONTROL state) then
m0.RName_SP_process
else m0.RName_SP_main
⊦ ∀P. P m0.Mode_Handler ∧ P m0.Mode_Thread ⇒ ∀a. P a
⊦ ∀b b0 b1. m0.CONTROL_SPSEL (m0.recordtype.CONTROL b b0 b1) ⇔ b
⊦ ∀b b0 b1. m0.CONTROL_control'rst (m0.recordtype.CONTROL b b0 b1) ⇔ b0
⊦ ∀b b0 b1. m0.CONTROL_nPRIV (m0.recordtype.CONTROL b b0 b1) ⇔ b1
⊦ ∀b b0 c. m0.CCR_STKALIGN (m0.recordtype.CCR b b0 c) ⇔ b
⊦ ∀b b0 c. m0.CCR_UNALIGN_TRP (m0.recordtype.CCR b b0 c) ⇔ b0
⊦ ∀b b0 c. m0.CCR_ccr'rst (m0.recordtype.CCR b b0 c) = c
⊦ ∀state.
m0.LR state =
m0.R
(words.n2w (arithmetic.BIT2 (arithmetic.BIT2 (arithmetic.BIT2 0))))
state
⊦ ∀state.
m0.SP state =
m0.R (words.n2w (bit1 (arithmetic.BIT2 (arithmetic.BIT2 0)))) state
⊦ ∀r. r < arithmetic.BIT2 0 ⇔ m0.Mode2num (m0.num2Mode r) = r
⊦ ∀c c0 c1. m0.SHPR3_PRI_14 (m0.recordtype.SHPR3 c c0 c1) = c
⊦ ∀c c0 c1. m0.SHPR3_PRI_15 (m0.recordtype.SHPR3 c c0 c1) = c0
⊦ ∀c c0 c1. m0.SHPR3_shpr3'rst (m0.recordtype.SHPR3 c c0 c1) = c1
⊦ ∀x. ∃b b0 c. x = m0.recordtype.CCR b b0 c
⊦ ∀x. ∃b b0 b1. x = m0.recordtype.CONTROL b b0 b1
⊦ ∀a a'. a = a' ⇔ m0.Mode2num a = m0.Mode2num a'
⊦ ∀a a'. m0.Mode2num a = m0.Mode2num a' ⇔ a = a'
⊦ ∀a. ∃r. a = m0.num2Mode r ∧ r < arithmetic.BIT2 0
⊦ ∀a a'. a = a' ⇔ m0.RName2num a = m0.RName2num a'
⊦ ∀a a'. m0.RName2num a = m0.RName2num a' ⇔ a = a'
⊦ ∀x. ∃c c0 c1. x = m0.recordtype.SHPR3 c c0 c1
⊦ ∀a a'. a = a' ⇔ m0.SRType2num a = m0.SRType2num a'
⊦ ∀a a'. m0.SRType2num a = m0.SRType2num a' ⇔ a = a'
⊦ ∀r. r < arithmetic.BIT2 0 ⇔ ∃a. r = m0.Mode2num a
⊦ ∀a a'. m0.ExternalInterrupt a = m0.ExternalInterrupt a' ⇔ a = a'
⊦ ∀a a'. m0.Multiply32 a = m0.Multiply32 a' ⇔ a = a'
⊦ ∀state. m0.PC state = m0.R (words.n2w 15) state
⊦ ∀r. r < bit1 (arithmetic.BIT2 0) ⇔ m0.SRType2num (m0.num2SRType r) = r
⊦ ∀a0 a1 a2. m0.SHPR3_size (m0.recordtype.SHPR3 a0 a1 a2) = 1
⊦ ∀a0 a1.
m0.PRIMASK_size (m0.recordtype.PRIMASK a0 a1) =
1 + basicSize.bool_size a0
⊦ ∀_.
m0.IncPC _ =
λstate.
m0.BranchTo
(words.word_add (m0.m0_state_REG state m0.RName_PC)
(m0.m0_state_pcinc state)) state
⊦ ∀a. ∃r. a = m0.num2SRType r ∧ r < bit1 (arithmetic.BIT2 0)
⊦ ∀r. r < bit1 (arithmetic.BIT2 0) ⇔ ∃a. r = m0.SRType2num a
⊦ ∀P. (∀a0 a1. P (m0.recordtype.PRIMASK a0 a1)) ⇒ ∀x. P x
⊦ ∀P. (∀a0 a1. P (m0.recordtype.SHPR2 a0 a1)) ⇒ ∀x. P x
⊦ ∀x carry_in. m0.RRX (x, carry_in) = fst (m0.RRX_C (x, carry_in))
⊦ ∀ReturningExceptionNumber.
m0.DeActivate ReturningExceptionNumber =
λstate.
m0.m0_state_ExceptionActive_fupd
(const
(combin.UPDATE ReturningExceptionNumber ⊥
(m0.m0_state_ExceptionActive state))) state
⊦ ∀value.
m0.write'PC value =
λstate.
m0.m0_state_REG_fupd
(const (combin.UPDATE m0.RName_PC value (m0.m0_state_REG state)))
state
⊦ ∀value.
m0.write'SP_main value =
λstate.
m0.m0_state_REG_fupd
(const
(combin.UPDATE m0.RName_SP_main value (m0.m0_state_REG state)))
state
⊦ ∀value.
m0.write'SP_process value =
λstate.
m0.m0_state_REG_fupd
(const
(combin.UPDATE m0.RName_SP_process value
(m0.m0_state_REG state))) state
⊦ ∀x0 x1. ∃f. f m0.Mode_Thread = x0 ∧ f m0.Mode_Handler = x1
⊦ ∀a0 a1 f. m0.PRIMASK_CASE (m0.recordtype.PRIMASK a0 a1) f = f a0 a1
⊦ ∀x. (∃c. x = m0.immediate_form c) ∨ ∃c. x = m0.register_form c
⊦ ∀x. (∃c. x = m0.Thumb c) ∨ ∃p. x = m0.Thumb2 p
⊦ ∀P.
∃b c.
P =
m0.PRIMASK_PM_fupd (const b)
(m0.PRIMASK_primask'rst_fupd (const c) bool.ARB)
⊦ ∀x.
m0.reg'PRIMASK x =
m0.PRIMASK_CASE x
(λPM primask'rst.
words.word_concat primask'rst (bitstring.v2w (PM :: [])))
⊦ ∀S.
∃c0 c.
S =
m0.SHPR2_PRI_11_fupd (const c0)
(m0.SHPR2_shpr2'rst_fupd (const c) bool.ARB)
⊦ ∀a0 a1 f. m0.SHPR2_CASE (m0.recordtype.SHPR2 a0 a1) f = f a0 a1
⊦ ∀address size.
m0.MemU (address, size) = λstate. m0.MemA (address, size) state
⊦ ∀unsigned w.
m0.Extend (unsigned, w) =
if unsigned then words.w2w w else words.sw2sw w
⊦ ∀_.
m0.CurrentModeIsPrivileged _ =
λstate.
m0.m0_state_CurrentMode state = m0.Mode_Handler ∨
¬m0.CONTROL_nPRIV (m0.m0_state_CONTROL state)
⊦ ∀w n. m0.Aligned (w, n) ⇔ w = m0.Align (w, n)
⊦ ∀value.
m0.write'LR value =
λstate.
m0.write'R
(value,
words.n2w (arithmetic.BIT2 (arithmetic.BIT2 (arithmetic.BIT2 0))))
state
⊦ ∀value.
m0.write'SP value =
λstate.
m0.write'R
(value, words.n2w (bit1 (arithmetic.BIT2 (arithmetic.BIT2 0))))
state
⊦ ∀f. ∃fn. ∀a0 a1. fn (m0.recordtype.PRIMASK a0 a1) = f a0 a1
⊦ ∀f. ∃fn. ∀a0 a1. fn (m0.recordtype.SHPR2 a0 a1) = f a0 a1
⊦ ∀r. r < bit1 (arithmetic.BIT2 3) ⇔ m0.RName2num (m0.num2RName r) = r
⊦ ∀f b c.
m0.PRIMASK_PM_fupd f (m0.recordtype.PRIMASK b c) =
m0.recordtype.PRIMASK (f b) c
⊦ ∀f c c0.
m0.SHPR2_PRI_11_fupd f (m0.recordtype.SHPR2 c c0) =
m0.recordtype.SHPR2 (f c) c0
⊦ ∀f c c0.
m0.SHPR2_shpr2'rst_fupd f (m0.recordtype.SHPR2 c c0) =
m0.recordtype.SHPR2 c (f c0)
⊦ ∀f b c.
m0.PRIMASK_primask'rst_fupd f (m0.recordtype.PRIMASK b c) =
m0.recordtype.PRIMASK b (f c)
⊦ ∀a. ∃r. a = m0.num2RName r ∧ r < bit1 (arithmetic.BIT2 3)
⊦ ∀r. r < bit1 (arithmetic.BIT2 3) ⇔ ∃a. r = m0.RName2num a
⊦ ∀w n. m0.Align (w, n) = words.n2w (n * (words.w2n w div n))
⊦ ∀_.
m0.ExceptionEntry _ =
λstate.
option.option_CASE (m0.m0_state_pending state) state
(λe. m0.ExceptionTaken (m0.ExcNumber e) (m0.PushStack () state))
⊦ ∀g f P.
m0.PRIMASK_primask'rst_fupd f (m0.PRIMASK_PM_fupd g P) =
m0.PRIMASK_PM_fupd g (m0.PRIMASK_primask'rst_fupd f P)
⊦ ∀P. (∀a0 a1 a2. P (m0.recordtype.CCR a0 a1 a2)) ⇒ ∀x. P x
⊦ ∀P. (∀a0 a1 a2. P (m0.recordtype.CONTROL a0 a1 a2)) ⇒ ∀x. P x
⊦ ∀P. (∀a0 a1 a2. P (m0.recordtype.SHPR3 a0 a1 a2)) ⇒ ∀x. P x
⊦ ∀g f S.
m0.SHPR2_shpr2'rst_fupd f (m0.SHPR2_PRI_11_fupd g S) =
m0.SHPR2_PRI_11_fupd g (m0.SHPR2_shpr2'rst_fupd f S)
⊦ ∀P.
(∀a. P (m0.immediate_form a)) ∧ (∀a. P (m0.register_form a)) ⇒ ∀x. P x
⊦ ∀P. (∀a. P (m0.Thumb a)) ∧ (∀a. P (m0.Thumb2 a)) ⇒ ∀x. P x
⊦ ∀a.
m0.Multiply_size (m0.Multiply32 a) =
1 + basicSize.pair_size (λv. 0) (basicSize.pair_size (λv. 0) (λv. 0)) a
⊦ (∀a. m0.offset_size (m0.immediate_form a) = 1) ∧
∀a. m0.offset_size (m0.register_form a) = 1
⊦ ∀b b0 b1 c c0. m0.AIRCR_ENDIANNESS (m0.recordtype.AIRCR b b0 b1 c c0) ⇔ b
⊦ ∀b b0 b1 c c0.
m0.AIRCR_SYSRESETREQ (m0.recordtype.AIRCR b b0 b1 c c0) ⇔ b0
⊦ ∀b b0 b1 c c0.
m0.AIRCR_VECTCLRACTIVE (m0.recordtype.AIRCR b b0 b1 c c0) ⇔ b1
⊦ ∀b b0 b1 c c0. m0.AIRCR_aircr'rst (m0.recordtype.AIRCR b b0 b1 c c0) = c0
⊦ ∀b b0 b1 c c0. m0.AIRCR_VECTKEY (m0.recordtype.AIRCR b b0 b1 c c0) = c
⊦ ∀w.
m0.HighestSetBit w =
if w = words.n2w 0 then integer.int_neg (integer.int_of_num 1)
else integer_word.w2i (words.word_log2 w)
⊦ ∀w.
m0.CountLeadingZeroBits w =
integer.Num
(integer.int_sub
(integer.int_sub
(integer.int_of_num (words.word_len (words.n2w 0)))
(integer.int_of_num 1)) (m0.HighestSetBit w))
⊦ ∀c c0 c1 c2 c3. m0.IPR_PRI_N0 (m0.recordtype.IPR c c0 c1 c2 c3) = c
⊦ ∀c c0 c1 c2 c3. m0.IPR_PRI_N1 (m0.recordtype.IPR c c0 c1 c2 c3) = c0
⊦ ∀c c0 c1 c2 c3. m0.IPR_PRI_N2 (m0.recordtype.IPR c c0 c1 c2 c3) = c1
⊦ ∀c c0 c1 c2 c3. m0.IPR_PRI_N3 (m0.recordtype.IPR c c0 c1 c2 c3) = c2
⊦ ∀c c0 c1 c2 c3. m0.IPR_ipr'rst (m0.recordtype.IPR c c0 c1 c2 c3) = c3
⊦ ∀x.
m0.rec'CONTROL x =
m0.recordtype.CONTROL (words.word_bit 1 x)
(words.word_bit (arithmetic.BIT2 0) x) (words.word_bit 0 x)
⊦ ∀imm32.
m0.dfn'Breakpoint imm32 =
λstate.
bool.LET
(λs.
m0.m0_state_count_fupd (const (m0.m0_state_count s + bool.ARB))
s) (m0.IncPC () state)
⊦ ∀imm32.
m0.dfn'SupervisorCall imm32 =
λstate.
bool.LET
(λs.
m0.m0_state_count_fupd (const (m0.m0_state_count s + bool.ARB))
s) (m0.CallSupervisor () state)
⊦ ∀a0 a1 a2 f.
m0.CONTROL_CASE (m0.recordtype.CONTROL a0 a1 a2) f = f a0 a1 a2
⊦ ∀a0 a1 a2 f. m0.CCR_CASE (m0.recordtype.CCR a0 a1 a2) f = f a0 a1 a2
⊦ ∀e.
m0.raise'exception e =
λstate.
(bool.ARB,
(if m0.m0_state_exception state = m0.NoException then
m0.m0_state_exception_fupd (const e) state
else state))
⊦ ∀x. ∃b b0 b1 c c0. x = m0.recordtype.AIRCR b b0 b1 c c0
⊦ ∀x. ∃c c0 c1 c2 c3. x = m0.recordtype.IPR c c0 c1 c2 c3
⊦ ∀P0.
(∀P. P0 P) ⇔
∀b c.
P0
(m0.PRIMASK_PM_fupd (const b)
(m0.PRIMASK_primask'rst_fupd (const c) bool.ARB))
⊦ ∀P0.
(∃P. P0 P) ⇔
∃b c.
P0
(m0.PRIMASK_PM_fupd (const b)
(m0.PRIMASK_primask'rst_fupd (const c) bool.ARB))
⊦ ∀P.
(∀x. P x) ⇔
∀c0 c.
P
(m0.SHPR2_PRI_11_fupd (const c0)
(m0.SHPR2_shpr2'rst_fupd (const c) bool.ARB))
⊦ ∀P.
(∃x. P x) ⇔
∃c0 c.
P
(m0.SHPR2_PRI_11_fupd (const c0)
(m0.SHPR2_shpr2'rst_fupd (const c) bool.ARB))
⊦ ∀a0 a1 a2 f. m0.SHPR3_CASE (m0.recordtype.SHPR3 a0 a1 a2) f = f a0 a1 a2
⊦ ∀_.
m0.dfn'NoOperation _ =
λstate.
bool.LET
(λs. m0.m0_state_count_fupd (const (m0.m0_state_count s + 1)) s)
(m0.IncPC () state)
⊦ ∀_.
m0.dfn'SendEvent _ =
λstate.
bool.LET
(λs. m0.m0_state_count_fupd (const (m0.m0_state_count s + 1)) s)
(m0.IncPC () state)
⊦ ∀_.
m0.dfn'WaitForEvent _ =
λstate.
bool.LET
(λs.
m0.m0_state_count_fupd
(const (m0.m0_state_count s + arithmetic.BIT2 0)) s)
(m0.IncPC () state)
⊦ ∀_.
m0.dfn'WaitForInterrupt _ =
λstate.
bool.LET
(λs.
m0.m0_state_count_fupd
(const (m0.m0_state_count s + arithmetic.BIT2 0)) s)
(m0.IncPC () state)
⊦ ∀_.
m0.dfn'Yield _ =
λstate.
bool.LET
(λs. m0.m0_state_count_fupd (const (m0.m0_state_count s + 1)) s)
(m0.IncPC () state)
⊦ ∀x.
(∃s. x = m0.ASSERT s) ∨ x = m0.NoException ∨ ∃s. x = m0.UNPREDICTABLE s
⊦ ∀a0 a1 a2 a3 a4. m0.IPR_size (m0.recordtype.IPR a0 a1 a2 a3 a4) = 1
⊦ ∀f. ∃fn. ∀a0 a1 a2. fn (m0.recordtype.CONTROL a0 a1 a2) = f a0 a1 a2
⊦ ∀f. ∃fn. ∀a0 a1 a2. fn (m0.recordtype.CCR a0 a1 a2) = f a0 a1 a2
⊦ ∀f. ∃fn. ∀a0 a1 a2. fn (m0.recordtype.SHPR3 a0 a1 a2) = f a0 a1 a2
⊦ ∀C.
∃b0 b c.
C =
m0.CCR_STKALIGN_fupd (const b0)
(m0.CCR_UNALIGN_TRP_fupd (const b)
(m0.CCR_ccr'rst_fupd (const c) bool.ARB))
⊦ ∀C.
∃b1 b0 b.
C =
m0.CONTROL_SPSEL_fupd (const b1)
(m0.CONTROL_control'rst_fupd (const b0)
(m0.CONTROL_nPRIV_fupd (const b) bool.ARB))
⊦ ∀x v0 v1.
m0.Mode_CASE x v0 v1 =
let m ← m0.Mode2num x in if m = 0 then v0 else v1
⊦ ∀P1 P2.
P1 = P2 ⇔
(m0.PRIMASK_PM P1 ⇔ m0.PRIMASK_PM P2) ∧
m0.PRIMASK_primask'rst P1 = m0.PRIMASK_primask'rst P2
⊦ ∀S1 S2.
S1 = S2 ⇔
m0.SHPR2_PRI_11 S1 = m0.SHPR2_PRI_11 S2 ∧
m0.SHPR2_shpr2'rst S1 = m0.SHPR2_shpr2'rst S2
⊦ ∀S.
∃c1 c0 c.
S =
m0.SHPR3_PRI_14_fupd (const c1)
(m0.SHPR3_PRI_15_fupd (const c0)
(m0.SHPR3_shpr3'rst_fupd (const c) bool.ARB))
⊦ ∀f b b0 b1.
m0.CONTROL_SPSEL_fupd f (m0.recordtype.CONTROL b b0 b1) =
m0.recordtype.CONTROL (f b) b0 b1
⊦ ∀f b b0 b1.
m0.CONTROL_control'rst_fupd f (m0.recordtype.CONTROL b b0 b1) =
m0.recordtype.CONTROL b (f b0) b1
⊦ ∀f b b0 b1.
m0.CONTROL_nPRIV_fupd f (m0.recordtype.CONTROL b b0 b1) =
m0.recordtype.CONTROL b b0 (f b1)
⊦ ∀f b b0 c.
m0.CCR_STKALIGN_fupd f (m0.recordtype.CCR b b0 c) =
m0.recordtype.CCR (f b) b0 c
⊦ ∀f b b0 c.
m0.CCR_UNALIGN_TRP_fupd f (m0.recordtype.CCR b b0 c) =
m0.recordtype.CCR b (f b0) c
⊦ ∀f c c0 c1.
m0.SHPR3_PRI_14_fupd f (m0.recordtype.SHPR3 c c0 c1) =
m0.recordtype.SHPR3 (f c) c0 c1
⊦ ∀f c c0 c1.
m0.SHPR3_PRI_15_fupd f (m0.recordtype.SHPR3 c c0 c1) =
m0.recordtype.SHPR3 c (f c0) c1
⊦ ∀f c c0 c1.
m0.SHPR3_shpr3'rst_fupd f (m0.recordtype.SHPR3 c c0 c1) =
m0.recordtype.SHPR3 c c0 (f c1)
⊦ ∀f b b0 c.
m0.CCR_ccr'rst_fupd f (m0.recordtype.CCR b b0 c) =
m0.recordtype.CCR b b0 (f c)
⊦ ∀a0 a1 a2.
m0.CCR_size (m0.recordtype.CCR a0 a1 a2) =
1 + (basicSize.bool_size a0 + basicSize.bool_size a1)
⊦ ∀state.
m0.Next state =
bool.LET
(pair.UNCURRY
(λv s.
bool.LET (pair.UNCURRY (λv s. m0.Run v s)) (m0.Decode v s)))
(m0.Fetch state)
⊦ ∀option.
m0.dfn'DataMemoryBarrier option =
λstate.
bool.LET
(λs.
m0.m0_state_count_fupd
(const (m0.m0_state_count s + arithmetic.BIT2 1)) s)
(m0.IncPC () state)
⊦ ∀option.
m0.dfn'DataSynchronizationBarrier option =
λstate.
bool.LET
(λs.
m0.m0_state_count_fupd
(const (m0.m0_state_count s + arithmetic.BIT2 1)) s)
(m0.IncPC () state)
⊦ ∀option.
m0.dfn'InstructionSynchronizationBarrier option =
λstate.
bool.LET
(λs.
m0.m0_state_count_fupd
(const (m0.m0_state_count s + arithmetic.BIT2 1)) s)
(m0.IncPC () state)
⊦ ∀x.
m0.rec'PRIMASK x =
m0.recordtype.PRIMASK (words.word_bit 0 x) (words.word_extract 31 1 x)
⊦ ∀P.
(∀a. P (m0.ASSERT a)) ∧ P m0.NoException ∧
(∀a. P (m0.UNPREDICTABLE a)) ⇒ ∀x. P x
⊦ ∀value address size.
m0.write'MemU (value, address, size) =
λstate. m0.write'MemA (value, address, size) state
⊦ (∀v0 v1. m0.Mode_CASE m0.Mode_Thread v0 v1 = v0) ∧
∀v0 v1. m0.Mode_CASE m0.Mode_Handler v0 v1 = v1
⊦ (∀b c. m0.PRIMASK_PM (m0.recordtype.PRIMASK b c) ⇔ b) ∧
∀b c. m0.PRIMASK_primask'rst (m0.recordtype.PRIMASK b c) = c
⊦ (∀c c0. m0.SHPR2_PRI_11 (m0.recordtype.SHPR2 c c0) = c) ∧
∀c c0. m0.SHPR2_shpr2'rst (m0.recordtype.SHPR2 c c0) = c0
⊦ ∀P b c.
m0.PRIMASK_PM_fupd (const b)
(m0.PRIMASK_primask'rst_fupd (const c) P) =
m0.PRIMASK_PM_fupd (const b)
(m0.PRIMASK_primask'rst_fupd (const c) bool.ARB)
⊦ ∀S c0 c.
m0.SHPR2_PRI_11_fupd (const c0) (m0.SHPR2_shpr2'rst_fupd (const c) S) =
m0.SHPR2_PRI_11_fupd (const c0)
(m0.SHPR2_shpr2'rst_fupd (const c) bool.ARB)
⊦ ∀w p.
m0.SignExtendFrom (w, p) =
bool.LET (λs. words.word_asr (words.word_lsl w s) s)
(arithmetic.- (words.word_len (words.n2w 0)) p)
⊦ ∀P.
P m0.SRType_ASR ∧ P m0.SRType_LSL ∧ P m0.SRType_LSR ∧ P m0.SRType_ROR ∧
P m0.SRType_RRX ⇒ ∀a. P a
⊦ ∀address.
m0.BranchWritePC address =
λstate.
m0.BranchTo
(words.word_concat (words.word_extract 31 1 address) (words.n2w 0))
state
⊦ ∀a.
a = m0.SRType_LSL ∨ a = m0.SRType_LSR ∨ a = m0.SRType_ASR ∨
a = m0.SRType_ROR ∨ a = m0.SRType_RRX
⊦ ∀P. (∀a0 a1 a2 a3 a4. P (m0.recordtype.AIRCR a0 a1 a2 a3 a4)) ⇒ ∀x. P x
⊦ ∀P. (∀a0 a1 a2 a3 a4. P (m0.recordtype.IPR a0 a1 a2 a3 a4)) ⇒ ∀x. P x
⊦ ∀m.
m0.dfn'BranchExchange m =
λstate.
bool.LET
(λs. m0.m0_state_count_fupd (const (m0.m0_state_count s + 3)) s)
(m0.BXWritePC (m0.R m state) state)
⊦ ∀f0 f1. ∃fn. (∀a. fn (m0.Thumb a) = f0 a) ∧ ∀a. fn (m0.Thumb2 a) = f1 a
⊦ ∀f0 f1.
∃fn.
(∀a. fn (m0.immediate_form a) = f0 a) ∧
∀a. fn (m0.register_form a) = f1 a
⊦ (∀a. m0.num2Mode (m0.Mode2num a) = a) ∧
∀r.
(let n ← r in n < arithmetic.BIT2 0) ⇔ m0.Mode2num (m0.num2Mode r) = r
⊦ ∀a0 a1 a0' a1'.
m0.recordtype.PRIMASK a0 a1 = m0.recordtype.PRIMASK a0' a1' ⇔
(a0 ⇔ a0') ∧ a1 = a1'
⊦ ∀a0 a1 a0' a1'.
m0.recordtype.SHPR2 a0 a1 = m0.recordtype.SHPR2 a0' a1' ⇔
a0 = a0' ∧ a1 = a1'
⊦ ∀a0 a1 a2.
m0.CONTROL_size (m0.recordtype.CONTROL a0 a1 a2) =
1 +
(basicSize.bool_size a0 +
(basicSize.bool_size a1 + basicSize.bool_size a2))
⊦ ∀b c b0 b1 b2 b3 c0. m0.PSR_C (m0.recordtype.PSR b c b0 b1 b2 b3 c0) ⇔ b
⊦ ∀b c b0 b1 b2 b3 c0. m0.PSR_N (m0.recordtype.PSR b c b0 b1 b2 b3 c0) ⇔ b0
⊦ ∀b c b0 b1 b2 b3 c0. m0.PSR_T (m0.recordtype.PSR b c b0 b1 b2 b3 c0) ⇔ b1
⊦ ∀b c b0 b1 b2 b3 c0. m0.PSR_V (m0.recordtype.PSR b c b0 b1 b2 b3 c0) ⇔ b2
⊦ ∀b c b0 b1 b2 b3 c0. m0.PSR_Z (m0.recordtype.PSR b c b0 b1 b2 b3 c0) ⇔ b3
⊦ ∀b c b0 b1 b2 b3 c0.
m0.PSR_ExceptionNumber (m0.recordtype.PSR b c b0 b1 b2 b3 c0) = c
⊦ ∀b c b0 b1 b2 b3 c0.
m0.PSR_psr'rst (m0.recordtype.PSR b c b0 b1 b2 b3 c0) = c0
⊦ ∀P.
(∀x. P x) ⇔
∀b0 b c.
P
(m0.CCR_STKALIGN_fupd (const b0)
(m0.CCR_UNALIGN_TRP_fupd (const b)
(m0.CCR_ccr'rst_fupd (const c) bool.ARB)))
⊦ ∀P.
(∃x. P x) ⇔
∃b0 b c.
P
(m0.CCR_STKALIGN_fupd (const b0)
(m0.CCR_UNALIGN_TRP_fupd (const b)
(m0.CCR_ccr'rst_fupd (const c) bool.ARB)))
⊦ ∀P.
(∀x. P x) ⇔
∀b1 b0 b.
P
(m0.CONTROL_SPSEL_fupd (const b1)
(m0.CONTROL_control'rst_fupd (const b0)
(m0.CONTROL_nPRIV_fupd (const b) bool.ARB)))
⊦ ∀P.
(∃x. P x) ⇔
∃b1 b0 b.
P
(m0.CONTROL_SPSEL_fupd (const b1)
(m0.CONTROL_control'rst_fupd (const b0)
(m0.CONTROL_nPRIV_fupd (const b) bool.ARB)))
⊦ ∀P.
(∀x. P x) ⇔
∀c1 c0 c.
P
(m0.SHPR3_PRI_14_fupd (const c1)
(m0.SHPR3_PRI_15_fupd (const c0)
(m0.SHPR3_shpr3'rst_fupd (const c) bool.ARB)))
⊦ ∀P.
(∃x. P x) ⇔
∃c1 c0 c.
P
(m0.SHPR3_PRI_14_fupd (const c1)
(m0.SHPR3_PRI_15_fupd (const c0)
(m0.SHPR3_shpr3'rst_fupd (const c) bool.ARB)))
⊦ ∀imm32.
m0.dfn'BranchTarget imm32 =
λstate.
bool.LET
(λs. m0.m0_state_count_fupd (const (m0.m0_state_count s + 3)) s)
(m0.BranchWritePC (words.word_add (m0.PC state) imm32) state)
⊦ (∀a. m0.num2SRType (m0.SRType2num a) = a) ∧
∀r.
(let n ← r in n < bit1 (arithmetic.BIT2 0)) ⇔
m0.SRType2num (m0.num2SRType r) = r
⊦ ∀x.
m0.reg'CONTROL x =
m0.CONTROL_CASE x
(λSPSEL control'rst nPRIV.
words.word_concat (bitstring.v2w (control'rst :: []))
(words.word_concat (bitstring.v2w (SPSEL :: []))
(bitstring.v2w (nPRIV :: []))))
⊦ ∀x. ∃b c b0 b1 b2 b3 c0. x = m0.recordtype.PSR b c b0 b1 b2 b3 c0
⊦ ∀r r'.
r < arithmetic.BIT2 0 ⇒ r' < arithmetic.BIT2 0 ⇒
(m0.num2Mode r = m0.num2Mode r' ⇔ r = r')
⊦ (∀a. m0.MachineCode_size (m0.Thumb a) = 1) ∧
∀a.
m0.MachineCode_size (m0.Thumb2 a) =
1 + basicSize.pair_size (λv. 0) (λv. 0) a
⊦ ∀w.
m0.boolify4 w =
(words.word_bit 3 w, words.word_bit (arithmetic.BIT2 0) w,
words.word_bit 1 w, words.word_bit 0 w)
⊦ (∀a. m0.num2RName (m0.RName2num a) = a) ∧
∀r.
(let n ← r in n < bit1 (arithmetic.BIT2 3)) ⇔
m0.RName2num (m0.num2RName r) = r
⊦ ∀a0 a1 a2 a3 a4 f.
m0.AIRCR_CASE (m0.recordtype.AIRCR a0 a1 a2 a3 a4) f = f a0 a1 a2 a3 a4
⊦ ∀C1 C2.
C1 = C2 ⇔
(m0.CCR_STKALIGN C1 ⇔ m0.CCR_STKALIGN C2) ∧
(m0.CCR_UNALIGN_TRP C1 ⇔ m0.CCR_UNALIGN_TRP C2) ∧
m0.CCR_ccr'rst C1 = m0.CCR_ccr'rst C2
⊦ ∀C1 C2.
C1 = C2 ⇔
(m0.CONTROL_SPSEL C1 ⇔ m0.CONTROL_SPSEL C2) ∧
(m0.CONTROL_control'rst C1 ⇔ m0.CONTROL_control'rst C2) ∧
(m0.CONTROL_nPRIV C1 ⇔ m0.CONTROL_nPRIV C2)
⊦ ∀S1 S2.
S1 = S2 ⇔
m0.SHPR3_PRI_14 S1 = m0.SHPR3_PRI_14 S2 ∧
m0.SHPR3_PRI_15 S1 = m0.SHPR3_PRI_15 S2 ∧
m0.SHPR3_shpr3'rst S1 = m0.SHPR3_shpr3'rst S2
⊦ ∀r r'.
r < bit1 (arithmetic.BIT2 0) ⇒ r' < bit1 (arithmetic.BIT2 0) ⇒
(m0.num2SRType r = m0.num2SRType r' ⇔ r = r')
⊦ ∀a0 a1 a2 a3 a4 f.
m0.IPR_CASE (m0.recordtype.IPR a0 a1 a2 a3 a4) f = f a0 a1 a2 a3 a4
⊦ (∀a. ¬(m0.ASSERT a = m0.NoException)) ∧
(∀a' a. ¬(m0.ASSERT a = m0.UNPREDICTABLE a')) ∧
∀a. ¬(m0.NoException = m0.UNPREDICTABLE a)
⊦ ∀f.
∃fn.
∀a0 a1 a2 a3 a4.
fn (m0.recordtype.AIRCR a0 a1 a2 a3 a4) = f a0 a1 a2 a3 a4
⊦ ∀f.
∃fn.
∀a0 a1 a2 a3 a4.
fn (m0.recordtype.IPR a0 a1 a2 a3 a4) = f a0 a1 a2 a3 a4
⊦ ∀b3 b2 b1 b0.
m0.bitify4 (b3, b2, b1, b0) =
bitstring.v2w (b3 :: b2 :: b1 :: b0 :: [])
⊦ ∀b3 b2 b1 b0.
m0.boolify4 (bitstring.v2w (b3 :: b2 :: b1 :: b0 :: [])) =
(b3, b2, b1, b0)
⊦ ∀mc.
m0.Decode mc =
λstate.
m0.MachineCode_CASE mc
(λh.
m0.DecodeThumb h
(m0.m0_state_pcinc_fupd
(const (words.n2w (arithmetic.BIT2 0))) state))
(λhs.
m0.DecodeThumb2 hs
(m0.m0_state_pcinc_fupd
(const (words.n2w (arithmetic.BIT2 1))) state))
⊦ ∀f b b0 b1 c c0.
m0.AIRCR_ENDIANNESS_fupd f (m0.recordtype.AIRCR b b0 b1 c c0) =
m0.recordtype.AIRCR (f b) b0 b1 c c0
⊦ ∀f b b0 b1 c c0.
m0.AIRCR_SYSRESETREQ_fupd f (m0.recordtype.AIRCR b b0 b1 c c0) =
m0.recordtype.AIRCR b (f b0) b1 c c0
⊦ ∀f b b0 b1 c c0.
m0.AIRCR_VECTCLRACTIVE_fupd f (m0.recordtype.AIRCR b b0 b1 c c0) =
m0.recordtype.AIRCR b b0 (f b1) c c0
⊦ ∀f c c0 c1 c2 c3.
m0.IPR_PRI_N0_fupd f (m0.recordtype.IPR c c0 c1 c2 c3) =
m0.recordtype.IPR (f c) c0 c1 c2 c3
⊦ ∀f c c0 c1 c2 c3.
m0.IPR_PRI_N1_fupd f (m0.recordtype.IPR c c0 c1 c2 c3) =
m0.recordtype.IPR c (f c0) c1 c2 c3
⊦ ∀f c c0 c1 c2 c3.
m0.IPR_PRI_N2_fupd f (m0.recordtype.IPR c c0 c1 c2 c3) =
m0.recordtype.IPR c c0 (f c1) c2 c3
⊦ ∀f c c0 c1 c2 c3.
m0.IPR_PRI_N3_fupd f (m0.recordtype.IPR c c0 c1 c2 c3) =
m0.recordtype.IPR c c0 c1 (f c2) c3
⊦ ∀f b b0 b1 c c0.
m0.AIRCR_aircr'rst_fupd f (m0.recordtype.AIRCR b b0 b1 c c0) =
m0.recordtype.AIRCR b b0 b1 c (f c0)
⊦ ∀f b b0 b1 c c0.
m0.AIRCR_VECTKEY_fupd f (m0.recordtype.AIRCR b b0 b1 c c0) =
m0.recordtype.AIRCR b b0 b1 (f c) c0
⊦ ∀f c c0 c1 c2 c3.
m0.IPR_ipr'rst_fupd f (m0.recordtype.IPR c c0 c1 c2 c3) =
m0.recordtype.IPR c c0 c1 c2 (f c3)
⊦ (∀a a'. m0.ASSERT a = m0.ASSERT a' ⇔ a = a') ∧
∀a a'. m0.UNPREDICTABLE a = m0.UNPREDICTABLE a' ⇔ a = a'
⊦ (∀a a'. m0.Thumb a = m0.Thumb a' ⇔ a = a') ∧
∀a a'. m0.Thumb2 a = m0.Thumb2 a' ⇔ a = a'
⊦ (∀a a'. m0.immediate_form a = m0.immediate_form a' ⇔ a = a') ∧
∀a a'. m0.register_form a = m0.register_form a' ⇔ a = a'
⊦ ∀P.
(∀a0 a1 a2 a3 a4 a5 a6. P (m0.recordtype.PSR a0 a1 a2 a3 a4 a5 a6)) ⇒
∀x. P x
⊦ ∀opc.
m0.ArithmeticOpcode opc ⇔
(words.word_bit (arithmetic.BIT2 0) opc ∨ words.word_bit 1 opc) ∧
¬(words.word_bit 3 opc ∧ words.word_bit (arithmetic.BIT2 0) opc)
⊦ (∀a f f1. m0.MachineCode_CASE (m0.Thumb a) f f1 = f a) ∧
∀a f f1. m0.MachineCode_CASE (m0.Thumb2 a) f f1 = f1 a
⊦ (∀a f f1. m0.offset_CASE (m0.immediate_form a) f f1 = f a) ∧
∀a f f1. m0.offset_CASE (m0.register_form a) f f1 = f1 a
⊦ ∀a0 a1 a2 a3 a4.
m0.AIRCR_size (m0.recordtype.AIRCR a0 a1 a2 a3 a4) =
1 +
(basicSize.bool_size a0 +
(basicSize.bool_size a1 + basicSize.bool_size a2))
⊦ ∀x.
(∃c. x = m0.BranchExchange c) ∨
(∃c. x = m0.BranchLinkExchangeRegister c) ∨
(∃c. x = m0.BranchLinkImmediate c) ∨ ∃c. x = m0.BranchTarget c
⊦ ∀x.
(∃b. x = m0.ChangeProcessorState b) ∨
(∃p. x = m0.MoveToRegisterFromSpecial p) ∨
(∃p. x = m0.MoveToSpecialRegister p) ∨ ∃c. x = m0.SupervisorCall c
⊦ ∀x.
m0.rec'SHPR2 x =
m0.recordtype.SHPR2
(words.word_extract 31
(arithmetic.BIT2
(arithmetic.BIT2 (arithmetic.BIT2 (arithmetic.BIT2 0)))) x)
(words.word_extract
(bit1 (arithmetic.BIT2 (arithmetic.BIT2 (arithmetic.BIT2 0)))) 0
x)
⊦ ∀A.
∃b1 b0 b c0 c.
A =
m0.AIRCR_ENDIANNESS_fupd (const b1)
(m0.AIRCR_SYSRESETREQ_fupd (const b0)
(m0.AIRCR_VECTCLRACTIVE_fupd (const b)
(m0.AIRCR_VECTKEY_fupd (const c0)
(m0.AIRCR_aircr'rst_fupd (const c) bool.ARB))))
⊦ ∀C b0 b c.
m0.CCR_STKALIGN_fupd (const b0)
(m0.CCR_UNALIGN_TRP_fupd (const b)
(m0.CCR_ccr'rst_fupd (const c) C)) =
m0.CCR_STKALIGN_fupd (const b0)
(m0.CCR_UNALIGN_TRP_fupd (const b)
(m0.CCR_ccr'rst_fupd (const c) bool.ARB))
⊦ ∀C b1 b0 b.
m0.CONTROL_SPSEL_fupd (const b1)
(m0.CONTROL_control'rst_fupd (const b0)
(m0.CONTROL_nPRIV_fupd (const b) C)) =
m0.CONTROL_SPSEL_fupd (const b1)
(m0.CONTROL_control'rst_fupd (const b0)
(m0.CONTROL_nPRIV_fupd (const b) bool.ARB))
⊦ ∀I.
∃c3 c2 c1 c0 c.
I =
m0.IPR_PRI_N0_fupd (const c3)
(m0.IPR_PRI_N1_fupd (const c2)
(m0.IPR_PRI_N2_fupd (const c1)
(m0.IPR_PRI_N3_fupd (const c0)
(m0.IPR_ipr'rst_fupd (const c) bool.ARB))))
⊦ ∀S c1 c0 c.
m0.SHPR3_PRI_14_fupd (const c1)
(m0.SHPR3_PRI_15_fupd (const c0)
(m0.SHPR3_shpr3'rst_fupd (const c) S)) =
m0.SHPR3_PRI_14_fupd (const c1)
(m0.SHPR3_PRI_15_fupd (const c0)
(m0.SHPR3_shpr3'rst_fupd (const c) bool.ARB))
⊦ ∀n.
m0.boolify4 (words.n2w n) =
bool.LET
(λn1.
bool.LET
(λn2.
bool.LET (λn3. (odd n3, odd n2, odd n1, odd n))
(arithmetic.DIV2 n2)) (arithmetic.DIV2 n1))
(arithmetic.DIV2 n)
⊦ ∀P.
(∀a. P (m0.BranchExchange a)) ∧
(∀a. P (m0.BranchLinkExchangeRegister a)) ∧
(∀a. P (m0.BranchLinkImmediate a)) ∧ (∀a. P (m0.BranchTarget a)) ⇒
∀x. P x
⊦ ∀P.
(∀a. P (m0.ChangeProcessorState a)) ∧
(∀a. P (m0.MoveToRegisterFromSpecial a)) ∧
(∀a. P (m0.MoveToSpecialRegister a)) ∧ (∀a. P (m0.SupervisorCall a)) ⇒
∀x. P x
⊦ ∀f0 f1 f2.
∃fn.
(∀a. fn (m0.ASSERT a) = f0 a) ∧ fn m0.NoException = f1 ∧
∀a. fn (m0.UNPREDICTABLE a) = f2 a
⊦ ∀x shift.
m0.ASR (x, shift) =
λstate.
if shift = 0 then (x, state)
else
bool.LET (pair.UNCURRY (λv s. (fst v, s)))
(m0.ASR_C (x, shift) state)
⊦ ∀x shift.
m0.LSL (x, shift) =
λstate.
if shift = 0 then (x, state)
else
bool.LET (pair.UNCURRY (λv s. (fst v, s)))
(m0.LSL_C (x, shift) state)
⊦ ∀x shift.
m0.LSR (x, shift) =
λstate.
if shift = 0 then (x, state)
else
bool.LET (pair.UNCURRY (λv s. (fst v, s)))
(m0.LSR_C (x, shift) state)
⊦ ∀x shift.
m0.ROR (x, shift) =
λstate.
if shift = 0 then (x, state)
else
bool.LET (pair.UNCURRY (λv s. (fst v, s)))
(m0.ROR_C (x, shift) state)
⊦ ∀n imm32.
m0.dfn'CompareImmediate (n, imm32) =
λstate.
m0.DataProcessing
(words.n2w (arithmetic.BIT2 (arithmetic.BIT2 1)), ⊤, bool.ARB, n,
imm32, m0.PSR_C (m0.m0_state_PSR state)) state
⊦ ∀M M' f.
M = M' ∧ (∀a. M' = m0.Multiply32 a ⇒ f a = f' a) ⇒
m0.Multiply_CASE M f = m0.Multiply_CASE M' f'
⊦ ∀r r'.
r < bit1 (arithmetic.BIT2 3) ⇒ r' < bit1 (arithmetic.BIT2 3) ⇒
(m0.num2RName r = m0.num2RName r' ⇔ r = r')
⊦ ∀x carry_in.
m0.RRX_C (x, carry_in) =
(bitstring.v2w
((carry_in :: []) @
bitstring.field (arithmetic.- (words.word_len (words.n2w 0)) 1) 1
(bitstring.w2v x)), words.word_bit 0 x)
⊦ ∀address.
m0.BLXWritePC address =
λstate.
m0.BranchTo
(words.word_concat (words.word_extract 31 1 address) (words.n2w 0))
(if ¬words.word_bit 0 address then m0.Raise m0.HardFault state
else state)
⊦ ∀P.
(∀a. P (m0.ExternalInterrupt a)) ∧ P m0.HardFault ∧ P m0.NMI ∧
P m0.PendSV ∧ P m0.Reset ∧ P m0.SVCall ∧ P m0.SysTick ⇒ ∀x. P x
⊦ ∀b1 c1 b2 c2.
m0.PRIMASK_PM_fupd (const b1)
(m0.PRIMASK_primask'rst_fupd (const c1) bool.ARB) =
m0.PRIMASK_PM_fupd (const b2)
(m0.PRIMASK_primask'rst_fupd (const c2) bool.ARB) ⇔
(b1 ⇔ b2) ∧ c1 = c2
⊦ ∀x.
m0.reg'SHPR3 x =
m0.SHPR3_CASE x
(λPRI_14 PRI_15 shpr3'rst.
words.word_concat PRI_15
(words.word_concat
(words.word_extract (bit1 (arithmetic.BIT2 0)) 0 shpr3'rst)
(words.word_concat PRI_14
(words.word_extract
(bit1 (bit1 (arithmetic.BIT2 (arithmetic.BIT2 0))))
(arithmetic.BIT2 (arithmetic.BIT2 0)) shpr3'rst))))
⊦ ∀c01 c1 c02 c2.
m0.SHPR2_PRI_11_fupd (const c01)
(m0.SHPR2_shpr2'rst_fupd (const c1) bool.ARB) =
m0.SHPR2_PRI_11_fupd (const c02)
(m0.SHPR2_shpr2'rst_fupd (const c2) bool.ARB) ⇔ c01 = c02 ∧ c1 = c2
⊦ (∀a.
m0.exception_size (m0.ASSERT a) =
1 + list.list_size string.char_size a) ∧
m0.exception_size m0.NoException = 0 ∧
∀a.
m0.exception_size (m0.UNPREDICTABLE a) =
1 + list.list_size string.char_size a
⊦ ∀im.
m0.dfn'ChangeProcessorState im =
λstate.
bool.LET
(λs. m0.m0_state_count_fupd (const (m0.m0_state_count s + 1)) s)
(m0.IncPC ()
(if m0.CurrentModeIsPrivileged () state then
m0.m0_state_PRIMASK_fupd
(const
(m0.PRIMASK_PM_fupd (const im)
(m0.m0_state_PRIMASK state))) state
else state))
⊦ ∀a0 a1 a2 a0' a1' a2'.
m0.recordtype.CONTROL a0 a1 a2 = m0.recordtype.CONTROL a0' a1' a2' ⇔
(a0 ⇔ a0') ∧ (a1 ⇔ a1') ∧ (a2 ⇔ a2')
⊦ ∀a0 a1 a2 a0' a1' a2'.
m0.recordtype.CCR a0 a1 a2 = m0.recordtype.CCR a0' a1' a2' ⇔
(a0 ⇔ a0') ∧ (a1 ⇔ a1') ∧ a2 = a2'
⊦ ∀a0 a1 a2 a0' a1' a2'.
m0.recordtype.SHPR3 a0 a1 a2 = m0.recordtype.SHPR3 a0' a1' a2' ⇔
a0 = a0' ∧ a1 = a1' ∧ a2 = a2'
⊦ m0.num2SRType 0 = m0.SRType_LSL ∧ m0.num2SRType 1 = m0.SRType_LSR ∧
m0.num2SRType (arithmetic.BIT2 0) = m0.SRType_ASR ∧
m0.num2SRType 3 = m0.SRType_ROR ∧
m0.num2SRType (arithmetic.BIT2 1) = m0.SRType_RRX
⊦ m0.SRType2num m0.SRType_LSL = 0 ∧ m0.SRType2num m0.SRType_LSR = 1 ∧
m0.SRType2num m0.SRType_ASR = arithmetic.BIT2 0 ∧
m0.SRType2num m0.SRType_ROR = 3 ∧
m0.SRType2num m0.SRType_RRX = arithmetic.BIT2 1
⊦ (∀f b c.
m0.PRIMASK_PM_fupd f (m0.recordtype.PRIMASK b c) =
m0.recordtype.PRIMASK (f b) c) ∧
∀f b c.
m0.PRIMASK_primask'rst_fupd f (m0.recordtype.PRIMASK b c) =
m0.recordtype.PRIMASK b (f c)
⊦ (∀f c c0.
m0.SHPR2_PRI_11_fupd f (m0.recordtype.SHPR2 c c0) =
m0.recordtype.SHPR2 (f c) c0) ∧
∀f c c0.
m0.SHPR2_shpr2'rst_fupd f (m0.recordtype.SHPR2 c c0) =
m0.recordtype.SHPR2 c (f c0)
⊦ ∀P.
(∀x. P x) ⇔
∀b1 b0 b c0 c.
P
(m0.AIRCR_ENDIANNESS_fupd (const b1)
(m0.AIRCR_SYSRESETREQ_fupd (const b0)
(m0.AIRCR_VECTCLRACTIVE_fupd (const b)
(m0.AIRCR_VECTKEY_fupd (const c0)
(m0.AIRCR_aircr'rst_fupd (const c) bool.ARB)))))
⊦ ∀P.
(∃x. P x) ⇔
∃b1 b0 b c0 c.
P
(m0.AIRCR_ENDIANNESS_fupd (const b1)
(m0.AIRCR_SYSRESETREQ_fupd (const b0)
(m0.AIRCR_VECTCLRACTIVE_fupd (const b)
(m0.AIRCR_VECTKEY_fupd (const c0)
(m0.AIRCR_aircr'rst_fupd (const c) bool.ARB)))))
⊦ ∀P.
(∀x. P x) ⇔
∀c3 c2 c1 c0 c.
P
(m0.IPR_PRI_N0_fupd (const c3)
(m0.IPR_PRI_N1_fupd (const c2)
(m0.IPR_PRI_N2_fupd (const c1)
(m0.IPR_PRI_N3_fupd (const c0)
(m0.IPR_ipr'rst_fupd (const c) bool.ARB)))))
⊦ ∀P.
(∃x. P x) ⇔
∃c3 c2 c1 c0 c.
P
(m0.IPR_PRI_N0_fupd (const c3)
(m0.IPR_PRI_N1_fupd (const c2)
(m0.IPR_PRI_N2_fupd (const c1)
(m0.IPR_PRI_N3_fupd (const c0)
(m0.IPR_ipr'rst_fupd (const c) bool.ARB)))))
⊦ ∀a0 a1 a2 a3 a4 a5 a6 f.
m0.PSR_CASE (m0.recordtype.PSR a0 a1 a2 a3 a4 a5 a6) f =
f a0 a1 a2 a3 a4 a5 a6
⊦ ∀x.
(∃c. x = m0.ExternalInterrupt c) ∨ x = m0.HardFault ∨ x = m0.NMI ∨
x = m0.PendSV ∨ x = m0.Reset ∨ x = m0.SVCall ∨ x = m0.SysTick
⊦ ∀value typ amount carry_in.
m0.Shift (value, typ, amount, carry_in) =
λstate.
bool.LET (pair.UNCURRY (λv s. (fst v, s)))
(m0.Shift_C (value, typ, amount, carry_in) state)
⊦ ∀f.
∃fn.
∀a0 a1 a2 a3 a4 a5 a6.
fn (m0.recordtype.PSR a0 a1 a2 a3 a4 a5 a6) =
f a0 a1 a2 a3 a4 a5 a6
⊦ ∀f b c b0 b1 b2 b3 c0.
m0.PSR_C_fupd f (m0.recordtype.PSR b c b0 b1 b2 b3 c0) =
m0.recordtype.PSR (f b) c b0 b1 b2 b3 c0
⊦ ∀f b c b0 b1 b2 b3 c0.
m0.PSR_N_fupd f (m0.recordtype.PSR b c b0 b1 b2 b3 c0) =
m0.recordtype.PSR b c (f b0) b1 b2 b3 c0
⊦ ∀f b c b0 b1 b2 b3 c0.
m0.PSR_T_fupd f (m0.recordtype.PSR b c b0 b1 b2 b3 c0) =
m0.recordtype.PSR b c b0 (f b1) b2 b3 c0
⊦ ∀f b c b0 b1 b2 b3 c0.
m0.PSR_V_fupd f (m0.recordtype.PSR b c b0 b1 b2 b3 c0) =
m0.recordtype.PSR b c b0 b1 (f b2) b3 c0
⊦ ∀f b c b0 b1 b2 b3 c0.
m0.PSR_Z_fupd f (m0.recordtype.PSR b c b0 b1 b2 b3 c0) =
m0.recordtype.PSR b c b0 b1 b2 (f b3) c0
⊦ ∀opc n m.
m0.dfn'TestCompareRegister (opc, n, m) =
λstate.
m0.doRegister
(words.word_concat (words.n2w (arithmetic.BIT2 0)) opc, ⊤,
words.n2w 0, n, m, m0.SRType_LSL, 0) state
⊦ ∀f b c b0 b1 b2 b3 c0.
m0.PSR_ExceptionNumber_fupd f (m0.recordtype.PSR b c b0 b1 b2 b3 c0) =
m0.recordtype.PSR b (f c) b0 b1 b2 b3 c0
⊦ ∀f b c b0 b1 b2 b3 c0.
m0.PSR_psr'rst_fupd f (m0.recordtype.PSR b c b0 b1 b2 b3 c0) =
m0.recordtype.PSR b c b0 b1 b2 b3 (f c0)
⊦ (∀g f P.
m0.PRIMASK_PM_fupd f (m0.PRIMASK_PM_fupd g P) =
m0.PRIMASK_PM_fupd (f ∘ g) P) ∧
∀g f P.
m0.PRIMASK_primask'rst_fupd f (m0.PRIMASK_primask'rst_fupd g P) =
m0.PRIMASK_primask'rst_fupd (f ∘ g) P
⊦ (∀g f S.
m0.SHPR2_PRI_11_fupd f (m0.SHPR2_PRI_11_fupd g S) =
m0.SHPR2_PRI_11_fupd (f ∘ g) S) ∧
∀g f S.
m0.SHPR2_shpr2'rst_fupd f (m0.SHPR2_shpr2'rst_fupd g S) =
m0.SHPR2_shpr2'rst_fupd (f ∘ g) S
⊦ ∀M M' f.
M = M' ∧
(∀a0 a1. M' = m0.recordtype.PRIMASK a0 a1 ⇒ f a0 a1 = f' a0 a1) ⇒
m0.PRIMASK_CASE M f = m0.PRIMASK_CASE M' f'
⊦ ∀M M' f.
M = M' ∧
(∀a0 a1. M' = m0.recordtype.SHPR2 a0 a1 ⇒ f a0 a1 = f' a0 a1) ⇒
m0.SHPR2_CASE M f = m0.SHPR2_CASE M' f'
⊦ ∀P.
(∀a. P (m0.LoadByte a)) ∧ (∀a. P (m0.LoadHalf a)) ∧
(∀a. P (m0.LoadLiteral a)) ∧ (∀a. P (m0.LoadMultiple a)) ∧
(∀a. P (m0.LoadWord a)) ⇒ ∀x. P x
⊦ ∀P.
(∀a. P (m0.ByteReverse a)) ∧ (∀a. P (m0.ByteReversePackedHalfword a)) ∧
(∀a. P (m0.ByteReverseSignedHalfword a)) ∧ (∀a. P (m0.ExtendByte a)) ∧
(∀a. P (m0.ExtendHalfword a)) ⇒ ∀x. P x
⊦ ∀P.
(∀a. P (m0.Push a)) ∧ (∀a. P (m0.StoreByte a)) ∧
(∀a. P (m0.StoreHalf a)) ∧ (∀a. P (m0.StoreMultiple a)) ∧
(∀a. P (m0.StoreWord a)) ⇒ ∀x. P x
⊦ ∀d imm32.
m0.dfn'Move (d, imm32) =
λstate.
m0.DataProcessing
(words.n2w (bit1 (arithmetic.BIT2 (arithmetic.BIT2 0))), ⊤, d,
words.n2w 15, imm32, m0.PSR_C (m0.m0_state_PSR state)) state
⊦ ∀x0 x1 x2 x3 x4.
∃f.
f m0.SRType_LSL = x0 ∧ f m0.SRType_LSR = x1 ∧ f m0.SRType_ASR = x2 ∧
f m0.SRType_ROR = x3 ∧ f m0.SRType_RRX = x4
⊦ ∀x.
(∃p. x = m0.LoadByte p) ∨ (∃p. x = m0.LoadHalf p) ∨
(∃p. x = m0.LoadLiteral p) ∨ (∃p. x = m0.LoadMultiple p) ∨
∃p. x = m0.LoadWord p
⊦ ∀x.
(∃p. x = m0.ByteReverse p) ∨ (∃p. x = m0.ByteReversePackedHalfword p) ∨
(∃p. x = m0.ByteReverseSignedHalfword p) ∨ (∃p. x = m0.ExtendByte p) ∨
∃p. x = m0.ExtendHalfword p
⊦ ∀x.
(∃c. x = m0.Push c) ∨ (∃p. x = m0.StoreByte p) ∨
(∃p. x = m0.StoreHalf p) ∨ (∃p. x = m0.StoreMultiple p) ∨
∃p. x = m0.StoreWord p
⊦ (∀a. m0.Branch_size (m0.BranchExchange a) = 1) ∧
(∀a. m0.Branch_size (m0.BranchLinkExchangeRegister a) = 1) ∧
(∀a. m0.Branch_size (m0.BranchLinkImmediate a) = 1) ∧
∀a. m0.Branch_size (m0.BranchTarget a) = 1
⊦ ∀opc setflags d n m.
m0.dfn'Register (opc, setflags, d, n, m) =
λstate. m0.doRegister (opc, setflags, d, n, m, m0.SRType_LSL, 0) state
⊦ ∀opc setflags d n imm32.
m0.dfn'ArithLogicImmediate (opc, setflags, d, n, imm32) =
λstate.
m0.DataProcessing
(opc, setflags, d, n, imm32, m0.PSR_C (m0.m0_state_PSR state))
state
⊦ ∀w.
m0.BitCount w =
fst
(snd
(state_transformer.FOR
(0, arithmetic.- (words.word_len (words.n2w 0)) 1,
(λi state.
((),
(if words.word_bit i w then (fst state + 1, ())
else state)))) (0, ())))
⊦ (∀g f.
m0.PRIMASK_primask'rst_fupd f ∘ m0.PRIMASK_PM_fupd g =
m0.PRIMASK_PM_fupd g ∘ m0.PRIMASK_primask'rst_fupd f) ∧
∀h g f.
m0.PRIMASK_primask'rst_fupd f ∘ (m0.PRIMASK_PM_fupd g ∘ h) =
m0.PRIMASK_PM_fupd g ∘ (m0.PRIMASK_primask'rst_fupd f ∘ h)
⊦ (∀g f.
m0.SHPR2_shpr2'rst_fupd f ∘ m0.SHPR2_PRI_11_fupd g =
m0.SHPR2_PRI_11_fupd g ∘ m0.SHPR2_shpr2'rst_fupd f) ∧
∀h g f.
m0.SHPR2_shpr2'rst_fupd f ∘ (m0.SHPR2_PRI_11_fupd g ∘ h) =
m0.SHPR2_PRI_11_fupd g ∘ (m0.SHPR2_shpr2'rst_fupd f ∘ h)
⊦ ∀M M' v0 v1.
M = M' ∧ (M' = m0.Mode_Thread ⇒ v0 = v0') ∧
(M' = m0.Mode_Handler ⇒ v1 = v1') ⇒
m0.Mode_CASE M v0 v1 = m0.Mode_CASE M' v0' v1'
⊦ ∀A1 A2.
A1 = A2 ⇔
(m0.AIRCR_ENDIANNESS A1 ⇔ m0.AIRCR_ENDIANNESS A2) ∧
(m0.AIRCR_SYSRESETREQ A1 ⇔ m0.AIRCR_SYSRESETREQ A2) ∧
(m0.AIRCR_VECTCLRACTIVE A1 ⇔ m0.AIRCR_VECTCLRACTIVE A2) ∧
m0.AIRCR_VECTKEY A1 = m0.AIRCR_VECTKEY A2 ∧
m0.AIRCR_aircr'rst A1 = m0.AIRCR_aircr'rst A2
⊦ ∀I1 I2.
I1 = I2 ⇔
m0.IPR_PRI_N0 I1 = m0.IPR_PRI_N0 I2 ∧
m0.IPR_PRI_N1 I1 = m0.IPR_PRI_N1 I2 ∧
m0.IPR_PRI_N2 I1 = m0.IPR_PRI_N2 I2 ∧
m0.IPR_PRI_N3 I1 = m0.IPR_PRI_N3 I2 ∧
m0.IPR_ipr'rst I1 = m0.IPR_ipr'rst I2
⊦ ∀P.
∃b3 c0 b2 b1 b0 b c.
P =
m0.PSR_C_fupd (const b3)
(m0.PSR_ExceptionNumber_fupd (const c0)
(m0.PSR_N_fupd (const b2)
(m0.PSR_T_fupd (const b1)
(m0.PSR_V_fupd (const b0)
(m0.PSR_Z_fupd (const b)
(m0.PSR_psr'rst_fupd (const c) bool.ARB))))))
⊦ ∀typ.
m0.DecodeRegShift typ =
bool.literal_case
(λv.
if v = words.n2w 0 then m0.SRType_LSL
else if v = words.n2w 1 then m0.SRType_LSR
else if v = words.n2w (arithmetic.BIT2 0) then m0.SRType_ASR
else if v = words.n2w 3 then m0.SRType_ROR
else bool.ARB) typ
⊦ (∀b b0 b1. m0.CONTROL_SPSEL (m0.recordtype.CONTROL b b0 b1) ⇔ b) ∧
(∀b b0 b1. m0.CONTROL_control'rst (m0.recordtype.CONTROL b b0 b1) ⇔ b0) ∧
∀b b0 b1. m0.CONTROL_nPRIV (m0.recordtype.CONTROL b b0 b1) ⇔ b1
⊦ (∀b b0 c. m0.CCR_STKALIGN (m0.recordtype.CCR b b0 c) ⇔ b) ∧
(∀b b0 c. m0.CCR_UNALIGN_TRP (m0.recordtype.CCR b b0 c) ⇔ b0) ∧
∀b b0 c. m0.CCR_ccr'rst (m0.recordtype.CCR b b0 c) = c
⊦ (∀c c0 c1. m0.SHPR3_PRI_14 (m0.recordtype.SHPR3 c c0 c1) = c) ∧
(∀c c0 c1. m0.SHPR3_PRI_15 (m0.recordtype.SHPR3 c c0 c1) = c0) ∧
∀c c0 c1. m0.SHPR3_shpr3'rst (m0.recordtype.SHPR3 c c0 c1) = c1
⊦ ∀M M' f.
M = M' ∧
(∀a0 a1 a2.
M' = m0.recordtype.CCR a0 a1 a2 ⇒ f a0 a1 a2 = f' a0 a1 a2) ⇒
m0.CCR_CASE M f = m0.CCR_CASE M' f'
⊦ ∀M M' f.
M = M' ∧
(∀a0 a1 a2.
M' = m0.recordtype.CONTROL a0 a1 a2 ⇒ f a0 a1 a2 = f' a0 a1 a2) ⇒
m0.CONTROL_CASE M f = m0.CONTROL_CASE M' f'
⊦ ∀M M' f.
M = M' ∧
(∀a0 a1 a2.
M' = m0.recordtype.SHPR3 a0 a1 a2 ⇒ f a0 a1 a2 = f' a0 a1 a2) ⇒
m0.SHPR3_CASE M f = m0.SHPR3_CASE M' f'
⊦ ∀a0 a1 a2 a3 a4 a5 a6.
m0.PSR_size (m0.recordtype.PSR a0 a1 a2 a3 a4 a5 a6) =
1 +
(basicSize.bool_size a0 +
(basicSize.bool_size a2 +
(basicSize.bool_size a3 +
(basicSize.bool_size a4 + basicSize.bool_size a5))))
⊦ (∀a. m0.ARM_Exception_size (m0.ExternalInterrupt a) = 1) ∧
m0.ARM_Exception_size m0.HardFault = 0 ∧
m0.ARM_Exception_size m0.NMI = 0 ∧ m0.ARM_Exception_size m0.PendSV = 0 ∧
m0.ARM_Exception_size m0.Reset = 0 ∧
m0.ARM_Exception_size m0.SVCall = 0 ∧
m0.ARM_Exception_size m0.SysTick = 0
⊦ ∀unsigned d m.
m0.dfn'ExtendByte (unsigned, d, m) =
λstate.
bool.LET
(λs. m0.m0_state_count_fupd (const (m0.m0_state_count s + 1)) s)
(m0.IncPC ()
(m0.write'R
(m0.Extend (unsigned, words.word_extract 7 0 (m0.R m state)),
d) state))
⊦ ∀P0.
(∀P. P0 P) ⇔
∀b3 c0 b2 b1 b0 b c.
P0
(m0.PSR_C_fupd (const b3)
(m0.PSR_ExceptionNumber_fupd (const c0)
(m0.PSR_N_fupd (const b2)
(m0.PSR_T_fupd (const b1)
(m0.PSR_V_fupd (const b0)
(m0.PSR_Z_fupd (const b)
(m0.PSR_psr'rst_fupd (const c) bool.ARB)))))))
⊦ ∀P0.
(∃P. P0 P) ⇔
∃b3 c0 b2 b1 b0 b c.
P0
(m0.PSR_C_fupd (const b3)
(m0.PSR_ExceptionNumber_fupd (const c0)
(m0.PSR_N_fupd (const b2)
(m0.PSR_T_fupd (const b1)
(m0.PSR_V_fupd (const b0)
(m0.PSR_Z_fupd (const b)
(m0.PSR_psr'rst_fupd (const c) bool.ARB)))))))
⊦ ∀unsigned d m.
m0.dfn'ExtendHalfword (unsigned, d, m) =
λstate.
bool.LET
(λs. m0.m0_state_count_fupd (const (m0.m0_state_count s + 1)) s)
(m0.IncPC ()
(m0.write'R
(m0.Extend
(unsigned, words.word_extract 15 0 (m0.R m state)), d)
state))
⊦ ∀f0 f1 f2 f3.
∃fn.
(∀a. fn (m0.ChangeProcessorState a) = f0 a) ∧
(∀a. fn (m0.MoveToRegisterFromSpecial a) = f1 a) ∧
(∀a. fn (m0.MoveToSpecialRegister a) = f2 a) ∧
∀a. fn (m0.SupervisorCall a) = f3 a
⊦ ∀m.
m0.dfn'BranchLinkExchangeRegister m =
λstate.
bool.LET
(λs. m0.m0_state_count_fupd (const (m0.m0_state_count s + 3)) s)
(m0.BLXWritePC (m0.R m state)
(m0.write'LR
(words.word_concat
(words.word_extract 31 1
(words.word_sub (m0.PC state)
(words.n2w (arithmetic.BIT2 0)))) (words.n2w 1))
state))
⊦ ∀f0 f1 f2 f3.
∃fn.
(∀a. fn (m0.BranchExchange a) = f0 a) ∧
(∀a. fn (m0.BranchLinkExchangeRegister a) = f1 a) ∧
(∀a. fn (m0.BranchLinkImmediate a) = f2 a) ∧
∀a. fn (m0.BranchTarget a) = f3 a
⊦ ∀e.
m0.ExcNumber e =
m0.ARM_Exception_CASE e
(λn. words.word_add (words.n2w (arithmetic.BIT2 7)) n) (words.n2w 3)
(words.n2w (arithmetic.BIT2 0))
(words.n2w (arithmetic.BIT2 (arithmetic.BIT2 (arithmetic.BIT2 0))))
(words.n2w 1) (words.n2w (bit1 (bit1 (arithmetic.BIT2 0))))
(words.n2w 15)
⊦ ∀b11 b01 b1 b12 b02 b2.
m0.CONTROL_SPSEL_fupd (const b11)
(m0.CONTROL_control'rst_fupd (const b01)
(m0.CONTROL_nPRIV_fupd (const b1) bool.ARB)) =
m0.CONTROL_SPSEL_fupd (const b12)
(m0.CONTROL_control'rst_fupd (const b02)
(m0.CONTROL_nPRIV_fupd (const b2) bool.ARB)) ⇔
(b11 ⇔ b12) ∧ (b01 ⇔ b02) ∧ (b1 ⇔ b2)
⊦ ∀b01 b1 c1 b02 b2 c2.
m0.CCR_STKALIGN_fupd (const b01)
(m0.CCR_UNALIGN_TRP_fupd (const b1)
(m0.CCR_ccr'rst_fupd (const c1) bool.ARB)) =
m0.CCR_STKALIGN_fupd (const b02)
(m0.CCR_UNALIGN_TRP_fupd (const b2)
(m0.CCR_ccr'rst_fupd (const c2) bool.ARB)) ⇔
(b01 ⇔ b02) ∧ (b1 ⇔ b2) ∧ c1 = c2
⊦ ∀A b1 b0 b c0 c.
m0.AIRCR_ENDIANNESS_fupd (const b1)
(m0.AIRCR_SYSRESETREQ_fupd (const b0)
(m0.AIRCR_VECTCLRACTIVE_fupd (const b)
(m0.AIRCR_VECTKEY_fupd (const c0)
(m0.AIRCR_aircr'rst_fupd (const c) A)))) =
m0.AIRCR_ENDIANNESS_fupd (const b1)
(m0.AIRCR_SYSRESETREQ_fupd (const b0)
(m0.AIRCR_VECTCLRACTIVE_fupd (const b)
(m0.AIRCR_VECTKEY_fupd (const c0)
(m0.AIRCR_aircr'rst_fupd (const c) bool.ARB))))
⊦ ∀I c3 c2 c1 c0 c.
m0.IPR_PRI_N0_fupd (const c3)
(m0.IPR_PRI_N1_fupd (const c2)
(m0.IPR_PRI_N2_fupd (const c1)
(m0.IPR_PRI_N3_fupd (const c0)
(m0.IPR_ipr'rst_fupd (const c) I)))) =
m0.IPR_PRI_N0_fupd (const c3)
(m0.IPR_PRI_N1_fupd (const c2)
(m0.IPR_PRI_N2_fupd (const c1)
(m0.IPR_PRI_N3_fupd (const c0)
(m0.IPR_ipr'rst_fupd (const c) bool.ARB))))
⊦ ∀c11 c01 c1 c12 c02 c2.
m0.SHPR3_PRI_14_fupd (const c11)
(m0.SHPR3_PRI_15_fupd (const c01)
(m0.SHPR3_shpr3'rst_fupd (const c1) bool.ARB)) =
m0.SHPR3_PRI_14_fupd (const c12)
(m0.SHPR3_PRI_15_fupd (const c02)
(m0.SHPR3_shpr3'rst_fupd (const c2) bool.ARB)) ⇔
c11 = c12 ∧ c01 = c02 ∧ c1 = c2
⊦ ∀t imm32.
m0.dfn'LoadLiteral (t, imm32) =
λstate.
bool.LET
(pair.UNCURRY
(λv s.
bool.LET
(λs.
m0.m0_state_count_fupd
(const (m0.m0_state_count s + arithmetic.BIT2 0)) s)
(m0.IncPC () (m0.write'R (v, t) s))))
(m0.MemU
(words.word_add (m0.Align (m0.PC state, arithmetic.BIT2 1))
imm32, arithmetic.BIT2 1) state)
⊦ ∀P.
(∀a. P (m0.ArithLogicImmediate a)) ∧ (∀a. P (m0.CompareImmediate a)) ∧
(∀a. P (m0.Move a)) ∧ (∀a. P (m0.Register a)) ∧
(∀a. P (m0.ShiftImmediate a)) ∧ (∀a. P (m0.ShiftRegister a)) ∧
(∀a. P (m0.TestCompareRegister a)) ⇒ ∀x. P x
⊦ (∀a f v f1. m0.exception_CASE (m0.ASSERT a) f v f1 = f a) ∧
(∀f v f1. m0.exception_CASE m0.NoException f v f1 = v) ∧
∀a f v f1. m0.exception_CASE (m0.UNPREDICTABLE a) f v f1 = f1 a
⊦ ∀M M' f f1.
M = M' ∧ (∀a. M' = m0.immediate_form a ⇒ f a = f' a) ∧
(∀a. M' = m0.register_form a ⇒ f1 a = f1' a) ⇒
m0.offset_CASE M f f1 = m0.offset_CASE M' f' f1'
⊦ ∀x.
m0.reg'AIRCR x =
m0.AIRCR_CASE x
(λENDIANNESS SYSRESETREQ VECTCLRACTIVE VECTKEY aircr'rst.
words.word_concat VECTKEY
(words.word_concat (bitstring.v2w (ENDIANNESS :: []))
(words.word_concat
(words.word_extract (bit1 (bit1 (arithmetic.BIT2 0))) 0
aircr'rst)
(words.word_concat (bitstring.v2w (SYSRESETREQ :: []))
(words.word_concat
(bitstring.v2w (VECTCLRACTIVE :: []))
(words.word_extract
(arithmetic.BIT2 (bit1 (arithmetic.BIT2 0)))
(arithmetic.BIT2 (bit1 (arithmetic.BIT2 0)))
aircr'rst))))))
⊦ ∀M M' f f1.
M = M' ∧ (∀a. M' = m0.Thumb a ⇒ f a = f' a) ∧
(∀a. M' = m0.Thumb2 a ⇒ f1 a = f1' a) ⇒
m0.MachineCode_CASE M f f1 = m0.MachineCode_CASE M' f' f1'
⊦ ∀x.
m0.rec'CCR x =
m0.recordtype.CCR (words.word_bit (bit1 (arithmetic.BIT2 1)) x)
(words.word_bit 3 x)
(words.word_concat (words.word_extract (arithmetic.BIT2 0) 0 x)
(words.word_concat
(words.word_extract (arithmetic.BIT2 3) (arithmetic.BIT2 1) x)
(words.word_extract 31 (arithmetic.BIT2 (arithmetic.BIT2 1))
x)))
⊦ (∀f S.
m0.SHPR2_PRI_11 (m0.SHPR2_shpr2'rst_fupd f S) = m0.SHPR2_PRI_11 S) ∧
(∀f S.
m0.SHPR2_shpr2'rst (m0.SHPR2_PRI_11_fupd f S) =
m0.SHPR2_shpr2'rst S) ∧
(∀f S.
m0.SHPR2_PRI_11 (m0.SHPR2_PRI_11_fupd f S) = f (m0.SHPR2_PRI_11 S)) ∧
∀f S.
m0.SHPR2_shpr2'rst (m0.SHPR2_shpr2'rst_fupd f S) =
f (m0.SHPR2_shpr2'rst S)
⊦ (∀f P.
m0.PRIMASK_PM (m0.PRIMASK_primask'rst_fupd f P) ⇔ m0.PRIMASK_PM P) ∧
(∀f P.
m0.PRIMASK_primask'rst (m0.PRIMASK_PM_fupd f P) =
m0.PRIMASK_primask'rst P) ∧
(∀f P. m0.PRIMASK_PM (m0.PRIMASK_PM_fupd f P) ⇔ f (m0.PRIMASK_PM P)) ∧
∀f P.
m0.PRIMASK_primask'rst (m0.PRIMASK_primask'rst_fupd f P) =
f (m0.PRIMASK_primask'rst P)
⊦ ∀x v0 v1 v2 v3 v4.
m0.SRType_CASE x v0 v1 v2 v3 v4 =
let m ← m0.SRType2num x in
if m < arithmetic.BIT2 0 then if m = 0 then v0 else v1
else if m < 3 then v2
else if m = 3 then v3
else v4
⊦ ∀M M' f.
M = M' ∧
(∀a0 a1 a2 a3 a4.
M' = m0.recordtype.AIRCR a0 a1 a2 a3 a4 ⇒
f a0 a1 a2 a3 a4 = f' a0 a1 a2 a3 a4) ⇒
m0.AIRCR_CASE M f = m0.AIRCR_CASE M' f'
⊦ ∀x.
(∃p. x = m0.ArithLogicImmediate p) ∨ (∃p. x = m0.CompareImmediate p) ∨
(∃p. x = m0.Move p) ∨ (∃p. x = m0.Register p) ∨
(∃p. x = m0.ShiftImmediate p) ∨ (∃p. x =