Potential incompleteness with postcondition for mutually recursive functions

[mschwerhoff]

Carbon fails to verify the postcondition of function coin_rec(), while it verifies in Silicon.

function min(a: Int, b: Int) : Int
  decreases a, b
{
  a < b ? a : b
}

// Predicate to check if the weights and values sequences are valid for the knapsack problem
define valid_coin_seq(coins) 
  |coins| >= 2 &&
  forall k: Int :: {coins[k]} 0 <= k < |coins| ==> coins[k] > 0

function coin_rec(amount: Int, coins: Seq[Int]) : Int
  requires valid_coin_seq(coins) // Required for termination
  ensures amount < 0 ==> result == -1 // ❌ Failing postcondition (in Carbon)
  decreases amount // Holds, but does not seem to affect verification behaviour
{
  amount == 0 ? 0 : minCoinsHelper(amount, |coins|, coins)
}


function minCoinsHelper(amount: Int, index: Int, coins: Seq[Int]) : Int 
  requires 0 <= index <= |coins|
  requires valid_coin_seq(coins) // Required for termination
  decreases amount, index // Holds, but does not seem to affect verification behaviour
{
  (amount == 0 ) ? 0 :
  (amount < 0 || index == 0) ? -1 :
  
  // If next two lines are commented and the last is replaced by 0, Carbon verifies the problematic postcondition
  (coin_rec(amount - coins[index-1], coins) == -1) ? minCoinsHelper(amount, index - 1, coins) : // Only this line commented ➜ error in Silicon
  (minCoinsHelper(amount, index - 1, coins) == -1) ? 1 + coin_rec(amount - coins[index-1], coins) : // Only this line (or this and the preceding line) commented ➜ Silicon OK
  
  min(1 + coin_rec(amount - coins[index-1], coins), minCoinsHelper(amount, index - 1, coins))
}

I could imagine that the problem/difference in verifiers is due to the order in which information becomes available during the verification of the mutually recursive functions.

The problem was originally reported by Sonja Joost.