diff --git a/.browser_info/index.json b/.browser_info/index.json index 1b36c77d..8086074d 100644 --- a/.browser_info/index.json +++ b/.browser_info/index.json @@ -11,6 +11,8 @@ {"name": "Proofs", "description": "Supporting proof theories and definitions"}, {"name": "Semantics", "description": "Semantics of the GraalVM IR"}, + {"name": "SemanticsPaper", + "description": "Content for IR semantics description paper"}, {"name": "Snippets", "description": "Additional commands to enable the generation of LaTeX snippets of theories"}, diff --git a/Canonicalizations/.browser_info/build_uuid b/Canonicalizations/.browser_info/build_uuid index a3f9c8fa..c84274f9 100644 --- a/Canonicalizations/.browser_info/build_uuid +++ b/Canonicalizations/.browser_info/build_uuid @@ -1 +1 @@ -94b2d873-b4be-4e0a-9045-3603d668dae4 \ No newline at end of file +9410185a-1397-4e37-823e-e573c61b1bda \ No newline at end of file diff --git a/Canonicalizations/AbsPhase.html b/Canonicalizations/AbsPhase.html index cbd12b85..30baa6f1 100644 --- a/Canonicalizations/AbsPhase.html +++ b/Canonicalizations/AbsPhase.html @@ -12,27 +12,27 @@
subsection ‹AbsNode Phase› +subsection ‹AbsNode Phase› theory AbsPhase imports Common Proofs.StampEvalThms begin -phase AbsNode +phase AbsNode terminating size begin -text ‹ -Note: - -We can't use @{const word_sless} for reasoning about @{const intval_less_than}. +text ‹ +Note: + +We can't use @{const word_sless} for reasoning about @{const intval_less_than}. @{const word_sless} will always treat the $64^{th}$ bit as the sign flag -while @{const intval_less_than} uses the $b^{th}$ bit depending on the size of the word. -› +while @{const intval_less_than} uses the $b^{th}$ bit depending on the size of the word. +› -value "val[new_int 32 0 < new_int 32 4294967286]" ― ‹0 < -10 = False› -value "(0::int64) <s 4294967286" ― ‹0 < 4294967286 = True› +value "val[new_int 32 0 < new_int 32 4294967286]" ― ‹0 < -10 = False› +value "(0::int64) <s 4294967286" ― ‹0 < 4294967286 = True› lemma signed_eqiv: @@ -64,15 +64,15 @@Theory AbsPhase
by (metis min_def nle_le take_bit_take_bit) -text ‹ -A special value exists for the maximum negative integer as its negation is itself. -We can define the value as @{term "(set_bit (b - 1) 0)::int64"} for any bit-width, b. -› +text ‹ +A special value exists for the maximum negative integer as its negation is itself. +We can define the value as @{term "(set_bit (b - 1) 0)::int64"} for any bit-width, b. +› -value "(set_bit 1 0)::2 word" ― ‹2› -value "-(set_bit 1 0)::2 word" ― ‹2› -value "(set_bit 31 0)::32 word" ― ‹2147483648› -value "-(set_bit 31 0)::32 word" ― ‹2147483648› +value "(set_bit 1 0)::2 word" ― ‹2› +value "-(set_bit 1 0)::2 word" ― ‹2› +value "(set_bit 31 0)::32 word" ― ‹2147483648› +value "-(set_bit 31 0)::32 word" ― ‹2147483648› lemma negative_def: @@ -89,7 +89,7 @@Theory AbsPhase
using assms by (simp add: bit_last_iff word_sless_alt) -(* +(* lemma invert1: fixes v :: "'a::len word" assumes "v <s 0" @@ -137,7 +137,7 @@Theory AbsPhase
assumes "v ≠ (2^(LENGTH('a) - 1))" shows "0 <s (-v)" using invert1 assms negative_lower_bound order_less_le by blast -*) +*) lemma negative_lower_bound: fixes v :: "'a::len word" @@ -154,14 +154,14 @@Theory AbsPhase
shows "2^(LENGTH('a) - 1) <s x" using assms sorry -(* +(* lemma min_int: fixes x :: "'a::len word" assumes "x <s 0 ∧ 0 <s x" shows "x = 2^(LENGTH('a) - 1)" using assms using signed.less_asym by blast -*) +*) lemma negate_min_int: fixes v :: "'a::len word" @@ -195,7 +195,7 @@Theory AbsPhase
qed qed -text ‹We need to do the same proof at the value level.› +text ‹We need to do the same proof at the value level.› lemma invert_intval: assumes "int_signed_value b v < 0" @@ -289,7 +289,7 @@Theory AbsPhase
shows "intval_abs x ≠ UndefVal" using assms by force -(* Value level proofs *) +(* Value level proofs *) lemma val_abs_idem: assumes "valid_value x (IntegerStamp b l h)" assumes "val[abs(abs(x))] ≠ UndefVal" @@ -327,14 +327,14 @@Theory AbsPhase
qed qed -paragraph ‹Optimisations› +paragraph ‹Optimisations› -(* +(* optimization AbsIdempotence: "abs(abs(x)) ⟼ abs(x) when wf_stamp x ∧ stamp_expr x = IntegerStamp b l h" using val_abs_idem using wf_stamp_def by fastforce -*) +*) end diff --git a/Canonicalizations/AddPhase.html b/Canonicalizations/AddPhase.html index 151ba70c..a94c8067 100644 --- a/Canonicalizations/AddPhase.html +++ b/Canonicalizations/AddPhase.html @@ -12,14 +12,14 @@Theory AddPhase
-subsection ‹AddNode Phase› +subsection ‹AddNode Phase› theory AddPhase imports Common begin -phase AddNode +phase AddNode terminating size begin @@ -28,7 +28,7 @@Theory AddPhase
shows "bin_eval BinAdd x y = bin_eval BinAdd y x" by (simp add: intval_add_sym) -(* horrible backward proof - needs improving *) +(* horrible backward proof - needs improving *) optimization AddShiftConstantRight: "((const v) + y) ⟼ y + (const v) when ¬(is_ConstantExpr y)" apply (metis add_2_eq_Suc' less_Suc_eq plus_1_eq_Suc size.simps(11) size_non_add) using le_expr_def binadd_commute by blast @@ -36,16 +36,16 @@Theory AddPhase
optimization AddShiftConstantRight2: "((const v) + y) ⟼ y + (const v) when ¬(is_ConstantExpr y)" using AddShiftConstantRight by auto -(* TODO: define is_neutral and then lemmas like this: +(* TODO: define is_neutral and then lemmas like this: lemma simp_neutral: assumes n: "is_neutral op (IntVal32 n)" shows "bin_eval op x (IntVal32 n) = x" apply (induction op) unfolding is_neutral.simps using n apply auto -*) +*) -(* poor-mans is_neutral lemma *) +(* poor-mans is_neutral lemma *) lemma is_neutral_0 [simp]: assumes "val[(IntVal b x) + (IntVal b 0)] ≠ UndefVal" shows "val[(IntVal b x) + (IntVal b 0)] = (new_int b x)" @@ -54,7 +54,7 @@Theory AddPhase
lemma AddNeutral_Exp: shows "exp[(e + (const (IntVal 32 0)))] ≥ exp[e]" apply auto - subgoal premises p for m p x + subgoal premises p for m p x proof - obtain ev where ev: "[m,p] ⊢ e ↦ ev" using p by auto @@ -87,7 +87,7 @@Theory AddPhase
lemma RedundantSubAdd_Exp: shows "exp[((a - b) + b)] ≥ a" apply auto - subgoal premises p for m p y xa ya + subgoal premises p for m p y xa ya proof - obtain bv where bv: "[m,p] ⊢ b ↦ bv" using p(1) by auto @@ -111,7 +111,7 @@Theory AddPhase
optimization RedundantSubAdd: "((e⇩1 - e⇩2) + e⇩2) ⟼ e⇩1" using RedundantSubAdd_Exp by blast -(* a little helper lemma for using universal quantified assumptions *) +(* a little helper lemma for using universal quantified assumptions *) lemma allE2: "(∀x y. P x y) ⟹ (P a b ⟹ R) ⟹ R" by simp @@ -126,7 +126,7 @@Theory AddPhase
by (smt (z3) NeutralLeftSubVal evalDet eval_unused_bits_zero intval_add_sym intval_sub.elims new_int.simps well_formed_equal_defn) -(* Demonstration of our FOUR levels of expression rewrites: +(* Demonstration of our FOUR levels of expression rewrites: ======================================================= level 1 (Java-like): "-e + y ⟼ y - e" level 2 (expr trees): "rewrite_preservation @@ -157,21 +157,21 @@Theory AddPhase
([m,p] ⊢ e ↦ ya) ∧ v = intval_sub x ya ∧ v ≠ UndefVal)" level 4 (Word library): "-ev + yv = yv - ev" (twice, for 32-bit and 64-bit) -*) +*) -(* The LowLevel version, intval_*, of this helper lemma is much easier +(* The LowLevel version, intval_*, of this helper lemma is much easier to prove than the bin_eval level. And equally easy to use in AddToSub. - *) + *) lemma AddToSubHelperLowLevel: shows "val[-e + y] = val[y - e]" (is "?x = ?y") by (induction y; induction e; auto) print_phases -(* ----- Starts here ----- *) +(* ----- Starts here ----- *) -(* +(* AddNode has 8 optimisations total Currently *6* optimisations are verified. @@ -191,9 +191,9 @@Theory AddPhase
- MergeSignExtendAdd - MergeZeroExtendAdd -*) +*) -(* Value level proofs *) +(* Value level proofs *) lemma val_redundant_add_sub: assumes "a = new_int bb ival" assumes "val[b + a] ≠ UndefVal" @@ -205,7 +205,7 @@Theory AddPhase
shows "val[x + (-e)] = val[x - e]" by (cases x; cases e; auto simp: assms) -(* Exp level proofs *) +(* Exp level proofs *) lemma exp_add_left_negate_to_sub: "exp[-e + y] ≥ exp[y - e]" by (cases e; cases y; auto simp: AddToSubHelperLowLevel) @@ -213,7 +213,7 @@Theory AddPhase
lemma RedundantAddSub_Exp: shows "exp[(b + a) - b] ≥ a" apply auto - subgoal premises p for m p y xa ya + subgoal premises p for m p y xa ya proof - obtain bv where bv: "[m,p] ⊢ b ↦ bv" using p(1) by auto @@ -235,7 +235,7 @@Theory AddPhase
qed done -text ‹Optimisations› +text ‹Optimisations› optimization RedundantAddSub: "(b + a) - b ⟼ a" using RedundantAddSub_Exp by blast @@ -250,17 +250,17 @@Theory AddPhase
numeral_2_eq_2 plus_1_eq_Suc size.simps(1) size.simps(11) size_binary_const size_non_add) using exp_add_left_negate_to_sub by simp -(* ----- Ends here ----- *) +(* ----- Ends here ----- *) end -(* Isabelle Isar Questions: +(* Isabelle Isar Questions: Why doesn't subgoal handle \forall and ⟶ ? Then this pattern might become just a single subgoal? subgoal premises p1 apply ((rule allI)+; rule impI) subgoal premises p2 for m p v -*) +*) end