Inconsistent lifting of `Lit` marker causes issues with computation on literals

Dafny rejects the following code as of today:

function method rsum(s: seq<int>): int {
  if |s| == 0 then 0
  else s[|s| - 1] + rsum(s[..|s| - 1])
}

method t() {
  assert rsum([1, 2, 3]) == 6;
}

Adding fuel using {:fuel rsum, 10} fixes the issue, but it should not be needed, because Dafny generates "free" reduction axioms for functions applied to literals. For example, this code verifies just fine:

function method sum(s: seq<int>): int {
  if |s| == 0 then 0
  else s[0] + sum(s[1..])
}

method t() {
  assert sum([1, 2, 3]) == 6;
}

The problem becomes clear if you look at the generated axioms:

This is what happens with sum:

// definition axiom for _module.__default.sum for all literals (revealed)
axiom 0 <= $FunctionContextHeight
   ==> (forall $ly: LayerType, s#0: Seq Box ::
    {:weight 3} { _module.__default.sum($LS($ly), Lit(s#0)) }
    … ==> _module.__default.sum($LS($ly), Lit(s#0))
        == (if Seq#Length(Lit(s#0)) == LitInt(0)
            then 0
            else $Unbox(Seq#Index(Lit(s#0), LitInt(0))): int
               + _module.__default.sum($LS($ly), Lit(Seq#Drop(Lit(s#0), LitInt(1))))));

But for rsum, the call to Seq#Take is not marked as Lit :

// definition axiom for _module.__default.rsum for all literals (revealed)
axiom 0 <= $FunctionContextHeight
   ==> (forall $ly: LayerType, s#0: Seq Box ::
    {:weight 3} { _module.__default.rsum($LS($ly), Lit(s#0)) }
    … ==> _module.__default.rsum($LS($ly), Lit(s#0))
        == (if Seq#Length(Lit(s#0)) == LitInt(0)
            then 0
            else $Unbox(Seq#Index(Lit(s#0), Seq#Length(Lit(s#0)) - 1)): int
               + _module.__default.rsum($LS($ly), Seq#Take(Lit(s#0), Seq#Length(Lit(s#0)) - 1))));

The problem is in the code that generates these axioms; specifically https://github.com/dafny-lang/dafny/blob/2b4b98072ebc13b71499a1de20d77aefde02f6c0/Source/Dafny/Verifier/Translator.ExpressionTranslator.cs#L723 does not propagate Lit past Seq#Length. Looking at the rest of the code, there are many more missing propagations — it's not just Seq#Length. Here is one other test, for example:

function method unions(s: seq<set<int>>, acc:set<int>): set<int> {
  if |s| == 0 then acc
  else unions(s[1..], s[0] + acc)
}

method t() {
  assert unions([{1}, {2}, {3}], {}) == {1, 2, 3}; // FAILS
}

dafny-lang / dafny

Inconsistent lifting of `Lit` marker causes issues with computation on literals #1912