perf(optimiser): eliminate absorbing arithmetic and bitwise expressions

src/Examples.thy

@@ -35,6 +35,14 @@ lemma neutral_bits:
   "optimise (Binary And (Binary Xor (Input Y) (Literal 0)) (Literal (-1))) = Input Y"
   by eval
 
+lemma absorbing_arithmetic:
+  "optimise (Binary Mul (Input X) (Literal 0)) = Literal 0"
+  by eval
+
+lemma absorbing_bits:
+  "optimise (Binary Or (Binary And (Input Y) (Literal 0)) (Literal (-1))) = Literal (-1)"
+  by eval
+
 lemma dead_branch:
   "optimise (Cond (Literal 0) (Input X) (Input Y)) = Input Y"
   by eval

src/Model.thy

@@ -49,7 +49,11 @@ fun fold_binary :: "operator \<Rightarrow> expression \<Rightarrow> expression \
     else if b = Literal 1 \<and> op = Mul then a
     else if a = Literal 1 \<and> op = Mul then b
     else if b = Literal (-1) \<and> op = And then a
-    else if a = Literal (-1) \<and> op = And then b else Binary op a b)"
+    else if a = Literal (-1) \<and> op = And then b
+    else if b = Literal 0 \<and> op \<in> {Mul,And} then Literal 0
+    else if a = Literal 0 \<and> op \<in> {Mul,And,Shl,Shr} then Literal 0
+    else if b = Literal (-1) \<and> op = Or then Literal (-1)
+    else if a = Literal (-1) \<and> op = Or then Literal (-1) else Binary op a b)"
 
 fun fold_cond :: "expression \<Rightarrow> expression \<Rightarrow> expression \<Rightarrow> expression" where
   "fold_cond (Literal c) a b = (if c = 0 then b else a)"

tests/native.py

@@ -67,6 +67,7 @@ def main():
     cases = [(op, "x", "y") for op in OPERATORS]
     cases += [(op, "x", 0) for op in ("+", "-", "or", "xor", "shl", "shr")]
     cases += [("*", "x", 1), ("*", 1, "x"), ("and", "x", MASK)]
+    cases += [("*", "x", 0), ("and", "x", 0), ("shl", 0, "y"), ("shr", 0, "y"), ("or", "x", MASK)]
     cases += [("let", "a", ("+", "x", 3), ("+", "y", ("let", "b", "t", ("*", "a", "b")))),
               ("let", "x", "y", ("if", "t", ("+", "x", 1), ("-", "x", 1)))]
     cases += [generate(rng, 5, ["x", "y", "t"]) for _ in range(117)]