===============
Developer Notes
===============

This page holds the facts a developer of Sprite needs and a user does not.
The user guide describes one backend, the C++ backend.  The second backend
of the source tree, the Python backend, is a reference implementation behind
a flag until its removal.  This page names the flag, says what the backend
is for, and lists its limits.

.. _reference-backend:

The reference backend
=====================

``curry.backends.py`` is a compiler from ICurry to Python and the Fair
Scheme scheduler in Python.  It was the first backend of Sprite and the
default until the C++ backend took its place (issue #82, 2026-10-06).  It
stays in the tree as a reference implementation until the removal gate
below: the oracle of the values of the C++ backend in the test suite, and a
debugging aid.

The flag
--------

The interpreter flag ``backend`` selects it with the value ``py``.  Every
surface that sets a flag takes the value:

* ``SPRITE_INTERPRETER_FLAGS=backend:py sprite-exec prog.curry``, or
  ``sprite-exec -b py prog.curry`` and ``python -m curry -b py prog.curry``.
  The help of ``-b`` lists no value, and the error for an unknown value
  (``unknown backend 'foo'``) lists none.
* ``:set backend py`` at the prompt of the REPL.  The listing of ``:set``
  shows the backend of the session, and the error for an unknown value
  (``Invalid backend: 'foo'.``) lists none.
* ``sprite-make --py M.curry`` (``-p``, ``--python``) writes the Python
  module of the saved form.  The help and the manual of ``sprite-make``
  omit the option; ``make stage`` and the test runner use it.
* ``Interpreter(flags={'backend': 'py'})`` and
  ``curry.reload({'backend': 'py'})`` in the Python API.  A new interpreter
  starts from the flags of the environment and takes its argument over
  them (:mod:`curry.interpreter.flags`).
* ``configure --with-default-backend py`` for an installation whose default
  it is.
* ``./run_tests --backend py`` or ``--backend both`` under ``tests/``, and
  ``run-tests.sh py`` in CI.

The name ``backend:py`` stays until the removal.  A second name, one that
says "reference", would add an alias to the flag, to the help texts, to
the REPL, to the test runner, to the CI workflow, to the conda recipe and to
the run scripts of the examples, for the month before the removal.  The
removal deletes every call site either way.

What it is for
--------------

* The oracle of the values of the C++ backend.  The test runner runs every
  file on both backends (``--backend both``), the functional tests compare
  both backends with PAKCS, and CI runs the unit and functional suites on
  this backend in the job ``py backend 1/1``, on the nightly schedule and
  on request, not on a push (stage 4 of issue #82).
* The generated code of a function as Python source.
  ``curry.inspect.getimpl(f)`` gives the Python step function on this
  backend.  The C++ backend gives the generated C++ of a compiled module, or
  the bytecode listing of an interpreted one.  Example 03 prints it.
* PDB into generated code.  Under the flag ``debug`` the backend writes each
  step function to a source file, so a breakpoint in generated code works.
* The flag ``trace``.  The backend prints each step (``S <<<``, ``S >>>``)
  and the queue of the scheduler::

     SPRITE_INTERPRETER_FLAGS=backend:py,trace:true sprite-exec prog.curry > spritelog

  ``spritelog.vim`` at the root of the repository highlights the output.
  The C++ backend accepts the flag and prints nothing; its trace is a build
  of the runtime with ``SPRITE_TRACE_ENABLED``.
* The profiler.  ``sprite-exec -p`` (``--profile``, with ``--psort`` for the
  sort key) runs the program under ``cProfile``.  The rewrite steps are
  Python functions on this backend alone, so the profile shows the program
  there; on the C++ backend it shows the driver, and ``--stats`` reports
  the counters::

     sprite-exec -b py Peano.curry --profile --psort=calls

* The saved form.  ``curry.save(M, 'M.py', goal='main')`` writes a Python
  program that holds the generated code of the module and evaluates the
  goal; ``curry.save(M, 'M.py', module_main=False)`` writes the module
  alone, and ``curry.load('M.py')`` reads it back.  A saved program runs
  under the Python of the installation and reads ``-g NAME`` and ``--help``
  as ``sprite-exec`` does; a goal without a signature is defaulted at run
  time from the type the file records.  ``sprite-make --py M.curry -o M.py
  -g main`` writes the same form (the option is hidden in the help), with
  the bytecode cache of the file beside it under ``__pycache__``, so that
  CPython compiles a generated module once per change.  Example 04 runs the round trip.  On the C++
  backend ``curry.save`` writes C++ source whose entry point is a stub, and
  ``curry.load`` reads the shared object that ``sprite-make --so`` writes;
  the C++ form of ``curry.save`` is an open decision of stage 5 of issue
  #82.  ``tests/unit_loadsave.py`` pins both routes.
* The stepper of the test library.  ``cytest.step`` takes a bounded number
  of rewrite steps of an expression through the step limit of the generic
  evaluator (``Evaluator.set_global_step_limit``).  Both backends provide
  the limit: the Python ``RuntimeState`` counts in its ``StepCounter``, and
  the C++ scheduler stops after the step that reaches
  ``RuntimeState::step_limit`` (``cyrt/state/rts.hpp``), which the adapter
  ``cyrtbindings.StepCounter`` presents as ``rts.stepcounter``.  The graph
  then holds the result of exactly that many steps on either backend, so
  the two tests that use it, ``test_interp_step`` of ``unit_py_runtime.py``
  and ``test_apply_nf`` of ``unit_prelude.py``, run on both;
  ``unit_cxx_steplimit.py`` pins the limit.  ``evaluator.single_step``
  takes one step at the root on both backends.
* The white-box tests of its evaluator: the ``unit_py_*`` files that drive
  the graph classes and the ``RuntimeState`` of the backend directly skip on
  the C++ backend.

Its limits
----------

* It suits small programs.  The C++ backend is more than a hundred times
  faster on the benchmark programs.  In the baseline record of 2026-10-03
  (:doc:`Performance`), 11 of the 30 programs of the dissertation timed out
  at 120 s on this backend and two failed (``Reverse`` and
  ``ReverseUser``); the record holds one repetition of this backend beside
  five of the C++ backend.
* The flag ``recursion_limit`` (default 262144) bounds the Python frames of
  one value: the recursion limit of the interpreter while the value is
  computed.  The backend nests about eight frames per element of a list
  under a function that is not tail recursive, such as ``length`` or
  ``sort``, so the default covers a list of about thirty thousand elements.
  An alternative that reaches the limit runs again after the others and is
  dropped when it overflows again without progress; its ``RecursionError``
  is reported after the other alternatives have run.  A larger limit costs
  about 4 KB of memory per nested element; ``None`` leaves the limit of the
  interpreter as it is.  Issue #62 records the failures of the list
  functions over about a thousand elements under an earlier limit.
* The flag ``step_budget`` (default 2048) is the number of rewrite steps one
  alternative gets before the queue rotates.  Rotation occurs only when
  another alternative waits, in the same queue or in an enclosing one, so a
  diverging alternative cannot starve the others, also not from inside a
  set function.  ``None`` turns the rotation by steps off; rotation on
  residuation and on a Python stack overflow still occurs.  The backend
  ignores the flags ``rotation``, ``stack_limit`` and ``interpret``, and
  the variables of the collector (``SPRITE_GC_*``).
* It has no collector of its own.  ``curry.stats`` reports 0 for
  ``collections``, ``gc_seconds``, ``swapped``, ``failed_compiles`` and the
  ``gc_`` keys.
* ``show`` of an ``Int`` bound by ``=:=`` under ``$##`` does not finish
  (issue #60); the C++ backend prints the value.
* The backend asserts on a set guard of an enclosing set at the root of a
  configuration, one known failure of the set-function corpus
  (``unit_cxx_scheduler.py``, ``unit_setfunctions_bugs.py``,
  ``unit_setfunctions_semantics.py``); the C++ backend passes it.
* The queues of a set function hold references to their configurations.
  After the escape of a choice the two queues of the split share them, and
  a step in one queue takes effect in the other; the C++ runtime clones a
  shared configuration before a queue steps it.  The clone of a capsule
  for an alternative that bound a variable of its goal after the start
  (issue #86) copies the configurations instead.  On both backends the
  clone goes into a private copy of the spine of the reference that read
  the binding, so a second reference of the same alternative to the
  capsule clones it again; a binding the alternative holds at the start
  of the capsule is absorbed then, with no clone.
* A string built by :func:`curry.expr` is one ``_biString`` node, which
  prints as ``_biString 'hello'`` until its first step unfolds it; on the
  C++ backend it is the list of its characters.  The ``repr`` of a negative
  ``Float`` node differs between the backends.

The checker mode
----------------

The interpreter flag ``checker`` (off by default) turns on 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.  Both backends have one.  The
runtime state of the reference backend holds one ``Checker``
(``curry.backends.py.eval.checker``) while the flag is on, and ``None``
otherwise; the runtime state of the C++ backend holds one ``Checker`` of
``src/cyrt/checker.hpp`` (``RuntimeState::checker``, a pointer that is null
otherwise).  Every hook in a runtime is one test of that attribute or
pointer, so the flag-off path costs one test per event and makes the same
steps, values and counters as before, and the checker changes no step, no
value and no counter when it is on; it costs time, and memory, since it
keeps every flagged cell alive for the life of the runtime state.  A
violation raises ``InvariantViolation``, an ``AssertionError`` whose
message names the invariant, the event, the configuration (its queue, its
set, its fingerprint, its groups, its root), the identifiers and the goal
position; on the C++ backend the class is
``curry.backends.cxx.cyrtbindings.InvariantViolation``, raised from the
hook through the scheduler as the step limit is.  To run a program under
the checker::

   SPRITE_DEBUG=1 SPRITE_INTERPRETER_FLAGS=backend:py,checker:true sprite-exec prog.curry
   SPRITE_DEBUG=1 SPRITE_INTERPRETER_FLAGS=backend:cxx,checker:true sprite-exec prog.curry

``sprite-exec`` prints an ``AssertionError`` as "an internal error
occurred" unless ``SPRITE_DEBUG=1`` is set, so the report of a violation
needs that variable under ``sprite-exec``; the Python API raises the
exception with its full message.

The hooks sit at the events the memo names, and each one runs the checks
of the invariants it names (``RI`` numbers the invariants of the review of
the implementation; the memo states them in its sections 2.1 to 2.5):

* A fork (``rts_fingerprint.fork``) and a yield (``rts_control.
  release_value``): the fingerprint of the configuration is a function and
  its group invariant holds (every decided identifier agrees with the root
  of its group, and no member disagrees), the fingerprints along the
  dispatch chain of the nested queues agree, and the escape sets only grow
  (B1, S0).  Each clone of a fork 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 of the memo; a fork on a free variable, which
  applies its bindings, may add more).  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 its queue was split on before (S0, def:s-escapes).
  At a yield no choice, operation, failure or constraint cell is reachable
  from the value, no bound variable remains in it, and for every variable
  with a decided root identifier the identifiers on the decided path of
  its generator are decided (B1, X-c).  Two exclusions, which the paper
  must carry: the walk does not enter the generator of a free variable,
  and it does not enter the arguments of a partial application, as the
  walk of ``N`` does not (a value may hold ``(+) (1 ? 2)`` as a function
  value with the choice unevaluated inside it).  At a fork, at a yield and
  at a constraint step at the root (rule D.beta) as well: a decided class
  of two or more variables has a generator at its root (E5, Def 2.74 of
  the note on the Fair Scheme; issue #127), and every binding sits under
  the root of its class, one binding per class (E11, Remark 2.70; issue
  #128), and no class holds a variable that lies inside the generator
  instance of another member (D15 (occurs check), the decision of
  2026-10-12: the union that would make such a class fails the step).
  At a constraint step as well: a binding the step dropped at the merge
  of two bound classes is guarded, above the result of the step, by its
  strict equality with the binding kept (D26 (guard at the merge), the
  decision of 2026-10-12).
* The dispatch of a configuration and a drop of it (``D``, and ``N`` at a
  failed successor of the root): the discards change no cell, so a
  constructor, set-guard or constraint cell at the root holds at the drop
  the symbol and the successors, through forward cells, it held at the
  dispatch (Def 2.40 (discard); issue #126 of the C++ scheduler).
* A slot write of an existing generator (``hnf``) and an instantiation
  inside a step of ``=:=`` or ``=:<=``: the step narrows a variable that
  is free in the configuration 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 (Def 2.62 (equality
  step); 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 escape, rule SF.1 (``rts_setfunctions.split_queue``): the escaping
  identifier is argument-derived for the capsule or for an enclosing one,
  or an enclosing configuration decided it; the kept queue holds the LEFT
  and the undecided configurations, the new one the RIGHT and the
  undecided, both record the identifier, and both name one escape set
  (S0, S-split).  An insertion into an escape set (a pull-tab across a
  box) is of an argument-derived identifier (S0).
* A pull-tab (``rts_fingerprint.pull_tab``): the created choice carries the
  identifier of its source, the source is at the recorded path, and the
  two alternatives are fresh copies of the spine that share the cells off
  the path (B1); the identifier is in the escape set of every box the path
  crosses (S0, def:s-pull).
* An instantiation, rule S.x (``rts_freevars.instantiate``), a generator
  (``_make_generator``) and the private copy of rule N.x (``N`` and
  ``hnf``): one generator per variable with the variable's identifier at
  its root (X1); 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 reduct of the private copy
  equals the reduct of the root it replaces (X-b').  The reduct is read
  with the generator image of the memo (a decided choice is its side, a
  bound variable its binding or its generator, a free variable its
  group) and compared through a digest, within a budget of cells per
  event; an event over the budget is counted, not compared.
* A step (``fairscheme.S``, after a completed step): the choice a step
  creates is tagged with the boxes above it, the set guards crossed from
  the root of each configuration of the dispatch chain to the redex, and
  the capsules whose arguments reached the redex (the entry walk of a
  capsule flags the cells reachable from its arguments, up to 50000 cells
  per capsule, and the cells a step, a pull-tab, a copy or a generator
  creates at a flagged cell inherit the flags, up to 1024 cells per event;
  the walk of a step starts at the successors of the result cell, since
  the redex itself carries the flags already, and a walk over its budget
  makes the sets of the flags unbounded, so their checks of S0 are
  suppressed from then on, as after an entry walk over its budget; a leaf
  value, a constructor or a failure without a successor cell, is not
  flagged).  The tags define
  "argument-derived" for the checks of S0.  A replacement
  by failure comes from an exempt leaf of the definitional tree of the
  operation, or from a built-in (B2).
* An inductive position (``fairscheme.hnf``, at entry): the position is a
  case of the definitional tree of the operation at the redex, rebuilt
  from the ICurry case structure, under branches that match the
  constructors already at the positions above it (B2).  B2 is asserted
  for the operations with an ICurry body alone.  The built-in steps of
  ``currylib`` are hand-written Python outside the generated code, have
  no tree and are not checked; they are most of the ``hnf`` calls of a
  run (on the set-function and functional-pattern goals of the suite,
  10773 of 16492 calls: ``plusInt``, ``nonstrictEq``, ``apply``, ``cond``,
  ``eqChar``, ``allValues``, ``_biString``, ``&``, ``constrEq``,
  ``ltEqInt``, ``evalS``, ``applyS``, ``set``, ``$!``, ``eqInt`` lead).

``tests/unit_py_checker.py`` holds one constructed violation per check and
runs the known-good programs of the suite under the checker.  The checker
does not check the lifts of the constraints of ``=:=`` and ``=:<=`` (the
memo's FS-β), the schedule replay of section 6.5, or the private copies
that a set function makes for a configuration.  "Argument-derived" is read
from the tags of an identifier (the boxes above its creation site and the
flags of the capsule's arguments), which over-approximate the escape sets:
the checks of the current capsule read the tags, the checks of the
enclosing capsules read the escape sets, as def:s-escapes does.

The checker of the C++ runtime (``src/cyrt/checker.hpp``,
``src/cyrt/checker.cpp``) mirrors the Python checker hook by hook and check
by check.  Its header is outside the include closure of ``cyrt/cyrt.hpp``:
the generated code never sees it, and the hooks reach the checker through
the pointer of the runtime state.  The hooks sit at the same events: the
fork (``rts_fingerprint.cpp``, after the clones went into the queue and
before the parent leaves it), the escape (``allValues_step`` of
``currylib/setfunctions.cpp``, around ``Queue::split``), the pull-tab
(``RuntimeState::pull_tab``, before the copies of the spine and after the
choice over them), the yield (``release_value``), the fresh variable
(``freshvar``), the generator (``_make_generator`` and
``clone_generator``), the value bindings and the private copies of rule N.x
(``replace_freevar``), the write of a generator into a slot (rule S.x:
``instantiate``, and the slot write of an existing generator in
``replace_freevar``), the step (``procS``, before and after the step
function) and the inductive position (``hnf``, at entry), the entry of a
capsule (``evalS_step``), the record of a failure in a capsule
(``RuntimeState::record_failure``) and the end of a capsule on the empty
queue (``allValues_step``).  The checker reads the state without changing
it: the union-find without path compression, the fingerprints without the
growth of ``check_alloc`` (it enumerates the used bits of the blocks of
the tree), the bindings without the absorption of ``get_binding``.  It
keeps alive, as roots of the collector, every cell it flags and one box of
every capsule it enters, so that the addresses in its tables stay those of
the objects they name (the table of the generators compares addresses
alone and roots nothing); under the MPS collector it also clamps the arena
for the life of the runtime state.  The checks of B1 at a fork cost the
same along a long chain of narrowings, where the Python checker reads
every entry of the fingerprint: the group invariant is read over the ids
the union-find united, the dispatch chain only inside a capsule, and rule
D.2 from a diff of the clone's fingerprint tree against its parent's that
skips the blocks the two share.  The group check rests on an invariant of
``UnionFind``: ``unite`` is the only writer of its data and appends both
ids to the list ``united``, so every member of a group of two or more is
in the list (the collector reads it for the same reason).  A writer that
bypassed ``unite`` would silence the check; ``test_group_invariant_at_fork``
reads the list.  The comparison of the reducts at a write
of rule S.x is skipped for a lone configuration (one queue of one
configuration, no capsule entered), which alone references the redex.  A
private copy of rule N.x whose slot is not a level of the scan is reported
as a violation of X-b' (``copy_spine`` copies the levels of the scan from
the slot down, so such a slot is a defect of the copy, not a case the check
can skip); no program of the suite reaches it.

Where the two checkers differ:

* B2 is checked for the operations the ICurry interpreter of the runtime
  runs: the definitional tree is rebuilt from the bytecode of the
  operation (``BIND_ROOT`` and ``BIND_VAR`` give a variable its position,
  ``COPY_VAR`` an alias, ``STORE_VAR`` a value that is not a position,
  ``CASE_CONS`` and ``CASE_LIT`` the cases) at its first use and kept, so
  an operation the tiered mode swaps to compiled code afterwards keeps its
  tree.  A compiled operation has no bytecode and no tree: under
  ``interpret:off``, and under ``tiered`` for a module loaded from its
  object, the ``hnf`` calls of the generated step functions are counted as
  untracked (``hnf_untracked``), not checked.  A compiled check would need
  the tree from another source: the bytecode kept beside the compiled step
  (the swap clears ``aux`` today), the ICurry of the module handed down
  from the Python side when the flag is on, or a tree table the emitter
  writes into the object.  Under ``interpret:all`` every operation with an
  ICurry body is checked.  The measure, on the 165 known-good goals of the
  test file (one runtime state per goal, ``steps:65536``): under the tiered
  default after the prepare pass of the runner, 411 of 66545 ``hnf`` calls
  are checked (0.6%; the rest are compiled steps and built-ins), under
  ``interpret:all`` 22254 of 66538 (33.4%; the rest are the built-ins of
  ``currylib``, which have no tree on either backend).  A run that checks
  B2 on the C++ backend therefore uses
  ``backend:cxx,checker:true,interpret:all``; the tiered pair exercises
  the compiled steps under the other invariants.
* A replacement by failure has three sources in the C++ runtime, where the
  Python backend has one.  An exempt leaf is one.  A failure at an
  inductive position is a completed step here (``hnf`` forwards the redex
  to the failure and the step returns; the Python backend unwinds, and its
  check never sees the step), and the check accepts it (B2 c names it).
  A return of a reference (``RET_REF``) forwards the redex to the node the
  reference denotes, which may be a failure; the tree tells such a leaf
  from the return of a built node, and the check accepts it (the Python
  backend writes a forward node there, which its check never sees).
* The write of rule S.x is a write into the slot of the variable
  (``*slot = genexpr``), not a copy of the spine, so the check is the
  memo's X-b (Inst-slot): the reduct of every configuration that references
  the redex is read before the write and compared after it, and no flags
  propagate (no cell is made).  The slot write of a generator that exists
  already (the ``has_generator`` branch of ``replace_freevar``, unhooked in
  the Python backend) is checked the same way (``slot_writes`` in the
  counts).  The reduct of a configuration with a binding of the variable
  reads the generator choice of the variable as the binding, as it reads
  the variable itself: the fork applies the binding to the generator.
* The configurations whose reducts are compared are those of the queues of
  the dispatch chain and of the capsules their graphs reach (the SetEval
  nodes the walk meets), not every queue the collector registers: the
  registry also holds the queues of other evaluations and of unloaded
  interpreters, whose nodes this evaluation must not read.  A capsule
  reachable from a yielded value alone is not read.
* The reduct of a variable without a generator of its own, decided through
  its group, is the generator of the representative of the group: that is
  the node the runtime puts into the copy of rule N.x (``get_generator``
  reads it by the group id), where the Python backend clones a generator
  for the variable first.
* The private copies that a set function makes for a configuration
  (``evalS_step``, the clone of a capsule) are not checked on either
  backend; the ``escape_all`` flag the Python checker reads is never set
  by the C++ runtime.

One false alarm was shared by the two checkers, found in the review of the
C++ mirror and fixed on 2026-10-09.  The step propagation of the flags was
a no-op on both backends: the walk started at the redex, which carries the
flags, and stopped there, so a cell a step made at a flagged redex
inherited nothing (the pull-tabs, the copies and the generators
propagated).  The consequence: a boxed argument whose evaluation outside
the box, after the capsule started, creates a choice got a false report of
S0 (E in A) at the pull-tab across the box, on both backends.  The program
(``lazyThenOutside2`` of the test files)::

   g2 n = case n of { 1 -> Just (A ? B); _ -> Nothing }
   f2 x = 0 ? (case x of Just y -> case y of { A -> 1; B -> 2 })
   lazyThenOutside2 = let a = g2 (length [()]) in
     let vs = valuesOf (set1 f2 a) in (head vs, fromJust' a, vs)

The capsule yields 0 without demanding ``a``; the enclosing configuration
steps ``g2`` at the flagged cell, then ``?``, whose choice carried the tags
of the boxes above it and the flags of the ``?`` cell, which were none; the
second alternative of the capsule pulls the choice across the box.  The
runtime gives ``(0, A, [0, 1])`` and ``(0, B, [0, 2])``, the values of
weakly encapsulated search.  The walk of a step starts at the successors
of the result cell now (``Checker::step_end`` propagates from the result,
when the step forwarded the redex to a fresh cell, and from each successor
of the result, under the budget of one walk; ``Checker.step`` propagates
from the successors of the node), so the ``?`` cell inherits the flags of
the redex of ``g2`` and the choice is argument-derived for the box.
``TestSharedArgument`` of both test files pins the values under the
checker on three shapes (``lazyThenOutside2``, ``twoCapsulesChoice2`` with
two capsules over the argument, ``capturedThenShared2`` with the argument
captured by a second set function), and the known-good goals of both files
report nothing with the same counts as before.

The walk of a step is bounded by 1024 cells.  A step whose result holds
more cells than that (``bigThenOutside`` of the test files: the step of
``gBig`` builds a list of 100 elements of about 23 cells each) leaves the
far cells without the flags, so a choice made there outside the box
carries no tag, and the pull-tab across the box would be reported.  A walk
over its budget therefore makes the sets of the flags unbounded, as the
entry walk does: the event is counted (``propagate_over_budget``) and the
checks of S0 of those sets are suppressed from then on.  The budget is a
policy of the instrumentation, not of the invariants.

``tests/unit_cxx_checker.py`` runs the known-good programs under the
checker, compiled and under ``interpret:all``, with the values and the
counters they have without it, and provokes one violation per check
through the debug entry points of the bindings
(``cyrtbindings.checker_debug_*``), which corrupt one configuration of a
runtime state on purpose or run one check on constructed nodes; the
entries refuse while the flag is off.  ``cyrtbindings.checker_counts``
gives the counts of the events a state saw.

The removal gate
----------------

Stage 6 of issue #82.  When the unit and functional suites pass under
``interpret:off``, ``tiered`` and ``all`` on the C++ backend for a month of
nightly runs, and no open bug names the Python backend as its only
reproduction, the source of the backend (``src/python/backends/py``), its
tests (the ``unit_py_*`` files, and the tests that skip or expect a failure
on one backend), its CI job and the value ``py`` of the flag go in one
commit; the issue records the date.  The month started with the first
nightly run after the merge of stages 1 to 4.  Examples 03 and 04 and the
Python form of ``curry.save`` follow the decision on the C++ form.

The depth bounds of the toolchain
=================================

A deep expression, such as the nest of cons calls of a long literal list
or a chain of nested if-then-else, met a recursive walk at every stage of
an import.  Issue #125 made the walks of the route from Curry to ICurry
iterative (``utility.trampoline`` and explicit stacks), and pothole batch 4
(2026-10-10) the walks of the import after it: the visitor of the
optimizer (``icurry.visit``), the copy of a function body and the other
walks over an expression in the inliner (``icurry.analysis.inlining``;
``copy.deepcopy`` of a call or a choice copies the nested calls and
choices on a stack of its own), the rewrite of the saturation pass
(``interpreter.optimize``) and the expression compiler of both backends
(``backends.generic.compiler.compileE``).  A literal list of 10800
elements imports and runs on both backends under ``interpret:new``
(``tests/unit_curry2icurry.py``, ``TestDeepExpressions``; about 9 s on
the C++ backend).  What still bounds a deep expression, as measured on the
machine of that lane:

* The JSON codec of the ICurry (``icurry.json``) recurses in C, in the
  codec of Python.  A nest of 12000 calls is written and read back; one of
  15000 overflows the 8 MB stack of the main thread (``RecursionError``,
  "Stack overflow").  The bound is a bound in levels of nesting of the
  ICurry, not in frames of Python, so ``maxrecursion`` does not move it; a
  thread with a larger stack, or a codec without the recursion, would.

* The monadic analysis (``icurry.analysis.monadic``) follows the call
  graph: a chain of nested if-then-else lifts into a chain of functions,
  one per level, and the analysis recurses once per function, four frames
  per level (``set_monadic_metadata``, ``visit``, the visitor and
  ``_checkmonadic``; 506 levels under a limit of 2048 frames), so about
  4000 levels under ``maxrecursion`` (16384 frames; about 680 before the
  visitor was made iterative).  The time of the case lifting of the port
  bounds such a chain first: it is quadratic in the chain, 74 s of the
  118 s of the import of a chain of 2000 levels; a chain of 3500 levels
  imports in 255 s.

* The hoisting depth of the Python backend, ``HOIST_DEPTH`` of
  ``backends.py.compiler`` (64): the parser of Python refuses more than
  200 nested parentheses, and a node of the generated code is one call,
  so a subexpression at that nesting under its statement goes into a
  temporary of the step function.  The C++ backend hoists nothing; g++
  accepts the nested call of a list of 1200 elements (19 s, 794 MB).