Skip to content

Commit

Permalink
test: stack underflow i/o sequence properties
Browse files Browse the repository at this point in the history
  • Loading branch information
jan-ferdinand committed Oct 23, 2023
1 parent eea37ca commit 4efffde
Showing 1 changed file with 17 additions and 0 deletions.
17 changes: 17 additions & 0 deletions triton-vm/src/op_stack.rs
Original file line number Diff line number Diff line change
Expand Up @@ -360,6 +360,7 @@ impl From<&OpStackElement> for BFieldElement {

#[cfg(test)]
mod tests {
use proptest::collection::vec;
use proptest::prelude::*;
use proptest_arbitrary_interop::arb;
use twenty_first::shared_math::b_field_element::BFieldElement;
Expand Down Expand Up @@ -487,4 +488,20 @@ mod tests {
assert!(shrinks_stack ^ grows_stack);
}
}

proptest! {
#[test]
fn non_empty_uniform_underflow_io_sequence_is_either_reading_or_writing(
sequence in vec(arb::<UnderflowIO>(), 1..OpStackElement::COUNT),
) {
let is_reading_sequence = UnderflowIO::is_reading_sequence(&sequence);
let is_writing_sequence = UnderflowIO::is_writing_sequence(&sequence);
if UnderflowIO::is_uniform_sequence(&sequence) {
prop_assert!(is_reading_sequence ^ is_writing_sequence);
} else {
prop_assert!(!is_reading_sequence);
prop_assert!(!is_writing_sequence);
}
}
}
}

0 comments on commit 4efffde

Please sign in to comment.