Google Git
Sign in
opensecura/3p/nicta/cogent/467b5dd3d8154baaa2ba188fa7382b79cdb70b6e/./impl/fs/bilby/proof/spec/SerialS.thy
blob: b995ee6b803c458a291c177ea4be093a1f2f3e0c [file]
(*
* Copyright 2016, NICTA
*
* This software may be distributed and modified according to the terms of
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
* See "LICENSE_GPLv2.txt" for details.
*
* @TAG(NICTA_GPL)
*)
theory SerialS
imports
PleSle
begin
type_synonym U8 = "8 word"
type_synonym U16 = "16 word"
type_synonym U32 = "32 word"
type_synonym U64 = "64 word"
lemma sle32_length:
"length (sle32 x) = 4"
by (simp add: sle32_def length_word_rsplit_exp_size' word_size)
lemma ple32_word_rcat_eq1:
"ple32 (sle32 x @ xs) 0 = x"
apply (simp only: ple32_def unat_0)
apply (subst drop_0)
apply (cut_tac x=x in sle32_length)
apply (simp add: sle32_def word_rcat_rsplit)
done
lemma ple32_word_rcat_eq2:
"length ys = (unat n) \<Longrightarrow> ple32 (ys @ sle32 x @ xs) n = x"
by (simp add: ple32_def ple32_word_rcat_eq1[simplified ple32_def, simplified])
lemmas ple32_word_rcat_eq = ple32_word_rcat_eq1 ple32_word_rcat_eq2
lemma sle64_length:
"length (sle64 x) = 8"
by (simp add: sle64_def length_word_rsplit_exp_size' word_size)
lemma ple64_word_rcat_eq1:
"ple64 (sle64 x @ xs) 0 = x"
apply (simp only: ple64_def unat_0)
apply (subst drop_0)
apply (cut_tac x=x in sle64_length)
apply (simp add: sle64_def word_rcat_rsplit)
done
lemma ple64_word_rcat_eq2:
"length ys = (unat n) \<Longrightarrow> ple64 (ys @ sle64 x @ xs) n = x"
by (simp add: ple64_def ple64_word_rcat_eq1[simplified ple64_def, simplified])
lemmas ple64_word_rcat_eq = ple64_word_rcat_eq1 ple64_word_rcat_eq2
definition pObjDel :: "U8 list \<Rightarrow> U32 \<Rightarrow> U64 ObjDel"
where
"pObjDel data' offs' \<equiv> ObjDel.make (ple64 data' offs') \<comment> \<open>id\<close>
\<comment> \<open>End 4 bytes\<close>"
definition sObjDel :: "ObjDel\<^sub>T \<Rightarrow> U8 list"
where
"sObjDel odel \<equiv> (sle64 $ ObjDel.id\<^sub>f odel) (* id *) (* End 8 bytes *)"
lemma objDel_inverse:
"pObjDel (sObjDel odel) 0 = odel"
apply(simp add: pObjDel_def sObjDel_def)
apply(simp add: ObjDel.defs)
using ple64_word_rcat_eq[where xs=Nil]
by simp
definition pObjData :: "U8 list \<Rightarrow> U32 \<Rightarrow> U32 \<Rightarrow> ObjData\<^sub>T"
where
"pObjData data offs olen \<equiv>
ObjData.make (ple64 data offs) (* id *)
(WordArrayT.make $ slice (unat (offs + 8)) (unat (offs + 8) + unat (olen - bilbyFsObjHeaderSize - bilbyFsObjDataHeaderSize)) data)"
definition sObjData :: "ObjData\<^sub>T \<Rightarrow> U32 \<Rightarrow> U8 list"
where
"sObjData odata len \<equiv> (sle64 $ ObjData.id\<^sub>f odata) @ take (unat len) (\<alpha>wa (ObjData.odata\<^sub>f odata))"
lemma length_sle32:
"length ((sle32 (x::U32))::U8 list) = 4"
by (simp add: Word.length_word_rsplit_exp_size' Word.word_size sle32_def )
lemma length_sle64:
"length ((sle64 (x::U64))::U8 list) = 8"
by (simp add: Word.length_word_rsplit_exp_size' Word.word_size sle64_def )
lemma objData_inverse:
"unat (len - bilbyFsObjHeaderSize - bilbyFsObjDataHeaderSize) = length (\<alpha>wa (odata\<^sub>f odata)) \<Longrightarrow>
len - bilbyFsObjHeaderSize - bilbyFsObjDataHeaderSize < len \<Longrightarrow>
pObjData (sObjData odata len) 0 len = odata"
apply(simp add: pObjData_def)
apply(simp add: sObjData_def)
apply(simp add: ObjData.defs)
apply(simp add: ple64_word_rcat_eq length_sle64 slice_def)
apply (subgoal_tac "unat len \<ge> length (\<alpha>wa (odata\<^sub>f odata)) ")
apply (simp add: wordarray_make')
apply unat_arith
done
definition
pu8 :: "U8 list \<Rightarrow> U32 \<Rightarrow> U8"
where
"pu8 xs offs = word_rcat (slice (unat offs) (unat offs+1) xs)"
definition pObjDentry :: "U8 list \<Rightarrow> U32 \<Rightarrow> ObjDentry\<^sub>T"
where
"pObjDentry data offs \<equiv>
let nlen = ple16 data (offs+6)
in ObjDentry.make
(ple32 data (offs+0)) (* ino *)
(pu8 data (offs+4)) (* dtype *)
(* 1 byte padding *)
nlen (* nlen *)
(WordArrayT.make $ slice (unat (offs+ 8)) (unat (offs + 8) + unat nlen) data) (* name *)"
definition pArrObjDentry :: "U8 list \<Rightarrow> U32 \<Rightarrow> U32 \<Rightarrow> (ObjDentry\<^sub>T Array \<times> 32 word \<times> 32 word list)"
where
"pArrObjDentry data offs nb_dentry =
(case (fold
(\<lambda>_ (xs,doffs,offslist).
let dentry = pObjDentry data doffs ;
newoffs = doffs + 8 + wordarray_length (ObjDentry.name\<^sub>f dentry)
in (xs@[Option.Some dentry], newoffs, offslist@ [newoffs])) [0..<unat nb_dentry] ([], offs, []))
of (xs, doffs, offslist) \<Rightarrow> (ArrayT.make (xs@ [Option.None ()]), doffs, offslist))"
definition pObjDentarr :: "U8 list \<Rightarrow> U32 \<Rightarrow> U32 \<Rightarrow> ObjDentarr\<^sub>T"
where
"pObjDentarr data offs olen \<equiv>
let nb_dentry = ple32 data (offs+8)
in ObjDentarr.make
(ple64 data offs) (* id *)
(nb_dentry) (* nb_dentry *)
(prod.fst (pArrObjDentry (take (unat (offs+olen-bilbyFsObjHeaderSize)) data) (offs+bilbyFsObjDentarrHeaderSize) nb_dentry))
"
definition pObjDentarrSize :: "U8 list \<Rightarrow> U32 \<Rightarrow> U32 \<Rightarrow> U32"
where
"pObjDentarrSize data offs olen \<equiv>
let nb_dentry = ple32 data (offs+8)
in (prod.fst (prod.snd (pArrObjDentry (take (unat (offs+olen-bilbyFsObjHeaderSize)) data) (offs+bilbyFsObjDentarrHeaderSize) nb_dentry)))
"
definition pObjSuper :: "U8 list \<Rightarrow> U32 \<Rightarrow> ObjSuper\<^sub>T"
where
"pObjSuper data offs \<equiv>
ObjSuper.make
(ple32 data offs) (* nb_eb *)
(ple32 data (offs+4)) (* eb_size *)
(ple32 data (offs+8)) (* io_size *)
(ple32 data (offs+12)) (* nb_reserved_gc *)
(ple32 data (offs+16)) (* nb_reserved_del *)
(ple32 data (offs+20)) (* cur_eb *)
(ple32 data (offs+24)) (* cur_offs *)
(ple32 data (offs+28)) (* last_inum *)
(ple64 data (offs+32)) (* next_sqnum *)
"
(* TODO: we do not have pObjSumEntry . Probably we need it.*)
definition sObjSumEntry :: "ObjSumEntry\<^sub>T \<Rightarrow> U8 list"
where
"sObjSumEntry ose \<equiv>
(sle64 $ ObjSumEntry.id\<^sub>f ose)
@ (sle64 $ ObjSumEntry.sqnum\<^sub>f ose)
@ (sle32 $ ObjSumEntry.len\<^sub>f ose)
@ (sle32 $ ObjSumEntry.del_flags_and_offs\<^sub>f ose)
@ (sle16 $ ObjSumEntry.count\<^sub>f ose)"
consts sObjSuper :: "ObjSuper\<^sub>T \<Rightarrow> U8 list"
type_synonym Buffer\<^sub>T = "(U8 WordArray, U32) Buffer"
definition bounded :: "Buffer\<^sub>T \<Rightarrow> U8 list"
where
"bounded buf = take (unat (bound\<^sub>f buf)) (WordArrayT.\<alpha>wa (data\<^sub>f buf))"
definition wellformed_buf :: "Buffer\<^sub>T \<Rightarrow> bool"
where
"wellformed_buf buf \<equiv> unat (bound\<^sub>f buf) \<le> List.length (\<alpha>wa (Buffer.data\<^sub>f buf))"
lemma elem_take_n:
"i<n \<Longrightarrow> (take n xs ! i) = xs ! i"
by simp
lemma deserialise_le32_bounded_ret:
assumes bounded:
"bbuf = bounded buf"
assumes valid_offs:
"unat offs + 3 < length (bounded buf)"
shows
"deserialise_le32 (buf, offs) = ple32 bbuf offs"
apply (simp add: bounded)
using valid_offs
apply (subgoal_tac "(\<forall>i\<in>{0..3}. unat (offs+i) < length (bounded buf))")
prefer 2
apply unat_arith
apply (simp add: bounded_def)
apply (clarsimp simp: wordarray_get_ret[where arr="data\<^sub>f buf"] ple32_def
deserialise_le32_def)
apply (subgoal_tac "\<forall>j\<in>{1..3}. (unat (offs + j) > 0)")
prefer 2
apply clarsimp
apply (drule_tac x=j in bspec, simp)
apply unat_arith
apply (subst take_drop_decomp, (simp+))+
apply (subst unatSuc[symmetric], (simp add: unat_gt_0[symmetric] add.commute[where b=offs]))+
apply simp
apply (rule trans, rule word_rcat_rsplit[symmetric])
apply (rule arg_cong[where f=word_rcat])
apply (subst word_rsplit_upt[where n=4], simp add: word_size)
apply simp
apply (simp add: upt_rec shiftr_over_or_dist shiftl_shiftr1 shiftl_shiftr2 word_size)
apply (safe intro!: word_eqI, simp_all add: word_size word_ops_nth_size nth_ucast
nth_shiftr nth_shiftl add.commute[where b=offs] test_bit_out_of_bounds)
done
lemma deserialise_le64_bounded_ret:
assumes bounded:
"bbuf = bounded buf"
assumes valid_offs:
"unat offs + 7 < length (bounded buf)"
shows
"deserialise_le64 (buf, offs) = ple64 bbuf offs"
apply (simp add: bounded)
using valid_offs
apply (subgoal_tac "(\<forall>i\<in>{0..7}. unat (offs+i) < length (bounded buf))")
prefer 2
apply unat_arith
apply (simp add: bounded_def)
apply (clarsimp simp: wordarray_get_ret[where arr="data\<^sub>f buf"] ple64_def
deserialise_le64_def)
apply (subgoal_tac "\<forall>j\<in>{1..7}. (unat (offs + j) > 0)")
prefer 2
apply clarsimp
apply (drule_tac x=j in bspec, simp)
apply unat_arith
(* feel free to improve this apply script..*)
apply (subst take_drop_decomp, (simp+))+
apply (subst unatSuc[symmetric], (simp add: unat_gt_0[symmetric] add.commute[where b=offs]))+
apply simp
apply (rule trans, rule word_rcat_rsplit[symmetric])
apply (rule arg_cong[where f=word_rcat])
apply (subst word_rsplit_upt[where n=8], simp add: word_size)
apply simp
apply (simp add: upt_rec shiftr_over_or_dist shiftl_shiftr1 shiftl_shiftr2 word_size)
apply (safe intro!: word_eqI, simp_all add: word_size word_ops_nth_size nth_ucast
nth_shiftr nth_shiftl add.commute[where b=offs] test_bit_out_of_bounds)
done
definition buf_unchanged :: "Buffer\<^sub>T \<Rightarrow> Buffer\<^sub>T \<Rightarrow> U32 \<Rightarrow> U32 \<Rightarrow> bool"
where
"buf_unchanged newbuf oldbuf offs' l \<equiv> take (unat offs') (\<alpha>wa (data\<^sub>f newbuf)) = take (unat offs') (\<alpha>wa (data\<^sub>f oldbuf)) \<and>
drop (unat offs' + unat l) (\<alpha>wa (data\<^sub>f newbuf)) = drop (unat offs' + unat l) (\<alpha>wa (data\<^sub>f oldbuf)) \<and>
bound\<^sub>f newbuf = bound\<^sub>f oldbuf"
lemma bounded_le_length:
"(length $ bounded x) \<le> length (\<alpha>wa $ data\<^sub>f x)"
by (simp add: bounded_def)
lemmas serialise_le64_simps = ArrA.make_def ElemA.make_def ElemAO.make_def ArrayUseValueP.defs
setu8_def[unfolded sanitizers] wordarray_make bounded_def
serialise_u8_def[unfolded tuple_simps sanitizers]
(*
lemma serialise_le64_ret:
assumes valid_offs:
"unat offs + 7 < length (bounded buf)"
assumes ret:
"P (buf\<lparr>data\<^sub>f := WordArrayT.make (\<alpha>wa (data\<^sub>f buf)[
unat offs := u64_to_u8 v,
unat (offs+1) := u64_to_u8 (v >> 8),
unat (offs+2) := u64_to_u8 (v >> 16),
unat (offs+3) := u64_to_u8 (v >> 24),
unat (offs+4) := u64_to_u8 (v >> 32),
unat (offs+5) := u64_to_u8 (v >> 40),
unat (offs+6) := u64_to_u8 (v >> 48),
unat (offs+7) := u64_to_u8 (v >> 56)])\<rparr>)"
notes wa_modify_ret = wordarray_modify_ret[rotated - 1, simplified Let_def ArrayUseValueP.defs ArrA.defs]
shows
"P (serialise_le64 (buf, offs, v))"
unfolding serialise_le64_def[unfolded tuple_simps sanitizers]
apply (simp add: serialise_le64_simps Let_def)
apply (rule wa_modify_ret[where index="offs"], simp add: serialise_le64_simps)
apply (rule wa_modify_ret[where index="offs+1"], simp add: serialise_le64_simps)
apply (rule wa_modify_ret[where index="offs+2"], simp add: serialise_le64_simps)
apply (rule wa_modify_ret[where index="offs+3"], simp add: serialise_le64_simps)
apply (rule wa_modify_ret[where index="offs+4"], simp add: serialise_le64_simps)
apply (rule wa_modify_ret[where index="offs+5"], simp add: serialise_le64_simps)
apply (rule wa_modify_ret[where index="offs+6"], simp add: serialise_le64_simps)
apply (rule wa_modify_ret[where index="offs+7"], simp add: serialise_le64_simps)
using ret apply simp
using valid_offs
apply ((simp add: serialise_le64_simps) , unat_arith?)+
done
*)
lemma take_irrelevance:
"P (xs!(unat (x + y))) \<Longrightarrow> unat (x + y) < unat z \<Longrightarrow>
P ((take (unat z) xs)!(unat (x + y)))"
by auto
lemma unat_space:
assumes "unat (x + y) < z"
and "unat (x + y) > unat x"
and "y' \<le> y"
shows "unat (x + y') < z"
proof -
have "\<And>x\<^sub>1. unat (x + y) \<le> x\<^sub>1 \<or> \<not> z \<le> x\<^sub>1"
using assms(1) by fastforce
thus ?thesis using assms
by (metis antisym_conv leI less_not_sym word_le_nat_alt word_plus_mono_right)
qed
lemma ple32_ret:
assumes 1:"unat offs < unat (offs + 3)"
assumes 2:"unat (offs + 3) < (length $ bounded buf)"
assumes 3:"P(ple32 (bounded buf) offs)"
shows "P (deserialise_le32 (buf, offs))"
proof -
from 1 2 have 4:"unat offs + 3 < (length $ bounded buf)" by (unat_arith, auto?)
show ?thesis
apply(subst deserialise_le32_bounded_ret)
apply simp
using 1 2 apply unat_arith
apply auto[1]
using 1 2 apply unat_arith
using 3 apply auto
done
qed
lemma ple64_ret:
assumes 1:"unat offs < unat (offs + 7)"
assumes 2:"unat (offs + 7) < (length $ bounded buf)"
assumes 3:"P (ple64 (bounded buf) offs)"
shows "P (deserialise_le64 (buf, offs))"
proof -
from 1 2 have 4:"unat offs + 7 < (length $ bounded buf)" by (unat_arith, auto?)
show ?thesis
apply(subst deserialise_le64_bounded_ret)
apply simp
using 1 2 apply unat_arith
apply auto[1]
using 1 2 apply unat_arith
using 3 apply auto
done
qed
lemma offs_le:
assumes "offs < offs+n"
assumes "unat (offs + n) \<le> ntake"
shows "unat offs < ntake"
using assms by unat_arith
lemma word_add_eq_unat:
assumes "(offs::('a::len word)) < offs + n"
assumes "i < n"
shows "unat (offs + i) = unat offs + unat i"
using assms by unat_arith
lemma ple16_eq_slice2:
assumes "offs < offs + 2"
assumes "unat offs + 2 \<le> length xs"
shows "ple16 xs offs = ple16 (slice (unat offs) (unat offs + 2) xs) 0"
using assms by (simp add: slice_def ple16_def drop_take word_add_eq_unat)
lemma ple32_eq_slice4:
assumes "offs < offs + 4"
assumes "unat offs + 4 \<le> length xs"
shows "ple32 xs offs = ple32 (slice (unat offs) (unat offs + 4) xs) 0"
using assms by (simp add: slice_def ple32_def drop_take word_add_eq_unat)
lemma ple64_eq_slice8:
assumes "offs < offs + 8"
assumes "unat offs + 8 \<le> length xs"
shows "ple64 xs offs = ple64 (slice (unat offs) (unat offs + 8) xs) 0"
using assms by (simp add: slice_def ple64_def drop_take word_add_eq_unat)
definition pObjInode :: "U8 list \<Rightarrow> U32 \<Rightarrow> ObjInode\<^sub>T"
where
"pObjInode data offs \<equiv>
ObjInode.make
(((ple64 data offs) AND (NOT (bilbyFsOidMaskAll OR ucast word32Max))) OR bilbyFsOidMaskInode) (* id *)
(ple64 data (offs+8)) (* size *)
(ple64 data (offs+16)) (* atime *)
(ple64 data (offs+24)) (* ctime *)
(ple64 data (offs+32)) (* mtime *)
(ple32 data (offs+40)) (* nlink *)
(ple32 data (offs+44)) (* uid *)
(ple32 data (offs+48)) (* gid *)
(ple32 data (offs+52)) (* mode *)
(ple32 data (offs+56)) (* flags *)
(* End 60 bytes *)"
definition sObjInode :: "ObjInode\<^sub>T \<Rightarrow> U8 list"
where
"sObjInode odata \<equiv>
(sle64 $ ObjInode.id\<^sub>f odata)
@ (sle64 $ ObjInode.size\<^sub>f odata)
@ (sle64 $ ObjInode.atime_sec\<^sub>f odata)
@ (sle64 $ ObjInode.ctime_sec\<^sub>f odata)
@ (sle64 $ ObjInode.mtime_sec\<^sub>f odata)
@ (sle32 $ ObjInode.nlink\<^sub>f odata)
@ (sle32 $ ObjInode.uid\<^sub>f odata)
@ (sle32 $ ObjInode.gid\<^sub>f odata)
@ (sle32 $ ObjInode.mode\<^sub>f odata)
@ (sle32 $ ObjInode.flags\<^sub>f odata) (* End 60 bytes *)"
definition pObjHeader :: "U8 list \<Rightarrow> U32 \<Rightarrow> Obj\<^sub>T"
where
"pObjHeader data offs \<equiv>
Obj.make
(ple32 data offs) (* magic *)
(ple32 data (offs+4)) (* crc *)
(ple64 data (offs+8)) (* sqnum *)
(offs) (* offs not stored on medium *) (* changed back to offs, otherwise this doesnt correspond to the code*)
(ple32 data (offs+16)) (* len *)
(* 2 padding bytes *)
(data!unat (offs+22)) (* trans *)
(data!unat (offs+23)) (* otype *)
undefined (* ounion *)
(* End 24 bytes *)"
definition sObjHeader :: "Obj\<^sub>T \<Rightarrow> U8 list"
where
"sObjHeader obj \<equiv>
(sle32 $ Obj.magic\<^sub>f obj)
@ (sle32 $ Obj.crc\<^sub>f obj)
@ (sle64 $ Obj.sqnum\<^sub>f obj)
@ (sle32 $ Obj.len\<^sub>f obj)
@ [bilbyFsPadByte]
@ [bilbyFsPadByte]
@ [Obj.trans\<^sub>f obj]
@ [Obj.otype\<^sub>f obj] (* End 24 bytes *)"
lemma ObjHeader_inverse:
"pObjHeader (sObjHeader obj@xs) 0 = (obj\<lparr> Obj.ounion\<^sub>f := undefined, Obj.offs\<^sub>f := 0\<rparr>) "
apply(clarsimp simp: pObjHeader_def sObjHeader_def)
apply(clarsimp simp: Obj.defs)
apply(clarsimp simp: ple32_word_rcat_eq length_sle32 length_sle64)
apply(clarsimp simp: bilbyFsObjHeaderSize_def bilbyFsPadByte_def)
proof -
let ?magic = "sle32 (magic\<^sub>f obj)"
let ?crc = "sle32 (crc\<^sub>f obj)"
let ?sqnum = "sle64 (Obj.sqnum\<^sub>f obj)"
let ?len = "sle32 (Obj.len\<^sub>f obj)"
let ?tail = "0x42 # 0x42 # trans\<^sub>f obj # otype\<^sub>f obj # xs"
have append_assoc_intro : "\<And>P ys1 ys2 xs.
P ((ys1 @ ys2) @ xs) \<Longrightarrow> P (ys1 @ (ys2 @ xs))" by auto
have sqnum: "ple64 (?magic @ ?crc @ ?sqnum @ ?len @ ?tail) 8 = (Obj.sqnum\<^sub>f obj)"
apply(rule append_assoc_intro)
apply(rule ple64_word_rcat_eq)
apply(subst List.length_append)
using length_sle32 by auto
have len: "ple32 (?magic @ ?crc @ ?sqnum @ ?len @ ?tail) 16 = Obj.len\<^sub>f obj"
apply(rule append_assoc_intro[of _ "?magic"])
apply(rule append_assoc_intro[of _ "?magic @ ?crc"])
apply(rule append_assoc_intro[of _ "?magic @ ?crc @ ?sqnum"])
apply(rule ple32_word_rcat_eq)
using length_sle32 length_sle64 by auto
have trans:"(?magic @ ?crc @ ?sqnum @ ?len @ ?tail) ! 22 = Obj.trans\<^sub>f obj"
proof -
have "length (?magic @ ?crc @ ?sqnum @ ?len @ (66::8 word) # [66::8 word]) = 22"
using length_sle32 length_sle64 by simp
from this show ?thesis
by (metis (erased, hide_lams) append_Cons append_Nil append_assoc nth_append_length)
qed
have otype:"(?magic @ ?crc @ ?sqnum @ ?len @ ?tail) ! 23 = Obj.otype\<^sub>f obj"
proof -
have "length (?magic @ ?crc @ ?sqnum @ ?len @ (66::8 word) # (66::8 word) # [trans\<^sub>f obj]) = 23"
using length_sle32 length_sle64 by simp
from this show ?thesis
by (metis (erased, hide_lams) append_Cons append_Nil append_assoc nth_append_length)
qed
from sqnum len trans otype
show
"\<lparr>magic\<^sub>f = magic\<^sub>f obj, crc\<^sub>f = crc\<^sub>f obj,
sqnum\<^sub>f = ple64 (?magic @ ?crc @ ?sqnum @ ?len @ ?tail) 8,
offs\<^sub>f = 0,
len\<^sub>f = ple32 (?magic @ ?crc @ ?sqnum @ ?len @ ?tail) 16,
trans\<^sub>f = (?magic @ ?crc @ ?sqnum @ ?len @ ?tail) ! 22,
otype\<^sub>f = (?magic @ ?crc @ ?sqnum @ ?len @ ?tail) ! 23,
ounion\<^sub>f = undefined\<rparr> = obj\<lparr>ounion\<^sub>f := undefined, Obj.offs\<^sub>f := 0\<rparr>"
by auto
qed
lemmas pObjHeader_simp =
pObjHeader_def Let_def Obj.make_def bilbyFsObjHeaderSize_def
definition is_valid_ObjHeader :: "Obj\<^sub>T \<Rightarrow> U8 list \<Rightarrow> bool"
where
"is_valid_ObjHeader obj data \<equiv>
magic\<^sub>f obj = bilbyFsMagic \<and>
(unat $ Obj.len\<^sub>f obj) \<le> length data \<and>
trans\<^sub>f obj \<in> {bilbyFsTransIn, bilbyFsTransCommit} \<and>
is_len_and_type_ok (otype\<^sub>f obj, Obj.len\<^sub>f obj)"
lemma is_len_and_type_ok_hdr_szD:
"is_len_and_type_ok (otype, olen) \<Longrightarrow> bilbyFsObjHeaderSize \<le> olen"
by (auto simp add:
is_len_and_type_ok_def[unfolded sanitizers tuple_simps]
bilbyFsObjHeaderSize_def
prod.case_eq_if split: if_splits)
unat_arith+
lemma is_valid_ObjHeader_len_facts:
"is_valid_ObjHeader obj data \<Longrightarrow> unat bilbyFsObjHeaderSize \<le> length data \<and>
bilbyFsObjHeaderSize \<le> Obj.len\<^sub>f obj"
apply (clarsimp simp: is_valid_ObjHeader_def)
apply (drule is_len_and_type_ok_hdr_szD)
apply unat_arith
done
lemmas otype_simps =
bilbyFsObjTypeInode_def
bilbyFsObjTypeData_def
bilbyFsObjTypeDentarr_def
bilbyFsObjTypeDel_def
bilbyFsObjTypePad_def
bilbyFsObjTypeSuper_def
bilbyFsObjTypeSum_def
lemma is_len_and_type_ok_otype_valD:
"is_len_and_type_ok (otype, olen) \<Longrightarrow> otype \<in> {bilbyFsObjTypeInode,bilbyFsObjTypeData,bilbyFsObjTypeDentarr,bilbyFsObjTypeDel,bilbyFsObjTypePad,bilbyFsObjTypeSuper,bilbyFsObjTypeSum} "
by (auto simp add:
is_len_and_type_ok_def[unfolded sanitizers tuple_simps]
otype_simps split: if_splits)
definition is_valid_Obj :: "Obj\<^sub>T \<Rightarrow> bool"
where
"is_valid_Obj obj \<equiv>
if otype\<^sub>f obj = bilbyFsObjTypePad then \<exists>v. ounion\<^sub>f obj = TObjPad v else
if otype\<^sub>f obj = bilbyFsObjTypeInode then \<exists>v. ounion\<^sub>f obj = TObjInode v else
if otype\<^sub>f obj = bilbyFsObjTypeData then \<exists>v. ounion\<^sub>f obj = TObjData v else
if otype\<^sub>f obj = bilbyFsObjTypeDentarr then \<exists>v. ounion\<^sub>f obj = TObjDentarr v else
if otype\<^sub>f obj = bilbyFsObjTypeDel then \<exists>v. ounion\<^sub>f obj = TObjDel v else
True"
lemma is_valid_ObjHeader_len:
"is_valid_ObjHeader obj data \<Longrightarrow> bilbyFsObjHeaderSize \<le> Obj.len\<^sub>f obj"
apply (clarsimp simp add: is_valid_ObjHeader_def)
apply (erule is_len_and_type_ok_hdr_szD)
done
lemma is_valid_ObjHeader_len_unat:
"is_valid_ObjHeader obj data \<Longrightarrow> unat bilbyFsObjHeaderSize \<le> unat (Obj.len\<^sub>f obj)"
by (drule is_valid_ObjHeader_len) unat_arith
lemma is_valid_ObjHeader_buf_len:
"is_valid_ObjHeader obj data \<Longrightarrow>
(unat $ Obj.len\<^sub>f obj) \<le> length data \<and>
unat bilbyFsObjHeaderSize \<le> length data"
apply (clarsimp simp add: is_valid_ObjHeader_def)
apply (drule is_len_and_type_ok_hdr_szD)
apply unat_arith
done
definition sObjPad :: "U32 \<Rightarrow> U8 list"
where
"sObjPad olen \<equiv> replicate (unat (olen - bilbyFsObjHeaderSize)) bilbyFsPadByte"
consts pObjSummary :: "U8 list \<Rightarrow> U32 \<Rightarrow> ObjSummary\<^sub>T"
consts pObjPad :: "U8 list \<Rightarrow> U32 \<Rightarrow> unit"
definition pObjUnion :: "U8 list \<Rightarrow> U8 \<Rightarrow> U32 \<Rightarrow> U32 \<Rightarrow> ObjUnion\<^sub>T"
where
"pObjUnion data otype olen offs \<equiv>
if otype = bilbyFsObjTypePad then
TObjPad ()
else if otype = bilbyFsObjTypeData then
TObjData (pObjData data offs olen)
else if otype = bilbyFsObjTypeInode then
TObjInode (pObjInode data offs)
else if otype = bilbyFsObjTypeDentarr then
TObjDentarr (pObjDentarr data offs olen)
else if otype = bilbyFsObjTypeDel then
TObjDel (pObjDel data offs)
else if otype = bilbyFsObjTypeSuper then
TObjSuper (pObjSuper data offs)
else (*if otype = bilbyFsObjTypeSum then
TObjSummary (pObjSummary data offs) *) (* see comments in: serial.cogent for deserialise_ObjUnion:*)
TObjPad ()"
definition pObj :: "U8 list \<Rightarrow> U32 \<Rightarrow> Obj\<^sub>T"
where
"pObj data offs \<equiv>
let obj = pObjHeader data offs
in obj \<lparr>ounion\<^sub>f:= pObjUnion (take (unat offs + unat (Obj.len\<^sub>f obj)) data) (otype\<^sub>f obj) (Obj.len\<^sub>f obj) (offs+bilbyFsObjHeaderSize)\<rparr>"
text {* This could be implemented in Cogent instead *}
definition serialise_size_summary_Obj :: "ObjSummary\<^sub>T \<Rightarrow> U32"
where
"serialise_size_summary_Obj summary \<equiv>
bilbyFsObjHeaderSize + serialise_size_ObjSummary (nb_sum_entry\<^sub>f summary)"
definition os_sum_sz :: "OstoreState\<^sub>T \<Rightarrow> U32"
where
"os_sum_sz ostore_st \<equiv> serialise_size_summary_Obj (summary\<^sub>f ostore_st)"
definition bilbyFsMinObjSize :: U32
where
"bilbyFsMinObjSize \<equiv> bilbyFsObjHeaderSize + 8"
lemma deserialise_u8_ret:
assumes wf: "wellformed_buf buf"
assumes valid_offs:
"offs < bound\<^sub>f buf"
shows
"deserialise_u8 (buf, offs) = (\<alpha>wa $ data\<^sub>f buf) ! (unat offs)"
using valid_offs wordarray_get_ret[where arr="data\<^sub>f buf" and index=offs]
wf[simplified wellformed_buf_def]
apply (simp add: deserialise_u8_def)
apply (erule meta_impE)
apply unat_arith
apply simp
done
lemmas objheaders_simps = bilbyFsMagic_def
bilbyFsObjTypeInode_def bilbyFsObjTypeData_def
bilbyFsObjTypeDentarr_def bilbyFsObjTypeDel_def bilbyFsObjTypePad_def
bilbyFsObjTypeSuper_def bilbyFsObjTypeSum_def
bilbyFsTransIn_def bilbyFsTransCommit_def is_valid_ObjHeader_def pObjHeader_def
Obj.make_def
lemma deserialise_ObjHeader_ret:
assumes wf: "wellformed_buf buf"
assumes bound: "offs + bilbyFsObjHeaderSize \<le> bound\<^sub>f buf"
assumes no_of: "offs < offs + bilbyFsObjHeaderSize"
assumes err: "\<And>obj. P (obj, Error eInval)"
assumes suc:
"\<And>obj offs'. \<lbrakk> is_valid_ObjHeader (pObjHeader (\<alpha>wa (data\<^sub>f buf)) offs) (bounded buf) ;
\<exists>v. obj\<lparr>ounion\<^sub>f:=v\<rparr> = pObjHeader (\<alpha>wa (data\<^sub>f buf)) offs;
offs' = offs + bilbyFsObjHeaderSize;
offs + Obj.len\<^sub>f obj \<le> bound\<^sub>f buf;
offs < offs + Obj.len\<^sub>f obj\<rbrakk> \<Longrightarrow>
P (obj, Success (offs'))"
notes bilbyFsObjHeaderSize_def[simp]
shows "P (deserialise_ObjHeader (buf, offs, obj))"
proof -
have des_u8:
"deserialise_u8 (buf, offs + 23) = (\<alpha>wa $ data\<^sub>f buf) ! unat (offs + 23)"
"deserialise_u8 (buf, offs + 22) = (\<alpha>wa $ data\<^sub>f buf) ! unat (offs + 22)"
using bound no_of
by - ((subst deserialise_u8_ret[OF wf]), (unat_arith, simp+))+
have des_le64:
"deserialise_le64 (buf, offs + 8) = (ple64 (\<alpha>wa $ data\<^sub>f buf) (offs + 8))"
apply (rule ple64_ret)
using no_of
apply (simp add: )
apply (simp add: unat_arith_simps, unat_arith)
using bound wf no_of
apply (simp add: bounded_def wellformed_buf_def unat_arith_simps)
apply unat_arith
apply (simp add: bounded_def)
apply (subst ple64_take)
using bound no_of
apply (simp add: bounded_def unat_arith_simps)
apply unat_arith
using wf bound no_of
apply (simp add: wellformed_buf_def unat_arith_simps)
apply unat_arith
apply simp
done
have des_le32:
"deserialise_le32 (buf, offs) = (ple32 (\<alpha>wa $ data\<^sub>f buf) offs)"
"deserialise_le32 (buf, offs+4) = (ple32 (\<alpha>wa $ data\<^sub>f buf) (offs + 4))"
"deserialise_le32 (buf, offs+16) = (ple32 (\<alpha>wa $ data\<^sub>f buf) (offs + 16))"
ML_prf{*
fun solve_deserialise_le32 ctxt =
let
val add_simp = Simplifier.add_simp;
fun add_simps ctxt [] = ctxt
| add_simps ctxt (thm::thms) = add_simps (add_simp thm ctxt) thms;
val simp = Simplifier.asm_full_simp_tac;
val unat = (unat_arith_tac ctxt 1);
val ple32 = Method.rule_tac ctxt @{thms ple32_ret} [] 1;
val wf_bounded_unat = @{thms wellformed_buf_def bounded_def unat_arith_simps};
val simp_wf_bounded_unat = simp (add_simps ctxt wf_bounded_unat) 1;
val simp_bounded = simp (add_simp @{thm bounded_def} ctxt) 1;
val ple32_take = Method.rule_tac ctxt @{thms ple32_take} [] 1;
val simp_unat_plus = REPEAT_DETERM_N 2 ( simp_wf_bounded_unat THEN unat);
in
DETERM (ple32 THEN simp_unat_plus )
THEN (simp_bounded THEN ple32_take THEN simp_unat_plus)
end
*}
using wf bound no_of
by - (tactic {* solve_deserialise_le32 @{context} *})+
show ?thesis
unfolding deserialise_ObjHeader_def[unfolded tuple_simps sanitizers]
apply (clarsimp simp:Let_def err[simplified eInval_def])
apply (frule is_len_and_type_ok_hdr_szD)
apply (rule suc)
apply (clarsimp simp: objheaders_simps buf_simps des_le32 des_u8 )
apply (subgoal_tac "\<exists>v. ple32 (\<alpha>wa (data\<^sub>f buf)) (offs + 0x10) = v")
prefer 2
apply clarsimp
apply (erule exE, simp add: bounded_def)
using bound no_of wf apply (simp add: wellformed_buf_def)
apply (rule conjI)
apply unat_arith
apply (unat_arith)
apply (rule_tac x=undefined in exI)
apply (simp add: pObjHeader_def Obj.defs buf_simps des_le32 des_u8 des_le64)
apply (simp)
apply (simp, unat_arith)+
done
qed
definition
sObjUnion :: "ObjUnion\<^sub>T \<Rightarrow> U8 \<Rightarrow> U32 \<Rightarrow> U8 list"
where
"sObjUnion (ou::ObjUnion\<^sub>T) (otype::U8) (olen::U32) \<equiv>
case ou of
TObjDentarr odent \<Rightarrow> undefined (* TODO: no dentarr support for now *)
| TObjInode oinod \<Rightarrow> sObjInode oinod
| TObjData odata \<Rightarrow> sObjData odata olen
| TObjDel odel \<Rightarrow> sObjDel odel
| TObjSuper osup \<Rightarrow> sObjSuper osup
| TObjSummary g \<Rightarrow> undefined (* TODO: sObjSummary is undefined*)
| TObjPad opad \<Rightarrow> sObjPad olen"
lemmas bilbyFsObjTypes =
bilbyFsObjTypePad_def
bilbyFsObjTypeInode_def
bilbyFsObjTypeData_def
bilbyFsObjTypeDentarr_def
bilbyFsObjTypeDel_def
bilbyFsObjTypeSuper_def
bilbyFsObjTypeSum_def
lemma ObjUnion_inverse:
"\<And>v. ounion = TObjPad v \<Longrightarrow> otype = bilbyFsObjTypePad \<Longrightarrow>
pObjUnion (sObjUnion ounion otype olen @ xs) otype olen 0 = ounion"
by (simp add: sObjUnion_def pObjUnion_def )
lemma length_sObjUnion:
"\<And>v. ounion = TObjPad v \<Longrightarrow> otype = bilbyFsObjTypePad \<Longrightarrow>
olen \<ge> bilbyFsObjHeaderSize \<Longrightarrow>
length (sObjUnion ounion otype olen) = unat olen - unat bilbyFsObjHeaderSize"
apply (simp add: sObjUnion_def sObjPad_def )
apply unat_arith
done
definition sObj :: "Obj\<^sub>T \<Rightarrow> U8 list"
where
"sObj obj \<equiv> sObjHeader obj @ sObjUnion (ounion\<^sub>f obj) (otype\<^sub>f obj) (Obj.len\<^sub>f obj)"
lemma length_sObjHeader:
"length (sObjHeader obj) = unat bilbyFsObjHeaderSize"
by (simp add: sObjHeader_def length_sle32 length_sle64 bilbyFsObjHeaderSize_def)
lemma length_sObj:
"Obj.len\<^sub>f obj \<ge> bilbyFsObjHeaderSize \<Longrightarrow>
otype\<^sub>f obj = bilbyFsObjTypePad \<Longrightarrow>
is_valid_Obj obj \<Longrightarrow>
length (sObj obj) = unat (Obj.len\<^sub>f obj)"
apply (clarsimp simp add: is_valid_Obj_def split:if_splits)
apply (drule (2) length_sObjUnion)
apply (simp add: sObj_def length_sObjHeader word_le_nat_alt)
done
lemma Obj_inverse:
"otype\<^sub>f obj = bilbyFsObjTypePad \<Longrightarrow>
is_valid_Obj obj \<Longrightarrow>
Obj.offs\<^sub>f obj = 0 \<Longrightarrow>
pObj (sObj obj @ xs) 0 = obj"
unfolding pObj_def sObj_def Let_def
apply (simp add: ObjHeader_inverse)
apply (clarsimp simp: is_valid_Obj_def)
apply (frule (1) ObjUnion_inverse)
apply (simp add: pObjUnion_def sObjHeader_def word_le_nat_alt length_sObjHeader)
done
lemma buf_sub_slice_len_simplified:
"length v1 = unat j \<Longrightarrow> unat (offs :: 32 word) < length (\<alpha>wa (data\<^sub>f buf)) \<Longrightarrow>
unat (offs + j) \<le> length (\<alpha>wa (data\<^sub>f buf)) \<Longrightarrow>
unat offs < unat (offs + j) \<Longrightarrow>
length (take (unat offs) (\<alpha>wa (data\<^sub>f buf)) @
v1 @
drop (unat (offs + j)) (\<alpha>wa (data\<^sub>f buf))) = length (\<alpha>wa (data\<^sub>f buf))"
by simp unat_arith
lemma buf_sub_slice_absorb:
assumes len1: "length v1 = unat j"
and len2: "length v2 = unat (k-j)"
and j_less: "j \<le> k"
and j_nz: "j > 0"
and no_of: "unat offs < unat (offs + k)"
and len_ge: "unat (offs + k) \<le> length (\<alpha>wa (data\<^sub>f buf))"
shows "(buf_sub_slice (buf \<lparr>data\<^sub>f := WordArrayT.make
(buf_sub_slice buf offs (offs + j) v1)\<rparr>)
(offs + j) (offs + k)
v2) =
buf_sub_slice buf offs (offs + k) (v1 @ v2)"
proof -
have j_sub: "unat (offs + j) - unat offs = unat j"
using no_of j_less by unat_arith
have j_max: "unat (offs + j) \<ge> unat offs"
using no_of j_less by unat_arith
have k_j_sub: "unat (offs + k) - unat (offs + j) = unat (k - j)"
using no_of j_less by unat_arith
have k_sub: "(unat (offs + k) - unat offs) = unat k"
using no_of by unat_arith
have k_max: "(unat (offs + k)) \<ge> (unat offs)"
using no_of by unat_arith
have k_j_max: "(unat (offs + k)) \<ge> (unat (offs + j))"
using no_of j_less by unat_arith
have xx: "\<And>x v. data\<^sub>f (x\<lparr>data\<^sub>f := v\<rparr>) = v"
by simp
have len_ge': " unat offs < length (\<alpha>wa (data\<^sub>f buf))"
using len_ge no_of by unat_arith
have len_ge'': " unat (offs + j) \<le> length (\<alpha>wa (data\<^sub>f buf))"
using len_ge no_of j_less by unat_arith
have no_of': "unat offs < unat (offs + j)"
using no_of j_less j_nz by unat_arith
have len_app: "length (v1 @ v2) = unat k"
using len1 len2 j_less by unat_arith
have take_prefix: "(take (unat (offs + j))
(take (unat offs) (\<alpha>wa (data\<^sub>f buf)) @
v1 @ drop (unat (offs + j)) (\<alpha>wa (data\<^sub>f buf))))
= take (unat offs) (\<alpha>wa (data\<^sub>f buf)) @
v1"
using len1 no_of' len_ge' j_sub by simp
have drop_prefix: "drop (unat (offs + k))
(take (unat offs) (\<alpha>wa (data\<^sub>f buf)) @
v1 @ drop (unat (offs + j)) (\<alpha>wa (data\<^sub>f buf)))
= drop (unat (offs + k))(\<alpha>wa (data\<^sub>f buf))"
apply (subgoal_tac "(unat k - unat j + unat (offs + j)) = unat (offs + k)")
prefer 2
using no_of j_less apply unat_arith
using len1 len_ge' k_sub j_less no_of apply simp
by unat_arith
thus ?thesis
unfolding buf_sub_slice_def
using j_sub j_max k_j_sub k_sub k_max k_j_max apply (simp only: max_absorb1)
using len1
apply (subst take_append[where n="unat j"])+
apply (simp only: diff_self_eq_0 take_0 append_Nil2)
using len2 apply (subst take_append[where n="unat (k-j)"])+
apply (simp only: diff_self_eq_0 take_0 append_Nil2)
using len_app apply (subst take_append[where n="unat k"])
apply (simp only: diff_self_eq_0 take_0 append_Nil2)
using len1 k_j_sub apply (simp only:)
apply (simp only: xx wordarray_make fun_app_def)
using len1 len2 len_app apply (simp only: take_all[where n="unat j"]
take_all[where n="unat k"]
take_all[where n="unat (k-j)"])
using len1 len_ge len_ge' len_ge'' no_of' len_app no_of
by (simp add: buf_sub_slice_len_simplified take_prefix drop_prefix)
qed
lemma serialise_u8_ret':
notes wa_modify_ret = wordarray_modify_ret[rotated - 1, simplified Let_def]
assumes no_of: "offs < offs + 1"
and len_ge: "unat offs + 1 \<le> length (\<alpha>wa (data\<^sub>f buf))"
shows "serialise_u8 (buf, offs, v) =
buf \<lparr>data\<^sub>f := WordArrayT.make (buf_sub_slice buf offs (offs + 1) [v])\<rparr>"
proof -
have offs_sub: "(unat (offs + 1) - unat offs) = 1" using no_of by unat_arith
have no_of_unat: " unat offs < unat (offs + 1)" using no_of by (simp add: word_less_nat_alt)
show ?thesis
unfolding serialise_u8_def[unfolded sanitizers] Let_def
using no_of len_ge
apply simp
apply (rule wa_modify_ret[where index="offs" and varr="(data\<^sub>f buf)"])
prefer 2
apply (unat_arith)
apply (simp_all add:ArrA.defs ElemAO.defs ElemA.defs
setu8_def[unfolded tuple_simps sanitizers] wordarray_make buf_simps
min_absorb1 min_absorb2)
apply (rule arg_cong[where f="\<lambda>v. Buffer.data\<^sub>f_update v buf"])
apply (rule ext)
apply (rule arg_cong[where f="WordArrayT.make"])
apply (simp only: list_eq_iff_nth_eq)
apply (clarsimp simp: buf_sub_slice_length)
apply (simp add: buf_sub_slice_def min_absorb1 min_absorb2)
apply (case_tac "i=unat offs")
apply (simp only: append_assoc[symmetric] nth_append)
apply (simp add: min_absorb1 min_absorb2)
apply unat_arith
apply (case_tac "i < unat offs")
apply (simp add: min_absorb1 offs_sub max_absorb1 no_of no_of_unat nth_append)
apply (simp add: min_absorb1 offs_sub max_absorb1)
apply (subgoal_tac "(max (unat (offs + 1)) (unat offs)) = unat (offs + 1)")
prefer 2
using no_of_unat apply auto[1]
apply (clarsimp simp add: nth_append nth_Cons split: nat.splits)
apply (subst nth_drop)
apply unat_arith
apply (subgoal_tac "unat (offs + 1) = unat offs + 1")
prefer 2
using no_of_unat offs_sub apply simp
apply simp
apply (subgoal_tac "i = Suc (unat offs + x2)")
apply simp
apply unat_arith
done
qed
lemma serialise_ObjHeader_ret:
assumes no_overflow: "offs \<le> offs + bilbyFsObjHeaderSize"
and is_valid_obj: "is_valid_ObjHeader obj (drop (unat offs) (\<alpha>wa (data\<^sub>f buf)))"
and suc: "\<And>buf' offs'.
offs' = offs + bilbyFsObjHeaderSize \<Longrightarrow>
buf' = buf\<lparr>data\<^sub>f := WordArrayT.make (buf_sub_slice buf offs (offs +bilbyFsObjHeaderSize) (sObjHeader obj))\<rparr> \<Longrightarrow>
P (buf', offs')"
shows
"P (serialise_ObjHeader (buf, offs, obj))"
proof -
have offs_le_length: "unat offs \<le> length (\<alpha>wa (data\<^sub>f buf))"
using is_valid_ObjHeader_len_facts[OF is_valid_obj]
by (clarsimp simp: is_valid_ObjHeader_def bilbyFsObjHeaderSize_def) unat_arith
have offs_sub_le: "(unat (offs + bilbyFsObjHeaderSize) - unat offs) \<le> (length (\<alpha>wa (data\<^sub>f buf)) - unat offs)"
using is_valid_obj is_valid_ObjHeader_len_facts[OF is_valid_obj]
by (clarsimp simp: is_valid_ObjHeader_def bilbyFsObjHeaderSize_def) unat_arith
have offs_len_sub_eq: "unat (offs + bilbyFsObjHeaderSize) - unat offs = unat (bilbyFsObjHeaderSize)"
using no_overflow by unat_arith
have offs_obj_len_le_length: "unat (offs + bilbyFsObjHeaderSize) \<le> length (\<alpha>wa (data\<^sub>f buf))"
using is_valid_obj offs_sub_le is_valid_ObjHeader_len_facts[OF is_valid_obj]
by (clarsimp simp: is_valid_ObjHeader_def bilbyFsObjHeaderSize_def) unat_arith
have offs_obj_len_le_length': "(unat (offs + bilbyFsObjHeaderSize) -
(unat offs + unat bilbyFsObjHeaderSize)) \<le> (length (\<alpha>wa (data\<^sub>f buf)) -
(unat offs + unat bilbyFsObjHeaderSize))"
using offs_obj_len_le_length by unat_arith
have offs_plus_eq: " (unat (offs + bilbyFsObjHeaderSize) = (unat offs + unat bilbyFsObjHeaderSize))"
using no_overflow by unat_arith
show ?thesis
unfolding serialise_ObjHeader_def[unfolded sanitizers tuple_simps]
apply (simp add: Let_def)
apply (rule suc)
apply (simp add: bilbyFsObjHeaderSize_def)
apply (simp add: buf_sub_slice_def wordarray_make)
apply (simp add: min_absorb1 offs_le_length offs_sub_le)
apply (simp add: offs_len_sub_eq length_sObjHeader
offs_obj_len_le_length' offs_plus_eq)
using no_overflow apply (simp add: word_le_nat_alt max_absorb1 bilbyFsObjHeaderSize_def)
using no_overflow offs_obj_len_le_length apply (simp add: bilbyFsObjHeaderSize_def)
apply (subst serialise_le32_ret[where v="magic\<^sub>f obj"])
apply ((unat_arith, auto)+)[2]
apply (subst serialise_le32_ret[where v="crc\<^sub>f obj"])
apply ((unat_arith, auto)+)[1]
apply (simp add: buf_sub_slice_length wordarray_make)
apply (unat_arith, auto)[1]
apply (simp)
apply (subst add.commute[where a=8])
apply (subst buf_sub_slice_absorb[where offs=offs and j=4 and k=8, simplified])
apply (simp add: length_sle32)+
apply unat_arith
apply auto[1]
apply unat_arith
apply auto[1]
apply (subst serialise_le64_ret)
apply (unat_arith, auto)[1]
apply (simp add: buf_sub_slice_length wordarray_make)
apply (unat_arith, auto)[1]
apply simp
apply (subst add.commute[where a="0x10"])
apply (subst buf_sub_slice_absorb)
apply (simp add: length_sle32 length_sle64)+
apply ((unat_arith, auto)+)[2]
apply (subst serialise_le32_ret)
apply ((unat_arith, auto)+)[1]
apply (simp add: buf_sub_slice_length wordarray_make)
apply (unat_arith, auto)[1]
apply (simp)
apply (subst add.commute[where a="0x14"])
apply (subst buf_sub_slice_absorb)
apply (simp add: length_sle32 length_sle64)+
apply ((unat_arith, auto)+)[2]
apply (subst serialise_u8_ret'[where offs="offs + 0x14"])
apply (unat_arith, auto)[1]
apply (simp add: buf_sub_slice_length wordarray_make)
apply (unat_arith, auto)[1]
apply (simp)
apply (subst add.commute[where a="0x15"])
apply (subst buf_sub_slice_absorb)
apply (simp add: length_sle32 length_sle64)+
apply ((unat_arith, auto)+)[2]
apply (subst serialise_u8_ret'[where offs="offs + 0x15"])
apply (unat_arith, auto)[1]
apply (simp add: buf_sub_slice_length wordarray_make)
apply (unat_arith, auto)[1]
apply (simp)
apply (subst add.commute[where a="0x16"])
apply (subst buf_sub_slice_absorb)
apply (simp add: length_sle32 length_sle64)+
apply ((unat_arith, auto)+)[2]
apply (subst serialise_u8_ret'[where offs="offs + 0x16"])
apply (unat_arith, auto)[1]
apply (simp add: buf_sub_slice_length wordarray_make)
apply (unat_arith, auto)[1]
apply (simp)
apply (subst add.commute[where a="0x17"])
apply (subst buf_sub_slice_absorb)
apply (simp add: length_sle32 length_sle64)+
apply ((unat_arith, auto)+)[2]
apply (subst serialise_u8_ret'[where offs="offs + 0x17"])
apply (unat_arith, auto)[1]
apply (simp add: buf_sub_slice_length wordarray_make)
apply (unat_arith, auto)[1]
apply (simp)
apply (subst add.commute[where a="0x18"])
apply (subst buf_sub_slice_absorb)
apply (simp add: length_sle32 length_sle64)+
apply ((unat_arith, auto)+)[2]
apply (simp add: sObjHeader_def bilbyFsPadByte_def)
apply (unfold buf_sub_slice_def)
apply (simp add: offs_len_sub_eq[unfolded bilbyFsObjHeaderSize_def, simplified])
apply (simp add: length_sle32 length_sle64)
apply (subgoal_tac "(length (\<alpha>wa (data\<^sub>f buf)) - unat offs) \<ge> 24")
prefer 2
using offs_len_sub_eq bilbyFsObjHeaderSize_def apply (unat_arith, auto)[1]
apply simp
apply (subgoal_tac "(unat (offs + 0x18)) > (unat offs)")
prefer 2
using no_overflow apply (unat_arith, auto)[1]
apply (simp add: max_absorb1)
apply (rule arg_cong[where f="\<lambda>v. Buffer.data\<^sub>f_update v buf"])
apply (rule ext)
apply (rule arg_cong[where f="WordArrayT.make"])
apply simp
by (subst take_all,
( simp add: length_sle32 length_sle64 | (unat_arith, auto)[1] )+
)+
qed
lemmas ObjUnion_splits = ObjUnion.splits
lemma take_drop_decomp:"x \<ge> a \<Longrightarrow> take (x - a) (drop a xs) @ drop x xs = drop a xs"
by (metis drop_take drop_take_drop)
lemma serialise_ObjPad_ret:
assumes no_overflow: "offs \<le> offs + (olen - bilbyFsObjHeaderSize)"
and no_underflow: "olen - bilbyFsObjHeaderSize \<ge> 0"
and bound: "offs+ (olen - bilbyFsObjHeaderSize) \<le> bound\<^sub>f buf \<and> unat (bound\<^sub>f buf) \<le> length (\<alpha>wa (data\<^sub>f buf))"
and suc: "\<And>buf' offs'.
offs' = offs + olen - bilbyFsObjHeaderSize \<Longrightarrow>
buf' = buf\<lparr>data\<^sub>f := WordArrayT.make (buf_sub_slice buf offs (offs + (olen - bilbyFsObjHeaderSize)) (sObjPad olen))\<rparr> \<Longrightarrow>
P (buf', offs')"
shows
"P (serialise_ObjPad (buf, offs, olen))"
proof -
have offs_le_bound: "offs \<le> bound\<^sub>f buf"
using bound no_overflow by unat_arith
have sub1: "(unat (olen - 0x18)) \<le> (unat (bound\<^sub>f buf) - unat offs)"
using bound no_overflow no_underflow apply (clarsimp simp: bilbyFsObjHeaderSize_def)
by unat_arith
have sub2: "(unat (offs + (olen - 0x18)) - unat offs) = unat (olen - 0x18)"
using bound no_overflow no_underflow apply (clarsimp simp: bilbyFsObjHeaderSize_def)
by unat_arith (* takes ages *)
have sub3: "unat (olen - 0x18) \<le> (length (\<alpha>wa (data\<^sub>f buf)) - unat offs)"
using bound no_overflow no_underflow apply (clarsimp simp: bilbyFsObjHeaderSize_def)
by unat_arith
have sub4: "(unat (offs + (olen - 0x18)) - (unat offs + unat (olen - 0x18))) = 0"
using bound no_overflow no_underflow apply (clarsimp simp: bilbyFsObjHeaderSize_def)
by unat_arith
have sub5: "(unat offs +
(unat (olen - 0x18) + length (\<alpha>wa (data\<^sub>f buf))) -
unat (offs + (olen - 0x18))) = length (\<alpha>wa (data\<^sub>f buf))"
using bound no_overflow no_underflow apply (clarsimp simp: bilbyFsObjHeaderSize_def)
by unat_arith
have no_of_unat: "unat offs \<le> (unat (offs + (olen - 0x18)))"
using no_overflow no_underflow by (simp add: bilbyFsObjHeaderSize_def word_le_nat_alt)
have assoc: "(unat (offs + (olen - 0x18))) = unat offs + unat (olen - 0x18)"
using no_overflow no_underflow by (simp add: bilbyFsObjHeaderSize_def) unat_arith
show ?thesis
unfolding serialise_ObjPad_def[unfolded sanitizers tuple_simps]
apply (simp add: Let_def split: ObjUnion_splits)
apply (rule suc)
apply (simp add: bilbyFsObjHeaderSize_def)
apply (subst buf_memset_eq)
using bound apply simp
using no_overflow apply (simp add: bilbyFsObjHeaderSize_def)
apply (rule arg_cong[where f="\<lambda>v. Buffer.data\<^sub>f_update v buf"])
apply (rule ext)
apply (rule arg_cong[where f="WordArrayT.make"])
using bound offs_le_bound apply (clarsimp simp: buf_sub_slice_def bilbyFsObjHeaderSize_def)
apply (simp add: sObjPad_def bilbyFsPadByte_def buf_simps
min_absorb1 min_absorb2 word_le_nat_alt sub1 sub2 sub3 sub4 sub5
bilbyFsObjHeaderSize_def no_of_unat max_absorb1 assoc)
apply (subst take_drop_decomp)
using no_overflow no_underflow apply (clarsimp simp: bilbyFsObjHeaderSize_def)
apply simp
done
qed
lemma serialise_ObjUnion_ret:
assumes no_overflow: "offs \<le> offs + (olen - bilbyFsObjHeaderSize)"
and otype: "otype = bilbyFsObjTypePad"
and ounion: "\<And>v. ounion = TObjPad v"
and olen: " 0 \<le> olen - bilbyFsObjHeaderSize"
and bound: "offs + (olen - bilbyFsObjHeaderSize) \<le> bound\<^sub>f buf \<and> unat (bound\<^sub>f buf) \<le> length (\<alpha>wa (data\<^sub>f buf))"
and suc: "\<And>buf' offs'.
offs' = offs + olen - bilbyFsObjHeaderSize \<Longrightarrow>
buf' = buf\<lparr>data\<^sub>f := WordArrayT.make (buf_sub_slice buf offs (offs + (olen - bilbyFsObjHeaderSize)) (sObjUnion ounion otype olen))\<rparr> \<Longrightarrow>
P (buf', offs')"
shows
"P (serialise_ObjUnion (buf, offs, ounion, olen))"
unfolding serialise_ObjUnion_def[unfolded sanitizers tuple_simps]
using ounion apply (simp add: Let_def split: ObjUnion_splits)
apply (rule serialise_ObjPad_ret)
using no_overflow apply simp
using olen apply simp
using bound apply simp
apply (rule suc, simp)
apply (simp add: sObjUnion_def)
done
lemma data\<^sub>f_of_data\<^sub>f_update:
"data\<^sub>f (x\<lparr>data\<^sub>f := v\<rparr>) = v"
by simp
lemma serialise_Obj_ret:
assumes no_overflow: "offs \<le> offs + Obj.len\<^sub>f obj"
and is_valid_obj: "is_valid_ObjHeader obj (drop (unat offs) (\<alpha>wa (data\<^sub>f buf)))"
and otype: "otype\<^sub>f obj = bilbyFsObjTypePad"
and ounion: "\<And>v. ounion\<^sub>f obj = TObjPad v"
and bound: " offs + Obj.len\<^sub>f obj \<le> bound\<^sub>f buf \<and>
unat (bound\<^sub>f buf) \<le> length (\<alpha>wa (data\<^sub>f buf))"
and suc: "\<And>buf'.
buf' = buf\<lparr>data\<^sub>f := WordArrayT.make (buf_sub_slice buf offs (offs + Obj.len\<^sub>f obj) (sObj obj))\<rparr> \<Longrightarrow>
P (buf', offs + Obj.len\<^sub>f obj)"
shows
"P (serialise_Obj (buf, offs, obj))"
unfolding serialise_Obj_def[unfolded tuple_simps sanitizers]
apply (simp add: Let_def)
apply (rule serialise_ObjHeader_ret)
using no_overflow is_valid_obj apply (clarsimp simp: is_valid_ObjHeader_def bilbyFsObjHeaderSize_def)
apply (frule is_len_and_type_ok_hdr_szD, simp add: bilbyFsObjHeaderSize_def)
apply unat_arith
using is_valid_obj apply assumption
apply simp
apply (rule serialise_ObjUnion_ret)
using is_valid_obj no_overflow apply (clarsimp simp: is_valid_ObjHeader_def bilbyFsObjHeaderSize_def )
apply (frule is_len_and_type_ok_hdr_szD)
apply (simp add: bilbyFsObjHeaderSize_def)
apply unat_arith
apply (rule otype)
using ounion apply simp
using is_valid_obj no_overflow apply (clarsimp simp: is_valid_ObjHeader_def bilbyFsObjHeaderSize_def)
using bound apply (simp add: wordarray_make buf_sub_slice_length)
apply simp
apply (rule suc)
apply (rule arg_cong[where f="\<lambda>v. Buffer.data\<^sub>f_update v buf"])
apply (rule ext)
apply (rule arg_cong[where f="WordArrayT.make"])
apply (thin_tac x for x)+
apply (subst buf_sub_slice_absorb)
apply (simp add: length_sObjHeader)
apply (subst length_sObjUnion[OF ounion otype])
using is_valid_obj apply (clarsimp simp: is_valid_ObjHeader_def is_len_and_type_ok_hdr_szD)
using is_valid_obj no_overflow apply (clarsimp simp: is_valid_ObjHeader_def unat_plus_simple)
apply (drule is_len_and_type_ok_hdr_szD)
apply (unat_arith)
apply (simp add: is_len_and_type_ok_hdr_szD)
apply(simp add: bilbyFsObjHeaderSize_def)
using no_overflow is_valid_obj apply (clarsimp simp: is_valid_ObjHeader_def bilbyFsObjHeaderSize_def)
apply (simp add: is_len_and_type_ok_def otype otype_simps)
apply (unat_arith)
using bound is_valid_obj apply (clarsimp simp: is_valid_ObjHeader_def)
apply unat_arith
apply (simp add: sObj_def)
done
lemma binNot_NOT: "binNot (x::64 word) = NOT x"
unfolding binNot_def[unfolded Let_def]
by (rule subst[where s="-1"], fastforce, fastforce)
lemma deserialise_ObjDel_ret:
assumes bound: "unat offs + 8 \<le> length (\<alpha>wa $ data\<^sub>f buf)"
assumes err: "P (Error (eInval, ex))"
assumes offs: "offs < offs + 8"
assumes suc:
"\<And>obj offs'. \<lbrakk>
obj = pObjDel (\<alpha>wa $ data\<^sub>f buf) offs;
ObjDel.id\<^sub>f obj AND NOT bilbyFsOidMaskAll \<in>
{ bilbyFsOidMaskData, bilbyFsOidMaskInode,bilbyFsOidMaskDentarr};
offs' = offs + 8\<rbrakk> \<Longrightarrow>
P (Success (ex, obj, offs'))"
shows "P (deserialise_ObjDel (ex, buf, offs))"
proof -
have des_le64: "deserialise_le64 (buf, offs) = ple64 (\<alpha>wa $ data\<^sub>f buf) offs"
using bound offs
by (fastforce intro!: deserialise_le64_ret simp: unat_arith_simps)
show ?thesis
unfolding deserialise_ObjDel_def[unfolded tuple_simps sanitizers]
apply (clarsimp simp: Let_def err[simplified eInval_def])
by (fastforce
intro: suc
simp: Let_def binNot_NOT bilbyFsOidMaskData_def des_le64 bilbyFsOidMaskAll_def
bilbyFsOidMaskInode_def bilbyFsOidMaskDentarr_def pObjDel_def ObjDel.make_def)
qed
lemma deserialise_ObjInode_ret:
assumes bound: "unat offs + 60 \<le> length (\<alpha>wa $ data\<^sub>f buf)"
assumes offs: "offs < offs + 60"
assumes err: "\<And>ex e. e \<in> {eInval, eNoMem} \<Longrightarrow> P (Error (e, ex))"
assumes suc:
"\<And>ex oi offs'. \<lbrakk>
oi = pObjInode (\<alpha>wa (data\<^sub>f buf)) offs;
offs' = offs + 60\<rbrakk> \<Longrightarrow>
P (Success (ex, oi, offs'))"
shows "P (deserialise_ObjInode (ex, buf, offs))"
proof -
have des_le64:
"deserialise_le64 (buf, offs) = (ple64 (\<alpha>wa $ data\<^sub>f buf) offs)"
"deserialise_le64 (buf, offs + 8) = (ple64 (\<alpha>wa $ data\<^sub>f buf) (offs + 8))"
"deserialise_le64 (buf, offs + 16) = (ple64 (\<alpha>wa $ data\<^sub>f buf) (offs + 16))"
"deserialise_le64 (buf, offs + 24) = (ple64 (\<alpha>wa $ data\<^sub>f buf) (offs + 24))"
"deserialise_le64 (buf, offs + 32) = (ple64 (\<alpha>wa $ data\<^sub>f buf) (offs + 32))"
using bound offs
by - (simp,rule deserialise_le64_ret[simplified];
(simp add: unat_arith_simps, unat_arith?))+
have des_le32:
"deserialise_le32 (buf, offs + 40) = (ple32 (\<alpha>wa $ data\<^sub>f buf) (offs + 40))"
"deserialise_le32 (buf, offs + 44) = (ple32 (\<alpha>wa $ data\<^sub>f buf) (offs + 44))"
"deserialise_le32 (buf, offs + 48) = (ple32 (\<alpha>wa $ data\<^sub>f buf) (offs + 48))"
"deserialise_le32 (buf, offs + 52) = (ple32 (\<alpha>wa $ data\<^sub>f buf) (offs + 52))"
"deserialise_le32 (buf, offs + 56) = (ple32 (\<alpha>wa $ data\<^sub>f buf) (offs + 56))"
using bound offs
by - (simp,rule deserialise_le32_ret[simplified];
(simp add: unat_arith_simps, unat_arith?))+
show ?thesis
unfolding deserialise_ObjInode_def[unfolded tuple_simps sanitizers]
by (fastforce
intro: suc err
split: R.split
simp: eInval_def eNoMem_def binNot_NOT Let_def bilbyFsOidMaskAll_def des_le32
bilbyFsOidMaskInode_def word32Max_def pObjInode_def ObjInode.make_def des_le64)
qed
lemma deserialise_ObjSuper_ret:
assumes bound: "unat offs + 40 \<le> length (\<alpha>wa $ data\<^sub>f buf)"
assumes offs: "offs \<le> offs + 40" (* added by Yutaka on 11th.*)
assumes err: "\<And>ex. P (Error (eNoMem, ex))"
assumes suc:
"\<And>ex osup offs'. \<lbrakk>
osup = pObjSuper (\<alpha>wa (data\<^sub>f buf)) offs;
offs' = offs + 40\<rbrakk> \<Longrightarrow>
P (Success (ex, osup, offs'))"
shows "P (deserialise_ObjSuper (ex, buf, offs))"
proof -
have des_le64:
"deserialise_le64 (buf, offs + 32) = (ple64 (\<alpha>wa $ data\<^sub>f buf) (offs + 32))"
using bound offs
by - (simp,rule deserialise_le64_ret[simplified];
(simp add: unat_arith_simps, unat_arith?))
have des_le32:
"deserialise_le32 (buf, offs) = (ple32 (\<alpha>wa $ data\<^sub>f buf) offs)"
"deserialise_le32 (buf, offs + 4) = (ple32 (\<alpha>wa $ data\<^sub>f buf) (offs + 4))"
"deserialise_le32 (buf, offs + 8) = (ple32 (\<alpha>wa $ data\<^sub>f buf) (offs + 8))"
"deserialise_le32 (buf, offs + 12) = (ple32 (\<alpha>wa $ data\<^sub>f buf) (offs + 12))"
"deserialise_le32 (buf, offs + 16) = (ple32 (\<alpha>wa $ data\<^sub>f buf) (offs + 16))"
"deserialise_le32 (buf, offs + 20) = (ple32 (\<alpha>wa $ data\<^sub>f buf) (offs + 20))"
"deserialise_le32 (buf, offs + 24) = (ple32 (\<alpha>wa $ data\<^sub>f buf) (offs + 24))"
"deserialise_le32 (buf, offs + 28) = (ple32 (\<alpha>wa $ data\<^sub>f buf) (offs + 28))"
using bound offs
by - (simp,rule deserialise_le32_ret[simplified];
(simp add: unat_arith_simps, unat_arith?))+
show ?thesis
unfolding deserialise_ObjSuper_def[unfolded tuple_simps sanitizers]
by (fastforce
intro: suc err[unfolded eNoMem_def]
split: R.split
simp: pObjSuper_def ObjSuper.make_def des_le32 des_le64)
qed
lemma slice_Cons_helper:
"i < length xs \<Longrightarrow>
xs \<noteq> [] \<Longrightarrow>
drop i xs =
(xs ! i) # drop ( (i + 1)) xs"
apply (cases xs, simp_all)
by (metis (no_types, hide_lams) drop_Suc_Cons Cons_nth_drop_Suc length_Cons)
lemma slice_singleton:
"f < length xs \<Longrightarrow> slice f (Suc f) xs = [xs ! f]"
unfolding slice_def by (simp add:drop_take list_eq_iff_nth_eq)
lemma take_n_minus_1_append:
"0<n \<Longrightarrow> xs \<noteq> [] \<Longrightarrow> n \<le> length xs \<Longrightarrow>
take (n - Suc 0) xs @ [xs ! (n - Suc 0)] = take n xs"
apply (simp only: list_eq_iff_nth_eq)
apply clarsimp
apply (case_tac "(length xs) < (n - Suc 0)")
apply (clarsimp simp add: min_absorb2)+
by (metis One_nat_def Suc_pred' elem_take_n le0 le_less_trans diff_le_self
less_not_refl linorder_neqE_nat diff_Suc_less take_Suc_conv_app_nth)
lemma take_n_minus_1_append_eq:
"v = xs ! (unat (n - 1)) \<Longrightarrow> unat n \<le> length xs \<Longrightarrow> n> 0 \<Longrightarrow>
take (unat ((n::U32) - 1)) xs @ [v] = take (unat n) xs"
apply (simp add: list_eq_iff_nth_eq min_absorb2 unat_arith_simps)
apply clarsimp
apply (subst take_n_minus_1_append)
apply simp+
apply (case_tac xs, simp_all)
done
lemma slice_n_minus_1_append_last:
"unat acc + unat n \<le> length xs \<Longrightarrow>
(n::U32) > 0 \<Longrightarrow>
acc \<le> acc + n \<Longrightarrow>
slice (unat acc) (unat acc + unat (n - 1)) xs @
[xs ! unat (acc + (n - 1))] =
slice (unat acc) (unat acc + unat n) xs"
apply (simp add: slice_def list_eq_iff_nth_eq)
apply (subgoal_tac "(length xs) \<ge> (unat acc + unat (n - 1))")
prefer 2
apply unat_arith
apply (rule conjI)
apply (simp add: min_absorb1 min_absorb2)
apply (clarsimp simp: drop_take min_absorb1 min_absorb2 )
apply (subst take_n_minus_1_append_eq)
apply simp
apply (rule arg_cong[where f="nth xs"])
apply unat_arith (* takes long *)
apply simp+
done
lemma map_deserialise_waU8_map_eq_slice_apply:
assumes nonempty: "xs \<noteq> []"
assumes "length xs = unat (n:: 32 word)"
assumes n_gr_0: "n > 0"
assumes no_overflow: "acc \<le> acc + n"
assumes bound: "unat acc + length xs \<le> length (\<alpha>wa d)"
shows "
(mapAccumObs 0 (length xs) deserialise_waU8_map xs acc d) =
(FunBucket.slice (unat acc) (unat acc + (length xs)) (\<alpha>wa d), acc + n)"
using assms
apply (clarsimp simp: mapAccumObs_def ElemAO.make_def
deserialise_waU8_map_def[unfolded tuple_simps sanitizers] slice_def[where frm=0])
apply (induct "xs" arbitrary: n rule: rev_nonempty_induct)
apply (drule sym, simp add: slice_singleton wordarray_get_ret unat_arith_simps)
apply (drule_tac x="n - 1" in meta_spec)
apply (erule meta_impE)
apply unat_arith
apply (erule meta_impE)
apply (subgoal_tac "unat n \<ge> 2")
apply unat_arith
apply (case_tac xs, simp, simp)
apply (erule meta_impE)
apply unat_arith
apply (erule meta_impE)
apply unat_arith
apply (simp add: prod.case_eq_if)
apply (rule wordarray_get_ret')
apply unat_arith (* takes a while *)
apply (simp only: slice_n_minus_1_append_last)
done
lemma map_deserialise_waU8_map_eq_slice:
assumes n_gr_0: "n > 0"
assumes no_overflow: "acc \<le> acc + n"
assumes bound: "unat acc + unat n \<le> length (\<alpha>wa d)"
assumes "length xs = unat (n:: 32 word)"
shows "
prod.fst (mapAccumObs 0 (unat n) deserialise_waU8_map xs acc d) =
(FunBucket.slice (unat acc) (unat acc + unat n ) (\<alpha>wa d))"
using map_deserialise_waU8_map_eq_slice_apply[THEN arg_cong[where f=prod.fst]]
assms
by (subgoal_tac "xs \<noteq> []") (fastforce simp: unat_arith_simps)+
lemma deserialise_wordarray_U8_ret:
assumes err: "\<And>ex. P (Error (eNoMem, ex))"
assumes suc:
"\<And>ex wa.
offs \<le> offs + len \<longrightarrow> unat offs + unat len \<le> length (\<alpha>wa $ data\<^sub>f buf) \<longrightarrow>
wa = WordArrayT.make (slice (unat offs) (unat offs + unat len) (\<alpha>wa (data\<^sub>f buf))) \<Longrightarrow>
P (Success (ex, wa))"
shows "P (deserialise_wordarray_U8 (ex, buf, offs, len))"
unfolding deserialise_wordarray_U8_def[unfolded tuple_simps sanitizers]
apply (simp add: Let_def)
apply (rule wordarray_create_ret)
apply simp
apply (simp add: err[unfolded eNoMem_def])
apply (rename_tac ex' wa)
apply simp
apply (rule wordarray_copy_ret)
apply (simp add:Let_def prod.case_eq_if)
apply (rule suc)
apply clarsimp
done
lemma deserialise_ObjData_ret:
assumes offs_no_of: "offs \<le> offs + (olen - bilbyFsObjHeaderSize)"
assumes buf_len: "unat (offs + (olen - bilbyFsObjHeaderSize)) \<le> length (\<alpha>wa (data\<^sub>f buf))"
assumes olen: "is_len_and_type_ok (bilbyFsObjTypeData, olen)"
assumes err: "\<And>ex e. e \<in> {eInval, eNoMem} \<Longrightarrow> P (Error (e, ex))"
assumes suc:
"\<And>ex od offs' . \<lbrakk>
ObjData.id\<^sub>f od AND NOT bilbyFsOidMaskAll OR bilbyFsOidMaskData = ObjData.id\<^sub>f od;
od = pObjData (\<alpha>wa (data\<^sub>f buf)) offs olen;
offs' = offs + olen - bilbyFsObjHeaderSize\<rbrakk> \<Longrightarrow>
P (Success (ex, od, offs'))"
shows "P (deserialise_ObjData (ex, buf, offs, olen))"
proof -
have hdr_le_olen: "bilbyFsObjDataHeaderSize \<le> (olen - bilbyFsObjHeaderSize)"
using olen
by (simp add: is_len_and_type_ok_def[unfolded sanitizers tuple_simps] otype_simps
bilbyFsObjHeaderSize_def bilbyFsObjDataHeaderSize_def) unat_arith
have offs_pl_hdr_le_offs_pl_olen:
"offs + bilbyFsObjDataHeaderSize \<le> offs + (olen - bilbyFsObjHeaderSize)"
using hdr_le_olen offs_no_of
by (simp add: bilbyFsObjDataHeaderSize_def bilbyFsObjHeaderSize_def word_plus_mono_right)
have offs_pl_hdr_no_of:
"offs < offs + bilbyFsObjDataHeaderSize"
using offs_no_of hdr_le_olen
by (simp add: bilbyFsObjDataHeaderSize_def bilbyFsObjHeaderSize_def)
unat_arith
have offs_pl_hdr_le_buf_len:
"unat offs + unat bilbyFsObjDataHeaderSize \<le> length (\<alpha>wa (data\<^sub>f buf))"
using buf_len hdr_le_olen offs_pl_hdr_no_of offs_pl_hdr_le_offs_pl_olen
by (simp add: bilbyFsObjHeaderSize_def bilbyFsObjDataHeaderSize_def)
unat_arith
have unat_offs_pl_olen_etc_eq: "unat (offs + (olen - bilbyFsObjHeaderSize)) = unat (offs + 8) + unat (0xFFFFFFE0 + olen)"
using olen hdr_le_olen offs_pl_hdr_no_of offs_pl_hdr_le_offs_pl_olen
apply (simp add: bilbyFsObjHeaderSize_def bilbyFsObjDataHeaderSize_def)
apply (simp add: is_len_and_type_ok_def[unfolded sanitizers tuple_simps] otype_simps bilbyFsObjHeaderSize_def)
apply (subgoal_tac "unat (offs + (olen - 0x18)) = unat (offs + 8) + unat (olen - 0x18 - 8)")
apply unat_arith
apply (simp add: unat_arith_simps)
apply unat_arith
done
show ?thesis
unfolding deserialise_ObjData_def[unfolded tuple_simps sanitizers]
apply (clarsimp simp: Let_def err[unfolded eNoMem_def eInval_def] binNot_NOT)
apply (rule deserialise_wordarray_U8_ret)
apply (simp add: err)
apply (erule impE)
using offs_pl_hdr_no_of apply (simp add: bilbyFsObjHeaderSize_def bilbyFsObjDataHeaderSize_def add.commute add.assoc)
apply (subgoal_tac "olen + 0xFFFFFFE8 = olen - 0x18") (* Oh! Beloved words <3 *)
prefer 2
apply simp
apply (simp only:)
apply simp
using offs_pl_hdr_le_offs_pl_olen apply (simp add: bilbyFsObjHeaderSize_def bilbyFsObjDataHeaderSize_def )
apply simp
apply (rule suc)
apply simp
apply (simp add: bilbyFsOidMaskAll_def bilbyFsOidMaskData_def
pObjData_def ObjData.make_def bilbyFsObjHeaderSize_def)
apply (simp add: Let_def pObjData_def ObjData.make_def bilbyFsObjHeaderSize_def bilbyFsObjDataHeaderSize_def)
apply (subst deserialise_le64_ret)
using offs_pl_hdr_le_buf_len[simplified bilbyFsObjHeaderSize_def bilbyFsObjDataHeaderSize_def]
apply (simp add:)
using offs_pl_hdr_no_of
apply (simp add: bilbyFsObjDataHeaderSize_def)
apply (erule impE)
using buf_len unat_offs_pl_olen_etc_eq
apply simp
apply simp
apply (simp add: bilbyFsObjHeaderSize_def)
done
qed
lemma deserialise_ObjPad_ret:
assumes err: "P (Error (eInval, ex))"
assumes suc: "\<And> out offs' .
\<lbrakk> olen - bilbyFsObjHeaderSize \<le> olen ;
out=();
offs' = offs + (olen - bilbyFsObjHeaderSize) \<rbrakk> \<Longrightarrow>
P (Success (ex, out, offs'))"
shows "P (deserialise_ObjPad (ex, buf, offs, olen))"
unfolding deserialise_ObjPad_def[unfolded tuple_simps sanitizers]
by (auto simp: Let_def err[unfolded eInval_def] suc[unfolded bilbyFsObjHeaderSize_def] split: R.split)
lemma no_offs_overflow:
assumes wellformed_buf: "wellformed_buf buf"
assumes no_overflow: "length (\<alpha>wa $ data\<^sub>f buf) \<le> unat bilbyFsMaxEbSize"
assumes offs_bound: "offs \<le> (bound\<^sub>f buf)"
assumes "n < bilbyFsMaxEbSize"
assumes "m < bilbyFsMaxEbSize"
shows "offs + n \<le> offs + n + m"
using assms
by (auto simp add: bilbyFsMaxEbSize_def wellformed_buf_def unat_arith_simps)
lemma no_offs_overflow_le:
assumes wellformed_buf: "wellformed_buf buf"
assumes no_overflow: "length (\<alpha>wa $ data\<^sub>f buf) \<le> unat bilbyFsMaxEbSize"
assumes offs_bound: "offs \<le> (bound\<^sub>f buf)"
assumes "n < bilbyFsMaxEbSize"
assumes "m < bilbyFsMaxEbSize"
assumes "m > 0"
shows "offs + n < offs + n + m"
using assms
by (auto simp add: bilbyFsMaxEbSize_def wellformed_buf_def unat_arith_simps)
lemma conc_offs_no_of:
assumes wellformed_buf: "wellformed_buf buf"
assumes no_overflow: "length (\<alpha>wa $ data\<^sub>f buf) \<le> unat bilbyFsMaxEbSize"
assumes offs_bound: "offs \<le> (bound\<^sub>f buf)"
assumes "m < bilbyFsMaxEbSize"
assumes "m > 0"
shows "offs < offs + m"
using assms
by (auto simp add: bilbyFsMaxEbSize_def wellformed_buf_def unat_arith_simps)
lemma slice_take:
"m \<le> l \<Longrightarrow>
slice n m (take l xs) = slice n m xs"
by (simp add: slice_def)
lemma deserialise_pu8_ret:
assumes valid_offs:
"unat offs + 1 < length (\<alpha>wa $ data\<^sub>f buf)"
assumes no_of:
"offs < offs + 1"
shows
"deserialise_u8 (buf, offs) = (pu8 (\<alpha>wa $ data\<^sub>f buf) offs)"
proof -
from no_of have no_of': "offs \<le> offs + 1" by simp
hence offs_pl_1: "unat (offs + 1) = unat offs + 1" by (simp add: unat_plus_simple)
show ?thesis
using valid_offs
apply (clarsimp simp: wordarray_get_ret[where arr="data\<^sub>f buf"]
deserialise_u8_def pu8_def)
apply (rule trans, rule word_rcat_rsplit[symmetric])
apply (rule arg_cong[where f=word_rcat])
apply (subst word_rsplit_upt[where n=1], simp add: word_size)
apply (simp)
apply (simp add: slice_def)
apply (simp add: ucast_def)
apply (subst Cons_nth_drop_Suc[symmetric])
apply simp
apply simp
done
qed
lemma pu8_take:
assumes offs:"offs < offs+1"
assumes ntake:"unat (offs + 1) \<le> ntake"
shows "pu8 (take ntake ys) offs = pu8 ys offs"
apply (simp add: pu8_def)
apply (rule arg_cong[where f="word_rcat"])
apply (rule slice_take)
using ntake offs by unat_arith
lemma deserialise_ObjDentry_ret:
assumes wellformed_buf: "wellformed_buf buf"
assumes no_buf_overflow: "length (\<alpha>wa $ data\<^sub>f buf) \<le> unat bilbyFsMaxEbSize"
assumes bound: "end_offs \<le> bound\<^sub>f buf"
assumes off_less_end_offs: "offs \<le> end_offs"
assumes err:
"\<And>ex e. e \<in> {eInval, eNoMem} \<Longrightarrow> P (Error (e, ex))"
assumes suc:
"\<And>ex dentry offs'. \<lbrakk>
unat offs + 8 + unat (wordarray_length (name\<^sub>f dentry)) \<le> unat (bound\<^sub>f buf);
wordarray_length (name\<^sub>f dentry) \<le> bilbyFsMaxNameLen + 1;
offs + 8 + wordarray_length (name\<^sub>f dentry) \<le> end_offs ;
dentry = pObjDentry (take (unat end_offs) (\<alpha>wa (data\<^sub>f buf))) offs ;
offs' = offs + 8 + wordarray_length (name\<^sub>f dentry);
offs' \<le> (bound\<^sub>f buf)
\<rbrakk> \<Longrightarrow>
P (Success (ex, dentry, offs'))"
shows "P (deserialise_ObjDentry (ex, buf, offs, end_offs))"
proof -
{
fix ex' dentry offs'
assume des_suc: "unat offs + 8 \<le> unat (bound\<^sub>f buf)"
then have offs_ok:"\<forall>n\<in>{0..7}. unat (offs + n) < length (\<alpha>wa $ data\<^sub>f buf)"
proof -
from wellformed_buf[unfolded wellformed_buf_def] des_suc
have "unat offs + 8 \<le> length (\<alpha>wa $ data\<^sub>f buf)"
by unat_arith
thus ?thesis
by unat_arith
qed
from des_suc have deserialises:
"deserialise_le32 (buf, offs) = (ple32 (\<alpha>wa $ data\<^sub>f buf) offs)"
"deserialise_u8 (buf, offs + 4) = (pu8 (\<alpha>wa $ data\<^sub>f buf) (offs + 4))"
"deserialise_le16 (buf, offs + 6) = (ple16 (\<alpha>wa $ data\<^sub>f buf) (offs + 6))"
apply clarsimp
apply(rule deserialise_le32_ret[simplified])
using assms[simplified bilbyFsMaxEbSize_def wellformed_buf_def]
apply unat_arith
using assms[simplified bilbyFsMaxEbSize_def ]
apply unat_arith
apply (subst deserialise_pu8_ret)
using offs_ok des_suc wellformed_buf
apply (simp add: wellformed_buf_def, unat_arith)
using des_suc
apply unat_arith
apply simp+
apply(rule deserialise_le16_ret[simplified])
using offs_ok des_suc wellformed_buf apply (simp add: wellformed_buf_def, unat_arith)
using des_suc
apply unat_arith
done
}
note deserialises = this
have offs_le_bound: "offs \<le> bound\<^sub>f buf"
using off_less_end_offs bound by simp
have const_offs_no_of: "\<And>n. n < bilbyFsMaxEbSize \<Longrightarrow> 0 < n \<Longrightarrow> offs < offs + n"
apply (rule conc_offs_no_of[OF wellformed_buf no_buf_overflow, unfolded bilbyFsMaxEbSize_def, simplified])
using offs_le_bound by (simp add:bilbyFsMaxEbSize_def)+
note no_of_8 = no_offs_overflow[OF wellformed_buf no_buf_overflow offs_le_bound, where m=8 and n=0, unfolded bilbyFsMaxEbSize_def, simplified, simplified unat_plus_simple]
show ?thesis
unfolding deserialise_ObjDentry_def[simplified tuple_simps sanitizers]
apply (clarsimp simp: Let_def err[unfolded eNoMem_def eInval_def])
apply (subst (asm) not_less)+
apply (rule deserialise_wordarray_U8_ret)
apply (clarsimp simp add: err)
apply(clarsimp simp add: err eNoMem_def Let_def prod.case_eq_if split: R.splits)
apply (erule impE)
apply (rule no_offs_overflow[OF wellformed_buf no_buf_overflow])
using off_less_end_offs bound apply fastforce
apply (simp add: bilbyFsMaxEbSize_def)+
apply unat_arith
apply (subgoal_tac "unat offs + unat (8::32word) + unat (ucast (deserialise_le16 (buf, offs + 6))) \<le> unat end_offs")
prefer 2
apply (subst add.assoc)
apply (subst unat_plus_simple[THEN iffD1, symmetric])
apply (simp add: unat_arith_simps)
apply (subst unat_plus_simple[THEN iffD1, symmetric])
apply (rule no_offs_overflow[OF wellformed_buf no_buf_overflow, where n=0, simplified])
using off_less_end_offs bound apply fastforce
apply (simp add: bilbyFsMaxEbSize_def)+
apply (simp add: unat_arith_simps)
apply (simp add: word_le_nat_alt[symmetric] add.assoc)
apply (erule impE)
using bound wellformed_buf[unfolded wellformed_buf_def]
apply (simp add: unat_arith_simps)
apply unat_arith
apply (subgoal_tac "unat offs + 8 \<le> unat (bound\<^sub>f buf)")
prefer 2
apply (subst unat_plus_simple[THEN iffD1, symmetric,
where y="8::32word", simplified])
apply (rule no_offs_overflow[OF wellformed_buf no_buf_overflow,
where n=0, simplified])
using off_less_end_offs bound apply fastforce
apply (simp add: bilbyFsMaxEbSize_def)+
apply (subst word_le_nat_alt[symmetric])
apply (cut_tac no_offs_overflow[OF wellformed_buf no_buf_overflow,
where offs=offs and n=8 and m="ucast (deserialise_le16 (buf, offs + 6))"])
using off_less_end_offs bound apply (simp_all add: bilbyFsMaxEbSize_def)
apply unat_arith
apply (simp add: deserialises)
apply (subgoal_tac "wordarray_length (WordArrayT.make
(FunBucket.slice (unat (offs + 8))
(unat (offs + 8) + unat (ucast (ple16 (\<alpha>wa (data\<^sub>f buf)) (offs + 6)) :: 32 word))
(\<alpha>wa (data\<^sub>f buf)))) \<le> ucast (ple16 (\<alpha>wa (data\<^sub>f buf)) (offs + 6))")
prefer 2
apply (subst wordarray_length_ofnat)
apply (simp add: wordarray_length_ret)
apply (subst wordarray_make)
apply (simp add: slice_length)
apply (subst min_absorb1)
prefer 3
using wellformed_buf[unfolded wellformed_buf_def] no_buf_overflow[unfolded bilbyFsMaxEbSize_def]
apply (simp add: unat_arith_simps)
apply (subgoal_tac
"unat (ucast (ple16 (\<alpha>wa (data\<^sub>f buf)) (offs + 6)) :: 32 word) =
unat (ple16 (\<alpha>wa (data\<^sub>f buf)) (offs + 6))")
prefer 2
apply (fastforce intro: uint_up_ucast simp: eq_nat_nat_iff unat_def is_up)
apply (rule suc)
apply (simp_all add: Let_def pObjDentry_def ObjDentry.make_def bilbyFsMaxNameLen_def)
using bound apply unat_arith
using wellformed_buf[unfolded wellformed_buf_def] no_buf_overflow[unfolded bilbyFsMaxEbSize_def]
apply (simp add: unat_arith_simps)
apply (simp add: ple16_take ple32_take const_offs_no_of bilbyFsMaxEbSize_def plus_no_overflow_unat_lift[OF const_offs_no_of[unfolded bilbyFsMaxEbSize_def, simplified]])
apply (subst ple16_take)
apply (rule no_offs_overflow_le[OF wellformed_buf no_buf_overflow offs_le_bound])
apply (simp add: bilbyFsMaxEbSize_def)+
using no_of_8
apply (simp add: add.commute)
apply (subst ple16_take)
apply (rule no_offs_overflow_le[OF wellformed_buf no_buf_overflow offs_le_bound])
apply (simp add: bilbyFsMaxEbSize_def)+
using no_of_8
apply (simp add: add.commute)
apply (subst pu8_take)
using no_offs_overflow[OF wellformed_buf no_buf_overflow offs_le_bound, where m=5 and n=0, unfolded bilbyFsMaxEbSize_def, simplified]
no_offs_overflow[OF wellformed_buf no_buf_overflow offs_le_bound, where m=4 and n=0, unfolded bilbyFsMaxEbSize_def, simplified]
apply (simp add: add.commute unat_plus_simple)
apply unat_arith
using no_of_8
no_offs_overflow[OF wellformed_buf no_buf_overflow offs_le_bound, where m=5 and n=0, unfolded bilbyFsMaxEbSize_def, simplified]
apply (fastforce simp add: unat_plus_simple add.commute)
apply (subst ObjDentry.surjective, simp)
apply (rule arg_cong[where f=WordArrayT.make])
apply (rule slice_take[symmetric], simp)
apply (rule word_unat.Rep_eqD)
apply (simp add: wordarray_length_ret wordarray_make length_slice)
using no_of_8 wellformed_buf
apply (simp add: wellformed_buf_def)
apply unat_arith
using wellformed_buf[unfolded wellformed_buf_def] no_buf_overflow[unfolded bilbyFsMaxEbSize_def]
apply (simp add: unat_arith_simps)
done
qed
lemma loop_deserialise_ObjDentry_ret:
assumes wellformed_buf: "wellformed_buf buf"
assumes no_buf_overflow: "length (\<alpha>wa $ data\<^sub>f buf) \<le> unat bilbyFsMaxEbSize"
assumes bound: "end_offs \<le> bound\<^sub>f buf"
assumes off_less_end_offs: "offs \<le> end_offs"
assumes st_offs: "st_offs \<le> offs"
shows "case loop_deserialise_ObjDentry (OptElemAO.make dentry (ex, offs) (buf, end_offs)) of
Break (none, e, ex) \<Rightarrow> none= Option.None () \<and> e = eInval
| Iterate (optdentry, ex, offs') \<Rightarrow>
\<exists>dentry. optdentry = Option.Some dentry \<and>
unat offs + 8 + unat (wordarray_length (name\<^sub>f dentry)) \<le> unat (bound\<^sub>f buf) \<and>
wordarray_length (name\<^sub>f dentry) \<le> bilbyFsMaxNameLen + 1 \<and>
offs + 8 + wordarray_length (name\<^sub>f dentry) \<le> end_offs \<and>
dentry = pObjDentry (take (unat end_offs) (\<alpha>wa (data\<^sub>f buf))) offs \<and>
offs' = offs + 8 + wordarray_length (name\<^sub>f dentry) \<and>
offs' \<le> (bound\<^sub>f buf)"
unfolding loop_deserialise_ObjDentry_def[unfolded tuple_simps sanitizers]
apply (clarsimp simp: Let_def OptElemAO.make_def)
apply (rule deserialise_ObjDentry_ret[OF assms(1-4)])
by (clarsimp simp: eInval_def)+
lemma slice_Cons:
"frm < length xs \<Longrightarrow> frm < to
\<Longrightarrow> slice frm to xs = xs ! frm # slice (Suc frm) to xs"
apply (simp add: slice_def)
apply (subst slice_Cons_helper[where i=frm], simp_all)
apply clarsimp
done
lemma slice_list_update:
"n < length xs
\<Longrightarrow> slice i j (xs[n := x]) = (if n < i then slice i j xs
else if n \<ge> j then slice i j xs
else (slice i j xs)[n - i := x])"
by (simp add: slice_def drop_list_update take_list_update)
lemma mapAccumObsOpt_step:
assumes frm: "frm < to" "frm < length xs"
shows "mapAccumObsOpt frm to fn xs vacc obs =
(case fn (OptElemAO.make (xs ! frm) vacc obs)
of Iterate (oelem, acc) \<Rightarrow>
mapAccumObsOpt (Suc frm) to fn (xs [frm := oelem]) acc obs
| Break (oelem, d) \<Rightarrow> Break (xs [frm := oelem], d))"
proof -
let ?folder = "(\<lambda>elem. case_LoopResult (\<lambda>(ys, d). Break (ys @ [elem], d))
(\<lambda>(ys, acc).
case fn (OptElemAO.make elem acc obs) of
Break (oelem, d) \<Rightarrow> Break (ys @ [oelem], d)
| Iterate (oelem, acc) \<Rightarrow> Iterate (ys @ [oelem], acc)))"
{ fix xs ys d
have fold_break: "fold ?folder xs (Break (ys, d))
= Break (ys @ xs, d)"
by (induct xs arbitrary: ys d, simp_all)
}
note fold_break = this
have fold_iterate_Cons: "\<And>xs. \<forall>y ys acc. fold ?folder xs (Iterate (y # ys, acc))
= (case (fold ?folder xs (Iterate (ys, acc)))
of Iterate (zs, acc) \<Rightarrow> Iterate (y # zs, acc)
| Break (zs, d) \<Rightarrow> Break (y # zs, d))"
apply (induct_tac xs, simp_all)
apply clarsimp
apply (case_tac "fn (OptElemAO.make a acc obs)")
apply (clarsimp simp add: fold_break)
apply clarsimp
done
from frm have drop_helper: "\<And>x xs. drop (to - frm) (x # xs) = drop (to - Suc frm) xs"
apply (cases "to - frm", simp_all)
apply (cases to, simp_all)
apply (cases frm, simp_all)
apply (metis Suc_diff_Suc Suc_inject)
done
show ?thesis using frm
apply (simp add: mapAccumObsOpt_def)
apply (simp add: slice_Cons)
apply (cases "fn (OptElemAO.make (xs ! frm) vacc obs)")
apply (clarsimp simp: fold_break)
apply (simp add: slice_def upd_conv_take_nth_drop max_absorb2)
apply (subst append_take_drop_id
[where xs="drop (Suc frm) xs" and n="to -frm - 1",
simplified take_drop, symmetric])
apply simp
apply (clarsimp simp: mapAccumObsOpt_def slice_list_update take_list_update)
apply (simp add: fold_iterate_Cons)
apply (simp split: LoopResult.split)
apply (clarsimp simp: slice_def upd_conv_take_nth_drop min_absorb2 max_absorb2
drop_helper)
done
qed
lemma mapAccumObsOpt_n_n:
"mapAccumObsOpt n n fn xs vacc obs = Iterate (xs, vacc)"
by (clarsimp simp: mapAccumObsOpt_def slice_n_n)
lemma mapAccumObsOpt_frm_eq_len:
"frm = length xs \<Longrightarrow> mapAccumObsOpt frm to fn xs vacc obs = Iterate (xs @ [], vacc)"
by (clarsimp simp: mapAccumObsOpt_def slice_def)
lemma snd_fold_simp:
"prod.snd (fold (\<lambda>_ (a, b). (f a b, f' b)) xs (a,b)) =
fold (\<lambda>_ b. f' b) xs b"
by (induct xs arbitrary: a b, simp_all)
lemma fst_fold_append_simp:
"prod.fst (fold (\<lambda>_ (xs, n). (xs @ [f n], f' n)) ls (f n' # xs, f' n)) =
f n' # prod.fst (fold (\<lambda>_ (xs, n). (xs @ [f n], f' n)) ls (xs, f' n)) "
by (induct ls arbitrary: n xs, simp_all)
lemma snd_snd_fold_simp:
"(prod.snd (fold (\<lambda>_ (xs, doffs, offslist). (f xs doffs, f' doffs, f'' doffs offslist)) ls (xs, n, offslist))) =
fold (\<lambda>_ (doffs, offslist). (f' doffs, f'' doffs offslist)) ls (n, offslist)"
by (induct ls arbitrary: xs n offslist, simp_all)
lemma snd_fold_append_gen_simp:
"prod.snd (fold (\<lambda>_ (x, xs). (f' x, xs @ [f x])) ls (x, xs @ ys)) =
xs @ prod.snd (fold (\<lambda>_ (x, xs). (f' x, xs @ [f x])) ls (x, ys))"
by (induct ls arbitrary: x ys, simp_all)
lemma snd_fold_append_simp:
"prod.snd (fold (\<lambda>_ (x, xs). (f' x, xs @ [f x])) ls (x, xs)) =
xs @ prod.snd (fold (\<lambda>_ (x, xs). (f' x, xs @ [f x])) ls (x, []))"
using snd_fold_append_gen_simp[where ys=Nil, simplified] .
lemma fst_fold_triple_simp:
"prod.fst (fold (\<lambda>_ (a, b, c). (f a b, f' b, f'' b c)) ns (a, b, c)) =
prod.fst (fold (\<lambda>_ (a, b). (f a b, f' b)) ns (a, b))"
by (induct ns arbitrary: a b c, simp_all)
lemma fst_snd_fold_triple_simp:
"prod.fst (prod.snd (fold (\<lambda>_ (a, b, c). (f a b, f' b, f'' b c)) ns (a, b, c))) =
prod.snd (fold (\<lambda>_ (a, b). (f a b, f' b)) ns (a, b))"
by (induct ns arbitrary: a b c, simp_all)
definition dentarr_offs_list_drop :: "U8 list \<Rightarrow> U32 \<Rightarrow> nat list \<Rightarrow> U32 \<Rightarrow> (32 word list)"
where
"dentarr_offs_list_drop data ost entriesno offs =
prod.snd (fold (\<lambda>_ (doffs, offslist).
let dentry = pObjDentry (drop (unat offs) data) (doffs - offs);
newoffs = doffs + 8 + wordarray_length (ObjDentry.name\<^sub>f dentry)
in (newoffs, offslist @ [newoffs]))
entriesno (ost, []))
"
definition
dentarr_offs_list_drop_end_offs_pred
where
"dentarr_offs_list_drop_end_offs_pred data ost entriesno offs end_offs \<equiv>
\<forall>v\<in>set (dentarr_offs_list_drop data ost entriesno offs).
v \<le> end_offs"
definition
"dentarr_offs_list data ost entriesno \<equiv>
(prod.snd (fold (\<lambda>_ (doffs, offslist).
let dentry = pObjDentry data doffs;
newoffs = doffs + 8 + wordarray_length (ObjDentry.name\<^sub>f dentry)
in (newoffs, offslist @ [newoffs]))
entriesno (ost, [])))"
definition
dentarr_offs_list_end_offs_pred
where
"dentarr_offs_list_end_offs_pred data ost entriesno end_offs \<equiv>
\<forall>v\<in>set (dentarr_offs_list data ost entriesno).
v \<le> end_offs"
definition
dentarr_otype_end_offs_pred
where
"dentarr_otype_end_offs_pred otype data offs end_offs \<equiv>
(otype = bilbyFsObjTypeDentarr \<longrightarrow>
(let nbentry = ple32 data (offs + 8)
in dentarr_offs_list_end_offs_pred data (offs+bilbyFsObjDentarrHeaderSize) [0..<unat nbentry] end_offs))"
lemmas dentarr_end_offs_simps = dentarr_offs_list_def dentarr_offs_list_end_offs_pred_def
dentarr_otype_end_offs_pred_def
definition
dentarr_otype_drop_end_offs_pred
where
"dentarr_otype_drop_end_offs_pred otype data offs end_offs \<equiv>
(otype = bilbyFsObjTypeDentarr \<longrightarrow>
(let nbentry = ple32 data (offs+8)
in dentarr_offs_list_drop_end_offs_pred data (offs+bilbyFsObjDentarrHeaderSize)
[0..<unat nbentry] offs end_offs))
"
definition
dentarr_otype_drop_end_offs_st_pred
where
"dentarr_otype_drop_end_offs_st_pred otype data offs st_offs end_offs \<equiv>
(otype = bilbyFsObjTypeDentarr \<longrightarrow>
(let nbentry = ple32 data (offs+8)
in dentarr_offs_list_drop_end_offs_pred data (offs+bilbyFsObjDentarrHeaderSize)
[0..<unat nbentry] st_offs end_offs))
"
lemmas dentarr_drop_end_offs_simps = dentarr_offs_list_drop_def dentarr_offs_list_drop_end_offs_pred_def
dentarr_otype_drop_end_offs_pred_def dentarr_otype_drop_end_offs_st_pred_def
lemma ple32_eq_slice:
assumes "offs < offs + 4"
assumes "unat offs + 4 \<le> length xs"
assumes "offs + 4 < end_offs"
shows "ple32 xs offs = ple32 (slice (unat offs) (unat end_offs) xs) 0"
using assms
apply (simp add: slice_def ple32_def drop_take word_add_eq_unat)
apply (drule less_to_le, simp add: unat_plus_simple word_less_nat_alt)
done
lemma split_upt_on_l_n:
"n < m \<Longrightarrow> l \<le> n \<Longrightarrow> [l ..< m] = [l ..< n] @ [n] @ [Suc n ..< m]"
apply (subst upt_add_eq_append')
apply simp+
apply (simp add: upt_conv_Cons)
done
lemma unat_plus_simple_imp:
"x \<le> (x::'a::len word) + y \<Longrightarrow> (unat (x + y) = unat x + unat y)"
by (simp add: unat_plus_simple)
lemma pObjDentry_drop_eq:
assumes offs_le_ost: "offs \<le> ost"
and ost_no_of8: " ost < ost + 8"
and ost_le_offs_olen: " ost \<le> end_offs"
and offs_olen_ys: "unat end_offs \<le> length ys"
and ys_le_max: " length ys \<le> unat bilbyFsMaxEbSize"
and end_offs: "end_offs_nat = unat end_offs"
shows " pObjDentry (take end_offs_nat ys) ost = pObjDentry (drop (unat offs) (take end_offs_nat ys)) (ost - offs)"
proof -
have ost_4_nat: "unat (ost + 4) = unat ost + 4"
using ost_no_of8 by (simp add: unat_arith_simps) unat_arith
have ost_le_max: "ost \<le> bilbyFsMaxEbSize" using ys_le_max offs_olen_ys ost_le_offs_olen
by unat_arith
hence offs_le_max: "offs \<le> bilbyFsMaxEbSize"
using offs_le_ost by unat_arith
have ost_minus_offs_bound: "ost - offs \<le> bilbyFsMaxEbSize"
using offs_le_ost ost_le_max
by unat_arith
have ost_no_ofs: "ost < ost + 4" "ost < ost + 6" using ost_no_of8
by (clarsimp simp add: unat_arith_simps , unat_arith)+
hence ost_offs_x: "unat (ost - offs + 4) = unat ost - unat offs + 4"
"unat (ost - offs + 6) = unat ost - unat offs + 6"
"unat (ost - offs + 8) = unat ost - unat offs + 8"
using offs_le_ost offs_le_ost[simplified word_le_nat_alt] ost_4_nat
ost_minus_offs_bound
apply (simp_all add: bilbyFsMaxEbSize_def)
apply ((drule plus_no_overflow_unat_lift)+,
(subst unat_plus_simple_imp,
simp only: word_le_nat_alt, unat_arith,subst unat_sub, simp+))
apply ((drule plus_no_overflow_unat_lift)+,
(subst unat_plus_simple_imp,
simp only: word_le_nat_alt, unat_arith,subst unat_sub, simp+))
apply ((drule plus_no_overflow_unat_lift)+)
apply (subst unat_plus_simple_imp)
apply (simp only: word_le_nat_alt word_less_nat_alt)
using offs_le_max[simplified bilbyFsMaxEbSize_def word_le_nat_alt]
ost_no_of8
apply (simp only:unat_arith_simps)
apply unat_arith
apply (subst unat_sub, simp+)
done
have offs_cancel: "(unat ost - unat offs + 4 + unat offs) = unat ost + 4"
"(unat ost - unat offs + 6 + unat offs) = unat ost + 6"
"(unat ost - unat offs + 8 + unat offs) = unat ost + 8"
using offs_le_ost[simplified word_less_nat_alt] by unat_arith+
have ple16_eq: "ple16 (take end_offs_nat ys) (ost + 6) = ple16 (drop (unat offs) (take end_offs_nat ys)) (ost - offs + 6)"
apply (simp add: ple16_def)
apply (rule arg_cong[where f=word_rcat])
apply (rule arg_cong[where f=rev])
apply (rule arg_cong[where f="take 2"])
apply (fastforce simp add: ost_offs_x offs_cancel less_to_le[OF ost_no_ofs(2), simplified unat_plus_simple])
done
have offs_cancel': "\<forall>v. unat ost - unat offs + 8 + unat v + unat offs = unat ost + 8 + unat v"
using offs_le_ost[simplified word_less_nat_alt]
by unat_arith
show ?thesis
apply (simp add: pObjDentry_def Let_def ObjDentry.make_def)
apply (rule conjI)
apply (simp add: ple32_def)
apply (rule arg_cong[where f=word_rcat])
apply (rule arg_cong[where f=rev])
apply (rule arg_cong[where f="take 4"])
apply (subst unat_sub[OF offs_le_ost])
using offs_le_ost
apply (subst add_diff_assoc2, fastforce simp: word_le_nat_alt)
apply fastforce
apply (rule conjI)
apply (simp add: pu8_def )
apply (rule arg_cong[where f=word_rcat])
apply (simp only: slice_def drop_take fun_app_def)
using ost_offs_x ost_4_nat
apply simp
apply (simp add: take_drop offs_cancel)
apply (subst add.commute, fastforce simp only: offs_cancel)
apply (simp add: ple16_eq )
apply (rule arg_cong[where f=WordArrayT.make])
apply (subgoal_tac "\<exists>v. ple16 (drop (unat offs) (take (unat offs + unat (Obj.len\<^sub>f obj)) ys)) (ost - offs + 6) = v")
apply (erule exE)
apply (simp only: ost_offs_x less_to_le[OF ost_no_of8, simplified unat_plus_simple])
apply (simp add: slice_def take_drop )
apply (simp add: offs_cancel offs_cancel')+
done
qed
lemma wa_length_ObjDentry_name_le:
"unat (wordarray_length (ObjDentry.name\<^sub>f (pObjDentry xs ost))) \<le> length xs"
by (simp add: pObjDentry_def Let_def ObjDentry.make_def wordarray_make wordarray_length_ret slice_def)
lemma wa_length_ObjDentry_name_le_len:
"unat (wordarray_length (ObjDentry.name\<^sub>f (pObjDentry xs ost))) \<le> unat (ple16 xs (ost + 6))"
by (simp add: pObjDentry_def Let_def ObjDentry.make_def wordarray_make wordarray_length_ret slice_def)
lemma dentarr_end_offs_list_induct_helper:
assumes diff: "Suc diff = unat to - frm"
and ih: "dentarr_offs_list_end_offs_pred (take (unat end_offs) (\<alpha>wa (data\<^sub>f buf))) (offs + 8 +
wordarray_length
(ObjDentry.name\<^sub>f (pObjDentry (take (unat end_offs) (\<alpha>wa (data\<^sub>f buf))) offs)))
[Suc frm..<unat to] end_offs"
and cur: " offs + 8 +
wordarray_length (ObjDentry.name\<^sub>f (pObjDentry (take (unat end_offs) (\<alpha>wa (data\<^sub>f buf))) offs))
\<le> end_offs"
shows
"dentarr_offs_list_end_offs_pred (take (unat end_offs) (\<alpha>wa (data\<^sub>f buf))) offs [frm..<unat to] end_offs"
proof -
have frm_lt_to: "frm < unat to" using diff by unat_arith
show ?thesis
apply (clarsimp simp: dentarr_end_offs_simps )
apply (subst (asm) upt_rec, simp add: frm_lt_to Let_def)
apply (subst (asm) snd_fold_append_simp)
apply clarsimp
apply (erule disjE)
using cur apply simp
using ih apply (simp add: dentarr_end_offs_simps Let_def)
done
qed
lemma offs_pl_8_name_of:
" wellformed_buf buf \<Longrightarrow>
length (\<alpha>wa $ data\<^sub>f buf) \<le> unat bilbyFsMaxEbSize \<Longrightarrow>
offs + 8 + wordarray_length (ObjDentry.name\<^sub>f (pObjDentry (take (unat end_offs) (\<alpha>wa (data\<^sub>f buf))) offs)) \<le> bound\<^sub>f buf \<Longrightarrow>
offs \<le> bilbyFsMaxEbSize \<Longrightarrow>
offs < offs + 8"
apply (simp add: bilbyFsMaxEbSize_def)
using wa_length_ObjDentry_name_le[where xs="(take (unat end_offs) (\<alpha>wa (data\<^sub>f buf)))" and ost=offs]
apply (clarsimp simp add: wellformed_buf_def)
apply (simp add: unat_arith_simps)
done
lemma mapAccumObsOpt_loop_deserialise_ObjDentry_ret:
assumes wellformed_buf: "wellformed_buf buf"
assumes no_buf_overflow: "length (\<alpha>wa $ data\<^sub>f buf) \<le> unat bilbyFsMaxEbSize"
assumes bound: "end_offs \<le> bound\<^sub>f buf"
assumes off_less_end_offs: "offs \<le> end_offs"
assumes frm: "frm \<le> unat (to::word32)" "unat to \<le> length ys"
assumes st_offs: "st_offs \<le> offs"
shows
"let list_spec =
case (fold (\<lambda>_ (xs, doffs, offslist).
let dentry = pObjDentry (take (unat end_offs) (\<alpha>wa (data\<^sub>f buf))) doffs ;
newoffs = doffs + 8 + wordarray_length (ObjDentry.name\<^sub>f dentry)
in (xs@[Option.Some dentry],
newoffs, offslist @ [newoffs]))
[frm..<unat to] ([], offs, []))
of (xs, offs) \<Rightarrow> ((take frm ys) @ xs @ (drop (unat to) ys), offs);
data = take (unat end_offs) (\<alpha>wa (data\<^sub>f buf)) in
(case mapAccumObsOpt frm (unat to) loop_deserialise_ObjDentry
ys (ex, offs) (buf, end_offs) of
Break (ys, d, ex) \<Rightarrow>
d \<in> {eInval, eNoMem}
| Iterate (ys, ex, offs') \<Rightarrow>
(ys, ex, offs') = (prod.fst list_spec, ex, prod.fst (prod.snd list_spec)) \<and>
offs' \<le> end_offs \<and>
dentarr_offs_list_end_offs_pred data offs [frm..<unat to] end_offs \<and>
dentarr_offs_list_drop_end_offs_pred data offs [frm..<unat to] st_offs end_offs)"
using assms
proof (induct "unat to - frm" arbitrary: frm ys ex offs)
case 0
thus ?case
by (simp add: dentarr_end_offs_simps mapAccumObsOpt_n_n dentarr_drop_end_offs_simps)
next
case (Suc diff)
note IH = this(1) and rest = this(2-)
have offs_le_max: "offs \<le> bilbyFsMaxEbSize"
using rest by (simp add: unat_arith_simps wellformed_buf_def)
hence offs_pl_8: "offs < offs + 8"
by (simp add: bilbyFsMaxEbSize_def unat_arith_simps)
have offs_pl_8_pl_name:
"offs + 8 \<le> offs + 8 + wordarray_length (ObjDentry.name\<^sub>f (pObjDentry (take (unat end_offs) (\<alpha>wa (data\<^sub>f buf))) offs))"
using wa_length_ObjDentry_name_le[where xs="take (unat end_offs) (\<alpha>wa (data\<^sub>f buf))" and ost=offs] rest offs_le_max
less_to_le[OF offs_pl_8]
by (simp add: wellformed_buf_def bilbyFsMaxEbSize_def unat_arith_simps)
have pObjDentry_eq:
"pObjDentry (drop (unat st_offs) (take (unat end_offs) (\<alpha>wa (data\<^sub>f buf)))) (offs - st_offs) = pObjDentry (take (unat end_offs) (\<alpha>wa (data\<^sub>f buf))) offs"
using rest offs_pl_8 by (fastforce intro: pObjDentry_drop_eq[symmetric,where end_offs=end_offs and offs=st_offs]
simp add: wellformed_buf_def word_le_nat_alt)
from rest show ?case
apply (subst mapAccumObsOpt_step, simp, simp)
apply (clarsimp simp: Let_def split: LoopResult.split)
apply (rule conjI)
using loop_deserialise_ObjDentry_ret[OF wellformed_buf no_buf_overflow bound ,
where dentry="ys ! frm" and ex = ex and offs=offs]
apply fastforce
apply clarsimp
apply (rename_tac elem ex' offs')
apply (cut_tac
frm="Suc frm" and
ys= "ys[frm := elem]" and
ex =ex' and offs = offs' in IH[OF _ wellformed_buf no_buf_overflow bound], simp_all)
apply(cut_tac loop_deserialise_ObjDentry_ret[OF wellformed_buf no_buf_overflow bound ,
where dentry="ys ! frm" and ex = ex and offs=offs and st_offs=st_offs], simp_all)
apply(cut_tac loop_deserialise_ObjDentry_ret[OF wellformed_buf no_buf_overflow bound ,
where dentry="ys ! frm" and ex = ex and offs=offs and st_offs=st_offs], simp_all)
apply clarsimp
using offs_pl_8_pl_name less_to_le[OF offs_pl_8]
apply (fastforce simp add: unat_plus_simple word_le_nat_alt)
apply (clarsimp simp: Let_def)
apply (rule conjI)
apply fastforce
apply (clarsimp simp: Let_def)
apply (rename_tac ex'')
apply (thin_tac "mapAccumObsOpt _ _ _ _ _ _ = _")
apply(cut_tac loop_deserialise_ObjDentry_ret[OF wellformed_buf no_buf_overflow bound,
where dentry="ys ! frm" and ex = ex and offs=offs], simp_all)
apply (clarsimp simp: Let_def fst_fold_triple_simp fst_snd_fold_triple_simp prod.case_eq_if)
apply (rule conjI)
apply (simp add: upt_conv_Cons[where i = frm])
apply (subst take_Suc_conv_app_nth, simp)
apply (simp add: take_list_update prod.case_eq_if snd_fold_simp)
apply (subst fst_fold_append_simp[where xs="[]", simplified, symmetric])
apply fastforce
apply (rule conjI)
apply (simp add: snd_fold_simp)
apply (case_tac "[frm..<unat to]")
apply (fastforce+)
apply (rename_tac l ls)
apply (subgoal_tac "[Suc frm..<unat to] = ls")
prefer 2
apply (subst (asm) upt_rec[where i=frm], case_tac "frm = unat to"; fastforce)
apply simp
apply (rule conjI)
apply (erule (2) dentarr_end_offs_list_induct_helper)
apply (simp add: dentarr_offs_list_drop_end_offs_pred_def)
apply clarsimp
apply (rename_tac offs')
apply (simp add: snd_fold_simp)
apply (case_tac "offs' = offs + 8 + wordarray_length (ObjDentry.name\<^sub>f (pObjDentry (take (unat end_offs) (\<alpha>wa (data\<^sub>f buf))) offs))")
apply simp
apply (simp add: dentarr_offs_list_drop_def)
apply (subst (asm) split_upt_on_l_n[where l=frm and n=frm, simplified], fastforce)
apply (simp add: Let_def)
apply (subst (asm) snd_fold_append_simp[where xs="[_]"])
apply (erule_tac x="offs' " in ballE, fastforce)
apply (fastforce simp add: pObjDentry_eq)
done
qed
lemma replicate_simp:
"replicate (unat to + 1 - unat to) (Option.None ()) = [Option.None ()]"
by (simp add: unat_arith_simps)
lemma mapAccumObsOpt_loop_deserialise_ObjDentry_array_ret:
assumes wellformed_buf: "wellformed_buf buf"
assumes no_buf_overflow: "length (\<alpha>wa $ data\<^sub>f buf) \<le> unat bilbyFsMaxEbSize"
assumes bound: "end_offs \<le> bound\<^sub>f buf"
assumes off_less_end_offs: "offs \<le> end_offs"
assumes st_offs: "st_offs \<le> offs"
shows
"let data = take (unat end_offs) (\<alpha>wa (data\<^sub>f buf));
arr_spec = pArrObjDentry data offs to in
(case mapAccumObsOpt 0 (unat to) loop_deserialise_ObjDentry
(replicate (unat to + 1) (Option.None ())) (ex, offs) (buf, end_offs) of
LoopResult.Break (ys, d, ex) \<Rightarrow>
d \<in> {eInval, eNoMem}
| LoopResult.Iterate (ys, ex, offs') \<Rightarrow>
(ys, ex, offs') = (\<alpha>a (prod.fst arr_spec), ex, prod.fst (prod.snd arr_spec)) \<and>
offs' \<le> end_offs \<and>
dentarr_offs_list_end_offs_pred data offs [0..<unat to] end_offs \<and>
dentarr_offs_list_drop_end_offs_pred data offs [0..<unat to] st_offs end_offs)"
unfolding pArrObjDentry_def Let_def
apply (clarsimp simp: array_make split: LoopResult.splits prod.splits)
using mapAccumObsOpt_loop_deserialise_ObjDentry_ret[OF assms(1-4), simplified Let_def,
where frm=0 and to=to and ex=ex and st_offs=st_offs and
ys="replicate (unat to + 1)(Option.None ())", simplified take_0 drop_replicate replicate_simp]
st_offs
apply (clarsimp split: LoopResult.splits)
done
lemma array_map_loop_deserialise_ObjDentry_ret:
assumes wellformed_buf: "wellformed_buf buf"
assumes no_buf_overflow: "length (\<alpha>wa $ data\<^sub>f buf) \<le> unat bilbyFsMaxEbSize"
assumes bound: "end_offs \<le> bound\<^sub>f buf"
assumes off_less_end_offs: "offs \<le> end_offs"
assumes st_offs: "st_offs \<le> offs"
shows "case array_map (ArrayMapP.make (ArrayT.make (replicate (unat to + 1) (Option.None ())))
0 to loop_deserialise_ObjDentry (ex, offs) (buf, end_offs)) of
LoopResult.Break (arr, err, ex) \<Rightarrow> err \<in> {eInval, eNoMem}
| LoopResult.Iterate (arr, ex', offs') \<Rightarrow>
let data = take (unat end_offs) (\<alpha>wa (data\<^sub>f buf));
(parr, poffs, poffslist) = pArrObjDentry data offs to;
ostlist = pArrObjDentry data offs to
in
arr = parr \<and> offs' = poffs \<and>
offs' \<le> end_offs \<and>
dentarr_offs_list_end_offs_pred data offs [0..<unat to] end_offs \<and>
dentarr_offs_list_drop_end_offs_pred data offs [0..<unat to] st_offs end_offs"
apply (clarsimp simp: ArrayMapP.make_def array_make array_map_ret)
using assms mapAccumObsOpt_loop_deserialise_ObjDentry_array_ret
[unfolded Let_def, where to=to and buf=buf and ex=ex and offs=offs and end_offs=end_offs and st_offs=st_offs]
by (clarsimp simp: array_make' Let_def split: LoopResult.splits)
lemma deserialise_Array_ObjDentry_ret:
assumes wellformed_buf: "wellformed_buf buf"
assumes no_buf_overflow: "length (\<alpha>wa $ data\<^sub>f buf) \<le> unat bilbyFsMaxEbSize"
assumes bound: "end_offs \<le> bound\<^sub>f buf"
assumes off_less_end_offs: "offs \<le> end_offs"
assumes st_offs: "st_offs \<le> offs"
assumes offs_pl_8_no_of: "offs \<le> offs + 8"
assumes offs_pl_8_le_end_offs: "offs + 8 \<le> end_offs"
assumes err: "\<And>ex e. e \<in> {eInval, eNoMem} \<Longrightarrow> P (Error (e, ex))"
assumes suc:
"\<And>ex arr offs' offslist data.
\<lbrakk> (arr, offs',offslist) = (pArrObjDentry (take (unat end_offs) (\<alpha>wa (data\<^sub>f buf))) offs nb_dentry);
offs' \<le> end_offs;
data = take (unat end_offs) (\<alpha>wa (data\<^sub>f buf));
dentarr_offs_list_end_offs_pred data offs [0..<unat nb_dentry] end_offs;
dentarr_offs_list_drop_end_offs_pred data offs [0..<unat nb_dentry] st_offs end_offs \<rbrakk> \<Longrightarrow>
P (Success (ex, arr, offs'))"
shows "P (deserialise_Array_ObjDentry (ex, buf, offs, nb_dentry, end_offs))"
unfolding deserialise_Array_ObjDentry_def[unfolded tuple_simps sanitizers]
apply (simp add: Let_def)
apply (rule array_create_ret)
apply (simp add: err[unfolded eNoMem_def])
apply (rename_tac ex' arr a)
apply (subgoal_tac "unat nb_dentry + 1 = unat (nb_dentry+1) ")
apply (clarsimp simp: prod.case_eq_if id_def Let_def split: LoopResult.splits)
apply (subgoal_tac "a = ArrayT.make (replicate (unat (nb_dentry + 1)) (Option.None ()))", simp)
apply (cut_tac ex=ex' in array_map_loop_deserialise_ObjDentry_ret[OF assms(1-5), where to = nb_dentry])
apply (clarsimp simp: Let_def err split: LoopResult.splits)
apply (rename_tac offslist a ex'' offs')
apply (rule suc)
apply simp+
apply (metis array_make')
apply unat_arith
done
lemma word_add_diff_assoc:
"(a::'a:: len0 word) + b - c = a + (b - c)"
by simp
method offs_olen_of_solver =
(((drule less_to_le)?, simp add: word_add_diff_assoc unat_plus_simple),
(simp only: unat_arith_simps)?, simp? ; unat_arith)
lemma deserialise_ObjDentarr_ret:
assumes wf: "wellformed_buf buf"
assumes buf_len: "length (\<alpha>wa $ data\<^sub>f buf) \<le> unat bilbyFsMaxEbSize"
assumes err: "\<And>ex e. e \<in> {eInval, eNoMem} \<Longrightarrow> P (Error (e, ex))"
assumes offs_bound: "offs + olen - bilbyFsObjHeaderSize \<le> (bound\<^sub>f buf)"
assumes offs_olen: "offs < offs + olen - bilbyFsObjHeaderSize"
assumes olen: "bilbyFsObjHeaderSize + bilbyFsObjDentarrHeaderSize + bilbyFsObjDentryHeaderSize \<le> olen"
assumes st_offs: "st_offs \<le> offs"
assumes suc:
"\<And>ex dentarr offs'. \<lbrakk>
dentarr = pObjDentarr (\<alpha>wa (data\<^sub>f buf)) offs olen;
offs' = pObjDentarrSize (\<alpha>wa (data\<^sub>f buf)) offs olen;
let end_offs = offs + olen - bilbyFsObjHeaderSize;
data = take (unat end_offs) (\<alpha>wa (data\<^sub>f buf));
nb_dentry = ple32 (\<alpha>wa (data\<^sub>f buf)) (offs+8) in
dentarr_offs_list_end_offs_pred data (offs+bilbyFsObjDentarrHeaderSize) [0..<unat nb_dentry] end_offs \<and>
dentarr_offs_list_drop_end_offs_pred data (offs+bilbyFsObjDentarrHeaderSize) [0..<unat nb_dentry] st_offs end_offs;
offs' \<le> offs + olen - bilbyFsObjHeaderSize
\<rbrakk> \<Longrightarrow>
P (Success (ex, dentarr, offs'))"
notes bilbyFsObjDentarrHeaderSize_def[simp] bilbyFsObjHeaderSize_def[simp]
bilbyFsObjDentryHeaderSize_def[simp]
shows "P (deserialise_ObjDentarr (ex, buf, offs, olen))"
proof -
have offs_no_of: "offs < offs + bilbyFsObjDentarrHeaderSize"
using olen and offs_olen by simp unat_arith
have bound_max: "bound\<^sub>f buf \<le> bilbyFsMaxEbSize"
using wf and buf_len by (simp add: wellformed_buf_def) unat_arith
have offs_bound': "offs < bilbyFsMaxEbSize"
using offs_bound offs_olen bound_max offs_no_of by simp
have offs_hdr_no_of: "offs < offs + bilbyFsObjDentarrHeaderSize"
using offs_bound' by (simp add: bilbyFsMaxEbSize_def unat_arith_simps)
have offs_pl_hdr_le_len: "unat offs + unat bilbyFsObjDentarrHeaderSize \<le> length (\<alpha>wa $ data\<^sub>f buf)"
using offs_bound wf offs_no_of offs_olen olen
by (simp add: wellformed_buf_def) unat_arith
have deserialises:
"deserialise_le32 (buf, offs + 8) = (ple32 (\<alpha>wa $ data\<^sub>f buf) (offs + 8))"
"deserialise_le64 (buf, offs) = (ple64 (\<alpha>wa $ data\<^sub>f buf) offs)"
using offs_pl_hdr_le_len apply (clarsimp simp:)
apply (rule deserialise_le32_ret[simplified])
using offs_hdr_no_of apply unat_arith
using offs_hdr_no_of apply (simp add: unat_arith_simps)
apply unat_arith
using offs_pl_hdr_le_len apply (clarsimp)
apply (rule deserialise_le64_ret[simplified])
using offs_hdr_no_of apply unat_arith
using offs_hdr_no_of apply (simp add: unat_arith_simps)
apply unat_arith
done
show ?thesis
unfolding deserialise_ObjDentarr_def[unfolded tuple_simps sanitizers]
apply (clarsimp simp: Let_def err[unfolded eInval_def])
apply (subgoal_tac "\<exists>v. olen - bilbyFsObjHeaderSize = v \<and> bilbyFsObjDentarrHeaderSize + bilbyFsObjDentryHeaderSize \<le> v")
apply (erule exE)
apply (erule conjE)
apply (rule deserialise_Array_ObjDentry_ret[OF assms(1,2), where st_offs=st_offs,
simplified])
using offs_bound apply simp
subgoal using offs_olen olen by - offs_olen_of_solver
subgoal for v
using st_offs offs_olen by - offs_olen_of_solver
subgoal for v
using offs_olen by - offs_olen_of_solver
subgoal for v
using offs_olen by (simp add: word_add_diff_assoc add.commute)
(rule word_plus_mono_right; simp)
subgoal for v _ e by (fastforce intro: err)
subgoal for v ex arr offs' offslist
apply (case_tac "R.Success (ex, arr, offs')", simp_all)
apply (clarsimp simp: Let_def err[unfolded eNoMem_def] split: R.split)
apply (rule suc)
subgoal
apply (simp add: pObjDentarr_def Let_def)
apply (subst ObjDentarr.surjective, simp add: ObjDentarr.make_def deserialises prod_eq_iff)
done
subgoal by (clarsimp simp add: prod_eq_iff pObjDentarrSize_def deserialises)
subgoal by (simp add: Let_def deserialises)
subgoal by simp
done
subgoal using olen by (simp) unat_arith
done
qed
lemmas pObjUnion_def' =
pObjUnion_def[unfolded otype_simps, simplified]
lemmas len_otype_ok = is_len_and_type_ok_def[unfolded sanitizers tuple_simps]
lemma olen_bound_trivial:
" 0x28 \<le> (olen::U32) \<Longrightarrow>
offs + olen - 0x18 \<le> bound\<^sub>f buf \<Longrightarrow>
offs \<le> offs + olen - 0x18 \<Longrightarrow> offs + 0x10 \<le> bound\<^sub>f buf"
by unat_arith
lemma offs_trivial:
"(offs::U32) \<le> offs + olen - 0x18 \<Longrightarrow>
0x28 \<le> olen \<Longrightarrow>
offs < offs + 0x10"
by unat_arith
lemma unat_obj_len_minus_hdrsz:
assumes len_otype_rel: "bilbyFsObjHeaderSize \<le> olen"
assumes offs_no_of: "offs \<le> offs + olen - bilbyFsObjHeaderSize"
shows
"unat (offs + olen - bilbyFsObjHeaderSize) = unat offs + unat olen - unat bilbyFsObjHeaderSize"
using assms
by (simp add: bilbyFsObjHeaderSize_def word_add_diff_assoc unat_plus_simple) (simp add: unat_arith_simps)
lemma deserialise_ObjUnion_ret:
assumes wf: "wellformed_buf buf"
assumes no_buf_overflow: "length (\<alpha>wa $ data\<^sub>f buf) \<le> unat bilbyFsMaxEbSize"
assumes bound: "offs + olen - bilbyFsObjHeaderSize \<le> bound\<^sub>f buf"
assumes len_otype_rel: "is_len_and_type_ok (otype, olen)"
assumes offs_no_of: "offs \<le> offs + olen - bilbyFsObjHeaderSize"
assumes offs_no_underflow: "offs - bilbyFsObjHeaderSize \<le> offs"
assumes err:
"\<And>ex e. e \<in> {eInval, eNoMem} \<Longrightarrow> P (Error (e, ex))"
assumes suc:
"\<And>ex ounion offs'. ounion = pObjUnion ((*take (unat (offs + olen))*) (\<alpha>wa (data\<^sub>f buf))) otype olen offs \<Longrightarrow>
offs' \<le> (offs + olen - bilbyFsObjHeaderSize) \<Longrightarrow>
let end_offs = offs + olen - bilbyFsObjHeaderSize;
data = take (unat end_offs) (\<alpha>wa (data\<^sub>f buf));
nb_dentry = ple32 (\<alpha>wa (data\<^sub>f buf)) (offs+8) in
dentarr_otype_end_offs_pred otype data offs end_offs \<and>
dentarr_otype_drop_end_offs_st_pred otype data offs (offs - bilbyFsObjHeaderSize) end_offs
\<Longrightarrow>
P (Success (ex, ounion, offs'))"
notes suc_simps = len_otype_ok Let_def pObjUnion_def' suc add.commute bilbyFsObjHeaderSize_def
otype_simps dentarr_end_offs_simps dentarr_drop_end_offs_simps
shows "P (deserialise_ObjUnion (ex, buf, offs, (otype, olen)))"
unfolding deserialise_ObjUnion_def[unfolded tuple_simps, simplified sanitizers]
using is_len_and_type_ok_hdr_szD[OF len_otype_rel]
apply (clarsimp simp: Let_def)
apply (rule conjI)
apply clarsimp
apply (rule deserialise_ObjSuper_ret, simp)
using len_otype_rel offs_no_of bound wf
apply (simp add: len_otype_ok Let_def prod.case_eq_if wellformed_buf_def bilbyFsObjHeaderSize_def)
apply unat_arith
using len_otype_rel offs_no_of bound wf
apply (simp add: len_otype_ok Let_def prod.case_eq_if wellformed_buf_def bilbyFsObjHeaderSize_def)
apply unat_arith
apply (simp add: err)
using len_otype_rel
apply (simp add: suc_simps)
apply clarsimp
apply (rule conjI)
apply clarsimp
apply (rule deserialise_ObjDel_ret, simp)
using len_otype_rel offs_no_of bound wf
apply (simp add: len_otype_ok Let_def prod.case_eq_if wellformed_buf_def bilbyFsObjHeaderSize_def)
apply unat_arith
apply (simp add: err)
using len_otype_rel offs_no_of bound wf
apply (simp add: len_otype_ok Let_def prod.case_eq_if wellformed_buf_def bilbyFsObjHeaderSize_def)
apply unat_arith
using len_otype_rel
apply (simp add: suc_simps)
apply clarsimp
apply (rule conjI)
apply clarsimp
apply (rule deserialise_ObjDentarr_ret[OF wf no_buf_overflow, where st_offs ="offs - bilbyFsObjHeaderSize"])
apply (simp add: err)
using bound offs_no_of len_otype_rel
apply (simp add: len_otype_ok Let_def prod.case_eq_if wellformed_buf_def bilbyFsObjHeaderSize_def)
using offs_no_of len_otype_rel
apply (simp add: len_otype_ok bilbyFsObjHeaderSize_def )
apply (simp add: word_add_diff_assoc unat_plus_simple word_less_nat_alt )
apply unat_arith
using len_otype_rel
apply (simp add: len_otype_ok bilbyFsObjHeaderSize_def bilbyFsObjDentryHeaderSize_def bilbyFsObjDentarrHeaderSize_def)
using offs_no_underflow apply simp
apply (simp add: suc pObjUnion_def' )
apply (rule suc)
apply (clarsimp simp add: pObjUnion_def')+
apply (simp add: dentarr_otype_drop_end_offs_st_pred_def dentarr_otype_end_offs_pred_def dentarr_otype_drop_end_offs_pred_def
bilbyFsObjTypeDentarr_def Let_def)
apply clarsimp
apply (subgoal_tac "ple32 (take (unat (offs + olen - bilbyFsObjHeaderSize)) (\<alpha>wa (data\<^sub>f buf))) (offs + 8) = ple32 (\<alpha>wa (data\<^sub>f buf)) (offs + 8)")
apply simp
apply (subgoal_tac "\<exists>v. olen - bilbyFsObjHeaderSize = v")
apply (erule exE)
apply (subst ple32_take)
(* <automate?> *)
using len_otype_rel
apply (simp add: len_otype_ok bilbyFsObjHeaderSize_def)
using offs_no_of apply (simp add: word_add_diff_assoc bilbyFsObjHeaderSize_def)
apply (simp add: word_add_diff_assoc unat_plus_simple word_less_nat_alt word_le_nat_alt add.commute)
apply (subst (asm) add.commute)
using offs_no_of apply (simp add: bilbyFsObjHeaderSize_def) apply (simp add: word_add_diff_assoc word_le_nat_alt)
apply (simp only: unat_arith_simps)
apply unat_arith
apply (simp add: bilbyFsObjHeaderSize_def word_add_diff_assoc)
using offs_no_of
apply (simp add: bilbyFsObjHeaderSize_def word_add_diff_assoc word_less_nat_alt add.commute)
apply (subst (asm) add.commute, simp add: unat_plus_simple)
using offs_no_of apply (simp add: bilbyFsObjHeaderSize_def)
apply (simp add: word_add_diff_assoc)
using len_otype_rel
apply (simp add: len_otype_ok)
apply (subgoal_tac "offs \<le> offs + 0xC")
apply (simp add: unat_plus_simple add.commute, simp only: word_le_nat_alt)
apply unat_arith
apply (simp add: unat_plus_simple add.commute, simp only: word_le_nat_alt)
apply unat_arith
(* </automate?> *)
apply simp
apply (fastforce)
apply clarsimp
apply (rule conjI)
apply clarsimp
apply (rule deserialise_ObjData_ret[OF ])
using offs_no_of
apply (simp only: diff_conv_add_uminus)
apply (simp only: add.assoc)
using bound wf offs_no_of apply (simp add: bilbyFsObjHeaderSize_def
wellformed_buf_def diff_conv_add_uminus add.assoc)
apply unat_arith
using len_otype_rel apply (simp add: otype_simps)
apply (simp add: err)
apply simp
apply (simp add: suc_simps)
apply (clarsimp)
apply (rule conjI)
apply clarsimp
apply (rule deserialise_ObjInode_ret)
using len_otype_rel offs_no_of bound
bound wf offs_no_of
apply (simp add: bilbyFsObjHeaderSize_def wellformed_buf_def )
using len_otype_rel apply (simp add: otype_simps len_otype_ok)
apply unat_arith
using len_otype_rel apply (simp add: otype_simps len_otype_ok)
using offs_no_of
apply (simp add: bilbyFsObjHeaderSize_def)
apply unat_arith
apply (simp add: err)
using len_otype_rel apply (simp add: otype_simps len_otype_ok)
apply (simp add: suc_simps)
apply clarsimp
apply (rule deserialise_ObjPad_ret)
apply (simp add:err)
apply (simp add: suc_simps add_diff_eq)+
done
lemma pObjDel_take:
"is_valid_ObjHeader (pObjHeader (\<alpha>wa (data\<^sub>f buf)) offs) (bounded buf) \<Longrightarrow>
offs + Obj.len\<^sub>f obj \<le> bound\<^sub>f buf \<Longrightarrow>
is_len_and_type_ok (otype\<^sub>f obj, Obj.len\<^sub>f obj) \<Longrightarrow>
offs < offs + Obj.len\<^sub>f obj \<Longrightarrow>
otype\<^sub>f obj = 3 \<Longrightarrow>
\<exists>v. obj\<lparr>ounion\<^sub>f := v\<rparr> = pObjHeader (\<alpha>wa (data\<^sub>f buf)) offs \<Longrightarrow>
pObjDel (\<alpha>wa (data\<^sub>f buf)) (offs + bilbyFsObjHeaderSize) =
pObjDel (take (unat (offs + Obj.len\<^sub>f obj)) (\<alpha>wa (data\<^sub>f buf))) (offs + bilbyFsObjHeaderSize)"
apply (simp add: pObjDel_def)
apply (frule is_valid_ObjHeader_buf_len, clarify)
apply (subst ple64_take, (simp add: otype_simps len_otype_ok bilbyFsObjHeaderSize_def, unat_arith)+)
apply simp
done
lemma pObjSuper_take:
"is_valid_ObjHeader (pObjHeader (\<alpha>wa (data\<^sub>f buf)) offs) (bounded buf) \<Longrightarrow>
offs + Obj.len\<^sub>f obj \<le> bound\<^sub>f buf \<Longrightarrow>
is_len_and_type_ok (otype\<^sub>f obj, Obj.len\<^sub>f obj) \<Longrightarrow>
offs < offs + Obj.len\<^sub>f obj \<Longrightarrow>
otype\<^sub>f obj = 4 \<Longrightarrow>
\<exists>v. obj\<lparr>ounion\<^sub>f := v\<rparr> = pObjHeader (\<alpha>wa (data\<^sub>f buf)) offs \<Longrightarrow>
pObjSuper (\<alpha>wa (data\<^sub>f buf)) (offs + bilbyFsObjHeaderSize) =
pObjSuper (take (unat (offs + Obj.len\<^sub>f obj)) (\<alpha>wa (data\<^sub>f buf))) (offs + bilbyFsObjHeaderSize)"
apply (simp add: pObjSuper_def)
apply (frule is_valid_ObjHeader_buf_len, clarify)
apply (subst ple64_take, ((simp add: otype_simps len_otype_ok bilbyFsObjHeaderSize_def, unat_arith)+)[2])
apply (subst ple32_take, ((simp add: otype_simps len_otype_ok bilbyFsObjHeaderSize_def, unat_arith)+)[2])+
apply simp
done
lemma pObjInode_take:
"is_valid_ObjHeader (pObjHeader (\<alpha>wa (data\<^sub>f buf)) offs) (bounded buf) \<Longrightarrow>
offs + Obj.len\<^sub>f obj \<le> bound\<^sub>f buf \<Longrightarrow>
is_len_and_type_ok (otype\<^sub>f obj, Obj.len\<^sub>f obj) \<Longrightarrow>
offs < offs + Obj.len\<^sub>f obj \<Longrightarrow>
otype\<^sub>f obj = 0 \<Longrightarrow>
\<exists>v. obj\<lparr>ounion\<^sub>f := v\<rparr> = pObjHeader (\<alpha>wa (data\<^sub>f buf)) offs \<Longrightarrow>
pObjInode (\<alpha>wa (data\<^sub>f buf)) (offs + bilbyFsObjHeaderSize) =
pObjInode (take (unat (offs + Obj.len\<^sub>f obj)) (\<alpha>wa (data\<^sub>f buf))) (offs + bilbyFsObjHeaderSize)"
apply (simp add: pObjInode_def)
apply (frule is_valid_ObjHeader_buf_len, clarify)
apply (subst ple64_take, ((simp add: otype_simps len_otype_ok bilbyFsObjHeaderSize_def, unat_arith)+)[2])+
apply (subst ple32_take, ((simp add: otype_simps len_otype_ok bilbyFsObjHeaderSize_def, unat_arith)+)[2])+
apply simp
done
lemma pObjDentarr_take:
"is_valid_ObjHeader (pObjHeader (\<alpha>wa (data\<^sub>f buf)) offs) (bounded buf) \<Longrightarrow>
offs + Obj.len\<^sub>f obj \<le> bound\<^sub>f buf \<Longrightarrow>
is_len_and_type_ok (otype\<^sub>f obj, Obj.len\<^sub>f obj) \<Longrightarrow>
offs < offs + Obj.len\<^sub>f obj \<Longrightarrow>
otype\<^sub>f obj = 2 \<Longrightarrow>
\<exists>v. obj\<lparr>ounion\<^sub>f := v\<rparr> = pObjHeader (\<alpha>wa (data\<^sub>f buf)) offs \<Longrightarrow>
pObjDentarr (\<alpha>wa (data\<^sub>f buf)) (offs + bilbyFsObjHeaderSize) (Obj.len\<^sub>f obj) =
pObjDentarr (take (unat (offs + Obj.len\<^sub>f obj)) (\<alpha>wa (data\<^sub>f buf))) (offs + bilbyFsObjHeaderSize) (Obj.len\<^sub>f obj)"
apply (simp add: pObjDentarr_def)
apply (frule is_valid_ObjHeader_buf_len, clarify)
apply (subst ple64_take, ((simp add: otype_simps len_otype_ok bilbyFsObjHeaderSize_def, unat_arith)+)[2])+
apply (subst ple32_take, ((simp add: otype_simps len_otype_ok bilbyFsObjHeaderSize_def, unat_arith)+)[2])+
apply (simp add: Let_def)
done
lemma pObjData_take:
"is_valid_ObjHeader (pObjHeader (\<alpha>wa (data\<^sub>f buf)) offs) (bounded buf) \<Longrightarrow>
offs + Obj.len\<^sub>f obj \<le> bound\<^sub>f buf \<Longrightarrow>
is_len_and_type_ok (otype\<^sub>f obj, Obj.len\<^sub>f obj) \<Longrightarrow>
offs < offs + Obj.len\<^sub>f obj \<Longrightarrow>
otype\<^sub>f obj = 1 \<Longrightarrow>
\<exists>v. obj\<lparr>ounion\<^sub>f := v\<rparr> = pObjHeader (\<alpha>wa (data\<^sub>f buf)) offs \<Longrightarrow>
pObjData (\<alpha>wa (data\<^sub>f buf)) (offs + bilbyFsObjHeaderSize) (Obj.len\<^sub>f obj) =
pObjData (take (unat (offs + Obj.len\<^sub>f obj)) (\<alpha>wa (data\<^sub>f buf))) (offs + bilbyFsObjHeaderSize)
(Obj.len\<^sub>f obj)"
apply (simp add: pObjData_def)
apply (subst ple64_take, ((simp add: otype_simps len_otype_ok bilbyFsObjHeaderSize_def, unat_arith)+)[2])+
apply (simp add: otype_simps len_otype_ok)
apply (subst slice_take)
apply (frule is_valid_ObjHeader_len)
apply (subgoal_tac " unat (Obj.len\<^sub>f obj - bilbyFsObjHeaderSize - bilbyFsObjDataHeaderSize) = unat (Obj.len\<^sub>f obj) - unat bilbyFsObjHeaderSize - unat bilbyFsObjDataHeaderSize")
apply (subgoal_tac "unat (offs + Obj.len\<^sub>f obj) = unat offs + unat ( Obj.len\<^sub>f obj)")
apply simp
apply (simp add: bilbyFsObjHeaderSize_def bilbyFsObjDataHeaderSize_def)
apply unat_arith
apply (simp add: word_less_nat_alt unat_plus_simple[symmetric], unat_arith)
apply (subst unat_sub, simp add: bilbyFsObjHeaderSize_def bilbyFsObjDataHeaderSize_def, unat_arith)+
apply simp+
done
lemma pObjUnion_take:
"is_valid_ObjHeader (pObjHeader (\<alpha>wa (data\<^sub>f buf)) offs) (bounded buf) \<Longrightarrow>
offs + Obj.len\<^sub>f obj \<le> bound\<^sub>f buf \<Longrightarrow>
is_len_and_type_ok (otype\<^sub>f obj, Obj.len\<^sub>f obj) \<Longrightarrow>
offs < offs + Obj.len\<^sub>f obj \<Longrightarrow>
\<exists>v. obj\<lparr>ounion\<^sub>f := v\<rparr> = pObjHeader (\<alpha>wa (data\<^sub>f buf)) offs \<Longrightarrow>
pObjUnion (\<alpha>wa (data\<^sub>f buf)) (otype\<^sub>f obj) (Obj.len\<^sub>f obj) (offs + bilbyFsObjHeaderSize) =
pObjUnion (take (unat (offs + Obj.len\<^sub>f obj)) (\<alpha>wa (data\<^sub>f buf))) (otype\<^sub>f obj) (Obj.len\<^sub>f obj) (offs + bilbyFsObjHeaderSize)"
apply (simp add: pObjUnion_def')
apply (case_tac "otype\<^sub>f obj = 0")
apply (simp add: pObjInode_take)
apply (case_tac "otype\<^sub>f obj = 1")
apply (simp add: pObjData_take)
apply (case_tac "otype\<^sub>f obj = 2")
apply (simp add: pObjDentarr_take)
apply (case_tac "otype\<^sub>f obj = 3")
apply (simp add: pObjDel_take)
apply (case_tac "otype\<^sub>f obj = 4")
apply (simp add: pObjSuper_take)
apply simp
done
lemmas Obj_ext_eq_expand = trans[OF _ Obj.ext_inject,
OF arg_cong2[where f="(=)"], OF refl Obj.surjective]
lemma deserialise_Obj_ret:
assumes wf: "wellformed_buf buf"
assumes buf_len: "length (\<alpha>wa $ data\<^sub>f buf) \<le> unat bilbyFsMaxEbSize"
assumes bound: "offs + bilbyFsObjHeaderSize \<le> bound\<^sub>f buf"
assumes no_of: "offs < offs + bilbyFsObjHeaderSize"
assumes err: "\<And>ex e. e \<in> {eInval, eNoMem} \<Longrightarrow> P (Error (e, ex))"
assumes suc:
"\<And>ex obj offs'. \<lbrakk>
is_valid_ObjHeader (pObjHeader (\<alpha>wa (data\<^sub>f buf)) offs) (\<alpha>wa (data\<^sub>f buf)) ;
let end_offs = offs + (Obj.len\<^sub>f obj);
data = take (unat end_offs) (\<alpha>wa (data\<^sub>f buf));
nb_dentry = ple32 (\<alpha>wa (data\<^sub>f buf)) (offs+8) in
dentarr_otype_end_offs_pred (Obj.otype\<^sub>f obj) data (offs + bilbyFsObjHeaderSize) end_offs \<and>
dentarr_otype_drop_end_offs_st_pred (Obj.otype\<^sub>f obj) data (offs + bilbyFsObjHeaderSize) offs end_offs;
obj = pObj (\<alpha>wa (data\<^sub>f buf)) offs;
offs' \<le> offs + Obj.len\<^sub>f obj \<rbrakk> \<Longrightarrow>
P (Success (ex, obj, offs'))"
notes bilbyFsObjHeaderSize_def[simp]
shows "P (deserialise_Obj (ex, buf, offs))"
unfolding deserialise_Obj_def[unfolded tuple_simps sanitizers]
apply (clarsimp simp: err eNoMem_def split: R.split)
apply (rule deserialise_ObjHeader_ret[OF wf bound no_of])
apply (simp add: err)
apply simp
apply (rule deserialise_ObjUnion_ret[OF wf buf_len])
apply (simp)
apply (clarsimp, drule sym[where t="pObjHeader (\<alpha>wa (data\<^sub>f buf)) offs"])
apply (clarsimp simp add: is_valid_ObjHeader_def)
apply simp
apply (drule is_valid_ObjHeader_len)
apply (clarsimp, drule sym[where t="pObjHeader (\<alpha>wa (data\<^sub>f buf)) offs"])
apply (drule arg_cong[where f=Obj.len\<^sub>f])
using no_of bound
apply simp
apply (simp only: word_le_nat_alt plus_no_overflow_unat_lift)
apply (drule is_valid_ObjHeader_len)
apply (clarsimp, drule sym[where t="pObjHeader (\<alpha>wa (data\<^sub>f buf)) offs"])
apply (drule arg_cong[where f=Obj.len\<^sub>f])
apply (clarsimp simp add: )
apply unat_arith
apply (simp add: err)
apply simp
apply (rule suc)
apply (clarsimp simp add: is_valid_ObjHeader_def bounded_def)
apply simp
apply (clarsimp simp add: pObj_def Let_def)
apply (drule sym[where t="pObjHeader (\<alpha>wa (data\<^sub>f buf)) offs"])
apply (subst pObjUnion_take[simplified], (fastforce simp add: is_valid_ObjHeader_def)+)
apply (rename_tac obj offs' v)
apply (subgoal_tac "pObjUnion (take (unat (offs + Obj.len\<^sub>f obj)) (\<alpha>wa (data\<^sub>f buf))) (otype\<^sub>f obj)
(Obj.len\<^sub>f obj) (offs + 0x18) = pObjUnion
(take (unat offs + unat (Obj.len\<^sub>f (pObjHeader (\<alpha>wa (data\<^sub>f buf)) offs))) (\<alpha>wa (data\<^sub>f buf)))
(otype\<^sub>f (pObjHeader (\<alpha>wa (data\<^sub>f buf)) offs))
(Obj.len\<^sub>f (pObjHeader (\<alpha>wa (data\<^sub>f buf)) offs)) (offs + 0x18)")
apply simp
apply (case_tac "pObjHeader (\<alpha>wa (data\<^sub>f buf)) offs", case_tac obj, simp)
apply (case_tac "pObjHeader (\<alpha>wa (data\<^sub>f buf)) offs", case_tac obj, simp)
apply (simp add: plus_no_overflow_unat_lift)+
done
lemma pObjHeader_take:
"is_valid_ObjHeader (pObjHeader xs (ObjAddr.offs\<^sub>f oaddr)) xs \<Longrightarrow>
is_obj_addr_consistent (pObj (take (unat (ObjAddr.offs\<^sub>f oaddr) + unat (ObjAddr.len\<^sub>f oaddr)) xs)
(ObjAddr.offs\<^sub>f oaddr)) oaddr \<Longrightarrow>
ObjAddr.offs\<^sub>f oaddr < ObjAddr.offs\<^sub>f oaddr + bilbyFsObjHeaderSize \<Longrightarrow>
bilbyFsObjHeaderSize \<le> ObjAddr.len\<^sub>f oaddr \<Longrightarrow>
pObjHeader xs (ObjAddr.offs\<^sub>f oaddr) = pObjHeader (take (unat (ObjAddr.offs\<^sub>f oaddr) + unat (ObjAddr.len\<^sub>f oaddr)) xs) (ObjAddr.offs\<^sub>f oaddr)"
apply (simp add: pObjHeader_def)
apply (subst ple32_take, ((simp add: bilbyFsObjHeaderSize_def, unat_arith, fastforce? )[2])+)+
apply (subst ple64_take, ((simp add: bilbyFsObjHeaderSize_def, unat_arith, fastforce? )[2])+)+
apply (subst nth_take, (simp add: bilbyFsObjHeaderSize_def, unat_arith))+
apply (rule refl)
done
end