theory StateTranslation_D

lemma transform_tcb_intent_invocation:
  "transform_intent label args = Some (TcbIntent ti)
   \<Longrightarrow>
   (
   ((label = GenInvocationLabel TCBReadRegisters) = (ti = (TcbReadRegistersIntent ((args ! 0)!!0) 0 (args ! 1)) \<and> length args \<ge> 2)) \<and>
   ((label = GenInvocationLabel TCBWriteRegisters) = (ti = (TcbWriteRegistersIntent ((args ! 0)!!0) 0 (args ! 1) (drop 2 args)) \<and> length args \<ge> 2)) \<and>
   ((label = GenInvocationLabel TCBCopyRegisters) = (ti = (TcbCopyRegistersIntent ((args ! 0)!!0) ((args ! 0)!!1) ((args ! 0)!!2) ((args ! 0)!!3) 0) \<and> length args \<ge> 1)) \<and>
   ((label = GenInvocationLabel TCBConfigure) = (ti = (TcbConfigureIntent (args ! 0) (args ! 1) (args ! 2) (args ! 3)) \<and> length args \<ge> 4)) \<and>
   ((label = GenInvocationLabel TCBSetPriority) = (ti = (TcbSetPriorityIntent (prio_from_arg (args ! 0))) \<and> length args \<ge> 1)) \<and>
   ((label = GenInvocationLabel TCBSetMCPriority) = (ti = (TcbSetMCPriorityIntent (prio_from_arg (args ! 0))) \<and> length args \<ge> 1)) \<and>
   ((label = GenInvocationLabel TCBSetSchedParams) = (ti = (TcbSetSchedParamsIntent (prio_from_arg (args ! 0)) (prio_from_arg (args ! 1))) \<and> length args \<ge> 2)) \<and>
   ((label = GenInvocationLabel TCBSetSpace) = (ti = (TcbSetSpaceIntent (args ! 0) (args ! 1) (args ! 2)) \<and> length args \<ge> 3)) \<and>
   ((label = GenInvocationLabel TCBSuspend) = (ti = TcbSuspendIntent)) \<and>
   ((label = GenInvocationLabel TCBResume) = (ti = TcbResumeIntent)) \<and>
   ((label = GenInvocationLabel TCBBindNotification) = (ti = TcbBindNTFNIntent)) \<and>
   ((label = GenInvocationLabel TCBUnbindNotification) = (ti = TcbUnbindNTFNIntent)) \<and>
   ((label = GenInvocationLabel TCBSetTLSBase) = (ti = TcbSetTLSBaseIntent))
   ) \<and>
   (
    label \<noteq> GenInvocationLabel InvalidInvocation \<and>
    label \<noteq> GenInvocationLabel UntypedRetype \<and>
    label \<noteq> GenInvocationLabel CNodeRevoke \<and>
    label \<noteq> GenInvocationLabel CNodeDelete \<and>
    label \<noteq> GenInvocationLabel CNodeCancelBadgedSends \<and>
    label \<noteq> GenInvocationLabel CNodeCopy \<and>
    label \<noteq> GenInvocationLabel CNodeMint \<and>
    label \<noteq> GenInvocationLabel CNodeMove \<and>
    label \<noteq> GenInvocationLabel CNodeMutate \<and>
    label \<noteq> GenInvocationLabel CNodeRotate \<and>
    label \<noteq> GenInvocationLabel CNodeSaveCaller \<and>
    label \<noteq> GenInvocationLabel IRQIssueIRQHandler \<and>
    label \<noteq> GenInvocationLabel IRQAckIRQ \<and>
    label \<noteq> GenInvocationLabel IRQSetIRQHandler \<and>
    label \<noteq> GenInvocationLabel IRQClearIRQHandler \<and>
    label \<noteq> ArchInvocationLabel ARMPageTableMap \<and>
    label \<noteq> ArchInvocationLabel ARMPageTableUnmap \<and>
    label \<noteq> ArchInvocationLabel ARMPageMap \<and>
    label \<noteq> ArchInvocationLabel ARMPageUnmap \<and>
    label \<noteq> ArchInvocationLabel ARMPageClean_Data \<and>
    label \<noteq> ArchInvocationLabel ARMPageInvalidate_Data \<and>
    label \<noteq> ArchInvocationLabel ARMPageCleanInvalidate_Data \<and>
    label \<noteq> ArchInvocationLabel ARMPageUnify_Instruction \<and>
    label \<noteq> ArchInvocationLabel ARMPageGetAddress \<and>
    label \<noteq> ArchInvocationLabel ARMPDClean_Data \<and>
    label \<noteq> ArchInvocationLabel ARMPDInvalidate_Data \<and>
    label \<noteq> ArchInvocationLabel ARMPDCleanInvalidate_Data \<and>
    label \<noteq> ArchInvocationLabel ARMPDUnify_Instruction \<and>
    label \<noteq> ArchInvocationLabel ARMASIDControlMakePool \<and>
    label \<noteq> GenInvocationLabel DomainSetSet)" apply(intro conjI) apply(rule iffI,
         simp add: transform_intent_def transform_intent_tcb_defs split: list.split_asm,
         simp add: transform_intent_def transform_intent_tcb_defs
              split: gen_invocation_labels.split_asm invocation_label.split_asm
                     arch_invocation_label.split_asm list.split_asm)+ 
                               (* 30 subgoals *)
                                apply(simp add: transform_intent_def transform_intent_tcb_defs
                                          split: gen_invocation_labels.split_asm invocation_label.split_asm
                                                 arch_invocation_label.split_asm)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. transform_intent label args = Some (TcbIntent ti) \<Longrightarrow> ((label = GenInvocationLabel TCBReadRegisters) = (ti = TcbReadRegistersIntent (args ! 0 !! 0) 0 (args ! 1) \<and> 2 \<le> length args) \<and> (label = GenInvocationLabel TCBWriteRegisters) = (ti = TcbWriteRegistersIntent (args ! 0 !! 0) 0 (args ! 1) (drop 2 args) \<and> 2 \<le> length args) \<and> (label = GenInvocationLabel TCBCopyRegisters) = (ti = TcbCopyRegistersIntent (args ! 0 !! 0) (args ! 0 !! 1) (args ! 0 !! 2) (args ! 0 !! 3) 0 \<and> 1 \<le> length args) \<and> (label = GenInvocationLabel TCBConfigure) = (ti = TcbConfigureIntent (args ! 0) (args ! 1) (args ! 2) (args ! 3) \<and> 4 \<le> length args) \<and> (label = GenInvocationLabel TCBSetPriority) = (ti = TcbSetPriorityIntent (prio_from_arg (args ! 0)) \<and> 1 \<le> length args) \<and> (label = GenInvocationLabel TCBSetMCPriority) = (ti = TcbSetMCPriorityIntent (prio_from_arg (args ! 0)) \<and> 1 \<le> length args) \<and> (label = GenInvocationLabel TCBSetSchedParams) = (ti = TcbSetSchedParamsIntent (prio_from_arg (args ! 0)) (prio_from_arg (args ! 1)) \<and> 2 \<le> length args) \<and> (label = GenInvocationLabel TCBSetSpace) = (ti = TcbSetSpaceIntent (args ! 0) (args ! 1) (args ! 2) \<and> 3 \<le> length args) \<and> (label = GenInvocationLabel TCBSuspend) = (ti = TcbSuspendIntent) \<and> (label = GenInvocationLabel TCBResume) = (ti = TcbResumeIntent) \<and> (label = GenInvocationLabel TCBBindNotification) = (ti = TcbBindNTFNIntent) \<and> (label = GenInvocationLabel TCBUnbindNotification) = (ti = TcbUnbindNTFNIntent) \<and> (label = GenInvocationLabel TCBSetTLSBase) = (ti = TcbSetTLSBaseIntent)) \<and> label \<noteq> GenInvocationLabel InvalidInvocation \<and> label \<noteq> GenInvocationLabel UntypedRetype \<and> label \<noteq> GenInvocationLabel CNodeRevoke \<and> label \<noteq> GenInvocationLabel CNodeDelete \<and> label \<noteq> GenInvocationLabel CNodeCancelBadgedSends \<and> label \<noteq> GenInvocationLabel CNodeCopy \<and> label \<noteq> GenInvocationLabel CNodeMint \<and> label \<noteq> GenInvocationLabel CNodeMove \<and> label \<noteq> GenInvocationLabel CNodeMutate \<and> label \<noteq> GenInvocationLabel CNodeRotate \<and> label \<noteq> GenInvocationLabel CNodeSaveCaller \<and> label \<noteq> GenInvocationLabel IRQIssueIRQHandler \<and> label \<noteq> GenInvocationLabel IRQAckIRQ \<and> label \<noteq> GenInvocationLabel IRQSetIRQHandler \<and> label \<noteq> GenInvocationLabel IRQClearIRQHandler \<and> label \<noteq> ArchInvocationLabel ARMPageTableMap \<and> label \<noteq> ArchInvocationLabel ARMPageTableUnmap \<and> label \<noteq> ArchInvocationLabel ARMPageMap \<and> label \<noteq> ArchInvocationLabel ARMPageUnmap \<and> label \<noteq> ArchInvocationLabel ARMPageClean_Data \<and> label \<noteq> ArchInvocationLabel ARMPageInvalidate_Data \<and> label \<noteq> ArchInvocationLabel ARMPageCleanInvalidate_Data \<and> label \<noteq> ArchInvocationLabel ARMPageUnify_Instruction \<and> label \<noteq> ArchInvocationLabel ARMPageGetAddress \<and> label \<noteq> ArchInvocationLabel ARMPDClean_Data \<and> label \<noteq> ArchInvocationLabel ARMPDInvalidate_Data \<and> label \<noteq> ArchInvocationLabel ARMPDCleanInvalidate_Data \<and> label \<noteq> ArchInvocationLabel ARMPDUnify_Instruction \<and> label \<noteq> ArchInvocationLabel ARMASIDControlMakePool \<and> label \<noteq> GenInvocationLabel DomainSetSet proof (prove)
goal (43 subgoals):
 1. transform_intent label args = Some (TcbIntent ti) \<Longrightarrow> (label = GenInvocationLabel TCBReadRegisters) = (ti = TcbReadRegistersIntent (args ! 0 !! 0) 0 (args ! 1) \<and> 2 \<le> length args)
 2. transform_intent label args = Some (TcbIntent ti) \<Longrightarrow> (label = GenInvocationLabel TCBWriteRegisters) = (ti = TcbWriteRegistersIntent (args ! 0 !! 0) 0 (args ! 1) (drop 2 args) \<and> 2 \<le> length args)
 3. transform_intent label args = Some (TcbIntent ti) \<Longrightarrow> (label = GenInvocationLabel TCBCopyRegisters) = (ti = TcbCopyRegistersIntent (args ! 0 !! 0) (args ! 0 !! 1) (args ! 0 !! 2) (args ! 0 !! 3) 0 \<and> 1 \<le> length args)
 4. transform_intent label args = Some (TcbIntent ti) \<Longrightarrow> (label = GenInvocationLabel TCBConfigure) = (ti = TcbConfigureIntent (args ! 0) (args ! 1) (args ! 2) (args ! 3) \<and> 4 \<le> length args)
 5. transform_intent label args = Some (TcbIntent ti) \<Longrightarrow> (label = GenInvocationLabel TCBSetPriority) = (ti = TcbSetPriorityIntent (prio_from_arg (args ! 0)) \<and> 1 \<le> length args)
 6. transform_intent label args = Some (TcbIntent ti) \<Longrightarrow> (label = GenInvocationLabel TCBSetMCPriority) = (ti = TcbSetMCPriorityIntent (prio_from_arg (args ! 0)) \<and> 1 \<le> length args)
 7. transform_intent label args = Some (TcbIntent ti) \<Longrightarrow> (label = GenInvocationLabel TCBSetSchedParams) = (ti = TcbSetSchedParamsIntent (prio_from_arg (args ! 0)) (prio_from_arg (args ! 1)) \<and> 2 \<le> length args)
 8. transform_intent label args = Some (TcbIntent ti) \<Longrightarrow> (label = GenInvocationLabel TCBSetSpace) = (ti = TcbSetSpaceIntent (args ! 0) (args ! 1) (args ! 2) \<and> 3 \<le> length args)
 9. transform_intent label args = Some (TcbIntent ti) \<Longrightarrow> (label = GenInvocationLabel TCBSuspend) = (ti = TcbSuspendIntent)
 10. transform_intent label args = Some (TcbIntent ti) \<Longrightarrow> (label = GenInvocationLabel TCBResume) = (ti = TcbResumeIntent)
A total of 43 subgoals... proof (prove)
goal (30 subgoals):
 1. transform_intent label args = Some (TcbIntent ti) \<Longrightarrow> label \<noteq> GenInvocationLabel InvalidInvocation
 2. transform_intent label args = Some (TcbIntent ti) \<Longrightarrow> label \<noteq> GenInvocationLabel UntypedRetype
 3. transform_intent label args = Some (TcbIntent ti) \<Longrightarrow> label \<noteq> GenInvocationLabel CNodeRevoke
 4. transform_intent label args = Some (TcbIntent ti) \<Longrightarrow> label \<noteq> GenInvocationLabel CNodeDelete
 5. transform_intent label args = Some (TcbIntent ti) \<Longrightarrow> label \<noteq> GenInvocationLabel CNodeCancelBadgedSends
 6. transform_intent label args = Some (TcbIntent ti) \<Longrightarrow> label \<noteq> GenInvocationLabel CNodeCopy
 7. transform_intent label args = Some (TcbIntent ti) \<Longrightarrow> label \<noteq> GenInvocationLabel CNodeMint
 8. transform_intent label args = Some (TcbIntent ti) \<Longrightarrow> label \<noteq> GenInvocationLabel CNodeMove
 9. transform_intent label args = Some (TcbIntent ti) \<Longrightarrow> label \<noteq> GenInvocationLabel CNodeMutate
 10. transform_intent label args = Some (TcbIntent ti) \<Longrightarrow> label \<noteq> GenInvocationLabel CNodeRotate
A total of 30 subgoals... proof (prove)
goal (30 subgoals):
 1. transform_intent label args = Some (TcbIntent ti) \<Longrightarrow> label \<noteq> GenInvocationLabel InvalidInvocation
 2. transform_intent label args = Some (TcbIntent ti) \<Longrightarrow> label \<noteq> GenInvocationLabel UntypedRetype
 3. transform_intent label args = Some (TcbIntent ti) \<Longrightarrow> label \<noteq> GenInvocationLabel CNodeRevoke
 4. transform_intent label args = Some (TcbIntent ti) \<Longrightarrow> label \<noteq> GenInvocationLabel CNodeDelete
 5. transform_intent label args = Some (TcbIntent ti) \<Longrightarrow> label \<noteq> GenInvocationLabel CNodeCancelBadgedSends
 6. transform_intent label args = Some (TcbIntent ti) \<Longrightarrow> label \<noteq> GenInvocationLabel CNodeCopy
 7. transform_intent label args = Some (TcbIntent ti) \<Longrightarrow> label \<noteq> GenInvocationLabel CNodeMint
 8. transform_intent label args = Some (TcbIntent ti) \<Longrightarrow> label \<noteq> GenInvocationLabel CNodeMove
 9. transform_intent label args = Some (TcbIntent ti) \<Longrightarrow> label \<noteq> GenInvocationLabel CNodeMutate
 10. transform_intent label args = Some (TcbIntent ti) \<Longrightarrow> label \<noteq> GenInvocationLabel CNodeRotate
A total of 30 subgoals... proof (prove)
goal:
No subgoals!