This notebook demonstrates check_stale() against the record notebook 02 built; after running it you can show that loosening the lemma’s own bound makes that record stale.
Evidence records are only as good as the model they reference. check_stale() compares a ReviewRecord’s stored content_hash against a model’s current source text. This notebook loads the AS-C08 record Ch8-02 persisted with save_record(), via load_record(), confirms it is current against ch08-cumulative.sysml, then loosens the lemma’s own bound and shows the record go stale.
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)}"A record with an empty identifier fails validation outright, distinct from staleness: it was never a valid record to begin with, regardless of which model it references.
from toaster.evidence import ReviewRecord, hash_content, validate_record
broken = ReviewRecord(
identifier="", # intentionally empty
kind="asserted_solution",
claim="Some claim",
subject_ref="ToasterDemo::deliveredEnergyBoundedBySupply",
model_ref="ToasterDemo",
content_hash=hash_content(source),
scope="Some scope",
criteria="Some criteria",
rationale="Some rationale",
counterevidence="Some counterevidence",
record_kind="worked_example",
)
errors = validate_record(broken, model=model)
assert errors == ["identifier is empty"], f"Expected exactly one identifier error, got {errors}"
print(f"Negative control ok: errors={errors}")Negative control ok: errors=['identifier is empty']
AS-C08 is loaded here from the record notebook 02 persisted with save_record(), already hashed against the ch08-cumulative.sysml source it was built from, so check_stale() has something to compare against.
from toaster.evidence import check_stale
from toaster.judgment_store import load_record
record = load_record("AS-C08")
assert not check_stale(record, source), "Record should be current"
print(f"Record is current: check_stale={check_stale(record, source)}")Record is current: check_stale=False
Loosening deliveredEnergyBoundedBySupply’s own bound from <= 1.0 to <= 1.2 is exactly the kind of change that should invalidate a record built against the tighter bound: the model still loads, but it no longer says what the record claims it says. This is the same partial safeguard the lemma’s own doc comment names: the record’s content_hash is computed from the whole model file, so any edit anywhere in it, including to HeatGenerator’s own efficiencyBounded or deliveredEnergy, would also stale this record, even though nothing automatically checks that the restated lemma still matches whatever changed.
# Loosen the bound the proof protects; the model still parses, the claim no longer matches.
revised_source = source.replace(
"heatGenCheck.efficiency <= 1.0",
"heatGenCheck.efficiency <= 1.2",
)
assert revised_source != source, "Expected the replacement to change the source"
revised_model = conn.load_from_content(revised_source, strict=False)
assert revised_model.ok, "Revised model should still parse"
stale = check_stale(record, revised_source)
assert stale, "Record should be stale after the bound changes"
print(f"After loosening the bound: check_stale={stale}")
print("Record requires re-review: the stored hash no longer matches the current model.")
conn.close()After loosening the bound: check_stale=True
Record requires re-review: the stored hash no longer matches the current model.
The record printed above, current against the model it was built from, went stale the moment the bound it cites changed underneath it: exactly the mismatch the loop is built to catch, whether the change is to the model or to the property a record depends on. Ch8-02 shows the same loosened bound reported undecided by verify_holds() itself, a second, independent way this exact change is caught.
Try the chapter exercise in exercises/ch08/exercise.ipynb: it works through the same verify_satisfaction() and stale-detection pattern on its own, separate coffee-maker exercise model.