Proving false using unproven lemmas

[mortensol]

Hi, it appears I am able to prove false in an EasyCrypt file where I am importing another file containing an incomplete "proof" of false.

Here is a minimal working example. I have one file called Test1.ec which looks like this:

lemma f1 : false.
proof.
qed.

Trying to run this of course results in an error: cannot save an incomplete proof.

But the following works fine.

require import Test1.

lemma f2 : false.
apply f1.
qed. 

So I am able to apply f1 from Test1.ec in the proof of f2 even though I don't have a proof for f1.

Is it supposed to be like this, and if so, why?

[strub]

Hou, good catch.

[fdupress]

I'm not sure this is a bug: there is a command-line flag to recursively check required theories -check-all, but we need to otherwise trust that the required theories contain only valid proofs (and trust that they are checked separately).

[mortensol]

Running easycrypt Test2.ec -check-all does not produce an error (Test2.ec is the file where I prove f2).

[fdupress]

I just checked: easycrypt Test2.ec -check-all does fail as expected except when there is a .eco file present indicating that Test2.ec has already been successfully checked. (In which case, it doesn't even try and just succeeds.)

The .eco should probably record the checking mode (including weak/full and recursive/non-recursive). This is certainly a bug.

But I'm still not convinced the original report is a bug.

[oskgo]

I would expect easycrypt to recursively check any dependencies without a valid .eco file and generate one by default. Not checking dependencies should, in my opinion, be the behavior that requires an additional option.

[chdoc]

I would expect easycrypt to recursively check any dependencies without a valid .eco file and generate one by default. Not checking dependencies should, in my opinion, be the behavior that requires an additional option.

That's something to be discussed. But the point of @fdupress was that EC should actually check the theory given on the command line when there is a -check-all argument and the .eco file has been generated without the recursive check.

Here one could also argue that it is reasonable to expect that a file given as argument is checked regardless of whether there already exists a .eco or not. Either way, EC should record the option in the .eco file to allow to correctly short-circuit -check-all invocations.

[strub]

After discussing this with @bgregoir, we came to a conclusion that we should add a flag that would enforce the behavior that you just described. However, the flag won’t be set by default and a warning will then be emitted when loading a .ec file whose .eco is out of date

[strub]

Either way, EC should record the option in the .eco file to allow to correctly short-circuit -check-all invocations.

Yes, the .eco file should record how the file has been checked.