Attention une mise à jour du service Gitlab va être effectuée le mardi 18 janvier (et non lundi 17 comme annoncé précédemment) entre 18h00 et 18h30. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes.

Commit 070328e5 authored by Sylvain Dailler's avatar Sylvain Dailler
Browse files

Tentatively update isabelle realization for bitvectors

parent 190492a8
theory Why3_BV
imports Why3_Int "~~/src/HOL/Word/Word" "~~/src/HOL/Word/Bit_Comparison"
theory Why3_BV imports Why3_Int "~~/src/HOL/Word/Word" "~~/src/HOL/Word/Bit_Comparison"
begin
abbreviation (input) pow2 :: "int \<Rightarrow> int"
......@@ -153,7 +152,6 @@ qed
lemma uint_pow: "uint ((b::'a::len word) ^ n) = uint b ^ n mod 2 ^ len_of TYPE('a)"
by (induct n) (simp_all add: mod_pos_pos_trivial uint_word_ariths pull_mods)
lemma eq_sub_equiv_aux:
"(\<forall>j. uint i \<le> j \<and> j < uint i + uint n \<longrightarrow>
(0 \<le> j \<and> a !! nat j) = (0 \<le> j \<and> b !! nat j)) =
......@@ -249,6 +247,9 @@ definition size_bv :: "'a::len word" where
type_synonym word8 = "8 word"
abbreviation is_signed_positive :: "word8 \<Rightarrow> bool"
where "is_signed_positive v \<equiv> \<not> (msb v)"
why3_open "bv/BV8.xml"
constants
zeros=zero_class.zero
......@@ -276,11 +277,11 @@ why3_open "bv/BV8.xml"
nth=bv_nth
nth_bv=nth_bv
tqtint=uint
to_int=sint
of_int=of_int
eq_sub_bv=eq_sub_bv
size_bv=size_bv
one=one_class.one
is_signed_positive=is_signed_positive
types
t=word8
......@@ -345,8 +346,6 @@ why3_vc lsl_zeros by simp
why3_vc to_uint_extensionality using assms by simp
why3_vc to_int_extensionality using assms by simp
why3_vc to_uint_bounds
using uint_lt [of v]
by simp_all
......@@ -440,11 +439,55 @@ why3_vc eq_sub_equiv
why3_vc eq_sub_bv_def
by (simp add: eq_sub_bv_defn mask_def)
lemma to_int_positive:
assumes "is_signed_positive v"
shows "to_int v \<ge> 0"
using assms
using to_int_def [of v]
by simp
lemma to_int_negative:
assumes "\<not> (is_signed_positive v)"
shows "to_int v < 0"
using assms
using to_int_def [of v]
by (simp add: to_uint_bounds(2))
lemma to_int_is_signed_positive:
assumes "to_int v = to_int vt"
shows "is_signed_positive v = is_signed_positive vt"
using assms
using to_int_negative [of v]
using to_int_positive [of v]
using to_int_negative [of vt]
using to_int_positive [of vt]
by linarith
why3_vc to_int_extensionality
using assms
using to_int_def [of v]
using to_int_def [of vqt]
using to_int_is_signed_positive [of v vqt]
proof -
have "uint vqt = uint v"
using \<open>to_int v = (if is_signed_positive v then uint v else - (256 - uint v))\<close> \<open>to_int v = to_int vqt \<Longrightarrow> is_signed_positive v = is_signed_positive vqt\<close> \<open>to_int v = to_int vqt\<close> \<open>to_int vqt = (if is_signed_positive vqt then uint vqt else - (256 - uint vqt))\<close> by fastforce
then show ?thesis
using to_uint_extensionality by blast
qed
why3_vc positive_is_ge_zeros
using sge_def [of x 0]
using not_le to_int_def to_int_negative by auto
why3_end
type_synonym word16 = "16 word"
abbreviation is_signed_positive16 :: "word16 \<Rightarrow> bool"
where "is_signed_positive16 v \<equiv> \<not> (msb v)"
why3_open "bv/BV16.xml"
constants
zeros=zero_class.zero
......@@ -472,11 +515,11 @@ why3_open "bv/BV16.xml"
nth=bv_nth
nth_bv=nth_bv
tqtint=uint
to_int=sint
of_int=of_int
eq_sub_bv=eq_sub_bv
size_bv=size_bv
one=one_class.one
is_signed_positive=is_signed_positive16
types
t=word16
......@@ -541,8 +584,6 @@ why3_vc lsl_zeros by simp
why3_vc to_uint_extensionality using assms by simp
why3_vc to_int_extensionality using assms by simp
why3_vc to_uint_bounds
using uint_lt [of v]
by simp_all
......@@ -636,11 +677,56 @@ why3_vc eq_sub_equiv
why3_vc eq_sub_bv_def
by (simp add: eq_sub_bv_defn mask_def)
lemma to_int_positive16:
assumes "is_signed_positive16 v"
shows "to_int v \<ge> 0"
using assms
using to_int_def [of v]
by simp
lemma to_int_negative16:
assumes "\<not> (is_signed_positive16 v)"
shows "to_int v < 0"
using assms
using to_int_def [of v]
by (simp add: to_uint_bounds(2))
lemma to_int_is_signed_positive16:
assumes "to_int v = to_int vt"
shows "is_signed_positive16 v = is_signed_positive16 vt"
using assms
using to_int_negative16 [of v]
using to_int_positive16 [of v]
using to_int_negative16 [of vt]
using to_int_positive16 [of vt]
by linarith
why3_vc to_int_extensionality
using assms
using to_int_def [of v]
using to_int_def [of vqt]
using to_int_is_signed_positive16 [of v vqt]
proof -
have "uint vqt = uint v"
using \<open>to_int v = (if is_signed_positive16 v then uint v else - (65536 - uint v))\<close> \<open>to_int v = to_int vqt \<Longrightarrow> is_signed_positive16 v = is_signed_positive16 vqt\<close> \<open>to_int v = to_int vqt\<close>
\<open>to_int vqt = (if is_signed_positive16 vqt then uint vqt else - (65536 - uint vqt))\<close> by fastforce
then show ?thesis
using to_uint_extensionality by blast
qed
why3_vc positive_is_ge_zeros
using sge_def [of x 0]
using not_le to_int_def to_int_negative16 by auto
why3_end
type_synonym word32 = "32 word"
abbreviation is_signed_positive32 :: "word32 \<Rightarrow> bool"
where "is_signed_positive32 v \<equiv> \<not> (msb v)"
why3_open "bv/BV32.xml"
constants
zeros=zero_class.zero
......@@ -668,11 +754,11 @@ why3_open "bv/BV32.xml"
nth=bv_nth
nth_bv=nth_bv
tqtint=uint
to_int=sint
of_int=of_int
eq_sub_bv=eq_sub_bv
size_bv=size_bv
one=one_class.one
is_signed_positive=is_signed_positive32
types
t=word32
......@@ -737,8 +823,6 @@ why3_vc lsl_zeros by simp
why3_vc to_uint_extensionality using assms by simp
why3_vc to_int_extensionality using assms by simp
why3_vc to_uint_bounds
using uint_lt [of v]
by simp_all
......@@ -832,11 +916,56 @@ why3_vc eq_sub_equiv
why3_vc eq_sub_bv_def
by (simp add: eq_sub_bv_defn mask_def)
lemma to_int_positive32:
assumes "is_signed_positive32 v"
shows "to_int v \<ge> 0"
using assms
using to_int_def [of v]
by simp
lemma to_int_negative32:
assumes "\<not> (is_signed_positive32 v)"
shows "to_int v < 0"
using assms
using to_int_def [of v]
by (simp add: to_uint_bounds(2))
lemma to_int_is_signed_positive32:
assumes "to_int v = to_int vt"
shows "is_signed_positive32 v = is_signed_positive32 vt"
using assms
using to_int_negative32 [of v]
using to_int_positive32 [of v]
using to_int_negative32 [of vt]
using to_int_positive32 [of vt]
by linarith
why3_vc to_int_extensionality
using assms
using to_int_def [of v]
using to_int_def [of vqt]
using to_int_is_signed_positive32 [of v vqt]
proof -
have "uint vqt = uint v"
using \<open>to_int v = (if is_signed_positive32 v then uint v else - (4294967296 - uint v))\<close> \<open>to_int v = to_int vqt \<Longrightarrow> is_signed_positive32 v = is_signed_positive32 vqt\<close> \<open>to_int v = to_int vqt\<close>
\<open>to_int vqt = (if is_signed_positive32 vqt then uint vqt else - (4294967296 - uint vqt))\<close> by fastforce
then show ?thesis
using to_uint_extensionality by blast
qed
why3_vc positive_is_ge_zeros
using sge_def [of x 0]
using not_le to_int_def to_int_negative32 by auto
why3_end
type_synonym word64 = "64 word"
abbreviation is_signed_positive64 :: "word64 \<Rightarrow> bool"
where "is_signed_positive64 v \<equiv> \<not> (msb v)"
why3_open "bv/BV64.xml"
constants
zeros=zero_class.zero
......@@ -864,11 +993,11 @@ why3_open "bv/BV64.xml"
nth=bv_nth
nth_bv=nth_bv
tqtint=uint
to_int=sint
of_int=of_int
eq_sub_bv=eq_sub_bv
size_bv=size_bv
one=one_class.one
is_signed_positive=is_signed_positive64
types
t=word64
......@@ -933,8 +1062,6 @@ why3_vc lsl_zeros by simp
why3_vc to_uint_extensionality using assms by simp
why3_vc to_int_extensionality using assms by simp
why3_vc to_uint_bounds
using uint_lt [of v]
by simp_all
......@@ -1028,6 +1155,49 @@ why3_vc eq_sub_equiv
why3_vc eq_sub_bv_def
by (simp add: eq_sub_bv_defn mask_def)
lemma to_int_positive64:
assumes "is_signed_positive64 v"
shows "to_int v \<ge> 0"
using assms
using to_int_def [of v]
by simp
lemma to_int_negative64:
assumes "\<not> (is_signed_positive64 v)"
shows "to_int v < 0"
using assms
using to_int_def [of v]
by (simp add: to_uint_bounds(2))
lemma to_int_is_signed_positive64:
assumes "to_int v = to_int vt"
shows "is_signed_positive64 v = is_signed_positive64 vt"
using assms
using to_int_negative64 [of v]
using to_int_positive64 [of v]
using to_int_negative64 [of vt]
using to_int_positive64 [of vt]
by linarith
why3_vc to_int_extensionality
using assms
using to_int_def [of v]
using to_int_def [of vqt]
using to_int_is_signed_positive64 [of v vqt]
proof -
have "uint vqt = uint v"
using \<open>to_int v = (if is_signed_positive64 v then uint v else - (18446744073709551616 - uint v))\<close> \<open>to_int v = to_int vqt \<Longrightarrow> is_signed_positive64 v = is_signed_positive64 vqt\<close> \<open>to_int v = to_int vqt\<close>
\<open>to_int vqt = (if is_signed_positive64 vqt then uint vqt else - (18446744073709551616 - uint vqt))\<close> by fastforce
then show ?thesis
using to_uint_extensionality by blast
qed
why3_vc positive_is_ge_zeros
using sge_def [of x 0]
using not_le to_int_def to_int_negative64 by auto
why3_end
......@@ -1120,4 +1290,4 @@ why3_vc toBig_to_uint
why3_end
end
\ No newline at end of file
end
......@@ -252,6 +252,9 @@ definition size_bv :: "'a::len word" where
type_synonym word8 = "8 word"
abbreviation is_signed_positive :: "word8 \<Rightarrow> bool"
where "is_signed_positive v \<equiv> \<not> (msb v)"
why3_open "bv/BV8.xml"
constants
zeros=zero_class.zero
......@@ -279,11 +282,11 @@ why3_open "bv/BV8.xml"
nth=bv_nth
nth_bv=nth_bv
tqtint=uint
to_int=sint
of_int=of_int
eq_sub_bv=eq_sub_bv
size_bv=size_bv
one=one_class.one
is_signed_positive=is_signed_positive
types
t=word8
......@@ -348,12 +351,10 @@ why3_vc lsl_zeros by simp
why3_vc to_uint_extensionality using assms by simp
why3_vc to_int_extensionality using assms by simp
why3_vc to_uint_bounds
using uint_lt [of v]
by simp_all
why3_vc to_uint_of_int
using assms
by (simp add: uint_in_range_def word_of_int uint_word_of_int mod_pos_pos_trivial)
......@@ -443,11 +444,55 @@ why3_vc eq_sub_equiv
why3_vc eq_sub_bv_def
by (simp add: eq_sub_bv_defn mask_def)
lemma to_int_positive:
assumes "is_signed_positive v"
shows "to_int v \<ge> 0"
using assms
using to_int_def [of v]
by simp
lemma to_int_negative:
assumes "\<not> (is_signed_positive v)"
shows "to_int v < 0"
using assms
using to_int_def [of v]
by (simp add: to_uint_bounds(2))
lemma to_int_is_signed_positive:
assumes "to_int v = to_int vt"
shows "is_signed_positive v = is_signed_positive vt"
using assms
using to_int_negative [of v]
using to_int_positive [of v]
using to_int_negative [of vt]
using to_int_positive [of vt]
by linarith
why3_vc to_int_extensionality
using assms
using to_int_def [of v]
using to_int_def [of vqt]
using to_int_is_signed_positive [of v vqt]
proof -
have "uint vqt = uint v"
using \<open>to_int v = (if is_signed_positive v then uint v else - (256 - uint v))\<close> \<open>to_int v = to_int vqt \<Longrightarrow> is_signed_positive v = is_signed_positive vqt\<close> \<open>to_int v = to_int vqt\<close> \<open>to_int vqt = (if is_signed_positive vqt then uint vqt else - (256 - uint vqt))\<close> by fastforce
then show ?thesis
using to_uint_extensionality by blast
qed
why3_vc positive_is_ge_zeros
using sge_def [of x 0]
using not_le to_int_def to_int_negative by auto
why3_end
type_synonym word16 = "16 word"
abbreviation is_signed_positive16 :: "word16 \<Rightarrow> bool"
where "is_signed_positive16 v \<equiv> \<not> (msb v)"
why3_open "bv/BV16.xml"
constants
zeros=zero_class.zero
......@@ -475,11 +520,11 @@ why3_open "bv/BV16.xml"
nth=bv_nth
nth_bv=nth_bv
tqtint=uint
to_int=sint
of_int=of_int
eq_sub_bv=eq_sub_bv
size_bv=size_bv
one=one_class.one
is_signed_positive=is_signed_positive16
types
t=word16
......@@ -544,8 +589,6 @@ why3_vc lsl_zeros by simp
why3_vc to_uint_extensionality using assms by simp
why3_vc to_int_extensionality using assms by simp
why3_vc to_uint_bounds
using uint_lt [of v]
by simp_all
......@@ -639,11 +682,56 @@ why3_vc eq_sub_equiv
why3_vc eq_sub_bv_def
by (simp add: eq_sub_bv_defn mask_def)
lemma to_int_positive16:
assumes "is_signed_positive16 v"
shows "to_int v \<ge> 0"
using assms
using to_int_def [of v]
by simp
lemma to_int_negative16:
assumes "\<not> (is_signed_positive16 v)"
shows "to_int v < 0"
using assms
using to_int_def [of v]
by (simp add: to_uint_bounds(2))
lemma to_int_is_signed_positive16:
assumes "to_int v = to_int vt"
shows "is_signed_positive16 v = is_signed_positive16 vt"
using assms
using to_int_negative16 [of v]
using to_int_positive16 [of v]
using to_int_negative16 [of vt]
using to_int_positive16 [of vt]
by linarith
why3_vc to_int_extensionality
using assms
using to_int_def [of v]
using to_int_def [of vqt]
using to_int_is_signed_positive16 [of v vqt]
proof -
have "uint vqt = uint v"
using \<open>to_int v = (if is_signed_positive16 v then uint v else - (65536 - uint v))\<close> \<open>to_int v = to_int vqt \<Longrightarrow> is_signed_positive16 v = is_signed_positive16 vqt\<close> \<open>to_int v = to_int vqt\<close>
\<open>to_int vqt = (if is_signed_positive16 vqt then uint vqt else - (65536 - uint vqt))\<close> by fastforce
then show ?thesis
using to_uint_extensionality by blast
qed
why3_vc positive_is_ge_zeros
using sge_def [of x 0]
using not_le to_int_def to_int_negative16 by auto
why3_end
type_synonym word32 = "32 word"
abbreviation is_signed_positive32 :: "word32 \<Rightarrow> bool"
where "is_signed_positive32 v \<equiv> \<not> (msb v)"
why3_open "bv/BV32.xml"
constants
zeros=zero_class.zero
......@@ -671,11 +759,11 @@ why3_open "bv/BV32.xml"
nth=bv_nth
nth_bv=nth_bv
tqtint=uint
to_int=sint
of_int=of_int
eq_sub_bv=eq_sub_bv
size_bv=size_bv
one=one_class.one
is_signed_positive=is_signed_positive32
types
t=word32
......@@ -740,8 +828,6 @@ why3_vc lsl_zeros by simp
why3_vc to_uint_extensionality using assms by simp
why3_vc to_int_extensionality using assms by simp
why3_vc to_uint_bounds
using uint_lt [of v]
by simp_all
......@@ -835,11 +921,56 @@ why3_vc eq_sub_equiv
why3_vc eq_sub_bv_def
by (simp add: eq_sub_bv_defn mask_def)
lemma to_int_positive32:
assumes "is_signed_positive32 v"
shows "to_int v \<ge> 0"
using assms
using to_int_def [of v]
by simp
lemma to_int_negative32:
assumes "\<not> (is_signed_positive32 v)"
shows "to_int v < 0"
using assms
using to_int_def [of v]
by (simp add: to_uint_bounds(2))
lemma to_int_is_signed_positive32:
assumes "to_int v = to_int vt"
shows "is_signed_positive32 v = is_signed_positive32 vt"
using assms
using to_int_negative32 [of v]
using to_int_positive32 [of v]
using to_int_negative32 [of vt]
using to_int_positive32 [of vt]
by linarith
why3_vc to_int_extensionality
using assms
using to_int_def [of v]
using to_int_def [of vqt]
using to_int_is_signed_positive32 [of v vqt]
proof -
have "uint vqt = uint v"
using \<open>to_int v = (if is_signed_positive32 v then uint v else - (4294967296 - uint v))\<close> \<open>to_int v = to_int vqt \<Longrightarrow> is_signed_positive32 v = is_signed_positive32 vqt\<close> \<open>to_int v = to_int vqt\<close>
\<open>to_int vqt = (if is_signed_positive32 vqt then uint vqt else - (4294967296 - uint vqt))\<close> by fastforce
then show ?thesis
using to_uint_extensionality by blast
qed
why3_vc positive_is_ge_zeros
using sge_def [of x 0]
using not_le to_int_def to_int_negative32 by auto
why3_end
type_synonym word64 = "64 word"
abbreviation is_signed_positive64 :: "word64 \<Rightarrow> bool"
where "is_signed_positive64 v \<equiv> \<not> (msb v)"
why3_open "bv/BV64.xml"
constants
zeros=zero_class.zero
......@@ -867,11 +998,11 @@ why3_open "bv/BV64.xml"
nth=bv_nth
nth_bv=nth_bv
tqtint=uint
to_int=sint
of_int=of_int
eq_sub_bv=eq_sub_bv
size_bv=size_bv
one=one_class.one
is_signed_positive=is_signed_positive64
types
t=word64
......@@ -936,8 +1067,6 @@ why3_vc lsl_zeros by simp
why3_vc to_uint_extensionality using assms by simp
why3_vc to_int_extensionality using assms by simp
why3_vc to_uint_bounds
using uint_lt [of v]
by simp_all
......@@ -1031,6 +1160,49 @@ why3_vc eq_sub_equiv
why3_vc eq_sub_bv_def
by (simp add: eq_sub_bv_defn mask_def)
lemma to_int_positive64:
assumes "is_signed_positive64 v"
shows "to_int v \<ge> 0"
using assms
using to_int_def [of v]
by simp
lemma to_int_negative64:
assumes "\<not> (is_signed_positive64 v)"
shows "to_int v < 0"
using assms
using to_int_def [of v]
by (simp add: to_uint_bounds(2))
lemma to_int_is_signed_positive64:
assumes "to_int v = to_int vt"
shows "is_signed_positive64 v = is_signed_positive64 vt"
using assms
using to_int_negative64 [of v]
using to_int_positive64 [of v]
using to_int_negative64 [of vt]
using to_int_positive64 [of vt]
by linarith
why3_vc to_int_extensionality
using assms
using to_int_def [of v]
using to_int_def [of vqt]
using to_int_is_signed_positive64 [of v vqt]
proof -
have "uint vqt = uint v"
using \<open>to_int v = (if is_signed_positive64 v then uint v else - (18446744073709551616 - uint v))\<close> \<open>to_int v = to_int vqt \<Longrightarrow> is_signed_positive64 v = is_signed_positive64 vqt\<close> \<open>to_int v = to_int vqt\<close>
\<open>to_int vqt = (if is_signed_positive64 vqt then uint vqt else - (18446744073709551616 - uint vqt))\<close> by fastforce
then show ?thesis
using to_uint_extensionality by blast
qed
why3_vc positive_is_ge_zeros
using sge_def [of x 0]
using not_le to_int_def to_int_negative64 by auto
why3_end
......
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
Markdown is supported
0% or .