1 files changed, 28 insertions, 0 deletions
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.