From 2e613cd29123583fb3378d5727217c359e818611 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 9 Jan 2020 08:54:33 +0100
Subject: more proofs

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

(limited to 'backend/ForwardMovesproof.v')

diff --git a/backend/ForwardMovesproof.v b/backend/ForwardMovesproof.v
index aa516df4..6562fc7b 100644
--- a/backend/ForwardMovesproof.v
+++ b/backend/ForwardMovesproof.v
@@ -199,6 +199,16 @@ Proof.
   reflexivity.
 Qed.
 
+Lemma top_ok :
+  forall rs, get_rb_sem (Some RELATION.top) rs.
+Proof.
+  unfold get_rb_sem, RELATION.top.
+  intros.
+  unfold get_r.
+  rewrite PTree.gempty.
+  reflexivity.
+Qed.
+
 Ltac TR_AT :=
   match goal with
   | [ A: (fn_code _)!_ = Some _ |- _ ] =>
@@ -447,7 +457,14 @@ Proof.
   eapply exec_function_internal; eauto.
   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 := Some RELATION.top).
+  {
+    eapply DS.fixpoint_entry with (code := fn_code f) (successors := successors_instr); try eassumption.
+  }
+  apply top_ok.
   
 (* external function *)
 - econstructor; split.
-- 
cgit