Release v1.8.0 — content-addressed object store, replay, revision-aware lineage

CHANGELOG.md

@@ -7,6 +7,34 @@ This file is the single source for release news: `make release` turns the matchi
 GitHub release notes, and the website's **/whats-new** page renders this file directly. Keep a
 `## [x.y.z]` heading per version, with `### Added` / `### Changed` / `### Fixed` subsections.
 
+## [1.8.0] — 2026-08-04
+
+### Added
+- **Content-addressed object store (`ponens objects`)** — an immutable, sha256-keyed blob store so a
+  trace can reference large content (source, formal model, tests) by `content_ref` instead of inlining
+  it: identical content is stored once (dedup) and a trace plus its reachable objects is a portable,
+  self-contained bundle. Layout is a stable spec (`<dir>/sha256/<ab>/<rest>`, overridable via
+  `$PONENS_OBJECTS_DIR`) so any producer that can hash may write blobs directly. New CLI:
+  `ponens objects put | get | externalize | inline | gc | stat`. `ponens bind --externalize` moves
+  inline blobs into the store at the share boundary; `objects inline` rehydrates a received bundle.
+- **`ponens trace replay` — re-run a ReproductionBundle.** Materializes the content-addressed model
+  from the object store and re-executes it through a pluggable **engine adapter** (`engines.py`, with an
+  ImandraX adapter), flagging where the fresh verdict **diverges** from the recorded one. Dry by default
+  (reports the plan + self-containment); `--run` executes the safe-allowlisted replay command and
+  preflights the engine (binary on PATH, credentials present).
+- **Revision-aware lineage (`supersedes` / `revision`).** Helpers for append-only revision chains:
+  `current_artifacts` (fold history to the latest revision), `superseded_ids`, and `revision_chain`
+  (walk a revision newest→oldest, cycle-safe). `trace validate` now warns on a dangling `supersedes`.
+
+### Changed
+- **`normalize_trace` surfaces failed/aborted attempts and resolves externalized blobs.** A
+  `CommandResult` (carrying an `outcome`/`exit_code`) is mapped onto its action so policies can
+  distinguish *attempted-and-failed* from *never-attempted*; externalized `content_ref` blobs are
+  resolved back to inline content for policy evaluation on a bound trace.
+- **Residual payload preserves `summary` / `property` / `counterexample`.** The plain-language lead, the
+  formal property that was checked, and a counterexample input now survive residual processing
+  (Trace Spec v1.8 §13), instead of being dropped by the residual-surface filter.
+
 ## [1.7.1] — 2026-07-29
 
 ### Added

cli/ponens/cli.py

@@ -18,6 +18,7 @@
 from . import otel as otel_mod
 from . import langfuse as langfuse_mod
 from . import sync as sync_mod
+from . import objects as objects_mod
 from . import emit as emit_mod
 from . import agent as agent_mod
 from . import reasoners as reasoners_mod
@@ -669,6 +670,8 @@ def build_parser():
     # ── git/hub sync (bind, push, pull, status) ──────────────────
     sync_mod.register(subparsers)
 
+    objects_mod.register(subparsers)
+
     # ── emit (derive a trace from an agent session transcript) ───
     emit_mod.register(subparsers)
 

cli/ponens/engines.py

@@ -0,0 +1,73 @@
+"""Engine adapters for reproduction replay (Gap 4).
+
+A ReproductionBundle names an ``execution_environment``; an engine adapter turns that environment into
+a concrete, safe replay command and PREFLIGHTS whether the engine is actually runnable here (binary on
+PATH, credentials present). Pluggable — a new engine (Lean, Z3, …) is one adapter — with a graceful
+fallback to the environment's own ``configuration.replay_command`` when no adapter matches.
+
+Keeping the engine specifics HERE (not in the replay loop) is the framework/consumer half of Gap 4:
+ponens owns replay execution; ImandraX is just one adapter.
+"""
+import os
+import shutil
+
+
+class EngineAdapter:
+    """Base adapter. Subclasses match an environment, supply a replay command (with a ``{model}``
+    placeholder replay substitutes), and preflight the local environment."""
+
+    name = "generic"
+
+    def matches(self, env) -> bool:
+        return False
+
+    def replay_command(self, env):
+        return ((env or {}).get("configuration") or {}).get("replay_command")
+
+    def preflight(self):
+        """Return None if the engine can run here, else a short human reason it cannot."""
+        return None
+
+
+class ImandraXAdapter(EngineAdapter):
+    """ImandraX, reached over the Imandra Universe API via ``codelogician-lite`` (a read-only check)."""
+
+    name = "imandrax"
+    BINARY = "codelogician-lite"
+
+    def matches(self, env) -> bool:
+        env = env or {}
+        if env.get("environment_id") == "env-imandrax":
+            return True
+        name = (env.get("name") or "").lower()
+        comps = " ".join((c or {}).get("name", "") for c in env.get("components", []) or []).lower()
+        return "imandra" in name or "imandra" in comps
+
+    def replay_command(self, env):
+        # Honor an explicit recipe if the trace carries one; otherwise the canonical check command.
+        return super().replay_command(env) or f"{self.BINARY} check --with-vgs {{model}}"
+
+    def preflight(self):
+        if not shutil.which(self.BINARY):
+            return f"{self.BINARY} not on PATH"
+        if not (os.environ.get("IMANDRA_UNI_KEY") or os.environ.get("IMANDRAX_API_KEY")):
+            return "no Imandra API key (set IMANDRA_UNI_KEY)"
+        return None
+
+
+# Registry — first match wins; register_adapter prepends (tests / a host app override it).
+_ADAPTERS = [ImandraXAdapter()]
+
+
+def register_adapter(adapter):
+    _ADAPTERS.insert(0, adapter)
+
+
+def adapter_for(env):
+    for a in _ADAPTERS:
+        try:
+            if a.matches(env or {}):
+                return a
+        except Exception:  # noqa: BLE001 — a broken adapter must not abort replay
+            continue
+    return None

cli/ponens/lineage.py

@@ -133,6 +133,9 @@ def provenance(artifact_id, trace):
 _RESIDUAL_PAYLOAD_KEYS = (
     "kind", "severity", "status", "source", "statement", "target",
     "related_artifact_ids", "suggested_check", "introduced_by_action_id", "tags", "derived",
+    # Plain-language lead (`summary`) shown first by viewers, with the formal IML kept as detail —
+    # the `property` that was checked and a `counterexample` input that breaks it (§13).
+    "summary", "property", "counterexample",
 )