Verification Rules

The compiler verifies a Form by generating proof obligations for every (transition, invariant) pair and discharging each obligation using the proof method determined by the invariant's class. If all obligations are discharged, the Form is accepted and compilation proceeds. If any obligation fails, the compiler produces a counterexample and rejects the Form. This section specifies the proof methods, the counterexample format, and provides complete verification traces for three representative forms.

Proof Methods by Invariant Class

1. Arithmetic Identity (Conservation)

For a conservation invariant sum(x) == y, the compiler substitutes the transition's updates into the invariant and simplifies algebraically. The method proceeds in three steps: extract deltas from each update, sum the deltas on both sides, and check whether the resulting equation is a tautology.

-- Method: Arithmetic Identity -- Input: transition t, invariant sum(x) == y -- -- Step 1: Extract deltas. -- For each update x[k] += d or x[k] -= d, record (k, +d) or (k, -d). -- For each update y += d or y -= d, record delta_y = +d or -d. -- If y is not modified, delta_y = 0. -- -- Step 2: Compute net delta to sum(x). -- delta_sum = sum of all individual key deltas. -- -- Step 3: Check identity. -- If delta_sum == delta_y (after algebraic simplification), -- the invariant is preserved. Otherwise, report the residual.

2. Ordering Proof (Monotonicity, State Machine)

For a monotonicity invariant x' >= x or a state machine invariant phase only advances, the compiler inspects each update to the constrained variable and verifies that the update is non-decreasing.

-- Method: Ordering Proof -- Input: transition t, invariant x' >= x -- -- For each update to x in t: -- Case x += d where d : Nat => x' = x + d >= x. QED. -- Case x = expr => prove expr >= x from -- the transition's preconditions and the pre-state. -- Case x -= d => x' = x - d. FAILS unless d == 0. -- -- If t does not modify x => x' = x >= x. QED (trivially).

3. Precondition Sufficiency (Access Control)

For an access control invariant, the compiler verifies that the required identity or temporal check appears as a require clause dominating all state mutations in the transition.

-- Method: Precondition Sufficiency -- Input: transition t, invariant (t => guard_predicate) -- -- Construct the dominator set D of the mutation block in t. -- D contains all require clauses that execute before any update. -- Check: guard_predicate is in D (syntactic match or entailment). -- -- If guard_predicate is in D, the invariant holds for t. -- If guard_predicate is NOT in D, reject with diagnostic: -- "transition 't' lacks required guard 'guard_predicate'".

4. Inductive Proof (Boundedness)

For a boundedness invariant x <= MAX, the compiler proves both the base case and the inductive step.

-- Method: Inductive Proof -- Input: transition t, invariant x <= MAX -- -- Base case (checked once, not per-transition): -- default(x) <= MAX. For Nat: 0 <= MAX. QED if MAX >= 0. -- -- Inductive step for each transition that modifies x: -- Given: x <= MAX (inductive hypothesis) -- Prove: x' <= MAX -- -- Case x = c where c <= MAX => QED. -- Case x += d with require x + d <= MAX => QED. -- Case x = f(...) => prove f(...) <= MAX using -- inductive hypothesis + preconditions.

Counterexample Generation

When a proof obligation cannot be discharged, the compiler constructs a counterexample. A counterexample consists of three components: a pre-state S that satisfies all invariants, a set of parameter values, and the resulting post-state S' where the invariant is violated.

-- Counterexample format: -- VERIFICATION FAILED -- Form: FormName -- Transition: transition_name -- Invariant: invariant_name -- -- Pre-state S (satisfies all invariants): -- field1 = value1 -- field2 = value2 -- ... -- -- Parameters: -- param1 = value1 -- param2 = value2 -- ... -- -- Post-state S' (violates invariant): -- field1 = value1' -- field2 = value2' -- ... -- -- Invariant evaluation: -- invariant_expr = false_value -- Expected: true

The counterexample is minimal: the compiler searches for the smallest state and parameter values that demonstrate the violation. For numeric types, it starts from the default values and increments. For addresses, it uses symbolic placeholder addresses. The goal is to produce the most readable counterexample that immediately shows why the invariant fails.

Example Counterexample

Consider a broken Token form where the mint transition increments the balance but forgets to increment the supply.

transition mint(to, amount) {
  require msg.sender == owner
  balance[to] += amount
  -- BUG: supply += amount is missing
}

-- VERIFICATION FAILED -- Form: Token -- Transition: mint -- Invariant: conservation (sum(balance) == supply) -- -- Pre-state S: -- balance = { addr_0: 0 } -- supply = 0 -- owner = addr_1 -- -- Parameters: -- to = addr_0 -- amount = 1 -- msg.sender = addr_1 (== owner, so require passes) -- -- Post-state S': -- balance = { addr_0: 1 } -- supply = 0 -- -- Invariant evaluation: -- sum(balance) = 1 -- supply = 0 -- sum(balance) == supply => 1 == 0 => false -- -- Delta analysis: -- sum(balance) changed by +1 -- supply changed by 0 -- Residual: +1 (sum increased without corresponding supply increase)

Verification Trace: Token (Conservation)

The following is the complete verification trace for the Token form. The Token form has 3 transitions and 1 invariant, producing 3 proof obligations.

Form: Token

-- State: balance : Nat per Address, supply : Nat, owner : Address -- Invariant: conservation : sum(balance) == supply -- Transitions: transfer, mint, burn -- Proof obligations: 3

Obligation 1 of 3: transfer x conservation

-- Method: Arithmetic Identity -- -- Updates: -- balance[from] -= amount => delta(from) = -amount -- balance[to] += amount => delta(to) = +amount -- supply unchanged => delta_y = 0 -- -- delta_sum = -amount + amount = 0 -- delta_y = 0 -- Check: 0 == 0 -- -- Result: PROVEN by arithmetic identity.

Obligation 2 of 3: mint x conservation

-- Method: Arithmetic Identity -- -- Updates: -- balance[to] += amount => delta(to) = +amount -- supply += amount => delta_y = +amount -- -- delta_sum = +amount -- delta_y = +amount -- Check: +amount == +amount -- -- Result: PROVEN by arithmetic co-variance.

Obligation 3 of 3: burn x conservation

-- Method: Arithmetic Identity -- -- Updates: -- balance[from] -= amount => delta(from) = -amount -- supply -= amount => delta_y = -amount -- -- delta_sum = -amount -- delta_y = -amount -- Check: -amount == -amount -- -- Result: PROVEN by arithmetic co-variance.

-- Token verification complete. -- 3 of 3 obligations proven. -- Conservation invariant holds for all transitions. -- Invariant erased from WASM output.

Verification Trace: Vault (Conservation + Time-Lock)

The following is the complete verification trace for the Vault form. The Vault form has 2 transitions and 2 invariants, producing 4 proof obligations.

Form: Vault

-- State: deposited : Nat per Address, total : Nat, -- lock_until : Nat per Address -- Invariants: -- conservation : sum(deposited) == total -- time_lock : withdraw => block.time >= lock_until[msg.sender] -- Transitions: deposit, withdraw -- Proof obligations: 4

Obligation 1 of 4: deposit x conservation

-- Method: Arithmetic Identity -- -- Updates: -- deposited[msg.sender] += amount => delta(sender) = +amount -- total += amount => delta_y = +amount -- -- delta_sum = +amount -- delta_y = +amount -- Check: +amount == +amount -- -- Result: PROVEN by arithmetic co-variance.

Obligation 2 of 4: deposit x time_lock

-- Method: Precondition Sufficiency -- -- The time_lock invariant constrains the withdraw transition only. -- The deposit transition is not withdraw, so the implication -- (withdraw => guard) is vacuously true for deposit. -- -- Result: PROVEN (vacuously; deposit is not the guarded transition).

Obligation 3 of 4: withdraw x conservation

-- Method: Arithmetic Identity -- -- Updates: -- deposited[msg.sender] -= amount => delta(sender) = -amount -- total -= amount => delta_y = -amount -- -- delta_sum = -amount -- delta_y = -amount -- Check: -amount == -amount -- -- Result: PROVEN by arithmetic co-variance.

Obligation 4 of 4: withdraw x time_lock

-- Method: Precondition Sufficiency -- -- The time_lock invariant requires: -- withdraw => block.time >= lock_until[msg.sender] -- -- The withdraw transition contains: -- require block.time >= lock_until[msg.sender] -- -- This require clause is in the dominator set of the mutation block. -- The guard predicate matches the invariant predicate exactly. -- -- Result: PROVEN by precondition sufficiency. -- Note: this require clause compiles to a runtime WASM check -- because block.time is a runtime context value.

-- Vault verification complete. -- 4 of 4 obligations proven. -- Conservation invariant erased from WASM output. -- Time-lock require retained as runtime WASM instruction.

Verification Trace: Escrow (Single-Release)

The following is the complete verification trace for the Escrow form. The Escrow form has 2 transitions and 1 invariant, producing 2 proof obligations. The single-release invariant combines implication logic with state machine reasoning.

Form: Escrow

-- State: amount : Nat, depositor : Address, beneficiary : Address, -- arbiter : Address, released : Bool, deadline : Nat -- Invariant: single_release : released => amount == 0 -- Transitions: release, refund -- Proof obligations: 2

Obligation 1 of 2: release x single_release

-- Method: Combined (Precondition + State Machine) -- -- The invariant is an implication: released => amount == 0 -- We must show: if released => amount == 0 holds in S, -- then released' => amount' == 0 holds in S'. -- -- Transition release() updates: -- require msg.sender == arbiter [R1] -- require !released [R2] -- send(beneficiary, amount) [side effect] -- amount = 0 [U1] -- released = true [U2] -- -- Post-state: -- released' = true -- amount' = 0 -- -- Evaluate invariant in S': -- released' => amount' == 0 -- true => 0 == 0 -- true => true -- true -- -- Result: PROVEN. -- The transition sets amount = 0 before setting released = true. -- The consequent is established before the antecedent becomes true. -- The require !released guard (R2) prevents re-entry once -- released is true, so the transition cannot execute again.

Obligation 2 of 2: refund x single_release

-- Method: Combined (Precondition + State Machine) -- -- Transition refund() updates: -- require block.time >= deadline [R1] -- require !released [R2] -- send(depositor, amount) [side effect] -- amount = 0 [U1] -- released = true [U2] -- -- Post-state: -- released' = true -- amount' = 0 -- -- Evaluate invariant in S': -- released' => amount' == 0 -- true => 0 == 0 -- true => true -- true -- -- Result: PROVEN. -- Identical structure to release: amount zeroed before released set. -- The require !released guard prevents re-entry. -- The deadline guard (R1) compiles to a runtime WASM check.

-- Escrow verification complete. -- 2 of 2 obligations proven. -- Single-release invariant erased from WASM output. -- Runtime checks retained: msg.sender == arbiter (release), -- block.time >= deadline (refund), !released (both).

Verification Completeness

The verification system is sound and complete for the restricted expression language of Forms. Soundness means that if the compiler accepts a Form, all invariants genuinely hold for all reachable states. Completeness means that if all invariants genuinely hold, the compiler will accept the Form. These properties follow from the decidability of the algebraic proof methods over the finite set of invariant classes and the restricted type system.

Soundness is the critical guarantee. It means that a compiled Form cannot violate its declared invariants through any sequence of transitions, regardless of parameter values, caller identities, or execution ordering. The compiler has examined every possible (transition, invariant) pair and proven each one. There is no execution path that escapes the proof.

Completeness means there are no false rejections for well-formed Forms within the supported invariant classes. If a Form genuinely preserves its invariants but the compiler rejects it, there is a bug in the compiler, not in the Form. In practice, the most common source of apparent false rejections is an invariant that requires reasoning outside the supported classes (e.g., a non-linear arithmetic relationship). Such invariants are outside the language's expressible set and should be decomposed into supported classes.

Specification

Overview Type System Invariant Algebra Transition Semantics WASM Compilation

Form Templates

Token Vault Escrow Governor Marketplace

Resources

Formagine home API documentation Membership