Transition Semantics

A transition is a named state mutation with parameters, preconditions, and updates. Transitions are the only mechanism by which a Form's state changes. The compiler analyzes each transition to generate proof obligations against every declared invariant. If all obligations are discharged, the transition is proven correct. If any obligation fails, compilation is rejected with a counterexample.

Transition Structure

A transition declaration has four components: a name, a parameter list, zero or more require clauses, and a sequence of state updates. The name becomes the entry point in the compiled WASM module. Parameters are typed by inference from their usage within the transition body.

transition name(param1, param2, ...) {
  require precondition_1
  require precondition_2
  -- ... more preconditions ...

  state_var_1 = new_value
  state_var_2 += delta
  map_var[key] -= delta
  -- ... more updates ...
}

The semantics are strictly sequential within a transition body. Require clauses are evaluated first, in declaration order. If any require clause evaluates to false, the transition aborts and the state is unchanged. If all require clauses pass, the updates execute in declaration order. After all updates complete, the post-state must satisfy every invariant.

Formal Semantics

A transition t(p1, ..., pk) defines a partial function from states to states. Given pre-state S and parameter values v1, ..., vk, the transition produces post-state S' according to the following rules.

-- Transition semantics for t(p1, ..., pk): -- Let S be the pre-state. -- Let v1, ..., vk be the parameter values. -- Let R1, ..., Rn be the require clauses. -- Let U1, ..., Um be the update statements. -- Step 1: Evaluate preconditions in S. -- For each Ri, evaluate Ri(S, v1, ..., vk). -- If any Ri evaluates to false, the transition is undefined -- (aborts). The state remains S. -- Step 2: Apply updates sequentially. -- S0 = S -- S1 = apply(U1, S0) -- S2 = apply(U2, S1) -- ... -- S' = Sm = apply(Um, S(m-1)) -- Step 3: Post-state S' must satisfy all invariants. -- For each invariant I: I(S') must hold.

The sequential application of updates means that later updates see the effects of earlier updates within the same transition. For example, if U1 sets x = 5 and U2 reads x, then U2 sees the value 5. This is important for verification because the compiler must thread the state through each update to compute the final post-state.

Require Clauses

A require clause is a boolean expression that must evaluate to true for the transition to proceed. If the expression evaluates to false, the transition aborts with no state change. Require clauses serve two purposes: they enforce runtime preconditions (access control, balance sufficiency, temporal guards), and they provide assumptions that the verifier uses to discharge proof obligations.

Require as Type Guard

Certain require clauses are necessary for type safety. The expression balance[from] -= amount is only well-typed when balance[from] >= amount, because Nat subtraction requires a non-negativity precondition. The require clause require balance[from] >= amount serves as the type guard that makes the subtraction legal. Without it, the compiler rejects the transition as a type error before verification even begins.

Require as Proof Assumption

During verification, the compiler assumes all require clauses hold when proving invariants. The proof obligation for a (transition, invariant) pair is not "the invariant holds in S'" unconditionally, but rather "if all require clauses hold in S and the invariant holds in S, then the invariant holds in S'." This conditional structure means that require clauses can provide facts that the verifier needs to complete a proof.

-- Require clauses as proof assumptions: transition withdraw(amount) { require deposited[msg.sender] >= amount -- [R1] require block.time >= lock_until[msg.sender] -- [R2] deposited[msg.sender] -= amount total -= amount } -- For invariant conservation: sum(deposited) == total -- Proof: assumes R1 holds (so subtraction is valid), -- shows sum(deposited') = sum(deposited) - amount -- total' = total - amount -- hence sum(deposited') == total'. QED -- For invariant time_lock: -- Proof: assumes R2 holds, which IS the invariant predicate. -- The require clause directly establishes the guard. -- QED

Update Statements

Update statements modify the Form's state. The Form language supports five update forms.

-- Direct assignment: x = expr -- sets x to expr -- Compound addition: x += expr -- sets x to x + expr -- Compound subtraction (requires precondition for Nat): x -= expr -- sets x to x - expr -- Map entry update: m[key] = expr -- sets the entry for key m[key] += expr -- increments the entry m[key] -= expr -- decrements the entry -- External call (for fund disbursement): send(address, amount) -- transfers native currency

The send statement is the only mechanism for transferring value out of the contract. It is a side effect, not a state update. The compiler treats send as opaque for verification purposes: it does not affect the Form's state variables. The verifier reasons only about the Form's internal state; the correctness of the external transfer is the responsibility of the target chain's runtime.

Proof Obligation Generation

The compiler generates one proof obligation for every (transition, invariant) pair. A Form with n transitions and m invariants produces n * m proof obligations. Each obligation has the following structure.

-- Proof Obligation Schema: -- Given: -- Transition t with requires R1, ..., Rn and updates U1, ..., Um -- Invariant I -- Prove: -- I(S) /\ R1(S) /\ R2(S) /\ ... /\ Rn(S) => I(S') -- Where S' is computed by applying U1, ..., Um to S sequentially.

The formula reads: if the invariant holds in the pre-state and all require clauses hold, then the invariant holds in the post-state. This is the standard inductive invariant proof structure. The base case (invariant holds in the initial state) is checked separately during Form initialization.

Token Transfer: Complete Proof Obligation Generation

The following derivation shows the complete proof obligation generation for the Token form's transfer transition against the conservation invariant.

transition transfer(from, to, amount) {
  require balance[from] >= amount        -- R1
  balance[from] -= amount                 -- U1
  balance[to]   += amount                 -- U2
}

invariant conservation : sum(balance) == supply

-- Proof obligation: transfer x conservation -- Given (pre-state assumptions): -- I(S): sum(balance) == supply [invariant holds in S] -- R1(S): balance[from] >= amount [require holds in S] -- Compute post-state S': -- After U1: balance'[from] = balance[from] - amount -- After U2: balance'[to] = balance[to] + amount -- All other balance entries unchanged. -- supply' = supply (supply not modified by transfer) -- Compute sum(balance'): -- sum(balance') = sum(balance) -- - amount [from U1: balance[from] decreased] -- + amount [from U2: balance[to] increased] -- = sum(balance) -- Prove I(S'): sum(balance') == supply' -- sum(balance') = sum(balance) = supply = supply' -- QED by arithmetic identity: -amount + amount = 0

Token Mint: Complete Proof Obligation Generation

transition mint(to, amount) {
  require msg.sender == owner              -- R1
  balance[to] += amount                    -- U1
  supply      += amount                    -- U2
}

-- Proof obligation: mint x conservation -- Given: -- I(S): sum(balance) == supply -- R1(S): msg.sender == owner -- Compute post-state S': -- balance'[to] = balance[to] + amount -- supply' = supply + amount -- Compute sum(balance'): -- sum(balance') = sum(balance) + amount -- Prove I(S'): sum(balance') == supply' -- sum(balance) + amount == supply + amount -- By I(S): sum(balance) = supply -- supply + amount == supply + amount -- QED by algebraic co-variance

Token Burn: Complete Proof Obligation Generation

transition burn(from, amount) {
  require balance[from] >= amount          -- R1
  balance[from] -= amount                   -- U1
  supply        -= amount                   -- U2
}

-- Proof obligation: burn x conservation -- Given: -- I(S): sum(balance) == supply -- R1(S): balance[from] >= amount -- Compute post-state S': -- balance'[from] = balance[from] - amount -- supply' = supply - amount -- Compute sum(balance'): -- sum(balance') = sum(balance) - amount -- Prove I(S'): sum(balance') == supply' -- sum(balance) - amount == supply - amount -- By I(S): sum(balance) = supply -- supply - amount == supply - amount -- QED by algebraic co-variance -- Note: R1 is needed for the Nat subtraction in U1 -- to be well-typed (balance[from] >= amount ensures -- the result is non-negative). I(S) together with R1 -- also implies supply >= amount (since sum(balance) -- = supply and balance[from] >= amount), making the -- supply subtraction in U2 well-typed.

Transition Atomicity

All updates within a transition execute atomically. Either all updates succeed and the post-state satisfies all invariants, or the transition aborts and the state is unchanged. There is no intermediate state visible to other transitions. This atomicity guarantee is essential for invariant preservation: the verifier reasons about the complete pre-state to post-state transformation, never about partial updates.

At the WASM level, atomicity is implemented by the target chain's transaction model. If a require clause fails or the WASM execution traps, the entire transaction is rolled back by the chain runtime. The Form compiler does not emit explicit rollback code; it relies on the host environment's transactional guarantees.

Parameter Typing

Transition parameters are not explicitly typed in the Form language. Their types are inferred from usage within the transition body. If amount appears in balance[from] -= amount where balance : Nat per Address, then amount : Nat. If from appears as a map key in balance[from] where balance : Map(Address, Nat), then from : Address.

-- Parameter type inference: transition transfer(from, to, amount) { require balance[from] >= amount balance[from] -= amount balance[to] += amount } -- from : Address (used as key in balance : Nat per Address) -- to : Address (used as key in balance : Nat per Address) -- amount : Nat (used in arithmetic with balance values : Nat)

If the compiler cannot infer a unique type for a parameter (e.g., the parameter is unused or used in ambiguous contexts), it rejects the transition with a type ambiguity diagnostic.

Specification

Overview Type System Invariant Algebra Verification Rules WASM Compilation

Form Templates

Token Vault Escrow Governor Marketplace

Resources

Formagine home API documentation Membership