Skip to content

Reality probe: Cognee #5161 passes local prune tests but the end-to-end claim is contradicted #45

Description

@hippoley

Source PR: topoteretes/cognee#5161

@siillee @dexters1 — I used #5161 as a CounterProof Reality Probe because the review has a very clean distinction between a local safety property that the new tests exercise and a broader end-to-end claim those tests do not cover.

I am not re-reviewing the PR or recommending a merge decision.

What the submitted tests establish

The new unit coverage checks that a shared PGVector adapter refuses its own prune() before clearing vector metadata or calling its relational delete_database().

That is a useful, narrow property.

What the broader flow still does

On the PR HEAD, prune_system._prune() currently executes:

graph_engine.delete_graph()
        ↓
vector_engine.prune()
        ↓
SharedDatabasePruneError

when graph=True, vector=True, metadata=False.

That matches @siillee's review reproduction: the vector refusal propagates only after graph deletion has already happened.

The changed test_vector_only_prune_propagates_shared_database_refusal uses graph=False, so it cannot establish the stronger end-to-end property.

There is a second, separate upgrade concern in the review: changing which DB the vector adapter connects to may strand existing vectors or point an upgraded deployment at a DB that does not yet exist.

Claim / evidence matrix

I encoded the review evidence without pretending CounterProof independently ran your PostgreSQL environment:

https://github.com/hippoley/CounterProof/blob/main/examples/claim_matrix/cognee-5161.yml

Current shape:

shared PGVector local refusal
  submitted tests: present on HEAD
  CounterProof BASE/HEAD replay: not run
  overall: UNPROVEN by CounterProof

no partial system prune before refusal
  submitted coverage: absent
  human oracle/reproduction: CONTRADICTED

upgrade data-location safety
  submitted coverage: absent
  oracle: UNVERIFIED

The important part is that human reviewer evidence is allowed to contradict a broader claim without being rewritten as a CounterProof-generated witness.

One question

As a reviewer/author, would this per-claim split be useful enough to keep around in a real review, or is the original inline review clearer than a separate evidence matrix?

A short “useful / not useful + why” is exactly the feedback I want.

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions