Final changes

2 files changed, 387 insertions, 14 deletions

diff --git a/Makefile b/Makefile
index e51f7ff..084f9d0 100644
--- a/Makefile
+++ b/Makefile
@@ -16,6 +16,10 @@ Main.v: main.org
 	@echo "TANGLE" $<
 	@emacs -batch -find-file main.org -funcall org-babel-tangle
 
+%.pdf: %.mkiv
+	@echo "CONTEXT" $<
+	@context $<
+
 Makefile.coq _CoqProject: force
 	@echo "COQMAKE Makefile.coq"
 	@$(COQMAKE) $(COQINCLUDES) $(VS) -o Makefile.coq
diff --git a/main.org b/main.org
index b45e96f..7758147 100644
--- a/main.org
+++ b/main.org
@@ -2,8 +2,9 @@
 #+author: Yann Herklotz
 #+context_preset: ymhg-article
 #+context_header_extra: \environment env
-#+options: syntax:vim
+#+options: syntax:vim h:2
 #+property: header-args:coq :noweb no-export :padline yes :tangle Main.v
+#+html_head_extra: <style>body{font-family:"Libertinus Serif",serif;margin:0 auto;max-width:40rem;}.title{text-align:center;font-size:2.5em;}.org-src-container{padding:1em 2em;background-color:#EAF5F2;border: 1px solid #6AB9A4;border-radius:5px;margin:1em 0px;}.org-src-container>pre{margin:0px;}pre.example{padding:1em 2em;background-color:#F5EBEA;border: 1px solid #B96F6A;border-radius:5px;}h2,h3,a,a:hover,a:active,a:focus{color:#066;}h1,h2,h3{font-family:"Libertinus Sans",sans-serif;}#table-of-contents>h2{display:none;}</style>
 #+auto_tangle: t
 
 #+context: \noindent
@@ -164,21 +165,12 @@ Finally, we will also define what an ~Rtree~ is, which is a mapping from resourc
 where ~R_indexed~ is a proof of injectivity from resources into the positives, and is further
 defined in the [[R_indexed-def-link][next section]].
 
+#+cindex: R_indexed-def
+#+cindex: apred-type-definitions
 #+begin_src coq
 <<R_indexed-def>>
 Module Rtree := ITree(R_indexed).
-#+end_src
-
-#+begin_src coq
-Definition apred : Type := expression.
-Definition apred_op := @Predicate.pred_op apred.
-Definition apredicated A := NE.non_empty (apred_op * A).
-Definition apred_expr := apredicated expression.
-#+end_src
-
-#+cindex: R_indexed-def
-#+begin_src coq
-Definition forest : Type := Rtree.t apred_expr.
+<<apred-type-definitions>>
 #+end_src
 
 I'll also quickly sneak in some execution semantics for expression trees and some helper functions
@@ -186,13 +178,13 @@ for the forest:
 
 #+cindex: forest-helpers
 #+cindex: sem-expr
+#+cindex: genv-preserved
 #+begin_src coq
 <<forest-helpers>>
 <<sem-expr>>
 <<genv-preserved>>
 #+end_src
 
-
 * About Execution Semantics
 
 The main idea is that given two expressions, if these expressions are equal, that they will also
@@ -292,6 +284,218 @@ same result.
 
 * Complicating Life a Bit With Abstract Predicates
 
+One solution to the predicate execution problem is to also evaluate predicates symbolically, so that
+one can execute them with the starting context as well.  This is an obvious extension to the
+previous method, and also reuses the symbolic execution that was done for predicates.  However, it
+definitely does not come for free.  Currently we had the following model, which even though the
+proof of correctness does not quite pass at the end, had a simple idea for doing the proof.  We had
+the following definition for predicated expressions, which had a direct representation when doing
+the SAT check, as one only has to turn all the expressions into uniquely identifying numbers.
+
+#+begin_src coq
+Definition example_pred_expr: pred_expr :=
+      (Plit (false, 1), Ebase (Reg 2))
+  ::| NE.singleton (Plit (true, 1), Ebase (Reg 1)).
+#+end_src
+
+This could be represented using the following formula, where $e_2$ is just a variable which is
+paired with the syntactic ~Ebase (Reg 2)~:
+
+#+begin_export context
+\startformula
+  \neg p_1 \rightarrow e_2 \land p_1 \rightarrow e_1
+\stopformula
+#+end_export
+
+#+begin_export html
+\begin{equation}
+  \neg p_1 \rightarrow e_2 \land p_1 \rightarrow e_1
+\end{equation}
+#+end_export
+
+However, let's now go over how symbolic execution would work with symbolic predicates.
+
+** Symbolic Execution with Symbolic Predicate
+
+We can define abstract predicates as the following, defined as a snippet called
+~<<apred-type-definitions>>~ which was inserted earlier, and we define a forest type like the
+following.
+
+#+cindex: apred-type-definitions
+#+name: apred-type-definitions
+#+begin_src coq :tangle no
+Definition apred : Type := expression.
+Definition apred_op := @Predicate.pred_op apred.
+Definition apredicated A := NE.non_empty (apred_op * A).
+Definition apred_expr := apredicated expression.
+
+Definition forest : Type := Rtree.t apred_expr.
+#+end_src
+
+We will first define the update function that works with symbolic predicates in the most general
+sense, just so that we can guarantee that we now have correct predicates which imply the runtime
+equivalence between two predicated expressions.  This means that everytime we encounter a predicate,
+we will have to evaluate it with the current expressions forest and retrieve the correct value for
+each of the literals at this moment in the execution.  We have to start by defining a function like
+that, starting by just simply turning a /symbolic predicated expression/ into a symbolic predicate,
+which is essentially what was done in the previous section, but now with more rich predicates.
+
+#+begin_src coq
+Fixpoint apredicated_to_apred_op
+         (b: bool)
+         (a: apredicated expression): apred_op :=
+  match a with
+  | NE.singleton (p, e) => p → Plit (b, e)
+  | (p, e) ::| r =>
+      (p → Plit (b, e)) ∧ apredicated_to_apred_op b r
+  end.
+#+end_src
+
+We then use this function to turn a standard predicated into an abstract predicate.  This works as
+expected for every case of the predicate syntax, except for the literal case, where we call the
+~apredicated_to_apred_op~ function to get a predicate that represents this expression.
+
+#+begin_src coq
+Fixpoint get_pred' (f: forest) (ap: pred_op): apred_op :=
+  match ap with
+  | Ptrue => Ptrue
+  | Pfalse => Pfalse
+  | Plit (a, b) =>
+      apredicated_to_apred_op a (f # (Pred b))
+  | Pand a b => Pand (get_pred' f a) (get_pred' f b)
+  | Por a b => Por (get_pred' f a) (get_pred' f b)
+  end.
+#+end_src
+
+There is already quite some nesting, because we used to only have predicates externally to
+expressions, but now they can be nested as well.  As a quick example, the expressions presented in
+the previous sections might look like the following in the current representation.
+
+The following represents the dynamic value that is present in predicate ~Pred 1~, which is the
+predicate we were evaluating in the previous section.
+
+#+begin_src coq
+Definition dynamic_esetpred: expression :=
+  Esetpred (Op.Ccomp Clt)
+           (to_elist ((Ebase (Reg 1))
+                        :: Ebase (Reg 2)
+                        :: nil)).
+#+end_src
+
+Then, this will be present in the final ~apred_expr~, which contains all the information of the
+current values of each of the predicates, including which expression should then hold.
+
+#+begin_src coq
+Definition example_pred_expr2: apred_expr :=
+  ((Ptrue → Plit (false, dynamic_esetpred)), Ebase (Reg 2))
+    ::| NE.singleton ((Ptrue → Plit (true, dynamic_esetpred)),
+                       Ebase (Reg 1)).
+#+end_src
+
+When we then want to pass this expression to the SAT solver to reason about the equivalence between
+two ~apred_expr~, you might realise that we have to turn each of the expressions into numbers again,
+which lands us back at exactly the same expression we already had previously.  This was the case
+where we were not doing any symbolic analysis of predicates.  In the following expression, $e_3$
+refers to the syntactic construct of the ~dynamic_esetpred~ expression.
+
+#+begin_export context
+\startformula
+  (\top \rightarrow \neg e_3) \rightarrow e_2 \land (\top \rightarrow e_3) \rightarrow e_1
+\stopformula
+#+end_export
+
+#+begin_export html
+\begin{equation}
+  (\top \rightarrow \neg e_3) \rightarrow e_2 \land (\top \rightarrow e_3) \rightarrow e_1
+\end{equation}
+#+end_export
+
+After simplification we get the exact same expression as before, with the only difference being
+$p_1$ is now represented as $e_3$, which is not really a distinction.  However, the benefit that we
+get from this is that we can now correctly identify more complicated input code like predicated
+set-predicate instructions.  The update function will then look something like the following.
+
+#+cindex: predicated-functions
+#+begin_src coq
+<<predicated-functions>>
+
+Definition update_wo_exit (fop : forest) (i : instr): forest :=
+  match i with
+  | RBnop => fop
+  | RBop p op rl r =>
+      let nv :=
+        app_predicated (get_pred fop p)
+                       (fop # (Reg r))
+                       (map_predicated (pred_ret (Eop op))
+                                       (merge (list_translation rl fop)))
+      in
+      fop # (Reg r) <- nv
+  | _ => fop
+  end.
+#+end_src
+
+So this is great, theoretically if two symbolic states are equivalent, then the behaviour should be
+the same.  However, there is still one last big problem with how predicates are represented.
+Now that the semantics of predicates are so rich, and that we go from predicates in the code to
+symbolic predicates in the forest, and then finally back to normal predicates with literals now
+referring to syntactic expressions, we have to reason about much more detailed semantics.  It was
+easy to reason about predicates earlier because if they were equivalent under the SAT solver, then
+one could deduce that if one is true, the other will also be true.  However, now that we have rich
+expressions inside of predicates, it means that the execution of predicates can actually block, so
+in addition to proving that two predicates are equivalent, one will also have to show that one can
+now execute both of these expressions.
+
+** Dealing with Hyperblock Exits
+
+One thing that we have not yet addressed is how to deal with exits, from the hyperblock.  This can
+be done by just remembering a predicate (in this case an abstract predicate), which represents the
+condition under which the current position in the code would be reached.  This means that if one
+hits an exit condition, one will add the condition of taking the exit to the current predicate one
+is remembering.  A new update function which describes all cases is now presented below, where the
+exit has been implemented correctly.
+
+#+cindex: update-function-rest
+#+begin_src coq
+Definition update (fop : option (apred_op * forest)) (i : instr)
+  : option (apred_op * forest) :=
+  do (pred, f) <- fop;
+  match i with
+  | RBnop => fop
+  | RBexit p c =>
+      let new_p :=
+        simplify (get_pred' f (negate (Option.default T p)) ∧ pred) in
+      do pruned <-
+           prune_predicated
+             (app_predicated (get_pred f p ∧ pred) (f # Exit)
+                             (pred_ret (Eexit c)));
+      Some (new_p, f # Exit <- pruned)
+  <<update-function-rest>>
+  end.
+#+end_src
+
+* A More Sane Proposition
+
+Finally, I believe that there is a better solution to this problem which avoids the evaluation issue
+of predicates from the previous section.  The trick is that if we restrict the predicates enough, we
+can get back to the first case where proving the correctness of the predicates without any runtime
+information and symbolic evaluation, still gives us a proof of semantic correctness.
+
+The main idea is that we can have the following conditions that restrict the block enough, while
+also allowing the scheduler to do anything it would want to do to the instructions.
+
+1. If a predicate is present within the input hyperblock, it will optionally be present within the
+   other hyperblock.  In practice this could be restricted further because the scheduler does not
+   change simplify or change the predicate expressions.
+2. If a set-predicate operation is present for a predicate, then the same set-predicate operation is
+   present in the output hyperblock.  This is verified by symbolically executing the set predicate
+   instructions, even though this is not used to replace the predicates of each register.
+3. If a set-predicate instruction is not present, then it should also not be present in the output
+   hyperblock.
+4. Finally, if a set-predicate instruction is present, then all instruction that depend on that
+   predicate need to either come all before or all after that instruction.  This will probably be
+   simplified into stating that set-predicate operations always need to come before instructions
+   that use the predicate.
+
 * Appendix
 :PROPERTIES:
 :APPENDIX:
@@ -643,6 +847,121 @@ Definition eval_predf_opt pr p :=
   match p with Some p' => eval_predf pr p' | None => true end.
 #+end_src
 
+*** ~predicated-functions~
+
+#+cindex: predicated-functions
+#+name: predicated-functions
+#+begin_src coq :tangle no
+Fixpoint list_translation (l : list reg) (f : forest) {struct l}
+  : list apred_expr :=
+  match l with
+  | nil => nil
+  | i :: l => (f # (Reg i)) :: (list_translation l f)
+  end.
+
+Fixpoint replicate {A} (n: nat) (l: A) :=
+  match n with
+  | O => nil
+  | S n => l :: replicate n l
+  end.
+
+Definition merge''' {A: Type} (x y: option (@Predicate.pred_op A)) :=
+  match x, y with
+  | Some p1, Some p2 => Some (Pand p1 p2)
+  | Some p, None | None, Some p => Some p
+  | None, None => None
+  end.
+
+Definition merge'' {A: Type} x :=
+  match x with
+  | ((a, e), (b, el)) => (@merge''' A a b, Econs e el)
+  end.
+
+Definition map_pred_op {A B P: Type} (pf: option (@Predicate.pred_op P) * (A -> B))
+           (pa: option (@Predicate.pred_op P) * A): option (@Predicate.pred_op P) * B :=
+  match pa, pf with
+  | (p, a), (p', f) => (merge''' p p', f a)
+  end.
+
+Definition predicated_prod {A B: Type} (p1: apredicated A) (p2: apredicated B) :=
+  NE.map (fun x => match x with ((a, b), (c, d)) => (Pand a c, (b, d)) end)
+         (NE.non_empty_prod p1 p2).
+
+Definition predicated_map {A B: Type} (f: A -> B) (p: apredicated A)
+  : apredicated B := NE.map (fun x => (fst x, f (snd x))) p.
+
+(*map (fun x => (fst x, Econs (snd x) Enil)) pel*)
+Definition merge' (pel: apred_expr) (tpel: apredicated expression_list) :=
+  predicated_map (uncurry Econs) (predicated_prod pel tpel).
+
+Fixpoint merge (pel: list apred_expr): apredicated expression_list :=
+  match pel with
+  | nil => NE.singleton (T, Enil)
+  | a :: b => merge' a (merge b)
+  end.
+
+Definition map_predicated {A B} (pf: apredicated (A -> B)) (pa: apredicated A)
+  : apredicated B :=
+  predicated_map (fun x => (fst x) (snd x)) (predicated_prod pf pa).
+
+Definition predicated_apply1 {A B} (pf: apredicated (A -> B)) (pa: A)
+  : apredicated B :=
+  NE.map (fun x => (fst x, (snd x) pa)) pf.
+
+Definition predicated_apply2 {A B C} (pf: apredicated (A -> B -> C)) (pa: A)
+           (pb: B): apredicated C :=
+  NE.map (fun x => (fst x, (snd x) pa pb)) pf.
+
+Definition predicated_apply3 {A B C D} (pf: apredicated (A -> B -> C -> D))
+           (pa: A) (pb: B) (pc: C): apredicated D :=
+  NE.map (fun x => (fst x, (snd x) pa pb pc)) pf.
+
+Definition predicated_from_opt {A: Type} (p: option apred_op) (a: A) :=
+  match p with
+  | Some p' => NE.singleton (p', a)
+  | None => NE.singleton (T, a)
+  end.
+
+Fixpoint NEfold_left {A B} (f: A -> B -> A) (l: NE.non_empty B) (a: A) : A :=
+  match l with
+  | NE.singleton a' => f a a'
+  | a' ::| b => NEfold_left f b (f a a')
+  end.
+
+Fixpoint NEapp {A} (l m: NE.non_empty A) :=
+  match l with
+  | NE.singleton a => a ::| m
+  | a ::| b => a ::| NEapp b m
+  end.
+
+Definition app_predicated' {A: Type} (a b: apredicated A) :=
+  let negation := ¬ (NEfold_left (fun a b => a ∨ (fst b)) b ⟂) in
+  NEapp (NE.map (fun x => (negation ∧ fst x, snd x)) a) b.
+
+Definition app_predicated {A: Type} (p': apred_op) (a b: apredicated A) :=
+  NEapp (NE.map (fun x => (¬ p' ∧ fst x, snd x)) a)
+        (NE.map (fun x => (p' ∧ fst x, snd x)) b).
+
+Definition prune_predicated {A: Type} (a: apredicated A) :=
+  NE.filter (fun x => match deep_simplify expression_dec (fst x) with ⟂ => false | _ => true end)
+            (NE.map (fun x => (deep_simplify expression_dec (fst x), snd x)) a).
+
+Definition pred_ret {A: Type} (a: A) : apredicated A :=
+  NE.singleton (T, a).
+
+Definition upd_pred_forest (p: apred_op) (f: forest) :=
+  PTree.map (fun i e =>
+               NE.map (fun (x: apred_op * expression) =>
+                         let (pred, expr) := x in
+                         (Pand p pred, expr)) e) f.
+
+Definition get_pred (f: forest) (ap: option pred_op): apred_op :=
+  get_pred' f (Option.default Ptrue ap).
+
+Definition simpl_combine {A: Type} (a b: option (@Predicate.pred_op A)) :=
+  Option.map simplify (combine_pred a b).
+#+end_src
+
 ** ~section-abstr-eval~
 
 #+cindex: section-abstr-eval
@@ -774,6 +1093,56 @@ Module PredOpVersion.
 End PredOpVersion.
 #+end_src
 
+** Definition of final version
+
+*** ~update-function-rest~
+
+#+cindex: update-function-rest
+#+name: update-function-rest
+#+begin_src coq :tangle no
+| RBop p op rl r =>
+    do pruned <-
+         prune_predicated
+           (app_predicated (get_pred f p ∧ pred)
+                           (f # (Reg r))
+                           (map_predicated (pred_ret (Eop op))
+                           (merge (list_translation rl f))));
+    Some (pred, f # (Reg r) <- pruned)
+| RBload p chunk addr rl r =>
+    do pruned <-
+         prune_predicated
+           (app_predicated (get_pred f p ∧ pred)
+                           (f # (Reg r))
+                           (map_predicated
+                              (map_predicated (pred_ret (Eload chunk addr))
+                                              (merge (list_translation rl f)))
+                              (f # Mem)));
+    Some (pred, f # (Reg r) <- pruned)
+| RBstore p chunk addr rl r =>
+    do pruned <-
+         prune_predicated
+           (app_predicated (get_pred f p ∧ pred)
+                           (f # Mem)
+                           (map_predicated
+                              (map_predicated
+                                 (predicated_apply2
+                                    (map_predicated (pred_ret Estore)
+                                                    (f # (Reg r))) chunk addr)
+                                 (merge (list_translation rl f))) (f # Mem)));
+    Some (pred, f # Mem <- pruned)
+| RBsetpred p' c args p =>
+    do pruned <-
+         prune_predicated
+           (app_predicated (get_pred f p' ∧ pred)
+                                  (f # (Pred p))
+                                  (map_predicated
+                                     (pred_ret (Esetpred c))
+                                     (merge (list_translation args f))));
+    Some (pred, f # (Pred p) <- pruned)
+#+end_src
+
+#+context: \page
+
 * Index
 :PROPERTIES:
 :APPENDIX: