"proofs" of false using clones of abstract theories

[oskgo]

I understand that this has been discussed before, but I can't access most of the old conversations and think I have a new perspective.

You can write proofs of false without using axiom or admit by using clones of abstract theories. This is because the cloning process adds any axioms not addressed by the proof ___ syntax, and those axioms might not be consistent with the parameters used for the abstract theory. Using proof * requires the ambient theory to prove all the axioms for the cloned theory.

This means that if there is no proof *, then you need to check the source code of all the dependent abstract theories, or check for axioms using automation. You cannot get by with just reading the source file and all the definitions involved in the lemma statements anymore (assuming you trust the cloned and imported theories from prior audits and that EasyCrypt validates the file).

It's possible that some researchers don't know that clones without proof * need more careful audits. I believe requiring proofs for all the axioms by default is less likely to lead to errors and would lead to more transparent code than the current default.

In cases where we would like parameters to stay uninstantiated or axioms to stay axioms (like when extending a theory of groups to a theory of cyclic groups, or a theory of groups to a theory of rings) we would have to opt out of the default.

Two different ways to mitigate the problem would be to only require proving the axioms when importing from an abstract theory to a regular theory, or to only require proofs for axioms that use no uninstantiated parameters.

Maybe this is considered a non-issue or unimportant, in which case it would still be useful to have a record of the rationale behind that decision. Maybe there could also be an "auditors guide" for what needs manual audits when looking at EasyCrypt proofs.

[alleystoughton]

It's theories in general that have this property, e.g.,

require import AllCore.

theory T.

op n : int.

axiom ax : n = 6.

end T.

clone T as U
  with op n <- 7.

print U.

(*
* In [theories]:

theory U.
  axiom ax: 7 = 6.
end U.
*)

lemma foo : false.
proof.
smt(U.ax).
qed.

What makes it challenging to solve is that often axioms are used to define what we can think of as abstract data types, as in Word.eca:

require import AllCore List Distr StdOrder.
require import FinType.
require (*--*) Tuple.
(*---*) import IntOrder RealOrder.

(* -------------------------------------------------------------------- *)
clone import FinType as Alphabet.

op n : {int | 0 <= n} as ge0_n.

type word.

op mkword : t list -> word.
op ofword : word -> t list.
op dchar  : t.

op wordw : t list = mkseq (fun _ => dchar) n.

(* -------------------------------------------------------------------- *)
lemma nosmt size_wordw: size wordw = n.
proof. by rewrite size_mkseq ler_maxr ?ge0_n. qed.

axiom nosmt mkwordK : cancel ofword mkword.

axiom nosmt ofwordK :
  forall (s : t list), size s = n =>
    ofword (mkword s) = s.

axiom nosmt mkword_out :
  forall (s : t list), size s <> n =>
    ofword (mkword s) = wordw.
...

If I remember correct Dominque Unruh and I were arguing some time (years?) ago that there should be a syntax for saying that some types and operators are not "parameters" of a theory, and so may not be instantiated. That might make sense for word, mkword, ofword and dchar above. Except that, as Pierre-Yves I believe replied, one actually might want to implement word using some concrete type.

I totally agree, though, that the status quo is not what we want. I strive to always use proof *, but of course one can't do that with Word, unless one can somehow implement the type word.

[oskgo]

Maybe there should be a mechanism for defining abstract data types in this way? In that case you could allow the related axioms to be unproven by default, and instead force them to be proven if the abstract data type is implemented.

I agree it would be useful to have some syntactical difference between types that are intended to be instantiated and types that can be left uninstantiated. There is barely any difference between abstract theories and regular theories otherwise, and it can be hard to tell the difference between parameters and abstract data types sometimes.

[alleystoughton]

The problem with abstract types is that, of course, they might be inconsistent. An alternative is the following: make Subtype and Quotient special cases with reference to the subtype and quotient type (which would be abstract), and then do what you propose, making proof * the default, so one has to explicitly mark when axioms aren't being proved. Given subtyping and quotient typing, everything else we want can be defined from concrete EasyCrypt types. So in particular, we can define bit words of length n as a subtype of bool list.

[oskgo]

If I understand you correctly you propose that we isolate all the abstract type machinery to Subtype and Quotient, making them the only exception needed? This would certainly make it harder to introduce inconsistencies on accident. I think we can do better by also preventing the final few ways to create inconsistencies with Subtype and Quotient. For Subtype we only want it to be possible to implement either just P such that P is true at some point, or every type and operator involved, with accompanying proofs for the axioms in case someone want to do a concrete implementation.

My only objection is that this would be either privileging parts of the standard library, or introducing syntax not intended for use. I suppose it would be fine if Quotient and Subtype were added to the language itself, but that has its own problems.

[alleystoughton]

Yes, that's what I meant regarding how Subtype and Quotient would be used. Essentially, this is like adding a new feature to the language. There are some other examples like the theory for the failure event lemma that are special-cased. Anyway, perhaps @strub will say if he's thinking of doing something like this or something else?

[strub]

Hi,

We (@AntoineSere) are currently adding a new mechanism to the language that will allow to define subtypes & quotients. The Subtype & Quotient libraries would then disappear & it should then be simpler to have axiom-free developments.

There is already a mechanism to tag axioms:

axiom [mytag] name : statement

and then you can pass these tags to the proof * command:

clone ... proof * [+mytag -mytag2]

I am not very confident about any heuristic that tries to decide whether an axiom should be left unproven or not. The only way to be sure that you do not have any left unattended axioms is to look at all the axioms that are in the current environment and to persuade yourself that they are consistent - think about a dev. that cloned Finite & RealDomain with the same base type (Admittedly, with the current encoding of subtypes, you're going to have a bunch of them... but as said, we are working on it) For that, we should add a command that allows to have a list of the axioms at disposition.

@alleystoughton The theory Word is an instance of Subtype (but inlined...). It should clone Subtype and not redo the work from scratch. To solve your problem about cloning Word with proof *, one could add a axiom ... subcommand to clone that allows to tell which axioms you want to left as-is.

Regarding making proof * the default, we could try that as long as we have an axiom * command - I don't think you want to state all the ordered field axioms one by one each time you need an abstract ordered field.