use std::{
collections::{BTreeMap, BTreeSet},
fmt::Debug,
};
use proptest::prelude::*;
use crate::{
DBData, OutputHandle, RootCircuit, Runtime, ZWeight,
circuit::CircuitConfig,
typed_batch::{IndexedZSetReader, OrdZSet, SpineSnapshot},
};
pub(super) type ZSet<T> = BTreeMap<T, ZWeight>;
pub(super) type Transaction<I> = Vec<I>;
pub(super) type Proposals<T> = Vec<(T, bool)>;
#[derive(Clone, Copy, Debug)]
pub(super) struct Config {
pub workers: usize,
pub chunk_size: Option<usize>,
}
impl Config {
fn circuit_config(&self) -> CircuitConfig {
let config = CircuitConfig::from(self.workers);
match self.chunk_size {
Some(records) => config.with_splitter_chunk_size_records(records as u64),
None => config,
}
}
}
pub(super) fn configs() -> Vec<Config> {
[1, 2, 3]
.into_iter()
.flat_map(|workers| {
[Some(1), Some(2), None]
.into_iter()
.map(move |chunk_size| Config {
workers,
chunk_size,
})
})
.collect()
}
pub(super) trait Program: Clone + Send + 'static {
type Input: Clone + Debug;
type Handles: Send + 'static;
type Output: PartialEq + Debug;
fn build(&self, circuit: &mut RootCircuit) -> Self::Handles;
fn push(&self, handles: &Self::Handles, input: &Self::Input);
fn read(&self, handles: &Self::Handles) -> Self::Output;
fn model(&self, inputs: &[Self::Input]) -> Self::Output;
}
pub(super) fn check<P: Program>(program: &P, workload: &[Transaction<P::Input>], config: Config) {
let builder = program.clone();
let (mut circuit, handles) = Runtime::init_circuit(config.circuit_config(), move |circuit| {
Ok(builder.build(circuit))
})
.unwrap();
let mut history = Vec::new();
for (index, transaction) in workload.iter().enumerate() {
if let [input] = transaction.as_slice() {
program.push(&handles, input);
circuit.transaction().unwrap();
} else {
circuit.start_transaction().unwrap();
for input in transaction {
program.push(&handles, input);
circuit.step().unwrap();
}
circuit.commit_transaction().unwrap();
}
history.extend(transaction.iter().cloned());
assert_eq!(
program.read(&handles),
program.model(&history),
"{config:?}, after transaction {index}"
);
}
circuit.kill().unwrap();
}
pub(super) fn read_zset<T: DBData>(handle: &OutputHandle<SpineSnapshot<OrdZSet<T>>>) -> ZSet<T> {
let mut rows = ZSet::new();
for (row, (), weight) in handle.concat().consolidate().iter() {
*rows.entry(row).or_default() += weight;
}
rows
}
pub(super) fn apply_proposals<T: Ord + Clone>(
live: &mut BTreeSet<T>,
proposals: &Proposals<T>,
) -> Vec<(T, ZWeight)> {
let mut changes = Vec::new();
for (row, delete) in proposals {
if !live.contains(row) {
live.insert(row.clone());
changes.push((row.clone(), 1));
} else if *delete {
live.remove(row);
changes.push((row.clone(), -1));
}
}
changes
}
pub(super) fn add_changes<T: Ord + Clone>(zset: &mut ZSet<T>, changes: &[(T, ZWeight)]) {
for (row, weight) in changes {
*zset.entry(row.clone()).or_default() += weight;
}
zset.retain(|_, weight| *weight != 0);
}
pub(super) fn set_after<'a, T: Ord + Clone + Debug + 'a>(
changes: impl IntoIterator<Item = &'a [(T, ZWeight)]>,
) -> BTreeSet<T> {
let mut zset = ZSet::new();
for step in changes {
add_changes(&mut zset, step);
}
assert!(
zset.values().all(|weight| *weight == 1),
"not a set: {zset:?}"
);
zset.into_keys().collect()
}
pub(super) fn fixpoint<S: PartialEq>(start: S, step: impl Fn(&S) -> S) -> S {
let mut current = start;
for _ in 0..10_000 {
let next = step(¤t);
if next == current {
return current;
}
current = next;
}
panic!("the model did not reach a fixed point");
}
pub(super) fn set_zset<T: Ord + Clone>(set: &BTreeSet<T>) -> ZSet<T> {
set.iter().map(|row| (row.clone(), 1)).collect()
}
pub(super) fn workloads<S: Strategy>(
step: S,
max_transactions: usize,
max_steps: usize,
) -> impl Strategy<Value = Vec<Vec<S::Value>>> {
prop::collection::vec(
prop::collection::vec(step, 1..=max_steps),
1..=max_transactions,
)
}
pub(super) fn proposals<T: Clone + Debug>(
element: impl Strategy<Value = T>,
max: usize,
) -> impl Strategy<Value = Proposals<T>> {
prop::collection::vec((element, any::<bool>()), 0..=max)
}
pub(super) fn map_steps<R, I>(
raw: Vec<Vec<R>>,
mut step: impl FnMut(R) -> I,
) -> Vec<Transaction<I>> {
raw.into_iter()
.map(|transaction| transaction.into_iter().map(&mut step).collect())
.collect()
}
pub(super) fn any_config() -> impl Strategy<Value = Config> {
prop::sample::select(configs())
}