theory VSpace_R

lemma setCurrentPD_corres:
  "corres dc \<top> \<top> (do_machine_op (setCurrentPD addr)) (doMachineOp (setCurrentPD addr))" apply (simp add: setCurrentPD_def writeTTBR0Ptr_def) apply (rule corres_machine_op) apply (rule corres_guard_imp) apply (rule corres_split_eqr) apply (rule corres_underlying_trivial) apply (wp setCurrentPD_no_fails) apply (rule corres_split_eqr) apply (rule corres_underlying_trivial) apply (wp setCurrentPD_no_fails) apply (rule corres_rel_imp) apply (rule corres_underlying_trivial) apply (wp setCurrentPD_no_fails) apply wpsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (\<lambda>_. True) (\<lambda>_. True) (do_machine_op (setCurrentPD addr)) (doMachineOp (setCurrentPD addr)) proof (prove)
goal (1 subgoal):
 1. corres dc (\<lambda>_. True) (\<lambda>_. True) (do_machine_op (do y <- dsb;
y <- writeTTBR0 (ARM_H.fromPAddr addr && 0xFFFFE000 || 0x18);
isb
od)) (doMachineOp (do y <- dsb;
y <- writeTTBR0 (ARM_H.fromPAddr addr && 0xFFFFE000 || 0x18);
isb
od)) proof (prove)
goal (1 subgoal):
 1. corres_underlying Id False True dc (\<lambda>_. True) (\<lambda>_. True) (do y <- dsb;
y <- writeTTBR0 (ARM_H.fromPAddr addr && 0xFFFFE000 || 0x18);
isb
od) (do y <- dsb;
y <- writeTTBR0 (ARM_H.fromPAddr addr && 0xFFFFE000 || 0x18);
isb
od) proof (prove)
goal (3 subgoals):
 1. corres_underlying Id False True dc ?Q2 ?Q'2 (do y <- dsb;
y <- writeTTBR0 (ARM_H.fromPAddr addr && 0xFFFFE000 || 0x18);
isb
od) (do y <- dsb;
y <- writeTTBR0 (ARM_H.fromPAddr addr && 0xFFFFE000 || 0x18);
isb
od)
 2. \<And>s. True \<Longrightarrow> ?Q2 s
 3. \<And>s. True \<Longrightarrow> ?Q'2 s proof (prove)
goal (6 subgoals):
 1. corres_underlying Id False True (=) ?P6 ?P'6 dsb dsb
 2. \<And>y. corres_underlying Id False True dc (?R6 y) (?R'6 y) (do y <- writeTTBR0 (ARM_H.fromPAddr addr && 0xFFFFE000 || 0x18);
isb
od) (do y <- writeTTBR0 (ARM_H.fromPAddr addr && 0xFFFFE000 || 0x18);
isb
od)
 3. \<lbrace>?Q6\<rbrace> dsb \<lbrace>?R6\<rbrace>
 4. \<lbrace>?Q'6\<rbrace> dsb \<lbrace>?R'6\<rbrace>
 5. \<And>s. True \<Longrightarrow> (?P6 and ?Q6) s
 6. \<And>s. True \<Longrightarrow> (?P'6 and ?Q'6) s proof (prove)
goal (6 subgoals):
 1. True \<Longrightarrow> no_fail ?P'6 dsb
 2. \<And>y. corres_underlying Id False True dc (?R6 y) (?R'6 y) (do y <- writeTTBR0 (ARM_H.fromPAddr addr && 0xFFFFE000 || 0x18);
isb
od) (do y <- writeTTBR0 (ARM_H.fromPAddr addr && 0xFFFFE000 || 0x18);
isb
od)
 3. \<lbrace>?Q6\<rbrace> dsb \<lbrace>?R6\<rbrace>
 4. \<lbrace>?Q'6\<rbrace> dsb \<lbrace>?R'6\<rbrace>
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 6. \<And>s. True \<Longrightarrow> (?P'6 and ?Q'6) s proof (prove)
goal (5 subgoals):
 1. \<And>y. corres_underlying Id False True dc (?R6 y) (?R'6 y) (do y <- writeTTBR0 (ARM_H.fromPAddr addr && 0xFFFFE000 || 0x18);
isb
od) (do y <- writeTTBR0 (ARM_H.fromPAddr addr && 0xFFFFE000 || 0x18);
isb
od)
 2. \<lbrace>?Q6\<rbrace> dsb \<lbrace>?R6\<rbrace>
 3. \<lbrace>?Q'6\<rbrace> dsb \<lbrace>?R'6\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s proof (prove)
goal (8 subgoals):
 1. \<And>y. corres_underlying Id False True (=) (?P15 y) (?P'15 y) (writeTTBR0 (ARM_H.fromPAddr addr && 0xFFFFE000 || 0x18)) (writeTTBR0 (ARM_H.fromPAddr addr && 0xFFFFE000 || 0x18))
 2. \<And>y ya. corres_underlying Id False True dc (?R15 y ya) (?R'15 y ya) isb isb
 3. \<And>y. \<lbrace>?Q15 y\<rbrace> writeTTBR0 (ARM_H.fromPAddr addr && 0xFFFFE000 || 0x18) \<lbrace>?R15 y\<rbrace>
 4. \<And>y. \<lbrace>?Q'15 y\<rbrace> writeTTBR0 (ARM_H.fromPAddr addr && 0xFFFFE000 || 0x18) \<lbrace>?R'15 y\<rbrace>
 5. \<lbrace>?Q6\<rbrace> dsb \<lbrace>\<lambda>y. ?P15 y and ?Q15 y\<rbrace>
 6. \<lbrace>?Q'6\<rbrace> dsb \<lbrace>\<lambda>y. ?P'15 y and ?Q'15 y\<rbrace>
 7. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 8. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s proof (prove)
goal (8 subgoals):
 1. \<And>y. True \<Longrightarrow> no_fail (?P'15 y) (writeTTBR0 (ARM_H.fromPAddr addr && 0xFFFFE000 || 0x18))
 2. \<And>y ya. corres_underlying Id False True dc (?R15 y ya) (?R'15 y ya) isb isb
 3. \<And>y. \<lbrace>?Q15 y\<rbrace> writeTTBR0 (ARM_H.fromPAddr addr && 0xFFFFE000 || 0x18) \<lbrace>?R15 y\<rbrace>
 4. \<And>y. \<lbrace>?Q'15 y\<rbrace> writeTTBR0 (ARM_H.fromPAddr addr && 0xFFFFE000 || 0x18) \<lbrace>?R'15 y\<rbrace>
 5. \<lbrace>?Q6\<rbrace> dsb \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q15 y\<rbrace>
 6. \<lbrace>?Q'6\<rbrace> dsb \<lbrace>\<lambda>y. ?P'15 y and ?Q'15 y\<rbrace>
 7. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 8. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s proof (prove)
goal (7 subgoals):
 1. \<And>y ya. corres_underlying Id False True dc (?R15 y ya) (?R'15 y ya) isb isb
 2. \<And>y. \<lbrace>?Q15 y\<rbrace> writeTTBR0 (ARM_H.fromPAddr addr && 0xFFFFE000 || 0x18) \<lbrace>?R15 y\<rbrace>
 3. \<And>y. \<lbrace>?Q'15 y\<rbrace> writeTTBR0 (ARM_H.fromPAddr addr && 0xFFFFE000 || 0x18) \<lbrace>?R'15 y\<rbrace>
 4. \<lbrace>?Q6\<rbrace> dsb \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q15 y\<rbrace>
 5. \<lbrace>?Q'6\<rbrace> dsb \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q'15 y\<rbrace>
 6. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 7. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s proof (prove)
goal (8 subgoals):
 1. \<And>y ya. corres_underlying Id False True (?r'25 y ya) (?R15 y ya) (?R'15 y ya) isb isb
 2. \<And>y ya x yb. ?r'25 y ya x yb \<Longrightarrow> dc x yb
 3. \<And>y. \<lbrace>?Q15 y\<rbrace> writeTTBR0 (ARM_H.fromPAddr addr && 0xFFFFE000 || 0x18) \<lbrace>?R15 y\<rbrace>
 4. \<And>y. \<lbrace>?Q'15 y\<rbrace> writeTTBR0 (ARM_H.fromPAddr addr && 0xFFFFE000 || 0x18) \<lbrace>?R'15 y\<rbrace>
 5. \<lbrace>?Q6\<rbrace> dsb \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q15 y\<rbrace>
 6. \<lbrace>?Q'6\<rbrace> dsb \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q'15 y\<rbrace>
 7. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 8. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s proof (prove)
goal (8 subgoals):
 1. \<And>y ya. True \<Longrightarrow> no_fail (?R'15 y ya) isb
 2. \<And>y ya x yb. x = yb \<Longrightarrow> dc x yb
 3. \<And>y. \<lbrace>?Q15 y\<rbrace> writeTTBR0 (ARM_H.fromPAddr addr && 0xFFFFE000 || 0x18) \<lbrace>\<lambda>ya _. True\<rbrace>
 4. \<And>y. \<lbrace>?Q'15 y\<rbrace> writeTTBR0 (ARM_H.fromPAddr addr && 0xFFFFE000 || 0x18) \<lbrace>?R'15 y\<rbrace>
 5. \<lbrace>?Q6\<rbrace> dsb \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q15 y\<rbrace>
 6. \<lbrace>?Q'6\<rbrace> dsb \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q'15 y\<rbrace>
 7. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 8. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s proof (prove)
goal (7 subgoals):
 1. \<And>y ya x yb. x = yb \<Longrightarrow> dc x yb
 2. \<And>y. \<lbrace>?Q15 y\<rbrace> writeTTBR0 (ARM_H.fromPAddr addr && 0xFFFFE000 || 0x18) \<lbrace>\<lambda>ya _. True\<rbrace>
 3. \<And>y. \<lbrace>?Q'15 y\<rbrace> writeTTBR0 (ARM_H.fromPAddr addr && 0xFFFFE000 || 0x18) \<lbrace>\<lambda>ya _. True\<rbrace>
 4. \<lbrace>?Q6\<rbrace> dsb \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q15 y\<rbrace>
 5. \<lbrace>?Q'6\<rbrace> dsb \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q'15 y\<rbrace>
 6. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 7. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s proof (prove)
goal:
No subgoals!