Implement soundness checking & corresponding diagnostics in lsp #103

umutdural · 2025-11-12T15:42:42Z

This PR implements the soundness checking described in #75.

Approximation kinds form a complete lattice, illustrated by the following diagram:

graph TD;
    Exact-->Over;
    Exact-->Under;
    Over-->Unknown;
    Under-->Unknown;

Each encoding annotation may approximate the actual program behavior using one of the approximation kinds shown above. The overall approximation of a block of statements is the infimum of the approximations of all statements in the block. For example if there are both under- and over-approximating statements in a block, the block has the approximation kind Unknown. But if every statement is under-approximating then the block also under-approximates.

To determine how an encoding annotation approximates, the (optional) calculus annotation of the surrounding procedure, the direction, and the encoding itself are important. Depending on these three aspects, the fixed-point semantics of the annotated loop are determined. Using a function attached to each encoding annotation, we can then decide how each encoding approximates based on the chosen fixed-point semantics and the approximation of its body.

Finally by looking the direction of the proc and the approximation kind of its body we choose a soundness type.

Soundness::Exact means that there is no approximation in the proc so any verification result or counter example is sound.
Soundness::Proof means that the verification result is sound when it is a proof, i.e., if the proc verifies. If the result is a counter-example then this counter-example might be spurious.
Soundness::Refutation means that the verification result is sound when it is a counter-example. If the program verifies it might be spurious and the original program might not actually verify.
Soundness::Unknown means that we can not give guarantees about the soundness of both proofs and refutations.

Closes #75.

Philipp15b

Thanks! I left a bunch of comments.

Philipp15b · 2025-11-14T13:26:23Z

src/driver/commands/verify.rs

        .into_iter()
        .flat_map(|item| {
-            item.flat_map(|unit| CoreVerifyTask::from_source_unit(unit, &mut depgraph))
+            let soundness_blame = soundness_map.get(item.name()).cloned().unwrap_or_default();


How does this map work? Is it really ever not a bug if an item has no associated SoundnessBlame?

Philipp15b · 2025-11-14T13:27:07Z

src/driver/commands/verify.rs

        // (depending on options).
        let vc_is_valid = lower_quant_prove_task(options, &limits_ref, &mut tcx, name, vc_expr)?;

+        let soundness_blame = verify_unit.soundness_blame.take().unwrap_or_default();


Why the .take() here? Do we really want to modify the VerifyUnit here?

Philipp15b · 2025-11-14T13:27:22Z

src/driver/core_verify.rs

    pub deps: Dependencies,
    pub direction: Direction,
    pub block: Block,
+    pub soundness_blame: Option<SoundnessBlame>,


If this is Option, it needs a comment for explanation.

Philipp15b · 2025-11-14T13:30:23Z

src/proof_rules/calculus/soundness_checker.rs

+#[derive(Debug, Clone)]
+pub struct ApproximationListEntry {
+    pub span: Span,
+    pub is_loop: bool,


To avoid the infamous Boolean blindness, I'd suggest creating something like a StmtKindName enum here, with two values: Stmt and Loop. This type should implement Display accordingly.

Philipp15b · 2025-11-14T13:31:23Z

src/proof_rules/calculus/soundness_checker.rs

+}
+pub type ApproximationList = Vec<ApproximationListEntry>;
+
+// pub type SoundnessBlame = (Soundness, ApproximationList);


Philipp15b · 2025-11-14T14:16:36Z

src/proof_rules/mod.rs

+    if let Some(ident) = proc.calculus.as_ref() {
+        match tcx.get(*ident) {
+            Some(decl) => {
+                // If the declaration is a calculus annotation, return it


Remove comment

Philipp15b · 2025-11-14T14:30:46Z

src/vc/explain.rs

        stmt_span,
        call_span,
        direction,
+        calculus: None,


needs comment

Philipp15b · 2025-11-14T14:39:49Z

src/proof_rules/calculus/soundness_checker.rs

+
+// pub type SoundnessBlame = (Soundness, ApproximationList);
+
+#[derive(Debug, Clone, Default)]


I think we might be able to simplify the type design here. SoundnessBlame is a very open type, and can be invalidated by everyone easily. I propose a slight refactoring, making a lot of the computations internal to one type.

Unify SoundnessBlame and Soundness, new name ProcSoundness.

The soundness field is replaced by two fields sound_proofs, sound_refutations of type bool.

All fields are private by default, with accessor methods.

Add methods to this type to generate diagnostics (c.f. https://github.com/moves-rwth/caesar/pull/103/files#r2527526668)

Philipp15b · 2025-11-14T14:47:35Z

src/proof_rules/calculus/soundness_checker.rs

+}
+
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Default)]
+pub enum ApproximationKind {


A possible idea: change this to be a struct with two fields, under, and over of type bool. The infimum and supremum operations become field-wise && and || operations, and you can even overload the built-in (bitwise) operators instead (e.g. https://doc.rust-lang.org/core/ops/trait.BitAnd.html).

~~partial_cmp can now be derived automatically by the compiler!~~ (that would be wrong!)

You can still have constants like ApproximationKind::EXACT, ApproximationKind::UNKNOWN declared.

Also, you can implement the Sum trait, and have that do the infimum operation. I think it's intuitive that that operation does the right thing here (i.e. folding with infimum).

Philipp15b · 2025-11-14T14:49:15Z

src/intrinsic/annotations.rs

                        "There must not be any statements after this annotated statement (and the annotated statement must not be nested in a block).",
                    ))
            }
-            AnnotationUnsoundnessError::CalculusEncodingMismatch{direction, span, calculus_name, enc_name } => {


Do we still have a corresponding test now for this case?

Philipp15b

Left a bunch of comments.

Philipp15b · 2025-11-29T10:26:24Z

src/proof_rules/calculus/soundness_checker.rs

+    }
+}
+
+impl std::ops::Deref for ApproximationList {


I consider these Deref and DerefMut impls a code smell. Either we abstract from the underlying data type and implement necessary operations like push on ApproximationList itself, OR we have Deref and DerefMut impls.

Philipp15b · 2025-11-29T10:27:25Z

src/proof_rules/calculus/soundness_checker.rs

+        calculus: Option<Calculus>,
+    ) -> Self {
+        let approx = approximations.infimum();
+        // The mapping between approximation kinds and soundness is as follows:


It cannot be this complicated. In particular, the XORs are impossible to read and explain. I suggest explicit if-then-else chains that make the code overall readable.

Philipp15b · 2025-11-29T10:28:55Z

src/proof_rules/calculus/soundness_checker.rs

-            (_, ApproximationKind::Unknown) => Some(std::cmp::Ordering::Greater),
-            (ApproximationKind::Under, ApproximationKind::Over)
-            | (ApproximationKind::Over, ApproximationKind::Under) => None,
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Default)]


This needs a very detailed doc comment explaining what the fields mean. Those fields can also be public, with proper comments like "if under is true, then the vp semantics under-approximates the original programs semantics".

Philipp15b · 2025-11-29T10:30:59Z

src/proof_rules/calculus/soundness_checker.rs

+    over: bool,
+}
+
+// Note that the operations are reversed because the exact approximation should be the top element in the lattice but we want it to be (false,false).


I don't understand at all why it's this way. over = true should mean that e.g. vp[S] >= wp[S]. And the bitwise and implementation must be the obvious one, i.e. pairwise conjunction.

As I understand it now, ApproximationKind seems to be the flipped lattice of the one you put in the PR description.

Philipp15b · 2025-11-29T10:31:30Z

src/proof_rules/calculus/soundness_checker.rs

-    Refutation,
-    Unknown,
+impl ApproximationKind {
+    pub const EXACT: Self = Self {


These constants need doc comments as well.

Philipp15b · 2025-11-29T10:35:37Z

src/proof_rules/calculus/soundness_checker.rs

-        ));
-        acc
-    })
+    block


I think the cleaner version of this would be to do a map first, and then flatten and then collect the result into the ApproximationList, no?

At this point, since ApproximationList doesn't seem to carry any guarantees, a no-newtype simple Vec type alias for ApproximationList would make this easier.

Philipp15b · 2025-11-29T10:35:53Z

src/proof_rules/calculus/soundness_checker.rs

+        // Composite statements are handled recursively to collect approximations from sub-statements
+        StmtKind::Seq(stmts) => stmts
+            .iter()
+            .fold(ApproximationList::default(), |mut acc, stmt| {


Same comment about map and flatten here

Philipp15b · 2025-11-29T10:39:27Z

src/proof_rules/calculus/soundness_checker.rs


        let approx_list = track_approximation_in_block(block, direction, calculus, tcx);
-        let infimum_approx = infimum_approximation_list(&approx_list);
+        let infimum_approx = approx_list.infimum();


This needs a comment on what happens with an empty approximation list (also on that function's doc comment).

Philipp15b · 2025-11-29T10:39:54Z

src/proof_rules/calculus/soundness_checker.rs

-            soundness: Soundness::from_approximation(infimum_approx, direction),
+        return Some(ProcSoundness {
+            sound_proofs: match direction {
+                Direction::Down => infimum_approx == ApproximationKind::UNDER,


This can't be right. What if it's ApproximationKind::EXACT?

Philipp15b · 2025-11-29T10:45:05Z

src/proof_rules/calculus/soundness_checker.rs

-            Some(std::cmp::Ordering::Greater) => self,
-            None => ApproximationKind::Exact, // If they are incomparable, return Exact (which is the top element)
+impl ApproximationList {
+    pub fn infimum(&self) -> ApproximationKind {


I suggest adding Rustdoc here, and also a bunch of Documentation tests to explain this, esp. with the list of zero items, one item, and two/three.

…d ProcSoundness logic

Philipp15b

Small comments

Philipp15b · 2025-12-04T10:15:42Z

src/proof_rules/calculus/soundness_checker.rs

+    pub kind: ApproximationKind,
+}
+// #[derive(Debug, Clone, Default)]
+// pub struct ApproximationList(pub Vec<ApproximationRecord>);


Philipp15b · 2025-12-04T10:17:08Z

src/proof_rules/calculus/soundness_checker.rs

+            calculus,
+        }
+    }
+    /// Get whether proofs for this procedure are sound.


newline missing

Philipp15b · 2025-12-04T10:18:22Z

src/proof_rules/calculus/soundness_checker.rs

+/// See also [`infer_fixpoint_semantics_kind`] for more details on how the semantics kind is inferred.
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Default)]
+pub struct ApproximationKind {
+    /// True if the vc semantics under-approximates the original program semantics


dots missing

Philipp15b · 2025-12-04T10:18:46Z

src/proof_rules/calculus/soundness_checker.rs

+}
+
+impl ApproximationKind {
+    /// vc is both under- and over-approximating the original program semantics


missing dots.

Philipp15b · 2025-12-04T10:19:42Z

src/proof_rules/calculus/soundness_checker.rs

+/// The original program semantics is based on the calculus annotation or the default fixpoint semantics for loops based on the direction and the encoding used.
+///
+/// See also [`infer_fixpoint_semantics_kind`] for more details on how the semantics kind is inferred.
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Default)]


remove default impl

Implement soundness checking & corresponding diagnostics in lsp

aa35777

Philipp15b requested changes Nov 14, 2025

View reviewed changes

Refactor SoundnessBlame and ApproximationKind

fec92f2

Philipp15b requested changes Nov 29, 2025

View reviewed changes

Refactor ApproximationList, correct and simplify ApproximationKind an…

1f30b0d

…d ProcSoundness logic

Philipp15b requested changes Dec 4, 2025

View reviewed changes

clean up doc comments

96c2220


		// pub type SoundnessBlame = (Soundness, ApproximationList);

		#[derive(Debug, Clone, Default)]

Implement soundness checking & corresponding diagnostics in lsp #103

Are you sure you want to change the base?

Implement soundness checking & corresponding diagnostics in lsp #103

Uh oh!

Conversation

umutdural commented Nov 12, 2025

Uh oh!

Philipp15b left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Philipp15b Nov 14, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Philipp15b left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Philipp15b left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Philipp15b Nov 14, 2025 •

edited

Loading