Generalized lemma broadcast, implements #37

[utaal-b]

This implements #37:

• a mechanism to produce quantified axioms from regular lemmas, broadcast proof fns,
• an accompanying mechanism to import these quantified facts (broadcast use) at either the module or function level, and
• a mechanism to construct groups of broadcast proof fns that can be broadcast used (broadcast group).

The underlying implementation uses the fuel mechanism that was already implemented for broadcast_forall, but extends it to allow the construction of groups and the ability to broadcast use at the module level.

Here's an example:

    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 succ_ensures(p: Ring)
                requires p.inv()
                ensures p.inv() && (#[trigger] p.succ()).prev() == p
            { }

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

            pub broadcast group properties {
                Ring::succ_ensures,
                Ring::prev_ensures,
            }
        }
    }

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

            proof fn t2(p: Ring) requires p.inv() {
                broadcast use Ring::succ_ensures;
                assert(p.succ().prev() == p);
            }

            proof fn t3(p: Ring) requires p.inv() {
                broadcast use Ring::succ_ensures;
                assert(p.succ().prev() == p);
                assert(p.prev().succ() == p); // FAILS
            }

            proof fn t4(p: Ring) requires p.inv() {
                assert(p.prev().succ() == p); // FAILS
            }

            proof fn t5(p: Ring) requires p.inv() {
                broadcast use Ring::succ_ensures, Ring::prev_ensures;
                assert(p.succ().prev() == p);
                assert(p.prev().succ() == p);
            }

            proof fn t6(p: Ring) requires p.inv() {
                broadcast use Ring::properties;
                assert(p.succ().prev() == p);
                assert(p.prev().succ() == p);
            }
    }

A significant part of this PR are syntax additions.

The most important from a soundness perspective are the additional function graph nodes and edges that represent groups and module-level reveals, to prevent circular reasoning. In particular:

https://github.com/verus-lang/verus/pull/1022/files#diff-b7fce60d4dba89afe470adb93f36bbc6d33da444e711c78c476970e52dee9105R322-R351

verus/source/vir/src/context.rs

Lines 322 to 351 in 852db35

	for group in &krate.reveal_groups {
	let group_node = Node::Fun(group.x.name.clone());
	func_call_graph.add_node(group_node.clone());
	for member in group.x.members.iter() {
	let target = Node::Fun(member.clone());
	func_call_graph.add_node(target.clone());
	func_call_graph.add_edge(group_node.clone(), target);
	}
	}
	for module in &krate.modules {
	if let Some(ref reveals) = module.x.reveals {
	let module_reveal_node = Node::ModuleReveal(module.x.path.clone());
	func_call_graph.add_node(module_reveal_node.clone());
	for fun in reveals.x.iter() {
	let target = Node::Fun(fun.clone());
	func_call_graph.add_node(target.clone());
	func_call_graph.add_edge(module_reveal_node.clone(), target);
	}
	for f in krate
	.functions
	.iter()
	.filter(|f| f.x.owning_module.as_ref() == Some(&module.x.path))
	{
	let source = Node::Fun(f.x.name.clone());
	func_call_graph.add_node(source.clone());
	func_call_graph.add_edge(source, module_reveal_node.clone());
	}
	}
	}

and

https://github.com/verus-lang/verus/pull/1022/files#diff-b7fce60d4dba89afe470adb93f36bbc6d33da444e711c78c476970e52dee9105R602-R622

verus/source/vir/src/context.rs

Lines 602 to 622 in 852db35

	for group in &self.reveal_groups {
	names.push(group.x.name.clone());
	}
	for name in names {
	let id = crate::def::prefix_fuel_id(&fun_to_air_ident(&name));
	ids.push(air::ast_util::ident_var(&id));
	let decl = Arc::new(DeclX::Const(id, str_typ(&FUEL_ID)));
	commands.push(Arc::new(CommandX::Global(decl)));
	}
	let distinct = Arc::new(air::ast::ExprX::Multi(MultiOp::Distinct, Arc::new(ids)));
	let decl = Arc::new(DeclX::Axiom(distinct));
	commands.push(Arc::new(CommandX::Global(decl)));
	for group in &self.reveal_groups {
	crate::func_to_air::broadcast_forall_group_axioms(
	self,
	&mut commands,
	group,
	&self.global.crate_name,
	);
	}
	crate::func_to_air::module_reveal_axioms(self, &mut commands, &self.module.x.reveals);

The PR also introduces two attributes for broadcast groups:

• #[verifier::hidden_unless_this_module_is_used] which instructs prune to remove the broadcasted axioms if this broadcast group was used indirectly but nothing else in the module was used (this is to preserve the existing pruning mechanism in vstd);

• #[verifier::broadcast_use_by_default_when_this_crate_is_imported] which can be used to tag a default broadcast group for a crate (currently intended for vstd) that will be automatically broadcast used in dependent crates.

---

A follow-on PR, #1023, uses this mechanism to replace the existing, unconditional broadcast via #[verifier::broadcast_forall] #[verifier::external_body].

[tjhance]

#[verifier::hidden_unless_this_module_is_used] which instructs prune to remove the broadcasted axioms if this broadcast group was used indirectly but nothing else in the module was used (this is to preserve the existing pruning mechanism in vstd);

I don't get what this means. What does it mean for a group to be used "indirectly"? What's an example where this changes behavior?

[utaal-b]

What does it mean for a group to be used "indirectly"? What's an example where this changes behavior?

That could have been phrased better (by me). A crate has a #[verifier::broadcast_use_by_default_when_this_crate_is_imported] which will broadcast use a default group. For vstd, this will be the equivalent group to the current broadcast_forall axioms, but those get pruned if nothing else in the module they appear in was used, so #[verifier::hidden_unless_this_module_is_used] will instruct the pruner to prune the broadcast proofs in this group unless the current module is used (to preserve the current behavior for the vstd axioms).

In fact, I meant to rename that to prune_unless_this_module_is_used. Let me do that.

[utaal-b]

This will be mergeable once verus-lang/verusfmt#48 is merged so that verusfmt passes.

[jaybosamiya]

verus-lang/verusfmt#48 is merged (thanks for making the PR @utaal-b!), and new version of verusfmt (v0.2.10) is released, so the CI should now pass here. Triggered a re-run of the failed CI, hopefully should be a green!