Verification parity between method and function.

[rdivyanshu]

In following code snippet method version verifies but function version timeout. It seems puzzling to end user as both version looks equivalent (modulo how verification encoding is done for method vs function which end user doesn't care about). Is there explanation for this behavior ?

method pairSetMap(ss: set<(int, int)>, i: int) returns (r: set<(int, int)>) 
  ensures forall p :: p in ss <==> (p.0 + i, p.1 + i) in r
  ensures |r| == |ss|
{
    if |ss| < 1 {
      r := set pair | pair in ss :: (pair.0 + i, pair.1 + i);
    }
    else { 
        var s :| s in ss;
        var t := pairSetMap(ss - {s}, i);
        assert |t| == |ss - {s}|;
        assert |ss| == |ss - {s}| + 1;
        assert (s.0 + i, s.1 + i) !in t by {
           if (s.0 + i, s.1 + i) in t {
                assert (s.0, s.1) in ss - {s};
                assert (s.0, s.1) !in ss - {s};
           }
        }
        r := t + { (s.0 + i, s.1 + i) };
    }
}

function pairSetMap(ss: set<(int, int)>, i: int) : (r: set<(int, int)>) 
  ensures forall p :: p in ss <==> (p.0 + i, p.1 + i) in r
  ensures |r| == |ss|
{
    if |ss| < 1 
      then set pair | pair in ss :: (pair.0 + i, pair.1 + i)
    else 
      var s :| s in ss;
      var t := pairSetMap(ss - {s}, i);
      assert |t| == |ss - {s}|;
      assert |ss| == |ss - {s}| + 1;
      assert (s.0 + i, s.1 + i) !in t by {
        if (s.0 + i, s.1 + i) in t {
          assert (s.0, s.1) in ss - {s};
          assert (s.0, s.1) !in ss - {s};
        }
        }
      t + { (s.0 + i, s.1 + i) }
}

[stefan-aws]

I suspect this has to do with i) triggers and ii) the such-that assignment :|. If you externalise the predicate in the quantifier, add {:trigger true}, and turn your function ghost to avoid having to prove the uniqueness of your choice, things work out:

ghost predicate P(p: (int, int), ss: set<(int, int)>, i: int, r: set<(int, int)>) {
    p in ss <==> (p.0 + i, p.1 + i) in r
}

method pairSetMap(ss: set<(int, int)>, i: int) returns (r: set<(int, int)>) 
  ensures forall p {:trigger true} :: P(p, ss, i, r)
  ensures |r| == |ss|
{
    if |ss| < 1 {
      r := set pair | pair in ss :: (pair.0 + i, pair.1 + i);
    }
    else { 
        var s :| s in ss;
        var t := pairSetMap(ss - {s}, i);
        assert |t| == |ss - {s}|;
        assert |ss| == |ss - {s}| + 1;
        assert (s.0 + i, s.1 + i) !in t by {
           if (s.0 + i, s.1 + i) in t {
                assert (s.0, s.1) in ss - {s};
                assert (s.0, s.1) !in ss - {s};
           }
        }
        r := t + { (s.0 + i, s.1 + i) };
    }
}

and

ghost predicate P(p: (int, int), ss: set<(int, int)>, i: int, r: set<(int, int)>) {
    p in ss <==> (p.0 + i, p.1 + i) in r
}

ghost function pairSetMap(ss: set<(int, int)>, i: int) : (r: set<(int, int)>) 
  ensures forall p {:trigger true} :: P(p, ss, i, r)
  ensures |r| == |ss|
{
    if |ss| < 1 
      then set pair | pair in ss :: (pair.0 + i, pair.1 + i)
    else 
      var s :| s in ss;
      var t := pairSetMap(ss - {s}, i);
      assert |t| == |ss - {s}|;
      assert |ss| == |ss - {s}| + 1;
      assert (s.0 + i, s.1 + i) !in t by {
        if (s.0 + i, s.1 + i) in t {
          assert (s.0, s.1) in ss - {s};
          assert (s.0, s.1) !in ss - {s};
        }
        }
      t + { (s.0 + i, s.1 + i) }
}