Verify

Requires the verify extra (pip install "longeron[verify]") for the Hypothesis-driven tiers; cover and prove reach Z3 through the bundled smt extra, and every tier degrades to recorded gaps where an engine is missing.

Model-driven requirement-violation hunting: the model fights back.

Everything a property-based tester needs is already declared in the .sysml text: attribute types give value domains, assert constraint bodies give minable ranges, assume/require constraints give the universal property assumptions-hold implies requirements-satisfied, state machines give the event alphabet, and variation catalogs give the discrete factors. This module derives all of it, hunts, shrinks, proves, and materializes every catch as re-checkable M0 individuals.

Four tiers over ONE oracle – the interpreter. Every verdict, in every tier, comes from instantiate + check + check_requirement (or simulate for sequences), never from a solver’s arithmetic; solvers propose, the interpreter decides (the same honesty contract longeron.analysis.trades keeps):

• hunt() – Hypothesis sampling + shrinking: is there a simple violating configuration? Strategies are derived from the model by the domain ladder (types -> direct constraint mining -> Z3 bounds through the reachability fixed point -> declared fallback), and every shrunk catch is paired with an oracle-bisected boundary.

• sequences() – Hypothesis stateful testing over the real StateMachine: is there a minimal violating event sequence?

• cover() – in-house IPOG-F t-way covering arrays (longeron.analysis._ipog) with Z3 as the constraint engine: which discrete mixes violate, at t-way coverage? Recall is measured against exhaustive ground truth whenever that stays feasible.

• prove() – Z3 over longeron.analysis.smt’s encoding: is violation impossible? Each check is negated one at a time under the assumption set; UNSAT is a proof of absence no sampling can deliver, SAT witnesses are re-checked by the interpreter before they are believed, and Optimize attributes exact rational feasibility bounds to the constraints that bind them.

verify() is the umbrella: it dispatches by what the scope is (a state machine runs sequences, an assembly with variation points runs cover, any other part runs hunt + prove where encodable) and returns one Report.

Semantics worth pinning (normative): a violated assume constraint makes a requirement inapplicable – a vacuous pass, never a failure (exactly check_requirement()’s existing contract). A configuration is a violation only when every assumption holds and a require constraint (or an assert constraint on the subject) is actually false. Vacuous outcomes are recorded on every report: a hunt that found only vacuous ground is telling you your assumptions fence off the whole search space – a finding, not a pass.

Determinism policy (ratified): every Hypothesis run uses derandomize=True, database=None, and explicit generate/shrink phases; seeds are accepted and echoed on every report, and reports are reproducible from their own fields alone.

Requires the verify extra: pip install "longeron[verify]" (Hypothesis for hunt/sequences; Z3 arrives via the bundled smt extra for cover/prove and the domain ladder’s third rung – each is imported lazily, and tiers degrade to recorded gaps where an engine is missing).

class longeron.analysis.verify.Boundary(attribute, value, violated)

Bases: object

One oracle-bisected edge: where violated flips along attribute.

class longeron.analysis.verify.Counterexample(bindings=<factory>, events=(), violated=(), source='hunt', selection=<factory>, _materializer=None)

Bases: object

One catch: shrunk bindings, a minimal event sequence, or a bad mix.

materialize()

The catch as an M0 Interpretation of identified individuals, re-checkable with the ordinary check / check_requirement machinery.

Return type:

Interpretation

longeron.analysis.verify.CounterexampleSource

which tier caught a counterexample

alias of Literal[‘hunt’, ‘sequences’, ‘cover’, ‘prove’]

class longeron.analysis.verify.Coverage(t, rows=<factory>, recall=None, exhaustive=None, violated_rows=0)

Bases: object

A covering array’s outcome: rows, and measured recall when feasible.

recall: float | None = None

violated-check recall vs interpreter-exact exhaustive ground truth; None when the exhaustive space was too large to enumerate (the honest guarantee is then: every valid t-tuple covered, violation coverage NOT guaranteed)

class longeron.analysis.verify.Domain(name, kind, lo=None, hi=None, mined_from=<factory>, literals=<factory>, unit=None, fallback=False)

Bases: object

The value domain of one free attribute, as derived from the model.

mined_from records the derivation ladder’s outcome rung by rung (types, mined constraints, Z3-derived assumption bounds, fallbacks), so the report always shows what was derived and what fell back.

unit: str | None = None

declared measurement annotation ([SI::kg]), informational only: unit-aware range derivation is a reserved rung of the ladder

fallback: bool = False

True when at least one side fell to the declared fallback range

class longeron.analysis.verify.Proof(requirement, status, bound='', binding_constraint='')

Bases: object

One negated check’s verdict, with exact bounds where asked.

status is 'proven-safe' (UNSAT: no configuration satisfying every other check and every assumption can violate this one), 'violation' (a SAT witness the interpreter confirmed), or 'unknown' (the solver gave up, or its witness did not survive the interpreter re-check). bound carries the exact rational supremum of a free attribute over the all-checks-hold region, attached to every proof of the query and attributed to binding_constraint – the check whose exclusion moves that bound.

longeron.analysis.verify.ProofStatus

one negated check’s verdict: UNSAT (nothing satisfying every other check and assumption can violate it), a SAT witness the interpreter confirmed, or the solver gave up / its witness did not survive the re-check

alias of Literal[‘proven-safe’, ‘violation’, ‘unknown’]

class longeron.analysis.verify.Report(scope, status='clean', violations=<factory>, counterexamples=<factory>, proofs=<factory>, vacuous=<factory>, domains=<factory>, gaps=<factory>, boundaries=<factory>, coverage=None, seed=None)

Bases: object

The one report shape every tier (and the umbrella) returns.

longeron.analysis.verify.ReportStatus

the whole report’s outcome: nothing found, at least one confirmed violation, or every negated check proven safe (prove only)

alias of Literal[‘clean’, ‘violated’, ‘proven’]

class longeron.analysis.verify.Verdict(bindings, violated=<factory>, vacuous=<factory>, error=None)

Bases: object

One configuration’s outcome under the universal property.

error: str | None = None

set when the oracle itself could not evaluate the configuration (physics outside its real domain: sqrt of a negative mass, …)

property ok: bool

True when nothing applicable failed (vacuous passes count as OK).

longeron.analysis.verify.attribute_domains(interp, defn, free, requirements=())

Value domains for the named free attributes of defn.

The derivation ladder, most specific source first, every rung recorded in Domain.mined_from:

1. attribute types (Real/Integer/Natural/Boolean; enum types become literal lists; Natural adds a >= 0 floor);

2. direct constraint mining – assert constraint bodies comparing the attribute against a literal (unary-minus literals folded), and-conjunctions folded, and constraints nested in a case’s objective included (the spec’s home for assume bounds);

3. Z3-derived bounds through smt’s reachability fixed point, under the assumption set (bounds that live only on derived attributes are found here);

4. the declared fallback (applied by strategies_for(), flagged).

A reserved rung (unit-aware ranges from the model’s measurement annotations) records the declared unit informationally only.

Return type:

dict[str, Domain]

longeron.analysis.verify.bisect_boundary(predicate, lo, hi, tol=1e-09)

The threshold where predicate flips from False (at lo) to True (at hi) – refine a shrunk counterexample to the exact edge, against the same oracle that produced it.

Return type:

float

longeron.analysis.verify.counterexample_values(counterexample)

A values= dict for the scoreboard from a materialized catch.

The trade-study bridge (longeron.analysis.scoreboard. architecture_values()) generalized to counterexamples: the violator is materialized to M0 and its root individual’s measured scalar slots become scoreboard bindings – the requirement it drives below its ramp floor renders as the red cell.

Return type:

dict[str, Any]

longeron.analysis.verify.cover(model, assembly, t=2, assume=(), seed=None, exhaustive_cap=4096)

A t-way covering array over the assembly’s variation points, every row evaluated interpreter-exact.

Factors come from TradeStudy’s variation points (homogeneous selection per point); rows are ordinary selection dicts, evaluated via the same path TradeStudy.evaluate uses. By default the array ranges over the WHOLE candidate space: the assembly’s constraints are the checks under test, and an array constrained by the checks it hunts could catch nothing by construction. assume= names the constraints that are build rules rather than checks (component compatibility: matching cell counts, prop fit); those are enforced during generation through the Z3 constraint engine, and violations are hunted among the rest – the covering-array reading of the universal property.

When the exhaustive space fits under exhaustive_cap candidate mixes, Coverage.recall measures violated-check recall against interpreter-exact ground truth (assumed constraints excluded on both sides); when it does not, the report states the honest guarantee instead – every valid t-tuple covered, violation coverage not guaranteed.

Return type:

Report

longeron.analysis.verify.events_of(interp, state_machine)

Event names accepted anywhere in a state machine definition.

Walks own + inherited members (nested states included) for event triggers – the alphabet a stateful hunt draws its rules from.

Return type:

list[str]

longeron.analysis.verify.hunt(model, part, requirements=(), free=(), max_examples=200, seed=None, fallback=(-1000000.0, 1000000.0))

Search for – and shrink to – a simple violating configuration.

Strategies are derived from the model (attribute_domains()); Hypothesis’s find locates and SHRINKS the simplest bindings whose verdict() reports a violation. The shrunk catch is simplest, not smallest: per free scalar and violated check, the report pairs it with the oracle-bisected edge in Report.boundaries (and prove() supplies the exact algebraic edge where the model encodes). Derandomized; seed is echoed on the report.

Return type:

Report

longeron.analysis.verify.prove(model, part, requirements=(), free=(), seed=None)

Negate each check one at a time under the assumption set.

Every require constraint of the named requirements and every assert constraint of the part is negated in turn, with the value pins, assumptions, and all other checks held: UNSAT is a proof of absence no sampling can deliver; SAT witnesses are re-checked by the interpreter before they are believed (the solver proposes, the interpreter decides). Per free attribute, Optimize computes the exact rational supremum over the all-checks-hold region and attributes it to the check whose exclusion moves it (the binding constraint) – carried on every Proof of the query.

Encodability is per-query, not per-model: where a free path reaches nonlinear algebra the encoder refuses honestly, the refusal lands in Report.gaps, and the signal is to fall back to hunt() over the same scope.

Return type:

Report

longeron.analysis.verify.sequences(model, state_machine, requirements=(), inputs=None, max_examples=100, max_steps=20, seed=None)

Search for – and shrink to – a minimal violating event sequence.

One generic rule sends an arbitrary event from the alphabet read off the model’s transitions (events_of(); a clock-advance rule is added when the machine declares after/at triggers), and one invariant checks the requirements against the live simulation environment. StateMachine.send records non-matching events as ignored, so the rule needs no preconditions and shrinking strips every irrelevant event from the reported sequence.

Return type:

Report

longeron.analysis.verify.strategies_for(interp, defn, free, requirements=(), fallback=(-1000000.0, 1000000.0), domains=None)

Hypothesis strategies for the free attributes (from their domains).

The values are hypothesis.strategies.SearchStrategy objects, annotated Any at this lazy-import boundary. Sides the ladder could not bound take the fallback range and are flagged on the domain (Domain.fallback) – never silent.

Return type:

dict[str, Any]

longeron.analysis.verify.verdict(interp, part, requirements, bindings)

Instantiate part under bindings and check everything.

assert constraint members of the part are violations when false; requirement require constraints are violations only when every assume constraint holds (otherwise the requirement is VACUOUS – recorded, never failed). The interpreter is the sole oracle here; configurations its physics cannot evaluate (a sampled negative mass reaching a real sqrt) come back with Verdict.error set – not a violation, not a pass, and never silently dropped.

Return type:

Verdict

longeron.analysis.verify.verify(model, scope, requirements=(), free=(), seed=None, t=2, max_examples=200, max_steps=20)

Every applicable tier for one scope, one report.

Dispatch is by what the scope is: a state machine runs sequences(); an assembly with variation points runs cover(); any other part definition/usage runs hunt() plus prove() where encodable. Tiers that do not apply are skipped silently; tiers that apply but cannot run (missing extra, no free attributes) are recorded in Report.gaps.

Return type:

Report