3 files changed, 17 insertions(+), 2 deletions(-)

M src/Examples.thy
M src/Model.thy
M tests/native.py

@@ 27,6 27,14 @@ lemma constant_fold:
   "optimise (Binary Add (Literal (-1)) (Literal 1)) = Literal 0"
   by eval
 
+lemma neutral_arithmetic:
+  "optimise (Binary Mul (Binary Add (Input X) (Literal 0)) (Literal 1)) = Input X"
+  by eval
+
+lemma neutral_bits:
+  "optimise (Binary And (Binary Xor (Input Y) (Literal 0)) (Literal (-1))) = Input Y"
+  by eval
+
 lemma dead_branch:
   "optimise (Cond (Literal 0) (Input X) (Input Y)) = Input Y"
   by eval

@@ 44,7 44,12 @@ fun scoped :: "nat \<Rightarrow> expression \<Rightarrow> bool" where
 
 fun fold_binary :: "operator \<Rightarrow> expression \<Rightarrow> expression \<Rightarrow> expression" where
   "fold_binary op (Literal a) (Literal b) = Literal (operate op a b)"
-| "fold_binary op a b = Binary op a b"
+| "fold_binary op a b = (if b = Literal 0 \<and> op \<in> {Add,Sub,Or,Xor,Shl,Shr} then a
+    else if a = Literal 0 \<and> op \<in> {Add,Or,Xor} then b
+    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)"
 
 fun fold_cond :: "expression \<Rightarrow> expression \<Rightarrow> expression \<Rightarrow> expression" where
   "fold_cond (Literal c) a b = (if c = 0 then b else a)"


@@ 58,7 63,7 @@ fun optimise :: "expression \<Rightarrow> expression" where
 
 lemma fold_binary_value:
   "evaluate (fold_binary op a b) env inputs = operate op (evaluate a env inputs) (evaluate b env inputs)"
-  by (cases a; cases b) auto
+  by (cases op; cases a; cases b) auto
 
 lemma fold_cond_value:
   "evaluate (fold_cond c a b) env inputs = (if evaluate c env inputs = 0 then evaluate b env inputs else evaluate a env inputs)"

@@ 65,6 65,8 @@ def main():
         raise RuntimeError("native differential tests require an x86-64 Linux host")
     rng = random.Random(0x52454D59)
     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 += [("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)]