Add #[kani::loop_decreases] for proving loop termination

cprover_bindings/src/goto_program/stmt.rs

@@ -86,6 +86,7 @@ pub enum StmtBody {
         // applied as loop contracts in CBMC if it is a backward goto.
         loop_invariants: Option<Expr>,
         loop_modifies: Option<Vec<Expr>>,
+        loop_decreases: Option<Expr>,
     },
     /// `if (i) { t } else { e }`
     Ifthenelse {
@@ -282,7 +283,7 @@ impl Stmt {
     pub fn goto<T: Into<InternedString>>(dest: T, loc: Location) -> Self {
         let dest = dest.into();
         assert!(!dest.is_empty());
-        stmt!(Goto { dest, loop_invariants: None, loop_modifies: None }, loc)
+        stmt!(Goto { dest, loop_invariants: None, loop_modifies: None, loop_decreases: None }, loc)
     }
 
     /// `if (i) { t } else { e }` or `if (i) { t }`
@@ -327,13 +328,14 @@ impl Stmt {
 
     /// `goto dest;` with loop invariant
     pub fn with_loop_contracts(self, inv: Expr) -> Self {
-        if let Goto { dest, loop_invariants, loop_modifies } = self.body() {
+        if let Goto { dest, loop_invariants, loop_modifies, loop_decreases } = self.body() {
             assert!(loop_invariants.is_none());
             stmt!(
                 Goto {
                     dest: *dest,
                     loop_invariants: Some(inv),
-                    loop_modifies: loop_modifies.clone()
+                    loop_modifies: loop_modifies.clone(),
+                    loop_decreases: loop_decreases.clone()
                 },
                 *self.location()
             )
@@ -343,20 +345,38 @@ impl Stmt {
     }
 
     pub fn with_loop_modifies(self, asg: Vec<Expr>) -> Self {
-        if let Goto { dest, loop_invariants, loop_modifies } = self.body() {
+        if let Goto { dest, loop_invariants, loop_modifies, loop_decreases } = self.body() {
             assert!(loop_modifies.is_none());
             stmt!(
                 Goto {
                     dest: *dest,
                     loop_invariants: loop_invariants.clone(),
-                    loop_modifies: Some(asg)
+                    loop_modifies: Some(asg),
+                    loop_decreases: loop_decreases.clone()
                 },
                 *self.location()
             )
         } else {
             unreachable!("Loop assigns should be annotated only to goto stmt")
         }
     }
+
+    pub fn with_loop_decreases(self, decreases: Expr) -> Self {
+        if let Goto { dest, loop_invariants, loop_modifies, loop_decreases } = self.body() {
+            assert!(loop_decreases.is_none());
+            stmt!(
+                Goto {
+                    dest: *dest,
+                    loop_invariants: loop_invariants.clone(),
+                    loop_modifies: loop_modifies.clone(),
+                    loop_decreases: Some(decreases)
+                },
+                *self.location()
+            )
+        } else {
+            unreachable!("Loop decreases should be annotated only to goto stmt")
+        }
+    }
 }
 
 /// Predicates

cprover_bindings/src/irep/irep_id.rs

@@ -595,6 +595,7 @@ pub enum IrepId {
     Used,
     IsUsed,
     CSpecLoopInvariant,
+    CSpecDecreases,
     CSpecRequires,
     CSpecEnsures,
     CSpecAssigns,
@@ -1485,6 +1486,7 @@ impl IrepId {
             IrepId::Used => "used",
             IrepId::IsUsed => "is_used",
             IrepId::CSpecLoopInvariant => "#spec_loop_invariant",
+            IrepId::CSpecDecreases => "#spec_decreases",
             IrepId::CSpecRequires => "#spec_requires",
             IrepId::CSpecEnsures => "#spec_ensures",
             IrepId::CSpecAssigns => "#spec_assigns",

cprover_bindings/src/irep/to_irep.rs

@@ -556,7 +556,7 @@ impl ToIrep for StmtBody {
                     arguments_irep(arguments.iter(), mm),
                 ],
             ),
-            StmtBody::Goto { dest, loop_invariants, loop_modifies } => {
+            StmtBody::Goto { dest, loop_invariants, loop_modifies, loop_decreases } => {
                 let inv = loop_invariants
                     .clone()
                     .map(|inv| inv.clone().and(Expr::bool_true()).to_irep(mm));
@@ -565,10 +565,12 @@ impl ToIrep for StmtBody {
                         assigns.iter().map(|assign| assign.to_irep(mm)).collect(),
                     )])
                 });
+                let decreases = loop_decreases.clone().map(|dec| dec.to_irep(mm));
                 code_irep(IrepId::Goto, vec![])
                     .with_named_sub(IrepId::Destination, Irep::just_string_id(dest.to_string()))
                     .with_named_sub_option(IrepId::CSpecLoopInvariant, inv)
                     .with_named_sub_option(IrepId::CSpecAssigns, assigns.clone())
+                    .with_named_sub_option(IrepId::CSpecDecreases, decreases)
             }
             StmtBody::Ifthenelse { i, t, e } => code_irep(
                 IrepId::Ifthenelse,

docs/src/reference/attributes.md

@@ -248,6 +248,6 @@ There are numerous attributes for function and loop contracts. At present, these
 - Proof harness for contracts: `#[kani::proof_for_contract(name-of-function)]`
 - Verified stubbing: `#[kani::stub_verified]`
 - Function contract specification: `#[kani::requires]`, `#[kani::modifies]`, `#[kani::ensures]`, `#[kani::recursion]`
-- Loop contract specification: `#[kani::loop_invariant]`, `#[kani::loop_modifies]`.
+- Loop contract specification: `#[kani::loop_invariant]`, `#[kani::loop_modifies]`, `#[kani::loop_decreases]`.
 
 See the documentation on [function contracts](./experimental/contracts.md) and [loop contracts](./experimental/loop-contracts.md) for details.