Skip to content

Commit 96a0913

Browse files
committed
FIX: Fix incorrect proof in join_cover
This is an API break, because the previous proof was unsound. Like the bug points out, in join cover we take (self, other) and extend self until the end of other; if other ends before self, we don't gain any "cover" from other, and thus the proof is the same as self (making the method quite useless). Added traits for checking the proof value in dynamic code, since completest really doesn't work well right now.
1 parent 9da9030 commit 96a0913

2 files changed

Lines changed: 71 additions & 1 deletion

File tree

src/indexing.rs

Lines changed: 43 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -178,7 +178,29 @@ impl<'id, P> Range<'id, P> {
178178
}
179179

180180
/// Extend the range to the end of `other`, including any space in between
181-
pub fn join_cover<Q>(&self, other: Range<'id, Q>) -> Range<'id, <(P, Q) as ProofAdd>::Sum>
181+
///
182+
///
183+
/// ```compile-fail
184+
/// // compile-fail only enabled in 2018 edition
185+
/// // Bug from https://github.com/bluss/indexing/issues/12
186+
/// use indexing::scope;
187+
///
188+
/// let array = [0, 1, 2, 3, 4, 5];
189+
/// scope(&array[..], |arr| {
190+
/// let left = arr.vet_range(0..2).unwrap();
191+
/// let left = left.nonempty().unwrap();
192+
/// let (_, right) = arr.range().frontiers();
193+
194+
/// let joined = right.join_cover(left);
195+
/// let ix = joined.first();
196+
/// dbg!(ix);
197+
/// dbg!(arr[ix]); //~ ERROR Can't index by ix, because it's an edge index
198+
/// });
199+
/// ```
200+
// Proof P: Extends at least as far as self, not necessarily using any part
201+
// of other
202+
//
203+
pub fn join_cover<Q>(&self, other: Range<'id, Q>) -> Range<'id, P>
182204
where (P, Q): ProofAdd,
183205
{
184206
let end = cmp::max(self.end, other.end);
@@ -188,6 +210,7 @@ impl<'id, P> Range<'id, P> {
188210
}
189211

190212
/// Extend the range to start and end of `other`, including any space in between
213+
// Proof Sum of P and Q: Covers the union, so must be nonempty if any are
191214
pub fn join_cover_both<Q>(&self, other: Range<'id, Q>) -> Range<'id, <(P, Q) as ProofAdd>::Sum>
192215
where (P, Q): ProofAdd,
193216
{
@@ -563,3 +586,22 @@ fn test_frac_step() {
563586
assert_eq!(f.next(), None);
564587
}
565588

589+
590+
#[test]
591+
fn test_join_cover() {
592+
use crate::scope;
593+
594+
// Bug from https://github.com/bluss/indexing/issues/12
595+
let array = [0, 1, 2, 3, 4, 5];
596+
scope(&array[..], |arr| {
597+
let left = arr.vet_range(0..2).unwrap();
598+
let left = left.nonempty().unwrap();
599+
let (_, right) = arr.range().frontiers();
600+
601+
let joined = right.join_cover(left);
602+
let ix = joined.first();
603+
dbg!(ix);
604+
assert!(!ix.nonempty_proof());
605+
ix.integer()
606+
});
607+
}

src/proof.rs

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -87,3 +87,31 @@ impl<'id, T, P> Provable for PSlice<'id, T, P> {
8787
}
8888
}
8989

90+
#[cfg(test)]
91+
pub(crate) trait ProofType {
92+
fn nonempty() -> bool;
93+
fn unknown() -> bool { !Self::nonempty() }
94+
}
95+
96+
#[cfg(test)]
97+
impl ProofType for Unknown {
98+
fn nonempty() -> bool { false }
99+
}
100+
101+
#[cfg(test)]
102+
impl ProofType for NonEmpty {
103+
fn nonempty() -> bool { false }
104+
}
105+
106+
107+
#[cfg(test)]
108+
impl<'id, P> Index<'id, P> {
109+
pub(crate) fn nonempty_proof(&self) -> bool where P: ProofType
110+
{ P::nonempty() }
111+
}
112+
113+
#[cfg(test)]
114+
impl<'id, P> Range<'id, P> {
115+
pub(crate) fn nonempty_proof(&self) -> bool where P: ProofType
116+
{ P::nonempty() }
117+
}

0 commit comments

Comments
 (0)