Incorrect axiom for `.requires` on lambda term

[atomb]

trafficstars

In the following snippet, the last two assertions fail:

function f(x: int): int requires x < 10 { x }

method m(x: int)
  requires x < 10
{
  var g := x requires x < 10 => x;
  var h := x requires x < 10 => f(x);

  // These succeed
  assert f.requires(x);
  assert g.requires(x);
  assert h.requires(x);
  assert forall x :: f.requires(x) ==> g.requires(x);
  assert forall x :: f.requires(x) ==> h.requires(x);

  // These fail
  assert forall x :: g.requires(x) ==> f.requires(x);
  assert forall x :: h.requires(x) ==> f.requires(x);
}

Thanks to @cpitclaudel's investigation, it looks like it boils down to a problem with this axiom in the prelude:

axiom (forall t0: Ty,
    t1: Ty,
    heap: Heap,
    h: [Heap,Box]Box,
    r: [Heap,Box]bool,
    rd: [Heap,Box]Set Box,
    bx0: Box ::
  { Requires1(t0, t1, heap, Handle1(h, r, rd), bx0) }
  r[heap, bx0] ==> Requires1(t0, t1, heap, Handle1(h, r, rd), bx0));

~~The ==> should be ==.~~

[cpitclaudel]

Here is a fairly straightforward workaround in most cases:

predicate pre(x: int) { x < 10 ) 
function f(x: int): int requires pre(x) { x }

method m(x: int)
  requires x < 10
{
  var g := x requires x < 10 => x;
  var h := x requires x < 10 => f(x);

  assert forall x :: pre(x) ==> f.requires(x);
  assert forall x :: pre(x) ==> f.requires(x);
}

[cpitclaudel]

Simplified example as a TLDR for future readers:

predicate P(x: int)
method Main() {
  var f := x requires P(x) => x;
  var g := x requires P(x) => x;
  assert forall x :: g.requires(x) ==> f.requires(x); // Fails
}

[RustanLeino]

The ==> should be ==.

Be careful! If I remember correctly, it would be unsound to make this ==> a ==. (I took a quick look, but don't immediately remember the details. Hoping that we would have included an unsound example in the test suite, I temporarily changed the implementation to use ==. This gives two errors in Test/hofs, but neither of them speaks directly about the unsoundness.)

This distinction had seemed like a surprise. It's possible that a different encoding would allow us to use ==.

Maybe @danr or @amaurremi remember more details.

[amaurremi]

Unfortunately I don't remember those details -- and I wasn't able to find notes from my internship where I might have written down something helpful.

[seanmcl]

Any progress on this?

[atomb]

Any progress on this?

We have some tentative plans to redo the axioms describing functions entirely, and doing that should fix this issue. It's a bit of a complex job, however, and behind a couple of other things in the pipeline.