Skip to content

Commit 92b6c62

Browse files
committed
Add proptest tests for new query subsumption
1 parent ec702a8 commit 92b6c62

File tree

1 file changed

+162
-0
lines changed
  • linera-core/src/client/requests_scheduler

1 file changed

+162
-0
lines changed

linera-core/src/client/requests_scheduler/request.rs

Lines changed: 162 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1852,4 +1852,166 @@ mod tests {
18521852
// Verify B does NOT subsume A (doesn't have all heights)
18531853
assert!(!key_b.subsumes(&key_a));
18541854
}
1855+
1856+
// Property-based tests for ChainInfo subsumption
1857+
// These tests use Arbitrary to generate random ChainInfoQuery instances and verify
1858+
// that subsumption properties hold across the entire input space.
1859+
1860+
#[cfg(all(test, not(target_arch = "wasm32")))]
1861+
mod property_tests {
1862+
use proptest::prelude::*;
1863+
use rand::seq::SliceRandom;
1864+
1865+
use super::*;
1866+
1867+
/// Returns a random subset of the input slice
1868+
fn random_subset<T: Clone>(items: &[T], rng: &mut impl rand::Rng) -> Vec<T> {
1869+
if items.is_empty() {
1870+
return vec![];
1871+
}
1872+
let subset_size = rng.gen_range(0..=items.len());
1873+
items.choose_multiple(rng, subset_size).cloned().collect()
1874+
}
1875+
1876+
/// Derives a subset query from a base query.
1877+
/// The resulting query should be subsumed by the base query.
1878+
fn derive_subset_query(base: &ChainInfoQuery, rng: &mut impl rand::Rng) -> ChainInfoQuery {
1879+
let mut subset = ChainInfoQuery::new(base.chain_id);
1880+
1881+
// Exact-match fields must be copied exactly
1882+
subset.request_owner_balance = base.request_owner_balance;
1883+
subset.test_next_block_height = base.test_next_block_height;
1884+
subset.request_leader_timeout = base.request_leader_timeout;
1885+
1886+
// Boolean flags: if base has true, subset can be true or false
1887+
// if base has false, subset must be false
1888+
subset.request_committees = base.request_committees && rng.gen_bool(0.5);
1889+
subset.request_pending_message_bundles =
1890+
base.request_pending_message_bundles && rng.gen_bool(0.5);
1891+
subset.request_manager_values = base.request_manager_values && rng.gen_bool(0.5);
1892+
subset.request_fallback = base.request_fallback && rng.gen_bool(0.5);
1893+
subset.create_network_actions = base.create_network_actions && rng.gen_bool(0.5);
1894+
1895+
// Collection fields: pick a random subset of heights
1896+
subset.request_sent_certificate_hashes_by_heights =
1897+
random_subset(&base.request_sent_certificate_hashes_by_heights, rng);
1898+
1899+
// Range field: if base excludes n entries, subset can exclude >= n entries
1900+
subset.request_received_log_excluding_first_n =
1901+
base.request_received_log_excluding_first_n.map(|n| {
1902+
let additional = rng.gen_range(0..=10);
1903+
n.saturating_add(additional)
1904+
});
1905+
1906+
subset
1907+
}
1908+
1909+
/// Derives a superset query that the base query cannot subsume.
1910+
/// The resulting query has additional requirements not in the base query.
1911+
fn derive_superset_query(
1912+
base: &ChainInfoQuery,
1913+
rng: &mut impl rand::Rng,
1914+
) -> ChainInfoQuery {
1915+
let mut superset = base.clone();
1916+
1917+
// Choose one way to add requirements
1918+
match rng.gen_range(0..4) {
1919+
0 => {
1920+
// Add a boolean flag requirement
1921+
if !base.request_committees {
1922+
superset.request_committees = true;
1923+
} else if !base.request_pending_message_bundles {
1924+
superset.request_pending_message_bundles = true;
1925+
} else if !base.request_manager_values {
1926+
superset.request_manager_values = true;
1927+
} else if !base.request_fallback {
1928+
superset.request_fallback = true;
1929+
}
1930+
}
1931+
1 => {
1932+
// Add a height not in base
1933+
let new_height = BlockHeight(rng.gen_range(1000..2000));
1934+
if !base
1935+
.request_sent_certificate_hashes_by_heights
1936+
.contains(&new_height)
1937+
{
1938+
superset
1939+
.request_sent_certificate_hashes_by_heights
1940+
.push(new_height);
1941+
}
1942+
}
1943+
2 => {
1944+
// Request more log entries
1945+
match base.request_received_log_excluding_first_n {
1946+
Some(n) if n > 0 => {
1947+
superset.request_received_log_excluding_first_n =
1948+
Some(n.saturating_sub(1))
1949+
}
1950+
None => superset.request_received_log_excluding_first_n = Some(0),
1951+
_ => {}
1952+
}
1953+
}
1954+
_ => {
1955+
// Change exact-match field to make queries incompatible
1956+
superset.test_next_block_height = Some(BlockHeight(rng.gen_range(1..1000)));
1957+
}
1958+
}
1959+
1960+
superset
1961+
}
1962+
1963+
proptest! {
1964+
/// Property: Every query subsumes itself (reflexivity)
1965+
#[test]
1966+
fn prop_subsumption_reflexivity(query in any::<ChainInfoQuery>()) {
1967+
let key = RequestKey::ChainInfo(query);
1968+
prop_assert!(key.subsumes(&key));
1969+
}
1970+
1971+
/// Property: Subsumption is transitive
1972+
/// If A subsumes B and B subsumes C, then A subsumes C
1973+
#[test]
1974+
fn prop_subsumption_transitivity(query_a in any::<ChainInfoQuery>()) {
1975+
let mut rng = rand::thread_rng();
1976+
let query_b = derive_subset_query(&query_a, &mut rng);
1977+
let query_c = derive_subset_query(&query_b, &mut rng);
1978+
1979+
let key_a = RequestKey::ChainInfo(query_a);
1980+
let key_b = RequestKey::ChainInfo(query_b);
1981+
let key_c = RequestKey::ChainInfo(query_c);
1982+
1983+
prop_assert!(key_a.subsumes(&key_b), "A should subsume B");
1984+
prop_assert!(key_b.subsumes(&key_c), "B should subsume C");
1985+
prop_assert!(key_a.subsumes(&key_c), "A should subsume C (transitivity)");
1986+
}
1987+
1988+
/// Property: A query subsumes all its proper subsets
1989+
#[test]
1990+
fn prop_subsumption_subset(query_a in any::<ChainInfoQuery>()) {
1991+
let mut rng = rand::thread_rng();
1992+
let query_b = derive_subset_query(&query_a, &mut rng);
1993+
1994+
let key_a = RequestKey::ChainInfo(query_a);
1995+
let key_b = RequestKey::ChainInfo(query_b);
1996+
1997+
prop_assert!(key_a.subsumes(&key_b), "Comprehensive query should subsume subset query");
1998+
}
1999+
2000+
/// Property: A query does not subsume queries with additional requirements
2001+
#[test]
2002+
fn prop_subsumption_non_subsumption(query_a in any::<ChainInfoQuery>()) {
2003+
let mut rng = rand::thread_rng();
2004+
let query_b = derive_superset_query(&query_a, &mut rng);
2005+
2006+
let key_a = RequestKey::ChainInfo(query_a.clone());
2007+
let key_b = RequestKey::ChainInfo(query_b.clone());
2008+
2009+
// Only assert non-subsumption if we actually added a requirement
2010+
// (superset derivation might not change anything in edge cases)
2011+
if query_a != query_b {
2012+
prop_assert!(!key_a.subsumes(&key_b), "Query should not subsume superset with additional requirements");
2013+
}
2014+
}
2015+
}
2016+
}
18552017
}

0 commit comments

Comments
 (0)