Unfolding and its effect are limited/scoped to the function body

The following program fails to verify in Silicon and Carbon, but by uncommenting the first assert statement everything goes through. The incompleteness is essentially by design, as explained by @mschwerhoff in https://github.com/viperproject/silicon/issues/529#issuecomment-777303780.

predicate P(x: Int) {
    x == 123
}

function property(x: Int): Bool
    requires P(x)
{
    unfolding P(x) in x == 123
}

method check_property(x: Int)
  requires P(x)
{
    // assert unfolding P(x) in true
    assert property(x); // Fails
}

Start with the minimal reproducer in the issue and run it in Silicon and Carbon to confirm the differing behavior. Read the linked Silicon issue comment for the existing rationale and determine the intended unfolding scope. Done should include an agreed behavior and regression coverage for the reproducer.