Ora v0.2: Sum Types, Honest Verification, and a Real Trait Surface

v0.2 lands three things that matter together: a real algebraic-data-type surface (enum payloads, Result<T, E>, unified pattern matching), an SMT verifier that fails closed where it used to fail silently (--explain cores, vacuity detection, datatype encoding for products and error unions), and the first slice of a static-dispatch trait system (impl conformance, bounded generics, extern trait for ABI-correct external calls). Underneath them: bounded loop unrolling and ADT-aware comptime, an LSP that reflects the new surface, and a debugger DAP server.

This post walks through what's in the box, with code that compiles today.

---

ADTs and Result, end-to-end

Until v0.2, Ora had error unions (!T | E) but no general sum types. Enums were tag-only. Pattern matching existed but didn't unify across the type families. v0.2 finishes that story.

error Failure(code: u256);

pub fn classify(flag: bool, value: u256) -> u256 {
    let outcome = checked_value(flag, value);
    return match (outcome) {
        Ok(inner)     => inner,
        Failure(code) => code,
    };
}

Result<T, E> is now a first-class type with constructors, public-ABI lowering, multi-error matching, named-error matching, payload-error decoding for extern calls, and dynamic-payload propagation. It's not a stdlib trick — it's a real algebraic data type backed by an !ora.adt IR node, with proper carrier layout (tag at offset 0, payload at offset 32, narrow vs wide encoding chosen by width), and per-variant SMT datatype constructors for the verifier.

Pattern matching unifies the surface:

match (deposit_result(amount)) {
    Ok(receipt)              => log Confirmed(receipt),
    InsufficientBalance(req) => return error.InsufficientBalance(req, available),
    Paused                   => return error.Paused,
}

Notes on the implementation:

• Sum-match exhaustiveness is unified. The same algorithm checks enum, error-union, and Result matches, and warns when a wildcard _ arm covers named variants the developer should have listed. The duplicate exhaustiveness implementation that lived in HIR is gone — sema is the authority.
• Recursive runtime ADTs are rejected. A struct or enum that recursively contains itself by value (not behind a slice<_> or map<_, _> indirection) is a compile error. This catches the unbounded-layout mistake at the type level.
• Anonymous struct identity is preserved. Two anonymous structs with the same fields in different orders are distinct types — the dialect type carries an ordered field-name list and an ordered field-type list, and field reordering produces a different MLIR type.
• Comptime parity. Constructors, payload extraction, and matching all work at comptime. match over a comptime-known Result evaluates at compile time and folds away.

Failure cases stop being scattered revert calls and become values you match on, which the verifier can reason about, the ABI can decode, and the debugger can step through.

The verifier got honest

The bigger story is what the verifier no longer lies about.

Before v0.2, several SMT encoding paths used opaque bv256 fallbacks when type metadata was missing. The fallback is sound in isolation — Z3 reasoning over an opaque 256-bit symbol is sound — but it silently weakened proofs whenever the encoder didn't have exact product/struct/error metadata. The verifier could come back with a green checkmark on a contract whose underlying SMT model never actually reasoned about the relevant structure.

v0.2 retires those paths:

• Products use exact datatype metadata. Named structs, anonymous structs, and tuples lower to per-sort SMT datatypes with named field accessors. When the metadata is missing, the encoder calls recordDegradation and the verifier-level gate trips, returning EncodingDegraded instead of a proof.
• Enums migrated to SMT datatypes. Tag-only enums use a real datatype constructor per variant, not a global UF.
• Error unions lower to per-error constructors. Each error variant gets its own constructor; discriminant recovery uses the canonical accessor. Multi-error try-propagation, named error payload roundtrip, and wide error-union catch propagation each have regressions.
• Width discipline tightened across the encoder. Signed/unsigned coercions, bitvector narrowing, mixed-width comparisons, and sequence-length-to-BV all require explicit sound coercion paths now. The encoder fails closed on width unknowns instead of guessing.
• UNKNOWN fails closed. A Z3_L_UNDEF return is no longer treated as success — it surfaces as an Unknown verifier error. Same for mid-proof degradation: if the encoder degrades after query preparation, the pass aborts with EncodingDegraded rather than reporting the obligations as proved.

Explain mode, unsat cores, and vacuity

When a proof fails, you want to know why:

ora build --explain

This routes verification through a tracked-assumption pipeline. Each obligation is solved against a set of named assumption proxies — user requires, environment and frame assumptions, callee obligations and ensures (with imported-callee provenance preserved), ghost axioms, and path guards. When a proof goes through, the unsat core is computed and reported, optionally minimized, with each contributing assumption tagged by source. Build artifacts include both a JSON and a markdown report; the JSON contains raw Z3 proof strings when --proofs is enabled, the markdown stays readable.

This matters most when proofs don't go through. The counterexample tells you a state where the obligation fails; the unsat core tells you which assumptions a successful proof relied on. Both views, side by side.

Closely related: a contract whose requires clauses are mutually contradictory used to pass verification with green checkmarks, because every obligation under contradictory premises is trivially provable. v0.2 detects this — --explain checks the assumption set for satisfiability before solving, reports vacuous obligations as PreconditionViolation, and fails closed if the consistency check itself returns UNDEF. Inconsistent ghost axioms are caught the same way, jointly.

The principle is the same throughout: if the verifier can't reason precisely about your code, it tells you.

Traits — the static slice

Ora now has traits. The slice that landed in v0.2 is intentionally narrow: static dispatch, comptime-resolvable, no runtime polymorphism. No dyn Trait, no vtables, no trait objects.

What works today:

trait Ledger {
    fn balance_of(self, account: address) -> u256;
    fn transfer(self, from: address, to: address, amount: u256) -> bool
        requires(amount > 0);
}

impl Ledger for Vault {
    fn balance_of(self, account: address) -> u256 {
        return self.balances[account];
    }
    fn transfer(self, from: address, to: address, amount: u256) -> bool {
        // ...
    }
}

Receivers in Ora are written as self — there's no &mut self distinction. Mutability is conferred by what the impl actually does to its own storage; the trait signature just declares the receiver shape.

• Trait declaration with method signatures, optional ghost blocks, and verification clauses.
• Impl conformance checking — missing methods, extra methods, signature mismatches, duplicate impls (within a module and across visible imported modules) are all reported.
• Trait bounds on generic functions (fn f<T: Ledger>(...)) — calls to bound methods resolve through the impl table at the call site.
• Ghost facts attached to trait methods are inherited by impl methods, with parameter-pattern aliasing so the proof obligations rewrite cleanly.

extern trait for external contracts

The other half is calling other contracts:

extern trait ERC20 {
    call fn transfer(self, to: address, amount: u256) -> bool
        errors(InsufficientBalance, InvalidRecipient);
    staticcall fn balanceOf(self, owner: address) -> u256;
    staticcall fn totalSupply(self) -> u256;
}

pub fn pay(token: address, recipient: address, amount: u256)
    -> !bool | InsufficientBalance | InvalidRecipient | TransferFailed | ExternalCallFailed
{
    return external<ERC20>(token, gas: 50000).transfer(recipient, amount);
}

extern trait declares a Solidity-compatible interface. Each method is annotated call (state-changing) or staticcall (read-only), with explicit errors(...) declaring the closed set of payload-bearing errors the callee may revert with. The compiler computes the canonical 4-byte selector by keccak-hashing the canonical signature, encodes arguments through the ABI layer, emits a CALL or STATICCALL with mandatory gas:, decodes the return value, and dispatches reverts through the declared error set.

transfer(address,uint256) produces selector 0xa9059cbb — the same selector Solidity would produce.

The trait surface is enough to write libraries that depend on conformance and to talk to other contracts safely. It is not yet a full type-class system — see the gaps section at the end for what's deferred.

Comptime expanded

The comptime evaluator got broader. New in v0.2:

• Bounded runtime loop unrolling. Constant for loops and bounded while loops get unrolled into straight-line code when the bounds are comptime-known, with provenance preserved so the debugger can show the inlined chain.
• Comptime nested struct field updates. let s = .{ .inner = .{ .field = ... } } with deep updates now folds.
• Comptime ADT matching. match on a comptime-constructed Result evaluates at compile time.
• Comptime payload persistence. Constructed payloads survive across comptime evaluation steps — you can build a value in one comptime block and match it in another.
• Trait-associated comptime methods. A trait method declared comptime fn is callable at comptime through a generic constraint and resolves to the impl's comptime body.
• Limit diagnostics. Comptime budget exhaustion produces a clear error, not a silent fallback.

The pattern is familiar: more code can be folded, fewer guards survive into runtime, fewer branches in the bytecode. Auditors see less surface area.

Tooling: LSP and debugger

The editor surface caught up with the language. v0.2's LSP (ora lsp) now knows about traits, impls, type aliases, ADT variant payloads, match, and the new verification clauses (modifies, decreases, increases):

• Symbol index collects trait, impl, and type declarations alongside contracts/structs/enums; trait method signatures render with self, parameters, return type, errors(...), and verification clauses; enum variant detail includes payload shape and explicit discriminant value.
• Hover signatures distinguish trait declarations from impls; an impl Token for Vault hovers as the impl with selection range on the trait name.
• Completion suggests match, type, tstore, init, modifies/decreases/increases, primitive types (u8 through u256, i8 through i256, bool, address, bytes, string, map, slice), and extern-trait keywords (call, staticcall, errors).
• Frontend diagnostics plumb sema resolution errors through to the editor — previously only typecheck diagnostics flowed through, so things like "undefined name 'result' in requires" only surfaced at build time.
• Semantic tokens classify match, Modifies/Decreases/Increases, Call/Staticcall/Errors correctly so themes light them up the same way as their classical counterparts.

The debugger (blog post) gained a DAP server in v0.2:

ora debug --dap

Implements initialize, launch, setBreakpoints, setExceptionBreakpoints, threads, stackTrace, scopes, variables, evaluate, continue, next, stepIn, stepOut, pause, disconnect. The TUI keeps its compiler-aware overlays — folded values, hoist origins, gas heatmap, coverage, and FV-proven dead branches dimmed via the verifier's proven_guard_positions sidecar. New since the original debugger post: storage watchpoints (:watch <slot>), conditional breakpoints (:break <line> when <expr>), ABI revert/event decoding, EIP-3155 trace export, and a session-replay determinism pin (SessionSeed.BlockEnv fixes timestamp/blockhash/coinbase/etc., so two replays of a contract reading block opcodes produce byte-identical traces).

DAP support is partial — scopes/variables aren't fully implemented and VS Code packaging isn't shipped. Both land in v0.3.

Putting it together

A pool contract that uses most of v0.2's surface lives at ora-example/dex/swap_pool.ora. It's a fixed-rate swap pool with internal balance accounting, multi-error returns, refinement-typed parameters, ghost state, and a verified pure helper. ora build produces bytecode + source map + SMT report.

The pure quote helper:

fn quote(in_amount: u256) -> !u256 | PriceOverflow
    requires(price_b_per_a > 0)
{
    if (in_amount > std.constants.U256_MAX / price_b_per_a) {
        return PriceOverflow;
    }
    return in_amount * price_b_per_a;
}

The swap function calling it via try:

pub fn swap_a_for_b(in_amount: NonZero<u256>, min_out: u256)
    -> !u256 | InsufficientLiquidity | InsufficientInput | InsufficientBalance | SlippageExceeded | PriceOverflow
    requires(price_b_per_a > 0)
    requires(reserve_a <= std.constants.U256_MAX - in_amount)
{
    let sender: NonZeroAddress = std.msg.sender();
    let user_a: u256 = balance_a[sender];
    if (user_a < in_amount) {
        return InsufficientBalance(in_amount, user_a);
    }
    if (reserve_b == 0) {
        return InsufficientLiquidity(in_amount, 0);
    }

    let out_amount: u256 = try quote(in_amount);

    if (out_amount == 0)        { return InsufficientInput; }
    if (out_amount > reserve_b) { return InsufficientLiquidity(out_amount, reserve_b); }
    if (out_amount < min_out)   { return SlippageExceeded(out_amount, min_out); }
    if (balance_b[sender] > std.constants.U256_MAX - out_amount) {
        return InsufficientLiquidity(out_amount, reserve_b);
    }

    balance_a[sender] = user_a - in_amount;
    balance_b[sender] += out_amount;
    reserve_a += in_amount;
    reserve_b -= out_amount;

    log Swap(sender, in_amount, out_amount, true);
    return out_amount;
}

Failure cases are values, not exceptions. Multi-error return tells the caller the closed set of variants they may receive. try propagates the inner error union. Refinement types (NonZero<u256>, NonZeroAddress) catch the "amount > 0 / sender ≠ 0" preconditions at the type level. The verifier proves every checked-arithmetic obligation in the function — no UNKNOWNs, no degradation. If you change a precondition and break a proof, the build tells you exactly which obligation failed and which assumptions a successful proof would have leaned on.

That's the v0.2 story. Sum types as values. A verifier that says "I don't know" instead of "looks good" when the encoding gets shaky. Traits enough to write libraries and call other contracts safely. Comptime that handles ADTs and bounded loops. An LSP and debugger that reflect all of it.

Gaps — closing in v0.3

Traits:

• No default trait methods. A trait method body is a parse error.
• No supertraits, no associated types. Both deferred.
• No runtime polymorphism, no trait objects. Every trait-bound generic call resolves to a concrete impl symbol at compile time.
• Extern trait parameter ABI is limited to primitives + bytes/string + arrays/slices in v0.2's first cut. Tuple, named-struct, and enum parameters land in v0.3.
• Cross-module duplicate impl detection uses simple-name keys. Two modules with impl Trait for Box where Box actually refers to different nominal types would be falsely flagged.

Verification:

• SMT verification of external call return types is not yet wired. Lowering is end-to-end; the SMT encoder treats the return value as opaque.
• Vacuity detection runs only with --explain. A vacuous contract built without --explain still passes today.
• Constant-product AMM math is at the edge of Z3's nonlinear arithmetic — proofs work but can time out across many obligations. Use stored-rate or fixed-ratio pricing if you want full verification today.

Surface:

• Result stdlib helpers are minimal. is_ok, is_err, unwrap_or only — no map/and_then/or_else yet.

Tooling:

• Debugger DAP scopes/variables are partial; VS Code packaging isn't shipped.

v0.3 closes most of these. Tracking lives in the repo at memory/v0.2-review.md and the v0.3 milestone.

---

v0.2 ships from the v0.2 branch. Try it: clone the repo, zig build install, then ora build ora-example/dex/swap_pool.ora for the example above. Feedback and bug reports welcome on GitHub.