Proposal: Globals (pre-cursor to Compilation Units)

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;
+  word_eqb := @Word.weqb 64
 |}.

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;

bedrock2/src/CompilationUnit.v

@@ -0,0 +1,107 @@
+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.
+
+  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.

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

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,14 +18,12 @@ Class parameters := {
   split : nat -> word -> byte * word;
 
   mem :> map word byte;
-  locals :> map varname word;
-
-  funname_eqb : funname -> funname -> bool
+  locals :> map varname word
 }.
 
 Section semantics.
   Context {pp : unique! parameters}.
-  
+
   Fixpoint load_rec (sz : nat) (m:mem) (a:word) : option word :=
     match sz with
     | O => Some word_zero

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;

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.

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.

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.

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 : 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
@@ -67,19 +70,20 @@ 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 ->
           expr m l e (fun b =>
           (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 =>
+      | cmd.call binds f arges =>
         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))
+          post t m l)))
       | cmd.interact binds action arges =>
         list_map (expr m l) arges (fun args =>
         let output := (m, action, args) in
@@ -89,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 (funname * (list varname * list varname * cmd.cmd)))
-                (fname : funname) (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 funname_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.

bedrock2/src/WeakestPreconditionProperties.v

@@ -24,22 +24,26 @@ 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).
     eapply Proper_literal; eauto.
     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)).
   Proof.
     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.

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;