1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory WordAbs 8imports "AutoCorres.AutoCorres" 9begin 10 11external_file "word_abs.c" 12install_C_file "word_abs.c" 13autocorres 14 [ (* signed_word_abs is implicit; these are the functions that would be abstracted: *) 15 (*signed_word_abs = 16 S_add_S S_sub_S S_mul_S S_div_S S_mod_S neg_S 17 S_and_S S_or_S S_xor_S not_S 18 U_shiftl_U_abs_S U_shiftr_U_abs_S U_shiftl_S_abs_S U_shiftr_S_abs_S 19 S_shiftl_U_abs_S S_shiftr_U_abs_S S_shiftl_S_abs_S S_shiftr_S_abs_S 20 U_shiftl_U_abs_US U_shiftr_U_abs_US U_shiftl_S_abs_US U_shiftr_S_abs_US 21 S_shiftl_U_abs_US S_shiftr_U_abs_US S_shiftl_S_abs_US S_shiftr_S_abs_US 22 ,*) no_signed_word_abs = 23 U_shiftl_U_no_abs U_shiftr_U_no_abs U_shiftl_S_no_abs U_shiftr_S_no_abs 24 S_shiftl_U_no_abs S_shiftr_U_no_abs S_shiftl_S_no_abs S_shiftr_S_no_abs 25 U_shiftl_U_abs_U U_shiftr_U_abs_U U_shiftl_S_abs_U U_shiftr_S_abs_U 26 S_shiftl_U_abs_U S_shiftr_U_abs_U S_shiftl_S_abs_U S_shiftr_S_abs_U 27 , unsigned_word_abs = 28 ver366 29 U_add_U U_sub_U U_mul_U U_div_U U_mod_U neg_U 30 U_and_U U_or_U U_xor_U not_U 31 U_shiftl_U_abs_U U_shiftr_U_abs_U U_shiftl_S_abs_U U_shiftr_S_abs_U 32 S_shiftl_U_abs_U S_shiftr_U_abs_U S_shiftl_S_abs_U S_shiftr_S_abs_U 33 U_shiftl_U_abs_US U_shiftr_U_abs_US U_shiftl_S_abs_US U_shiftr_S_abs_US 34 S_shiftl_U_abs_US S_shiftr_U_abs_US S_shiftl_S_abs_US S_shiftr_S_abs_US 35 , ts_rules = nondet 36] "word_abs.c" 37 38context word_abs begin 39 40lemma "\<lbrace> P \<rbrace> ver366' 0 \<lbrace> \<lambda>v s. v = 0 \<and> P s \<rbrace>" 41 by (wpsimp simp: ver366'_def) 42lemma "\<lbrace> P \<rbrace> ver366' UINT_MAX \<lbrace> \<lambda>v s. v = UINT_MAX-1 \<and> P s \<rbrace>" 43 by (wpsimp simp: ver366'_def UINT_MAX_def) 44 45section \<open>Arithmetic ops\<close> 46thm S_add_S'_def S_sub_S'_def S_mul_S'_def S_div_S'_def S_mod_S'_def neg_S'_def 47 U_add_U'_def U_sub_U'_def U_mul_U'_def U_div_U'_def U_mod_U'_def neg_U'_def 48 49lemma "x + y < INT_MIN \<or> x + y > INT_MAX \<Longrightarrow> \<not> no_fail \<top> (S_add_S' (x::int) (y::int))" 50 by (monad_eq simp: S_add_S'_def no_fail_def INT_MIN_def INT_MAX_def) 51lemma "\<lbrace>\<lambda>s. INT_MIN \<le> x + y \<and> x + y \<le> INT_MAX \<and> P s\<rbrace> 52 S_add_S' (x::int) (y::int) 53 \<lbrace>\<lambda>r s. r = x + y \<and> P s\<rbrace>!" 54 by (wpsimp simp: S_add_S'_def INT_MIN_def INT_MAX_def) 55lemma "x - y < INT_MIN \<or> x - y > INT_MAX \<Longrightarrow> \<not> no_fail \<top> (S_sub_S' (x::int) (y::int))" 56 by (monad_eq simp: S_sub_S'_def no_fail_def INT_MIN_def INT_MAX_def) 57lemma "\<lbrace>\<lambda>s. INT_MIN \<le> x - y \<and> x - y \<le> INT_MAX \<and> P s\<rbrace> 58 S_sub_S' (x::int) (y::int) 59 \<lbrace>\<lambda>r s. r = x - y \<and> P s\<rbrace>!" 60 by (wpsimp simp: S_sub_S'_def INT_MIN_def INT_MAX_def) 61lemma "x * y < INT_MIN \<or> x * y > INT_MAX \<Longrightarrow> \<not> no_fail \<top> (S_mul_S' (x::int) (y::int))" 62 by (monad_eq simp: S_mul_S'_def no_fail_def INT_MIN_def INT_MAX_def) 63lemma "\<lbrace>\<lambda>s. INT_MIN \<le> x * y \<and> x * y \<le> INT_MAX \<and> P s\<rbrace> 64 S_mul_S' (x::int) (y::int) 65 \<lbrace>\<lambda>r s. r = x * y \<and> P s\<rbrace>!" 66 by (wpsimp simp: S_mul_S'_def INT_MIN_def INT_MAX_def) 67lemma "y = 0 \<or> x sdiv y < INT_MIN \<or> x sdiv y > INT_MAX \<Longrightarrow> \<not> no_fail \<top> (S_div_S' (x::int) (y::int))" 68 by (monad_eq simp: S_div_S'_def no_fail_def INT_MIN_def INT_MAX_def) 69lemma "\<lbrace>\<lambda>s. y \<noteq> 0 \<and> INT_MIN \<le> x sdiv y \<and> x sdiv y \<le> INT_MAX \<and> P s\<rbrace> 70 S_div_S' (x::int) (y::int) 71 \<lbrace>\<lambda>r s. r = x sdiv y \<and> P s\<rbrace>!" 72 by (wpsimp simp: S_div_S'_def INT_MIN_def INT_MAX_def) 73lemma "y = 0 \<or> x smod y < INT_MIN \<or> x smod y > INT_MAX \<Longrightarrow> \<not> no_fail \<top> (S_mod_S' (x::int) (y::int))" 74 by (monad_eq simp: S_mod_S'_def no_fail_def INT_MIN_def INT_MAX_def) 75lemma "\<lbrace>\<lambda>s. y \<noteq> 0 \<and> INT_MIN \<le> x smod y \<and> x smod y \<le> INT_MAX \<and> P s\<rbrace> 76 S_mod_S' (x::int) (y::int) 77 \<lbrace>\<lambda>r s. r = x smod y \<and> P s\<rbrace>!" 78 by (wpsimp simp: S_mod_S'_def INT_MIN_def INT_MAX_def) 79lemma "x \<le> INT_MIN \<or> x > -INT_MIN \<Longrightarrow> \<not> no_fail \<top> (neg_S' (x::int))" 80 by (monad_eq simp: neg_S'_def no_fail_def INT_MIN_def) 81lemma "\<lbrace>\<lambda>s. INT_MIN < x \<and> x \<le> -INT_MIN \<and> P s\<rbrace> neg_S' (x::int) \<lbrace>\<lambda>r s. r = -x \<and> P s\<rbrace>!" 82 by (wpsimp simp: neg_S'_def INT_MIN_def) 83 84lemma "x + y > UINT_MAX \<Longrightarrow> \<not> no_fail \<top> (U_add_U' (x::nat) (y::nat))" 85 by (monad_eq simp: U_add_U'_def no_fail_def) 86lemma "\<lbrace>\<lambda>s. x + y \<le> UINT_MAX \<and> P s\<rbrace> 87 U_add_U' (x::nat) (y::nat) 88 \<lbrace>\<lambda>r s. r = x + y \<and> P s\<rbrace>!" 89 by (wpsimp simp: U_add_U'_def UINT_MAX_def) 90lemma "x < y \<Longrightarrow> \<not> no_fail \<top> (U_sub_U' (x::nat) (y::nat))" 91 by (monad_eq simp: U_sub_U'_def no_fail_def) 92lemma "\<lbrace>\<lambda>s. x \<ge> y \<and> P s\<rbrace> 93 U_sub_U' (x::nat) (y::nat) 94 \<lbrace>\<lambda>r s. r = x - y \<and> P s\<rbrace>!" 95 by (wpsimp simp: U_sub_U'_def) 96lemma "x * y > UINT_MAX \<Longrightarrow> \<not> no_fail \<top> (U_mul_U' (x::nat) (y::nat))" 97 by (monad_eq simp: U_mul_U'_def no_fail_def) 98lemma "\<lbrace>\<lambda>s. x * y \<le> UINT_MAX \<and> P s\<rbrace> 99 U_mul_U' (x::nat) (y::nat) 100 \<lbrace>\<lambda>r s. r = x * y \<and> P s\<rbrace>!" 101 by (wpsimp simp: U_mul_U'_def UINT_MAX_def) 102lemma "y = 0 \<Longrightarrow> \<not> no_fail \<top> (U_div_U' (x::nat) (y::nat))" 103 by (monad_eq simp: U_div_U'_def no_fail_def) 104lemma "\<lbrace>\<lambda>s. y \<noteq> 0 \<and> P s\<rbrace> 105 U_div_U' (x::nat) (y::nat) 106 \<lbrace>\<lambda>r s. r = x div y \<and> P s\<rbrace>!" 107 by (wpsimp simp: U_div_U'_def UINT_MAX_def) 108lemma "y = 0 \<Longrightarrow> \<not> no_fail \<top> (U_mod_U' (x::nat) (y::nat))" 109 by (monad_eq simp: U_mod_U'_def no_fail_def) 110lemma "\<lbrace>\<lambda>s. y \<noteq> 0 \<and> P s\<rbrace> 111 U_mod_U' (x::nat) (y::nat) 112 \<lbrace>\<lambda>r s. r = x mod y \<and> P s\<rbrace>!" 113 by (wpsimp simp: U_mod_U'_def UINT_MAX_def) 114lemma "\<lbrace>P\<rbrace> neg_U' (x::nat) \<lbrace>\<lambda>r s. r = (if x = 0 then 0 else Suc UINT_MAX - x) \<and> P s\<rbrace>!" 115 unfolding neg_U'_def by (wp, simp) 116 117 118section \<open>Bitwise ops\<close> 119 120thm S_and_S'_def S_or_S'_def S_xor_S'_def not_S'_def 121 U_and_U'_def U_or_U'_def U_xor_U'_def not_U'_def 122 123lemma "\<lbrace>P\<rbrace> S_and_S' (x::int) (y::int) \<lbrace>\<lambda>r s. r = x AND y \<and> P s\<rbrace>!" 124 by (wpsimp simp: S_and_S'_def) 125lemma "\<lbrace>P\<rbrace> S_or_S' (x::int) (y::int) \<lbrace>\<lambda>r s. r = x OR y \<and> P s\<rbrace>!" 126 by (wpsimp simp: S_or_S'_def) 127lemma "\<lbrace>P\<rbrace> S_xor_S' (x::int) (y::int) \<lbrace>\<lambda>r s. r = x XOR y \<and> P s\<rbrace>!" 128 by (wpsimp simp: S_xor_S'_def) 129lemma "\<lbrace>P\<rbrace> not_S' (x::int) \<lbrace>\<lambda>r s. r = NOT x \<and> P s\<rbrace>!" 130 by (wpsimp simp: not_S'_def) 131 132lemma "\<lbrace>P\<rbrace> U_and_U' (x::nat) (y::nat) \<lbrace>\<lambda>r s. r = x AND y \<and> P s\<rbrace>!" 133 by (wpsimp simp: U_and_U'_def) 134lemma "\<lbrace>P\<rbrace> U_or_U' (x::nat) (y::nat) \<lbrace>\<lambda>r s. r = x OR y \<and> P s\<rbrace>!" 135 by (wpsimp simp: U_or_U'_def) 136lemma "\<lbrace>P\<rbrace> U_xor_U' (x::nat) (y::nat) \<lbrace>\<lambda>r s. r = x XOR y \<and> P s\<rbrace>!" 137 by (wpsimp simp: U_xor_U'_def) 138lemma "\<lbrace>P\<rbrace> not_U' (x::nat) \<lbrace>\<lambda>r s. r = UINT_MAX - x \<and> P s\<rbrace>!" 139 by (wpsimp simp: not_U'_def) 140 141 142section \<open>Left shifts\<close> 143 144thm U_shiftl_U_abs_US'_def U_shiftr_U_abs_US'_def U_shiftl_S_abs_US'_def U_shiftr_S_abs_US'_def 145 S_shiftl_U_abs_US'_def S_shiftr_U_abs_US'_def S_shiftl_S_abs_US'_def S_shiftr_S_abs_US'_def 146thm U_shiftl_U_abs_U'_def U_shiftr_U_abs_U'_def U_shiftl_S_abs_U'_def U_shiftr_S_abs_U'_def 147 S_shiftl_U_abs_U'_def S_shiftr_U_abs_U'_def S_shiftl_S_abs_U'_def S_shiftr_S_abs_U'_def 148thm U_shiftl_U_abs_S'_def U_shiftr_U_abs_S'_def U_shiftl_S_abs_S'_def U_shiftr_S_abs_S'_def 149 S_shiftl_U_abs_S'_def S_shiftr_U_abs_S'_def S_shiftl_S_abs_S'_def S_shiftr_S_abs_S'_def 150thm U_shiftl_U_no_abs'_def U_shiftr_U_no_abs'_def U_shiftl_S_no_abs'_def U_shiftr_S_no_abs'_def 151 S_shiftl_U_no_abs'_def S_shiftr_U_no_abs'_def S_shiftl_S_no_abs'_def S_shiftr_S_no_abs'_def 152 153subsection \<open>@{text U_shiftl_U}\<close> 154 155lemma "n \<ge> 32 \<Longrightarrow> \<not> no_fail \<top> (U_shiftl_U_abs_US' (x :: nat) (n :: nat))" 156 by (monad_eq simp: U_shiftl_U_abs_US'_def no_fail_def) 157lemma "\<lbrace>\<lambda>s. n < 32 \<and> x << n \<le> UINT_MAX\<rbrace> 158 U_shiftl_U_abs_US' (x::nat) (n::nat) 159 \<lbrace>\<lambda>r s. r = x << n\<rbrace>!" 160 by (wpsimp simp: U_shiftl_U_abs_US'_def UINT_MAX_def) 161 162lemma "n \<ge> 32 \<Longrightarrow> \<not> no_fail \<top> (U_shiftl_U_abs_U' (x :: nat) (n :: nat))" 163 by (monad_eq simp: U_shiftl_U_abs_U'_def no_fail_def) 164lemma "\<lbrace>\<lambda>s. n < 32 \<and> x << n \<le> UINT_MAX\<rbrace> 165 U_shiftl_U_abs_U' (x::nat) (n::nat) 166 \<lbrace>\<lambda>r s. r = x << n\<rbrace>!" 167 by (wpsimp simp: U_shiftl_U_abs_U'_def UINT_MAX_def) 168 169lemma "n \<ge> 32 \<Longrightarrow> \<not> no_fail \<top> (U_shiftl_U_abs_S' (x :: word32) (n :: word32))" 170 by (monad_eq simp: U_shiftl_U_abs_S'_def no_fail_def word_le_not_less) 171lemma "\<lbrace>\<lambda>s. n < 32\<rbrace> 172 U_shiftl_U_abs_S' (x::word32) (n::word32) 173 \<lbrace>\<lambda>r s. r = x << unat n\<rbrace>!" 174 by (wpsimp simp: U_shiftl_U_abs_S'_def) 175 176lemma "n \<ge> 32 \<Longrightarrow> \<not> no_fail \<top> (U_shiftl_U_no_abs' (x :: word32) (n :: word32))" 177 by (monad_eq simp: U_shiftl_U_no_abs'_def no_fail_def word_le_not_less) 178lemma "\<lbrace>\<lambda>s. n < 32\<rbrace> 179 U_shiftl_U_no_abs' (x::word32) (n::word32) 180 \<lbrace>\<lambda>r s. r = x << unat n\<rbrace>!" 181 by (wpsimp simp: U_shiftl_U_no_abs'_def) 182 183subsection \<open>@{text U_shiftl_S}\<close> 184 185lemma "n < 0 \<Longrightarrow> \<not> no_fail \<top> (U_shiftl_S_abs_US' (x :: nat) (n :: int))" 186 by (monad_eq simp: U_shiftl_S_abs_US'_def no_fail_def) 187lemma "n \<ge> 32 \<Longrightarrow> \<not> no_fail \<top> (U_shiftl_S_abs_US' (x :: nat) (n :: int))" 188 by (monad_eq simp: U_shiftl_S_abs_US'_def no_fail_def) 189lemma "x << nat n > UINT_MAX \<Longrightarrow> \<not> no_fail \<top> (U_shiftl_S_abs_US' (x :: nat) (n :: int))" 190 by (monad_eq simp: U_shiftl_S_abs_US'_def no_fail_def UINT_MAX_def) 191lemma "\<lbrace>\<lambda>s. 0 \<le> n \<and> n < 32 \<and> x << nat n \<le> UINT_MAX\<rbrace> 192 U_shiftl_S_abs_US' (x::nat) (n::int) 193 \<lbrace>\<lambda>r s. r = x << nat n\<rbrace>!" 194 by (wpsimp simp: U_shiftl_S_abs_US'_def UINT_MAX_def) 195 196lemma "n <s 0 \<Longrightarrow> \<not> no_fail \<top> (U_shiftl_S_abs_U' (x :: nat) (n :: sword32))" 197 by (monad_eq simp: U_shiftl_S_abs_U'_def no_fail_def word_sless_alt word_sle_def) 198lemma "32 <=s n \<Longrightarrow> \<not> no_fail \<top> (U_shiftl_S_abs_U' (x :: nat) (n :: sword32))" 199 by (monad_eq simp: U_shiftl_S_abs_U'_def no_fail_def word_sless_alt word_sle_def) 200lemma "x << unat n > UINT_MAX \<Longrightarrow> \<not> no_fail \<top> (U_shiftl_S_abs_U' (x :: nat) (n :: sword32))" 201 by (monad_eq simp: U_shiftl_S_abs_U'_def no_fail_def 202 word_sless_alt word_sle_def nat_sint UINT_MAX_def) 203lemma "\<lbrace>\<lambda>s. 0 <=s n \<and> n <s 32 \<and> x << unat n \<le> UINT_MAX\<rbrace> 204 U_shiftl_S_abs_U' (x::nat) (n::sword32) 205 \<lbrace>\<lambda>r s. r = x << unat n\<rbrace>!" 206 by (wpsimp simp: U_shiftl_S_abs_U'_def UINT_MAX_def nat_sint word_sle_def word_sless_alt) 207 208lemma "n < 0 \<Longrightarrow> \<not> no_fail \<top> (U_shiftl_S_abs_S' (x :: word32) (n :: int))" 209 by (monad_eq simp: U_shiftl_S_abs_S'_def no_fail_def) 210lemma "n \<ge> 32 \<Longrightarrow> \<not> no_fail \<top> (U_shiftl_S_abs_S' (x :: word32) (n :: int))" 211 by (monad_eq simp: U_shiftl_S_abs_S'_def no_fail_def) 212lemma "\<lbrace>\<lambda>s. 0 \<le> n \<and> n < 32\<rbrace> 213 U_shiftl_S_abs_S' (x::word32) (n::int) 214 \<lbrace>\<lambda>r s. r = x << nat n\<rbrace>!" 215 by (wpsimp simp: U_shiftl_S_abs_S'_def UINT_MAX_def unat_of_int) 216 217lemma "n <s 0 \<Longrightarrow> \<not> no_fail \<top> (U_shiftl_S_no_abs' (x :: word32) (n :: sword32))" 218 by (monad_eq simp: U_shiftl_S_no_abs'_def no_fail_def word_sle_def word_sless_alt) 219lemma "32 <=s n \<Longrightarrow> \<not> no_fail \<top> (U_shiftl_S_no_abs' (x :: word32) (n :: sword32))" 220 by (monad_eq simp: U_shiftl_S_no_abs'_def no_fail_def word_sle_def word_sless_alt) 221lemma "\<lbrace>\<lambda>s. 0 <=s n \<and> n <s 32\<rbrace> 222 U_shiftl_S_no_abs' (x :: word32) (n :: sword32) 223 \<lbrace>\<lambda>r s. r = x << unat n\<rbrace>!" 224 by (wpsimp simp: U_shiftl_S_no_abs'_def UINT_MAX_def) 225 226subsection \<open>@{text S_shiftl_U}\<close> 227 228lemma "x < 0 \<Longrightarrow> \<not> no_fail \<top> (S_shiftl_U_abs_US' (x :: int) (n :: nat))" 229 by (monad_eq simp: S_shiftl_U_abs_US'_def no_fail_def) 230lemma "n \<ge> 32 \<Longrightarrow> \<not> no_fail \<top> (S_shiftl_U_abs_US' (x :: int) (n :: nat))" 231 by (monad_eq simp: S_shiftl_U_abs_US'_def no_fail_def) 232lemma "x << nat n > INT_MAX \<Longrightarrow> \<not> no_fail \<top> (S_shiftl_U_abs_US' (x :: int) (n :: nat))" 233 by (monad_eq simp: S_shiftl_U_abs_US'_def no_fail_def INT_MAX_def) 234lemma "\<lbrace>\<lambda>s. n < 32 \<and> 0 \<le> x \<and> x << nat n \<le> INT_MAX\<rbrace> 235 S_shiftl_U_abs_US' (x::int) (n::nat) 236 \<lbrace>\<lambda>r s. r = x << nat n\<rbrace>!" 237 apply (wpsimp simp: S_shiftl_U_abs_US'_def INT_MAX_def shiftl_nat_def shiftl_int_def) 238 apply (subst unat_of_int) 239 apply simp 240 apply (drule le_less_trans[where x="x*2^n" and z="2^32"]) 241 apply simp 242 apply (subst mult_less_cancel_left_pos[where c="2^n", symmetric]) 243 apply simp 244 apply (subst (asm) mult.commute) 245 apply (erule less_le_trans) 246 apply simp 247 apply (simp flip: nat_mult_distrib nat_power_eq nat_numeral) 248 done 249 250lemma "x <s 0 \<Longrightarrow> \<not> no_fail \<top> (S_shiftl_U_abs_U' (x :: sword32) (n :: nat))" 251 by (monad_eq simp: S_shiftl_U_abs_U'_def no_fail_def word_sle_def word_sless_alt) 252lemma "n \<ge> 32 \<Longrightarrow> \<not> no_fail \<top> (S_shiftl_U_abs_U' (x :: sword32) (n :: nat))" 253 apply (monad_eq simp: S_shiftl_U_abs_U'_def no_fail_def) 254 oops \<comment> \<open>C parser issue: Jira VER-509\<close> 255lemma "sint x << n > INT_MAX \<Longrightarrow> \<not> no_fail \<top> (S_shiftl_U_abs_U' (x :: sword32) (n :: nat))" 256 by (monad_eq simp: S_shiftl_U_abs_U'_def no_fail_def shiftl_int_def INT_MAX_def 257 nat_int_comparison(2) int_unat_nonneg) 258lemma "\<lbrace>\<lambda>s. n < 32 \<and> 0 <=s x \<and> sint x << nat n \<le> INT_MAX\<rbrace> 259 S_shiftl_U_abs_U' (x::sword32) (n::nat) 260 \<lbrace>\<lambda>r s. r = x << nat n\<rbrace>!" 261 by (wpsimp simp: S_shiftl_U_abs_U'_def INT_MAX_def shiftl_int_def 262 nat_int_comparison(2) int_unat_nonneg) 263 264lemma "x < 0 \<Longrightarrow> \<not> no_fail \<top> (S_shiftl_U_abs_S' (x :: int) (n :: word32))" 265 by (monad_eq simp: S_shiftl_U_abs_S'_def no_fail_def) 266lemma "n \<ge> 32 \<Longrightarrow> \<not> no_fail \<top> (S_shiftl_U_abs_S' (x :: int) (n :: word32))" 267 by (monad_eq simp: S_shiftl_U_abs_S'_def no_fail_def word_le_nat_alt) 268lemma "x << unat n > INT_MAX \<Longrightarrow> \<not> no_fail \<top> (S_shiftl_U_abs_S' (x :: int) (n :: word32))" 269 by (monad_eq simp: S_shiftl_U_abs_S'_def no_fail_def INT_MAX_def) 270lemma "\<lbrace>\<lambda>s. n < 32 \<and> 0 \<le> x \<and> x << unat n \<le> INT_MAX\<rbrace> 271 S_shiftl_U_abs_S' (x::int) (n::word32) 272 \<lbrace>\<lambda>r s. r = x << unat n\<rbrace>!" 273 apply (wpsimp simp: S_shiftl_U_abs_S'_def INT_MAX_def shiftl_nat_def shiftl_int_def 274 word_less_nat_alt) 275 apply (subst unat_of_int) 276 apply simp 277 apply (drule le_less_trans[where x="x*2^unat n" and z="2^32"]) 278 apply simp 279 apply simp 280 apply (subst mult_less_cancel_left_pos[where c="2^unat n", symmetric]) 281 apply simp 282 apply (subst (asm) mult.commute) 283 apply (erule less_le_trans) 284 apply simp 285 apply (simp flip: nat_mult_distrib nat_power_eq nat_numeral) 286 done 287 288lemma "x <s 0 \<Longrightarrow> \<not> no_fail \<top> (S_shiftl_U_no_abs' (x :: sword32) (n :: word32))" 289 by (monad_eq simp: S_shiftl_U_no_abs'_def no_fail_def word_sle_def word_sless_alt) 290lemma "n \<ge> 32 \<Longrightarrow> \<not> no_fail \<top> (S_shiftl_U_no_abs' (x :: sword32) (n :: word32))" 291 apply (monad_eq simp: S_shiftl_U_no_abs'_def no_fail_def) 292 oops \<comment> \<open>C parser issue: Jira VER-509\<close> 293lemma "sint x << unat n > INT_MAX \<Longrightarrow> \<not> no_fail \<top> (S_shiftl_U_no_abs' (x :: sword32) (n :: word32))" 294 by (monad_eq simp: S_shiftl_U_no_abs'_def no_fail_def shiftl_int_def INT_MAX_def 295 nat_int_comparison(2) int_unat_nonneg) 296lemma "\<lbrace>\<lambda>s. n < 32 \<and> 0 <=s x \<and> sint x << unat n \<le> INT_MAX\<rbrace> 297 S_shiftl_U_no_abs' (x::sword32) (n::word32) 298 \<lbrace>\<lambda>r s. r = x << unat n\<rbrace>!" 299 by (wpsimp simp: S_shiftl_U_no_abs'_def INT_MAX_def shiftl_int_def 300 nat_int_comparison(2) int_unat_nonneg) 301 302subsection \<open>@{text S_shiftl_S}\<close> 303 304lemma "x < 0 \<Longrightarrow> \<not> no_fail \<top> (S_shiftl_S_abs_US' (x :: int) (n :: int))" 305 by (monad_eq simp: S_shiftl_S_abs_US'_def no_fail_def) 306lemma "n < 0 \<Longrightarrow> \<not> no_fail \<top> (S_shiftl_S_abs_US' (x :: int) (n :: int))" 307 by (monad_eq simp: S_shiftl_S_abs_US'_def no_fail_def) 308lemma "x << nat n > INT_MAX \<Longrightarrow> \<not> no_fail \<top> (S_shiftl_S_abs_US' (x :: int) (n :: int))" 309 by (monad_eq simp: S_shiftl_S_abs_US'_def no_fail_def INT_MAX_def) 310lemma "n \<ge> 32 \<Longrightarrow> \<not> no_fail \<top> (S_shiftl_S_abs_US' (x :: int) (n :: int))" 311 by (monad_eq simp: S_shiftl_S_abs_US'_def no_fail_def) 312lemma "\<lbrace>\<lambda>s. 0 \<le> n \<and> n < 32 \<and> 0 \<le> x \<and> x << nat n \<le> INT_MAX\<rbrace> 313 S_shiftl_S_abs_US' (x::int) (n::int) 314 \<lbrace>\<lambda>r s. r = x << nat n\<rbrace>!" 315 apply (wpsimp simp: S_shiftl_S_abs_US'_def INT_MAX_def shiftl_nat_def shiftl_int_def) 316 apply (subst unat_of_int) 317 apply simp 318 apply simp 319 apply (drule le_less_trans[where x="x*2^nat n" and z="2^32"]) 320 apply simp 321 apply (subst mult_less_cancel_left_pos[where c="2^nat n", symmetric]) 322 apply simp 323 apply (subst (asm) mult.commute) 324 apply (erule less_le_trans) 325 apply simp 326 apply (subst unat_of_int) 327 apply simp 328 apply simp 329 apply (simp flip: nat_mult_distrib nat_power_eq nat_numeral) 330 done 331 332lemma "x <s 0 \<Longrightarrow> \<not> no_fail \<top> (S_shiftl_S_abs_U' (x :: sword32) (n :: sword32))" 333 by (monad_eq simp: S_shiftl_S_abs_U'_def no_fail_def word_sle_def word_sless_alt) 334lemma "n <s 0 \<Longrightarrow> \<not> no_fail \<top> (S_shiftl_S_abs_U' (x :: sword32) (n :: sword32))" 335 by (monad_eq simp: S_shiftl_S_abs_U'_def no_fail_def word_sle_def word_sless_alt) 336lemma "32 <=s n \<Longrightarrow> \<not> no_fail \<top> (S_shiftl_S_abs_U' (x :: sword32) (n :: sword32))" 337 apply (monad_eq simp: S_shiftl_S_abs_U'_def no_fail_def word_sle_def word_sless_alt) 338 oops \<comment> \<open>C parser issue: Jira VER-509\<close> 339lemma "sint x << unat n > INT_MAX \<Longrightarrow> \<not> no_fail \<top> (S_shiftl_S_abs_U' (x :: sword32) (n :: sword32))" 340 by (monad_eq simp: S_shiftl_S_abs_U'_def no_fail_def shiftl_int_def INT_MAX_def 341 nat_int_comparison(2) int_unat_nonneg) 342lemma "\<lbrace>\<lambda>s. 0 <=s n \<and> n <s 32 \<and> 0 <=s x \<and> sint x << unat n \<le> INT_MAX\<rbrace> 343 S_shiftl_S_abs_U' (x::sword32) (n::sword32) 344 \<lbrace>\<lambda>r s. r = x << unat n\<rbrace>!" 345 by (wpsimp simp: S_shiftl_S_abs_U'_def INT_MAX_def shiftl_int_def 346 nat_int_comparison(2) int_unat_nonneg) 347 348lemma "x < 0 \<Longrightarrow> \<not> no_fail \<top> (S_shiftl_S_abs_S' (x :: int) (n :: int))" 349 by (monad_eq simp: S_shiftl_S_abs_S'_def no_fail_def) 350lemma "n < 0 \<Longrightarrow> \<not> no_fail \<top> (S_shiftl_S_abs_S' (x :: int) (n :: int))" 351 by (monad_eq simp: S_shiftl_S_abs_S'_def no_fail_def) 352lemma "n \<ge> 32 \<Longrightarrow> \<not> no_fail \<top> (S_shiftl_S_abs_S' (x :: int) (n :: int))" 353 by (monad_eq simp: S_shiftl_S_abs_S'_def no_fail_def) 354lemma "x << n > INT_MAX \<Longrightarrow> \<not> no_fail \<top> (S_shiftl_S_abs_S' (x :: int) (n :: int))" 355 by (monad_eq simp: S_shiftl_S_abs_S'_def no_fail_def INT_MAX_def) 356lemma "\<lbrace>\<lambda>s. 0 \<le> n \<and> n < 32 \<and> 0 \<le> x \<and> x << n \<le> INT_MAX\<rbrace> 357 S_shiftl_S_abs_S' (x::int) (n::int) 358 \<lbrace>\<lambda>r s. r = x << nat n\<rbrace>!" 359 apply (wpsimp simp: S_shiftl_S_abs_S'_def INT_MAX_def shiftl_nat_def shiftl_int_def) 360 apply (subst unat_of_int) 361 apply simp 362 apply (drule le_less_trans[where x="x*2^n" and z="2^32"]) 363 apply simp 364 apply (subst mult_less_cancel_left_pos[where c="2^n", symmetric]) 365 apply simp 366 apply (subst (asm) mult.commute) 367 apply (erule less_le_trans) 368 apply simp 369 apply (simp add: le_unat_uoi[where z="32"]) 370 apply (simp flip: nat_mult_distrib nat_power_eq nat_numeral) 371 done 372 373lemma "x <s 0 \<Longrightarrow> \<not> no_fail \<top> (S_shiftl_S_no_abs' (x :: sword32) (n :: sword32))" 374 by (monad_eq simp: S_shiftl_S_no_abs'_def no_fail_def word_sle_def word_sless_alt) 375lemma "n <s 0 \<Longrightarrow> \<not> no_fail \<top> (S_shiftl_S_no_abs' (x :: sword32) (n :: sword32))" 376 by (monad_eq simp: S_shiftl_S_no_abs'_def no_fail_def word_sle_def word_sless_alt) 377lemma "32 <=s n \<Longrightarrow> \<not> no_fail \<top> (S_shiftl_S_no_abs' (x :: sword32) (n :: sword32))" 378 apply (monad_eq simp: S_shiftl_S_no_abs'_def no_fail_def) 379 oops \<comment> \<open>C parser issue: Jira VER-509\<close> 380lemma "sint x << unat n > INT_MAX \<Longrightarrow> \<not> no_fail \<top> (S_shiftl_S_no_abs' (x :: sword32) (n :: sword32))" 381 by (monad_eq simp: S_shiftl_S_no_abs'_def no_fail_def shiftl_int_def INT_MAX_def 382 nat_int_comparison(2) int_unat_nonneg) 383lemma "\<lbrace>\<lambda>s. 0 <=s n \<and> n <s 32 \<and> 0 <=s x \<and> sint x << unat n \<le> INT_MAX\<rbrace> 384 S_shiftl_S_no_abs' (x::sword32) (n::sword32) 385 \<lbrace>\<lambda>r s. r = x << unat n\<rbrace>!" 386 by (wpsimp simp: S_shiftl_S_no_abs'_def INT_MAX_def shiftl_int_def 387 nat_int_comparison(2) int_unat_nonneg) 388 389 390section \<open>Right shifts\<close> 391 392subsection \<open>@{text U_shiftr_U}\<close> 393 394lemma "n \<ge> 32 \<Longrightarrow> \<not> no_fail \<top> (U_shiftr_U_abs_US' (x :: nat) (n :: nat))" 395 by (monad_eq simp: U_shiftr_U_abs_US'_def no_fail_def) 396lemma "\<lbrace>\<lambda>s. n < 32\<rbrace> U_shiftr_U_abs_US' (x::nat) (n::nat) \<lbrace>\<lambda>r s. r = x >> n\<rbrace>!" 397 by (wpsimp simp: U_shiftr_U_abs_US'_def) 398 399lemma "n \<ge> 32 \<Longrightarrow> \<not> no_fail \<top> (U_shiftr_U_abs_U' (x :: nat) (n :: nat))" 400 by (monad_eq simp: U_shiftr_U_abs_U'_def no_fail_def) 401lemma "\<lbrace>\<lambda>s. n < 32\<rbrace> U_shiftr_U_abs_U' (x::nat) (n::nat) \<lbrace>\<lambda>r s. r = x >> n\<rbrace>!" 402 by (wpsimp simp: U_shiftr_U_abs_U'_def) 403 404lemma "n \<ge> 32 \<Longrightarrow> \<not> no_fail \<top> (U_shiftr_U_abs_S' (x :: word32) (n :: word32))" 405 by (monad_eq simp: U_shiftr_U_abs_S'_def no_fail_def word_le_not_less) 406lemma "\<lbrace>\<lambda>s. n < 32\<rbrace> U_shiftr_U_abs_S' (x::word32) (n::word32) \<lbrace>\<lambda>r s. r = x >> unat n\<rbrace>!" 407 by (wpsimp simp: U_shiftr_U_abs_S'_def) 408 409lemma "n \<ge> 32 \<Longrightarrow> \<not> no_fail \<top> (U_shiftr_U_no_abs' (x :: word32) (n :: word32))" 410 by (monad_eq simp: U_shiftr_U_no_abs'_def no_fail_def word_le_not_less) 411lemma "\<lbrace>\<lambda>s. n < 32\<rbrace> U_shiftr_U_no_abs' (x::word32) (n::word32) \<lbrace>\<lambda>r s. r = x >> unat n\<rbrace>!" 412 by (wpsimp simp: U_shiftr_U_no_abs'_def) 413 414subsection \<open>@{text U_shiftr_S}\<close> 415 416lemma "n < 0 \<Longrightarrow> \<not> no_fail \<top> (U_shiftr_S_abs_US' (x :: nat) (n :: int))" 417 by (monad_eq simp: U_shiftr_S_abs_US'_def no_fail_def) 418lemma "n \<ge> 32 \<Longrightarrow> \<not> no_fail \<top> (U_shiftr_S_abs_US' (x :: nat) (n :: int))" 419 by (monad_eq simp: U_shiftr_S_abs_US'_def no_fail_def) 420lemma "\<lbrace>\<lambda>s. 0 \<le> n \<and> n < 32\<rbrace> U_shiftr_S_abs_US' (x::nat) (n::int) \<lbrace>\<lambda>r s. r = x >> nat n\<rbrace>!" 421 by (wpsimp simp: U_shiftr_S_abs_US'_def) 422 423lemma "n <s 0 \<Longrightarrow> \<not> no_fail \<top> (U_shiftr_S_abs_U' (x :: nat) (n :: sword32))" 424 by (monad_eq simp: U_shiftr_S_abs_U'_def no_fail_def word_sless_alt word_sle_def) 425lemma "32 <=s n \<Longrightarrow> \<not> no_fail \<top> (U_shiftr_S_abs_U' (x :: nat) (n :: sword32))" 426 by (monad_eq simp: U_shiftr_S_abs_U'_def no_fail_def word_sless_alt word_sle_def) 427lemma "\<lbrace>\<lambda>s. 0 <=s n \<and> n <s 32\<rbrace> U_shiftr_S_abs_U' (x::nat) (n::sword32) \<lbrace>\<lambda>r s. r = x >> unat n\<rbrace>!" 428 by (wpsimp simp: U_shiftr_S_abs_U'_def nat_sint word_sle_def word_sless_alt) 429 430lemma "n < 0 \<Longrightarrow> \<not> no_fail \<top> (U_shiftr_S_abs_S' (x :: word32) (n :: int))" 431 by (monad_eq simp: U_shiftr_S_abs_S'_def no_fail_def) 432lemma "n \<ge> 32 \<Longrightarrow> \<not> no_fail \<top> (U_shiftr_S_abs_S' (x :: word32) (n :: int))" 433 by (monad_eq simp: U_shiftr_S_abs_S'_def no_fail_def) 434lemma "\<lbrace>\<lambda>s. 0 \<le> n \<and> n < 32\<rbrace> U_shiftr_S_abs_S' (x::word32) (n::int) \<lbrace>\<lambda>r s. r = x >> nat n\<rbrace>!" 435 by (wpsimp simp: U_shiftr_S_abs_S'_def unat_of_int) 436 437lemma "n <s 0 \<Longrightarrow> \<not> no_fail \<top> (U_shiftr_S_no_abs' (x :: word32) (n :: sword32))" 438 by (monad_eq simp: U_shiftr_S_no_abs'_def no_fail_def word_sle_def word_sless_alt) 439lemma "32 <=s n \<Longrightarrow> \<not> no_fail \<top> (U_shiftr_S_no_abs' (x :: word32) (n :: sword32))" 440 by (monad_eq simp: U_shiftr_S_no_abs'_def no_fail_def word_sle_def word_sless_alt) 441lemma "\<lbrace>\<lambda>s. 0 <=s n \<and> n <s 32\<rbrace> U_shiftr_S_no_abs' (x :: word32) (n :: sword32) \<lbrace>\<lambda>r s. r = x >> unat n\<rbrace>!" 442 by (wpsimp simp: U_shiftr_S_no_abs'_def) 443 444subsection \<open>@{text S_shiftr_U}\<close> 445 446lemma "x < 0 \<Longrightarrow> \<not> no_fail \<top> (S_shiftr_U_abs_US' (x :: int) (n :: nat))" 447 by (monad_eq simp: S_shiftr_U_abs_US'_def no_fail_def) 448lemma "n \<ge> 32 \<Longrightarrow> \<not> no_fail \<top> (S_shiftr_U_abs_US' (x :: int) (n :: nat))" 449 by (monad_eq simp: S_shiftr_U_abs_US'_def no_fail_def) 450lemma "\<lbrace>\<lambda>s. n < 32 \<and> 0 \<le> x\<rbrace> S_shiftr_U_abs_US' (x::int) (n::nat) \<lbrace>\<lambda>r s. r = x >> nat n\<rbrace>!" 451 by (wpsimp simp: S_shiftr_U_abs_US'_def) 452 453lemma "x <s 0 \<Longrightarrow> \<not> no_fail \<top> (S_shiftr_U_abs_U' (x :: sword32) (n :: nat))" 454 by (monad_eq simp: S_shiftr_U_abs_U'_def no_fail_def word_sle_def word_sless_alt) 455lemma "n \<ge> 32 \<Longrightarrow> \<not> no_fail \<top> (S_shiftr_U_abs_U' (x :: sword32) (n :: nat))" 456 by (monad_eq simp: S_shiftr_U_abs_U'_def no_fail_def) 457lemma "\<lbrace>\<lambda>s. n < 32 \<and> 0 <=s x\<rbrace> S_shiftr_U_abs_U' (x::sword32) (n::nat) \<lbrace>\<lambda>r s. r = x >> nat n\<rbrace>!" 458 by (wpsimp simp: S_shiftr_U_abs_U'_def) 459 460lemma "x < 0 \<Longrightarrow> \<not> no_fail \<top> (S_shiftr_U_abs_S' (x :: int) (n :: word32))" 461 by (monad_eq simp: S_shiftr_U_abs_S'_def no_fail_def) 462lemma "n \<ge> 32 \<Longrightarrow> \<not> no_fail \<top> (S_shiftr_U_abs_S' (x :: int) (n :: word32))" 463 by (monad_eq simp: S_shiftr_U_abs_S'_def no_fail_def word_le_nat_alt) 464lemma "\<lbrace>\<lambda>s. n < 32 \<and> 0 \<le> x\<rbrace> S_shiftr_U_abs_S' (x::int) (n::word32) \<lbrace>\<lambda>r s. r = x >> unat n\<rbrace>!" 465 by (wpsimp simp: S_shiftr_U_abs_S'_def word_less_nat_alt) 466 467lemma "x <s 0 \<Longrightarrow> \<not> no_fail \<top> (S_shiftr_U_no_abs' (x :: sword32) (n :: word32))" 468 by (monad_eq simp: S_shiftr_U_no_abs'_def no_fail_def word_sle_def word_sless_alt) 469lemma "n \<ge> 32 \<Longrightarrow> \<not> no_fail \<top> (S_shiftr_U_no_abs' (x :: sword32) (n :: word32))" 470 by (monad_eq simp: S_shiftr_U_no_abs'_def no_fail_def word_le_not_less) 471lemma "\<lbrace>\<lambda>s. n < 32 \<and> 0 <=s x\<rbrace> S_shiftr_U_no_abs' (x::sword32) (n::word32) \<lbrace>\<lambda>r s. r = x >> unat n\<rbrace>!" 472 by (wpsimp simp: S_shiftr_U_no_abs'_def) 473 474subsection \<open>@{text S_shiftr_S}\<close> 475 476lemma "x < 0 \<Longrightarrow> \<not> no_fail \<top> (S_shiftr_S_abs_US' (x :: int) (n :: int))" 477 by (monad_eq simp: S_shiftr_S_abs_US'_def no_fail_def) 478lemma "n < 0 \<Longrightarrow> \<not> no_fail \<top> (S_shiftr_S_abs_US' (x :: int) (n :: int))" 479 by (monad_eq simp: S_shiftr_S_abs_US'_def no_fail_def) 480lemma "n \<ge> 32 \<Longrightarrow> \<not> no_fail \<top> (S_shiftr_S_abs_US' (x :: int) (n :: int))" 481 by (monad_eq simp: S_shiftr_S_abs_US'_def no_fail_def) 482lemma "\<lbrace>\<lambda>s. 0 \<le> n \<and> n < 32 \<and> 0 \<le> x\<rbrace> S_shiftr_S_abs_US' (x::int) (n::int) \<lbrace>\<lambda>r s. r = x >> nat n\<rbrace>!" 483 by (wpsimp simp: S_shiftr_S_abs_US'_def) 484 485lemma "x <s 0 \<Longrightarrow> \<not> no_fail \<top> (S_shiftr_S_abs_U' (x :: sword32) (n :: sword32))" 486 by (monad_eq simp: S_shiftr_S_abs_U'_def no_fail_def word_sle_def word_sless_alt) 487lemma "n <s 0 \<Longrightarrow> \<not> no_fail \<top> (S_shiftr_S_abs_U' (x :: sword32) (n :: sword32))" 488 by (monad_eq simp: S_shiftr_S_abs_U'_def no_fail_def word_sle_def word_sless_alt) 489lemma "32 <=s n \<Longrightarrow> \<not> no_fail \<top> (S_shiftr_S_abs_U' (x :: sword32) (n :: sword32))" 490 by (monad_eq simp: S_shiftr_S_abs_U'_def no_fail_def word_sle_def word_sless_alt) 491lemma "\<lbrace>\<lambda>s. 0 <=s n \<and> n <s 32 \<and> 0 <=s x\<rbrace> 492 S_shiftr_S_abs_U' (x::sword32) (n::sword32) 493 \<lbrace>\<lambda>r s. r = x >> unat n\<rbrace>!" 494 by (wpsimp simp: S_shiftr_S_abs_U'_def) 495 496lemma "x < 0 \<Longrightarrow> \<not> no_fail \<top> (S_shiftr_S_abs_S' (x :: int) (n :: int))" 497 by (monad_eq simp: S_shiftr_S_abs_S'_def no_fail_def) 498lemma "n < 0 \<Longrightarrow> \<not> no_fail \<top> (S_shiftr_S_abs_S' (x :: int) (n :: int))" 499 by (monad_eq simp: S_shiftr_S_abs_S'_def no_fail_def) 500lemma "n \<ge> 32 \<Longrightarrow> \<not> no_fail \<top> (S_shiftr_S_abs_S' (x :: int) (n :: int))" 501 by (monad_eq simp: S_shiftr_S_abs_S'_def no_fail_def) 502lemma "\<lbrace>\<lambda>s. 0 \<le> n \<and> n < 32 \<and> 0 \<le> x\<rbrace> 503 S_shiftr_S_abs_S' (x::int) (n::int) 504 \<lbrace>\<lambda>r s. r = x >> nat n\<rbrace>!" 505 by (wpsimp simp: S_shiftr_S_abs_S'_def) 506 507lemma "x <s 0 \<Longrightarrow> \<not> no_fail \<top> (S_shiftr_S_no_abs' (x :: sword32) (n :: sword32))" 508 by (monad_eq simp: S_shiftr_S_no_abs'_def no_fail_def word_sle_def word_sless_alt) 509lemma "n <s 0 \<Longrightarrow> \<not> no_fail \<top> (S_shiftr_S_no_abs' (x :: sword32) (n :: sword32))" 510 by (monad_eq simp: S_shiftr_S_no_abs'_def no_fail_def word_sle_def word_sless_alt) 511lemma "32 <=s n \<Longrightarrow> \<not> no_fail \<top> (S_shiftr_S_no_abs' (x :: sword32) (n :: sword32))" 512 by (monad_eq simp: S_shiftr_S_no_abs'_def no_fail_def word_sle_def word_sless_alt) 513lemma "\<lbrace>\<lambda>s. 0 <=s n \<and> n <s 32 \<and> 0 <=s x\<rbrace> 514 S_shiftr_S_no_abs' (x::sword32) (n::sword32) 515 \<lbrace>\<lambda>r s. r = x >> unat n\<rbrace>!" 516 by (wpsimp simp: S_shiftr_S_no_abs'_def) 517 518end 519 520end 521