From 8a57683e35e761389e0ca976d79f2a5a4c387733 Mon Sep 17 00:00:00 2001
From: Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>
Date: Mon, 8 Feb 2021 14:01:06 +0100
Subject: intro RTLpathWFcheck

---
 Makefile                      |  2 +-
 scheduling/RTLpathScheduler.v |  8 ++++----
 scheduling/RTLpathWFcheck.v   | 28 ++++++++++++++++++++++++++++
 3 files changed, 33 insertions(+), 5 deletions(-)
 create mode 100644 scheduling/RTLpathWFcheck.v

diff --git a/Makefile b/Makefile
index aabd01a4..9adeb6db 100644
--- a/Makefile
+++ b/Makefile
@@ -140,7 +140,7 @@ SCHEDULING= \
   RTLpathLivegen.v         RTLpathSE_impl.v \
   RTLpathproof.v           RTLpathSE_theory.v \
   RTLpathSchedulerproof.v  RTLpath.v \
-  RTLpathScheduler.v
+  RTLpathScheduler.v       RTLpathWFcheck.v
 
 # C front-end modules (in cfrontend/)
 
diff --git a/scheduling/RTLpathScheduler.v b/scheduling/RTLpathScheduler.v
index beab405f..6f90b455 100644
--- a/scheduling/RTLpathScheduler.v
+++ b/scheduling/RTLpathScheduler.v
@@ -7,7 +7,7 @@ This module is inspired from [Duplicate] and [Duplicateproof]
 Require Import AST Linking Values Maps Globalenvs Smallstep Registers.
 Require Import Coqlib Maps Events Errors Op.
 Require Import RTL RTLpath RTLpathLivegen RTLpathLivegenproof RTLpathSE_theory RTLpathSE_impl.
-
+Require RTLpathWFcheck.
 
 Notation "'ASSERT' A 'WITH' MSG 'IN' B" := (if A then B else Error (msg MSG))
          (at level 200, A at level 100, B at level 200)
@@ -32,14 +32,14 @@ Extract Constant untrusted_scheduler => "RTLpathScheduleraux.scheduler".
 
 Program Definition function_builder (tfr: RTL.function) (tpm: path_map) : 
   { r : res RTLpath.function | forall f', r = OK f' -> fn_RTL f' = tfr} :=
-  match RTLpathLivegen.function_checker tfr tpm with
+  match RTLpathWFcheck.function_checker tfr tpm with
   | false => Error (msg "In function_builder: (tfr, tpm) is not wellformed")
   | true => OK {| fn_RTL := tfr; fn_path := tpm |}
   end.
 Next Obligation.
-  apply function_checker_path_entry. auto.
+  apply RTLpathWFcheck.function_checker_path_entry. auto.
 Defined. Next Obligation.
-  apply function_checker_wellformed_path_map. auto.
+  apply RTLpathWFcheck.function_checker_wellformed_path_map. auto.
 Defined.
 
 Definition entrypoint_check (dm: PTree.t node) (fr tfr: RTL.function) : res unit :=
diff --git a/scheduling/RTLpathWFcheck.v b/scheduling/RTLpathWFcheck.v
new file mode 100644
index 00000000..eca5b24e
--- /dev/null
+++ b/scheduling/RTLpathWFcheck.v
@@ -0,0 +1,28 @@
+Require Import Coqlib.
+Require Import Maps.
+Require Import Lattice.
+Require Import AST.
+Require Import Op.
+Require Import Registers.
+Require Import Globalenvs Smallstep RTL RTLpath.
+Require Import Bool Errors.
+Require Import Program.
+Require RTLpathLivegen.
+
+Local Open Scope lazy_bool_scope.
+
+Local Open Scope option_monad_scope.
+
+Definition function_checker (f: RTL.function) (pm: path_map): bool := 
+  pm!(f.(fn_entrypoint)) &&& true. (* TODO: &&& list_path_checker f pm (PTree.elements pm) *)
+
+Lemma function_checker_wellformed_path_map f pm:
+  function_checker f pm = true -> wellformed_path_map f.(fn_code) pm.
+Admitted.
+
+Lemma function_checker_path_entry f pm:
+  function_checker f pm = true -> path_entry pm (f.(fn_entrypoint)).
+Proof.
+  unfold function_checker; rewrite RTLpathLivegen.lazy_and_Some_true;
+  unfold path_entry. firstorder congruence.
+Qed.
-- 
cgit