Package m0-model: M0 model

Information

namem0-model
version1.0
descriptionM0 model
authorHOL OpenTheory Packager <opentheory-packager@hol-theorem-prover.org>
licenseMIT
checksumb0f8e11bf1ea11b8133b9f5375fd2f48dbd4676c
requiresbase
hol-base
hol-words
hol-string
hol-integer
hol-monad
hol-floating-point
showData.Bool
Data.List
Data.Option
Data.Pair
Data.Unit
Function
HOL4
Number.Natural
Relation

Files

Defined Type Operators

Defined Constants

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 =