WASM Compilation

Phase 2: Erasure

Erasure is the compilation phase that makes Form verification economically useful. Every invariant that was proven at compile time produces zero WASM instructions. The proof is a compile-time artifact; it does not appear in the deployed binary. This means that a Form with ten invariants, all proven, produces the same WASM as a Form with zero invariants and the same transitions.

The erasure rule is precise: a code fragment is erased if and only if it exists solely to enforce an invariant that was fully proven at compile time. The three categories of erasable and non-erasable code are as follows.

The distinction between erased and retained code is determined by analyzing each require clause's dependencies. If a require clause references only state variables whose values are known to satisfy the condition (because the invariant was proven), it is erased. If a require clause references any runtime context value or serves as a type guard for a Nat subtraction, it is retained.

Erasure Example: Token Transfer

In the Token form's transfer transition, the conservation invariant is proven by arithmetic identity. The invariant itself and any assertion of sum(balance) == supply are erased. The require balance[from] >= amount clause is retained because it serves as a type guard for the Nat subtraction balance[from] -= amount.

Erasure Example: Token Mint

Phase 3: Target Adaptation

Target adaptation emits the chain-specific wrapper around the lowered and erased WASM core. Each target chain has different requirements for entry points, message encoding, and storage APIs. The Form compiler supports four targets.

CosmWasm

CosmWasm requires four exported functions: instantiate, execute, query, and migrate. Each Form transition becomes a variant of the execute message. The compiler emits JSON schema-compatible message definitions. Storage uses the CosmWasm db_read and db_write host imports. Entry points receive a JSON-encoded message, and the compiler emits a minimal JSON parser for the message discriminant. See CosmWasm target details.

Near

Near Protocol exports each transition as a named function. Parameters are received as a JSON argument to the exported function. Storage uses storage_read and storage_write host imports with byte-array keys. The compiler emits borsh or JSON serialization depending on the method's annotation. See Near target details.

Stylus (Arbitrum)

Stylus uses Solidity-compatible ABI encoding. Each transition becomes a function selector (the first 4 bytes of the keccak256 hash of the function signature). Parameters are ABI-encoded in the calldata. Storage uses EVM-compatible sload and sstore host calls with 256-bit slots. The compiler emits Solidity ABI metadata for compatibility with existing tooling. See Stylus target details.

Polkadot (ink!)

Polkadot ink! contracts export a call and deploy function. The message discriminant is a 4-byte selector derived from the method name. Parameters use SCALE encoding. Storage uses the Substrate storage host functions. The compiler emits ink! metadata for the contract registry. See Polkadot target details.

Annotated WASM: Token Transfer (CosmWasm)

The following is an approximate WAT (WebAssembly Text Format) representation of the compiled Token transfer transition targeting CosmWasm. Each instruction group is annotated with its origin: whether it comes from a require clause, a state update, or the chain ABI.

;; Token transfer — CosmWasm target
;; Source:
;;   transition transfer(from, to, amount) {
;;     require balance[from] >= amount
;;     balance[from] -= amount
;;     balance[to]   += amount
;;   }
;;
;; conservation invariant: ERASED (proven at compile time)

(func $execute_transfer
  (param $msg_ptr i32) (param $msg_len i32)
  (result i32)

  ;; --- CHAIN ABI: decode JSON message ---
  ;; Parse "from", "to", "amount" from JSON payload.
  (local $from_ptr i32)
  (local $to_ptr i32)
  (local $amount i64)
  (call $json_decode_transfer
    (local.get $msg_ptr)
    (local.get $msg_len))
  ;; Results stored in locals.

  ;; --- REQUIRE: balance[from] >= amount ---
  ;; Origin: require clause (type guard, retained)
  (call $storage_read                ;; read balance[from]
    (call $make_key
      (i32.const 0)                  ;; field_index = 0 (balance)
      (local.get $from_ptr)))
  (local.set $bal_from)
  (i64.lt_u                          ;; balance[from] < amount?
    (local.get $bal_from)
    (local.get $amount))
  (if (then
    (call $abort)                   ;; abort: insufficient balance
    (unreachable)))

  ;; --- UPDATE: balance[from] -= amount ---
  ;; Origin: state update (retained)
  (call $storage_write
    (call $make_key
      (i32.const 0)
      (local.get $from_ptr))
    (i64.sub
      (local.get $bal_from)
      (local.get $amount)))

  ;; --- UPDATE: balance[to] += amount ---
  ;; Origin: state update (retained)
  (call $storage_read                ;; read balance[to]
    (call $make_key
      (i32.const 0)
      (local.get $to_ptr)))
  (local.set $bal_to)
  (call $storage_write
    (call $make_key
      (i32.const 0)
      (local.get $to_ptr))
    (i64.add
      (local.get $bal_to)
      (local.get $amount)))

  ;; --- CHAIN ABI: return success response ---
  (call $make_response (i32.const 0))
)

The annotations show the three sources of WASM instructions in the compiled output. Instructions from the chain ABI (JSON decoding, response encoding) exist because the CosmWasm runtime requires them. Instructions from the require clause exist because the balance check is a type guard that prevents Nat underflow. Instructions from state updates exist because they implement the actual state mutation. No instructions exist for the conservation invariant, because it was proven and erased.

Binary Size Impact of Erasure

Erasure directly reduces the compiled binary size. A Form with a conservation invariant that would require a runtime sum(balance) == supply check on every transition would need to iterate over all storage entries, compute the aggregate, and compare. This operation is O(n) in the number of addresses and would add significant code and gas cost. Erasure eliminates this entirely.

The size savings depend on the invariant class. Conservation invariants, which would require aggregation loops, produce the largest savings. Monotonicity invariants, which would require a single comparison, produce smaller but still meaningful savings. Access control invariants are never erased (they depend on runtime values), so they contribute no size savings.

Annotated WASM: Token Mint (CosmWasm)

The mint transition demonstrates how an access control require clause is retained while the conservation invariant is erased.

;; Token mint — CosmWasm target
;; conservation invariant: ERASED
;; access control (msg.sender == owner): RETAINED

(func $execute_mint
  (param $msg_ptr i32) (param $msg_len i32)
  (result i32)

  ;; --- CHAIN ABI: decode ---
  (local $to_ptr i32)
  (local $amount i64)
  (call $json_decode_mint
    (local.get $msg_ptr)
    (local.get $msg_len))

  ;; --- REQUIRE: msg.sender == owner ---
  ;; Origin: access control (runtime context, retained)
  (call $get_sender)                 ;; push sender address
  (i32.load (i32.const 8))           ;; load owner from memory offset 8
  (call $addr_eq)                    ;; compare addresses
  (i32.eqz)
  (if (then
    (call $abort)                   ;; abort: unauthorized
    (unreachable)))

  ;; --- UPDATE: balance[to] += amount ---
  (call $storage_read
    (call $make_key
      (i32.const 0) (local.get $to_ptr)))
  (local.set $bal_to)
  (call $storage_write
    (call $make_key
      (i32.const 0) (local.get $to_ptr))
    (i64.add (local.get $bal_to) (local.get $amount)))

  ;; --- UPDATE: supply += amount ---
  (i64.load (i32.const 0))           ;; load supply from memory offset 0
  (i64.add (local.get $amount))
  (i64.store (i32.const 0))          ;; store updated supply

  ;; --- CHAIN ABI: return success ---
  (call $make_response (i32.const 0))
)

The msg.sender == owner check compiles to a runtime comparison and conditional abort. The conservation invariant, proven by showing that the balance increment and supply increment are equal, produces no instructions at all. The balance and supply updates are the minimum necessary code to implement the state mutation.

Host Imports

The compiled WASM module imports host functions from the target chain's runtime environment. These imports are the interface between the Form's verified logic and the chain's infrastructure. The compiler emits the correct import declarations for the selected target.

Compilation Guarantees

The three-phase compilation pipeline provides the following guarantees for the emitted WASM binary.

Correctness. Every invariant declared in the Form holds for all reachable states of the compiled contract. This follows from the verification phase (which precedes compilation) and the fact that lowering and target adaptation are semantics-preserving transformations.

Minimality. No WASM instruction exists for any property that was proven at compile time. The binary contains only the code needed to implement transitions (state reads, writes, arithmetic) and the runtime checks that cannot be statically discharged.

Determinism. The same Form definition with the same target chain always produces the identical WASM binary. There is no randomness or non-determinism in the compilation pipeline. This is important for reproducible builds and on-chain verification of deployed bytecode.

Target fidelity. The emitted WASM conforms to the target chain's ABI, entry point conventions, and storage API. A CosmWasm binary produced by the compiler is indistinguishable (at the ABI level) from a hand-written CosmWasm contract. It can be uploaded, instantiated, and queried using standard CosmWasm tooling.

Specification

Target Chains

Form Templates

Resources