query: gate the monotone oracle's entry diff by static footprint
commit ea0c493
query: gate the monotone oracle's entry diff by static footprint
entry_sets_equal_the_oracle_diff_over_random_histories computed every
query’s entry as full(after) minus full(before) unconditionally, so a
ref transition outside a query’s own footprint (recreating a deleted
branch at an already-tested commit) could flip the oracle’s shared
reachable-universe helper and make a results()-only query appear to
gain a member, even though the real evaluator’s footprint gate
correctly reports no entry for a ref it never looks at. Per adjudicated
semantics (query.results), results() membership is decided by the
presence of the recorded results ref alone; an out-of-footprint
transition is a non-event for that query, so the oracle’s diff must be
suppressed exactly where entry_set already short-circuits, not left to
leak through the universe used only by full evaluation.
Adds a hand-written, from-scratch mirror of each of the five fixture
queries' static footprints (never calling Query::footprint) to gate
the diff; full evaluation is untouched since it and the evaluator’s
own eval() intentionally share the same reachable-universe resolution
for decoding a results ref’s short-oid segment. Checks in the
regression seed proptest shrank to, per convention.
query.footprint: annotate as verified by this test
query.results: annotate as verified by this test
Assisted-by: Claude:claude-sonnet-5
No reviews of this commit yet — record a verdict below.
Start a review
crates/ents-query/tests/monotone.rs
@@ -3,8 +3,12 @@
//! synthetic ref histories — advances, force-pushes, deletions, result
//! recordings — checked after every transition against an independent
//! naive oracle. The evaluator's incremental entry set must equal the
-//! oracle's `full(after) − full(before)` for every query, every time;
-//! the work set must equal the entry set minus recorded prefixes.
+//! oracle's `full(after) − full(before)` for every query whose static
+//! footprint the transitioned ref touches, and the empty set otherwise
+//! (`query.footprint`, `query.results`): a `results()` atom's entry set
+//! cannot be moved by an unrelated ref's reachability, only by its own
+//! results refs. The work set must equal the entry set minus recorded
+//! prefixes.
#![expect(
clippy::expect_used,
@@ -184,6 +188,29 @@
"rev(refs/heads/main) | rev(refs/heads/dev)",
];
+/// Each of the five queries' static ref-footprint (`query.footprint`),
+/// hand-written independently of `Query::footprint` — this is what the
+/// oracle checks against, not a call into the thing under test.
+///
+/// A `results()` atom's footprint is its own results namespace, nothing
+/// else (`query.results`): a transition outside a query's footprint,
+/// such as deleting and recreating an unrelated branch, is a non-event
+/// for that query's entry set, even though it can change which commits
+/// `oracle`'s shared reachable-universe helper currently sees (a
+/// reconciliation-grade concern the diff below must not leak into
+/// incremental entry).
+fn footprint_touches(query_index: usize, moved: &str) -> bool {
+ let results_of = |effect: &str| moved.starts_with(&format!("refs/meta/results/{effect}/"));
+ match query_index {
+ 0 => moved == "refs/heads/main",
+ 1 => moved.starts_with("refs/heads/"),
+ 2 => moved == "refs/heads/main" || results_of("unit"),
+ 3 => results_of("unit") || results_of("integ"),
+ 4 => moved == "refs/heads/main" || moved == "refs/heads/dev",
+ _ => unreachable!("five queries"),
+ }
+}
+
// ---------------------------------------------------------------------
// The property.
// ---------------------------------------------------------------------
@@ -191,7 +218,7 @@
proptest! {
#![proptest_config(ProptestConfig::with_cases(48))]
- // @relation(query.monotone, query.incremental, query.set-ops, query.workset, scope=function, role=Verifies)
+ // @relation(query.monotone, query.incremental, query.set-ops, query.workset, query.footprint, query.results, scope=function, role=Verifies)
#[test]
fn entry_sets_equal_the_oracle_diff_over_random_histories(
ops in proptest::collection::vec(op_strategy(), 1..14)
@@ -265,10 +292,16 @@
let full_before = oracle(&objects, &before, index);
let full_after = oracle(&objects, &after, index);
- // Incremental entry == full(after) − full(before):
- // entry-only, no retraction, no full re-evaluation.
+ // Incremental entry == full(after) − full(before), but
+ // only within the query's own footprint; a transition
+ // outside it is a non-event no matter what the raw diff
+ // of two full evaluations would suggest.
let expected: std::collections::BTreeSet<ObjectId> =
- full_after.difference(&full_before).copied().collect();
+ if footprint_touches(index, &moved) {
+ full_after.difference(&full_before).copied().collect()
+ } else {
+ std::collections::BTreeSet::new()
+ };
let entered = evaluator
.entry_set(query, &transition)
.expect("evaluates");
crates/ents-query/tests/monotone.proptest-regressions
@@ -1,0 +1,7 @@
+# Seeds for failure cases proptest has generated in the past. It is
+# automatically read and these particular cases re-run before any
+# novel cases are generated.
+#
+# It is recommended to check this file in to source control so that
+# everyone who runs the test benefits from these saved cases.
+cc 3e0082f30eec9fbd60151b22cccac793b91f2c53f1097cdb9136c68ae5edbfff # shrinks to ops = [Advance { branch: 0, count: 1 }, Delete { branch: 0 }, Record { effect: 0, commit: 0, status: 0, short_len: 7 }, Record { effect: 1, commit: 0, status: 0, short_len: 7 }, ForceTo { branch: 0, commit: 0 }]