From aed203ab3eeea43d84f4e50c5720111208ba7881 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Mon, 28 Mar 2022 12:13:09 +0100
Subject: Add specification for RTLBlockgenproof

---
 src/hls/RTLBlockgen.v      |  6 +++--
 src/hls/RTLBlockgenproof.v | 63 +++++++++++++++++++++++++++++++++++-----------
 2 files changed, 53 insertions(+), 16 deletions(-)

(limited to 'src/hls')

diff --git a/src/hls/RTLBlockgen.v b/src/hls/RTLBlockgen.v
index a29709b..dc65cc2 100644
--- a/src/hls/RTLBlockgen.v
+++ b/src/hls/RTLBlockgen.v
@@ -19,6 +19,8 @@
 ===========
 RTLBlockgen
 ===========
+
+.. coq:: none
 |*)
 
 Require compcert.backend.RTL.
@@ -34,8 +36,6 @@ Require Import vericert.hls.RTLBlock.
 
 #[local] Open Scope positive.
 
-Parameter partition : RTL.function -> Errors.res function.
-
 (*|
 ``find_block max nodes index``: Does not need to be sorted, because we use
 filter and the max fold function to find the desired element.
@@ -171,6 +171,8 @@ Definition check_present_blocks (c: code) (n: list positive) (max: positive) (i:
   | None => false
   end.
 
+Parameter partition : RTL.function -> Errors.res function.
+
 Definition transl_function (f: RTL.function) :=
   match partition f with
   | Errors.OK f' =>
diff --git a/src/hls/RTLBlockgenproof.v b/src/hls/RTLBlockgenproof.v
index 1544b5f..8434542 100644
--- a/src/hls/RTLBlockgenproof.v
+++ b/src/hls/RTLBlockgenproof.v
@@ -19,6 +19,8 @@
 ================
 RTLBlockgenproof
 ================
+
+.. coq:: none
 |*)
 
 Require compcert.backend.RTL.
@@ -58,14 +60,27 @@ For case number 3, there should be a ``nop`` instruction in the basic block, and
 then the equivalent control-flow instruction ending the basic block.
 |*)
 
-Parameter find_block_spec : code -> node -> RTL.instruction -> node -> Prop.
+Parameter find_block_spec : code -> node -> node -> Prop.
 
-Definition find_instr_spec (c: code) (n: node) (i: RTL.instruction) (n': node) (i': instr) :=
-    find_block_spec c n i n'
+Definition find_instr_spec (c: code) (n: node) (i: RTL.instruction)
+           (n': node) (i': instr) :=
+    find_block_spec c n n'
     /\ exists il,
       c ! n' = Some il
       /\ nth_error il.(bb_body) (Pos.to_nat n - Pos.to_nat n')%nat = Some i'.
 
+(*|
+.. index::
+   pair: semantics; transl_code_spec
+
+Translation Specification
+-------------------------
+
+This specification should describe the translation that the unverified
+transformation performs.  This should be proven from the validation of the
+transformation.
+|*)
+
 Inductive transl_code_spec (c: RTL.code) (tc: code) :=
 | transl_code_standard_bb :
   forall x x' i i',
@@ -73,16 +88,38 @@ Inductive transl_code_spec (c: RTL.code) (tc: code) :=
     find_instr_spec tc x i x' i' ->
     check_instr x i i' = true ->
     transl_code_spec c tc
-| transl_code_standard_goto :
-  forall
+| transl_code_standard_cf :
+  forall x x' i i' il,
+    c ! x = Some i ->
+    tc ! x' = Some il ->
+    find_instr_spec tc x i x' i' ->
+    check_cf_instr_body i i' = true ->
+    check_cf_instr i il.(bb_exit) = true ->
+    transl_code_spec c tc
 .
 
-Inductive match_states : RTL.state -> RTLBlock.state -> Prop :=
+Lemma transl_function_correct :
+  forall f tf,
+    transl_function f = OK tf ->
+    transl_code_spec f.(RTL.fn_code) tf.(fn_code).
+Proof. Admitted.
+
+Variant match_stackframe : RTL.stackframe -> stackframe -> Prop :=
+| match_stackframe_init :
+  forall a b,
+    match_stackframe a b.
+
+Variant match_states : RTL.state -> RTLBlock.state -> Prop :=
 | match_state :
-  forall stk f tf sp pc rs m
-         (TF: transl_function f = OK tf),
+  forall stk stk' f tf sp pc rs m pc' ps
+         (TF: transl_function f = OK tf)
+         (PC: find_block_spec tf.(fn_code) pc pc')
+         (STK: Forall2 match_stackframe stk stk'),
     match_states (RTL.State stk f sp pc rs m)
-                 (State stk tf sp (find_block max n i) rs m).
+                 (State stk' tf sp pc' rs ps m).
+
+Definition match_prog (p: RTL.program) (tp: RTLBlock.program) :=
+  Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp.
 
 Section CORRECTNESS.
 
@@ -92,10 +129,8 @@ Section CORRECTNESS.
   Context (TRANSL : match_prog prog tprog).
 
   Theorem transf_program_correct:
-    Smallstep.forward_simulation (RTL.semantics prog) (RTLBlock.semantics tprog).
-  Proof.
-    eapply Smallstep.forward_simulation_plus; eauto with htlproof.
-    apply senv_preserved.
+    Smallstep.forward_simulation (RTL.semantics prog)
+                                 (RTLBlock.semantics tprog).
+  Proof. Admitted.
 
 End CORRECTNESS.
-*)
-- 
cgit