From 1639e566acf0398fe31f1d0469c1e0f25b6dc0b0 Mon Sep 17 00:00:00 2001
From: Upamanyu Sharma <upamanyu@mit.edu>
Date: Thu, 5 Dec 2024 13:17:19 -0500
Subject: [PATCH] Add go globals implementation

---
 new/golang/defn.v         |  2 +-
 new/golang/defn/globals.v | 24 ++++++++++++++++++++++++
 2 files changed, 25 insertions(+), 1 deletion(-)
 create mode 100644 new/golang/defn/globals.v

diff --git a/new/golang/defn.v b/new/golang/defn.v
index b99358dd6..26fea7571 100644
--- a/new/golang/defn.v
+++ b/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.
diff --git a/new/golang/defn/globals.v b/new/golang/defn/globals.v
new file mode 100644
index 000000000..a062fd99a
--- /dev/null
+++ b/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.