How FCSTM Becomes a Bounded Transition System

Bounded model checking (BMC) does not execute an FCSTM one cycle at a time. It allocates one symbolic copy of the control state and persistent variables for every frame, allocates event inputs and case observations for every step, and asks Z3 whether all copies can satisfy one finite formula. This page derives that formula from the data structures in pyfcstm.bmc.relation.

This is an explanation of the relation layer. It does not define FBMCQ syntax, compile a property objective, interpret SAT as a property verdict, or claim an unbounded proof. The relation builder deliberately stops at \(Core_N\); property compilation and witness/replay are later layers.

Start with a small door-latch trace. Suppose a door controller starts with Door.Locked active and latch_engaged=1. A maintenance event opens the door without clearing the latch. At bound 2, the encoded horizon has frames \(F_0,F_1,F_2\) and steps \(0,1\): \(F_0\) is the snapshot before the first encoded cycle, step 0 is the whole runtime cycle from \(F_0\) to \(F_1\), and step 1 is the whole runtime cycle from \(F_1\) to \(F_2\). In this page, step means one FCSTM macro-step: one symbolic edge between neighboring observable frames, including the selected transition and any ordered entry, exit, effect, or during actions executed inside that cycle.

The derivation uses the following sets throughout:

• \(N\) is the query bound; frames use indices \(0..N\), while steps use \(0..N-1\). Example: the door bound \(N=2\) has three frames and two macro-steps.

• \(V\) is the set of persistent FCSTM variables and \(\tau(v)\) is the Z3 sort selected for variable \(v\). Example: latch_engaged is one member of \(V\).

• \(\mathcal{A}\) is the set of fully qualified event paths. Example: Door.MaintenanceOpen contributes one event input per step.

• \(K_i\) is the finite macro-case set expanded for step \(i\). Example: a step may choose the maintenance transition case or a fallback case, but not both.

• \(\mathbb{B}\) is the Boolean domain. \(S_0\) and \(S_{\mathrm{rec}}\) are the legal frame-0 and recurrence state-id sets.

The door trace fixes the vocabulary. The next table uses a checked-in concrete trace with small numeric values so the formulas can be audited without long code. Section 1 then replaces each concrete observation with the symbolic families that Z3 actually solves.

A concrete trace used by every section

The checked-in FCSTM model has one event, three persistent variables, and two leaf states. Go takes A to B; the transition adds ten to counter, then the target leaf’s during block adds one. Later idle cycles remain in B and execute that during block.

def int counter = 0;
def float ratio = 0.5;
def int keep = 5;

state Root {
    event Go;

    state A;
    state B {
        during {
            counter = counter + 1;
        }
    }

    [*] -> A;
    A -> B : Go effect {
        counter = counter + 10;
    }
}

The bound-three query fixes Go to true at step 0 and false at steps 1 and 2.

init state("Root.A");

assume event("Root.Go", 0) == true;
assume event("Root.Go", 1..2) == false;

check reach <= 3: active("Root.B");

Building BmcEngine(model).prepare(query) and then build_bmc_core_formula(context) yields SAT. Reading the Z3 model gives the following actual relation trace; state ids 1 and 2 denote Root.A and Root.B in this model.

Bound-three relation trace

Frame/step	Control state	counter	ratio	keep	Root.Go	Selected case	\(\Delta_i / \Gamma_i\)
\(F_0 / E_0\)	Root.A (1)	0	\(1/2\)	5	true	transition	false / false
\(F_1 / E_1\)	Root.B (2)	11	\(1/2\)	5	false	fallback	false / true
\(F_2 / E_2\)	Root.B (2)	12	\(1/2\)	5	false	fallback	false / true
\(F_3\)	Root.B (2)	13	\(1/2\)	5	n/a	n/a	n/a

The first row is worth reading carefully: a bound of three means four frames but only three event slots. Also, counter becomes 11, not 10, because the macro step preserves runtime ordering through the target leaf’s first during action. The runtime-alignment tests independently check the same ordering boundary.

1. Allocate the symbolic trace

Frames

Each frame is a control-state symbol paired with a valuation of every persistent variable. Frame 0 may use the initial-source domain; later frames use the recurrence domain.

(1)\[\begin{split}\mathcal{F}_N=(F_i)_{i=0}^{N},\qquad F_i=(s_i,\nu_i)\in S_i\times\prod_{v\in V}\tau(v),\qquad S_i=\begin{cases}S_0&i=0,\\S_{\mathrm{rec}}&1\le i\le N,\end{cases} \qquad |\mathcal{F}_N|=N+1.\end{split}\]

BmcTraceSymbols.allocate creates F_i_state and one mapping of variable symbols per frame. BmcTraceSymbols.__post_init__ rejects any bundle whose frame-state or frame-variable tuple does not contain exactly bound + 1 entries. test_core_formula_constrains_initial_state_and_variable_initializers anchors the values at frame 0. The working trace therefore contains exactly \(F_0,F_1,F_2,F_3\).

Counterexample: treating bound 3 as three frames discards \(F_3\) and changes the meaning of reach <= 3. It is an off-by-one error, not an alternative notation.

Event inputs

Events belong to the edge from \(F_i\) to \(F_{i+1}\), so no event vector exists after the final frame.

(2)\[\mathcal{E}_N=(E_i)_{i=0}^{N-1},\qquad E_i=(e_{i,a})_{a\in\mathcal{A}}\in\mathbb{B}^{|\mathcal{A}|},\qquad |\mathcal{E}_N|=N,\qquad |\{e_{i,a}\}|=N|\mathcal{A}|.\]

The allocator loops over domain.steps and domain.events, creating one Boolean E_i_event_* per pair. test_event_selector_star_and_ranges_lower_to_each_selected_cycle shows that a bound-three query has event indices 0, 1, and 2. In the working trace these values are true, false, false.

Counterexample: \(E_3\) is not an unconstrained final input; it does not exist. Any response or assumption calculation that reads it has moved beyond the encoded horizon.

Persistent-variable families

The frame tuple is materialized as a distinct symbol family for each persistent variable. Integers use z3.Int and FCSTM floats use z3.Real.

(3)\[X_v^N=(x_{i,v})_{i=0}^{N}\in\tau(v)^{N+1}\quad(v\in V),\qquad |\{x_{i,v}\mid 0\le i\le N,\ v\in V\}|=(N+1)|V|.\]

The example has three families and twelve variable symbols: four integer counter symbols, four real ratio symbols, and four integer keep symbols. The initializer test checks both integer and real values, while the case-relation test checks that an unwritten variable is carried.

Counterexample: temporary action variables are not members of \(V\) and must not receive frame families. test_relation_temporary_variables_do_not_enter_post_var_pool freezes this boundary.

Selectors and progress observations

Each expanded macro case receives a selector. Two additional observations exist for every step: \(\Delta_i\) for a semantic-delta case and \(\Gamma_i\) for a stable fallback case.

(4)\[\mathcal{C}_N= \{C_{i,k}\mid 0\le i<N,\ k\in K_i\} \cup\{\Delta_i,\Gamma_i\mid 0\le i<N\},\qquad C_{i,k},\Delta_i,\Gamma_i\in\mathbb{B},\qquad |\mathcal{C}_N|=\sum_{i=0}^{N-1}|K_i|+2N.\]

allocate receives the actual case labels produced for each step, checks label uniqueness, and creates C_i_*. The working trace has two cases at step 0 and four recurrence cases at each later step; only the transition selector is true at step 0 and only the Root.B fallback selector is true at steps 1 and 2.

Counterexample: selectors are observations bound to antecedents. Their mere allocation does not prove that a malformed upstream macro partition is exactly-one; macro expansion owns that invariant.

2. Restrict the legal frames and initial frame

Control-state domain

The allocation type only says that \(s_i\) is an integer. \(D_N\) turns that integer into a valid BMC state id, with a potentially wider domain at frame 0 than at recurrence frames.

(5)\[D_N=\left(s_0\in S_0\right)\land \bigwedge_{i=1}^{N}\left(s_i\in S_{\mathrm{rec}}\right),\qquad (s_i\in S)\equiv\bigvee_{q\in S}(s_i=q).\]

_relation_frame_domain derives both sets, and _build_domain_formula emits the disjunction for every frame. In the working model, the printed formula admits the initial sentinel and model states at \(F_0\), but only the terminate sentinel and stable leaves at later frames.

Counterexample: an arbitrary integer such as 999 cannot be used as a cheap unknown state. Conjoining \(s_1=999\) with (5) is UNSAT.

Initial control

The query’s initial mode selects one concrete source id. It is not left as a choice inside the solver.

(6)\[\begin{split}I_0^{\mathrm{ctrl}}\equiv s_0=\operatorname{src}(m),\qquad \operatorname{src}(m)= \begin{cases} \mathrm{STATE\_INIT}&m=\mathrm{cold},\\ \operatorname{id}(p)&m=\mathrm{state}(p),\\ \mathrm{STATE\_TERMINATE}&m=\mathrm{terminated}. \end{cases}\end{split}\]

_initial_source calls source_from_initial_spec and checks the bound state id against the resolved source. _build_initial_formula then emits the equality. The working query uses state("Root.A"), hence \(s_0=1\). Tests separately cover default cold start and terminated start.

Counterexample: init state("Root.A") does not execute the cold-entry path before \(F_0\); it establishes a hot initial control state. Confusing the two can replay entry effects that the query did not request.

Retained initializers

Let \(H\) be the query’s havoc set. Every persistent variable outside \(H\) retains its model initializer, including its runtime-definedness conditions.

(7)\[I_0^{\mathrm{ret}}(H)= \bigwedge_{v\in V\setminus H} \left(\operatorname{Def}(\operatorname{init}_v(\nu_0))\land x_{0,v}=\operatorname{init}_v(\nu_0)\right).\]

_build_initial_formula translates each non-havoc model initializer against the frame-0 environment, appends its domain constraints, then appends the equality. The working trace therefore fixes counter=0, ratio=1/2, and keep=5. test_core_formula_constrains_initial_state_and_variable_initializers proves these equalities by making their negations UNSAT.

Counterexample: a division-by-zero initializer is not silently assigned an arbitrary value. Without havoc its definedness conjunct makes the core UNSAT.

Havoc removes initializer equalities

Havoc changes the set of initializer conjuncts; it does not create a second assignment or a magic value.

(8)\[\operatorname{Conj}\!\left(I_0^{\mathrm{ret}}(H)\right)= \operatorname{Conj}\!\left(I_0^{\mathrm{ret}}(\varnothing)\right) \setminus \left\{\operatorname{Def}(\operatorname{init}_v(\nu_0)), \ x_{0,v}=\operatorname{init}_v(\nu_0)\mid v\in H\right\}.\]

The implementation literally skips the initializer translation when a name is in havoc_names. test_initial_havoc_variable_skips_initializer_but_where_constrains_frame0 shows the important consequence: a havoced x may be fixed to 7 by where x == 7, while a retained variable still equals its initializer.

Counterexample: “havoc means unconstrained” is too strong. It means “unconstrained by the model initializer”; \(D_N\), where, assumptions, and transition relations may still constrain that symbol.

The initial where predicate

The optional where expression is evaluated at frame 0 and conjoined with control and retained-variable constraints. Its own definedness is mandatory.

(9)\[\begin{split}I_0=I_0^{\mathrm{ctrl}}\land I_0^{\mathrm{ret}}(H)\land \begin{cases} \operatorname{Def}(W(F_0))\land W(F_0)&\text{if a where predicate }W\text{ is present},\\ \top&\text{otherwise}. \end{cases}\end{split}\]

_lower_bmc_cond_expr(..., frame_index=0) produces the value and domain constraints. test_initial_where_without_havoc_keeps_initializer_and_can_be_unsat uses an initializer and contradictory where to make \(I_0\) UNSAT.

Counterexample: where is not a macro-case guard. It constrains \(I_0\) only; test_initial_where_only_constrains_i0_not_macro_case_partition checks that no case label contains or re-expands it.

3. Lower each macro case

Case antecedent

For case \(k\) at step \(i\), macro expansion has already assembled a Boolean template from event atoms, transition guards, priority masks, and any accepted-case dependencies. Relation lowering combines that condition with the source-state equality. The formula below names the condition only; its runtime-definedness is carried by (12) so a total Z3 division cannot hide a runtime division-by-zero.

(10)\[A_{i,k}\equiv \left(s_i=\operatorname{src}(k)\right)\land Q_{i,k}\!\left(F_i,E_i,(A_{i,j})_{j\prec k}\right).\]

_lower_bool_template maps event atoms to \(e_{i,a}\), guard atoms to lowered guard terms, and accepted atoms to recursively lowered earlier antecedents. _build_case_relation adds the source guard. The working step-0 transition antecedent is true because \(s_0\) is Root.A and Root.Go is true.

Counterexample: a true Go input cannot activate an A -> B case when \(s_i\) is B. Event truth alone omits the source-state conjunct.

Selected-case definedness

A selected case must be executable, not merely Boolean-selectable. Let \(\mathcal{D}^{Q}_{i,k}\) be the path-sensitive definedness needed to decide the macro condition \(Q_{i,k}\), including guard atoms reached through priority or accepted-case dependencies. Let \(\mathcal{D}^{R}_{i,k}\) be the definedness accumulated while symbolically executing the selected case’s ordered action blocks. Their union is the selected-case definedness payload. The exact union and conjunction are defined alongside the guarded relation in (12).

Example: if the door maintenance case has guard latch_engaged / y > 0 and \(y=0\), then \(\mathcal{D}^{Q}_{i,k}\) contains \(y\ne0\). If its effect writes latch_engaged = 1 / 0, then \(\mathcal{D}^{R}_{i,k}\) contains \(0\ne0\). Either conjunct makes the selected case UNSAT; an unselected case does not impose that conjunct on the current step.

Selector equivalence

The public case selector is exactly an observation of the antecedent, in both directions.

(11)\[C_{i,k}\leftrightarrow A_{i,k}.\]

The code is the Z3 equality selector == antecedent. The case-relation test constrains Go false and proves the fallback selector cannot be arbitrarily flipped when its antecedent is false; canonical dumps expose both expressions.

Counterexample: the one-way constraint \(C_{i,k}\Rightarrow A_{i,k}\) would allow \(A_{i,k}\) to be true while the selector remains false. That would corrupt case coverage and call-count observations even if the post-state implication still fired.

Guarded case relation

The postcondition belongs under an implication. An unselected case must not write its target state or variables. Let \(\mathcal{D}_{i,k}\) contain every runtime-definedness condition accumulated while lowering the case’s guards and ordered action blocks. Those conditions are part of the selected case’s postcondition, not optional diagnostics.

(12)\[\begin{split}\begin{aligned} \mathcal{D}_{i,k} &\equiv \mathcal{D}^{Q}_{i,k}\cup\mathcal{D}^{R}_{i,k},\\ \operatorname{DefCase}_{i,k} &\equiv \bigwedge_{d\in\mathcal{D}_{i,k}}d,\\ T_{i,k} &\equiv \left(C_{i,k}\leftrightarrow A_{i,k}\right)\land \left(A_{i,k}\Rightarrow \left(R_{i,k}\land\operatorname{DefCase}_{i,k}\right)\right). \end{aligned}\end{split}\]

BmcCaseRelation.formula is the conjunction shown above. test_case_relation_uses_implication_not_global_and_and_carries_vars fixes Go true and obtains the transition target, then fixes it false and obtains the fallback target. The separate runtime-alignment suite checks transition effects against SimulationRuntime. _lower_bool_template contributes \(\mathcal{D}^{Q}_{i,k}\) for condition and accepted-case guard definedness, _prepare_case_lowering contributes \(\mathcal{D}^{R}_{i,k}\) for ordered action execution, and _build_case_relation appends the resulting \(\operatorname{DefCase}_{i,k}\) constraints to consequent. For example, a selected transition effect x = 1 / 0 contributes \(0\ne0\); because \(0\ne0\) is false, \(A_{i,k}\Rightarrow(R_{i,k}\land\operatorname{DefCase}_{i,k})\) cannot be satisfied when \(A_{i,k}\) is true. The selected case, and therefore that attempted execution, is UNSAT. The same impossible operation in an unselected case does not constrain the step because the conjunction remains under the implication.

Counterexample: replacing the implication with a global conjunction \(A_{i,k}\land R_{i,k}\) would require every expanded case to be selected simultaneously, usually making the step UNSAT. Omitting \(\mathcal{D}_{i,k}\) is also unsound: Z3 could assign an arbitrary value to a partial arithmetic operation and manufacture a transition that the runtime cannot execute.

Post-control write

Every selected case has one expanded target id. This includes stable leaves, the init sentinel for a delta stutter, and the terminate sentinel.

(13)\[R_{i,k}^{\mathrm{ctrl}}\equiv s_{i+1}=\operatorname{tgt}(k).\]

_build_case_relation makes this the first post constraint. The working transition writes Root.B to \(s_1\); the runtime-alignment test proves that asking for any other state id is UNSAT under Go.

Counterexample: the target is not derived merely from the FCSTM transition endpoint at this layer. Macro expansion may resolve pseudo-state descent and termination before relation lowering, so bypassing case.target_state_id loses that semantics.

Written variables

Actions are executed symbolically in runtime order. For the set \(W_k\) of variables changed by case \(k\), the final symbolic environment becomes the next-frame value.

(14)\[R_{i,k}^{\mathrm{write}}\equiv \bigwedge_{v\in W_k} \left(x_{i+1,v}=\operatorname{Eval}_v(\operatorname{ops}_k,\nu_i)\right).\]

_prepare_case_lowering and _execute_action_block build final_env; _build_case_relation writes every resulting expression to frame \(i+1\). In the working trace, transition effect +10 followed by the target during action +1 gives \(x_{1,\mathrm{counter}}=11\). test_relation_exit_effect_enter_order_matches_simulation_runtime similarly freezes exit, transition-effect, and enter order as 5 + 10 + 2 = 17.

Counterexample: lowering action blocks as an unordered set is unsound whenever two blocks write the same variable. The later expression consumes the earlier symbolic result.

Unwritten-variable carry

The symbolic executor starts from the current frame environment. A variable that no action changes therefore retains its incoming expression.

(15)\[R_{i,k}^{\mathrm{carry}}\equiv \bigwedge_{v\in V\setminus W_k}\left(x_{i+1,v}=x_{i,v}\right).\]

The implementation does not need a separate carry loop: final_env still maps an unwritten name to its \(F_i\) symbol, and the common post-write loop emits the equality. keep and ratio remain 5 and \(1/2\) through all four working frames. The core test explicitly makes keep inequality UNSAT.

Counterexample: leaving an unwritten post variable unconstrained invents nondeterministic state that neither FCSTM nor SimulationRuntime has.

4. Assemble one step and the bounded transition relation

Fallback cases

Fallback is an explicit expanded case, not an implicit “do nothing” inserted after solving. Its condition contains the negation of earlier accepted transition cases, and it may execute during actions.

(16)\[T_i^{\mathrm{fb}}\equiv \bigwedge_{k\in K_i^{\mathrm{fb}}} \left[\left(C_{i,k}\leftrightarrow A_{i,k}\right)\land \left(A_{i,k}\Rightarrow \left(R_{i,k}\land\operatorname{DefCase}_{i,k}\right)\right)\right],\qquad A_{i,k}\Rightarrow\bigwedge_{j\prec k}\neg A_{i,j}.\]

_build_step_relation lowers fallback cases exactly like other cases, including \(\operatorname{DefCase}_{i,k}\). test_relation_fallback_negates_failed_guard_and_runs_during sees the negated accepted atom and observes the during update. Working steps 1 and 2 select the Root.B fallback and increment counter. Short example: if a prior transition guard needs x / y and \(y=0\), the fallback cannot use that undefined guard as evidence that the transition simply failed; the selected fallback inherits the guard definedness and the step is UNSAT.

Counterexample: fallback does not necessarily stutter every variable. In the working model it changes counter on each idle cycle; only ratio and keep carry.

Terminated absorption

Termination is absorbing. The absorb case also rejects all later event input and carries persistent variables.

(17)\[s_i=\mathrm{STATE\_TERMINATE}\Rightarrow \left(s_{i+1}=\mathrm{STATE\_TERMINATE}\right)\land \bigwedge_{a\in\mathcal{A}}\neg e_{i,a}\land \bigwedge_{v\in V}\left(x_{i+1,v}=x_{i,v}\right).\]

_recurrence_formals expands terminated_source; the absorb branch in _build_case_relation appends every negated event input. The terminated tests check state absorption, variable carry, and UNSAT when an event is forced true after termination.

Counterexample: allowing events after termination would create inputs that the runtime cannot consume and would make witness event accounting disagree with replay.

Delta, fallback, and mutual exclusion

The two progress observations are exact disjunctions of their respective case antecedents. They are also explicitly mutually exclusive.

(18)\[\Delta_i\leftrightarrow\bigvee_{k\in K_i^{\delta}}A_{i,k},\qquad \Gamma_i\leftrightarrow\bigvee_{k\in K_i^{\mathrm{fb}}}A_{i,k},\qquad \neg(\Delta_i\land\Gamma_i).\]

_build_step_relation emits these three constraints after all case relations. A cold source blocked on a required event selects a delta and stutters; a stable leaf with no transition selects fallback and may run during. test_cold_no_progress_delta_stutters_state_and_vars and test_stable_leaf_fallback_gamma_commits_during_actions freeze the contrast.

Counterexample: \(\Delta_i\) does not mean “no event input”, and \(\Gamma_i\) does not mean “no variable changed”. They classify expanded case semantics, not raw vector equality.

All steps

One step conjoins every case formula and the observation constraints; the bounded transition formula conjoins all \(N\) steps.

(19)\[T_i=\left(\bigwedge_{k\in K_i}T_{i,k}\right)\land \left(\Delta_i\leftrightarrow\bigvee_{k\in K_i^{\delta}}A_{i,k}\right)\land \left(\Gamma_i\leftrightarrow\bigvee_{k\in K_i^{\mathrm{fb}}}A_{i,k}\right)\land \neg(\Delta_i\land\Gamma_i),\qquad T_N=\bigwedge_{i=0}^{N-1}T_i.\]

build_bmc_core_formula builds each BmcStepRelation and conjoins its formula. The working bound produces \(T_0\land T_1\land T_2\), which links four frames. The bound-two termination test confirms that recurrence formals, including absorb, are used after the initial step.

Counterexample: conjoining only \(T_0\) in a bound-three query leaves \(F_2\) and \(F_3\) disconnected from execution even if their state ids still satisfy \(D_N\).

5. Add environment assumptions and freeze the core

Environment assumptions

Let \(\mathcal{H}_F\) contain frame assumptions as a frame-index set and predicate pair; \(\mathcal{H}_E\) contain fixed event literals; and \(\mathcal{H}_{\le1}\) contain event pools subject to at-most-one on every step. any contributes no cardinality conjunct.

(20)\[ENV_N= \bigwedge_{(J,p)\in\mathcal{H}_F}\ \bigwedge_{i\in J} \left(\operatorname{Def}(p(F_i))\land p(F_i)\right) \land \bigwedge_{(J,a,b)\in\mathcal{H}_E}\ \bigwedge_{i\in J} \left(e_{i,a}=b\right) \land \bigwedge_{B\in\mathcal{H}_{\le1}}\ \bigwedge_{i=0}^{N-1} \operatorname{AtMostOne}\!\left((e_{i,a})_{a\in B}\right).\]

_build_environment_formula expands always to frames 0 through \(N\), lowers at to its one frame, applies resolved event selectors, and calls z3.AtMost for an explicitly requested pool. The working \(ENV_3\) is simply Go_0 and not Go_1 and not Go_2. Environment tests prove both frame ranges and event ranges.

Counterexample: there is no implicit global at-most-one policy. Two distinct events may both be true in one step unless the query requests cardinality at_most_one; the environment tests check both SAT and UNSAT forms.

The core formula

The relation layer’s final operation is conjunction. It neither adds nor interprets the property objective.

(21)\[Core_N=D_N\land I_0\land T_N\land ENV_N.\]

build_bmc_core_formula constructs the four named fields in this order and stores their conjunction in BmcCoreFormula.core. The core tests inspect the canonical node and prove consequences by adding a negated expected value to \(Core_N\) and obtaining UNSAT. Property compilation later forms a separate solve formula from this core and an objective.

Counterexample: UNSAT of \(Core_3\) means that no length-three encoded trace satisfies these initial and environment constraints. It does not prove that the model has no trace at larger bounds, and it is not an unbounded model checking theorem.

Formula ledger and review anchors

The table is the forward audit map for the frozen equations on this page. Function names refer to pyfcstm/bmc/relation.py; tests are repository-local semantic regressions, while the downloadable files above are independent documentation resources.

Frozen relation-equation ledger

Equation	Implementation anchor	Test anchor	Working evidence
(1)	BmcTraceSymbols.allocate	test_relation_core.py initial/core tests	Four frames at bound 3
(2)	BmcTraceSymbols.allocate	test_relation_environment.py selector-range test	Three Go slots
(3)	BmcTraceSymbols.allocate	test_relation_core.py initializer/carry tests	Three families, twelve symbols
(4)	BmcTraceSymbols.allocate	test_relation_core.py case/progress tests	Transition then two fallbacks
(5)	_build_domain_formula	test_relation_core.py domain consequences	State ids 1, 2 only on shown trace
(6)	_build_initial_formula	cold/hot/terminated initial tests	Root.A at frame 0
(7)	_build_initial_formula	initializer type/value test	0, \(1/2\), 5
(8)	_build_initial_formula	havoc/where tests	Counterexample described above
(9)	_build_initial_formula	contradictory where test	Frame-0-only constraint
(10)	_build_case_relation	semantic fixture and priority tests	A plus Go at step 0
(11)	_build_case_relation	selector truth checks	One selected label per shown step
(12)	_lower_bool_template / _prepare_case_lowering / _build_case_relation	implication, definedness, and runtime-alignment tests	Selected-case-only writes; undefined selected case is UNSAT
(13)	_build_case_relation	event transition alignment test	Root.A to Root.B
(14)	_build_case_relation	action-order alignment tests	counter 0 to 11
(15)	_build_case_relation	unwritten carry test	ratio and keep unchanged
(16)	_build_step_relation	fallback runtime-alignment test	Idle B increments
(17)	_build_step_relation / absorb branch	terminated/event rejection tests	Forged post-termination event is UNSAT
(18)	_build_step_relation	delta/gamma contrast tests	false/true on idle B
(19)	_build_step_relation and core builder	bound-two recurrence test	Three linked steps
(20)	_build_environment_formula	frame/event/cardinality tests	true, false, false event vector
(21)	build_bmc_core_formula	test_relation_core.py	SAT complete prepared query

Reviewing the page therefore has two distinct parts. Sphinx can verify that all (21)-style references resolve, and a bilingual drift check can compare labels and literal LaTeX. Neither check proves the semantic claims: a reviewer must still compare every row with the named code, test, and working trace.