Skip to main content

Online edition for BLOGE 0.9.8-RC1 · facts verified 2026-09-15 · 中文

Chapter 28 — Bounded Property Verification and Useful Counterexamples

Chapter promise: Explore a declared finite loan-risk domain, separate sample failures from relation failures, replay BLOGE's deterministic shrink trace, and know when a smaller counterexample still needs business review.

Learning goals​

  1. Define a bounded generator attached to an existing Case and its Expectations.
  2. Distinguish a failing sample, a relation counterexample, and a value-shrink result.
  3. Read budget exhaustion and incomplete shrink as non-pass outcomes.
  4. Keep the Oracle independent enough to challenge the candidate.

Five samples answer more than one example—and less than a proof​

The loan team trusts three named Cases but worries about risk-score boundaries. They keep auto-approve as the anchor and replace only given.context.riskScore with five declared values.

Figure 28.1: A bounded generator executes the original contract at five reviewable points

schemaVersion: 1
propertySetId: loan-risk-boundaries
scenario: loan-approval.scenario.yaml
rootSeed: 11
sampleBudget: 5
generator:
  generatorId: risk-scores
  requirementRef: LOAN-DECISION-001
  caseId: auto-approve
  contextKey: riskScore
  integerRange: {minimum: 10, maximum: 90, step: 20}
  expectationIds: [decision-valid, risk-score-recorded]
relations:
  - relationId: risk-never-decreases
    kind: NON_DECREASING
    actual: {kind: BUSINESS_OUTPUT, outputId: computedRiskScore}
VerificationPropertyReport property = verifier.verifyProperties(propertyPath);

Each sample still runs every non-diagnostic Expectation in the anchor Case. rootSeed makes supported sample selection and ordering repeatable; it does not control clocks, randomness, network state, or environment reads inside customer Operators. The claim is exactly five declared points, not “all integer risk scores.”

Three failures answer three different questions​

Evidence objectWhat failed?How it becomes smaller
sampleordinary business Expectations for one generated inputvalue shrink may reexecute candidates
relation counterexamplea relation across executed samplesselects a smaller subset of those sample IDs
property reportany required sample, relation, or shrink protocolaggregates status and stable reason codes

A relation shrinkTrace never invents an input. A monotonicity violation can reduce the executed set to the first pair that demonstrates inversion. Value shrink is different: it performs new executions after one relation-free sample has failed.

Replay the actual integer shrink​

For a relation-free integer plan with maximumAttempts: 64, RC1 test deterministicallyShrinksAnIntegerFailureByReexecutingCandidates observes this exact sequence twice:

Figure 28.2: Value shrink reexecutes deterministic candidates until the same reason codes stop reproducing

1,000,000 → 0 → 1 → 2 → 4 → 8 → 16 → 32 → 64 → 128

The first value is the original failing sample. Candidates begin at zero and then use same-sign powers of two. A candidate counts only when it reproduces the original ordered reason codes. The test repeats the experiment and compares both the observed sequence and candidate context digests; both runs are identical.

The final accepted candidate is not “the mathematically smallest bad loan.” It is the minimal witness produced by this candidate order and failure-equivalence rule.

Counterexample reduction does not promote the Oracle​

Suppose [10, 30, 50, 70, 90] yields [10, 30, 80, 70, 90]. Every sample may satisfy local shape checks, but NON_DECREASING fails because 80 → 70 reverses direction. A relation counterexample can retain only those two sample IDs.

That pair is a diagnostic asset, not automatically a new Golden Case. The business owner still decides whether the relation is correct, whether generated contexts are legal, and whether the reduced input deserves an approved expected answer.

Shrink can end without a usable minimum​

  • If the original sample passes, BLOGE does not attempt shrink.
  • If the attempt budget ends while candidates remain, the result is INCOMPLETE / RESOURCE_LIMIT_EXCEEDED.
  • If no candidate reproduces the original ordered reason codes, the result is INCOMPLETE / PROPERTY_SHRINK_INCOMPLETE.
  • If a candidate fails for a different reason, it is not evidence of the same bug.

None can be relabeled as business PASS. “Could not finish diagnosis” and “verified correct” are opposite statements.

Keep the judge outside the candidate​

verifyOracleIndependence(Path) separates three inspectable facts:

  • CONTENT_BOUND: approved Oracle bytes match the catalog digest.
  • OWNER_SEPARATED: catalog owner labels differ; this is a declaration, not identity authentication.
  • REFERENCE_MODEL: a bound implementation may run in a child JVM, with its content closure checked against candidate runtime and Operator bytes.

The evidence reader may rerun only that reference model; it does not run candidate Operators or customer bootstrap. Byte disjointness cannot detect copied decision logic, so conceptual independence and owner identity remain external governance questions.

Lab: turn one inversion into a review card​

  1. Run the five-score plan and save sample IDs, outputs, root seed, and receipt.
  2. Introduce one threshold inversion while keeping every other input fixed.
  3. Record the failing relation and its minimal sample-ID subset.
  4. Use a separate relation-free plan to trigger value shrink; do not mix the two mechanisms.
  5. Copy the complete candidate order into the review card.
  6. Ask the business owner whether the reduced witness is legal, meaningful, and worthy of a governed Case.
  7. Restore the implementation and confirm both the property and original Case pass.

Transfer: shrink a logistics-ordering failure​

For shipment tracking, sample a bounded set of event sequences and require deliveredAt >= shippedAt. If one sequence violates the relation, reduce the sequence to the smallest replayable pair of events while retaining the original seed and candidate order. The reduced trace is a diagnosis aid; a logistics owner still decides whether it is a valid governed Case.

Chapter boundary​

  • Bounded property verification covers the declared finite plan, not an infinite domain or statistical confidence.
  • Relation reduction chooses among executed samples; value shrink creates and reexecutes candidates.
  • Deterministic shrink means reproducible search order, not globally minimal business input.
  • Oracle byte separation is useful evidence, not proof of human independence or conceptual originality.

Experiment acceptance card​

  • Expected and observed: A bounded domain finds and shrinks a counterexample to a reviewable candidate.
  • Failure and recovery: Move the oracle into the candidate or stall shrinking; restore an external judge and stop reason.
  • Proof boundary: Proves a property within chosen bounds, not a universal proof.
  • Exercise contract: One property and bounded domain; change the bound; deliver seed, counterexample, and shrink trace; stop when stable and replayable.

Summary​

Property verification expands one named Case into a controlled finite experiment. Counterexamples identify a small already-observed relation failure; value shrink reexecutes candidates to leave a smaller reproducible witness. The next chapter asks whether these results still deserve trust after their files, receipt, source, or runtime context changes.

Next: Chapter 29 — From Report to Source-bound Evidence

Coding Agent: Open the versioned task guide.