From bf1af1f7a8be4d5fb5c94c2a5f60cf9941af6516 Mon Sep 17 00:00:00 2001
From: Dan Connolly <connolly@agoric.com>
Date: Fri, 21 Jan 2022 12:49:42 -0600
Subject: [PATCH] docs(ERTP): toward Algebraic properties of amounts

refs #557
CommutativeMonoid specification
---
 packages/ERTP/spec/Amount.tla | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)
 create mode 100644 packages/ERTP/spec/Amount.tla

diff --git a/packages/ERTP/spec/Amount.tla b/packages/ERTP/spec/Amount.tla
new file mode 100644
index 000000000000..2dd630b3f6e1
--- /dev/null
+++ b/packages/ERTP/spec/Amount.tla
@@ -0,0 +1,17 @@
+------------------------------ MODULE Amount ------------------------------
+EXTENDS Integers
+
+Semigroup(S, combine(_, _)) ==
+    \A a \in S: \A b \in S: \A c \in S:
+    combine(a, b) \in S \* Closure
+    /\  combine(combine(a, b), c) = combine(a, combine(b, c)) \* Associativity
+
+Monoid(M, combine(_, _)) ==
+    Semigroup(M, combine)
+    /\ \E id \in M : \A a \in M: combine(id, a) = a /\ combine(a, id) = a \* Identity
+
+CommutativeMonoid(M, combine(_, _)) ==
+    Monoid(M, combine) /\
+    \A a \in M: \A b \in M: combine(a, b) = combine(b, a)
+
+===============================================================================