When working with trait implementations, I sometimes get silly failures that can be resolved by asserting (inside the fn body) the requires or ensures expression that the fn should have inherited from the trait definition. These assertions should never be necessary because the requires or ensures expression should be providing the necessary triggering mentions.
Here is a recorded example. In the recording, VariableSizedElementSeq_v.rs:146 fn try_length fails with both pre- and post-condition failures. If you uncomment the assertions on lines 148, 149, and 151, this fn passes verification.
The precondition failure is a little different than what I wrote above. Uncommenting just 148 (the literal precondition) isn't sufficient, but uncommenting line 149 (which appears as the first conjunct of the precondition at line 132 in the same file) provides the necessary trigger. This still should have been "discovered" by mentioning seq_valid; I think it's related.
When working with trait implementations, I sometimes get silly failures that can be resolved by asserting (inside the fn body) the requires or ensures expression that the fn should have inherited from the trait definition. These assertions should never be necessary because the requires or ensures expression should be providing the necessary triggering mentions.
Here is a recorded example. In the recording, VariableSizedElementSeq_v.rs:146
fn try_lengthfails with both pre- and post-condition failures. If you uncomment the assertions on lines 148, 149, and 151, this fn passes verification.The precondition failure is a little different than what I wrote above. Uncommenting just 148 (the literal precondition) isn't sufficient, but uncommenting line 149 (which appears as the first conjunct of the precondition at line 132 in the same file) provides the necessary trigger. This still should have been "discovered" by mentioning seq_valid; I think it's related.
2024-05-31-09-07-43.zip
I've seen this problem not infrequently, but haven't found a consistent initial condition, hence the recording.