Skip to content

Commit be9d4f4

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 be9d4f4

File tree

2 files changed

+69
-1
lines changed

2 files changed

+69
-1
lines changed

src/indexing.rs

Lines changed: 41 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -178,7 +178,28 @@ 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!(arr[ix]); //~ ERROR Can't index by ix, because it's an edge index
197+
/// });
198+
/// ```
199+
// Proof P: Extends at least as far as self, not necessarily using any part
200+
// of other
201+
//
202+
pub fn join_cover<Q>(&self, other: Range<'id, Q>) -> Range<'id, P>
182203
where (P, Q): ProofAdd,
183204
{
184205
let end = cmp::max(self.end, other.end);
@@ -188,6 +209,7 @@ impl<'id, P> Range<'id, P> {
188209
}
189210

190211
/// Extend the range to start and end of `other`, including any space in between
212+
// Proof Sum of P and Q: Covers the union, so must be nonempty if any are
191213
pub fn join_cover_both<Q>(&self, other: Range<'id, Q>) -> Range<'id, <(P, Q) as ProofAdd>::Sum>
192214
where (P, Q): ProofAdd,
193215
{
@@ -563,3 +585,21 @@ fn test_frac_step() {
563585
assert_eq!(f.next(), None);
564586
}
565587

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

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)