theory Fastpath_C

lemma fastpath_mi_check:
  "((mi && mask 9) + 3) && ~~ mask 3 = 0
      = (msgExtraCaps (messageInfoFromWord mi) = 0
            \<and> msgLength (messageInfoFromWord mi) \<le> scast n_msgRegisters
            \<and> length_CL (seL4_MessageInfo_lift (seL4_MessageInfo_C (FCP (K mi))))
                  \<le> scast n_msgRegisters)"
  (is "?P = (?Q \<and> ?R \<and> ?S)") proof - have le_Q: "?P = (?Q \<and> ?S)" apply (simp add: mask_def messageInfoFromWord_def Let_def
                     msgExtraCapBits_def msgLengthBits_def
                     seL4_MessageInfo_lift_def fcp_beta n_msgRegisters_def) apply word_bitwise apply blast done have Q_R: "?S \<Longrightarrow> ?R" apply (clarsimp simp: messageInfoFromWord_def Let_def msgLengthBits_def
                          msgExtraCapBits_def mask_def n_msgRegisters_def
                          seL4_MessageInfo_lift_def fcp_beta) apply (subst if_not_P, simp_all) apply (simp add: msgMaxLength_def linorder_not_less) apply (erule order_trans, simp) done from le_Q Q_R show ?thesis by blast qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((mi && mask 9) + 3 && ~~ mask 3 = 0) = (msgExtraCaps (messageInfoFromWord mi) = 0 \<and> msgLength (messageInfoFromWord mi) \<le> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<and> length_CL (seL4_MessageInfo_lift (seL4_MessageInfo_C (FCP (K mi)))) \<le> SCAST(32 signed \<rightarrow> 32) n_msgRegisters) proof (state)
goal (1 subgoal):
 1. ((mi && mask 9) + 3 && ~~ mask 3 = 0) = (msgExtraCaps (messageInfoFromWord mi) = 0 \<and> msgLength (messageInfoFromWord mi) \<le> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<and> length_CL (seL4_MessageInfo_lift (seL4_MessageInfo_C (FCP (K mi)))) \<le> SCAST(32 signed \<rightarrow> 32) n_msgRegisters) proof (prove)
goal (1 subgoal):
 1. ((mi && mask 9) + 3 && ~~ mask 3 = 0) = (msgExtraCaps (messageInfoFromWord mi) = 0 \<and> length_CL (seL4_MessageInfo_lift (seL4_MessageInfo_C (FCP (K mi)))) \<le> SCAST(32 signed \<rightarrow> 32) n_msgRegisters) proof (prove)
goal (1 subgoal):
 1. ((mi && 0x1FF) + 3 && 0xFFFFFFF8 = 0) = ((mi >> 7) && 3 = 0 \<and> mi && 0x7F \<le> 4) proof (prove)
goal (1 subgoal):
 1. (mi !! 3 = (mi !! 2 \<and> (mi !! 1 \<or> mi !! 0)) \<and> mi !! 4 = (mi !! 2 \<and> mi !! 3 \<and> (mi !! 1 \<or> mi !! 0)) \<and> mi !! 5 = (mi !! 2 \<and> mi !! 3 \<and> mi !! 4 \<and> (mi !! 1 \<or> mi !! 0)) \<and> mi !! 6 = (mi !! 2 \<and> mi !! 3 \<and> mi !! 4 \<and> mi !! 5 \<and> (mi !! 1 \<or> mi !! 0)) \<and> mi !! 7 = (mi !! 2 \<and> mi !! 3 \<and> mi !! 4 \<and> mi !! 5 \<and> mi !! 6 \<and> (mi !! 1 \<or> mi !! 0)) \<and> mi !! 8 = (mi !! 2 \<and> mi !! 3 \<and> mi !! 4 \<and> mi !! 5 \<and> mi !! 6 \<and> mi !! 7 \<and> (mi !! 1 \<or> mi !! 0)) \<and> (mi !! 8 \<longrightarrow> mi !! 7 \<longrightarrow> mi !! 6 \<longrightarrow> mi !! 5 \<longrightarrow> mi !! 4 \<longrightarrow> mi !! 3 \<longrightarrow> mi !! 2 \<longrightarrow> \<not> mi !! 1 \<and> \<not> mi !! 0)) = (\<not> mi !! 7 \<and> \<not> mi !! 8 \<and> \<not> mi !! 6 \<and> \<not> mi !! 5 \<and> \<not> mi !! 4 \<and> \<not> mi !! 3 \<and> (mi !! 2 \<longrightarrow> \<not> mi !! 1 \<and> \<not> mi !! 0)) proof (prove)
goal:
No subgoals! proof (state)
this:
((mi && mask 9) + 3 && ~~ mask 3 = 0) = (msgExtraCaps (messageInfoFromWord mi) = 0 \<and> length_CL (seL4_MessageInfo_lift (seL4_MessageInfo_C (FCP (K mi)))) \<le> SCAST(32 signed \<rightarrow> 32) n_msgRegisters)

goal (1 subgoal):
 1. ((mi && mask 9) + 3 && ~~ mask 3 = 0) = (msgExtraCaps (messageInfoFromWord mi) = 0 \<and> msgLength (messageInfoFromWord mi) \<le> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<and> length_CL (seL4_MessageInfo_lift (seL4_MessageInfo_C (FCP (K mi)))) \<le> SCAST(32 signed \<rightarrow> 32) n_msgRegisters) proof (prove)
goal (1 subgoal):
 1. length_CL (seL4_MessageInfo_lift (seL4_MessageInfo_C (FCP (K mi)))) \<le> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<Longrightarrow> msgLength (messageInfoFromWord mi) \<le> SCAST(32 signed \<rightarrow> 32) n_msgRegisters proof (prove)
goal (1 subgoal):
 1. mi && 0x7F \<le> 4 \<Longrightarrow> (if msgMaxLength < mi && 0x7F then msgMaxLength else mi && 0x7F) \<le> 4 proof (prove)
goal (1 subgoal):
 1. mi && 0x7F \<le> 4 \<Longrightarrow> \<not> msgMaxLength < mi && 0x7F proof (prove)
goal (1 subgoal):
 1. mi && 0x7F \<le> 4 \<Longrightarrow> mi && 0x7F \<le> 0x78 proof (prove)
goal:
No subgoals! proof (state)
this:
length_CL (seL4_MessageInfo_lift (seL4_MessageInfo_C (FCP (K mi)))) \<le> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<Longrightarrow> msgLength (messageInfoFromWord mi) \<le> SCAST(32 signed \<rightarrow> 32) n_msgRegisters

goal (1 subgoal):
 1. ((mi && mask 9) + 3 && ~~ mask 3 = 0) = (msgExtraCaps (messageInfoFromWord mi) = 0 \<and> msgLength (messageInfoFromWord mi) \<le> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<and> length_CL (seL4_MessageInfo_lift (seL4_MessageInfo_C (FCP (K mi)))) \<le> SCAST(32 signed \<rightarrow> 32) n_msgRegisters) proof (chain)
picking this:
((mi && mask 9) + 3 && ~~ mask 3 = 0) = (msgExtraCaps (messageInfoFromWord mi) = 0 \<and> length_CL (seL4_MessageInfo_lift (seL4_MessageInfo_C (FCP (K mi)))) \<le> SCAST(32 signed \<rightarrow> 32) n_msgRegisters)
length_CL (seL4_MessageInfo_lift (seL4_MessageInfo_C (FCP (K mi)))) \<le> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<Longrightarrow> msgLength (messageInfoFromWord mi) \<le> SCAST(32 signed \<rightarrow> 32) n_msgRegisters proof (prove)
using this:
((mi && mask 9) + 3 && ~~ mask 3 = 0) = (msgExtraCaps (messageInfoFromWord mi) = 0 \<and> length_CL (seL4_MessageInfo_lift (seL4_MessageInfo_C (FCP (K mi)))) \<le> SCAST(32 signed \<rightarrow> 32) n_msgRegisters)
length_CL (seL4_MessageInfo_lift (seL4_MessageInfo_C (FCP (K mi)))) \<le> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<Longrightarrow> msgLength (messageInfoFromWord mi) \<le> SCAST(32 signed \<rightarrow> 32) n_msgRegisters

goal (1 subgoal):
 1. ((mi && mask 9) + 3 && ~~ mask 3 = 0) = (msgExtraCaps (messageInfoFromWord mi) = 0 \<and> msgLength (messageInfoFromWord mi) \<le> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<and> length_CL (seL4_MessageInfo_lift (seL4_MessageInfo_C (FCP (K mi)))) \<le> SCAST(32 signed \<rightarrow> 32) n_msgRegisters) proof (state)
this:
((mi && mask 9) + 3 && ~~ mask 3 = 0) = (msgExtraCaps (messageInfoFromWord mi) = 0 \<and> msgLength (messageInfoFromWord mi) \<le> SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<and> length_CL (seL4_MessageInfo_lift (seL4_MessageInfo_C (FCP (K mi)))) \<le> SCAST(32 signed \<rightarrow> 32) n_msgRegisters)

goal:
No subgoals!