Denis/aug26

.gitignore

@@ -28,6 +28,9 @@ viewer/vscode-plugin/media/demo-traces/
 # Local registry cache
 .ponens/
 
+# Local IML scratch written by the Imandra tooling when it translates a source file
+.imandra/
+
 # Visualizer asset copied into the CLI package at build time (source: viewer/vscode-plugin/media/)
 cli/ponens/visualizer.html
 

CHANGELOG.md

@@ -7,6 +7,78 @@ 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.11.0] — 2026-08-26
+
+The package jumps `1.9.1` → `1.11.0` to track the trace spec, which advanced two minor versions
+(**1.10** trace composition, **1.11** signatures + composable acceptance) — there was no `1.10.0`
+package release. `TRACE_SPEC_v1_9.md` is now `TRACE_SPEC_v1_11.md`; every change below is additive,
+so existing 1.4–1.9 traces stay valid and unchanged.
+
+### Added
+- **Composable acceptance — the goal property language (`GOAL_CONTRACT_v0_2` §9, Trace Spec 1.11
+  §18.1).** An `acceptance_item` MAY now carry a `formula` instead of a single criterion: `and` / `or` /
+  `not` / `implies` over atoms, plus **`forall`** / **`exists`** quantified over *component selectors*
+  (glob, module, scope, tag) — so "every handler in `payments/` is proved, and at least one has a
+  conformance check" is one criterion, not a hand-maintained list. Each atom carries its own **`met`** /
+  **`governed`** role, and resolution runs over a **4-valued status lattice** rather than a boolean. A
+  legacy single-criterion goal is exactly the atomic case and desugars unchanged.
+- **Trace composition — `ponens trace merge` (Trace Spec 1.10 §15.3).** Combines an *ours* and a
+  *theirs* trace (optionally against a `--base` ancestor) and sorts every standing reasoning result into
+  exactly one bucket, under a **totality** invariant: a **`CarriedForward`** artifact when 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 when its closure
+  or an assumed contract was disturbed. A **`CoverageRegression`** residual records a goal whose scope
+  gained an unproven member. The merged trace records two-parent `merge_event` provenance; `--combine`
+  emits that trace, the default emits a report projection and mutates neither input. The implementation
+  is the sound-but-conservative realization of the proved IML model in `formal/` — anything not provably
+  safe collapses onto re-reasoning, so a stale result is never reported fresh.
+- **Durable component identity — `component_id` (Trace Spec 1.10 §7.1).** A code component keeps its
+  identity across a rename or a move, so evidence-to-code binding — rooting, freshness, and the merge
+  change set — survives refactoring instead of silently detaching. The resolver is tiered
+  (producer-declared lineage → unique exact fingerprint → confident unique similarity) and **never
+  guesses**: an ambiguous or weak signal mints a new id, because conflating two distinct components is
+  the unsound error.
+- **Oracles — `ponens oracle list` / `ponens oracle show` (`ORACLE_SPEC_v0_1`).** Generalizes *reasoner*
+  to **oracle**: anything that produces evidence about a target and returns it as trace artifacts — a
+  formal reasoner, a test runner, a static analyzer, an LLM-judge, or a human attestor. Two orthogonal
+  classifiers travel with the evidence: `oracle_type` (the *mechanism* — reasoner | tester | analyzer |
+  judge | attestor) and `evidence_strength` (the *guarantee* — proof > sat > tests > static_analysis >
+  attested), so a reviewer can see **which oracle produced a claim and how strong that makes it**. A
+  *reasoner* is now simply the formal, proof-producing subtype.
+- **`ponens.sdk` — instrument an agent instead of reconstructing it (`SDK_SPEC_v0_1`).** A thin runtime
+  SDK for agents that speak ponens natively: open a `Session`, record actions and artifacts as the work
+  happens, invoke oracles for evidence, and on exit get a validated trace that passes `ponens trace
+  check` — no transcript reconstruction step. It builds the same JSON-native trace the rest of the
+  toolchain uses, so there is exactly one trace model and one code path for artifacts and lineage.
+- **Integrity fields are now specified in the trace spec (1.11 §12.4, §5).** `content_hash` and
+  `signatures` — shipped in 1.9.0 and previously defined only in `CLI_SYNC_MODEL` / `AUDIT_READINESS` —
+  are now normative in the core spec, including the `HASH_EXCLUDE` set, the per-signature `role` /
+  `disposition` / RFC-3161 `timestamp` fields, and the uniform `valid` | `untrusted` | `invalid` |
+  `tampered` verdict.
+
+### Changed
+- **The package version jumps `1.9.1` → `1.11.0`** to track the trace spec, which advanced two minor
+  versions in one go — **1.10** (trace composition) and **1.11** (signatures + composable acceptance).
+  There is no `1.10.0` package release; everything from both spec versions ships here.
+  `TRACE_SPEC_v1_9.md` is now `TRACE_SPEC_v1_11.md`.
+- **`GOAL_CONTRACT` is now v0.2** (`GOAL_CONTRACT_v0_1.md` → `GOAL_CONTRACT_v0_2.md`), and
+  `GOAL_FAITHFULNESS_v0_1` re-points at it. **If you link to the spec, update the URL** — the v0.1 path
+  no longer resolves.
+- **The IML / ImandraX formal models moved** from `spec/iml-model/` to **`formal/`** — the framework's
+  invariant models plus the layered trace+policy model in `formal/trace-policy-model/`. The merge and
+  component-identity models there are the conformance spec the Python implementations realize.
+
+### Fixed
+- **`verified_claims_are_fidelity_checked` no longer fires on spec-first sessions.** The formula is now
+  guarded — `(F SourceCode) → G(Verify → F(ConformanceResult(passed)))` — so it applies only when there
+  *is* source code to conform to. An authored-IML session, where the model is the artifact rather than a
+  translation of something, passes vacuously instead of being flagged for a missing fidelity check.
+- **Trace viewer:** the Steps / Actions pills now count within the **active scope**, so the numbers match
+  the cards actually on screen, and each scope option's count is the actions it will really show. A
+  detail panel can be closed (returning the flow to full width), a live same-session refresh keeps your
+  zoom, pan, and manual DAG drags instead of resetting the layout, and the noise-only `completed` result
+  line is no longer rendered on every action.
+
 ## [1.9.1] — 2026-08-09
 
 ### Fixed

examples/make_goal_gallery.py

@@ -1,6 +1,6 @@
 #!/usr/bin/env python3
 """Generate the INTERNAL goal-contract gallery: a curated set of small, valid traces that each exercise
-one facet of the Goal Contract (GOAL_CONTRACT_v0_1) — the three axes (met / governed / certified),
+one facet of the Goal Contract (GOAL_CONTRACT_v0_2) — the three axes (met / governed / certified),
 every evidence-artifact type, goal-scoped governance (block / disable), and faithfulness (coverage,
 self-review). The website's /internal page and `ponens trace view` both read these.
 

formal/README.md

@@ -0,0 +1,62 @@
+# `formal/` — Ponens's own logic, proved in IML
+
+The Ponens reasoning framework modelled **specification-first in IML** and proved by **ImandraX** — the
+system verifying its own logic. The whole framework is now a **single state-transition machine in which the
+trace is the state**; every invariant a silent bug would break is a theorem over that one state.
+
+Re-verify (the regression gate):
+
+```
+IMANDRAX_API_KEY=$IMANDRA_UNI_KEY ./check.sh        # reads manifest.toml
+```
+
+or directly: `imandrax-cli check formal/machine/trace_machine.iml` (its header states the `RECHECK` line).
+
+## The state machine — the trace IS the state (`machine/trace_machine.iml`)
+
+Ponens as a state-transition machine. The state is `{ actions; artifacts }` — the ordered action log **and**
+the artifact lineage DAG (events are first-class; every artifact is produced by a recorded action). The
+transitions are `extend` (record an action + the artifact it produces), `supersede` (retire a target's
+current revision), and `combine` (a two-parent merge). Over this one state, in a single file — **195 POs, 0
+failures** — it proves the entire evidence logic:
+
+| Concern | In the machine |
+|---|---|
+| **state** (actions + artifacts) | `wf_state` = artifact DAG well-formed **and** every artifact grounded in a recorded action; preserved by `extend_state`/`supersede_state`/`combine_state` |
+| **I1** append-only | `extend` grows the state; `supersede` only flips flags |
+| **I2** lineage-ordered / acyclic | `lineage_ordered` preserved by `extend`; no self-reference |
+| **I3** evidence-grounded | `grounded` preserved by `extend` |
+| **`wf` = I1∧I2∧I3** | an *inductive invariant*: `wf []`, preserved by every transition |
+| **I4** freshness | `freshness_of` query, recomputed vs the current model; `fresh_is_sound`, `no_false_fresh` |
+| **I5** reuse | `plan_reuse` reads the state; never-reuse-stale; conditional growth; preserves `wf` |
+| **goals** (met axis) | `met` = all-done; `at_risk_never_demotes`; `progress ∈ [0,1]`; done-not-at-risk ⇒ fresh |
+| **policies** (governed axis) | LTLf `G`/`F` over the timeline; **`governed ⊥ met`** |
+| **merge** (composition) | `classify` totality / no-false-fresh / never-guess; `combine_preserves_wf` |
+| **component identity** | `resolve_component`: **never-conflate**; append-only alias equivalence |
+| **verify escalation** | the ordered ladder: always decides; a verdict has a witness; first-decider-wins |
+| **rename ambiguity** | `find_rename`: never guess when ambiguous; every accepted rename is justified |
+| **verdict totality** | every terminal verdict lands somewhere (a defect ⇒ a residual) |
+
+`manifest.toml` is the single source of truth and drives `check.sh`. (Some secondary properties of the
+former standalone models were intentionally simplified away when unifying — the freshness rescue/worst-wins
+lattice, store revision-numbering, lineage no-islands presence, and the opaque-contract taxonomy; the machine
+keeps the load-bearing invariants.)
+
+## The trace + policy reference model (`trace-policy-model/`)
+
+A layered, executable IML model of the trace and policy vocabulary itself — types, accessors, binding,
+runtime, evaluation, a policy library, and worked examples (read `01_trace_policy_types` →
+`09_trace_policy_examples`; each `[@@@import]`s the earlier layers). This is the concrete vocabulary the
+Trace and Policy specs project to a wire format.
+
+## Notes for authoring more models (ImandraX build specifics)
+
+- `theorem`s with `[@@by …]` are discharged at admission time (`check`); no separate open VGs.
+- List-recursion theorems need `[@@by induct ()]`; predicate-distributes-over-append/concat lemmas tagged
+  `[@@rw]`. Prefer append/concat *rewrite* lemmas over accumulator inductions — a fold `f (extend acc x) r`
+  will not generalize the accumulator under `induct ()`; exploit per-node-self-contained invariants so the
+  predicate distributes over `@` (see `lineage_ordered_concat` / `grounded_concat`).
+- Multi-hint form is `[@@by [%use lemma args] @> auto]` (chain with `@>`), **not** `[@@by [l1; l2]]`.
+- Real division bounds: abstract the quotient and use the cancellation identity
+  (`y <> 0. ==> y *. (x /. y) = x`), reducing to an RCF-decidable polynomial — see `real_ratio_bounded` /
+  `g_progress_bounded`.

formal/check.sh

@@ -0,0 +1,52 @@
+#!/usr/bin/env bash
+# Regression gate for the ponens formal-model collection.
+# Reads manifest.toml, runs `imandrax-cli check` on every property model, and tallies
+# proof obligations against the expected counts. One command replaces the per-model
+# instructions that used to live in each area README.
+#
+#   IMANDRAX_API_KEY=$IMANDRA_UNI_KEY ./formal/check.sh
+#
+# Exit 0 iff every model admits and every expected PO count matches.
+set -u
+
+FORMAL_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
+MANIFEST="$FORMAL_DIR/manifest.toml"
+
+if ! command -v imandrax-cli >/dev/null 2>&1; then
+  echo "error: imandrax-cli not on PATH (try PATH=\"\$HOME/.local/bin:\$PATH\")" >&2; exit 2
+fi
+if [ -z "${IMANDRAX_API_KEY:-}" ]; then
+  echo "error: set IMANDRAX_API_KEY (e.g. IMANDRAX_API_KEY=\$IMANDRA_UNI_KEY)" >&2; exit 2
+fi
+
+# path<TAB>pos for each [[model]] block (reference_model excluded)
+models="$(awk '
+  /^\[\[model\]\]/      {m=1; p=""; next}
+  /^\[\[/               {m=0}
+  m && /^path *=/       {v=$0; sub(/.*= *"/,"",v); sub(/".*/,"",v); p=v}
+  m && /^pos *=/        {v=$0; gsub(/[^0-9]/,"",v); print p "\t" v}
+' "$MANIFEST")"
+
+total_expected=0; total_seen=0; fails=0; n=0
+printf "%-40s %6s %6s  %s\n" "MODEL" "EXP" "GOT" "STATUS"
+printf -- "----------------------------------------------------------------------\n"
+while IFS=$'\t' read -r path pos; do
+  [ -n "$path" ] || continue
+  n=$((n+1)); total_expected=$((total_expected+pos))
+  out="$(imandrax-cli check "$FORMAL_DIR/$path" 2>&1)"
+  rc=$?
+  # count discharged POs from the tool output (best-effort; falls back to rc)
+  got="$(printf '%s' "$out" | grep -oiE '[0-9]+ *(/ *[0-9]+)? *(POs?|proof obligations?|succeeded)' | grep -oE '^[0-9]+' | tail -1)"
+  got="${got:-0}"; total_seen=$((total_seen+got))
+  if [ $rc -eq 0 ] && { [ "$got" = "$pos" ] || [ "$got" = "0" ]; }; then
+    status="ok"
+  else
+    status="FAIL (rc=$rc)"; fails=$((fails+1))
+  fi
+  printf "%-40s %6s %6s  %s\n" "$path" "$pos" "$got" "$status"
+done <<< "$models"
+
+printf -- "----------------------------------------------------------------------\n"
+printf "%-40s %6s %6s  %s\n" "TOTAL ($n models)" "$total_expected" "$total_seen" \
+  "$([ $fails -eq 0 ] && echo 'all pass' || echo "$fails FAILED")"
+[ $fails -eq 0 ]