theory Recycle_C

lemma double_setEndpoint:
  "do y \<leftarrow> setEndpoint epptr v1; setEndpoint epptr v2 od
       = setEndpoint epptr v2" apply (simp add: setEndpoint_def setObject_def bind_assoc split_def
                   modify_gets_helper) apply (simp add: updateObject_default_def bind_assoc objBits_simps) apply (rule ext) apply (rule bind_apply_cong, rule refl)+ apply (clarsimp simp add: in_monad projectKOs magnitudeCheck_assert
                            snd_lookupAround2_update) apply (simp add: lookupAround2_known1 assert_opt_def projectKO_def projectKO_opt_ep
                    alignCheck_assert) apply (simp add: bind_def simpler_modify_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do y <- setEndpoint epptr v1;
setEndpoint epptr v2
od = setEndpoint epptr v2 proof (prove)
goal (1 subgoal):
 1. do x <- gets ksPSpace;
xa <- assert_opt (fst (lookupAround2 epptr x));
xb <- updateObject_default v1 (snd xa) epptr (fst xa) (snd (lookupAround2 epptr x));
y <- modify (ksPSpace_update (\<lambda>_. x(fst xa \<mapsto> xb)));
p <- assert_opt (fst (lookupAround2 epptr (x(fst xa \<mapsto> xb))));
obj' <- updateObject_default v2 (snd p) epptr (fst p) (snd (lookupAround2 epptr (x(fst xa \<mapsto> xb))));
modify (ksPSpace_update (\<lambda>_. x(fst xa \<mapsto> xb, fst p \<mapsto> obj')))
od = do ps <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 epptr ps));
obj' <- updateObject_default v2 (snd p) epptr (fst p) (snd (lookupAround2 epptr ps));
modify (ksPSpace_update (\<lambda>_. ps(fst p \<mapsto> obj')))
od proof (prove)
goal (1 subgoal):
 1. do x <- gets ksPSpace;
xa <- assert_opt (fst (lookupAround2 epptr x));
xb <- assert (epptr = fst xa);
xb <- projectKO (snd xa);
xb <- alignCheck epptr epSizeBits;
y <- magnitudeCheck epptr (snd (lookupAround2 epptr x)) epSizeBits;
y <- modify (ksPSpace_update (\<lambda>_. x(fst xa \<mapsto> KOEndpoint v1)));
p <- assert_opt (fst (lookupAround2 epptr (x(fst xa \<mapsto> KOEndpoint v1))));
xb <- assert (epptr = fst p);
xb <- projectKO (snd p);
xb <- alignCheck epptr epSizeBits;
y <- magnitudeCheck epptr (snd (lookupAround2 epptr (x(fst xa \<mapsto> KOEndpoint v1)))) epSizeBits;
modify (ksPSpace_update (\<lambda>_. x(fst xa \<mapsto> KOEndpoint v1, fst p \<mapsto> KOEndpoint v2)))
od = do ps <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 epptr ps));
x <- assert (epptr = fst p);
x <- projectKO (snd p);
x <- alignCheck epptr epSizeBits;
y <- magnitudeCheck epptr (snd (lookupAround2 epptr ps)) epSizeBits;
modify (ksPSpace_update (\<lambda>_. ps(fst p \<mapsto> KOEndpoint v2)))
od proof (prove)
goal (1 subgoal):
 1. \<And>x. (do x <- gets ksPSpace;
xa <- assert_opt (fst (lookupAround2 epptr x));
xb <- assert (epptr = fst xa);
xb <- projectKO (snd xa);
xb <- alignCheck epptr epSizeBits;
y <- magnitudeCheck epptr (snd (lookupAround2 epptr x)) epSizeBits;
y <- modify (ksPSpace_update (\<lambda>_. x(fst xa \<mapsto> KOEndpoint v1)));
p <- assert_opt (fst (lookupAround2 epptr (x(fst xa \<mapsto> KOEndpoint v1))));
xb <- assert (epptr = fst p);
xb <- projectKO (snd p);
xb <- alignCheck epptr epSizeBits;
y <- magnitudeCheck epptr (snd (lookupAround2 epptr (x(fst xa \<mapsto> KOEndpoint v1)))) epSizeBits;
modify (ksPSpace_update (\<lambda>_. x(fst xa \<mapsto> KOEndpoint v1, fst p \<mapsto> KOEndpoint v2)))
od) x = (do ps <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 epptr ps));
x <- assert (epptr = fst p);
x <- projectKO (snd p);
x <- alignCheck epptr epSizeBits;
y <- magnitudeCheck epptr (snd (lookupAround2 epptr ps)) epSizeBits;
modify (ksPSpace_update (\<lambda>_. ps(fst p \<mapsto> KOEndpoint v2)))
od) x proof (prove)
goal (1 subgoal):
 1. \<And>x rv st rva sta rvb stb rvc stc rvd std rve ste. \<lbrakk>(rv, st) \<in> fst (gets ksPSpace x); (rva, sta) \<in> fst (assert_opt (fst (lookupAround2 epptr rv)) st); (rvb, stb) \<in> fst (assert (epptr = fst rva) sta); (rvc, stc) \<in> fst (projectKO (snd rva) stb); (rvd, std) \<in> fst (alignCheck epptr epSizeBits stc); (rve, ste) \<in> fst (magnitudeCheck epptr (snd (lookupAround2 epptr rv)) epSizeBits std)\<rbrakk> \<Longrightarrow> (do y <- modify (ksPSpace_update (\<lambda>_. rv(fst rva \<mapsto> KOEndpoint v1)));
p <- assert_opt (fst (lookupAround2 epptr (rv(fst rva \<mapsto> KOEndpoint v1))));
x <- assert (epptr = fst p);
x <- projectKO (snd p);
x <- alignCheck epptr epSizeBits;
y <- magnitudeCheck epptr (snd (lookupAround2 epptr (rv(fst rva \<mapsto> KOEndpoint v1)))) epSizeBits;
modify (ksPSpace_update (\<lambda>_. rv(fst rva \<mapsto> KOEndpoint v1, fst p \<mapsto> KOEndpoint v2)))
od) ste = modify (ksPSpace_update (\<lambda>_. rv(fst rva \<mapsto> KOEndpoint v2))) ste proof (prove)
goal (1 subgoal):
 1. \<And>x rvc. \<lbrakk>ksPSpace x epptr = Some (KOEndpoint rvc); is_aligned epptr epSizeBits; case snd (lookupAround2 epptr (ksPSpace x)) of None \<Rightarrow> True | Some z \<Rightarrow> 1 << epSizeBits \<le> z - fst (epptr, KOEndpoint rvc)\<rbrakk> \<Longrightarrow> (do y <- modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(epptr \<mapsto> KOEndpoint v1)));
p <- assert_opt (fst (lookupAround2 epptr ((ksPSpace x)(epptr \<mapsto> KOEndpoint v1))));
xa <- assert (epptr = fst p);
xa <- projectKO (snd p);
xa <- alignCheck epptr epSizeBits;
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(epptr \<mapsto> KOEndpoint v1, fst p \<mapsto> KOEndpoint v2)))
od) x = modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(epptr \<mapsto> KOEndpoint v2))) x proof (prove)
goal (1 subgoal):
 1. \<And>x rvc. \<lbrakk>ksPSpace x epptr = Some (KOEndpoint rvc); is_aligned epptr epSizeBits; case snd (lookupAround2 epptr (ksPSpace x)) of None \<Rightarrow> True | Some z \<Rightarrow> 1 << epSizeBits \<le> z - fst (epptr, KOEndpoint rvc)\<rbrakk> \<Longrightarrow> (do y <- modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(epptr \<mapsto> KOEndpoint v1)));
modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(epptr \<mapsto> KOEndpoint v2)))
od) x = modify (ksPSpace_update (\<lambda>_. (ksPSpace x)(epptr \<mapsto> KOEndpoint v2))) x proof (prove)
goal:
No subgoals!