From 4360d3ef60721b9a50804b25c363a7cbe3ea107d Mon Sep 17 00:00:00 2001 From: Denis Ignatovich Date: Wed, 26 Aug 2026 15:38:50 -0500 Subject: [PATCH] =?UTF-8?q?release:=20ponens=201.11.0=20=E2=80=94=20compos?= =?UTF-8?q?able=20acceptance=20+=20accumulated=20trace-spec=20work?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Bumps the package to 1.11.0 (cli/pyproject.toml) and lands the working-tree package + spec docs. - Composable acceptance / goal property language (GOAL_CONTRACT v0.2; TRACE_SPEC 1.11 §18.1 optional `formula`): and/or/not/implies + forall/exists over component selectors (glob/module/scope/tag), per-atom met/governed roles, and a 4-valued status lattice. Legacy single-criterion goals desugar unchanged. - Trace-spec 1.10/1.11 features (already specified): trace composition + component identity, cryptographic signatures. - Oracle registry + SDK modules (oracles.py, sdk.py) with ORACLE_SPEC/SDK_SPEC. Spec docs updated and cross-referenced (README, GOAL_FAITHFULNESS re-pointed to v0.2). CLI test suite: 588 passed, 46 skipped. --- cli/ponens/cli.py | 3 + cli/ponens/component.py | 343 ++++++++++ cli/ponens/emit.py | 50 +- cli/ponens/goals.py | 313 ++++++++- cli/ponens/lineage.py | 52 +- cli/ponens/merge.py | 593 ++++++++++++++++++ cli/ponens/oracles.py | 302 +++++++++ cli/ponens/sdk.py | 198 ++++++ cli/ponens/trace.py | 53 +- cli/pyproject.toml | 2 +- cli/tests/unit/test_component.py | 162 +++++ cli/tests/unit/test_component_identity.py | 261 ++++++++ cli/tests/unit/test_goal_formula.py | 205 ++++++ cli/tests/unit/test_goal_quantifiers.py | 168 +++++ cli/tests/unit/test_merge.py | 336 ++++++++++ cli/tests/unit/test_merge_combine.py | 224 +++++++ cli/tests/unit/test_merge_coverage.py | 161 +++++ cli/tests/unit/test_merge_skipcontract.py | 215 +++++++ cli/tests/unit/test_oracles.py | 80 +++ cli/tests/unit/test_sdk.py | 84 +++ spec/AUDIT_READINESS_v0_1.md | 4 +- ...CONTRACT_v0_1.md => GOAL_CONTRACT_v0_2.md} | 94 ++- spec/GOAL_FAITHFULNESS_v0_1.md | 10 +- spec/ORACLE_SPEC_v0_1.md | 128 ++++ spec/POLICY_LANGUAGE_v0_2.md | 2 +- spec/PRIOR_ART_ALIGNMENT_v0_1.md | 2 +- spec/PROV_INTERCHANGE_v0_1.md | 2 +- spec/README.md | 8 +- spec/SDK_SPEC_v0_1.md | 254 ++++++++ ...TRACE_SPEC_v1_9.md => TRACE_SPEC_v1_11.md} | 162 ++++- spec/schema/README.md | 2 +- 31 files changed, 4413 insertions(+), 60 deletions(-) create mode 100644 cli/ponens/component.py create mode 100644 cli/ponens/merge.py create mode 100644 cli/ponens/oracles.py create mode 100644 cli/ponens/sdk.py create mode 100644 cli/tests/unit/test_component.py create mode 100644 cli/tests/unit/test_component_identity.py create mode 100644 cli/tests/unit/test_goal_formula.py create mode 100644 cli/tests/unit/test_goal_quantifiers.py create mode 100644 cli/tests/unit/test_merge.py create mode 100644 cli/tests/unit/test_merge_combine.py create mode 100644 cli/tests/unit/test_merge_coverage.py create mode 100644 cli/tests/unit/test_merge_skipcontract.py create mode 100644 cli/tests/unit/test_oracles.py create mode 100644 cli/tests/unit/test_sdk.py rename spec/{GOAL_CONTRACT_v0_1.md => GOAL_CONTRACT_v0_2.md} (73%) create mode 100644 spec/ORACLE_SPEC_v0_1.md create mode 100644 spec/SDK_SPEC_v0_1.md rename spec/{TRACE_SPEC_v1_9.md => TRACE_SPEC_v1_11.md} (81%) diff --git a/cli/ponens/cli.py b/cli/ponens/cli.py index 4005425..4c5260d 100644 --- a/cli/ponens/cli.py +++ b/cli/ponens/cli.py @@ -22,6 +22,7 @@ from . import emit as emit_mod from . import agent as agent_mod from . import reasoners as reasoners_mod +from . import oracles as oracles_mod # ── Helpers ───────────────────────────────────────────────────── @@ -667,6 +668,8 @@ def build_parser(): # ── reasoners (the reasoner registry) ──────────────────────── reasoners_mod.register(subparsers) + oracles_mod.register(subparsers) + # ── git/hub sync (bind, push, pull, status) ────────────────── sync_mod.register(subparsers) diff --git a/cli/ponens/component.py b/cli/ponens/component.py new file mode 100644 index 0000000..f8df01b --- /dev/null +++ b/cli/ponens/component.py @@ -0,0 +1,343 @@ +"""Component-identity resolver: decide whether a code descriptor is the SAME component as a prior one +(-> reuse its component_id) or a NEW one (-> mint a fresh id). The Python realization of the PROVED +model in `formal/component/identity.iml` (the conformance spec). + +The dangerous error is CONFLATION: reusing an id for a genuinely-DIFFERENT code element. So the SAFE +fallback is MINT-NEW ("treat as a distinct component") — conflation is the unsound error, and the +resolver NEVER guesses when the signal is weak or ambiguous. + +Tiers, most-confident first (mirrors identity.iml `resolve`): + 1. LINEAGE — a producer-declared same-model-line link (`lineage_id is not None`) -> reuse it. + 2. UNIQUE-EXACT — exactly ONE prior with an identical fingerprint -> reuse it. + (0 -> nothing to reuse; >1 -> ambiguous -> mint, never conflate.) + 3. SIMILARITY — a confident, UNIQUE match: best >= SIM_MIN AND best - second >= SIM_MARGIN -> + reuse the best candidate. (Same floor/margin as ambiguity.iml: 80 / 15.) + 4. else -> MINT (the caller then allocates a fresh id). + +Similarity is an integer percentage (0..100). `_line_similarity` is the Sørensen–Dice coefficient over +the SET of trimmed non-empty lines — the concrete signal the abstract `best`/`second` percentages stand +for in the proved model. +""" + +import fnmatch +import re + +SIM_MIN = 80 +SIM_MARGIN = 15 + + +def _lines(s): + """The SET of trimmed, non-empty lines of `s`.""" + return {ln.strip() for ln in (s or "").splitlines() if ln.strip()} + + +def _line_similarity(a, b): + """Sørensen–Dice over the SET of trimmed non-empty lines, as an integer percentage 0..100: + `2*|A∩B| / (|A|+|B|)`. Empty/empty -> 0 (no lines to agree on).""" + A, B = _lines(a), _lines(b) + denom = len(A) + len(B) + if denom == 0: + return 0 + return (2 * len(A & B) * 100) // denom + + +def confident_sim(best, second): + """The confident-similarity predicate (identity.iml `confident_sim`): the best candidate clears the + minimum AND beats the runner-up by the margin. Integer percents.""" + return best >= SIM_MIN and best - second >= SIM_MARGIN + + +def resolve_component_id(lineage_id, exact_count, exact_id, best, second, sim_id): + """The low-level proved resolver (identity.iml `resolve`), 4 tiers in order. Returns + `("reuse", )` or `("mint", None)`. + + lineage_id : a producer-declared same-model-line link (not None) if present. + exact_count : # priors with an identical fingerprint. + exact_id : the sole exact match's id (meaningful only when exact_count == 1). + best,second : top-two similarity percentages (0..100). + sim_id : the best similarity candidate's id. + Returns mint when unsure — the CALLER allocates the fresh id.""" + if lineage_id is not None: + return ("reuse", lineage_id) # Tier 1: lineage wins + if exact_count == 1: + return ("reuse", exact_id) # Tier 2: unique exact + if confident_sim(best, second): + return ("reuse", sim_id) # Tier 3: confident sim + return ("mint", None) # Tier 4: mint new + + +def match_descriptor(descriptor, candidates, lineage_id=None): + """Convenience wrapper over `resolve_component_id`. + + descriptor : {"fingerprint": ..., "text": ...} + candidates : [{"id": ..., "fingerprint": ..., "text": ...}] + + Computes `exact_count` (# candidates whose fingerprint == descriptor's), `exact_id` (the sole exact + match's id when the count is exactly 1), and `best`/`second`/`sim_id` from `_line_similarity` of the + descriptor's text against each candidate's text, then calls `resolve_component_id`. Returns + `("reuse", id)` or `("mint", None)`.""" + fp = descriptor.get("fingerprint") + text = descriptor.get("text") + + exact = [c for c in candidates if c.get("fingerprint") == fp] + exact_count = len(exact) + exact_id = exact[0].get("id") if exact_count == 1 else None + + # Best / second similarity across candidates, tracking the best candidate's id. + best, second, sim_id = 0, 0, None + for c in candidates: + sim = _line_similarity(text, c.get("text")) + if sim > best: + second = best + best = sim + sim_id = c.get("id") + elif sim > second: + second = sim + + return resolve_component_id(lineage_id, exact_count, exact_id, best, second, sim_id) + + +# ================================================================ +# 2c — STAMP component_ids on a trace (durable component identity) +# ================================================================ +# +# `assign_component_ids` walks the trace's model artifacts oldest-first, groups their top-level symbols +# into stable COMPONENTS via the proved resolver above, and returns the grouping. It is the record-time +# realization of identity.iml's `resolve` (which decides SAME vs NEW per descriptor): each symbol either +# REUSES a known component id (lineage / unique-exact / confident-unique similarity) or MINTS a fresh +# `cmpN`. The dangerous error is conflation, so the resolver mints when the signal is weak or ambiguous. +# +# The point: a component_id FOLLOWS A RENAME (clamp -> clamp_int, identical body -> same cmp), so goal +# rooting and staleness can chain across the rename by component instead of by name. Purely additive: +# the caller (enrich) STAMPS the ids onto a COPY/projection; the source trace on disk is never mutated. + + +def _same_model_line(m1, m2): + """Are two model artifacts revisions of the SAME model line (share a `derived_from` source node)? + Mirrors goals.py `_same_model_line`: bare models (no `derived_from`) are treated as one evolving + line. Used to supply the lineage tier — a symbol carried across two revisions of one model line is a + producer-declared same-model-line link, the highest-confidence identity signal.""" + d1 = set(m1.get("derived_from") or []) + d2 = set(m2.get("derived_from") or []) + if not d1 and not d2: + return True + return bool(d1 & d2) + + +def assign_component_ids(trace): + """Group the trace's model symbols into stable components and STAMP the ids onto the trace's + descriptors (mutates the trace passed in — call on a COPY / the enrich projection, never the source). + + Walks model artifacts (`artifact_type` in `_MODEL_TYPES`) in ascending `producer_action_id`. Keeps a + running list of known components `[{id, fingerprint, text, names, model}]`. For each top-level symbol + of each model, builds its NAME-INDEPENDENT descriptor (`_symbol_descriptor`, exactly as merge.py) and + resolves it against the known components with the proved `match_descriptor`: + + * lineage tier — if a known component last appeared in a model on the SAME model line as this one + (shared `derived_from`) and under the SAME name, that is a producer-declared same-model-line link + -> its id is passed as `lineage_id` (Tier 1: lineage wins). + * `("reuse", id)` -> the same component: update its fingerprint / text / names / model to this + (latest) revision. + * `("mint", None)` -> a new component, id `f"cmp{n}"`. + + Stamps, on the trace: + * each model artifact -> `payload.component_ids = {symbol_name: component_id}`. + * each VerificationGoal -> `payload.target_component_id` = the component id of its `target_symbol` + AS OF that goal's revision (the latest component id known for that name at/ before the goal's + `producer_action_id`). + + Returns `{"components": [...], "by_name": {name: component_id}}` where `by_name` is LATEST-wins — the + convenience map a goal criterion authored with a NAME uses to reach the current component id.""" + # Imported lazily to avoid any import-order coupling (goals.py imports this module transitively). + from .merge import _symbol_descriptor + from .goals import _top_level_defs, _model_src, _MODEL_TYPES + + arts = trace.get("artifacts", []) or [] + models = [a for a in arts + if a.get("artifact_type") in _MODEL_TYPES and _model_src(a)] + models.sort(key=lambda a: (a.get("producer_action_id") or 0)) + + known = [] # [{id, fingerprint, text, names:set, model}] + n_minted = [0] + + def _mint(): + cid = f"cmp{n_minted[0]}" + n_minted[0] += 1 + return cid + + # Per-name history of (step, component_id) so a VerificationGoal resolves to the component id current + # AT its own revision — not merely the global latest (which would misattribute a pre-rename goal). + name_history = {} # name -> [(step, component_id)] in ascending step order + + for m in models: + step = m.get("producer_action_id") or 0 + src = _model_src(m) + defs = _top_level_defs(src) + stamp = {} + claimed = set() # component ids already stamped by an EARLIER symbol of THIS same model + for sym in defs: + desc = _symbol_descriptor(src, sym) + # Two top-level defs that COEXIST in one model are necessarily DISTINCT components — a + # component already claimed by an earlier symbol of this same model is not a candidate for a + # later one (otherwise two identical-body siblings would conflate onto one id). + avail = [c for c in known if c["id"] not in claimed] + # Lineage tier: a known component that last lived on the SAME model line under the SAME name. + lineage_id = None + for c in avail: + if sym in c["names"] and c.get("model") is not None and _same_model_line(c["model"], m): + lineage_id = c["id"] + break + candidates = [{"id": c["id"], "fingerprint": c["fingerprint"], "text": c["text"]} + for c in avail] + decision, cid = match_descriptor(desc, candidates, lineage_id=lineage_id) + if decision == "reuse": + comp = next(c for c in known if c["id"] == cid) + comp["fingerprint"] = desc["fingerprint"] + comp["text"] = desc["text"] + comp["names"].add(sym) + comp["model"] = m + else: + cid = _mint() + known.append({"id": cid, "fingerprint": desc["fingerprint"], "text": desc["text"], + "names": {sym}, "model": m}) + stamp[sym] = cid + claimed.add(cid) + name_history.setdefault(sym, []).append((step, cid)) + m.setdefault("payload", {})["component_ids"] = stamp + + def _comp_at(name, at): + """The component id known for `name` as of step `at` (latest at/before `at`; else the earliest).""" + hist = name_history.get(name) + if not hist: + return None + prior = [(s, c) for (s, c) in hist if s <= at] + chosen = prior[-1] if prior else hist[0] + return chosen[1] + + # Latest-wins name -> component id, for a NAME-authored criterion to reach the current component. + by_name = {} + for name, hist in name_history.items(): + by_name[name] = hist[-1][1] + + # Stamp each VerificationGoal with the component id of its target_symbol as of that goal's revision. + for a in arts: + if a.get("artifact_type") != "VerificationGoal": + continue + p = a.get("payload") or {} + tsym = p.get("target_symbol") + if not tsym: + continue + cid = _comp_at(tsym, a.get("producer_action_id") or 0) + if cid is not None: + a.setdefault("payload", {})["target_component_id"] = cid + + return {"components": known, "by_name": by_name} + + +# ================================================================ +# §8.8 Phase 2: selector resolver — enumerate the elements a quantifier ranges over +# ================================================================ +# +# A selector maps to a list of ELEMENTS, element = {symbol, component_id?, file?}. It reuses the data the +# trace already carries: model top-level symbols (_top_level_defs), the component_ids stamped by +# assign_component_ids, model/source file paths, and high_stakes_paths. Deduped by component_id (stable +# identity) else symbol. An unknown/empty selector returns [] — the quantifier turns [] into `todo` +# (never a vacuous `done`; see eval_formula). + +_SRC_EXTS = ("py", "ts", "tsx", "js", "jsx", "mjs", "cjs", "iml", "ml", "go", "rs", "java", "kt", "cs", "scala", "fs") + + +def _artifact_path(a): + """Best-effort file path for an artifact: a producer-stamped path field, else a name/summary that + looks like a path. None when the trace carries no path (then glob/module can't place the symbol).""" + p = a.get("payload") or {} + for k in ("path", "file", "file_path", "src_path", "source_file", "source_path"): + v = p.get(k) or a.get(k) + if isinstance(v, str) and v: + return v + for k in ("name", "summary"): + v = a.get(k) + if isinstance(v, str) and ("/" in v or v.rsplit(".", 1)[-1] in _SRC_EXTS): + return v + return None + + +def _model_file(model, trace): + """The source file a model came from: the model's own path, else its SourceCode ancestor's.""" + f = _artifact_path(model) + if f: + return f + by_id = {a.get("artifact_id"): a for a in (trace.get("artifacts") or [])} + for src_id in (model.get("derived_from") or []): + src = by_id.get(src_id) + if src is not None: + f = _artifact_path(src) + if f: + return f + return None + + +def _symbol_index(trace): + """Latest-per-symbol element list across model artifacts: {symbol, component_id?, file?}. Reads the + component_ids stamped by assign_component_ids when present (else component_id is None).""" + from .goals import _top_level_defs, _model_src, _MODEL_TYPES + arts = trace.get("artifacts") or [] + models = sorted([a for a in arts if a.get("artifact_type") in _MODEL_TYPES and _model_src(a)], + key=lambda a: (a.get("producer_action_id") or 0)) + idx = {} # symbol -> element (latest model wins) + for m in models: + stamp = (m.get("payload") or {}).get("component_ids") or {} + f = _model_file(m, trace) + for sym in _top_level_defs(_model_src(m)): + idx[sym] = {"symbol": sym, "component_id": stamp.get(sym), "file": f} + return list(idx.values()) + + +def _dedup(elements): + """De-dup by component_id (stable identity) else symbol, order-preserving.""" + seen, out = set(), [] + for e in elements: + key = ("cid", e["component_id"]) if e.get("component_id") else ("sym", e.get("symbol")) + if key in seen: + continue + seen.add(key) + out.append(e) + return out + + +def resolve_selector(sel, trace, goal=None): + """Resolve a §8.8 selector to a list of elements {symbol, component_id?, file?}. Supported: + {"glob": "payments/**"} -- symbols whose source file matches the glob (needs file paths). + {"module": "pricing"} -- symbols whose file path contains that module/path segment. + {"scope": true} -- the resolving goal's `scope` symbols (synthesized if unknown to the trace). + {"tag": ""} -- BEST-EFFORT over `high_stakes_paths` (the only tag-like surface today). + Returns [] for an unknown/empty selector.""" + if not isinstance(sel, dict): + return [] + index = _symbol_index(trace) + if "glob" in sel: + pat = sel.get("glob") or "" + return _dedup([e for e in index if e.get("file") and fnmatch.fnmatch(e["file"], pat)]) + if "module" in sel: + mod = (sel.get("module") or "").strip() + if not mod: + return [] + + def _in_module(f): + if not f: + return False + return mod in re.split(r"[\\/.]", f) or mod in f + return _dedup([e for e in index if _in_module(e.get("file"))]) + if "scope" in sel and sel.get("scope"): + scope = list((goal or {}).get("scope") or []) + by_sym = {e["symbol"]: e for e in index} + return _dedup([by_sym.get(s) or {"symbol": s, "component_id": None, "file": None} for s in scope]) + if "tag" in sel: + # DOCUMENTED GAP: there is no real symbol->tag index in the trace today. The one tag-like surface + # is `high_stakes_paths` (substring path fragments), which is NOT keyed by tag name — so a `tag` + # selector matches symbols whose source file contains a high-stakes fragment, REGARDLESS of the tag + # name (we cannot tell "money" from "risk" without a real tag source). A proper symbol->tag index + # is future work; this is the honest best-effort over what exists. + stakes = trace.get("high_stakes_paths") or [] + return _dedup([e for e in index if e.get("file") and any(p in e["file"] for p in stakes)]) + return [] diff --git a/cli/ponens/emit.py b/cli/ponens/emit.py index 010b369..5ae603a 100644 --- a/cli/ponens/emit.py +++ b/cli/ponens/emit.py @@ -14,6 +14,7 @@ import json import os +import re import sys import uuid from collections import Counter @@ -179,11 +180,12 @@ def _synthesize_artifacts(actions): since the last commit) and produce a TestResult / Commit. Wires action inputs/outputs so every consumed artifact has a strictly-earlier producer (data_flow_integrity holds).""" artifacts = [] + residuals = [] # derived counter-evidence (e.g. a failing test run → an open defeater) file_art = {} # file path -> latest artifact id (its current version) working = {} # file path -> artifact id, edited since the last commit n = 0 - def _new(atype, name, producer, derived=None, summary=None): + def _new(atype, name, producer, derived=None, summary=None, status=None, payload=None): nonlocal n n += 1 art = {"artifact_id": f"art{n}", "artifact_type": atype, "name": name, @@ -192,6 +194,10 @@ def _new(atype, name, producer, derived=None, summary=None): art["derived_from"] = list(dict.fromkeys(derived)) if summary: art["summary"] = summary + if status: + art["status"] = status + if payload: + art["payload"] = payload artifacts.append(art) return art["artifact_id"] @@ -210,11 +216,25 @@ def _new(atype, name, producer, derived=None, summary=None): a["outputs"] = list(dict.fromkeys(a.get("outputs", []) + outs)) elif t == "RunTests": ins = list(working.values()) + v = a.get("test_verdict") or {} + counts = {k: v[k] for k in ("passed", "failed") if v.get(k) is not None} aid = _new("TestResult", _short(a.get("label", "tests"), 50), a["id"], ins or None, - _short(a.get("result_summary"), 200) if a.get("result_summary") else None) + _short(a.get("result_summary"), 200) if a.get("result_summary") else None, + status=v.get("status"), payload=counts or None) if ins: a["inputs"] = list(dict.fromkeys(a.get("inputs", []) + ins)) a["outputs"] = list(dict.fromkeys(a.get("outputs", []) + [aid])) + # A failing run is live counter-evidence: an OPEN defeater on the TestResult so a + # `tested(component)` obligation blocks (§18.2), rather than resolving on mere existence. + if v.get("status") == "failed": + residuals.append({ + "residual_id": f"test-fail-{aid}", "kind": "defeater", + "severity": "high", "status": "open", + "statement": "Tests failed: " + (_short(a.get("result_summary"), 160) or _short(a.get("label", "tests"), 80)), + "suggested_check": "Fix the failing tests and re-run.", + "target": {"target_type": "artifact", "target_id": aid}, + "derived": True, + }) elif t == "GitCommit": ins = list(working.values()) aid = _new("Commit", _short(a.get("label", "commit"), 50), a["id"], ins or None) @@ -222,7 +242,23 @@ def _new(atype, name, producer, derived=None, summary=None): a["inputs"] = list(dict.fromkeys(a.get("inputs", []) + ins)) a["outputs"] = list(dict.fromkeys(a.get("outputs", []) + [aid])) working.clear() - return artifacts + return artifacts, residuals + + +_TEST_FAILED_RE = re.compile(r"(\d+)\s+fail", re.I) # "2 failed", "1 failure" +_TEST_PASSED_RE = re.compile(r"(\d+)\s+pass", re.I) # "148 passed" + + +def _test_verdict(output, errored): + """Best-effort pass/fail from a test runner's output. Trusts an explicit failure count and the + tool's error flag; deliberately conservative (no fuzzy keyword matching) so a test *named* `error` + or a stray 'fail' in a log line can't manufacture a false failure.""" + text = str(output or "") + fm, pm = _TEST_FAILED_RE.search(text), _TEST_PASSED_RE.search(text) + failed = int(fm.group(1)) if fm else None + passed = int(pm.group(1)) if pm else None + status = "failed" if (errored or (failed or 0) > 0) else "passed" + return {"status": status, "passed": passed, "failed": failed} def _build_action(ev, aid, cur_dir, active_task): @@ -266,6 +302,10 @@ def _build_action(ev, aid, cur_dir, active_task): action["reproducibility"]["expected_output"] = {"result_summary": result_summary} if result_summary: action["result_summary"] = result_summary + # A test run carries a structured verdict (parsed from the FULL result, before truncation) so the + # synthesized TestResult means "passed / failed", not merely "ran". + if ev.get("type") == "RunTests": + action["test_verdict"] = _test_verdict(result, ev.get("error")) return action @@ -318,7 +358,7 @@ def build_trace(parsed, title=None, summarize=False): a.pop(k, None) # derive the lineage DAG, and attribute each produced artifact to its meta-action - artifacts = _synthesize_artifacts(actions) + artifacts, synth_residuals = _synthesize_artifacts(actions) a_by_id = {a["id"]: a for a in actions} m_by_id = {m["id"]: m for m in meta_actions} for art in artifacts: @@ -341,7 +381,7 @@ def build_trace(parsed, title=None, summarize=False): "artifacts": artifacts, "policies": [], "policy_evaluations": [], - "residuals": [], + "residuals": synth_residuals, "files_modified": sorted(set(files_modified)), "reproducibility": { "status": "partially_reproducible", diff --git a/cli/ponens/goals.py b/cli/ponens/goals.py index cbc4530..df8d5bc 100644 --- a/cli/ponens/goals.py +++ b/cli/ponens/goals.py @@ -91,10 +91,13 @@ def _canon_art_type(s): return _ART_TYPE_ALIASES.get(k, k) -def _resolve_typed(item, trace): +def _resolve_typed(item, trace, gate_defeater=True, gate_fresh=False): """Resolve a typed criterion (`component` + `evidence: {artifact}`) by lineage: MET iff an artifact of the required type roots in the component. Quality of derivation is left to policies. Returns a - resolution dict, or None if the item is not a typed criterion (caller falls back to legacy).""" + resolution dict, or None if the item is not a typed criterion (caller falls back to legacy). + + `gate_defeater` / `gate_fresh` are the role gates (§8.8): the defaults reproduce today's behavior + exactly (defeater-gated, not freshness-gated); `met` clears `gate_defeater`, `governed` sets both.""" compd = item.get("component") or {} # A criterion may name the source `function` (for display / authoring) AND a formal `symbol` — the # name the engine actually gave the formalization (e.g. source `clamp` -> IML `clamp_decomp`). The @@ -117,14 +120,19 @@ def _resolve_typed(item, trace): if not matches: return keep a = max(matches, key=lambda x: x.get("producer_action_id") or 0) # the latest such artifact + aid = a.get("artifact_id") # Counter-evidence (§13 Defeater / §18.2): an OPEN defeater contesting the evidence (or the provenance # it derives from) blocks the criterion — a contested result is never done, exactly like the legacy # property path. This is what makes a FAILING conformance (its ConformanceResult carries an undermines - # defeater) leave a `conformance` criterion unmet, not silently `done` on mere existence. - contest_ids = {a.get("artifact_id")} | set(a.get("derived_from") or []) - if _open_defeater_contests(contest_ids, trace): - return {"status": "blocked", "from_trace": True, "evidence": a.get("artifact_id")} - return {"status": "done", "from_trace": True, "evidence": a.get("artifact_id")} + # defeater) leave a `conformance` criterion unmet, not silently `done` on mere existence. Role-gated: + # the default (and `governed`) apply it; `met` = mere existence, so it does not. + contest_ids = {aid} | set(a.get("derived_from") or []) + if gate_defeater and _open_defeater_contests(contest_ids, trace): + return {"status": "blocked", "from_trace": True, "evidence": aid} + # Freshness (§18.3): `governed` additionally requires the evidence be non-stale. + if gate_fresh and _evidence_stale(aid, trace): + return {"status": "blocked", "from_trace": True, "evidence": aid} + return {"status": "done", "from_trace": True, "evidence": aid} def _open_defeater_contests(ids, trace): @@ -143,11 +151,40 @@ def _open_defeater_contests(ids, trace): return False -def resolve_item(item, trace): - """Resolve one acceptance item to {status, from_trace, evidence} against the trace's evidence.""" +# ================================================================ +# §8.8 property-language front-end: formula AST + recursive evaluator (Phase 1) +# ================================================================ +# +# The evidence logic is the design of record for acceptance; its LEAF ATOMS already exist (the kind / +# typed resolution in `_resolve_criterion` below). Phase 1 adds the COMBINATOR layer so criteria +# compose. A `formula` is JSON the agent can author: +# {"atom": , "role"?: "met"|"governed"} -- a leaf; is the legacy item shape +# {"and": [F, ...]} {"or": [F, ...]} {"not": F} {"implies": [F, F]} +# `role` (inherited down a subtree) gates HOW an atom is judged, orthogonal to the boolean shape: +# (default, no role) -- today's behavior: the evidence EXISTS and is UNCONTESTED (defeater-gated), +# NOT freshness-gated. A desugared legacy item uses this → identical results. +# "met" -- the evidence merely EXISTS (no defeater / no freshness gate). +# "governed" -- EXISTS and UNCONTESTED and FRESH (§18.3). +# Phase 1 = combinators + roles only. Selectors / quantifiers (forall/exists over glob/module/tag) and +# stable property ids (properties(S)) are later phases; the AST is shaped to accept a future +# {"forall": {"in": , "holds": F}} node without disturbing this layer. + + +def _evidence_stale(aid, trace): + """True if an OPEN stale/detached residual (§18.3) targets `aid`. Used only by the `governed` + role; recomputed per governed atom (Phase 1 simplicity — `governed` is opt-in and rare).""" + if not aid: + return False + return any((r.get("target") or {}).get("target_id") == aid for r in stale_evidence(trace)) + + +def _resolve_criterion(item, trace, gate_defeater=True, gate_fresh=False): + """Resolve ONE leaf criterion (an atom) to {status, from_trace, evidence}. This is the historical + kind-switch, now parameterized by the two gates the role selects. The defaults + (gate_defeater=True, gate_fresh=False) are exactly today's behavior.""" # Goal Contract typed criterion (component + evidence) → resolve by lineage (§4), not text. if item.get("component") is not None and item.get("evidence") is not None: - typed = _resolve_typed(item, trace) + typed = _resolve_typed(item, trace, gate_defeater, gate_fresh) if typed is not None: return typed keep = {"status": item.get("status", "todo"), "from_trace": False, "evidence": None} @@ -191,11 +228,14 @@ def resolve_item(item, trace): vr = max(vrs, key=lambda a: a.get("producer_action_id") or 0) s = _lc(_payload(vr).get("status")) st = "done" if s in ("proved", "sat") else "blocked" if s == "refuted" else "doing" - # Counter-evidence (§13 Defeater / §18.2): an OPEN defeater contesting the result (or its goal) - # blocks it — a contested proof is never done, exactly like a refutation. - if st == "done" and _open_defeater_contests({vr.get("artifact_id")} | vg_ids, trace): + vid = vr.get("artifact_id") + # Counter-evidence (§13 / §18.2): a contested proof is never done — role-gated (`met` skips it). + if st == "done" and gate_defeater and _open_defeater_contests({vid} | vg_ids, trace): + st = "blocked" + # Freshness (§18.3): `governed` additionally requires the proof be non-stale. + if st == "done" and gate_fresh and _evidence_stale(vid, trace): st = "blocked" - return {"status": st, "from_trace": True, "evidence": vr.get("artifact_id")} + return {"status": st, "from_trace": True, "evidence": vid} if kind == "change": sym = binding.get("symbol") @@ -208,6 +248,144 @@ def resolve_item(item, trace): return keep +# ---- status lattice: compose child STATUSES (not booleans) so doing/blocked propagate ------------- +# DESIGN DECISION (reviewable): a criterion resolves to a 4-valued status, not a bool, so the +# combinators lift and/or/not/implies over {done, doing, todo, blocked}: +# and: blocked if ANY blocked; else done if ALL done; else doing if ANY done|doing; else todo. +# or : done if ANY done; else doing if ANY doing; else blocked if ALL blocked; else todo. +# not: done<->todo; doing->doing; blocked->blocked (contested stays contested — absence of proof is +# not proof of absence; a defeater against P is not evidence FOR not-P. Defeasible; documented.) +# implies(a, b) = or(not(a), b). +# Empty and/or -> todo (no evidence), avoiding a vacuous `done`. + +def _pick_evidence(rs, want): + """Best-effort representative evidence id: prefer a child whose status drove the result, else any.""" + for r in rs: + if r.get("status") == want and r.get("evidence"): + return r.get("evidence") + for r in rs: + if r.get("evidence"): + return r.get("evidence") + return None + + +def _combine(status, rs, want_for_evidence): + return {"status": status, + "from_trace": any(r.get("from_trace") for r in rs), + "evidence": _pick_evidence(rs, want_for_evidence)} + + +def _combine_and(rs): + ss = [r.get("status") for r in rs] + if any(s == "blocked" for s in ss): + return _combine("blocked", rs, "blocked") + if rs and all(s == "done" for s in ss): + return _combine("done", rs, "done") + if any(s in ("done", "doing") for s in ss): + return _combine("doing", rs, "doing") + return _combine("todo", rs, "doing") + + +def _combine_or(rs): + ss = [r.get("status") for r in rs] + if any(s == "done" for s in ss): + return _combine("done", rs, "done") + if any(s == "doing" for s in ss): + return _combine("doing", rs, "doing") + if rs and all(s == "blocked" for s in ss): + return _combine("blocked", rs, "blocked") + return _combine("todo", rs, "doing") + + +_NOT_STATUS = {"done": "todo", "todo": "done", "doing": "doing", "blocked": "blocked"} + + +def _combine_not(r): + return {"status": _NOT_STATUS.get(r.get("status"), "todo"), + "from_trace": r.get("from_trace", False), "evidence": None} + + +def _empty_resolution(): + return {"status": "todo", "from_trace": False, "evidence": None} + + +def _subst_atom(atom, env): + """Substitute a bound quantifier variable into an atom's element slots (§8.8 Phase 2). An inner atom + references the bound element as `{"component": {"var": "f"}}` and/or `binding: {"symbol": {"var": + "f"}}`; at eval time the element's concrete symbol replaces it. No-op with no env / no `var` refs.""" + if not env or not isinstance(atom, dict): + return atom + a = dict(atom) + comp = a.get("component") + if isinstance(comp, dict) and "var" in comp: + el = env.get(comp["var"]) or {} + a["component"] = {"function": el.get("symbol"), "symbol": el.get("symbol")} + b = a.get("binding") + if isinstance(b, dict): + nb = dict(b) + for k in ("symbol", "property"): + v = nb.get(k) + if isinstance(v, dict) and "var" in v: + nb[k] = (env.get(v["var"]) or {}).get("symbol") + a["binding"] = nb + return a + + +def eval_formula(node, trace, inherited_role=None, env=None, goal=None): + """Recursively resolve a formula node to {status, from_trace, evidence}. `role` on any node is + inherited by descendant atoms that don't set their own; `env` carries quantifier variable bindings + (var -> element); `goal` is the resolving goal (its `scope` feeds the `{"scope": true}` selector).""" + if not isinstance(node, dict): + return _empty_resolution() + role = node.get("role", inherited_role) + if "atom" in node: + return _resolve_criterion(_subst_atom(node["atom"], env), trace, + gate_defeater=(role != "met"), gate_fresh=(role == "governed")) + if "and" in node: + return _combine_and([eval_formula(c, trace, role, env, goal) for c in (node.get("and") or [])]) + if "or" in node: + return _combine_or([eval_formula(c, trace, role, env, goal) for c in (node.get("or") or [])]) + if "not" in node: + return _combine_not(eval_formula(node.get("not"), trace, role, env, goal)) + if "implies" in node: + parts = node.get("implies") or [] + a = eval_formula(parts[0], trace, role, env, goal) if len(parts) > 0 else _empty_resolution() + b = eval_formula(parts[1], trace, role, env, goal) if len(parts) > 1 else _empty_resolution() + return _combine_or([_combine_not(a), b]) + if "forall" in node or "exists" in node: + is_forall = "forall" in node + q = (node.get("forall") if is_forall else node.get("exists")) or {} + from .component import resolve_selector # lazy: component imports goals transitively + elements = resolve_selector(q.get("in"), trace, goal) + # Empty selector -> todo (REVIEWABLE DECISION): an empty match is almost always a mis-spec, and a + # vacuous `done` (∀ over ∅) would be false-green — the dangerous direction. Same for exists. + if not elements: + return _empty_resolution() + var = q.get("as") or "x" + holds = q.get("holds") + results = [eval_formula(holds, trace, role, {**(env or {}), var: el}, goal) for el in elements] + return _combine_and(results) if is_forall else _combine_or(results) + return _empty_resolution() + + +def eval_atom(atom, trace, role=None, env=None): + """Resolve a single leaf criterion under a role (None = default/today, 'met', 'governed').""" + return _resolve_criterion(_subst_atom(atom, env), trace, + gate_defeater=(role != "met"), gate_fresh=(role == "governed")) + + +def resolve_item(item, trace, goal=None): + """Resolve one acceptance item to {status, from_trace, evidence} against the trace's evidence. + + §8.8: if the item carries a `formula`, evaluate the AST (quantifier selectors read `goal.scope`). + Otherwise the item IS a single leaf criterion (the legacy kind-switch / typed criterion), desugared + to an atom with the default role — byte-for-byte identical to before the formula layer existed.""" + formula = item.get("formula") + if formula is not None: + return eval_formula(formula, trace, goal=goal) + return _resolve_criterion(item, trace, gate_defeater=True, gate_fresh=False) + + def progress_of(items): if not items: return 0.0 @@ -362,6 +540,29 @@ def _freshness_verdict(vr, sym, proved_at, arts): return None +def _freshness_verdict_renamed(vr, old_sym, new_sym, proved_at, arts): + """Freshness of a result recorded against `old_sym` whose component is now named `new_sym` (2d, + component-identity rename path). The stored (proof-time) signal is `old_sym`'s closure checksum in + the model current AT proof time (the model that still defined `old_sym`); the current signal is + `new_sym`'s closure checksum in the latest model that defines `new_sym`. A mismatch is "stale"; equal + (a pure rename, identical body) is "fresh"; None when it can't be recomputed (caller falls back).""" + step = lambda a: a.get("producer_action_id") or 0 # noqa: E731 + src_models = [a for a in arts if a.get("artifact_type") in _MODEL_TYPES and _model_src(a)] + old_defs = [m for m in src_models if old_sym in _top_level_defs(_model_src(m))] + new_defs = [m for m in src_models if new_sym in _top_level_defs(_model_src(m))] + if not old_defs or not new_defs: + return None + stored_ck = (_payload(vr).get("fingerprint") or {}).get("task_checksum") + if stored_ck is None: + prior = [m for m in old_defs if step(m) <= proved_at] or old_defs + stored_ck = _closure_checksum(_model_src(max(prior, key=step)), old_sym) + cur_model = max(new_defs, key=step) + cur_ck = _closure_checksum(_model_src(cur_model), new_sym) + if cur_ck is not None and stored_ck is not None: + return "fresh" if cur_ck == stored_ck else "stale" + return None + + def stale_evidence(trace): """Proofs invalidated by a later model change (Stale) or by their target's removal (Detached), as derived residuals (tagged `derived: True`). TRACE_SPEC §18.3. @@ -406,23 +607,58 @@ def _candidate(a): return ("ssa", sym, label, True) # a decomposition is always standing evidence return None - latest = {} # (kind, sym) -> (step, art, label, standing) + # Component-identity (2d): when the trace carries stamped `component_ids` (via assign_component_ids, + # injected by enrich), key the latest-per grouping on the COMPONENT id instead of the raw symbol name + # — so a proof of `clamp` and a later model that renamed it to `clamp_int` chain as the SAME component + # (the proof correctly follows the rename and goes stale). The current name of a component is read + # from the latest model's stamped map, so the freshness closure is recomputed under the CURRENT name. + # Additive: absent component_ids, `_component_id_for` returns None and the key is (kind, sym) as before. + comp_by_name = lineage._component_by_name(trace) # name -> component_id (latest wins) + # component_id -> its CURRENT name: walk model stamps in ascending producer order so the latest + # model's name for a component wins (a rename's newest name, not an arbitrary dict order). + cur_name_of_comp = {} + _stamped_models = sorted( + (a for a in arts if a.get("artifact_type") in _MODEL_TYPES and _payload(a).get("component_ids")), + key=lambda a: a.get("producer_action_id") or 0) + for m in _stamped_models: + for name, cid in (_payload(m).get("component_ids") or {}).items(): + cur_name_of_comp[cid] = name + + def _component_id_for(a, sym): + """The component id stamped for this result's target, or None (pre-2d / unstamped).""" + if a.get("artifact_type") == "VerificationResult": + vg = _vg_for(a) + cid = _payload(vg).get("target_component_id") if vg else None + else: + cid = _payload(a).get("target_component_id") + return cid or comp_by_name.get(sym) + + latest = {} # (kind, key) -> (step, art, label, standing, sym, comp_id) for a in arts: c = _candidate(a) if not c: continue kind, sym, label, standing = c step = a.get("producer_action_id") or 0 - key = (kind, sym) + comp_id = _component_id_for(a, sym) + key = (kind, comp_id) if comp_id is not None else (kind, sym) if key not in latest or step > latest[key][0]: - latest[key] = (step, a, label, standing) + latest[key] = (step, a, label, standing, sym, comp_id) out = [] - for (kind, sym), (at, art, label, standing) in latest.items(): + for _key, (at, art, label, standing, sym, comp_id) in latest.items(): if not standing: continue vid = art.get("artifact_id") - verdict = _freshness_verdict(art, sym, at, arts) + # Follow the rename: check freshness under the component's CURRENT name when it differs from the + # name the result was recorded against (e.g. proof of `clamp`, component now named `clamp_int`). + # The rename path compares the OLD name's proof-time closure against the NEW name's current + # closure, so a renamed+changed component goes stale; a pure rename stays fresh. + fresh_sym = cur_name_of_comp.get(comp_id, sym) if comp_id is not None else sym + if fresh_sym != sym: + verdict = _freshness_verdict_renamed(art, sym, fresh_sym, at, arts) + else: + verdict = _freshness_verdict(art, sym, at, arts) if verdict == "fresh": continue if verdict == "detached": @@ -728,6 +964,12 @@ def enrich(trace): The source trace (authored goals + emitted steps) is untouched. """ t = copy.deepcopy(trace) + # Component identity (2c/2d): stamp durable component_ids onto the enrich PROJECTION (never the + # source trace) so the downstream consumers — roots_in_component (goal rooting) and stale_evidence + # (freshness) — can FOLLOW A RENAME by component instead of by name. Purely additive: on a trace with + # no stampable models the stamp is empty and every consumer is byte-identical to its pre-2d behavior. + from .component import assign_component_ids + assign_component_ids(t) # Residuals are first-class artifacts (§13, v1.8): fold any legacy list forward, then merge the # derived stale-evidence residuals in as Residual artifacts so the viewer sees a single surface. lineage.migrate_residuals(t) @@ -763,10 +1005,28 @@ def _freshness_for(aid): return fr return None + # An OPEN drift residual the EXTENSION emitted for this evidence (freshness `limitation`/`defeater` + # over a stale/gone/hand-edited artifact), related to the evidence id. Lets the hash-based at_risk + # path name a residual + carry its statement, exactly like the structural stale_evidence path, so + # `at_risk_residual_id`/`at_risk_reason` are populated consistently however the drift was detected. + _DRIFT_KINDS = {"limitation", "defeater", "stale_evidence"} + + def _drift_residual_for(aid): + if not aid: + return None + for r in lineage.residual_surface(t): + if str(r.get("status") or "open").lower() != "open" or r.get("kind") not in _DRIFT_KINDS: + continue + rel = r.get("related_artifact_ids") or [] + if any(aid == x or (isinstance(aid, str) and isinstance(x, str) + and (aid.startswith(x + "-") or x.startswith(aid + "-"))) for x in rel): + return r + return None + for g in t.get("goals", []): resolved = [] for item in g.get("acceptance", []): - r = resolve_item(item, t) + r = resolve_item(item, t, goal=g) it = dict(item) it["status"] = r["status"] it["from_trace"] = r["from_trace"] @@ -788,9 +1048,16 @@ def _freshness_for(aid): it["at_risk_residual_id"] = stale.get("residual_id") elif fr in ("stale", "gone"): it["at_risk"] = True - it["at_risk_reason"] = ("The source was removed since this was verified." - if fr == "gone" - else "The code changed since this was verified — re-check to restore the guarantee.") + # Name the extension's drift residual when present, so this path carries an + # `at_risk_residual_id` + statement like the structural path above. + drift = _drift_residual_for(r["evidence"]) + if drift: + it["at_risk_reason"] = drift.get("statement") + it["at_risk_residual_id"] = drift.get("residual_id") + else: + it["at_risk_reason"] = ("The source was removed since this was verified." + if fr == "gone" + else "The code changed since this was verified — re-check to restore the guarantee.") resolved.append(it) g["acceptance"] = resolved g["progress"] = progress_of(resolved) diff --git a/cli/ponens/lineage.py b/cli/ponens/lineage.py index f6a78f5..fd0bccb 100644 --- a/cli/ponens/lineage.py +++ b/cli/ponens/lineage.py @@ -5,7 +5,7 @@ and does its provenance root in a given code component / kind of step?" — e.g. does this `VerificationResult` trace back to autoformalizing `settle`? -This is the substrate for Goal-Contract acceptance resolution (GOAL_CONTRACT_v0_1 §4 — resolve by +This is the substrate for Goal-Contract acceptance resolution (GOAL_CONTRACT_v0_2 §4 — resolve by lineage, not description text) and for provenance policies (APPLY_FORMAL_METHODS_PACK — "a proof or a decomposition in its lineage"). Kept dependency-free (walks the trace dict only) so both `goals.py` and the policy engine can use it without an import cycle. @@ -84,9 +84,55 @@ def source_symbols(artifact_id, trace): def roots_in_component(artifact_id, component, trace): """Does this artifact's lineage rest SPECIFICALLY on the given component (function / symbol)? An artifact that declares its own `target_symbol` is about THAT symbol — not every symbol the shared - model formalized. Only when nothing in the lineage names a target do we fall back to model symbols.""" + model formalized. Only when nothing in the lineage names a target do we fall back to model symbols. + + ADDITIVE component-identity path (2d): when the trace carries stamped `component_ids` (via + `assign_component_ids`, injected by enrich), the artifact ALSO roots in `component` if its own (or a + lineage ancestor's) `target_component_id` equals the component id that the NAME `component` currently + resolves to. This makes rooting FOLLOW A RENAME (clamp -> clamp_int chains to the same component id). + The result is `name_result OR component_id_result` — purely additive: a trace with no component_ids + is byte-identical to the pre-2d behavior, and nothing that matched by name before stops matching.""" specific, model = _lineage_symbols(artifact_id, trace) - return component in specific if specific else component in model + name_result = component in specific if specific else component in model + if name_result: + return True + + # Component-identity alternative — only when the trace has been stamped. + by_name = _component_by_name(trace) + if not by_name: + return False + want = by_name.get(component) + if want is None: + return False + return want in _lineage_component_ids(artifact_id, trace) + + +def _component_by_name(trace): + """The trace's LATEST-wins `name -> component_id` map, recovered from stamped `component_ids` on + model artifacts (`assign_component_ids`). Empty dict when the trace was never stamped — the signal + that turns the whole component-identity path off (pre-2d behavior). Latest wins: model artifacts are + read in ascending `producer_action_id` so a later revision's mapping overrides an earlier one.""" + models = [a for a in trace.get("artifacts", []) or [] + if isinstance(a, dict) and (_payload(a).get("component_ids"))] + models.sort(key=lambda a: a.get("producer_action_id") or 0) + out = {} + for m in models: + for name, cid in (_payload(m).get("component_ids") or {}).items(): + out[name] = cid + return out + + +def _lineage_component_ids(artifact_id, trace): + """The set of `target_component_id`s stamped on an artifact's lineage (self + ancestors) — mirrors + `_lineage_symbols`'s specific-target read, but over the stamped component id. A VerificationResult + has no target of its own; its VerificationGoal (an ancestor) carries the `target_component_id`.""" + out = set() + for a in lineage_artifacts(artifact_id, trace): + p = _payload(a) + cid = p.get("target_component_id") or a.get("target_component_id") + if cid: + out.add(cid) + return out def autoformalized(artifact_id, trace): diff --git a/cli/ponens/merge.py b/cli/ponens/merge.py new file mode 100644 index 0000000..38b114d --- /dev/null +++ b/cli/ponens/merge.py @@ -0,0 +1,593 @@ +"""Residual-aware trace MERGE: carry forward the provably-unaffected standing results, flag the rest. + +This is the THIN, sound-but-conservative Python realization of the proved merge-composition model in +`formal/merge/{delta,classify}.iml` (the conformance spec). Scope: the SkipDisjoint, SkipContract, and +ReReason branches — the SkipContract / opaque-contract branch is implemented for the SOUND slice only +(`uninterpreted`-abstracted dependencies). A `contract` whose callee changed has a stale discharge and +would need re-proof (no reproof formula is recorded in the trace), so it re-reasons; `pinned`/`concrete`/ +no-assumption re-reason too. Anything not provably safe collapses onto ReReason (never-false-fresh). + +The pipeline mirrors the IML: + * merge_delta ~ delta.iml — the component-wise change set THEIRS introduces vs the ancestor. The + never-guess rule is automatic: any checksum divergence counts as + `changed`, so nothing genuinely-changed is ever dropped from the delta. + * classify ~ classify.iml — per standing result R over `touched = closure ∩ delta`: + touched == ∅ -> SkipDisjoint (CarriedForward); + else, EVERY touched dep is `uninterpreted` in OURS's model assumptions + -> SkipContract (CarriedForward, basis "uninterpreted-opaque"): the + result proved its property for ALL values of the opaque dep, so any + merge change to it leaves the property holding; + else -> ReReason (a `needs_rereasoning` + residual). The proved classifier's opaque `dep_kind` is realized by + the model's structured `payload.assumptions` (`_assumptions_index`). + +`merge()` returns a REPORT projection; it never mutates its inputs. + +Reuses goals.py for all the IML-source machinery (top-level defs, symbol closure, closure checksum), +and replicates stale_evidence's "standing result" extraction so the two derived views agree on what a +standing result IS. +""" + +from .goals import ( + _top_level_defs, + _symbol_closure, + _closure_checksum, + _model_src, + _payload, + _lc, + _MODEL_TYPES, +) +from . import lineage +from .component import match_descriptor + + +# ================================================================ +# Trace-level source / symbol helpers (over the model artifacts) +# ================================================================ + +def _trace_defs(trace): + """Every top-level def in the trace's model source. The model artifacts (types in `_MODEL_TYPES`) + carry inline IML under `payload.formal_code`/`iml_code`; we concatenate them in ASCENDING + `producer_action_id` order so a LATER revision of a symbol overwrites an earlier one (the latest + revision wins), matching the freshness convention in goals.py.""" + return _top_level_defs(_concat_src(trace)) + + +def _concat_src(trace): + """The trace's model source, concatenated in ascending producer-action order (latest revision last + so `_top_level_defs` keeps the newest definition of each symbol).""" + models = [a for a in trace.get("artifacts", []) or [] + if a.get("artifact_type") in _MODEL_TYPES and _model_src(a)] + models.sort(key=lambda a: a.get("producer_action_id") or 0) + return "\n".join(_model_src(a) for a in models) + + +def _symbol_checksum(trace, sym): + """Checksum of `sym`'s definition + its full dependency closure in the trace's model source, or None + if `sym` is not defined anywhere in the trace.""" + return _closure_checksum(_concat_src(trace), sym) + + +def _symbols(trace): + """The set of top-level def names defined in the trace's model source.""" + return set(_trace_defs(trace).keys()) + + +def _standing_results(trace): + """The latest STANDING result per (kind, symbol): proved/sat VerificationResults (via their + VerificationGoal's `target_symbol`) and StateSpaceAnalysisResults (via `target_symbol`). Replicates + stale_evidence's candidate + latest-per-(kind,sym) logic so both derived views agree on the standing + set. Returns a list of {result_id, kind, symbol}.""" + arts = trace.get("artifacts", []) or [] + by_id = {a.get("artifact_id"): a for a in arts} + + def _vg_for(vr): + vg = by_id.get(_payload(vr).get("goal_artifact_id")) + if not (vg and vg.get("artifact_type") == "VerificationGoal"): + vg = next((a for a in arts if a.get("artifact_type") == "VerificationGoal" + and _payload(a).get("goal_id") == _payload(vr).get("goal_id")), None) + return vg + + def _candidate(a): + t = a.get("artifact_type") + if t == "VerificationResult": + status = _lc(_payload(a).get("status")) + # Only a standing PROOF (proved/sat) survives a merge as evidence; a refutation is a live + # issue, not a fact to carry forward — so it is not a standing result here. + if status not in ("proved", "sat"): + return None + vg = _vg_for(a) + sym = _payload(vg).get("target_symbol") if vg else None + if not sym: + return None + return ("vr", sym) + if t == "StateSpaceAnalysisResult": + sym = _payload(a).get("target_symbol") + if not sym: + return None + return ("ssa", sym) + return None + + latest = {} # (kind, sym) -> (step, art) + for a in arts: + c = _candidate(a) + if not c: + continue + kind, sym = c + step = a.get("producer_action_id") or 0 + key = (kind, sym) + if key not in latest or step > latest[key][0]: + latest[key] = (step, a) + + return [{"result_id": art.get("artifact_id"), "kind": kind, "symbol": sym} + for (kind, sym), (_step, art) in latest.items()] + + +# ================================================================ +# Delta (delta.iml) — the change set THEIRS introduces vs the ancestor +# ================================================================ + +import hashlib as _hashlib +import re as _re + + +def _symbol_descriptor(src, sym): + """A component descriptor for `sym` in `src`: {fingerprint, text}. + + The fingerprint is a NAME-INDEPENDENT content fingerprint of `sym`'s definition: the def text with + the symbol's OWN name replaced by a placeholder before hashing, so a pure rename (same body, new + name) yields the SAME fingerprint — which is exactly what lets tier-2 exactness distinguish a + rename-unchanged (identical fingerprint) from a rename-changed (different fingerprint). Renaming a + symbol necessarily edits its signature line, so a plain closure checksum would ALWAYS differ across a + rename and could never witness "content unchanged". `text` is the raw def block — the concrete signal + `_line_similarity` compares (the similarity tier tolerates the changed signature line).""" + defs = _top_level_defs(src) + text = defs.get(sym, "") + normed = _re.sub(r"\b" + _re.escape(sym) + r"\b", "\x00SYM\x00", text) + fp = "sha256-body:" + _hashlib.sha256(normed.encode("utf-8")).hexdigest() + return {"id": sym, "fingerprint": fp, "text": text} + + +def merge_delta(ours, theirs, base=None): + """The component-wise change set THEIRS introduces relative to the ancestor (`base` if given, else + `ours`). For each symbol in the union of symbols across the traces: + * in THEIRS, absent in the reference -> added, + * in the reference, absent in THEIRS -> removed, + * in both but closure-checksum differs -> changed. + + RENAME-AWARENESS (component-identity aware, via `match_descriptor`): a symbol renamed by THEIRS looks + like a name-based remove+add, which over-fires (the caller re-reasons needlessly). After the + name-based sets are computed, each `removed` symbol `r` is matched (as a descriptor) against the + `added` symbols (as candidates) with the PROVED resolver: + * reuse with IDENTICAL fingerprint -> a rename, content unchanged: drop `r` from removed and the + matched symbol from added, record it under `renamed` (changed: False) — NOT a change, so NOT in + the delta set. + * reuse with a DIFFERENT fingerprint -> a rename, content changed: drop from removed/added, record + under `renamed` (changed: True), and add `r` to `changed` (one changed component, not remove+add). + * mint (no confident/unique match, incl. the never-guess ambiguous case) -> genuinely removed: `r` + stays in removed and any unmatched added stay in added (conservative, sound). + + `added ∪ removed ∪ changed` (renamed-unchanged excluded) is the full delta set. When no rename is + detected the output is byte-for-byte the pre-rename behavior (`renamed` is empty).""" + reference = base if base is not None else ours + ref_src = _concat_src(reference) + their_src = _concat_src(theirs) + ref_syms = _symbols(reference) + their_syms = _symbols(theirs) + added, removed, changed = [], [], [] + for sym in sorted(ref_syms | their_syms): + in_ref = sym in ref_syms + in_theirs = sym in their_syms + if in_theirs and not in_ref: + added.append(sym) + elif in_ref and not in_theirs: + removed.append(sym) + else: # in both + if _symbol_checksum(theirs, sym) != _symbol_checksum(reference, sym): + changed.append(sym) + + # Rename reconciliation: match each removed symbol against the still-available added symbols. + renamed = [] + if removed and added: + available = list(added) # candidates consumed as they are matched (each added maps to ≤1 rename) + still_removed = [] + for r in removed: + r_desc = _symbol_descriptor(ref_src, r) + candidates = [_symbol_descriptor(their_src, a) for a in available] + decision, matched = match_descriptor(r_desc, candidates) + if decision != "reuse": + still_removed.append(r) # mint / ambiguous -> genuinely removed + continue + available.remove(matched) # this added symbol is the rename target, not a new add + matched_fp = next(c["fingerprint"] for c in candidates if c["id"] == matched) + content_changed = matched_fp != r_desc["fingerprint"] + renamed.append({"from": r, "to": matched, "changed": content_changed}) + if content_changed: + changed.append(r) # one changed component (its old name), not remove+add + removed = still_removed + added = available + + delta = {"changed": sorted(changed), "added": sorted(added), "removed": sorted(removed)} + if renamed: + delta["renamed"] = renamed + return delta + + +def _delta_symbols(delta): + """The flat delta set: added ∪ removed ∪ changed. Renamed-unchanged symbols are deliberately absent + (they are not a change), so they never force a re-reason.""" + return set(delta["changed"]) | set(delta["added"]) | set(delta["removed"]) + + +# ================================================================ +# Assumption abstraction index (dep_kind, from the model's structured assumptions) +# ================================================================ + +def _assumptions_index(trace): + """`target -> abstraction` over the trace's model artifacts, the trace-level realization of the + proved classifier's opaque `dep_kind ∈ {Uninterpreted, Typed, Axiomatized, Pinned}`. + + A model artifact records the dependencies it abstracted as structured `payload.assumptions`, a list of + `{target, abstraction, discharged?, ...}` where `abstraction ∈ 'concrete'|'contract'|'uninterpreted'| + 'pinned'` (the producer's `ArtifactAssumption`). We scan every model artifact (`_MODEL_TYPES`) and map + each assumption's `target` to its `abstraction`; the LATEST model revision wins (ascending + `producer_action_id`, so a later entry for the same target overwrites an earlier one), matching the + freshness convention elsewhere in this module. Tolerant: missing/empty `assumptions`, or an entry + lacking `target`/`abstraction`, is skipped.""" + out = {} + models = [a for a in trace.get("artifacts", []) or [] if a.get("artifact_type") in _MODEL_TYPES] + models.sort(key=lambda a: a.get("producer_action_id") or 0) + for a in models: + for asm in _payload(a).get("assumptions", []) or []: + if not isinstance(asm, dict): + continue + target = asm.get("target") + abstraction = asm.get("abstraction") + if not target or not abstraction: + continue + out[target] = _lc(abstraction) + return out + + +# ================================================================ +# Coverage regression (SelectorRegression, realized over goal.scope) +# ================================================================ + +def _in_scope(name, scope): + """Is component `name` in a goal's `scope`? Reuses goals.py's scope predicate: a scope entry (case- + insensitively) SUBSTRING-matches the component name. `scope` is the goal's raw `scope` list.""" + if not name: + return False + hay = _lc(name) + return any(_lc(s) in hay for s in scope if s) + + +# ================================================================ +# Residual-awareness — open assumptions standing on a result +# ================================================================ + +def _assumptions_in_question(result_id, trace): + """Ids of OPEN `assumption`-kind residuals in `trace` whose `related_artifact_ids` include + `result_id`. A re-reasoned result that stood on an open assumption cites it as an extra cause. Coarse + — we do not re-check the assumption here, only surface that it is in question.""" + out = [] + for r in lineage.residual_surface(trace): + if _lc(r.get("kind")) != "assumption": + continue + if _lc(r.get("status") or "open") != "open": + continue + if result_id in (r.get("related_artifact_ids") or []): + out.append(r.get("residual_id")) + return out + + +# ================================================================ +# The merge report (classify.iml, thin: SkipDisjoint | ReReason) +# ================================================================ + +def merge(ours, theirs, base=None): + """Combine two traces: carry forward the provably-unaffected standing results of OURS, flag the rest + for re-reasoning. A REPORT projection — inputs are never mutated. + + For each standing result R of symbol `sym` from OURS: + * closure = `sym`'s dependency closure in OURS's model source, + * touched = closure ∩ delta_syms, + * touched == ∅ -> SkipDisjoint -> carried_forward + (basis "closure-disjoint"), + * else, EVERY component in `touched` is `uninterpreted` in OURS's assumptions -> SkipContract -> + carried_forward (basis "uninterpreted-opaque", recording the relied-on `via_assumptions`), + * else -> ReReason -> a + needs_rereasoning residual. + """ + delta = merge_delta(ours, theirs, base=base) + delta_syms = _delta_symbols(delta) + defs = _trace_defs(ours) + standing = _standing_results(ours) + assumptions_idx = _assumptions_index(ours) + reference = base if base is not None else ours + ref_src = _concat_src(reference) + their_src = _concat_src(theirs) + + def _own_body_changed(t): + """Did component `t`'s OWN definition body change between the reference and THEIRS (name-independent + fingerprint)? A touched component that is only in the delta because a DEPENDENCY of it changed (its + own body is byte-identical) is not itself an obstacle to a SkipContract carry-forward — only a + genuine change to its own body is.""" + return _symbol_descriptor(ref_src, t)["fingerprint"] != _symbol_descriptor(their_src, t)["fingerprint"] + + carried, rereason = [], [] + for r in standing: + rid, sym = r["result_id"], r["symbol"] + closure = _symbol_closure(sym, defs) # includes sym itself when defined + # A symbol OURS proved about but that isn't in OURS's own model source has an empty closure; + # fall back to the bare symbol so a direct touch of it is still caught. + if not closure: + closure = {sym} + touched = sorted(closure & delta_syms) + if not touched: + carried.append({ + "result_id": rid, + "symbol": sym, + "kind": r["kind"], + "closure": sorted(closure), + "basis": "closure-disjoint", + }) + continue + + # SkipContract (sound slice): every touched component that genuinely CHANGED its own body is an + # `uninterpreted` dependency in OURS's model assumptions. The result proved its property for ALL + # possible values of each such opaque dep, so any merge change to it leaves the property holding — + # carry forward. A touched component whose OWN body is unchanged (in the delta only because a + # dependency of it changed) is not itself an obstacle. Requires ALL genuinely-changed touched + # components be uninterpreted; a single non-opaque change (concrete/contract/pinned/absent — incl. + # the result's own symbol changing its body) falls through to ReReason. A contract's discharge is + # stale once its callee changed and there is no recorded reproof formula, so contracts are + # (soundly) NOT skipped here (future work: reproof needs the formula). + changed_touched = [t for t in touched if _own_body_changed(t)] + if changed_touched and all(assumptions_idx.get(t) == "uninterpreted" for t in changed_touched): + carried.append({ + "result_id": rid, + "symbol": sym, + "kind": r["kind"], + "closure": sorted(closure), + "basis": "uninterpreted-opaque", + "via_assumptions": changed_touched, + }) + else: + assumptions = _assumptions_in_question(rid, ours) + cause = "closure-changed" + statement = (f"Standing result `{rid}` about `{sym}` needs re-reasoning: the merge touched " + f"{', '.join('`%s`' % t for t in touched)} in its dependency closure.") + if assumptions: + statement += (f" It also stands on open assumption(s) " + f"{', '.join('`%s`' % a for a in assumptions)}, now in question.") + rereason.append({ + "residual_id": f"rereason-{rid}", + "kind": "needs_rereasoning", + "status": "open", + "result_id": rid, + "symbol": sym, + "touched": touched, + "cause": cause, + "assumptions_in_question": assumptions, + "statement": statement, + "derived": True, + "target": {"target_type": "artifact", "target_id": rid}, + }) + + # Totality (the proved invariant, classify_total + basis_disjoint restricted to the two branches): + # every standing result is bucketed EXACTLY once — the standing set == disjoint union of + # carried_forward ∪ rereason (none missing, none in both). + standing_ids = [r["result_id"] for r in standing] + carried_ids = [c["result_id"] for c in carried] + rereason_ids = [rr["result_id"] for rr in rereason] + totality_ok = ( + len(carried_ids) + len(rereason_ids) == len(standing_ids) + and set(carried_ids).isdisjoint(rereason_ids) + and set(carried_ids) | set(rereason_ids) == set(standing_ids) + ) + + coverage_regressions = _coverage_regressions(ours, theirs, delta) + + report = { + "delta": delta, + "carried_forward": carried, + "rereason": rereason, + "totality_ok": totality_ok, + "counts": { + "standing": len(standing_ids), + "carried": len(carried_ids), + "rereason": len(rereason_ids), + "delta": len(delta_syms), + }, + } + # Purely additive: only surface the field when there is something to report, so a merge with no + # scoped goals (or no in-scope membership change) is byte-for-byte its pre-coverage output. + if coverage_regressions: + report["coverage_regressions"] = coverage_regressions + return report + + +import copy as _copy + + +def combine(ours, theirs, base=None): + """Materialize `merge(ours, theirs, base)` into a VALID merged trace (not just the report). + + The merged trace is a deepcopy of OURS — it carries the standing results + goals we reason about — + then augmented so it faithfully records the two-parent COMBINE and the merge's findings: + + 1. MergeEvent (two-parent provenance): a top-level `merge` field naming both parents + the base, a + fresh `trace_id`, and a `trace_links` entry recording the parents. The merged trace's own + `derived_from` DAG stays well-founded (the two-parent link lives in `merge`/`trace_links`, not in + the artifact DAG). + 2. Overlay theirs's changed/added model artifacts so the merged trace reflects the incoming code + (union by `artifact_id`; on collision prefer THEIRS's version for a changed/added component). + 3. Materialize the findings: + * each `carried_forward` entry -> a `CarriedForward` artifact, + * each `rereason` entry -> a `needs_rereasoning` residual, + * each `coverage_regression` -> a `coverage_regression` residual. + 4. A `merge` action so the materialized artifacts/residuals have a resolvable `producer_action_id`. + 5. Totality: every standing result of the parents is represented exactly once (a CarriedForward + artifact OR a needs_rereasoning residual) — asserted before returning. + + `merge()` is reused verbatim; neither input trace is mutated (the skeleton is a deepcopy).""" + report = merge(ours, theirs, base=base) + + merged = _copy.deepcopy(ours) + ours_id = ours.get("trace_id") + theirs_id = theirs.get("trace_id") + base_id = base.get("trace_id") if base is not None else None + merged["trace_id"] = f"merge-{ours_id}-{theirs_id}" + + # 1. MergeEvent — two-parent provenance recorded off the artifact DAG. + merged["merge"] = { + "parents": [ours_id, theirs_id], + "base": base_id, + "kind": "merge", + } + links = merged.setdefault("trace_links", []) + links.append({"kind": "merge", "parents": [ours_id, theirs_id], "base": base_id}) + + arts = merged.setdefault("artifacts", []) + + # 2. Overlay theirs's changed/added model artifacts. `changed`/`added` name the components THEIRS + # revised/introduced; bring in the model artifacts of THEIRS that carry those symbols, preferring + # theirs's version on an artifact_id collision (dedup by artifact_id). + changed_added = set(report["delta"].get("changed", [])) | set(report["delta"].get("added", [])) + if changed_added: + their_models = [a for a in theirs.get("artifacts", []) or [] + if a.get("artifact_type") in _MODEL_TYPES and _model_src(a)] + by_id = {a.get("artifact_id"): i for i, a in enumerate(arts)} + for m in their_models: + syms = set(_top_level_defs(_model_src(m)).keys()) + if not (syms & changed_added): + continue + aid = m.get("artifact_id") + m_copy = _copy.deepcopy(m) + if aid in by_id: + arts[by_id[aid]] = m_copy # prefer theirs's version for a changed/added component + else: + by_id[aid] = len(arts) + arts.append(m_copy) + + # 4. A merge action (added first so its id is available to the materialized artifacts/residuals). + existing_ids = [a.get("id") for a in merged.get("actions", []) or [] if isinstance(a.get("id"), int)] + merge_action_id = (max(existing_ids) + 1) if existing_ids else 1 + merged.setdefault("actions", []).append({ + "id": merge_action_id, + "type": "merge", + "rationale": "combine ours + theirs", + }) + + # 3a. CarriedForward artifacts — one per carried result. + for c in report["carried_forward"]: + rid = c["result_id"] + arts.append({ + "artifact_id": f"carried-{rid}", + "artifact_type": "CarriedForward", + "producer_action_id": merge_action_id, + "derived_from": [rid], + "payload": { + "basis": c.get("basis"), + "symbol": c.get("symbol"), + "closure": c.get("closure"), + }, + }) + + # 3b/3c. Residuals — needs_rereasoning (per re-reasoned result) and coverage_regression. + residuals = merged.setdefault("residuals", []) + for rr in report["rereason"]: + residuals.append({ + "residual_id": rr["residual_id"], + "kind": "needs_rereasoning", + "status": rr.get("status", "open"), + "statement": rr.get("statement"), + "derived": True, + "introduced_by_action_id": merge_action_id, + "target": rr.get("target"), + }) + for cr in report.get("coverage_regressions", []): + residuals.append({ + "residual_id": cr["residual_id"], + "kind": "coverage_regression", + "status": cr.get("status", "open"), + "statement": cr.get("statement"), + "severity": cr.get("severity"), + "derived": True, + "introduced_by_action_id": merge_action_id, + "goal_id": cr.get("goal_id"), + }) + + # 5. Totality: every standing result is represented exactly once (CarriedForward OR needs_rereasoning). + standing_ids = {r["result_id"] for r in _standing_results(ours)} + carried_ids = {c["result_id"] for c in report["carried_forward"]} + rereason_ids = {rr["result_id"] for rr in report["rereason"]} + assert carried_ids.isdisjoint(rereason_ids), "combine: a result was both carried and re-reasoned" + assert carried_ids | rereason_ids == standing_ids, "combine: standing results not totally represented" + assert report["totality_ok"], "combine: merge report totality invariant failed" + + return merged + + +def _coverage_regressions(ours, theirs, delta): + """Goal-COVERAGE layer of the merge (SelectorRegression, realized over `goal.scope`): a merge that + changes WHAT A GOAL MUST COVER — adds/removes an in-scope component — regresses the obligation, even + when no existing proof's closure changed (that's the distinct RESULT-level concern above). + + For each OURS goal with a non-empty `scope`: + * added in-scope, unproven -> regression. A component in `delta["added"]` that is in the goal's + scope AND has NO covering standing result in the MERGED view (no proved/sat VerificationResult or + StateSpaceAnalysisResult about it) widened the goal's surface with unproven ground. + * removed in-scope -> coverage shrank (lower severity: the goal's surface got smaller). + + Renames are already reconciled by `merge_delta` (matched renames are excluded from `added`/`removed`), + so using the post-rename delta sets here never double-counts a rename as add+remove. + + One entry per affected goal, aggregating its added/removed members. Returns [] when no goal has scope + or no membership changed.""" + goals = ours.get("goals", []) or [] + if not goals: + return [] + added = delta.get("added", []) + removed = delta.get("removed", []) + if not added and not removed: + return [] + + # Covering evidence in the MERGED view: a component is "covered" if there is a standing proof/ssa + # about it in EITHER side (the added symbol comes from theirs, so its proof — if any — lives there). + covered = {r["symbol"] for r in _standing_results(ours)} + covered |= {r["symbol"] for r in _standing_results(theirs)} + + out = [] + for i, goal in enumerate(goals): + scope = goal.get("scope", []) or [] + if not scope: + continue + added_members = [c for c in added if _in_scope(c, scope) and c not in covered] + removed_members = [c for c in removed if _in_scope(c, scope)] + if not added_members and not removed_members: + continue + gid = goal.get("id") or goal.get("goal_id") or goal.get("intent") or f"goal-{i}" + parts = [] + if added_members: + parts.append(f"gained {len(added_members)} in-scope unproven component(s) " + f"({', '.join(added_members)})") + if removed_members: + parts.append(f"lost {len(removed_members)} in-scope component(s) " + f"({', '.join(removed_members)})") + # Added unproven ground is the hard regression; a pure shrink is a lower-severity note. + severity = "medium" if added_members else "low" + out.append({ + "residual_id": f"coverage-{gid}", + "kind": "coverage_regression", + "status": "open", + "derived": True, + "goal_id": gid, + "scope": scope, + "added_members": added_members, + "removed_members": removed_members, + "statement": f"Goal `{gid}` " + "; ".join(parts) + ".", + "severity": severity, + }) + return out diff --git a/cli/ponens/oracles.py b/cli/ponens/oracles.py new file mode 100644 index 0000000..ee6fa84 --- /dev/null +++ b/cli/ponens/oracles.py @@ -0,0 +1,302 @@ +"""Oracles — invocable evidence producers, the supertype of *reasoner*. + +An **oracle** is anything that produces evidence about a target and returns it as trace +artifacts: a formal reasoner (ImandraX, an SMT solver, a model checker), a test runner, a +static analyzer, an LLM-judge, or a human attestor. This aligns the code with the paper's +vocabulary ("which oracle produced it, under what assumptions") — a *reasoner* is simply the +formal, proof-producing subtype of oracle. + +Two orthogonal classifiers: + - ``oracle_type`` — the *mechanism* (reasoner | tester | analyzer | judge | attestor) + - ``evidence_strength`` — the *guarantee* (proof > sat > tests > static_analysis > attested) + +The gallery/catalog side (reference metadata, remote registry) lives in ``reasoners.py`` and is +retained; this module adds the *invocable* runtime side — the ``Oracle`` an SDK ``Session`` can +call to actually produce evidence. See ``spec/ORACLE_SPEC_v0_1.md``. +""" +from __future__ import annotations + +import hashlib +import os +import shutil +import subprocess +import tempfile + +# --- taxonomy --------------------------------------------------------------- + +# Mechanism of an oracle. "reasoner" is the formal, proof-producing subtype. +ORACLE_TYPES = ("reasoner", "tester", "analyzer", "judge", "attestor") + +# Guarantee carried by an oracle's output, strongest first. `strength_rank` lets callers +# compare/sort evidence (a policy can demand "at least `tests`", a merge can prefer stronger). +EVIDENCE_STRENGTH = ("proof", "sat", "tests", "static_analysis", "attested") + +# Legacy `reasoners` catalog `kind` -> oracle_type (all current reasoners are the formal subtype). +_KIND_TO_TYPE = { + "formal_verification": "reasoner", + "smt": "reasoner", + "model_checking": "reasoner", +} + + +def strength_rank(s: str) -> int: + """Rank of an evidence strength (0 = strongest). Unknown strengths sort last.""" + return EVIDENCE_STRENGTH.index(s) if s in EVIDENCE_STRENGTH else len(EVIDENCE_STRENGTH) + + +def oracle_type_for_kind(kind: str | None) -> str: + """Map a legacy reasoner ``kind`` to an ``oracle_type`` (defaults to ``reasoner``).""" + return _KIND_TO_TYPE.get(kind or "", "reasoner") + + +# --- the Oracle base -------------------------------------------------------- + +class Oracle: + """Base class for an invocable evidence producer. + + Subclasses set the class attributes and implement ``invoke(target, context) -> [artifact]``, + returning a list of artifact dicts (without ``artifact_id``/``producer_action_id`` — the SDK + assigns those). Each artifact's payload should carry ``evidence_strength``. + """ + + id: str = "oracle" + name: str = "Oracle" + oracle_type: str = "reasoner" + evidence_strength: str = "attested" + produces: tuple[str, ...] = () + vendor: str = "" + description: str = "" + + def invoke(self, target, context=None): # pragma: no cover - abstract + raise NotImplementedError + + def as_dict(self) -> dict: + return { + "id": self.id, + "name": self.name, + "oracle_type": self.oracle_type, + "evidence_strength": self.evidence_strength, + "produces": list(self.produces), + "vendor": self.vendor, + "description": self.description, + } + + +# --- the CodeLogician oracle (oracle #1: proof strength) -------------------- +# Drives Imandra's `codelogician-lite` CLI (the LLM-friendly front end to the ImandraX engine), +# not the raw engine: `codelogician-lite check-vg --json` executes the `verify`/`instance` +# goals in an IML model and returns per-goal proved / refuted (with counterexample) / bounded / unknown. + + +def _codelogician_bin(): + """The codelogician-lite command: env override (CODELOGICIAN_CLI) then PATH.""" + return os.environ.get("CODELOGICIAN_CLI") or shutil.which("codelogician-lite") + + +def _eval_ok(eval_res) -> bool: + """Did the model admit? `eval_res` is "Success" (string) or {success: bool, ...}.""" + if isinstance(eval_res, str): + return "success" in eval_res.lower() + if isinstance(eval_res, dict): + return eval_res.get("success") is True + return False + + +def _verdict_of(vg_res) -> str: + """Per-goal verdict from a `check-vg` `vg_res` object (proved > refuted > sat > unknown).""" + if not isinstance(vg_res, dict): + return "unknown" + if vg_res.get("refuted"): + return "refuted" + if vg_res.get("proved"): + return "proved" + if vg_res.get("verified_upto"): + return "sat" # bounded — verified up to a depth, not a full proof + return "unknown" + + +def _counterexample(vg_res): + r = vg_res.get("refuted") if isinstance(vg_res, dict) else None + if isinstance(r, dict): + return r.get("model_str") or r.get("model") or r.get("src") + return str(r) if r else None + + +def _aggregate(verdicts) -> str: + """Fold per-goal verdicts into one result status (a refutation dominates).""" + if not verdicts: + return "unknown" + if "refuted" in verdicts: + return "refuted" + if all(v == "proved" for v in verdicts): + return "proved" + if all(v in ("proved", "sat") for v in verdicts): + return "sat" + return "unknown" + + +def _codelogician_lite_runner(target, context=None): + """Run `codelogician-lite check-vg --json` and aggregate the verdicts. + + `target` is a dict carrying `iml_code` (the model + its verify/instance goals). Returns the + fields of a VerificationResult payload. Dependency-injectable so tests / CLI-less environments + don't require the tool. ImandraX (over the CodeLogician CLI) is the engine. + """ + iml = target.get("iml_code") if isinstance(target, dict) else None + fingerprint = hashlib.sha256((iml or "").encode("utf-8")).hexdigest()[:16] if iml else None + binp = _codelogician_bin() + if not binp or not iml: + return {"status": "unknown", "engine": "imandrax", + "result": "codelogician-lite or iml_code unavailable", + "reasoning_fingerprint": fingerprint} + fd, path = tempfile.mkstemp(suffix=".iml") + try: + with os.fdopen(fd, "w") as f: + f.write(iml) + proc = subprocess.run([binp, "check-vg", path, "--json"], + capture_output=True, text=True, timeout=600) + try: + data = json.loads(proc.stdout) + except (ValueError, TypeError): + return {"status": "unknown", "engine": "imandrax", + "result": ((proc.stdout or "") + (proc.stderr or "")).strip()[-2000:], + "reasoning_fingerprint": fingerprint} + if not _eval_ok(data.get("eval_res")): + return {"status": "unknown", "engine": "imandrax", + "result": f"admit failed: {data.get('eval_res')}", + "reasoning_fingerprint": fingerprint} + vgs = data.get("vg_res_list") or [] + verdicts = [_verdict_of(v.get("vg_res")) for v in vgs] + cex = next((_counterexample(v.get("vg_res")) for v in vgs + if _verdict_of(v.get("vg_res")) == "refuted"), None) + return {"status": _aggregate(verdicts), "engine": "imandrax", + "result": (f"{len(vgs)} VG(s): " + ", ".join(verdicts)) if verdicts + else "no verification goals", + "reasoning_fingerprint": fingerprint, "counterexample": cex} + except (subprocess.SubprocessError, OSError) as ex: + return {"status": "unknown", "engine": "imandrax", + "result": f"codelogician-lite error: {ex}", "reasoning_fingerprint": fingerprint} + finally: + try: + os.unlink(path) + except OSError: + pass + + +# Status -> the honest strength of the established evidence (None when nothing was established, +# so an `unknown`/error result never masquerades as graded evidence). +_STATUS_STRENGTH = {"proved": "proof", "refuted": "proof", "sat": "sat"} + + +class CodeLogicianOracle(Oracle): + """CodeLogician (ImandraX engine, via `codelogician-lite`) — a proof-strength reasoner oracle. + + `invoke(target)` runs the target's verify/instance goals and returns a `VerificationResult` + whose `evidence_strength` reflects the *actual* verdict (proved/refuted → proof, bounded → sat, + otherwise unestablished and unlabeled). The runner is injectable for testing / CLI-less use. + """ + + id = "codelogician" + name = "CodeLogician" + oracle_type = "reasoner" + evidence_strength = "proof" + produces = ("VerificationResult", "StateSpaceAnalysisResult") + vendor = "Imandra" + description = "CodeLogician drives ImandraX (via codelogician-lite) — proof-strength verification." + + def __init__(self, runner=None): + self.runner = runner or _codelogician_lite_runner + + def invoke(self, target, context=None): + res = self.runner(target, context) + goal = target.get("goal") if isinstance(target, dict) else None + symbol = target.get("target_symbol") if isinstance(target, dict) else None + status = res.get("status", "unknown") + payload = { + "status": status, + "engine": res.get("engine", "imandrax"), + "result": res.get("result", ""), + "reasoning_fingerprint": res.get("reasoning_fingerprint"), + } + strength = _STATUS_STRENGTH.get(status) + if strength: + payload["evidence_strength"] = strength + if res.get("counterexample"): + payload["counterexample"] = res["counterexample"] + if symbol: + payload["target_symbol"] = symbol + return [{ + "artifact_type": "VerificationResult", + "artifact_role": "CounterexampleRole" if status == "refuted" else "ProofRole", + "name": f"verify:{goal or symbol or 'target'}", + "format": "json", + "payload": payload, + }] + + +# --- in-process registry (the invocable oracles) ---------------------------- + +_REGISTRY: dict[str, Oracle] = {} + + +def register_oracle(oracle: Oracle) -> None: + _REGISTRY[oracle.id] = oracle + + +def get_oracle(oracle_id: str) -> Oracle | None: + return _REGISTRY.get(oracle_id) + + +def list_oracles() -> list[Oracle]: + return list(_REGISTRY.values()) + + +# Built-in oracles available out of the box. +register_oracle(CodeLogicianOracle()) + + +# --- CLI: `ponens oracle list|show` ----------------------------------------- + +def register(subparsers): + from .formatting import heading, table, gray, cyan, blue, magenta + + op = subparsers.add_parser( + "oracle", help="Inspect invocable oracles (reasoner is the formal subtype)") + sub = op.add_subparsers(dest="oracle_command", required=True) + + def cmd_list(args): + import json as _json + rows = [o.as_dict() for o in list_oracles()] + if getattr(args, "json", False): + print(_json.dumps(rows, indent=2, ensure_ascii=False)) + return 0 + heading(f"Oracles ({len(rows)})") + if not rows: + print(gray(" none registered")) + return 0 + table(rows, [ + {"label": "ID", "get": lambda e: e["id"], "color": cyan}, + {"label": "Name", "get": lambda e: e.get("name", "")}, + {"label": "Type", "get": lambda e: e.get("oracle_type", ""), "color": magenta}, + {"label": "Evidence", "get": lambda e: e.get("evidence_strength", ""), "color": blue}, + {"label": "Produces", "get": lambda e: ", ".join(e.get("produces", []))}, + ]) + print(gray("\n a reasoner is the formal, proof-producing subtype of oracle")) + return 0 + + p = sub.add_parser("list", aliases=["ls"], help="List invocable oracles") + p.add_argument("--json", action="store_true") + p.set_defaults(func=cmd_list) + + def cmd_show(args): + import json as _json + o = get_oracle(args.oracle_id) + if not o: + print(gray(f" no such oracle: '{args.oracle_id}'")) + return 1 + print(_json.dumps(o.as_dict(), indent=2, ensure_ascii=False)) + return 0 + + p = sub.add_parser("show", help="Show an oracle's definition") + p.add_argument("oracle_id") + p.set_defaults(func=cmd_show) diff --git a/cli/ponens/sdk.py b/cli/ponens/sdk.py new file mode 100644 index 0000000..1d89be7 --- /dev/null +++ b/cli/ponens/sdk.py @@ -0,0 +1,198 @@ +"""ponens.sdk — a thin runtime SDK for building agents that *speak ponens* natively. + +Instead of reconstructing a trace from a transcript after the fact (``ponens emit``), an agent +instruments itself as it runs: open a ``Session``, record actions and artifacts, invoke oracles +for evidence, and on exit get a validated trace that passes ``ponens trace check``. + +The SDK is deliberately thin: it builds the same JSON-native trace dict the rest of ``ponens`` +already uses (via ``trace.create_empty_trace`` / ``next_action_id`` / ``save_trace``), so there is +exactly one trace model and one code path for constructing artifacts and lineage. + + from ponens.sdk import Session + + with Session(model="claude-opus", assistant="my-agent", path="trace.json", + intent="prove charge() is idempotent") as s: + a = s.action("EditFile", label="edit pricing.py", rationale="fix retry path", + evidence=[{"type": "FileRef", "ref": "pricing.py"}]) + model = s.artifact("IMLModel", name="pricing.iml", content=iml_src, format="iml", + producer_action_id=a) + s.verify({"iml_code": iml_src, "goal": "idempotent charge"}, + oracle="imandra-x", derived_from=model) +""" +from __future__ import annotations + +from . import trace as trace_mod +from . import objects as objects_mod +from . import oracles as oracles_mod + + +class Session: + """A live reasoning trace under construction. + + Use as a context manager (recommended): on exit it stamps an outcome if none was set, + validates, externalizes large blobs, and writes ``path`` if one was given. + """ + + def __init__(self, model="example-model", assistant="ponens", path=None, + intent=None, trigger=None): + self.trace = trace_mod.create_empty_trace(model=model, assistant=assistant) + self.path = path + if trigger or intent: + self.trace["trigger"] = {"type": "TaskReceived", "text": trigger or intent} + if intent: + self.goal(intent) + + # --- recording primitives ------------------------------------------------ + + def action(self, type, label=None, rationale=None, detail=None, category="activity", + inputs=None, outputs=None, evidence=None): + """Record a step; returns its integer action id.""" + aid = trace_mod.next_action_id(self.trace) + act = { + "id": aid, + "type": type, + "category": category, + "label": label or type, + "rationale": rationale or "", + "detail": detail or "", + "inputs": list(inputs or []), + "outputs": list(outputs or []), + "evidence": list(evidence or []), + } + self.trace["actions"].append(act) + return aid + + def artifact(self, artifact_type, name=None, payload=None, derived_from=None, + producer_action_id=None, content=None, format=None, role=None): + """Record a typed artifact; returns its artifact id. Large ``content`` is + content-addressed into the object store and referenced via ``content_ref``.""" + art_id = trace_mod.next_artifact_id(self.trace) + art = { + "artifact_id": art_id, + "artifact_type": artifact_type, + "name": name or art_id, + "derived_from": _as_list(derived_from), + } + if role: + art["artifact_role"] = role + if format: + art["format"] = format + if producer_action_id is not None: + art["producer_action_id"] = producer_action_id + for a in self.trace["actions"]: + if a["id"] == producer_action_id and art_id not in a["outputs"]: + a["outputs"].append(art_id) + if payload is not None: + art["payload"] = payload + if content is not None: + art["content_ref"] = objects_mod.put_text(content) + self.trace["artifacts"].append(art) + return art_id + + def goal(self, intent, scope=None, acceptance=None): + """Declare a goal (intent + optional scope/acceptance). Returns its id.""" + gid = f"g{len(self.trace.get('goals', [])) + 1}" + self.trace.setdefault("goals", []).append({ + "id": gid, + "intent": intent, + "scope": list(scope or []), + "status": "in_progress", + "acceptance": list(acceptance or []), + }) + return gid + + def residual(self, kind, statement, severity="medium", status="open", + suggested_check=None, derived_from=None): + """Declare negative space (an assumption, gap, limitation, ...) as a Residual artifact.""" + payload = {"kind": kind, "severity": severity, "status": status, "statement": statement} + if suggested_check: + payload["suggested_check"] = suggested_check + return self.artifact("Residual", name=f"residual:{kind}", payload=payload, + derived_from=derived_from, role="ResidualRole") + + def verify(self, target, oracle, derived_from=None, label=None, rationale=None): + """Invoke an oracle for evidence and record it. + + ``oracle`` is an oracle id (resolved from the registry) or an ``Oracle`` instance. + Records a ``Verify`` action and appends the oracle's evidence artifact(s), wiring lineage + from ``derived_from``. Returns the list of new artifact ids. + """ + oc = oracle if isinstance(oracle, oracles_mod.Oracle) else oracles_mod.get_oracle(oracle) + if oc is None: + raise ValueError(f"unknown oracle: {oracle!r} (see `ponens oracle list`)") + aid = self.action( + "Verify", category="reasoning", + label=label or f"verify with {oc.name}", + rationale=rationale or f"produce {oc.evidence_strength}-strength evidence via {oc.name}", + inputs=_as_list(derived_from), + ) + new_ids = [] + for art in oc.invoke(target): + art = dict(art) + art.setdefault("derived_from", _as_list(derived_from)) + aid_art = self.artifact( + art.pop("artifact_type"), + name=art.pop("name", None), + payload=art.pop("payload", None), + derived_from=art.pop("derived_from", None), + producer_action_id=aid, + format=art.pop("format", None), + role=art.pop("artifact_role", None), + ) + new_ids.append(aid_art) + return new_ids + + def outcome(self, type="ProcessCompleted", summary=None): + self.trace["outcome"] = {"type": type} + if summary: + self.trace["outcome"]["summary"] = summary + + # --- lifecycle ----------------------------------------------------------- + + def validate(self): + """Return (errors, warnings) from the structural validator.""" + return trace_mod.validate_trace(self.trace) + + def save(self, path=None, strict=True): + """Externalize blobs, validate, and write the trace. + + With ``strict`` (the default) structural errors raise. On an aborted run the SDK saves + with ``strict=False`` so a partial trace is never lost and the original exception is never + masked.""" + target = path or self.path + if not target: + raise ValueError("no path given to save()") + objects_mod.externalize(self.trace) + if strict: + errors, _ = self.validate() + if errors: + raise ValueError("trace has structural errors: " + "; ".join(errors)) + trace_mod.save_trace(target, self.trace) + return target + + def __enter__(self): + return self + + def __exit__(self, exc_type, exc, tb): + if exc_type is not None: + # Record how the run ended and persist the partial trace, but never mask the + # original exception (best-effort, non-strict save) and never swallow it. + if not self.trace.get("outcome", {}).get("type"): + self.outcome("ProcessAborted", summary=str(exc)) + if self.path: + try: + self.save(strict=False) + except Exception: + pass + return False + if not self.trace.get("outcome", {}).get("type"): + self.outcome("ProcessCompleted") + if self.path: + self.save() + return False + + +def _as_list(x): + if x is None: + return [] + return list(x) if isinstance(x, (list, tuple, set)) else [x] diff --git a/cli/ponens/trace.py b/cli/ponens/trace.py index df06f06..4d87e55 100644 --- a/cli/ponens/trace.py +++ b/cli/ponens/trace.py @@ -26,6 +26,7 @@ ) from . import goals as goalops from . import lineage +from . import merge as mergeops # ================================================================ @@ -418,7 +419,14 @@ def evaluate_formula(node, trace, ctx=None): a = ctx['action'] name = node.name if name in ACTION_TYPES: - return _canon_type(a.get('type')) == _canon_type(name) + if _canon_type(a.get('type')) == _canon_type(name): + return True + # A dual-purpose name (also an artifact type, e.g. `SourceCode` / `Test`) that did NOT match + # the action's type falls through to artifact-output matching below — otherwise the artifact + # sense is permanently shadowed and an atom like `SourceCode` can never match a produced + # SourceCode artifact (only an action literally typed "SourceCode", which does not occur). + if name not in ARTIFACT_TYPES: + return False if name in ARTIFACT_TYPES: if _canon_type(a.get('type')) == _canon_type(name): return True @@ -909,7 +917,11 @@ def cmd_complete(args): return 0 -RESIDUAL_KINDS = {'assumption', 'unverified', 'out_of_scope', 'limitation', 'open_question', 'defeater'} +RESIDUAL_KINDS = {'assumption', 'unverified', 'out_of_scope', 'limitation', 'open_question', 'defeater', + # Merge-derived open obligations (materialized by `ponens trace merge --combine`): + # a standing result whose closure the merge touched, and a goal whose covered surface + # the merge changed. Genuine open-obligation kinds, hence first-class residual kinds. + 'needs_rereasoning', 'coverage_regression'} DEFEATER_KINDS = {'rebuts', 'undermines', 'undercuts'} # what a Defeater attacks (§13.1) RESIDUAL_SEVERITIES = {'info', 'low', 'medium', 'high', 'critical'} RESIDUAL_STATUSES = {'open', 'acknowledged', 'addressed', 'waived'} @@ -2104,7 +2116,7 @@ def cmd_resolve(args): for g in trace.get('goals', []): items = [] for item in g.get('acceptance', []): - r = goalops.resolve_item(item, trace) + r = goalops.resolve_item(item, trace, goal=g) it = {**item, 'status': r['status'], 'from_trace': r['from_trace']} # Preserve a typed criterion's {artifact} spec; put the resolved id in evidence_ref. if isinstance(item.get('evidence'), dict): @@ -2148,6 +2160,31 @@ def cmd_enrich(args): return 0 +def cmd_merge(args): + """Merge two traces: carry forward the standing results OURS proved whose dependency closure the + incoming change never touches (SkipDisjoint), and flag the rest for re-reasoning (ReReason). Emits a + report projection; neither input trace is modified. Sound-but-conservative: the SkipContract branch + is deferred, so every touched result re-reasons.""" + ours = load_trace(args.ours) + theirs = load_trace(args.theirs) + base = load_trace(args.base) if getattr(args, 'base', None) else None + if getattr(args, 'combine', False): + result = mergeops.combine(ours, theirs, base=base) + label = "merged trace" + else: + result = mergeops.merge(ours, theirs, base=base) + label = "merge report" + text = json.dumps(result, indent=2, ensure_ascii=False) + out_path = getattr(args, 'output', None) + if out_path: + with open(out_path, 'w') as f: + f.write(text + '\n') + print(f"Wrote {label} -> {out_path}", file=sys.stderr) + else: + print(text) + return 0 + + def _find_visualizer(): here = os.path.dirname(__file__) candidates = [ @@ -2589,6 +2626,16 @@ def register(subparsers): p.add_argument("-o", "--output", help="Write the enriched trace here (default: stdout)") p.set_defaults(func=cmd_enrich) + # merge (carry forward the provably-unaffected standing results, flag the rest) + p = trace_sub.add_parser("merge", help="Combine two traces: carry forward the provably-unaffected, flag the rest for re-reasoning") + p.add_argument("ours", help="Our trace (the standing results to carry or re-reason)") + p.add_argument("theirs", help="Their trace (the incoming changes)") + p.add_argument("--base", default=None, help="Common ancestor trace for 3-way delta attribution") + p.add_argument("--combine", "--emit-trace", dest="combine", action="store_true", + help="Emit a materialized MERGED TRACE (validate/enrich/check-able) instead of the report") + p.add_argument("-o", "--output", help="Write the merge report (or merged trace) here (default: stdout)") + p.set_defaults(func=cmd_merge) + # residual (declare) rp = trace_sub.add_parser("residual", help="Declare a residual (a gap the trace does not establish)") rp_sub = rp.add_subparsers(dest="residual_command", required=True) diff --git a/cli/pyproject.toml b/cli/pyproject.toml index b248ef9..f496c66 100644 --- a/cli/pyproject.toml +++ b/cli/pyproject.toml @@ -1,6 +1,6 @@ [project] name = "ponens" -version = "1.9.1" +version = "1.11.0" description ="Author, govern, and validate reasoning traces — the open CLI for the reasoning-policies ecosystem" readme = "README.md" requires-python = ">=3.11" diff --git a/cli/tests/unit/test_component.py b/cli/tests/unit/test_component.py new file mode 100644 index 0000000..7696b2b --- /dev/null +++ b/cli/tests/unit/test_component.py @@ -0,0 +1,162 @@ +"""Unit tests for the component-identity resolver (ponens.component). + +Ports the PROVED example battery of `formal/component/identity.iml` as direct `resolve_component_id` +cases (each theorem `exN_*` becomes one assertion), plus a few `_line_similarity` and `match_descriptor` +cases exercising the convenience wrapper. `("reuse", id)` mirrors `Reuse id`; `("mint", None)` mirrors +`Mint`. +""" + +from ponens.component import ( + _line_similarity, + resolve_component_id, + match_descriptor, + SIM_MIN, + SIM_MARGIN, +) + + +# ---- resolver battery (ports of identity.iml example theorems) ------------ + +def test_ex1_lineage_beats_weak(): + # resolve (Some 7) 0 0 70 10 99 = Reuse 7 + assert resolve_component_id(7, 0, 0, 70, 10, 99) == ("reuse", 7) + + +def test_ex2_unique_exact(): + # resolve None 1 42 0 0 99 = Reuse 42 + assert resolve_component_id(None, 1, 42, 0, 0, 99) == ("reuse", 42) + + +def test_ex3_two_exact_mints(): + # resolve None 2 42 0 0 99 = Mint (ambiguous exact -> never conflate) + assert resolve_component_id(None, 2, 42, 0, 0, 99) == ("mint", None) + + +def test_ex4_confident_rename(): + # resolve None 0 0 90 40 55 = Reuse 55 + assert resolve_component_id(None, 0, 0, 90, 40, 55) == ("reuse", 55) + + +def test_ex5_weak_sim_mints(): + # resolve None 0 0 70 10 55 = Mint (best 70 < floor) + assert resolve_component_id(None, 0, 0, 70, 10, 55) == ("mint", None) + + +def test_ex6_close_runnerup_mints(): + # resolve None 0 0 85 75 55 = Mint (margin 10 < 15, ambiguous) + assert resolve_component_id(None, 0, 0, 85, 75, 55) == ("mint", None) + + +def test_ex7_nothing_mints(): + # resolve None 0 0 0 0 0 = Mint + assert resolve_component_id(None, 0, 0, 0, 0, 0) == ("mint", None) + + +def test_ex_edge_exactly_at_floor(): + # resolve None 0 0 80 65 55 = Reuse 55 (best at floor, margin exactly met) + assert resolve_component_id(None, 0, 0, 80, 65, 55) == ("reuse", 55) + + +def test_ex_edge_margin_one_short(): + # resolve None 0 0 80 66 55 = Mint (margin one short: 14 < 15) + assert resolve_component_id(None, 0, 0, 80, 66, 55) == ("mint", None) + + +def test_ex_edge_zero_exact_confident_sim(): + # resolve None 0 0 95 20 33 = Reuse 33 + assert resolve_component_id(None, 0, 0, 95, 20, 33) == ("reuse", 33) + + +def test_ex_edge_many_exact_confident_sim(): + # resolve None 3 0 95 20 33 = Reuse 33 (exact_count <> 1, confident sim still fires) + assert resolve_component_id(None, 3, 0, 95, 20, 33) == ("reuse", 33) + + +def test_thresholds(): + assert SIM_MIN == 80 + assert SIM_MARGIN == 15 + + +# ---- _line_similarity ----------------------------------------------------- + +def test_similarity_identical_is_100(): + src = "let g x = x + 1\nlet f x = g x + 2\n" + assert _line_similarity(src, src) == 100 + + +def test_similarity_empty_is_zero(): + assert _line_similarity("", "") == 0 + assert _line_similarity("", "let f x = x\n") == 0 + + +def test_similarity_disjoint_is_zero(): + assert _line_similarity("let a x = x\n", "let b y = y\n") == 0 + + +def test_similarity_partial(): + # A = {p, q}, B = {p, r}: 2*1 / (2+2) = 50%. + a = "p\nq\n" + b = "p\nr\n" + assert _line_similarity(a, b) == 50 + + +def test_similarity_ignores_blank_and_whitespace(): + a = " let f x = x \n\n\n" + b = "let f x = x\n" + assert _line_similarity(a, b) == 100 + + +# ---- match_descriptor ----------------------------------------------------- + +def test_match_identical_text_via_similarity(): + # A confident rename: same body text (100% similar), different fingerprint -> reuse the candidate. + body = "let f x = x + 1\nlet helper y = y * 2\n" + desc = {"fingerprint": "fp-new", "text": body} + cands = [{"id": "c1", "fingerprint": "fp-old", "text": body}] + assert match_descriptor(desc, cands) == ("reuse", "c1") + + +def test_match_unique_exact_fingerprint(): + desc = {"fingerprint": "fp-x", "text": "totally different"} + cands = [{"id": "c1", "fingerprint": "fp-x", "text": "unrelated body"}] + assert match_descriptor(desc, cands) == ("reuse", "c1") + + +def test_match_two_identical_fingerprints_mints(): + # Two candidates share the descriptor's fingerprint -> ambiguous exact, AND no confident-unique + # similarity winner (both bodies unrelated to the descriptor) -> mint, never conflate. + desc = {"fingerprint": "fp-x", "text": "let target q = q + 1\n"} + cands = [ + {"id": "c1", "fingerprint": "fp-x", "text": "let a b = b - 9\n"}, + {"id": "c2", "fingerprint": "fp-x", "text": "let c d = d * 3\n"}, + ] + assert match_descriptor(desc, cands) == ("mint", None) + + +def test_match_weak_similarity_mints(): + desc = {"fingerprint": "fp-new", "text": "let f x = x + 1\n"} + cands = [{"id": "c1", "fingerprint": "fp-old", "text": "let z q = q - 99\n"}] + assert match_descriptor(desc, cands) == ("mint", None) + + +def test_match_lineage_wins(): + # An explicit lineage link short-circuits even weak candidates. + desc = {"fingerprint": "fp-new", "text": "let f x = x + 1\n"} + cands = [{"id": "c1", "fingerprint": "fp-old", "text": "unrelated"}] + assert match_descriptor(desc, cands, lineage_id="line-7") == ("reuse", "line-7") + + +def test_match_ambiguous_similarity_mints(): + # Two candidates equally similar to the descriptor -> no confident-unique winner -> mint. + body = "let f x = x + 1\nlet helper y = y * 2\n" + desc = {"fingerprint": "fp-new", "text": body} + cands = [ + {"id": "c1", "fingerprint": "fp-a", "text": body}, + {"id": "c2", "fingerprint": "fp-b", "text": body}, + ] + assert match_descriptor(desc, cands) == ("mint", None) + + +def test_match_no_candidates_mints(): + desc = {"fingerprint": "fp", "text": "let f x = x\n"} + assert match_descriptor(desc, []) == ("mint", None) diff --git a/cli/tests/unit/test_component_identity.py b/cli/tests/unit/test_component_identity.py new file mode 100644 index 0000000..a78e22c --- /dev/null +++ b/cli/tests/unit/test_component_identity.py @@ -0,0 +1,261 @@ +"""Unit tests for component-identity STAMPING + CONSUMPTION (2c / 2d). + +`assign_component_ids` (component.py) groups a trace's model symbols into stable components and stamps +`payload.component_ids` (models) + `payload.target_component_id` (VerificationGoals). The consumers — +`lineage.roots_in_component` (goal rooting) and `goals.stale_evidence` (freshness) — then FOLLOW A +RENAME by component instead of by name. Everything is additive: a trace with no stamped ids resolves +exactly as before. + +Each trace is a tiny in-memory dict (same shape as test_merge.py): a model artifact carries +`payload.iml_code`; a proof is a VerificationGoal{target_symbol} + a proved VerificationResult. +""" + +import copy + +from ponens.component import assign_component_ids, match_descriptor +from ponens import lineage +from ponens.goals import enrich, stale_evidence, _resolve_typed + + +# ---- trace builders ------------------------------------------------------- + +def _model(src, aid="m1", step=1, derived_from=None): + a = {"artifact_id": aid, "artifact_type": "IMLModel", "producer_action_id": step, + "payload": {"iml_code": src}} + if derived_from is not None: + a["derived_from"] = derived_from + return a + + +def _proof(sym, vg="vg1", vr="vr1", step=2, desc=None): + return [ + {"artifact_id": vg, "artifact_type": "VerificationGoal", "producer_action_id": step, + "payload": {"goal_id": vg + "-G", "target_symbol": sym, + "description": desc or f"property of {sym}"}}, + {"artifact_id": vr, "artifact_type": "VerificationResult", "producer_action_id": step + 1, + "derived_from": [vg], "payload": {"goal_id": vg + "-G", "goal_artifact_id": vg, + "status": "proved"}}, + ] + + +# A distinctive multi-line body: a rename touches only the signature line, so similarity stays +# confidently above the 80% floor (identity.iml SIM_MIN) while an unrelated symbol is far below it. The +# body is long enough that a rename PLUS a single-line body edit still clears the floor by a margin (so +# a renamed+changed component is recognized as the SAME component, and its proof correctly goes stale). +_CLAMP = ("let clamp x =\n" + " let lo = 0 in\n" + " let hi = 100 in\n" + " let a = x + 1 in\n" + " let b = a * 2 in\n" + " let c = b - 3 in\n" + " let d = c + 4 in\n" + " let e = d * 5 in\n" + " let f0 = e - 6 in\n" + " if x < lo then lo\n" + " else if x > hi then hi\n" + " else x\n") +_CLAMP_INT_SAME = _CLAMP.replace("let clamp x =", "let clamp_int x =") # rename, identical body +_CLAMP_INT_CHANGED = _CLAMP_INT_SAME.replace("let d = c + 4 in", "let d = c + 99 in") # rename + 1-line change + + +# ================================================================ +# 1. rename ROOTS the goal (roots_in_component follows the rename) +# ================================================================ + +def test_rename_roots_the_goal(): + # ours proves clamp (m1); a later model (m2, same model line) renames clamp -> clamp_int, identical + # body. A typed goal criterion `component: clamp, evidence: VerificationResult` should STILL resolve. + trace = {"trace_id": "t", "artifacts": [ + _model(_CLAMP, aid="m1", step=1, derived_from=["src"]), + *_proof("clamp", vg="vg1", vr="vr1", step=2), + _model(_CLAMP_INT_SAME, aid="m2", step=5, derived_from=["src"]), + ]} + stamped = copy.deepcopy(trace) + info = assign_component_ids(stamped) + # clamp and clamp_int chain to the SAME component (rename, identical body). + assert info["by_name"]["clamp"] == info["by_name"]["clamp_int"] + + item = {"component": {"function": "clamp"}, "evidence": {"artifact": "VerificationResult"}} + res = _resolve_typed(item, stamped) + assert res["status"] == "done" # roots via component_id across the rename + assert res["evidence"] == "vr1" + + # CONTRAST: strip the component_ids -> name mismatch -> does NOT root (the goal names `clamp`, but the + # VR's lineage now would only be reachable by the component-identity path, which is gone). + stripped = copy.deepcopy(stamped) + for a in stripped["artifacts"]: + a.get("payload", {}).pop("component_ids", None) + a.get("payload", {}).pop("target_component_id", None) + # roots_in_component still matches by NAME here (the VG's target_symbol IS clamp), so isolate the pure + # component-identity contribution: a goal naming the NEW name `clamp_int` roots ONLY via component id. + item_new = {"component": {"function": "clamp_int"}, "evidence": {"artifact": "VerificationResult"}} + assert _resolve_typed(item_new, stamped)["status"] == "done" # follows rename via component id + assert _resolve_typed(item_new, stripped)["status"] == "todo" # no component id -> name mismatch + + +# ================================================================ +# 2. stale FOLLOWS the rename (stale_evidence chains by component) +# ================================================================ + +def test_stale_follows_rename(): + # prove clamp (m1); later model renames clamp -> clamp_int AND changes the body (hi 100 -> 255). + trace = {"trace_id": "t", "artifacts": [ + _model(_CLAMP, aid="m1", step=1, derived_from=["src"]), + *_proof("clamp", vg="vg1", vr="vr1", step=2), + _model(_CLAMP_INT_CHANGED, aid="m2", step=5, derived_from=["src"]), + ]} + stamped = copy.deepcopy(trace) + assign_component_ids(stamped) + res = stale_evidence(stamped) + stale = [r for r in res if r.get("kind") == "stale_evidence" and r.get("target", {}).get("target_id") == "vr1"] + assert stale, "the proof of clamp should go stale under the renamed+changed component" + + +# ================================================================ +# 3. name FALLBACK — a trace with NO component_ids resolves as before +# ================================================================ + +def test_name_fallback_no_component_ids(): + # No renames, no stamping: an existing NAME-based rooting must still resolve identically. + trace = {"trace_id": "t", "artifacts": [ + _model(_CLAMP, aid="m1", step=1), + *_proof("clamp", vg="vg1", vr="vr1", step=2), + ]} + # roots_in_component with NO component_ids in the trace -> pure name path. + assert lineage._component_by_name(trace) == {} + assert lineage.roots_in_component("vr1", "clamp", trace) is True + item = {"component": {"function": "clamp"}, "evidence": {"artifact": "VerificationResult"}} + assert _resolve_typed(item, trace)["status"] == "done" + # A goal about a genuinely-different symbol does not root. + assert lineage.roots_in_component("vr1", "other", trace) is False + + +# ================================================================ +# 4. never-conflate — two different symbols get DIFFERENT ids +# ================================================================ + +_OTHER = ("let scale y =\n" + " let k = 3 in\n" + " let base = 7 in\n" + " y * k + base\n") + + +def test_never_conflate_distinct_symbols(): + trace = {"trace_id": "t", "artifacts": [ + _model(_CLAMP + _OTHER, aid="m1", step=1, derived_from=["src"]), + *_proof("clamp", vg="vg1", vr="vr1", step=2), + *_proof("scale", vg="vg2", vr="vr2", step=4), + ]} + stamped = copy.deepcopy(trace) + info = assign_component_ids(stamped) + assert info["by_name"]["clamp"] != info["by_name"]["scale"] # distinct components + # A goal about clamp roots in clamp's proof, NOT scale's. + item_clamp = {"component": {"function": "clamp"}, "evidence": {"artifact": "VerificationResult"}} + assert _resolve_typed(item_clamp, stamped)["evidence"] == "vr1" + # roots_in_component never conflates across the two components. + assert lineage.roots_in_component("vr2", "clamp", stamped) is False + assert lineage.roots_in_component("vr1", "scale", stamped) is False + + +# ================================================================ +# 5. assign_component_ids resolution unit — lineage / exact / similar / distinct / ambiguous +# ================================================================ + +def test_assign_exact_same_id(): + # Same body, same model line, same name across two revisions -> SAME component id (lineage/exact). + trace = {"trace_id": "t", "artifacts": [ + _model(_CLAMP, aid="m1", step=1, derived_from=["src"]), + _model(_CLAMP, aid="m2", step=5, derived_from=["src"]), # identical re-model + ]} + info = assign_component_ids(trace) + ids = [m["payload"]["component_ids"]["clamp"] for m in trace["artifacts"]] + assert ids[0] == ids[1] + assert info["by_name"]["clamp"] == ids[0] + + +def test_assign_similar_rename_same_id(): + # Rename with identical body (similarity/exact-fingerprint) -> SAME component id. + trace = {"trace_id": "t", "artifacts": [ + _model(_CLAMP, aid="m1", step=1, derived_from=["src"]), + _model(_CLAMP_INT_SAME, aid="m2", step=5, derived_from=["src"]), + ]} + info = assign_component_ids(trace) + assert info["by_name"]["clamp"] == info["by_name"]["clamp_int"] + + +def test_assign_distinct_new_id(): + # Two genuinely-different symbols in one model -> two DIFFERENT ids. + trace = {"trace_id": "t", "artifacts": [_model(_CLAMP + _OTHER, aid="m1", step=1)]} + info = assign_component_ids(trace) + assert info["by_name"]["clamp"] != info["by_name"]["scale"] + assert {info["by_name"]["clamp"], info["by_name"]["scale"]} == {"cmp0", "cmp1"} + + +def test_assign_ambiguous_mints_new(): + # ONE renamed symbol facing TWO equally-similar prior candidates -> never guess WHICH -> mint fresh + # (never conflate). m1 defines two identical-body siblings (distinct components); m2 (a DIFFERENT + # model line, so no lineage-by-name) has a single `clamp_new` with that same body -> two exact- + # fingerprint candidates -> ambiguous -> mint. + c1a = _CLAMP.replace("let clamp x =", "let clamp_a x =") + c1b = _CLAMP.replace("let clamp x =", "let clamp_b x =") + c_new = _CLAMP.replace("let clamp x =", "let clamp_new x =") + trace = {"trace_id": "t", "artifacts": [ + _model(c1a + c1b, aid="m1", step=1, derived_from=["srcA"]), # two distinct identical-body sibs + _model(c_new, aid="m2", step=5, derived_from=["srcB"]), # different model line -> no lineage + ]} + info = assign_component_ids(trace) + a_id = trace["artifacts"][0]["payload"]["component_ids"]["clamp_a"] + b_id = trace["artifacts"][0]["payload"]["component_ids"]["clamp_b"] + new_id = info["by_name"]["clamp_new"] + assert a_id != b_id # the two siblings are distinct components + assert new_id != a_id and new_id != b_id # ambiguous match -> minted fresh, never conflated + + +def test_assign_lineage_carries_across_body_change(): + # Same model line + same name but a CHANGED body: the lineage tier (producer-declared same-model-line + # link) still reuses the id — identity follows the model line even when the fingerprint diverges. + trace = {"trace_id": "t", "artifacts": [ + _model(_CLAMP, aid="m1", step=1, derived_from=["src"]), + _model(_CLAMP.replace("let hi = 100 in", "let hi = 42 in"), aid="m2", step=5, derived_from=["src"]), + ]} + info = assign_component_ids(trace) + ids = [m["payload"]["component_ids"]["clamp"] for m in trace["artifacts"]] + assert ids[0] == ids[1] # lineage keeps them one component across the edit + + +# ================================================================ +# enrich wiring: the source trace is NOT mutated; the projection carries ids +# ================================================================ + +def test_enrich_does_not_mutate_source(): + trace = {"trace_id": "t", "goals": [], "artifacts": [ + _model(_CLAMP, aid="m1", step=1, derived_from=["src"]), + *_proof("clamp", vg="vg1", vr="vr1", step=2), + _model(_CLAMP_INT_SAME, aid="m2", step=5, derived_from=["src"]), + ]} + before = copy.deepcopy(trace) + out = enrich(trace) + # source untouched (no component_ids leaked back onto the on-disk trace) + assert trace == before + for a in trace["artifacts"]: + assert "component_ids" not in a.get("payload", {}) + # the projection carries the stamped ids + m2 = next(a for a in out["artifacts"] if a.get("artifact_id") == "m2") + assert "component_ids" in m2["payload"] + + +def test_enrich_goal_roots_across_rename(): + # End-to-end through enrich: a typed goal named `clamp_int` (the new name) resolves `done` because the + # enrich projection stamps component_ids and rooting follows the rename. + trace = {"trace_id": "t", "artifacts": [ + _model(_CLAMP, aid="m1", step=1, derived_from=["src"]), + *_proof("clamp", vg="vg1", vr="vr1", step=2), + _model(_CLAMP_INT_SAME, aid="m2", step=5, derived_from=["src"]), + ], "goals": [{ + "id": "g1", "intent": "clamp is verified", + "acceptance": [{"id": "a1", "component": {"function": "clamp_int"}, + "evidence": {"artifact": "VerificationResult"}}], + }]} + out = enrich(trace) + item = out["goals"][0]["acceptance"][0] + assert item["status"] == "done" diff --git a/cli/tests/unit/test_goal_formula.py b/cli/tests/unit/test_goal_formula.py new file mode 100644 index 0000000..584bc70 --- /dev/null +++ b/cli/tests/unit/test_goal_formula.py @@ -0,0 +1,205 @@ +"""§8.8 property-language front-end, Phase 1: the formula AST + recursive evaluator (ponens.goals). + +Covers three things: + 1. Regression — a legacy acceptance item (each kind) desugars to a single atom and resolves + IDENTICALLY to a bare item (byte-for-byte), so the formula layer is non-breaking. + 2. Combinators — and/or/not/implies lift over the 4-valued status lattice {done,doing,todo,blocked}. + 3. Roles — [met] vs [governed] gate defeater/freshness; the default (no role) reproduces today. +""" + +from ponens import lineage +from ponens.goals import ( + resolve_item, eval_formula, eval_atom, + _combine_and, _combine_or, _combine_not, +) + + +# --------------------------------------------------------------------------- +# Fixtures +# --------------------------------------------------------------------------- + +def _open_defeater(target_id): + return lineage.residual_to_artifact({ + "residual_id": "d-" + target_id, "kind": "defeater", "defeater_kind": "undermines", + "statement": "model diverges from code", "status": "open", + "target": {"target_type": "artifact", "target_id": target_id}}) + + +def _trace(): + """src → model(settle, refund, hold, aged) → VGs/VRs, plus a policy eval, a residual, a diff.""" + return { + "actions": [{"id": i} for i in range(1, 30)], + "artifacts": [ + {"artifact_id": "src", "artifact_type": "SourceCode", "derived_from": None, "producer_action_id": 1}, + {"artifact_id": "model", "artifact_type": "IMLModel", "derived_from": ["src"], "producer_action_id": 2, + "payload": {"symbols": ["settle", "refund", "hold", "aged"]}}, + # settle: PROVED + {"artifact_id": "vg_s", "artifact_type": "VerificationGoal", "derived_from": ["model"], "producer_action_id": 3, + "payload": {"goal_id": "g_s", "target_symbol": "settle"}}, + {"artifact_id": "vr_s", "artifact_type": "VerificationResult", "derived_from": ["vg_s"], "producer_action_id": 4, + "payload": {"goal_id": "g_s", "goal_artifact_id": "vg_s", "status": "proved"}}, + # refund: REFUTED → property kind resolves `blocked` + {"artifact_id": "vg_r", "artifact_type": "VerificationGoal", "derived_from": ["model"], "producer_action_id": 5, + "payload": {"goal_id": "g_r", "target_symbol": "refund"}}, + {"artifact_id": "vr_r", "artifact_type": "VerificationResult", "derived_from": ["vg_r"], "producer_action_id": 6, + "payload": {"goal_id": "g_r", "goal_artifact_id": "vg_r", "status": "refuted"}}, + # hold: VG but NO result → property kind resolves `doing` + {"artifact_id": "vg_h", "artifact_type": "VerificationGoal", "derived_from": ["model"], "producer_action_id": 7, + "payload": {"goal_id": "g_h", "target_symbol": "hold"}}, + # aged: PROVED at step 8, then the symbol changes at step 25 → the proof goes STALE + {"artifact_id": "vg_a", "artifact_type": "VerificationGoal", "derived_from": ["model"], "producer_action_id": 8, + "payload": {"goal_id": "g_a", "target_symbol": "aged"}}, + {"artifact_id": "vr_a", "artifact_type": "VerificationResult", "derived_from": ["vg_a"], "producer_action_id": 9, + "payload": {"goal_id": "g_a", "goal_artifact_id": "vg_a", "status": "proved"}}, + # obligation / gap fixtures + {"artifact_id": "diff_settle", "artifact_type": "Diff", "derived_from": ["src"], "producer_action_id": 10, + "payload": {"target_symbol": "settle"}, "summary": "edit settle"}, + ], + "policy_evaluations": [{"policy_id": "p_ok", "status": "passed"}, + {"policy_id": "p_bad", "status": "failed"}], + "residuals": [{"residual_id": "res_open", "kind": "limitation", "status": "open"}, + {"residual_id": "res_done", "kind": "limitation", "status": "addressed"}], + } + + +# Leaf items (bare = legacy; each resolves to a known status against _trace()). +PROVED = {"id": "a", "kind": "property", "binding": {"symbol": "settle"}} # done +REFUTED = {"id": "b", "kind": "property", "binding": {"symbol": "refund"}} # blocked +DOING = {"id": "c", "kind": "property", "binding": {"symbol": "hold"}} # doing +TODO = {"id": "d", "kind": "property", "binding": {"symbol": "ghost"}} # todo (no VG) +OBL_OK = {"id": "e", "kind": "obligation", "binding": {"policy_id": "p_ok"}} # done +OBL_BAD = {"id": "f", "kind": "obligation", "binding": {"policy_id": "p_bad"}} # blocked +GAP_OPEN = {"id": "g", "kind": "gap", "binding": {"residual_id": "res_open"}} # todo +GAP_DONE = {"id": "h", "kind": "gap", "binding": {"residual_id": "res_done"}} # done +TYPED = {"id": "i", "component": {"function": "settle"}, "evidence": {"artifact": "VerificationResult"}} # done + + +# --------------------------------------------------------------------------- +# 1. Regression: legacy item == {"formula": {"atom": item}} (desugar is identical) +# --------------------------------------------------------------------------- + +def test_legacy_desugar_is_identical_across_kinds(): + t = _trace() + for item, expect in [(PROVED, "done"), (REFUTED, "blocked"), (DOING, "doing"), (TODO, "todo"), + (OBL_OK, "done"), (OBL_BAD, "blocked"), (GAP_OPEN, "todo"), (GAP_DONE, "done"), + (TYPED, "done")]: + bare = resolve_item(item, t) + wrapped = resolve_item({"id": item["id"], "formula": {"atom": item}}, t) + assert bare["status"] == expect, (item["id"], bare) + assert bare == wrapped, (item["id"], bare, wrapped) # byte-for-byte + + +# --------------------------------------------------------------------------- +# 2a. Status lattice (pure combinators) +# --------------------------------------------------------------------------- + +def _r(s): + return {"status": s, "from_trace": True, "evidence": None} + + +def test_and_lattice(): + st = lambda xs: _combine_and([_r(s) for s in xs])["status"] + assert st(["done", "done"]) == "done" + assert st(["done", "doing"]) == "doing" + assert st(["done", "todo"]) == "doing" # any done|doing → doing + assert st(["todo", "todo"]) == "todo" + assert st(["done", "blocked"]) == "blocked" # any blocked dominates + assert st(["doing", "blocked"]) == "blocked" + assert _combine_and([])["status"] == "todo" # empty → todo (no vacuous done) + + +def test_or_lattice(): + st = lambda xs: _combine_or([_r(s) for s in xs])["status"] + assert st(["todo", "done"]) == "done" + assert st(["blocked", "done"]) == "done" # any done wins + assert st(["todo", "doing"]) == "doing" + assert st(["blocked", "blocked"]) == "blocked" + assert st(["blocked", "todo"]) == "todo" # not all blocked, no done/doing + assert _combine_or([])["status"] == "todo" + + +def test_not_lattice(): + n = lambda s: _combine_not(_r(s))["status"] + assert n("done") == "todo" + assert n("todo") == "done" + assert n("doing") == "doing" + assert n("blocked") == "blocked" # contested stays contested + + +# --------------------------------------------------------------------------- +# 2b. Combinators over REAL atoms (through eval_formula) +# --------------------------------------------------------------------------- + +def _f(node): + return resolve_item({"id": "x", "formula": node}, _trace())["status"] + + +def test_and_of_atoms(): + assert _f({"and": [{"atom": PROVED}, {"atom": TYPED}]}) == "done" # both done + assert _f({"and": [{"atom": PROVED}, {"atom": REFUTED}]}) == "blocked" # refuted propagates + assert _f({"and": [{"atom": PROVED}, {"atom": DOING}]}) == "doing" + + +def test_or_of_atoms(): + assert _f({"or": [{"atom": TODO}, {"atom": PROVED}]}) == "done" + assert _f({"or": [{"atom": REFUTED}, {"atom": REFUTED}]}) == "blocked" + assert _f({"or": [{"atom": TODO}, {"atom": DOING}]}) == "doing" + + +def test_not_of_atom(): + assert _f({"not": {"atom": PROVED}}) == "todo" + assert _f({"not": {"atom": TODO}}) == "done" + + +def test_implies_of_atoms(): + # implies(a,b) = or(not a, b). Antecedent unmet (todo→not=done) ⇒ vacuously done. + assert _f({"implies": [{"atom": TODO}, {"atom": REFUTED}]}) == "done" + # Antecedent met (done→not=todo), consequent done ⇒ done. + assert _f({"implies": [{"atom": PROVED}, {"atom": TYPED}]}) == "done" + # Antecedent met, consequent todo ⇒ or(todo, todo) = todo. + assert _f({"implies": [{"atom": PROVED}, {"atom": TODO}]}) == "todo" + + +# --------------------------------------------------------------------------- +# 3. Roles: [met] vs [governed] vs default +# --------------------------------------------------------------------------- + +def test_role_defeater_met_vs_governed_vs_default(): + t = _trace() + t["artifacts"].append(_open_defeater("vr_s")) # contest the proof of `settle` + # default (legacy, no role): a contested proof is blocked — today's behavior. + assert resolve_item(PROVED, t)["status"] == "blocked" + # met: mere existence — the defeater is ignored. + assert eval_formula({"atom": PROVED, "role": "met"}, t)["status"] == "done" + # governed: contested ⇒ blocked. + assert eval_formula({"atom": PROVED, "role": "governed"}, t)["status"] == "blocked" + + +def test_role_freshness_governed_only(): + t = _trace() + # `aged` was proved at step 9, but a later Diff renames/changes it → the proof is stale (§18.3). + t["artifacts"].append({"artifact_id": "diff_aged", "artifact_type": "Diff", "derived_from": ["src"], + "producer_action_id": 25, "payload": {"target_symbol": "aged"}, "summary": "edit aged"}) + AGED = {"id": "z", "kind": "property", "binding": {"symbol": "aged"}} + # default & met do NOT freshness-gate → still done. + assert resolve_item(AGED, t)["status"] == "done" + assert eval_formula({"atom": AGED, "role": "met"}, t)["status"] == "done" + # governed requires fresh → stale ⇒ blocked. + assert eval_formula({"atom": AGED, "role": "governed"}, t)["status"] == "blocked" + + +def test_role_inherited_down_subtree(): + t = _trace() + t["artifacts"].append(_open_defeater("vr_s")) + # role on the combinator node is inherited by the child atom → met ignores the defeater. + assert resolve_item({"id": "x", "formula": {"and": [{"atom": PROVED}], "role": "met"}}, t)["status"] == "done" + # without the inherited role, the same shape blocks (default). + assert resolve_item({"id": "x", "formula": {"and": [{"atom": PROVED}]}}, t)["status"] == "blocked" + + +def test_eval_atom_helper_roles(): + t = _trace() + t["artifacts"].append(_open_defeater("vr_s")) + assert eval_atom(PROVED, t)["status"] == "blocked" # default + assert eval_atom(PROVED, t, role="met")["status"] == "done" + assert eval_atom(PROVED, t, role="governed")["status"] == "blocked" diff --git a/cli/tests/unit/test_goal_quantifiers.py b/cli/tests/unit/test_goal_quantifiers.py new file mode 100644 index 0000000..3795a9b --- /dev/null +++ b/cli/tests/unit/test_goal_quantifiers.py @@ -0,0 +1,168 @@ +"""§8.8 property-language front-end, Phase 2: selectors + quantifiers (ponens.goals + ponens.component). + +Covers: + - resolve_selector per kind: glob / module / scope / tag(best-effort over high_stakes_paths). + - forall / exists over a selector, combined with the Phase-1 status lattice. + - variable binding/substitution into inner atoms ({"var": "f"}). + - empty selector -> todo (no vacuous done) for both quantifiers. + - quantifiers nested under Phase-1 combinators. +""" + +from ponens.goals import resolve_item, eval_formula, _subst_atom +from ponens.component import resolve_selector, _dedup + + +def _trace(): + """Two files: payments/charge.py (charge PROVED, refund REFUTED) and pricing/tiers.py (fee_tier + PROVED). Component ids stamped as assign_component_ids would. high_stakes_paths = payments/.""" + return { + "actions": [{"id": i} for i in range(1, 20)], + "high_stakes_paths": ["payments/"], + "artifacts": [ + {"artifact_id": "src_pay", "artifact_type": "SourceCode", "derived_from": None, + "producer_action_id": 1, "name": "payments/charge.py"}, + {"artifact_id": "m_pay", "artifact_type": "IMLModel", "derived_from": ["src_pay"], + "producer_action_id": 2, + "payload": {"iml_code": "let charge x = x\nlet refund y = y", + "component_ids": {"charge": "cmp0", "refund": "cmp1"}}}, + {"artifact_id": "src_price", "artifact_type": "SourceCode", "derived_from": None, + "producer_action_id": 3, "name": "pricing/tiers.py"}, + {"artifact_id": "m_price", "artifact_type": "IMLModel", "derived_from": ["src_price"], + "producer_action_id": 4, + "payload": {"iml_code": "let fee_tier z = z", "component_ids": {"fee_tier": "cmp2"}}}, + # verdicts: charge proved, refund refuted, fee_tier proved + {"artifact_id": "vg_c", "artifact_type": "VerificationGoal", "derived_from": ["m_pay"], + "producer_action_id": 5, "payload": {"goal_id": "gc", "target_symbol": "charge"}}, + {"artifact_id": "vr_c", "artifact_type": "VerificationResult", "derived_from": ["vg_c"], + "producer_action_id": 6, "payload": {"goal_id": "gc", "goal_artifact_id": "vg_c", "status": "proved"}}, + {"artifact_id": "vg_r", "artifact_type": "VerificationGoal", "derived_from": ["m_pay"], + "producer_action_id": 7, "payload": {"goal_id": "gr", "target_symbol": "refund"}}, + {"artifact_id": "vr_r", "artifact_type": "VerificationResult", "derived_from": ["vg_r"], + "producer_action_id": 8, "payload": {"goal_id": "gr", "goal_artifact_id": "vg_r", "status": "refuted"}}, + {"artifact_id": "vg_f", "artifact_type": "VerificationGoal", "derived_from": ["m_price"], + "producer_action_id": 9, "payload": {"goal_id": "gf", "target_symbol": "fee_tier"}}, + {"artifact_id": "vr_f", "artifact_type": "VerificationResult", "derived_from": ["vg_f"], + "producer_action_id": 10, "payload": {"goal_id": "gf", "goal_artifact_id": "vg_f", "status": "proved"}}, + ], + } + + +GOAL = {"id": "g", "scope": ["charge", "fee_tier"]} +PROVED_VAR = {"atom": {"kind": "property", "binding": {"symbol": {"var": "f"}}}} # per-element property + + +def _syms(elements): + return sorted(e["symbol"] for e in elements) + + +# --------------------------------------------------------------------------- +# resolve_selector +# --------------------------------------------------------------------------- + +def test_selector_glob(): + assert _syms(resolve_selector({"glob": "payments/**"}, _trace())) == ["charge", "refund"] + + +def test_selector_module(): + assert _syms(resolve_selector({"module": "pricing"}, _trace())) == ["fee_tier"] + + +def test_selector_scope(): + assert _syms(resolve_selector({"scope": True}, _trace(), GOAL)) == ["charge", "fee_tier"] + + +def test_selector_tag_best_effort_over_high_stakes(): + # tag matches by high_stakes_paths substring regardless of tag name (documented gap). + assert _syms(resolve_selector({"tag": "money"}, _trace())) == ["charge", "refund"] + assert _syms(resolve_selector({"tag": "anything"}, _trace())) == ["charge", "refund"] + + +def test_selector_carries_component_id_and_file(): + el = next(e for e in resolve_selector({"glob": "payments/**"}, _trace()) if e["symbol"] == "charge") + assert el["component_id"] == "cmp0" + assert el["file"] == "payments/charge.py" + + +def test_selector_unknown_or_empty_is_empty_list(): + assert resolve_selector({"glob": "nope/**"}, _trace()) == [] + assert resolve_selector({"bogus": 1}, _trace()) == [] + assert resolve_selector("notadict", _trace()) == [] + + +def test_dedup_by_component_id(): + els = [{"symbol": "a", "component_id": "cmp0"}, {"symbol": "a2", "component_id": "cmp0"}, + {"symbol": "b", "component_id": None}, {"symbol": "b", "component_id": None}] + assert _dedup(els) == [{"symbol": "a", "component_id": "cmp0"}, {"symbol": "b", "component_id": None}] + + +# --------------------------------------------------------------------------- +# variable substitution +# --------------------------------------------------------------------------- + +def test_subst_binding_symbol(): + a = _subst_atom({"kind": "property", "binding": {"symbol": {"var": "f"}}}, {"f": {"symbol": "charge"}}) + assert a["binding"]["symbol"] == "charge" + + +def test_subst_component_var(): + a = _subst_atom({"component": {"var": "f"}, "evidence": {"artifact": "VerificationResult"}}, + {"f": {"symbol": "charge", "component_id": "cmp0"}}) + assert a["component"] == {"function": "charge", "symbol": "charge"} + + +def test_subst_noop_without_env(): + atom = {"kind": "property", "binding": {"symbol": {"var": "f"}}} + assert _subst_atom(atom, None) is atom + + +# --------------------------------------------------------------------------- +# quantifiers (through resolve_item, with the goal for scope) +# --------------------------------------------------------------------------- + +def _f(node): + return resolve_item({"id": "x", "formula": node}, _trace(), goal=GOAL)["status"] + + +def test_forall_over_glob_blocks_when_one_refuted(): + # payments/** = {charge PROVED, refund REFUTED}; forall(proved) → and → blocked. + assert _f({"forall": {"in": {"glob": "payments/**"}, "as": "f", "holds": PROVED_VAR}}) == "blocked" + + +def test_exists_over_glob_done_when_one_proved(): + # exists(proved) over payments/** → or(done, blocked) → done. + assert _f({"exists": {"in": {"glob": "payments/**"}, "as": "f", "holds": PROVED_VAR}}) == "done" + + +def test_forall_over_module_all_proved(): + assert _f({"forall": {"in": {"module": "pricing"}, "as": "f", "holds": PROVED_VAR}}) == "done" + + +def test_forall_over_scope_all_proved(): + # scope = {charge, fee_tier}, both proved → done. + assert _f({"forall": {"in": {"scope": True}, "as": "f", "holds": PROVED_VAR}}) == "done" + + +def test_empty_selector_is_todo_for_both_quantifiers(): + assert _f({"forall": {"in": {"glob": "nope/**"}, "as": "f", "holds": PROVED_VAR}}) == "todo" + assert _f({"exists": {"in": {"glob": "nope/**"}, "as": "f", "holds": PROVED_VAR}}) == "todo" + + +def test_quantifier_nested_under_combinator(): + # and[ forall(module pricing: proved)=done , exists(payments: proved)=done ] → done + node = {"and": [ + {"forall": {"in": {"module": "pricing"}, "as": "f", "holds": PROVED_VAR}}, + {"exists": {"in": {"glob": "payments/**"}, "as": "f", "holds": PROVED_VAR}}, + ]} + assert _f(node) == "done" + # and[ forall(payments: proved)=blocked , ... ] → blocked propagates + node2 = {"and": [ + {"forall": {"in": {"glob": "payments/**"}, "as": "f", "holds": PROVED_VAR}}, + {"forall": {"in": {"module": "pricing"}, "as": "f", "holds": PROVED_VAR}}, + ]} + assert _f(node2) == "blocked" + + +def test_role_inherited_into_quantifier_body(): + # governed role on the quantifier flows to the per-element atom (here no defeater/staleness, so done). + node = {"forall": {"in": {"module": "pricing"}, "as": "f", "holds": PROVED_VAR}, "role": "met"} + assert _f(node) == "done" diff --git a/cli/tests/unit/test_merge.py b/cli/tests/unit/test_merge.py new file mode 100644 index 0000000..bb3ee4b --- /dev/null +++ b/cli/tests/unit/test_merge.py @@ -0,0 +1,336 @@ +"""Unit tests for residual-aware trace MERGE (ponens.merge). + +Ports the IML example battery (formal/merge/{delta,classify}.iml) down to the trace level. Each trace +is a tiny in-memory dict: model artifacts carry `payload.iml_code`, and a standing result is an +IMLModel + VerificationGoal{target_symbol} + VerificationResult{status:proved}. Scope is the two live +branches: SkipDisjoint (carried_forward) and ReReason (needs_rereasoning). +""" + +from ponens.merge import merge, merge_delta, _standing_results, _symbols + + +# ---- trace builders ------------------------------------------------------- + +def _model(src, aid="m1", step=1, derived_from=None): + a = {"artifact_id": aid, "artifact_type": "IMLModel", "producer_action_id": step, + "payload": {"iml_code": src}} + if derived_from is not None: + a["derived_from"] = derived_from + return a + + +def _proved(sym, vg="vg1", vr="vr1", step=2, desc=None): + """A standing proof about `sym`: a VerificationGoal (target_symbol) + a proved VerificationResult.""" + return [ + {"artifact_id": vg, "artifact_type": "VerificationGoal", "producer_action_id": step, + "payload": {"goal_id": vg + "-G", "target_symbol": sym, + "description": desc or f"property of {sym}"}}, + {"artifact_id": vr, "artifact_type": "VerificationResult", "producer_action_id": step + 1, + "derived_from": [vg], "payload": {"goal_id": vg + "-G", "goal_artifact_id": vg, + "status": "proved"}}, + ] + + +def _trace(src, results=None, residuals=None, step=1): + t = {"trace_id": "t", "artifacts": [_model(src, step=step)]} + for r in results or []: + t["artifacts"].extend(r) + if residuals: + t["residuals"] = residuals + return t + + +# Common source fixtures: f depends on g (transitive), h is unrelated. +SRC = "let g x = x + 1\nlet f x = g x + 2\nlet h x = x * 10\n" + + +# ---- 1. disjoint: theirs changes an unrelated symbol -> CarriedForward ----- + +def test_disjoint_carried_forward(): + ours = _trace(SRC, results=[_proved("f")]) + theirs = _trace("let g x = x + 1\nlet f x = g x + 2\nlet h x = x * 999\n") # only h changed + rep = merge(ours, theirs) + assert rep["delta"]["changed"] == ["h"] + assert [c["result_id"] for c in rep["carried_forward"]] == ["vr1"] + assert rep["carried_forward"][0]["basis"] == "closure-disjoint" + assert rep["rereason"] == [] + + +# ---- 2. direct touch: theirs changes the proved symbol itself -> ReReason -- + +def test_direct_touch_rereason(): + ours = _trace(SRC, results=[_proved("f")]) + theirs = _trace("let g x = x + 1\nlet f x = g x + 99\nlet h x = x * 10\n") # f's body changed + rep = merge(ours, theirs) + assert "f" in rep["delta"]["changed"] + assert rep["carried_forward"] == [] + assert [r["result_id"] for r in rep["rereason"]] == ["vr1"] + rr = rep["rereason"][0] + assert rr["kind"] == "needs_rereasoning" + assert rr["residual_id"] == "rereason-vr1" + assert "f" in rr["touched"] + assert rr["cause"] == "closure-changed" + assert rr["target"] == {"target_type": "artifact", "target_id": "vr1"} + + +# ---- 3. transitive (the killer case): theirs changes helper g, not f ------- + +def test_transitive_touch_rereason(): + ours = _trace(SRC, results=[_proved("f")]) + # g's body changes; f's own text is untouched, but g is in f's closure. + theirs = _trace("let g x = x + 500\nlet f x = g x + 2\nlet h x = x * 10\n") + rep = merge(ours, theirs) + # g's edit changes g's checksum AND (via the closure checksum) f's — both land in the delta. + assert "g" in rep["delta"]["changed"] + assert rep["carried_forward"] == [] + rr = rep["rereason"][0] + assert rr["result_id"] == "vr1" + assert "g" in rr["touched"] # closure caught the cross-cut + + +# ---- 4. added / removed symbol present in delta --------------------------- + +def test_added_and_removed_in_delta(): + ours = _trace("let g x = x + 1\nlet f x = g x + 2\n") + theirs = _trace("let f x = 42\nlet k x = x - 1\n") # g removed, k added, f changed + rep = merge(ours, theirs) + assert rep["delta"]["added"] == ["k"] + assert rep["delta"]["removed"] == ["g"] + assert "f" in rep["delta"]["changed"] + + +# ---- 5. totality: every standing result bucketed exactly once ------------- + +def test_totality(): + ours = _trace(SRC, results=[ + _proved("f", vg="vgf", vr="vrf"), + _proved("h", vg="vgh", vr="vrh"), + ]) + theirs = _trace("let g x = x + 1\nlet f x = g x + 2\nlet h x = x * 999\n") # h changed + rep = merge(ours, theirs) + assert rep["totality_ok"] is True + ids = {c["result_id"] for c in rep["carried_forward"]} | {r["result_id"] for r in rep["rereason"]} + assert ids == {"vrf", "vrh"} + # h touched -> rereason; f disjoint -> carried; each exactly once + assert {c["result_id"] for c in rep["carried_forward"]} == {"vrf"} + assert {r["result_id"] for r in rep["rereason"]} == {"vrh"} + assert rep["counts"] == {"standing": 2, "carried": 1, "rereason": 1, "delta": 1} + + +# ---- 6. no-false-fresh: a genuinely-affected result is NEVER carried ------ + +def test_no_false_fresh(): + ours = _trace(SRC, results=[_proved("f")]) + theirs = _trace("let g x = x + 500\nlet f x = g x + 2\nlet h x = x * 10\n") # transitive hit + rep = merge(ours, theirs) + carried_ids = {c["result_id"] for c in rep["carried_forward"]} + assert "vr1" not in carried_ids # affected result never appears as fresh + assert "vr1" in {r["result_id"] for r in rep["rereason"]} + + +# ---- 7. 3-way base attribution ------------------------------------------- + +def test_three_way_base_attribution(): + base = _trace("let g x = x + 1\nlet f x = g x + 2\n") + # OURS changed g (vs base); THEIRS is identical to base (didn't touch g). + ours = _trace("let g x = x + 7\nlet f x = g x + 2\n", results=[_proved("f")]) + theirs = _trace("let g x = x + 1\nlet f x = g x + 2\n") + + # With --base: theirs did NOT change g vs base -> g not in delta -> f carried forward. + rep3 = merge(ours, theirs, base=base) + assert rep3["delta"]["changed"] == [] + assert {c["result_id"] for c in rep3["carried_forward"]} == {"vr1"} + assert rep3["rereason"] == [] + + # Contrast 2-way (no base): reference is OURS, whose g differs from theirs -> g in delta -> rereason. + rep2 = merge(ours, theirs) + assert "g" in rep2["delta"]["changed"] + assert {r["result_id"] for r in rep2["rereason"]} == {"vr1"} + + +# ---- 8. assumption-awareness --------------------------------------------- + +def test_assumption_awareness(): + ours = _trace(SRC, results=[_proved("f")], + residuals=[{"residual_id": "as1", "kind": "assumption", "status": "open", + "statement": "assume g is monotone", "related_artifact_ids": ["vr1"]}]) + theirs = _trace("let g x = x + 500\nlet f x = g x + 2\nlet h x = x * 10\n") # touches closure + rep = merge(ours, theirs) + rr = rep["rereason"][0] + assert rr["assumptions_in_question"] == ["as1"] + assert "as1" in rr["statement"] + + +def test_assumption_ignored_when_disjoint(): + # An open assumption on a result that is NOT touched stays silent (it's carried forward). + ours = _trace(SRC, results=[_proved("f")], + residuals=[{"residual_id": "as1", "kind": "assumption", "status": "open", + "related_artifact_ids": ["vr1"]}]) + theirs = _trace("let g x = x + 1\nlet f x = g x + 2\nlet h x = x * 999\n") # only h + rep = merge(ours, theirs) + assert {c["result_id"] for c in rep["carried_forward"]} == {"vr1"} + assert rep["rereason"] == [] + + +def test_closed_assumption_not_cited(): + ours = _trace(SRC, results=[_proved("f")], + residuals=[{"residual_id": "as1", "kind": "assumption", "status": "addressed", + "related_artifact_ids": ["vr1"]}]) + theirs = _trace("let g x = x + 500\nlet f x = g x + 2\nlet h x = x * 10\n") + rep = merge(ours, theirs) + assert rep["rereason"][0]["assumptions_in_question"] == [] + + +# ---- edge cases ---------------------------------------------------------- + +def test_empty_delta_all_carried(): + ours = _trace(SRC, results=[_proved("f"), _proved("h", vg="vgh", vr="vrh")]) + theirs = _trace(SRC) # identical source -> empty delta + rep = merge(ours, theirs) + assert rep["delta"] == {"changed": [], "added": [], "removed": []} + assert len(rep["carried_forward"]) == 2 + assert rep["rereason"] == [] + assert rep["totality_ok"] is True + + +def test_empty_trace(): + ours = {"trace_id": "t", "artifacts": []} + theirs = {"trace_id": "t", "artifacts": []} + rep = merge(ours, theirs) + assert rep["counts"]["standing"] == 0 + assert rep["carried_forward"] == [] + assert rep["rereason"] == [] + assert rep["totality_ok"] is True + + +def test_standing_only_proved_counts(): + # A refuted result is a live issue, not a standing fact -> not a standing result. + refuted = [ + {"artifact_id": "vgr", "artifact_type": "VerificationGoal", "producer_action_id": 2, + "payload": {"goal_id": "GR", "target_symbol": "f"}}, + {"artifact_id": "vrr", "artifact_type": "VerificationResult", "producer_action_id": 3, + "payload": {"goal_id": "GR", "goal_artifact_id": "vgr", "status": "refuted"}}, + ] + t = _trace(SRC, results=[refuted]) + assert _standing_results(t) == [] + + +def test_latest_standing_wins(): + # Two proofs about f; the later one is the standing result. + ours = _trace(SRC, results=[ + _proved("f", vg="vg_old", vr="vr_old", step=2), + _proved("f", vg="vg_new", vr="vr_new", step=10), + ]) + ids = {r["result_id"] for r in _standing_results(ours)} + assert ids == {"vr_new"} + + +def test_symbols_latest_revision_wins(): + # A later model revision that drops h changes the symbol set / checksums accordingly. + t = {"trace_id": "t", "artifacts": [ + _model("let g x = x + 1\nlet h x = x\n", aid="m1", step=1), + _model("let g x = x + 2\n", aid="m2", step=5), # later: g redefined, h still present from m1 + ]} + # h from m1 survives (never redefined), g's latest def wins. + assert "g" in _symbols(t) and "h" in _symbols(t) + + +def test_delta_helper_direct(): + ours = _trace("let a x = x\nlet b x = x\n") + theirs = _trace("let a x = x + 1\nlet c x = x\n") # a changed; b -> c is a rename (identical body) + d = merge_delta(ours, theirs) + # Component-aware (2b): `b` and `c` have byte-identical bodies modulo their own name, so `b -> c` is + # an exact-fingerprint rename (content unchanged), NOT a remove+add. `a` still changed. + assert d["changed"] == ["a"] + assert d["added"] == [] and d["removed"] == [] + assert d["renamed"] == [{"from": "b", "to": "c", "changed": False}] + + +# ---- 2b. rename-aware merge_delta ---------------------------------------- + +# A helper `g` with a distinctive multi-line body. A rename touches only the signature line, so with a +# body of enough shared lines the similarity stays confidently above the 80% floor (identity.iml's +# SIM_MIN) while an unrelated add is far below it. +_G_BODY = ("let g x =\n" + " let a = x + 1 in\n" + " let b = a * 2 in\n" + " let c = b + 4 in\n" + " let d = c * 5 in\n" + " let e = d - 6 in\n" + " let f0 = e + 8 in\n" + " let g0 = f0 * 9 in\n" + " let h0 = g0 - 10 in\n" + " let i0 = h0 + 11 in\n" + " let j0 = i0 * 12 in\n" + " j0 + 7\n") +_G2_BODY_SAME = _G_BODY.replace("let g x =", "let g2 x =") # rename, identical body +_G2_BODY_CHANGED = _G2_BODY_SAME.replace(" j0 + 7\n", " j0 + 999\n") # rename + one-line body change +_F_ON_G = "let f x = g x + 2\n" +_F_ON_G2 = "let f x = g2 x + 2\n" + + +def test_rename_unchanged_carried_forward(): + # ours proves f (which calls helper g); theirs renames g -> g2 with an IDENTICAL body. + ours = _trace(_G_BODY + _F_ON_G, results=[_proved("f")]) + theirs = _trace(_G2_BODY_SAME + _F_ON_G2) + rep = merge(ours, theirs) + # g is a rename, content unchanged -> NOT in the delta; renamed records g -> g2 (changed:false). + assert rep["delta"]["renamed"] == [{"from": "g", "to": "g2", "changed": False}] + assert "g" not in rep["delta"]["removed"] + assert "g2" not in rep["delta"]["added"] + assert "g" not in rep["delta"]["changed"] + # f only differs by the callee's NAME; f's own text changed (g -> g2) so f is a real change and + # re-reasons. The payoff is that g's *proof/closure* is not spuriously remove+add'd. + # (Contrast pre-2b: g removed + g2 added would put both in the delta.) + assert rep["delta"]["removed"] == [] and rep["delta"]["added"] == [] + + +def test_rename_unchanged_pure_helper_carried_forward(): + # Isolate the payoff: theirs renames ONLY the unused helper g -> g2, f untouched (does not call g). + src = _G_BODY + "let f x = x + 2\n" + ours = _trace(src, results=[_proved("f")]) + theirs = _trace(_G2_BODY_SAME + "let f x = x + 2\n") + rep = merge(ours, theirs) + assert rep["delta"]["renamed"] == [{"from": "g", "to": "g2", "changed": False}] + # Nothing in the delta at all -> f's proof is carried forward, NOT re-reasoned. + assert rep["delta"]["changed"] == [] + assert rep["delta"]["added"] == [] and rep["delta"]["removed"] == [] + assert {c["result_id"] for c in rep["carried_forward"]} == {"vr1"} + assert rep["rereason"] == [] + + +def test_rename_changed_rereasons(): + # theirs renames g -> g2 AND changes its body; f calls the helper. + ours = _trace(_G_BODY + _F_ON_G, results=[_proved("f")]) + theirs = _trace(_G2_BODY_CHANGED + _F_ON_G2) + rep = merge(ours, theirs) + assert rep["delta"]["renamed"] == [{"from": "g", "to": "g2", "changed": True}] + # A content-changed rename: g (the old name) lands in `changed`, not remove+add. + assert "g" in rep["delta"]["changed"] + assert "g" not in rep["delta"]["removed"] + assert "g2" not in rep["delta"]["added"] + # g is in f's closure -> f re-reasons. + assert {r["result_id"] for r in rep["rereason"]} == {"vr1"} + assert rep["carried_forward"] == [] + + +def test_genuine_remove_add_stays(): + # A removed symbol with no similar added counterpart stays removed; the unrelated add stays added. + ours = _trace(_G_BODY + "let f x = x + 2\n", results=[_proved("f")]) + theirs = _trace("let totally_new p q = p * q - 7\nlet f x = x + 2\n") # g removed, unrelated add + rep = merge(ours, theirs) + assert rep["delta"].get("renamed") is None # no rename detected + assert rep["delta"]["removed"] == ["g"] + assert rep["delta"]["added"] == ["totally_new"] + + +def test_ambiguous_rename_stays_remove_add(): + # Two added symbols equally similar to the removed one -> never-guess -> stays remove+add. + g2a = _G_BODY.replace("let g x =", "let g2a x =") + g2b = _G_BODY.replace("let g x =", "let g2b x =") + ours = _trace(_G_BODY + "let f x = x + 2\n", results=[_proved("f")]) + theirs = _trace(g2a + g2b + "let f x = x + 2\n") # g removed; two equally-similar adds + rep = merge(ours, theirs) + assert rep["delta"].get("renamed") is None + assert rep["delta"]["removed"] == ["g"] + assert set(rep["delta"]["added"]) == {"g2a", "g2b"} diff --git a/cli/tests/unit/test_merge_combine.py b/cli/tests/unit/test_merge_combine.py new file mode 100644 index 0000000..7c307a6 --- /dev/null +++ b/cli/tests/unit/test_merge_combine.py @@ -0,0 +1,224 @@ +"""Unit tests for the two-parent trace COMBINE (ponens.merge.combine). + +`combine` materializes `merge()`'s report into a VALID merged trace that `ponens trace +validate`/`enrich`/`check` accept. These tests reuse the trace builders from test_merge and assert the +materialized trace validates, records the two-parent MergeEvent, carries CarriedForward artifacts + +needs_rereasoning/coverage_regression residuals, is total, and enriches cleanly. +""" + +import json +import os +import subprocess +import sys + +from ponens.merge import combine, merge, _standing_results +from ponens.trace import validate_trace +from ponens import goals as goalops + +# The source-tree `cli/` dir (…/cli/tests/unit/this_file → …/cli). CLI subprocesses run with this as +# cwd + on PYTHONPATH so they exercise the SOURCE `ponens`, not any pip-installed copy. +_CLI_DIR = os.path.abspath(os.path.join(os.path.dirname(__file__), "..", "..")) + + +def _run_cli(*argv): + env = dict(os.environ, PYTHONPATH=_CLI_DIR + os.pathsep + os.environ.get("PYTHONPATH", "")) + return subprocess.run([sys.executable, "-m", "ponens.cli", *argv], + capture_output=True, text=True, cwd=_CLI_DIR, env=env) + + +# ---- trace builders (mirrors test_merge) ---------------------------------- + +def _model(src, aid="m1", step=1, derived_from=None): + a = {"artifact_id": aid, "artifact_type": "IMLModel", "producer_action_id": step, + "payload": {"iml_code": src}} + if derived_from is not None: + a["derived_from"] = derived_from + return a + + +def _proved(sym, vg="vg1", vr="vr1", step=2, desc=None): + return [ + {"artifact_id": vg, "artifact_type": "VerificationGoal", "producer_action_id": step, + "payload": {"goal_id": vg + "-G", "target_symbol": sym, + "description": desc or f"property of {sym}"}}, + {"artifact_id": vr, "artifact_type": "VerificationResult", "producer_action_id": step + 1, + "derived_from": [vg], "payload": {"goal_id": vg + "-G", "goal_artifact_id": vg, + "status": "proved"}}, + ] + + +def _trace(src, results=None, residuals=None, step=1, tid="t"): + t = {"trace_id": tid, "artifacts": [_model(src, step=step)]} + for r in results or []: + t["artifacts"].extend(r) + if residuals: + t["residuals"] = residuals + return t + + +SRC = "let g x = x + 1\nlet f x = g x + 2\nlet h x = x * 10\n" + + +# ---- 1. combine() produces a trace validate accepts ------------------------ + +def test_combine_validates_disjoint(): + ours = _trace(SRC, results=[_proved("f")], tid="ours") + theirs = _trace("let g x = x + 1\nlet f x = g x + 2\nlet h x = x * 999\n", tid="theirs") # only h + merged = combine(ours, theirs) + errors, _warnings = validate_trace(merged) + assert errors == [], errors + + +def test_combine_validates_rereason(): + ours = _trace(SRC, results=[_proved("f")], tid="ours") + theirs = _trace("let g x = x + 1\nlet f x = g x + 99\nlet h x = x * 10\n", tid="theirs") # f changed + merged = combine(ours, theirs) + errors, _warnings = validate_trace(merged) + assert errors == [], errors + + +# ---- 2. MergeEvent: two parents + base + fresh trace_id -------------------- + +def test_combine_records_mergeevent(): + ours = _trace(SRC, results=[_proved("f")], tid="ours") + theirs = _trace(SRC.replace("999", "x"), tid="theirs") + merged = combine(ours, theirs) + assert merged["merge"]["parents"] == ["ours", "theirs"] + assert merged["merge"]["base"] is None + assert merged["merge"]["kind"] == "merge" + assert merged["trace_id"] == "merge-ours-theirs" + assert merged["trace_id"] not in ("ours", "theirs") + # trace_links records the two-parent lineage too. + assert any(l.get("kind") == "merge" and l.get("parents") == ["ours", "theirs"] + for l in merged.get("trace_links", [])) + + +def test_combine_records_base(): + base = _trace(SRC, tid="base") + ours = _trace(SRC, results=[_proved("f")], tid="ours") + theirs = _trace("let g x = x + 1\nlet f x = g x + 2\nlet h x = x * 999\n", tid="theirs") + merged = combine(ours, theirs, base=base) + assert merged["merge"]["base"] == "base" + + +# ---- 3. materialized findings --------------------------------------------- + +def test_combine_carried_forward_artifact(): + ours = _trace(SRC, results=[_proved("f")], tid="ours") + theirs = _trace("let g x = x + 1\nlet f x = g x + 2\nlet h x = x * 999\n", tid="theirs") # only h + merged = combine(ours, theirs) + cf = [a for a in merged["artifacts"] if a["artifact_type"] == "CarriedForward"] + assert [a["artifact_id"] for a in cf] == ["carried-vr1"] + a = cf[0] + assert a["derived_from"] == ["vr1"] + assert a["payload"]["symbol"] == "f" + assert a["payload"]["basis"] == "closure-disjoint" + # producer_action_id resolves to a real merge action. + action_ids = {act["id"] for act in merged["actions"]} + assert a["producer_action_id"] in action_ids + merge_actions = [act for act in merged["actions"] if act["type"] == "merge"] + assert len(merge_actions) == 1 + + +def test_combine_needs_rereasoning_residual(): + ours = _trace(SRC, results=[_proved("f")], tid="ours") + theirs = _trace("let g x = x + 1\nlet f x = g x + 99\nlet h x = x * 10\n", tid="theirs") # f changed + merged = combine(ours, theirs) + rr = [r for r in merged["residuals"] if r["kind"] == "needs_rereasoning"] + assert [r["residual_id"] for r in rr] == ["rereason-vr1"] + assert rr[0]["status"] == "open" + assert rr[0]["derived"] is True + assert rr[0]["target"] == {"target_type": "artifact", "target_id": "vr1"} + # no CarriedForward for a re-reasoned result. + assert [a for a in merged["artifacts"] if a["artifact_type"] == "CarriedForward"] == [] + + +def test_combine_coverage_regression_residual(): + # OURS has a goal scoped over `newf`; theirs ADDS an in-scope, unproven component `newf`. + ours = {"trace_id": "ours", + "artifacts": [_model(SRC)], + "goals": [{"id": "G", "intent": "cover", "scope": ["newf"]}]} + theirs = _trace(SRC + "let newf x = x + 7\n", tid="theirs") # newf added, unproven + rep = merge(ours, theirs) + assert rep.get("coverage_regressions"), "fixture should trigger a coverage regression" + merged = combine(ours, theirs) + cov = [r for r in merged["residuals"] if r["kind"] == "coverage_regression"] + assert len(cov) == 1 + assert cov[0]["goal_id"] == "G" + assert cov[0]["derived"] is True + errors, _ = validate_trace(merged) + assert errors == [], errors + + +# ---- 4. totality ---------------------------------------------------------- + +def test_combine_totality(): + # two standing results: one carried (h unrelated), one re-reasoned (f touched) + ours = _trace(SRC, + results=[_proved("f", vg="vgf", vr="vrf"), + _proved("h", vg="vgh", vr="vrh")], + tid="ours") + theirs = _trace("let g x = x + 1\nlet f x = g x + 99\nlet h x = x * 10\n", tid="theirs") # f changed + merged = combine(ours, theirs) + standing = {r["result_id"] for r in _standing_results(ours)} + carried = {a["derived_from"][0] for a in merged["artifacts"] + if a["artifact_type"] == "CarriedForward"} + rereasoned = set() + rep = merge(ours, theirs) + rereasoned = {r["result_id"] for r in rep["rereason"]} + assert carried | rereasoned == standing + assert carried.isdisjoint(rereasoned) + assert carried == {"vrh"} + assert rereasoned == {"vrf"} + + +# ---- 5. enrich runs + a carried goal still resolves ------------------------ + +def test_combine_enriches_and_goal_resolves(): + ours = _trace(SRC, results=[_proved("f")], tid="ours") + theirs = _trace("let g x = x + 1\nlet f x = g x + 2\nlet h x = x * 999\n", tid="theirs") # only h + merged = combine(ours, theirs) + enriched = goalops.enrich(merged) # must not raise + assert enriched is not None + # the carried result survived into the merged/enriched trace. + cf = [a for a in enriched["artifacts"] if a["artifact_type"] == "CarriedForward"] + assert cf and cf[0]["payload"]["symbol"] == "f" + + +# ---- 6. CLI: --combine -o writes a validate-passing file ------------------- + +def test_cli_combine_writes_valid_trace(tmp_path): + ours = _trace(SRC, results=[_proved("f")], tid="ours") + theirs = _trace("let g x = x + 1\nlet f x = g x + 2\nlet h x = x * 999\n", tid="theirs") + ours_p = tmp_path / "ours.json" + theirs_p = tmp_path / "theirs.json" + merged_p = tmp_path / "merged.json" + ours_p.write_text(json.dumps(ours)) + theirs_p.write_text(json.dumps(theirs)) + + r = _run_cli("trace", "merge", str(ours_p), str(theirs_p), "--combine", "-o", str(merged_p)) + assert r.returncode == 0, r.stderr + assert merged_p.exists() + merged = json.loads(merged_p.read_text()) + errors, _ = validate_trace(merged) + assert errors == [], errors + assert merged["merge"]["parents"] == ["ours", "theirs"] + + # validate via the CLI too. + v = _run_cli("trace", "validate", str(merged_p)) + assert v.returncode == 0, v.stderr + + +def test_cli_merge_default_still_report(tmp_path): + """Backward-compat: without --combine the CLI still prints the merge REPORT.""" + ours = _trace(SRC, results=[_proved("f")], tid="ours") + theirs = _trace("let g x = x + 1\nlet f x = g x + 2\nlet h x = x * 999\n", tid="theirs") + ours_p = tmp_path / "ours.json" + theirs_p = tmp_path / "theirs.json" + ours_p.write_text(json.dumps(ours)) + theirs_p.write_text(json.dumps(theirs)) + r = _run_cli("trace", "merge", str(ours_p), str(theirs_p)) + assert r.returncode == 0, r.stderr + out = json.loads(r.stdout) + assert "carried_forward" in out and "delta" in out + assert "merge" not in out # a report, not a trace diff --git a/cli/tests/unit/test_merge_coverage.py b/cli/tests/unit/test_merge_coverage.py new file mode 100644 index 0000000..9eecde4 --- /dev/null +++ b/cli/tests/unit/test_merge_coverage.py @@ -0,0 +1,161 @@ +"""Unit tests for the goal-COVERAGE layer of trace MERGE (ponens.merge). + +SelectorRegression, realized over `goal.scope` (the coverage mechanism that exists today): a merge that +changes WHAT A GOAL MUST COVER — adds/removes an in-scope component — regresses the obligation, even when +no existing proof's closure changed. This is a distinct goal-level section from the result-level +carried_forward/rereason buckets, and is purely additive to the merge report. +""" + +from ponens.merge import merge, _in_scope + + +# ---- trace builders (mirroring test_merge.py) ----------------------------- + +def _model(src, aid="m1", step=1): + return {"artifact_id": aid, "artifact_type": "IMLModel", "producer_action_id": step, + "payload": {"iml_code": src}} + + +def _proved(sym, vg="vg1", vr="vr1", step=2): + return [ + {"artifact_id": vg, "artifact_type": "VerificationGoal", "producer_action_id": step, + "payload": {"goal_id": vg + "-G", "target_symbol": sym, + "description": f"property of {sym}"}}, + {"artifact_id": vr, "artifact_type": "VerificationResult", "producer_action_id": step + 1, + "derived_from": [vg], "payload": {"goal_id": vg + "-G", "goal_artifact_id": vg, + "status": "proved"}}, + ] + + +def _trace(src, results=None, goals=None, step=1): + t = {"trace_id": "t", "artifacts": [_model(src, step=step)]} + for r in results or []: + t["artifacts"].extend(r) + if goals is not None: + t["goals"] = goals + return t + + +def _goal(gid="G1", scope=None): + return {"id": gid, "intent": f"cover {gid}", "scope": scope or []} + + +# ---- 1. added in-scope unproven -> regression ----------------------------- + +def test_added_in_scope_unproven_regresses(): + ours = _trace("let payments x = x + 1\n", + goals=[_goal("G1", scope=["payments"])]) + theirs = _trace("let payments x = x + 1\nlet payments_newfee x = x + 5\n") + rep = merge(ours, theirs) + assert "payments_newfee" in rep["delta"]["added"] + cr = rep["coverage_regressions"] + assert len(cr) == 1 + entry = cr[0] + assert entry["goal_id"] == "G1" + assert entry["kind"] == "coverage_regression" + assert entry["residual_id"] == "coverage-G1" + assert entry["added_members"] == ["payments_newfee"] + assert entry["removed_members"] == [] + assert entry["severity"] == "medium" + assert entry["status"] == "open" + assert entry["derived"] is True + assert entry["scope"] == ["payments"] + + +# ---- 2. added out-of-scope -> no regression ------------------------------- + +def test_added_out_of_scope_no_regression(): + ours = _trace("let payments x = x + 1\n", + goals=[_goal("G1", scope=["payments"])]) + theirs = _trace("let payments x = x + 1\nlet shipping x = x + 5\n") # not matching scope + rep = merge(ours, theirs) + assert "shipping" in rep["delta"]["added"] + assert "coverage_regressions" not in rep + + +# ---- 3. added in-scope BUT already proved -> no regression ---------------- + +def test_added_in_scope_but_proved_no_regression(): + ours = _trace("let payments x = x + 1\n", + goals=[_goal("G1", scope=["payments"])]) + # theirs adds payments_newfee AND carries a standing proof about it -> covered in merged view. + theirs = _trace("let payments x = x + 1\nlet payments_newfee x = x + 5\n", + results=[_proved("payments_newfee", vg="vgn", vr="vrn")]) + rep = merge(ours, theirs) + assert "payments_newfee" in rep["delta"]["added"] + assert "coverage_regressions" not in rep + + +# ---- 4. removed in-scope -> recorded ------------------------------------- + +def test_removed_in_scope_recorded(): + ours = _trace("let payments x = x + 1\nlet payments_legacy x = x - 1\n", + goals=[_goal("G1", scope=["payments"])]) + theirs = _trace("let payments x = x + 1\n") # payments_legacy removed + rep = merge(ours, theirs) + assert "payments_legacy" in rep["delta"]["removed"] + cr = rep["coverage_regressions"] + assert len(cr) == 1 + entry = cr[0] + assert entry["removed_members"] == ["payments_legacy"] + assert entry["added_members"] == [] + assert entry["severity"] == "low" + + +# ---- 5. no scope / no goals -> field omitted ----------------------------- + +def test_goal_without_scope_no_field(): + ours = _trace("let payments x = x + 1\n", goals=[_goal("G1", scope=[])]) + theirs = _trace("let payments x = x + 1\nlet payments_newfee x = x + 5\n") + rep = merge(ours, theirs) + assert "coverage_regressions" not in rep + + +def test_no_goals_no_field(): + ours = _trace("let payments x = x + 1\n") # no goals key at all + theirs = _trace("let payments x = x + 1\nlet payments_newfee x = x + 5\n") + rep = merge(ours, theirs) + assert "coverage_regressions" not in rep + # sanity: the rest of the report is present and unchanged in shape + assert set(rep.keys()) == {"delta", "carried_forward", "rereason", "totality_ok", "counts"} + + +# ---- 6. rename not double-counted ---------------------------------------- + +# A distinctive multi-line in-scope helper whose rename touches only the signature line, so the +# similarity resolver confidently detects a rename (see test_merge.py's _G_BODY convention). +_PAY_BODY = ("let payments_calc x =\n" + " let a = x + 1 in\n" + " let b = a * 2 in\n" + " let c = b + 4 in\n" + " let d = c * 5 in\n" + " let e = d - 6 in\n" + " let f0 = e + 8 in\n" + " let g0 = f0 * 9 in\n" + " let h0 = g0 - 10 in\n" + " let i0 = h0 + 11 in\n" + " let j0 = i0 * 12 in\n" + " j0 + 7\n") +_PAY_BODY_RENAMED = _PAY_BODY.replace("let payments_calc x =", "let payments_compute x =") + + +def test_rename_not_double_counted(): + ours = _trace(_PAY_BODY, goals=[_goal("G1", scope=["payments"])]) + theirs = _trace(_PAY_BODY_RENAMED) # payments_calc -> payments_compute, identical body + rep = merge(ours, theirs) + # rename reconciled by merge_delta: not in added/removed. + assert rep["delta"].get("renamed") == [{"from": "payments_calc", "to": "payments_compute", + "changed": False}] + assert rep["delta"]["added"] == [] and rep["delta"]["removed"] == [] + # so no coverage churn: the renamed component appears as neither added nor removed member. + assert "coverage_regressions" not in rep + + +# ---- helper predicate ---------------------------------------------------- + +def test_in_scope_predicate(): + assert _in_scope("payments_newfee", ["payments"]) is True # substring + assert _in_scope("payments", ["Payments"]) is True # case-insensitive + assert _in_scope("shipping", ["payments"]) is False + assert _in_scope("", ["payments"]) is False + assert _in_scope("payments", []) is False diff --git a/cli/tests/unit/test_merge_skipcontract.py b/cli/tests/unit/test_merge_skipcontract.py new file mode 100644 index 0000000..7467ef9 --- /dev/null +++ b/cli/tests/unit/test_merge_skipcontract.py @@ -0,0 +1,215 @@ +"""Unit tests for the SkipContract branch of residual-aware trace MERGE (ponens.merge). + +Upgrades `classify` from two live branches (SkipDisjoint / ReReason) to the three the proved model in +`formal/merge/classify.iml` has, for the SOUND slice only: the SkipContract branch fires when EVERY +genuinely-changed touched dependency of a standing result is `uninterpreted` in OURS's model +assumptions. The proved classifier's opaque `dep_kind ∈ {Uninterpreted, Typed, Axiomatized, Pinned}` is +realized at the trace level by the model artifact's structured `payload.assumptions` list of +`{target, abstraction, discharged?, ...}` (the producer's `ArtifactAssumption`, where +`abstraction ∈ 'concrete'|'contract'|'uninterpreted'|'pinned'`). + +The sound rule: `uninterpreted` = the result proved its property for ALL values of that opaque dep, so +any merge change to the dep leaves the property holding -> carry forward. `contract` (even discharged), +`pinned`, `concrete`, and no-assumption -> re-reason (stale discharge / genuine dependence). +""" + +from ponens.merge import merge, _assumptions_index + + +# ---- trace builders (mirror test_merge.py, plus payload.assumptions) ------- + +def _model(src, aid="m1", step=1, assumptions=None): + payload = {"iml_code": src} + if assumptions is not None: + payload["assumptions"] = assumptions + return {"artifact_id": aid, "artifact_type": "IMLModel", "producer_action_id": step, + "payload": payload} + + +def _proved(sym, vg="vg1", vr="vr1", step=2): + return [ + {"artifact_id": vg, "artifact_type": "VerificationGoal", "producer_action_id": step, + "payload": {"goal_id": vg + "-G", "target_symbol": sym, + "description": f"property of {sym}"}}, + {"artifact_id": vr, "artifact_type": "VerificationResult", "producer_action_id": step + 1, + "derived_from": [vg], "payload": {"goal_id": vg + "-G", "goal_artifact_id": vg, + "status": "proved"}}, + ] + + +def _trace(src, results=None, assumptions=None): + t = {"trace_id": "t", "artifacts": [_model(src, assumptions=assumptions)]} + for r in results or []: + t["artifacts"].extend(r) + return t + + +# f depends on g (transitive); f's OWN body is unchanged across the merge in every "g changes" case. +SRC = "let g x = x + 1\nlet f x = g x + 2\n" +SRC_G_CHANGED = "let g x = x + 500\nlet f x = g x + 2\n" # only g's body differs; f's body identical + +# f depends on g AND h; both g and h are dependencies of f. +SRC_GH = "let g x = x + 1\nlet h x = x - 1\nlet f x = g x + h x\n" +SRC_GH_BOTH_CHANGED = "let g x = x + 500\nlet h x = x - 500\nlet f x = g x + h x\n" + + +def _assert_totality(rep): + carried = {c["result_id"] for c in rep["carried_forward"]} + rereason = {r["result_id"] for r in rep["rereason"]} + assert rep["totality_ok"] is True + assert carried.isdisjoint(rereason) + assert carried | rereason == {"vr1"} # single standing result in these fixtures + + +# ---- 0. the index reads payload.assumptions ------------------------------- + +def test_assumptions_index_reads_payload(): + ours = _trace(SRC, results=[_proved("f")], + assumptions=[{"target": "g", "kind": "callee", "abstraction": "uninterpreted"}]) + assert _assumptions_index(ours) == {"g": "uninterpreted"} + # tolerant: an entry missing target/abstraction is skipped, empty/missing yields {} + assert _assumptions_index(_trace(SRC, results=[_proved("f")])) == {} + messy = _trace(SRC, results=[_proved("f")], + assumptions=[{"kind": "callee"}, {"target": "g"}, "not-a-dict", None]) + assert _assumptions_index(messy) == {} + + +# ---- 1. uninterpreted -> carried forward (the SkipContract win) ----------- + +def test_uninterpreted_carried_forward(): + ours = _trace(SRC, results=[_proved("f")], + assumptions=[{"target": "g", "kind": "callee", "abstraction": "uninterpreted"}]) + theirs = _trace(SRC_G_CHANGED) # g's body changes + rep = merge(ours, theirs) + assert "g" in rep["delta"]["changed"] + assert rep["rereason"] == [] + assert [c["result_id"] for c in rep["carried_forward"]] == ["vr1"] + cf = rep["carried_forward"][0] + assert cf["basis"] == "uninterpreted-opaque" + assert cf["via_assumptions"] == ["g"] + _assert_totality(rep) + + +def test_contrast_no_assumption_rereasons(): + """Same code change, but WITHOUT the uninterpreted assumption -> re-reason. Isolates that the + SkipContract win comes from the assumption data, not the code.""" + ours = _trace(SRC, results=[_proved("f")]) # no assumptions declared + theirs = _trace(SRC_G_CHANGED) + rep = merge(ours, theirs) + assert rep["carried_forward"] == [] + assert [r["result_id"] for r in rep["rereason"]] == ["vr1"] + _assert_totality(rep) + + +# ---- 2. pinned -> re-reason ----------------------------------------------- + +def test_pinned_rereasons(): + ours = _trace(SRC, results=[_proved("f")], + assumptions=[{"target": "g", "kind": "callee", "abstraction": "pinned"}]) + theirs = _trace(SRC_G_CHANGED) + rep = merge(ours, theirs) + assert rep["carried_forward"] == [] + assert [r["result_id"] for r in rep["rereason"]] == ["vr1"] + _assert_totality(rep) + + +# ---- 3. contract (discharged) but callee changed -> re-reason ------------- + +def test_contract_discharged_but_callee_changed_rereasons(): + """A discharged contract's proof was over the OLD callee body; the callee changed, so the discharge is + stale and there is no recorded reproof formula -> re-reason (sound; reproof deferred).""" + ours = _trace(SRC, results=[_proved("f")], + assumptions=[{"target": "g", "kind": "callee", "abstraction": "contract", + "discharged": True}]) + theirs = _trace(SRC_G_CHANGED) + rep = merge(ours, theirs) + assert rep["carried_forward"] == [] + assert [r["result_id"] for r in rep["rereason"]] == ["vr1"] + _assert_totality(rep) + + +# ---- 4. concrete / no assumption -> re-reason (sound fallback) ------------ + +def test_concrete_rereasons(): + ours = _trace(SRC, results=[_proved("f")], + assumptions=[{"target": "g", "kind": "callee", "abstraction": "concrete"}]) + theirs = _trace(SRC_G_CHANGED) + rep = merge(ours, theirs) + assert rep["carried_forward"] == [] + assert [r["result_id"] for r in rep["rereason"]] == ["vr1"] + _assert_totality(rep) + + +# ---- 5. mixed touched: one uninterpreted, one concrete -> re-reason ------- + +def test_mixed_touched_rereasons(): + """R touches g (uninterpreted) AND h (concrete); BOTH change. Not ALL genuinely-changed touched deps + are opaque -> re-reason (never-false-fresh).""" + ours = _trace(SRC_GH, results=[_proved("f")], + assumptions=[{"target": "g", "kind": "callee", "abstraction": "uninterpreted"}, + {"target": "h", "kind": "callee", "abstraction": "concrete"}]) + theirs = _trace(SRC_GH_BOTH_CHANGED) + rep = merge(ours, theirs) + assert rep["carried_forward"] == [] + assert [r["result_id"] for r in rep["rereason"]] == ["vr1"] + _assert_totality(rep) + + +def test_mixed_touched_all_uninterpreted_carried(): + """Complement of test 5: both changed deps are uninterpreted -> carry forward.""" + ours = _trace(SRC_GH, results=[_proved("f")], + assumptions=[{"target": "g", "kind": "callee", "abstraction": "uninterpreted"}, + {"target": "h", "kind": "callee", "abstraction": "uninterpreted"}]) + theirs = _trace(SRC_GH_BOTH_CHANGED) + rep = merge(ours, theirs) + assert rep["rereason"] == [] + cf = rep["carried_forward"][0] + assert cf["basis"] == "uninterpreted-opaque" + assert cf["via_assumptions"] == ["g", "h"] + _assert_totality(rep) + + +# ---- 5b. result's OWN body changed -> re-reason even if a dep is opaque --- + +def test_own_body_change_blocks_skip(): + """f's own body changes (not just g). Even with g uninterpreted, f is a genuinely-changed touched + component that is not opaque -> re-reason.""" + ours = _trace(SRC, results=[_proved("f")], + assumptions=[{"target": "g", "kind": "callee", "abstraction": "uninterpreted"}]) + theirs = _trace("let g x = x + 500\nlet f x = g x + 99\n") # BOTH g and f bodies change + rep = merge(ours, theirs) + assert rep["carried_forward"] == [] + assert [r["result_id"] for r in rep["rereason"]] == ["vr1"] + _assert_totality(rep) + + +# ---- 6. disjoint still SkipDisjoint (unchanged) --------------------------- + +def test_disjoint_still_skipdisjoint(): + """An unrelated symbol changes; f's closure is untouched -> SkipDisjoint, regardless of assumptions.""" + ours = _trace("let g x = x + 1\nlet f x = g x + 2\nlet k x = x * 10\n", results=[_proved("f")], + assumptions=[{"target": "g", "kind": "callee", "abstraction": "uninterpreted"}]) + theirs = _trace("let g x = x + 1\nlet f x = g x + 2\nlet k x = x * 999\n") # only k changed + rep = merge(ours, theirs) + assert rep["delta"]["changed"] == ["k"] + assert rep["rereason"] == [] + cf = rep["carried_forward"][0] + assert cf["basis"] == "closure-disjoint" # NOT uninterpreted-opaque: nothing in f's closure touched + _assert_totality(rep) + + +# ---- 7. totality holds in every case (covered by _assert_totality above) -- + +def test_totality_across_cases(): + for maker in ( + lambda: (_trace(SRC, results=[_proved("f")], + assumptions=[{"target": "g", "abstraction": "uninterpreted"}]), + _trace(SRC_G_CHANGED)), + lambda: (_trace(SRC, results=[_proved("f")], + assumptions=[{"target": "g", "abstraction": "pinned"}]), + _trace(SRC_G_CHANGED)), + lambda: (_trace(SRC, results=[_proved("f")]), _trace(SRC_G_CHANGED)), + ): + ours, theirs = maker() + rep = merge(ours, theirs) + _assert_totality(rep) diff --git a/cli/tests/unit/test_oracles.py b/cli/tests/unit/test_oracles.py new file mode 100644 index 0000000..8084ad1 --- /dev/null +++ b/cli/tests/unit/test_oracles.py @@ -0,0 +1,80 @@ +"""Oracles — the invocable evidence-producer abstraction (ORACLE_SPEC v0.1): the taxonomy, the +in-process registry, the CodeLogician oracle (driving codelogician-lite → ImandraX), and the +parsing of a real `check-vg --json` result into graded VerificationResults.""" +from ponens import oracles as oc + + +def test_evidence_strength_is_a_total_order_strongest_first(): + assert oc.EVIDENCE_STRENGTH[0] == "proof" + assert oc.strength_rank("proof") < oc.strength_rank("tests") < oc.strength_rank("attested") + # Unknown strengths sort last (never beat a real one). + assert oc.strength_rank("made-up") == len(oc.EVIDENCE_STRENGTH) + + +def test_reasoner_is_the_formal_subtype_of_oracle(): + assert "reasoner" in oc.ORACLE_TYPES + assert oc.oracle_type_for_kind("formal_verification") == "reasoner" + assert oc.oracle_type_for_kind("smt") == "reasoner" + assert oc.oracle_type_for_kind(None) == "reasoner" # default + + +def test_codelogician_oracle_is_registered_and_proof_strength(): + o = oc.get_oracle("codelogician") + assert isinstance(o, oc.CodeLogicianOracle) + assert o.oracle_type == "reasoner" + assert o.evidence_strength == "proof" + assert "VerificationResult" in o.produces + assert any(x.id == "codelogician" for x in oc.list_oracles()) + + +def test_invoke_proved_yields_proof_strength_result(): + # Inject a fake runner so the test is hermetic (no codelogician-lite needed). + fake = lambda target, context=None: { + "status": "proved", "engine": "imandrax", + "result": "1 VG(s): proved", "reasoning_fingerprint": "abc123", + } + o = oc.CodeLogicianOracle(runner=fake) + arts = o.invoke({"iml_code": "let f x = x + 1", "goal": "increases", "target_symbol": "f"}) + assert len(arts) == 1 + art = arts[0] + assert art["artifact_type"] == "VerificationResult" + assert art["artifact_role"] == "ProofRole" + assert art["payload"]["status"] == "proved" + assert art["payload"]["evidence_strength"] == "proof" # graded from the verdict + assert art["payload"]["target_symbol"] == "f" + assert art["name"] == "verify:increases" + + +def test_invoke_refuted_carries_counterexample_and_is_definitive(): + fake = lambda target, context=None: { + "status": "refuted", "engine": "imandrax", "result": "1 VG(s): refuted", + "reasoning_fingerprint": "dead", "counterexample": "x = 0", + } + art = oc.CodeLogicianOracle(runner=fake).invoke({"iml_code": "...", "goal": "g"})[0] + assert art["payload"]["status"] == "refuted" + assert art["payload"]["evidence_strength"] == "proof" # a counterexample is definitive + assert art["payload"]["counterexample"] == "x = 0" + assert art["artifact_role"] == "CounterexampleRole" + + +def test_invoke_unknown_is_not_labeled_with_a_strength(): + # Default runner with no iml_code / no tool -> unknown, and NO evidence_strength claim. + art = oc.CodeLogicianOracle().invoke({"goal": "nothing to check"})[0] + assert art["payload"]["status"] == "unknown" + assert "evidence_strength" not in art["payload"] # never overstate + + +def test_check_vg_json_parsing_against_the_real_schema(): + # Shapes taken verbatim from `codelogician-lite check-vg --json`. + assert oc._eval_ok("Success") is True + assert oc._eval_ok({"success": True}) is True + assert oc._eval_ok({"success": False}) is False + assert oc._verdict_of({"proved": {"proof_pp": "..."}, "refuted": None}) == "proved" + assert oc._verdict_of({"refuted": {"model_str": "x=0"}, "proved": None}) == "refuted" + assert oc._verdict_of({"verified_upto": {"depth": 5}}) == "sat" + assert oc._verdict_of({"unknown": None, "proved": None}) == "unknown" + assert oc._aggregate(["proved", "proved"]) == "proved" + assert oc._aggregate(["proved", "refuted"]) == "refuted" + assert oc._aggregate(["proved", "sat"]) == "sat" + assert oc._aggregate([]) == "unknown" + assert oc._counterexample({"refuted": {"model_str": "x = 0"}}) == "x = 0" diff --git a/cli/tests/unit/test_sdk.py b/cli/tests/unit/test_sdk.py new file mode 100644 index 0000000..57a2530 --- /dev/null +++ b/cli/tests/unit/test_sdk.py @@ -0,0 +1,84 @@ +"""ponens.sdk — the thin runtime SDK: a Session builds a valid trace incrementally, verify() +invokes an oracle inline with lineage, and the context manager validates + saves on exit.""" +import json + +from ponens import sdk +from ponens import oracles as oc +from ponens import trace as trace_mod + + +def test_session_builds_a_structurally_valid_trace(tmp_path): + s = sdk.Session(model="claude-opus", assistant="test-agent", + intent="prove charge() is idempotent") + a = s.action("EditFile", label="edit pricing.py", rationale="fix the retry path", + evidence=[{"type": "FileRef", "ref": "pricing.py"}]) + art = s.artifact("IMLModel", name="pricing.iml", content="let charge x = x", + format="iml", producer_action_id=a) + s.residual("assumption", "gateway returns within 30s", severity="low") + s.outcome("ProcessCompleted") + + errors, _ = s.validate() + assert errors == [] + # The producer action now lists the artifact as an output (lineage wiring). + assert art in s.trace["actions"][0]["outputs"] + # Content was externalized to the object store, not inlined. + assert s.trace["artifacts"][0]["content_ref"].startswith("sha256:") + # The intent became a goal. + assert s.trace["goals"][0]["intent"].startswith("prove charge") + + +def test_verify_records_action_and_graded_evidence_with_lineage(): + fake = lambda target, context=None: { + "status": "proved", "engine": "imandrax", + "result": "Success: 1/1 POs succeeded", "reasoning_fingerprint": "f00d", + } + s = sdk.Session(assistant="test-agent") + model = s.artifact("IMLModel", name="pricing.iml", payload={"iml_code": "let f x = x"}) + ids = s.verify({"iml_code": "let f x = x", "goal": "idempotent"}, + oracle=oc.CodeLogicianOracle(runner=fake), derived_from=model) + + assert len(ids) == 1 + vr = next(x for x in s.trace["artifacts"] if x["artifact_id"] == ids[0]) + assert vr["artifact_type"] == "VerificationResult" + assert vr["payload"]["evidence_strength"] == "proof" + # Lineage: the result derives from the model it verified. + assert model in vr["derived_from"] + # A Verify action was recorded and produced the result. + verify_action = next(a for a in s.trace["actions"] if a["type"] == "Verify") + assert verify_action["category"] == "reasoning" + assert vr["producer_action_id"] == verify_action["id"] + + +def test_verify_rejects_unknown_oracle(): + s = sdk.Session() + try: + s.verify({"goal": "x"}, oracle="does-not-exist") + assert False, "expected ValueError for unknown oracle" + except ValueError as e: + assert "unknown oracle" in str(e) + + +def test_context_manager_saves_valid_trace_and_stamps_outcome(tmp_path): + path = str(tmp_path / "trace.json") + with sdk.Session(assistant="test-agent", path=path, intent="do a thing") as s: + s.action("ReadFile", rationale="read the spec") + # File written, reloads, and passes the structural validator. + reloaded = trace_mod.load_trace(path) + assert reloaded["outcome"]["type"] == "ProcessCompleted" + errors, _ = trace_mod.validate_trace(reloaded) + assert errors == [] + assert reloaded["assistant"] == "test-agent" + + +def test_context_manager_records_abort_on_exception(tmp_path): + path = str(tmp_path / "trace.json") + try: + with sdk.Session(assistant="test-agent", path=path) as s: + s.action("RunCommand", rationale="boom") + raise RuntimeError("kaboom") + except RuntimeError: + pass + # Aborted runs are still saved, marked ProcessAborted (not silently lost). + reloaded = trace_mod.load_trace(path) + assert reloaded["outcome"]["type"] == "ProcessAborted" + assert "kaboom" in reloaded["outcome"]["summary"] diff --git a/spec/AUDIT_READINESS_v0_1.md b/spec/AUDIT_READINESS_v0_1.md index 97d3aae..66d10f3 100644 --- a/spec/AUDIT_READINESS_v0_1.md +++ b/spec/AUDIT_READINESS_v0_1.md @@ -14,7 +14,7 @@ upon as evidence."* A roadmap and a scoping discipline, not a compliance claim. Most "AI governance" tooling produces **attestation** — checklists and self-reported claims. A ponens trace is **evidence**: an immutable, lineage-linked record where every "done" resolves to a specific -artifact ([`TRACE_SPEC_v1_9.md`](TRACE_SPEC_v1_9.md) §18) and every verdict comes from a formal engine +artifact ([`TRACE_SPEC_v1_11.md`](TRACE_SPEC_v1_11.md) §18) and every verdict comes from a formal engine an auditor can **re-run** (§12). That is the difference between *"we assert we did X"* and *"here is X, here is the proof, re-check it yourself."* Everything below follows from holding that line: the trace's value is that it is checkable, not that it is signed off. @@ -98,7 +98,7 @@ qualification, is the bar) rather than safety-certification credit. ## 5. References - Integrity / bind: [`CLI_SYNC_MODEL_v0_1.md`](CLI_SYNC_MODEL_v0_1.md) -- Grounded resolution, freshness, defeaters: [`TRACE_SPEC_v1_9.md`](TRACE_SPEC_v1_9.md) §12, §13, §18 +- Grounded resolution, freshness, defeaters: [`TRACE_SPEC_v1_11.md`](TRACE_SPEC_v1_11.md) §12, §13, §18 - Policy / governance: [`POLICY_SPEC_v0_2.md`](POLICY_SPEC_v0_2.md), [`POLICY_SOURCES_v0_1.md`](POLICY_SOURCES_v0_1.md), the `*_PACK.md` files - Review / certification: [`REVIEW_CASE_SPEC_v0_2.md`](REVIEW_CASE_SPEC_v0_2.md), [`GOAL_FAITHFULNESS_v0_1.md`](GOAL_FAITHFULNESS_v0_1.md) - Interoperability: [`PROV_INTERCHANGE_v0_1.md`](PROV_INTERCHANGE_v0_1.md) diff --git a/spec/GOAL_CONTRACT_v0_1.md b/spec/GOAL_CONTRACT_v0_2.md similarity index 73% rename from spec/GOAL_CONTRACT_v0_1.md rename to spec/GOAL_CONTRACT_v0_2.md index f9b328d..1f5f181 100644 --- a/spec/GOAL_CONTRACT_v0_1.md +++ b/spec/GOAL_CONTRACT_v0_2.md @@ -1,11 +1,17 @@ -# Goal Contract — accomplish these things, subject to these policies (v0.1) +# Goal Contract — accomplish these things, subject to these policies (v0.2) -**Status:** design spec. Refines [Trace Spec §18 (Goals & Acceptance)](TRACE_SPEC_v1_9.md) and +**Status:** design spec. Refines [Trace Spec §18 (Goals & Acceptance)](TRACE_SPEC_v1_11.md) and complements [Goal Faithfulness v0.1](GOAL_FAITHFULNESS_v0_1.md), [Policy Spec v0.2](POLICY_SPEC_v0_2.md), and the [Apply Formal Methods Pack](APPLY_FORMAL_METHODS_PACK.md). Additive and backward-compatible — existing text-bound acceptance items keep resolving (§8). Driven by the CodeLogician Desktop goal loop (`declare_goal` → per-session active goal → `ponens trace enrich`). +> **v0.2 adds composable acceptance (§9).** Criteria compose with `and`/`or`/`not`/`⇒` and quantify +> (`forall`/`exists`) over component **selectors** (`glob`/`module`/`scope`/`tag`), with a per-atom +> **role** (`met` | `governed`) that selects which axis (§2) it is judged on. The atomic criterion of §3 +> is the leaf of this language, so **legacy single-criterion goals are unchanged** — they are the +> implicit `Atom` case and resolve exactly as before. + ## 1. Motivation — two unstructured seams §18 makes acceptance rigorous *once an item binds to evidence*. But the binding for the two kinds that @@ -199,14 +205,82 @@ The enriched goal exposes `met / governed / certified` plus the residuals that e | policy engine | evaluate a goal's effective policy set over its cone; default layering (§5) | | `viewer/core/faithfulness.mjs` | mirror §4 resolution (parity) | -## 9. Open questions +## 9. Composable acceptance — the property language (v0.2) + +§3 gives one criterion = one required artifact over one component (the *atomic* case). v0.2 lets criteria +**compose** and **quantify**, so a goal can state *"every payments function is proved **and** +decomposition-backed"* in a single acceptance item. The atomic criterion is unchanged; it becomes the +**leaf** of a small formula language evaluated by the same lineage resolution (§4). + +### 9.1 Formula + +```ocaml +type formula = + | Atom of acceptance_criterion (* §3 — resolves by lineage (§4) *) + | And of formula list + | Or of formula list + | Not of formula + | Implies of formula * formula + | Forall of { in_ : selector; as_ : string; holds : formula } + | Exists of { in_ : selector; as_ : string; holds : formula } + (* optional `role`, inherited down a subtree — how strictly each atom is judged (§9.2) *) +``` + +An acceptance item MAY carry a `formula` in place of a bare binding. An item **without** one is exactly +today's atomic criterion (an implicit `Atom`), so **legacy goals resolve unchanged** (§7). + +### 9.2 Roles — met vs governed, per atom + +A `role` on a formula (inherited by its subtree) selects which axis of §2 an atom is judged on: + +| role | an atom resolves `done` when… | +| --- | --- | +| `met` | the evidence artifact **exists** in the component's lineage (§4) — the *met* axis only | +| `governed` | it exists **and** is uncontested (no open `Defeater`, §18.2) **and** fresh (§18.3) | +| *(default)* | today's behavior — exists **and** uncontested (defeater-gated), not freshness-gated | + +Roles make the met/governed split of §2 addressable *inside* a single criterion. + +### 9.3 Quantifiers & selectors + +`Forall`/`Exists` range a bound variable over a **selector** — a component set drawn from data the trace +already carries (`component_id`s §7.1, per-model symbols, `high_stakes_paths`): + +| selector | the set | +| --- | --- | +| `glob("payments/**")` | components whose source file matches the glob | +| `module("pricing")` | components in that module / path segment | +| `scope` | the goal's own `scope` | +| `tag("money")` | *(partial)* components under a high-stakes path — a full symbol→tag index is future work | + +A body atom names the bound component as `{ component = var "f" }` (substituted per element). `Forall` is +`And` over the set; `Exists` is `Or`. An **empty selector resolves `todo`, never a vacuous `done`** — an +empty match is almost always a mis-spec, and false-green is the dangerous direction. + +### 9.4 Status lattice -1. **Component cardinality** — is a criterion always 1 component, or may `component` be a set ("these - three functions each verified")? (Proposed: singular; use one criterion per component for clarity.) -2. **Disambiguating within a component** — evidence names an artifact *type*, so if a component has - several artifacts of that type (e.g. two proved properties), the latest is taken. Do we need an - optional per-criterion selector (a property/name filter) to pin *which* one, or is one criterion per - (component, artifact) enough? (Proposed: keep evidence to `{artifact}`; add a selector only if a real - case needs it.) +Combinators compose the four resolved statuses (not booleans), so a contested or partial branch stays +visible instead of collapsing to true/false: + +| op | result | +| --- | --- | +| `and` | `blocked` if any blocked; else `done` if all done; else `doing` if any progress; else `todo` | +| `or` | `done` if any done; else `doing` if any progress; else `blocked` if all blocked; else `todo` | +| `not` | `done`↔`todo`; `doing`→`doing`; `blocked`→`blocked` (contested stays contested — absence of proof is not proof of absence) | +| `implies(a, b)` | `or(not a, b)` | + +Evaluation is additive to §4 and mirrored across the Python (`cli/ponens/goals.py`) and JS resolvers +under the parity harness (§7). + +## 10. Open questions + +1. **Component cardinality** — *Resolved (v0.2, §9.3):* a criterion may quantify over a component set via + `Forall`/`Exists` over a selector; the singular criterion remains the atomic (`Atom`) case. +2. **Disambiguating within a component** — *Partially addressed (v0.2).* The selector language pins which + *components* a criterion ranges over, but within a single component the latest artifact of the required + type is still taken (§4). An optional per-atom *artifact* filter (pin *which* of two proved properties) + is deferred until a real case needs it. 3. **Baseline contents** — exactly which rules are non-optional global baseline vs. opt-in pack. 4. **`satisfies` back-reference** — adopt now (airtight) or defer behind lineage matching. +5. **A symbol→tag index** — `tag(...)` (§9.3) is best-effort over `high_stakes_paths` today; a first-class + tag index would make `tag` selectors precise. diff --git a/spec/GOAL_FAITHFULNESS_v0_1.md b/spec/GOAL_FAITHFULNESS_v0_1.md index 93db8ec..c04ab0a 100644 --- a/spec/GOAL_FAITHFULNESS_v0_1.md +++ b/spec/GOAL_FAITHFULNESS_v0_1.md @@ -1,6 +1,6 @@ # Goal Faithfulness — the definition of done, done right (v0.1) -**Status:** design spec. Refines [Trace Spec §18 (Goals & Acceptance)](TRACE_SPEC_v1_9.md) — additive, +**Status:** design spec. Refines [Trace Spec §18 (Goals & Acceptance)](TRACE_SPEC_v1_11.md) — additive, backward-compatible. Driven by the concrete goal use case in CodeLogician Desktop (the `declare_goal` tool → per-session active goal → `ponens trace enrich` resolution loop). @@ -35,7 +35,7 @@ This is the formal-methods **"wrong spec / vacuous proof"** problem: proving a t Faithfulness cannot be decided mechanically — whether a formal acceptance faithfully captures an informal intent is the **formalization gap**, and "intent" lives in a human's head. So this spec does not try to *verify* faithfulness. It makes the seam **visible, reviewed by a different principal, -coverage-checked, and hard to retrofit** (evidence rigor is the [governed axis](GOAL_CONTRACT_v0_1.md), +coverage-checked, and hard to retrofit** (evidence rigor is the [governed axis](GOAL_CONTRACT_v0_2.md), not a faithfulness signal) — by separating two questions the current model conflates: | Question | Mechanism | Principal | Status | @@ -52,7 +52,7 @@ The single normative rule of this spec: | Failure | What it looks like | Defense (§ below) | | --- | --- | --- | | **Incomplete** | a clause of the intent has no acceptance item ("3DS *and* 2-approval"; acceptance covers only 3DS → all green, intent unmet) | §5 coverage (`covers` + critic) | -| **Weak evidence** | a `Diff` where a proof was needed ("add 2-approval" backed only by "an edit landed") | the [governed axis](GOAL_CONTRACT_v0_1.md) — a policy, not faithfulness (§6 superseded) | +| **Weak evidence** | a `Diff` where a proof was needed ("add 2-approval" backed only by "an edit landed") | the [governed axis](GOAL_CONTRACT_v0_2.md) — a policy, not faithfulness (§6 superseded) | | **Vacuous** | a `Property` proved but trivially true (holds for *any* implementation) | §5 criteria review + refutation-bite | | **Adjacent** | proves something near but not the intent ("amount ≥ 0" when the user meant "captured ≤ authorized") | §5 criteria approval by the intent's author | | **Retrofitted** | acceptance authored *after* the evidence that resolves it (goalposts moved to match the work) | §7 temporal anchoring + append-only | @@ -140,7 +140,7 @@ means"* — **before** it starts counting, by a principal that is **not the doer > **Superseded (Goal Contract v0.1).** This section originally graded evidence *strength* here and > emitted a `weakly_specified` flag. That overlapped with policy: "is a diff enough, or do you need a -> proof?" is a **rigor** question, and rigor is the [Goal Contract](GOAL_CONTRACT_v0_1.md) **governed +> proof?" is a **rigor** question, and rigor is the [Goal Contract](GOAL_CONTRACT_v0_2.md) **governed > axis** (policies over the goal's cone), not a faithfulness signal. To avoid two mechanisms answering > one question, `faithfulness_of` **no longer computes `weakly_specified`** and `certified` no longer > depends on it. The historical design is kept below for reference. @@ -176,7 +176,7 @@ Acceptance is a claim about intent; intent precedes the work. So: - **met** (unchanged, §18): a goal is *reached* when all `required` items resolve `AcceptDone`. - **right** (new): a goal is *certified* when it carries a `criteria_review` with `verdict = Approved` by a non-doer principal and has **no uncovered `intent_clauses`**. (Evidence strength is no longer a - certification condition — it is the [governed axis](GOAL_CONTRACT_v0_1.md), §6 superseded.) + certification condition — it is the [governed axis](GOAL_CONTRACT_v0_2.md), §6 superseded.) - The two are **orthogonal**: a goal may be met-but-uncertified (green, but the definition was never reviewed) or certified-but-unmet (the right target, work in progress). The desktop should show both axes — never collapse "met" into "done" without "right". diff --git a/spec/ORACLE_SPEC_v0_1.md b/spec/ORACLE_SPEC_v0_1.md new file mode 100644 index 0000000..143e708 --- /dev/null +++ b/spec/ORACLE_SPEC_v0_1.md @@ -0,0 +1,128 @@ +# ORACLE_SPEC v0.1 — Oracles and graded evidence + +**Status:** draft · additive over TRACE_SPEC v1.11 · **Version:** 0.1 + +An **oracle** is an invocable producer of evidence about a target, returning that evidence as +trace artifacts. Crucially, an oracle is **ANY producer of evidence — emphatically not just a formal +tool.** A prover is one kind of oracle; a test run, a static analysis, a runtime monitor, an LLM's +judgment, a data-freshness check, and a human sign-off are *equally* oracles. What unifies them is not +the mechanism but the contract: each returns evidence about a target, tagged with an **honest +strength**. A *reasoner* is simply the formal, proof-producing **subtype**. + +This breadth is the point. It is what lets ponens govern the *full spectrum of how work actually gets +checked* — proof, tests, observation, judgment, attestation — under one trace, and what makes the +substrate tool- and prover-agnostic (ImandraX, Lean, a fuzzer, an LLM judge, a reviewer are all +oracles). The trace model's own language reflects it: every claim records *which oracle produced it, +under what assumptions, and how strong the evidence is*. + +## 1. Classification + +Two orthogonal classifiers travel with every oracle and with the evidence it produces. + +### 1.1 `oracle_type` — the mechanism + +| `oracle_type` | What it is | Examples | +|---|---|---| +| `reasoner` | Formal engines — proof / decision procedures | ImandraX, Lean, Z3, a model checker | +| `tester` | Dynamic execution — run it and observe | test runners, property-based testing, fuzzers, simulators, backtests | +| `analyzer` | Static inspection without execution | type checkers, SAST, linters, schema / contract checks | +| `monitor` | Runtime / observational evidence from a live system or external source | production telemetry, runtime assertions, canaries; **data-freshness / rate-fixing / calendar / rulebook-version checks** | +| `judge` | Heuristic / probabilistic assessment | LLM-as-judge, rubric evaluators, model-graded eval | +| `attestor` | Human or external sign-off | a reviewer, a domain expert, an external certification, a regulator | + +Non-formal oracles are first-class, not an afterthought: a `monitor` that confirms a rate fixing is +today's official value, a `tester` backtest, an `analyzer` schema check, a `judge`'s rubric score, and +an `attestor`'s role-bearing sign-off all produce governed evidence in the same trace as a proof — +each honestly graded (§1.2), never dressed up as stronger than it is. + +### 1.2 `evidence_strength` — the guarantee + +A total order, strongest first. It is the *guarantee the output carries*, distinct from the +mechanism that produced it (a `reasoner` model checker may yield `sat`, not full `proof`). + + proof > sat > tests > static_analysis > attested + +- `proof` — a property holds over the entire (possibly unbounded) state space. +- `sat` — a model/witness was found, or a bounded check passed. +- `tests` — empirical evidence from executed cases (sampled, not exhaustive). +- `static_analysis` — sound-ish over-approximation without execution. +- `attested` — asserted by a heuristic judge or a human; not mechanically established. + +`evidence_strength` is a **new, additive field**; traces and oracles that omit it are treated as +unranked (sorts last). Policies and merge composition MAY require a minimum strength. + +### 1.3 Reasoner-agnostic + +The `reasoner` subtype is deliberately **plural**. The layer is reasoner-agnostic: **ImandraX** +(driven via `codelogician-lite`) is the reference, shipped reasoner oracle, but it is *one of several* +— **Lean**, **Z3**, and other provers / SMT / model checkers register as `reasoner` oracles on equal +footing. Nothing in the trace, the SDK, or a policy is hardwired to a single engine: + +- `verify(target, oracle=…)` selects a reasoner by id; a policy may `require` a specific reasoner (or + a minimum `evidence_strength`); absent that, a configurable default applies (ImandraX out of the box). +- Every result records **which reasoner** produced it, so a claim is attributable and re-checkable by + another party — potentially with a *different* engine. + +This neutrality is a moat, not a hedge: ponens becomes the governance layer *over the whole +formal-verification ecosystem* (and, via §1.1, over non-formal evidence too), rather than a front end +for one prover. Evidence from ImandraX, Lean, a fuzzer, an LLM judge, or a human reviewer all lands in +the same governed, re-checkable trace. + +## 2. The oracle contract + +An oracle exposes metadata and one operation: + +``` +oracle := { + id : String, + name : String, + oracle_type : one of §1.1, + evidence_strength : one of §1.2, # the strength it typically produces + produces : [ArtifactType], + vendor : String?, + description : String?, +} + +invoke(target, context?) -> [artifact] +``` + +`invoke` returns zero or more artifact objects (TRACE_SPEC §7) **without** `artifact_id` or +`producer_action_id` — the caller (e.g. an SDK `Session`) assigns those, records the invoking +`Verify` action, and wires `derived_from` lineage from the target. Each returned artifact SHOULD +carry `evidence_strength` in its payload. + +## 3. Evidence payloads + +`VerificationResult` (and sibling result artifacts) gain an optional `evidence_strength`: + +``` +VerificationResult.payload := { + status : proved | sat | refuted | unknown, + engine : String, + result : String, + reasoning_fingerprint : String?, + evidence_strength : one of §1.2, # NEW + target_symbol : String?, +} +``` + +## 4. Registry + +Oracles are discoverable two ways, kept consistent: +- **Catalog** (reference metadata, remote/gallery) — the `reasoners` registry, whose `kind` maps to + `oracle_type` (`formal_verification`/`smt`/`model_checking` → `reasoner`). +- **Invocable registry** (runtime) — the in-process oracles an SDK can actually call + (`ponens.oracles.register_oracle` / `get_oracle` / `list_oracles`; `ponens oracle list`). + +The registry is expected to hold **many** oracles across all types (§1.1). Shipped today: the +**ImandraX** reasoner (id `codelogician`, via `codelogician-lite`) as the reference implementation. +Planned reference oracles to demonstrate the full spectrum — a second reasoner (e.g. **Lean**), a +`tester` (test runner → `tests`), a `judge` (LLM-as-judge → `attested`), a `monitor` (data-freshness +check), and an `attestor` (human sign-off) — so the registry is visibly reasoner-agnostic and evidence +spans proof → tests → attested, not formal-only. + +## 5. Migration + +`reasoner` remains valid everywhere it is used today (the policy `reasoner` field requires an +oracle whose `oracle_type = reasoner`). New authoring SHOULD prefer the oracle vocabulary. The +`ponens reasoners` catalog command is retained; `ponens oracle` lists the invocable oracles. diff --git a/spec/POLICY_LANGUAGE_v0_2.md b/spec/POLICY_LANGUAGE_v0_2.md index 3889ed9..32c6828 100644 --- a/spec/POLICY_LANGUAGE_v0_2.md +++ b/spec/POLICY_LANGUAGE_v0_2.md @@ -258,5 +258,5 @@ log. See also the [Policy Specification](./POLICY_SPEC_v0_2.md) (the policy object, selectors, and evaluation records) and the -[Trace Specification](./TRACE_SPEC_v1_9.md) (the actions and artifacts these +[Trace Specification](./TRACE_SPEC_v1_11.md) (the actions and artifacts these formulas range over). diff --git a/spec/PRIOR_ART_ALIGNMENT_v0_1.md b/spec/PRIOR_ART_ALIGNMENT_v0_1.md index 49d33e4..c422919 100644 --- a/spec/PRIOR_ART_ALIGNMENT_v0_1.md +++ b/spec/PRIOR_ART_ALIGNMENT_v0_1.md @@ -17,7 +17,7 @@ ponens maintains a **tree/DAG of typed artifacts** (source, formal model, verifi diff, region-decomposition) linked by derivation edges, plus first-class **residuals** (open obligations/assumptions with a lifecycle), **goals & acceptance** resolved from evidence, **policies** (temporal-logic invariants over the trace), and **freshness** (an artifact goes stale when the code it -depends on changes). See [`TRACE_SPEC_v1_9.md`](TRACE_SPEC_v1_9.md) §7 (artifacts/lineage), §13 +depends on changes). See [`TRACE_SPEC_v1_11.md`](TRACE_SPEC_v1_11.md) §7 (artifacts/lineage), §13 (residual surface), §18 (goals & acceptance), and [`POLICY_SPEC_v0_2.md`](POLICY_SPEC_v0_2.md). That combination doesn't exist off-the-shelf. But each *part* of it has strong prior art, and this diff --git a/spec/PROV_INTERCHANGE_v0_1.md b/spec/PROV_INTERCHANGE_v0_1.md index 78653e9..761c005 100644 --- a/spec/PROV_INTERCHANGE_v0_1.md +++ b/spec/PROV_INTERCHANGE_v0_1.md @@ -5,7 +5,7 @@ **Version:** 0.1 **Status:** Draft **Purpose:** Define how a ponens trace projects onto **W3C PROV** so it interoperates with the -provenance-tooling ecosystem. This is a lossy *interchange* view — the trace ([`TRACE_SPEC_v1_9.md`](TRACE_SPEC_v1_9.md)) +provenance-tooling ecosystem. This is a lossy *interchange* view — the trace ([`TRACE_SPEC_v1_11.md`](TRACE_SPEC_v1_11.md)) remains the semantic source of truth; PROV is an export target. Implemented by `ponens trace export --to prov` (PROV-JSON) and `ponens/prov.py`. diff --git a/spec/README.md b/spec/README.md index 1e32a05..0a4f2b7 100644 --- a/spec/README.md +++ b/spec/README.md @@ -9,11 +9,11 @@ pins the current set. | Spec | Version | Status | What it defines | |---|---|---|---| -| [`TRACE_SPEC_v1_9.md`](TRACE_SPEC_v1_9.md) | **1.9** | Draft | **The core.** The typed reasoning-trace format — actions, **meta-actions** (§8.4), artifacts & lineage (§7), the **residual surface** (§13), **goals & acceptance** (§18), reproducibility (§12). Everything else is a companion over this. | +| [`TRACE_SPEC_v1_11.md`](TRACE_SPEC_v1_11.md) | **1.10** | Draft | **The core.** The typed reasoning-trace format — actions, **meta-actions** (§8.4), artifacts & lineage (§7), the **residual surface** (§13), **goals & acceptance** (§18), reproducibility (§12). Everything else is a companion over this. | | [`POLICY_SPEC_v0_2.md`](POLICY_SPEC_v0_2.md) | 0.2 | Draft | **Computable Governance.** The policy object model and the temporal/structural DSL (LTL over finite traces + lineage/residual/field predicates) evaluated over a trace. | | [`POLICY_LANGUAGE_v0_2.md`](POLICY_LANGUAGE_v0_2.md) | 0.2 | Draft | **Operator reference** (reader-friendly companion to `POLICY_SPEC` §9–13). The full operator set — future/past/scoped-past LTLf, boolean connectives, atomic propositions, structural predicates, quantifiers — trace semantics, and the `language_level` fragments. | | [`GOAL_FAITHFULNESS_v0_1.md`](GOAL_FAITHFULNESS_v0_1.md) | 0.1 | Draft | **Definition of done, done right.** Refines TRACE §18 — separates *met* (resolution) from *right* (criteria reviewed by a non-doer), with strength grading, coverage (`covers`), and temporal anchoring against retrofitting. | -| [`GOAL_CONTRACT_v0_1.md`](GOAL_CONTRACT_v0_1.md) | 0.1 | Draft | **Accomplish these things, subject to these policies.** Typed acceptance criteria (component + evidence kind) resolved by artifact **lineage** (not description text — fixes the "goal never ticks" seam), plus goal-scoped **policies** with default layering. Composes *met ∧ governed ∧ certified*. | +| [`GOAL_CONTRACT_v0_2.md`](GOAL_CONTRACT_v0_2.md) | 0.2 | Draft | **Accomplish these things, subject to these policies.** Typed acceptance criteria (component + evidence kind) resolved by artifact **lineage** (not description text — fixes the "goal never ticks" seam), plus goal-scoped **policies** with default layering. Composes *met ∧ governed ∧ certified*. **v0.2** adds a composable property language (`and`/`or`/`not`/`⇒`, `forall`/`exists` over selectors, per-atom `met`/`governed` roles). | | [`REVIEW_CASE_SPEC_v0_2.md`](REVIEW_CASE_SPEC_v0_2.md) | 0.2 | Draft | The reviewer-side object — comments, review items, dispositions, and the verdict over a trace (or a chain). | | [`TRACE_POLICY_REVIEWCASE_SEMANTICS_v0_2.md`](TRACE_POLICY_REVIEWCASE_SEMANTICS_v0_2.md) | 0.2 | Draft | The semantics tying the three together — how policy satisfaction is interpreted over a trace and its review-case context. | | [`REVIEW_HANDOFF_v0_1.md`](REVIEW_HANDOFF_v0_1.md) | 0.1 | Draft | The protocol by which a reviewing agent (or human) consumes a trace — triage the residual surface, re-verify claims, hunt undeclared gaps. | @@ -24,7 +24,9 @@ pins the current set. | [`AUDIT_READINESS_v0_1.md`](AUDIT_READINESS_v0_1.md) | 0.1 | Draft | **Evidence, not attestation.** What makes a trace credible to an auditor/regulator, which credibility axes the specs already deliver (grounded resolution, freshness, defeaters, reproducibility, PROV export, packs, review), and the honest gap-list to "relied upon" — signing/non-repudiation, tool qualification, validated framework mappings, human accountability, claim-scoping. | Also here: [`schema/`](schema/) — JSON Schemas derived from the trace spec (§16, "Interchange -Projection"); [`iml-model/`](iml-model/) — the IML / ImandraX formal model. +Projection"). The IML / ImandraX formal models live in [`../formal/`](../formal/) — the framework's +invariant models plus the layered trace+policy model in +[`../formal/trace-policy-model/`](../formal/trace-policy-model/). ## How they relate diff --git a/spec/SDK_SPEC_v0_1.md b/spec/SDK_SPEC_v0_1.md new file mode 100644 index 0000000..17ec932 --- /dev/null +++ b/spec/SDK_SPEC_v0_1.md @@ -0,0 +1,254 @@ +# SDK_SPEC v0.1 — the ponens developer SDK and oracle model + +**Status:** draft · design frozen for handoff · **Version:** 0.1 +**Companion specs:** `ORACLE_SPEC_v0_1.md` (graded evidence + oracle contract), `TRACE_SPEC_v1_11.md` (wire format), `POLICY_SPEC_v0_2.md`. +**Reference implementation:** branch `denis/ponens-sdk-oracle-slice` (`cli/ponens/sdk.py`, `cli/ponens/oracles.py`, tests `test_sdk.py` / `test_oracles.py`). + +--- + +## 1. Purpose & scope + +The SDK lets a developer build an agent that **speaks ponens natively** — it instruments itself as it +runs and, on exit, produces a validated trace that passes `ponens trace check`. This is the +runtime counterpart to `ponens emit` (which reconstructs a trace from a transcript *after* the fact). + +Strategic role (context, not normative): the SDK is the **bottom-up adoption engine** for the ponens +trace format — "OpenTelemetry for agent reasoning." Ubiquity of the format is the moat for the +independent-verification/utility play; the SDK is the top of the funnel, monetized at the +enterprise/utility layer, not the SDK itself. Keep it open and free. + +### Design principles + +1. **One trace model.** The SDK builds the *same* JSON-native trace dict the rest of `ponens` uses + (`trace.create_empty_trace`, `next_action_id`, `save_trace`, `validate_trace`, `objects.externalize`). + No parallel model, no dialect fork. `emit` (post-hoc) and the SDK (native) share the artifact and + lineage builders. +2. **Thin.** The SDK is a recording layer, not a framework. It appends to the dict; it does not own + control flow. +3. **Singular spec.** The format the SDK emits is exactly the format COGITO's invariants/processes + consume. Bottom-up and top-down converge on one wire format. +4. **Honest evidence.** Evidence carries a *graded* strength and the SDK never overstates it (see §4). + +--- + +## 2. The `Session` API + +A `Session` is a live trace under construction. Recommended use is as a context manager: on clean +exit it stamps an outcome if none was set, validates, externalizes blobs, and writes `path`; on an +exception it marks the run aborted, best-effort saves the partial trace, and never masks the error. + +```python +from ponens.sdk import Session + +with Session(model="claude-opus", assistant="my-agent", path="trace.json", + intent="prove charge() is idempotent") as s: + a = s.action("EditFile", label="edit pricing.py", rationale="route retries via an idempotency key", + evidence=[{"type": "FileRef", "ref": "pricing.py"}]) + m = s.artifact("IMLModel", name="pricing.iml", content=iml_src, format="iml", + producer_action_id=a) + s.verify({"iml_code": iml_src, "goal": "idempotent charge", "target_symbol": "charge"}, + oracle="codelogician", derived_from=m) + s.residual("assumption", "gateway is at-least-once", suggested_check="model duplicate delivery") +``` + +### Constructor + +``` +Session(model="example-model", assistant="ponens", path=None, intent=None, trigger=None) +``` +- `path` — where `save()` / context-exit writes. If omitted, build in memory and `save(path)` explicitly. +- `intent` / `trigger` — sets `trigger = {type: "TaskReceived", text: …}`; `intent` also opens a goal. + +### Recording primitives + +| Method | Returns | Effect | +|---|---|---| +| `action(type, label=, rationale=, detail=, category="activity", inputs=, outputs=, evidence=)` | `int` (action id) | Appends an action; auto-assigns the id. | +| `artifact(artifact_type, name=, payload=, derived_from=, producer_action_id=, content=, format=, role=)` | `str` (artifact id) | Appends a typed artifact; `content` is content-addressed into the object store as `content_ref`; wires the producing action's `outputs`. | +| `goal(intent, scope=, acceptance=)` | `str` (goal id) | Declares a goal (intent + optional scope/acceptance). | +| `residual(kind, statement, severity="medium", status="open", suggested_check=, derived_from=)` | `str` | Declares negative space as a `Residual` artifact. | +| `verify(target, oracle, derived_from=, label=, rationale=)` | `list[str]` | Invokes an oracle and records a `Verify` action + the evidence artifact(s), wiring lineage. See §3. | +| `outcome(type="ProcessCompleted", summary=)` | — | Stamps the terminal event. | + +### Lifecycle + +| Method | Behavior | +|---|---| +| `validate()` | Returns `(errors, warnings)` from `trace.validate_trace`. | +| `save(path=None, strict=True)` | Externalizes blobs; with `strict`, structural errors raise; writes the trace. | +| `__enter__` / `__exit__` | On success: stamp `ProcessCompleted` if unset, `save()` if `path` given. On exception: stamp `ProcessAborted(summary=str(exc))`, best-effort `save(strict=False)`, **re-raise** (never swallow, never mask). | + +--- + +## 3. Oracles and `verify()` + +`verify(target, oracle, …)`: +1. Resolves `oracle` — an oracle id (from the registry, §4.4) or an `Oracle` instance. +2. Records a `Verify` action (`category="reasoning"`). +3. Calls `oracle.invoke(target)`, appends each returned artifact with `producer_action_id` = the + Verify action and `derived_from` = the target lineage, and returns the new artifact ids. + +`target` is oracle-specific; for the CodeLogician oracle it is `{iml_code, goal?, target_symbol?}`. + +Unknown oracle id raises `ValueError`. + +--- + +## 4. The oracle model (see ORACLE_SPEC v0.1) + +An **oracle** is an invocable evidence producer. A **reasoner** is the formal, proof-producing +*subtype* of oracle. Two orthogonal classifiers travel with each oracle and its evidence: + +### 4.1 `oracle_type` (mechanism) +`reasoner | tester | analyzer | judge | attestor` — provers, test runners, static analysis, +LLM-judges, human attestation. + +### 4.2 `evidence_strength` (guarantee), strongest first +``` +proof > sat > tests > static_analysis > attested +``` +`strength_rank(s)` ranks a strength (0 = strongest; unknown sorts last), so a policy can require a +minimum and a merge can prefer stronger evidence. + +### 4.3 The `Oracle` contract +``` +class Oracle: + id: str + name: str + oracle_type: str # §4.1 + evidence_strength: str # §4.2 — the strength it is capable of + produces: tuple[str, ...] # artifact types + vendor: str; description: str + def invoke(self, target, context=None) -> list[artifact_dict]: ... + def as_dict(self) -> dict +``` +`invoke` returns artifact dicts **without** `artifact_id` / `producer_action_id` (the SDK assigns +those). Each artifact's payload SHOULD carry the *actual* `evidence_strength` of the result. + +### 4.4 Registries +- **Invocable (runtime):** in-process — `register_oracle`, `get_oracle`, `list_oracles`; surfaced by + `ponens oracle list|show`. These are the oracles an SDK `Session` can actually call. +- **Catalog (reference):** the `reasoners` gallery (`reasoners.py`, `PONENS_REASONER_URL`), retained; + its `kind` maps to `oracle_type` via `oracle_type_for_kind` (all current entries → `reasoner`). + +### 4.5 Honesty rule +`evidence_strength` in a result reflects the **actual verdict**, not the oracle's capability: +`proved`/`refuted` → `proof`, bounded → `sat`, otherwise the result carries **no** strength (an +`unknown`/error result never masquerades as graded evidence). + +--- + +## 5. The CodeLogician oracle (oracle #1) + +`CodeLogicianOracle` (`id="codelogician"`, `oracle_type="reasoner"`, `evidence_strength="proof"`, +`vendor="Imandra"`) drives Imandra's **`codelogician-lite`** CLI (the LLM-friendly front end to the +ImandraX engine) — **not** the raw engine. The runner is dependency-injectable (tests / CLI-less +environments pass a fake). + +### 5.1 Invocation +``` +codelogician-lite check-vg .iml --json +``` +Binary resolution: env `CODELOGICIAN_CLI`, then `codelogician-lite` on `PATH`. + +### 5.2 `check-vg --json` schema (ground truth) +```json +{ + "eval_res": "Success", // admit: "Success" | {success: bool, errors:[…]} + "diags": [], + "vg_res_list": [ + { "vg_req_index": 0, "kind": "verify", "src": "fun x -> f x > x", + "vg_res": { "proved": {"proof_pp": "…"}, "refuted": null, + "verified_upto": null, "unknown": null, "err": null, "errors": [] } } + ] +} +``` + +### 5.3 Verdict mapping +Per goal (`_verdict_of`): `refuted` (non-null) → refuted; else `proved` → proved; else +`verified_upto` → sat; else unknown. Counterexample extracted from `refuted.model_str|model|src`. +Aggregate (`_aggregate`): any `refuted` → refuted; all `proved` → proved; all `proved|sat` → sat; +else unknown. Admit failure (`eval_res` not success) → unknown. + +### 5.4 Produced artifact +`VerificationResult` with payload `{status, engine:"imandrax", result, reasoning_fingerprint, +evidence_strength?, counterexample?, target_symbol?}`; `artifact_role` = `CounterexampleRole` when +refuted, else `ProofRole`. + +--- + +## 6. CLI surface + +- **Now:** `ponens oracle list|show` — the invocable oracles (id, name, oracle_type, + evidence_strength, produces). `ponens reasoners …` (catalog) retained. +- **Planned:** `ponens verify --oracle --target …` — surface `Session.verify` from the + command line. + +--- + +## 7. CodeLogician as the first consumer + +The SDK should be **extracted from** the CodeLogician agent (imandra-pi-agent), not bolted on — that +agent already speaks ponens (records verify/decompose/testgen artifacts, policy eval, goals/trace). +CodeLogician is the dogfood *and* the strongest demo (its oracle is proof-strength). + +**Language boundary:** CodeLogician is TypeScript/Node; the SDK is Python-first. +- **Near-term:** integrate via the `codelogician-lite` / `ponens` **CLI/subprocess** (already the + pattern for policy checks). +- **Native:** requires a **TypeScript SDK** — CodeLogician is the forcing function that raises TS-SDK + priority. Migrate incrementally (parallel path → parity → cut over); do not destabilize the shipping agent. + +--- + +## 8. Roadmap (phased) + +| Phase | Content | Status | +|---|---|---| +| **0** | Oracle contract + `evidence_strength` + `oracle_type` (ORACLE_SPEC v0.1); schema bump | **implemented** (spec) | +| **1** | Thin runtime SDK (`Session`) | **implemented** | +| **2** | Oracle interface + registry + CodeLogician oracle (proof) | **implemented**; more reference oracles pending | +| 3 | `ponens init` scaffolding / codegen (instrumented agent template, `.ponens/`, CI gate) | planned | +| 4 | Framework adapters — MCP server, LangChain/CrewAI callback | planned | +| 4.5 | **TypeScript SDK** (bumped up — CodeLogician is TS) | planned | +| 5 | Hosting / PLG — hosted traces, org policy, grading service, public oracle marketplace | **deferred** (= COGITO/utility; don't split focus) | + +### Recommended next increments +1. `ponens verify` CLI verb (surface `Session.verify`). +2. **Prove reasoner-agnosticism:** a second *reasoner* oracle (e.g. **Lean**) alongside ImandraX, so + `verify` / policies can pick the engine and a claim records which one produced it (ORACLE_SPEC §1.3). +3. **Span the evidence spectrum (oracles ≠ formal-only):** non-formal reference oracles — a `tester` + (test runner → `tests`), a `judge` (LLM-as-judge → `attested`), a `monitor` (data-freshness check), + an `attestor` (human sign-off) — so the registry visibly covers proof → tests → attested. +4. CodeLogician integration via subprocess (the extract-from step). +5. Full `reasoners → oracles` rename with deprecation aliases (currently additive; both coexist). + +--- + +## 9. Naming & migration + +`reasoner` remains valid everywhere it is used today (the policy `reasoner` field requires an oracle +whose `oracle_type = reasoner`). New authoring prefers the oracle vocabulary. Full rename +(`reasoners.py` → `oracles.py`, `ponens reasoners` → `ponens oracle`, `PONENS_REASONER_URL` → +`PONENS_ORACLE_URL`, cache dir) should ship with deprecation aliases — do it **before** the SDK/registry +reach wide adoption. Currently the two coexist (additive). + +--- + +## 10. Open decisions + +- **Lock the `evidence_strength` taxonomy** (§4.2) — it propagates into policies, merge, and payloads. +- **Oracle trust/sandboxing** — fine for local dev; the *public* registry needs curation (a bad + oracle = false assurance). The "curated trust layer" is a differentiator. +- **`oracle_type` vs `evidence_strength`** — kept as two fields (mechanism vs guarantee); could + collapse to strength alone, but type is the browse/filter axis for the registry. +- **TS SDK timing** — gated by CodeLogician's native-integration need. + +--- + +## 11. Test / run notes + +- Run tests with a pytest-capable interpreter from `cli/` (e.g. `~/miniconda3/bin/python3 -m pytest + tests/unit/`). The uv-tool `ponens` env lacks pytest; `ponens` imports resolve when run from `cli/`. +- The reference-implementation slice: full unit suite green (557 passed / 1 skipped at freeze), plus + `test_sdk.py` + `test_oracles.py`. E2e: an SDK-built trace grades cleanly via `ponens trace grade` + (Structure/Lineage 100%, proof evidence recorded). diff --git a/spec/TRACE_SPEC_v1_9.md b/spec/TRACE_SPEC_v1_11.md similarity index 81% rename from spec/TRACE_SPEC_v1_9.md rename to spec/TRACE_SPEC_v1_11.md index 635330b..3e921ea 100644 --- a/spec/TRACE_SPEC_v1_9.md +++ b/spec/TRACE_SPEC_v1_11.md @@ -2,11 +2,15 @@ ## Version -**Version:** 1.9 +**Version:** 1.11 **Status:** Draft **Format:** Canonical typed specification with JSON/Pydantic projection notes **Positioning:** Reasoner-agnostic trace specification, with IML / ImandraX as one concrete instantiation +> **Changes in 1.11 (additive, backward-compatible).** Specifies **integrity and cryptographic signatures** (§12.4) - the fields the sync/sign-off layer writes onto a trace, previously defined only in `CLI_SYNC_MODEL_v0_1.md` and `AUDIT_READINESS_v0_1.md`. Adds two top-level fields (§5): a **`content_hash`** (sha256 over the canonical trace, *excluding* transport/binding metadata and signatures - the `HASH_EXCLUDE` set) and a **`signatures`** list of cryptographic sign-offs *over* that `content_hash`. A **`signature`** (§12.4) records the `signer`, the `content_hash` it covers, the `algo` (**`ssh`** | **`gpg`** | **`sigstore`**), the backend-specific `signature` material, and optional `role`/`disposition` (what the party is attesting) and an RFC-3161 trusted **`timestamp`** (a TSA-attested "existed by *t*", not a machine-clock claim). Because `signatures` is excluded from `content_hash`, multiple parties **co-sign the same content** with whatever backend they trust; verification yields a uniform verdict (**`valid` | `untrusted` | `invalid` | `tampered`**). All additive: a trace may carry neither field, so existing 1.4-1.10 traces remain valid and unchanged. Also additive in 1.11: an **`acceptance_item`** (§18.1) MAY carry a composable **`formula`** — the goal *property language* (`and` / `or` / `not` / `⇒` and `forall` / `exists` over component selectors, with per-atom `met` / `governed` roles). A single-criterion item is the atomic case and resolves exactly as before; grammar and status-lattice semantics are in `GOAL_CONTRACT_v0_2` §9. + +> **Changes in 1.10 (additive, backward-compatible).** Adds **trace composition** - the sound combination of two traces across a merge (§15.3). A `merge` operation combines a `base`, an *ours*, and a *theirs* trace into a merged trace recording a two-parent **`merge_event`** provenance; for every carried-over reasoning result it emits either a **`CarriedForward`** artifact (the result is *provably unaffected* - its dependency closure is disjoint from the merge's change set, or every touched dependency was assumed `uninterpreted`) or a **`NeedsRereasoning`** residual (its closure or an assumed contract was disturbed), under a **totality** invariant: every prior result lands in exactly one bucket. A **`CoverageRegression`** residual records a goal whose scope gained an unproven member. Adds a **`component_id`** field (§7.1): a durable identity for a code component, stable across rename/move, so evidence-to-code binding (rooting, freshness, and the merge change-set) survives a rename. All additive: a trace without these carries none of them; `NeedsRereasoning` / `CoverageRegression` / `CarriedForward` / `component_id` are optional, so existing 1.4-1.9 traces remain valid and unchanged. + > **Changes in 1.9 (additive, backward-compatible).** Makes **evidence freshness sound**, for *every* formal-reasoning result (§18.3). Any reasoning result — `VerificationResult`, `StateSpaceAnalysisResult`, `ConformanceResult`, `CoSimulationResult` — may now carry a **`reasoning_fingerprint`** (§10.4a): a checksum (and optional structural *shape*) of the **task it was computed over** (the target symbol **plus its dependency closure in the model**, not just the target's own text), together with the `engine` and `engine_version` that produced it. Freshness becomes a **derived** verdict — `Fresh | Stale | Detached` (§18.3) — obtained by recomputing the current fingerprint and comparing: an exact checksum match is `Fresh`; a mismatch (or an advanced engine version) is `Stale`; a result whose target no longer exists in the current model is `Detached` (orphaned work — kept for audit and recovery, never counted as evidence). This replaces the 1.7 heuristic ("the target symbol was edited at a later action"), which both **missed** staleness (a result invalidated by a change to a *dependency* rather than the target itself read as fresh) and **over-reported** it (a comment/format edit that left the task unchanged read as stale). The fingerprint is **optional** on every result kind: a result without one falls back to the 1.7 action-ordering heuristic, so existing 1.5–1.8 traces remain valid and unchanged. > **Also in 1.9 (additive, backward-compatible).** Adds **counter-evidence** to the residual @@ -210,9 +214,13 @@ type trace = ; trace_lineage : trace_lineage option ; files_modified : string list ; metrics : metrics option + ; content_hash : string option (* sha256 over the canonical trace, excluding HASH_EXCLUDE — §12.4; CLI_SYNC_MODEL §5.3 *) + ; signatures : signature list (* cryptographic sign-offs over content_hash — §12.4 *) } ``` +`content_hash` is the trace's **content digest** and `signatures` its **cryptographic sign-offs** (§12.4). Both are additive: a trace that has not been hashed or signed carries `content_hash = None` and `signatures = []`. Transport/binding fields (`repo`, `branch`, `commit_sha`) may also appear at the top level; like `content_hash` and `signatures` they are **excluded from the content hash** (the `HASH_EXCLUDE` set, §12.4) and their semantics belong to the sync layer (`CLI_SYNC_MODEL_v0_1.md`). + `residuals` is the legacy carrier for the **residual surface** — a trace's declared negative space (§13). As of 1.8 a residual is a first-class **artifact** (`artifact_type` `Residual`); this field is retained only so pre-1.8 traces stay readable and canonicalizes to the empty list. `goals` is the trace's **goals & acceptance** — its declared intent and definition of done (§18). It canonicalizes to the empty list. @@ -288,6 +296,9 @@ type artifact_common = ; supersedes : string option ; content_ref : string option ; summary : string option + ; component_id : string option (* durable identity of the code component this artifact is about, + stable across rename/move (§15.3); distinct from artifact_id + (which identifies the RECORD, not the code element) *) ; metadata : artifact_metadata option } ``` @@ -333,6 +344,7 @@ type artifact = | UserApprovalArtifact of artifact_common | CommitArtifact of artifact_common | ReproductionBundleArtifact of artifact_common * reproduction_bundle_payload + | CarriedForwardArtifact of artifact_common * carried_forward_payload (* §15.3 *) ``` ## 7.2 Why strict artifacts @@ -1031,6 +1043,83 @@ type execution_environment = Consequential reasoning outcomes should either be reproducible directly or linked to a reproducible downstream validation step. +## 12.4 Integrity, content hash, and signatures + +Reproducibility answers *can this trace be re-derived?* Integrity answers two further questions an auditor asks: *has this trace been altered since it was produced?* and *who stands behind it?* The trace layer answers both with a content hash and cryptographic signatures over it. (The end-to-end audit ethos is `AUDIT_READINESS_v0_1.md`; the sync/binding verbs that compute and move the hash are `CLI_SYNC_MODEL_v0_1.md` §5.3.) + +### Content hash + +`content_hash` is `sha256` over a canonical serialization of the trace with a fixed set of fields excluded — the **`HASH_EXCLUDE`** set: `timestamp`, `content_hash` itself, the binding metadata `repo` / `branch` / `commit_sha`, and `signatures`. These are excluded because they are *transport/binding* metadata, not reasoning content: the hash must be stable under binding to a commit and, crucially, under **appending a signature** — so that signing the content does not invalidate the very hash the signature is over. + +```ocaml +(* HASH_EXCLUDE = { timestamp; content_hash; repo; branch; commit_sha; signatures } *) +content_hash = sha256 (canonical { trace without HASH_EXCLUDE fields }) +``` + +### Signatures + +A **signature** is a sign-off by a party over the trace's `content_hash`. Because the signature is over the content digest, any later edit to reasoning content breaks it (**tamper-evidence**); because it is made with the signer's private key or identity, it names **who** signed (**non-repudiation**). Signatures live in the `signatures` list, which is in `HASH_EXCLUDE`, so several parties — the producer, a reviewer, an independent auditor — **co-sign the same content**, each with whatever backend they trust. + +```ocaml +type signature = + { signer : string (* human-facing identity: ssh comment / gpg uid / sigstore OIDC identity *) + ; content_hash : string (* the sha256 digest this signature was made over *) + ; algo : string (* "ssh" | "gpg" | "sigstore" — verification dispatches on this *) + ; signed_at : string (* ISO-8601 wall-clock time the signer asserts *) + ; signature : string (* backend material: armored ssh sig / armored gpg detached sig / sigstore bundle JSON *) + ; key_type : string option (* e.g. "ssh-ed25519" | "gpg" | "sigstore" *) + ; key_id : string option (* ssh key fingerprint / gpg fingerprint / None for sigstore *) + ; public_key : string option (* ssh public-key line / inlined gpg public key / absent for sigstore *) + ; namespace : string option (* ssh only: the ssh-keygen signing namespace *) + ; bundle : string option (* sigstore only: the verification bundle JSON *) + ; oidc_issuer : string option (* sigstore only: the expected OIDC issuer *) + ; transparency_log : string option (* sigstore only: "rekor" *) + ; role : string option (* the signer's role, e.g. "auditor", "reviewer" *) + ; disposition : string option (* the sign-off, e.g. "approved", "rejected" *) + ; timestamp : rfc3161_timestamp option (* RFC-3161 trusted timestamp over `signature` *) + } + +type rfc3161_timestamp = + { standard : string (* "rfc3161" *) + ; tsa : string (* the Time-Stamping Authority URL *) + ; hash_alg : string (* "sha256" *) + ; message_imprint : string (* sha256 of the signature bytes *) + ; token : string (* base64 DER TSA response token *) + ; time : string option (* the TSA-attested time, parsed from the token *) + } +``` + +**Backends.** The `algo` selects one of three interchangeable backends, each with its own trust model, sharing one verification interface: + +- **`ssh`** — OpenSSH signatures (`ssh-keygen -Y sign|verify`). No new dependencies, reuses existing keys, verifies fully **offline**. Trust: the key is in an **allowed-signers roster** (git's model). +- **`gpg`** — GnuPG detached signatures. The signer's `public_key` is inlined on the record so verification is **offline** against an ephemeral keyring. Trust: the key fingerprint (`key_id`) is in a **gpg fingerprint roster**. +- **`sigstore`** — keyless, identity-bound signing. A short-lived Fulcio certificate binds the signature to an **OIDC identity** (`signer` + `oidc_issuer`) and the proof is recorded in the **Rekor** public transparency log (`transparency_log = "rekor"`). Trust: the certificate identity matches the expected `--identity` / `--oidc-issuer`; there is no long-lived key to manage or leak. + +**Sign-off semantics.** `role` and `disposition` make a signature an *attestation*, not merely a countersignature: they record **what** the party is claiming (e.g. `role = "auditor"`, `disposition = "approved"`), connecting a signature to the review verdict (§14.3). Where `content_hash` fixes *what* was signed and the key fixes *who*, the optional RFC-3161 `timestamp` fixes *when*: a Time-Stamping Authority countersigns the `signature`, giving a TSA-attested "existed by *t*" rather than a machine-clock assertion (`signed_at`). + +**Verification.** For each signature, verification dispatches on `algo` and yields a uniform status. A separate check confirms the trace's current `content_hash` still matches the digest the signature covers. + +```ocaml +type signature_status = + | Valid (* good signature from a signer trusted under the backend's model *) + | Untrusted (* cryptographically good, but the signer is not in the roster / expected identity *) + | Invalid (* the cryptographic check failed *) + | Tampered (* the trace's content_hash no longer matches the digest the signature covers *) + +type signature_verdict = + { signer : string + ; key_id : string option + ; algo : string + ; role : string option + ; disposition : string option + ; status : signature_status + ; detail : string + ; timestamp : timestamp_verdict option (* Valid | Untrusted | Invalid | Unknown over the RFC-3161 token *) + } +``` + +A verifier may **gate on failure** (treat anything other than `Valid` as a hard error), which is how an autonomous pipeline enforces "no unsigned or untrusted trace advances." A signature is the cryptographic complement of a review sign-off (§14.3): where a review item records a disposition *inside* the trace, a signature binds a role-bearing disposition to the exact content it vouches for and to an attestable time, verifiable by a party other than the one that produced the trace. + --- # 13. Residual Surface @@ -1058,6 +1147,11 @@ type residual_kind = | OpenQuestion (* a decision deferred to a reviewer or human *) | Defeater (* counter-evidence AGAINST a claim (not a gap): a reason to believe a stated result is wrong. Carries a `defeater_kind`; anchors to the claim it contests. *) + | NeedsRereasoning (* an established result whose evidence a trace MERGE disturbed - a dependency in + its closure changed, or an assumed contract was invalidated: re-establish it + against the merged code (§15.3) *) + | CoverageRegression (* a goal whose scope gained an unproven member after a merge - the obligation is + no longer fully covered even though no existing result changed (§15.3) *) (* What a Defeater attacks (Pollock / SEI Eliminative Argumentation taxonomy). *) type defeater_kind = @@ -1355,6 +1449,65 @@ type trace_lineage = Traces are immutable; iteration is represented by linked successor traces. +## 15.3 Trace composition (merge) + +A **merge** combines two lines of reasoning - the everyday case being a `git merge`/`pull` that brings +another branch's code, the general case being two independently-produced traces (a hub, multi-agent, or +multi-domain setting). A merge is the point at which two **individually-valid** results can become +**jointly invalid**: a result proved against one branch may depend, transitively, on a definition the +other branch changed, with no textual conflict and no rule broken. Composition is therefore defined to +**carry forward only the provably-unaffected** and flag the rest for re-establishment - it never asserts a +carried result is still valid without a warrant. + +### Canonical model + +```ocaml +type merge_event = + { parents : string list (* the source trace ids being combined (ours, theirs) *) + ; base : string option (* the common-ancestor trace id, for a three-way combine *) + ; kind : string (* "merge" | "rebase" | "cherry-pick" | "squash" *) + } +(* Recorded on the merged trace as `merge : merge_event`. The two-parent link is provenance kept OFF the + artifact lineage DAG, so §7.3 revisioning and lineage acyclicity (a `derived_from` points only at an + EARLIER artifact) are preserved. *) + +type carried_forward_basis = + | ClosureDisjoint (* the result's dependency closure did not intersect the merge's change set *) + | UninterpretedOpaque (* every changed dependency it touched was assumed `uninterpreted` - the result + holds for ALL values of that dependency, so a change to it cannot invalidate it *) + +type carried_forward_payload = + { result_id : string (* the carried-over reasoning result *) + ; basis : carried_forward_basis + ; closure : string list (* the component ids checked - the falsifiable witness *) + ; via_assumptions : string list (* for UninterpretedOpaque: the assumptions relied upon *) + } +``` + +A `CarriedForward` is the **positive dual of a residual**: where a residual (§13) records negative space, +a `CarriedForward` records a claim that was *deliberately not re-checked because it is provably safe* - +independently re-verifiable by recomputing the closure/change-set intersection. So a merged trace's +account of each prior result is one of three: **carried forward** (`CarriedForward`), **must re-reason** +(`NeedsRereasoning`, §13), or already re-reasoned during the merge. + +### Affected set + +Whether a result is carried or re-reasoned is decided by its **dependency closure** (§10.4a) intersected +with the merge's **change set** - the components that differ, matched by `component_id` (§7.1) so a rename +is recognized as one component, not a delete plus an add. A result is carried forward when the +intersection is empty (`ClosureDisjoint`), or when every intersecting dependency was assumed +`uninterpreted` (`UninterpretedOpaque`); otherwise it is flagged `NeedsRereasoning`. A goal whose scope +gains an unproven component yields a `CoverageRegression`. The soundness obligation is **closure +completeness**: a skip is only as sound as the closure is complete, so an omitted or ambiguously-matched +dependency is conservatively treated as changed (re-reasoned), never silently carried. + +### Totality + +For every reasoning result carried from a parent trace, the merged trace contains **exactly one** of: a +`CarriedForward` artifact, a `NeedsRereasoning` residual, or a freshly re-established result. This is a +checkable invariant - it makes "we only re-reasoned the parts the merge affected" auditable rather than +assumed, and lets a policy (§13.5) refuse a merged trace that silently drops a prior result. + --- # 16. Interchange Projection Notes @@ -1521,6 +1674,13 @@ type acceptance_item = ; label : string (* what this criterion means, in plain language *) ; binding : acceptance_binding option (* how it resolves; if absent, `status` is manual *) ; status : acceptance_status option (* authored fallback when unbound or unresolved *) + ; formula : json option (* composable acceptance (v1.11, additive): a formula tree over + atomic criteria — and / or / not / implies / forall / exists, + with per-atom `met` | `governed` roles and component selectors + (glob / module / scope / tag). When present it drives + resolution and `binding` / `status` are the atomic fallback; + absent ⇒ today's single-criterion item, unchanged. Grammar and + status-lattice semantics: GOAL_CONTRACT_v0_2 §9. *) } type goal_status = diff --git a/spec/schema/README.md b/spec/schema/README.md index 60e46be..1039a7a 100644 --- a/spec/schema/README.md +++ b/spec/schema/README.md @@ -9,7 +9,7 @@ trace.v1_1/ schema.json + examples/ trace.v1_4/ schema.json + schema.iml + concretize.iml + concrete_schema.iml + Makefile ``` -The canonical prose specs live one level up in [`../`](..) (`TRACE_SPEC_v1_9.md` etc.); +The canonical prose specs live one level up in [`../`](..) (`TRACE_SPEC_v1_11.md` etc.); these are the derived schemas (see Trace Spec §16, "Interchange Projection"). Provenance: imported from the `imandra-ai/reasoning-policies` repository.