creusot icon indicating copy to clipboard operation
creusot copied to clipboard

Published 20 hours ago • verified publisher icon creusot-rs

Map

Open xldenis opened this issue 1 year ago • 2 comments

Some more proofs about iterators.

xldenis avatar Sep 13 '22 22:09 xldenis

I've significantly weakend the conditions on the invariant of Map, but this comes at a cost: the proof of next is extremely painful to get to go through, and it seems like instantiating map for closures is trickier than with the simplified versions. If we can remove self.iter.produces(initial.produced.subsequence(self.produced.len(), initial.produced.len()), initial.iter) ==> then it significantly speeds things up. Otherwise perhaps some refactoring could help guide provers?

xldenis avatar Sep 15 '22 23:09 xldenis

I've proved that an identity map and incrementing map are safe but have not yet checked their results (i'm scared of looking at the proofs).

xldenis avatar Sep 15 '22 23:09 xldenis

@jhjourdan I'm going to merge Map despite not having working benchmarks. We can fine tune the spec of map afterwards.

xldenis avatar Sep 20 '22 15:09 xldenis