Update dependencies

4 files changed, 228 insertions, 64 deletions

diff --git a/env.tex b/env.tex
deleted file mode 100644
index 718d0f6..0000000
--- a/env.tex
+++ /dev/null
@@ -1,38 +0,0 @@
-\startenvironment env
-
-\setupinteraction[
-    state=start,
-    title={Predicate Aware Abstract Interpretation},
-    author={Yann Herklotz},
-    color=darkcyan,
-    contrastcolor=darkcyan,
-    openaction=ToggleViewer,
-    focus=height,
-    click=yes,
-    style=\rm,
-]
-
-\setuppapersize[A4][A4]
-
-\definefontfeature[default][default][protrusion=quality,expansion=quality]
-\setupbodyfont[ymhg]
-\setupinterlinespace[big]
-\setupindenting[yes,medium,next]
-
-\setuphead[title][
-  style={\bfd\ss},
-  header=empty,
-  align=center,
-  before={\blank[2*line,force]},
-]
-
-\setuphead[subject][style={\bfb\ss}]
-\setuphead[subsubject][style={\bfa\ss}]
-\setuphead[subsubsubject][style={\ita\ss}]
-\setuphead[subsubsubsubject][style={\it\ss}]
-\setuphead[section][style={\bfb\ss}]
-\setuphead[subsection][style={\bfa\ss}]
-\setuphead[subsubsection][style={\ita\ss}]
-\setuphead[subsubsubsection][style={\it\ss}]
-
-\stopenvironment
diff --git a/flake.lock b/flake.lock
new file mode 100644
index 0000000..63ef7a4
--- /dev/null
+++ b/flake.lock
@@ -0,0 +1,26 @@
+{
+  "nodes": {
+    "nixpkgs": {
+      "locked": {
+        "lastModified": 1656083042,
+        "narHash": "sha256-G6m/OAIcmoEWeS+DbU70aNv21QB3kZCtJuUo+33s5VY=",
+        "owner": "nixos",
+        "repo": "nixpkgs",
+        "rev": "dc0380bb215ce001fcfccf4609d902115f87ddf9",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nixos",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "root": {
+      "inputs": {
+        "nixpkgs": "nixpkgs"
+      }
+    }
+  },
+  "root": "root",
+  "version": 7
+}
diff --git a/flake.nix b/flake.nix
new file mode 100644
index 0000000..7303d3b
--- /dev/null
+++ b/flake.nix
@@ -0,0 +1,56 @@
+{
+  description = "Vericert dependencies";
+
+  inputs = { nixpkgs.url = "github:nixos/nixpkgs"; };
+
+  outputs = { self, nixpkgs }:
+    let
+      pkgs = nixpkgs.legacyPackages.x86_64-linux;
+      ncoq = pkgs.coq_8_14;
+      ncoqPackages = pkgs.coqPackages_8_14;
+      dpkgs = nixpkgs.legacyPackages.x86_64-darwin;
+      dncoq = dpkgs.coq_8_14;
+      dncoqPackages = dpkgs.coqPackages_8_14;
+    in {
+      devShell.x86_64-linux = pkgs.mkShell {
+        buildInputs = with pkgs;
+          [ ncoq
+            dune_2
+            gcc
+            ncoq.ocaml
+            ncoq.ocamlPackages.findlib
+            ncoq.ocamlPackages.menhir
+            ncoq.ocamlPackages.ocamlgraph
+            ncoq.ocamlPackages.menhirLib
+
+            ncoq.ocamlPackages.ocp-indent
+            ncoq.ocamlPackages.utop
+
+            ncoqPackages.serapi
+            python3
+            python3Packages.alectryon
+            python3Packages.sphinx_rtd_theme
+          ];
+      };
+      devShell.x86_64-darwin = dpkgs.mkShell {
+        buildInputs = with dpkgs;
+          [ dncoq
+            dune_2
+            gcc
+            dncoq.ocaml
+            dncoq.ocamlPackages.findlib
+            dncoq.ocamlPackages.menhir
+            dncoq.ocamlPackages.ocamlgraph
+            dncoq.ocamlPackages.menhirLib
+
+            dncoq.ocamlPackages.ocp-indent
+            dncoq.ocamlPackages.utop
+
+            dncoqPackages.serapi
+            python3
+            python3Packages.alectryon
+            python3Packages.sphinx_rtd_theme
+          ];
+      };
+    };
+}
diff --git a/main.org b/main.org
index 830af60..e43e4b5 100644
--- a/main.org
+++ b/main.org
@@ -3,6 +3,7 @@
 #+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
 
@@ -12,37 +13,156 @@ instructions using the same resource.  Verifying this algorithm requires formali
 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.
 
-** Phasellus et tortor eget tellus
+** Initialising the file
 
-*** aroiesntoirensnt
+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.
 
-Ornare gravida nec vitae lectus. Vivamus sed velit quis odio sagittis tincidunt. Praesent non
-faucibus ante, vel gravida nulla. Phasellus arcu eros, maximus fermentum nisl sed, iaculis pretium
-erat. Praesent eu risus vel sapien malesuada faucibus tempor nec mi. Vivamus eu purus tempor,
-molestie neque mollis, feugiat orci. Praesent magna diam, condimentum at bibendum posuere, dapibus
-vel ipsum. Phasellus ut sapien sit amet enim mollis elementum. Sed vel odio eu lacus interdum
-ultrices at sed dolor. Nam maximus tincidunt orci vel egestas. Vivamus scelerisque risus leo,
-malesuada tristique ex tempus ullamcorper. Nullam accumsan augue non nisi consectetur luctus. Cras
-erat nulla, suscipit et felis sit amet, congue laoreet lorem. Curabitur malesuada neque purus, ut
-consectetur nunc condimentum condimentum.
+[[#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]].
 
-Fusce at orci lorem. Vestibulum tempus mauris eget sapien dictum rutrum. Aenean faucibus massa non
-risus consectetur molestie. Curabitur cursus eget nisl sed pellentesque. Nulla facilisi. Suspendisse
-at quam eget nisi euismod bibendum et in ex. Morbi facilisis posuere felis non ultrices. Nulla
-sodales nunc ultricies, iaculis mi eget, molestie odio.
+** Definition of R_indexed
+:PROPERTIES:
+:CUSTOM_ID: R_indexed-def-link
+:END:
 
-Nullam ultricies elit sit amet lorem tempor faucibus. Orci varius natoque penatibus et magnis dis
-parturient montes, nascetur ridiculus mus. Vestibulum in erat vel nunc dictum suscipit vel non
-nulla. Donec imperdiet viverra diam, at pretium lorem aliquet at. Phasellus ornare aliquet magna a
-faucibus. Aenean nec eros ut nulla placerat ultricies ac at tortor. In imperdiet turpis mauris, ac
-sodales ante rutrum eu.
+~<<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
 
-** oaiernstoiaernst
+~<<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
 
-aoristna risetn oiarstn
+~<<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.
 
-#+begin_src c
-int main (int x) {
-    return x;
-}
+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.