Contracts and state invariants

Gale can verify arithmetic properties and state invariants during compilation. Write the property in Gale; the compiler emits F* and runs its Z3-backed verifier. You do not write F* code or a separate model of your implementation.

Named type invariants

A verified state type has a representation and a Boolean predicate:

pub opaque type State = { reserved: Integer, capacity: Integer }
invariant state {
  state.reserved >= 0 and state.reserved <= state.capacity
}

Within its module, the representation remains available for calculations. Functions use ordinary fn syntax. The invariant automatically selects functions whose signatures or local construction involve State, including nested types and annotations. The verifier checks that values constructed as State satisfy the predicate. It assumes that arguments of type State already satisfy it, then proves each transition preserves it. Outside the module, ordinary opacity prevents record literals and updates from manufacturing a State.

Opacity is optional. A transparent type alias can carry the same invariant:

pub type State = { reserved: Integer, capacity: Integer }
invariant state {
  state.reserved >= 0 and state.reserved <= state.capacity
}

pub fn empty(capacity: Integer) -> State
requires { capacity >= 0 } { { reserved: 0, capacity: capacity } }

Other modules and dependencies can read, construct, and update this record. Whenever a value is required to have type State, the verifier checks its invariant, including function arguments, results, and local annotations. A raw temporary record may be invalid while a calculation is in progress; passing it as State must establish validity again. Generic aliases and aliases of existing sum types use the same checks.

A struct can declare its invariant directly after its fields:

module reservation_state
struct { reserved: Integer, capacity: Integer }
invariant state {
  state.reserved >= 0 and state.reserved <= state.capacity
}

pub fn empty(capacity: Integer) -> ReservationState
requires { capacity >= 0 } {
  ReservationState { reserved: 0, capacity: capacity }
}

Every struct construction and update must establish its invariant, including unused values and operations through a type alias. Defaults contribute to the check when used by a constructor. These checks also apply in dependencies and inside effectful functions. The emitted value remains an ordinary Elixir struct; the invariant adds no runtime wrapper or assertion. Within its predicate, the bound value exposes the declared fields without assuming its own invariant.

A sum type can also declare its own invariant:

pub type Tree = Leaf(Integer) | Branch(Tree, Tree)
invariant value {
  match value {
    Leaf(count) -> count >= 0
    Branch(_, _) -> true
  }
}

pub fn total(value: Tree) -> Integer
ensures result { result >= 0 } {
  match value {
    Leaf(count) -> count
    Branch(left, right) -> total(left) + total(right)
  }
}

Every constructed Leaf must have a nonnegative count. A Branch retains the validity of both children, so recursive descent can use their invariants. This also works for children stored in supported lists, tuples, records, Option, maps, disjoint native unions, and user-defined generic containers, including containers passed from another function. The invariant checks the unvalidated representation of the sum without assuming its own conclusion. The runtime representation remains native tagged tuples.

Map keys and values retain their declared invariants. A branch may also constrain the map itself:

pub type Tree = Leaf(Integer) | Branch(Map<Integer, Tree>)
invariant value {
  match value {
    Leaf(count) -> count >= 0
    Branch(children) -> map_size(children) <= 2
  }
}

pub fn attach(children: Map<Integer, Tree>) -> Tree
requires { map_size(children) <= 2 } { Branch(children) }

The input type supplies valid children, while the requirement supplies the size bound. An ordinary extern returning Map<Integer, Tree> supplies the declared payload invariant; it supplies a size bound only if its contract states one. These checks preserve native maps and do not replace the foreign implementation.

Mutually recursive sums preserve the same guarantees:

pub type Tree = Leaf(Integer) | Branch(Forest)
invariant value {
  match value { Leaf(count) -> count >= 0 Branch(_) -> true }
}
pub type Forest = Empty | More(Tree, Forest)

pub fn total(value: Tree) -> Integer
ensures result { result >= 0 } {
  match value { Leaf(count) -> count Branch(children) -> sum(children) }
}
fn sum(values: Forest) -> Integer
ensures result { result >= 0 } {
  match values { Empty -> 0 More(child, rest) -> total(child) + sum(rest) }
}

Forest needs no modifier to retain the validity of its Tree fields. It can declare an additional invariant of its own. These types may be generic, live in different modules, or come from a dependency. Neither predicate assumes the validity it is defining, and every constructed member must establish its typed children’s invariants as well as its own property.

These cycles can also pass through aliases and structs with their own invariants:

pub type Tree = Leaf(Integer) | Branch(Children)
invariant value {
  match value { Leaf(count) -> count >= 0 Branch(_) -> true }
}
pub type Children = List<Tree>
invariant values { builtin.length(values) <= 2 }

pub fn attach(children: List<Tree>) -> Tree
requires { builtin.length(children) <= 2 } { Branch(children) }

Here every leaf has a nonnegative count and every branch has at most two valid children. A record alias or struct can instead hold both the children and a count, with an invariant equating that count to their length. Construction and updates must establish both properties; projecting the children retains their invariants. Transparent and represented opaque aliases, alias chains, generic types, and dependencies follow the same rules.

A recursive struct does not need a sum constructor:

module tree_state
struct { children: List<TreeState>, count: Integer }
invariant value { builtin.length(value.children) == value.count }

pub fn create(children: List<TreeState>) -> TreeState {
  TreeState { children: children, count: builtin.length(children) }
}

Every child has the same guarantee as its parent. Structs can recurse through record or list aliases with additional invariants, and can use function contracts without declaring a type invariant. Their runtime representation remains a native struct. Cycles made entirely of aliases are rejected by the language’s type checker; use a nominal struct or sum type as the recursive definition. More general recursive dependencies between types and predicates remain open. An unsupported translation fails compilation rather than silently assuming the invariant.

The invariant also applies inside supported tuples, lists, structs, Option, Result, and nonrecursive user variants. This includes already-created containers: using an existing Option<Record> as Option<State> must establish the invariant for its payload. Error payloads receive the same checks as success payloads. A constructor returning Result<State, Error> can reject invalid input explicitly and construct a valid state on its successful branch. Recursive generic variants can also carry invariant-bearing payloads: constructing a Tree<State> checks each constructed State. Existing recursive containers can also move between supported instances, such as Tree<Integer> and Tree<State>, when the verifier can establish every payload invariant. Invalid nested payloads fail verification before Elixir is emitted.

This arrangement fits an ordinary GenServer: use the invariant-bearing type as the State parameter of its behaviour, create it in init, and call verified transitions from callbacks. The callback’s return type enforces that its next state still has that type. See the complete example.

The same rules apply to a raw process: give its recursive loop the state type and handle a typed message union. Importing the state from another module or dependency still selects those functions for verification. The bounded-job example uses the same transitions in job_process and job_server; it checks capacity, attempt-ID allocation, exact outcome accounting, and unchanged state for stale reports. Initialization, dispatch continuations, and the copied state-bearing OTP defaults also enter the proof. Runtime tests separately exercise both hosts and a system code change. A worker report is an ordinary typed claim, not proof of who sent it or whether the job executed.

Function contracts

A public or private function may require a property of its arguments. Every Gale caller must establish that property, including callers in dependencies. A postcondition names the result:

pub fn add_nonnegative(a: Integer, b: Integer) -> Integer
requires { b >= 0 }
ensures result { result >= a } {
  a + b
}

An unannotated caller is still checked when it calls a function with a precondition. Branch facts can establish the requirement, or a caller can expose its own requires clause. Invariant input types are useful when a property should travel with the value; a checked Result is useful when invalid input is expected. Gale bodies must prove their postconditions under their preconditions.

Function references cannot bypass these obligations. Adapting a function to a callback must establish its precondition from the callback’s input types. A behaviour implementation must accept every input admitted by its declared callback interface, including calls made by OTP. It cannot add an unsupported precondition merely because its own body verifies under that assumption.

Foreign callers must honor the exported interface or enter through a validating wrapper. Preconditions do not add automatic runtime assertions.

Universal and repeated contracts

A postcondition can introduce typed variables that range over every value of their types. These variables belong only to the postcondition:

pub fn identity(value: Integer) -> Integer
ensures result forall (offset: Integer) {
  result + offset == value + offset
} { value }

forall (first: Type, second: Type) binds one or more variables after the result name, or directly after requires. It does not add function arguments, enumerate values, or execute code at runtime. The body must still be a total, effect-free Boolean predicate. A requires clause restricts the function’s inputs; it does not restrict the quantified domain. An invariant-bearing binder type restricts that domain to its valid values.

Gale bodies must establish the property for every admitted binder value. Extern postconditions supply trusted properties of each individual call’s result. Callers can use these properties across modules, dependencies, function references, and supported higher-order helpers. No repeated extern call is implied. Quantification over an empty type is vacuous; it supplies no unconditional fact about the result. forall is available at the outer boundary of a requires or ensures clause, not as a runtime Boolean expression or inside an invariant.

A requirement can express a fact about every value of a type. Callers must establish the entire quantified property before calling the function:

pub fn zero(value: Integer) -> Integer
requires { value >= 0 }
requires forall (offset: Integer) { value + offset == offset }
ensures result { result == 0 } { value }

pub fn example() -> Integer { zero(0) }

Functions and externs can have several requires clauses, followed by their ensures clauses. Every requirement must hold. Each quantified binder belongs only to its own clause; it cannot be used in a sibling clause or the function body. An empty quantified domain cannot erase a separate ordinary requirement. The function body and its postconditions can use all the required facts. These rules also apply across dependency boundaries and when adapting a function to a callback. Arguments still execute once, and no runtime checking is added.

A function or extern can have several ensures clauses. Every clause describes the same returned value, and every clause must hold. Each result name and any quantified variables belong only to their own clause:

pub fn unchanged(value: Integer) -> Integer
ensures returned { returned == value }
ensures result forall (offset: Integer) {
  result + offset == value + offset
} { value }

Separate ordinary guarantees from per-element guarantees this way. Ordinary clauses remain available even when another clause quantifies over an empty type. Requirements apply to all clauses; none permits effects or introduces runtime arguments or assertions. Libraries and function references preserve every clause.

This is useful for contracts that describe unchanged map entries. The stdlib’s put, put_new, update, delete, and pop contracts preserve membership and values at every unrelated native key. A caller can use those contracts without writing a quantifier:

pub fn replace_other(map: Map<Integer, Integer>, value: Integer) -> Map<Integer, Integer>
requires { is_map_key(1, map) }
ensures result {
  is_map_key(1, result) and map_get(1, result) == map_get(1, map)
} {
  gale_std.map.put(map, 2, value)
}

Library authors can write the same kind of universal contract for their own functions. The compiler emits a quantified proof obligation and asks F*/Z3 to check it. Quantification extends what can be expressed; it does not guarantee that every true property will be solved automatically.

Ordinary total Gale functions can also supply checked proof steps. For example, a recursive helper can require equal list lengths and equal values at every position, then establish whole-list equality. A caller may state the length and position facts in earlier postconditions and use that helper in a later clause. The helper’s requirements must be established where it is used, and its Gale body must verify, including when it comes from a dependency. A helper used only in a contract adds no runtime call. The compiler can reuse eligible checked helper contracts automatically, and explicit proof steps remain available when needed.

Automatic use of checked helpers

The compiler can make a total binary helper’s checked input relation available to other proofs. Its implementation must verify, its preconditions remain the condition on that fact, and its ensures clause must state a direct equality between its two input roots. This works with public helpers supplied by dependencies and private helpers in the same module.

Assistance also sees ordinary local bindings. A computed list can be related to an earlier local list or a record field while those values remain in scope, even when the function ultimately returns a Boolean. Shadowed variables keep their distinct checked identities. The compiler infers generic arguments from one exact ordered argument tuple, including records with additional fields. Applying a helper that requires fewer record fields uses the same checked width conversion as an ordinary function call. These proof steps do not evaluate a local initializer again or add runtime calls.

For example, the stdlib’s checked list-equality helper supplies the induction argument needed for this ordinary function:

pub fn restore<A>(values: List<A>) -> List<A>
ensures result { result == values } {
  gale_std.list.reverse(gale_std.list.reverse(values))
}

The runtime function still performs the same two reverse calls. The compiler does not recognize a particular helper or foreign target name to prove this. A renamed helper in a user dependency can supply the same contract. Without a suitable checked helper, pointwise extern contracts alone may be insufficient to establish whole-value equality.

Candidate discovery looks for precondition observations that cover both inputs without depending on locally bound or quantified values, plus a result-independent equality in ensures. Checked calls and whole equality relations can both be observations. This is an assistance rule rather than a restriction on contracts. A helper that does not fit it can still be called explicitly in a contract or proof step. The compiler reuses exact checked values from caller equalities, normal returns, local bindings, and corresponding state projections; it does not enumerate every same-typed value or invent induction.

Only total, effect-free helpers can supply an automatic conditional theorem. Effectful functions and externs still supply normal-return contracts at their calls. Their declarations do not establish that any call returns. Helpers are checked before their theorems become available, and dependency checks include contracts and type invariants to prevent circular justification.

If a contract explicitly calls a guarded total Gale helper, the compiler ties that exact application to the helper’s complete checked postcondition when its requirements hold. This supports result-dependent properties such as guarded map lookup without exposing the helper’s full contract to unrelated callers. Total helpers without requirements already expose their checked result type directly and need no extra theorem. The call and any proof theorem are erased from runtime code when they occur only in a contract.

Helpers can use this assistance too: a helper can establish its own contract using a library’s checked facts, then supply its contract to another caller. Copied callback defaults retain access to private proof helpers from their original module. That access does not extend to unrelated functions in the implementing module.

The compiler includes applicable checked helper relations in the proof it submits to F*. The theorem contains only the direct input equality, conditional on the helper’s requirements. The helper’s result and unrelated postconditions do not enter the caller query. An unmet prerequisite establishes no fact and never becomes an assumption. The compiler emits a stable runtime model, one proof module per Gale source owner, and a complete-program root. F* checks that whole graph in one invocation and loads a checked source module only when its source and imports are still valid. Changed sources and their dependents are rechecked; unrelated checked sources remain reusable. F* stores its checked modules in the proof directory’s checked/ subdirectory.

The generated graph and verifier log remain at the usual artifact path on success or failure. An unproved obligation, solver resource limit, or backend failure is reported directly. Gale does not retry with different helper subsets or an unassisted graph. Test-harness timeouts are separate from verification.

Local proof steps

Use prove { condition } when a contract needs an explicit intermediate step. The compiler must establish the Boolean condition from the facts available at that point in the program. A failed proof stops compilation. The block and calls made inside it are erased from the generated runtime code.

For example, the stdlib supplies a checked list-equality helper. It requires equal lengths and equal values at every position, then derives whole-list equality by recursion. Native reverse contracts supply those input facts:

pub fn restore<A>(values: List<A>) -> List<A>
ensures result { result == values } {
  let restored = gale_std.list.reverse(gale_std.list.reverse(values))
  prove { gale_std.list.equal_from_positions?(restored, values) }
  restored
}

The emitted function contains the two native reverse calls and returns their result. equal_from_positions? has an ordinary checked Gale body. A dependency can supply its own helpers in the same way; their implementations must verify. Regular functions can continue to perform effects before or after a proof step.

A proof block can inspect saved immutable values, perform total calculations, and call total logical helpers. It cannot perform effects or invoke externs. Each helper’s requirements must hold at the call. Bindings created inside the block stay inside it. Used as an expression, a proof block has type nil; its calculated values cannot become runtime results. Proof steps work in ordinary function bodies, closures, result-binding sequences, and receive loops.

This makes explicit induction steps reusable without editing generated proof files. Automatic assistance handles the double-reversal example above, so its explicit proof step is optional. Other properties may still need intermediate facts or stronger helper contracts.

Receive-loop state transitions do not inject automatic relation helpers. Put the checked helper in a prove block to make the required relation explicit. This keeps mailbox verification bounded and avoids making solver search behavior part of the accepted program surface.

Explicit native primitives

builtin provides qualified access to the same native primitives available in the prelude. Use it when a local declaration shadows a primitive name, especially when declaring an extern with that name:

pub extern ":erlang.length" length<A>(items: List<A>) -> Integer
ensures result { result == builtin.length(items) }

pub fn count(items: List<Integer>) -> Integer
ensures result { result == builtin.length(items) } { length(items) }

The extern supplies a trusted relationship between its observed result and the list’s native length. Its body still calls Erlang. The predicate uses the native value operation, without replaying the external call. A different extern named length, or targeting :erlang.length, gains only its own declared properties.

Qualified primitives work in ordinary bodies, contracts, guards, pipelines, and function references such as builtin.length. Guards preserve the same type refinements as unqualified primitives. alias builtin as primitive is a static alias. The namespace cannot be declared by a library or used as a runtime module value or mod builtin type. Local variables can shadow its name.

Extern calls remain potentially effectful. Logical predicates use native observations or total Gale definitions. For example, after calling gale_std.list.length(items) in a body, its contract supplies the equality to builtin.length(items); putting another gale_std.list.length(items) call inside a predicate would replay an extern and is rejected.

Callback contracts

Ordinary verified helpers receive checked summaries of supported return relationships, including when they call externs. This preserves facts such as unchanged state fields across effectful helper calls. Higher-order helpers can also preserve a callback’s postcondition without additional annotations. For example:

pub fn invoke<A, B>(operation: fn(A) -> B, value: A) -> B {
  operation(value)
}

pub extern ":erlang.abs" magnitude(value: Integer) -> Integer
ensures result { result >= 0 }

pub fn example(value: Integer) -> Integer
ensures result { result >= 0 } {
  invoke(magnitude, value)
}

The compiler infers a checked summary for the helper and supplies the callback’s actual contract at the call. This also works across libraries, helper chains, closures, named Gale callbacks and their helpers, and known local function bindings. Separate calls remain separate observations: the same arguments do not imply the same result.

Inference covers bindings, if, cond, guarded matches, calls, and supported stable expressions. Calls can appear directly inside constructors and other strict expressions. Summaries are shared across callers. Guard failures select the next matching clause, and later cond conditions are observed only when earlier conditions fail. Inference preserves these same execution paths without replaying effects.

Prelude primitives such as abs, length, map_size, map_get, and the supported native type predicates retain their result facts when passed as function values. Direct calls, aliases, higher-order calls, and copied callback defaults use the same primitive observations. A same-target extern still supplies only its declared guarantees. Named Gale callbacks have checked summaries of their own bodies and reachable helpers, including effects; changing a lambda to a named function does not discard those inferred facts.

Size primitives retain their ordinary input types: length takes a list, while byte_size and bit_size take Binary. Use an is_binary(value) pattern guard to narrow a dynamic Term before either binary-size operation. Bits count as eight per byte, including for multibyte text. tuple_size accepts Term; a nontuple has no normal return in ordinary code and fails a guard. Its logical uses must establish that the input is a tuple, just as logical map lookups establish key membership. Native predicates whose value representations are still unsupported, such as is_float, remain explicit compiler gaps.

Structurally recursive helpers, such as list mapping, can retain the relationship between each callback input and its observed result. This includes mutually recursive helpers, such as a tree walker and a list-of-children walker, across dependency modules. The compiler handles unchanged forwarding calls when every recursive cycle eventually consumes a subterm. F* checks that the generated logical summaries decrease; no source termination annotation is needed for these cases. The runtime callback can still block, crash, or diverge; these are normal-return guarantees. Other recursive helpers retain their explicit contracts and typed result invariants. Arbitrary unknown function values provide only their types. Callback preconditions must still follow from the input types accepted by the helper; inference does not silently narrow those inputs.

Modules and library dependencies

Contracts compose across modules and Gale libraries, including transitive Mix dependencies. A call such as gale_std.integer.abs(value) can establish that its result is nonnegative in an application postcondition. Aliases resolve to the same library implementation.

The compiler reads Gale source from every resolved dependency and verifies all its declared contracts and invariants, including unused declarations. Selected calls pull in their actual Gale bodies and helpers, even when those helpers have no explicit contract. One generated F* program contains these definitions with separate identities for each module. A false contract on a Gale dependency body fails the application build before its Elixir sidecars are written. Previously generated BEAM files or proof logs are not accepted as proof certificates.

At a call with explicit postconditions, Gale injects the declared relation rather than an additional body-derived summary. This keeps unrelated implementation observations out of the ordinary solver context. v0.1 still checks transparent source definitions in one F* program, so this is not an opaque module boundary; the compiler rewrite must enforce that stronger separation.

Contract equality is an observable BEAM-value relation. It may be insufficient for the bounded prover to unfold a later generic recursive computation that needs the value’s constructors. Factor that computation into a checked helper with the result property you need, or leave the intermediate helper without an explicit postcondition so Gale can infer its structural summary. A solver resource limit or unproved result remains a rejected build.

Mix supplies its resolved transitive dependency graph. Direct compiler builds also follow nested path dependencies; GALE_DEPS supplies additional library roots. Libraries must distribute their Gale source to participate in verification. An extern declaration alone is not a proof of the foreign implementation. Foreign function guarantees come from their Gale declarations; no extern name selects special proof behavior.

Standard library contracts

The standard library keeps native implementations behind extern declarations. Gale verifies callers against those declared contracts and trusts the external implementation to honor them. Existing Gale adapters, such as tagged Option selectors and clamp, have their bodies checked against their contracts.

These interfaces provide the following guarantees:

Module	Functions	Guaranteed properties
gale_std.integer	abs, min, max, clamp, modulo, even, odd	Absolute value, selected extrema, inclusive clamp bounds, divisor-signed modulo bounds and exact result, and parity
gale_std.list	length, append, reverse, subtract, duplicate, flatten, contains, element_at, occurrences, first, last, is_empty	Length, membership, position, and duplicate-count laws; total observations; empty/singleton flatten identities; element selection and empty-list detection
gale_std.map	Single-key operations, merge, drop, take	Addressed and retained values, exact key selection, merge precedence, and cardinality bounds
gale_std.enum	map, filter, reject, find, count, member, empty, take, drop, sort, uniq, reduce, reduce_while, any, all	Length, membership, position, and occurrence-count laws, exact observations, and empty-iteration results
gale_std.option	is_some, is_none, unwrap_or, flatten, from_option	Variant tests and exact preservation of selected payloads or fallbacks
gale_std.result	is_ok, is_error, unwrap_or	Variant tests and exact preservation of the success payload or fallback

Append and reverse describe every output position and preserve occurrence counts. Subtract removes exactly the supplied number of copies of each value, up to the available count. Duplicate requires a nonnegative count and describes every position and occurrence count. Flatten uses native one-level concatenation, so list-valued elements keep their declared type; its current contracts state empty and singleton input identities.

element_at and occurrences are total ordinary Gale predicates, available to application code and contracts. Positions are zero-based; negative and out-of-range positions return None. Occurrences use strict native equality, including hidden record fields. These helpers let extern declarations state library properties; they do not replace the native implementations of append, reverse, or iteration. For example, enqueueing an item preserves a nonempty queue’s front:

module queue_front
pub fn enqueue<A>(items: List<A>, item: A) -> List<A>
requires { builtin.length(items) > 0 }
ensures result { gale_std.list.element_at(result, 0) == gale_std.list.element_at(items, 0) } {
  gale_std.list.append(items, [item])
}

The remaining stdlib functions retain their ordinary typed APIs. Foreign declarations supply trusted types and any explicit contracts; they do not acquire these stronger stdlib laws just by having similar names. See the bounded queue example for an invariant built on these library guarantees.

Supported first version

Verification follows local helper dependencies and local callers in both directions, including function references. This prevents unchecked callers from forging refined arguments or bypassing function preconditions. Checked call and reference identities distinguish overloads and shadowed local bindings. Ordinary effectful callers outside the type’s owning module can still use its opaque API. Externs participating in verification use their declared trusted interface, as described below. Foreign target names do not grant additional proof guarantees.

Selected functions support integers, booleans, atoms, tuples, records, structs, immutable updates, lists, Option, Result, supported recursive user variants, and disjoint native atom/tagged-tuple unions. First-order generic functions work over supported value types, including generic lists and variant payloads. Named aliases and represented opaques may come from other modules or libraries. Generic aliases, records, structs, native tagged unions, and opaque invariants are supported. For example, an opaque State<A> can constrain the length of its List<A> field while retaining the payload type. These contracts compose through library calls, copied behaviour defaults, and function references. Recursive and mutually recursive data definitions can contain supported lists, tuples, and record layouts. Generic and concrete recursive values preserve their native contents when stored in records or widened to Term. The compiler passes representation functions internally in the generated proof; no Gale annotations or runtime arguments are needed. Recursive conversions traverse supported lists, tuples, records, variants, and native unions. Widening retains hidden record fields and the complete native value. Strengthening requires proof that every converted payload satisfies its target type; the compiler can use concrete values, existing type refinements, and branch facts. Relating a separate recursive validation predicate to a whole-container conversion may require induction that is not yet inferred automatically. A checked recursive constructor or validator can instead build the refined result directly. Expressions include static local and qualified calls, bindings, if, cond, and supported patterns with checked guards. Equality and inequality use exact native equality, including when comparing values widened to Term.

Record views preserve extra fields. Struct views also preserve the native struct tag, so a struct remains different from a plain record with the same visible fields. Proof conversions introduce no runtime casts or value reconstruction.

Invariants and function contracts can call total, effect-free verified helpers, including library functions. Logical use is determined across modules and dependencies before emission. The compiler identifies structural descent through checked pattern bindings and aliases, independent of parameter order; F* verifies the resulting termination measure. Logical helpers without such an inferred measure use a data or integer argument whose decrease must still be proved.

Runtime recursion without inferred structural descent uses partial correctness. It can loop forever, including when it has list parameters. Every recursive call still checks its argument invariants and every normal return must satisfy its contract. Receives and potentially effectful callbacks or externs also use partial correctness. Mutually recursive runtime functions use the same safety rules: a process loop may alternate between functions without a terminating branch. Mutually recursive logical helpers are emitted as a group whose termination F* checks, including helpers split across modules or supplied by a library default. Each logical member needs a decreasing data or integer argument. Cyclic contracts remain rejected; a function cannot justify its postcondition by referring to that same contract, directly or through another function.

Closures, named and generic function references, higher-order calls, and typed receive expressions with supported guards are implemented. Calls through a concrete mod library value use the known library function’s contract and retain evaluation of the receiver. Abstract behaviour calls retain the callback’s input and result types, including invariants, and its mailbox requirement. They do not inherit postconditions from one particular implementation. Generic behaviour parameters and polymorphic callbacks are supported. Concrete Gale modules supply checked implementations and defaults; runtime dispatch remains an ordinary module call. Behaviour values can pass through generic library helpers and containers; equality uses their native module identity. Concrete foreign-module interfaces and absent native optional callbacks still have translation gaps. Floats remain unsupported in verified code. Behaviour helpers may carry contracts and proof steps, including when copied into a default. Helpers that mention a behaviour header type parameter bind it as an ordinary generic function parameter; separate implementations instantiate it independently. Explicit helper type parameters shadow header parameters. Invariant types declared in behaviour modules work like ordinary library types: give the type its own parameters, then use it in the callback signature. Copied defaults must preserve those invariants. Extern helpers may carry contracts as usual. Integer proofs use mathematical unbounded integers, matching BEAM integer arithmetic.

Map<K, V> values participate in contracts, state invariants, generic helpers, and callbacks. Their keys and values retain refinements, including recursive payloads and records with additional fields. A conversion must establish any new payload invariant and preserve the full native value. Native unions such as Map<K, V> | :error retain the map payload after matching the error alternative. Map entries follow the backend’s existing value-type limits.

The map_size, is_map_key(key, map), and map_get(key, map) primitives work in bodies, predicates, and guards. Search keys may be any Term; map_get retains the map’s value type. An is_map guard on Term gives its branch a Map<Term, Term> view without changing the native value. Typed and dynamic views agree on lookup, including keys with hidden record fields.

A missing key makes ordinary map_get raise at runtime and makes a guard fail. In logical predicates, establish membership before looking up a value: is_map_key(key, result) and map_get(key, result) == value. The predicate must be defined for every candidate result; the function body cannot supply a missing membership check inside its own postcondition.

Stdlib contracts describe addressed entries, preservation of unrelated entries, and cardinality. Insertion stores the supplied value and increases size only for a new key. Deletion establishes absence and decreases size only for an existing key. get and pop distinguish missing keys from stored nil. These facts establish bounds such as map_size(state.jobs) <= state.capacity, including replacement at full capacity. Foreign declarations supply the contracts; Gale checks the bodies of wrappers such as gale_std.map.get and gale_std.map.pop against them. An update callback may have effects: its contract does not invoke the callback again to describe its result.

merge retains exactly the keys in either input and selects the right input’s value on a collision. An empty input leaves the other map unchanged. drop and take specify which requested keys survive and preserve their original values, including with duplicate or missing selection keys. For example:

pub fn prune(map: Map<Integer, Integer>, keys: List<Integer>) -> Map<Integer, Integer>
requires { is_map_key(1, map) and not gale_std.list.contains?(keys, 1) }
ensures result {
  is_map_key(1, result) and map_get(1, result) == map_get(1, map)
} { gale_std.map.drop(map, keys) }

gale_std.list.contains? is an ordinary total Gale predicate over immutable values. It compares full native values, including hidden record fields, and accepts a Term search value. Contracts can use it without calling a foreign operation. The native gale_std.enum.member? extern declares its result equal to that predicate; its implementation remains Enum.member?.

Map cardinality guarantees remain bounds for bulk operations. Contracts do not describe map iteration order. MapSet values and their operations still need a proof representation.

Native iteration has data guarantees that do not replay its callbacks. gale_std.enum.map preserves list length. Filtering and rejection return only input values and cannot increase length. find returns an input value when successful; its existing Gale body proves that property. Sorting and deduplication retain membership. Sorting preserves duplicate counts; deduplication leaves exactly one copy of each original native value. List take/drop specify lengths and exact element positions for positive and negative counts. Filtering, rejection, take, and drop cannot increase the count of any value. Empty reductions retain the initial accumulator, while empty any and all return false and true respectively.

These contracts do not describe callback invocation counts, order, or equality with a second evaluation of the callback. Callback result types still carry their invariants through the trusted foreign interface. Exact transformation relations for arbitrary foreign higher-order functions need further contract support.

Irrefutable let patterns can destructure tuples, records, structs, and single-constructor variants in bodies and contracts. Destructuring an effectful result evaluates it once and retains the component relationships in callback summaries.

Integer div and rem work in ordinary code, callback summaries, and logical predicates. Division truncates toward zero, and a nonzero remainder has the dividend’s sign: -7 div 3 == -2 and -7 rem 3 == -1. In runtime code, a zero divisor crashes and contributes no normal return. This does not prove crash freedom. Logical expressions must be defined: their surrounding requirement or branch must establish a nonzero divisor. For example, divisor != 0 and result == dividend div divisor safely guards the division in a postcondition.

gale_std.integer.modulo calls Integer.mod through an extern and requires a nonzero divisor. Its trusted contract gives the exact result and bounds; a nonzero result has the divisor’s sign. even and odd also have exact checked contracts and can be used in predicates without a purity modifier.

Binary values, string literals, equality, and literal patterns are supported, including in state invariants and library contracts. Binaries retain their native identity when widened to Term; they are distinct from lists of byte integers. The model admits arbitrary bytes, including invalid UTF8. is_binary guards can refine native inputs, and byte_size counts bytes rather than characters.

String interpolation supports binaries, integers, Booleans, and atoms. It preserves binary bytes, formats integers in decimal, and uses atom names, except that nil formats as an empty string. Each embedded expression runs once in source order; effects remain separate observations. These rules also work in contracts and through library callbacks. For example, a formatter can declare ensures result { result == "job=#{id}" }, and callers can use that property through an ordinary higher-order helper. Extern formatters can declare the same property as a trusted interface contract; gale_std.integer.to_string exposes an exact decimal conversion contract this way. Float interpolation remains unsupported.

Guards support integer arithmetic and comparisons, signed integer div/rem, equality, Boolean short-circuiting, abs, tuple_size, and typed list length. Supported native type tests are is_integer, is_atom, is_boolean, is_pid, is_reference, is_tuple, and is_map; is_list is supported on already typed lists. A successful guard can refine Term to an integer, atom, Boolean, or PID for the body. Other refinements and primitives fail with an explicit unsupported model diagnostic. In particular, is_list on arbitrary Term does not establish a proper typed list: BEAM also accepts improper lists in that test.

An operation failing inside a guard rejects its clause. The verifier preserves short-circuit behavior and tests subsequent clauses for the same value in order. Guarded receives retain the native-message boundary restrictions described below; they introduce no delivery or eventual-selection guarantee. Guards can also appear in logical contracts, and copied library callback defaults use the same rules.

Proof annotations do not change the generated Elixir bodies. Invariants remain opaque types in emitted specs; the specs do not express the predicate. Automatic value-generated spectests exclude selected functions, since a broad runtime typespec cannot generate values satisfying a verified invariant. Ordinary tests can construct state through its verified API.

Trusted extern contracts

An extern signature is already a trusted interface. On normal return, verification assumes its declared result type, including any invariant. An extern may also have requires and ensures clauses:

pub extern ":erlang.abs" absolute(value: Integer) -> Integer
requires { value >= 0 }
ensures result { result == value }

Every Gale caller must establish the precondition, including unannotated callers and callers in other libraries. Function references cannot bypass that obligation. The postcondition is available after normal return. The compiler uses the same call interface for Gale functions and externs. It checks a Gale implementation and trusts an extern declaration; stdlib has no special privilege. A stronger result property needed through an effectful wrapper must appear in that wrapper’s result type or postcondition; a plain Integer return does not retain an internal integer bound.

The foreign body is not verified. A false extern contract is a false assumption and can invalidate downstream proofs. extern identifies that trust boundary; there is no additional trust modifier. With raises E, clauses follow raises, and the postcondition’s result is the Gale wrapper’s Result<Return, E> value. Predicates are typechecked and can use verified logical helpers, but cannot call externs or other potentially effectful computations.

A contract can describe an extern using a verified Gale specification:

fn count_elements<A>(xs: List<A>) -> Integer {
  match xs {
    [] -> 0
    [_ | rest] -> 1 + count_elements(rest)
  }
}

pub extern ":erlang.length" size<A>(xs: List<A>) -> Integer
ensures result { result == count_elements(xs) }

Callers can use the returned size’s relationship to count_elements. Changing only the foreign target to "MyRuntime.size" leaves the proof obligations unchanged. The foreign implementation must honor the declaration. This contract does not make size callable inside an invariant; use the verified specification there. Logical use of foreign functions is not currently supported.

Every extern may communicate, change external resources, crash, or diverge. Its signature supplies no termination, repeated-call equality, delivery, or shared-resource preservation guarantee. Foreign code must honor the declared value, callback, and typed-resource interfaces. Dynamic values outside such an interface enter as Term and require explicit validation. These declarations introduce no automatic runtime assertions.

Callbacks and receive loops

Function values retain their checked argument and result types, including state invariants. Each invocation is conservatively a possibly effectful, diverging computation. Closures may capture values, return other closures, send messages, and invoke externs. A receiving callback shares the enclosing typed mailbox. No source purity modifier is needed. Effect-polymorphic logical callbacks and specialization of known-pure function values are not implemented: invoking a function value inside a logical predicate is currently rejected.

A receive observes any value admitted by its mailbox type. Both finite timeout and :infinity forms are supported; a finite timeout adds an arbitrary timeout outcome. The verifier checks every admitted branch, including its next-state arguments. It assumes no message order, elapsed duration, fairness, or delivery. A loop may run indefinitely while each state-carrying call preserves its invariant. Postconditions describe normal returns only; they do not prove termination or crash freedom. Native monitor and exit handlers are supported as described below. Guarded receives still need a proof lowering.

Monitor and exit handlers

down(monitor) and exit(trap) arms use the same state and normal-return obligations as application messages. A DOWN event retains the pinned monitor reference. Its process identity and reason are otherwise arbitrary; an EXIT event likewise has an arbitrary process identity and reason. Emitted native patterns guard the sender with is_pid, matching the declared AnyPid field. Malformed senders do not enter these native handlers.

The verifier does not authenticate an event, infer that a process died, promise a notification, or assume that two calls to monitor return different references. It checks every written native handler, even one that could be shadowed by an earlier pattern. This conservative treatment proves local state safety without modeling selective-receive order. A crash that ends the receiving process’s lifetime introduces no later state transition.

Reasons have type Term. Proofs can retain these opaque native values, compare them, and distinguish supported atom, Boolean, or integer literals. Supported concrete values can widen to Term without losing their native identity. This does not add general dynamic decoding or support for all concrete value types. Monitor and timer values use abstract reference identities, including in records.

A catch-all can capture native VM tuples even when the declared application mailbox type excludes them. A verified handler may ignore such a value, bind it as Term, or use a mailbox type that includes both event shapes. Binding it as an unrelated application type is rejected. Tagged application patterns such as (:job, payload) keep those bindings separate from native events. This check also applies to receiving helpers that have no explicit native arms. An ignored catch-all branch must still preserve the invariant when a native event can reach it, even if application messages were already covered by preceding patterns.

Messaging without purity modifiers

Ordinary verified functions can call gale_std.process.send and gale_std.gen_server.reply. Effects propagate through their helpers and dependencies automatically. There is no pure or impure modifier. Predicates in requires, ensures, and invariant cannot perform effects, including through an indirect helper call: a property describes execution rather than sending additional messages.

Messaging functions use their declared extern interfaces, just like any other library call. The compiler does not infer semantics from a foreign target name. For example, the stdlib’s send extern declares that a normal return equals the sent payload; its Gale wrapper returns :ok. These declared properties are trusted, and Gale wrappers are checked against them.

AnyPid, the stdlib’s external Pid<M>, ReplyTo<R>, and monitor/timer handles have native value representations in the proof model. Sending does not mutate an immutable Gale value. The verifier checks returned values and local state invariants; it does not model communication histories, counts, or ordering.

For functions containing messaging effects, postconditions apply if execution returns normally. They do not establish termination, crash freedom, delivery, or eventual response. In particular, send attempts are not mailbox entries: receivers can die and distributed signals can be lost. See the BEAM signal semantics and GenServer reply API.

The bounded queue’s enqueue_and_notify and enqueue_and_reply demonstrate effects in the same module that owns its invariant. Both branches preserve a valid state; ordinary runtime tests separately exercise actual process messages and GenServer replies.

Target boundary: local state safety and transition correctness

The release target is local state safety and transition correctness, supported by automatically inferred effects. The intended state guarantee is inductive: initialization establishes a valid state, and every handled transition preserves it for every state satisfying the invariant and every admitted message value. Checking all such transitions establishes the invariant for every finite message sequence, rather than only the sequences covered by tests. This requires models for all relevant calls, casts, info messages, continuations, and failure paths. Foreign senders must honor the declared typed mailbox interface; genuinely dynamic input needs explicit validation. The guarantee applies independently to each process lifetime: a crash ends that lifetime, and a restart runs initialization again. It does not promise continuity across restarts. Typed receive loops with supported guards are implemented. Full OTP callback lifecycle verification remains unfinished.

Useful safety specifications include capacity bounds, valid lifecycle transitions, and ensuring that stale or duplicate completions leave state unchanged. Ordinary typed messages and reply payload checks remain part of the language. Communication protocol proofs, such as at-most-once replies across a computation, are excluded from release requirements and have no committed follow-up milestone. They would need additional application specifications and event models; reconsidering them requires a concrete use case. Shared storage invariants and coordinated multi-process proofs are also outside this local-state scope.

Eventual response or resolution is a separate liveness claim. It can be proved relative to explicit assumptions, such as eventual scheduling, eventual delivery, terminating handlers, and sufficient process survival. It cannot be promised when the environment may permanently stop the process or lose communication. A timeout outcome does not prove that the requested operation completed, and a long-running server need not terminate to behave correctly. See Safety, Liveness, and Fairness.

Liveness is outside Gale’s proof scope and roadmap. There is no planned optional liveness layer or requirement for users to provide scheduling, fairness, or survival assumptions. Local termination checks needed for sound logical definitions remain; they do not establish whole-process termination or eventual response. Ordinary functions need no purity annotations. The compiler infers effects and automatically checks declared safety properties against its supported models. Unsupported operations and solver failures must remain explicit; inability to prove a claim is not by itself evidence that the claim is false. Every build asks F* to validate the complete generated module graph. F* may load a checked module across builds only while its generated source and imported module identities remain valid. Clean release validation removes those checked artifacts and proves the graph from source.

Verification and failures

gale compile verifies the selected functions and invariant declarations before writing any Elixir sidecars. It writes GaleProof_Model.fst, readable GaleProof_Source_*.fst modules, and the GaleProof_Program.fst root under _build/gale/proofs/. Each adjacent .fst.map.json file maps generated ranges back to Gale source. The root .log records the complete F* invocation. trusted-externs.txt lists the foreign declarations assumed by that proof, and the same report is included in the verifier log. A false property, unsupported construct, missing verifier, or solver failure stops compilation. There is no admission or skip-verification switch.

When a source range is available, failures identify the Gale file, line, function, and expression involved. A related location identifies the precondition, postcondition, or invariant being checked, including properties declared in dependencies. Copied callback defaults and their private helpers retain their original library locations. Failures without a mapped range identify the generated proof and link to its log.

The diagnostic category distinguishes what stopped verification:

Category	Meaning
[unproved]	The verifier could not establish an obligation. This does not establish that the property is false.
[unsupported]	The compiler cannot yet translate this construct for verification.
[solver-resource-limit]	The solver reported resource exhaustion; the property remains unproved.
[verifier-failure]	The verifier could not start or encountered a tool failure.
[backend-error]	The generated proof was rejected for another reason that needs compiler investigation.

The terminal keeps the source diagnostic concise and links to the full verifier log. Solver details and generated names remain in that log for investigation.

mix_gale installs the pinned official F*/Z3 bundle when needed. To install it explicitly, run mix gale_std.prover. GALE_FSTAR_PATH selects an existing installation. The compiler’s IDE checks types and supported proof shapes; solver verification occurs during compilation.

Set F*’s per-query logical resource budget in mix.exs:

gale: [fstar_resource_limit: 50]

The value must be a positive integer and defaults to 50. It is independent of test-runner wall-clock timeouts and does not select or retry proof plans. Direct compiler invocations can set GALE_FSTAR_RESOURCE_LIMIT.

What the guarantee covers

Within Gale-checked code, assuming the compiler and verifier are correct, verified opaque values originate from checked constructors and transitions. Foreign code and declared extern interfaces must honor that contract. The BEAM does not make opaque representations inaccessible to handwritten Elixir: a foreign caller can forge a map, and a dishonest extern can claim it is State. Validate dynamic input through the verified constructors before treating it as verified state.

A state invariant does not prove that a request receives a reply, that a mailbox is empty, that processes never crash, or that the chosen business policy is the right one. For example, preserving a valid state rather than applying a requested transition can preserve the invariant; use function postconditions to state additional transition properties when they matter.

Collection syntax and verification

Binary concatenation (<>) and list concatenation (++) have direct verifier models. Map literals and the list subtraction operator (--) currently support runtime code only; a proof that needs their bodies receives an explicit [unsupported] diagnostic. Typed map and list stdlib operations retain their existing trusted extern contracts. This is a verification-coverage boundary, not a different runtime meaning for the operators or literals.