1 files changed, 14 insertions, 0 deletions
diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v
index 0e60796..711bb33 100644
--- a/arm/ConstpropOpproof.v
+++ b/arm/ConstpropOpproof.v
@@ -19,6 +19,7 @@ Require Import Floats.
 Require Import Values.
 Require Import Memory.
 Require Import Globalenvs.
+Require Import Events.
 Require Import Op.
 Require Import Registers.
 Require Import RTL.
@@ -417,6 +418,19 @@ Proof.
   auto.
 Qed.
 
+Lemma builtin_strength_reduction_correct:
+  forall ef args vl m t vres m',
+  vl = approx_regs app args ->
+  external_call ef ge rs##args m t vres m' ->
+  let (ef', args') := builtin_strength_reduction ef args vl in
+  external_call ef' ge rs##args' m t vres m'.
+Proof.
+  (* force MATCH to be used *)
+  assert (val_match_approx (approx_reg app 1%positive) rs#(1%positive))
+    by (apply MATCH).
+  unfold builtin_strength_reduction; intros; simpl; auto.
+Qed.
+
 End STRENGTH_REDUCTION.
 
 End ANALYSIS.