From 6b118a38913fe272347bd7b3cf6fb476463a519a Mon Sep 17 00:00:00 2001
From: Gregory Malecha <gmalecha@gmail.com>
Date: Mon, 10 Sep 2018 09:05:24 -0400
Subject: [PATCH 1/8] compilation units.

---
 bedrock2/src/BasicC64Semantics.v             |  2 +-
 bedrock2/src/BasicC64Syntax.v                |  2 +-
 bedrock2/src/Examples/Swap.v                 | 14 ++++++----
 bedrock2/src/Semantics.v                     |  4 +--
 bedrock2/src/StringNamesSyntax.v             |  2 +-
 bedrock2/src/Syntax.v                        |  5 ++--
 bedrock2/src/ToCString.v                     |  9 +++---
 bedrock2/src/Variables.v                     |  3 +-
 bedrock2/src/WeakestPrecondition.v           | 29 ++++++++++++--------
 bedrock2/src/WeakestPreconditionProperties.v |  9 ++++--
 bedrock2/src/ZNamesSyntax.v                  |  2 +-
 11 files changed, 49 insertions(+), 32 deletions(-)

diff --git a/bedrock2/src/BasicC64Semantics.v b/bedrock2/src/BasicC64Semantics.v
index 9bca98d29..2c5ad0f02 100644
--- a/bedrock2/src/BasicC64Semantics.v
+++ b/bedrock2/src/BasicC64Semantics.v
@@ -33,5 +33,5 @@ Instance parameters : parameters := {|
   (* TODO: faster maps *)
   mem := UnorderedList.map {| UnorderedList.key_eqb a b := if Word.weq a b then true else false |};
   locals := UnorderedList.map {| UnorderedList.key_eqb := String.eqb |};
-  funname_eqb := String.eqb;
+  globname_eqb := String.eqb;
 |}.
diff --git a/bedrock2/src/BasicC64Syntax.v b/bedrock2/src/BasicC64Syntax.v
index 2a29d14f4..cbff58302 100644
--- a/bedrock2/src/BasicC64Syntax.v
+++ b/bedrock2/src/BasicC64Syntax.v
@@ -33,7 +33,7 @@ Definition to_c_parameters : ToCString.parameters := {|
              | eq => e1++"=="++e2
              end%string;
      c_var := id;
-     c_fun := id;
+     c_glob := id;
      c_act := ToCString.c_call;
 
      varname_eqb := String.eqb;
diff --git a/bedrock2/src/Examples/Swap.v b/bedrock2/src/Examples/Swap.v
index dfbbc9354..c564a7a95 100644
--- a/bedrock2/src/Examples/Swap.v
+++ b/bedrock2/src/Examples/Swap.v
@@ -16,8 +16,8 @@ Section bsearch.
   )).
 
   Definition swap_swap : list varname * list varname * cmd := (("a"::"b"::nil), nil, bedrock_func_body:(
-    cmd.call nil "swap" (var "a"::var "b"::nil);
-    cmd.call nil "swap" (var "a"::var "b"::nil)
+    cmd.call nil (expr.global "swap") (var "a"::var "b"::nil);
+    cmd.call nil (expr.global "swap") (var "a"::var "b"::nil)
   )).
 End bsearch.
 
@@ -92,10 +92,10 @@ end.
 
 Context (__A : map.ok Semantics.mem).
 Lemma swap_ok : 
-  forall a_addr a b_addr b (m:map.rep (value:=@Semantics.byte _)) R t,
+  forall l a_addr a b_addr b (m:map.rep (value:=@Semantics.byte _)) R t,
     (sep (ptsto 1 a_addr a) (sep (ptsto 1 b_addr b) R)) m ->
   WeakestPrecondition.func
-    (fun _ => True) (fun _ => False) (fun _ _ => True) (fun _ _ _ _ _ => False)
+    (fun _ => True) (fun _ => False) (fun _ _ => True) l (fun _ _ _ _ _ => False)
     (@swap BasicC64Syntax.params) t m (a_addr::b_addr::nil)
     (fun t' m' rets => t=t' /\ (sep (ptsto 1 a_addr b) (sep (ptsto 1 b_addr a) R)) m' /\ rets = nil).
 Proof.
@@ -104,13 +104,14 @@ Proof.
 Qed.
 
 Lemma swap_swap_ok : 
-  forall a_addr a b_addr b (m:map.rep (value:=@Semantics.byte _)) R t,
+  forall l a_addr a b_addr b (m:map.rep (value:=@Semantics.byte _)) R t,
     (sep (ptsto 1 a_addr a) (sep (ptsto 1 b_addr b) R)) m ->
   WeakestPrecondition.func
-    (fun _ => True) (fun _ => False) (fun _ _ => True) (WeakestPrecondition.call (fun _ => True) (fun _ => False) (fun _ _ => True) [("swap", (@swap BasicC64Syntax.params))])
+    (fun _ => True) (fun _ => False) (fun _ _ => True) l (WeakestPrecondition.call (fun _ => True) (fun _ => False) (fun _ _ => True) l [("swap", (@swap BasicC64Syntax.params))])
     (@swap_swap BasicC64Syntax.params) t m (a_addr::b_addr::nil)
     (fun t' m' rets => t=t' /\ (sep (ptsto 1 a_addr a) (sep (ptsto 1 b_addr b) R)) m' /\ rets = nil).
 Proof.
+  Print WeakestPrecondition.func.
   intros. rename H into Hm.
   eexists.
   eexists.
@@ -121,6 +122,7 @@ Proof.
   eexists.
   eexists.
   eexists.
+  unfold WeakestPrecondition.list_map.
   intros. eapply WeakestPreconditionProperties.Proper_func.
   6: eapply swap_ok.
   1,2,3,4,5 : cbv [Morphisms.pointwise_relation trace Basics.flip Basics.impl Morphisms.respectful]; try solve [typeclasses eauto with core].
diff --git a/bedrock2/src/Semantics.v b/bedrock2/src/Semantics.v
index e766564bc..6dc72e69e 100644
--- a/bedrock2/src/Semantics.v
+++ b/bedrock2/src/Semantics.v
@@ -19,12 +19,12 @@ Class parameters := {
   mem :> map word byte;
   locals :> map varname word;
 
-  funname_eqb : funname -> funname -> bool
+  globname_eqb : globname -> globname -> bool
 }.
 
 Section semantics.
   Context {pp : unique! parameters}.
-  
+
   Fixpoint load_rec (sz : nat) (m:mem) (a:word) : option word :=
     match sz with
     | O => Some word_zero
diff --git a/bedrock2/src/StringNamesSyntax.v b/bedrock2/src/StringNamesSyntax.v
index 87635dafd..9f7c9302f 100644
--- a/bedrock2/src/StringNamesSyntax.v
+++ b/bedrock2/src/StringNamesSyntax.v
@@ -9,7 +9,7 @@ Class parameters := {
 
 Instance make (p : parameters) : Syntax.parameters := {|
   Syntax.varname := string;
-  Syntax.funname := string;
+  Syntax.globname := string;
 
   Syntax.actname := actname;
   Syntax.bopname := bopname;
diff --git a/bedrock2/src/Syntax.v b/bedrock2/src/Syntax.v
index f5a11c423..023225ed6 100644
--- a/bedrock2/src/Syntax.v
+++ b/bedrock2/src/Syntax.v
@@ -4,7 +4,7 @@ Require Import Coq.Numbers.BinNums.
   
 Class parameters := {
   varname : Set;
-  funname : Set;
+  globname : Set;
   actname : Set;
   bopname : Set;
 }.
@@ -15,6 +15,7 @@ Module expr. Section expr.
   Inductive expr  : Type :=
   | literal (v: Z)
   | var (x: varname)
+  | global (_ : globname)
   | load (access_size_in_bytes:Z) (addr:expr)
   | op (op: bopname) (e1 e2: expr).
 End expr. End expr. Notation expr := expr.expr.
@@ -28,6 +29,6 @@ Module cmd. Section cmd.
   | cond (condition : expr) (nonzero_branch zero_branch : cmd)
   | seq (s1 s2: cmd)
   | while (test : expr) (body : cmd)
-  | call (binds : list varname) (function : funname) (args: list expr)
+  | call (binds : list varname) (function : expr) (args: list expr)
   | interact (binds : list varname) (action : actname) (args: list expr).
 End cmd. End cmd. Notation cmd := cmd.cmd.
\ No newline at end of file
diff --git a/bedrock2/src/ToCString.v b/bedrock2/src/ToCString.v
index 4a42e780f..23cf53bce 100644
--- a/bedrock2/src/ToCString.v
+++ b/bedrock2/src/ToCString.v
@@ -11,7 +11,7 @@ Class parameters := {
   c_lit : Z -> String.string;
   c_bop : string -> bopname -> string -> string;
   c_var : varname -> String.string;
-  c_fun : funname -> String.string;
+  c_glob : globname -> String.string;
   c_act : list varname -> actname -> list String.string -> string;
 }.
 
@@ -33,6 +33,7 @@ Section ToCString.
     match e with
     | expr.literal v => c_lit v
     | expr.var x => c_var x
+    | expr.global x => c_glob x
     | expr.load s ea => "*(" ++ c_size s ++ "*)(" ++ c_expr ea ++ ")"
     | expr.op op e1 e2 => c_bop ("(" ++ c_expr e1 ++ ")") op ("(" ++ c_expr e2 ++ ")")
     end.
@@ -79,13 +80,13 @@ Section ToCString.
     | cmd.skip =>
       indent ++ "/*skip*/" ++ LF
     | cmd.call args f es =>
-      indent ++ c_call (List.map c_var args) (c_fun f) (List.map c_expr es)
+      indent ++ c_call (List.map c_var args) (c_expr f) (List.map c_expr es)
     | cmd.interact binds action es =>
       indent ++ c_act binds action (List.map c_expr es)
     end%string.
 
-  Definition c_decl (rett : string) (args : list varname) (name : funname) (retptrs : list varname) : string :=
-    (rett ++ " " ++ c_fun name ++ "(" ++ concat ", " (
+  Definition c_decl (rett : string) (args : list varname) (name : globname) (retptrs : list varname) : string :=
+    (rett ++ " " ++ c_glob name ++ "(" ++ concat ", " (
                     List.map (fun a => "uintptr_t "++c_var a) args ++
                     List.map (fun r => "uintptr_t* "++c_var r) retptrs) ++
                   ")")%string.
diff --git a/bedrock2/src/Variables.v b/bedrock2/src/Variables.v
index 6e8fc56ac..dfac3ad76 100644
--- a/bedrock2/src/Variables.v
+++ b/bedrock2/src/Variables.v
@@ -6,8 +6,9 @@ Module expr. Section expr. Import Syntax.expr.
   Context {p : unique! Syntax.parameters}.
   Fixpoint vars (e : expr) : list varname :=
     match e with
-    | literal v => nil
+    | literal _ => nil
     | var x => cons x nil
+    | global _ => nil
     | load _ ea => vars ea
     | op _ e1 e2 => List.app (vars e1) (vars e2)
     end.
diff --git a/bedrock2/src/WeakestPrecondition.v b/bedrock2/src/WeakestPrecondition.v
index 4e0517c2e..48b9f95e1 100644
--- a/bedrock2/src/WeakestPrecondition.v
+++ b/bedrock2/src/WeakestPrecondition.v
@@ -5,6 +5,7 @@ Require Import Coq.ZArith.BinIntDef.
 Section WeakestPrecondition.
   Context {p : unique! Semantics.parameters}.
   Context (rely guarantee : trace -> Prop) (progress : trace -> trace -> Prop).
+  Variable resolver : globname -> option word.
 
   Definition literal v post : Prop :=
     bind_ex_Some v <- word_of_Z v; post v.
@@ -23,6 +24,8 @@ Section WeakestPrecondition.
         literal v post
       | expr.var x =>
         get l x post
+      | expr.global g =>
+        bind_ex_Some v <- resolver g ; post v
       | expr.op op e1 e2 =>
         expr e1 (fun v1 =>
         expr e2 (fun v2 =>
@@ -46,7 +49,7 @@ Section WeakestPrecondition.
   End WithF.
 
   Section WithFunctions.
-    Context (call : funname -> trace -> mem -> list word -> (trace -> mem -> list word -> Prop) -> Prop).
+    Context (call : globname -> mem -> list word -> (trace -> mem -> list word -> Prop) -> Prop).
     Fixpoint cmd (c : cmd) (t : trace) (m : mem) (l : locals)
              (post : trace -> mem -> locals -> Prop) {struct c} : Prop :=
       match c with
@@ -67,7 +70,7 @@ Section WeakestPrecondition.
       | cmd.seq c1 c2 =>
         cmd c1 t m l (fun t m l => cmd c2 t m l post)
       | cmd.while e c =>
-        exists measure (lt:measure->measure->Prop) (inv:measure->trace->mem->locals->Prop), 
+        exists measure (lt:measure->measure->Prop) (inv:measure->trace->mem->locals->Prop),
         Coq.Init.Wf.well_founded lt /\
         (exists v, inv v t m l) /\
         (forall v t m l, inv v t m l ->
@@ -75,11 +78,15 @@ Section WeakestPrecondition.
           (word_test b = true -> cmd c t m l (fun t' m l =>
             exists v', inv v' t' m l /\ (progress t' t \/ lt v' v))) /\
           (word_test b = false -> post t m l)))
-      | cmd.call binds fname arges =>
-        list_map (expr m l) arges (fun args =>
-        call fname t m args (fun t m rets =>
-          bind_ex_Some l <- map.putmany binds rets l;
-          post t m l))
+      | cmd.call binds f arges =>
+        match f with
+        | expr.global fname =>
+          list_map (expr m l) arges (fun args =>
+          call fname t m args (fun t m rets =>
+            bind_ex_Some l <- map.putmany binds rets l;
+            post t m l))
+        | _ => False (* function pointers are not supported *)
+        end
       | cmd.interact binds action arges =>
         list_map (expr m l) arges (fun args =>
         let output := (m, action, args) in
@@ -94,14 +101,14 @@ Section WeakestPrecondition.
       cmd call c t m l (fun t m l =>
         list_map (get l) outnames (fun rets =>
         post t m rets)).
-          
-  Fixpoint call (functions : list (funname * (list varname * list varname * cmd.cmd)))
-                (fname : funname) (t : trace) (m : mem) (args : list word)
+
+  Fixpoint call (functions : list (globname * (list varname * list varname * cmd.cmd)))
+                (fname : globname) (t : trace) (m : mem) (args : list word)
                 (post : trace -> mem -> list word -> Prop) {struct functions} : Prop :=
     match functions with
     | nil => False
     | cons (f, decl) functions =>
-      if funname_eqb f fname
+      if globname_eqb f fname
       then func (call functions) decl t m args post
       else call functions fname t m args post
     end.
diff --git a/bedrock2/src/WeakestPreconditionProperties.v b/bedrock2/src/WeakestPreconditionProperties.v
index 7b0d04bf6..554bc0c4e 100644
--- a/bedrock2/src/WeakestPreconditionProperties.v
+++ b/bedrock2/src/WeakestPreconditionProperties.v
@@ -24,7 +24,9 @@ Section WeakestPrecondition.
   Global Instance Proper_store : Proper (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ ((pointwise_relation _ Basics.impl) ==> Basics.impl))))) WeakestPrecondition.store.
   Proof. cbv [WeakestPrecondition.load]; cbv [Proper respectful pointwise_relation Basics.impl]; firstorder idtac. Qed.
 
-  Global Instance Proper_expr : Proper (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ ((pointwise_relation _ Basics.impl) ==> Basics.impl)))) WeakestPrecondition.expr.
+(*
+  Global Instance Proper_expr
+  : Proper (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ ((pointwise_relation _ Basics.impl) ==> Basics.impl)))) WeakestPrecondition.expr.
   Proof.
     cbv [Proper respectful pointwise_relation Basics.impl]; ind_on Syntax.expr.expr;
       cbn in *; intuition (try typeclasses eauto with core).
@@ -32,6 +34,7 @@ Section WeakestPrecondition.
     eapply Proper_get; eauto.
     { eapply IHa1; eauto; intuition idtac. eapply Proper_load; eauto using Proper_load. }
   Qed.
+*)
 
   Global Instance Proper_list_map {A B} :
     Proper ((pointwise_relation _ (pointwise_relation _ Basics.impl ==> Basics.impl)) ==> pointwise_relation _ (pointwise_relation _ Basics.impl ==> Basics.impl)) (WeakestPrecondition.list_map (A:=A) (B:=B)).
@@ -39,7 +42,8 @@ Section WeakestPrecondition.
     cbv [Proper respectful pointwise_relation Basics.impl]; ind_on (list A);
       cbn in *; intuition (try typeclasses eauto with core).
   Qed.
- 
+
+(* 
   Global Instance Proper_cmd :
     Proper (
      (pointwise_relation _ (Basics.flip Basics.impl)) ==> (
@@ -167,4 +171,5 @@ Section WeakestPrecondition.
     try solve [typeclasses eauto with core].
     eauto.
   Qed.
+*)
 End WeakestPrecondition.
\ No newline at end of file
diff --git a/bedrock2/src/ZNamesSyntax.v b/bedrock2/src/ZNamesSyntax.v
index 956093361..b2277a530 100644
--- a/bedrock2/src/ZNamesSyntax.v
+++ b/bedrock2/src/ZNamesSyntax.v
@@ -4,7 +4,7 @@ Require Import bedrock2.Basic_bopnames.
 
 Instance ZNames : Syntax.parameters := {|
   Syntax.varname := Z;
-  Syntax.funname := Z;
+  Syntax.globname := Z;
 
   Syntax.actname := Empty_set;
   Syntax.bopname := bopname;

From 4dd974a45ea9ee9759e9eca81d97cc1710a8e18c Mon Sep 17 00:00:00 2001
From: Gregory Malecha <gmalecha@gmail.com>
Date: Mon, 10 Sep 2018 14:44:39 -0400
Subject: [PATCH 2/8] allow for recursive functions.

---
 bedrock2/src/BasicC64Semantics.v   |  2 +-
 bedrock2/src/Semantics.v           |  5 +--
 bedrock2/src/WeakestPrecondition.v | 71 +++++++++++++++++++++++-------
 3 files changed, 59 insertions(+), 19 deletions(-)

diff --git a/bedrock2/src/BasicC64Semantics.v b/bedrock2/src/BasicC64Semantics.v
index 2c5ad0f02..a610fe566 100644
--- a/bedrock2/src/BasicC64Semantics.v
+++ b/bedrock2/src/BasicC64Semantics.v
@@ -33,5 +33,5 @@ Instance parameters : parameters := {|
   (* TODO: faster maps *)
   mem := UnorderedList.map {| UnorderedList.key_eqb a b := if Word.weq a b then true else false |};
   locals := UnorderedList.map {| UnorderedList.key_eqb := String.eqb |};
-  globname_eqb := String.eqb;
+  word_eqb := @Word.weqb 64
 |}.
diff --git a/bedrock2/src/Semantics.v b/bedrock2/src/Semantics.v
index 6dc72e69e..eaf65f340 100644
--- a/bedrock2/src/Semantics.v
+++ b/bedrock2/src/Semantics.v
@@ -9,6 +9,7 @@ Class parameters := {
   word_succ : word -> word;
   word_test : word -> bool;
   word_of_Z : BinNums.Z -> option word;
+  word_eqb : word -> word -> bool;
   interp_binop : bopname -> word -> word -> word;
 
   byte : Type;
@@ -17,9 +18,7 @@ Class parameters := {
   split : nat -> word -> byte * word;
 
   mem :> map word byte;
-  locals :> map varname word;
-
-  globname_eqb : globname -> globname -> bool
+  locals :> map varname word
 }.
 
 Section semantics.
diff --git a/bedrock2/src/WeakestPrecondition.v b/bedrock2/src/WeakestPrecondition.v
index 48b9f95e1..cf0ddee60 100644
--- a/bedrock2/src/WeakestPrecondition.v
+++ b/bedrock2/src/WeakestPrecondition.v
@@ -49,7 +49,7 @@ Section WeakestPrecondition.
   End WithF.
 
   Section WithFunctions.
-    Context (call : globname -> mem -> list word -> (trace -> mem -> list word -> Prop) -> Prop).
+    Context (call : word -> trace -> mem -> list word -> (trace -> mem -> list word -> Prop) -> Prop).
     Fixpoint cmd (c : cmd) (t : trace) (m : mem) (l : locals)
              (post : trace -> mem -> locals -> Prop) {struct c} : Prop :=
       match c with
@@ -79,14 +79,11 @@ Section WeakestPrecondition.
             exists v', inv v' t' m l /\ (progress t' t \/ lt v' v))) /\
           (word_test b = false -> post t m l)))
       | cmd.call binds f arges =>
-        match f with
-        | expr.global fname =>
-          list_map (expr m l) arges (fun args =>
-          call fname t m args (fun t m rets =>
-            bind_ex_Some l <- map.putmany binds rets l;
-            post t m l))
-        | _ => False (* function pointers are not supported *)
-        end
+        list_map (expr m l) arges (fun args =>
+        expr m l f (fun fname =>
+        call fname t m args (fun t m rets =>
+          bind_ex_Some l <- map.putmany binds rets l;
+          post t m l)))
       | cmd.interact binds action arges =>
         list_map (expr m l) arges (fun args =>
         let output := (m, action, args) in
@@ -96,22 +93,66 @@ Section WeakestPrecondition.
       end.
   End WithFunctions.
 
-  Definition func call '(innames, outnames, c) (t : trace) (m : mem) (args : list word) (post : trace -> mem -> list word -> Prop) :=
+  Section list_lookup.
+    Context {A B : Type} (eqA : A -> A -> bool) (key : A).
+    Fixpoint list_lookup (ls : list (A * B)) : option B :=
+      match ls with
+      | nil => None
+      | cons (key', val) ls =>
+        if eqA key key' then Some val
+        else list_lookup ls
+      end.
+  End list_lookup.
+
+  Definition func call '(innames, outnames, c)
+             (t : trace) (m : mem) (args : list word)
+             (post : trace -> mem -> list word -> Prop) :=
       bind_ex_Some l <- map.putmany innames args map.empty;
       cmd call c t m l (fun t m l =>
         list_map (get l) outnames (fun rets =>
         post t m rets)).
 
-  Fixpoint call (functions : list (globname * (list varname * list varname * cmd.cmd)))
-                (fname : globname) (t : trace) (m : mem) (args : list word)
-                (post : trace -> mem -> list word -> Prop) {struct functions} : Prop :=
+  Section rec.
+    Variable (functions : list (word * (list varname * list varname * cmd.cmd))).
+
+    (* This definition allows for recursive functions using step-indexing.
+     *
+     * note(gmm): using this definition, you would likely write something like:
+     * `forall n, func (call_rec (3 + n)) ...` which would allow you to make
+     * calls to functions that have a call depth of at most 3.
+     * This is equivalent to the previous definition is you use the length
+     * of the rest of the list.
+     * in general, the `n` could be dependent (relationally or functionally)
+     * on both the arguments to the function and the heap.
+     *)
+    Fixpoint call_rec (n : nat)
+             (fname : word) (t : trace) (m : mem) (args : list word)
+             (post : trace -> mem -> list word -> Prop) {struct n} : Prop :=
+      match n with
+      | 0 => False
+      | S n =>
+        match list_lookup word_eqb fname functions with
+        | None => False
+        | Some decl => func (call_rec n) decl t m args post
+        end
+      end.
+
+    (* note(gmm): `call_rec` is monotone in `n` *)
+
+  End rec.
+
+  Fixpoint call
+           (functions : list (word * (list varname * list varname * cmd.cmd)))
+           (fname : word) (t : trace) (m : mem) (args : list word)
+           (post : trace -> mem -> list word -> Prop) {struct functions} : Prop :=
     match functions with
     | nil => False
     | cons (f, decl) functions =>
-      if globname_eqb f fname
+      if word_eqb f fname
       then func (call functions) decl t m args post
       else call functions fname t m args post
     end.
 
-  Definition program funcs main t m l post : Prop := cmd (call funcs) main t m l post.
+  Definition program funcs main t m l post : Prop :=
+    cmd (call funcs) main t m l post.
 End WeakestPrecondition.
\ No newline at end of file

From ae9de05bff74e67e2cc640ec7784644d56e02bd7 Mon Sep 17 00:00:00 2001
From: Gregory Malecha <gmalecha@gmail.com>
Date: Mon, 10 Sep 2018 15:53:57 -0400
Subject: [PATCH 3/8] very rough sketch of what a compilation unit might look
 like.

---
 bedrock2/src/CompilationUnit.v | 102 +++++++++++++++++++++++++++++++++
 1 file changed, 102 insertions(+)
 create mode 100644 bedrock2/src/CompilationUnit.v

diff --git a/bedrock2/src/CompilationUnit.v b/bedrock2/src/CompilationUnit.v
new file mode 100644
index 000000000..9edefe6bd
--- /dev/null
+++ b/bedrock2/src/CompilationUnit.v
@@ -0,0 +1,102 @@
+Require Import Coq.Strings.String.
+Require Import Coq.ZArith.BinIntDef.
+Require Import ExtLib.Data.HList.
+Require Import ExtLib.Data.Fin.
+Require Import ExtLib.Data.Map.FMapAList.
+Require Import bedrock2.Macros bedrock2.Notations bedrock2.Map.
+Require Import bedrock2.Syntax.
+Require Import bedrock2.Semantics.
+
+(* Compilation units should be fairly simple
+ * - the basic idea is that you have "externals", "internals", and "exports"
+ * - definitions can call externals and internals
+ * - exports must be a subset of external and internal
+ * - in the module-level semantics, one type of interaction needs to be
+ *   external call.
+ * - note(gmm): we don't have to support recursive linking if we want to keep
+ *   the terminating semantics.
+ *)
+
+Module module.
+Section with_parameters.
+  Context {p : Syntax.parameters}.
+
+  Variant data : Set :=
+  | Data (_ : list Z).
+
+  Variant definition : Type :=
+  | X (_ : list data)
+  | Function (_ : list varname * list varname * Syntax.cmd).
+
+
+  (* note(gmm): this could be made more uniform with the rest of the development
+   * if we used `map`.
+   *)
+  Record module : Type :=
+  { imports     : list globname
+  ; internal    : list globname
+  ; exports     : list globname
+  ; definitions : list (globname * definition)
+  }.
+
+End with_parameters.
+End module.
+
+(* the meaning of a module is a function of the meaning of the imports to the
+ * meaning of the outputs.
+ * note(gmm): an alternative way to represent this to treat calls to imports
+ * as actions.
+ *)
+
+Require Import bedrock2.WeakestPrecondition.
+
+Section module_semantics.
+  Variable p : Semantics.parameters.
+  Variable resolver : globname -> option word.
+
+  Definition func_meaning : Type :=
+    (trace -> Prop) ->
+    (trace -> Prop) ->
+    (trace -> trace -> Prop) ->
+    trace ->
+    mem ->
+    list word ->
+    (trace -> mem -> list word -> Prop) -> Prop.
+
+  Variables (mod : module.module)
+            (denoteImports : globname -> func_meaning).
+
+  Definition functions : list _ :=
+    (fix functions ls :=
+       match ls with
+       | nil => nil
+       | cons (a, module.Function b) ls =>
+         match resolver a with
+         | Some a => cons (a,b) (functions ls)
+         | None => functions ls
+         end
+       | cons _ ls => functions ls
+       end) mod.(module.definitions).
+
+  Definition module_definitions
+             (g : globname)
+  : func_meaning.
+  refine (fun rely guarantee progress t mem args post =>
+            exists body, List.In (g, body) mod.(module.definitions) /\
+            match body with
+            | module.Function body =>
+              exists n,
+              WeakestPrecondition.func rely guarantee progress resolver
+                 (fun w t mem args post =>
+                    exists g, resolver g = Some w /\
+                           (List.In g mod.(module.imports) /\
+                            denoteImports g rely guarantee progress t mem args post)
+                         \/ call_rec rely guarantee progress resolver
+                                    functions n w t mem args post)
+                 body
+                 t mem args post
+            | _ => False
+            end).
+  Defined.
+
+End module_semantics.
\ No newline at end of file

From bafffad397701f359dbdfacc81511beabf66d755 Mon Sep 17 00:00:00 2001
From: Gregory Malecha <gmalecha@gmail.com>
Date: Mon, 10 Sep 2018 15:56:03 -0400
Subject: [PATCH 4/8] only export the exports

---
 bedrock2/src/CompilationUnit.v | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/bedrock2/src/CompilationUnit.v b/bedrock2/src/CompilationUnit.v
index 9edefe6bd..7f08a9d13 100644
--- a/bedrock2/src/CompilationUnit.v
+++ b/bedrock2/src/CompilationUnit.v
@@ -78,8 +78,7 @@ Section module_semantics.
        | cons _ ls => functions ls
        end) mod.(module.definitions).
 
-  Definition module_definitions
-             (g : globname)
+  Definition module_definitions (g : globname)
   : func_meaning.
   refine (fun rely guarantee progress t mem args post =>
             exists body, List.In (g, body) mod.(module.definitions) /\
@@ -99,4 +98,10 @@ Section module_semantics.
             end).
   Defined.
 
+  Definition module (g : globname)
+  : func_meaning :=
+    fun rely guarantee progress t mem args post =>
+      List.In g mod.(module.exports) /\
+      module_definitions g rely guarantee progress t mem args post.
+
 End module_semantics.
\ No newline at end of file

From c8c1d75e18ba883c84fe6afe68d0912a2abb186a Mon Sep 17 00:00:00 2001
From: Gregory Malecha <gmalecha@gmail.com>
Date: Mon, 10 Sep 2018 22:14:29 -0400
Subject: [PATCH 5/8] reverting function pointers.

---
 bedrock2/src/CompilationUnit.v     | 3 ---
 bedrock2/src/Examples/Swap.v       | 4 ++--
 bedrock2/src/Syntax.v              | 4 ++--
 bedrock2/src/ToCString.v           | 2 +-
 bedrock2/src/WeakestPrecondition.v | 8 +++++---
 5 files changed, 10 insertions(+), 11 deletions(-)

diff --git a/bedrock2/src/CompilationUnit.v b/bedrock2/src/CompilationUnit.v
index 7f08a9d13..8aa8cec01 100644
--- a/bedrock2/src/CompilationUnit.v
+++ b/bedrock2/src/CompilationUnit.v
@@ -1,8 +1,5 @@
 Require Import Coq.Strings.String.
 Require Import Coq.ZArith.BinIntDef.
-Require Import ExtLib.Data.HList.
-Require Import ExtLib.Data.Fin.
-Require Import ExtLib.Data.Map.FMapAList.
 Require Import bedrock2.Macros bedrock2.Notations bedrock2.Map.
 Require Import bedrock2.Syntax.
 Require Import bedrock2.Semantics.
diff --git a/bedrock2/src/Examples/Swap.v b/bedrock2/src/Examples/Swap.v
index c564a7a95..3aa7eb6b0 100644
--- a/bedrock2/src/Examples/Swap.v
+++ b/bedrock2/src/Examples/Swap.v
@@ -16,8 +16,8 @@ Section bsearch.
   )).
 
   Definition swap_swap : list varname * list varname * cmd := (("a"::"b"::nil), nil, bedrock_func_body:(
-    cmd.call nil (expr.global "swap") (var "a"::var "b"::nil);
-    cmd.call nil (expr.global "swap") (var "a"::var "b"::nil)
+    cmd.call nil "swap" (var "a"::var "b"::nil);
+    cmd.call nil "swap" (var "a"::var "b"::nil)
   )).
 End bsearch.
 
diff --git a/bedrock2/src/Syntax.v b/bedrock2/src/Syntax.v
index 023225ed6..ccfc0d1b2 100644
--- a/bedrock2/src/Syntax.v
+++ b/bedrock2/src/Syntax.v
@@ -1,7 +1,7 @@
 Require Import bedrock2.Macros.
 
 Require Import Coq.Numbers.BinNums.
-  
+
 Class parameters := {
   varname : Set;
   globname : Set;
@@ -29,6 +29,6 @@ Module cmd. Section cmd.
   | cond (condition : expr) (nonzero_branch zero_branch : cmd)
   | seq (s1 s2: cmd)
   | while (test : expr) (body : cmd)
-  | call (binds : list varname) (function : expr) (args: list expr)
+  | call (binds : list varname) (function : globname) (args: list expr)
   | interact (binds : list varname) (action : actname) (args: list expr).
 End cmd. End cmd. Notation cmd := cmd.cmd.
\ No newline at end of file
diff --git a/bedrock2/src/ToCString.v b/bedrock2/src/ToCString.v
index 23cf53bce..248cc9288 100644
--- a/bedrock2/src/ToCString.v
+++ b/bedrock2/src/ToCString.v
@@ -80,7 +80,7 @@ Section ToCString.
     | cmd.skip =>
       indent ++ "/*skip*/" ++ LF
     | cmd.call args f es =>
-      indent ++ c_call (List.map c_var args) (c_expr f) (List.map c_expr es)
+      indent ++ c_call (List.map c_var args) (c_glob f) (List.map c_expr es)
     | cmd.interact binds action es =>
       indent ++ c_act binds action (List.map c_expr es)
     end%string.
diff --git a/bedrock2/src/WeakestPrecondition.v b/bedrock2/src/WeakestPrecondition.v
index cf0ddee60..6535d4299 100644
--- a/bedrock2/src/WeakestPrecondition.v
+++ b/bedrock2/src/WeakestPrecondition.v
@@ -7,6 +7,8 @@ Section WeakestPrecondition.
   Context (rely guarantee : trace -> Prop) (progress : trace -> trace -> Prop).
   Variable resolver : globname -> option word.
 
+  Definition global g post : Prop :=
+    bind_ex_Some v <- resolver g; post v.
   Definition literal v post : Prop :=
     bind_ex_Some v <- word_of_Z v; post v.
   Definition get (l : locals) (x : varname) (post : word -> Prop) : Prop :=
@@ -25,7 +27,7 @@ Section WeakestPrecondition.
       | expr.var x =>
         get l x post
       | expr.global g =>
-        bind_ex_Some v <- resolver g ; post v
+        global g post
       | expr.op op e1 e2 =>
         expr e1 (fun v1 =>
         expr e2 (fun v2 =>
@@ -78,9 +80,9 @@ Section WeakestPrecondition.
           (word_test b = true -> cmd c t m l (fun t' m l =>
             exists v', inv v' t' m l /\ (progress t' t \/ lt v' v))) /\
           (word_test b = false -> post t m l)))
-      | cmd.call binds f arges =>
+      | cmd.call binds fname arges =>
         list_map (expr m l) arges (fun args =>
-        expr m l f (fun fname =>
+        global fname (fun fname =>
         call fname t m args (fun t m rets =>
           bind_ex_Some l <- map.putmany binds rets l;
           post t m l)))

From 8e9acb2468385e6cbda3169ef60ca269bd4ea691 Mon Sep 17 00:00:00 2001
From: Gregory Malecha <gmalecha@gmail.com>
Date: Mon, 10 Sep 2018 22:30:23 -0400
Subject: [PATCH 6/8] porting ExprImp.

---
 compiler/src/ExprImp.v | 48 ++++++++++++++++++++++++------------------
 1 file changed, 28 insertions(+), 20 deletions(-)

diff --git a/compiler/src/ExprImp.v b/compiler/src/ExprImp.v
index 1c8fb761e..5edbf885d 100644
--- a/compiler/src/ExprImp.v
+++ b/compiler/src/ExprImp.v
@@ -20,24 +20,27 @@ Section ExprImp1.
   Context {p : unique! Semantics.parameters}.
 
   Notation mword := (@Semantics.word p).
-  Context {MW: MachineWidth mword}.  
-  
+  Context {MW: MachineWidth mword}.
+
   Notation var := (@varname (@syntax p)).
-  Notation func := (@funname (@syntax p)).
+  Notation glob := (@globname (@syntax p)).
 
   Context {stateMap: MapFunctions var (mword)}.
   Notation state := (map var mword).
   Context {varset: SetFunctions var}.
   Notation vars := (set var).
 
+  Variable resolve : glob -> option word.
+
   Hypothesis actname_empty: actname = Empty_set.
-  
+
   Ltac state_calc := state_calc_generic (@varname (@syntax p)) (@Semantics.word p).
   Ltac set_solver := set_solver_generic (@varname (@syntax p)).
 
   Fixpoint eval_expr(st: state)(e: expr): option mword :=
     match e with
     | expr.literal v => Return (ZToReg v)
+    | expr.global g => resolve g
     | expr.var x => get st x
     | expr.load x a => None (* TODO *)
     | expr.op op e1 e2 =>
@@ -47,8 +50,8 @@ Section ExprImp1.
     end.
 
   Section WithEnv.
-    Context {funcMap: MapFunctions func (list var * list var * cmd)}.
-    Notation env := (map func (list var * list var * cmd)).
+    Context {funcMap: MapFunctions glob (list var * list var * cmd)}.
+    Notation env := (map glob (list var * list var * cmd)).
     Context (e: env).
 
     Fixpoint eval_cmd(f: nat)(st: state)(m: mem)(s: cmd): option (state * mem) :=
@@ -100,6 +103,7 @@ Section ExprImp1.
     Fixpoint expr_size(e: expr): nat :=
       match e with
       | expr.literal _ => 8
+      | expr.global _ => 8
       | expr.load _ e => S (expr_size e)
       | expr.var _ => 1
       | expr.op op e1 e2 => S (S (expr_size e1 + expr_size e2))
@@ -145,7 +149,7 @@ Section ExprImp1.
     Lemma invert_eval_cond: forall f st1 m1 p2 cond bThen bElse,
       eval_cmd (S f) st1 m1 (cmd.cond cond bThen bElse) = Some p2 ->
       exists cv,
-        eval_expr st1 cond = Some cv /\ 
+        eval_expr st1 cond = Some cv /\
         (cv <> ZToReg 0 /\ eval_cmd f st1 m1 bThen = Some p2 \/
          cv = ZToReg 0  /\ eval_cmd f st1 m1 bElse = Some p2).
     Proof. inversion_lemma. Qed.
@@ -154,7 +158,7 @@ Section ExprImp1.
       eval_cmd (S f) st1 m1 (cmd.while cond body) = Some p3 ->
       exists cv,
         eval_expr st1 cond = Some cv /\
-        (cv <> ZToReg 0 /\ (exists st2 m2, eval_cmd f st1 m1 body = Some (st2, m2) /\ 
+        (cv <> ZToReg 0 /\ (exists st2 m2, eval_cmd f st1 m1 body = Some (st2, m2) /\
                                      eval_cmd f st2 m2 (cmd.while cond body) = Some p3) \/
          cv = ZToReg 0 /\ p3 = (st1, m1)).
     Proof. inversion_lemma. Qed.
@@ -192,12 +196,13 @@ Section ExprImp1.
   Fixpoint allVars_expr(e: expr): list var :=
     match e with
     | expr.literal v => []
+    | expr.global v => []
     | expr.var x => [x]
     | expr.load nbytes e => allVars_expr e
     | expr.op op e1 e2 => (allVars_expr e1) ++ (allVars_expr e2)
     end.
 
-  Fixpoint allVars_cmd(s: cmd): list var := 
+  Fixpoint allVars_cmd(s: cmd): list var :=
     match s with
     | cmd.store _ a e => (allVars_expr a) ++ (allVars_expr e)
     | cmd.set v e => v :: allVars_expr e
@@ -211,7 +216,7 @@ Section ExprImp1.
 
   (* Returns a static approximation of the set of modified vars.
      The returned set might be too big, but is guaranteed to include all modified vars. *)
-  Fixpoint modVars(s: cmd): vars := 
+  Fixpoint modVars(s: cmd): vars :=
     match s with
     | cmd.store _ _ _ => empty_set
     | cmd.set v _ => singleton_set v
@@ -252,7 +257,7 @@ End ExprImp1.
 
 Ltac invert_eval_cmd :=
   lazymatch goal with
-  | E: eval_cmd _ (S ?fuel) _ _ ?s = Some _ |- _ =>
+  | E: eval_cmd _ _ (S ?fuel) _ _ ?s = Some _ |- _ =>
     destruct s;
     [ apply invert_eval_skip in E
     | apply invert_eval_set in E
@@ -263,7 +268,7 @@ Ltac invert_eval_cmd :=
     | apply invert_eval_call in E
     | apply invert_eval_interact in E ];
     deep_destruct E;
-    [ let x := fresh "Case_skip" in pose proof tt as x; move x at top 
+    [ let x := fresh "Case_skip" in pose proof tt as x; move x at top
     | let x := fresh "Case_set" in pose proof tt as x; move x at top
     | let x := fresh "Case_store" in pose proof tt as x; move x at top
     | let x := fresh "Case_cond_Then" in pose proof tt as x; move x at top
@@ -282,10 +287,10 @@ Section ExprImp2.
   Context {p : unique! Semantics.parameters}.
 
   Notation mword := (@Semantics.word p).
-  Context {MW: MachineWidth mword}.  
-  
+  Context {MW: MachineWidth mword}.
+
   Notation var := (@varname (@syntax p)).
-  Notation func := (@funname (@syntax p)).
+  Notation glob := (@globname (@syntax p)).
 
   Context {stateMap: MapFunctions var (mword)}.
   Notation state := (map var mword).
@@ -294,17 +299,20 @@ Section ExprImp2.
 
   (* TODO this one should be wrapped somewhere *)
   Context {varname_eq_dec: DecidableEq var}.
-  
+
   Hypothesis actname_empty: actname = Empty_set.
-  
+
   Ltac state_calc := state_calc_generic (@varname (@syntax p)) (@Semantics.word p).
   Ltac set_solver := set_solver_generic (@varname (@syntax p)).
 
-  Context {funcMap: MapFunctions func (list var * list var * @cmd (@syntax p))}.
-  Notation env := (map func (list var * list var * cmd)).
+  Variable resolver : glob -> option word.
+
+  Context {funcMap: MapFunctions glob (list var * list var * @cmd (@syntax p))}.
+  Notation env := (map glob (list var * list var * cmd)).
+
 
   Lemma modVarsSound: forall (e: env) fuel s initialS initialM finalS finalM,
-    eval_cmd e fuel initialS initialM s = Some (finalS, finalM) ->
+    eval_cmd resolver e fuel initialS initialM s = Some (finalS, finalM) ->
     only_differ initialS (modVars s) finalS.
   Proof.
     induction fuel; introv Ev.

From 2ad2788f258576bcffe3a576f215204aa331622d Mon Sep 17 00:00:00 2001
From: Gregory Malecha <gmalecha@gmail.com>
Date: Tue, 11 Sep 2018 20:49:10 -0400
Subject: [PATCH 7/8] fixing the broken proofs in the bedrock2 directory

- the automation needs some work right now.
---
 bedrock2/src/Examples/Swap.v                 | 58 ++++++++++++++------
 bedrock2/src/WeakestPreconditionProperties.v | 49 ++++++++++++-----
 2 files changed, 77 insertions(+), 30 deletions(-)

diff --git a/bedrock2/src/Examples/Swap.v b/bedrock2/src/Examples/Swap.v
index 3aa7eb6b0..26a2419ed 100644
--- a/bedrock2/src/Examples/Swap.v
+++ b/bedrock2/src/Examples/Swap.v
@@ -103,16 +103,33 @@ Proof.
   repeat t.
 Qed.
 
+Lemma skipn_here : forall {T} (l : list T), List.skipn 0 l = l.
+Proof. reflexivity. Qed.
+Lemma skipn_next : forall {T} n l (ls ls' : list T), List.skipn n ls = ls' -> List.skipn (S n) (l :: ls) = ls'.
+Proof. intros. subst. reflexivity. Qed.
+
+Ltac find_in_list :=
+  repeat first [ apply skipn_here
+               | apply skipn_next ].
+
+Lemma wp_call_resolve : forall r g p l funcs addr t m args post i body rest,
+    List.skipn i funcs = (addr, body) :: rest ->
+    WeakestPrecondition.func r g p l (WeakestPrecondition.call r g p l rest) body t m args post ->
+    WeakestPrecondition.call r g p l funcs addr t m args post.
+Proof.
+Admitted.
+
+
 Lemma swap_swap_ok : 
-  forall l a_addr a b_addr b (m:map.rep (value:=@Semantics.byte _)) R t,
+  forall l swap_addr a_addr a b_addr b (m:map.rep (value:=@Semantics.byte _)) R t,
+    l "swap" = Some swap_addr ->
     (sep (ptsto 1 a_addr a) (sep (ptsto 1 b_addr b) R)) m ->
   WeakestPrecondition.func
-    (fun _ => True) (fun _ => False) (fun _ _ => True) l (WeakestPrecondition.call (fun _ => True) (fun _ => False) (fun _ _ => True) l [("swap", (@swap BasicC64Syntax.params))])
+    (fun _ => True) (fun _ => False) (fun _ _ => True) l (WeakestPrecondition.call (fun _ => True) (fun _ => False) (fun _ _ => True) l [(swap_addr, (@swap BasicC64Syntax.params))])
     (@swap_swap BasicC64Syntax.params) t m (a_addr::b_addr::nil)
     (fun t' m' rets => t=t' /\ (sep (ptsto 1 a_addr a) (sep (ptsto 1 b_addr b) R)) m' /\ rets = nil).
 Proof.
-  Print WeakestPrecondition.func.
-  intros. rename H into Hm.
+  intros. rename H0 into Hm.
   eexists.
   eexists.
   eexists.
@@ -122,12 +139,17 @@ Proof.
   eexists.
   eexists.
   eexists.
-  unfold WeakestPrecondition.list_map.
-  intros. eapply WeakestPreconditionProperties.Proper_func.
-  6: eapply swap_ok.
-  1,2,3,4,5 : cbv [Morphisms.pointwise_relation trace Basics.flip Basics.impl Morphisms.respectful]; try solve [typeclasses eauto with core].
-  1,2: cycle 1.
-  refine ((?[sep]:@Lift1Prop.impl1 mem _ _) m Hm). reflexivity. (* TODO: ecancel *)
+  eexists.
+  eexists. eassumption.
+  intros.
+  eapply wp_call_resolve.
+  find_in_list.
+  eapply WeakestPreconditionProperties.Proper_func.
+  7: eapply swap_ok.
+  all: try reflexivity.
+  cbv [Morphisms.pointwise_relation trace Basics.flip Basics.impl Morphisms.respectful]; try solve [typeclasses eauto with core].
+  tauto.
+  2: refine ((?[sep]:@Lift1Prop.impl1 mem _ _) m Hm); reflexivity. (* TODO: ecancel *)
   intros ? m' ? (?&Hm'&?).
   clear Hm.
   clear m.
@@ -144,11 +166,16 @@ Proof.
   eexists.
   eexists.
   eexists.
-  intros. eapply WeakestPreconditionProperties.Proper_func.
-  6: eapply swap_ok.
-  1,2,3,4,5 : cbv [Morphisms.pointwise_relation trace Basics.flip Basics.impl Morphisms.respectful]; try solve [typeclasses eauto with core].
-  1,2: cycle 1.
-  refine ((?[sep]:@Lift1Prop.impl1 mem _ _) m Hm). reflexivity. (* TODO: ecancel *)
+  eexists.
+  eexists; [ eassumption | ].
+  eapply wp_call_resolve.
+  find_in_list.
+  eapply WeakestPreconditionProperties.Proper_func.
+  7: eapply swap_ok.
+  all: try reflexivity.
+  cbv [Morphisms.pointwise_relation trace Basics.flip Basics.impl Morphisms.respectful]; try solve [typeclasses eauto with core]; tauto.
+  2: refine ((?[sep]:@Lift1Prop.impl1 mem _ _) m Hm); reflexivity. (* TODO: ecancel *)
+  cbv [Morphisms.pointwise_relation trace Basics.flip Basics.impl Morphisms.respectful]; try solve [typeclasses eauto with core].
   intros ? m' ? (?&Hm'&?).
   clear Hm.
   clear m.
@@ -165,4 +192,3 @@ Proof.
   eassumption.
   eexists.
 Qed.
-  
\ No newline at end of file
diff --git a/bedrock2/src/WeakestPreconditionProperties.v b/bedrock2/src/WeakestPreconditionProperties.v
index 554bc0c4e..2f9e27387 100644
--- a/bedrock2/src/WeakestPreconditionProperties.v
+++ b/bedrock2/src/WeakestPreconditionProperties.v
@@ -3,6 +3,16 @@ Require bedrock2.WeakestPrecondition.
 
 Require Import Coq.Classes.Morphisms.
 
+Inductive Roption {T} : option T -> option T -> Prop :=
+| Rnone {x} : Roption None x
+| Rsome {x} : Roption (Some x) (Some x).
+
+Global Instance Reflexive_Roption {T} : Reflexive (@Roption T).
+Proof. compute. destruct x; constructor. Qed.
+
+Global Instance Transitive_Roption {T} : Transitive (@Roption T).
+Proof. compute. destruct 1; inversion 1; subst; auto. constructor. Qed.
+
 Section WeakestPrecondition.
   Context {p : unique! Semantics.parameters}.
 
@@ -18,23 +28,30 @@ Section WeakestPrecondition.
   Global Instance Proper_get : Proper (pointwise_relation _ (pointwise_relation _ ((pointwise_relation _ Basics.impl) ==> Basics.impl))) WeakestPrecondition.get.
   Proof. cbv [WeakestPrecondition.get]; cbv [Proper respectful pointwise_relation Basics.impl]; firstorder idtac. Qed.
 
+  Global Instance Proper_global : Proper ((pointwise_relation _ Roption) ==> (pointwise_relation _ ((pointwise_relation _ Basics.impl) ==> Basics.impl))) WeakestPrecondition.global.
+  Proof.
+    cbv [WeakestPrecondition.global]; cbv [Proper respectful pointwise_relation Basics.impl]; firstorder idtac.
+    destruct (H a); try congruence.
+    injection H1; clear H1; intros; subst.
+    eexists; split; eauto.
+  Qed.
+
   Global Instance Proper_load : Proper (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ ((pointwise_relation _ Basics.impl) ==> Basics.impl)))) WeakestPrecondition.load.
   Proof. cbv [WeakestPrecondition.load]; cbv [Proper respectful pointwise_relation Basics.impl]; firstorder idtac. Qed.
 
   Global Instance Proper_store : Proper (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ ((pointwise_relation _ Basics.impl) ==> Basics.impl))))) WeakestPrecondition.store.
   Proof. cbv [WeakestPrecondition.load]; cbv [Proper respectful pointwise_relation Basics.impl]; firstorder idtac. Qed.
 
-(*
   Global Instance Proper_expr
-  : Proper (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ ((pointwise_relation _ Basics.impl) ==> Basics.impl)))) WeakestPrecondition.expr.
+  : Proper (pointwise_relation _ Roption ==> (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ ((pointwise_relation _ Basics.impl) ==> Basics.impl))))) WeakestPrecondition.expr.
   Proof.
     cbv [Proper respectful pointwise_relation Basics.impl]; ind_on Syntax.expr.expr;
       cbn in *; intuition (try typeclasses eauto with core).
     eapply Proper_literal; eauto.
     eapply Proper_get; eauto.
+    eapply Proper_global; eauto.
     { eapply IHa1; eauto; intuition idtac. eapply Proper_load; eauto using Proper_load. }
   Qed.
-*)
 
   Global Instance Proper_list_map {A B} :
     Proper ((pointwise_relation _ (pointwise_relation _ Basics.impl ==> Basics.impl)) ==> pointwise_relation _ (pointwise_relation _ Basics.impl ==> Basics.impl)) (WeakestPrecondition.list_map (A:=A) (B:=B)).
@@ -43,19 +60,19 @@ Section WeakestPrecondition.
       cbn in *; intuition (try typeclasses eauto with core).
   Qed.
 
-(* 
   Global Instance Proper_cmd :
     Proper (
      (pointwise_relation _ (Basics.flip Basics.impl)) ==> (
      (pointwise_relation _ Basics.impl) ==> (
      (pointwise_relation _ (pointwise_relation _ Basics.impl)) ==> (
+     (pointwise_relation _ Roption) ==> (
      (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ ((pointwise_relation _ (pointwise_relation _ Basics.impl))) ==> Basics.impl)))) ==>
      pointwise_relation _ (
      pointwise_relation _ (
      pointwise_relation _ (
      pointwise_relation _ (
      (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ Basics.impl))) ==>
-     Basics.impl))))))))) WeakestPrecondition.cmd.
+     Basics.impl)))))))))) WeakestPrecondition.cmd.
   Proof.
     cbv [Proper respectful pointwise_relation Basics.flip Basics.impl]; ind_on Syntax.cmd.cmd;
       cbn in *; intuition (try typeclasses eauto with core).
@@ -67,7 +84,7 @@ Section WeakestPrecondition.
     { eapply IHa1; try solve [typeclasses eauto with core]. eapply H.
       intros. eapply IHa2; try solve [typeclasses eauto with core]. eapply H.
       eauto. }
-    { destruct H4 as (?&?&?&?&?&HH).
+    { destruct H5 as (?&?&?&?&?&HH).
       eassumption || eexists.
       eassumption || eexists.
       eassumption || eexists.
@@ -79,17 +96,18 @@ Section WeakestPrecondition.
       specialize (HH X Y Z T W).
       eapply Proper_expr; eauto; cbv [pointwise_relation Basics.impl]; intuition eauto 2.
       eapply IHa; eauto; cbn; intros.
-      destruct H7 as (v'&H7); exists v'.
+      destruct H8 as (v'&H8); exists v'.
       intuition eauto. }
     { eapply Proper_list_map; eauto; cbv [respectful pointwise_relation Basics.impl]; intuition eauto 2.
       { eapply Proper_expr; eauto. }
-      { eapply H2; eauto; firstorder eauto. } }
+      { eapply Proper_global; eauto. do 2 red. intros.
+        eapply H3; eauto; firstorder eauto. } }
     { eapply Proper_list_map; eauto; cbv [respectful pointwise_relation Basics.impl].
       { eapply Proper_expr; eauto. }
       intros.
-      edestruct H5.
+      edestruct H6.
       split; [solve [eauto]|]; intros.
-      destruct (H7 ltac:(eauto)); intuition eauto. }
+      destruct (H8 ltac:(eauto)); intuition eauto. }
   Qed.
 
   Global Instance Proper_func :
@@ -97,6 +115,7 @@ Section WeakestPrecondition.
      (pointwise_relation _ (Basics.flip Basics.impl)) ==> (
      (pointwise_relation _ Basics.impl) ==> (
      (pointwise_relation _ (pointwise_relation _ Basics.impl)) ==> (
+     (pointwise_relation _ Roption) ==>
      (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ ((pointwise_relation _ (pointwise_relation _ Basics.impl))) ==> Basics.impl)))) ==>
      pointwise_relation _ (
      pointwise_relation _ (
@@ -107,7 +126,7 @@ Section WeakestPrecondition.
   Proof.
     cbv [Proper respectful pointwise_relation Basics.flip Basics.impl  WeakestPrecondition.func]; intros.
     destruct a. destruct p0.
-    destruct H4; intuition idtac.
+    destruct H5; intuition idtac.
     eexists.
     split.
     eauto.
@@ -130,6 +149,7 @@ Section WeakestPrecondition.
      (pointwise_relation _ (Basics.flip Basics.impl)) ==> (
      (pointwise_relation _ Basics.impl) ==> (
      (pointwise_relation _ (pointwise_relation _ Basics.impl)) ==> (
+     pointwise_relation _ Roption ==>
      (pointwise_relation _ (
      (pointwise_relation _ (
      pointwise_relation _ (
@@ -138,10 +158,10 @@ Section WeakestPrecondition.
      (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ Basics.impl))) ==>
      Basics.impl))))))))))) WeakestPrecondition.call.
   Proof.
-    cbv [Proper respectful pointwise_relation Basics.impl]; ind_on (list (Syntax.funname * (list Syntax.varname * list Syntax.varname * Syntax.cmd.cmd)));
+    cbv [Proper respectful pointwise_relation Basics.impl]; ind_on (list (Semantics.word * (list Syntax.varname * list Syntax.varname * Syntax.cmd.cmd)));
       cbn in *; intuition (try typeclasses eauto with core).
     destruct a.
-    destruct (Semantics.funname_eqb f a1); eauto.
+    destruct (Semantics.word_eqb w a1); eauto.
     eapply Proper_func; 
       cbv [Proper respectful pointwise_relation Basics.flip Basics.impl  WeakestPrecondition.func];
       eauto.
@@ -152,6 +172,7 @@ Section WeakestPrecondition.
      (pointwise_relation _ (Basics.flip Basics.impl)) ==> (
      (pointwise_relation _ Basics.impl) ==> (
      (pointwise_relation _ (pointwise_relation _ Basics.impl)) ==> (
+     pointwise_relation _ Roption ==>
      pointwise_relation _ (
      pointwise_relation _ (
      pointwise_relation _ (
@@ -171,5 +192,5 @@ Section WeakestPrecondition.
     try solve [typeclasses eauto with core].
     eauto.
   Qed.
-*)
+
 End WeakestPrecondition.
\ No newline at end of file

From dd1f540eef04ebdc1c67de22299d94d1b75e9254 Mon Sep 17 00:00:00 2001
From: Gregory Malecha <gmalecha@gmail.com>
Date: Fri, 19 Oct 2018 15:08:08 -0400
Subject: [PATCH 8/8] verification condition for compilation units.

---
 bedrock2/src/WeakestPrecondition.v | 90 ++++++++++++++++++++++++++++++
 compiler/src/FlatImp.v             | 72 ++++++++++++------------
 compiler/src/FlattenExpr.v         |  7 ++-
 3 files changed, 132 insertions(+), 37 deletions(-)

diff --git a/bedrock2/src/WeakestPrecondition.v b/bedrock2/src/WeakestPrecondition.v
index 6535d4299..72b7b520b 100644
--- a/bedrock2/src/WeakestPrecondition.v
+++ b/bedrock2/src/WeakestPrecondition.v
@@ -155,6 +155,96 @@ Section WeakestPrecondition.
       else call functions fname t m args post
     end.
 
+  (* function specifications *)
+  Definition fspec : Type :=
+    trace -> mem -> list word -> (trace -> mem -> list word -> Prop) -> nat -> Prop.
+  (* the final natural number is the depth of the function stack that this
+   * function is allowed to make
+   *)
+
+  Definition to_spec (call : _ -> _ -> _ -> _ -> _ -> _ -> Prop) (gs : globname * fspec) : Prop :=
+    let '(g,s) := gs in
+    (exists addr, resolver g = Some addr /\
+             forall n, forall t m a post,
+                 s t m a post n -> call n addr t m a post).
+
+  Require Coq.Lists.List.
+
+  Definition specs call (ls : list (globname * fspec)) : Prop :=
+    List.Forall (to_spec call) ls.
+
+  Definition module
+    (functions : list (globname * fspec * (list varname * list varname * cmd.cmd)))
+  : Prop :=
+      forall call,
+        specs call (List.map (fun '(a,b,_) => (a,b)) functions) ->
+        @List.Forall (_ * fspec * _)
+                     (fun '(g,P,body) =>
+                        forall t m a q n, P t m a q n ->
+                                     func (match n with
+                                           | 0 => fun _ _ _ _ _ => False
+                                           | S n => call n
+                                           end) body t m a q) functions.
+
+(* demo(gmm):
+  Axiom word_to_nat : word -> nat.
+
+  Goal forall even odd n res sub,
+      let s : fspec :=
+           fun t m args q r =>
+             (* todo: how do recursive calls work? *)
+             match args return Prop with
+             | cons n nil => r >= word_to_nat n /\ q t m (cons word_zero nil)
+             | _ => False
+             end
+       in
+       let e := (even, s,
+                         (cons n nil, cons res nil,
+                           cmd.cond (expr.var n)
+                                    (cmd.set res (expr.literal 0))
+                                    (cmd.call (cons res nil) odd
+                                              (cons (expr.op sub (expr.var n) (expr.literal 1)) nil)))) in
+       let o := (odd, s, (cons n nil, cons res nil,
+                          cmd.cond (expr.var n)
+                                   (cmd.set res (expr.literal 0))
+                                   (cmd.call (cons res nil) even
+                                             (cons (expr.op sub (expr.var n) (expr.literal 1)) nil)))) in
+       module (cons e (cons o nil)).
+  Proof.
+    unfold module. simpl.
+    split; [ | split; [ | tauto ] ].
+    { (* proof of even assuming odd *)
+      intros.
+      destruct a; try contradiction.
+      destruct a; try contradiction.
+      inversion H; clear H; subst.
+      inversion H4; clear H4; subst. clear H3 H5.
+      red in H2. destruct H2 as [ ? [ ? ? ] ].
+      destruct H0.
+      repeat eexists.
+      eapply map.get_put_same.
+      instantiate (1:= word_zero).
+      admit.
+      subst.
+      erewrite map.get_put_same. reflexivity.
+      assumption.
+      erewrite map.get_put_same. reflexivity.
+      admit.
+      eassumption.
+      Require Import Coq.micromega.Lia.
+      destruct n0; [ admit | ].
+      eapply H1.
+      eexists. admit.
+      eexists. split.
+      reflexivity.
+      unfold get. eexists. erewrite map.get_put_same.
+      split; [ reflexivity | ]. eassumption. }
+    {
+*)
+
   Definition program funcs main t m l post : Prop :=
+    (* note(gmm): this should really just be something like:
+     *   exists s, module funcs s /\ ...the spec for main satisfies the wp
+     *)
     cmd (call funcs) main t m l post.
 End WeakestPrecondition.
\ No newline at end of file
diff --git a/compiler/src/FlatImp.v b/compiler/src/FlatImp.v
index 4e8e2eb23..09c8ce0f9 100644
--- a/compiler/src/FlatImp.v
+++ b/compiler/src/FlatImp.v
@@ -15,8 +15,8 @@ Section FlatImp1.
 
   Variable var: Set.
   Context {var_eq_dec: DecidableEq var}.
-  Variable func: Set.
-  Context {func_eq_dec: DecidableEq func}.
+  Variable glob: Set.
+  Context {glob_eq_dec: DecidableEq glob}.
 
   Context {stateMap: MapFunctions var mword}.
   Notation state := (map var mword).
@@ -29,18 +29,20 @@ Section FlatImp1.
     | SLoad(x: var)(a: var): stmt
     | SStore(a: var)(v: var): stmt
     | SLit(x: var)(v: Z): stmt
+    | SGlob (x : var) (v : glob) : stmt
     | SOp(x: var)(op: bopname)(y z: var): stmt
     | SSet(x y: var): stmt
     | SIf(cond: var)(bThen bElse: stmt): stmt
     | SLoop(body1: stmt)(cond: var)(body2: stmt): stmt
     | SSeq(s1 s2: stmt): stmt
     | SSkip: stmt
-    | SCall(binds: list var)(f: func)(args: list var).
+    | SCall(binds: list var)(f: glob)(args: list var).
 
   Section WithEnv.
-    Context {funcMap: MapFunctions func (list var * list var * stmt)}.
-    Notation env := (map func (list var * list var * stmt)).
+    Context {funcMap: MapFunctions glob (list var * list var * stmt)}.
+    Notation env := (map glob (list var * list var * stmt)).
     Context (e: env).
+    Variable resolve : glob -> option mword.
 
     (* If we want a bigstep evaluation relation, we either need to put
        fuel into the SLoop constructor, or give it as argument to eval *)
@@ -59,6 +61,12 @@ Section FlatImp1.
             Return (st, m)
         | SLit x v =>
             Return (put st x (ZToReg v), m)
+        | SGlob x v =>
+          match resolve v with
+          | None => None
+          | Some v =>
+            Return (put st x v, m)
+          end
         | SOp x op y z =>
             y <- get st y;
             z <- get st z;
@@ -186,6 +194,7 @@ Section FlatImp1.
     | SLoad x a => 1
     | SStore a v => 1
     | SLit x v => 8
+    | SGlob x v => 8
     | SOp x op y z => 2
     | SSet x y => 1
     | SIf cond bThen bElse => 1 + (rec bThen) + (rec bElse)
@@ -205,6 +214,7 @@ Section FlatImp1.
     | SLoad x y => singleton_set x
     | SStore x y => empty_set
     | SLit x v => singleton_set x
+    | SGlob x v => singleton_set x
     | SOp x op y z => singleton_set x
     | SSet x y => singleton_set x
     | SIf cond bThen bElse =>
@@ -222,6 +232,7 @@ Section FlatImp1.
     | SLoad x y => union (singleton_set x) (singleton_set y)
     | SStore x y => union (singleton_set x) (singleton_set y)
     | SLit x v => singleton_set x
+    | SGlob x v => singleton_set x
     | SOp x op y z => union (singleton_set x) (union (singleton_set y) (singleton_set z))
     | SSet x y => union (singleton_set x) (singleton_set y)
     | SIf cond bThen bElse =>
@@ -244,7 +255,7 @@ End FlatImp1.
 
 Ltac invert_eval_stmt :=
   lazymatch goal with
-  | E: eval_stmt _ _ _ (S ?fuel) _ _ ?s = Some _ |- _ =>
+  | E: eval_stmt _ _ _ _ (S ?fuel) _ _ ?s = Some _ |- _ =>
     destruct s;
     [ apply invert_eval_SLoad in E
     | apply invert_eval_SStore in E
@@ -289,53 +300,44 @@ Section FlatImp2.
 
   Variable var: Set.
   Context {var_eq_dec: DecidableEq var}.
-  Variable func: Set.
-  Context {func_eq_dec: DecidableEq func}.
+  Variable glob: Set.
+  Context {glob_eq_dec: DecidableEq glob}.
 
   Context {stateMap: MapFunctions var mword}.
   Notation state := (map var mword).
   Context {varset: SetFunctions var}.
   Notation vars := (set var).
 
-  Context {funcMap: MapFunctions func (list var * list var * stmt var func)}.
-  Notation env := (map func (list var * list var * stmt var func)).
+  Context {funcMap: MapFunctions glob (list var * list var * stmt var glob)}.
+  Notation env := (map glob (list var * list var * stmt var glob)).
 
   Ltac state_calc := state_calc_generic var mword.
 
-  Lemma increase_fuel_still_Success: forall fuel1 fuel2 (e: env) initialSt initialM s final,
+  Lemma increase_fuel_still_Success: forall resolver fuel1 fuel2 (e: env) initialSt initialM s final,
     fuel1 <= fuel2 ->
-    eval_stmt var func e fuel1 initialSt initialM s = Some final ->
-    eval_stmt var func e fuel2 initialSt initialM s = Some final.
+    eval_stmt var glob e resolver fuel1 initialSt initialM s = Some final ->
+    eval_stmt var glob e resolver fuel2 initialSt initialM s = Some final.
   Proof.
     induction fuel1; introv L Ev.
     - inversions Ev.
     - destruct fuel2; [omega|].
       assert (fuel1 <= fuel2) as F by omega. specialize IHfuel1 with (1 := F).
       destruct final as [finalSt finalM].
-      invert_eval_stmt; cbn in *;
-      repeat match goal with
-      | IH: _, H: _ |- _ =>
-          let IH' := fresh IH in pose proof IH as IH';
-          specialize IH' with (1 := H);
-          ensure_new IH'
-      end;
-      repeat match goal with
-      | H: _ = Some _ |- _ => rewrite H
-      end;
-      try congruence;
-      try simpl_if;
-      rewrite? (proj2 (reg_eqb_true _ _) eq_refl);
-      repeat match goal with
-             | H:     (@eq mword _ _)  |- _ => apply reg_eqb_eq in H; rewrite H
-             | H: not (@eq mword _ _)  |- _ => apply reg_eqb_ne in H; rewrite H
-             end;
-      rewrite? reg_eqb_eq by reflexivity;
-      eauto.
+      revert Ev. clear - IHfuel1.
+      simpl.
+      destruct s; intro;
+        repeat lazymatch goal with
+               | _ : match eval_stmt ?v ?g ?e ?r ?z ?x1 ?i ?b with _ => _ end = _ |- _ =>
+                 generalize (IHfuel1 e x1 i b) ;
+                   destruct (eval_stmt v g e r z x1 i b) ; [ let H := fresh in intro H ; specialize (H _ eq_refl) ; rewrite H ; clear H | congruence ]
+               | _ : match ?X with _ => _ end = _ |- _ =>
+                 destruct X; eauto
+               end; auto.
   Qed.
 
-  Lemma modVarsSound: forall fuel e s initialSt initialM finalSt finalM,
-    eval_stmt var func e fuel initialSt initialM s = Some (finalSt, finalM) ->
-    only_differ initialSt (modVars var func s) finalSt.
+  Lemma modVarsSound: forall resolver fuel e s initialSt initialM finalSt finalM,
+    eval_stmt var glob e resolver fuel initialSt initialM s = Some (finalSt, finalM) ->
+    only_differ initialSt (modVars var glob s) finalSt.
   Proof.
     induction fuel; introv Ev.
     - discriminate.
diff --git a/compiler/src/FlattenExpr.v b/compiler/src/FlattenExpr.v
index 57f3d5438..608d028b2 100644
--- a/compiler/src/FlattenExpr.v
+++ b/compiler/src/FlattenExpr.v
@@ -22,10 +22,10 @@ Section FlattenExpr.
 
   (* TODO this should be wrapped somewhere *)
   Context {varname_eq_dec: DecidableEq (@Syntax.varname (@Semantics.syntax p))}.
-  Context {funname_eq_dec: DecidableEq (@Syntax.funname (@Semantics.syntax p))}.
+  Context {globname_eq_dec: DecidableEq (@Syntax.globname (@Semantics.syntax p))}.
 
   Notation var := (@Syntax.varname (@Semantics.syntax p)).
-  Notation func := (@Syntax.funname (@Semantics.syntax p)).
+  Notation func := (@Syntax.globname (@Semantics.syntax p)).
 
   Context {stateMap: MapFunctions var mword}.
   Notation state := (map var mword).
@@ -59,6 +59,9 @@ Section FlattenExpr.
     | Syntax.expr.literal n =>
         let '(x, ngs') := genFresh ngs in
         (FlatImp.SLit x n, x, ngs')
+    | Syntax.expr.global n =>
+        let '(x, ngs') := genFresh ngs in
+        (FlatImp.SLit x n, x, ngs')
     | Syntax.expr.var x =>
         (* (FlatImp.SSkip, x, ngs)  would be simpler but doesn't satisfy the invariant that
            the returned var is in modVars of the returned statement *)