Add more text

2 files changed, 590 insertions, 20 deletions

diff --git a/env.mkiv b/env.mkiv
index ee8619f..6eecce9 100644
--- a/env.mkiv
+++ b/env.mkiv
@@ -67,25 +67,51 @@
 \setupfootnotes[align={stretch,verytolerant,hz,hanging,hyphenated}]
 \setupmargindata[stack=yes]
 
-\definecolor[codeblockcolor][x=EAF5F2]
-\definecolor[codeblockborder][x=6AB9A4]
 \definetextbackground[codeblockbg][
   location=paragraph,
-  background=color,
-  backgroundcolor=codeblockcolor,
-  bottomoffset=\bodyfontsize,
+  topoffset=\bodyfontsize,
   corner=round,
-  framecolor=codeblockborder,
+]
+
+\definecolor[codeblockexportcolor][x=EAF5F2]
+\definecolor[codeblockexportborder][x=6AB9A4]
+\definetextbackground[codeblockexportbg][codeblockbg][
+  background=color,
+  backgroundcolor=codeblockexportcolor,
+  framecolor=codeblockexportborder,
+]
+
+\definecolor[codeblockexamplecolor][x=F5EBEA]
+\definecolor[codeblockexampleborder][x=B96F6A]
+\definetextbackground[codeblockexamplebg][codeblockbg][
+  background=color,
+  backgroundcolor=codeblockexamplecolor,
+  framecolor=codeblockexampleborder,
 ]
 
 \setupenumeration
   [OrgListingEnumEmpty]
   [alternative=empty,
-   before={\blank\startcodeblockbg},
-   after={\stopcodeblockbg\blank},
-   margin=0pt]
+   before=,
+   after=\blank,
+   margin=0pt,
+   indentnext=no,]
 
-\setupvimtyping[OrgBlkSrcCoq][margin=5mm]
+\setupenumeration
+  [OrgExampleEnumEmpty]
+  [indentnext=no,]
+
+\setupvimtyping[OrgBlkSrcCoq][
+  margin=5mm,
+  before={\startcodeblockexportbg\blank},
+  after={\stopcodeblockexportbg},
+]
+
+\setuptyping[OrgExample][
+  margin=5mm,
+  before={\startcodeblockexamplebg\blank},
+  after={\stopcodeblockexamplebg},
+]
 
 \setupregister[OrgConcept][
   style={\bfa\tt},
@@ -93,4 +119,8 @@
   textstyle=tt,
 ]
 
+\define\OrgTitleContents{}
+\setupcombinedlist[content][alternative=c]
+\setupsectionblock[frontpart][before=\blank,after=\blank,]
+
 \stopenvironment
diff --git a/main.org b/main.org
index 17194ef..b45e96f 100644
--- a/main.org
+++ b/main.org
@@ -2,10 +2,11 @@
 #+author: Yann Herklotz
 #+context_preset: ymhg-article
 #+context_header_extra: \environment env
-#+options: syntax:vim toc:nil
+#+options: syntax:vim
 #+property: header-args:coq :noweb no-export :padline yes :tangle Main.v
 #+auto_tangle: t
 
+#+context: \noindent
 One main optimisation in compilers targeting parallel architectures is /instruction scheduling/,
 where instructions are placed into time-slots statically so that these can be executed in parallel.
 To make this more manageable, the scheduler takes smaller chunks of code and schedules these instead
@@ -24,7 +25,7 @@ This post[fn:1] covers multiple symbolic analysis passes and discusses their cor
 The general goal is to talk about a realistic implementation and correctness proof inside of
 Vericert, which uses the CompCert verified C compiler as the front end.
 
-* Syntax Definitions
+* Syntax Definition
 
 This section will cover some syntax definitions for the various constructs we will use, especially
 the syntax of a hyperblock and the symbolic expressions that are the result of the symbolic
@@ -32,7 +33,35 @@ analysis.
 
 ** Quick Overview of Hyperblocks
 
-Hyperblocks are a list of predicated instructions, which contain the
+Hyperblocks are a list of predicated instructions, however, there are various ways in which these
+predicates can be represented.  Early works about predicated execution would have instructions that
+are optionally paired with a literal, which can either be a true or false predicate.  Then, there is
+a predicated set-predicate instruction which defines the value for the predicate.
+
+#+begin_example
+p  ::= (b, n)
+i  ::= (p) instr
+     | (p) p = c
+#+end_example
+
+However, there are various other possible definitions of this, for example the most general version
+would be the following, which is the one we will be using in this file:
+
+#+begin_example
+p  ::= (b, n) | p ∨ p | p ∧ p
+i  ::= (p) instr
+     | (p) (b, n) = c
+#+end_example
+
+There are also intermediate versions, where one can assign predicates using the set-predicate
+operation or have unpredicate set-predicate operations.
+
+#+begin_example
+p  ::= (b, n) | p ∨ p | p ∧ p         |         p  ::= (b, n) | p ∨ p | p ∧ p
+i  ::= (p) instr                      |         i  ::= (b, n) instr
+     | (b, n) = c                     |              | (b, n) = c
+                                      |              | (b, n) = p
+#+end_example
 
 ** Syntax of Symbolic Expressions
 
@@ -123,7 +152,22 @@ Definition predicated A := NE.non_empty (pred_op * A).
 Definition pred_expr := predicated expression.
 #+end_src
 
-We can then also speak about equivalence between two predicates by
+We can then also speak about equivalence between two predicates by using a SAT query, which uses a
+formally verified SAT solver.
+
+#+begin_src coq
+Compute sat_pred_simple (Plit (true, 1) ∨ Plit (false, 1)).
+(* ==> None *)
+#+end_src
+
+Finally, we will also define what an ~Rtree~ is, which is a mapping from resources to "something".
+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]].
+
+#+begin_src coq
+<<R_indexed-def>>
+Module Rtree := ITree(R_indexed).
+#+end_src
 
 #+begin_src coq
 Definition apred : Type := expression.
@@ -133,23 +177,320 @@ Definition apred_expr := apredicated expression.
 #+end_src
 
 #+cindex: R_indexed-def
-
 #+begin_src coq
-<<R_indexed-def>>
-Module Rtree := ITree(R_indexed).
 Definition forest : Type := Rtree.t apred_expr.
 #+end_src
 
-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]].
+I'll also quickly sneak in some execution semantics for expression trees and some helper functions
+for the forest:
+
+#+cindex: forest-helpers
+#+cindex: sem-expr
+#+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
+behave the same.  In the following Lemma, ~ictx~ is the execution context (register state, memory
+state, etc...) of the input program, and ~octx~ is the execution context of the output program.
+
+#+begin_src coq :exports none
+<<section-abstr-eval>>
+#+end_src
+
+#+cindex: lemma-sem-value-det
+#+name: lemma-sem-value-det
+#+begin_src coq :tangle no
+Lemma sem_value_det :
+  forall e v1 v2, sem_value ictx e v1 -> sem_value octx e v2 -> v1 = v2.
+Proof. Abort. (* exercise left to the reader ;) *)
+#+end_src
+
+However, this assumes that ~e~ is actually executable in both contexts, which is not something you
+can assume.  Instead, the only thing you know is that the input program is executable, so you want
+to be able to show that if you have syntactically the same expressions on both sides, that the
+output expression is also executable in its context.  This means the Lemma should look like the
+following:
+
+#+cindex: lemma-sem-value-det-better
+#+name: lemma-sem-value-det-better
+#+begin_src coq :tangle no
+Lemma sem_value_det_better :
+  forall e v, sem_value ictx e v -> sem_value octx e v.
+Proof. Abort.
+#+end_src
+
+* Naive symbolic execution
+
+Now, doing /sound/ symbolic execution is a tricky business in the first place.  Even without
+predicates, you might assume that if you just collect all the possible values that each register can
+take, and then get two states that are exactly the same, that this implies they two initial blocks
+must execute the same in all cases.  However, there are various issues when actually trying to prove
+this formally.  Semantics often block in cases where execution does not make sense, a common case
+being division by zero.
+
+For the simple case where we are executing linear instructions, we can see how we can write a
+function that will contain all possible values of instructions at the end.
+
+#+begin_src coq
+Definition update_no_predicates f i: Rtree.t pred_expr :=
+  match i with
+  | RBnop => f
+  | RBop _ op args dst =>
+      f ! (Reg dst) <-
+        (NE.singleton
+           (T, (Eop op (to_elist (map (fun x => f ! (Reg x)) args)))))
+  | _ => f (* Not defining other cases. *)
+  end.
+#+end_src
+
+The final version of this function will then allow you to prove the equivalence between two basic
+blocks according to their semantics.  Now let's add predicates to the function and try and do the
+same.
+
+#+begin_src coq :exports none
+<<module-pred-op>>
+#+end_src
+
+#+cindex: update-function-simple-predicate
+#+name: update-function-simple-predicate
+#+begin_src coq :tangle no
+Definition update (fop : Rtree.t pred_expr) (i : instr): Rtree.t pred_expr :=
+  match i with
+  | RBnop => fop
+  | RBop p op rl r =>
+      Rtree.set (Reg r)
+                (app_predicated (Option.default T p)
+                                (get_forest' (Reg r) fop)
+                                (map_predicated
+                                   (pred_ret (Eop op))
+                                   (merge (list_translation rl fop)))) fop
+  | _ => fop (* Still not defining other cases. *)
+  end.
+#+end_src
+
+Here we can see that the symbolic execution already becomes a bit more complicated, because we now
+need to correctly deal with predicated instructions.  The final representation is a /non-empty/ list
+of /predicated/ symbolic expressions.  The reason this representation is convenient instead of a
+more recursive structure is that the result of this ~update~ function can just be passed to a SAT
+solver, by referring to expressions as numbers.  This will tell us that two of these predicated
+expression lists are equivalent /iff/ a pair of predicates from each list is equivalent under
+satisfiability and their expressions are syntactically equal.
 
-* First Attempt at Symbolic Analysis
+** Does This Imply Equivalent Behaviour
+
+Now the question is if this implies equivalent behaviour, and the answer is it doesn't, because we
+don't have good enough execution semantics for the predicates.  From the update function, we are
+taking predicates directly from the instruction, meaning even if any literals inside of those
+predicates are changed using a set-predicate instruction, the predicates will still evaluate to the
+same result.
+
+* Complicating Life a Bit With Abstract Predicates
 
 * Appendix
 :PROPERTIES:
 :APPENDIX:
 :END:
 
+** Semantics of Expressions
+
+*** ~sem-expr~
+:PROPERTIES:
+:CUSTOM_ID: sem-expr-link
+:END:
+
+#+cindex: sem-expr
+#+name: sem-expr
+#+begin_src coq :tangle no
+Section SEMANTICS.
+
+Context {A : Type}.
+
+Record ctx : Type := mk_ctx {
+  ctx_is: instr_state;
+  ctx_sp: val;
+  ctx_ge: Genv.t A unit;
+}.
+
+Definition ctx_rs ctx := is_rs (ctx_is ctx).
+Definition ctx_ps ctx := is_ps (ctx_is ctx).
+Definition ctx_mem ctx := is_mem (ctx_is ctx).
+
+Inductive sem_value : ctx -> expression -> val -> Prop :=
+| Sbase_reg:
+    forall r ctx,
+    sem_value ctx (Ebase (Reg r)) ((ctx_rs ctx) !! r)
+| Sop:
+    forall ctx op args v lv,
+    sem_val_list ctx args lv ->
+    Op.eval_operation (ctx_ge ctx) (ctx_sp ctx) op lv (ctx_mem ctx) = Some v ->
+    sem_value ctx (Eop op args) v
+| Sload :
+    forall ctx mexp addr chunk args a v m' lv,
+    sem_mem ctx mexp m' ->
+    sem_val_list ctx args lv ->
+    Op.eval_addressing (ctx_ge ctx) (ctx_sp ctx) addr lv = Some a ->
+    Memory.Mem.loadv chunk m' a = Some v ->
+    sem_value ctx (Eload chunk addr args mexp) v
+with sem_pred : ctx -> expression -> bool -> Prop :=
+| Spred:
+    forall ctx args c lv v,
+    sem_val_list ctx args lv ->
+    Op.eval_condition c lv (ctx_mem ctx) = Some v ->
+    sem_pred ctx (Esetpred c args) v
+| Sbase_pred:
+    forall ctx p,
+    sem_pred ctx (Ebase (Pred p)) ((ctx_ps ctx) !! p)
+with sem_mem : ctx -> expression -> Memory.mem -> Prop :=
+| Sstore :
+    forall ctx mexp vexp chunk addr args lv v a m' m'',
+    sem_mem ctx mexp m' ->
+    sem_value ctx vexp v ->
+    sem_val_list ctx args lv ->
+    Op.eval_addressing (ctx_ge ctx) (ctx_sp ctx) addr lv = Some a ->
+    Memory.Mem.storev chunk m' a v = Some m'' ->
+    sem_mem ctx (Estore vexp chunk addr args mexp) m''
+| Sbase_mem :
+    forall ctx,
+    sem_mem ctx (Ebase Mem) (ctx_mem ctx)
+with sem_exit : ctx -> expression -> option cf_instr -> Prop :=
+| Sexit :
+  forall ctx cf,
+    sem_exit ctx (Eexit cf) (Some cf)
+| Sbase_exit :
+  forall ctx,
+    sem_exit ctx (Ebase Exit) None
+with sem_val_list : ctx -> expression_list -> list val -> Prop :=
+| Snil :
+    forall ctx,
+    sem_val_list ctx Enil nil
+| Scons :
+    forall ctx e v l lv,
+    sem_value ctx e v ->
+    sem_val_list ctx l lv ->
+    sem_val_list ctx (Econs e l) (v :: lv)
+.
+
+Inductive eval_apred (c: ctx): apred_op -> bool -> Prop :=
+| eval_APtrue : eval_apred c Ptrue true
+| eval_APfalse : eval_apred c Pfalse false
+| eval_APlit : forall p (b: bool) bres,
+    sem_pred c p (if b then bres else negb bres) ->
+    eval_apred c (Plit (b, p)) bres
+| eval_APand : forall p1 p2 b1 b2,
+  eval_apred c p1 b1 ->
+  eval_apred c p2 b2 ->
+  eval_apred c (Pand p1 p2) (b1 && b2)
+| eval_APor1 : forall p1 p2 b1 b2,
+  eval_apred c p1 b1 ->
+  eval_apred c p2 b2 ->
+  eval_apred c (Por p1 p2) (b1 || b2).
+
+Inductive sem_pred_expr {B: Type} (sem: ctx -> expression -> B -> Prop):
+  ctx -> apred_expr -> B -> Prop :=
+| sem_pred_expr_cons_true :
+  forall ctx e pr p' v,
+    eval_apred ctx pr true ->
+    sem ctx e v ->
+    sem_pred_expr sem ctx ((pr, e) ::| p') v
+| sem_pred_expr_cons_false :
+  forall ctx e pr p' v,
+    eval_apred ctx pr false ->
+    sem_pred_expr sem ctx p' v ->
+    sem_pred_expr sem ctx ((pr, e) ::| p') v
+| sem_pred_expr_single :
+  forall ctx e pr v,
+    eval_apred ctx pr true ->
+    sem ctx e v ->
+    sem_pred_expr sem ctx (NE.singleton (pr, e)) v
+.
+
+Definition collapse_pe (p: apred_expr) : option expression :=
+  match p with
+  | NE.singleton (APtrue, p) => Some p
+  | _ => None
+  end.
+
+Inductive sem_predset : ctx -> forest -> predset -> Prop :=
+| Spredset:
+    forall ctx f rs',
+    (forall x, sem_pred_expr sem_pred ctx (f # (Pred x)) (rs' !! x)) ->
+    sem_predset ctx f rs'.
+
+Inductive sem_regset : ctx -> forest -> regset -> Prop :=
+| Sregset:
+    forall ctx f rs',
+    (forall x, sem_pred_expr sem_value ctx (f # (Reg x)) (rs' !! x)) ->
+    sem_regset ctx f rs'.
+
+Inductive sem : ctx -> forest -> instr_state * option cf_instr -> Prop :=
+| Sem:
+    forall ctx rs' m' f pr' cf,
+    sem_regset ctx f rs' ->
+    sem_predset ctx f pr' ->
+    sem_pred_expr sem_mem ctx (f # Mem) m' ->
+    sem_pred_expr sem_exit ctx (f # Exit) cf ->
+    sem ctx f (mk_instr_state rs' pr' m', cf).
+
+End SEMANTICS.
+#+end_src
+
+*** ~genv-preserved~
+:PROPERTIES:
+:CUSTOM_ID: genv-preserved-link
+:END:
+
+#+cindex: genv-preserved
+#+name: genv-preserved
+#+begin_src coq :tangle no
+Definition ge_preserved {A B C D: Type} (ge: Genv.t A B) (tge: Genv.t C D) : Prop :=
+  (forall sp op vl m, Op.eval_operation ge sp op vl m =
+                      Op.eval_operation tge sp op vl m)
+  /\ (forall sp addr vl, Op.eval_addressing ge sp addr vl =
+                         Op.eval_addressing tge sp addr vl).
+
+Lemma ge_preserved_same:
+  forall A B ge, @ge_preserved A B A B ge ge.
+Proof. unfold ge_preserved; auto. Qed.
+#[local] Hint Resolve ge_preserved_same : core.
+
+Inductive match_states : instr_state -> instr_state -> Prop :=
+| match_states_intro:
+  forall ps ps' rs rs' m m',
+    (forall x, rs !! x = rs' !! x) ->
+    (forall x, ps !! x = ps' !! x) ->
+    m = m' ->
+    match_states (mk_instr_state rs ps  m) (mk_instr_state rs' ps' m').
+
+Lemma match_states_refl x : match_states x x.
+Proof. destruct x; constructor; crush. Qed.
+
+Lemma match_states_commut x y : match_states x y -> match_states y x.
+Proof. inversion 1; constructor; crush. Qed.
+
+Lemma match_states_trans x y z :
+  match_states x y -> match_states y z -> match_states x z.
+Proof. repeat inversion 1; constructor; crush. Qed.
+
+#[global]
+Instance match_states_Equivalence : Equivalence match_states :=
+  { Equivalence_Reflexive := match_states_refl ;
+    Equivalence_Symmetric := match_states_commut ;
+    Equivalence_Transitive := match_states_trans ; }.
+
+Inductive similar {A B} : @ctx A -> @ctx B -> Prop :=
+| similar_intro :
+    forall ist ist' sp ge tge,
+    ge_preserved ge tge ->
+    match_states ist ist' ->
+    similar (mk_ctx ist sp ge) (mk_ctx ist' sp tge).
+#+end_src
+
 ** ~abstr-imports~
 :PROPERTIES:
 :CUSTOM_ID: abstr-imports-link
@@ -179,13 +520,19 @@ Require Import vericert.hls.HashTree.
 Require Import vericert.hls.Predicate.
 Require Import vericert.common.DecEq.
 Require        vericert.common.NonEmpty.
+Require Import vericert.common.Monad.
 
 Module NE := NonEmpty.
 Import NE.NonEmptyNotation.
 
+Module OptionExtra := MonadExtra(Option).
+Import OptionExtra.
+Import OptionExtra.MonadNotation.
+
 #[local] Open Scope positive.
 #[local] Open Scope pred_op.
 #[local] Open Scope non_empty_scope.
+#[local] Open Scope monad_scope.
 #+end_src
 
 ** Definition of ~R_indexed~
@@ -234,6 +581,199 @@ Module R_indexed.
 End R_indexed.
 #+end_src
 
+** Forest helpers
+
+*** ~forest-helpers~
+:PROPERTIES:
+:CUSTOM_ID: forest-helpers-link
+:END:
+
+#+cindex: forest-helpers
+#+name: forest-helpers
+#+begin_src coq :tangle no
+Definition get_forest v (f: forest) :=
+  match Rtree.get v f with
+  | None => NE.singleton (Ptrue, (Ebase v))
+  | Some v' => v'
+  end.
+
+Definition get_forest' v (f: Rtree.t pred_expr) :=
+  match Rtree.get v f with
+  | None => NE.singleton (Ptrue, (Ebase v))
+  | Some v' => v'
+  end.
+
+Definition get_forest2 v (f: Rtree.t pred_expr) :=
+  match Rtree.get v f with
+  | None => (Ebase v)
+  | Some v' =>
+      match v' with
+      | NE.singleton (_, e) => e
+      | _ => (Ebase v) (* Just a place-holder. *)
+      end
+  end.
+
+Fixpoint to_elist l :=
+  match l with
+  | nil => Enil
+  | a :: b => Econs a (to_elist b)
+  end.
+
+Declare Scope forest.
+
+Notation "a # b" := (get_forest b a) (at level 1) : forest.
+Notation "a # b <- c" := (Rtree.set b c a) (at level 1, b at next level) : forest.
+
+Notation "a ! b" := (get_forest2 b a) (at level 1) : forest.
+Notation "a ! b <- c" := (Rtree.set b c a) (at level 1, b at next level) : forest.
+
+#[local] Open Scope forest.
+
+Definition maybe {A: Type} (vo: A) (pr: predset) p (v: A) :=
+  match p with
+  | Some p' => if eval_predf pr p' then v else vo
+  | None => v
+  end.
+
+Definition get_pr i := match i with mk_instr_state a b c => b end.
+
+Definition get_m i := match i with mk_instr_state a b c => c end.
+
+Definition eval_predf_opt pr p :=
+  match p with Some p' => eval_predf pr p' | None => true end.
+#+end_src
+
+** ~section-abstr-eval~
+
+#+cindex: section-abstr-eval
+#+name: section-abstr-eval
+#+begin_src coq :tangle no
+Section ABSTR_EVAL.
+  Definition fd := GibleSeq.fundef.
+  Definition tfd := GiblePar.fundef.
+
+  Context (ictx: @ctx fd) (octx: @ctx tfd) (HSIM: similar ictx octx).
+
+  <<lemma-sem-value-det>>
+  <<lemma-sem-value-det-better>>
+End ABSTR_EVAL.
+#+end_src
+
+** Definition of pred_op version
+
+#+cindex: predicated-op-defs
+#+name: predicated-op-defs
+#+begin_src coq :tangle no
+Fixpoint list_translation (l : list reg) (f : Rtree.t pred_expr) {struct l}
+  : list pred_expr :=
+  match l with
+  | nil => nil
+  | i :: l => (get_forest' (Reg i) f) :: (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: predicated A) (p2: predicated 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: predicated A)
+  : predicated B := NE.map (fun x => (fst x, f (snd x))) p.
+
+(*map (fun x => (fst x, Econs (snd x) Enil)) pel*)
+Definition merge' (pel: pred_expr) (tpel: predicated expression_list) :=
+  predicated_map (uncurry Econs) (predicated_prod pel tpel).
+
+Fixpoint merge (pel: list pred_expr): predicated expression_list :=
+  match pel with
+  | nil => NE.singleton (T, Enil)
+  | a :: b => merge' a (merge b)
+  end.
+
+Definition map_predicated {A B} (pf: predicated (A -> B)) (pa: predicated A)
+  : predicated B :=
+  predicated_map (fun x => (fst x) (snd x)) (predicated_prod pf pa).
+
+Definition predicated_apply1 {A B} (pf: predicated (A -> B)) (pa: A)
+  : predicated B :=
+  NE.map (fun x => (fst x, (snd x) pa)) pf.
+
+Definition predicated_apply2 {A B C} (pf: predicated (A -> B -> C)) (pa: A)
+           (pb: B): predicated C :=
+  NE.map (fun x => (fst x, (snd x) pa pb)) pf.
+
+Definition predicated_apply3 {A B C D} (pf: predicated (A -> B -> C -> D))
+           (pa: A) (pb: B) (pc: C): predicated 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.
+
+#[local] Open Scope non_empty_scope.
+#[local] Open Scope pred_op.
+
+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: predicated 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': pred_op) (a b: predicated 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: predicated A) :=
+  NE.filter (fun x => match deep_simplify peq (fst x) with ⟂ => false | _ => true end)
+            (NE.map (fun x => (deep_simplify peq (fst x), snd x)) a).
+
+Definition pred_ret {A: Type} (a: A) : predicated A :=
+  NE.singleton (T, a).
+#+end_src
+
+#+cindex: module-pred-op
+#+name: module-pred-op
+#+begin_src coq :tangle no
+Module PredOpVersion.
+  <<predicated-op-defs>>
+  <<update-function-simple-predicate>>
+End PredOpVersion.
+#+end_src
+
 * Index
 :PROPERTIES:
 :APPENDIX: