From 75a424748c5ea5ba6e60975c0ae06c28c15898c2 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Thu, 26 Mar 2026 15:04:59 -0400 Subject: [PATCH] feat: make requires and assumptions optional Some specs do not have requires, and some invariants do not have assumptions. Logically, these can be set to TRUE, but syntactically, it is convenient to omit them in these cases. --- cvlr-spec/src/macros.rs | 47 ++++++++++++++++++++++++++---- cvlr-spec/tests/test_spec.rs | 55 ++++++++++++++++++++++++++++++++++++ 2 files changed, 97 insertions(+), 5 deletions(-) diff --git a/cvlr-spec/src/macros.rs b/cvlr-spec/src/macros.rs index b2cf1d8..9fb4307 100644 --- a/cvlr-spec/src/macros.rs +++ b/cvlr-spec/src/macros.rs @@ -611,17 +611,23 @@ macro_rules! cvlr_rules { /// requires: requires_expression, /// ensures: ensures_expression, /// } +/// +/// // Or omit `requires` to use [`cvlr_true`](crate::cvlr_true) as the precondition: +/// cvlr_spec! { +/// ensures: ensures_expression, +/// } /// ``` /// /// # Parameters /// -/// * `requires` - A boolean expression over the context type representing the precondition +/// * `requires` (optional) - A boolean expression over the context type representing the precondition. +/// If omitted, [`cvlr_true`](crate::cvlr_true) is used for the same context as `ensures`. /// * `ensures` - A boolean expression over the context type that uses [`eval_with_states`](crate::CvlrFormula::eval_with_states) /// to evaluate over both pre-state and post-state /// /// # Returns /// -/// Returns a value implementing [`CvlrSpec`](crate::spec::CvlrSpec) with the same context type as the requires expression. +/// Returns a value implementing [`CvlrSpec`](crate::spec::CvlrSpec) with the same context type as the `ensures` expression. /// /// # Examples /// @@ -656,6 +662,9 @@ macro_rules! cvlr_spec { (requires: $r:expr, ensures: $e:expr $(,)?) => { $crate::cvlr_spec($r, $e) }; + (ensures: $e:expr $(,)?) => { + $crate::cvlr_spec($crate::cvlr_true::<_>(), $e) + }; } /// Creates an invariant specification from an assumption and an invariant. @@ -674,16 +683,22 @@ macro_rules! cvlr_spec { /// assumption: assumption_expression, /// invariant: invariant_expression, /// } +/// +/// // Or omit `assumption` to use [`cvlr_true`](crate::cvlr_true) as the extra precondition: +/// cvlr_invar_spec! { +/// invariant: invariant_expression, +/// } /// ``` /// /// # Parameters /// -/// * `assumption` - A boolean expression representing an additional precondition +/// * `assumption` (optional) - A boolean expression representing an additional precondition. +/// If omitted, [`cvlr_true`](crate::cvlr_true) is used for the same context as `invariant`. /// * `invariant` - A boolean expression representing an invariant that must hold before and after /// /// # Returns /// -/// Returns a value implementing [`CvlrSpec`](crate::spec::CvlrSpec) with the same context type as the assumption expression. +/// Returns a value implementing [`CvlrSpec`](crate::spec::CvlrSpec) with the same context type as the `invariant` expression. /// /// # Examples /// @@ -710,6 +725,9 @@ macro_rules! cvlr_invar_spec { (assumption: $a:expr, invariant: $i:expr $(,)?) => { $crate::cvlr_invar_spec($a, $i) }; + (invariant: $i:expr $(,)?) => { + $crate::cvlr_invar_spec($crate::cvlr_true::<_>(), $i) + }; } /// Defines multiple rules for an invariant specification across multiple base functions. @@ -732,12 +750,20 @@ macro_rules! cvlr_invar_spec { /// base_function3, /// ] /// } +/// +/// // `assumption` may be omitted (uses [`cvlr_true`](crate::cvlr_true)): +/// cvlr_invariant_rules! { +/// name: "rule_name", +/// invariant: invariant_expression, +/// bases: [ base_function1 ] +/// } /// ``` /// /// # Parameters /// /// * `name` - A string literal that will be converted to snake_case and combined with each base function name -/// * `assumption` - A boolean expression representing an additional precondition +/// * `assumption` (optional) - A boolean expression representing an additional precondition. +/// If omitted, [`cvlr_true`](crate::cvlr_true) is used for the same context as `invariant`. /// * `invariant` - A boolean expression representing an invariant that must hold before and after /// * `bases` - A list of function identifiers (if they start with `base_`, that prefix is stripped) /// @@ -760,6 +786,8 @@ macro_rules! cvlr_invar_spec { /// cvlr_rule_for_spec!{name: "non_negative", spec: cvlr_invar_spec(assumption_expr, invariant_expr), base: base_function2} /// ``` /// +/// If `assumption` is omitted, `cvlr_invar_spec(cvlr_true::<_>(), invariant_expr)` is used instead. +/// /// # Examples /// /// ```ignore @@ -801,6 +829,15 @@ macro_rules! cvlr_invariant_rules { } )* }; + (name: $name:literal, invariant: $i:expr, bases: [ $( $base:ident ),* $(,)? ] ) => { + $( + $crate::__macro_support::cvlr_rule_for_spec!{ + name: $name, + spec: $crate::spec::cvlr_invar_spec($crate::cvlr_true::<_>(), $i), + base: $base + } + )* + }; } /// Creates a boolean expression representing the logical AND of two or more expressions. diff --git a/cvlr-spec/tests/test_spec.rs b/cvlr-spec/tests/test_spec.rs index 43e6a7e..b85ea95 100644 --- a/cvlr-spec/tests/test_spec.rs +++ b/cvlr-spec/tests/test_spec.rs @@ -1027,6 +1027,31 @@ fn test_cvlr_spec_macro() { spec.check_ensures(&post, &pre); // Should assert YPositive holds for post } +#[test] +fn test_cvlr_spec_macro_omitted_requires() { + let spec_macro = cvlr_spec! { + ensures: YPositive, + }; + let spec_fn = cvlr_spec(cvlr_true::(), YPositive); + + let pre_bad = TestCtx { + x: -1, + y: 0, + flag: false, + }; + let post_ok = TestCtx { + x: -1, + y: 10, + flag: false, + }; + + // No precondition: assume_requires is a no-op for the macro form + spec_macro.assume_requires(&pre_bad); + spec_fn.assume_requires(&pre_bad); + spec_macro.check_ensures(&post_ok, &pre_bad); + spec_fn.check_ensures(&post_ok, &pre_bad); +} + #[test] fn test_cvlr_spec_macro_with_predicates() { // Test cvlr_spec! macro with cvlr_predicate! @@ -1071,6 +1096,25 @@ fn test_cvlr_invar_spec_macro() { spec.check_ensures(&ctx, &ctx); } +#[test] +fn test_cvlr_invar_spec_macro_omitted_assumption() { + let spec_macro = cvlr_invar_spec! { + invariant: YPositive, + }; + let spec_fn = cvlr_invar_spec(cvlr_true::(), YPositive); + + let ctx_bad_x = TestCtx { + x: -1, + y: 10, + flag: false, + }; + + spec_macro.assume_requires(&ctx_bad_x); + spec_fn.assume_requires(&ctx_bad_x); + spec_macro.check_ensures(&ctx_bad_x, &ctx_bad_x); + spec_fn.check_ensures(&ctx_bad_x, &ctx_bad_x); +} + #[test] fn test_cvlr_invar_spec_macro_with_predicates() { // Test cvlr_invar_spec! macro with cvlr_predicate! @@ -1200,6 +1244,17 @@ fn test_cvlr_invariant_rules_macro_single_base() { } } +#[test] +fn test_cvlr_invariant_rules_macro_omitted_assumption() { + cvlr_invariant_rules! { + name: "invar_no_assume", + invariant: YPositive, + bases: [ + base_single_function, + ] + } +} + // Tests for cvlr_and! macro #[test] fn test_cvlr_and_macro_with_identifiers() {