Properties and mutations

ActionsArtifactVerify

Task and place

Passing scenarios confirm the probed points; this stage asks two harder questions. Do answer-wide properties hold across cases, and would the scenarios fail if the model were wrong? Properties assert the first, mutations probe the second. The stage sits after scenarios pass and before review: review reads the properties and the surviving mutants alongside the rules.

Inputs

• A passing suite with its plan from the previous stage.
• The expectation vocabulary: the seven result fields and their values.
• The demo readme with the base rule, the intentionally broken copy, and the shared test.
• The built-in mutation helper of the law tool, whose listing run is shown below.

Actions

• Assert end-properties with the expect vocabulary. Each field below is checkable on an answer; the running example uses only the first row, and that is enough for its seven checks.

Field	Values
truth status	established only, denied only, both, neither
result kind	data, collection, proposition, and further kinds
applicability status	applicable, not applicable, undetermined, conflicted
trigger status	satisfied, not satisfied, undetermined, conflicted
evaluation status	computed, missing input, and further outcomes
normative status	created, pending, active, satisfied, and further states
value	no vocabulary: the data term itself

• Write distinguishing scenarios: the same facts, then the one fact that tells two readings apart. Loss thirty against loss twenty-nine and loss one hundred against loss one hundred one are the running-example pairs; loss twenty-five is the demo pair below.
• Mutate by hand for the decisive condition: copy the package, weaken one guard, keep the tests identical, and require the expected failures — every failure explained by the weakened requirement, no unexpected ones. A lone failing test is the isolated-probe special case, not the general rule.
• List tool-made mutants for the same rule to see the variations an author would miss. Observed run with tool version law 0.1.0, semantics law.core/0.2, over the lowered demo base:

Terminal

$ law engine lower docs/handbook/files/fixtures/mutant-demo/base > /tmp/mutant-base.json
$ law engine mutate /tmp/mutant-base.json

Output

мутанты CLIR (law.mutate/0.1): кандидатов 9, обследовано 9, валидных 7, invalid 2, stillborn 0, cap нет
  invalid mutant:sha256:5e20b02a0e4cc9bf16962577351a82c368738f04aa93761940a0d43c730f45e6: rule urn:handbook:mutant-demo:base#PayoutFromThirty: unbound var after mutation: v0, v1
  invalid mutant:sha256:bb52154dfdb9439355ca8c4ba7bb6198943ff421d1babf8114fe45f5479fbc9f: rule urn:handbook:mutant-demo:base#PayoutFromThirty: unbound var after mutation: v1

[translation] The summary line reads: nine candidates, nine examined, seven valid, two invalid, zero stillborn, no cap. The two invalid mutants leave variables unbound after the change. Structured output of the same run names ten candidate operators; the seven valid mutants came from three of them: dropping a conjunct, swapping a comparison, and removing a rule.

The same listing over the lowered accepted candidate (local law 0.1.0 build — the published build has no mutate command) reads sixty-seven candidates, sixty-seven examined, fifty-three valid, fourteen invalid, zero stillborn, no cap: twelve comparison swaps, six conjunct drops, four variable substitutions, two variable freshens, and twenty-nine rule removals, twenty-two of which drop one tariff row each. The listing hunts; the hand-applied weakenings below judge.

Output

мутанты CLIR (law.mutate/0.1): кандидатов 67, обследовано 67, валидных 53, invalid 14, stillborn 0, cap нет

[translation] The summary line reads: sixty-seven candidates, sixty-seven examined, fifty-three valid, fourteen invalid, zero stillborn, no cap.

Decisions

• Which properties the package asserts and over which domain. The running example asserts one narrow property over workers collected at exactly thirty percent loss, plus a world probe with the same facts.
• Hand-made or tool-listed mutants: hand-make the decisive weakening the suite must fail, and use the tool listing to hunt for missing scenarios.
• What a surviving mutant means: either a missing scenario to write or a recorded reason why the variation is out of scope. Silence is not a reason.
• Broken copies never ship: mutants live in fixtures, out of the package.

Artifact

The artifact is the property block plus the fixture pair. The property below is quoted from the running-example goals suite.

Arxo Law

property GoalEstablishedCapacityLossHasPayout {
 label ru-KZ unofficial "работнику с установленной утратой профессиональной трудоспособности от 30 процентов причитается страховая выплата";
 basis EAI_ART19;
 forall worker in collect v: Employee where capacity_loss_percent(v, 30);
 expect insurance_payout_due(worker);
}

[translation] The label reads: a worker with an established professional-capacity loss of thirty percent or more is due an insurance payout.

The fixture pair is the base rule with its guard at thirty and the intentionally broken copy with the guard weakened to twenty while the rule name stays unchanged — that mismatch is the planted fault. Both packages run the same shared test: loss thirty qualifies, loss twenty-five stays undecided.

EAI example

The running example is the employee accident insurance package: name kz.corpus.employee_accident_insurance, version 0.1.0, language 0.2, zero dependencies, explicit local imports. Sources are pinned to edition EAI_EDITION with materialization PINNED_UNOFFICIAL_COPY — an Adilet API copy retrieved 2026-09-13, sha256 pinned, local copy kept in the package. Its world probe and property both read Article Nineteen: the probe fixes one worker at thirty percent loss and expects payout established, and the property expects payout for every worker the collect gathers. All thirty-seven candidate checks assert truth status only. The distinguishing pairs double as tripwires for the decision records: the two boundary pairs trip EAI-D2 end by end, the per-row tariff checks trip EAI-D1 row by row, the fractional probe trips EAI-D3, and the premium-base probes trip EAI-D4.

Pitfall

A mutant that changes nothing observable teaches nothing: if no tested point can tell it apart, it survives no matter how strong the suite looks. Its mirror is a property over an empty domain — always confirm the collected domain is the one meant, since the run report carries the domain size, counterexamples, and unexecuted checks. The dullest failure is shipping the mutant: a weakened copy left in the package reads like the act until someone diffs it.

Verify

The stage is done when the base run passes fully and the mutant run produces the expected failures — every failure explained by the weakening, no unexpected ones. In this two-check demo the expected set happens to be one test; on the candidate below, one weakening trips three. Observed runs with tool version law 0.1.0, semantics law.core/0.2:

Terminal

$ law test docs/handbook/files/fixtures/mutant-demo/base

Output

law test handbook.mutant_demo.base: мир handbook.mutant_demo.base
  ok   [handbook.mutant_demo.base#authored] tests/core.lawtest / LOSS-THIRTY-QUALIFIES
  ok   [handbook.mutant_demo.base#authored] tests/core.lawtest / LOSS-TWENTY-FIVE-STAYS-UNDECIDED
итого: 2 проверено, 2 прошли, 0 не прошли, 0 не исполнены; код 0

[translation] The header line names the tested world; the summary line reads: two checked, two passed, zero failed, zero unexecuted, exit code zero.

Terminal

$ law test docs/handbook/files/fixtures/mutant-demo/mutant

Output

law test handbook.mutant_demo.mutant: мир handbook.mutant_demo.mutant
  ok   [handbook.mutant_demo.mutant#authored] tests/core.lawtest / LOSS-THIRTY-QUALIFIES
  FAIL [handbook.mutant_demo.mutant#authored] tests/core.lawtest / LOSS-TWENTY-FIVE-STAYS-UNDECIDED
        truth_status == NEITHER: в документе TRUE_ONLY
итого: 2 проверено, 1 прошли, 1 не прошли, 0 не исполнены; код 1

[translation] The summary line reads: two checked, one passed, one failed, zero unexecuted, exit code one. The failing line reads: truth status expected neither, the document holds established only.

Criterion: the base run reads ok twice, and the mutant run fails exactly the twenty-five case with established-only where neither was expected, exiting nonzero. A suite that passes on the mutant misses the weakening entirely.

The candidate kill matrix, each weakening hand-applied on a scratch copy with the suite identical (pinned law 0.1.0 build):

Weakening	Failing checks	Read
drop percent <= 100	EAI-LOSS-101-SILENT only, 36 of 37	killed — the source seven passed this mutant seven of seven
drop percent >= 30	EAI-LOSS-TWENTY-NINE only, 36 of 37	killed
<= 100 to < 100	EAI-LOSS-100-QUALIFIES only, 36 of 37	killed
>= 30 to > 30	loss-thirty core check plus the world probe and the property, 34 of 37	killed — all three read the same bound
remove the TariffClass7 rule	EAI-TARIFF-CLASS-07 only, 36 of 37	killed — rows fail independently
smuggle round(…, 0, "HALF_UP") into the penalty	EAI-PENALTY-FRACTIONAL-EXACT only, 36 of 37; the round-figure 3000 check still passes	killed — the source seven passed this mutant seven of seven
remove the PremiumMinimumFloor rule	EAI-PREMIUM-MINIMUM-FLOOR only, 36 of 37	killed — the floor probe bites
base >= floor to base > floor	EAI-PREMIUM-MINIMUM-BOUNDARY only, 36 of 37	killed — the equal-base edge is pinned

Limits

Finite tests prove less than they suggest. They do not prove the model matches the act; they say nothing about untested points such as a loss above one hundred one, a negative loss, a fractional payroll, a below-payroll insured sum, or a missing loss fact; and they say nothing about other packages, versions, or editions. Properties cover only the collected finite domain — the running-example property pins loss at exactly thirty rather than sweeping the interval. Mutants probe only the variations listed: each hand mutant weakens one guard the author chose, and the tool lists candidates over the lowered form without judging which ones the suite must fail. Consider a mutant that drops the upper guard: it changes only points no demo test probes, so both demo tests would still pass — that survival marks a hole in the suite, not strength in the rule. The candidate’s 101 check exists to close exactly that hole, and the matrix above shows it closed.

Next step

Continue with Draft workbench, which takes the probed model through the pin, check, eval, compare, measure, and impact round.

Sources

• Writing tests — the expect vocabulary and property execution.
• Four states of support — established, denied, both, and neither.
• Command line — the lower, mutate, and test commands used above.
• Diagnostics — reading refusals and warnings.
• Writing scenarios — the previous stage.