What Is a Form in Formagine?
A Form is Formagine's core primitive. It is a self-contained algebraic type that combines three things: state declarations that define the contract's data, invariant specifications that define properties the state must always satisfy, and transition definitions that define how the state changes. The compiler proves that every transition preserves every invariant, then erases the invariant annotations and emits optimized WASM. A Form is simultaneously a contract definition, a formal specification, and a proof obligation.
The Three Components of a Form
State defines the data the contract holds. Each field has a name and a type. Scalar fields like supply : Nat hold a single value. Mapped fields like balance : Nat per Address associate a value with each element of a domain. State fields are the variables that invariants constrain and transitions modify.
Invariants are named equations or inequalities over state fields that must hold in every reachable state. The invariant sum(balance) == supply states that the aggregate of all balance entries must equal the supply scalar. Invariants are not runtime checks. They are mathematical properties that the compiler proves at compile time. Once proven, they are erased from the output.
Transitions are named functions that modify state. Each transition can include require clauses (preconditions that must hold for the transition to execute) and assignment statements that update state fields. The compiler analyzes each transition to verify that every invariant holds in the post-state, given that it held in the pre-state.
Complete Token Example
form Token { state { balance : Nat per Address supply : Nat owner : Address } invariant conservation : sum(balance) == supply transition transfer(from, to, amount) { require balance[from] >= amount balance[from] -= amount balance[to] += amount } transition mint(to, amount) { require msg.sender == owner balance[to] += amount supply += amount } transition burn(from, amount) { require balance[from] >= amount balance[from] -= amount supply -= amount } }
This Form declares three state fields, one invariant, and three transitions. The compiler verifies that transfer, mint, and burn all preserve the conservation invariant. Transfer preserves it by arithmetic cancellation (the sum does not change). Mint and burn preserve it by co-variance (both sides of the equation change by the same delta). The algebraic verification runs at compile time, and the proven invariant is erased from the WASM output.
The Algebraic Structure of a Form
Formally, a Form defines an algebraic structure consisting of three components:
State space S. The set of all possible valuations of the state fields. For the Token form, S is the set of all triples (balance, supply, owner) where balance is a function from addresses to natural numbers, supply is a natural number, and owner is an address.
Transition function T. Each transition is a partial function from S to S. It is partial because the require clauses restrict its domain. The transfer transition is defined only on states where balance[from] >= amount.
Invariant predicates I. Each invariant is a predicate on S. The conservation invariant is the predicate I(s) = (sum(s.balance) == s.supply). The verification problem is: for every invariant I and every transition T, if I(s) holds and T is defined at s, then I(T(s)) holds. This is an inductive invariant proof. The compiler performs it by algebraic reasoning over the structure of T.
How Forms Differ from Other Contract Primitives
Solidity contracts are imperative programs. They define storage variables and functions, but invariants are implicit. A Solidity developer might intend that the sum of balances equals total supply, but this intention exists only in comments and tests. The Solidity compiler cannot verify it. A Form makes the invariant explicit and machine-checkable.
Rust structs (as used in CosmWasm or Near) define data layout and can have methods, but the Rust compiler verifies memory safety and type correctness, not domain-specific invariants. You can write a Rust struct that represents a token, but the compiler will not prove that your transfer function preserves conservation. You would need to add runtime assertions or use an external verification tool.
Move resources provide linear type guarantees: resources cannot be copied or implicitly discarded. This prevents a class of bugs (double-spending at the type level) but does not verify arbitrary arithmetic invariants. A Move resource cannot express "the sum of all balances equals total supply" as a type-level property. Forms and Move resources address overlapping but distinct concerns.
The key difference is that a Form integrates the specification (invariants) with the implementation (transitions) and the verification (compiler) in a single construct. In every other system, these three concerns are separate artifacts maintained by separate processes. By unifying them, Forms ensure that the specification is always in sync with the implementation, and verification is always up to date.
Frequently Asked Questions
- How does a Form differ from a Solidity contract?
- A Solidity contract is imperative code with implicit invariants. A Form makes invariants explicit and first-class. The compiler proves them automatically. Solidity allows arbitrary code including external calls and inline assembly. A Form is constrained to state, invariants, and structured transitions, precisely the subset that can be algebraically verified.
- How does a Form differ from a Rust struct or Move resource?
- Rust structs define data layout but the compiler does not verify domain-specific invariants like conservation. Move resources provide linear type guarantees but cannot express arbitrary arithmetic properties. A Form combines data definition, behavioral specification, and proof obligation in a single construct.
- Can a Form have multiple invariants?
- Yes. A Form can declare any number of invariants. Each transition must preserve all of them. The compiler verifies each invariant independently against each transition and reports the specific pair if any proof obligation fails.
- What types can Form state fields have?
- Nat (natural numbers), Int (integers), Bool (booleans), Address (blockchain addresses), and mappings via the
perkeyword. These types correspond to the values that appear in smart contract state and that the algebraic verification engine can reason about.