proof versus point evaluation

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 require constraint referencing an undefined attribute fails.
bad_source = """
package P {
    private import ScalarValues::*;
    part def T { attribute x : Real default = 5.0; }
    requirement def R {
        subject t : T;
        require constraint { t.missingAttr <= 10.0 }
    }
}
"""
bad = conn.load_from_content(bad_source, strict=False)
assert not bad.ok, "Expected failure for undeclared attribute"
print(f"Negative control ok: bad.ok={bad.ok}")

verdicts = model.verify_satisfaction()
for v in verdicts:
    status = "holds" if v.holds else "FAILS"
    extra = f"  ({v.error})" if v.error else ""
    print(f"  [{status}] {v.element}{extra}")

by_element = {v.element: v for v in verdicts}
assert by_element["not satisfy timely by slow"].holds is True
assert by_element["satisfy heatGenerationReq by rated"].holds is True
assert by_element["not satisfy heatGenerationReq by weak"].holds is True
print("\nEach of the three claims above is observed at one fixed set of attribute values.")

from toaster import conformance

report = conformance.report(model, stage=(8, 1))
for r in report["project"]:
    print(r)

result = next(r for r in report["project"] if r.check_id == "satisfaction-claims-evaluated")
assert result.status == "passed"
assert result.findings == []
print("\nsatisfaction-claims-evaluated now reports passed on a real, non-vacuous check: "
      "every claim this check can evaluate evaluates to what it says it evaluates to.")

import os
from pathlib import Path
from toaster import modelcheck as mc
from toaster.tools import resolve_library, resolve_sysmlv2, resolve_z3, tool_env

BINARY = resolve_sysmlv2()
LIB = resolve_library()
Z3 = resolve_z3()
os.environ["PATH"] = tool_env()["PATH"]  # later cells call the CLI without z3=; it finds z3 on PATH

# A fixed scratch directory and fixed filenames (not tempfile.NamedTemporaryFile's own
# randomized name) keep this notebook's own printed output, including any error message
# that embeds a companion file's path, byte-for-byte reproducible run to run.
SCRATCH_DIR = Path("companion-check-scratch")  # repo-relative, portable across machines
SCRATCH_DIR.mkdir(exist_ok=True)

def _write_companion(name: str, content: str) -> Path:
    p = SCRATCH_DIR / name
    p.write_text(content)
    return p

# Restates deliveredEnergyBoundedBySupply exactly as committed in ch08-cumulative.sysml
# (https://github.com/Open-MBEE/toaster/blob/main/models/ch08-cumulative.sysml),
# with a minimal HeatGenerator stub, and no assert satisfy declaration (D-029).
COMPANION_POSITIVE = """\
package ConservationCheck {
    private import ScalarValues::*;
    private import SI::*;
    private import ISQ::*;
    private import MeasurementReferences::*;

    abstract part def HeatGenerator {
        attribute power : ISQ::PowerValue;
        attribute efficiency : DimensionOneValue;
    }
    part heatGenCheck : HeatGenerator;
    attribute heatGenCheckDuration : ISQ::DurationValue;

    assert constraint deliveredEnergyBoundedBySupply {
        (heatGenCheck.efficiency >= 0.0 and heatGenCheck.efficiency <= 1.0
         and heatGenCheck.power >= 0.0 [SI::W] and heatGenCheckDuration >= 0.0 [SI::s])
        implies (heatGenCheck.power * heatGenCheckDuration * heatGenCheck.efficiency)
                <= heatGenCheck.power * heatGenCheckDuration
    }
}
"""

def _ascii(reason: str) -> str:
    """The CLI's own reason text may carry an em dash; this display copy swaps it for a
    plain double hyphen so what this notebook prints stays plain ASCII. Only the printed
    copy changes; the verdict objects themselves keep the CLI's own text."""
    return reason.replace("\u2014", "--")

companion_path = _write_companion("conservation_check.sysml", COMPANION_POSITIVE)

pos_verdicts = mc.verify_holds(str(companion_path), lib=str(LIB), binary=str(BINARY), z3=str(Z3), solve=True)
pos_verdict = pos_verdicts[0]
print(f"[{pos_verdict.status}] {pos_verdict.element}  ({_ascii(pos_verdict.reason)})")
assert pos_verdict.status == "satisfied"
# "satisfied" can come from interval propagation alone, not necessarily Z3 (DEFERRED.md,
# the note beside D-029): this checks the reason text actually names z3, not just the
# status, confirming the solver itself resolved this one.
assert "z3" in pos_verdict.reason
assert mc.holds(str(companion_path), lib=str(LIB), binary=str(BINARY), z3=str(Z3), solve=True) is True
print("\nProved for every value of heatGenCheck.efficiency, heatGenCheck.power and "
      "heatGenCheckDuration the antecedent admits, not evaluated at one.")

# Negative control: the FULL negation of the lemma (A and not B), which Z3 must resolve
# as unsatisfiable to report violated -- not "A implies not B" (a different, weaker
# statement, confirmed undecided in this toolchain: see the markdown above).
COMPANION_NEGATIVE = """\
package ConservationCheckBroken {
    private import ScalarValues::*;
    private import SI::*;
    private import ISQ::*;
    private import MeasurementReferences::*;

    abstract part def HeatGenerator {
        attribute power : ISQ::PowerValue;
        attribute efficiency : DimensionOneValue;
    }
    part heatGenCheck : HeatGenerator;
    attribute heatGenCheckDuration : ISQ::DurationValue;

    assert constraint deliveredEnergyExceedsSupply {
        (heatGenCheck.efficiency >= 0.0 and heatGenCheck.efficiency <= 1.0
         and heatGenCheck.power >= 0.0 [SI::W] and heatGenCheckDuration >= 0.0 [SI::s])
        and (heatGenCheck.power * heatGenCheckDuration * heatGenCheck.efficiency)
            > heatGenCheck.power * heatGenCheckDuration
    }
}
"""

negative_path = _write_companion("conservation_check_broken.sysml", COMPANION_NEGATIVE)

neg_verdicts = mc.verify_holds(str(negative_path), lib=str(LIB), binary=str(BINARY), solve=True)
neg_verdict = neg_verdicts[0]
print(f"[{neg_verdict.status}] {neg_verdict.element}  ({_ascii(neg_verdict.reason)})")
assert neg_verdict.status == "violated"
assert mc.holds(str(negative_path), lib=str(LIB), binary=str(BINARY), solve=True) is False
print("\nThe loop catches a fully broken lemma: violated, not undecided, not silently accepted.")

# A realistically weakened variant: the same lemma, its own bound loosened from 1.0 to
# 1.2. Neither a tautology nor a contradiction any more: undecided, with a witness.
COMPANION_WEAKENED = """\
package ConservationCheckWeakened {
    private import ScalarValues::*;
    private import SI::*;
    private import ISQ::*;
    private import MeasurementReferences::*;

    abstract part def HeatGenerator {
        attribute power : ISQ::PowerValue;
        attribute efficiency : DimensionOneValue;
    }
    part heatGenCheck : HeatGenerator;
    attribute heatGenCheckDuration : ISQ::DurationValue;

    assert constraint deliveredEnergyBoundedBySupply {
        (heatGenCheck.efficiency >= 0.0 and heatGenCheck.efficiency <= 1.2
         and heatGenCheck.power >= 0.0 [SI::W] and heatGenCheckDuration >= 0.0 [SI::s])
        implies (heatGenCheck.power * heatGenCheckDuration * heatGenCheck.efficiency)
                <= heatGenCheck.power * heatGenCheckDuration
    }
}
"""

weakened_path = _write_companion("conservation_check_weakened.sysml", COMPANION_WEAKENED)

weak_verdicts = mc.verify_holds(str(weakened_path), lib=str(LIB), binary=str(BINARY), solve=True)
weak_verdict = weak_verdicts[0]
print(f"[{weak_verdict.status}] {weak_verdict.element}  ({_ascii(weak_verdict.reason)})")
assert weak_verdict.status == "undecided"
assert "z3" in weak_verdict.reason

try:
    mc.holds(str(weakened_path), lib=str(LIB), binary=str(BINARY), solve=True)
    raise AssertionError("expected holds() to raise ModelCheckInconclusiveError")
except mc.ModelCheckInconclusiveError as exc:
    print(f"holds() correctly refuses to answer: {exc}")

# Clean up the fixed scratch files now that every demo in this notebook has used them.
for p in (companion_path, negative_path, weakened_path):
    p.unlink(missing_ok=True)

# what is being claimed, and what, specifically, it is about
subject_ref = "ToasterDemo::deliveredEnergyBoundedBySupply"
AS_C08_TAG = """\
metadata asC08Tag : ReviewRecordRef about deliveredEnergyBoundedBySupply {
    identifier = "AS-C08";
}
"""
print(AS_C08_TAG)

TOASTER_INCREMENT = AS_C08_TAG

from toaster.evidence import ReviewRecord, hash_content, validate_record

claim = (
    "deliveredEnergyBoundedBySupply, a hand-restated real-arithmetic lemma of the same "
    "shape as HeatGenerator's efficiencyBounded constraint and deliveredEnergy's own "
    "definition, holds for every value of efficiency in [0,1] and every non-negative "
    "power and duration a companion restatement admits."
)
model_ref = "ToasterDemo::deliveredEnergyBoundedBySupply"
print(claim)

scope = (
    "The lemma governs the companion restatement's own heatGenCheck.efficiency, "
    "heatGenCheck.power and heatGenCheckDuration features; it is not a solver-checked "
    "reference to HeatGenerator's own efficiencyBounded or deliveredEnergy (DEFERRED.md "
    "D-030, D-031), only a hand-restated copy of the same shape."
)
criteria = (
    "verify_holds() reports a single satisfied verdict for deliveredEnergyBoundedBySupply, "
    "with the reason text naming z3 (not propagation alone), proved for all values of the "
    "unbound heatGenCheck.efficiency, heatGenCheck.power and heatGenCheckDuration features."
)
print(scope)
print(criteria)

premises = []
assumption_refs = []
print("No prior ReviewRecord is assumed; this claim rests on the proof itself.")

evidence_refs = [f"verify_holds: {pos_verdict.element} {pos_verdict.status} ({_ascii(pos_verdict.reason)})"]
rationale = (
    "verify_holds() calls sysml-toolkit's real verify --solve command, which runs Z3 "
    "over the unbound features of a companion restatement of this lemma (see the "
    "narration above for why a companion file is used) and reports "
    "deliveredEnergyBoundedBySupply as satisfied: proved for all values the restatement "
    "admits, not read back from one entered value. This is a materially different kind of "
    "evidence from an evaluate-only verdict: verify_satisfaction() could only ever check "
    "a relation at whichever single power, duration and efficiency a candidate happens to "
    "carry. It is also, deliberately, a narrower claim than 'this proves HeatGenerator's "
    "own conservation property': see counterevidence."
)
print(evidence_refs)
print(rationale)

counterevidence = (
    "This proof is NOT a solver-checked reference to HeatGenerator's own "
    "efficiencyBounded constraint or deliveredEnergy calc: this toolchain's Z3 backend "
    "does not compose two separately declared assert constraints, whether sibling or "
    "inherited (DEFERRED.md D-030), and cannot reason through a chained calc invocation "
    "like heatGenCheck.deliveredEnergy(...) (D-031). Confirmed directly: loosening "
    "efficiencyBounded's own literal bound to <= 1.5, or doubling deliveredEnergy's own "
    "definition by a factor of 2.0, in the real committed model changes neither the "
    "original elements' own verdicts nor this lemma's verdict at all, because the lemma "
    "restates its own copy of both rather than referencing either. The companion file "
    "used by verify_holds also restates the construct rather than checking the "
    "committed model directly, because toaster.modelcheck's own text parser does not "
    "yet handle the extra annotation the CLI prints for assert satisfy declarations "
    "(DEFERRED.md D-029)."
)
residual_uncertainties = (
    "Whether efficiency, power and duration ever take values outside the bound in a "
    "real candidate is not addressed by this proof; it establishes only that the "
    "restated lemma respects conservation wherever its own bound is honored. If "
    "HeatGenerator's own efficiencyBounded or deliveredEnergy is ever edited, this "
    "record's content_hash (computed from the whole model file) does go stale, which "
    "forces a re-review, but nothing automatically re-checks that the restated copy "
    "still matches the edited original; that check would be manual. No physical heat "
    "generator has been checked against this property; HeatGenerator remains an "
    "abstract carrier with no concrete realization of its own."
)
print(counterevidence)
print(residual_uncertainties)

from toaster.query import get_review_record_refs
from toaster.judgment_store import save_record

record = ReviewRecord(
    identifier="AS-C08",
    kind="asserted_solution",
    claim=claim,
    subject_ref=subject_ref,
    model_ref=model_ref,
    content_hash=hash_content(source),
    scope=scope,
    criteria=criteria,
    premises=premises,
    assumption_refs=assumption_refs,
    evidence_refs=evidence_refs,
    rationale=rationale,
    counterevidence=counterevidence,
    residual_uncertainties=residual_uncertainties,
    disposition="pending",
    dependency_freshness="current",
    engineering_conclusion="supported",
    record_kind="worked_example",
)

errors = validate_record(record, model=model)
tag = next((t for t in get_review_record_refs(model) if t["identifier"] == record.identifier), None)
print(f"Model tag: {tag}")
print(f"Validation errors: {errors}")
assert errors == [], f"Validation errors: {errors}"
save_record(record)
print(f"Record valid: identifier={record.identifier!r}  engineering_conclusion={record.engineering_conclusion!r}")
conn.close()