Remove literal files again

1 files changed, 99 insertions, 43 deletions

diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v
index bd40516..d23850a 100644
--- a/src/hls/RTLBlockInstr.v
+++ b/src/hls/RTLBlockInstr.v
@@ -16,7 +16,6 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-(* [[file:../../docs/scheduler-languages.org::rtlblockinstr-imports][rtlblockinstr-imports]] *)
 Require Import Coq.micromega.Lia.
 
 Require Import compcert.backend.Registers.
@@ -31,20 +30,47 @@ Require Import compcert.verilog.Op.
 
 Require Import Predicate.
 Require Import Vericertlib.
-(* rtlblockinstr-imports ends here *)
 
-(* [[file:../../docs/scheduler-languages.org::rtlblockinstr-instr-def][rtlblockinstr-instr-def]] *)
 Definition node := positive.
 
+(*|
+=============
+RTLBlockInstr
+=============
+
+These instructions are used for ``RTLBlock`` and ``RTLPar``, so that they have
+consistent instructions, which greatly simplifies the proofs, as they will by
+default have the same instruction syntax and semantics.  The only changes are
+therefore at the top-level of the instructions.
+
+Instruction Definition
+======================
+
+First, we define the instructions that can be placed into a basic block, meaning
+they won't branch.  The main changes to how instructions are defined in ``RTL``,
+is that these instructions don't have a next node, as they will be in a basic
+block, and they also have an optional predicate (``pred_op``).
+|*)
+
 Inductive instr : Type :=
 | RBnop : instr
-| RBop : option pred_op -> operation -> list reg -> reg -> instr
-| RBload : option pred_op -> memory_chunk -> addressing -> list reg -> reg -> instr
-| RBstore : option pred_op -> memory_chunk -> addressing -> list reg -> reg -> instr
-| RBsetpred : option pred_op -> condition -> list reg -> predicate -> instr.
-(* rtlblockinstr-instr-def ends here *)
+| RBop :
+  option pred_op -> operation -> list reg -> reg -> instr
+| RBload :
+  option pred_op -> memory_chunk -> addressing -> list reg -> reg -> instr
+| RBstore :
+  option pred_op -> memory_chunk -> addressing -> list reg -> reg -> instr
+| RBsetpred :
+  option pred_op -> condition -> list reg -> predicate -> instr.
+
+(*|
+Control-Flow Instruction Definition
+===================================
+
+These are the instructions that count as control-flow, and will be placed at the
+end of the basic blocks.
+|*)
 
-(* [[file:../../docs/scheduler-languages.org::rtlblockinstr-cf-instr-def][rtlblockinstr-cf-instr-def]] *)
 Inductive cf_instr : Type :=
 | RBcall : signature -> reg + ident -> list reg -> reg -> node -> cf_instr
 | RBtailcall : signature -> reg + ident -> list reg -> cf_instr
@@ -55,9 +81,12 @@ Inductive cf_instr : Type :=
 | RBreturn : option reg -> cf_instr
 | RBgoto : node -> cf_instr
 | RBpred_cf : pred_op -> cf_instr -> cf_instr -> cf_instr.
-(* rtlblockinstr-cf-instr-def ends here *)
 
-(* [[file:../../docs/scheduler-languages.org::rtlblockinstr-helpers][rtlblockinstr-helpers]] *)
+(*|
+Helper Functions
+================
+|*)
+
 Fixpoint successors_instr (i : cf_instr) : list node :=
   match i with
   | RBcall sig ros args res s => s :: nil
@@ -67,7 +96,8 @@ Fixpoint successors_instr (i : cf_instr) : list node :=
   | RBjumptable arg tbl => tbl
   | RBreturn optarg => nil
   | RBgoto n => n :: nil
-  | RBpred_cf p c1 c2 => concat (successors_instr c1 :: successors_instr c2 :: nil)
+  | RBpred_cf p c1 c2 =>
+      concat (successors_instr c1 :: successors_instr c2 :: nil)
   end.
 
 Definition max_reg_instr (m: positive) (i: instr) :=
@@ -136,7 +166,8 @@ Lemma eval_predf_pr_equiv :
     eval_predf ps p = eval_predf ps' p.
 Proof.
   induction p; simplify; auto;
-    try (unfold eval_predf; simplify; repeat (destruct_match; []); inv Heqp0; rewrite <- H; auto);
+    try (unfold eval_predf; simplify;
+         repeat (destruct_match; []); inv Heqp0; rewrite <- H; auto);
   [repeat rewrite eval_predf_Pand|repeat rewrite eval_predf_Por];
   erewrite IHp1; try eassumption; erewrite IHp2; eauto.
 Qed.
@@ -146,17 +177,30 @@ Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset :=
   | r1 :: rs, v1 :: vs => Regmap.set r1 v1 (init_regs vs rs)
   | _, _ => Regmap.init Vundef
   end.
-(* rtlblockinstr-helpers ends here *)
 
-(* [[file:../../docs/scheduler-languages.org::rtlblockinstr-instr-state][rtlblockinstr-instr-state]] *)
+(*|
+Instruction State
+-----------------
+
+Definition of the instruction state, which contains the following:
+
+:is_rs: This is the current state of the registers.
+:is_ps: This is the current state of the predicate registers, which is in a
+  separate namespace and area compared to the standard registers in [is_rs].
+:is_mem: The current state of the memory.
+|*)
+
 Record instr_state := mk_instr_state {
   is_rs: regset;
   is_ps: predset;
   is_mem: mem;
 }.
-(* rtlblockinstr-instr-state ends here *)
 
-(* [[file:../../docs/scheduler-languages.org::rtlblockinstr-type-def][rtlblockinstr-type-def]] *)
+(*|
+Top-Level Type Definitions
+==========================
+|*)
+
 Section DEFINITION.
 
   Context {bblock_body: Type}.
@@ -193,11 +237,17 @@ Section DEFINITION.
              (sp: val)             (**r stack pointer in calling function *)
              (pc: node)            (**r program point in calling function *)
              (rs: regset)          (**r register state in calling function *)
-             (pr: predset),        (**r predicate state of the calling function *)
+             (pr: predset),        (**r predicate state of the calling
+                                        function *)
       stackframe.
-(* rtlblockinstr-type-def ends here *)
 
-(* [[file:../../docs/scheduler-languages.org::#state][rtlblockinstr-state]] *)
+(*|
+State Definition
+----------------
+
+Definition of the ``state`` type, which is used by the ``step`` functions.
+|*)
+
   Variant state : Type :=
   | State:
       forall (stack: list stackframe) (**r call stack *)
@@ -219,13 +269,14 @@ Section DEFINITION.
              (v: val)                 (**r return value for the call *)
              (m: mem),                (**r memory state *)
       state.
-(* rtlblockinstr-state ends here *)
 
-(* [[file:../../docs/scheduler-languages.org::#state][rtlblockinstr-state]] *)
 End DEFINITION.
-(* rtlblockinstr-state ends here *)
 
-(* [[file:../../docs/scheduler-languages.org::rtlblockinstr-semantics][rtlblockinstr-semantics]] *)
+(*|
+Semantics
+=========
+|*)
+
 Section RELSEM.
 
   Context {bblock_body : Type}.
@@ -245,7 +296,8 @@ Section RELSEM.
       end
     end.
 
-  Inductive eval_pred: option pred_op -> instr_state -> instr_state -> instr_state -> Prop :=
+  Inductive eval_pred:
+    option pred_op -> instr_state -> instr_state -> instr_state -> Prop :=
   | eval_pred_true:
       forall i i' p,
       eval_predf (is_ps i) p = true ->
@@ -256,9 +308,7 @@ Section RELSEM.
       eval_pred (Some p) i i' i
   | eval_pred_none:
       forall i i', eval_pred None i i' i.
-(* rtlblockinstr-semantics ends here *)
 
-(* [[file:../../docs/scheduler-languages.org::#step_instr][rtlblockinstr-step_instr]] *)
   Inductive step_instr: val -> instr_state -> instr -> instr_state -> Prop :=
   | exec_RBnop:
       forall sp ist,
@@ -266,28 +316,33 @@ Section RELSEM.
   | exec_RBop:
       forall op v res args rs m sp p ist pr,
         eval_operation ge sp op rs##args m = Some v ->
-        eval_pred p (mk_instr_state rs pr m) (mk_instr_state (rs#res <- v) pr m) ist ->
+        eval_pred p (mk_instr_state rs pr m)
+                    (mk_instr_state (rs#res <- v) pr m) ist ->
         step_instr sp (mk_instr_state rs pr m) (RBop p op args res) ist
   | exec_RBload:
       forall addr rs args a chunk m v dst sp p pr ist,
         eval_addressing ge sp addr rs##args = Some a ->
         Mem.loadv chunk m a = Some v ->
-        eval_pred p (mk_instr_state rs pr m) (mk_instr_state (rs#dst <- v) pr m) ist ->
-        step_instr sp (mk_instr_state rs pr m) (RBload p chunk addr args dst) ist
+        eval_pred p (mk_instr_state rs pr m)
+                    (mk_instr_state (rs#dst <- v) pr m) ist ->
+        step_instr sp (mk_instr_state rs pr m)
+                      (RBload p chunk addr args dst) ist
   | exec_RBstore:
       forall addr rs args a chunk m src m' sp p pr ist,
         eval_addressing ge sp addr rs##args = Some a ->
         Mem.storev chunk m a rs#src = Some m' ->
-        eval_pred p (mk_instr_state rs pr m) (mk_instr_state rs pr m') ist ->
-        step_instr sp (mk_instr_state rs pr m) (RBstore p chunk addr args src) ist
+        eval_pred p (mk_instr_state rs pr m)
+                    (mk_instr_state rs pr m') ist ->
+        step_instr sp (mk_instr_state rs pr m)
+                      (RBstore p chunk addr args src) ist
   | exec_RBsetpred:
       forall sp rs pr m p c b args p' ist,
       Op.eval_condition c rs##args m = Some b ->
-      eval_pred p' (mk_instr_state rs pr m) (mk_instr_state rs (pr#p <- b) m) ist ->
-      step_instr sp (mk_instr_state rs pr m) (RBsetpred p' c args p) ist.
-(* rtlblockinstr-step_instr ends here *)
+      eval_pred p' (mk_instr_state rs pr m)
+                   (mk_instr_state rs (pr#p <- b) m) ist ->
+      step_instr sp (mk_instr_state rs pr m)
+                    (RBsetpred p' c args p) ist.
 
-(* [[file:../../docs/scheduler-languages.org::#step_cf_instr][rtlblockinstr-step_cf_instr]] *)
   Inductive step_cf_instr: state -> cf_instr -> trace -> state -> Prop :=
   | exec_RBcall:
     forall s f sp rs m res fd ros sig args pc pc' pr,
@@ -300,7 +355,8 @@ Section RELSEM.
       find_function ros rs = Some fd ->
       funsig fd = sig ->
       Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
-      step_cf_instr (State s f (Vptr stk Ptrofs.zero) pc rs pr m) (RBtailcall sig ros args)
+      step_cf_instr (State s f (Vptr stk Ptrofs.zero) pc rs pr m)
+                    (RBtailcall sig ros args)
         E0 (Callstate s fd rs##args m')
   | exec_RBbuiltin:
       forall s f sp rs m ef args res pc' vargs t vres m' pc pr,
@@ -327,13 +383,13 @@ Section RELSEM.
         E0 (Returnstate s (regmap_optget or Vundef rs) m')
   | exec_RBgoto:
       forall s f sp pc rs pr m pc',
-      step_cf_instr (State s f sp pc rs pr m) (RBgoto pc') E0 (State s f sp pc' rs pr m)
+      step_cf_instr (State s f sp pc rs pr m) (RBgoto pc') E0
+                    (State s f sp pc' rs pr m)
   | exec_RBpred_cf:
       forall s f sp pc rs pr m cf1 cf2 st' p t,
-      step_cf_instr (State s f sp pc rs pr m) (if eval_predf pr p then cf1 else cf2) t st' ->
-      step_cf_instr (State s f sp pc rs pr m) (RBpred_cf p cf1 cf2) t st'.
-(* rtlblockinstr-step_cf_instr ends here *)
+      step_cf_instr (State s f sp pc rs pr m)
+                    (if eval_predf pr p then cf1 else cf2) t st' ->
+      step_cf_instr (State s f sp pc rs pr m)
+                    (RBpred_cf p cf1 cf2) t st'.
 
-(* [[file:../../docs/scheduler-languages.org::#step_cf_instr][rtlblockinstr-end_RELSEM]] *)
 End RELSEM.
-(* rtlblockinstr-end_RELSEM ends here *)