Non-boolean inputs constrained

The check is nonbool_inputs_constrained. It is SPEC-stage plus audit. Severity is warning. The hop reads every variable with direction: input or direction: mode whose type is not bool, in a component that already has at least one active FRETish-formalized requirement. It does not rewrite the YAML. It does not call Z3. It does not call Kind2.

It fires when that variable carries no domain model. The accepted forms are the same extraction proof gaps uses, so the check and the enumeration cannot drift. A pass is one of: the variable's own range: block with both min and max; a sibling data_constraint whose variable: field or parameter list names it; or a domain.tables enum input that names it with declared values. Plain type: enum has no values field of its own. An unbounded string is a finding for the same reason: nothing can enumerate it.

Variables marked proof_auxiliary: true are exempt, with a mandatory reason. Their constraints are still consumed by proof gaps for boundary derivation. A code comment proof:domain-exempt: next to an incidental in-code compare is the per-line opt-out, matched by compare text, with a reason of at least 16 characters. A blank marker does not suppress.

This check asks you to model the domain of variables the requirements already name. It is never satisfied by declaring a new variable. Adding one to make the count look better trades a warning here for a variable orphans clean error there.

This is not a contradiction finding. A parseable, satisfiable, fully traced shall can still leave the gram input with no range. The help file teaches that first.

# shipping.vars.yaml
#   total_weight_g: int, direction input
#   no range, no data_constraint, no table
#
# two shalls cover 0..1000 and 1001..5000
# nothing names 5001
#
# proof audit --check nonbool_inputs_constrained
# [SPEC] nonbool_inputs_constrained
# 1 of 1 non-bool input/mode variables
# across 1 formalized component
# carry no domain model
# silent domain: last VALID still on two bands

The fix is on the model, not on another test. Declare the domain the input actually has. A ranged int is enough when the contract is a closed interval. A sibling data_constraint is the form when the bands are partitioned. A domain.tables input is the form when the values are an enum. Then proof gaps can sample the boundaries, including 5001.

proof audit --check nonbool_inputs_constrained --verbose
proof help domain-modeling
proof gaps specs/system shipping

The teaching graph is still one shipping component whose two bands sat on an unconstrained total_weight_g. Close it by writing range: {min: 0, max: 5000}, or a sibling data_constraint that names the variable, or a table input with declared values. Do not add a spare variable to look covered. Do not waive the hop with a one-word reason. With no domain the hop still fires, and 5001 did not go anywhere. It just stayed invisible.

# shipping.vars.yaml now names the domain
#   total_weight_g: int, direction input
#   range: {min: 0, max: 5000}
#
# proof audit --check nonbool_inputs_constrained
# 0 unconstrained non-bool inputs. this hop is quiet
#
# proof gaps specs/system shipping
# now samples 0, 5000, and the ±1 neighbors

An unconstrained output while Kind2 still printed realisable stays on gaps clean. A description that named a domain no variable models stays on solver modeling opportunity. A load-bearing compare on the implements function stays on code predicates modeled. Jama still authors. Proof vs Jama.

Warning, not fail on its own. Auxiliary and domain-exempt are silence with a reason, not a proof that 5001 is safe. A missing pin is not this hop. The hop does not rewrite the YAML. It does not add a variable. It does not prove the Go. It does not run the gap matrix; that is proof gaps. Combined enumeration is capped at 4096 states by default, boundaries first. A quiet hop is not a proof that the model is enough, only that every collected non-bool input or mode was constrained or exempted. We have not scored this floor against a frozen Jama pack or a ReqIF export. The loss is named, not scored.

The unconstrained-output hop stays on gaps clean. The description-domain hop stays on solver modeling opportunity. The implements-compare hop stays on code predicates modeled. The partition hop stays on data constraints complete. The engagement stays on software correctness audit. Jama still authors.

What is non-boolean inputs constrained? Same question. Same URL.

Is this gaps clean? No. That hop is an unconstrained output while Kind2 still printed realisable. This hop is a non-bool input or mode with no domain. See gaps clean.

Is this data constraints complete? No. That hop is whether authored constraint groups already cover without overlap. This hop is whether any domain model exists. See data constraints complete.

Is this solver modeling? No. That hop is a description that named a domain no variable models. This hop is a variable you already declared. See solver modeling opportunity.

Is this code predicates modeled? No. That hop is a load-bearing compare on the implements function. This hop is the spec-side input. See code predicates modeled.

Is this domain modeling? No. Ads 880 on that string is DDD. Ads 720 on data domains is warehouse glossary. Neither is this check.

Does a domain-exempt comment prove 5001 is safe? No. It names why the compare is not a spec domain. The hop still counts it in the summary.

Does a quiet hop prove the code matches the shall? No. The hop observes declared non-bool inputs against range, constraint, and table. It does not prove the Go.

Is Proof a Jama alternative for the shall? No. Jama still authors. Proof vs Jama.