Add one prelude axiom to be identified in axiom-usage-info (#1397)

The proof of concrete sequence sorted by mergesort requires a prelude axiom, which is not reflected by verus -V broadcast-usage-info before, as the verus will only take the named axioms in unsat-core. We named one axiom in air prelude (which seems to be the only one not about unboxing/boxing conversions or has_type).

We also changed broadcast-usage-info to axiom-usage-info to match the vargo build option (vargo build --features axiom-usage-info)

---

Co-authored-by: Andrea Lattuada <andrea@mpi-sws.org>

source/rust_verify/src/config.rs

@@ -106,7 +106,7 @@ pub struct ArgsX {
     pub use_crate_name: bool,
     pub solver: SmtSolver,
     #[cfg(feature = "axiom-usage-info")]
-    pub broadcast_usage_info: bool,
+    pub axiom_usage_info: bool,
 }
 
 impl ArgsX {
@@ -150,7 +150,7 @@ impl ArgsX {
             use_crate_name: Default::default(),
             solver: Default::default(),
             #[cfg(feature = "axiom-usage-info")]
-            broadcast_usage_info: Default::default(),
+            axiom_usage_info: Default::default(),
         }
     }
 }
@@ -280,7 +280,7 @@ pub fn parse_args_with_imports(
     const EXTENDED_ALLOW_INLINE_AIR: &str = "allow-inline-air";
     const EXTENDED_USE_CRATE_NAME: &str = "use-crate-name";
     #[cfg(feature = "axiom-usage-info")]
-    const EXTENDED_BROADCAST_USAGE_INFO: &str = "broadcast-usage-info";
+    const EXTENDED_AXIOM_USAGE_INFO: &str = "axiom-usage-info";
     const EXTENDED_KEYS: &[(&str, &str)] = &[
         (EXTENDED_IGNORE_UNEXPECTED_SMT, "Ignore unexpected SMT output"),
         (EXTENDED_DEBUG, "Enable debugging of proof failures"),
@@ -304,10 +304,7 @@ pub fn parse_args_with_imports(
             "Use the crate name in paths (useful when verifying vstd without --export)",
         ),
         #[cfg(feature = "axiom-usage-info")]
-        (
-            EXTENDED_BROADCAST_USAGE_INFO,
-            "Print usage info for broadcasted axioms, lemmas, and groups",
-        ),
+        (EXTENDED_AXIOM_USAGE_INFO, "Print usage info for broadcasted axioms, lemmas, and groups"),
     ];
 
     let default_num_threads: usize = std::thread::available_parallelism()
@@ -652,7 +649,7 @@ pub fn parse_args_with_imports(
         use_crate_name: extended.get(EXTENDED_USE_CRATE_NAME).is_some(),
         solver: if extended.get(EXTENDED_CVC5).is_some() { SmtSolver::Cvc5 } else { SmtSolver::Z3 },
         #[cfg(feature = "axiom-usage-info")]
-        broadcast_usage_info: extended.get(EXTENDED_BROADCAST_USAGE_INFO).is_some(),
+        axiom_usage_info: extended.get(EXTENDED_AXIOM_USAGE_INFO).is_some(),
     };
 
     (Arc::new(args), unmatched)

source/rust_verify/src/verifier.rs

@@ -1127,7 +1127,7 @@ impl Verifier {
             air_context.set_z3_param(&option, &value);
         }
         #[cfg(feature = "axiom-usage-info")]
-        if self.args.broadcast_usage_info {
+        if self.args.axiom_usage_info {
             air_context.enable_usage_info();
         }
 
@@ -1595,6 +1595,10 @@ impl Verifier {
                                     let axioms_list = used_axioms
                                         .iter()
                                         .map(|x| {
+                                            if x.starts_with(vir::def::AXIOM_NAME_PRELUDE) {
+                                                return format!("  - (prelude) {}", x);
+                                            }
+
                                             let funx = &function_opgen.ctx().fun_ident_map[x];
                                             let is_reveal_group = krate
                                                 .reveal_groups

source/vir/src/def.rs

@@ -221,6 +221,9 @@ pub const PERVASIVE_PREFIX: &str = "pervasive::";
 
 pub const RUST_DEF_CTOR: &str = "ctor%";
 
+// used by axiom-usage-info to identify axioms from the prelude
+pub const AXIOM_NAME_PRELUDE: &str = "prelude_axiom_";
+
 // List of pre-defined error messages
 pub const ASSERTION_FAILURE: &str = "assertion failure";
 pub const PRECONDITION_FAILURE: &str = "precondition not satisfied";
@@ -662,6 +665,11 @@ pub fn snapshot_ident(name: &str) -> Ident {
     Arc::new(format!("{}{}", PREFIX_SNAPSHOT, name))
 }
 
+// only used by axiom-usage-info to identify prelude axioms
+pub fn prelude_axiom_name(name: &str) -> String {
+    format!("{AXIOM_NAME_PRELUDE}{name}")
+}
+
 /// For a given snapshot, does it represent the state
 /// at the start of the corresponding span, the end, or the full span?
 #[derive(Debug)]

source/vir/src/prelude.rs

@@ -748,6 +748,7 @@ pub(crate) fn array_functions(box_array: &str) -> Vec<Node> {
     let type_id_const_int = str_to_node(TYPE_ID_CONST_INT);
     #[allow(non_snake_case)]
     let Poly = str_to_node(POLY);
+    let prelude_axiom_array_index = str_to_node(&prelude_axiom_name("array_index"));
 
     nodes_vec!(
         // array literals
@@ -794,12 +795,16 @@ pub(crate) fn array_functions(box_array: &str) -> Vec<Node> {
         // Rewrite as ([array_index] ...), which vstd can more easily trigger on.
         // (Note that there's no axiom in the reverse direction converting array_index to apply,
         // because that would create a matching loop on i via I and %I.)
-        (axiom (forall ((Tdcr [decoration]) (T [typ]) (N Int) (Fn Fun) (i Int)) (!
+        (axiom (!
+            (forall ((Tdcr [decoration]) (T [typ]) (N Int) (Fn Fun) (i Int)) (!
             (= ([array_index] Tdcr T $ ([type_id_const_int] N) Fn (I i)) (apply [Poly] Fn i))
             :pattern (([array_new] Tdcr T N Fn) (apply [Poly] Fn i))
             :qid prelude_array_index_trigger
             :skolemid skolem_prelude_array_index_trigger
-        )))
+            ))
+            :named
+            [prelude_axiom_array_index]
+        ))
     )
 }