path: root/main.org

#+title: Formal Predicate Aware Symbolic Execution
#+author: Yann Herklotz
#+context_preset: ymhg-article
#+context_header_extra: \environment env
#+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
of the whole program at the same time.  Instructions that can executed in parallel are therefore
grouped together.  The scheduler can also optimise for various other goals, such as minimum number
of clock cycles in the block, or minimum amount of resources used in the block.

/Hyperblocks/ combine multiple basic blocks using predicated execution.  A scheduling algorithm can
then schedule the hyperblock by also analysing instruction predicates, and remove data dependencies
between operations that have independent predicates.  The question is then how do we integrate this
algorithm inside of a formally verified compiler.  Verifying the algorithm directly requires
formalising various heuristics, whereas the schedule is easier to check for correctness after the
fact.  We can verify the checker and run it to check that the schedule is correct.

This post[fn:1] covers multiple symbolic analysis passes and discusses their correctness arguments.
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 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
analysis.

** Quick Overview of Hyperblocks

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

Let us first define what a resource is in our symbolic expressions.  We want to keep track of four
main components.  Firstly, we are separating predicate registers ~Pred~ from standard registers
~Reg~.  Then, we also want to track memory, which can be done using a single global memory ~Mem~.
Finally, we might have different exit points under different conditions, so we also need to keep
track under which conditions we exit using ~Exit~.

#+cindex: abstr-imports
#+begin_src coq
<<abstr-imports>>

Definition reg := positive.

Inductive resource : Set :=
| Reg : reg -> resource
| Pred : reg -> resource
| Mem : resource
| Exit : resource.
#+end_src

We can then create expressions that mimic the expressions defined in RTLBlock
and RTLPar, which use expressions instead of registers as their inputs and
outputs.  This means that we can accumulate all the results of the operations as
general expressions that will be present in those registers.

- ~Ebase~ :: the starting value of the register.
- ~Eop~ :: Some arithmetic operation on a number of registers.
- ~Eload~ :: A load from a memory location into a register.
- ~Estore~ :: A store from a register to a memory location.
- ~Esetpred~ :: A predicate definition by taking a condition with an expression list.
- ~Eexit~ :: A syntactic exit instruction.

Then, to make recursion over expressions easier, ~expression_list~ is also defined in the datatype,
as that enables mutual recursive definitions over the datatypes.

#+begin_src coq
Inductive expression : Type :=
| Ebase : resource -> expression
| Eop : Op.operation -> expression_list -> expression
| Eload :
    AST.memory_chunk -> Op.addressing ->
    expression_list -> expression -> expression
| Estore :
    expression -> AST.memory_chunk ->
    Op.addressing -> expression_list ->
    expression -> expression
| Esetpred : Op.condition -> expression_list -> expression
| Eexit : cf_instr -> expression
with expression_list : Type :=
| Enil : expression_list
| Econs : expression -> expression_list -> expression_list.
#+end_src

The interesting thing to note about this abstract expression type is that it is weakly typed,
meaning predicates are not any different to standard expressions.  The correctness is therefore
governed by how the expressions are generated, and to what resource they are assigned to in the
final expression tree.[fn:2] We will also need some kind of equality check for these expressions, so
we can assume that we can implement a decidable check like the following:

#+begin_src coq
Axiom expression_dec:
  forall e1 e2: expression, {e1 = e2} + {e1 <> e2}.
#+end_src

Speaking of the tree, we can also define the forest that contains a mapping from resource to
corresponding expression.

First, let's define what a predicate is, by reusing a general predicate expression defined in
=vericert.hls.Predicate=.  The initial version of the predicate will be the same that is used in the
~SeqBB.t~ syntax, meaning literals are positive numbers.  The two logical operations that are
allowed are conjunction and disjunction.

#+begin_src coq
Definition predicate := positive.
Definition pred_op := @Predicate.pred_op predicate.
#+end_src

In addition to that, we also want to define a predicated expression.  To make our lives a bit easier
later on, we first define what a predicated "something" is, and then specialise it to define the
predicated expression.  This allows us to easily construct our symbolic values later on.  The main
thing to note is that a predicated expression is a non-empty list of a predicate combined with an
expression.

#+begin_src coq
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 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.
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.
#+end_src

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.

** 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
:END:

#+cindex: abstr-imports
#+name: abstr-imports
#+begin_src coq :tangle no
Require Import Coq.Logic.Decidable.
Require Import Coq.Structures.Equalities.

Require Import compcert.backend.Registers.
Require Import compcert.common.AST.
Require Import compcert.common.Globalenvs.
Require Import compcert.common.Memory.
Require Import compcert.common.Values.
Require Import compcert.lib.Floats.
Require Import compcert.lib.Integers.
Require Import compcert.lib.Maps.
Require compcert.verilog.Op.

Require Import vericert.common.Vericertlib.
Require Import vericert.hls.GibleSeq.
Require Import vericert.hls.GiblePar.
Require Import vericert.hls.Gible.
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~
:PROPERTIES:
:CUSTOM_ID: R_indexed-def-link
:END:

*** ~R_indexed-index-def~

#+cindex: R_indexed-index-def
#+name: R_indexed-index-def
#+begin_src coq :tangle no
Definition index (rs: resource) : positive :=
  match rs with
  | Reg r => xO (xO r)
  | Pred r => xI (xI r)
  | Mem => 1
  | Exit => 2
  end.
#+end_src

*** ~R_indexed-injectivity~

#+cindex: R_indexed-injectivity
#+name: R_indexed-injectivity
#+begin_src coq :tangle no
Lemma index_inj:  forall (x y: t), index x = index y -> x = y.
Proof. destruct x; destruct y; crush. Qed.
#+end_src

*** ~R_indexed-def~

#+cindex: R_indexed-def
#+cindex: R_indexed-index-def
#+cindex: R_indexed-injectivity
#+name: R_indexed-def
#+begin_src coq :tangle no
Lemma resource_eq : forall (r1 r2 : resource), {r1 = r2} + {r1 <> r2}.
Proof. decide equality; apply Pos.eq_dec. Defined.

Module R_indexed.
  Definition t := resource.
  Definition eq := resource_eq.
  <<R_indexed-index-def>>
  <<R_indexed-injectivity>>
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:
:END:

#+toc: cp

* Footnotes

[fn:2] We can see that predicates are actually not needed in the semantics of any other
expressions.  It might therefore be better to create a separate ~predicate_expression~ which will
only set predicates based on a condition.

[fn:1] This post uses noweb syntax to specify pieces of code defined elsewhere, and will link to
those pieces of code directly.