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