#+title: Formal Predicate Aware Symbolic Execution
#+author: Yann Herklotz
#+context_preset: ymhg-article
#+context_header_extra: \environment env
#+options: syntax:vim toc:nil
#+property: header-args:coq :noweb no-export :padline yes :tangle Main.v

* Framing the Problem

/Hyperblocks/ combine multiple basic blocks using predicated execution.  A scheduling algorithm can
take this hyperblock and parallelise it, taking advantage of independent predicates to schedule
instructions using the same resource.  Verifying this algorithm requires formalising various
heuristics, whereas the schedule is easier to check correct.  If the checker is formalised, it can
be run to check that the schedule is correct.

** Initialising the file

We first add a few imports defined at the end of the file[fn:1] to get everything we are going to
use to define the abstract language.

[[#abstr-imports-link][=<<abstr-imports>>=]]
#+begin_src coq :exports none
<<abstr-imports>>
#+end_src

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

#+begin_src coq
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.  Speaking of the tree, we can also define the forest that contains a mapping
from resource to corresponding expression.

#+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]].

** Definition of R_indexed
:PROPERTIES:
:CUSTOM_ID: R_indexed-def-link
:END:

~<<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>> ::=~
#+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>> ::=~
#+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

* Top-level imports
:PROPERTIES:
:CUSTOM_ID: abstr-imports-link
:END:

~<<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.

#[local] Open Scope positive.
#[local] Open Scope pred_op.
#+end_src

* Footnotes

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