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,104 @@
+Require Import Coq.Strings.String.
+Require Import Coq.ZArith.BinIntDef.
+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

@@ -92,26 +92,44 @@ 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.
   intros. rename H into Hm.
   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 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) (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_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.
-  intros. rename H into Hm.
+  intros. rename H0 into Hm.
   eexists.
   eexists.
   eexists.
@@ -121,11 +139,17 @@ 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.
+  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.
@@ -142,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.
@@ -163,4 +192,3 @@ Proof.
   eassumption.
   eexists.
 Qed.
-

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

@@ -1,10 +1,10 @@
 Require Import bedrock2.Macros.
 
 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 : globname) (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_glob 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.