Rel: make progress checking in head_matches_delta stricter

FStarLang / FStar

A Proof-oriented Programming Language

https://www.fstar-lang.org

Apache License 2.0

2.65k stars 232 forks source link

Rel: make progress checking in head_matches_delta stricter #3297

Closed mtzguido closed 1 month ago

mtzguido commented 1 month ago

Fixes a regression in DICE* reported by @aseemr. I think this may have popped up when we did the fv_delta change (#3272), but the offending code is there since before.

I am running a local everest build before merging.

mtzguido commented 1 month ago

Everest came back green, merging.