From 4c38dab821c3a80a9a22f61e00b54e945c0daf0c Mon Sep 17 00:00:00 2001
From: Upamanyu Sharma <upamanyu@mit.edu>
Date: Tue, 17 Dec 2024 18:30:37 -0500
Subject: [PATCH] Update gold

---
 .../examples/append_log/append_log.gold.v     |  9 ++-
 testdata/examples/async/async.gold.v          |  7 ++-
 testdata/examples/comments/comments.gold.v    |  6 +-
 .../externalglobals/externalglobals.gold.v    | 24 ++++++++
 testdata/examples/externalglobals/g.go        |  9 +++
 testdata/examples/logging2/logging2.gold.v    |  9 ++-
 testdata/examples/semantics/semantics.gold.v  |  9 ++-
 testdata/examples/simpledb/simpledb.gold.v    | 10 +++-
 testdata/examples/unittest/unittest.gold.v    | 60 +++++++++++--------
 testdata/examples/wal/wal.gold.v              |  9 ++-
 10 files changed, 120 insertions(+), 32 deletions(-)
 create mode 100644 testdata/examples/externalglobals/externalglobals.gold.v
 create mode 100644 testdata/examples/externalglobals/g.go

diff --git a/testdata/examples/append_log/append_log.gold.v b/testdata/examples/append_log/append_log.gold.v
index 7f37ea4..0cd8fc7 100644
--- a/testdata/examples/append_log/append_log.gold.v
+++ b/testdata/examples/append_log/append_log.gold.v
@@ -196,10 +196,17 @@ Definition Open : val :=
        "diskSz" ::= "$diskSz"
      }]))).
 
+Definition pkg_name' : string := "github.com/goose-lang/goose/testdata/examples/append_log".
+
 Definition define' : val :=
   rec: "define'" <> :=
     exception_do (do:  #()).
 
 Definition initialize' : val :=
   rec: "initialize'" <> :=
-    exception_do (do:  (define' #())).
+    globals.package_init pkg_name' (λ: <>,
+      exception_do (do:  disk.initialize';;;
+      do:  marshal.initialize';;;
+      do:  sync.initialize';;;
+      do:  (define' #()))
+      ).
diff --git a/testdata/examples/async/async.gold.v b/testdata/examples/async/async.gold.v
index 0d859dc..308e914 100644
--- a/testdata/examples/async/async.gold.v
+++ b/testdata/examples/async/async.gold.v
@@ -22,10 +22,15 @@ Definition UseDisk : val :=
     (interface.get "Write" (![disk.Disk] "d")) "$a0" "$a1");;;
     do:  ((interface.get "Barrier" (![disk.Disk] "d")) #())).
 
+Definition pkg_name' : string := "github.com/goose-lang/goose/testdata/examples/async".
+
 Definition define' : val :=
   rec: "define'" <> :=
     exception_do (do:  #()).
 
 Definition initialize' : val :=
   rec: "initialize'" <> :=
-    exception_do (do:  (define' #())).
+    globals.package_init pkg_name' (λ: <>,
+      exception_do (do:  async_disk.initialize';;;
+      do:  (define' #()))
+      ).
diff --git a/testdata/examples/comments/comments.gold.v b/testdata/examples/comments/comments.gold.v
index 1025a4f..6cab700 100644
--- a/testdata/examples/comments/comments.gold.v
+++ b/testdata/examples/comments/comments.gold.v
@@ -18,12 +18,16 @@ Definition Foo__mset : list (string * val) := [
 Definition Foo__mset_ptr : list (string * val) := [
 ].
 
+Definition pkg_name' : string := "github.com/goose-lang/goose/testdata/examples/comments".
+
 Definition define' : val :=
   rec: "define'" <> :=
     exception_do (do:  #()).
 
 Definition initialize' : val :=
   rec: "initialize'" <> :=
-    exception_do (do:  (define' #())).
+    globals.package_init pkg_name' (λ: <>,
+      exception_do (do:  (define' #()))
+      ).
 
 End code.
diff --git a/testdata/examples/externalglobals/externalglobals.gold.v b/testdata/examples/externalglobals/externalglobals.gold.v
new file mode 100644
index 0000000..8ce69fd
--- /dev/null
+++ b/testdata/examples/externalglobals/externalglobals.gold.v
@@ -0,0 +1,24 @@
+(* autogenerated from github.com/goose-lang/goose/testdata/examples/externalglobals *)
+From New.golang Require Import defn.
+From New.code Require github_com.goose_lang.goose.testdata.examples.unittest.
+
+From New Require Import disk_prelude.
+
+(* go: g.go:7:6 *)
+Definition f : val :=
+  rec: "f" <> :=
+    exception_do (let: "$r0" := #(W64 11) in
+    do:  ((globals.get unittest.GlobalX #()) <-[uint64T] "$r0")).
+
+Definition pkg_name' : string := "github.com/goose-lang/goose/testdata/examples/externalglobals".
+
+Definition define' : val :=
+  rec: "define'" <> :=
+    exception_do (do:  #()).
+
+Definition initialize' : val :=
+  rec: "initialize'" <> :=
+    globals.package_init pkg_name' (λ: <>,
+      exception_do (do:  unittest.initialize';;;
+      do:  (define' #()))
+      ).
diff --git a/testdata/examples/externalglobals/g.go b/testdata/examples/externalglobals/g.go
new file mode 100644
index 0000000..1f5c753
--- /dev/null
+++ b/testdata/examples/externalglobals/g.go
@@ -0,0 +1,9 @@
+package externalglobals
+
+import (
+	"github.com/goose-lang/goose/testdata/examples/unittest"
+)
+
+func f() {
+	unittest.GlobalX = 11
+}
diff --git a/testdata/examples/logging2/logging2.gold.v b/testdata/examples/logging2/logging2.gold.v
index 730e89f..2e8b3b9 100644
--- a/testdata/examples/logging2/logging2.gold.v
+++ b/testdata/examples/logging2/logging2.gold.v
@@ -431,10 +431,17 @@ Definition Begin : val :=
     do:  ("txn" <-[Txn] "$r0");;;
     return: (![Txn] "txn")).
 
+Definition pkg_name' : string := "github.com/goose-lang/goose/testdata/examples/logging2".
+
 Definition define' : val :=
   rec: "define'" <> :=
     exception_do (do:  #()).
 
 Definition initialize' : val :=
   rec: "initialize'" <> :=
-    exception_do (do:  (define' #())).
+    globals.package_init pkg_name' (λ: <>,
+      exception_do (do:  sync.initialize';;;
+      do:  disk.initialize';;;
+      do:  primitive.initialize';;;
+      do:  (define' #()))
+      ).
diff --git a/testdata/examples/semantics/semantics.gold.v b/testdata/examples/semantics/semantics.gold.v
index 65e725c..ec10f39 100644
--- a/testdata/examples/semantics/semantics.gold.v
+++ b/testdata/examples/semantics/semantics.gold.v
@@ -3109,10 +3109,17 @@ Definition disabled_testWal : val :=
     do:  ("ok" <-[boolT] "$r0");;;
     return: (![boolT] "ok")).
 
+Definition pkg_name' : string := "github.com/goose-lang/goose/testdata/examples/semantics".
+
 Definition define' : val :=
   rec: "define'" <> :=
     exception_do (do:  #()).
 
 Definition initialize' : val :=
   rec: "initialize'" <> :=
-    exception_do (do:  (define' #())).
+    globals.package_init pkg_name' (λ: <>,
+      exception_do (do:  disk.initialize';;;
+      do:  sync.initialize';;;
+      do:  primitive.initialize';;;
+      do:  (define' #()))
+      ).
diff --git a/testdata/examples/simpledb/simpledb.gold.v b/testdata/examples/simpledb/simpledb.gold.v
index 84f2fc9..73fcfd8 100644
--- a/testdata/examples/simpledb/simpledb.gold.v
+++ b/testdata/examples/simpledb/simpledb.gold.v
@@ -1048,12 +1048,20 @@ Definition Close : val :=
     do:  (let: "$a0" := (![Database] "db") in
     Shutdown "$a0")).
 
+Definition pkg_name' : string := "github.com/goose-lang/goose/testdata/examples/simpledb".
+
 Definition define' : val :=
   rec: "define'" <> :=
     exception_do (do:  #()).
 
 Definition initialize' : val :=
   rec: "initialize'" <> :=
-    exception_do (do:  (define' #())).
+    globals.package_init pkg_name' (λ: <>,
+      exception_do (do:  marshal.initialize';;;
+      do:  filesys.initialize';;;
+      do:  primitive.initialize';;;
+      do:  sync.initialize';;;
+      do:  (define' #()))
+      ).
 
 End code.
diff --git a/testdata/examples/unittest/unittest.gold.v b/testdata/examples/unittest/unittest.gold.v
index c200287..dbdcc6d 100644
--- a/testdata/examples/unittest/unittest.gold.v
+++ b/testdata/examples/unittest/unittest.gold.v
@@ -896,25 +896,27 @@ Definition foo : val :=
   rec: "foo" <> :=
     exception_do (return: (#(W64 10))).
 
-Definition GlobalX : val := #"github.com/goose-lang/goose/testdata/examples/unittest.GlobalX".
+Definition pkg_name' : string := "github.com/goose-lang/goose/testdata/examples/unittest".
 
-Definition globalY : val := #"github.com/goose-lang/goose/testdata/examples/unittest.globalY".
+Definition GlobalX : (string * string) := (pkg_name', "GlobalX").
 
-Definition globalA : val := #"github.com/goose-lang/goose/testdata/examples/unittest.globalA".
+Definition globalY : (string * string) := (pkg_name', "globalY").
 
-Definition globalB : val := #"github.com/goose-lang/goose/testdata/examples/unittest.globalB".
+Definition globalA : (string * string) := (pkg_name', "globalA").
+
+Definition globalB : (string * string) := (pkg_name', "globalB").
 
 (* go: globals.go:12:6 *)
 Definition other : val :=
   rec: "other" <> :=
     exception_do (let: "$r0" := #"ok" in
-    do:  ((globals.get globalY) <-[stringT] "$r0")).
+    do:  ((globals.get globalY #()) <-[stringT] "$r0")).
 
 (* go: globals.go:16:6 *)
 Definition bar : val :=
   rec: "bar" <> :=
     exception_do (do:  (other #());;;
-    (if: ((![uint64T] (globals.get GlobalX)) ≠ #(W64 10)) || ((![stringT] (globals.get globalY)) ≠ #"ok")
+    (if: ((![uint64T] (globals.get GlobalX #())) ≠ #(W64 10)) || ((![stringT] (globals.get globalY #())) ≠ #"ok")
     then
       do:  (let: "$a0" := (interface.make string__mset #"bad") in
       Panic "$a0")
@@ -2440,25 +2442,33 @@ Definition testVariadicPassThrough : val :=
 
 Definition define' : val :=
   rec: "define'" <> :=
-    exception_do (globals.put globalB (ref_ty stringT (zero_val stringT));;;
-    globals.put globalA (ref_ty stringT (zero_val stringT));;;
-    globals.put globalY (ref_ty stringT (zero_val stringT));;;
-    globals.put GlobalX (ref_ty uint64T (zero_val uint64T))).
+    exception_do (do:  (globals.put globalB (ref_ty stringT (zero_val stringT)));;;
+    do:  (globals.put globalA (ref_ty stringT (zero_val stringT)));;;
+    do:  (globals.put globalY (ref_ty stringT (zero_val stringT)));;;
+    do:  (globals.put GlobalX (ref_ty uint64T (zero_val uint64T)))).
 
 Definition initialize' : val :=
   rec: "initialize'" <> :=
-    exception_do (do:  (define' #());;;
-    let: "$r0" := (foo #()) in
-    do:  ((globals.get GlobalX) <-[uint64T] "$r0");;;
-    let: "$r0" := #"a" in
-    do:  ((globals.get globalA) <-[stringT] "$r0");;;
-    let: "$r0" := #"b" in
-    do:  ((globals.get globalB) <-[stringT] "$r0");;;
-    do:  ((λ: <>,
-      exception_do (let: "$r0" := (![uint64T] (globals.get GlobalX)) in
-      do:  ((globals.get GlobalX) <-[uint64T] "$r0"))
-      ) #());;;
-    do:  ((λ: <>,
-      exception_do (let: "$r0" := #"" in
-      do:  ((globals.get globalY) <-[stringT] "$r0"))
-      ) #())).
+    globals.package_init pkg_name' (λ: <>,
+      exception_do (do:  marshal.initialize';;;
+      do:  log.initialize';;;
+      do:  disk.initialize';;;
+      do:  primitive.initialize';;;
+      do:  sync.initialize';;;
+      do:  fmt.initialize';;;
+      do:  (define' #());;;
+      let: "$r0" := (foo #()) in
+      do:  ((globals.get GlobalX #()) <-[uint64T] "$r0");;;
+      let: "$r0" := #"a" in
+      do:  ((globals.get globalA #()) <-[stringT] "$r0");;;
+      let: "$r0" := #"b" in
+      do:  ((globals.get globalB #()) <-[stringT] "$r0");;;
+      do:  ((λ: <>,
+        exception_do (let: "$r0" := (![uint64T] (globals.get GlobalX #())) in
+        do:  ((globals.get GlobalX #()) <-[uint64T] "$r0"))
+        ) #());;;
+      do:  ((λ: <>,
+        exception_do (let: "$r0" := #"" in
+        do:  ((globals.get globalY #()) <-[stringT] "$r0"))
+        ) #()))
+      ).
diff --git a/testdata/examples/wal/wal.gold.v b/testdata/examples/wal/wal.gold.v
index d4a705a..07b81a8 100644
--- a/testdata/examples/wal/wal.gold.v
+++ b/testdata/examples/wal/wal.gold.v
@@ -377,10 +377,17 @@ Definition Open : val :=
        "length" ::= "$length"
      }])).
 
+Definition pkg_name' : string := "github.com/goose-lang/goose/testdata/examples/wal".
+
 Definition define' : val :=
   rec: "define'" <> :=
     exception_do (do:  #()).
 
 Definition initialize' : val :=
   rec: "initialize'" <> :=
-    exception_do (do:  (define' #())).
+    globals.package_init pkg_name' (λ: <>,
+      exception_do (do:  disk.initialize';;;
+      do:  primitive.initialize';;;
+      do:  sync.initialize';;;
+      do:  (define' #()))
+      ).