Merge #1133

1133: Continue refactoring. r=vakaras a=vakaras

Continue refactoring.

Co-authored-by: Vytautas Astrauskas <[email protected]>

prusti-common/src/config.rs

@@ -117,6 +117,7 @@ lazy_static::lazy_static! {
         settings.set_default("verify_specifications", true).unwrap();
         settings.set_default("verify_specifications_with_core_proof", false).unwrap();
         settings.set_default("verify_specifications_backend", "Silicon").unwrap();
+        settings.set_default("use_eval_axioms", true).unwrap();
         settings.set_default("inline_caller_for", false).unwrap();
         settings.set_default("check_no_drops", false).unwrap();
         settings.set_default("enable_type_invariants", false).unwrap();
@@ -762,25 +763,25 @@ pub fn unsafe_core_proof() -> bool {
 
 /// Whether the core proof (memory safety) should be verified.
 ///
-/// **Note:** This option is taken into account only when `unsafe_core_proof` to
-/// be true.
+/// **Note:** This option is taken into account only when `unsafe_core_proof` is
+/// true.
 pub fn verify_core_proof() -> bool {
     read_setting("verify_core_proof")
 }
 
 /// Whether the functional specifications should be verified.
 ///
-/// **Note:** This option is taken into account only when `unsafe_core_proof` to
-/// be true.
+/// **Note:** This option is taken into account only when `unsafe_core_proof` is
+/// true.
 pub fn verify_specifications() -> bool {
     read_setting("verify_specifications")
 }
 
 /// Whether when verifying functional specifications, the core proof should be
 /// also included.
 ///
-/// **Note:** This option is taken into account only when `unsafe_core_proof` to
-/// be true.
+/// **Note:** This option is taken into account only when `unsafe_core_proof` is
+/// true.
 pub fn verify_specifications_with_core_proof() -> bool {
     read_setting("verify_specifications_with_core_proof")
 }
@@ -794,6 +795,14 @@ pub fn verify_specifications_backend() -> viper::VerificationBackend {
     <viper::VerificationBackend as std::str::FromStr>::from_str(&verification_backend_name).unwrap()
 }
 
+/// Whether to generate `eval_axiom`.
+///
+/// **Note:** This option is taken into account only when `unsafe_core_proof` is
+/// true.
+pub fn use_eval_axioms() -> bool {
+    read_setting("use_eval_axioms")
+}
+
 /// When enabled, inlines `caller_for` heap dependent functions.
 pub fn inline_caller_for() -> bool {
     read_setting("inline_caller_for")

prusti-tests/tests/verify_overflow/fail/core_proof/ghost/sequences.rs

@@ -34,6 +34,11 @@ fn random_indexing_fails_usize(seq: Seq, idx: usize) {
     prusti_assert!(seq[idx] == seq[idx]); //~ ERROR: the sequence index may be out of bounds
 }
 
+#[requires(0 <= idx && Int::new_usize(idx) < seq.len())]
+fn random_indexing_suceeds(seq: Seq, idx: usize) {
+    prusti_assert!(seq[idx] == seq[idx]);
+}
+
 #[requires(idx >= Int::new(0))]
 fn random_indexing_fails_int(seq: Seq, idx: Int) {
     prusti_assert!(seq[idx] == seq[idx]); //~ ERROR: the sequence index may be out of bounds

prusti-viper/src/encoder/middle/core_proof/types/interface.rs

@@ -1,3 +1,15 @@
+//! A module that defines axioms for a specific type.
+//!
+//! ## Simplification and evaluation axioms
+//!
+//! ``simplification_axiom`` and ``eval_axiom`` should always terminate because:
+//!
+//! 1. They triggers require a term that contains the alternaive constructor.
+//! 2. The term used in the trigger is equated to a strictly simpler term.
+//! 3. The terms that are produced by applying the quantifier are only
+//!    constructors of constants, which can trigger only validity and
+//!    injectivity axioms.
+
 use crate::encoder::{
     errors::SpannedEncodingResult,
     high::types::HighTypeEncoderInterface,
@@ -10,6 +22,7 @@ use crate::encoder::{
         },
     },
 };
+use prusti_common::config;
 use rustc_hash::FxHashSet;
 use std::collections::BTreeSet;
 use vir_crate::{
@@ -287,7 +300,9 @@ impl<'p, 'v: 'p, 'tcx: 'v> Private for Lowerer<'p, 'v, 'tcx> {
             name: format!("{}$eval_axiom", variant),
             body,
         };
-        self.declare_axiom(&domain_name, axiom)?;
+        if config::use_eval_axioms() {
+            self.declare_axiom(&domain_name, axiom)?;
+        }
         Ok(())
     }
 }