From abaaea3bfb81827974f395a422843153d2b91a13 Mon Sep 17 00:00:00 2001 From: Tej Chajed Date: Fri, 6 Sep 2024 11:26:56 -0500 Subject: [PATCH] Make Var a coercion It was originally not due to failing the "uniform inheritance criteria", but this criteria is no longer required. This should ensure that variables are actually printed as strings, hiding the Var coercion, which will make code much more readable without the ugly hack of the `Var'` coercions. The massive fallout is due to removing many coercions Var' that were defined for specific type parameters, all of which can now use the single coercion on Var. --- _CoqProject | 1 + .../goose/internal/examples/comments.v | 1 - .../goose/internal/examples/rfc1813.v | 1 - .../goose/internal/examples/simpledb.v | 1 - .../goose/internal/examples/trust_import.v | 1 - .../examples/trust_import/trusted_example.v | 1 - .../internal/examples/unittest/generic.v | 1 - external/Goose/github_com/goose_lang/std.v | 1 - .../github_com/mit_pdos/go_journal/alloc.v | 1 - .../github_com/mit_pdos/go_journal/lockmap.v | 1 - .../github_com/mit_pdos/go_journal/util.v | 1 - .../github_com/mit_pdos/go_nfsd/nfstypes.v | 1 - .../Goose/github_com/mit_pdos/gokv/bank.v | 1 - .../github_com/mit_pdos/gokv/dmvcc/example.v | 1 - .../github_com/mit_pdos/gokv/dmvcc/index.v | 1 - .../mit_pdos/gokv/dmvcc/prophname.v | 1 - .../github_com/mit_pdos/gokv/dmvcc/txn.v | 1 - .../mit_pdos/gokv/dmvcc/txncoordinator.v | 1 - .../github_com/mit_pdos/gokv/dmvcc/txnmgr.v | 1 - .../Goose/github_com/mit_pdos/gokv/erpc.v | 1 - external/Goose/github_com/mit_pdos/gokv/kv.v | 1 - .../github_com/mit_pdos/gokv/lockservice.v | 1 - .../github_com/mit_pdos/gokv/map_marshal.v | 1 - .../mit_pdos/gokv/map_string_marshal.v | 1 - .../mit_pdos/gokv/tutorial/basics.v | 1 - .../github_com/mit_pdos/gokv/tutorial/queue.v | 1 - .../Goose/github_com/mit_pdos/gokv/vrsm/e.v | 1 - .../Goose/github_com/mit_pdos/pav/cryptoffi.v | 1 - .../github_com/mit_pdos/pav/cryptoutil.v | 1 - .../github_com/mit_pdos/pav/marshalutil.v | 1 - .../Goose/github_com/mit_pdos/pav/merkle.v | 1 - .../mit_pdos/perennial_examples/alloc.v | 1 - .../Goose/github_com/mit_pdos/rsm/distx.v | 1 - .../Goose/github_com/mit_pdos/rsm/mpaxos.v | 1 - external/Goose/github_com/mit_pdos/rsm/pcr.v | 1603 +++++++++++++++++ .../Goose/github_com/mit_pdos/rsm/spaxos.v | 1 - external/Goose/github_com/mit_pdos/rsm/tpl.v | 1 - .../Goose/github_com/mit_pdos/vmvcc/common.v | 1 - .../Goose/github_com/mit_pdos/vmvcc/config.v | 1 - .../mit_pdos/vmvcc/examples/strnum.v | 1 - .../Goose/github_com/mit_pdos/vmvcc/index.v | 1 - .../Goose/github_com/mit_pdos/vmvcc/tuple.v | 1 - .../Goose/github_com/mit_pdos/vmvcc/wrbuf.v | 1 - external/Goose/github_com/tchajed/marshal.v | 1 - new/golang/defn/noop.v | 1 - new/golang/defn/notation.v | 2 + src/goose_lang/ffi/async_disk_prelude.v | 2 - src/goose_lang/ffi/disk_prelude.v | 4 - .../ffi/grove_ffi/grove_ffi_typed.v | 1 - src/goose_lang/ffi/grove_ffi/typed_impl.v | 1 - src/goose_lang/ffi/grove_prelude.v | 4 - src/goose_lang/interpreter/test_config.v | 1 - src/goose_lang/lang.v | 11 - src/goose_lang/lib/barrier/barrier.v | 1 - src/goose_lang/lib/barrier/impl.v | 1 - src/goose_lang/lib/channel/impl.v | 3 +- src/goose_lang/lib/encoding/impl.v | 3 - src/goose_lang/lib/list/impl.v | 1 - src/goose_lang/lib/list/list_slice.v | 1 - src/goose_lang/lib/lock/impl.v | 2 - src/goose_lang/lib/lock/lock.v | 2 - src/goose_lang/lib/map/impl.v | 1 - src/goose_lang/lib/rand/impl.v | 2 - src/goose_lang/lib/rwlock/impl.v | 2 - src/goose_lang/lib/rwlock/rwlock.v | 2 - src/goose_lang/lib/rwlock/rwlock_derived.v | 2 - src/goose_lang/lib/rwlock/rwlock_noncrash.v | 2 - src/goose_lang/lib/slice/impl.v | 2 - src/goose_lang/lib/slice/slice.v | 1 - src/goose_lang/lib/string/impl.v | 1 - src/goose_lang/lib/time/impl.v | 2 - src/goose_lang/lib/waitgroup/impl.v | 2 - src/goose_lang/lib/waitgroup/waitgroup.v | 2 - src/goose_lang/notation.v | 9 +- .../examples/trust_import/trusted_example.v | 2 - .../github_com/mit_pdos/gokv/trusted_hash.v | 1 - .../github_com/mit_pdos/gokv/trusted_proph.v | 2 - .../github_com/mit_pdos/vmvcc/trusted_proph.v | 2 - src/program_proof/bad_nil_slice.v | 1 - src/program_proof/bad_zero_func.v | 1 - 80 files changed, 1612 insertions(+), 114 deletions(-) create mode 100644 external/Goose/github_com/mit_pdos/rsm/pcr.v 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" <> :=