[Easycrypt-club] How to use local variable in a lemma

François Dupressoir fdupress at gmail.com
Mon Jan 22 11:11:49 CET 2018


Hello Sarah,

You cannot use local variable x in the statement of a lemma: at the points where the precondition and postcondition are interpreted (semantically), the variable does not exist in memory.

Going slightly further, although EasyCrypt lets you define G as you did, it should have warned that x was used before being defined. This will be problematic for a lot of proofs (in particular anything that involves probabilities will likely be very hard to prove—probabilistic and non-deterministic behaviours do not mix).

So you have two options moving forward:
1) Make x a parameter to procedure G.g (and your statement will then mean what you want);
2) Make x a global variable of module G (and you then need to replace x with G.x in your theorem statement).

That being said, I do not want to necessarily close the discussion on interpreting pure hoare specifications for non-deterministic procedures: if you feel you really need this, please do try and convince us (mostly Pierre-Yves and Benjamin).

Best,
François

From: sarah chabane
Sent: 22 January 2018 10:00
To: easycrypt-club at lists.gforge.inria.fr
Subject: [Easycrypt-club] How to use local variable in a lemma

Hi, 
I need to use a local variable of a procedure in a lemma, 

for example , for this module : 

module G = {
 proc g() : int ={
  var r, x : int;
  if (x < 0) {
   r = 5; } else {
   r = 10;
  }
  return r;
 }
}.

I want to proof this lemma: 

lemma ex : forall v, 
 hoare [ G.g : v = x ==> if v < 0  then  res = 5 else res <> 5 ].

How can i use the x of the proc G.g ? 


Best regards.
Sarah.

-------------- section suivante --------------
Une pièce jointe HTML a été nettoyée...
URL: <http://lists.gforge.inria.fr/pipermail/easycrypt-club/attachments/20180122/f7641db5/attachment.html>


More information about the Easycrypt-club mailing list