From dd8d4ae9c320668ac5fd70f72ea76b768edf8165 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Sat, 26 Mar 2022 15:48:47 +0000
Subject: Remove literal files again

---
 src/hls/RTLBlockgenproof.v | 38 ++++++++++++++++++++++++++++++--------
 1 file changed, 30 insertions(+), 8 deletions(-)

(limited to 'src/hls/RTLBlockgenproof.v')

diff --git a/src/hls/RTLBlockgenproof.v b/src/hls/RTLBlockgenproof.v
index d51e5d4..4568185 100644
--- a/src/hls/RTLBlockgenproof.v
+++ b/src/hls/RTLBlockgenproof.v
@@ -16,25 +16,47 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-(* [[file:../../docs/basic-block-generation.org::rtlblockgenproof-imports][rtlblockgenproof-imports]] *)
 Require compcert.backend.RTL.
 Require Import compcert.common.AST.
 Require Import compcert.lib.Maps.
+Require Import compcert.common.Errors.
 
+Require Import vericert.hls.RTLBlockInstr.
 Require Import vericert.hls.RTLBlock.
 Require Import vericert.hls.RTLBlockgen.
-(* rtlblockgenproof-imports ends here *)
 
-(* [[file:../../docs/basic-block-generation.org::rtlblockgenproof-match-states][rtlblockgenproof-match-states]] *)
+(*|
+Defining a find block specification
+-----------------------------------
+
+Basically, it should be able to find the location of the block without using the
+``find_block`` function, so that this is more useful for the proofs.  There are
+various different types of options that could come up though:
+
+1. The instruction is a standard instruction present inside of a basic block.
+2. The instruction is a standard instruction which ends with a ``goto``.
+3. The instruction is a control-flow instruction.
+
+For case number 1, there should exist a value in the list of instructions, such
+that the instructions match exactly, and the indices match as well.  In the
+original code, this instruction must have been going from the current node to
+the node - 1.  For case number 2, there should be an instruction at the right
+index again, however, this time there will also be a ``goto`` instruction in the
+control-flow part of the basic block.
+|*)
+
+(*Definition find_block_spec (c1: RTL.code) (c2: code) :=
+  forall x i,
+    c1 ! x = Some i ->
+    exists y li, c2 ! y = Some li /\ nth_error li.(bb_body) ((Pos.to_nat y) - (Pos.to_nat x))%nat = Some i.
+
 Inductive match_states : RTL.state -> RTLBlock.state -> Prop :=
 | match_state :
   forall stk f tf sp pc rs m
          (TF: transl_function f = OK tf),
-  match_states (RTL.State stk f sp pc rs m)
-               (RTLBlock.State stk tf sp (find_block max n i) rs m).
-(* rtlblockgenproof-match-states ends here *)
+    match_states (RTL.State stk f sp pc rs m)
+                 (State stk tf sp (find_block max n i) rs m).
 
-(* [[file:../../docs/basic-block-generation.org::rtlblockgenproof-correctness][rtlblockgenproof-correctness]] *)
 Section CORRECTNESS.
 
   Context (prog : RTL.program).
@@ -49,4 +71,4 @@ Section CORRECTNESS.
     apply senv_preserved.
 
 End CORRECTNESS.
-(* rtlblockgenproof-correctness ends here *)
+*)
-- 
cgit