diff --git a/_CoqProject b/_CoqProject
index c10d88a6a..72fad8b3a 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -13,6 +13,7 @@
 -arg -w -arg -deprecated-typeclasses-transparency-without-locality
 # Iris-disabled warnings
 -arg -w -arg -notation-overridden,-redundant-canonical-projection,-unknown-warning,-argument-scope-delimiter
+-arg -w -arg +ambiguous-paths
 -Q external/stdpp/stdpp stdpp
 -Q external/stdpp/stdpp_unstable stdpp.unstable
 -Q external/stdpp/stdpp_bitvector stdpp.bitvector
diff --git a/external/Goose/github_com/goose_lang/goose/internal/examples/comments.v b/external/Goose/github_com/goose_lang/goose/internal/examples/comments.v
index 8ed826ce3..61cddea1e 100644
--- a/external/Goose/github_com/goose_lang/goose/internal/examples/comments.v
+++ b/external/Goose/github_com/goose_lang/goose/internal/examples/comments.v
@@ -3,7 +3,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 (* 0consts.go *)
 
diff --git a/external/Goose/github_com/goose_lang/goose/internal/examples/rfc1813.v b/external/Goose/github_com/goose_lang/goose/internal/examples/rfc1813.v
index 50b051427..849732b5e 100644
--- a/external/Goose/github_com/goose_lang/goose/internal/examples/rfc1813.v
+++ b/external/Goose/github_com/goose_lang/goose/internal/examples/rfc1813.v
@@ -3,7 +3,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition PROGRAM : expr := #(U32 100003).
 
diff --git a/external/Goose/github_com/goose_lang/goose/internal/examples/simpledb.v b/external/Goose/github_com/goose_lang/goose/internal/examples/simpledb.v
index 968b7d5ae..aee60a67c 100644
--- a/external/Goose/github_com/goose_lang/goose/internal/examples/simpledb.v
+++ b/external/Goose/github_com/goose_lang/goose/internal/examples/simpledb.v
@@ -4,7 +4,6 @@ From Goose Require github_com.tchajed.marshal.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 (* Package simpledb implements a one-table version of LevelDB
 
diff --git a/external/Goose/github_com/goose_lang/goose/internal/examples/trust_import.v b/external/Goose/github_com/goose_lang/goose/internal/examples/trust_import.v
index fc107c9d0..aa88562a8 100644
--- a/external/Goose/github_com/goose_lang/goose/internal/examples/trust_import.v
+++ b/external/Goose/github_com/goose_lang/goose/internal/examples/trust_import.v
@@ -4,7 +4,6 @@ From Perennial.goose_lang.trusted Require Import github_com.goose_lang.goose.int
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition Bar: val :=
   rec: "Bar" <> :=
diff --git a/external/Goose/github_com/goose_lang/goose/internal/examples/trust_import/trusted_example.v b/external/Goose/github_com/goose_lang/goose/internal/examples/trust_import/trusted_example.v
index 28f8d50e5..277a7de28 100644
--- a/external/Goose/github_com/goose_lang/goose/internal/examples/trust_import/trusted_example.v
+++ b/external/Goose/github_com/goose_lang/goose/internal/examples/trust_import/trusted_example.v
@@ -3,7 +3,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition Foo: val :=
   rec: "Foo" <> :=
diff --git a/external/Goose/github_com/goose_lang/goose/internal/examples/unittest/generic.v b/external/Goose/github_com/goose_lang/goose/internal/examples/unittest/generic.v
index 7c1f40357..d92568009 100644
--- a/external/Goose/github_com/goose_lang/goose/internal/examples/unittest/generic.v
+++ b/external/Goose/github_com/goose_lang/goose/internal/examples/unittest/generic.v
@@ -3,7 +3,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition SliceMap (T:ty) (U:ty): val :=
   rec: "SliceMap" "f" "s" :=
diff --git a/external/Goose/github_com/goose_lang/std.v b/external/Goose/github_com/goose_lang/std.v
index b3c3e9c6a..185ac1ef6 100644
--- a/external/Goose/github_com/goose_lang/std.v
+++ b/external/Goose/github_com/goose_lang/std.v
@@ -3,7 +3,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 (* BytesEqual returns if the two byte slices are equal. *)
 Definition BytesEqual: val :=
diff --git a/external/Goose/github_com/mit_pdos/go_journal/alloc.v b/external/Goose/github_com/mit_pdos/go_journal/alloc.v
index e320b9989..e51d43eef 100644
--- a/external/Goose/github_com/mit_pdos/go_journal/alloc.v
+++ b/external/Goose/github_com/mit_pdos/go_journal/alloc.v
@@ -3,7 +3,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 (* Allocator uses a bit map to allocate and free numbers. Bit 0
    corresponds to number 0, bit 1 to 1, and so on. *)
diff --git a/external/Goose/github_com/mit_pdos/go_journal/lockmap.v b/external/Goose/github_com/mit_pdos/go_journal/lockmap.v
index d34e67869..ce19ece30 100644
--- a/external/Goose/github_com/mit_pdos/go_journal/lockmap.v
+++ b/external/Goose/github_com/mit_pdos/go_journal/lockmap.v
@@ -3,7 +3,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 (* lockmap is a sharded lock map.
 
diff --git a/external/Goose/github_com/mit_pdos/go_journal/util.v b/external/Goose/github_com/mit_pdos/go_journal/util.v
index d8e8c0901..7520cd4e0 100644
--- a/external/Goose/github_com/mit_pdos/go_journal/util.v
+++ b/external/Goose/github_com/mit_pdos/go_journal/util.v
@@ -3,7 +3,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition Debug : expr := #0.
 
diff --git a/external/Goose/github_com/mit_pdos/go_nfsd/nfstypes.v b/external/Goose/github_com/mit_pdos/go_nfsd/nfstypes.v
index 353dc6249..6dfca3b47 100644
--- a/external/Goose/github_com/mit_pdos/go_nfsd/nfstypes.v
+++ b/external/Goose/github_com/mit_pdos/go_nfsd/nfstypes.v
@@ -3,7 +3,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition PROGRAM : expr := #(U32 100003).
 
diff --git a/external/Goose/github_com/mit_pdos/gokv/bank.v b/external/Goose/github_com/mit_pdos/gokv/bank.v
index 140504208..b73a72338 100644
--- a/external/Goose/github_com/mit_pdos/gokv/bank.v
+++ b/external/Goose/github_com/mit_pdos/gokv/bank.v
@@ -6,7 +6,6 @@ From Goose Require github_com.tchajed.marshal.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition BAL_TOTAL : expr := #1000.
 
diff --git a/external/Goose/github_com/mit_pdos/gokv/dmvcc/example.v b/external/Goose/github_com/mit_pdos/gokv/dmvcc/example.v
index 67f6aa366..cfcfb41d2 100644
--- a/external/Goose/github_com/mit_pdos/gokv/dmvcc/example.v
+++ b/external/Goose/github_com/mit_pdos/gokv/dmvcc/example.v
@@ -7,7 +7,6 @@ From Goose Require github_com.mit_pdos.gokv.dmvcc.txnmgr.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition main: val :=
   rec: "main" <> :=
diff --git a/external/Goose/github_com/mit_pdos/gokv/dmvcc/index.v b/external/Goose/github_com/mit_pdos/gokv/dmvcc/index.v
index d37a4ce27..5d8a91fd2 100644
--- a/external/Goose/github_com/mit_pdos/gokv/dmvcc/index.v
+++ b/external/Goose/github_com/mit_pdos/gokv/dmvcc/index.v
@@ -4,7 +4,6 @@ From Goose Require github_com.mit_pdos.vmvcc.index.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 (* 0_server.go *)
 
diff --git a/external/Goose/github_com/mit_pdos/gokv/dmvcc/prophname.v b/external/Goose/github_com/mit_pdos/gokv/dmvcc/prophname.v
index 8bc627253..837317346 100644
--- a/external/Goose/github_com/mit_pdos/gokv/dmvcc/prophname.v
+++ b/external/Goose/github_com/mit_pdos/gokv/dmvcc/prophname.v
@@ -3,7 +3,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition Get: val :=
   rec: "Get" <> :=
diff --git a/external/Goose/github_com/mit_pdos/gokv/dmvcc/txn.v b/external/Goose/github_com/mit_pdos/gokv/dmvcc/txn.v
index 7e2640d0c..1a37467d5 100644
--- a/external/Goose/github_com/mit_pdos/gokv/dmvcc/txn.v
+++ b/external/Goose/github_com/mit_pdos/gokv/dmvcc/txn.v
@@ -8,7 +8,6 @@ From Perennial.goose_lang.trusted Require Import github_com.mit_pdos.vmvcc.trust
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition Clerk := struct.decl [
   "p" :: ProphIdT;
diff --git a/external/Goose/github_com/mit_pdos/gokv/dmvcc/txncoordinator.v b/external/Goose/github_com/mit_pdos/gokv/dmvcc/txncoordinator.v
index 4de6e289e..a91432136 100644
--- a/external/Goose/github_com/mit_pdos/gokv/dmvcc/txncoordinator.v
+++ b/external/Goose/github_com/mit_pdos/gokv/dmvcc/txncoordinator.v
@@ -4,7 +4,6 @@ From Goose Require github_com.mit_pdos.gokv.dmvcc.index.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 (* 0_server.go *)
 
diff --git a/external/Goose/github_com/mit_pdos/gokv/dmvcc/txnmgr.v b/external/Goose/github_com/mit_pdos/gokv/dmvcc/txnmgr.v
index 0bc566edf..49a91ec68 100644
--- a/external/Goose/github_com/mit_pdos/gokv/dmvcc/txnmgr.v
+++ b/external/Goose/github_com/mit_pdos/gokv/dmvcc/txnmgr.v
@@ -3,7 +3,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 (* clerk.go *)
 
diff --git a/external/Goose/github_com/mit_pdos/gokv/erpc.v b/external/Goose/github_com/mit_pdos/gokv/erpc.v
index de7ec7ef8..aa4c20138 100644
--- a/external/Goose/github_com/mit_pdos/gokv/erpc.v
+++ b/external/Goose/github_com/mit_pdos/gokv/erpc.v
@@ -5,7 +5,6 @@ From Goose Require github_com.tchajed.marshal.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 (* Implements "exactly-once RPCs" with a reply table. *)
 
diff --git a/external/Goose/github_com/mit_pdos/gokv/kv.v b/external/Goose/github_com/mit_pdos/gokv/kv.v
index 86a559d96..c6aee99c0 100644
--- a/external/Goose/github_com/mit_pdos/gokv/kv.v
+++ b/external/Goose/github_com/mit_pdos/gokv/kv.v
@@ -3,7 +3,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition Kv := struct.decl [
   "Put" :: (stringT -> stringT -> unitT)%ht;
diff --git a/external/Goose/github_com/mit_pdos/gokv/lockservice.v b/external/Goose/github_com/mit_pdos/gokv/lockservice.v
index b352cf123..cd1aaef4e 100644
--- a/external/Goose/github_com/mit_pdos/gokv/lockservice.v
+++ b/external/Goose/github_com/mit_pdos/gokv/lockservice.v
@@ -4,7 +4,6 @@ From Goose Require github_com.mit_pdos.gokv.kv.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition LockClerk := struct.decl [
   "kv" :: ptrT
diff --git a/external/Goose/github_com/mit_pdos/gokv/map_marshal.v b/external/Goose/github_com/mit_pdos/gokv/map_marshal.v
index f2c3d646d..507f99d8f 100644
--- a/external/Goose/github_com/mit_pdos/gokv/map_marshal.v
+++ b/external/Goose/github_com/mit_pdos/gokv/map_marshal.v
@@ -4,7 +4,6 @@ From Goose Require github_com.tchajed.marshal.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition EncodeMapU64ToU64: val :=
   rec: "EncodeMapU64ToU64" "kvs" :=
diff --git a/external/Goose/github_com/mit_pdos/gokv/map_string_marshal.v b/external/Goose/github_com/mit_pdos/gokv/map_string_marshal.v
index 98662902f..30f6c77a1 100644
--- a/external/Goose/github_com/mit_pdos/gokv/map_string_marshal.v
+++ b/external/Goose/github_com/mit_pdos/gokv/map_string_marshal.v
@@ -4,7 +4,6 @@ From Goose Require github_com.tchajed.marshal.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition EncodeStringMap: val :=
   rec: "EncodeStringMap" "kvs" :=
diff --git a/external/Goose/github_com/mit_pdos/gokv/tutorial/basics.v b/external/Goose/github_com/mit_pdos/gokv/tutorial/basics.v
index 6cd79d453..e7c0c1340 100644
--- a/external/Goose/github_com/mit_pdos/gokv/tutorial/basics.v
+++ b/external/Goose/github_com/mit_pdos/gokv/tutorial/basics.v
@@ -3,7 +3,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition Tracker := struct.decl [
   "mu" :: ptrT;
diff --git a/external/Goose/github_com/mit_pdos/gokv/tutorial/queue.v b/external/Goose/github_com/mit_pdos/gokv/tutorial/queue.v
index daadd54f5..9c8cd0876 100644
--- a/external/Goose/github_com/mit_pdos/gokv/tutorial/queue.v
+++ b/external/Goose/github_com/mit_pdos/gokv/tutorial/queue.v
@@ -3,7 +3,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition Queue := struct.decl [
   "queue" :: slice.T uint64T;
diff --git a/external/Goose/github_com/mit_pdos/gokv/vrsm/e.v b/external/Goose/github_com/mit_pdos/gokv/vrsm/e.v
index bdc7d68f4..3f2221a31 100644
--- a/external/Goose/github_com/mit_pdos/gokv/vrsm/e.v
+++ b/external/Goose/github_com/mit_pdos/gokv/vrsm/e.v
@@ -4,7 +4,6 @@ From Goose Require github_com.tchajed.marshal.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Notation Error := uint64T (only parsing).
 
diff --git a/external/Goose/github_com/mit_pdos/pav/cryptoffi.v b/external/Goose/github_com/mit_pdos/pav/cryptoffi.v
index f8b20c31c..781713359 100644
--- a/external/Goose/github_com/mit_pdos/pav/cryptoffi.v
+++ b/external/Goose/github_com/mit_pdos/pav/cryptoffi.v
@@ -2,7 +2,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition HashLen : expr := #32.
 
diff --git a/external/Goose/github_com/mit_pdos/pav/cryptoutil.v b/external/Goose/github_com/mit_pdos/pav/cryptoutil.v
index 018e8c935..6c4005863 100644
--- a/external/Goose/github_com/mit_pdos/pav/cryptoutil.v
+++ b/external/Goose/github_com/mit_pdos/pav/cryptoutil.v
@@ -4,7 +4,6 @@ From Goose Require github_com.mit_pdos.pav.cryptoffi.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Notation Hasher := (slice.T byteT) (only parsing).
 
diff --git a/external/Goose/github_com/mit_pdos/pav/marshalutil.v b/external/Goose/github_com/mit_pdos/pav/marshalutil.v
index 4477e6ca3..e8fdc0e46 100644
--- a/external/Goose/github_com/mit_pdos/pav/marshalutil.v
+++ b/external/Goose/github_com/mit_pdos/pav/marshalutil.v
@@ -4,7 +4,6 @@ From Goose Require github_com.tchajed.marshal.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Notation errorTy := boolT (only parsing).
 
diff --git a/external/Goose/github_com/mit_pdos/pav/merkle.v b/external/Goose/github_com/mit_pdos/pav/merkle.v
index e4e53ee14..82f8048cb 100644
--- a/external/Goose/github_com/mit_pdos/pav/merkle.v
+++ b/external/Goose/github_com/mit_pdos/pav/merkle.v
@@ -6,7 +6,6 @@ From Goose Require github_com.mit_pdos.pav.cryptoutil.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Notation errorTy := boolT (only parsing).
 
diff --git a/external/Goose/github_com/mit_pdos/perennial_examples/alloc.v b/external/Goose/github_com/mit_pdos/perennial_examples/alloc.v
index afb5007fd..69791754b 100644
--- a/external/Goose/github_com/mit_pdos/perennial_examples/alloc.v
+++ b/external/Goose/github_com/mit_pdos/perennial_examples/alloc.v
@@ -3,7 +3,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition unit := struct.decl [
 ].
diff --git a/external/Goose/github_com/mit_pdos/rsm/distx.v b/external/Goose/github_com/mit_pdos/rsm/distx.v
index 536cf5748..f173088c0 100644
--- a/external/Goose/github_com/mit_pdos/rsm/distx.v
+++ b/external/Goose/github_com/mit_pdos/rsm/distx.v
@@ -4,7 +4,6 @@ From Goose Require github_com.goose_lang.std.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition Value := struct.decl [
   "b" :: boolT;
diff --git a/external/Goose/github_com/mit_pdos/rsm/mpaxos.v b/external/Goose/github_com/mit_pdos/rsm/mpaxos.v
index 29fd2325c..b450c9128 100644
--- a/external/Goose/github_com/mit_pdos/rsm/mpaxos.v
+++ b/external/Goose/github_com/mit_pdos/rsm/mpaxos.v
@@ -3,7 +3,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition Paxos := struct.decl [
 ].
diff --git a/external/Goose/github_com/mit_pdos/rsm/pcr.v b/external/Goose/github_com/mit_pdos/rsm/pcr.v
new file mode 100644
index 000000000..7ec1194c7
--- /dev/null
+++ b/external/Goose/github_com/mit_pdos/rsm/pcr.v
@@ -0,0 +1,1603 @@
+(* autogenerated from github.com/mit-pdos/rsm/pcr *)
+From Perennial.goose_lang Require Import prelude.
+From Goose Require github_com.goose_lang.std.
+
+Section code.
+Context `{ext_ty: ext_types}.
+
+Definition Value := struct.decl [
+  "b" :: boolT;
+  "s" :: stringT
+].
+
+Definition WriteEntry := struct.decl [
+  "k" :: stringT;
+  "v" :: struct.t Value
+].
+
+Definition N_SHARDS : expr := #2.
+
+(* @ts
+   Starting timestamp of this version, and also ending timestamp of the next
+   version. Lifetime is a half-open interval: [ts of this, ts of next).
+
+   @val
+   Value of this version. *)
+Definition Version := struct.decl [
+  "ts" :: uint64T;
+  "val" :: struct.t Value
+].
+
+Definition Tuple__Own: val :=
+  rec: "Tuple__Own" "tuple" "tid" :=
+    #false.
+
+Definition Tuple__ReadVersion: val :=
+  rec: "Tuple__ReadVersion" "tuple" "tid" :=
+    (struct.mk Version [
+     ], #false).
+
+Definition Tuple__Extend: val :=
+  rec: "Tuple__Extend" "tuple" "tid" :=
+    #false.
+
+Definition Tuple__AppendVersion: val :=
+  rec: "Tuple__AppendVersion" "tuple" "tid" "val" :=
+    #().
+
+Definition Tuple__KillVersion: val :=
+  rec: "Tuple__KillVersion" "tuple" "tid" :=
+    #().
+
+Definition Tuple__Free: val :=
+  rec: "Tuple__Free" "tuple" :=
+    #().
+
+(* @owned
+   Write lock of this tuple. Acquired before committing.
+
+   @tslast
+   Timestamp of the last reader or last writer + 1.
+
+   @vers
+   Versions. *)
+Definition Tuple := struct.decl [
+  "latch" :: ptrT;
+  "owned" :: boolT;
+  "tslast" :: uint64T;
+  "vers" :: slice.T (struct.t Version)
+].
+
+Definition Index := struct.decl [
+].
+
+Definition Index__GetTuple: val :=
+  rec: "Index__GetTuple" "idx" "key" :=
+    struct.new Tuple [
+    ].
+
+Definition Cmd := struct.decl [
+  "kind" :: uint64T;
+  "ts" :: uint64T;
+  "pwrs" :: slice.T (struct.t WriteEntry);
+  "key" :: stringT
+].
+
+Definition TxnLog := struct.decl [
+].
+
+(* Arguments:
+   @ts: Transaction timestamp.
+
+   Return values:
+   @lsn (uint64): @lsn = 0 indicates failure; otherwise, this indicates the
+   logical index this command is supposed to be placed at.
+
+   @term (uint64): The @term this command is supposed to have.
+
+   Notes:
+   1) Passing @lsn and @term to @WaitUntilSafe allows us to determine whether
+   the command we just submitted actually get safely replicated (and wait until
+   that happens up to some timeout).
+
+   2) Although @term is redundant in that we can always detect failure by
+   comparing the content of the command to some application state (e.g., a reply
+   table), it can be seen as a performance optimization that would allow us to
+   know earlier that our command has not been safely replicated (and hence
+   resubmit). Another upside of having it would be that this allows the check to
+   be done in a general way, without relying on the content. *)
+Definition TxnLog__SubmitCommit: val :=
+  rec: "TxnLog__SubmitCommit" "log" "ts" "pwrs" :=
+    (#0, #0).
+
+(* Arguments and return values: see description of @SubmitPrepare. *)
+Definition TxnLog__SubmitAbort: val :=
+  rec: "TxnLog__SubmitAbort" "log" "ts" :=
+    (#0, #0).
+
+(* Arguments:
+   @lsn: LSN of the command whose replication to wait for.
+
+   @term: Expected term of the command.
+
+   Return values:
+   @replicated (bool): If @true, then the command at @lsn has term @term;
+   otherwise, we know nothing, but the upper layer is suggested to resubmit the
+   command.
+
+   TODO: maybe this is a bad interface since now the users would have to make
+   another call. *)
+Definition TxnLog__WaitUntilSafe: val :=
+  rec: "TxnLog__WaitUntilSafe" "log" "lsn" "term" :=
+    #false.
+
+(* Argument:
+   @lsn: Logical index of the queried command. *)
+Definition TxnLog__Lookup: val :=
+  rec: "TxnLog__Lookup" "log" "lsn" :=
+    (struct.mk Cmd [
+     ], #false).
+
+Definition PrepareProposal := struct.decl [
+  "rank" :: uint64T;
+  "dec" :: boolT
+].
+
+Definition PrepareStatusEntry := struct.decl [
+  "rankl" :: uint64T;
+  "prep" :: struct.t PrepareProposal
+].
+
+Definition Replica := struct.decl [
+  "mu" :: ptrT;
+  "rid" :: uint64T;
+  "txnlog" :: ptrT;
+  "lsna" :: uint64T;
+  "prepm" :: mapT (slice.T (struct.t WriteEntry));
+  "ptgsm" :: mapT (slice.T uint64T);
+  "pstbl" :: mapT (struct.t PrepareStatusEntry);
+  "txntbl" :: mapT boolT;
+  "idx" :: ptrT;
+  "rps" :: mapT ptrT;
+  "leader" :: uint64T
+].
+
+(* Arguments:
+   @ts: Transaction timestamp.
+
+   Return values:
+   @terminated: Whether txn @ts has terminated (committed or aborted). *)
+Definition Replica__queryTxnTermination: val :=
+  rec: "Replica__queryTxnTermination" "rp" "ts" :=
+    let: (<>, "terminated") := MapGet (struct.loadF Replica "txntbl" "rp") "ts" in
+    "terminated".
+
+Definition Replica__QueryTxnTermination: val :=
+  rec: "Replica__QueryTxnTermination" "rp" "ts" :=
+    lock.acquire (struct.loadF Replica "mu" "rp");;
+    let: "terminated" := Replica__queryTxnTermination "rp" "ts" in
+    lock.release (struct.loadF Replica "mu" "rp");;
+    "terminated".
+
+(* Arguments:
+   @ts: Transaction timestamp.
+
+   Return values:
+   @ok: If @true, this transaction is committed. *)
+Definition Replica__Commit: val :=
+  rec: "Replica__Commit" "rp" "ts" "pwrs" :=
+    let: "committed" := Replica__QueryTxnTermination "rp" "ts" in
+    (if: "committed"
+    then #true
+    else
+      let: ("lsn", "term") := TxnLog__SubmitCommit (struct.loadF Replica "txnlog" "rp") "ts" "pwrs" in
+      (if: "lsn" = #0
+      then #false
+      else
+        let: "safe" := TxnLog__WaitUntilSafe (struct.loadF Replica "txnlog" "rp") "lsn" "term" in
+        (if: (~ "safe")
+        then #false
+        else #true))).
+
+(* Arguments:
+   @ts: Transaction timestamp.
+
+   Return values:
+   @ok: If @true, this transaction is aborted. *)
+Definition Replica__Abort: val :=
+  rec: "Replica__Abort" "rp" "ts" :=
+    let: "aborted" := Replica__QueryTxnTermination "rp" "ts" in
+    (if: "aborted"
+    then #true
+    else
+      let: ("lsn", "term") := TxnLog__SubmitAbort (struct.loadF Replica "txnlog" "rp") "ts" in
+      (if: "lsn" = #0
+      then #false
+      else
+        let: "safe" := TxnLog__WaitUntilSafe (struct.loadF Replica "txnlog" "rp") "lsn" "term" in
+        (if: (~ "safe")
+        then #false
+        else #true))).
+
+(* Arguments:
+   @ts: Transaction timestamp.
+   @key: Key to be read.
+
+   Return values:
+   @value: Value of the key.
+   @ok: @value is meaningful iff @ok is true. *)
+Definition Replica__Read: val :=
+  rec: "Replica__Read" "rp" "ts" "key" :=
+    let: "terminated" := Replica__QueryTxnTermination "rp" "ts" in
+    (if: "terminated"
+    then
+      (struct.mk Version [
+       ], #false)
+    else
+      let: "tpl" := Index__GetTuple (struct.loadF Replica "idx" "rp") "key" in
+      Tuple__Extend "tpl" "ts";;
+      let: ("v", "ok") := Tuple__ReadVersion "tpl" "ts" in
+      ("v", "ok")).
+
+Definition Replica__acquire: val :=
+  rec: "Replica__acquire" "rp" "ts" "pwrs" :=
+    let: "pos" := ref_to uint64T #0 in
+    Skip;;
+    (for: (λ: <>, (![uint64T] "pos") < (slice.len "pwrs")); (λ: <>, Skip) := λ: <>,
+      let: "ent" := SliceGet (struct.t WriteEntry) "pwrs" (![uint64T] "pos") in
+      let: "tpl" := Index__GetTuple (struct.loadF Replica "idx" "rp") (struct.get WriteEntry "k" "ent") in
+      let: "ret" := Tuple__Own "tpl" "ts" in
+      (if: (~ "ret")
+      then Break
+      else
+        "pos" <-[uint64T] ((![uint64T] "pos") + #1);;
+        Continue));;
+    (if: (![uint64T] "pos") < (slice.len "pwrs")
+    then
+      let: "i" := ref_to uint64T #0 in
+      Skip;;
+      (for: (λ: <>, (![uint64T] "i") < (![uint64T] "pos")); (λ: <>, Skip) := λ: <>,
+        let: "ent" := SliceGet (struct.t WriteEntry) "pwrs" (![uint64T] "i") in
+        let: "tpl" := Index__GetTuple (struct.loadF Replica "idx" "rp") (struct.get WriteEntry "k" "ent") in
+        Tuple__Free "tpl";;
+        "i" <-[uint64T] ((![uint64T] "i") + #1);;
+        Continue);;
+      #false
+    else #true).
+
+Definition RESULT_OK : expr := #0.
+
+Definition RESULT_COMMITTED_TXN : expr := #1.
+
+Definition RESULT_ABORTED_TXN : expr := #2.
+
+Definition RESULT_STALE_COORDINATOR : expr := #3.
+
+Definition RESULT_FAILED_VALIDATION : expr := #4.
+
+Definition RESULT_INVALID_RANK : expr := #5.
+
+(* Arguments:
+   @ts: Transaction timestamp.
+   @pwrs: Write set of transaction @ts.
+   @ptgs: Participant groups of transaction @ts.
+
+   Return values:
+   @error: Error code. *)
+Definition Replica__validate: val :=
+  rec: "Replica__validate" "rp" "ts" "pwrs" "ptgs" :=
+    let: ("cmted", "done") := MapGet (struct.loadF Replica "txntbl" "rp") "ts" in
+    (if: "done"
+    then
+      (if: "cmted"
+      then RESULT_COMMITTED_TXN
+      else RESULT_ABORTED_TXN)
+    else
+      let: (<>, "validated") := MapGet (struct.loadF Replica "prepm" "rp") "ts" in
+      (if: "validated"
+      then RESULT_OK
+      else
+        let: "acquired" := Replica__acquire "rp" "ts" "pwrs" in
+        (if: (~ "acquired")
+        then RESULT_FAILED_VALIDATION
+        else
+          MapInsert (struct.loadF Replica "prepm" "rp") "ts" "pwrs";;
+          MapInsert (struct.loadF Replica "ptgsm" "rp") "ts" "ptgs";;
+          RESULT_OK))).
+
+(* Keep alive coordinator for @ts at @rank. *)
+Definition Replica__refresh: val :=
+  rec: "Replica__refresh" "rp" "ts" "rank" :=
+    #().
+
+Definition Replica__Validate: val :=
+  rec: "Replica__Validate" "rp" "ts" "rank" "pwrs" "ptgs" :=
+    lock.acquire (struct.loadF Replica "mu" "rp");;
+    let: "res" := Replica__validate "rp" "ts" "pwrs" "ptgs" in
+    Replica__refresh "rp" "ts" "rank";;
+    lock.release (struct.loadF Replica "mu" "rp");;
+    "res".
+
+(* Arguments:
+   @ts: Transaction timestamp.
+
+   @pwrs: Transaction write set.
+
+   Return values:
+
+   @error: Error code. *)
+Definition Replica__fastPrepare: val :=
+  rec: "Replica__fastPrepare" "rp" "ts" "pwrs" "ptgs" :=
+    let: ("cmted", "done") := MapGet (struct.loadF Replica "txntbl" "rp") "ts" in
+    (if: "done"
+    then
+      (if: "cmted"
+      then RESULT_COMMITTED_TXN
+      else RESULT_ABORTED_TXN)
+    else
+      let: ("ps", "ok") := MapGet (struct.loadF Replica "pstbl" "rp") "ts" in
+      (if: "ok"
+      then
+        let: "pp" := struct.get PrepareStatusEntry "prep" "ps" in
+        (if: #0 < (struct.get PrepareProposal "rank" "pp")
+        then RESULT_STALE_COORDINATOR
+        else
+          (if: (~ (struct.get PrepareProposal "dec" "pp"))
+          then RESULT_FAILED_VALIDATION
+          else RESULT_OK))
+      else
+        let: "acquired" := Replica__acquire "rp" "ts" "pwrs" in
+        let: "pp" := struct.mk PrepareProposal [
+          "rank" ::= #0;
+          "dec" ::= "acquired"
+        ] in
+        let: "psnew" := struct.mk PrepareStatusEntry [
+          "rankl" ::= #1;
+          "prep" ::= "pp"
+        ] in
+        MapInsert (struct.loadF Replica "pstbl" "rp") "ts" "psnew";;
+        (if: (~ "acquired")
+        then RESULT_FAILED_VALIDATION
+        else
+          MapInsert (struct.loadF Replica "prepm" "rp") "ts" "pwrs";;
+          MapInsert (struct.loadF Replica "ptgsm" "rp") "ts" "ptgs";;
+          RESULT_OK))).
+
+Definition Replica__FastPrepare: val :=
+  rec: "Replica__FastPrepare" "rp" "ts" "pwrs" "ptgs" :=
+    lock.acquire (struct.loadF Replica "mu" "rp");;
+    let: "res" := Replica__fastPrepare "rp" "ts" "pwrs" "ptgs" in
+    Replica__refresh "rp" "ts" #0;;
+    lock.release (struct.loadF Replica "mu" "rp");;
+    "res".
+
+(* Accept the prepare decision for @ts at @rank, if @rank is most recent.
+
+   Arguments:
+   @ts: Transaction timestamp.
+   @rank: Coordinator rank.
+   @dec: Prepared or unprepared.
+
+   Return values:
+   @error: Error code. *)
+Definition Replica__acceptPreparedness: val :=
+  rec: "Replica__acceptPreparedness" "rp" "ts" "rank" "dec" :=
+    let: ("cmted", "done") := MapGet (struct.loadF Replica "txntbl" "rp") "ts" in
+    (if: "done"
+    then
+      (if: "cmted"
+      then RESULT_COMMITTED_TXN
+      else RESULT_ABORTED_TXN)
+    else
+      let: ("ps", "ok") := MapGet (struct.loadF Replica "pstbl" "rp") "ts" in
+      (if: "ok" && ("rank" < (struct.get PrepareStatusEntry "rankl" "ps"))
+      then RESULT_STALE_COORDINATOR
+      else
+        let: "pp" := struct.mk PrepareProposal [
+          "rank" ::= "rank";
+          "dec" ::= "dec"
+        ] in
+        let: "psnew" := struct.mk PrepareStatusEntry [
+          "rankl" ::= "rank" + #1;
+          "prep" ::= "pp"
+        ] in
+        MapInsert (struct.loadF Replica "pstbl" "rp") "ts" "psnew";;
+        RESULT_OK)).
+
+Definition Replica__Prepare: val :=
+  rec: "Replica__Prepare" "rp" "ts" "rank" :=
+    lock.acquire (struct.loadF Replica "mu" "rp");;
+    let: "res" := Replica__acceptPreparedness "rp" "ts" "rank" #true in
+    Replica__refresh "rp" "ts" "rank";;
+    lock.release (struct.loadF Replica "mu" "rp");;
+    "res".
+
+Definition Replica__Unprepare: val :=
+  rec: "Replica__Unprepare" "rp" "ts" "rank" :=
+    lock.acquire (struct.loadF Replica "mu" "rp");;
+    let: "res" := Replica__acceptPreparedness "rp" "ts" "rank" #false in
+    Replica__refresh "rp" "ts" "rank";;
+    lock.release (struct.loadF Replica "mu" "rp");;
+    "res".
+
+Definition Replica__inquire: val :=
+  rec: "Replica__inquire" "rp" "ts" "rank" :=
+    let: ("cmted", "done") := MapGet (struct.loadF Replica "txntbl" "rp") "ts" in
+    (if: "done"
+    then
+      (if: "cmted"
+      then
+        (struct.mk PrepareProposal [
+         ], #false, RESULT_COMMITTED_TXN)
+      else
+        (struct.mk PrepareProposal [
+         ], #false, RESULT_ABORTED_TXN))
+    else
+      let: ("ps", "ok") := MapGet (struct.loadF Replica "pstbl" "rp") "ts" in
+      (if: "ok" && ("rank" ≤ (struct.get PrepareStatusEntry "rankl" "ps"))
+      then
+        (struct.mk PrepareProposal [
+         ], #false, RESULT_INVALID_RANK)
+      else
+        let: "pp" := struct.get PrepareStatusEntry "prep" "ps" in
+        let: "psnew" := struct.mk PrepareStatusEntry [
+          "rankl" ::= "rank";
+          "prep" ::= "pp"
+        ] in
+        MapInsert (struct.loadF Replica "pstbl" "rp") "ts" "psnew";;
+        let: (<>, "vd") := MapGet (struct.loadF Replica "prepm" "rp") "ts" in
+        ("pp", "vd", RESULT_OK))).
+
+Definition Replica__Inquire: val :=
+  rec: "Replica__Inquire" "rp" "ts" "rank" :=
+    lock.acquire (struct.loadF Replica "mu" "rp");;
+    let: (("pp", "vd"), "res") := Replica__inquire "rp" "ts" "rank" in
+    Replica__refresh "rp" "ts" "rank";;
+    lock.release (struct.loadF Replica "mu" "rp");;
+    ("pp", "vd", "res").
+
+Definition Replica__query: val :=
+  rec: "Replica__query" "rp" "ts" "rank" :=
+    let: ("cmted", "done") := MapGet (struct.loadF Replica "txntbl" "rp") "ts" in
+    (if: "done"
+    then
+      (if: "cmted"
+      then RESULT_COMMITTED_TXN
+      else RESULT_ABORTED_TXN)
+    else
+      let: ("ps", "ok") := MapGet (struct.loadF Replica "pstbl" "rp") "ts" in
+      (if: "ok" && ("rank" < (struct.get PrepareStatusEntry "rankl" "ps"))
+      then RESULT_STALE_COORDINATOR
+      else RESULT_OK)).
+
+Definition Replica__Query: val :=
+  rec: "Replica__Query" "rp" "ts" "rank" :=
+    lock.acquire (struct.loadF Replica "mu" "rp");;
+    let: "res" := Replica__query "rp" "ts" "rank" in
+    Replica__refresh "rp" "ts" "rank";;
+    lock.release (struct.loadF Replica "mu" "rp");;
+    "res".
+
+Definition Replica__multiwrite: val :=
+  rec: "Replica__multiwrite" "rp" "ts" "pwrs" :=
+    ForSlice (struct.t WriteEntry) <> "ent" "pwrs"
+      (let: "key" := struct.get WriteEntry "k" "ent" in
+      let: "value" := struct.get WriteEntry "v" "ent" in
+      let: "tpl" := Index__GetTuple (struct.loadF Replica "idx" "rp") "key" in
+      (if: struct.get Value "b" "value"
+      then Tuple__AppendVersion "tpl" "ts" (struct.get Value "s" "value")
+      else Tuple__KillVersion "tpl" "ts");;
+      Tuple__Free "tpl");;
+    #().
+
+Definition Replica__applyCommit: val :=
+  rec: "Replica__applyCommit" "rp" "ts" "pwrs" :=
+    let: "committed" := Replica__queryTxnTermination "rp" "ts" in
+    (if: "committed"
+    then #()
+    else
+      Replica__multiwrite "rp" "ts" "pwrs";;
+      MapDelete (struct.loadF Replica "prepm" "rp") "ts";;
+      MapInsert (struct.loadF Replica "txntbl" "rp") "ts" #true;;
+      #()).
+
+Definition Replica__abort: val :=
+  rec: "Replica__abort" "rp" "pwrs" :=
+    ForSlice (struct.t WriteEntry) <> "ent" "pwrs"
+      (let: "key" := struct.get WriteEntry "k" "ent" in
+      let: "tpl" := Index__GetTuple (struct.loadF Replica "idx" "rp") "key" in
+      Tuple__Free "tpl");;
+    #().
+
+Definition Replica__applyAbort: val :=
+  rec: "Replica__applyAbort" "rp" "ts" :=
+    let: "aborted" := Replica__queryTxnTermination "rp" "ts" in
+    (if: "aborted"
+    then #()
+    else
+      let: ("pwrs", "prepared") := MapGet (struct.loadF Replica "prepm" "rp") "ts" in
+      (if: "prepared"
+      then
+        Replica__abort "rp" "pwrs";;
+        MapDelete (struct.loadF Replica "prepm" "rp") "ts"
+      else #());;
+      MapInsert (struct.loadF Replica "txntbl" "rp") "ts" #false;;
+      #()).
+
+Definition Replica__apply: val :=
+  rec: "Replica__apply" "rp" "cmd" :=
+    (if: (struct.get Cmd "kind" "cmd") = #0
+    then #()
+    else
+      (if: (struct.get Cmd "kind" "cmd") = #1
+      then
+        Replica__applyCommit "rp" (struct.get Cmd "ts" "cmd") (struct.get Cmd "pwrs" "cmd");;
+        #()
+      else
+        Replica__applyAbort "rp" (struct.get Cmd "ts" "cmd");;
+        #())).
+
+Definition Replica__Start: val :=
+  rec: "Replica__Start" "rp" :=
+    lock.acquire (struct.loadF Replica "mu" "rp");;
+    Skip;;
+    (for: (λ: <>, #true); (λ: <>, Skip) := λ: <>,
+      let: "lsn" := std.SumAssumeNoOverflow (struct.loadF Replica "lsna" "rp") #1 in
+      let: ("cmd", "ok") := TxnLog__Lookup (struct.loadF Replica "txnlog" "rp") "lsn" in
+      (if: (~ "ok")
+      then
+        lock.release (struct.loadF Replica "mu" "rp");;
+        time.Sleep (#1 * #1000000);;
+        lock.acquire (struct.loadF Replica "mu" "rp");;
+        Continue
+      else
+        Replica__apply "rp" "cmd";;
+        struct.storeF Replica "lsna" "rp" "lsn";;
+        Continue));;
+    #().
+
+Definition GCOORD_VALIDATING : expr := #0.
+
+Definition GCOORD_PREPARING : expr := #1.
+
+Definition GCOORD_UNPREPARING : expr := #2.
+
+Definition GCOORD_WAITING : expr := #3.
+
+Definition GCOORD_PREPARED : expr := #4.
+
+Definition GCOORD_COMMITTED : expr := #5.
+
+Definition GCOORD_ABORTED : expr := #6.
+
+Definition GCOORD_FAST_PREPARE : expr := #0.
+
+Definition GCOORD_VALIDATE : expr := #1.
+
+Definition GCOORD_PREPARE : expr := #2.
+
+Definition GCOORD_UNPREPARE : expr := #3.
+
+Definition GCOORD_QUERY : expr := #4.
+
+Definition GCOORD_COMPLETE : expr := #5.
+
+Definition GroupCoordinator := struct.decl [
+  "rps" :: mapT ptrT;
+  "pwrs" :: mapT (struct.t Value);
+  "mu" :: ptrT;
+  "leader" :: uint64T;
+  "phase" :: uint64T;
+  "fresps" :: mapT boolT;
+  "sresps" :: mapT boolT
+].
+
+(* Argument:
+   @rid: ID of the replica to which a new action is performed.
+
+   Return value:
+   @action: Next action to perform. *)
+Definition GroupCoordinator__action: val :=
+  rec: "GroupCoordinator__action" "gcoord" "rid" :=
+    (if: (struct.loadF GroupCoordinator "phase" "gcoord") = GCOORD_VALIDATING
+    then
+      let: (<>, "fresp") := MapGet (struct.loadF GroupCoordinator "fresps" "gcoord") "rid" in
+      (if: (~ "fresp")
+      then GCOORD_FAST_PREPARE
+      else
+        let: (<>, "validated") := MapGet (struct.loadF GroupCoordinator "sresps" "gcoord") "rid" in
+        (if: (~ "validated")
+        then GCOORD_VALIDATE
+        else GCOORD_QUERY))
+    else
+      (if: (struct.loadF GroupCoordinator "phase" "gcoord") = GCOORD_PREPARING
+      then
+        let: (<>, "prepared") := MapGet (struct.loadF GroupCoordinator "sresps" "gcoord") "rid" in
+        (if: (~ "prepared")
+        then GCOORD_PREPARE
+        else GCOORD_QUERY)
+      else
+        (if: (struct.loadF GroupCoordinator "phase" "gcoord") = GCOORD_UNPREPARING
+        then
+          let: (<>, "unprepared") := MapGet (struct.loadF GroupCoordinator "sresps" "gcoord") "rid" in
+          (if: (~ "unprepared")
+          then GCOORD_UNPREPARE
+          else GCOORD_QUERY)
+        else
+          (if: (struct.loadF GroupCoordinator "phase" "gcoord") = GCOORD_WAITING
+          then GCOORD_QUERY
+          else GCOORD_COMPLETE)))).
+
+Definition GroupCoordinator__Action: val :=
+  rec: "GroupCoordinator__Action" "gcoord" "rid" :=
+    lock.acquire (struct.loadF GroupCoordinator "mu" "gcoord");;
+    let: "act" := GroupCoordinator__action "gcoord" "rid" in
+    lock.release (struct.loadF GroupCoordinator "mu" "gcoord");;
+    "act".
+
+Definition GroupCoordinator__tryResign: val :=
+  rec: "GroupCoordinator__tryResign" "gcoord" "res" :=
+    (if: GCOORD_PREPARED ≤ (struct.loadF GroupCoordinator "phase" "gcoord")
+    then #true
+    else
+      (if: "res" = RESULT_COMMITTED_TXN
+      then
+        struct.storeF GroupCoordinator "phase" "gcoord" GCOORD_COMMITTED;;
+        #true
+      else
+        (if: "res" = RESULT_ABORTED_TXN
+        then
+          struct.storeF GroupCoordinator "phase" "gcoord" GCOORD_ABORTED;;
+          #true
+        else
+          (if: "res" = RESULT_STALE_COORDINATOR
+          then
+            struct.storeF GroupCoordinator "phase" "gcoord" GCOORD_WAITING;;
+            #true
+          else #false)))).
+
+Definition FastQuorum: val :=
+  rec: "FastQuorum" "n" :=
+    (("n" + #1) * #3) `quot` #4.
+
+Definition ClassicQuorum: val :=
+  rec: "ClassicQuorum" "n" :=
+    ("n" `quot` #2) + #1.
+
+Definition Half: val :=
+  rec: "Half" "n" :=
+    ("n" + #1) `quot` #2.
+
+Definition GroupCoordinator__fquorum: val :=
+  rec: "GroupCoordinator__fquorum" "gcoord" "n" :=
+    (FastQuorum (MapLen (struct.loadF GroupCoordinator "rps" "gcoord"))) ≤ "n".
+
+Definition GroupCoordinator__cquorum: val :=
+  rec: "GroupCoordinator__cquorum" "gcoord" "n" :=
+    (ClassicQuorum (MapLen (struct.loadF GroupCoordinator "rps" "gcoord"))) ≤ "n".
+
+Definition countbm: val :=
+  rec: "countbm" "m" "b" :=
+    let: "n" := ref_to uint64T #0 in
+    MapIter "m" (λ: <> "v",
+      (if: "v" = "b"
+      then "n" <-[uint64T] ((![uint64T] "n") + #1)
+      else #()));;
+    ![uint64T] "n".
+
+Definition GroupCoordinator__tryBecomeAborted: val :=
+  rec: "GroupCoordinator__tryBecomeAborted" "gcoord" :=
+    let: "n" := countbm (struct.loadF GroupCoordinator "fresps" "gcoord") #false in
+    (if: GroupCoordinator__fquorum "gcoord" "n"
+    then
+      struct.storeF GroupCoordinator "phase" "gcoord" GCOORD_ABORTED;;
+      #()
+    else #()).
+
+Definition GroupCoordinator__tryBecomePrepared: val :=
+  rec: "GroupCoordinator__tryBecomePrepared" "gcoord" :=
+    let: "n" := countbm (struct.loadF GroupCoordinator "fresps" "gcoord") #true in
+    (if: GroupCoordinator__fquorum "gcoord" "n"
+    then
+      struct.storeF GroupCoordinator "phase" "gcoord" GCOORD_PREPARED;;
+      #true
+    else #false).
+
+Definition GroupCoordinator__tryBecomePreparing: val :=
+  rec: "GroupCoordinator__tryBecomePreparing" "gcoord" :=
+    let: "n" := MapLen (struct.loadF GroupCoordinator "sresps" "gcoord") in
+    (if: GroupCoordinator__cquorum "gcoord" "n"
+    then
+      struct.storeF GroupCoordinator "phase" "gcoord" GCOORD_PREPARING;;
+      struct.storeF GroupCoordinator "sresps" "gcoord" (NewMap uint64T boolT #());;
+      #()
+    else #()).
+
+Definition GroupCoordinator__processFastPrepareResult: val :=
+  rec: "GroupCoordinator__processFastPrepareResult" "gcoord" "rid" "res" :=
+    (if: GroupCoordinator__tryResign "gcoord" "res"
+    then #()
+    else
+      (if: "res" = RESULT_FAILED_VALIDATION
+      then
+        MapInsert (struct.loadF GroupCoordinator "fresps" "gcoord") "rid" #false;;
+        GroupCoordinator__tryBecomeAborted "gcoord";;
+        #()
+      else
+        MapInsert (struct.loadF GroupCoordinator "fresps" "gcoord") "rid" #true;;
+        (if: GroupCoordinator__tryBecomePrepared "gcoord"
+        then #()
+        else
+          (if: (struct.loadF GroupCoordinator "phase" "gcoord") ≠ GCOORD_VALIDATING
+          then #()
+          else
+            MapInsert (struct.loadF GroupCoordinator "sresps" "gcoord") "rid" #true;;
+            GroupCoordinator__tryBecomePreparing "gcoord";;
+            #())))).
+
+Definition GroupCoordinator__ProcessFastPrepareResult: val :=
+  rec: "GroupCoordinator__ProcessFastPrepareResult" "gcoord" "rid" "res" :=
+    lock.acquire (struct.loadF GroupCoordinator "mu" "gcoord");;
+    GroupCoordinator__processFastPrepareResult "gcoord" "rid" "res";;
+    lock.release (struct.loadF GroupCoordinator "mu" "gcoord");;
+    #().
+
+Definition GroupCoordinator__processValidateResult: val :=
+  rec: "GroupCoordinator__processValidateResult" "gcoord" "rid" "res" :=
+    (if: GroupCoordinator__tryResign "gcoord" "res"
+    then #()
+    else
+      (if: (struct.loadF GroupCoordinator "phase" "gcoord") ≠ GCOORD_VALIDATING
+      then #()
+      else
+        (if: "res" = RESULT_FAILED_VALIDATION
+        then #()
+        else
+          MapInsert (struct.loadF GroupCoordinator "sresps" "gcoord") "rid" #true;;
+          GroupCoordinator__tryBecomePreparing "gcoord";;
+          #()))).
+
+Definition GroupCoordinator__ProcessValidateResult: val :=
+  rec: "GroupCoordinator__ProcessValidateResult" "gcoord" "rid" "res" :=
+    lock.acquire (struct.loadF GroupCoordinator "mu" "gcoord");;
+    GroupCoordinator__processValidateResult "gcoord" "rid" "res";;
+    lock.release (struct.loadF GroupCoordinator "mu" "gcoord");;
+    #().
+
+Definition GroupCoordinator__ProcessPrepareResult: val :=
+  rec: "GroupCoordinator__ProcessPrepareResult" "gcoord" "rid" "res" :=
+    lock.acquire (struct.loadF GroupCoordinator "mu" "gcoord");;
+    (if: GroupCoordinator__tryResign "gcoord" "res"
+    then
+      lock.release (struct.loadF GroupCoordinator "mu" "gcoord");;
+      #()
+    else
+      MapInsert (struct.loadF GroupCoordinator "sresps" "gcoord") "rid" #true;;
+      let: "n" := MapLen (struct.loadF GroupCoordinator "sresps" "gcoord") in
+      (if: GroupCoordinator__cquorum "gcoord" "n"
+      then struct.storeF GroupCoordinator "phase" "gcoord" GCOORD_PREPARED
+      else #());;
+      lock.release (struct.loadF GroupCoordinator "mu" "gcoord");;
+      #()).
+
+Definition GroupCoordinator__ProcessUnprepareResult: val :=
+  rec: "GroupCoordinator__ProcessUnprepareResult" "gcoord" "rid" "res" :=
+    lock.acquire (struct.loadF GroupCoordinator "mu" "gcoord");;
+    (if: GroupCoordinator__tryResign "gcoord" "res"
+    then
+      lock.release (struct.loadF GroupCoordinator "mu" "gcoord");;
+      #()
+    else
+      MapInsert (struct.loadF GroupCoordinator "sresps" "gcoord") "rid" #true;;
+      let: "n" := MapLen (struct.loadF GroupCoordinator "sresps" "gcoord") in
+      (if: GroupCoordinator__cquorum "gcoord" "n"
+      then struct.storeF GroupCoordinator "phase" "gcoord" GCOORD_ABORTED
+      else #());;
+      lock.release (struct.loadF GroupCoordinator "mu" "gcoord");;
+      #()).
+
+Definition GroupCoordinator__ProcessQueryResult: val :=
+  rec: "GroupCoordinator__ProcessQueryResult" "gcoord" "rid" "res" :=
+    lock.acquire (struct.loadF GroupCoordinator "mu" "gcoord");;
+    GroupCoordinator__tryResign "gcoord" "res";;
+    lock.release (struct.loadF GroupCoordinator "mu" "gcoord");;
+    #().
+
+Definition GroupCoordinator__PrepareDone: val :=
+  rec: "GroupCoordinator__PrepareDone" "gcoord" :=
+    lock.acquire (struct.loadF GroupCoordinator "mu" "gcoord");;
+    let: "done" := GCOORD_PREPARED ≤ (struct.loadF GroupCoordinator "phase" "gcoord") in
+    lock.release (struct.loadF GroupCoordinator "mu" "gcoord");;
+    "done".
+
+Definition GroupCoordinator__GetPhase: val :=
+  rec: "GroupCoordinator__GetPhase" "gcoord" :=
+    lock.acquire (struct.loadF GroupCoordinator "mu" "gcoord");;
+    let: "phase" := struct.loadF GroupCoordinator "phase" "gcoord" in
+    lock.release (struct.loadF GroupCoordinator "mu" "gcoord");;
+    "phase".
+
+Definition GroupCoordinator__changeLeader: val :=
+  rec: "GroupCoordinator__changeLeader" "gcoord" :=
+    #().
+
+Definition slicem: val :=
+  rec: "slicem" "m" :=
+    slice.nil.
+
+Definition GroupCoordinator__BeginSession: val :=
+  rec: "GroupCoordinator__BeginSession" "gcoord" "rid" "ts" "ptgs" :=
+    let: "rp" := Fst (MapGet (struct.loadF GroupCoordinator "rps" "gcoord") "rid") in
+    let: "pwrs" := slicem (struct.loadF GroupCoordinator "pwrs" "gcoord") in
+    let: "act" := ref_to uint64T (GroupCoordinator__Action "gcoord" "rid") in
+    Skip;;
+    (for: (λ: <>, (![uint64T] "act") ≠ GCOORD_COMPLETE); (λ: <>, Skip) := λ: <>,
+      (if: (![uint64T] "act") = GCOORD_FAST_PREPARE
+      then
+        let: "res" := Replica__FastPrepare "rp" "ts" "pwrs" "ptgs" in
+        GroupCoordinator__ProcessFastPrepareResult "gcoord" "rid" "res"
+      else
+        (if: (![uint64T] "act") = GCOORD_VALIDATE
+        then
+          let: "res" := Replica__Validate "rp" "ts" #1 "pwrs" "ptgs" in
+          GroupCoordinator__ProcessValidateResult "gcoord" "rid" "res"
+        else
+          (if: (![uint64T] "act") = GCOORD_PREPARE
+          then
+            let: "res" := Replica__Prepare "rp" "ts" #1 in
+            GroupCoordinator__ProcessPrepareResult "gcoord" "rid" "res"
+          else
+            (if: (![uint64T] "act") = GCOORD_UNPREPARE
+            then
+              let: "res" := Replica__Unprepare "rp" "ts" #1 in
+              GroupCoordinator__ProcessUnprepareResult "gcoord" "rid" "res"
+            else
+              (if: (![uint64T] "act") = GCOORD_QUERY
+              then
+                let: "res" := Replica__Query "rp" "ts" #1 in
+                GroupCoordinator__ProcessQueryResult "gcoord" "rid" "res"
+              else #())))));;
+      "act" <-[uint64T] (GroupCoordinator__Action "gcoord" "rid");;
+      Continue);;
+    #().
+
+Definition TXN_PREPARED : expr := #0.
+
+Definition TXN_COMMITTED : expr := #1.
+
+Definition TXN_ABORTED : expr := #2.
+
+(* Arguments:
+   @ts: Transaction timestamp.
+
+   Return values:
+   @status: Transaction status. *)
+Definition GroupCoordinator__Prepare: val :=
+  rec: "GroupCoordinator__Prepare" "gcoord" "ts" "ptgs" :=
+    MapIter (struct.loadF GroupCoordinator "rps" "gcoord") (λ: "ridloop" <>,
+      let: "rid" := "ridloop" in
+      Fork (GroupCoordinator__BeginSession "gcoord" "rid" "ts" "ptgs"));;
+    Skip;;
+    (for: (λ: <>, (~ (GroupCoordinator__PrepareDone "gcoord"))); (λ: <>, Skip) := λ: <>,
+      Continue);;
+    let: "phase" := GroupCoordinator__GetPhase "gcoord" in
+    (if: "phase" = GCOORD_COMMITTED
+    then TXN_COMMITTED
+    else
+      (if: "phase" = GCOORD_ABORTED
+      then TXN_ABORTED
+      else TXN_PREPARED)).
+
+Definition GroupCoordinator__Commit: val :=
+  rec: "GroupCoordinator__Commit" "gcoord" "ts" :=
+    let: "pwrs" := slicem (struct.loadF GroupCoordinator "pwrs" "gcoord") in
+    Skip;;
+    (for: (λ: <>, #true); (λ: <>, Skip) := λ: <>,
+      let: "rp" := Fst (MapGet (struct.loadF GroupCoordinator "rps" "gcoord") (struct.loadF GroupCoordinator "leader" "gcoord")) in
+      let: "ok" := Replica__Commit "rp" "ts" "pwrs" in
+      (if: "ok"
+      then Break
+      else
+        GroupCoordinator__changeLeader "gcoord";;
+        Continue));;
+    #().
+
+Definition GroupCoordinator__Abort: val :=
+  rec: "GroupCoordinator__Abort" "gcoord" "ts" :=
+    Skip;;
+    (for: (λ: <>, #true); (λ: <>, Skip) := λ: <>,
+      let: "rp" := Fst (MapGet (struct.loadF GroupCoordinator "rps" "gcoord") (struct.loadF GroupCoordinator "leader" "gcoord")) in
+      let: "ok" := Replica__Abort "rp" "ts" in
+      (if: "ok"
+      then Break
+      else
+        GroupCoordinator__changeLeader "gcoord";;
+        Continue));;
+    #().
+
+Definition GroupReader := struct.decl [
+  "rps" :: mapT ptrT;
+  "mu" :: ptrT;
+  "rds" :: mapT (struct.t Value);
+  "versm" :: mapT (mapT (struct.t Version))
+].
+
+Definition Txn := struct.decl [
+  "ts" :: uint64T;
+  "wrs" :: mapT (mapT (struct.t Value));
+  "grds" :: mapT ptrT;
+  "leaders" :: mapT uint64T
+].
+
+Definition TxnCoordinator := struct.decl [
+  "ts" :: uint64T;
+  "gcoords" :: mapT ptrT
+].
+
+Definition GetTS: val :=
+  rec: "GetTS" <> :=
+    #0.
+
+Definition Txn__begin: val :=
+  rec: "Txn__begin" "txn" :=
+    struct.storeF Txn "ts" "txn" (GetTS #());;
+    #().
+
+(* Main proof for this simplified program. *)
+Definition TxnCoordinator__prepare: val :=
+  rec: "TxnCoordinator__prepare" "tcoord" :=
+    let: "ptgs" := ref_to (slice.T uint64T) (NewSliceWithCap uint64T #0 (MapLen (struct.loadF TxnCoordinator "gcoords" "tcoord"))) in
+    MapIter (struct.loadF TxnCoordinator "gcoords" "tcoord") (λ: "gid" <>,
+      "ptgs" <-[slice.T uint64T] (SliceAppend uint64T (![slice.T uint64T] "ptgs") "gid"));;
+    let: "status" := ref_to uint64T TXN_PREPARED in
+    let: "gid" := ref_to uint64T #0 in
+    Skip;;
+    (for: (λ: <>, (![uint64T] "gid") < (MapLen (struct.loadF TxnCoordinator "gcoords" "tcoord"))); (λ: <>, Skip) := λ: <>,
+      let: "gcoord" := Fst (MapGet (struct.loadF TxnCoordinator "gcoords" "tcoord") (![uint64T] "gid")) in
+      "status" <-[uint64T] (GroupCoordinator__Prepare "gcoord" (struct.loadF TxnCoordinator "ts" "tcoord") (![slice.T uint64T] "ptgs"));;
+      (if: (![uint64T] "status") ≠ TXN_PREPARED
+      then Break
+      else
+        "gid" <-[uint64T] ((![uint64T] "gid") + #1);;
+        Continue));;
+    ![uint64T] "status".
+
+Definition TxnCoordinator__commit: val :=
+  rec: "TxnCoordinator__commit" "tcoord" :=
+    MapIter (struct.loadF TxnCoordinator "gcoords" "tcoord") (λ: <> "gcoord",
+      GroupCoordinator__Commit "gcoord" (struct.loadF TxnCoordinator "ts" "tcoord"));;
+    #().
+
+Definition TxnCoordinator__abort: val :=
+  rec: "TxnCoordinator__abort" "tcoord" :=
+    MapIter (struct.loadF TxnCoordinator "gcoords" "tcoord") (λ: <> "gcoord",
+      GroupCoordinator__Abort "gcoord" (struct.loadF TxnCoordinator "ts" "tcoord"));;
+    #().
+
+Definition KeyToGroup: val :=
+  rec: "KeyToGroup" "key" :=
+    #0.
+
+Definition GroupReader__cquorum: val :=
+  rec: "GroupReader__cquorum" "grd" "n" :=
+    (ClassicQuorum (MapLen (struct.loadF GroupReader "rps" "grd"))) ≤ "n".
+
+Definition GroupReader__latestVersion: val :=
+  rec: "GroupReader__latestVersion" "grd" "key" :=
+    let: "latest" := ref (zero_val (struct.t Version)) in
+    let: "vers" := Fst (MapGet (struct.loadF GroupReader "versm" "grd") "key") in
+    MapIter "vers" (λ: <> "ver",
+      (if: (struct.get Version "ts" (![struct.t Version] "latest")) < (struct.get Version "ts" "ver")
+      then "latest" <-[struct.t Version] "ver"
+      else #()));;
+    ![struct.t Version] "latest".
+
+Definition GroupReader__replicaDone: val :=
+  rec: "GroupReader__replicaDone" "grd" "rid" "key" :=
+    let: (<>, "final") := MapGet (struct.loadF GroupReader "rds" "grd") "key" in
+    (if: "final"
+    then #true
+    else
+      let: "vers" := Fst (MapGet (struct.loadF GroupReader "versm" "grd") "key") in
+      let: (<>, "responded") := MapGet "vers" "rid" in
+      (if: "responded"
+      then #true
+      else #false)).
+
+Definition GroupReader__ReplicaDone: val :=
+  rec: "GroupReader__ReplicaDone" "grd" "rid" "key" :=
+    lock.acquire (struct.loadF GroupReader "mu" "grd");;
+    let: "ready" := GroupReader__replicaDone "grd" "rid" "key" in
+    lock.release (struct.loadF GroupReader "mu" "grd");;
+    "ready".
+
+Definition GroupReader__processReadResult: val :=
+  rec: "GroupReader__processReadResult" "grd" "rid" "key" "ver" :=
+    let: (<>, "final") := MapGet (struct.loadF GroupReader "rds" "grd") "key" in
+    (if: "final"
+    then #()
+    else
+      let: "vers" := Fst (MapGet (struct.loadF GroupReader "versm" "grd") "key") in
+      let: (<>, "responded") := MapGet "vers" "rid" in
+      (if: "responded"
+      then #()
+      else
+        MapInsert "vers" "rid" "ver";;
+        let: "n" := MapLen "vers" in
+        (if: (~ (GroupReader__cquorum "grd" "n"))
+        then #()
+        else
+          let: "latest" := GroupReader__latestVersion "grd" "key" in
+          MapInsert (struct.loadF GroupReader "rds" "grd") "key" (struct.get Version "val" "latest");;
+          MapDelete (struct.loadF GroupReader "versm" "grd") "key";;
+          #()))).
+
+Definition GroupReader__ProcessReadResult: val :=
+  rec: "GroupReader__ProcessReadResult" "grd" "rid" "key" "ver" :=
+    lock.acquire (struct.loadF GroupReader "mu" "grd");;
+    GroupReader__processReadResult "grd" "rid" "key" "ver";;
+    lock.release (struct.loadF GroupReader "mu" "grd");;
+    #().
+
+Definition GroupReader__BeginSession: val :=
+  rec: "GroupReader__BeginSession" "grd" "rid" "ts" "key" :=
+    let: "rp" := Fst (MapGet (struct.loadF GroupReader "rps" "grd") "rid") in
+    Skip;;
+    (for: (λ: <>, GroupReader__ReplicaDone "grd" "rid" "key"); (λ: <>, Skip) := λ: <>,
+      let: ("ver", "ok") := Replica__Read "rp" "ts" "key" in
+      (if: "ok"
+      then
+        GroupReader__ProcessReadResult "grd" "rid" "key" "ver";;
+        Continue
+      else Continue));;
+    #().
+
+Definition GroupReader__Done: val :=
+  rec: "GroupReader__Done" "grd" "key" :=
+    lock.acquire (struct.loadF GroupReader "mu" "grd");;
+    let: (<>, "final") := MapGet (struct.loadF GroupReader "rds" "grd") "key" in
+    lock.release (struct.loadF GroupReader "mu" "grd");;
+    "final".
+
+Definition GroupReader__Read: val :=
+  rec: "GroupReader__Read" "grd" "ts" "key" :=
+    MapIter (struct.loadF GroupReader "rps" "grd") (λ: "ridloop" <>,
+      let: "rid" := "ridloop" in
+      Fork (GroupReader__BeginSession "grd" "rid" "ts" "key"));;
+    Skip;;
+    (for: (λ: <>, (~ (GroupReader__Done "grd" "key"))); (λ: <>, Skip) := λ: <>,
+      Continue);;
+    lock.acquire (struct.loadF GroupReader "mu" "grd");;
+    let: "v" := Fst (MapGet (struct.loadF GroupReader "rds" "grd") "key") in
+    lock.release (struct.loadF GroupReader "mu" "grd");;
+    "v".
+
+Definition Txn__Read: val :=
+  rec: "Txn__Read" "txn" "key" :=
+    let: "gid" := KeyToGroup "key" in
+    let: "grd" := Fst (MapGet (struct.loadF Txn "grds" "txn") "gid") in
+    let: "v" := GroupReader__Read "grd" (struct.loadF Txn "ts" "txn") "key" in
+    "v".
+
+Definition Txn__Write: val :=
+  rec: "Txn__Write" "txn" "key" "value" :=
+    let: "gid" := KeyToGroup "key" in
+    let: "pwrs" := Fst (MapGet (struct.loadF Txn "wrs" "txn") "gid") in
+    let: "v" := struct.mk Value [
+      "b" ::= #true;
+      "s" ::= "value"
+    ] in
+    MapInsert "pwrs" "key" "v";;
+    #().
+
+Definition Txn__Delete: val :=
+  rec: "Txn__Delete" "txn" "key" :=
+    let: "gid" := KeyToGroup "key" in
+    let: "pwrs" := Fst (MapGet (struct.loadF Txn "wrs" "txn") "gid") in
+    let: "v" := struct.mk Value [
+      "b" ::= #false
+    ] in
+    MapInsert "pwrs" "key" "v";;
+    #().
+
+Definition Txn__mkTxnCoordinator: val :=
+  rec: "Txn__mkTxnCoordinator" "txn" :=
+    let: "gcoords" := NewMap uint64T ptrT #() in
+    MapIter (struct.loadF Txn "grds" "txn") (λ: "gid" "grd",
+      let: "gcoord" := struct.mk GroupCoordinator [
+        "rps" ::= struct.loadF GroupReader "rps" "grd";
+        "leader" ::= Fst (MapGet (struct.loadF Txn "leaders" "txn") "gid");
+        "pwrs" ::= Fst (MapGet (struct.loadF Txn "wrs" "txn") "gid");
+        "phase" ::= GCOORD_VALIDATING;
+        "fresps" ::= NewMap uint64T boolT #();
+        "sresps" ::= NewMap uint64T boolT #()
+      ] in
+      MapInsert "gcoords" "gid" "gcoord");;
+    let: "tcoord" := struct.new TxnCoordinator [
+      "ts" ::= struct.loadF Txn "ts" "txn";
+      "gcoords" ::= "gcoords"
+    ] in
+    "tcoord".
+
+(* Main proof for this simplifed program. *)
+Definition Txn__Run: val :=
+  rec: "Txn__Run" "txn" "body" :=
+    Txn__begin "txn";;
+    let: "cmt" := "body" "txn" in
+    (if: (~ "cmt")
+    then #false
+    else
+      let: "tcoord" := Txn__mkTxnCoordinator "txn" in
+      let: "status" := TxnCoordinator__prepare "tcoord" in
+      (if: "status" = TXN_COMMITTED
+      then #true
+      else
+        (if: "status" = TXN_ABORTED
+        then
+          TxnCoordinator__abort "tcoord";;
+          #false
+        else
+          TxnCoordinator__commit "tcoord";;
+          #true))).
+
+Definition NewTxn: val :=
+  rec: "NewTxn" <> :=
+    struct.new Txn [
+    ].
+
+Definition BackupGroupCoordinator := struct.decl [
+  "rps" :: mapT ptrT;
+  "pwrs" :: mapT (struct.t Value);
+  "mu" :: ptrT;
+  "leader" :: uint64T;
+  "phase" :: uint64T;
+  "pps" :: mapT (struct.t PrepareProposal);
+  "resps" :: mapT boolT
+].
+
+Definition BGCOORD_INQUIRING : expr := #0.
+
+Definition BGCOORD_VALIDATING : expr := #1.
+
+Definition BGCOORD_PREPARING : expr := #2.
+
+Definition BGCOORD_UNPREPARING : expr := #3.
+
+Definition BGCOORD_OVERTHROWN : expr := #4.
+
+Definition BGCOORD_PREPARED : expr := #5.
+
+Definition BGCOORD_COMMITTED : expr := #6.
+
+Definition BGCOORD_ABORTED : expr := #7.
+
+Definition BGCOORD_INQUIRE : expr := #0.
+
+Definition BGCOORD_VALIDATE : expr := #1.
+
+Definition BGCOORD_PREPARE : expr := #2.
+
+Definition BGCOORD_UNPREPARE : expr := #3.
+
+Definition BGCOORD_QUERY : expr := #4.
+
+Definition BGCOORD_COMPLETE : expr := #5.
+
+(* Argument:
+   @rid: ID of the replica to which a new action is performed.
+
+   Return value:
+   @action: Next action to perform. *)
+Definition BackupGroupCoordinator__action: val :=
+  rec: "BackupGroupCoordinator__action" "gcoord" "rid" :=
+    (if: (struct.loadF BackupGroupCoordinator "phase" "gcoord") = BGCOORD_INQUIRING
+    then
+      let: (<>, "inquired") := MapGet (struct.loadF BackupGroupCoordinator "pps" "gcoord") "rid" in
+      (if: (~ "inquired")
+      then BGCOORD_INQUIRE
+      else BGCOORD_QUERY)
+    else
+      (if: (struct.loadF BackupGroupCoordinator "phase" "gcoord") = BGCOORD_VALIDATING
+      then
+        let: (<>, "inquired") := MapGet (struct.loadF BackupGroupCoordinator "pps" "gcoord") "rid" in
+        (if: (~ "inquired")
+        then BGCOORD_INQUIRE
+        else
+          let: (<>, "validated") := MapGet (struct.loadF BackupGroupCoordinator "resps" "gcoord") "rid" in
+          (if: (~ "validated")
+          then BGCOORD_VALIDATE
+          else BGCOORD_QUERY))
+      else
+        (if: (struct.loadF BackupGroupCoordinator "phase" "gcoord") = BGCOORD_PREPARING
+        then
+          let: (<>, "prepared") := MapGet (struct.loadF BackupGroupCoordinator "resps" "gcoord") "rid" in
+          (if: (~ "prepared")
+          then BGCOORD_PREPARE
+          else BGCOORD_QUERY)
+        else
+          (if: (struct.loadF BackupGroupCoordinator "phase" "gcoord") = BGCOORD_UNPREPARING
+          then
+            let: (<>, "unprepared") := MapGet (struct.loadF BackupGroupCoordinator "resps" "gcoord") "rid" in
+            (if: (~ "unprepared")
+            then BGCOORD_UNPREPARE
+            else BGCOORD_QUERY)
+          else BGCOORD_COMPLETE)))).
+
+Definition BackupGroupCoordinator__Action: val :=
+  rec: "BackupGroupCoordinator__Action" "gcoord" "rid" :=
+    lock.acquire (struct.loadF BackupGroupCoordinator "mu" "gcoord");;
+    let: "act" := BackupGroupCoordinator__action "gcoord" "rid" in
+    lock.release (struct.loadF BackupGroupCoordinator "mu" "gcoord");;
+    "act".
+
+Definition BackupGroupCoordinator__fquorum: val :=
+  rec: "BackupGroupCoordinator__fquorum" "gcoord" "n" :=
+    (FastQuorum (MapLen (struct.loadF BackupGroupCoordinator "rps" "gcoord"))) ≤ "n".
+
+Definition BackupGroupCoordinator__cquorum: val :=
+  rec: "BackupGroupCoordinator__cquorum" "gcoord" "n" :=
+    (ClassicQuorum (MapLen (struct.loadF BackupGroupCoordinator "rps" "gcoord"))) ≤ "n".
+
+Definition BackupGroupCoordinator__hcquorum: val :=
+  rec: "BackupGroupCoordinator__hcquorum" "gcoord" "n" :=
+    (Half (ClassicQuorum (MapLen (struct.loadF BackupGroupCoordinator "rps" "gcoord")))) ≤ "n".
+
+Definition BackupGroupCoordinator__tryResign: val :=
+  rec: "BackupGroupCoordinator__tryResign" "gcoord" "res" :=
+    (if: BGCOORD_PREPARED ≤ (struct.loadF BackupGroupCoordinator "phase" "gcoord")
+    then #true
+    else
+      (if: "res" = RESULT_COMMITTED_TXN
+      then
+        struct.storeF BackupGroupCoordinator "phase" "gcoord" BGCOORD_COMMITTED;;
+        #true
+      else
+        (if: "res" = RESULT_ABORTED_TXN
+        then
+          struct.storeF BackupGroupCoordinator "phase" "gcoord" BGCOORD_ABORTED;;
+          #true
+        else
+          (if: "res" = RESULT_STALE_COORDINATOR
+          then
+            struct.storeF BackupGroupCoordinator "phase" "gcoord" BGCOORD_OVERTHROWN;;
+            #true
+          else #false)))).
+
+Definition BackupGroupCoordinator__ProcessPrepareResult: val :=
+  rec: "BackupGroupCoordinator__ProcessPrepareResult" "gcoord" "rid" "res" :=
+    lock.acquire (struct.loadF BackupGroupCoordinator "mu" "gcoord");;
+    (if: BackupGroupCoordinator__tryResign "gcoord" "res"
+    then
+      lock.release (struct.loadF BackupGroupCoordinator "mu" "gcoord");;
+      #()
+    else
+      MapInsert (struct.loadF BackupGroupCoordinator "resps" "gcoord") "rid" #true;;
+      let: "n" := MapLen (struct.loadF BackupGroupCoordinator "resps" "gcoord") in
+      (if: BackupGroupCoordinator__cquorum "gcoord" "n"
+      then struct.storeF BackupGroupCoordinator "phase" "gcoord" BGCOORD_PREPARED
+      else #());;
+      lock.release (struct.loadF BackupGroupCoordinator "mu" "gcoord");;
+      #()).
+
+Definition BackupGroupCoordinator__ProcessUnprepareResult: val :=
+  rec: "BackupGroupCoordinator__ProcessUnprepareResult" "gcoord" "rid" "res" :=
+    lock.acquire (struct.loadF BackupGroupCoordinator "mu" "gcoord");;
+    (if: BackupGroupCoordinator__tryResign "gcoord" "res"
+    then
+      lock.release (struct.loadF BackupGroupCoordinator "mu" "gcoord");;
+      #()
+    else
+      MapInsert (struct.loadF BackupGroupCoordinator "resps" "gcoord") "rid" #true;;
+      let: "n" := MapLen (struct.loadF BackupGroupCoordinator "resps" "gcoord") in
+      (if: BackupGroupCoordinator__cquorum "gcoord" "n"
+      then struct.storeF BackupGroupCoordinator "phase" "gcoord" BGCOORD_ABORTED
+      else #());;
+      lock.release (struct.loadF BackupGroupCoordinator "mu" "gcoord");;
+      #()).
+
+(* Return value:
+   @latest: The latest non-fast proposal if @latest.rank > 0; @gcoord.pps
+   contain only fast proposals if @latest.rank == 0. *)
+Definition BackupGroupCoordinator__latestProposal: val :=
+  rec: "BackupGroupCoordinator__latestProposal" "gcoord" :=
+    let: "latest" := ref (zero_val (struct.t PrepareProposal)) in
+    MapIter (struct.loadF BackupGroupCoordinator "pps" "gcoord") (λ: <> "pp",
+      (if: (struct.get PrepareProposal "rank" (![struct.t PrepareProposal] "latest")) < (struct.get PrepareProposal "rank" "pp")
+      then "latest" <-[struct.t PrepareProposal] "pp"
+      else #()));;
+    ![struct.t PrepareProposal] "latest".
+
+(* Return value:
+   @nprep: The number of fast unprepares collected in @gcoord.pps. *)
+Definition BackupGroupCoordinator__countFastUnprepare: val :=
+  rec: "BackupGroupCoordinator__countFastUnprepare" "gcoord" :=
+    let: "nprep" := ref (zero_val uint64T) in
+    MapIter (struct.loadF BackupGroupCoordinator "pps" "gcoord") (λ: <> "pp",
+      (if: ((struct.get PrepareProposal "rank" "pp") = #0) && (~ (struct.get PrepareProposal "dec" "pp"))
+      then "nprep" <-[uint64T] ((![uint64T] "nprep") + #1)
+      else #()));;
+    ![uint64T] "nprep".
+
+Definition BackupGroupCoordinator__processInquireResult: val :=
+  rec: "BackupGroupCoordinator__processInquireResult" "gcoord" "rid" "pp" "vd" "res" :=
+    (if: BackupGroupCoordinator__tryResign "gcoord" "res"
+    then #()
+    else
+      (if: ((struct.loadF BackupGroupCoordinator "phase" "gcoord") = BGCOORD_PREPARING) || ((struct.loadF BackupGroupCoordinator "phase" "gcoord") = BGCOORD_UNPREPARING)
+      then #()
+      else
+        MapInsert (struct.loadF BackupGroupCoordinator "pps" "gcoord") "rid" "pp";;
+        (if: "vd"
+        then MapInsert (struct.loadF BackupGroupCoordinator "resps" "gcoord") "rid" #true
+        else #());;
+        let: "n" := MapLen (struct.loadF BackupGroupCoordinator "pps" "gcoord") in
+        (if: (~ (BackupGroupCoordinator__cquorum "gcoord" "n"))
+        then #()
+        else
+          let: "latest" := BackupGroupCoordinator__latestProposal "gcoord" in
+          (if: (struct.get PrepareProposal "rank" "latest") ≠ #0
+          then
+            (if: struct.get PrepareProposal "dec" "latest"
+            then struct.storeF BackupGroupCoordinator "phase" "gcoord" BGCOORD_PREPARING
+            else struct.storeF BackupGroupCoordinator "phase" "gcoord" BGCOORD_UNPREPARING);;
+            #()
+          else
+            let: "nfu" := BackupGroupCoordinator__countFastUnprepare "gcoord" in
+            (if: BackupGroupCoordinator__hcquorum "gcoord" "nfu"
+            then
+              struct.storeF BackupGroupCoordinator "phase" "gcoord" BGCOORD_UNPREPARING;;
+              #()
+            else
+              let: "nvd" := MapLen (struct.loadF BackupGroupCoordinator "resps" "gcoord") in
+              (if: BackupGroupCoordinator__cquorum "gcoord" "nvd"
+              then
+                struct.storeF BackupGroupCoordinator "phase" "gcoord" BGCOORD_PREPARING;;
+                #()
+              else
+                struct.storeF BackupGroupCoordinator "phase" "gcoord" BGCOORD_VALIDATING;;
+                #())))))).
+
+Definition BackupGroupCoordinator__ProcessInquireResult: val :=
+  rec: "BackupGroupCoordinator__ProcessInquireResult" "gcoord" "rid" "pp" "vd" "res" :=
+    lock.acquire (struct.loadF BackupGroupCoordinator "mu" "gcoord");;
+    BackupGroupCoordinator__processInquireResult "gcoord" "rid" "pp" "vd" "res";;
+    lock.release (struct.loadF BackupGroupCoordinator "mu" "gcoord");;
+    #().
+
+Definition BackupGroupCoordinator__processValidateResult: val :=
+  rec: "BackupGroupCoordinator__processValidateResult" "gcoord" "rid" "res" :=
+    (if: BackupGroupCoordinator__tryResign "gcoord" "res"
+    then #()
+    else
+      (if: (struct.loadF BackupGroupCoordinator "phase" "gcoord") ≠ BGCOORD_VALIDATING
+      then #()
+      else
+        (if: "res" = RESULT_FAILED_VALIDATION
+        then #()
+        else
+          MapInsert (struct.loadF BackupGroupCoordinator "resps" "gcoord") "rid" #true;;
+          let: "nvd" := MapLen (struct.loadF BackupGroupCoordinator "resps" "gcoord") in
+          (if: BackupGroupCoordinator__cquorum "gcoord" "nvd"
+          then
+            struct.storeF BackupGroupCoordinator "phase" "gcoord" BGCOORD_PREPARING;;
+            #()
+          else #())))).
+
+Definition BackupGroupCoordinator__ProcessValidateResult: val :=
+  rec: "BackupGroupCoordinator__ProcessValidateResult" "gcoord" "rid" "res" :=
+    lock.acquire (struct.loadF BackupGroupCoordinator "mu" "gcoord");;
+    BackupGroupCoordinator__processValidateResult "gcoord" "rid" "res";;
+    lock.release (struct.loadF BackupGroupCoordinator "mu" "gcoord");;
+    #().
+
+Definition BackupGroupCoordinator__ProcessQueryResult: val :=
+  rec: "BackupGroupCoordinator__ProcessQueryResult" "gcoord" "rid" "res" :=
+    lock.acquire (struct.loadF BackupGroupCoordinator "mu" "gcoord");;
+    BackupGroupCoordinator__tryResign "gcoord" "res";;
+    lock.release (struct.loadF BackupGroupCoordinator "mu" "gcoord");;
+    #().
+
+Definition BackupGroupCoordinator__BeginSession: val :=
+  rec: "BackupGroupCoordinator__BeginSession" "gcoord" "rid" "ts" "rank" "ptgs" :=
+    let: "rp" := Fst (MapGet (struct.loadF BackupGroupCoordinator "rps" "gcoord") "rid") in
+    let: "pwrs" := slicem (struct.loadF BackupGroupCoordinator "pwrs" "gcoord") in
+    let: "act" := ref_to uint64T (BackupGroupCoordinator__Action "gcoord" "rid") in
+    Skip;;
+    (for: (λ: <>, (![uint64T] "act") ≠ BGCOORD_COMPLETE); (λ: <>, Skip) := λ: <>,
+      (if: (![uint64T] "act") = BGCOORD_INQUIRE
+      then
+        let: (("pp", "vd"), "res") := Replica__Inquire "rp" "ts" "rank" in
+        BackupGroupCoordinator__ProcessInquireResult "gcoord" "rid" "pp" "vd" "res"
+      else
+        (if: (![uint64T] "act") = BGCOORD_VALIDATE
+        then
+          let: "res" := Replica__Validate "rp" "ts" "rank" "pwrs" "ptgs" in
+          BackupGroupCoordinator__ProcessValidateResult "gcoord" "rid" "res"
+        else
+          (if: (![uint64T] "act") = BGCOORD_PREPARE
+          then
+            let: "res" := Replica__Prepare "rp" "ts" "rank" in
+            BackupGroupCoordinator__ProcessPrepareResult "gcoord" "rid" "res"
+          else
+            (if: (![uint64T] "act") = BGCOORD_UNPREPARE
+            then
+              let: "res" := Replica__Unprepare "rp" "ts" "rank" in
+              BackupGroupCoordinator__ProcessUnprepareResult "gcoord" "rid" "res"
+            else
+              (if: (![uint64T] "act") = BGCOORD_QUERY
+              then
+                let: "res" := Replica__Query "rp" "ts" "rank" in
+                BackupGroupCoordinator__ProcessQueryResult "gcoord" "rid" "res"
+              else #())))));;
+      "act" <-[uint64T] (BackupGroupCoordinator__Action "gcoord" "rid");;
+      Continue);;
+    #().
+
+Definition BackupGroupCoordinator__InquireDone: val :=
+  rec: "BackupGroupCoordinator__InquireDone" "gcoord" :=
+    lock.acquire (struct.loadF BackupGroupCoordinator "mu" "gcoord");;
+    let: "done" := BGCOORD_PREPARED ≤ (struct.loadF BackupGroupCoordinator "phase" "gcoord") in
+    lock.release (struct.loadF BackupGroupCoordinator "mu" "gcoord");;
+    "done".
+
+Definition BackupGroupCoordinator__GetPhase: val :=
+  rec: "BackupGroupCoordinator__GetPhase" "gcoord" :=
+    lock.acquire (struct.loadF BackupGroupCoordinator "mu" "gcoord");;
+    let: "phase" := struct.loadF BackupGroupCoordinator "phase" "gcoord" in
+    lock.release (struct.loadF BackupGroupCoordinator "mu" "gcoord");;
+    "phase".
+
+Definition BackupGroupCoordinator__changeLeader: val :=
+  rec: "BackupGroupCoordinator__changeLeader" "gcoord" :=
+    #().
+
+(* Arguments:
+   @ts: Transaction timestamp.
+
+   Return values:
+   @status: Transaction status.
+   @valid: The @Inquire process goes through without encountering a more recent
+   coordinator. @status is meaningful iff @valid is true. *)
+Definition BackupGroupCoordinator__Inquire: val :=
+  rec: "BackupGroupCoordinator__Inquire" "gcoord" "ts" "rank" "ptgs" :=
+    MapIter (struct.loadF BackupGroupCoordinator "rps" "gcoord") (λ: "ridloop" <>,
+      let: "rid" := "ridloop" in
+      Fork (BackupGroupCoordinator__BeginSession "gcoord" "rid" "ts" "rank" "ptgs"));;
+    Skip;;
+    (for: (λ: <>, (~ (BackupGroupCoordinator__InquireDone "gcoord"))); (λ: <>, Skip) := λ: <>,
+      Continue);;
+    let: "phase" := BackupGroupCoordinator__GetPhase "gcoord" in
+    (if: "phase" = BGCOORD_OVERTHROWN
+    then (TXN_PREPARED, #false)
+    else
+      (if: "phase" = GCOORD_COMMITTED
+      then (TXN_COMMITTED, #true)
+      else
+        (if: "phase" = GCOORD_ABORTED
+        then (TXN_ABORTED, #true)
+        else (TXN_PREPARED, #true)))).
+
+Definition BackupGroupCoordinator__Commit: val :=
+  rec: "BackupGroupCoordinator__Commit" "gcoord" "ts" :=
+    let: "pwrs" := slicem (struct.loadF BackupGroupCoordinator "pwrs" "gcoord") in
+    Skip;;
+    (for: (λ: <>, #true); (λ: <>, Skip) := λ: <>,
+      let: "rp" := Fst (MapGet (struct.loadF BackupGroupCoordinator "rps" "gcoord") (struct.loadF BackupGroupCoordinator "leader" "gcoord")) in
+      let: "ok" := Replica__Commit "rp" "ts" "pwrs" in
+      (if: "ok"
+      then Break
+      else
+        BackupGroupCoordinator__changeLeader "gcoord";;
+        Continue));;
+    #().
+
+Definition BackupGroupCoordinator__Abort: val :=
+  rec: "BackupGroupCoordinator__Abort" "gcoord" "ts" :=
+    Skip;;
+    (for: (λ: <>, #true); (λ: <>, Skip) := λ: <>,
+      let: "rp" := Fst (MapGet (struct.loadF BackupGroupCoordinator "rps" "gcoord") (struct.loadF BackupGroupCoordinator "leader" "gcoord")) in
+      let: "ok" := Replica__Abort "rp" "ts" in
+      (if: "ok"
+      then Break
+      else
+        BackupGroupCoordinator__changeLeader "gcoord";;
+        Continue));;
+    #().
+
+Definition BackupTxnCoordinator := struct.decl [
+  "ts" :: uint64T;
+  "rank" :: uint64T;
+  "ptgs" :: slice.T uint64T;
+  "gcoords" :: mapT ptrT
+].
+
+Definition Replica__mkBackupTxnCoordinator: val :=
+  rec: "Replica__mkBackupTxnCoordinator" "rp" "ts" :=
+    let: "gcoords" := NewMap uint64T ptrT #() in
+    let: "ptgs" := Fst (MapGet (struct.loadF Replica "ptgsm" "rp") "ts") in
+    ForSlice uint64T <> "gid" "ptgs"
+      (let: "gcoord" := struct.mk BackupGroupCoordinator [
+        "leader" ::= struct.loadF Replica "leader" "rp";
+        "rps" ::= struct.loadF Replica "rps" "rp";
+        "phase" ::= BGCOORD_INQUIRING;
+        "pps" ::= NewMap uint64T (struct.t PrepareProposal) #();
+        "resps" ::= NewMap uint64T boolT #()
+      ] in
+      MapInsert "gcoords" "gid" "gcoord");;
+    let: "ps" := Fst (MapGet (struct.loadF Replica "pstbl" "rp") "ts") in
+    let: "rank" := (struct.get PrepareStatusEntry "rankl" "ps") + #1 in
+    let: "tcoord" := struct.new BackupTxnCoordinator [
+      "ts" ::= "ts";
+      "rank" ::= "rank";
+      "ptgs" ::= "ptgs";
+      "gcoords" ::= "gcoords"
+    ] in
+    "tcoord".
+
+Definition BackupTxnCoordinator__inquire: val :=
+  rec: "BackupTxnCoordinator__inquire" "tcoord" :=
+    let: "status" := ref_to uint64T TXN_PREPARED in
+    let: "valid" := ref_to boolT #true in
+    let: "gid" := ref_to uint64T #0 in
+    Skip;;
+    (for: (λ: <>, (![uint64T] "gid") < (MapLen (struct.loadF BackupTxnCoordinator "gcoords" "tcoord"))); (λ: <>, Skip) := λ: <>,
+      let: "gcoord" := Fst (MapGet (struct.loadF BackupTxnCoordinator "gcoords" "tcoord") (![uint64T] "gid")) in
+      let: ("0_ret", "1_ret") := BackupGroupCoordinator__Inquire "gcoord" (struct.loadF BackupTxnCoordinator "ts" "tcoord") (struct.loadF BackupTxnCoordinator "rank" "tcoord") (struct.loadF BackupTxnCoordinator "ptgs" "tcoord") in
+      "status" <-[uint64T] "0_ret";;
+      "valid" <-[boolT] "1_ret";;
+      (if: (~ (![boolT] "valid"))
+      then Break
+      else
+        (if: (![uint64T] "status") ≠ TXN_PREPARED
+        then Break
+        else
+          "gid" <-[uint64T] ((![uint64T] "gid") + #1);;
+          Continue)));;
+    (![uint64T] "status", ![boolT] "valid").
+
+Definition BackupTxnCoordinator__commit: val :=
+  rec: "BackupTxnCoordinator__commit" "tcoord" :=
+    MapIter (struct.loadF BackupTxnCoordinator "gcoords" "tcoord") (λ: <> "gcoord",
+      BackupGroupCoordinator__Commit "gcoord" (struct.loadF BackupTxnCoordinator "ts" "tcoord"));;
+    #().
+
+Definition BackupTxnCoordinator__abort: val :=
+  rec: "BackupTxnCoordinator__abort" "tcoord" :=
+    MapIter (struct.loadF BackupTxnCoordinator "gcoords" "tcoord") (λ: <> "gcoord",
+      BackupGroupCoordinator__Abort "gcoord" (struct.loadF BackupTxnCoordinator "ts" "tcoord"));;
+    #().
+
+(* Top-level method of backup transaction coordinator. *)
+Definition BackupTxnCoordinator__Finalize: val :=
+  rec: "BackupTxnCoordinator__Finalize" "tcoord" :=
+    let: ("status", "valid") := BackupTxnCoordinator__inquire "tcoord" in
+    (if: (~ "valid")
+    then #()
+    else
+      (if: "status" = TXN_COMMITTED
+      then #()
+      else
+        (if: "status" = TXN_ABORTED
+        then
+          BackupTxnCoordinator__abort "tcoord";;
+          #()
+        else
+          BackupTxnCoordinator__commit "tcoord";;
+          #()))).
+
+(* Example *)
+Definition swap: val :=
+  rec: "swap" "txn" :=
+    let: "x" := Txn__Read "txn" #(str"0") in
+    let: "y" := Txn__Read "txn" #(str"1") in
+    Txn__Write "txn" #(str"0") (struct.get Value "s" "y");;
+    Txn__Write "txn" #(str"1") (struct.get Value "s" "x");;
+    #true.
+
+Definition AtomicSwap: val :=
+  rec: "AtomicSwap" <> :=
+    let: "txn" := NewTxn #() in
+    let: "committed" := Txn__Run "txn" swap in
+    "committed".
+
+End code.
diff --git a/external/Goose/github_com/mit_pdos/rsm/spaxos.v b/external/Goose/github_com/mit_pdos/rsm/spaxos.v
index f59cf506c..c8c98256b 100644
--- a/external/Goose/github_com/mit_pdos/rsm/spaxos.v
+++ b/external/Goose/github_com/mit_pdos/rsm/spaxos.v
@@ -4,7 +4,6 @@ From Goose Require github_com.goose_lang.std.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition Paxos := struct.decl [
   "mu" :: ptrT;
diff --git a/external/Goose/github_com/mit_pdos/rsm/tpl.v b/external/Goose/github_com/mit_pdos/rsm/tpl.v
index d57ff4119..508448f16 100644
--- a/external/Goose/github_com/mit_pdos/rsm/tpl.v
+++ b/external/Goose/github_com/mit_pdos/rsm/tpl.v
@@ -3,7 +3,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition Keys: ty := slice.T stringT.
 
diff --git a/external/Goose/github_com/mit_pdos/vmvcc/common.v b/external/Goose/github_com/mit_pdos/vmvcc/common.v
index 38581b74b..f2a48ab51 100644
--- a/external/Goose/github_com/mit_pdos/vmvcc/common.v
+++ b/external/Goose/github_com/mit_pdos/vmvcc/common.v
@@ -3,7 +3,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition RET_SUCCESS : expr := #0.
 
diff --git a/external/Goose/github_com/mit_pdos/vmvcc/config.v b/external/Goose/github_com/mit_pdos/vmvcc/config.v
index 69d92c835..014a6847e 100644
--- a/external/Goose/github_com/mit_pdos/vmvcc/config.v
+++ b/external/Goose/github_com/mit_pdos/vmvcc/config.v
@@ -3,7 +3,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition N_TXN_SITES : expr := #32.
 
diff --git a/external/Goose/github_com/mit_pdos/vmvcc/examples/strnum.v b/external/Goose/github_com/mit_pdos/vmvcc/examples/strnum.v
index 43c02367f..e2c0147fd 100644
--- a/external/Goose/github_com/mit_pdos/vmvcc/examples/strnum.v
+++ b/external/Goose/github_com/mit_pdos/vmvcc/examples/strnum.v
@@ -3,7 +3,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 (* / This package converts between strings and numbers. Currently Goose has
    / limited support for manipulating string, so this package is trusted. *)
diff --git a/external/Goose/github_com/mit_pdos/vmvcc/index.v b/external/Goose/github_com/mit_pdos/vmvcc/index.v
index bffafafd2..f3f3e8da8 100644
--- a/external/Goose/github_com/mit_pdos/vmvcc/index.v
+++ b/external/Goose/github_com/mit_pdos/vmvcc/index.v
@@ -5,7 +5,6 @@ From Goose Require github_com.mit_pdos.vmvcc.tuple.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition IndexBucket := struct.decl [
   "latch" :: ptrT;
diff --git a/external/Goose/github_com/mit_pdos/vmvcc/tuple.v b/external/Goose/github_com/mit_pdos/vmvcc/tuple.v
index 7fafca31d..fc19169b5 100644
--- a/external/Goose/github_com/mit_pdos/vmvcc/tuple.v
+++ b/external/Goose/github_com/mit_pdos/vmvcc/tuple.v
@@ -4,7 +4,6 @@ From Goose Require github_com.mit_pdos.vmvcc.common.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 (* @ts
    Starting timestamp of this version, and also ending timestamp of the next
diff --git a/external/Goose/github_com/mit_pdos/vmvcc/wrbuf.v b/external/Goose/github_com/mit_pdos/vmvcc/wrbuf.v
index 5c58fc9f5..7ceaa652c 100644
--- a/external/Goose/github_com/mit_pdos/vmvcc/wrbuf.v
+++ b/external/Goose/github_com/mit_pdos/vmvcc/wrbuf.v
@@ -6,7 +6,6 @@ From Goose Require github_com.mit_pdos.vmvcc.tuple.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 (* @key and @val
    Key-value pair of the write entry.
diff --git a/external/Goose/github_com/tchajed/marshal.v b/external/Goose/github_com/tchajed/marshal.v
index 7940443eb..85b3022e3 100644
--- a/external/Goose/github_com/tchajed/marshal.v
+++ b/external/Goose/github_com/tchajed/marshal.v
@@ -4,7 +4,6 @@ From Goose Require github_com.goose_lang.std.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 (* marshal.go *)
 
diff --git a/new/golang/defn/noop.v b/new/golang/defn/noop.v
index 3e97254e9..3fbff9a14 100644
--- a/new/golang/defn/noop.v
+++ b/new/golang/defn/noop.v
@@ -2,7 +2,6 @@ From Perennial.goose_lang Require Import lang notation.
 
 Section goose_lang.
 Context {ext:ffi_syntax}.
-Local Coercion Var' (s:string) : expr := Var s.
 
 Definition variadic_noop : val :=
   rec: "variadic_noop" "x" :=
diff --git a/new/golang/defn/notation.v b/new/golang/defn/notation.v
index 1a0776899..b9f266928 100644
--- a/new/golang/defn/notation.v
+++ b/new/golang/defn/notation.v
@@ -1,4 +1,6 @@
 From Perennial.goose_lang Require Export lang notation.
 
+(*
 #[warnings="-uniform-inheritance"]
 Coercion Var : string >-> expr.
+*)
diff --git a/src/goose_lang/ffi/async_disk_prelude.v b/src/goose_lang/ffi/async_disk_prelude.v
index d9957d372..261c38a1c 100644
--- a/src/goose_lang/ffi/async_disk_prelude.v
+++ b/src/goose_lang/ffi/async_disk_prelude.v
@@ -6,8 +6,6 @@ Existing Instances async_disk_syntax.disk_op async_disk_proph.disk_model async_d
 Existing Instances async_disk_proph.disk_semantics async_disk_proph.disk_interp.
 #[global]
 Existing Instance goose_diskGS.
-(* Now that the TC parameter is fixed, we can make this a coercion. *)
-Coercion Var' (s: string) := Var s.
 
 
 Module disk.
diff --git a/src/goose_lang/ffi/disk_prelude.v b/src/goose_lang/ffi/disk_prelude.v
index 31f706efa..56e2da7f0 100644
--- a/src/goose_lang/ffi/disk_prelude.v
+++ b/src/goose_lang/ffi/disk_prelude.v
@@ -7,8 +7,4 @@ Existing Instances disk_op disk_model disk_ty.
 Existing Instances disk_semantics disk_interp.
 #[global]
 Existing Instance goose_diskGS.
-(* Now that the TC parameter is fixed, we can make this a coercion. Sadly,
-[Var'] gets replaced by [Var] on the first substitution, so printing terms still
-prints that [Var] -- but we barely look at those parts of the terms anyway. *)
-Coercion Var' (s: string) := Var s.
 Export disk.
diff --git a/src/goose_lang/ffi/grove_ffi/grove_ffi_typed.v b/src/goose_lang/ffi/grove_ffi/grove_ffi_typed.v
index c64b9167e..ce34d415e 100644
--- a/src/goose_lang/ffi/grove_ffi/grove_ffi_typed.v
+++ b/src/goose_lang/ffi/grove_ffi/grove_ffi_typed.v
@@ -22,7 +22,6 @@ Section grove.
   suddenly cause all FFI parameters to be inferred as the grove model *)
   (* FIXME: figure out which of these clients need to set *)
   Existing Instances grove_op grove_model grove_ty grove_semantics grove_interp goose_groveGS goose_groveNodeGS.
-  Local Coercion Var' (s:string) : expr := Var s.
 
   Context `{!heapGS Σ}.
 
diff --git a/src/goose_lang/ffi/grove_ffi/typed_impl.v b/src/goose_lang/ffi/grove_ffi/typed_impl.v
index afc7dd177..0feda1b7b 100644
--- a/src/goose_lang/ffi/grove_ffi/typed_impl.v
+++ b/src/goose_lang/ffi/grove_ffi/typed_impl.v
@@ -16,7 +16,6 @@ Module grove_ffi.
 Section grove.
   (* FIXME: figure out which of these clients need to set *)
   Existing Instances grove_op grove_model grove_ty grove_semantics.
-  Local Coercion Var' (s:string) : expr := Var s.
 
   (** [extT] have size 1 so this fits with them being pointers in Go. *)
   Definition Listener : ty := extT GroveListenTy.
diff --git a/src/goose_lang/ffi/grove_prelude.v b/src/goose_lang/ffi/grove_prelude.v
index 192668804..6919024bd 100644
--- a/src/goose_lang/ffi/grove_prelude.v
+++ b/src/goose_lang/ffi/grove_prelude.v
@@ -6,7 +6,3 @@ Existing Instances grove_op grove_model.
 Existing Instances grove_semantics grove_interp.
 #[global]
 Existing Instances goose_groveGS goose_groveNodeGS.
-(* Now that the TC parameter is fixed, we can make this a coercion. Sadly,
-[Var'] gets replaced by [Var] on the first substitution, so printing terms still
-prints that [Var] -- but we barely look at those parts of the terms anyway. *)
-Coercion Var' (s: string) := Var s.
diff --git a/src/goose_lang/interpreter/test_config.v b/src/goose_lang/interpreter/test_config.v
index 8311b76f0..0e3240436 100644
--- a/src/goose_lang/interpreter/test_config.v
+++ b/src/goose_lang/interpreter/test_config.v
@@ -74,7 +74,6 @@ Notation W32_val z := (Naive.mk z eq_refl).
 Notation W8_val z := (Naive.mk z eq_refl).
 
 Module Examples.
-  Coercion Var' := Var.
   Definition computeSix : val :=
     (rec: <> <> :=
        #3 + #3).
diff --git a/src/goose_lang/lang.v b/src/goose_lang/lang.v
index b80618d5e..2c3b9d1c3 100644
--- a/src/goose_lang/lang.v
+++ b/src/goose_lang/lang.v
@@ -1726,14 +1726,3 @@ Notation Load := (Primitive1 LoadOp).
 Notation Input := (Primitive1 InputOp).
 Notation Output := (Primitive1 OutputOp).
 Notation nonAtomic T := (naMode * T)%type.
-
-(* TODO: use this now that coercions are more powerful:
-https://github.com/coq/coq/pull/15789
-
-(the tricky part for us is that the translator has to stop emitting [Var'] or we
-get ambiguous coercions)
-*)
-(*
-#[warning="-uniform-inheritance"]
-Coercion Var : string >-> expr.
-*)
diff --git a/src/goose_lang/lib/barrier/barrier.v b/src/goose_lang/lib/barrier/barrier.v
index 1de50a078..f4a89a9e4 100644
--- a/src/goose_lang/lib/barrier/barrier.v
+++ b/src/goose_lang/lib/barrier/barrier.v
@@ -26,7 +26,6 @@ Context `{ffi_sem: ffi_semantics}.
 Context `{!ffi_interp ffi}.
 Context {ext_tys: ext_types ext}.
 
-Local Coercion Var' (s:string): expr := Var s.
 Section proof.
   Context `{!heapGS Σ}.
   Context `{!stagedG Σ, !barrierG Σ}.
diff --git a/src/goose_lang/lib/barrier/impl.v b/src/goose_lang/lib/barrier/impl.v
index 68adc1e00..1a22beae2 100644
--- a/src/goose_lang/lib/barrier/impl.v
+++ b/src/goose_lang/lib/barrier/impl.v
@@ -3,7 +3,6 @@ From Perennial.goose_lang Require Export notation typing.
 Module barrier.
   Section goose_lang.
     Context {ext:ffi_syntax}.
-    Local Coercion Var' (s:string): expr := Var s.
     Definition newbarrier : val := λ: <>, ref #false.
     Definition signal : val := λ: "x", CAS "x" #false #true.
     Definition wait : val :=
diff --git a/src/goose_lang/lib/channel/impl.v b/src/goose_lang/lib/channel/impl.v
index 97c3a70fb..15a72b966 100644
--- a/src/goose_lang/lib/channel/impl.v
+++ b/src/goose_lang/lib/channel/impl.v
@@ -13,7 +13,6 @@ Notation ChannelConsV elem content:= (InjRV (elem, content)) (only parsing).
 Section goose_lang.
 Context {ext:ffi_syntax}.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' (s:string) : expr := Var s.
 
   (* 
   infinite loop for nil channels
@@ -175,4 +174,4 @@ Definition ChannelReceive: val :=
   end) ("channel").
 
 
-End goose_lang.
\ No newline at end of file
+End goose_lang.
diff --git a/src/goose_lang/lib/encoding/impl.v b/src/goose_lang/lib/encoding/impl.v
index d287238f8..7443cd028 100644
--- a/src/goose_lang/lib/encoding/impl.v
+++ b/src/goose_lang/lib/encoding/impl.v
@@ -7,9 +7,6 @@ Set Default Proof Using "Type".
 Section goose_lang.
   Context {ext} {ext_ty:ext_types ext}.
 
-  Definition Var' s : @expr ext := Var s.
-  Local Coercion Var' : string >-> expr.
-
   Definition EncodeUInt32: val :=
     λ: "n" "p",
     "p" +ₗ #0 <-[u8T] to_u8 ("n" ≫ #(W32 $ 0*8));;
diff --git a/src/goose_lang/lib/list/impl.v b/src/goose_lang/lib/list/impl.v
index def06d6d4..8f75c3480 100644
--- a/src/goose_lang/lib/list/impl.v
+++ b/src/goose_lang/lib/list/impl.v
@@ -6,7 +6,6 @@ Notation ListCons hd tl := (InjR (Pair hd tl)).
 
 Section goose_lang.
 Context {ext:ffi_syntax}.
-Local Coercion Var' (s:string) : expr := Var s.
 
 Definition ListMatch : val :=
   λ: "l" "nilfun" "consfun",
diff --git a/src/goose_lang/lib/list/list_slice.v b/src/goose_lang/lib/list/list_slice.v
index 6ec848f5f..ecb25103e 100644
--- a/src/goose_lang/lib/list/list_slice.v
+++ b/src/goose_lang/lib/list/list_slice.v
@@ -5,7 +5,6 @@ From Perennial.goose_lang Require Import slice.impl list.impl.
 Section goose_lang.
 Context `{ffi_sem: ffi_semantics}.
 Context {ext_ty:ext_types ext}.
-Local Coercion Var' (s:string) : expr := Var s.
 
 Definition SliceToListFrom t : val :=
   rec: "loop" "s" "i" :=
diff --git a/src/goose_lang/lib/lock/impl.v b/src/goose_lang/lib/lock/impl.v
index 86787979a..3739ac1bc 100644
--- a/src/goose_lang/lib/lock/impl.v
+++ b/src/goose_lang/lib/lock/impl.v
@@ -4,8 +4,6 @@ Module lock.
   Section goose_lang.
     Context {ext:ffi_syntax}.
 
-    Local Coercion Var' (s:string): expr := Var s.
-
     Definition new: val := λ: <>, ref #false.
     Definition try_acquire : val := λ: "l", CAS "l" #false #true.
     Definition acquire : val :=
diff --git a/src/goose_lang/lib/lock/lock.v b/src/goose_lang/lib/lock/lock.v
index c1adbe446..dd5ddc2f0 100644
--- a/src/goose_lang/lib/lock/lock.v
+++ b/src/goose_lang/lib/lock/lock.v
@@ -15,8 +15,6 @@ Context `{ffi_sem: ffi_semantics}.
 Context `{!ffi_interp ffi}.
 Context {ext_tys: ext_types ext}.
 
-Local Coercion Var' (s:string): expr := Var s.
-
 Section proof.
   Context `{!heapGS Σ} (N : namespace).
 
diff --git a/src/goose_lang/lib/map/impl.v b/src/goose_lang/lib/map/impl.v
index 21c27a61b..1967887b6 100644
--- a/src/goose_lang/lib/map/impl.v
+++ b/src/goose_lang/lib/map/impl.v
@@ -8,7 +8,6 @@ Notation AllocMap v := (Alloc (MapNilV v)) (only parsing).
 
 Section goose_lang.
 Context {ext:ffi_syntax}.
-Local Coercion Var' (s:string) : expr := Var s.
 
 (* We store the values of the map into single memory cells, even if they are
 entire structs that would usually be laid out with one memory cell per field.
diff --git a/src/goose_lang/lib/rand/impl.v b/src/goose_lang/lib/rand/impl.v
index adc76fbac..6488d9f9a 100644
--- a/src/goose_lang/lib/rand/impl.v
+++ b/src/goose_lang/lib/rand/impl.v
@@ -4,8 +4,6 @@ Module rand.
   Section goose_lang.
     Context {ext:ffi_syntax}.
 
-    Local Coercion Var' (s:string): expr := Var s.
-
     Definition RandomUint64: val := λ: <>, ArbitraryInt.
   End goose_lang.
 End rand.
diff --git a/src/goose_lang/lib/rwlock/impl.v b/src/goose_lang/lib/rwlock/impl.v
index db1298c1e..58e2c360d 100644
--- a/src/goose_lang/lib/rwlock/impl.v
+++ b/src/goose_lang/lib/rwlock/impl.v
@@ -4,8 +4,6 @@ Module rwlock.
   Section goose_lang.
     Context {ext:ffi_syntax}.
 
-    Local Coercion Var' (s:string): expr := Var s.
-
     (* RWlock is a reference call containing a uint 64:
       - If value is 0, lock is write locked
       - If value is 1, lock is free
diff --git a/src/goose_lang/lib/rwlock/rwlock.v b/src/goose_lang/lib/rwlock/rwlock.v
index 9304ccd47..e663d8fbf 100644
--- a/src/goose_lang/lib/rwlock/rwlock.v
+++ b/src/goose_lang/lib/rwlock/rwlock.v
@@ -19,8 +19,6 @@ Context `{ffi_sem: ffi_semantics}.
 Context `{!ffi_interp ffi}.
 Context {ext_tys: ext_types ext}.
 
-Local Coercion Var' (s:string): expr := Var s.
-
 Section proof.
   Context `{!heapGS Σ} (N : namespace).
   Context `{!stagedG Σ}.
diff --git a/src/goose_lang/lib/rwlock/rwlock_derived.v b/src/goose_lang/lib/rwlock/rwlock_derived.v
index d9eb8c634..e87681baa 100644
--- a/src/goose_lang/lib/rwlock/rwlock_derived.v
+++ b/src/goose_lang/lib/rwlock/rwlock_derived.v
@@ -20,8 +20,6 @@ Context `{ffi_sem: ffi_semantics}.
 Context `{!ffi_interp ffi}.
 Context {ext_tys: ext_types ext}.
 
-Local Coercion Var' (s:string): expr := Var s.
-
 Section proof.
   Context `{!heapGS Σ} (N : namespace).
   Context `{!stagedG Σ}.
diff --git a/src/goose_lang/lib/rwlock/rwlock_noncrash.v b/src/goose_lang/lib/rwlock/rwlock_noncrash.v
index c6977e865..dddfc2d04 100644
--- a/src/goose_lang/lib/rwlock/rwlock_noncrash.v
+++ b/src/goose_lang/lib/rwlock/rwlock_noncrash.v
@@ -19,8 +19,6 @@ Context `{ffi_sem: ffi_semantics}.
 Context `{!ffi_interp ffi}.
 Context {ext_tys: ext_types ext}.
 
-Local Coercion Var' (s:string): expr := Var s.
-
 Section proof.
   Context `{!heapGS Σ} (N : namespace).
   Context `{!stagedG Σ}.
diff --git a/src/goose_lang/lib/slice/impl.v b/src/goose_lang/lib/slice/impl.v
index f8289c12a..b0fe562e4 100644
--- a/src/goose_lang/lib/slice/impl.v
+++ b/src/goose_lang/lib/slice/impl.v
@@ -43,8 +43,6 @@ Implicit Types (t:ty).
 
 Set Default Proof Using "ext ext_ty".
 
-Local Coercion Var' s: expr := Var s.
-
 Theorem has_zero_slice_T t : has_zero (slice.T t).
 Proof.
   auto.
diff --git a/src/goose_lang/lib/slice/slice.v b/src/goose_lang/lib/slice/slice.v
index 611ccbf03..effe081cc 100644
--- a/src/goose_lang/lib/slice/slice.v
+++ b/src/goose_lang/lib/slice/slice.v
@@ -1189,7 +1189,6 @@ Proof.
   wp_apply wp_slice_cap. wp_pures.
   rewrite bool_decide_eq_false_2; [ wp_pures | word ].
   rewrite /SliceCopy.
-  rewrite /impl.Var'.
   wp_pures.
   wp_apply wp_slice_ptr.
   wp_apply wp_slice_cap.
diff --git a/src/goose_lang/lib/string/impl.v b/src/goose_lang/lib/string/impl.v
index cdf7d5fa9..26fc0b0e3 100644
--- a/src/goose_lang/lib/string/impl.v
+++ b/src/goose_lang/lib/string/impl.v
@@ -4,7 +4,6 @@ From Perennial.goose_lang.lib Require Import control.impl.
 Section goose_lang.
 Context {ext:ffi_syntax}.
 Context {ext_ty:ext_types ext}. (* need this to use slice *)
-Local Coercion Var' (s:string) : expr := Var s.
 
 Definition StringFromBytes : val :=
   (rec: "StringFromBytes" "b" :=
diff --git a/src/goose_lang/lib/time/impl.v b/src/goose_lang/lib/time/impl.v
index 83ad501f2..bcce100e8 100644
--- a/src/goose_lang/lib/time/impl.v
+++ b/src/goose_lang/lib/time/impl.v
@@ -6,8 +6,6 @@ Module time.
   Section goose_lang.
     Context {ext:ffi_syntax}.
 
-    Local Coercion Var' (s:string): expr := Var s.
-
     Definition Millisecond: val := #1000000.
     Definition Second: val := #1000000000.
     Definition Sleep: val := λ: "duration", #().
diff --git a/src/goose_lang/lib/waitgroup/impl.v b/src/goose_lang/lib/waitgroup/impl.v
index fb6635dd2..aa59e82ec 100644
--- a/src/goose_lang/lib/waitgroup/impl.v
+++ b/src/goose_lang/lib/waitgroup/impl.v
@@ -7,8 +7,6 @@ Module waitgroup.
     Context {ext:ffi_syntax}.
     Context {ext_tys: ext_types ext}.
 
-    Local Coercion Var' (s:string): expr := Var s.
-
     Definition New: val := λ: <>, (lock.new #(), ref_to uint64T #0).
     Definition Add: val := λ: "wg" "delta",
         let: ("mu", "v") := "wg" in
diff --git a/src/goose_lang/lib/waitgroup/waitgroup.v b/src/goose_lang/lib/waitgroup/waitgroup.v
index 6536bb3fc..c7ffe6bed 100644
--- a/src/goose_lang/lib/waitgroup/waitgroup.v
+++ b/src/goose_lang/lib/waitgroup/waitgroup.v
@@ -20,8 +20,6 @@ Context `{ffi_sem: ffi_semantics}.
 Context `{!ffi_interp ffi}.
 Context {ext_tys: ext_types ext}.
 
-Local Coercion Var' (s:string): expr := Var s.
-
 (*
   XXX:
   The waitgroup docs/comments stresses the fact that "the first WaitGroup.Add
diff --git a/src/goose_lang/notation.v b/src/goose_lang/notation.v
index b8a2af0ec..f6c011c94 100644
--- a/src/goose_lang/notation.v
+++ b/src/goose_lang/notation.v
@@ -13,15 +13,13 @@ Global Open Scope Z. (* Make sure everyone gets this scope. *)
    note that we can't also make W32 a coercion because otherwise we would have
    ambiguous paths between Z and base_lit.
  *)
-Coercion W64 : Z >-> u64.
+Coercion W64 : Z >-> w64.
 Add Printing Coercion W64.
 
 Coercion LitBool : bool >-> base_lit.
 Coercion LitLoc : loc >-> base_lit.
 (* TODO: this should be added *)
 (* Coercion LitString : string >-> base_lit. *)
-(* Coercion LitInt' (x:u64_class) : base_lit := LitInt x.
-Coercion LitInt32' (x:u32_class) : base_lit := LitInt32 x. *)
 Coercion LitInt : u64 >-> base_lit.
 Coercion LitInt32 : u32 >-> base_lit.
 Coercion LitByte : u8 >-> base_lit.
@@ -38,7 +36,10 @@ Qed.
 Coercion App : expr >-> Funclass.
 
 Coercion Val : val >-> expr.
-(* Coercion Var : string >-> expr.  Doesn't work as [Var] has a typeclass parameter. *)
+(** As of https://github.com/coq/coq/pull/15789 Coq does not require the uniform
+inheritance criteria, but silencing the warning is still required. *)
+#[warning="-uniform-inheritance"]
+Coercion Var : string >-> expr.
 
 (** Define some derived forms. *)
 Notation Lam x e := (Rec BAnon x e) (only parsing).
diff --git a/src/goose_lang/trusted/github_com/goose_lang/goose/internal/examples/trust_import/trusted_example.v b/src/goose_lang/trusted/github_com/goose_lang/goose/internal/examples/trust_import/trusted_example.v
index 6a6e8dd72..82dc3020b 100644
--- a/src/goose_lang/trusted/github_com/goose_lang/goose/internal/examples/trust_import/trusted_example.v
+++ b/src/goose_lang/trusted/github_com/goose_lang/goose/internal/examples/trust_import/trusted_example.v
@@ -5,8 +5,6 @@ Module trusted_example.
     Context {ext:ffi_syntax}.
     Context {ext_tys: ext_types ext}.
 
-    Local Coercion Var' (s:string): expr := Var s.
-
     Definition Foo: val := λ: <>, #().
   End goose_lang.
 End trusted_example.
diff --git a/src/goose_lang/trusted/github_com/mit_pdos/gokv/trusted_hash.v b/src/goose_lang/trusted/github_com/mit_pdos/gokv/trusted_hash.v
index f84341fdd..77f45e00e 100644
--- a/src/goose_lang/trusted/github_com/mit_pdos/gokv/trusted_hash.v
+++ b/src/goose_lang/trusted/github_com/mit_pdos/gokv/trusted_hash.v
@@ -3,7 +3,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Axiom Hash: val.
 
diff --git a/src/goose_lang/trusted/github_com/mit_pdos/gokv/trusted_proph.v b/src/goose_lang/trusted/github_com/mit_pdos/gokv/trusted_proph.v
index 9c07e8242..de62d9dc0 100644
--- a/src/goose_lang/trusted/github_com/mit_pdos/gokv/trusted_proph.v
+++ b/src/goose_lang/trusted/github_com/mit_pdos/gokv/trusted_proph.v
@@ -4,8 +4,6 @@ Section goose_lang.
 Context `{ffi_sem: ffi_semantics}.
 Context {ext_ty:ext_types ext}.
 
-Local Coercion Var' (s:string) : expr := Var s.
-
 Definition ActReadId : Z := 0.
 Definition ActAbortId : Z := 1.
 Definition ActCommitId : Z := 2.
diff --git a/src/goose_lang/trusted/github_com/mit_pdos/vmvcc/trusted_proph.v b/src/goose_lang/trusted/github_com/mit_pdos/vmvcc/trusted_proph.v
index 20cd87693..746af0fb0 100644
--- a/src/goose_lang/trusted/github_com/mit_pdos/vmvcc/trusted_proph.v
+++ b/src/goose_lang/trusted/github_com/mit_pdos/vmvcc/trusted_proph.v
@@ -5,8 +5,6 @@ Section goose_lang.
 Context `{ffi_sem: ffi_semantics}.
 Context {ext_ty:ext_types ext}.
 
-Local Coercion Var' (s:string) : expr := Var s.
-
 Definition ActReadId : Z := 0.
 Definition ActAbortId : Z := 1.
 Definition ActCommitId : Z := 2.
diff --git a/src/program_proof/bad_nil_slice.v b/src/program_proof/bad_nil_slice.v
index 1cfd5f638..c09172f0f 100644
--- a/src/program_proof/bad_nil_slice.v
+++ b/src/program_proof/bad_nil_slice.v
@@ -15,7 +15,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 (* FIXME: should not be possible to prove this assert *)
 Definition test: val :=
diff --git a/src/program_proof/bad_zero_func.v b/src/program_proof/bad_zero_func.v
index ad8b8a3b1..80c9a6c22 100644
--- a/src/program_proof/bad_zero_func.v
+++ b/src/program_proof/bad_zero_func.v
@@ -17,7 +17,6 @@ From Perennial.goose_lang Require Import prelude.
 
 Section code.
 Context `{ext_ty: ext_types}.
-Local Coercion Var' s: expr := Var s.
 
 Definition main: val :=
   rec: "main" <> :=