This notebook introduces Hawkins’ sufficiency check (see the sufficiency glossary entry), applied to two real ReviewRecords already built earlier in this tutorial; after running it you can tell, for each, whether its own counterevidence and residual_uncertainties are genuinely substantive and whether its engineering_conclusion honestly matches what its own evidence supports.
This tutorial has no central registry of every ReviewRecord it has ever built: each chapter’s notebook constructs its own records as local Python objects, per the construction-zone pattern, with nothing shared beyond the file each one lives in. A search of src/toaster for anything resembling a record store or registry (a dataclass, a database, a persisted list) found none. So this notebook does not scan “every record the tutorial has ever produced” -- that would need a real registry, which does not exist. Instead it reconstructs two real records verbatim, field for field, from Chapter 6 notebook 02 (AS-C06, a mechanism-selection judgment argued from a domain premise) and Chapter 8 notebook 02 (AS-C08, grounded in Chapter 8’s real Z3 proof), and demonstrates what a sufficiency check on each one actually looks like. What follows demonstrates the mechanics of the check on a small, representative sample, not an exhaustive audit of every judgment record this tutorial has ever produced.
from pathlib import Path
import opensysml
from toaster.report import format_diagnostics
conn = opensysml.connect(version="v0.9.0")
source = Path("../../models/ch08-cumulative.sysml").read_text()
model = conn.load_from_content(source, strict=False)
assert model.ok, f"Model failed: {format_diagnostics(model.diagnostics)}"
Before reconstructing two real records, the mechanized half of a sufficiency check: validate_record() already refuses a record whose counterevidence field is empty outright, distinct from asking whether a populated field is substantive, which this notebook goes on to ask.
from toaster.evidence import ReviewRecord, hash_content, validate_record
blank_counterevidence = ReviewRecord(
identifier="AS-BAD",
kind="asserted_solution",
claim="Some claim",
subject_ref="ToasterDemo::ResistanceCoil",
model_ref="ToasterDemo",
content_hash=hash_content(source),
scope="Some scope",
criteria="Some criteria",
rationale="Some rationale",
counterevidence="", # intentionally empty
record_kind="worked_example",
)
errors = validate_record(blank_counterevidence, model=model)
assert errors == ["counterevidence is empty"], f"Expected exactly one error, got {errors}"
print(f"Negative control ok: errors={errors}")
Negative control ok: errors=['counterevidence is empty']
AS-C06, loaded below via load_record() from the record Chapter 6 notebook 02 persisted with save_record(): a mechanism-selection judgment, argued from a domain premise about how a resistive element and a combustion burner each respond to a discrete timing signal. Its content_hash is computed against models/ch06-cumulative.sysml, the real model it was actually written against, not against the current model this chapter uses -- the same file it was built from, unchanged. Two of its own field strings say “above” and “notebook 01”, pointing at Chapter 6’s own earlier cells; they are quoted here exactly as Chapter 6 wrote them, since this is what the record itself actually says, not a rewrite of it.
from toaster.judgment_store import load_record
as_c06 = load_record("AS-C06")
errors = validate_record(as_c06, model=model)
print(f"AS-C06 validation errors: {errors}")
AS-C06 validation errors: []
AS-C08, loaded the same way, via load_record(), from the record Chapter 8 notebook 02 persisted with save_record(): the record grounded in the chapter’s real Z3 proof of deliveredEnergyBoundedBySupply. Its content_hash is computed against models/ch08-cumulative.sysml -- the same file this chapter’s own notebooks already load, since Chapter 8 is the real, current model. Its evidence_refs entry is copied from what that notebook’s own proof actually printed, not restated.
as_c08 = load_record("AS-C08")
errors = validate_record(as_c08, model=model)
print(f"AS-C08 validation errors: {errors}")
AS-C08 validation errors: []
Both records validate cleanly. Hawkins’ sufficiency idea is about whether stated PREMISES make a conclusion’s probable truth follow, so the premises themselves belong in this check, not only counterevidence and residual_uncertainties. AS-C06’s two premises entries are exactly what its own selection argument rests on (a confirmed model fact, plus a domain premise about how the two mechanisms work); AS-C08’s premises and assumption_refs are both genuinely empty.
print(f"AS-C06 premises: {as_c06.premises}")
print(f"AS-C06 assumption_refs: {as_c06.assumption_refs}")
print()
print(f"AS-C08 premises: {as_c08.premises}")
print(f"AS-C08 assumption_refs: {as_c08.assumption_refs}")
AS-C06 premises: ['ControlSystem declares durationOut : DurationPort (Chapter 5), a discrete duration signal, confirmed by model.find() above.', "Domain premise, not derived from the model: a resistive element responds to being switched on and off directly, while a combustion source needs separate ignition and fuel-metering machinery to do the same. Neither HeatGenerator nor any of its realizations is yet connected to ControlSystem's port in this model; this premise is about the physical mechanisms themselves, not about what the model currently wires together."]
AS-C06 assumption_refs: ['HeatGenerator::energyIn and GenerateHeat carry no energy-form commitment (notebook 01): this record is what actually commits to an electrical form, not a fact already built into the port or the function.']
AS-C08 premises: []
AS-C08 assumption_refs: []
Is AS-C08’s empty premises field itself a sufficiency concern? Read against what the record actually claims, no: AS-C06’s claim is an inductive engineering judgment (a mechanism selected FOR stated reasons, reasons that could be wrong), exactly what Hawkins’ idea is about, so it needs premises to carry the inductive weight. AS-C08’s claim, narrowly read (see its own claim and scope above), is that a stated lemma was PROVED by Z3 -- a deductive result, not an inductive one, so there is no separate premise beyond the proof itself for the record to name; evidence_refs carries the proof, and that is the right place for it to live. The genuine risk is not the empty premises field but a claim that quietly outgrows its own narrow scope -- which is exactly what AS-C08’s own counterevidence exists to prevent, by refusing to let the proved lemma stand in for a claim about HeatGenerator’s real efficiencyBounded and deliveredEnergy.
def word_count(text: str) -> int:
return len(text.split())
def word_label(text: str) -> str:
n = word_count(text)
return f"{n} word" if n == 1 else f"{n} words"
for record in (as_c06, as_c08):
print(f"{record.identifier}:")
print(f" counterevidence ({word_label(record.counterevidence)}): {record.counterevidence[:80]}...")
print(f" residual_uncertainties ({word_label(record.residual_uncertainties)}): {record.residual_uncertainties[:80]}...")
print(f" disposition: {record.disposition}")
print(f" engineering_conclusion: {record.engineering_conclusion}")
AS-C06:
counterevidence (78 words): This does not rule out a combustion design: a burner controlled by its own timed...
residual_uncertainties (26 words): Once a supply and a control policy are modeled together, this selection could be...
disposition: pending
engineering_conclusion: undetermined
AS-C08:
counterevidence (133 words): This proof is NOT a solver-checked reference to HeatGenerator's own efficiencyBo...
residual_uncertainties (101 words): Whether efficiency, power and duration ever take values outside the bound in a r...
disposition: pending
engineering_conclusion: supported
Both read as substantive, not placeholder: AS-C06’s counterevidence names a specific competing design (a valve-controlled burner) and a specific unmodeled relation (Joule heating), not a generic hedge; AS-C08’s counterevidence names three specific, cited toolchain limits (DEFERRED.md D-029, D-030, D-031) and the exact edits that were tried and failed to move the lemma’s verdict. Where the two records differ most is what engineering_conclusion claims. AS-C06 stays undetermined even though the record does make a selection: its own counterevidence admits the selection is argued from a domain premise, not a trade study, so undetermined is the honest reading of what the evidence actually supports, not underclaiming. AS-C08 is supported: because its own claim field is already narrowed to the hand-restated lemma, not to HeatGenerator’s original elements, the thing that actually got a Z3 proof is exactly what the record claims was established.
A structural check alone cannot tell substantive text from a placeholder that happens to be non-empty. The record below has every field validate_record() requires, populated with text that would pass it outright.
placeholder_record = ReviewRecord(
identifier="AS-PLACEHOLDER",
kind="asserted_solution",
claim="The chosen design meets its requirement.",
subject_ref="ToasterDemo::ResistanceCoil",
model_ref="ToasterDemo",
content_hash=hash_content(source),
scope="ToasterDemo",
criteria="The design meets its requirement.",
rationale="Analysis shows it does.",
counterevidence="None known.",
residual_uncertainties="None.",
disposition="pending",
dependency_freshness="current",
engineering_conclusion="supported",
record_kind="worked_example",
)
errors = validate_record(placeholder_record, model=model)
print(f"validate_record: errors={errors}")
print(f"counterevidence: {placeholder_record.counterevidence!r} ({word_label(placeholder_record.counterevidence)})")
print(f"residual_uncertainties: {placeholder_record.residual_uncertainties!r} ({word_label(placeholder_record.residual_uncertainties)})")
assert errors == [], "validate_record accepts this outright: every required field is non-empty"
conn.close()
validate_record: errors=[]
counterevidence: 'None known.' (2 words)
residual_uncertainties: 'None.' (1 word)
validate_record() accepts this record outright, the same as AS-C06 and AS-C08 above: beyond requiring subject_ref to resolve in the model (a structural check AS-PLACEHOLDER also passes, since ResistanceCoil is a real element), the mechanized floor only checks non-emptiness, and “None known.” and “None.” both satisfy it. A sufficiency reading must reject it anyway: neither field names a specific design alternative, a specific unmodeled relation, or a specific toolchain limit the way AS-C06’s and AS-C08’s own fields do; there is nothing here a reader could go check, disagree with, or find wrong. That is the actual difference sufficiency asks for, and it is a judgment a person makes by reading the field’s content, not something validate_record() -- or any fixed rule -- can certify.
Sufficiency and staleness are different, related questions. A record can be well-argued and honest -- sufficient, by the reading above -- and still go stale later as the model it cites keeps growing around it; being sufficient when written is not a guarantee of staying so. Notebook 03 checks exactly that, for both records above.
The two records rebuilt above, verbatim from their own chapters, both validate cleanly, and reading their actual counterevidence, residual_uncertainties and premises (not just checking they are non-empty) shows two different, both honest, levels of confidence -- exactly what a reader would need to decide how much to lean on each one.
Try the chapter exercise in exercises/ch09/exercise.ipynb: it asks you to apply the same sufficiency reading, including the premises argument above, to two of your own already-built judgment records.