Compare commits
3 Commits
51f3d8fe82
...
e59d6ad091
Author | SHA1 | Date |
---|---|---|
Achim D. Brucker | e59d6ad091 | |
Achim D. Brucker | 99c79b50df | |
Achim D. Brucker | c71c31d163 |
2
ROOTS
2
ROOTS
|
@ -11,7 +11,7 @@ lib/Basics
|
|||
lib/Eisbach_Tools
|
||||
lib/ML_Utils
|
||||
lib/Monads
|
||||
lib/Word_Lib
|
||||
lib/Word_Lib_l4v
|
||||
lib/sep_algebra
|
||||
lib/EVTutorial
|
||||
docs
|
||||
|
|
|
@ -6,7 +6,7 @@
|
|||
*)
|
||||
|
||||
theory CLib
|
||||
imports Word_Lib.Many_More
|
||||
imports Word_Lib_l4v.Many_More
|
||||
begin
|
||||
|
||||
lemma nat_diff_less:
|
||||
|
|
|
@ -9,7 +9,7 @@ This session contains basic library theories that are needed in other sessions
|
|||
of this repository, such as [Monads] or [CParser], but that we do not want to
|
||||
put into these sessions to avoid circular session dependencies.
|
||||
|
||||
Dependencies on `Word_Lib` and the Isabelle distribution (e.g. `HOL-Libary`) are
|
||||
Dependencies on `Word_Lib_l4v` and the Isabelle distribution (e.g. `HOL-Libary`) are
|
||||
fine, but avoid introducing any further session dependencies.
|
||||
|
||||
[Monads]: ../Monads/
|
||||
|
|
|
@ -6,7 +6,7 @@
|
|||
|
||||
chapter Lib
|
||||
|
||||
session Basics (lib) = Word_Lib +
|
||||
session Basics (lib) = Word_Lib_l4v +
|
||||
|
||||
theories
|
||||
CLib
|
|
@ -22,7 +22,7 @@ imports
|
|||
Monads.Monad_Lib
|
||||
Basics.CLib
|
||||
NICTATools
|
||||
"Word_Lib.WordSetup"
|
||||
"Word_Lib_l4v.WordSetup"
|
||||
begin
|
||||
|
||||
(* FIXME: eliminate *)
|
||||
|
|
|
@ -5,7 +5,7 @@
|
|||
*)
|
||||
|
||||
theory More_Numeral_Type
|
||||
imports "Word_Lib.WordSetup"
|
||||
imports "Word_Lib_l4v.WordSetup"
|
||||
begin
|
||||
|
||||
(* This theory provides additional setup for numeral types, which should probably go into
|
||||
|
|
|
@ -18,7 +18,7 @@ imports
|
|||
Oblivious
|
||||
Injection_Handler
|
||||
Monads.Nondet_While_Loop_Rules_Completeness
|
||||
"Word_Lib.Distinct_Prop" (* for distinct_tuple_helper *)
|
||||
"Word_Lib_l4v.Distinct_Prop" (* for distinct_tuple_helper *)
|
||||
Monads.Reader_Option_VCG
|
||||
begin
|
||||
|
||||
|
|
2
lib/ROOT
2
lib/ROOT
|
@ -6,7 +6,7 @@
|
|||
|
||||
chapter Lib
|
||||
|
||||
session Lib (lib) = Word_Lib +
|
||||
session Lib (lib) = Word_Lib_l4v +
|
||||
sessions
|
||||
"HOL-Library"
|
||||
Basics
|
||||
|
|
|
@ -5,7 +5,7 @@
|
|||
*)
|
||||
|
||||
|
||||
theory WordSetup (* part of non-AFP Word_Lib *)
|
||||
theory WordSetup (* part of non-AFP Word_Lib_l4v *)
|
||||
imports
|
||||
Word_Lemmas_64_Internal
|
||||
Distinct_Prop
|
|
@ -5,7 +5,7 @@
|
|||
*)
|
||||
|
||||
|
||||
theory WordSetup (* part of non-AFP Word_Lib *)
|
||||
theory WordSetup (* part of non-AFP Word_Lib_l4v *)
|
||||
imports
|
||||
Word_Lemmas_32_Internal
|
||||
Distinct_Prop
|
|
@ -5,7 +5,7 @@
|
|||
*)
|
||||
|
||||
|
||||
theory WordSetup (* part of non-AFP Word_Lib *)
|
||||
theory WordSetup (* part of non-AFP Word_Lib_l4v *)
|
||||
imports
|
||||
Word_Lemmas_32_Internal
|
||||
Distinct_Prop
|
|
@ -8,10 +8,10 @@ section \<open>Bitwise Operations on integers\<close>
|
|||
|
||||
theory Bits_Int
|
||||
imports
|
||||
"Word_Lib.Most_significant_bit"
|
||||
"Word_Lib.Least_significant_bit"
|
||||
"Word_Lib.Generic_set_bit"
|
||||
"Word_Lib.Bit_Comprehension"
|
||||
"Word_Lib_l4v.Most_significant_bit"
|
||||
"Word_Lib_l4v.Least_significant_bit"
|
||||
"Word_Lib_l4v.Generic_set_bit"
|
||||
"Word_Lib_l4v.Bit_Comprehension"
|
||||
begin
|
||||
|
||||
subsection \<open>Implicit bit representation of \<^typ>\<open>int\<close>\<close>
|
|
@ -6,7 +6,7 @@
|
|||
|
||||
section "Distinct Proposition"
|
||||
|
||||
theory Distinct_Prop (* part of non-AFP Word_Lib *)
|
||||
theory Distinct_Prop (* part of non-AFP Word_Lib_l4v *)
|
||||
imports
|
||||
Many_More
|
||||
"HOL-Library.Prefix_Order"
|
|
@ -198,35 +198,35 @@ text \<open>
|
|||
|
||||
\<^descr>[Syntax]
|
||||
|
||||
\<^descr>[\<^theory>\<open>Word_Lib.Syntax_Bundles\<close>]
|
||||
\<^descr>[\<^theory>\<open>Word_Lib_l4v.Syntax_Bundles\<close>]
|
||||
Bundles to provide alternative syntax for various bit operations.
|
||||
|
||||
\<^descr>[\<^theory>\<open>Word_Lib.Hex_Words\<close>]
|
||||
\<^descr>[\<^theory>\<open>Word_Lib_l4v.Hex_Words\<close>]
|
||||
Printing word numerals as hexadecimal numerals.
|
||||
|
||||
\<^descr>[\<^theory>\<open>Word_Lib.Type_Syntax\<close>]
|
||||
\<^descr>[\<^theory>\<open>Word_Lib_l4v.Type_Syntax\<close>]
|
||||
Pretty type-sensitive syntax for cast operations.
|
||||
|
||||
\<^descr>[\<^theory>\<open>Word_Lib.Word_Syntax\<close>]
|
||||
\<^descr>[\<^theory>\<open>Word_Lib_l4v.Word_Syntax\<close>]
|
||||
Specific ASCII syntax for prominent bit operations on word.
|
||||
|
||||
\<^descr>[Proof tools]
|
||||
|
||||
\<^descr>[\<^theory>\<open>Word_Lib.Norm_Words\<close>]
|
||||
\<^descr>[\<^theory>\<open>Word_Lib_l4v.Norm_Words\<close>]
|
||||
Rewriting word numerals to normal forms.
|
||||
|
||||
\<^descr>[\<^theory>\<open>Word_Lib.Bitwise\<close>]
|
||||
\<^descr>[\<^theory>\<open>Word_Lib_l4v.Bitwise\<close>]
|
||||
Method @{method word_bitwise} decomposes word equalities and inequalities into bit propositions.
|
||||
|
||||
\<^descr>[\<^theory>\<open>Word_Lib.Bitwise_Signed\<close>]
|
||||
\<^descr>[\<^theory>\<open>Word_Lib_l4v.Bitwise_Signed\<close>]
|
||||
Method @{method word_bitwise_signed} decomposes word equalities and inequalities into bit propositions.
|
||||
|
||||
\<^descr>[\<^theory>\<open>Word_Lib.Word_EqI\<close>]
|
||||
\<^descr>[\<^theory>\<open>Word_Lib_l4v.Word_EqI\<close>]
|
||||
Method @{method word_eqI_solve} decomposes word equalities and inequalities into bit propositions.
|
||||
|
||||
\<^descr>[Operations]
|
||||
|
||||
\<^descr>[\<^theory>\<open>Word_Lib.Signed_Division_Word\<close>]
|
||||
\<^descr>[\<^theory>\<open>Word_Lib_l4v.Signed_Division_Word\<close>]
|
||||
|
||||
Signed division on word:
|
||||
|
||||
|
@ -234,16 +234,16 @@ text \<open>
|
|||
|
||||
\<^item> @{term [source] \<open>(smod) :: 'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>}
|
||||
|
||||
\<^descr>[\<^theory>\<open>Word_Lib.Aligned\<close>] \
|
||||
\<^descr>[\<^theory>\<open>Word_Lib_l4v.Aligned\<close>] \
|
||||
|
||||
\<^item> @{thm [mode=iff] is_aligned_iff_udvd [no_vars]}
|
||||
|
||||
\<^descr>[\<^theory>\<open>Word_Lib.Least_significant_bit\<close>]
|
||||
\<^descr>[\<^theory>\<open>Word_Lib_l4v.Least_significant_bit\<close>]
|
||||
|
||||
The least significant bit as an alias:
|
||||
@{thm [mode=iff] lsb_odd [where ?'a = int, no_vars]}
|
||||
|
||||
\<^descr>[\<^theory>\<open>Word_Lib.Most_significant_bit\<close>]
|
||||
\<^descr>[\<^theory>\<open>Word_Lib_l4v.Most_significant_bit\<close>]
|
||||
|
||||
The most significant bit:
|
||||
|
||||
|
@ -255,7 +255,7 @@ text \<open>
|
|||
|
||||
\<^item> @{thm [mode=iff] msb_word_iff_bit [no_vars]}
|
||||
|
||||
\<^descr>[\<^theory>\<open>Word_Lib.Bit_Shifts_Infix_Syntax\<close>]
|
||||
\<^descr>[\<^theory>\<open>Word_Lib_l4v.Bit_Shifts_Infix_Syntax\<close>]
|
||||
|
||||
Bit shifts decorated with infix syntax:
|
||||
|
||||
|
@ -265,57 +265,57 @@ text \<open>
|
|||
|
||||
\<^item> @{thm Bit_Shifts_Infix_Syntax.sshiftr_def [no_vars]}
|
||||
|
||||
\<^descr>[\<^theory>\<open>Word_Lib.Next_and_Prev\<close>] \
|
||||
\<^descr>[\<^theory>\<open>Word_Lib_l4v.Next_and_Prev\<close>] \
|
||||
|
||||
\<^item> @{thm word_next_unfold [no_vars]}
|
||||
|
||||
\<^item> @{thm word_prev_unfold [no_vars]}
|
||||
|
||||
\<^descr>[\<^theory>\<open>Word_Lib.Enumeration_Word\<close>]
|
||||
\<^descr>[\<^theory>\<open>Word_Lib_l4v.Enumeration_Word\<close>]
|
||||
|
||||
More on explicit enumeration of word types.
|
||||
|
||||
\<^descr>[\<^theory>\<open>Word_Lib.More_Word_Operations\<close>]
|
||||
\<^descr>[\<^theory>\<open>Word_Lib_l4v.More_Word_Operations\<close>]
|
||||
|
||||
Even more operations on word.
|
||||
|
||||
\<^descr>[Types]
|
||||
|
||||
\<^descr>[\<^theory>\<open>Word_Lib.Signed_Words\<close>]
|
||||
\<^descr>[\<^theory>\<open>Word_Lib_l4v.Signed_Words\<close>]
|
||||
|
||||
Formal tagging of word types with a \<^text>\<open>signed\<close> marker.
|
||||
|
||||
\<^descr>[Lemmas]
|
||||
|
||||
\<^descr>[\<^theory>\<open>Word_Lib.More_Word\<close>]
|
||||
\<^descr>[\<^theory>\<open>Word_Lib_l4v.More_Word\<close>]
|
||||
|
||||
More lemmas on words.
|
||||
|
||||
\<^descr>[\<^theory>\<open>Word_Lib.Word_Lemmas\<close>]
|
||||
\<^descr>[\<^theory>\<open>Word_Lib_l4v.Word_Lemmas\<close>]
|
||||
|
||||
More lemmas on words, covering many other theories mentioned here.
|
||||
|
||||
\<^descr>[Words of popular lengths].
|
||||
|
||||
\<^descr>[\<^theory>\<open>Word_Lib.Word_8\<close>]
|
||||
\<^descr>[\<^theory>\<open>Word_Lib_l4v.Word_8\<close>]
|
||||
|
||||
for 8-bit words.
|
||||
|
||||
\<^descr>[\<^theory>\<open>Word_Lib.Word_16\<close>]
|
||||
\<^descr>[\<^theory>\<open>Word_Lib_l4v.Word_16\<close>]
|
||||
|
||||
for 16-bit words.
|
||||
|
||||
\<^descr>[\<^theory>\<open>Word_Lib.Word_32\<close>]
|
||||
\<^descr>[\<^theory>\<open>Word_Lib_l4v.Word_32\<close>]
|
||||
|
||||
for 32-bit words.
|
||||
|
||||
\<^descr>[\<^theory>\<open>Word_Lib.Word_64\<close>]
|
||||
\<^descr>[\<^theory>\<open>Word_Lib_l4v.Word_64\<close>]
|
||||
|
||||
for 64-bit words. This theory is not part of \<^text>\<open>Word_Lib_Sumo\<close>, because it shadows
|
||||
names from \<^theory>\<open>Word_Lib.Word_32\<close>. They can be used together, but then will have
|
||||
names from \<^theory>\<open>Word_Lib_l4v.Word_32\<close>. They can be used together, but then will have
|
||||
to use qualified names in applications.
|
||||
|
||||
\<^descr>[\<^theory>\<open>Word_Lib.Machine_Word_32\<close> and \<^theory>\<open>Word_Lib.Machine_Word_64\<close>]
|
||||
\<^descr>[\<^theory>\<open>Word_Lib_l4v.Machine_Word_32\<close> and \<^theory>\<open>Word_Lib_l4v.Machine_Word_64\<close>]
|
||||
|
||||
provide lemmas for 32-bit words and 64-bit words under the same name,
|
||||
which can help to organize applications relying on some form
|
||||
|
@ -343,36 +343,36 @@ text \<open>
|
|||
from those theories. However theorem coverage may still
|
||||
be terse in some cases.
|
||||
|
||||
\<^descr>[\<^theory>\<open>Word_Lib.Word_Lib_Sumo\<close>]
|
||||
\<^descr>[\<^theory>\<open>Word_Lib_l4v.Word_Lib_Sumo\<close>]
|
||||
|
||||
An entry point importing any relevant theory in that session. Intended
|
||||
for backward compatibility: start importing this theory when
|
||||
migrating applications to Isabelle2021, and later sort out
|
||||
what you really need. You may need to include
|
||||
\<^theory>\<open>Word_Lib.Word_64\<close> separately.
|
||||
\<^theory>\<open>Word_Lib_l4v.Word_64\<close> separately.
|
||||
|
||||
\<^descr>[\<^theory>\<open>Word_Lib.Generic_set_bit\<close>]
|
||||
\<^descr>[\<^theory>\<open>Word_Lib_l4v.Generic_set_bit\<close>]
|
||||
|
||||
Kind of an alias: @{thm set_bit_eq [no_vars]}
|
||||
|
||||
\<^descr>[\<^theory>\<open>Word_Lib.Typedef_Morphisms\<close>]
|
||||
\<^descr>[\<^theory>\<open>Word_Lib_l4v.Typedef_Morphisms\<close>]
|
||||
|
||||
A low-level extension to HOL typedef providing
|
||||
conversions along type morphisms. The @{method transfer} method
|
||||
seems to be sufficient for most applications though.
|
||||
|
||||
\<^descr>[\<^theory>\<open>Word_Lib.Bit_Comprehension\<close>]
|
||||
\<^descr>[\<^theory>\<open>Word_Lib_l4v.Bit_Comprehension\<close>]
|
||||
|
||||
Comprehension syntax for bit values over predicates
|
||||
\<^typ>\<open>nat \<Rightarrow> bool\<close>, for \<^typ>\<open>'a::len word\<close>; straightforward
|
||||
alternatives exist.
|
||||
|
||||
\<^descr>[\<^theory>\<open>Word_Lib.Bit_Comprehension_Int\<close>]
|
||||
\<^descr>[\<^theory>\<open>Word_Lib_l4v.Bit_Comprehension_Int\<close>]
|
||||
|
||||
Comprehension syntax for bit values over predicates
|
||||
\<^typ>\<open>nat \<Rightarrow> bool\<close>, for \<^typ>\<open>int\<close>; inherently non-computational.
|
||||
|
||||
\<^descr>[\<^theory>\<open>Word_Lib.Reversed_Bit_Lists\<close>]
|
||||
\<^descr>[\<^theory>\<open>Word_Lib_l4v.Reversed_Bit_Lists\<close>]
|
||||
|
||||
Representation of bit values as explicit list in
|
||||
\<^emph>\<open>reversed\<close> order.
|
||||
|
@ -383,11 +383,11 @@ text \<open>
|
|||
|
||||
@{thm [display] horner_sum_bit_eq_take_bit [where ?'a = int, no_vars]}
|
||||
|
||||
\<^descr>[\<^theory>\<open>Word_Lib.Many_More\<close>]
|
||||
\<^descr>[\<^theory>\<open>Word_Lib_l4v.Many_More\<close>]
|
||||
|
||||
Collection of operations and theorems which are kept for backward
|
||||
compatibility and not used in other theories in session \<^text>\<open>Word_Lib\<close>.
|
||||
They are used in applications of \<^text>\<open>Word_Lib\<close>, but should be migrated to there.
|
||||
compatibility and not used in other theories in session \<^text>\<open>Word_Lib_l4v\<close>.
|
||||
They are used in applications of \<^text>\<open>Word_Lib_l4v\<close>, but should be migrated to there.
|
||||
\<close>
|
||||
|
||||
section \<open>Changelog\<close>
|
||||
|
@ -395,31 +395,31 @@ section \<open>Changelog\<close>
|
|||
text \<open>
|
||||
\<^descr>[Changes since AFP 2022] ~
|
||||
|
||||
\<^item> Theory \<^text>\<open>Word_Lib.Ancient_Numeral\<close> has been removed from session.
|
||||
\<^item> Theory \<^text>\<open>Word_Lib_l4v.Ancient_Numeral\<close> has been removed from session.
|
||||
|
||||
\<^item> Bit comprehension syntax for \<^typ>\<open>int\<close> moved to separate theory
|
||||
\<^theory>\<open>Word_Lib.Bit_Comprehension_Int\<close>.
|
||||
\<^theory>\<open>Word_Lib_l4v.Bit_Comprehension_Int\<close>.
|
||||
|
||||
\<^descr>[Changes since AFP 2021] ~
|
||||
|
||||
\<^item> Theory \<^text>\<open>Word_Lib.Ancient_Numeral\<close> is not part of \<^theory>\<open>Word_Lib.Word_Lib_Sumo\<close>
|
||||
\<^item> Theory \<^text>\<open>Word_Lib_l4v.Ancient_Numeral\<close> is not part of \<^theory>\<open>Word_Lib_l4v.Word_Lib_Sumo\<close>
|
||||
any longer.
|
||||
|
||||
\<^item> Infix syntax for \<^term>\<open>(AND)\<close>, \<^term>\<open>(OR)\<close>, \<^term>\<open>(XOR)\<close> organized in
|
||||
syntax bundle \<^bundle>\<open>bit_operations_syntax\<close>.
|
||||
|
||||
\<^item> Abbreviation \<^abbrev>\<open>max_word\<close> moved from distribution into theory
|
||||
\<^theory>\<open>Word_Lib.Legacy_Aliases\<close>.
|
||||
\<^theory>\<open>Word_Lib_l4v.Legacy_Aliases\<close>.
|
||||
|
||||
\<^item> Operation \<^const>\<open>test_bit\<close> replaced by input abbreviation \<^abbrev>\<open>test_bit\<close>.
|
||||
|
||||
\<^item> Abbreviations \<^abbrev>\<open>bin_nth\<close>, \<^abbrev>\<open>bin_last\<close>, \<^abbrev>\<open>bin_rest\<close>,
|
||||
\<^abbrev>\<open>bintrunc\<close>, \<^abbrev>\<open>sbintrunc\<close>, \<^abbrev>\<open>norm_sint\<close>,
|
||||
\<^abbrev>\<open>bin_cat\<close> moved into theory \<^theory>\<open>Word_Lib.Legacy_Aliases\<close>.
|
||||
\<^abbrev>\<open>bin_cat\<close> moved into theory \<^theory>\<open>Word_Lib_l4v.Legacy_Aliases\<close>.
|
||||
|
||||
\<^item> Operations \<^abbrev>\<open>bshiftr1\<close>,
|
||||
\<^abbrev>\<open>setBit\<close>, \<^abbrev>\<open>clearBit\<close> moved from distribution into theory
|
||||
\<^theory>\<open>Word_Lib.Legacy_Aliases\<close> and replaced by input abbreviations.
|
||||
\<^theory>\<open>Word_Lib_l4v.Legacy_Aliases\<close> and replaced by input abbreviations.
|
||||
|
||||
\<^item> Operations \<^const>\<open>shiftl1\<close>, \<^const>\<open>shiftr1\<close>, \<^const>\<open>sshiftr1\<close>
|
||||
moved here from distribution.
|
|
@ -5,7 +5,7 @@
|
|||
*)
|
||||
|
||||
|
||||
theory WordSetup (* part of non-AFP Word_Lib *)
|
||||
theory WordSetup (* part of non-AFP Word_Lib_l4v *)
|
||||
imports
|
||||
Word_Lemmas_64_Internal
|
||||
Distinct_Prop
|
|
@ -6,8 +6,8 @@
|
|||
|
||||
chapter Lib
|
||||
|
||||
session Word_Lib (lib) = HOL +
|
||||
options [timeout = 300, document=pdf]
|
||||
session Word_Lib_l4v (lib) = HOL +
|
||||
options [timeout = 900, document=pdf]
|
||||
sessions
|
||||
"HOL-Library"
|
||||
"HOL-Eisbach"
|
|
@ -48,12 +48,12 @@ lemma signed_ge_zero_scast_eq_ucast:
|
|||
"0 <=s x \<Longrightarrow> scast x = ucast x"
|
||||
by (simp add: scast_eq_ucast word_sle_msb_le)
|
||||
|
||||
(* FIXME: move out of Word_Lib *)
|
||||
(* FIXME: move out of Word_Lib_l4v *)
|
||||
lemma disjCI2:
|
||||
"(\<not> P \<Longrightarrow> Q) \<Longrightarrow> P \<or> Q"
|
||||
by blast
|
||||
|
||||
(* FIXME: move out of Word_Lib *)
|
||||
(* FIXME: move out of Word_Lib_l4v *)
|
||||
lemma nat_diff_diff_le_lhs:
|
||||
"a + c - b \<le> d \<Longrightarrow> a - (b - c) \<le> (d :: nat)"
|
||||
by arith
|
||||
|
@ -664,7 +664,7 @@ lemma FF_eq_minus_1:
|
|||
lemmas shiftl_t2n' = shiftl_eq_mult[where x="w::'a::len word" for w]
|
||||
|
||||
|
||||
(* candidates for moving to AFP Word_Lib: *)
|
||||
(* candidates for moving to AFP Word_Lib_l4v: *)
|
||||
|
||||
lemma word_mask_shift_eqI:
|
||||
"\<lbrakk> x && mask n = y && mask n; x >> n = y >> n \<rbrakk> \<Longrightarrow> x = y"
|
|
@ -5,7 +5,7 @@
|
|||
*)
|
||||
|
||||
|
||||
theory WordSetup (* part of non-AFP Word_Lib *)
|
||||
theory WordSetup (* part of non-AFP Word_Lib_l4v *)
|
||||
imports
|
||||
Word_Lemmas_64_Internal
|
||||
Distinct_Prop
|
|
@ -6,7 +6,7 @@
|
|||
|
||||
chapter Lib
|
||||
|
||||
session Sep_Algebra (lib) = Word_Lib +
|
||||
session Sep_Algebra (lib) = Word_Lib_l4v +
|
||||
sessions
|
||||
"HOL-Eisbach"
|
||||
"HOL-Hoare"
|
||||
|
|
|
@ -53,7 +53,7 @@
|
|||
|
||||
<!-- Build Isabelle and common theories (Pure, HOL, Word). -->
|
||||
<sequence>
|
||||
<test name="isabelle" cwd="../.." cpu-timeout="3600">isabelle/bin/isabelle build -d . -vb Word_Lib</test>
|
||||
<test name="isabelle" cwd="../.." cpu-timeout="3600">isabelle/bin/isabelle build -d . -vb Word_Lib_l4v</test>
|
||||
</sequence>
|
||||
|
||||
<!-- Ensure that all of our XML files are strictly correct. -->
|
||||
|
|
|
@ -250,7 +250,7 @@ lemma is_aligned_ptrFromPAddr_pageBitsForSize:
|
|||
"is_aligned p (pageBitsForSize sz) \<Longrightarrow> is_aligned (ptrFromPAddr p) (pageBitsForSize sz)"
|
||||
by (cases sz ; simp add: is_aligned_ptrFromPAddr_n pageBits_def)
|
||||
|
||||
(* FIXME: generalise, move to Word_Lib, and/or rewrite using
|
||||
(* FIXME: generalise, move to Word_Lib_l4v, and/or rewrite using
|
||||
'leq_high_bits_shiftr_low_bits_leq_bits' *)
|
||||
lemma le_mask_asid_bits_helper:
|
||||
"x \<le> 2 ^ asid_high_bits - 1 \<Longrightarrow> (x::word32) << asid_low_bits \<le> mask asid_bits"
|
||||
|
@ -271,7 +271,7 @@ lemma is_aligned_pageBitsForSize_minimum:
|
|||
apply (erule is_aligned_weaken, simp)+
|
||||
done
|
||||
|
||||
(* FIXME: generalise, move to Word_Lib, and/or rewrite using 'shift_then_mask_eq_shift_low_bits' *)
|
||||
(* FIXME: generalise, move to Word_Lib_l4v, and/or rewrite using 'shift_then_mask_eq_shift_low_bits' *)
|
||||
lemma shiftr_asid_low_bits_mask_asid_high_bits:
|
||||
"(asid :: word32) \<le> mask asid_bits
|
||||
\<Longrightarrow> (asid >> asid_low_bits) && mask asid_high_bits = asid >> asid_low_bits"
|
||||
|
@ -288,7 +288,7 @@ lemma ucast_asid_high_bits_is_shift:
|
|||
unfolding asid_bits_def asid_low_bits_def asid_high_bits_of_def
|
||||
by (rule ucast_ucast_eq_mask_shift, simp)
|
||||
|
||||
(* FIXME: generalise, move to Word_Lib, and/or rewrite using 'leq_low_bits_iff_zero' *)
|
||||
(* FIXME: generalise, move to Word_Lib_l4v, and/or rewrite using 'leq_low_bits_iff_zero' *)
|
||||
lemma shiftr_asid_low_bits_mask_eq_0:
|
||||
"\<lbrakk> (asid :: word32) \<le> mask asid_bits; asid >> asid_low_bits = 0 \<rbrakk>
|
||||
\<Longrightarrow> (asid && mask asid_low_bits = 0) = (asid = 0)"
|
||||
|
|
|
@ -174,7 +174,7 @@ lemma to_bool_if:
|
|||
"(if w \<noteq> 0 then 1 else 0) = (if to_bool w then 1 else 0)"
|
||||
by (auto simp: to_bool_def)
|
||||
|
||||
(* FIXME: move to Word_Lib *)
|
||||
(* FIXME: move to Word_Lib_l4v *)
|
||||
lemma word_upcast_shiftr:
|
||||
assumes "LENGTH('a::len) \<le> LENGTH('b::len)"
|
||||
shows "UCAST('a \<rightarrow> 'b) (w >> n) = UCAST('a \<rightarrow> 'b) w >> n"
|
||||
|
@ -187,12 +187,12 @@ lemma word_upcast_neg_msb:
|
|||
unfolding ucast_def msb_word_of_int
|
||||
by clarsimp (metis Suc_pred bit_imp_le_length lens_gt_0(2) not_less_eq)
|
||||
|
||||
(* FIXME: move to Word_Lib *)
|
||||
(* FIXME: move to Word_Lib_l4v *)
|
||||
lemma word_upcast_0_sle:
|
||||
"LENGTH('a::len) < LENGTH('b::len) \<Longrightarrow> 0 <=s UCAST('a \<rightarrow> 'b) w"
|
||||
by (simp add: word_sle_iff_le[OF word_msb_0 word_upcast_neg_msb])
|
||||
|
||||
(* FIXME: move to Word_Lib *)
|
||||
(* FIXME: move to Word_Lib_l4v *)
|
||||
lemma scast_ucast_up_eq_ucast:
|
||||
assumes "LENGTH('a::len) < LENGTH('b::len)"
|
||||
shows "SCAST('b \<rightarrow> 'c) (UCAST('a \<rightarrow> 'b) w) = UCAST('a \<rightarrow> 'c::len) w"
|
||||
|
@ -361,7 +361,7 @@ lemma shiftr_and_eq_shiftl:
|
|||
thus ?thesis using word_eq_iff by blast
|
||||
qed
|
||||
|
||||
(* FIXME: move to Word_Lib *)
|
||||
(* FIXME: move to Word_Lib_l4v *)
|
||||
lemma sign_extend_0[simp]:
|
||||
"sign_extend a 0 = 0"
|
||||
by (simp add: sign_extend_def)
|
||||
|
@ -382,7 +382,7 @@ lemma name_seq_bound_helper:
|
|||
apply (rule ccontr, simp add: linorder_not_le)
|
||||
done
|
||||
|
||||
(* FIXME: what's being proven here? it's a pure word lemma - should it go in Word_Lib? *)
|
||||
(* FIXME: what's being proven here? it's a pure word lemma - should it go in Word_Lib_l4v? *)
|
||||
lemma reset_name_seq_bound_helper:
|
||||
fixes sz
|
||||
fixes v :: "('a :: len) word"
|
||||
|
@ -1318,7 +1318,7 @@ lemma word_ctz_0[simp]:
|
|||
"word_ctz (0::64 word) = 64"
|
||||
by (clarsimp simp: word_ctz_def to_bl_def)+
|
||||
|
||||
(* FIXME move to Word_Lib *)
|
||||
(* FIXME move to Word_Lib_l4v *)
|
||||
lemma unat_trans_ucast_helper:
|
||||
"\<lbrakk> unat x < n ; n \<le> Suc 0 \<rbrakk> \<Longrightarrow> ucast x = 0"
|
||||
by (simp add: le_Suc_eq unsigned_eq_0_iff)
|
||||
|
|
|
@ -1456,7 +1456,7 @@ lemma mask_inj_if:
|
|||
"\<lbrakk>a && mask n = a; b && mask n = b; a && mask n = b && mask n\<rbrakk>\<Longrightarrow> a = b"
|
||||
by (rule box_equals)
|
||||
|
||||
(* FIXME: move to Word_Lib, generalise *)
|
||||
(* FIXME: move to Word_Lib_l4v, generalise *)
|
||||
lemma bound_preserve_mask:
|
||||
"\<lbrakk> is_aligned (x::word32) n; x\<le> mask k; (z::word32)\<le> mask n; n < 32; k < 32; n \<le> k \<rbrakk> \<Longrightarrow>
|
||||
x+z \<le> mask k"
|
||||
|
|
|
@ -526,7 +526,7 @@ lemma pt_offs_range_correct:
|
|||
"x \<in> pt_offs_range High_pt_ptr \<Longrightarrow> \<exists>y. x = High_pt_ptr + (ucast (y:: 8 word) << 2)"
|
||||
by (simp_all add: pt_offs_range_correct' s0_ptrs_aligned)
|
||||
|
||||
(* FIXME: move to Word_Lib *)
|
||||
(* FIXME: move to Word_Lib_l4v *)
|
||||
lemma bl_to_bin_le2p_aux:
|
||||
"bl_to_bin_aux bs w \<le> (w + 1) * (2 ^ length bs) - 1"
|
||||
apply (induct bs arbitrary: w)
|
||||
|
@ -536,7 +536,7 @@ lemma bl_to_bin_le2p_aux:
|
|||
apply (drule meta_spec, erule xtr8 [rotated], simp)+
|
||||
done
|
||||
|
||||
(* FIXME: move to Word_Lib *)
|
||||
(* FIXME: move to Word_Lib_l4v *)
|
||||
lemma bl_to_bin_le2p: "bl_to_bin bs \<le> (2 ^ length bs) - 1"
|
||||
apply (unfold bl_to_bin_def)
|
||||
apply (rule xtr3)
|
||||
|
@ -545,7 +545,7 @@ lemma bl_to_bin_le2p: "bl_to_bin bs \<le> (2 ^ length bs) - 1"
|
|||
apply simp
|
||||
done
|
||||
|
||||
(* FIXME: move to Word_Lib *)
|
||||
(* FIXME: move to Word_Lib_l4v *)
|
||||
lemma of_bl_length_le:
|
||||
"length x = k \<Longrightarrow> k < len_of TYPE('a) \<Longrightarrow> (of_bl x :: 'a :: len word) \<le> 2 ^ k - 1"
|
||||
by (simp add: of_bl_length_less)
|
||||
|
@ -606,11 +606,11 @@ lemma cnode_offs_in_range:
|
|||
"length x = 10 \<Longrightarrow> Silc_cnode_ptr + of_bl x * 0x10 \<in> cnode_offs_range Silc_cnode_ptr"
|
||||
by (simp_all add: cnode_offs_in_range' s0_ptrs_aligned)
|
||||
|
||||
(* FIXME: move to Word_Lib *)
|
||||
(* FIXME: move to Word_Lib_l4v *)
|
||||
lemma le_mask_eq: "x \<le> 2 ^ n - 1 \<Longrightarrow> x AND mask n = (x :: 'a :: len word)"
|
||||
by (metis and_mask_eq_iff_le_mask mask_2pm1)
|
||||
|
||||
(* FIXME: move to Word_Lib *)
|
||||
(* FIXME: move to Word_Lib_l4v *)
|
||||
lemma word_div_mult':
|
||||
fixes c :: "'a::len word"
|
||||
shows "\<lbrakk>0 < c; a \<le> b * c \<rbrakk> \<Longrightarrow> a div c \<le> b"
|
||||
|
|
|
@ -64,7 +64,7 @@ lemma invs_valid_irq_states[elim!]:
|
|||
"invs s \<Longrightarrow> valid_irq_states s"
|
||||
by(auto simp: invs_def valid_state_def)
|
||||
|
||||
(* FIXME: move to Word_Lib *)
|
||||
(* FIXME: move to Word_Lib_l4v *)
|
||||
lemma uint_ucast:
|
||||
"(x :: 'a :: len word) < 2 ^ LENGTH('b) \<Longrightarrow> uint (ucast x :: 'b :: len word) = uint x"
|
||||
by (metis Word.of_nat_unat mod_less of_nat_numeral semiring_1_class.of_nat_power unat_less_helper
|
||||
|
|
|
@ -27,7 +27,7 @@ chapter "Specifications"
|
|||
*)
|
||||
|
||||
(* Session on which most other sessions build. *)
|
||||
session ASpec in "abstract" = Word_Lib +
|
||||
session ASpec in "abstract" = Word_Lib_l4v +
|
||||
options [document=pdf]
|
||||
sessions
|
||||
"HOL-Library"
|
||||
|
@ -61,7 +61,7 @@ session ASpec in "abstract" = Word_Lib +
|
|||
* Executable/Design Specification
|
||||
*)
|
||||
|
||||
session ExecSpec in "design" = Word_Lib +
|
||||
session ExecSpec in "design" = Word_Lib_l4v +
|
||||
options [document = false]
|
||||
sessions
|
||||
Lib
|
||||
|
@ -106,7 +106,7 @@ session CKernel in "cspec/$L4V_ARCH" = CParser +
|
|||
* CapDL
|
||||
*)
|
||||
|
||||
session DSpec in capDL = Word_Lib +
|
||||
session DSpec in capDL = Word_Lib_l4v +
|
||||
sessions
|
||||
ExecSpec
|
||||
ASpec
|
||||
|
@ -119,7 +119,7 @@ session DSpec in capDL = Word_Lib +
|
|||
* Take-Grant.
|
||||
*)
|
||||
|
||||
session TakeGrant in "take-grant" = Word_Lib +
|
||||
session TakeGrant in "take-grant" = Word_Lib_l4v +
|
||||
theories
|
||||
"System_S"
|
||||
"Isolation_S"
|
||||
|
|
|
@ -24,7 +24,7 @@
|
|||
|
||||
theory Intents_D
|
||||
imports
|
||||
"Word_Lib.WordSetup"
|
||||
"Word_Lib_l4v.WordSetup"
|
||||
"ASpec.CapRights_A"
|
||||
begin
|
||||
|
||||
|
|
|
@ -6,7 +6,7 @@
|
|||
|
||||
theory KernelState_C
|
||||
imports
|
||||
"Word_Lib.WordSetup"
|
||||
"Word_Lib_l4v.WordSetup"
|
||||
"CLib.BitFieldProofsLib"
|
||||
"Substitute"
|
||||
begin
|
||||
|
|
|
@ -246,7 +246,7 @@ theory_header = """(*
|
|||
chapter "Kernel Configuration"
|
||||
|
||||
theory Kernel_Config
|
||||
imports Word_Lib.WordSetup
|
||||
imports Word_Lib_l4v.WordSetup
|
||||
begin
|
||||
|
||||
(*
|
||||
|
|
|
@ -7,6 +7,7 @@ chapter "AARCH64 Machine Types"
|
|||
|
||||
theory MachineTypes
|
||||
imports
|
||||
Word_Lib_l4v.WordSetup
|
||||
Word_Lib.WordSetup
|
||||
Monads.Nondet_Empty_Fail
|
||||
Monads.Nondet_No_Fail
|
||||
|
|
|
@ -8,6 +8,7 @@ chapter "ARM Machine Types"
|
|||
|
||||
theory MachineTypes
|
||||
imports
|
||||
Word_Lib_l4v.WordSetup
|
||||
Word_Lib.WordSetup
|
||||
Monads.Nondet_Empty_Fail
|
||||
Monads.Nondet_No_Fail
|
||||
|
|
|
@ -8,7 +8,7 @@ chapter \<open>ARM\_HYP Machine Types\<close>
|
|||
|
||||
theory MachineTypes
|
||||
imports
|
||||
Word_Lib.WordSetup
|
||||
Word_Lib_l4v.WordSetup
|
||||
Monads.Nondet_Empty_Fail
|
||||
Monads.Nondet_No_Fail
|
||||
Monads.Reader_Option_ND
|
||||
|
|
|
@ -8,7 +8,7 @@ chapter "RISCV 64bit Machine Types"
|
|||
|
||||
theory MachineTypes
|
||||
imports
|
||||
Word_Lib.WordSetup
|
||||
Word_Lib_l4v.WordSetup
|
||||
Monads.Nondet_Empty_Fail
|
||||
Monads.Nondet_No_Fail
|
||||
Monads.Reader_Option_ND
|
||||
|
|
|
@ -8,6 +8,7 @@ chapter "x86-64bit Machine Types"
|
|||
|
||||
theory MachineTypes
|
||||
imports
|
||||
Word_Lib_l4v.WordSetup
|
||||
Word_Lib.WordSetup
|
||||
Monads.Nondet_Empty_Fail
|
||||
Monads.Nondet_No_Fail
|
||||
|
|
|
@ -8,7 +8,7 @@ chapter "Architecture-specific Invocation Labels"
|
|||
|
||||
theory ArchInvocationLabels_H
|
||||
imports
|
||||
"Word_Lib.Enumeration"
|
||||
"Word_Lib_l4v.Enumeration"
|
||||
Setup_Locale
|
||||
begin
|
||||
context Arch begin global_naming AARCH64_H
|
||||
|
|
|
@ -8,7 +8,7 @@ chapter "Architecture-specific Invocation Labels"
|
|||
|
||||
theory ArchInvocationLabels_H
|
||||
imports
|
||||
"Word_Lib.Enumeration"
|
||||
"Word_Lib_l4v.Enumeration"
|
||||
Setup_Locale
|
||||
begin
|
||||
context Arch begin global_naming ARM_H
|
||||
|
|
|
@ -8,7 +8,7 @@ chapter "Architecture-specific Invocation Labels"
|
|||
|
||||
theory ArchInvocationLabels_H
|
||||
imports
|
||||
"Word_Lib.Enumeration"
|
||||
"Word_Lib_l4v.Enumeration"
|
||||
Setup_Locale
|
||||
begin
|
||||
context Arch begin global_naming ARM_HYP_H
|
||||
|
|
|
@ -8,7 +8,7 @@ chapter "Architecture-specific Invocation Labels"
|
|||
|
||||
theory ArchInvocationLabels_H
|
||||
imports
|
||||
"Word_Lib.Enumeration"
|
||||
"Word_Lib_l4v.Enumeration"
|
||||
Setup_Locale
|
||||
begin
|
||||
context Arch begin global_naming RISCV64_H
|
||||
|
|
|
@ -8,7 +8,7 @@ chapter "Architecture-specific Invocation Labels"
|
|||
|
||||
theory ArchInvocationLabels_H
|
||||
imports
|
||||
"Word_Lib.Enumeration"
|
||||
"Word_Lib_l4v.Enumeration"
|
||||
Setup_Locale
|
||||
begin
|
||||
context Arch begin global_naming X64_H
|
||||
|
|
|
@ -9,6 +9,7 @@ chapter "Machine Operations"
|
|||
|
||||
theory MachineOps
|
||||
imports
|
||||
Word_Lib_l4v.WordSetup
|
||||
Word_Lib.WordSetup
|
||||
Monads.Nondet_Monad
|
||||
MachineMonad
|
||||
|
|
|
@ -9,7 +9,7 @@ chapter "Platform Definitions"
|
|||
theory Platform
|
||||
imports
|
||||
"Lib.Lib"
|
||||
"Word_Lib.WordSetup"
|
||||
"Word_Lib_l4v.WordSetup"
|
||||
"Lib.Defs"
|
||||
Setup_Locale
|
||||
Kernel_Config
|
||||
|
|
|
@ -10,7 +10,7 @@ theory Platform
|
|||
imports
|
||||
"Lib.Defs"
|
||||
"Lib.Lib"
|
||||
"Word_Lib.WordSetup"
|
||||
"Word_Lib_l4v.WordSetup"
|
||||
Setup_Locale
|
||||
Kernel_Config
|
||||
begin
|
||||
|
|
|
@ -10,7 +10,7 @@ theory Platform
|
|||
imports
|
||||
"Lib.Defs"
|
||||
"Lib.Lib"
|
||||
"Word_Lib.WordSetup"
|
||||
"Word_Lib_l4v.WordSetup"
|
||||
Setup_Locale
|
||||
Kernel_Config
|
||||
begin
|
||||
|
|
|
@ -8,7 +8,7 @@ chapter "Machine Operations"
|
|||
|
||||
theory MachineOps
|
||||
imports
|
||||
"Word_Lib.WordSetup"
|
||||
"Word_Lib_l4v.WordSetup"
|
||||
"Monads.Nondet_Monad"
|
||||
MachineMonad
|
||||
begin
|
||||
|
|
|
@ -9,7 +9,7 @@ chapter "Platform Definitions"
|
|||
theory Platform
|
||||
imports
|
||||
"Lib.Lib"
|
||||
"Word_Lib.WordSetup"
|
||||
"Word_Lib_l4v.WordSetup"
|
||||
"Lib.Defs"
|
||||
Setup_Locale
|
||||
Kernel_Config
|
||||
|
|
|
@ -8,7 +8,7 @@ chapter "Machine Operations"
|
|||
|
||||
theory MachineOps
|
||||
imports
|
||||
"Word_Lib.WordSetup"
|
||||
"Word_Lib_l4v.WordSetup"
|
||||
"Monads.Nondet_Monad"
|
||||
MachineMonad
|
||||
begin
|
||||
|
|
|
@ -9,7 +9,7 @@ chapter "Platform Definitions"
|
|||
theory Platform
|
||||
imports
|
||||
"Lib.Lib"
|
||||
"Word_Lib.WordSetup"
|
||||
"Word_Lib_l4v.WordSetup"
|
||||
"Lib.Defs"
|
||||
Setup_Locale
|
||||
Kernel_Config
|
||||
|
|
Some files were not shown because too many files have changed in this diff Show More
Loading…
Reference in New Issue