annotations: calculus annotations (wp,ert,wlp) #7

umutdural · 2024-01-04T14:54:48Z

Implemented the system to add calculus annotations and implemented three main calculi:

wp
wlp
ert

These annotations can be used only on top of procedures at the moment in the following format:

@wp
proc main() -> () {
    ...
}

Calculus annotations allow or reject certain proof rule encodings depending on the calculi that the proof rule argue about.

For example k-induction is a proof rule that proves an upper bound on the wp of the program. Therefore using k-induction in a proc (lower bound reasoning) is invalid. If the proc is annotated with @wp, Caesar will reject the file and throw an error. On the other hand, coproc (upper bound reasoning) with @wp allows @k_induction(...) annotations inside the procedure.

Technical:

To implement a new calculus annotation, one must create a new struct for the annotation in the src/calculi directory and this struct should implement the Calculus trait, which requires a simple name function and a check_encoding function that returns a Result<(),()> based on the given encoding annotation and direction. Afterward the corresponding declaration of the annotation must happen in the init_calculi function.

Philipp15b

Thanks for your PR! I left some comments about simplifying the code.

Philipp15b · 2024-01-04T16:08:56Z

src/calculi/mod.rs

@@ -0,0 +1,121 @@
+mod ert;


Please add a module comment in this file outlining what the module does (introducing the calculus annotations and that they check which proof rules can be used where).

Philipp15b · 2024-01-04T16:11:14Z

src/calculi/mod.rs

+pub trait Calculus: fmt::Debug {
+    fn name(&self) -> Ident;
+
+    fn check_encoding(&self, encoding: EncodingKind, direction: Direction) -> Result<(), ()>;


Instead of returning () in case of error, return a singleton error type, e.g. CalculusAnnotationError that implements std::fmt::Error (you can do this via the thiserror crate we're using).

Also it would be good to add a comment describing what this method is supposed to do.

Result<(),()> is used as a boolean success flag in this context. The returned error is wrapped with a proper AnnotationError::CalculusEncodingMismatch by the visitor. Should I use the singleton error type in this case?

Philipp15b · 2024-01-04T16:11:41Z

src/calculi/mod.rs

+    fn check_encoding(&self, encoding: EncodingKind, direction: Direction) -> Result<(), ()>;
+}
+
+pub struct CalculusVisitor<'tcx> {


Please add a comment describing shortly what this visitor does.

Philipp15b · 2024-01-04T16:15:11Z

src/calculi/mod.rs

+                        {
+                            if let Some(direction) = self.direction {
+                                if calculus
+                                    .check_encoding(encoding_ref.clone(), direction)


Why do you need to clone encoding_ref? Why doesn't check_encoding simply accept a reference?

Philipp15b · 2024-01-04T16:20:41Z

src/calculi/wlp.rs

@@ -0,0 +1,44 @@
+use std::fmt;


I feel like these implementation files require surprisingly lots of boilerplate. Why not have one struct type for a calculus annotation that maintains the Ident and an enum Calculus (with values Wp, Wlp, etc.)? Then you have one (or multiple) functions that simply match on the Calculus value for the visitor. I don't see the need to pass these abstract dyn Trait objects around if the set of possible calculi is always known by Caesar and not extensible.

Philipp15b · 2024-01-04T16:22:54Z

src/calculi/wlp.rs

+
+    fn check_encoding(&self, encoding: EncodingKind, direction: Direction) -> Result<(), ()> {
+        match encoding {
+            EncodingKind::Invariant(_) | EncodingKind::KInduction(_) | EncodingKind::Unroll(_) => {


These match statements could also be simplified. Instead of nesting every possible case and returning Ok or Err, simply match on the encoding kind and then return the expected direction from the match statement (or immediately abort for Ast, Past, Ost). Then, you can raise an Err if the direction does not match.

Philipp15b · 2024-01-04T16:26:45Z

src/proof_rules/induction.rs

@@ -26,7 +26,8 @@ use super::{Encoding, EncodingEnvironment, EncodingGenerated};
 use super::util::*;

 /// Syntactic sugar encoding for K-Induction encodings of type k=1
-pub struct InvariantAnnotation(AnnotationInfo);
+#[derive(Clone)]


I don't see the reason why these types should be cloneable.

Philipp15b · 2024-01-04T16:30:39Z

src/proof_rules/induction.rs

@@ -26,7 +26,8 @@ use super::{Encoding, EncodingEnvironment, EncodingGenerated};
 use super::util::*;

 /// Syntactic sugar encoding for K-Induction encodings of type k=1
-pub struct InvariantAnnotation(AnnotationInfo);
+#[derive(Clone)]
+pub struct InvariantAnnotation(pub AnnotationInfo);


Why is this AnnotationInfo pub?

Philipp15b · 2024-01-04T16:37:10Z

src/proof_rules/mod.rs

+    Ast(ASTAnnotation),
+}
+
+impl EncodingKind {


I feel these impls are pretty verbose we'll need to think of a better approach to architect the types here. A very simple alternative would be to simply add a method to the Encoding trait called check_calculus that receives a simple value of a new enum type Calculus and a direction and then returns Ok(()) or an Err(EncodingCalculusError). Then the checks wouldn't be part of a specific calculus, but rather of the encoding.

Philipp15b · 2024-01-04T16:47:03Z

src/intrinsic/annotations.rs

+            AnnotationError::UnknownAnnotation(span, anno_name ) => {
+                Diagnostic::new(ReportKind::Error, span)
+                    .with_message(format!(
+                        "The '{}' annotation is unknown.",


Does this error occur from the user? Or is it always a compiler error? If the latter is true, then we should simply panic instead of emitting an error if the user can't fix it.

Philipp15b · 2024-01-04T16:50:48Z

src/ast/decl.rs

@@ -210,6 +210,7 @@ pub struct ProcDecl {
    /// (read) access to the proc declaration.
    pub body: RefCell<Option<Block>>,
    pub span: Span,
+    pub calculus: Option<Ident>,


Why would this be an Ident if the calculus is always from a fixed set of values that are built into the compiler? Couldn't you save a value of an enum type Calculus here?

Philipp15b

Thanks a lot! I left a number of minor comments.

Philipp15b · 2024-01-25T12:31:43Z

src/intrinsic/annotations.rs

+#[derive(Debug, Clone)]
+
+pub enum CalculusType {
+    WP,


The enum items should be named Wp, Wlp, Ert

Philipp15b · 2024-02-01T09:44:23Z

src/proof_rules/induction.rs

@@ -192,6 +207,18 @@ impl Encoding for KIndAnnotation {
        resolve.visit_expr(invariant)
    }

+    fn check_calculus(&self, calculus: &Calculus, direction: Direction) -> Result<(), ()> {


This method should return a descriptive error type, e.g. just an AnnotationError

Philipp15b · 2024-02-01T09:44:42Z

src/proof_rules/induction.rs

+        }
+
+        Ok(())
+    }


There should be an empty line after an fn

Philipp15b · 2024-02-01T09:46:12Z

src/proof_rules/induction.rs

@@ -81,6 +84,19 @@ impl Encoding for InvariantAnnotation {
        resolve.visit_expr(invariant)
    }

+    fn check_calculus(&self, calculus: &Calculus, direction: Direction) -> Result<(), ()> {
+        if direction


The inline match expression inside an if statement should be rewritten to just a single match statement that either returns an Err or Ok without the if then else.

Philipp15b · 2024-02-01T09:47:05Z

src/proof_rules/mciver_ast.rs

@@ -115,6 +117,15 @@ impl Encoding for ASTAnnotation {
        check_annotation_call(tycheck, call_span, &self.0, args)?;
        Ok(())
    }
+    fn check_calculus(&self, calculus: &Calculus, direction: Direction) -> Result<(), ()> {
+        if let CalculusType::WP = calculus.calculus_type {


Why not just if calculus.calculus_type == CalculusType::Wp && direction == Direction::Down?

Philipp15b · 2024-02-01T09:51:57Z

src/proof_rules/past.rs

@@ -85,6 +87,16 @@ impl Encoding for PASTAnnotation {
        resolve.visit_expr(k)
    }

+    fn check_calculus(&self, calculus: &Calculus, direction: Direction) -> Result<(), ()> {
+        if let CalculusType::ERT = calculus.calculus_type {


Rewrite into single if as described above.

Philipp15b · 2024-02-01T09:52:40Z

src/proof_rules/unroll.rs

+        }
+
+        Ok(())
+    }


Empty line after fn.

Philipp15b · 2024-02-01T09:53:14Z

src/proof_rules/util.rs

+    ]
+}
+
+/// Encode the extend step in bmc recursively for k times


Colon after end of sentence and empty line before heading.

Philipp15b · 2024-02-01T09:53:48Z

src/proof_rules/util.rs

    let builder = ExprBuilder::new(span);
+    let extrem_lit = match direction {


extreme_lit

Philipp15b · 2024-02-01T09:57:30Z

src/intrinsic/annotations.rs

        }
    }
 }

+#[derive(Debug, Clone)]
+pub struct Calculus {


I don't quite understand why this struct exists. Shouldn't the CalculusType enum be sufficient? Why have the additional Ident?

Philipp15b

Thanks a lot! This is looking very good. I'm traveling right now, but I'll create some documentation for this and then merge it in the next couple of days! :)

Philipp15b · 2024-02-12T18:09:43Z

src/proof_rules/ost.rs

-
-        Err(())
+    fn is_calculus_allowed(&self, calculus: &Calculus, direction: Direction) -> bool {
+        matches!(calculus.calculus_type, CalculusType::Wp) && direction == Direction::Down


Just a side note, if you derive PartialEq and Eq for the CalculusType enum, then you can use normal == to compare these values.

Philipp15b · 2024-02-12T18:11:38Z

src/proof_rules/induction.rs

@@ -207,17 +202,17 @@ impl Encoding for KIndAnnotation {
        resolve.visit_expr(invariant)
    }

-    fn check_calculus(&self, calculus: &Calculus, direction: Direction) -> Result<(), ()> {
+    fn is_calculus_allowed(&self, calculus: &Calculus, direction: Direction) -> bool {
        if direction


The logic here seems a bit convoluted. Why not simply immediately return direction == match calculus.calculus_type { CalculusType::Wp | CalculusType::Ert => Direction::Up, CalculusType::Wlp => Direction::Down, }?

darionhaase · 2024-04-29T19:53:34Z

src/intrinsic/annotations.rs

+            AnnotationError::CalculusEncodingMismatch(span, calculus_name, encoding_name ) => {
+                Diagnostic::new(ReportKind::Error, span)
+                    .with_message(format!(
+                        "The '{}' calculus does not support the '{}' encoding.",


Maybe also include the direction? E.g. using @invariant with @wlp in a coproc causes confusion because the diagnostic "The 'wlp' calculus does not support the 'invariant' encoding." makes it look like the invariant-rule cannot be used for wlp at all.

annotations: calculus annotations (wp,ert,wlp)

a286130

Philipp15b requested changes Jan 4, 2024

View reviewed changes

Philipp15b reviewed Jan 4, 2024

View reviewed changes

umutdural added 5 commits January 16, 2024 21:51

annotations: calculus refactoring

ad861f3

encodings: util refactor

a10ff34

encodings: appropriate direction for const

59c6bc9

encodings: fixed tests

068757a

encodings: fixed hey_const

d28c5c6

Philipp15b requested changes Feb 1, 2024

View reviewed changes

annotations: function refactoring

62ae301

Philipp15b approved these changes Feb 12, 2024

View reviewed changes

annotations: tiny refactoring

bd5bbb6

Philipp15b mentioned this pull request Mar 21, 2024

Rewrite tests to use proof rule annotations #8

Open

darionhaase reviewed Apr 29, 2024

View reviewed changes

Philipp15b added a commit that referenced this pull request May 1, 2024

Merge PR #7: calculus annotations for wp, wlp, ert

8a67eb6

Philipp15b merged commit 9116a6f into moves-rwth:main May 1, 2024
4 checks passed

umutdural deleted the calculus-anno branch May 8, 2024 11:23

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

annotations: calculus annotations (wp,ert,wlp) #7

annotations: calculus annotations (wp,ert,wlp) #7

umutdural commented Jan 4, 2024

Philipp15b left a comment

Philipp15b Jan 4, 2024

Philipp15b Jan 4, 2024

Philipp15b Jan 4, 2024

umutdural Jan 16, 2024

Philipp15b Jan 4, 2024

Philipp15b Jan 4, 2024

Philipp15b Jan 4, 2024

Philipp15b Jan 4, 2024

Philipp15b Jan 4, 2024

Philipp15b Jan 4, 2024

Philipp15b Jan 4, 2024

Philipp15b Jan 4, 2024

Philipp15b Jan 4, 2024

Philipp15b left a comment

Philipp15b Jan 25, 2024

Philipp15b Feb 1, 2024

Philipp15b Feb 1, 2024

Philipp15b Feb 1, 2024

Philipp15b Feb 1, 2024

Philipp15b Feb 1, 2024

Philipp15b Feb 1, 2024

Philipp15b Feb 1, 2024

Philipp15b Feb 1, 2024

Philipp15b Feb 1, 2024

Philipp15b left a comment

Philipp15b Feb 12, 2024

Philipp15b Feb 12, 2024

darionhaase Apr 29, 2024

+                      }
+                      Ok(())
+                  }

		let builder = ExprBuilder::new(span);
		let extrem_lit = match direction {

annotations: calculus annotations (wp,ert,wlp) #7

annotations: calculus annotations (wp,ert,wlp) #7

Conversation

umutdural commented Jan 4, 2024

Technical:

Philipp15b left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Philipp15b left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Philipp15b left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment