Too Many Assertions

[jonhnet]

I have a module with two pairs of mutually-recursive definitions, can_crop_head_records and crop_head_records. In the inductive proofs of can_crop_monotonic and can_crop_more_yields_some, I had to add explicit assertion triggers to instantiate the "other half" of the corresponding definitions.

Dafny didn't need that extra help. The finished proofs are quite a lot more cluttered, and the discovery process was painful. I did get diagnostics that said Note: this function is recursive with fuel 1, which helped me guess the problem, but I don't think that would be much help to a new user.

Repro:

git clone github.com:vmware-labs/verified-betrfs.git
git checkout c8b125cc0e3f2f0580d34736f46152cc3259331c
clear; time /home/jonh/verus-rust/source/tools/rust-verify.sh src/bundle.rs --verify-module journal::PagedJournal_v --time --expand-errors --multiple-errors 65

[jonhnet]

If you want to browse a preview, here are the lemmas that needed help.

[utaal]

We are working towards a-la-carte additional automation, that will hopefully help address this.