Fix logical variable shadowing program variables

[strub]

Currently, when resolving an identifier, EasyCrypt tries to resolve it as a logical variable first, and then as a program variable (in the active memory), even when a memory specifier is given.

This commit adds a new memory specifier that changes the resolution order: when using it, we first try to resolve the identifier as a program variable (in the given memory), and then as a logical variable if no program variable matching that name is found.

The syntax is form{!memory}.

The pretty-printer has been updated accordingly.

Fix #122, fix #196

[strub]

The implemented solution has been discussed at length in #122. Let's try not to put a new coin in the machine.

[alleystoughton]

I think you might have missed a case. In

module M = {
  proc f(z : int) : bool = {
    return z = 3;
  }
}.

lemma foo (z : int) :
  equiv [M.f ~ M.f : z{1} = z ==> res{1}].
proof.
(*
Current goal

Type variables: <none>

z: int
------------------------------------------------------------------------
pre = z = z

    M.f ~ M.f

post = res{!1}

do you instead want

Type variables: <none>

z: int
------------------------------------------------------------------------
pre = z{!1} = z

    M.f ~ M.f

post = res{!1)

Also, I find your description "This commit adds a new memory specifier that changes the resolution order: program variables firs & then logical variables." confusing. It seems that when there is a conflict about whether z, say, is a program variable or a logical variable in a pre or postcondition, that the answer is logical unless the {!hr}/{!1}/{!2} annotation is used to say it should be the program variable.

[alleystoughton]

Ah, and in pRHL pre- and postconditions, I guess I don't understand why you aren't still using {1} and {2}. In

&1 (left ) : {b : bool}
&2 (right) : {b1, b2 : bool}

pre = true

b <$ {0,1}                 (1)  b2 <$ {0,1}              

post = b{!1} = b1{!2} ^^ b2{!2}

do you want the user to run

rnd (fun x => x ^^ b1{2}).

still or

rnd (fun x => x ^^ b1{!2}).

Some of the ambiguity is only there in Hoare or pHL, right, because in pRHL program variables are always decorated with sides in pre- and postconditions. The problem was one couldn't write z{&hr} in a Hoare pre- or post-condition.

[strub]

I think you might have missed a case.

No. As discussed in #122, e{m} activate the memory m when type-checking the expression e - i.e. when EasyCrypt tries to resolve a program variable, it does it in m. However, the resolution of a variable stays the same: first try to resolve it as a logical variable and if this fails, try to resolve it as a program variable. As said, this behaviour is independent from m (i.e. m being hr or 1 or 2...)

Ah, and in pRHL pre- and postconditions, I guess I don't understand why you aren't still using {1} and {2}.

Because we already have a lot of technical debts that I am pruning and I don't want to add extra exceptions to the code (i.e. have a behaviour that depends on the memory name)

The problem was one couldn't write z{&hr} in a Hoare pre- or post-condition.

You can use hr (not &hr) in the pre/post of a Hoare/pHoare goal. E.g. in current main, this works:

require import AllCore.

module M = {
  proc f(x : int) = {
    return x;
  }
}.

lemma L : hoare[M.f : x{hr} = 0 ==> res = 0].

But if x also exist as a logical variable, then x is going to be resolved as this logical variable. (as explained in my first point)

In #122, we discussed two solutions: the one implemented here & the one where x{m} and e{m} (when e does not reduce to a variable) have different meanings: x{m} forces the resolution of x in m while e{m} activate the memory m but does not change the resolution order.

...

What is a bug is that the pretty-printer is using the {!_} too often. When there is no ambiguity, the pretty-printer should simply print the raw variable name, as before.

Let's remember here that we are fixing an ambiguity issue that happens when one has the (IMO bad) idea to use the same name for a program variable & a logical variable.

[strub]

...

Also, EasyCrypt used to print a warning message when a memory annotation was not used by the typer. This seems to fail in the pre/post. Should also be fixed. In your first example, you should get a warning telling you that hr was unused.

[alleystoughton]

OK, thanks, I was misunderstanding things.

"What is a bug is that the pretty-printer is using the {!_} too often. When there is no ambiguity, the pretty-printer should simply print the raw variable name, as before." So are you going to fix this before merging?

[strub]

OK, thanks, I was misunderstanding things.

"What is a bug is that the pretty-printer is using the {!_} too often. When there is no ambiguity, the pretty-printer should simply print the raw variable name, as before." So are you going to fix this before merging?

Pushed. You first example now gives the warning + unused memory &1, while typing z. If you add a !, then the correct program variable is selected. The ! modified is only printed when there is an ambiguity.

[alleystoughton]

Looks good to me.