Feature Proposal: File-scoped/Module-scoped broadcast-forall attribute

[tenzinhl]

Per-file Broadcast foralls

Let's say that I know I'm going to be using a specific data structure within a given refinement proof file over and over again. Say I've developed an algebra around this data structure (an example of this for us is MsgHistory, which is kind of like a list datastructure that can be sliced etc.)

A property of MsgHistory is that slicing works how you'd expect:

a[x:y] + a[y:z] = a[x:z]

However verus does not believe this without proof since MsgHistory is built containing a map, and we know that map extensionality arguments need to be made manually. So you write the lemma and then use it.

This property feels very natural however and when writing a bunch of proofs it's easy to forget to re-call the lemma (and it can take some time to figure out that you need to call it). It feels like something that we want always available when working frequently with it.

That being said: there will still be many files (a majority) where it is not relevant for us to have access to this property at all. Thus I think per-file broadcast-forall's (could even make them block/module scoped if you want to get fancy) provide a good level of granularity for limiting pollution of the triggers available to the verifier while also allowing users to call and forget once per file/module for frequently used lemmas.

[parno]

One way to do this might be by giving the library developer (in this case, the developer of the MsgHistory library) the ability to define multiple "export sets" of types, functions, lemmas, etc. One export set might be MsgHistory::auto that includes a bunch of useful broadcast-foralls, while another might be a more conservative MsgHistory::std without those lemmas. Then consumers could choose which one they want to import and hence determine how much automation/context-pollution they want.

Judging from our Dafny experience, this would also be quite useful for the sequence library, where we typically want the convenience of the automation, but occasionally we want to turn it off when we're in the midst of a difficult proof.

[Chris-Hawblitzel]

I'd love to have these kind of import/export sets for broadcast_forall. There's been some discussion on #37 , but it's been a while since we've looked at the details. I think we can be much more flexible about the syntax now. Maybe in the meeting tomorrow we can discuss prioritization a little bit.

[utaal]

Moved into #37.