Theory TreeSnippets

section ‹Verifying term graph optimizations using Isabelle/HOL›

theory TreeSnippets
  imports
    Canonicalizations.BinaryNode
    Canonicalizations.ConditionalPhase
    Canonicalizations.AddPhase
    Semantics.TreeToGraphThms
    Snippets.Snipping
    "HOL-Library.OptionalSugar"
begin

― ‹First, we disable undesirable markup.›
declare [[show_types=false,show_sorts=false]]
no_notation ConditionalExpr ("_ ? _ : _")

― ‹We want to disable and reduce how aggressive automated tactics are as obligations are generated in the paper›
method unfold_size = -
method unfold_optimization = 
  (unfold rewrite_preservation.simps, unfold rewrite_termination.simps,
    rule conjE, simp, simp del: le_expr_def)

subsection ‹Markup syntax for common operations›

notation (latex)
  kind ("_⟪_⟫")

notation (latex)
  stamp_expr ("\<^latex>‹\\pitchfork› _")

notation (latex)
  valid_value ("_ ∈ _")

notation (latex)
  val_to_bool ("_\<^latex>‹\\ensuremath{_{\\mathit{›bool\<^latex>‹}}}›")

notation (latex)
  constantAsStamp ("\<^latex>‹stamp-from-value› _")

notation (latex)
  find_node_and_stamp ("\<^latex>‹find-matching› _")

notation (latex)
  add_node ("\<^latex>‹insert› _")

notation (latex)
  get_fresh_id ("\<^latex>‹fresh-id› _")



notation (latex)
  size ("\<^latex>‹trm(›_\<^latex>‹)›")


subsection ‹Representing canonicalization optimizations›

text ‹
We wish to provide an example of the semantics layers 
at which optimizations can be expressed.
›

― ‹Algebraic laws›
lemma diff_self:
  fixes x :: int
  shows "x - x = 0"
  by simp
lemma diff_diff_cancel:
  fixes x y :: int
  shows "x - (x - y) = y"
  by simp
thm diff_self
thm diff_diff_cancel
snipbegin ‹algebraic-laws›
text ‹\begin{align}
@{thm diff_self[show_types=false]}\\
@{thm diff_diff_cancel[show_types=false]}
\end{align}›
snipend -

― ‹Values›
lemma diff_self_value: "∀x::'a::len word. x - x = 0"
  by simp
lemma diff_diff_cancel_value:
  "∀ x y::'a::len word . x - (x - y) = y"
  by simp

snipbegin ‹algebraic-laws-values›
text_raw ‹\begin{align}
@{thm diff_self_value[show_types]} \label{prop-v-minus-v}\\
@{thm diff_diff_cancel_value[show_types]} \label{prop-redundant-sub}
\end{align}›
snipend -

― ‹Expression›
translations
  "n" <= "CONST ConstantExpr (CONST IntVal b n)"
  "x - y" <= "CONST BinaryExpr (CONST BinSub) x y"
notation (ExprRule output)
  Refines ("_ ⟼ _")
lemma diff_self_expr:
  assumes "∀m p v. [m,p] ⊢ exp[x - x] ↦ IntVal b v"
  shows "exp[x - x] ≥ exp[const (IntVal b 0)]"
  using assms apply simp
  by (metis(full_types) evalDet val_to_bool.simps(1) zero_neq_one)

method open_eval = (simp; (rule impI)?; (rule allI)+; rule impI)

lemma diff_diff_cancel_expr:
  shows "exp[x - (x - y)] ≥ exp[y]"
  apply open_eval
  subgoal premises eval for m p v
  proof -
    obtain vx where vx: "[m, p] ⊢ x ↦ vx"
      using eval by blast
    obtain vy where vy: "[m, p] ⊢ y ↦ vy"
      using eval by blast
    then have e: "[m, p] ⊢ exp[x - (x - y)] ↦ val[vx - (vx - vy)]"
      using vx vy eval
      by (smt (verit, ccfv_SIG) bin_eval.simps(2) evalDet unfold_binary)
    then have notUn: "val[vx - (vx - vy)] ≠ UndefVal"
      using evaltree_not_undef by auto
    then have "val[vx - (vx - vy)] = vy"
      apply (cases vx; cases vy; auto simp: notUn)
      using eval_unused_bits_zero vy apply blast
      by (metis(full_types) intval_sub.simps(6))
    then show ?thesis 
      by (metis e eval evalDet vy)
  qed
  done

thm_oracles diff_diff_cancel_expr

snipbegin ‹algebraic-laws-expressions›
text_raw ‹\begin{align}
@{thm[mode=ExprRule] (concl) diff_self_expr} \label{prop-MinusSame} \\
@{thm[mode=ExprRule] (concl) diff_diff_cancel_expr}
\end{align}›
snipend -
no_translations
  "n" <= "CONST ConstantExpr (CONST IntVal b n)"
  "x - y" <= "CONST BinaryExpr (CONST BinSub) x y"


definition wf_stamp :: "IRExpr ⇒ bool" where
  "wf_stamp e = (∀m p v. ([m, p] ⊢ e ↦ v) ⟶ valid_value v (stamp_expr e))"

lemma wf_stamp_eval:
  assumes "wf_stamp e"
  assumes "stamp_expr e = IntegerStamp b lo hi"
  shows "∀m p v. ([m, p] ⊢ e ↦ v) ⟶ (∃vv. v = IntVal b vv)"
  using assms unfolding wf_stamp_def
  using valid_int_same_bits valid_int
  by metis

phase SnipPhase
  terminating size
begin
lemma sub_same_val:
  assumes "val[x - x] = IntVal b v"
  shows "val[x - x] = val[IntVal b 0]"
  using assms by (cases x; auto)

snipbegin ‹sub-same-32›
optimization SubIdentity:
  "x - x ⟼ ConstantExpr (IntVal b 0)
     when ((stamp_expr exp[x - x] = IntegerStamp b lo hi) ∧ wf_stamp exp[x - x])"
  snipend -
   using IRExpr.disc(42) size.simps(4) size_non_const
   apply simp
  apply (rule impI) apply simp
proof -
  assume assms: "stamp_binary BinSub (stamp_expr x) (stamp_expr x) = IntegerStamp b lo hi ∧ wf_stamp exp[x - x]"
  have "∀m p v . ([m, p] ⊢ exp[x - x] ↦ v) ⟶ (∃vv. v = IntVal b vv)"
    using assms wf_stamp_eval
    by (metis stamp_expr.simps(2))
  then show "∀m p v. ([m,p] ⊢ BinaryExpr BinSub x x ↦ v) ⟶ ([m,p] ⊢ ConstantExpr (IntVal b 0) ↦ v)"
    using wf_value_def
    by (smt (verit, best) BinaryExprE TreeSnippets.wf_stamp_def assms bin_eval.simps(2) constantAsStamp.simps(1) evalDet stamp_expr.simps(2) sub_same_val unfold_const valid_stamp.simps(1) valid_value.simps(1))
qed
thm_oracles SubIdentity

snipbegin ‹RedundantSubtract›
optimization RedundantSubtract:
  "x - (x - y) ⟼ y"
snipend -
  using size_simps apply simp
  using diff_diff_cancel_expr by presburger
end

subsection ‹Representing terms›

text ‹
We wish to show a simple example of expressions represented as terms.
›

snipbegin ‹ast-example›
text "@{value[display,margin=40] ‹BinaryExpr BinAdd (BinaryExpr BinMul x x) (BinaryExpr BinMul x x)›}"
snipend -

text ‹
Then we need to show the datatypes that compose the example expression.
›

snipbegin ‹abstract-syntax-tree›
text ‹@{datatype[display,margin=40] IRExpr}›
snipend -

snipbegin ‹value›
text ‹@{datatype[display,margin=40,show_abbrevs] Value}›
snipend -


subsection ‹Term semantics›

text ‹
The core expression evaluation functions need to be introduced.
›

snipbegin ‹eval›
text ‹@{term_type[mode=type_def] unary_eval}\\
@{term_type[mode=type_def] bin_eval}›
snipend -

text ‹
We then provide the full semantics of IR expressions.
›

no_translations
  ("prop") "P ∧ Q ⟹ R" <= ("prop") "P ⟹ Q ⟹ R"
translations
  ("prop") "P ⟹ Q ⟹ R" <= ("prop") "P ∧ Q ⟹ R"
snipbegin ‹tree-semantics›
text ‹
\induct{@{thm[mode=Rule] evaltree.UnaryExpr [no_vars]}}{semantics:unary}
\induct{@{thm[mode=Rule] evaltree.BinaryExpr [no_vars]}}{semantics:binary}
\induct{@{thm[mode=Rule] evaltree.ConditionalExpr [no_vars]}}{semantics:conditional}
\induct{@{thm[mode=Rule] evaltree.ConstantExpr [no_vars]}}{semantics:constant}
\induct{@{thm[mode=Rule] evaltree.ParameterExpr [no_vars]}}{semantics:parameter}
\induct{@{thm[mode=Rule] evaltree.LeafExpr [no_vars]}}{semantics:leaf}
›
snipend -
no_translations
  ("prop") "P ⟹ Q ⟹ R" <= ("prop") "P ∧ Q ⟹ R"
translations
  ("prop") "P ∧ Q ⟹ R" <= ("prop") "P ⟹ Q ⟹ R"


text ‹And show that expression evaluation is deterministic.›

snipbegin ‹tree-evaluation-deterministic›
text ‹@{thm[display] evalDet [no_vars]}›
snipend -


text ‹
We then want to start demonstrating the obligations for optimizations.
For this we define refinement over terms.
›

snipbegin ‹expression-refinement›
text ‹@{thm le_expr_def [no_vars]} ›
snipend -

text ‹
To motivate this definition we show the obligations generated
by optimization definitions.
›

phase SnipPhase
  terminating size
begin
snipbegin ‹InverseLeftSub›
optimization InverseLeftSub:
  "(x - y) + y ⟼ x"
snipend -
  snipbegin ‹InverseLeftSubObligation›
  text ‹@{subgoals[display]}›
  snipend -
  using RedundantSubAdd by auto

snipbegin ‹InverseRightSub›
optimization InverseRightSub: "y + (x - y) ⟼ x"
snipend -
  snipbegin ‹InverseRightSubObligation›
  text ‹@{subgoals[display]}›
  snipend -
  using RedundantSubAdd2(2) rewrite_termination.simps(1) apply blast
  using RedundantSubAdd2(1) rewrite_preservation.simps(1) by blast
end

snipbegin ‹expression-refinement-monotone›
text ‹@{thm[display,margin=60] mono_unary}
@{thm[display,margin=60] mono_binary}
@{thm[display,margin=60] mono_conditional}
›
snipend -

phase SnipPhase 
  terminating size
begin
snipbegin ‹BinaryFoldConstant›
optimization BinaryFoldConstant: "BinaryExpr op (const v1) (const v2) ⟼ ConstantExpr (bin_eval op v1 v2)"
snipend -
  snipbegin ‹BinaryFoldConstantObligation›
  text ‹@{subgoals[display]}›
  snipend -
  using BinaryFoldConstant(1) by auto

snipbegin ‹AddCommuteConstantRight›
optimization AddCommuteConstantRight:
  "(const v) + y ⟼ y + (const v) when ¬(is_ConstantExpr y)"
snipend -
  snipbegin ‹AddCommuteConstantRightObligation›
  text ‹@{subgoals[display,margin=50]}›
  snipend -
  using AddShiftConstantRight by auto

snipbegin ‹AddNeutral›
optimization AddNeutral: "x + (const (IntVal 32 0)) ⟼ x"
snipend -
  snipbegin ‹AddNeutralObligation›
  text ‹@{subgoals[display]}›
  snipend -
  apply auto
  using AddNeutral(1) rewrite_preservation.simps(1) by force

snipbegin ‹AddToSub›
optimization AddToSub: "-x + y ⟼ y - x"
snipend -
  snipbegin ‹AddToSubObligation›
  text ‹@{subgoals[display]}›
  snipend -
  using AddLeftNegateToSub by auto

end

definition trm where "trm = size"

lemma trm_defn[size_simps]:
  "trm x = size x"
  by (simp add: trm_def)

snipbegin ‹phase›
phase AddCanonicalizations
  terminating trm
begin
  text_raw "\\dots"
end
snipend -

hide_const (open) "Form.wf_stamp"

snipbegin ‹phase-example›
phase Conditional
  terminating trm
begin
snipend -

snipbegin ‹phase-example-1›optimization NegateCond: "((!c) ? t : f) ⟼ (c ? f : t)"snipend -
  apply (simp add: size_simps)
  using ConditionalPhase.NegateConditionFlipBranches(1) by simp

snipbegin ‹phase-example-2›optimization TrueCond: "(true ? t : f) ⟼ t"snipend -
  by (auto simp: trm_def)

snipbegin ‹phase-example-3›optimization FalseCond: "(false ? t : f) ⟼ f"snipend -
  by (auto simp: trm_def)

snipbegin ‹phase-example-4›optimization BranchEqual: "(c ? x : x) ⟼ x"snipend -
  by (auto simp: trm_def)
 
snipbegin ‹phase-example-5›optimization LessCond: "((u < v) ? t : f) ⟼ t
                   when (stamp_under (stamp_expr u) (stamp_expr v) 
                            ∧ wf_stamp u ∧ wf_stamp v)"snipend -
  apply (auto simp: trm_def)
  using ConditionalPhase.condition_bounds_x(1)
  by (metis(full_types) StampEvalThms.wf_stamp_def TreeSnippets.wf_stamp_def bin_eval.simps(14) stamp_under_defn)

snipbegin ‹phase-example-6›optimization condition_bounds_y: "((x < y) ? x : y) ⟼ y
                   when (stamp_under (stamp_expr y) (stamp_expr x) ∧ wf_stamp x ∧ wf_stamp y)"snipend -
  apply (auto simp: trm_def)
  using ConditionalPhase.condition_bounds_y(1)
  by (metis(full_types) StampEvalThms.wf_stamp_def TreeSnippets.wf_stamp_def bin_eval.simps(14) stamp_under_defn_inverse)


snipbegin ‹phase-example-7›end snipend -

lemma simplified_binary: "¬(is_ConstantExpr b) ⟹ size (BinaryExpr op a b) = size a + size b + 2"
  by (induction b; induction op; auto simp: is_ConstantExpr_def)

thm bin_size
thm bin_const_size
thm unary_size
thm size_non_add
snipbegin ‹termination›
text ‹
@{thm[display,margin=80] unary_size}
@{thm[display,margin=80] bin_const_size}
@{thm[display,margin=80] (concl) simplified_binary}
@{thm[display,margin=80] cond_size}
@{thm[display,margin=80] const_size}
@{thm[display,margin=80] param_size}
@{thm[display,margin=80] leaf_size}
›
snipend -


(* definition 5 (semantics-preserving) is there a distinction in Isabelle? *)

snipbegin ‹graph-representation›
text ‹@{bold ‹typedef›} IRGraph = 

@{term[source] ‹{g :: ID ⇀ (IRNode × Stamp) . finite (dom g)}›}›
snipend -

no_translations
  ("prop") "P ∧ Q ⟹ R" <= ("prop") "P ⟹ Q ⟹ R"
translations
  ("prop") "P ⟹ Q ⟹ R" <= ("prop") "P ∧ Q ⟹ R"
snipbegin ‹graph2tree›
text ‹
\induct{@{thm[mode=Rule] rep.ConstantNode [no_vars]}}{rep:constant}
\induct{@{thm[mode=Rule] rep.ParameterNode [no_vars]}}{rep:parameter}
\induct{@{thm[mode=Rule] rep.ConditionalNode [no_vars]}}{rep:conditional}
\induct{@{thm[mode=Rule] rep.AbsNode [no_vars]}}{rep:unary}
\induct{@{thm[mode=Rule] rep.SignExtendNode [no_vars]}}{rep:convert}
\induct{@{thm[mode=Rule] rep.AddNode [no_vars]}}{rep:binary}
\induct{@{thm[mode=Rule] rep.LeafNode [no_vars]}}{rep:leaf}
\induct{@{thm[mode=Rule] rep.RefNode [no_vars]}}{rep:ref}
›
snipend -

snipbegin ‹unique›
text ‹
\induct{@{thm[mode=Rule] unique.Exists [no_vars]}}{unique:exists}
\induct{@{thm[mode=Rule] unique.New [no_vars]}}{unique:new}
›
snipend -

snipbegin ‹tree2graph›
text ‹
\induct{@{thm[mode=Rule] unrep.UnrepConstantNode [no_vars]}}{unrep:constantnew}
\induct{@{thm[mode=Rule] unrep.UnrepParameterNode [no_vars]}}{unrep:parameternew}
\induct{@{thm[mode=Rule] unrep.UnrepUnaryNode [no_vars]}}{unrep:unarynew}
\induct{@{thm[mode=Rule] unrep.UnrepBinaryNode [no_vars]}}{unrep:binarynew}
\induct{@{thm[mode=Rule] unrep.AllLeafNodes [no_vars]}}{unrep:leaf}
›
snipend -
no_translations
  ("prop") "P ⟹ Q ⟹ R" <= ("prop") "P ∧ Q ⟹ R"
translations
  ("prop") "P ∧ Q ⟹ R" <= ("prop") "P ⟹ Q ⟹ R"


snipbegin ‹preeval›
text ‹@{thm is_preevaluated.simps}›
snipend -

snipbegin ‹deterministic-representation›
text ‹@{thm[display] repDet [no_vars]}›
snipend -
thm_oracles repDet

snipbegin ‹well-formed-term-graph›
text "@{thm (rhs) wf_term_graph_def [no_vars]}"
snipend -

(* definition 9 (well-formed graph) no? *)

snipbegin ‹graph-semantics›
text ‹@{thm encodeeval.intros}›
snipend -

snipbegin ‹graph-semantics-deterministic›
text ‹@{thm graphDet [no_vars]}›
snipend -
thm_oracles graphDet

notation (latex)
  graph_refinement ("\<^latex>‹term-graph-refinement› _")

snipbegin ‹graph-refinement›
text ‹@{thm[display, margin=60] graph_refinement_def [no_vars]}›
snipend -

(* hide as_set, should treat IRGraph as a set of pairs in paper *)
translations
  "n" <= "CONST as_set n"

snipbegin ‹graph-semantics-preservation›
text ‹@{thm[display, margin=30] graph_semantics_preservation_subscript [no_vars]}›
snipend -
thm_oracles graph_semantics_preservation_subscript

snipbegin ‹maximal-sharing›
text ‹@{thm[display, margin=50] maximal_sharing [no_vars]}›
snipend -

snipbegin ‹tree-to-graph-rewriting›
text ‹@{thm[display, margin=30] tree_to_graph_rewriting [no_vars]}›
snipend -
thm_oracles tree_to_graph_rewriting

snipbegin ‹term-graph-refines-term›
text ‹@{thm[display] graph_represents_expression_def [no_vars]}›
snipend -

snipbegin ‹term-graph-evaluation›
text ‹@{thm[display] term_graph_evaluation [no_vars]}›
snipend -

snipbegin ‹graph-construction›
text ‹@{thm[display, margin=40] graph_construction [no_vars]}›
snipend -
thm_oracles graph_construction

snipbegin ‹term-graph-reconstruction›
text ‹@{thm[display] term_graph_reconstruction [no_vars]}›
snipend -

snipbegin ‹refined-insert›
text ‹@{thm[display, margin=40] refined_insert [no_vars]}›
snipend -

end