Pre and Post conditions in Rholang as transaction and payment boundaries

Motivation

I have been looking for a compelling transaction model for Rholang for a long time. We want to be able to prevent certain half-baked states from occurring. We would rather the computation revert rather than be half-cocked.

Background

Rholang can't use call return semantics to manage transaction boundaries, because it doesn't have them. It isn't a confluent language. In order to specify a transaction in Rholang, it was clear to me that we would need to specify a structural type that the state would evolve to.

The problem with that is that the system may evolve further than the state specified, for example if you wanted the system to evolve to two writes, those writes may in turn reduce. How do you know when to stop the system.

Insight

The insight was that for transaction boundaries to make sense, you had to be able to specify pre and post conditions. Let's look at two examples:

contract cell(method, @initval) = {
	new state in {
		state!(initval) |
		for (@"get", ret <= method; @val <= state): {=method!("get", ret) | =state!(val) ▶ =state!(=val) | =ret!(=val) } {
			state!(val) | ret!(val)
		}
		for (@"modify", f <= method; @val <= state): {=method!("modify", f) | =state!(val) | for(@x, ret <- =f) { _ } ▶ =state!(_) } {
			new ret in {
				f!(val, *ret) |
				for (x <- ret) { state!(x) }
			}
		}
		// Possibly other methods.
	}
}
		
		


The first example is fairly simple. If we evaluate a single copy of the receive where only the matching writes are available, then we reduce to a return call and a replacement write of the state.

The second example starts to show the power of this approach. We specify that something must be listening on f, matching the pattern that we are sending. If f correctly follows function discipline, then the postcondition will be satisfied.

Notes

These are linear preconditons. They may only be used once, and if not used, must be present in the postcondition.

These act in some sense like import statements. We will recursively import pre-conditions of pre-conditions.