From 36f336d8c57f053342ec794e5bc802ebb66fc82b Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 9 Jan 2020 08:59:28 +0100
Subject: proof for jumptable

---
 backend/ForwardMovesproof.v | 18 +++++++++++++++++-
 1 file changed, 17 insertions(+), 1 deletion(-)

(limited to 'backend/ForwardMovesproof.v')

diff --git a/backend/ForwardMovesproof.v b/backend/ForwardMovesproof.v
index 6562fc7b..7727bc38 100644
--- a/backend/ForwardMovesproof.v
+++ b/backend/ForwardMovesproof.v
@@ -436,7 +436,23 @@ Proof.
   rewrite subst_arg_ok; eassumption.
   constructor; auto.
 
-  admit.
+  simpl in *.
+  unfold fmap_sem in *.
+  destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
+  apply get_rb_sem_ge with (rb2 := map # pc); trivial.
+  replace (map # pc) with (apply_instr' (fn_code f) pc (map # pc)).
+  {
+    eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
+    2: apply apply_instr'_bot.
+    simpl.
+    apply list_nth_z_in with (n := Int.unsigned n).
+    assumption.
+  }
+  unfold apply_instr'.
+  unfold get_rb_sem in *.
+  destruct (map # pc) in *; try contradiction.
+  rewrite H.
+  reflexivity.
   
 (* return *)
 - destruct or as [arg | ].
-- 
cgit