Import sets for ambient lemmas/axioms

[utaal]

NOTE: This initial design is outdated, and uses outdates syntax.

@Chris-Hawblitzel, @jonhnet, and I discussed allowing control over automation by providing multiple import sets for ambient lemmas/axioms (global foralls), in part inspired by how some rust libraries re-export traits.

To access a function defined as an impl for a certain trait, in Rust, you import the trait name, and get all the functions it defines as methods on objects with types that implement the trait. This is sometimes used to provide multiple import sets, sometimes including a “prelude” with some default imports, by constructing a module that re-exports various trait identifiers.

Here's an example:

mod a {
    trait A {
        fn doo(&self) -> u64;
    }
    impl A for u64 {
        fn doo(&self) -> u64 { unimplemented!() }
    }
}

mod b {
    trait B {
        fn foo(&self) -> bool;
    }
    impl B for u64 { ... }
}

mod c {
    pub use crate::a::*;
    pub use crate::b::*;   
}

// importing `c` makes both `doo` and `foo` available for u64s.

This would allow library authors to provide different levels of automation, with pre-packaged import sets of increasing power, and also allows the user to switch to a less "dangerous" set of foralls, and then selectively import the ones they need (or they can decide to call the lemmas explicitly).

We considered what the syntax may look like:

// set.rs
#[proof] #[forall]
pub fn some_axiom()

// 
pub fn module_A() {
    use set::*;
}

pub fn module_C() {
    use module_A;
}

#[axiom_import]
fn axiom_import() {
    axiom_use(some_axiom);
}

axiom_import!(some_axiom); // allow(dead_code)

macro_rules! some_axiom {
    
}

[tjhance]

Recording these notes from chris for posterity:

The reason [a broadcast_forall function must be external_body] is to limit broadcast_forall to trusted axioms for the moment. And one reason for this is for untrusted lemmas, we need to make sure that there are no cycles in the lemmas. Since broadcast_forall goes into global scope, it matters what order we emit the lemmas in SMT. At the very least, if a broadcast_forall lemma b explicitly calls a lemma a, then a should precede b in the SMT. If a broadcast_forall lemma b2 implicitly depends on another broadcast_forall lemma b1, it's not obvious to Verus that b1 should precede b2 , so there's an interesting design question in this case. (In F*, this isn't an issue, because unlike Rust, F* declarations must appear in order in the source code.)

Basically, to implement broadcast_forall for non-trusted axioms, Verus's termination checker needs a way to determine which lemmas are allowed to depend on a given broadcast_forall. It's likely that the import set concept here will play a role in that.

[utaal]

Tracking of libraries we may want to include:

• nonlinear/multiplication lemmas for non "regular" code (with smt.arith.nl set to false), e.g.https://github.com/microsoft/Ironclad/blob/main/ironfleet/src/Dafny/Libraries/Math/mul_auto.i.dfy

[chanheec]

Bit-vector lemmas for bounded integers (integers in normal query) (https://github.com/secure-foundations/verus/blob/main/source/rust_verify/example/bitvector_basic.rs)

[matthias-brun]

This feature would be useful in the page table verification project. Currently I'm using multiple lemmas with very general postconditions, which I call separately at the beginning of a lemma. I'd like to group them into one or more larger lemmas that simply re-export the postconditions but currently I have to re-state every postcondition I want to have on such a "collection lemma". This is possible but inconvenient. In particular re-exporting would make it easier to experiment with different collections of lemmas or to have multiple versions of them.

[utaal]

@tenzinhl (from #560):

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.

[utaal]

@parno (from #560 (comment)):

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.

[utaal]

@Chris-Hawblitzel (from #560 (comment)):

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]

Notes from the [Verus all-hands]:

• Import sets inspired by the pattern of importing traits in Rust
• Re-exporting groups together also would work
• Plan: allow library authors to construct sets of lemmas that you can import as context, either at level of certain proof function, or at level of a module
• Complications around well-ordering of lemmas, and well-foundedness consideration wrt soundness
• Intent: something that is a regular lemma becomes a broadcasted lemma
• What about triggers?
  • If you want to be able to do this, you might have to specify triggers, at point of definition (where you’d mark the lemma as exportable)
• We’re not using use as syntax; will be orthogonal to namespacing
• Think kinda like _auto lemmas but with nice support/syntax for the following operations
  1. Converting a lemma to an _auto lemma
  2. Unioning multiple _auto lemmas together
  3. Importing/exposing an _auto lemma set at module level (i.e., at all functions within it)
  4. Importing/exposing an _auto lemma set at function level
• Look into related “hint databases” in Coq (affects the auto tactic on Coq)
• Singleton is also a set
• Subtraction might not be part of first cut, but would be very good for later on
• Need to also make sure that things like “length of empty sequence is zero” would still be importable
• Also need to think about reveal for opaque, and have reveal sets
  • Can handle this by having lemmas of the kind f == f.body or similar; or by introducing a new keyword specifically for reveals?
• Useful feature: which lemmas were used for this?

[utaal-b]

There is a work-in-progress implementation at https://github.com/verus-lang/verus/tree/reveal_group

Here is a concrete syntax proposal, after discussion with @Chris-Hawblitzel (he suggested the lemma_call(*) syntax to invoke the "_auto" version of a lemma.

mod ring {
    use builtin::*;

    pub struct Ring {
        pub i: nat,
    }

    impl Ring {
        pub closed spec fn inv(&self) -> bool {
            self.i < 10
        }

        pub closed spec fn succ(&self) -> Ring {
            Ring { i: if self.i == 9 { 0 } else { self.i + 1 } }
        }

        pub closed spec fn prev(&self) -> Ring {
            Ring { i: if self.i == 0 { 9 } else { (self.i - 1) as nat } }
        }
    }

    pub broadcast proof fn Ring_succ(p: Ring)
        requires p.inv()
        ensures p.inv() && (#[trigger] p.succ()).prev() == p
    { }

    pub broadcast proof fn Ring_prev(p: Ring)
        requires p.inv()
        ensures p.inv() && (#[trigger] p.prev()).succ() == p
    { }

    pub broadcast group Ring_properties (
        Ring_succ,
        Ring_prev,
    )
    
    pub broadcast group Ring_less_properties (
        Ring_properties,
        remove Ring_prev,
    )
}

mod m1 {
    use crate::ring::*;

    proof fn p1(p: Ring) {
        Ring_succ(p);
        assert(p.succ().prev() == p);
    }

    proof fn p2(p: Ring) {
        Ring_succ(*);
        assert(p.succ().prev() == p);
    }
    
    proof fn p3(p: Ring) {
        Ring_properties(*);
        assert(p.succ().prev() == p);
        assert(p.prev().succ() == p);
    }
}

mod m2 {
    use crate::ring::*;

    broadcast ( // module-level
        Ring_prev,
        Ring_succ,
    )

    proof fn p3(p: Ring) {
        assert(p.succ().prev() == p);
        assert(p.prev().succ() == p);
    }
}

[Chris-Hawblitzel]

Here are some slight variations on the syntax proposed above:

    pub broadcast group Ring_properties {
        Ring_succ,
        Ring_prev,
    }

    broadcast use Ring_properties;

    broadcast use {Ring_prev, Ring_succ};

Subtraction could be supported outside of groups as well, like the current hide syntax. I expect it would be rarely used, but we should probably have a plan for the syntax. For example:

    broadcast remove Ring_prev;

    proof fn p2(p: Ring) {
        broadcast remove Ring_prev;
        Ring_succ(*);
        assert(p.succ().prev() == p);
    }

In the implementation, broadcast is just a way of manipulating fuel, like reveal. In fact, reveal(f);, broadcast use f;, and f(*); are all semantically equivalent. Do we want to allow these as synonyms? Is this too much redundancy? Do we want to restrict reveal(f); to opaque functions and broadcast use f; and f(*); to broadcast functions/groups, even though reveal is semantically the same as broadcast? Is it ok that broadcast use f; and f(*); are synonyms inside functions? Or do we want to restrict broadcast use f; to the module level and f(*); to the function level, even though the (rarely seen) broadcast remove f; could be used at either the module level or function level?

[utaal-b]

I like these!

Is the proposed syntax for removal when defining a group

pub broadcast group Ring_less_properties {
    Ring_properties,
    remove Ring_prev,
}

?

And I really like broadcast use, but perhaps, for consistency with use, we can do:

broadcast use Ring_properties;

broadcast use Ring_prev, Ring_succ;

?

Do we want to allow these as synonyms? Is this too much redundancy?

I have a preference for having only one way to access a feature, to reduce the risk that one may interpret reveal and broadcast use as doing two (perhaps subtly) different things.

Do we want to restrict reveal(f); to opaque functions and broadcast use f; and f(*); to broadcast functions/groups, even though reveal is semantically the same as broadcast?

I'd say so, for the motivation above.

Is it ok that broadcast use f; and f(*); are synonyms inside functions?

This seems okay to me.

[utaal-b]

I thought I had a slight preference for parentheses () instead of braces {} for the broadcast group definition, but on second thought, I think braces are more than fine.

[Chris-Hawblitzel]

Is the proposed syntax for removal when defining a group

pub broadcast group Ring_less_properties {
    Ring_properties,
    remove Ring_prev,
}

yes

And I really like broadcast use, but perhaps, for consistency with use, we can do:

broadcast use Ring_properties;

broadcast use Ring_prev, Ring_succ;

Ah, yes, that makes more sense than what I wrote. I was intending to be consistent with use, but I got the syntaxes mixed up.

[utaal]

This feature is now largely implemented. More work is necessary in determining which (if any) other broadcast groups we should offer in vstd among other things.