Contracts and the lifecycle

Everything in Geas is a contract. The contract is the unit of the language, not the function: it groups the state a signing locks, the commitments a host fulfills, the internal methods those commitments share, and the policy that decides when the whole is fulfilled, partially fulfilled, or broken.

This page uses skeleton/payment.geas from the repository as its running example:

payment.geas

contract PaymentService {
    vow currency: String = "USD"

    subcontract Validation {
        pledge validate_card(card: String) -> Result<Bool, Int> {
            return Ok(true)
        }
        pledge validate_amount(amount: Float) -> Result<Bool, Int> {
            if amount > 0.0 {
                return Ok(true)
            }
            return Err(1)
        }
    }

    subcontract Processing {
        pledge charge(card: String, amount: Float) -> Result<Bool, Int>
    }

    pledge notify_user(ok: Bool) -> Result<Bool, Int> {
        return Ok(true)
    }

    requirements {
        fulfill: Validation && Processing && notify_user
        partial: Validation || Processing
        break: !Validation && !Processing && !notify_user
    }
}

Vows

A vow is an immutable field, locked the moment the contract is signed:

vow currency: String = "USD"

A vow carries a type and an optional default, and the default is a constant of the vow’s type. Nothing inside the contract may assign to a vow. A host may override a vow at sign, supplying a value of the declared type, which is how the same contract runs against different configurations without changing a line:

c1 = rt.sign("PaymentService", vows={"currency": "EUR"})
assert c1.vow("currency") == "EUR"

A vow with no default and no override at sign is an unbound signing and is refused. A pledge body reads a vow by name.

Pledges

A pledge is a callable commitment with a declared return type, and it is a first class element of the language. Its return type is a Result, an Option, or Unit, never a bare fallible value:

pledge charge(card: String, amount: Float) -> Result<Bool, Int>

A pledge with a body is concrete. A pledge with no body is abstract: the contract cannot be signed until a host binds an implementation for it. In PaymentService, charge is abstract on purpose, so the host decides how money actually moves. A Python host binds an ordinary function over it:

def charge(inst, args):
    card, amount = args
    if amount > 0:
        return Ok(True)
    return Err(41)

A pledge is fulfilled through method syntax on a signed instance from inside the language, and by name from a foreign host.

Clauses

A clause is an internal method. It never leaves its contract, has no place in the lifecycle, and is not a first class value. Clauses exist so pledges can share logic:

clause compare(a: Int, b: Int) -> Int {
    if a < b { return -1 }
    if a > b { return 1 }
    return 0
}

Subcontracts

A subcontract groups pledges so a contract can be partially fulfilled and so the requirements policy can name a group as a unit. Validation groups the two checks; Processing holds the abstract charge. A subcontract is satisfied when every pledge inside it has latched fulfilled. A pledge declared outside any subcontract, like notify_user, is a loose pledge and stands on its own in the policy.

The requirements policy

The requirements block writes the contract’s fulfillment as boolean logic over its subcontracts and loose pledges:

requirements {
    fulfill: Validation && Processing && notify_user
    partial: Validation || Processing
    break: !Validation && !Processing && !notify_user
}

A bare name means that item is fulfilled, and &&, ||, 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.

Read the policy out loud. PaymentService is fulfilled when Validation and Processing and notify_user all land. It is partially fulfilled when either Validation or Processing lands. It breaks when none of the three has landed and something has failed.

The compiler proves at build time that no single state satisfies both the fulfill and the break line, naming a witness if one exists, and rejects a policy no state can satisfy. 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, defaults are synthesized into the same table form.

The lifecycle

A contract moves through five states:

Unsigned -> Signed -> Fulfilled
                   -> PartiallyFulfilled
                   -> Broken

sign() validates the contract’s shape, locks its vows, and activates it. It takes named vow overrides and an optional expected shape hash, and it refuses an abstract pledge that nothing has bound, an override naming no vow, an override of the wrong type, and a hash that disagrees.

break() tears the contract down and reclaims every allocation the runtime owns for it, in one walk. Every later fulfillment on a broken contract is a state error.

Latching

Fulfilling a pledge runs it and records the outcome. A pledge latches on its first Ok: it becomes fulfilled and stays fulfilled, and later calls run and return results but never change the latched state. An Err before any Ok latches the pledge broken with the error payload kept readable. Contract state never regresses.

Automatic re-evaluation

The runtime evaluates the requirements policy after every outcome, under the instance’s lock, in the priority break, then fulfill, then partial. 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 is armed only once something has actually broken, so an empty contract does not break on the vacuous truth of its negations.

The partial surface

The payoff is the partial surface: at any moment a host can ask which subcontracts and loose pledges are fulfilled, which are pending, and which are broken, with the latched errors attached by name. Watching PaymentService from Python, Validation lands and the contract goes partial:

c1.fulfill_sync("validate_card", "4111 1111")
c1.fulfill("validate_amount", 25.0).wait()

p = c1.partial()
# p.fulfilled == ["Validation"], p.pending == ["Processing", "notify_user"]

Drive charge and notify_user, and the policy declares the contract fulfilled. Or send a bad amount, and the break line fires by itself:

c2 = rt.sign("PaymentService")
out = c2.fulfill_sync("charge", "4111 1111", -2.0)
# out == Err(41), and c2 broke automatically
p = c2.partial()
# p.broken == ["Processing"], p.errors == [("charge", 41)]

The partial surface is readable from inside the language too. A pledge body can call instance.partial() and read state, fulfilled, and pending as ordinary fields of a record.

Where to go next

• Errors as values for how latched errors are declared, matched, and read.
• The store layer for subcontracts that become database transactions.
• Interop for driving this same contract from C and Python.
• Reference for the normative rules on contracts and the policy.