feat(cli): closure fingerprint, canonical proof states, journal accounting #28

Merged

hugooconnor merged 0 commits from refs/pull/28/head into main 2026-07-16 13:08:42 +00:00

Conversation 1 Commits - Files changed -

hugooconnor commented 2026-07-16 09:44:24 +00:00 (Migrated from codeberg.org)

Copy link

What & why

Three CLI observability / reproducibility follow-ups reported from the grounded
two-machine FLF run, where the harness had to reconstruct each of these by hand
with bespoke jq | shasum pipelines and hard-coded SIDs.

Closes #20 — canonical semantic closure fingerprint

A first-class, versioned fingerprint so two replicas (or a clean replay)
can check they reached the same semantic closure without ad-hoc hashing.

• src/core/fingerprint.rs — elephant.closure.v1 / sha256 over every
  non-membership conclusion's proof tag. Excludes everything
  identity-/deployment-specific (membership, local aliases, theory id, signers,
  timestamps). Byte framing is fully specified and tested: LF-joined
  {tag} {literal} lines, sorted by (literal, tag), de-duplicated, no
  terminal LF.
• elephant closure fingerprint [--sequence], elephant status --fingerprint
  (same digest, embedded), and elephant closure compare a.json b.json —
  recomputes each status --json file's fingerprint offline; exit 0 on
  match, exit 10 on mismatch.
• Verified: same corpus under a different identity → same digest; a single
  changed proof tag → different digest.

Closes #26 — canonical plain-language proof states

• Shared, versioned mapping (closure::proof_state, top-level
  proof_state_map) from the compact +D/+d/-D/-d tags to
  {proof_state, positive, level}, applied in status, trace, and
  what-if JSON. -v names the state in text output without making the
  default noisy. Names follow the engine's own ConclusionType variants, so
  the mapping is authoritative, not a paraphrase.

Closes #22 — journal accounting + log filters

• elephant theory inspect <theory> breaks the single journal total into
  active / retracted assertions, retraction entries, and setup (meta/member)
  vs. content, from the same status semantics log uses.
• elephant log gains composable (AND) filters: --status,
  --performative, --signer, --sid, --retracts. An empty match is a
  valid empty structured result.

#17 — defeater polarity docs

Already resolved on main by 834d4e7 (polarity section + executable fixture;
the enumerated files live in the out-of-scope Spindle repo). No change here.

Contract note

Adds exit code 10 (Predicate: a checked condition ran cleanly but did not
hold) to the pinned exit-code contract — used by closure compare and reusable
by the deferred sync-wait barrier (#24).

Tests

• New tests/observability_cli.rs drives all three features end-to-end
  (proof-state fields, fingerprint agreement across surfaces,
  identity-independence, match/mismatch exit codes, theory inspect counts,
  composable log filters).
• src/core/fingerprint.rs unit tests cover order-independence, member
  exclusion, tag-sensitivity, and the exact byte framing.
• Full suite: 229 passed, 2 ignored. cargo clippy clean on all touched
  files (one pre-existing warning in src/p2p/sync.rs, untouched).

Deferred follow-ups (not in this PR)

Left as separate work; several build on the fingerprint landed here:
#21 idempotent assert --ensure, #23 SPL lint, #24 sync wait
barriers (can reuse the fingerprint + exit 10), #25 explain --all --provenance, #27 theory export/replay (can reuse the fingerprint and
theory inspect accounting).

🤖 Generated with Claude Code

## What & why Three CLI observability / reproducibility follow-ups reported from the grounded two-machine FLF run, where the harness had to reconstruct each of these by hand with bespoke `jq | shasum` pipelines and hard-coded SIDs. ### Closes #20 — canonical semantic closure fingerprint A first-class, **versioned** fingerprint so two replicas (or a clean replay) can check they reached the same semantic closure without ad-hoc hashing. - `src/core/fingerprint.rs` — `elephant.closure.v1` / sha256 over every **non-membership** conclusion's proof tag. Excludes everything identity-/deployment-specific (membership, local aliases, theory id, signers, timestamps). Byte framing is fully specified and tested: LF-joined `{tag} {literal}` lines, sorted by `(literal, tag)`, de-duplicated, **no** terminal LF. - `elephant closure fingerprint [--sequence]`, `elephant status --fingerprint` (same digest, embedded), and `elephant closure compare a.json b.json` — recomputes each `status --json` file's fingerprint offline; **exit 0 on match, exit 10 on mismatch**. - Verified: same corpus under a different identity → same digest; a single changed proof tag → different digest. ### Closes #26 — canonical plain-language proof states - Shared, versioned mapping (`closure::proof_state`, top-level `proof_state_map`) from the compact `+D/+d/-D/-d` tags to `{proof_state, positive, level}`, applied in `status`, `trace`, and `what-if` JSON. `-v` names the state in text output without making the default noisy. Names follow the engine's own `ConclusionType` variants, so the mapping is authoritative, not a paraphrase. ### Closes #22 — journal accounting + log filters - `elephant theory inspect <theory>` breaks the single journal total into active / retracted assertions, retraction entries, and **setup (meta/member) vs. content**, from the same status semantics `log` uses. - `elephant log` gains composable (**AND**) filters: `--status`, `--performative`, `--signer`, `--sid`, `--retracts`. An empty match is a valid empty structured result. ### #17 — defeater polarity docs Already resolved on `main` by 834d4e7 (polarity section + executable fixture; the enumerated files live in the out-of-scope Spindle repo). No change here. ## Contract note Adds exit code **10** (`Predicate`: a checked condition ran cleanly but did not hold) to the pinned exit-code contract — used by `closure compare` and reusable by the deferred sync-wait barrier (#24). ## Tests - New `tests/observability_cli.rs` drives all three features end-to-end (proof-state fields, fingerprint agreement across surfaces, identity-independence, match/mismatch exit codes, `theory inspect` counts, composable `log` filters). - `src/core/fingerprint.rs` unit tests cover order-independence, member exclusion, tag-sensitivity, and the exact byte framing. - Full suite: **229 passed, 2 ignored**. `cargo clippy` clean on all touched files (one pre-existing warning in `src/p2p/sync.rs`, untouched). ## Deferred follow-ups (not in this PR) Left as separate work; several build on the fingerprint landed here: **#21** idempotent `assert --ensure`, **#23** SPL lint, **#24** `sync wait` barriers (can reuse the fingerprint + exit 10), **#25** `explain --all --provenance`, **#27** `theory export`/`replay` (can reuse the fingerprint and `theory inspect` accounting). 🤖 Generated with [Claude Code](https://claude.com/claude-code)

hugooconnor commented 2026-07-16 11:33:32 +00:00 (Migrated from codeberg.org)

Copy link

Addressed all seven review findings in 31bdb55:

[P2] Reject malformed status rows — of_status_json now returns Result and rejects any row missing a string tag/literal or carrying a tag outside +D/+d/-D/-d, naming the offending index. No more silent drop → no false convergence. Unit test malformed_rows_are_rejected_not_dropped.

[P2] Exclude negated member conclusions — is_member unwraps a single (not …) and checks membership on both the literal and its inner form, so (not (member …)) is excluded too. Test members_excluded_both_polarities.

[P2] Classify setup from parsed SPL — is_setup_assert parses the payload and checks metadata()/predicate_metadata()/predicate_declarations() and member facts via the head literal's name, so all membership/meta spellings count as setup. Test membership_fact_counts_as_setup.

[P2] Account for retracted non-assert acts — retracted commits/requests now increment other_retracted; the total is fully explained. Test retracted_commit_is_accounted.

[P2] Include malformed corpus elements in totals — journal_entries now adds store.entries().1.len(), matching theory list; exposed as a malformed field.

[P2] Reject invalid closed-set log filters — --status/--performative are now clap ValueEnums, so --status activ is a parse error (exit 1). Test invalid_closed_set_filters_are_rejected.

[P3] No store for offline compare — closure compare is routed before Paths::resolve() and takes only json; works with every home var unset. Test compare_needs_no_store (env_clear()).

Full suite: 234 passed.

Addressed all seven review findings in 31bdb55: **[P2] Reject malformed status rows** — `of_status_json` now returns `Result` and rejects any row missing a string `tag`/`literal` or carrying a tag outside `+D/+d/-D/-d`, naming the offending index. No more silent drop → no false convergence. Unit test `malformed_rows_are_rejected_not_dropped`. **[P2] Exclude negated member conclusions** — `is_member` unwraps a single `(not …)` and checks membership on both the literal and its inner form, so `(not (member …))` is excluded too. Test `members_excluded_both_polarities`. **[P2] Classify setup from parsed SPL** — `is_setup_assert` parses the payload and checks `metadata()`/`predicate_metadata()`/`predicate_declarations()` and member facts via the head literal's name, so all membership/meta spellings count as setup. Test `membership_fact_counts_as_setup`. **[P2] Account for retracted non-assert acts** — retracted commits/requests now increment `other_retracted`; the total is fully explained. Test `retracted_commit_is_accounted`. **[P2] Include malformed corpus elements in totals** — `journal_entries` now adds `store.entries().1.len()`, matching `theory list`; exposed as a `malformed` field. **[P2] Reject invalid closed-set log filters** — `--status`/`--performative` are now clap `ValueEnum`s, so `--status activ` is a parse error (exit 1). Test `invalid_closed_set_filters_are_rejected`. **[P3] No store for offline compare** — `closure compare` is routed before `Paths::resolve()` and takes only `json`; works with every home var unset. Test `compare_needs_no_store` (`env_clear()`). Full suite: 234 passed.

Sign in to join this conversation.

Reviewers

No reviewers

Labels

Clear labels

No items

No labels

Milestone

Clear milestone

No items

No milestone

Projects

Clear projects

No items

No project

Assignees

Clear assignees

No assignees

1 participant

Notifications

Subscribe

Due date

The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set.

Reference

anuna-research/elephant!28

No description provided.