From c9c842bad22e9e7ef4173f92756c2f0eaa8e7320 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Sat, 16 Mar 2024 11:30:08 +0100 Subject: [PATCH] word_lib+crefine: move lemmas to Word_Lib - move AARCH64 word lemmas to the holding area in Word_Lib - generalise word_ctz_upcast_id and provide word_ctz_upcast_id_32_64 Signed-off-by: Gerwin Klein --- lib/Word_Lib/Word_Lemmas_64_Internal.thy | 9 +++ lib/Word_Lib/Word_Lemmas_Internal.thy | 93 ++++++++++++++++++++++++ proof/crefine/AARCH64/ADT_C.thy | 4 +- proof/crefine/AARCH64/Arch_C.thy | 38 ---------- proof/crefine/AARCH64/CSpace_C.thy | 5 -- proof/crefine/AARCH64/Finalise_C.thy | 9 --- proof/crefine/AARCH64/Recycle_C.thy | 5 -- proof/crefine/AARCH64/Syscall_C.thy | 20 +---- proof/crefine/AARCH64/VSpace_C.thy | 17 ----- proof/crefine/ARM_HYP/ADT_C.thy | 4 +- proof/crefine/ARM_HYP/Ipc_C.thy | 1 - proof/crefine/Move_C.thy | 13 ---- proof/crefine/RISCV64/Ipc_C.thy | 1 - proof/crefine/X64/Ipc_C.thy | 1 - 14 files changed, 105 insertions(+), 115 deletions(-) diff --git a/lib/Word_Lib/Word_Lemmas_64_Internal.thy b/lib/Word_Lib/Word_Lemmas_64_Internal.thy index 71af9f3fd9..374e624684 100644 --- a/lib/Word_Lib/Word_Lemmas_64_Internal.thy +++ b/lib/Word_Lib/Word_Lemmas_64_Internal.thy @@ -57,4 +57,13 @@ lemmas mask_64_id[simp] = mask_len_id[where 'a=64, folded word_bits_def] lemma neq_0_unat: "x \ 0 \ 0 < unat x" for x::machine_word by (simp add: unat_gt_0) +(* The 32-bit version is occasionally needed on 64-bit platforms *) +lemma word_rsplit_0_32: + "word_rsplit (0::32 word) = [0, 0, 0, (0::8 word)]" + by (simp add: word_rsplit_def bin_rsplit_def word_bits_def word_size_def Cons_replicate_eq) + +lemma word_ctz_upcast_id_32_64: + "x \ 0 \ word_ctz (UCAST(32 \ 64) x) = word_ctz x" + by (simp add: word_ctz_upcast_id is_up) + end \ No newline at end of file diff --git a/lib/Word_Lib/Word_Lemmas_Internal.thy b/lib/Word_Lib/Word_Lemmas_Internal.thy index 643786b46f..73159d12cf 100644 --- a/lib/Word_Lib/Word_Lemmas_Internal.thy +++ b/lib/Word_Lib/Word_Lemmas_Internal.thy @@ -745,4 +745,97 @@ lemma shiftr_anti_mono: apply (simp add: drop_bit_eq_div zdiv_mono2) done +lemma mask_shift_neg_mask_eq: + "\ n' \ n; x \ mask (m+n') \ \ (x && ~~ mask n) && (mask m << n') = x && ~~ mask n" + by word_eqI_solve + +lemma from_bool_inj[simp]: + "(from_bool x = from_bool y) = (x = y)" + unfolding from_bool_def + by (auto split: bool.splits) + +lemma word_le_1_and_idem: + "w \ 1 \ w AND 1 = w" for w :: "_ word" + by (metis word_bw_same(1) word_le_1 word_log_esimps(7)) + +lemma from_to_bool_le_1_idem: + "w \ 1 \ from_bool (to_bool w) = w" + apply (subst word_le_1_and_idem[symmetric], assumption) + apply (simp add: from_to_bool_last_bit) + apply (simp add: word_le_1_and_idem) + done + +lemma and_1_0_not_bit_0: + "(w && 1 = 0) = (\ (w::'a::len word) !! 0)" + using to_bool_and_1[simplified to_bool_def, where x=w] + by auto + +lemma unat_scast_up: + "\ LENGTH('a) \ LENGTH('b); 0 \ sint x \ \unat (scast x::'b::len word) = unat x" + for x :: "'a :: len word" + apply (simp flip: bit_last_iff not_less) + apply word_eqI + apply (clarsimp simp: min_def split: if_splits) + apply (rule conjI; clarsimp) + apply (drule test_bit_lenD) + apply clarsimp + apply (metis le_antisym nat_le_Suc_less_imp) + apply fastforce + done + +lemma unat_uint_less: + "unat x < nat i \ uint x < i" for x :: "'a :: len word" + by (simp add: zless_nat_eq_int_zless) + +lemma sint_ge_zero_uint: + "uint x < 2 ^ (LENGTH('a) - 1) \ sint (x :: 'a :: len word) \ 0" + by (simp add: sint_eq_uint_2pl word_2p_lem wsst_TYs(3)) + +lemma sint_ge_zero_unat: + "unat x < 2 ^ (LENGTH('a) - 1) \ sint (x :: 'a :: len word) \ 0" + by (fastforce intro: sint_ge_zero_uint unat_uint_less simp: nat_power_eq) + +lemma mask_shiftl_le_mask: + "mask n << m \ (mask (n+m) :: 'a::len word)" + by (subst add.commute) + (rule leq_high_bits_shiftr_low_bits_leq_bits, simp) + +(* This is more useful for getting rid of a downcast *) +lemma unat_ucast_unat_id: + "unat x < 2 ^ LENGTH('b) \ unat (UCAST('a::len \ 'b::len) x) = unat x" + by (simp add: unat_eq_of_nat) + +lemma ucast_up_preserves_gt0: + "\ 0 < x; LENGTH('a) < LENGTH('b) \ \ 0 < (ucast x :: 'b::len word)" for x :: "'a::len word" + by (metis ucast_0 ucast_less_ucast_weak) + +lemma ucast_up_preserves_not0: + "\ x \ 0; LENGTH('a) < LENGTH('b::len) \ \ (ucast x :: 'b::len word) \ 0" + for x :: "'a::len word" + by (metis ucast_0 ucast_ucast_id) + +lemma unat_le_fold: + "n < 2 ^ LENGTH('a) \ (unat x \ n) = (x \ of_nat n)" for x::"'a::len word" + by (simp add: word_le_nat_alt unat_of_nat_eq) + +lemma ucast_and_mask_drop: + "LENGTH('a) \ n \ (ucast w :: 'b::len word) && mask n = ucast w" for w::"'a::len word" + by word_eqI (fastforce dest: test_bit_lenD) + +lemma add_mask_ignore: + "x && mask n = 0 \ v + x && mask n = v && mask n" + by (metis add_0_right mask_eqs(2)) + +lemma word_ctz_upcast_id: + "\ x \ 0; is_up (ucast::'a word \'b word) \ \ + word_ctz (ucast x :: 'b::len word) = word_ctz x" for x :: "'a::len word" + unfolding word_ctz_def + by (simp add: ucast_up_app[where n="LENGTH('b) - LENGTH('a)"] + source_size_def target_size_def is_up_def eq_zero_set_bl) + +lemma ucast_ucast_mask_id: + "\ LENGTH('b::len) < LENGTH('a); n = LENGTH('b) \ \ + UCAST('b \ 'a) (UCAST('a \ 'b) (x && mask n)) = x && mask n" for x :: "'a::len word" + by (simp add: ucast_ucast_len[OF eq_mask_less]) + end diff --git a/proof/crefine/AARCH64/ADT_C.thy b/proof/crefine/AARCH64/ADT_C.thy index 5d893a009a..8b15aefd26 100644 --- a/proof/crefine/AARCH64/ADT_C.thy +++ b/proof/crefine/AARCH64/ADT_C.thy @@ -953,9 +953,7 @@ lemma cpspace_vcpu_relation_unique: apply (case_tac "64 \ r"; simp) apply (rule conjI) apply (rule ext, blast) - apply (rule conjI) - apply (rule ext, rename_tac vppi) - apply (rule from_bool_eqI, blast) + apply (rule conjI, blast) apply (case_tac vtimer, case_tac vtimer') apply clarsimp done diff --git a/proof/crefine/AARCH64/Arch_C.thy b/proof/crefine/AARCH64/Arch_C.thy index bd27a30ae5..ae1656fe87 100644 --- a/proof/crefine/AARCH64/Arch_C.thy +++ b/proof/crefine/AARCH64/Arch_C.thy @@ -921,10 +921,6 @@ lemma capVSMappedASID_CL_masked[unfolded asid_bits_def, simplified]: apply (clarsimp simp: cap_lift_def Let_def asid_bits_def split: if_splits) done -lemma mask_shift_neg_mask_eq: (* FIXME AARCH64: move to Word_Lib *) - "\ n' \ n; x \ mask (m+n') \ \ (x && ~~ mask n) && (mask m << n') = x && ~~ mask n" - by word_eqI_solve - lemma pptrUserTop_le_canonical_val[unfolded canonical_bit_def, simplified]: "x \ pptrUserTop \ x \ mask (Suc canonical_bit)" by (simp add: pptrUserTop_def canonical_bit_def order_trans[OF _ mask_mono] split: if_split_asm) @@ -1336,11 +1332,6 @@ lemma cpte_relation_pte_invalid_eq: "cpte_relation pte pte' \ (pte_lift pte' = Some Pte_pte_invalid) = (pte = InvalidPTE)" by (clarsimp simp: cpte_relation_def Let_def split: if_splits pte.splits) -lemma from_bool_inj[simp]: (* FIXME AARCH64: move to Word_Lib *) - "(from_bool x = from_bool y) = (x = y)" - unfolding from_bool_def - by (auto split: bool.splits) - lemma performPageInvocationMap_ccorres: "ccorres (K (K \) \ dc) (liftxf errstate id (K ()) ret__unsigned_long_') (invs' and cte_at' slot and (\s. 7 \ gsMaxObjectSize s) @@ -1626,11 +1617,6 @@ lemma ccap_relation_FrameCap_IsMapped: apply (clarsimp simp: cap_to_H_def Let_def split: cap_CL.splits if_splits) done -lemma and_1_0_not_bit_0: (* FIXME AARCH64: move to Word_Lib *) - "(w && 1 = 0) = (\ (w::'a::len word) !! 0)" - using to_bool_and_1[simplified to_bool_def, where x=w] - by auto - lemma cte_wp_at'_frame_at': "\ cte_wp_at' ((=) (capability.ArchObjectCap (arch_capability.FrameCap p v1 sz d m)) \ cteCap) slot s; @@ -1764,30 +1750,6 @@ lemma isPageFlushLabel_disj: isPageFlushLabel label" by (auto simp: isPageFlushLabel_def split: invocation_label.split arch_invocation_label.split) -lemma unat_scast_up: (* FIXME AARCH64: currently unused, move to Word_Lib *) - "\ LENGTH('a) \ LENGTH('b); 0 \ sint x \ \ unat (scast x::'b::len word) = unat x" for x :: "'a :: len word" - apply (simp flip: bit_last_iff not_less) - apply (word_eqI) - apply (clarsimp simp: min_def split: if_splits) - apply (rule conjI; clarsimp) - apply (drule test_bit_lenD) - apply clarsimp - apply (metis le_antisym nat_le_Suc_less_imp) - apply fastforce - done - -lemma unat_uint_less: (* FIXME AARCH64: currently unused, move to Word_Lib *) - "unat x < nat i \ uint x < i" for x :: "'a :: len word" - by (simp add: zless_nat_eq_int_zless) - -lemma sint_ge_zero_uint: (* FIXME AARCH64: currently unused, move to Word_Lib *) - "uint x < 2 ^ (LENGTH('a) - 1) \ sint (x :: 'a :: len word) \ 0" - by (simp add: sint_eq_uint_2pl word_2p_lem wsst_TYs(3)) - -lemma sint_ge_zero_unat: (* FIXME AARCH64: currently unused, move to Word_Lib *) - "unat x < 2 ^ (LENGTH('a) - 1) \ sint (x :: 'a :: len word) \ 0" - by (fastforce intro: sint_ge_zero_uint unat_uint_less simp: nat_power_eq) - lemma flushtype_relation_triv: "isPageFlushLabel (invocation_type label) \ isVSpaceFlushLabel (invocation_type label) \ flushtype_relation (labelToFlushType label) label" diff --git a/proof/crefine/AARCH64/CSpace_C.thy b/proof/crefine/AARCH64/CSpace_C.thy index 494fe0de8a..fc13c5994e 100644 --- a/proof/crefine/AARCH64/CSpace_C.thy +++ b/proof/crefine/AARCH64/CSpace_C.thy @@ -1902,11 +1902,6 @@ lemma clearUntypedFreeIndex_noop_ccorres: apply simp done -lemma mask_shiftl_le_mask: (* FIXME AARCH64 move to Word_Lib *) - "mask n << m \ (mask (n+m) :: 'a::len word)" - by (subst add.commute) - (rule leq_high_bits_shiftr_low_bits_leq_bits, simp) - lemma canonical_address_mdbNext_CL: "canonical_address (mdbNext_CL (mdb_node_lift (cteMDBNode_C cte')))" apply (simp add: mdb_node_lift_def canonical_address_def canonical_address_of_def diff --git a/proof/crefine/AARCH64/Finalise_C.thy b/proof/crefine/AARCH64/Finalise_C.thy index 1e88f94e17..1daea13689 100644 --- a/proof/crefine/AARCH64/Finalise_C.thy +++ b/proof/crefine/AARCH64/Finalise_C.thy @@ -873,11 +873,6 @@ definition ucast irq \ UCAST(32 signed \ irq_len) Kernel_C.maxIRQ) | None \ cirq = ucast irqInvalid" -(* FIXME AARCH64 move to word lib, this is more useful for getting rid of a downcast *) -lemma unat_ucast_unat_id: - "\ unat x < 2^LENGTH('b) \ \ unat (UCAST('a::len \ 'b::len) x) = unat x" - by (simp add: unat_eq_of_nat) - lemma irq_opt_relation_Some_ucast: "\ x && mask (LENGTH(irq_len)) = x; ucast x \ irqInvalid; ucast x \ (scast Kernel_C.maxIRQ :: irq_len word) \ x \ (scast Kernel_C.maxIRQ :: machine_word) \ @@ -1425,10 +1420,6 @@ lemmas lookupPTFromLevel_val_helpers = of_nat_ptTranslationBits_NormalPT_T_val of_nat_ptTranslationBits_VSRootPT_T_val -lemma from_bool_inj[simp]: (* FIXME AARCH64: move to Word_Lib *) - "(from_bool x = from_bool y) = (x = y)" - by (simp add: from_bool_def split: bool.splits) - lemma lookupPTFromLevel_ccorres[unfolded lookupPTFromLevel_val_helpers]: notes Collect_const[simp del] call_ignore_cong[cong] defines "idx i \ of_nat (ptBitsLeft maxPTLevel) - of_nat (ptTranslationBits NormalPT_T) * i" diff --git a/proof/crefine/AARCH64/Recycle_C.thy b/proof/crefine/AARCH64/Recycle_C.thy index 1e020eabfe..df0103866a 100644 --- a/proof/crefine/AARCH64/Recycle_C.thy +++ b/proof/crefine/AARCH64/Recycle_C.thy @@ -1089,11 +1089,6 @@ lemma access_ti_list_word8_array: apply (simp add: typ_info_word word_rsplit_0 word_rsplit_same replicateHider_def replicate_append_same) done -(* FIXME AARCH64 move, original word_rsplit_0 assumes machine word *) -lemma word_rsplit_0_32: - "word_rsplit (0::32 word) = [0, 0, 0, (0::8 word)]" - by (simp add: word_rsplit_def bin_rsplit_def word_bits_def word_size_def Cons_replicate_eq) - lemma coerce_memset_to_heap_update: "heap_update_list x (replicateHider (size_of (TYPE (tcb_C))) 0) = heap_update (tcb_Ptr x) diff --git a/proof/crefine/AARCH64/Syscall_C.thy b/proof/crefine/AARCH64/Syscall_C.thy index 7932ce9289..7cb14a79f7 100644 --- a/proof/crefine/AARCH64/Syscall_C.thy +++ b/proof/crefine/AARCH64/Syscall_C.thy @@ -1700,24 +1700,6 @@ lemma vgicUpdateLR_ccorres_armHSCurVCPU: apply (clarsimp dest!: rf_sr_ksArchState_armHSCurVCPU simp: cur_vcpu_relation_def split: option.splits) done -(* FIXME AARCH64 move to word lib *) -lemma ucast_up_preserves_gt0: - "\ 0 < x; LENGTH('a) < LENGTH('b) \ \ 0 < (ucast x :: 'b::len word)" - for x :: "'a::len word" - by (metis ucast_0 ucast_less_ucast_weak) - -(* FIXME AARCH64 move to word lib *) -lemma ucast_up_preserves_not0: - "\ x \ 0; LENGTH('a) < LENGTH('b::len) \ \ (ucast x :: 'b::len word) \ 0" - for x :: "'a::len word" - by (metis ucast_0 ucast_ucast_id) - -(* FIXME AARCH64 move to word lib *) -lemma word_ctz_upcast_id: - "x \ 0 \ word_ctz (UCAST(32 \ 64) x) = word_ctz x" - unfolding word_ctz_def - by (simp add: ucast_up_app source_size_def target_size_def eq_zero_set_bl) - (* folded calculation of eisr used in vgicMaintenance *) definition eisr_calc :: "32 word \ 32 word \ nat" @@ -1901,7 +1883,7 @@ proof - apply (rule conseqPre, vcg) - subgoal by (clarsimp simp: ucast_up_preserves_not0 word_ctz_upcast_id scast_s64_int_ctz_eq + subgoal by (clarsimp simp: ucast_up_preserves_not0 word_ctz_upcast_id_32_64 scast_s64_int_ctz_eq ctz_add_0x20_s64_int_eq sint_s64_ctz_ge_0 order.trans[OF sint_s64_ctz_le_32]) diff --git a/proof/crefine/AARCH64/VSpace_C.thy b/proof/crefine/AARCH64/VSpace_C.thy index f25894bc9f..65153570b3 100644 --- a/proof/crefine/AARCH64/VSpace_C.thy +++ b/proof/crefine/AARCH64/VSpace_C.thy @@ -526,10 +526,6 @@ lemma levelType_maxPTLevel[simp]: (* FIXME AARCH64: move *) "levelType maxPTLevel = VSRootPT_T" by (simp add: levelType_def) -lemma unat_le_fold: (* FIXME AARCH64: move to Word_Lib *) - "n < 2 ^ LENGTH('a) \ (unat x \ n) = (x \ of_nat n)" for x::"'a::len word" - by (simp add: word_le_nat_alt unat_of_nat_eq) - lemma pte_at_rf_sr: (* FIXME AARCH64: move *) "\ko_at' pte p s; (s, s') \ rf_sr\ \ \pte'. cslift s' (pte_Ptr p) = Some pte' \ cpte_relation pte pte'" @@ -1485,10 +1481,6 @@ lemma findFreeHWASID_ccorres: apply simp done -lemma ucast_and_mask_drop: (* FIXME AARCH64: move to Word_Lib *) - "LENGTH('a) \ n \ (ucast w :: 'b::len word) && mask n = ucast w" for w::"'a::len word" - by word_eqI (fastforce dest: test_bit_lenD) - lemma storeHWASID_ccorres: "ccorres dc xfdc \ (\\asid___unsigned_long = asid\ \ \\hw_asid = vmid\) [] (storeVMID asid vmid) (Call storeHWASID_'proc)" @@ -1709,10 +1701,6 @@ lemma setVMRoot_ccorres: elim!: ccap_relationE split: if_split_asm cap_CL.splits) -lemma add_mask_ignore: (* FIXME AARCH64: move to WordLib *) - "x && mask n = 0 \ v + x && mask n = v && mask n" - by (metis arith_simps(50) mask_eqs(2)) - lemma pptrBaseOffset_cacheLineSize_aligned[simp]: (* FIXME AARCH64: move *) "pptrBaseOffset && mask cacheLineSize = 0" by (simp add: pptrBaseOffset_def paddrBase_def pptrBase_def cacheLineSize_def mask_def) @@ -1911,11 +1899,6 @@ lemma casid_map_relation_vspace_tag: asid_map_get_tag casid_map = scast asid_map_asid_map_vspace" by (clarsimp simp: casid_map_relation_def asid_map_lift_def Let_def split: if_splits) -lemma ucast_ucast_mask_id: (* FIXME AARCH64: move to Word_Lib *) - "\ LENGTH('b::len) < LENGTH('a); n = LENGTH('b) \ \ - UCAST('b \ 'a) (UCAST('a \ 'b) (x && mask n)) = x && mask n" for x :: "'a::len word" - by (simp add: ucast_ucast_len[OF eq_mask_less]) - lemma invalidateTLBByASIDVA_ccorres: "ccorres dc xfdc (valid_arch_state' and K (asid_wf asid)) diff --git a/proof/crefine/ARM_HYP/ADT_C.thy b/proof/crefine/ARM_HYP/ADT_C.thy index 9e90927251..0ceb18e157 100644 --- a/proof/crefine/ARM_HYP/ADT_C.thy +++ b/proof/crefine/ARM_HYP/ADT_C.thy @@ -1014,9 +1014,7 @@ lemma cpspace_vcpu_relation_unique: apply (case_tac "64 \ r"; simp) apply (rule conjI) apply (rule ext, blast) - apply (rule conjI) - apply (rule ext, rename_tac vppi) - apply (rule from_bool_eqI, blast) + apply (rule conjI, blast) apply (case_tac vtimer, case_tac vtimer') apply clarsimp done diff --git a/proof/crefine/ARM_HYP/Ipc_C.thy b/proof/crefine/ARM_HYP/Ipc_C.thy index 8e8a9c706c..1a97373e54 100644 --- a/proof/crefine/ARM_HYP/Ipc_C.thy +++ b/proof/crefine/ARM_HYP/Ipc_C.thy @@ -4074,7 +4074,6 @@ apply (ctac(no_vcg) add: Arch_getSanitiseRegisterInfo_ccorres) msg_align_bits sanitiseRegister_def simp del: upt_rec_numeral cong: if_cong register.case_cong, simp_all add: word_less_nat_alt unat_add_lem[THEN iffD1] unat_of_nat)[1] - apply (rule_tac x=rv in exI, auto)[1] apply (clarsimp simp: n_syscallMessage_def n_msgRegisters_def msgRegisters_ccorres syscallMessage_ccorres diff --git a/proof/crefine/Move_C.thy b/proof/crefine/Move_C.thy index 647c647f23..997c196e24 100644 --- a/proof/crefine/Move_C.thy +++ b/proof/crefine/Move_C.thy @@ -1480,17 +1480,4 @@ lemma multiple_add_less_nat: apply simp done -(* FIXME AARCH64 move to wherever we keep the from_bool/to_bool lemmas *) -lemma word_le_1_and_idem: - "w \ 1 \ w AND 1 = w" for w :: "_ word" - by (metis word_bw_same(1) word_le_1 word_log_esimps(7)) - -(* FIXME AARCH64 move to wherever we keep the from_bool/to_bool lemmas *) -lemma from_to_bool_le_1_idem: - "w \ 1 \ from_bool (to_bool w) = w" - apply (subst word_le_1_and_idem[symmetric], assumption) - apply (simp add: from_to_bool_last_bit) - apply (simp add: word_le_1_and_idem) - done - end diff --git a/proof/crefine/RISCV64/Ipc_C.thy b/proof/crefine/RISCV64/Ipc_C.thy index c66872cdf3..237167fb84 100644 --- a/proof/crefine/RISCV64/Ipc_C.thy +++ b/proof/crefine/RISCV64/Ipc_C.thy @@ -3816,7 +3816,6 @@ lemma copyMRsFaultReply_ccorres_syscall: msg_align_bits sanitiseRegister_def simp del: upt_rec_numeral cong: if_cong register.case_cong, simp_all add: word_less_nat_alt unat_add_lem[THEN iffD1] unat_of_nat)[1] - apply (rule_tac x=rv in exI, auto)[1] apply (clarsimp simp: n_syscallMessage_def n_msgRegisters_def msgRegisters_ccorres syscallMessage_ccorres diff --git a/proof/crefine/X64/Ipc_C.thy b/proof/crefine/X64/Ipc_C.thy index 2adbeff243..4e856790ca 100644 --- a/proof/crefine/X64/Ipc_C.thy +++ b/proof/crefine/X64/Ipc_C.thy @@ -3828,7 +3828,6 @@ lemma copyMRsFaultReply_ccorres_syscall: msg_align_bits sanitiseRegister_def simp del: upt_rec_numeral cong: if_cong register.case_cong, simp_all add: word_less_nat_alt unat_add_lem[THEN iffD1] unat_of_nat)[1] - apply (rule_tac x=rv in exI, auto)[1] apply (clarsimp simp: n_syscallMessage_def n_msgRegisters_def msgRegisters_ccorres syscallMessage_ccorres