diff --git a/new/code/github_com/goose_lang/goose/testdata/examples/channel.v b/new/code/github_com/goose_lang/goose/testdata/examples/channel.v
index c1a4738db..95a1eeaec 100644
--- a/new/code/github_com/goose_lang/goose/testdata/examples/channel.v
+++ b/new/code/github_com/goose_lang/goose/testdata/examples/channel.v
@@ -1,5 +1,7 @@
 (* autogenerated from github.com/goose-lang/goose/testdata/examples/channel *)
 Require Export New.code.github_com.goose_lang.goose.model.channel.
+Require Export New.code.strings.
+Require Export New.code.time.
 
 From New.golang Require Import defn.
 Definition chan_spec_raw_examples : go_string := "github.com/goose-lang/goose/testdata/examples/channel".
@@ -10,339 +12,1041 @@ Section code.
 Context `{ffi_syntax}.
 
 
-Definition SendMessage : go_string := "github.com/goose-lang/goose/testdata/examples/channel.SendMessage"%go.
+Definition sys_hello_world : go_string := "github.com/goose-lang/goose/testdata/examples/channel.sys_hello_world"%go.
 
-(* Example 1: Simple goroutine sending a string, check basic message passing without
-   synchronization
+(* Fake syscall for demonstration.
 
-   go: examples.go:10:6 *)
-Definition SendMessageⁱᵐᵖˡ : val :=
+   go: examples.go:9:6 *)
+Definition sys_hello_worldⁱᵐᵖˡ : val :=
   λ: <>,
-    exception_do (let: "messageChan" := (mem.alloc (type.zero_val #ptrT)) in
-    let: "$r0" := (let: "$a0" := #(W64 0) in
-    (func_call #channel.NewChannelRef #stringT) "$a0") in
-    do:  ("messageChan" <-[#ptrT] "$r0");;;
+    exception_do (return: (#"Hello, World!"%go)).
+
+Definition HelloWorldAsync : go_string := "github.com/goose-lang/goose/testdata/examples/channel.HelloWorldAsync"%go.
+
+(* go: examples.go:13:6 *)
+Definition HelloWorldAsyncⁱᵐᵖˡ : val :=
+  λ: <>,
+    exception_do (let: "ch" := (mem.alloc (type.zero_val (type.chanT #stringT))) in
+    let: "$r0" := (chan.make #stringT #(W64 1)) in
+    do:  ("ch" <-[type.chanT #stringT] "$r0");;;
     let: "$go" := (λ: <>,
-      exception_do (do:  (let: "$a0" := #"hello world"%go in
-      (method_call #(ptrT.id channel.Channel.id) #"Send"%go (![#ptrT] "messageChan") #stringT) "$a0");;;
+      exception_do (do:  (let: "$chan" := (![type.chanT #stringT] "ch") in
+      let: "$v" := ((func_call #sys_hello_world) #()) in
+      chan.send "$chan" "$v");;;
       return: #())
       ) in
     do:  (Fork ("$go" #()));;;
-    let: "message" := (mem.alloc (type.zero_val #stringT)) in
-    let: "$r0" := ((method_call #(ptrT.id channel.Channel.id) #"ReceiveDiscardOk"%go (![#ptrT] "messageChan") #stringT) #()) in
-    do:  ("message" <-[#stringT] "$r0");;;
-    (if: (![#stringT] "message") ≠ #"hello world"%go
-    then
-      do:  (let: "$a0" := (interface.make #stringT.id #"Did not receive expected message"%go) in
-      Panic "$a0")
-    else do:  #());;;
-    return: #()).
+    return: (![type.chanT #stringT] "ch")).
+
+Definition HelloWorldSync : go_string := "github.com/goose-lang/goose/testdata/examples/channel.HelloWorldSync"%go.
+
+(* go: examples.go:21:6 *)
+Definition HelloWorldSyncⁱᵐᵖˡ : val :=
+  λ: <>,
+    exception_do (return: (Fst (chan.receive ((func_call #HelloWorldAsync) #())))).
+
+Definition HelloWorldCancellable : go_string := "github.com/goose-lang/goose/testdata/examples/channel.HelloWorldCancellable"%go.
+
+(* Simulates the error/done channel components of Context
+
+   go: examples.go:26:6 *)
+Definition HelloWorldCancellableⁱᵐᵖˡ : val :=
+  λ: "done" "err",
+    exception_do (let: "err" := (mem.alloc "err") in
+    let: "done" := (mem.alloc "done") in
+    let: "future" := (mem.alloc (type.zero_val (type.chanT #stringT))) in
+    let: "$r0" := ((func_call #HelloWorldAsync) #()) in
+    do:  ("future" <-[type.chanT #stringT] "$r0");;;
+    chan.select [chan.select_receive (![type.chanT #stringT] "future") (λ: "$recvVal",
+       let: "resolved" := (mem.alloc (type.zero_val #stringT)) in
+       let: "$r0" := (Fst "$recvVal") in
+       do:  ("resolved" <-[#stringT] "$r0");;;
+       return: (![#stringT] "resolved")
+       ); chan.select_receive (![type.chanT (type.structT [
+     ])] "done") (λ: "$recvVal",
+       return: (![#stringT] (![#ptrT] "err"))
+       )] chan.select_no_default).
 
-Definition JoinWithReceive : go_string := "github.com/goose-lang/goose/testdata/examples/channel.JoinWithReceive"%go.
+Definition HelloWorldWithTimeout : go_string := "github.com/goose-lang/goose/testdata/examples/channel.HelloWorldWithTimeout"%go.
 
-(* Example 2: Join goroutine with receive on unbuffered channel
+(* Uses cancellation as a timeout mechanism.
 
-   go: examples.go:29:6 *)
-Definition JoinWithReceiveⁱᵐᵖˡ : val :=
+   go: examples.go:37:6 *)
+Definition HelloWorldWithTimeoutⁱᵐᵖˡ : val :=
   λ: <>,
-    exception_do (let: "message" := (mem.alloc (type.zero_val #ptrT)) in
-    let: "$r0" := (mem.alloc (type.zero_val #stringT)) in
-    do:  ("message" <-[#ptrT] "$r0");;;
-    let: "done" := (mem.alloc (type.zero_val #ptrT)) in
-    let: "$r0" := (let: "$a0" := #(W64 0) in
-    (func_call #channel.NewChannelRef #uint64T) "$a0") in
-    do:  ("done" <-[#ptrT] "$r0");;;
+    exception_do (let: "done" := (mem.alloc (type.zero_val (type.chanT (type.structT [
+    ])))) in
+    let: "$r0" := (chan.make (type.structT [
+    ]) #(W64 0)) in
+    do:  ("done" <-[type.chanT (type.structT [
+    ])] "$r0");;;
+    let: "errMsg" := (mem.alloc (type.zero_val #stringT)) in
+    let: "$r0" := #""%go in
+    do:  ("errMsg" <-[#stringT] "$r0");;;
     let: "$go" := (λ: <>,
-      exception_do (let: "$r0" := #"hello world"%go in
-      do:  ((![#ptrT] "message") <-[#stringT] "$r0");;;
-      do:  (let: "$a0" := #(W64 0) in
-      (method_call #(ptrT.id channel.Channel.id) #"Send"%go (![#ptrT] "done") #uint64T) "$a0");;;
+      exception_do (do:  (let: "$a0" := (#(W64 10) * time.Millisecond) in
+      (func_call #time.Sleep) "$a0");;;
+      let: "$r0" := #"operation timed out"%go in
+      do:  ("errMsg" <-[#stringT] "$r0");;;
+      do:  (let: "$a0" := (![type.chanT (type.structT [
+      ])] "done") in
+      chan.close "$a0");;;
       return: #())
       ) in
     do:  (Fork ("$go" #()));;;
-    do:  ((method_call #(ptrT.id channel.Channel.id) #"ReceiveDiscardOk"%go (![#ptrT] "done") #uint64T) #());;;
-    (if: (![#stringT] (![#ptrT] "message")) ≠ #"hello world"%go
-    then
-      do:  (let: "$a0" := (interface.make #stringT.id #"Message was not set correctly"%go) in
-      Panic "$a0")
-    else do:  #());;;
+    return: (let: "$a0" := (![type.chanT (type.structT [
+     ])] "done") in
+     let: "$a1" := "errMsg" in
+     (func_call #HelloWorldCancellable) "$a0" "$a1")).
+
+Definition DSPExample : go_string := "github.com/goose-lang/goose/testdata/examples/channel.DSPExample"%go.
+
+(* prog3 from Actris 2.0 intro: https://arxiv.org/pdf/2010.15030
+
+   go: examples.go:52:6 *)
+Definition DSPExampleⁱᵐᵖˡ : val :=
+  λ: <>,
+    exception_do (let: "c" := (mem.alloc (type.zero_val (type.chanT #ptrT))) in
+    let: "$r0" := (chan.make #ptrT #(W64 0)) in
+    do:  ("c" <-[type.chanT #ptrT] "$r0");;;
+    let: "signal" := (mem.alloc (type.zero_val (type.chanT (type.structT [
+    ])))) in
+    let: "$r0" := (chan.make (type.structT [
+    ]) #(W64 0)) in
+    do:  ("signal" <-[type.chanT (type.structT [
+    ])] "$r0");;;
+    let: "$go" := (λ: <>,
+      exception_do (let: "ptr" := (mem.alloc (type.zero_val #ptrT)) in
+      let: "$r0" := (Fst (chan.receive (![type.chanT #ptrT] "c"))) in
+      do:  ("ptr" <-[#ptrT] "$r0");;;
+      let: "$r0" := ((![#intT] (![#ptrT] "ptr")) + #(W64 2)) in
+      do:  ((![#ptrT] "ptr") <-[#intT] "$r0");;;
+      do:  (let: "$chan" := (![type.chanT (type.structT [
+      ])] "signal") in
+      let: "$v" := (struct.make (type.structT [
+      ]) [{
+      }]) in
+      chan.send "$chan" "$v");;;
+      return: #())
+      ) in
+    do:  (Fork ("$go" #()));;;
+    let: "val" := (mem.alloc (type.zero_val #intT)) in
+    let: "$r0" := #(W64 40) in
+    do:  ("val" <-[#intT] "$r0");;;
+    let: "ptr" := (mem.alloc (type.zero_val #ptrT)) in
+    let: "$r0" := "val" in
+    do:  ("ptr" <-[#ptrT] "$r0");;;
+    do:  (let: "$chan" := (![type.chanT #ptrT] "c") in
+    let: "$v" := (![#ptrT] "ptr") in
+    chan.send "$chan" "$v");;;
+    do:  (Fst (chan.receive (![type.chanT (type.structT [
+    ])] "signal")));;;
+    return: (![#intT] (![#ptrT] "ptr"))).
+
+Definition fibonacci : go_string := "github.com/goose-lang/goose/testdata/examples/channel.fibonacci"%go.
+
+(* https://go.dev/tour/concurrency/4
+
+   go: examples.go:70:6 *)
+Definition fibonacciⁱᵐᵖˡ : val :=
+  λ: "n" "c",
+    exception_do (let: "c" := (mem.alloc "c") in
+    let: "n" := (mem.alloc "n") in
+    let: "y" := (mem.alloc (type.zero_val #intT)) in
+    let: "x" := (mem.alloc (type.zero_val #intT)) in
+    let: "$r0" := #(W64 0) in
+    let: "$r1" := #(W64 1) in
+    do:  ("x" <-[#intT] "$r0");;;
+    do:  ("y" <-[#intT] "$r1");;;
+    (let: "i" := (mem.alloc (type.zero_val #intT)) in
+    let: "$r0" := #(W64 0) in
+    do:  ("i" <-[#intT] "$r0");;;
+    (for: (λ: <>, int_lt (![#intT] "i") (![#intT] "n")); (λ: <>, do:  ("i" <-[#intT] ((![#intT] "i") + #(W64 1)))) := λ: <>,
+      do:  (let: "$chan" := (![type.chanT #intT] "c") in
+      let: "$v" := (![#intT] "x") in
+      chan.send "$chan" "$v");;;
+      let: "$r0" := (![#intT] "y") in
+      let: "$r1" := ((![#intT] "x") + (![#intT] "y")) in
+      do:  ("x" <-[#intT] "$r0");;;
+      do:  ("y" <-[#intT] "$r1")));;;
+    do:  (let: "$a0" := (![type.chanT #intT] "c") in
+    chan.close "$a0");;;
     return: #()).
 
-Definition JoinWithSend : go_string := "github.com/goose-lang/goose/testdata/examples/channel.JoinWithSend"%go.
+Definition fib_consumer : go_string := "github.com/goose-lang/goose/testdata/examples/channel.fib_consumer"%go.
+
+(* go: examples.go:79:6 *)
+Definition fib_consumerⁱᵐᵖˡ : val :=
+  λ: <>,
+    exception_do (let: "c" := (mem.alloc (type.zero_val (type.chanT #intT))) in
+    let: "$r0" := (chan.make #intT #(W64 10)) in
+    do:  ("c" <-[type.chanT #intT] "$r0");;;
+    let: "$a0" := (let: "$a0" := (![type.chanT #intT] "c") in
+    chan.cap "$a0") in
+    let: "$a1" := (![type.chanT #intT] "c") in
+    let: "$go" := (func_call #fibonacci) in
+    do:  (Fork ("$go" "a0" "a1"));;;
+    let: "results" := (mem.alloc (type.zero_val #sliceT)) in
+    let: "$r0" := #slice.nil in
+    do:  ("results" <-[#sliceT] "$r0");;;
+    let: "$range" := (![type.chanT #intT] "c") in
+    (let: "i" := (mem.alloc (type.zero_val #intT)) in
+    chan.for_range "$range" (λ: "$key",
+      do:  ("i" <-[#intT] "$key");;;
+      let: "$r0" := (let: "$a0" := (![#sliceT] "results") in
+      let: "$a1" := ((let: "$sl0" := (![#intT] "i") in
+      slice.literal #intT ["$sl0"])) in
+      (slice.append #intT) "$a0" "$a1") in
+      do:  ("results" <-[#sliceT] "$r0")));;;
+    return: (![#sliceT] "results")).
+
+Definition select_nb_no_panic : go_string := "github.com/goose-lang/goose/testdata/examples/channel.select_nb_no_panic"%go.
 
-(* Example 3: Join goroutine with send on unbuffered channel
+(* Show that it isn't possible to have 2 nonblocking ops that match.
 
-   go: examples.go:55:6 *)
-Definition JoinWithSendⁱᵐᵖˡ : val :=
+   go: examples.go:91:6 *)
+Definition select_nb_no_panicⁱᵐᵖˡ : val :=
   λ: <>,
-    exception_do (let: "message" := (mem.alloc (type.zero_val #ptrT)) in
-    let: "$r0" := (mem.alloc (type.zero_val #stringT)) in
-    do:  ("message" <-[#ptrT] "$r0");;;
-    let: "done" := (mem.alloc (type.zero_val #ptrT)) in
-    let: "$r0" := (let: "$a0" := #(W64 0) in
-    (func_call #channel.NewChannelRef #uint64T) "$a0") in
-    do:  ("done" <-[#ptrT] "$r0");;;
+    exception_do (let: "ch" := (mem.alloc (type.zero_val (type.chanT (type.structT [
+    ])))) in
+    let: "$r0" := (chan.make (type.structT [
+    ]) #(W64 0)) in
+    do:  ("ch" <-[type.chanT (type.structT [
+    ])] "$r0");;;
     let: "$go" := (λ: <>,
-      exception_do (let: "$r0" := #"hello world"%go in
-      do:  ((![#ptrT] "message") <-[#stringT] "$r0");;;
-      do:  ((method_call #(ptrT.id channel.Channel.id) #"ReceiveDiscardOk"%go (![#ptrT] "done") #uint64T) #());;;
+      exception_do (chan.select [chan.select_receive (![type.chanT (type.structT [
+       ])] "ch") (λ: "$recvVal",
+         do:  (let: "$a0" := (interface.make #stringT.id #"bad"%go) in
+         Panic "$a0")
+         )] (chan.select_default (λ: <>,
+        do:  #()
+        ));;;
       return: #())
       ) in
     do:  (Fork ("$go" #()));;;
-    do:  (let: "$a0" := #(W64 0) in
-    (method_call #(ptrT.id channel.Channel.id) #"Send"%go (![#ptrT] "done") #uint64T) "$a0");;;
-    (if: (![#stringT] (![#ptrT] "message")) ≠ #"hello world"%go
+    chan.select [chan.select_send (struct.make (type.structT [
+     ]) [{
+     }]) (![type.chanT (type.structT [
+     ])] "ch") (λ: <>,
+       do:  (let: "$a0" := (interface.make #stringT.id #"bad"%go) in
+       Panic "$a0")
+       )] (chan.select_default (λ: <>,
+      do:  #()
+      ));;;
+    return: #()).
+
+Definition select_ready_case_no_panic : go_string := "github.com/goose-lang/goose/testdata/examples/channel.select_ready_case_no_panic"%go.
+
+(* Show that a guaranteed to be ready case makes default impossible
+
+   go: examples.go:109:6 *)
+Definition select_ready_case_no_panicⁱᵐᵖˡ : val :=
+  λ: <>,
+    exception_do (let: "ch" := (mem.alloc (type.zero_val (type.chanT (type.structT [
+    ])))) in
+    let: "$r0" := (chan.make (type.structT [
+    ]) #(W64 0)) in
+    do:  ("ch" <-[type.chanT (type.structT [
+    ])] "$r0");;;
+    do:  (let: "$a0" := (![type.chanT (type.structT [
+    ])] "ch") in
+    chan.close "$a0");;;
+    chan.select [chan.select_receive (![type.chanT (type.structT [
+     ])] "ch") (λ: "$recvVal",
+       do:  #()
+       )] (chan.select_default (λ: <>,
+      do:  (let: "$a0" := (interface.make #stringT.id #"Shouldn't be possible!"%go) in
+      Panic "$a0")
+      ));;;
+    return: #()).
+
+Definition TestHelloWorldSync : go_string := "github.com/goose-lang/goose/testdata/examples/channel.TestHelloWorldSync"%go.
+
+(* Various tests that should panic when failing, which also means verifying { True } e { True } is
+   sufficient since panic can't be verified.
+
+   go: examples.go:123:6 *)
+Definition TestHelloWorldSyncⁱᵐᵖˡ : val :=
+  λ: <>,
+    exception_do (let: "result" := (mem.alloc (type.zero_val #stringT)) in
+    let: "$r0" := ((func_call #HelloWorldSync) #()) in
+    do:  ("result" <-[#stringT] "$r0");;;
+    (if: (![#stringT] "result") ≠ #"Hello, World!"%go
     then
-      do:  (let: "$a0" := (interface.make #stringT.id #"Message was not set correctly"%go) in
+      do:  (let: "$a0" := (interface.make #stringT.id #"incorrect output"%go) in
       Panic "$a0")
     else do:  #());;;
     return: #()).
 
-Definition BroadcastNotification : go_string := "github.com/goose-lang/goose/testdata/examples/channel.BroadcastNotification"%go.
+Definition TestHelloWorldWithTimeout : go_string := "github.com/goose-lang/goose/testdata/examples/channel.TestHelloWorldWithTimeout"%go.
+
+(* go: examples.go:130:6 *)
+Definition TestHelloWorldWithTimeoutⁱᵐᵖˡ : val :=
+  λ: <>,
+    exception_do (let: "result" := (mem.alloc (type.zero_val #stringT)) in
+    let: "$r0" := ((func_call #HelloWorldWithTimeout) #()) in
+    do:  ("result" <-[#stringT] "$r0");;;
+    (if: ((![#stringT] "result") ≠ #"operation timed out"%go) && ((![#stringT] "result") ≠ #"Hello, World!"%go)
+    then
+      do:  (let: "$a0" := (interface.make #stringT.id #"incorrect output"%go) in
+      Panic "$a0")
+    else do:  #());;;
+    return: #()).
 
-(* Example 4: Broadcast notification with close. This is testing a case where
-   we transfer disjoint ownership to different threads in a single broadcast
+Definition TestDSPExample : go_string := "github.com/goose-lang/goose/testdata/examples/channel.TestDSPExample"%go.
 
-   go: examples.go:82:6 *)
-Definition BroadcastNotificationⁱᵐᵖˡ : val :=
+(* go: examples.go:137:6 *)
+Definition TestDSPExampleⁱᵐᵖˡ : val :=
   λ: <>,
-    exception_do (let: "notifyCh" := (mem.alloc (type.zero_val #ptrT)) in
-    let: "$r0" := (let: "$a0" := #(W64 0) in
-    (func_call #channel.NewChannelRef #uint64T) "$a0") in
-    do:  ("notifyCh" <-[#ptrT] "$r0");;;
-    let: "done1" := (mem.alloc (type.zero_val #ptrT)) in
-    let: "$r0" := (let: "$a0" := #(W64 0) in
-    (func_call #channel.NewChannelRef #uint64T) "$a0") in
-    do:  ("done1" <-[#ptrT] "$r0");;;
-    let: "done2" := (mem.alloc (type.zero_val #ptrT)) in
-    let: "$r0" := (let: "$a0" := #(W64 0) in
-    (func_call #channel.NewChannelRef #uint64T) "$a0") in
-    do:  ("done2" <-[#ptrT] "$r0");;;
-    let: "done3" := (mem.alloc (type.zero_val #ptrT)) in
-    let: "$r0" := (let: "$a0" := #(W64 0) in
-    (func_call #channel.NewChannelRef #uint64T) "$a0") in
-    do:  ("done3" <-[#ptrT] "$r0");;;
-    let: "results" := (mem.alloc (type.zero_val #sliceT)) in
-    let: "$r0" := (let: "$a0" := (![#sliceT] "results") in
-    let: "$a1" := ((let: "$sl0" := #""%go in
-    slice.literal #stringT ["$sl0"])) in
-    (slice.append #stringT) "$a0" "$a1") in
-    do:  ("results" <-[#sliceT] "$r0");;;
-    let: "$r0" := (let: "$a0" := (![#sliceT] "results") in
-    let: "$a1" := ((let: "$sl0" := #""%go in
-    slice.literal #stringT ["$sl0"])) in
-    (slice.append #stringT) "$a0" "$a1") in
-    do:  ("results" <-[#sliceT] "$r0");;;
-    let: "$r0" := (let: "$a0" := (![#sliceT] "results") in
-    let: "$a1" := ((let: "$sl0" := #""%go in
-    slice.literal #stringT ["$sl0"])) in
-    (slice.append #stringT) "$a0" "$a1") in
-    do:  ("results" <-[#sliceT] "$r0");;;
-    let: "$go" := (λ: <>,
-      exception_do (let: "ok" := (mem.alloc (type.zero_val #boolT)) in
-      let: ("$ret0", "$ret1") := ((method_call #(ptrT.id channel.Channel.id) #"Receive"%go (![#ptrT] "notifyCh") #uint64T) #()) in
+    exception_do (let: "result" := (mem.alloc (type.zero_val #intT)) in
+    let: "$r0" := ((func_call #DSPExample) #()) in
+    do:  ("result" <-[#intT] "$r0");;;
+    (if: (![#intT] "result") ≠ #(W64 42)
+    then
+      do:  (let: "$a0" := (interface.make #stringT.id #"incorrect output"%go) in
+      Panic "$a0")
+    else do:  #());;;
+    return: #()).
+
+Definition TestFibConsumer : go_string := "github.com/goose-lang/goose/testdata/examples/channel.TestFibConsumer"%go.
+
+(* go: examples.go:144:6 *)
+Definition TestFibConsumerⁱᵐᵖˡ : val :=
+  λ: <>,
+    exception_do (let: "result" := (mem.alloc (type.zero_val #sliceT)) in
+    let: "$r0" := ((func_call #fib_consumer) #()) in
+    do:  ("result" <-[#sliceT] "$r0");;;
+    let: "expected" := (mem.alloc (type.zero_val #sliceT)) in
+    let: "$r0" := ((let: "$sl0" := #(W64 0) in
+    let: "$sl1" := #(W64 1) in
+    let: "$sl2" := #(W64 1) in
+    let: "$sl3" := #(W64 2) in
+    let: "$sl4" := #(W64 3) in
+    let: "$sl5" := #(W64 5) in
+    let: "$sl6" := #(W64 8) in
+    let: "$sl7" := #(W64 13) in
+    let: "$sl8" := #(W64 21) in
+    let: "$sl9" := #(W64 34) in
+    slice.literal #intT ["$sl0"; "$sl1"; "$sl2"; "$sl3"; "$sl4"; "$sl5"; "$sl6"; "$sl7"; "$sl8"; "$sl9"])) in
+    do:  ("expected" <-[#sliceT] "$r0");;;
+    (if: (let: "$a0" := (![#sliceT] "result") in
+    slice.len "$a0") ≠ (let: "$a0" := (![#sliceT] "expected") in
+    slice.len "$a0")
+    then
+      do:  (let: "$a0" := (interface.make #stringT.id #"incorrect output"%go) in
+      Panic "$a0")
+    else do:  #());;;
+    let: "$range" := (![#sliceT] "expected") in
+    (let: "i" := (mem.alloc (type.zero_val #intT)) in
+    slice.for_range #intT "$range" (λ: "$key" "$value",
+      do:  ("i" <-[#intT] "$key");;;
+      (if: (![#intT] (slice.elem_ref #intT (![#sliceT] "result") (![#intT] "i"))) ≠ (![#intT] (slice.elem_ref #intT (![#sliceT] "expected") (![#intT] "i")))
+      then
+        do:  (let: "$a0" := (interface.make #stringT.id #"incorrect output"%go) in
+        Panic "$a0")
+      else do:  #())));;;
+    return: #()).
+
+Definition TestSelectNbNoPanic : go_string := "github.com/goose-lang/goose/testdata/examples/channel.TestSelectNbNoPanic"%go.
+
+(* go: examples.go:159:6 *)
+Definition TestSelectNbNoPanicⁱᵐᵖˡ : val :=
+  λ: <>,
+    exception_do (let: "iterations" := (mem.alloc (type.zero_val #intT)) in
+    let: "$r0" := #(W64 10000) in
+    do:  ("iterations" <-[#intT] "$r0");;;
+    (let: "i" := (mem.alloc (type.zero_val #intT)) in
+    let: "$r0" := #(W64 0) in
+    do:  ("i" <-[#intT] "$r0");;;
+    (for: (λ: <>, int_lt (![#intT] "i") (![#intT] "iterations")); (λ: <>, do:  ("i" <-[#intT] ((![#intT] "i") + #(W64 1)))) := λ: <>,
+      do:  ((func_call #select_nb_no_panic) #());;;
+      do:  (let: "$a0" := (#(W64 1) * time.Microsecond) in
+      (func_call #time.Sleep) "$a0")));;;
+    return: #()).
+
+Definition TestSelectReadyCaseNoPanic : go_string := "github.com/goose-lang/goose/testdata/examples/channel.TestSelectReadyCaseNoPanic"%go.
+
+(* go: examples.go:168:6 *)
+Definition TestSelectReadyCaseNoPanicⁱᵐᵖˡ : val :=
+  λ: <>,
+    exception_do (let: "iterations" := (mem.alloc (type.zero_val #intT)) in
+    let: "$r0" := #(W64 10000) in
+    do:  ("iterations" <-[#intT] "$r0");;;
+    (let: "i" := (mem.alloc (type.zero_val #intT)) in
+    let: "$r0" := #(W64 0) in
+    do:  ("i" <-[#intT] "$r0");;;
+    (for: (λ: <>, int_lt (![#intT] "i") (![#intT] "iterations")); (λ: <>, do:  ("i" <-[#intT] ((![#intT] "i") + #(W64 1)))) := λ: <>,
+      do:  ((func_call #select_ready_case_no_panic) #())));;;
+    return: #()).
+
+Definition load : go_string := "github.com/goose-lang/goose/testdata/examples/channel.load"%go.
+
+(* load writes the next letter into the buffer.
+
+   go: examples.go:179:6 *)
+Definition loadⁱᵐᵖˡ : val :=
+  λ: "b" "letter",
+    exception_do (let: "letter" := (mem.alloc "letter") in
+    let: "b" := (mem.alloc "b") in
+    let: "$r0" := (string.to_bytes (![#stringT] "letter")) in
+    do:  ((![#ptrT] "b") <-[#sliceT] "$r0");;;
+    return: #()).
+
+Definition process : go_string := "github.com/goose-lang/goose/testdata/examples/channel.process"%go.
+
+(* process consumes the buffer and appends it to the output.
+
+   go: examples.go:184:6 *)
+Definition processⁱᵐᵖˡ : val :=
+  λ: "b" "output",
+    exception_do (let: "output" := (mem.alloc "output") in
+    let: "b" := (mem.alloc "b") in
+    do:  ((![#ptrT] "output") <-[#stringT] ((![#stringT] (![#ptrT] "output")) + (let: "$a0" := (string.from_bytes (![#sliceT] (![#ptrT] "b"))) in
+    (func_call #strings.ToUpper) "$a0")));;;
+    return: #()).
+
+Definition client : go_string := "github.com/goose-lang/goose/testdata/examples/channel.client"%go.
+
+(* go: examples.go:188:6 *)
+Definition clientⁱᵐᵖˡ : val :=
+  λ: "input" "freeList" "serverChan",
+    exception_do (let: "serverChan" := (mem.alloc "serverChan") in
+    let: "freeList" := (mem.alloc "freeList") in
+    let: "input" := (mem.alloc "input") in
+    let: "$range" := (![#sliceT] "input") in
+    (let: "letter" := (mem.alloc (type.zero_val #stringT)) in
+    slice.for_range #stringT "$range" (λ: "$key" "$value",
+      do:  ("letter" <-[#stringT] "$value");;;
+      do:  "$key";;;
+      let: "b" := (mem.alloc (type.zero_val #sliceT)) in
+      chan.select [chan.select_receive (![type.chanT #sliceT] "freeList") (λ: "$recvVal",
+         let: "$r0" := (Fst "$recvVal") in
+         do:  ("b" <-[#sliceT] "$r0");;;
+         do:  #()
+         )] (chan.select_default (λ: <>,
+        let: "$r0" := ((let: "$sl0" := #(W8 0) in
+        slice.literal #byteT ["$sl0"])) in
+        do:  ("b" <-[#sliceT] "$r0")
+        ));;;
+      do:  (let: "$a0" := "b" in
+      let: "$a1" := (![#stringT] "letter") in
+      (func_call #load) "$a0" "$a1");;;
+      do:  (let: "$chan" := (![type.chanT #sliceT] "serverChan") in
+      let: "$v" := (![#sliceT] "b") in
+      chan.send "$chan" "$v")));;;
+    do:  (let: "$a0" := (![type.chanT #sliceT] "serverChan") in
+    chan.close "$a0");;;
+    return: #()).
+
+Definition server : go_string := "github.com/goose-lang/goose/testdata/examples/channel.server"%go.
+
+(* go: examples.go:209:6 *)
+Definition serverⁱᵐᵖˡ : val :=
+  λ: "output" "freeList" "serverChan" "done",
+    exception_do (let: "done" := (mem.alloc "done") in
+    let: "serverChan" := (mem.alloc "serverChan") in
+    let: "freeList" := (mem.alloc "freeList") in
+    let: "output" := (mem.alloc "output") in
+    (for: (λ: <>, #true); (λ: <>, #()) := λ: <>,
+      let: "ok" := (mem.alloc (type.zero_val #boolT)) in
+      let: "b" := (mem.alloc (type.zero_val #sliceT)) in
+      let: ("$ret0", "$ret1") := (chan.receive (![type.chanT #sliceT] "serverChan")) in
       let: "$r0" := "$ret0" in
       let: "$r1" := "$ret1" in
-      do:  "$r0";;;
+      do:  ("b" <-[#sliceT] "$r0");;;
       do:  ("ok" <-[#boolT] "$r1");;;
       (if: (~ (![#boolT] "ok"))
       then
-        (if: (![#stringT] (slice.elem_ref #stringT (![#sliceT] "results") #(W64 0))) ≠ #"thread1"%go
-        then
-          do:  (let: "$a0" := (interface.make #stringT.id #"Thread 1 received incorrect value"%go) in
-          Panic "$a0")
-        else do:  #());;;
-        do:  (let: "$a0" := #(W64 0) in
-        (method_call #(ptrT.id channel.Channel.id) #"Send"%go (![#ptrT] "done1") #uint64T) "$a0")
+        do:  (let: "$chan" := (![type.chanT (type.structT [
+        ])] "done") in
+        let: "$v" := (struct.make (type.structT [
+        ]) [{
+        }]) in
+        chan.send "$chan" "$v");;;
+        return: (#())
       else do:  #());;;
+      do:  (let: "$a0" := "b" in
+      let: "$a1" := (![#ptrT] "output") in
+      (func_call #process) "$a0" "$a1");;;
+      chan.select [chan.select_send (![#sliceT] "b") (![type.chanT #sliceT] "freeList") (λ: <>,
+         do:  #()
+         )] (chan.select_default (λ: <>,
+        do:  #()
+        )));;;
+    return: #()).
+
+Definition LeakyBufferPipeline : go_string := "github.com/goose-lang/goose/testdata/examples/channel.LeakyBufferPipeline"%go.
+
+(* go: examples.go:231:6 *)
+Definition LeakyBufferPipelineⁱᵐᵖˡ : val :=
+  λ: <>,
+    exception_do (let: "freeList" := (mem.alloc (type.zero_val (type.chanT #sliceT))) in
+    let: "$r0" := (chan.make #sliceT #(W64 5)) in
+    do:  ("freeList" <-[type.chanT #sliceT] "$r0");;;
+    let: "serverChan" := (mem.alloc (type.zero_val (type.chanT #sliceT))) in
+    let: "$r0" := (chan.make #sliceT #(W64 0)) in
+    do:  ("serverChan" <-[type.chanT #sliceT] "$r0");;;
+    let: "done" := (mem.alloc (type.zero_val (type.chanT (type.structT [
+    ])))) in
+    let: "$r0" := (chan.make (type.structT [
+    ]) #(W64 0)) in
+    do:  ("done" <-[type.chanT (type.structT [
+    ])] "$r0");;;
+    let: "output" := (mem.alloc (type.zero_val #stringT)) in
+    let: "$r0" := #""%go in
+    do:  ("output" <-[#stringT] "$r0");;;
+    let: "$a0" := "output" in
+    let: "$a1" := (![type.chanT #sliceT] "freeList") in
+    let: "$a2" := (![type.chanT #sliceT] "serverChan") in
+    let: "$a3" := (![type.chanT (type.structT [
+    ])] "done") in
+    let: "$go" := (func_call #server) in
+    do:  (Fork ("$go" "a0" "a1" "a2" "a3"));;;
+    do:  (let: "$a0" := ((let: "$sl0" := #"h"%go in
+    let: "$sl1" := #"e"%go in
+    let: "$sl2" := #"l"%go in
+    let: "$sl3" := #"l"%go in
+    let: "$sl4" := #"o"%go in
+    let: "$sl5" := #","%go in
+    let: "$sl6" := #" "%go in
+    let: "$sl7" := #"w"%go in
+    let: "$sl8" := #"o"%go in
+    let: "$sl9" := #"r"%go in
+    let: "$sl10" := #"l"%go in
+    let: "$sl11" := #"d"%go in
+    slice.literal #stringT ["$sl0"; "$sl1"; "$sl2"; "$sl3"; "$sl4"; "$sl5"; "$sl6"; "$sl7"; "$sl8"; "$sl9"; "$sl10"; "$sl11"])) in
+    let: "$a1" := (![type.chanT #sliceT] "freeList") in
+    let: "$a2" := (![type.chanT #sliceT] "serverChan") in
+    (func_call #client) "$a0" "$a1" "$a2");;;
+    do:  (Fst (chan.receive (![type.chanT (type.structT [
+    ])] "done")));;;
+    (if: (![#stringT] "output") ≠ #"HELLO, WORLD"%go
+    then
+      do:  (let: "$a0" := (interface.make #stringT.id #"incorrect output"%go) in
+      Panic "$a0")
+    else do:  #());;;
+    return: #()).
+
+Definition HelloWorldAsyncX : go_string := "github.com/goose-lang/goose/testdata/examples/channel.HelloWorldAsyncX"%go.
+
+(* go: examples_xlated.go:13:6 *)
+Definition HelloWorldAsyncXⁱᵐᵖˡ : val :=
+  λ: <>,
+    exception_do (let: "ch" := (mem.alloc (type.zero_val #ptrT)) in
+    let: "$r0" := (let: "$a0" := #(W64 1) in
+    (func_call #channel.NewChannelRef #stringT) "$a0") in
+    do:  ("ch" <-[#ptrT] "$r0");;;
+    let: "$go" := (λ: <>,
+      exception_do (do:  (let: "$a0" := ((func_call #sys_hello_world) #()) in
+      (method_call #(ptrT.id channel.Channel.id) #"Send"%go (![#ptrT] "ch") #stringT) "$a0");;;
       return: #())
       ) in
     do:  (Fork ("$go" #()));;;
+    return: (![#ptrT] "ch")).
+
+Definition HelloWorldSyncX : go_string := "github.com/goose-lang/goose/testdata/examples/channel.HelloWorldSyncX"%go.
+
+(* go: examples_xlated.go:21:6 *)
+Definition HelloWorldSyncXⁱᵐᵖˡ : val :=
+  λ: <>,
+    exception_do (return: ((method_call #(ptrT.id channel.Channel.id) #"ReceiveDiscardOk"%go ((func_call #HelloWorldAsyncX) #()) #stringT) #())).
+
+Definition HelloWorldCancellableX : go_string := "github.com/goose-lang/goose/testdata/examples/channel.HelloWorldCancellableX"%go.
+
+(* Simulates the error/done channel components of Context
+
+   go: examples_xlated.go:26:6 *)
+Definition HelloWorldCancellableXⁱᵐᵖˡ : val :=
+  λ: "done" "err",
+    exception_do (let: "err" := (mem.alloc "err") in
+    let: "done" := (mem.alloc "done") in
+    let: "future" := (mem.alloc (type.zero_val #ptrT)) in
+    let: "$r0" := ((func_call #HelloWorldAsyncX) #()) in
+    do:  ("future" <-[#ptrT] "$r0");;;
+    let: "resolved" := (mem.alloc (type.zero_val #stringT)) in
+    let: "selected_case" := (mem.alloc (type.zero_val #uint64T)) in
+    let: ((("$ret0", "$ret1"), "$ret2"), "$ret3") := (let: "$a0" := (![#ptrT] "future") in
+    let: "$a1" := channel.SelectRecv in
+    let: "$a2" := #""%go in
+    let: "$a3" := (![#ptrT] "done") in
+    let: "$a4" := channel.SelectRecv in
+    let: "$a5" := (struct.make (type.structT [
+    ]) [{
+    }]) in
+    (func_call #channel.BlockingSelect2 #stringT (type.structT [
+    ])) "$a0" "$a1" "$a2" "$a3" "$a4" "$a5") in
+    let: "$r0" := "$ret0" in
+    let: "$r1" := "$ret1" in
+    let: "$r2" := "$ret2" in
+    let: "$r3" := "$ret3" in
+    do:  ("selected_case" <-[#uint64T] "$r0");;;
+    do:  ("resolved" <-[#stringT] "$r1");;;
+    do:  "$r2";;;
+    do:  "$r3";;;
+    (if: (![#uint64T] "selected_case") = #(W64 0)
+    then return: (![#stringT] "resolved")
+    else return: (![#stringT] (![#ptrT] "err")))).
+
+Definition HelloWorldWithTimeoutX : go_string := "github.com/goose-lang/goose/testdata/examples/channel.HelloWorldWithTimeoutX"%go.
+
+(* Uses cancellation as a timeout mechanism.
+
+   go: examples_xlated.go:39:6 *)
+Definition HelloWorldWithTimeoutXⁱᵐᵖˡ : val :=
+  λ: <>,
+    exception_do (let: "done" := (mem.alloc (type.zero_val #ptrT)) in
+    let: "$r0" := (let: "$a0" := #(W64 0) in
+    (func_call #channel.NewChannelRef (type.structT [
+    ])) "$a0") in
+    do:  ("done" <-[#ptrT] "$r0");;;
+    let: "errMsg" := (mem.alloc (type.zero_val #stringT)) in
+    let: "$r0" := #""%go in
+    do:  ("errMsg" <-[#stringT] "$r0");;;
     let: "$go" := (λ: <>,
-      exception_do (let: "ok" := (mem.alloc (type.zero_val #boolT)) in
-      let: ("$ret0", "$ret1") := ((method_call #(ptrT.id channel.Channel.id) #"Receive"%go (![#ptrT] "notifyCh") #uint64T) #()) in
-      let: "$r0" := "$ret0" in
-      let: "$r1" := "$ret1" in
-      do:  "$r0";;;
-      do:  ("ok" <-[#boolT] "$r1");;;
-      (if: (~ (![#boolT] "ok"))
-      then
-        (if: (![#stringT] (slice.elem_ref #stringT (![#sliceT] "results") #(W64 1))) ≠ #"thread2"%go
-        then
-          do:  (let: "$a0" := (interface.make #stringT.id #"Thread 2 received incorrect value"%go) in
-          Panic "$a0")
-        else do:  #());;;
-        do:  (let: "$a0" := #(W64 0) in
-        (method_call #(ptrT.id channel.Channel.id) #"Send"%go (![#ptrT] "done2") #uint64T) "$a0")
-      else do:  #());;;
+      exception_do (do:  (let: "$a0" := (#(W64 10) * time.Millisecond) in
+      (func_call #time.Sleep) "$a0");;;
+      let: "$r0" := #"operation timed out"%go in
+      do:  ("errMsg" <-[#stringT] "$r0");;;
+      do:  ((method_call #(ptrT.id channel.Channel.id) #"Close"%go (![#ptrT] "done") (type.structT [
+      ])) #());;;
       return: #())
       ) in
     do:  (Fork ("$go" #()));;;
+    return: (let: "$a0" := (![#ptrT] "done") in
+     let: "$a1" := "errMsg" in
+     (func_call #HelloWorldCancellableX) "$a0" "$a1")).
+
+Definition DSPExampleX : go_string := "github.com/goose-lang/goose/testdata/examples/channel.DSPExampleX"%go.
+
+(* prog3 from Actris 2.0 intro: https://arxiv.org/pdf/2010.15030
+
+   go: examples_xlated.go:52:6 *)
+Definition DSPExampleXⁱᵐᵖˡ : val :=
+  λ: <>,
+    exception_do (let: "c" := (mem.alloc (type.zero_val #ptrT)) in
+    let: "$r0" := (let: "$a0" := #(W64 0) in
+    (func_call #channel.NewChannelRef #ptrT) "$a0") in
+    do:  ("c" <-[#ptrT] "$r0");;;
+    let: "signal" := (mem.alloc (type.zero_val #ptrT)) in
+    let: "$r0" := (let: "$a0" := #(W64 0) in
+    (func_call #channel.NewChannelRef (type.structT [
+    ])) "$a0") in
+    do:  ("signal" <-[#ptrT] "$r0");;;
     let: "$go" := (λ: <>,
-      exception_do (let: "ok" := (mem.alloc (type.zero_val #boolT)) in
-      let: ("$ret0", "$ret1") := ((method_call #(ptrT.id channel.Channel.id) #"Receive"%go (![#ptrT] "notifyCh") #uint64T) #()) in
+      exception_do (let: "ptr" := (mem.alloc (type.zero_val #ptrT)) in
+      let: "$r0" := ((method_call #(ptrT.id channel.Channel.id) #"ReceiveDiscardOk"%go (![#ptrT] "c") #ptrT) #()) in
+      do:  ("ptr" <-[#ptrT] "$r0");;;
+      let: "$r0" := ((![#intT] (![#ptrT] "ptr")) + #(W64 2)) in
+      do:  ((![#ptrT] "ptr") <-[#intT] "$r0");;;
+      do:  (let: "$a0" := (struct.make (type.structT [
+      ]) [{
+      }]) in
+      (method_call #(ptrT.id channel.Channel.id) #"Send"%go (![#ptrT] "signal") (type.structT [
+      ])) "$a0");;;
+      return: #())
+      ) in
+    do:  (Fork ("$go" #()));;;
+    let: "val" := (mem.alloc (type.zero_val #intT)) in
+    let: "$r0" := #(W64 40) in
+    do:  ("val" <-[#intT] "$r0");;;
+    let: "ptr" := (mem.alloc (type.zero_val #ptrT)) in
+    let: "$r0" := "val" in
+    do:  ("ptr" <-[#ptrT] "$r0");;;
+    do:  (let: "$a0" := (![#ptrT] "ptr") in
+    (method_call #(ptrT.id channel.Channel.id) #"Send"%go (![#ptrT] "c") #ptrT) "$a0");;;
+    do:  ((method_call #(ptrT.id channel.Channel.id) #"ReceiveDiscardOk"%go (![#ptrT] "signal") (type.structT [
+    ])) #());;;
+    return: (![#intT] (![#ptrT] "ptr"))).
+
+Definition fibonacciX : go_string := "github.com/goose-lang/goose/testdata/examples/channel.fibonacciX"%go.
+
+(* https://go.dev/tour/concurrency/4
+
+   go: examples_xlated.go:68:6 *)
+Definition fibonacciXⁱᵐᵖˡ : val :=
+  λ: "n" "c",
+    exception_do (let: "c" := (mem.alloc "c") in
+    let: "n" := (mem.alloc "n") in
+    let: "y" := (mem.alloc (type.zero_val #intT)) in
+    let: "x" := (mem.alloc (type.zero_val #intT)) in
+    let: "$r0" := #(W64 0) in
+    let: "$r1" := #(W64 1) in
+    do:  ("x" <-[#intT] "$r0");;;
+    do:  ("y" <-[#intT] "$r1");;;
+    (let: "i" := (mem.alloc (type.zero_val #intT)) in
+    let: "$r0" := #(W64 0) in
+    do:  ("i" <-[#intT] "$r0");;;
+    (for: (λ: <>, int_lt (![#intT] "i") (![#intT] "n")); (λ: <>, do:  ("i" <-[#intT] ((![#intT] "i") + #(W64 1)))) := λ: <>,
+      do:  (let: "$a0" := (![#intT] "x") in
+      (method_call #(ptrT.id channel.Channel.id) #"Send"%go (![#ptrT] "c") #intT) "$a0");;;
+      let: "$r0" := (![#intT] "y") in
+      let: "$r1" := ((![#intT] "x") + (![#intT] "y")) in
+      do:  ("x" <-[#intT] "$r0");;;
+      do:  ("y" <-[#intT] "$r1")));;;
+    do:  ((method_call #(ptrT.id channel.Channel.id) #"Close"%go (![#ptrT] "c") #intT) #());;;
+    return: #()).
+
+Definition fib_consumerX : go_string := "github.com/goose-lang/goose/testdata/examples/channel.fib_consumerX"%go.
+
+(* go: examples_xlated.go:77:6 *)
+Definition fib_consumerXⁱᵐᵖˡ : val :=
+  λ: <>,
+    exception_do (let: "c" := (mem.alloc (type.zero_val #ptrT)) in
+    let: "$r0" := (let: "$a0" := #(W64 10) in
+    (func_call #channel.NewChannelRef #intT) "$a0") in
+    do:  ("c" <-[#ptrT] "$r0");;;
+    let: "$a0" := #(W64 10) in
+    let: "$a1" := (![#ptrT] "c") in
+    let: "$go" := (func_call #fibonacciX) in
+    do:  (Fork ("$go" "a0" "a1"));;;
+    let: "results" := (mem.alloc (type.zero_val #sliceT)) in
+    let: "$r0" := #slice.nil in
+    do:  ("results" <-[#sliceT] "$r0");;;
+    (for: (λ: <>, #true); (λ: <>, #()) := λ: <>,
+      let: "ok" := (mem.alloc (type.zero_val #boolT)) in
+      let: "i" := (mem.alloc (type.zero_val #intT)) in
+      let: ("$ret0", "$ret1") := ((method_call #(ptrT.id channel.Channel.id) #"Receive"%go (![#ptrT] "c") #intT) #()) in
       let: "$r0" := "$ret0" in
       let: "$r1" := "$ret1" in
-      do:  "$r0";;;
+      do:  ("i" <-[#intT] "$r0");;;
       do:  ("ok" <-[#boolT] "$r1");;;
       (if: (~ (![#boolT] "ok"))
-      then
-        (if: (![#stringT] (slice.elem_ref #stringT (![#sliceT] "results") #(W64 2))) ≠ #"thread3"%go
-        then
-          do:  (let: "$a0" := (interface.make #stringT.id #"Thread 3 received incorrect value"%go) in
-          Panic "$a0")
-        else do:  #());;;
-        do:  (let: "$a0" := #(W64 0) in
-        (method_call #(ptrT.id channel.Channel.id) #"Send"%go (![#ptrT] "done3") #uint64T) "$a0")
+      then break: #()
       else do:  #());;;
-      return: #())
-      ) in
-    do:  (Fork ("$go" #()));;;
-    let: "$r0" := #"thread1"%go in
-    do:  ((slice.elem_ref #stringT (![#sliceT] "results") #(W64 0)) <-[#stringT] "$r0");;;
-    let: "$r0" := #"thread2"%go in
-    do:  ((slice.elem_ref #stringT (![#sliceT] "results") #(W64 1)) <-[#stringT] "$r0");;;
-    let: "$r0" := #"thread3"%go in
-    do:  ((slice.elem_ref #stringT (![#sliceT] "results") #(W64 2)) <-[#stringT] "$r0");;;
-    do:  ((method_call #(ptrT.id channel.Channel.id) #"Close"%go (![#ptrT] "notifyCh") #uint64T) #());;;
-    do:  ((method_call #(ptrT.id channel.Channel.id) #"ReceiveDiscardOk"%go (![#ptrT] "done1") #uint64T) #());;;
-    do:  ((method_call #(ptrT.id channel.Channel.id) #"ReceiveDiscardOk"%go (![#ptrT] "done2") #uint64T) #());;;
-    do:  ((method_call #(ptrT.id channel.Channel.id) #"ReceiveDiscardOk"%go (![#ptrT] "done3") #uint64T) #());;;
-    return: #()).
+      let: "$r0" := (let: "$a0" := (![#sliceT] "results") in
+      let: "$a1" := ((let: "$sl0" := (![#intT] "i") in
+      slice.literal #intT ["$sl0"])) in
+      (slice.append #intT) "$a0" "$a1") in
+      do:  ("results" <-[#sliceT] "$r0"));;;
+    return: (![#sliceT] "results")).
 
-Definition CoordinatedChannelClose : go_string := "github.com/goose-lang/goose/testdata/examples/channel.CoordinatedChannelClose"%go.
+Definition select_nb_no_panicX : go_string := "github.com/goose-lang/goose/testdata/examples/channel.select_nb_no_panicX"%go.
 
-(* Example 5: Join sending goroutine before closing a buffered channel.
-   This should demonstrate the spec's ability to prevent closing on a channel
-   without joining all the senders.
+(* Show that it isn't possible to have 2 nonblocking ops that match.
 
-   go: examples.go:149:6 *)
-Definition CoordinatedChannelCloseⁱᵐᵖˡ : val :=
+   go: examples_xlated.go:92:6 *)
+Definition select_nb_no_panicXⁱᵐᵖˡ : val :=
   λ: <>,
-    exception_do (let: "bufCh" := (mem.alloc (type.zero_val #ptrT)) in
-    let: "$r0" := (let: "$a0" := #(W64 2) in
-    (func_call #channel.NewChannelRef #uint64T) "$a0") in
-    do:  ("bufCh" <-[#ptrT] "$r0");;;
-    let: "syncCh" := (mem.alloc (type.zero_val #ptrT)) in
+    exception_do (let: "ch" := (mem.alloc (type.zero_val #ptrT)) in
     let: "$r0" := (let: "$a0" := #(W64 0) in
-    (func_call #channel.NewChannelRef #uint64T) "$a0") in
-    do:  ("syncCh" <-[#ptrT] "$r0");;;
+    (func_call #channel.NewChannelRef (type.structT [
+    ])) "$a0") in
+    do:  ("ch" <-[#ptrT] "$r0");;;
     let: "$go" := (λ: <>,
-      exception_do (do:  (let: "$a0" := #(W64 42) in
-      (method_call #(ptrT.id channel.Channel.id) #"Send"%go (![#ptrT] "bufCh") #uint64T) "$a0");;;
-      do:  (let: "$a0" := #(W64 0) in
-      (method_call #(ptrT.id channel.Channel.id) #"Send"%go (![#ptrT] "syncCh") #uint64T) "$a0");;;
+      exception_do (let: "selected" := (mem.alloc (type.zero_val #boolT)) in
+      let: (("$ret0", "$ret1"), "$ret2") := (let: "$a0" := (![#ptrT] "ch") in
+      let: "$a1" := channel.SelectRecv in
+      let: "$a2" := (struct.make (type.structT [
+      ]) [{
+      }]) in
+      (func_call #channel.NonBlockingSelect1 (type.structT [
+      ])) "$a0" "$a1" "$a2") in
+      let: "$r0" := "$ret0" in
+      let: "$r1" := "$ret1" in
+      let: "$r2" := "$ret2" in
+      do:  ("selected" <-[#boolT] "$r0");;;
+      do:  "$r1";;;
+      do:  "$r2";;;
+      (if: ![#boolT] "selected"
+      then
+        do:  (let: "$a0" := (interface.make #stringT.id #"bad"%go) in
+        Panic "$a0")
+      else do:  #());;;
       return: #())
       ) in
     do:  (Fork ("$go" #()));;;
-    do:  (let: "$a0" := #(W64 84) in
-    (method_call #(ptrT.id channel.Channel.id) #"Send"%go (![#ptrT] "bufCh") #uint64T) "$a0");;;
-    do:  ((method_call #(ptrT.id channel.Channel.id) #"ReceiveDiscardOk"%go (![#ptrT] "syncCh") #uint64T) #());;;
-    do:  ((method_call #(ptrT.id channel.Channel.id) #"Close"%go (![#ptrT] "bufCh") #uint64T) #());;;
-    let: "ok1" := (mem.alloc (type.zero_val #boolT)) in
-    let: "val1" := (mem.alloc (type.zero_val #uint64T)) in
-    let: ("$ret0", "$ret1") := ((method_call #(ptrT.id channel.Channel.id) #"Receive"%go (![#ptrT] "bufCh") #uint64T) #()) in
+    let: "selected" := (mem.alloc (type.zero_val #boolT)) in
+    let: (("$ret0", "$ret1"), "$ret2") := (let: "$a0" := (![#ptrT] "ch") in
+    let: "$a1" := channel.SelectSend in
+    let: "$a2" := (struct.make (type.structT [
+    ]) [{
+    }]) in
+    (func_call #channel.NonBlockingSelect1 (type.structT [
+    ])) "$a0" "$a1" "$a2") in
     let: "$r0" := "$ret0" in
     let: "$r1" := "$ret1" in
-    do:  ("val1" <-[#uint64T] "$r0");;;
-    do:  ("ok1" <-[#boolT] "$r1");;;
-    let: "ok2" := (mem.alloc (type.zero_val #boolT)) in
-    let: "val2" := (mem.alloc (type.zero_val #uint64T)) in
-    let: ("$ret0", "$ret1") := ((method_call #(ptrT.id channel.Channel.id) #"Receive"%go (![#ptrT] "bufCh") #uint64T) #()) in
+    let: "$r2" := "$ret2" in
+    do:  ("selected" <-[#boolT] "$r0");;;
+    do:  "$r1";;;
+    do:  "$r2";;;
+    (if: ![#boolT] "selected"
+    then
+      do:  (let: "$a0" := (interface.make #stringT.id #"bad"%go) in
+      Panic "$a0")
+    else do:  #());;;
+    return: #()).
+
+Definition select_ready_case_no_panicX : go_string := "github.com/goose-lang/goose/testdata/examples/channel.select_ready_case_no_panicX"%go.
+
+(* Show that a guaranteed to be ready case makes default impossible
+
+   go: examples_xlated.go:107:6 *)
+Definition select_ready_case_no_panicXⁱᵐᵖˡ : val :=
+  λ: <>,
+    exception_do (let: "ch" := (mem.alloc (type.zero_val #ptrT)) in
+    let: "$r0" := (let: "$a0" := #(W64 0) in
+    (func_call #channel.NewChannelRef (type.structT [
+    ])) "$a0") in
+    do:  ("ch" <-[#ptrT] "$r0");;;
+    do:  ((method_call #(ptrT.id channel.Channel.id) #"Close"%go (![#ptrT] "ch") (type.structT [
+    ])) #());;;
+    let: "selected" := (mem.alloc (type.zero_val #boolT)) in
+    let: (("$ret0", "$ret1"), "$ret2") := (let: "$a0" := (![#ptrT] "ch") in
+    let: "$a1" := channel.SelectRecv in
+    let: "$a2" := (struct.make (type.structT [
+    ]) [{
+    }]) in
+    (func_call #channel.NonBlockingSelect1 (type.structT [
+    ])) "$a0" "$a1" "$a2") in
     let: "$r0" := "$ret0" in
     let: "$r1" := "$ret1" in
-    do:  ("val2" <-[#uint64T] "$r0");;;
-    do:  ("ok2" <-[#boolT] "$r1");;;
-    (if: (~ (![#boolT] "ok1")) || (~ (![#boolT] "ok2"))
+    let: "$r2" := "$ret2" in
+    do:  ("selected" <-[#boolT] "$r0");;;
+    do:  "$r1";;;
+    do:  "$r2";;;
+    (if: (~ (![#boolT] "selected"))
     then
-      do:  (let: "$a0" := (interface.make #stringT.id #"Channel shouldn't be empty yet"%go) in
+      do:  (let: "$a0" := (interface.make #stringT.id #"Shouldn't be possible!"%go) in
       Panic "$a0")
     else do:  #());;;
-    (if: (~ ((((![#uint64T] "val1") = #(W64 42)) && ((![#uint64T] "val2") = #(W64 84))) || (((![#uint64T] "val1") = #(W64 84)) && ((![#uint64T] "val2") = #(W64 42)))))
+    return: #()).
+
+Definition TestHelloWorldSyncX : go_string := "github.com/goose-lang/goose/testdata/examples/channel.TestHelloWorldSyncX"%go.
+
+(* Various tests that should panic when failing, which also means verifying { True } e { True } is
+   sufficient since panic can't be verified.
+
+   go: examples_xlated.go:119:6 *)
+Definition TestHelloWorldSyncXⁱᵐᵖˡ : val :=
+  λ: <>,
+    exception_do (let: "result" := (mem.alloc (type.zero_val #stringT)) in
+    let: "$r0" := ((func_call #HelloWorldSync) #()) in
+    do:  ("result" <-[#stringT] "$r0");;;
+    (if: (![#stringT] "result") ≠ #"Hello, World!"%go
+    then
+      do:  (let: "$a0" := (interface.make #stringT.id #"incorrect output"%go) in
+      Panic "$a0")
+    else do:  #());;;
+    return: #()).
+
+Definition TestHelloWorldWithTimeoutX : go_string := "github.com/goose-lang/goose/testdata/examples/channel.TestHelloWorldWithTimeoutX"%go.
+
+(* go: examples_xlated.go:126:6 *)
+Definition TestHelloWorldWithTimeoutXⁱᵐᵖˡ : val :=
+  λ: <>,
+    exception_do (let: "result" := (mem.alloc (type.zero_val #stringT)) in
+    let: "$r0" := ((func_call #HelloWorldWithTimeout) #()) in
+    do:  ("result" <-[#stringT] "$r0");;;
+    (if: ((![#stringT] "result") ≠ #"operation timed out"%go) && ((![#stringT] "result") ≠ #"Hello, World!"%go)
+    then
+      do:  (let: "$a0" := (interface.make #stringT.id #"incorrect output"%go) in
+      Panic "$a0")
+    else do:  #());;;
+    return: #()).
+
+Definition TestDSPExampleX : go_string := "github.com/goose-lang/goose/testdata/examples/channel.TestDSPExampleX"%go.
+
+(* go: examples_xlated.go:133:6 *)
+Definition TestDSPExampleXⁱᵐᵖˡ : val :=
+  λ: <>,
+    exception_do (let: "result" := (mem.alloc (type.zero_val #intT)) in
+    let: "$r0" := ((func_call #DSPExample) #()) in
+    do:  ("result" <-[#intT] "$r0");;;
+    (if: (![#intT] "result") ≠ #(W64 42)
+    then
+      do:  (let: "$a0" := (interface.make #stringT.id #"incorrect output"%go) in
+      Panic "$a0")
+    else do:  #());;;
+    return: #()).
+
+Definition TestFibConsumerX : go_string := "github.com/goose-lang/goose/testdata/examples/channel.TestFibConsumerX"%go.
+
+(* go: examples_xlated.go:140:6 *)
+Definition TestFibConsumerXⁱᵐᵖˡ : val :=
+  λ: <>,
+    exception_do (let: "result" := (mem.alloc (type.zero_val #sliceT)) in
+    let: "$r0" := ((func_call #fib_consumer) #()) in
+    do:  ("result" <-[#sliceT] "$r0");;;
+    let: "expected" := (mem.alloc (type.zero_val #sliceT)) in
+    let: "$r0" := ((let: "$sl0" := #(W64 0) in
+    let: "$sl1" := #(W64 1) in
+    let: "$sl2" := #(W64 1) in
+    let: "$sl3" := #(W64 2) in
+    let: "$sl4" := #(W64 3) in
+    let: "$sl5" := #(W64 5) in
+    let: "$sl6" := #(W64 8) in
+    let: "$sl7" := #(W64 13) in
+    let: "$sl8" := #(W64 21) in
+    let: "$sl9" := #(W64 34) in
+    slice.literal #intT ["$sl0"; "$sl1"; "$sl2"; "$sl3"; "$sl4"; "$sl5"; "$sl6"; "$sl7"; "$sl8"; "$sl9"])) in
+    do:  ("expected" <-[#sliceT] "$r0");;;
+    (if: (let: "$a0" := (![#sliceT] "result") in
+    slice.len "$a0") ≠ (let: "$a0" := (![#sliceT] "expected") in
+    slice.len "$a0")
     then
-      do:  (let: "$a0" := (interface.make #stringT.id #"Did not receive both expected values"%go) in
+      do:  (let: "$a0" := (interface.make #stringT.id #"incorrect output"%go) in
       Panic "$a0")
     else do:  #());;;
+    let: "$range" := (![#sliceT] "expected") in
+    (let: "i" := (mem.alloc (type.zero_val #intT)) in
+    slice.for_range #intT "$range" (λ: "$key" "$value",
+      do:  ("i" <-[#intT] "$key");;;
+      (if: (![#intT] (slice.elem_ref #intT (![#sliceT] "result") (![#intT] "i"))) ≠ (![#intT] (slice.elem_ref #intT (![#sliceT] "expected") (![#intT] "i")))
+      then
+        do:  (let: "$a0" := (interface.make #stringT.id #"incorrect output"%go) in
+        Panic "$a0")
+      else do:  #())));;;
+    return: #()).
+
+Definition TestSelectNbNoPanicX : go_string := "github.com/goose-lang/goose/testdata/examples/channel.TestSelectNbNoPanicX"%go.
+
+(* go: examples_xlated.go:153:6 *)
+Definition TestSelectNbNoPanicXⁱᵐᵖˡ : val :=
+  λ: <>,
+    exception_do (do:  ((func_call #select_nb_no_panic) #());;;
+    return: #()).
+
+Definition TestSelectReadyCaseNoPanicX : go_string := "github.com/goose-lang/goose/testdata/examples/channel.TestSelectReadyCaseNoPanicX"%go.
+
+(* go: examples_xlated.go:157:6 *)
+Definition TestSelectReadyCaseNoPanicXⁱᵐᵖˡ : val :=
+  λ: <>,
+    exception_do (do:  ((func_call #select_ready_case_no_panic) #());;;
+    return: #()).
+
+Definition clientX : go_string := "github.com/goose-lang/goose/testdata/examples/channel.clientX"%go.
+
+(* go: examples_xlated.go:164:6 *)
+Definition clientXⁱᵐᵖˡ : val :=
+  λ: "input" "freeList" "serverChan",
+    exception_do (let: "serverChan" := (mem.alloc "serverChan") in
+    let: "freeList" := (mem.alloc "freeList") in
+    let: "input" := (mem.alloc "input") in
+    let: "$range" := (![#sliceT] "input") in
+    (let: "letter" := (mem.alloc (type.zero_val #stringT)) in
+    slice.for_range #stringT "$range" (λ: "$key" "$value",
+      do:  ("letter" <-[#stringT] "$value");;;
+      do:  "$key";;;
+      let: "b" := (mem.alloc (type.zero_val #sliceT)) in
+      let: "v" := (mem.alloc (type.zero_val #sliceT)) in
+      let: "selected" := (mem.alloc (type.zero_val #boolT)) in
+      let: (("$ret0", "$ret1"), "$ret2") := (let: "$a0" := (![#ptrT] "freeList") in
+      let: "$a1" := channel.SelectRecv in
+      let: "$a2" := ((let: "$sl0" := #(W8 0) in
+      slice.literal #byteT ["$sl0"])) in
+      (func_call #channel.NonBlockingSelect1 #sliceT) "$a0" "$a1" "$a2") in
+      let: "$r0" := "$ret0" in
+      let: "$r1" := "$ret1" in
+      let: "$r2" := "$ret2" in
+      do:  ("selected" <-[#boolT] "$r0");;;
+      do:  ("v" <-[#sliceT] "$r1");;;
+      do:  "$r2";;;
+      (if: ![#boolT] "selected"
+      then
+        let: "$r0" := (![#sliceT] "v") in
+        do:  ("b" <-[#sliceT] "$r0")
+      else
+        let: "$r0" := ((let: "$sl0" := #(W8 0) in
+        slice.literal #byteT ["$sl0"])) in
+        do:  ("b" <-[#sliceT] "$r0"));;;
+      do:  (let: "$a0" := "b" in
+      let: "$a1" := (![#stringT] "letter") in
+      (func_call #load) "$a0" "$a1");;;
+      do:  (let: "$a0" := (![#sliceT] "b") in
+      (method_call #(ptrT.id channel.Channel.id) #"Send"%go (![#ptrT] "serverChan") #sliceT) "$a0")));;;
+    do:  ((method_call #(ptrT.id channel.Channel.id) #"Close"%go (![#ptrT] "serverChan") #sliceT) #());;;
     return: #()).
 
-Definition DoubleValues : go_string := "github.com/goose-lang/goose/testdata/examples/channel.DoubleValues"%go.
+Definition serverX : go_string := "github.com/goose-lang/goose/testdata/examples/channel.serverX"%go.
+
+(* go: examples_xlated.go:183:6 *)
+Definition serverXⁱᵐᵖˡ : val :=
+  λ: "output" "freeList" "serverChan" "join",
+    exception_do (let: "join" := (mem.alloc "join") in
+    let: "serverChan" := (mem.alloc "serverChan") in
+    let: "freeList" := (mem.alloc "freeList") in
+    let: "output" := (mem.alloc "output") in
+    (for: (λ: <>, #true); (λ: <>, #()) := λ: <>,
+      let: "ok" := (mem.alloc (type.zero_val #boolT)) in
+      let: "b" := (mem.alloc (type.zero_val #sliceT)) in
+      let: ("$ret0", "$ret1") := ((method_call #(ptrT.id channel.Channel.id) #"Receive"%go (![#ptrT] "serverChan") #sliceT) #()) in
+      let: "$r0" := "$ret0" in
+      let: "$r1" := "$ret1" in
+      do:  ("b" <-[#sliceT] "$r0");;;
+      do:  ("ok" <-[#boolT] "$r1");;;
+      (if: (~ (![#boolT] "ok"))
+      then
+        do:  (let: "$a0" := (struct.make (type.structT [
+        ]) [{
+        }]) in
+        (method_call #(ptrT.id channel.Channel.id) #"Send"%go (![#ptrT] "join") (type.structT [
+        ])) "$a0");;;
+        return: (#())
+      else do:  #());;;
+      do:  (let: "$a0" := "b" in
+      let: "$a1" := (![#ptrT] "output") in
+      (func_call #process) "$a0" "$a1");;;
+      do:  (let: "$a0" := (![#ptrT] "freeList") in
+      let: "$a1" := channel.SelectSend in
+      let: "$a2" := (![#sliceT] "b") in
+      (func_call #channel.NonBlockingSelect1 #sliceT) "$a0" "$a1" "$a2"));;;
+    return: #()).
 
-(* Example 6: A basic pipeline that just passes pointers
-   to a single worker who doubles the value of what they
-   point to.
+Definition LeakyBufferPipelineX : go_string := "github.com/goose-lang/goose/testdata/examples/channel.LeakyBufferPipelineX"%go.
 
-   go: examples.go:189:6 *)
-Definition DoubleValuesⁱᵐᵖˡ : val :=
+(* go: examples_xlated.go:204:6 *)
+Definition LeakyBufferPipelineXⁱᵐᵖˡ : val :=
   λ: <>,
-    exception_do (let: "val1" := (mem.alloc (type.zero_val #uint64T)) in
-    let: "$r0" := #(W64 5) in
-    do:  ("val1" <-[#uint64T] "$r0");;;
-    let: "val2" := (mem.alloc (type.zero_val #uint64T)) in
-    let: "$r0" := #(W64 10) in
-    do:  ("val2" <-[#uint64T] "$r0");;;
-    let: "val3" := (mem.alloc (type.zero_val #uint64T)) in
-    let: "$r0" := #(W64 15) in
-    do:  ("val3" <-[#uint64T] "$r0");;;
-    let: "values" := (mem.alloc (type.zero_val #sliceT)) in
-    let: "$r0" := (let: "$a0" := (![#sliceT] "values") in
-    let: "$a1" := ((let: "$sl0" := "val1" in
-    slice.literal #ptrT ["$sl0"])) in
-    (slice.append #ptrT) "$a0" "$a1") in
-    do:  ("values" <-[#sliceT] "$r0");;;
-    let: "$r0" := (let: "$a0" := (![#sliceT] "values") in
-    let: "$a1" := ((let: "$sl0" := "val2" in
-    slice.literal #ptrT ["$sl0"])) in
-    (slice.append #ptrT) "$a0" "$a1") in
-    do:  ("values" <-[#sliceT] "$r0");;;
-    let: "$r0" := (let: "$a0" := (![#sliceT] "values") in
-    let: "$a1" := ((let: "$sl0" := "val3" in
-    slice.literal #ptrT ["$sl0"])) in
-    (slice.append #ptrT) "$a0" "$a1") in
-    do:  ("values" <-[#sliceT] "$r0");;;
-    let: "ch" := (mem.alloc (type.zero_val #ptrT)) in
+    exception_do (let: "freeList" := (mem.alloc (type.zero_val #ptrT)) in
     let: "$r0" := (let: "$a0" := #(W64 0) in
-    (func_call #channel.NewChannelRef #ptrT) "$a0") in
-    do:  ("ch" <-[#ptrT] "$r0");;;
-    let: "done" := (mem.alloc (type.zero_val #ptrT)) in
+    (func_call #channel.NewChannelRef #sliceT) "$a0") in
+    do:  ("freeList" <-[#ptrT] "$r0");;;
+    let: "serverChan" := (mem.alloc (type.zero_val #ptrT)) in
     let: "$r0" := (let: "$a0" := #(W64 0) in
-    (func_call #channel.NewChannelRef #uint64T) "$a0") in
-    do:  ("done" <-[#ptrT] "$r0");;;
-    let: "$go" := (λ: <>,
-      exception_do ((for: (λ: <>, #true); (λ: <>, #()) := λ: <>,
-        let: "ok" := (mem.alloc (type.zero_val #boolT)) in
-        let: "ptr" := (mem.alloc (type.zero_val #ptrT)) in
-        let: ("$ret0", "$ret1") := ((method_call #(ptrT.id channel.Channel.id) #"Receive"%go (![#ptrT] "ch") #ptrT) #()) in
-        let: "$r0" := "$ret0" in
-        let: "$r1" := "$ret1" in
-        do:  ("ptr" <-[#ptrT] "$r0");;;
-        do:  ("ok" <-[#boolT] "$r1");;;
-        (if: (~ (![#boolT] "ok"))
-        then break: #()
-        else do:  #());;;
-        let: "$r0" := ((![#uint64T] (![#ptrT] "ptr")) * #(W64 2)) in
-        do:  ((![#ptrT] "ptr") <-[#uint64T] "$r0"));;;
-      do:  ((method_call #(ptrT.id channel.Channel.id) #"Close"%go (![#ptrT] "done") #uint64T) #());;;
-      return: #())
-      ) in
-    do:  (Fork ("$go" #()));;;
-    do:  (let: "$a0" := (![#ptrT] (slice.elem_ref #ptrT (![#sliceT] "values") #(W64 0))) in
-    (method_call #(ptrT.id channel.Channel.id) #"Send"%go (![#ptrT] "ch") #ptrT) "$a0");;;
-    do:  (let: "$a0" := (![#ptrT] (slice.elem_ref #ptrT (![#sliceT] "values") #(W64 1))) in
-    (method_call #(ptrT.id channel.Channel.id) #"Send"%go (![#ptrT] "ch") #ptrT) "$a0");;;
-    do:  (let: "$a0" := (![#ptrT] (slice.elem_ref #ptrT (![#sliceT] "values") #(W64 2))) in
-    (method_call #(ptrT.id channel.Channel.id) #"Send"%go (![#ptrT] "ch") #ptrT) "$a0");;;
-    do:  ((method_call #(ptrT.id channel.Channel.id) #"Close"%go (![#ptrT] "ch") #ptrT) #());;;
-    do:  ((method_call #(ptrT.id channel.Channel.id) #"Receive"%go (![#ptrT] "done") #uint64T) #());;;
-    (if: (~ ((((![#uint64T] "val1") = #(W64 10)) && ((![#uint64T] "val2") = #(W64 20))) && ((![#uint64T] "val3") = #(W64 30))))
+    (func_call #channel.NewChannelRef #sliceT) "$a0") in
+    do:  ("serverChan" <-[#ptrT] "$r0");;;
+    let: "join" := (mem.alloc (type.zero_val #ptrT)) in
+    let: "$r0" := (let: "$a0" := #(W64 0) in
+    (func_call #channel.NewChannelRef (type.structT [
+    ])) "$a0") in
+    do:  ("join" <-[#ptrT] "$r0");;;
+    let: "output" := (mem.alloc (type.zero_val #stringT)) in
+    let: "$r0" := #""%go in
+    do:  ("output" <-[#stringT] "$r0");;;
+    let: "$a0" := "output" in
+    let: "$a1" := (![#ptrT] "freeList") in
+    let: "$a2" := (![#ptrT] "serverChan") in
+    let: "$a3" := (![#ptrT] "join") in
+    let: "$go" := (func_call #serverX) in
+    do:  (Fork ("$go" "a0" "a1" "a2" "a3"));;;
+    do:  (let: "$a0" := ((let: "$sl0" := #"h"%go in
+    let: "$sl1" := #"e"%go in
+    let: "$sl2" := #"l"%go in
+    let: "$sl3" := #"l"%go in
+    let: "$sl4" := #"o"%go in
+    let: "$sl5" := #","%go in
+    let: "$sl6" := #" "%go in
+    let: "$sl7" := #"w"%go in
+    let: "$sl8" := #"o"%go in
+    let: "$sl9" := #"r"%go in
+    let: "$sl10" := #"l"%go in
+    let: "$sl11" := #"d"%go in
+    slice.literal #stringT ["$sl0"; "$sl1"; "$sl2"; "$sl3"; "$sl4"; "$sl5"; "$sl6"; "$sl7"; "$sl8"; "$sl9"; "$sl10"; "$sl11"])) in
+    let: "$a1" := (![#ptrT] "freeList") in
+    let: "$a2" := (![#ptrT] "serverChan") in
+    (func_call #clientX) "$a0" "$a1" "$a2");;;
+    do:  ((method_call #(ptrT.id channel.Channel.id) #"Receive"%go (![#ptrT] "join") (type.structT [
+    ])) #());;;
+    (if: (![#stringT] "output") ≠ #"HELLO, WORLD"%go
     then
-      do:  (let: "$a0" := (interface.make #stringT.id #"Values were not doubled correctly"%go) in
+      do:  (let: "$a0" := (interface.make #stringT.id #"incorrect output"%go) in
       Panic "$a0")
     else do:  #());;;
     return: #()).
 
 Definition vars' : list (go_string * go_type) := [].
 
-Definition functions' : list (go_string * val) := [(SendMessage, SendMessageⁱᵐᵖˡ); (JoinWithReceive, JoinWithReceiveⁱᵐᵖˡ); (JoinWithSend, JoinWithSendⁱᵐᵖˡ); (BroadcastNotification, BroadcastNotificationⁱᵐᵖˡ); (CoordinatedChannelClose, CoordinatedChannelCloseⁱᵐᵖˡ); (DoubleValues, DoubleValuesⁱᵐᵖˡ)].
+Definition functions' : list (go_string * val) := [(sys_hello_world, sys_hello_worldⁱᵐᵖˡ); (HelloWorldAsync, HelloWorldAsyncⁱᵐᵖˡ); (HelloWorldSync, HelloWorldSyncⁱᵐᵖˡ); (HelloWorldCancellable, HelloWorldCancellableⁱᵐᵖˡ); (HelloWorldWithTimeout, HelloWorldWithTimeoutⁱᵐᵖˡ); (DSPExample, DSPExampleⁱᵐᵖˡ); (fibonacci, fibonacciⁱᵐᵖˡ); (fib_consumer, fib_consumerⁱᵐᵖˡ); (select_nb_no_panic, select_nb_no_panicⁱᵐᵖˡ); (select_ready_case_no_panic, select_ready_case_no_panicⁱᵐᵖˡ); (TestHelloWorldSync, TestHelloWorldSyncⁱᵐᵖˡ); (TestHelloWorldWithTimeout, TestHelloWorldWithTimeoutⁱᵐᵖˡ); (TestDSPExample, TestDSPExampleⁱᵐᵖˡ); (TestFibConsumer, TestFibConsumerⁱᵐᵖˡ); (TestSelectNbNoPanic, TestSelectNbNoPanicⁱᵐᵖˡ); (TestSelectReadyCaseNoPanic, TestSelectReadyCaseNoPanicⁱᵐᵖˡ); (load, loadⁱᵐᵖˡ); (process, processⁱᵐᵖˡ); (client, clientⁱᵐᵖˡ); (server, serverⁱᵐᵖˡ); (LeakyBufferPipeline, LeakyBufferPipelineⁱᵐᵖˡ); (HelloWorldAsyncX, HelloWorldAsyncXⁱᵐᵖˡ); (HelloWorldSyncX, HelloWorldSyncXⁱᵐᵖˡ); (HelloWorldCancellableX, HelloWorldCancellableXⁱᵐᵖˡ); (HelloWorldWithTimeoutX, HelloWorldWithTimeoutXⁱᵐᵖˡ); (DSPExampleX, DSPExampleXⁱᵐᵖˡ); (fibonacciX, fibonacciXⁱᵐᵖˡ); (fib_consumerX, fib_consumerXⁱᵐᵖˡ); (select_nb_no_panicX, select_nb_no_panicXⁱᵐᵖˡ); (select_ready_case_no_panicX, select_ready_case_no_panicXⁱᵐᵖˡ); (TestHelloWorldSyncX, TestHelloWorldSyncXⁱᵐᵖˡ); (TestHelloWorldWithTimeoutX, TestHelloWorldWithTimeoutXⁱᵐᵖˡ); (TestDSPExampleX, TestDSPExampleXⁱᵐᵖˡ); (TestFibConsumerX, TestFibConsumerXⁱᵐᵖˡ); (TestSelectNbNoPanicX, TestSelectNbNoPanicXⁱᵐᵖˡ); (TestSelectReadyCaseNoPanicX, TestSelectReadyCaseNoPanicXⁱᵐᵖˡ); (clientX, clientXⁱᵐᵖˡ); (serverX, serverXⁱᵐᵖˡ); (LeakyBufferPipelineX, LeakyBufferPipelineXⁱᵐᵖˡ)].
 
 Definition msets' : list (go_string * (list (go_string * val))) := [].
 
@@ -351,13 +1055,15 @@ Definition msets' : list (go_string * (list (go_string * val))) := [].
     pkg_vars := vars';
     pkg_functions := functions';
     pkg_msets := msets';
-    pkg_imported_pkgs := [code.github_com.goose_lang.goose.model.channel.channel];
+    pkg_imported_pkgs := [code.strings.strings; code.time.time; code.github_com.goose_lang.goose.model.channel.channel];
   |}.
 
 Definition initialize' : val :=
   λ: <>,
     package.init #channel.chan_spec_raw_examples (λ: <>,
       exception_do (do:  (channel.initialize' #());;;
+      do:  (time.initialize' #());;;
+      do:  (strings.initialize' #());;;
       do:  (package.alloc channel.chan_spec_raw_examples #()))
       ).
 
diff --git a/new/generatedproof/github_com/goose_lang/goose/testdata/examples/channel.v b/new/generatedproof/github_com/goose_lang/goose/testdata/examples/channel.v
index 1ec7290a7..e3cd57f2f 100644
--- a/new/generatedproof/github_com/goose_lang/goose/testdata/examples/channel.v
+++ b/new/generatedproof/github_com/goose_lang/goose/testdata/examples/channel.v
@@ -1,5 +1,7 @@
 (* autogenerated by goose proofgen; do not modify *)
 Require Export New.proof.proof_prelude.
+Require Export New.generatedproof.strings.
+Require Export New.generatedproof.time.
 Require Export New.generatedproof.github_com.goose_lang.goose.model.channel.
 Require Export New.golang.theory.
 
@@ -20,6 +22,8 @@ Global Instance is_pkg_defined_pure_chan_spec_raw_examples : IsPkgDefinedPure ch
   {|
     is_pkg_defined_pure_def go_ctx :=
       is_pkg_defined_pure_single chan_spec_raw_examples ∧
+      is_pkg_defined_pure code.strings.strings ∧
+      is_pkg_defined_pure code.time.time ∧
       is_pkg_defined_pure code.github_com.goose_lang.goose.model.channel.channel;
   |}.
 
@@ -28,33 +32,167 @@ Global Program Instance is_pkg_defined_chan_spec_raw_examples : IsPkgDefined cha
   {|
     is_pkg_defined_def go_ctx :=
       (is_pkg_defined_single chan_spec_raw_examples ∗
+       is_pkg_defined code.strings.strings ∗
+       is_pkg_defined code.time.time ∗
        is_pkg_defined code.github_com.goose_lang.goose.model.channel.channel)%I
   |}.
 Final Obligation. iIntros. iFrame "#%". Qed.
 #[local] Opaque is_pkg_defined_single is_pkg_defined_pure_single.
 
-Global Instance wp_func_call_SendMessage :
-  WpFuncCall chan_spec_raw_examples.SendMessage _ (is_pkg_defined chan_spec_raw_examples) :=
+Global Instance wp_func_call_sys_hello_world :
+  WpFuncCall chan_spec_raw_examples.sys_hello_world _ (is_pkg_defined chan_spec_raw_examples) :=
   ltac:(solve_wp_func_call).
 
-Global Instance wp_func_call_JoinWithReceive :
-  WpFuncCall chan_spec_raw_examples.JoinWithReceive _ (is_pkg_defined chan_spec_raw_examples) :=
+Global Instance wp_func_call_HelloWorldAsync :
+  WpFuncCall chan_spec_raw_examples.HelloWorldAsync _ (is_pkg_defined chan_spec_raw_examples) :=
   ltac:(solve_wp_func_call).
 
-Global Instance wp_func_call_JoinWithSend :
-  WpFuncCall chan_spec_raw_examples.JoinWithSend _ (is_pkg_defined chan_spec_raw_examples) :=
+Global Instance wp_func_call_HelloWorldSync :
+  WpFuncCall chan_spec_raw_examples.HelloWorldSync _ (is_pkg_defined chan_spec_raw_examples) :=
   ltac:(solve_wp_func_call).
 
-Global Instance wp_func_call_BroadcastNotification :
-  WpFuncCall chan_spec_raw_examples.BroadcastNotification _ (is_pkg_defined chan_spec_raw_examples) :=
+Global Instance wp_func_call_HelloWorldCancellable :
+  WpFuncCall chan_spec_raw_examples.HelloWorldCancellable _ (is_pkg_defined chan_spec_raw_examples) :=
   ltac:(solve_wp_func_call).
 
-Global Instance wp_func_call_CoordinatedChannelClose :
-  WpFuncCall chan_spec_raw_examples.CoordinatedChannelClose _ (is_pkg_defined chan_spec_raw_examples) :=
+Global Instance wp_func_call_HelloWorldWithTimeout :
+  WpFuncCall chan_spec_raw_examples.HelloWorldWithTimeout _ (is_pkg_defined chan_spec_raw_examples) :=
   ltac:(solve_wp_func_call).
 
-Global Instance wp_func_call_DoubleValues :
-  WpFuncCall chan_spec_raw_examples.DoubleValues _ (is_pkg_defined chan_spec_raw_examples) :=
+Global Instance wp_func_call_DSPExample :
+  WpFuncCall chan_spec_raw_examples.DSPExample _ (is_pkg_defined chan_spec_raw_examples) :=
+  ltac:(solve_wp_func_call).
+
+Global Instance wp_func_call_fibonacci :
+  WpFuncCall chan_spec_raw_examples.fibonacci _ (is_pkg_defined chan_spec_raw_examples) :=
+  ltac:(solve_wp_func_call).
+
+Global Instance wp_func_call_fib_consumer :
+  WpFuncCall chan_spec_raw_examples.fib_consumer _ (is_pkg_defined chan_spec_raw_examples) :=
+  ltac:(solve_wp_func_call).
+
+Global Instance wp_func_call_select_nb_no_panic :
+  WpFuncCall chan_spec_raw_examples.select_nb_no_panic _ (is_pkg_defined chan_spec_raw_examples) :=
+  ltac:(solve_wp_func_call).
+
+Global Instance wp_func_call_select_ready_case_no_panic :
+  WpFuncCall chan_spec_raw_examples.select_ready_case_no_panic _ (is_pkg_defined chan_spec_raw_examples) :=
+  ltac:(solve_wp_func_call).
+
+Global Instance wp_func_call_TestHelloWorldSync :
+  WpFuncCall chan_spec_raw_examples.TestHelloWorldSync _ (is_pkg_defined chan_spec_raw_examples) :=
+  ltac:(solve_wp_func_call).
+
+Global Instance wp_func_call_TestHelloWorldWithTimeout :
+  WpFuncCall chan_spec_raw_examples.TestHelloWorldWithTimeout _ (is_pkg_defined chan_spec_raw_examples) :=
+  ltac:(solve_wp_func_call).
+
+Global Instance wp_func_call_TestDSPExample :
+  WpFuncCall chan_spec_raw_examples.TestDSPExample _ (is_pkg_defined chan_spec_raw_examples) :=
+  ltac:(solve_wp_func_call).
+
+Global Instance wp_func_call_TestFibConsumer :
+  WpFuncCall chan_spec_raw_examples.TestFibConsumer _ (is_pkg_defined chan_spec_raw_examples) :=
+  ltac:(solve_wp_func_call).
+
+Global Instance wp_func_call_TestSelectNbNoPanic :
+  WpFuncCall chan_spec_raw_examples.TestSelectNbNoPanic _ (is_pkg_defined chan_spec_raw_examples) :=
+  ltac:(solve_wp_func_call).
+
+Global Instance wp_func_call_TestSelectReadyCaseNoPanic :
+  WpFuncCall chan_spec_raw_examples.TestSelectReadyCaseNoPanic _ (is_pkg_defined chan_spec_raw_examples) :=
+  ltac:(solve_wp_func_call).
+
+Global Instance wp_func_call_load :
+  WpFuncCall chan_spec_raw_examples.load _ (is_pkg_defined chan_spec_raw_examples) :=
+  ltac:(solve_wp_func_call).
+
+Global Instance wp_func_call_process :
+  WpFuncCall chan_spec_raw_examples.process _ (is_pkg_defined chan_spec_raw_examples) :=
+  ltac:(solve_wp_func_call).
+
+Global Instance wp_func_call_client :
+  WpFuncCall chan_spec_raw_examples.client _ (is_pkg_defined chan_spec_raw_examples) :=
+  ltac:(solve_wp_func_call).
+
+Global Instance wp_func_call_server :
+  WpFuncCall chan_spec_raw_examples.server _ (is_pkg_defined chan_spec_raw_examples) :=
+  ltac:(solve_wp_func_call).
+
+Global Instance wp_func_call_LeakyBufferPipeline :
+  WpFuncCall chan_spec_raw_examples.LeakyBufferPipeline _ (is_pkg_defined chan_spec_raw_examples) :=
+  ltac:(solve_wp_func_call).
+
+Global Instance wp_func_call_HelloWorldAsyncX :
+  WpFuncCall chan_spec_raw_examples.HelloWorldAsyncX _ (is_pkg_defined chan_spec_raw_examples) :=
+  ltac:(solve_wp_func_call).
+
+Global Instance wp_func_call_HelloWorldSyncX :
+  WpFuncCall chan_spec_raw_examples.HelloWorldSyncX _ (is_pkg_defined chan_spec_raw_examples) :=
+  ltac:(solve_wp_func_call).
+
+Global Instance wp_func_call_HelloWorldCancellableX :
+  WpFuncCall chan_spec_raw_examples.HelloWorldCancellableX _ (is_pkg_defined chan_spec_raw_examples) :=
+  ltac:(solve_wp_func_call).
+
+Global Instance wp_func_call_HelloWorldWithTimeoutX :
+  WpFuncCall chan_spec_raw_examples.HelloWorldWithTimeoutX _ (is_pkg_defined chan_spec_raw_examples) :=
+  ltac:(solve_wp_func_call).
+
+Global Instance wp_func_call_DSPExampleX :
+  WpFuncCall chan_spec_raw_examples.DSPExampleX _ (is_pkg_defined chan_spec_raw_examples) :=
+  ltac:(solve_wp_func_call).
+
+Global Instance wp_func_call_fibonacciX :
+  WpFuncCall chan_spec_raw_examples.fibonacciX _ (is_pkg_defined chan_spec_raw_examples) :=
+  ltac:(solve_wp_func_call).
+
+Global Instance wp_func_call_fib_consumerX :
+  WpFuncCall chan_spec_raw_examples.fib_consumerX _ (is_pkg_defined chan_spec_raw_examples) :=
+  ltac:(solve_wp_func_call).
+
+Global Instance wp_func_call_select_nb_no_panicX :
+  WpFuncCall chan_spec_raw_examples.select_nb_no_panicX _ (is_pkg_defined chan_spec_raw_examples) :=
+  ltac:(solve_wp_func_call).
+
+Global Instance wp_func_call_select_ready_case_no_panicX :
+  WpFuncCall chan_spec_raw_examples.select_ready_case_no_panicX _ (is_pkg_defined chan_spec_raw_examples) :=
+  ltac:(solve_wp_func_call).
+
+Global Instance wp_func_call_TestHelloWorldSyncX :
+  WpFuncCall chan_spec_raw_examples.TestHelloWorldSyncX _ (is_pkg_defined chan_spec_raw_examples) :=
+  ltac:(solve_wp_func_call).
+
+Global Instance wp_func_call_TestHelloWorldWithTimeoutX :
+  WpFuncCall chan_spec_raw_examples.TestHelloWorldWithTimeoutX _ (is_pkg_defined chan_spec_raw_examples) :=
+  ltac:(solve_wp_func_call).
+
+Global Instance wp_func_call_TestDSPExampleX :
+  WpFuncCall chan_spec_raw_examples.TestDSPExampleX _ (is_pkg_defined chan_spec_raw_examples) :=
+  ltac:(solve_wp_func_call).
+
+Global Instance wp_func_call_TestFibConsumerX :
+  WpFuncCall chan_spec_raw_examples.TestFibConsumerX _ (is_pkg_defined chan_spec_raw_examples) :=
+  ltac:(solve_wp_func_call).
+
+Global Instance wp_func_call_TestSelectNbNoPanicX :
+  WpFuncCall chan_spec_raw_examples.TestSelectNbNoPanicX _ (is_pkg_defined chan_spec_raw_examples) :=
+  ltac:(solve_wp_func_call).
+
+Global Instance wp_func_call_TestSelectReadyCaseNoPanicX :
+  WpFuncCall chan_spec_raw_examples.TestSelectReadyCaseNoPanicX _ (is_pkg_defined chan_spec_raw_examples) :=
+  ltac:(solve_wp_func_call).
+
+Global Instance wp_func_call_clientX :
+  WpFuncCall chan_spec_raw_examples.clientX _ (is_pkg_defined chan_spec_raw_examples) :=
+  ltac:(solve_wp_func_call).
+
+Global Instance wp_func_call_serverX :
+  WpFuncCall chan_spec_raw_examples.serverX _ (is_pkg_defined chan_spec_raw_examples) :=
+  ltac:(solve_wp_func_call).
+
+Global Instance wp_func_call_LeakyBufferPipelineX :
+  WpFuncCall chan_spec_raw_examples.LeakyBufferPipelineX _ (is_pkg_defined chan_spec_raw_examples) :=
   ltac:(solve_wp_func_call).
 
 End names.