I'm proposing a Petri-net based standard for smart contract state machines.
I think UX is greatly improved when event-based designs are implemented ast state machines. This approach seeks to apply formal Petri-net designs to smart contract development.
Please review a sample contract here:
https://github.com/pflow-xyz/pflow-eth/blob/main/hardhat/contracts/MyStateMachine.sol#L50-L56
Models can be shared as SVG images via this markdown.
[![pflow](https://pflow.dev/img/zb2rhkizUC1o2JuvgwhbH1XrLZkdK8x66pP1KR7sWAEw9c5FE.svg)](https://pflow.dev/p/zb2rhkizUC1o2JuvgwhbH1XrLZkdK8x66pP1KR7sWAEw9c5FE/)
Models are stored and referenced via CID's, a golang library provides a consistent encoding for each petri-net design: https://github.com/pflow-xyz/pflow-xyz/blob/main/protocol/zblob/zblob.go
The model interface provides a means to send 1 or many signals to the contract at a time.
interface ModelInterface {
function context() external returns (Model.Head memory);
function signal(uint8 action, uint256 scalar) external;
function signalMany(uint8[] calldata actions, uint256[] calldata scalars) external;
}
There's a few other parts involved, but the idea is to expand the model syntax with enough syntactic sugar to be readable and composable. Here's the demo model above
abstract contract MyModelContract is Metamodel {
enum Roles {role0, HALT}
enum Properties {place0, SIZE}
enum Actions {txn0, txn1, txn2, txn3, HALT}
int256[] public state = new int256[](uint8(Properties.SIZE));
constructor() {
cell("place0", 0, 3, Model.Position(1, 2));
func("txn0", uint8(Properties.SIZE), uint8(0), uint8(Roles.role0), Model.Position(0, 1));
func("txn1", uint8(Properties.SIZE), uint8(1), uint8(Roles.role0), Model.Position(2, 1));
func("txn2", uint8(Properties.SIZE), uint8(2), uint8(Roles.role0), Model.Position(0, 3));
func("txn3", uint8(Properties.SIZE), uint8(3), uint8(Roles.role0), Model.Position(2, 3));
arrow(1, transitions[0], places[0]);
arrow(3, places[0], transitions[1]);
guard(3, transitions[2], places[0]);
guard(1, places[0], transitions[3]);
for (uint8 i = 0; i < uint8(Properties.SIZE); i++) {
state[i] = int256(places[i].initial);
}
}
}
Notice above a declarative syntax for constructing a petri-net.
There is a demo UI here: app.pflow.xyz that presents a clickable diagram that will initiate calls to the sigal()
api.
The underlying data structures are provided by this library - all state-transitions result in the emission of SignaledEven
library Model {
event SignaledEvent(
uint8 indexed role,
uint8 indexed actionId,
uint256 indexed scalar,
uint256 sequence
);
struct PetriNet {
Place[] places;
Transition[] transitions;
}
struct Position {
uint8 x;
uint8 y;
}
struct Transition {
string label;
uint8 offset;
Position position;
uint8 role;
int256[] delta;
int256[] guard;
}
struct Place {
string label;
uint8 offset;
Position position;
uint256 initial;
uint256 capacity;
}
struct Head {
uint256[10] latestBlocks;
uint256 sequence;
int256[] state;
Place[] places;
Transition[] transitions;
}
}
On the Front end - we read the contract head to present the diagram to the user for wallet interaction: see demo at: app.pflow.xyz
For future study - I'm hoping to apply this type of notation to build interactive state channels.
Docs available https://pflow.xyz/docs