Skip to content
Geas

Requirements and state

The requirements block writes a contract’s fulfillment as boolean logic over its subcontracts and loose pledges. This page is normative: the rules here are the ones the compiler proves and the runtime evaluates.

The block

Section titled “The block”
requirements {
    fulfill: Validation && Processing && notify_user
    partial: Validation || Processing
    break: !Validation && !Processing && !notify_user
}

A bare name means that item is fulfilled. &&, ||, and ! combine the conditions. Three lines are defined:

  • fulfill: the condition under which the contract is fully fulfilled.
  • partial: the condition under which it is partially fulfilled.
  • break: the condition under which it breaks.

An atom names a subcontract or a pledge declared outside any subcontract, a loose pledge. At most 16 atoms per contract. The grammar of a requirements expression:

ReqExpr  ::= ReqOr
ReqOr    ::= ReqAnd { "||" ReqAnd }
ReqAnd   ::= ReqNot { "&&" ReqNot }
ReqNot   ::= [ "!" ] ReqAtom
ReqAtom  ::= IDENT | "(" ReqExpr ")"

When the block is absent the defaults apply: fulfill when every subcontract and every loose pledge is fulfilled, partial when at least one subcontract is, break when everything is broken.

Latching

Section titled “Latching”

A pledge latches. It becomes fulfilled on its first Ok and broken on an Err that lands before any Ok. Later calls still run and still return their results to the caller, but the latched state never changes, so contract state never regresses. The error payload of a broken pledge is kept readable until an explicit break reclaims it.

A subcontract is fulfilled when every pledge inside it has latched fulfilled, and broken when every pledge inside it has latched broken.

Evaluation and priority

Section titled “Evaluation and priority”

The runtime evaluates the policy after every outcome, under the instance’s lock, in the priority break, then fulfill, then partial. The first line that matches sets the contract state.

A state that satisfies both fulfill and partial is fine; fulfill wins by priority. When the break line holds, the contract transitions to broken by itself, keeping its heap alive so the error payloads stay readable until an explicit break reclaims them.

The break line arms only once something has actually broken. Before at least one pledge has latched broken, the break line never matches, whatever its expression says. Without this rule a policy like break: !Validation && !Processing would tear the contract down after its very first successful fulfillment, when nothing has broken and nothing is yet fulfilled, on the vacuous truth of its negations.

The compile time proof

Section titled “The compile time proof”

The compiler proves at build time that no single state satisfies both the fulfill and the break line, by enumerating the atom assignments. If a contradiction exists, the compiler names a witness, a concrete assignment of fulfilled and broken atoms under which both lines hold, so the diagnosis is a counterexample and not a shrug. A policy no state can satisfy is also rejected.

The requirements block compiles to a shared table the static checker and the runtime evaluator both read, so the two can never diverge. When a contract writes no requirements block, the grammar’s defaults are synthesized into the same table form.

The partial surface

Section titled “The partial surface”

The partial surface reports, at any moment, which subcontracts and loose pledges are fulfilled, which are pending, and which are broken, with the latched errors attached by name.

Inside the language, instance.partial() returns the PartialResult, a builtin record every program carries without declaring it:

record PartialResult {
    state: String
    fulfilled: List<String>
    pending: List<String>
    broken: List<String>
}

The name lists come back in the runtime’s insertion order. It is an ordinary record value, its fields read like any record’s, and the copy is independent the way every read is. The Err payloads stay on the C surface, where geas_partial_error hands them over, because their types vary per pledge and a record field carries one type. Declaring your own PartialResult collides with the builtin and is an error.

instance.status() returns the state’s canonical spelling as a String: "Unsigned", "Signed", "Fulfilled", "Partial", or "Broken".

Versioned contracts

Section titled “Versioned contracts”

A contract carries an optional version attribute, default 1:

contract PaymentService [version: 2] {
    ...
}

The version is baked into every mangled name the contract produces, alongside a 64 bit FNV-1a hash of the type signature. The mangled name has the form:

__geas_ash_{contract}_{symbol}_{sighash}_v{n}

Because the name carries both the shape hash and the version, a host that signs against the wrong version is refused at discovery time with a descriptive error, never corrupted at call time. geas emit-header writes these names as C defines so a host resolves against generated names instead of string literals. See The geas CLI.

Section titled “Related pages”