Algebraic properties of amounts

[erights]

An amount is a group defined by the following abstract operators (represented by methods of AmountMath. The two most common abstract examples of amounts are natural numbers and sets.

These operators must always be pure deterministic predicates and functions, up to equivalence regarding these operators.

name	nats	sets
empty	0	empty set
isGTE	>=	superset (note: not strict superset)
isEqual	==	set equality (matching elements—∀x, x ∈ S1 ⇔ x ∈ S2)
add	+	union
subtract	-	relative complement S1 \ S2 ({x ∈ S1 : x ∉ S2}), defined only where the left operand S1 is a superset of the right S2

We need to define the algebraic properties that these operators have in relationship to each other. All amount implementations, and therefore all extent implementations, must be verified (initially by hand) to have these algebraic properties. Our own generically parametrizable code, such as Zoe and most of our contracts, must not count on any algebraic properties not guaranteed by the amount specification. This issue is a start on gathering such algebraic properties. Note I am not a formalist and this should be taken up by someone who is.

forall x, y, z which are amounts from the same amount group, where 0 is the empty of that group:

• x >= y is a total predicate, i.e., always gives true or false, never an error.
• x >= 0, all amounts include the empty amount. Thus, no negatives.
• >= is a partial order
• x == y iff x and y are indistinguishable by these operators. == is a total predicate.
• x + y is total and closed, meaning it is defined for all x and y and always produces a new amount from the same group.
• x + y == y + x, so + is commutative
• (x + y) + z == x + (y + z), so + is associative
• x + y >= x (therefore x + y >= y), so + is monotonic
• x + 0 == x (therefore 0 + x == x), so empty is the identity element
• x - y is not total. It is defined iff x >= y. It is closed, i.e., where it is defined, its result is another amount of the same group.
• x + y == z iff z - x == y (therefore z - y == x). Since the left equation implies z >= x and z >= y, the subtraction is defined everywhere that the left equation holds.

(question: are any of the above bullets implied by the others, and can therefore be dropped as definitional?)

Given only the above guarantees, we should be able to prove that, with purses and payments of a well behaved issuer ( Agoric/documentation#663 ) , but without access to that issuer's mint, one cannot violate conservation of currency. This should follow from the mapping of deposit to +, of withdraw to - (including the >= check), the associative, commutative nature of + and the relationship of + to -. We should be able to generalize the other proofs in https://research.google/pubs/pub44272/ in the same manner.

Design

• property testing for copyBag
• property testing for other nat and other AssetKinds
• add these properties to ERTP API documentation

[erights]

In writing the issue, I realized that it is already wrong. The relationship between + and - does not hold for sets, because set union loses information. We need to replace our + row with something like

name	nats	sets
add	+	disjoint union, i.e., union defined only when the intersection is empty.

and add a new column for multisets (or bags), which are equivalent to @katelynsills maps from set elements to naturals. On multisets, + does not lose info. The + vs - relationships above still hold. And + is still total and closed.

On sets with + being disjoint union, + would not be total. However, I'm not sure what I can say in general about where + is guaranteed to be defined without referring to sets.

The reason our purses and payments still work when + is disjoint union is subtle. The sets represent sets of elements, where each element is an atomic exclusively transferable eright. Any one element should only be in one place at a time --- because of exclusive erights transfer. Thus, the use of + within the purse and payment logic will never attempt a union of two sets that fail. Before we separated purse and payment, depositing a purse into itself might have encountered this failure, depending on how it was written. With the separation, the remaining aliasing hazard is combining a payment with itself, which I will now look at.

It is clear that the difference between exclusive and shared erights will not be in the AmountMath but rather in the way purses and payments use these operations to transfer erights around. TBD.

[erights]

Looked at #523 . Bottoms out in reallocate which we'd already gone over, where aliasing correctly causes an error.

But the interesting thing is that combine checks conservation first. In the aliasing case, where the amountMath add is not total, but for example enforces disjoint union, the aliasing may only cause the combine to fail earlier. Both failure points precede any side effects, so everything looks fine.

[erights]

which are equivalent to @katelynsills maps from set elements to naturals.

I'm wrong. @katelynsills 's lists of naturals is doing something else. We don't yet have multiset amountMath.

[erights]

Because x + y >= y and z - y is defined when z >= y, we know that x + y - y is defined everywhere x + y is defined. The constraint I was looking for above is: Everywhere that x + y is defined, x + y - y == x. IOW, everywhere that x + y - y == x would not hold if x + y were defined, x + y must not be defined.

From this we can conclude that + cannot be normal set union. But it can be set disjoint union or multiset union. It seems a general way to state what I was getting at above with "loses information". With this constraint, we can say the if y erights are deposited into a purse, and then y erights are withdrawn from the purse, that the purse's balance is restored.

[katelynsills]

This all sounds very good to me. I had previously been thinking that the AmountMath should intentionally handle duplicates. For example, even if the situation would never come up in withdraw or deposit, I was thinking that users who were using AmountMath for their own calculations might be a little sloppy and accidentally have duplicates. Now it sounds like we might want to disallow any duplicates in both the left and right arguments as well as the union (I think this is the disjoin union option, but I don't understand the multiset union yet, needs googling).

[erights]

Following up on @katelynsills last comment above. We discussed further and decided that indeed, the right semantics for most uses is sets, not multisets, where add is disjoint union, i.e., collisions cause an error. Further, set creation should error on duplicates.

[erights]

@katelynsills @Chris-Hibbert @tyg I think this needs to be settled and carefully written down. Given the refactorings we're in the midst of, this is a good time to at least refamiliarize ourselves with it. So assigning the four of us.

[erights]

Searching, the closest math concept I found is the Commutative Monoid https://en.wikipedia.org/wiki/Monoid#Commutative_monoid . The monoid's add operator implies its ordering operator. The properties of all these seem to match.

[tgrecojs]

Searching, the closest math concept I found is the Commutative Monoid https://en.wikipedia.org/wiki/Monoid#Commutative_monoid . The monoid's add operator implies its ordering operator. The properties of all these seem to match.

hey @erights, I've spent some time looking into this issue this week and have a quick question. Is the end goal for this issue to express that AmountMath is an object that contains nested algebraic data types that can be used within ERTP for the purposes of checking equality of amounts, adding amounts, subtracting amounts, etc.? I get the impression that this may be the case, but seeing the amount of discussion around the add method, I want to make sure that addition is not the only operation that this issue is concerned with.

[erights]

I want to make sure that addition is not the only operation that this issue is concerned with.

Correct. Reusing the table from the top (which is still accurate for amountMath) a use we make of each is:

name	example use
empty	Zoe making fresh escrow purse from shared issuer, solving a mutual trust problem
isGTE	Offer safety: would this allocation satisfy the proposal's give or want?
isEqual	Is the amount escrowed the same as the give?
add	Purse deposit
subtract	Purse withdraw

[dckc]

@erights writes Aug 5, 2021:

Searching, the closest math concept I found is the Commutative Monoid

I learned enough TLA+ to specify CommutativeMonoid:

https://github.com/Agoric/agoric-sdk/blob/dc-ertp-spec/packages/ERTP/spec/Amount.tla
bf1af1f

agoric-sdk/packages/ERTP/spec$ apalache-mc parse Amount.tla 
# Tool home: /home/connolly/opt/apalache-v0.19.3
# Package:   /home/connolly/opt/apalache-v0.19.3/mod-distribution/target/apalache-pkg-0.19.3-full.jar
# APALACHE version 0.19.3 build 52f9fe2
Parse Amount.tla                                                  I@12:57:07.428
Root module: Amount with 3 declarations                           I@12:57:07.713
Total time: 0.651 sec                                             I@12:57:07.715
EXITCODE: OK

TLA+ Crash Course

These are the materials I learned from:

• informalsystems/apalache: APALACHE: symbolic model checker for TLA+
  • tla-apalache-workshop/clock-sync-steps.md at main · informalsystems/tla-apalache-workshop
  • agoric-kernel-models/kernel.tla at main · informalsystems/agoric-kernel-models
• Operators :: Learn TLA+
• TLA+ in Practice and Theory
  Part 2: The + in TLA+
  • Curry On Talk: The Practice and Theory of TLA+
  • Ron Pressler - The Practice and Theory of TLA+ - YouTube

[dckc]

since AmountMath is stateless, property testing is about the same thing as model checking with TLA+:

packages/ERTP/test/unitTests/test-amountProperties.js

[erights]

Hi @Tyrosine22 and @dckc , I just removed Tom and added you two. It would be cool to get this written down in a coherent and clear manner, and to put into into the appropriate findable place. Where would that be?

[dckc]

In ERTP docs, after basics of fungible amounts, when we give details about nfts, SET, and COPY_BAG.