#+title: Formal Predicate Aware Symbolic Execution
#+author: Yann Herklotz
#+context_preset: ymhg-article
#+context_header_extra: \environment env
#+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
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]].

#+cindex: R_indexed-def
#+cindex: apred-type-definitions
#+begin_src coq
<<R_indexed-def>>
Module Rtree := ITree(R_indexed).
<<apred-type-definitions>>
#+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
#+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
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

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

*** ~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
#+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

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