curry.backends.py.eval.checker module

The checker of the run-time invariants of the Fair Scheme: the checker mode of section 6.5 of the memo on the Fair Scheme proofs, behind the interpreter flag checker. The runtime state holds one Checker when the flag is on (RuntimeState.checker) and None otherwise; every hook in the runtime is one test of that attribute. The checker observes. It changes no step, no value and no counter. A violation raises InvariantViolation, an AssertionError whose message names the invariant, the event, the configuration, the identifiers and the goal position.

The events the memo names, and the checks at each:

• A fork (a choice at the root of a configuration; rts_fingerprint.fork). B1: the fingerprint of the configuration and of each clone is a function, its group invariant holds (every decided identifier agrees with the root of its group, and no member disagrees), and the fingerprints along the dispatch chain agree; each clone keeps every decision of its parent, has the decision of the fork and adds at most the forked identifier and its group root (rule D.2). S0: a fork inside a capsule is on an identifier that is function-derived for the capsule, that is in the escape set of no enclosing capsule and that no enclosing configuration decided, or on one the queue was split on before (def:s-escapes). The escape sets only grow.

• An escape (rule SF.1, the split of a queue; rts_setfunctions.split_queue). B1 for every configuration of the queue. S0: the escaping identifier is argument-derived for the capsule or for an enclosing one, or an enclosing configuration decided it. S-split: the kept queue holds the LEFT and the undecided configurations, the new one the RIGHT and the undecided, nothing else and nothing lost, both record the identifier, both name one set (one escape set).

• An insertion into an escape set (a pull-tab across a box; update_escape_set). S0: the identifier is argument-derived for the set.

• A pull-tab (rts_fingerprint.pull_tab). B1: the created choice carries the identifier of its source, and the two alternatives are faithful copies of the spine: fresh cells along the path, the cells off the path shared, the alternative at the end. S0 (def:s-pull): the identifier is in the escape set of every box the path crosses.

• A yield (rts_control.release_value). B1 as at a fork; no choice cell, operation cell, failure or constraint is reachable from the value (the generator of a free variable and the arguments of a partial application are not entered); X-c: no bound variable remains in the value, and for every variable with a decided root identifier the identifiers on the decided path of its generator are decided.

• The constraint step at the root (rule D.beta; fairscheme.D after constrain_equal kept the configuration). B1 as at a fork. At a fork, a constraint step and a yield as well: E5, a decided class of two or more variables has a generator at its root (Def 2.74, Thm 3.28 of the note on the Fair Scheme; issue #127); E11, every binding sits under the root of its class, so a class holds one binding (Remark 2.70; issue #128); D15, no class holds a variable that lies inside the generator instance of another member, the occurs check of the decision of 2026-10-12 (the union that would make such a class fails the step).

• The dispatch of a configuration (fairscheme.D) and a drop of the dispatched configuration (D at a failed root, N at a failed successor of the root). Def 2.40 (discard): the discards change no cell, so the root cell holds at the drop the symbol and the successors (through forward nodes) it held at the dispatch; a constructor, a set guard or a constraint cell at the root is recorded, an operation cell is not (a step rewrites it in place; issue #126). The record is one per scheduler: a nested D (allValues) pushes its own (enter_scheduler, leave_scheduler).

• The record of a failure in a capsule (rts_setfunctions.record_failure) and the end of a capsule on the empty queue (allValues). F2 (d1), the failure rule in its deferred form (Definition 2.94 of the note on the Fair Scheme): a failure that crossed no set guard on the path from the root of the configuration is recorded as an inside failure, and one that crossed a guard as an outside failure that names the crossed sets less the set of the capsule, with the level at which it entered the chain of the capsules. F2 (d2): the capsule is a failure when it produced no value, recorded no inside failure and recorded some outside failure, and the empty set otherwise. F2 (d3): the failure goes under the guards of the records at the least level, together.

• A slot write of an existing generator (fairscheme.hnf) and an instantiation. Def 2.62 (equality step): a step of =:= or =:<= narrows a variable that is free in the configuration (its group undecided, no binding) against a constructor alone; two free variables make a constraint cell, and a free left side of =:<= takes the right side as a binding without a step at it (issue #129). A step of =:= that meets a decided variable and a variable that is free in the configuration records the pair: it neither narrows the free one against the instance nor replaces the decided one by its generator (decision D25 of 2026-10-12).

• An instantiation (rule S.x; rts_freevars.instantiate), the copy of rule N.x (fairscheme.N and hnf), and the creation of a generator. X1: one generator per variable, with the variable’s identifier at its root. X-b’: the write is a faithful copy of the spine with the generator at the end, and the reduct of every configuration that references the redex, read under the fingerprint it is compatible with, is the same before and after the write; the same for the private copy of rule N.x against the root it replaces. The reduct is read with the generator image of the memo: a decided choice is its side, a bound variable is its binding or its generator, a free variable is its group. The comparison is bounded (SIGNATURE_BUDGET cells per event); an event over the budget is counted, not checked.

• A step (fairscheme.S, after a completed step). The choice a step creates is tagged with the boxes above it: the set guards crossed on the path from the root of each configuration of the dispatch chain to the redex, and the capsules whose arguments reached the redex (the flags of the cell, set by the entry walk of the capsule and inherited by the cells a step creates at a flagged redex: the walk starts at the successors of the result, under PROPAGATE_BUDGET). The tags define “argument-derived”. B2: a replacement by failure comes from an exempt leaf of the definitional tree of the operation, or from a built-in.

• An inductive position (fairscheme.hnf, at entry). B2: the position is an inductive position of a branch of the definitional tree of the operation at the redex that matches the constructors already at the positions above it. The tree is rebuilt from the ICurry case structure of the operation. A built-in has no tree and is not checked.

Section 6.5 of the memo asks for these checks in the Python backend first; the C++ runtime mirrors them behind the same flag in a later lane.

class curry.backends.py.eval.checker.Checker(rts)

Bases: object

capsule_end(qid, failure_sids)

After allValues gave its verdict on the empty queue qid: failure_sids is None when the list ended, and the set ids of the guards of the failure written otherwise.

capsule_entry(sid, goal)

After create_queue set the goal of set sid: every cell reachable from a boxed argument of the goal is inside the capsule (the entry step of def:s-flags).

check_capsule_end(produced, inside_failure, outside_failures, failure_sids)

F2 (d2): the capsule is a failure when it produced no value, recorded no inside failure and recorded some outside failure, and the empty list otherwise. F2 (d3): the failure goes under the guards of the records at the least level, the failures that entered the chain innermost, together.

check_failure_record(Q, crossed, record)

F2 (d1): an inside failure crossed no guard; an outside failure names the crossed sets less the set of the capsule, with the level of the outermost capsule of the chain among them (zero when none is on the chain).

constrain_begin(config)

Before the unions of a constraint step at the root (D): the bindings of config, which constrained compares with the bindings after the step (_check_merge_guards).

constrained(config)

After a constraint step at the root kept config (rule D.beta): the fingerprint, with the group and generator clauses, and the bindings.

copied(old, new, realpath, end, kind)

After a private copy of the spine from old along realpath with end at its end replaced the root of the current configuration (rule N.x; kind names the replacement).

discard(root)

At a drop of the dispatched configuration (D, and N at the root): the discards change no cell (Def 2.40: D.1, D.3, D.4 and N.1; Def 2.24 admits a replacement by failure at an operation cell alone), so the root cell recorded at the dispatch holds the symbol and the successors it held then. A successor is compared through forward nodes, read now for both: a step below the root forwards its operation cell, and the compression of a chain writes the slot to the end of the chain, a no-op modulo the dereference (Def 2.9). A failure written over the shared root of a failed configuration took the value of a sibling (issue #126 of the C++ backend; the C++ checker has the same check).

dispatch(root)

At the dispatch of a configuration (D): its root cell, its symbol and its successors, for discard. A constructor, a set guard or a constraint cell is recorded: a step rewrites an operation cell at the root in place.

enter_scheduler()

A nested D runs on this checker (allValues): its dispatches and drops get their own record.

escape(qid, cid, before, rhs_qid)

After split_queue split queue qid on cid (rule SF.1): before is the list of its configurations before the split and rhs_qid the new queue.

escape_insert(sid, cid)

After update_escape_set added cid to the escape set of sid.

failure_recorded(config, guards, record)

After record_failure recorded a failure that config met in the current queue: guards are the guards of the position in hand, and record the pair of the level and the set ids recorded, or None for an inside failure. The hook reads the guards the path crossed from the call stack of the configuration, as record_failure does, and the check compares them with the record.

fork(config, clones)

After rts_fingerprint.fork made clones of config, whose root is a choice.

generator(x, gen)

After _make_generator gave the variable x the generator gen.

hnf(var, typedef, values)

At the entry of hnf for the inductive position var.

instantiate_begin(var)

Before instantiate writes the generator into the spine of the redex var.root: the variable at the slot, the spine, and the reducts of the configurations that reference the redex.

instantiate_end(var, before)

After the write of instantiate.

leave_scheduler()

merge_guard(config, dropped, kept)

A merge of two bound classes in the constraint step in flight (update_binding; decision D26 of 2026-10-12): the binding dropped and the binding kept. The pair goes into the record, and constrained compares the record with the store and the continuation (_check_merge_guards).

pulltab(root, target, realpath, lhs, rhs)

Before pull_tab rewrites: the two copies of the spine from root along realpath with the alternatives of target at their ends.

pulltab_done(node, target)

After pull_tab made node, the choice over the copies.

slot_write(var)

Before hnf writes the generator of the variable at var into the spine of the redex var.root (rule S.x with an existing generator).

step(node, info, args)

After S completed a step at node, which held info with the successors args before the step.

unguarded_merge(config)

A merge of two bound classes with distinct binding cells outside the constraint step at the root (update_binding without a list: the fork, the pairing of get_generator). The step fails as before D26. No known program reaches it; the count makes a reach visible, and the tests pin it at zero. The C++ checker has the same count.

value_bindings(x, tree)

After make_value_bindings made tree for the variable x.

variable(node)

After freshvar made the free variable node.

yield_(config)

Before release_value makes a value of config.

exception curry.backends.py.eval.checker.InvariantViolation(invariant, event, detail, context=())

Bases: AssertionError

A run-time invariant of the Fair Scheme does not hold.