Type System

The Form language uses a static type system that ensures all state fields, transition parameters, and invariant expressions are well-typed before verification begins. The type system is intentionally restricted: it admits only the types needed to express state machine properties and excludes general-purpose computation. This restriction is what makes compile-time verification decidable.

Base Types

Every value in a Form has one of six base types. Base types are the atomic building blocks from which all compound state is constructed.

Type	Description	Default
Nat	Natural numbers. Non-negative integers (0, 1, 2, ...). The primary numeric type for token amounts, counters, and quantities.	0
Int	Integers. The full range of positive, negative, and zero values. Used when negative values are semantically meaningful (e.g., signed deltas).	0
Bool	Boolean values. Either true or false. Used for flags, release states, and guard conditions.	false
Address	Chain-specific opaque address. Represents an account, contract, or externally-owned identity on the target chain. The only supported operation on Address values is equality comparison.	zero address
Bytes	Variable-length byte sequence. Used for arbitrary data payloads, hashes, and signatures.	empty (0 bytes)
String	UTF-8 text. Used for human-readable identifiers, labels, and metadata.	empty string

Parameterized Types

Parameterized types construct compound values from base types. Each parameterized type takes one or two type arguments.

Type	Description	Default
Map(K, V)	Finite mapping from keys of type K to values of type V. Accessing a key not present in the map returns the default value of V. Maps support read, write, delete, and iteration. The sum() aggregation function operates over all values of a Map(K, Nat) or Map(K, Int).	empty map
Set(T)	Unordered collection of unique values of type T. Supports membership testing, insertion, removal, and cardinality.	empty set
List(T)	Ordered sequence of values of type T. Supports indexed access, append, length, and iteration.	empty list
Option(T)	Either a value of type T (Some) or the absence of a value (None). Used for fields that may not be initialized or may be cleared.	None

Quantified State: per Address

The per keyword is syntactic sugar for declaring a mapping over a domain. Writing x : T per Address in a state declaration is equivalent to writing x : Map(Address, T). The per-Address form is preferred when each address in the system has its own independent copy of a value, such as a balance or a vote flag.

-- These two declarations are equivalent:
balance : Nat per Address
balance : Map(Address, Nat)

-- Access syntax is identical:
balance[addr]          -- reads the value for addr, or 0 if absent
balance[addr] += 10    -- updates the value for addr

The per-Address quantifier is significant for verification because it tells the compiler that sum(balance) ranges over all addresses. When the compiler encounters sum(x) where x : T per Address, it interprets the expression as the summation of x[a] for all addresses a in the domain. This interpretation is central to conservation invariant proofs.

Arithmetic Typing Rules

Arithmetic operations on Nat and Int are governed by closure rules that ensure type safety and enable the verifier to reason about numeric properties.

Nat Arithmetic

-- Addition: closed on Nat rule Nat + Nat = Nat -- Multiplication: closed on Nat rule Nat * Nat = Nat -- Subtraction: requires a precondition to remain in Nat rule a - b : Nat when a : Nat, b : Nat, a >= b -- Without the precondition, Nat subtraction is a type error. -- The compiler enforces this by requiring a 'require a >= b' -- clause before any expression 'a - b' where both are Nat.

The subtraction rule is the key constraint. Because Nat values cannot be negative, the expression a - b is only well-typed when the compiler can verify that a >= b holds at the point of subtraction. In a transition, this means a require clause must precede the subtraction. This structural requirement is what makes require balance[from] >= amount necessary in a token transfer: without it, the expression balance[from] -= amount would be a type error.

Int Arithmetic

-- All basic operations are closed on Int rule Int + Int = Int rule Int - Int = Int rule Int * Int = Int -- Mixed arithmetic: Nat is a subtype of Int rule Nat + Int = Int rule Int + Nat = Int rule Nat - Int = Int -- result may be negative

Nat is a subtype of Int. Any expression that expects an Int accepts a Nat. The converse does not hold: assigning an Int to a Nat field requires a proof that the value is non-negative.

Comparison Rules

-- Numeric comparison: full ordering on Nat and Int rule (a : Nat) < (b : Nat) : Bool rule (a : Nat) <= (b : Nat) : Bool rule (a : Nat) > (b : Nat) : Bool rule (a : Nat) >= (b : Nat) : Bool rule (a : Nat) == (b : Nat) : Bool -- Same rules apply to Int. -- Address comparison: equality only rule (a : Address) == (b : Address) : Bool rule (a : Address) != (b : Address) : Bool -- Ordering operations (<, <=, >, >=) on Address are type errors. -- Addresses are opaque identifiers with no natural ordering. -- Bool comparison: equality and logical operations rule (a : Bool) == (b : Bool) : Bool rule (a : Bool) && (b : Bool) : Bool rule (a : Bool) || (b : Bool) : Bool rule !(a : Bool) : Bool rule (a : Bool) => (b : Bool) : Bool -- implication

Map Access and Default Values

Map access uses bracket notation. When a key is not present in the map, the access expression returns the default value of the value type. This design eliminates the need for explicit existence checks and simplifies invariant proofs.

-- Map read: returns V or default(V) if key absent rule (m : Map(K, V))[k : K] : V -- Map write: sets the value for key k rule (m : Map(K, V))[k : K] = (v : V) : Map(K, V) -- Map compound assignment: sugar for read-modify-write rule (m : Map(K, Nat))[k] += (n : Nat) : Map(K, Nat) rule (m : Map(K, Nat))[k] -= (n : Nat) : Map(K, Nat) when m[k] >= n -- Default values by type: -- Nat -> 0 -- Int -> 0 -- Bool -> false -- Address -> zero address -- Bytes -> empty -- String -> empty

The default value semantics are critical for conservation proofs. When balance : Nat per Address is declared, any address not yet seen in a transition has balance 0. This means sum(balance) over all addresses is well-defined and equal to the sum of only the non-default entries. The compiler exploits this to reduce sum-preservation proofs to finite checks over the addresses modified by each transition.

The sum() Aggregation Function

The built-in sum() function computes the total of all values in a Map(K, Nat) or Map(K, Int). It is the only aggregation function in the Form language and exists specifically to express conservation invariants.

rule sum(m : Map(K, Nat)) : Nat rule sum(m : Map(K, Int)) : Int -- sum() is not defined on other types. -- sum(m) = m[k1] + m[k2] + ... + m[kn] for all keys ki in m.

The compiler does not evaluate sum() at compile time. Instead, it reasons about the algebraic properties of sum under state updates. When a transition modifies m[k] += delta, the compiler derives sum(m') = sum(m) + delta. When a transition modifies two entries m[a] -= delta and m[b] += delta, the compiler derives sum(m') = sum(m) - delta + delta = sum(m). These derivations are the foundation of all conservation proofs.

Built-in Context Values

Transitions have access to built-in context values that represent runtime information about the executing environment. These values are not part of the Form state but can appear in require clauses and assignment expressions.

Value	Type	Description
msg.sender	Address	The address of the account that invoked the current transition.
msg.value	Nat	The amount of native currency attached to the current transition invocation.
block.time	Nat	The timestamp of the current block, in seconds since epoch.
block.height	Nat	The height (sequence number) of the current block.

Context values are opaque to the verifier at compile time. The compiler cannot know the value of msg.sender or block.time in advance, so require clauses that reference context values always produce runtime WASM instructions rather than being erased. This is the mechanism by which access control and time-lock invariants survive into the deployed contract.

Specification

Overview Invariant Algebra Transition Semantics Verification Rules WASM Compilation

Form Templates

Token Vault Escrow Governor Marketplace

Resources

Formagine home API documentation Membership