Unsoundness of glob

[dominique-unruh]

The new treatment of globs (introduced in #440 which fixes #102) leads to an unsoundness.
The theory below illustrates that.

(There are some admits, I can fill them in if they are required, but I think the admitted facts that have nothing to do with modules or globs should be uncontroversial.)

Maybe it is time to fix the glob-problem by first giving a definition to what glob means? This is the third unsoundness based on inconsistent glob treatment that I have posted.

require import AllCore.

module type AT = {
  proc p():unit
}.

module A : AT = {
  var x : bool
  proc p() = {}
}.

module type BT(A:AT) = {
  proc p():unit
}.

module B(A':AT) = {
  proc p() = { A.x <- A.x; A'.p(); }
}.

(* I am axiomatizing a constant `card` here.
   The intended meaning is: If 'a is a type with finitely many values, then `card<:'a>` is the number of these values.
                            If 'a is a type with infinitely many values, then `card<:'a> = 0`.  
   It could be defined properly but that is a bit tedious.
   I believe that existence of that constant and the two lemmas `card_bool` and `card_prod` are uncontroversial, so I leave them admitted here.
   If there is doubt, I can come up with a definition and proofs. *)

op card ['a] : int = witness.
lemma card_bool: card<:bool> = 2. admitted.
lemma card_prod ['a 'b]: card<:'a*'b> = card<:'a> * card<:'b>. admitted.
    
(* The trouble starts here *)
lemma contradiction: false.
  (* When the argument to B is abstract, `glob B(A')` is unfolded to `glob A * glob A'`. *)  
  have H1: forall (A'<:AT), card<:glob B(A')> = 2 * card<:glob A'>.
    move => A'.
    rewrite card_prod<:glob A, glob A'> card_bool.
    trivial.
  (* When the argument to B is the concrete A, `glob B(A)` is unfolded to `bool` (=`glob A`) (because the variables of `B` and `A` are the same). *)  
  have H2: card<:glob B(A)> = 2.
    rewrite card_bool.
    trivial.
  (* By instantiating the abstract, we get a different cardinality. *)  
  have H3: card<:glob B(A)> = 4.
    rewrite (H1 A).
    rewrite card_bool.
    trivial.
  clear H1.
  (* And we derive a contradiction. *)
  have H4: 2=4.
    rewrite -H2 -H3.
    trivial.
  clear H2 H3.
  trivial.
qed.

[strub]

glob B(A) should reduce to glob A * glob A.

[oskgo]

For what it's worth your card, card_bool and card_prod are inconsistent. witness isn't magic, it's just an unspecified constant in each type, and the witness you use in the definition of card is witness<:int>, so your axioms are in effect stating that this is both equal to 2 and idempotent under multiplication, from which it is easy to derive a contradiction:

lemma foo: false.
proof.
have H1: witness = 2. 
- by apply/(eq_trans _ card<:bool> _)/card_bool.
have H2: witness = 4.
- apply/(eq_trans _ card<:bool * bool> _) => //.
  by rewrite card_prod card_bool.
by have: 4 = 2 by rewrite -H1 -H2.
qed.

The correct way to axiomatize card would be by leaving the definition empty as follows:

op card ['a] : int.

Curiously I'm unable to reproduce your proof of false after changing card like this. I also tried with a non-axiomatized version as follows:

require import Finite List.
op card ['a] : int = size (to_seq predT<:'a>).

This fails to reproduce your proof of false as well.

Maybe I've stumbled upon another bug or this is one of those "consistent by accident" situations or maybe there's a way to fix your proof that I'm not seeing.

This doesn't invalidate your objections though.

[dominique-unruh]

@oskgo You are, of course, perfectly right.
The embarrassing thing is that I noticed that problem myself, noticed the problem you mention, and ... from that point, I don't remember what I did next and I don't know how the outdated version came to end up in this issue and I don't find the file where I was trying without witness...

I will try to fix the counterexample and report back.

[dominique-unruh]

For counterexamples like this, is there some pragma to actually show the types that EasyCrypt uses? It is very hard to work with goals like "card = 2" when I have to guess how the type parameter of "card" is instantiated...

[fdupress]

There is none. But we're accepting this as a bug (as tagged) and are working on a long-term fix to glob-related issues.

I do not think it is worth spending time refining the counter-example further. It would, however, be worth searching for other examples that leverage other forgotten corners of the glob system. A conditional proof of false under a reasonable condition (for example, that there exists a memory) would be sufficient for our purpose, which is to catalogue places where we should expect the soundness proof to be a PITA (and where we should therefore be careful when redefining and redesigning).

[dominique-unruh]

So my analysis: The counterexample given here is incorrect. Easycrypt eagerly rewrites globs already during parsing. As far as I can tell, this rewriting means that

have H1: forall (A'<:AT), card<:glob B(A')> = 2 * card<:glob A'>

actually just is the same as if we had input

have H1: forall (A'<:AT), card<:glob B * glob A'> = 2 * card<:glob A'>

This is is, of course, true. So we don't get a contradiction because further down in the proof, we use H1 A to prove H3. But since H1 A does not talk about glob B(A) at all, this doesn't work.

The reason why it worked before (when I used witness) is probably because EasyCrypt figured out that all cards are equal.

In fact, if EasyCrypt rewrites upon input all glob types to types that are either (a) just a glob of an abstract module (no instantiation) or (b) involving only concrete modules, then this means that essentially (up to syntactic sugar), we just cannot talk about globs that are not of type (a) or (b). So counterexamples like the one I tried might well be impossible, and @oskgo might be right that there is soundness by accident (or by design?)

But this leaves some problems:

• That we cannot prove H3 using H1 means that something that has been proven for all modules might not be usable for a concrete module. Even if that does not lead to unsoundness, it might be very confusing and maybe a stopper in proofs.
• I am not sure that everything can be rewritten into globs of types (a) or (b) always. E.g., abstract-module(concrete-module). So there might be a different problem based on that. I will investigate and potentially open a separate issue.

Concerning type annotations in printing: This trick helps somewhat when debugging:

lemma visible_card ['a]: card<:'a> = fst (card<:'a>, fun (x:'a) => x).
  trivial.
qed.

and then a rewrite visible_card reveals types.

[strub]

Hi @dominique-unruh. Could you report the printing issue in a separate ticket? Otherwise, I will forget to fix it.

[dominique-unruh]

I didn't get unsoundness when using the pattern abstract-module(concrete-module) but various confusing situations.
I can't tell if they are bugs or intended, and whether they are separate from this issue or not.
But especially the lemma suspicious seems suspicious (and not just due to its name).

So I am posting them here, instead.

require import AllCore.

module type T = { proc p():bool }.
module type T1(M:T) = { proc p():bool }.
module type T2(M:T1) = { proc p():bool }.

module A:T = { var x : bool proc p():bool = { return A.x; } }.
module B(A:T) = { proc p():bool = { var r : bool; r <@ A.p(); return r; } }.
module C(B:T1) = { proc p():bool = { var r : bool; r <@ B(A).p(); return r; } }.

(* Lemma looks suspicious: C(B).p might read variables of C, so ={glob C} should not be a sufficient precondition.
   Reason for this: glob C(B) seems to rewrite to glob C. *)
lemma suspicious (C<:T2) (B<:T1): equiv [ C(B).p ~ C(B).p : ={glob C} ==> ={res} ].
  proc*.
  call (_: true).
  progress.    
qed.

(* Intuitively, lemma suspicious should give a contradiction when instantiating it with the concrete C and B from above.
   I didn't manage to do so because I get an error I don't understand.
   Maybe that's accidental, maybe this is intentional to make the glob-reasoning sound.
   In any case, it is a confusing error. *)  
lemma false_try: true.
(*

  (* invalid argument (incompatible module type):
  procedure `p' is not compatible: the function is not allowed to use B(A).p *)
  have H := suspicious C B.

  *)
  trivial.
qed.  

(* Nothing fishy here. *)
lemma correct (A<:T) &m &n: (glob A){m} = (glob A){n} => Pr[A.p() @ &m : res] = Pr[A.p() @ &n : res].
    move => H.
    byequiv.
    proc*.
    call (_: true).
    auto.
    smt.
    smt.
qed.

(* Hoping for some unsoundness because "glob B(A)" might be rewritten to something undesirable.
   Instead, EasyCrypt crashes (more precisely: an anomaly is raised that gets ProofGeneral out of sync) *)    
lemma test (B<:T1) &m &n : (glob B){m} = (glob B){n} => Pr[B(A).p() @ &m : res] = Pr[B(A).p() @ &n : res].  
  have H := correct (B(A)).