Add go globals implementation

new/golang/defn.v

@@ -1,4 +1,4 @@
 From Perennial.goose_lang Require Export lang notation.
 From New.golang.defn Require Export exception list typing noop loop struct mem
-  slice map string interface defer chan builtin array.
+  slice map string interface defer chan builtin array globals.
 Open Scope struct_scope.

new/golang/defn/globals.v

@@ -0,0 +1,24 @@
+From New.golang.defn Require Export mem typing.
+
+Module globals.
+Section defns.
+Context `{ffi_syntax}.
+
+Definition get : val :=
+  λ: "x", match: GlobalGet "x" with
+            SOME "x" => "x"
+          | NONE => #() #()
+          end.
+
+Definition put: val :=
+  λ: "x" "y", GlobalPut "x" "y".
+
+Definition is_uninitialized : val :=
+  λ: "pkgId",
+    match: GlobalGet "pkgId" with
+      SOME <> => #false
+    | NONE => #true
+    end.
+
+End defns.
+End globals.