New Subtype theory.

[dominique-unruh]

A replacement for Subtype that permits using proof * without impossible proof obligations.
Partly resolves #275.
See #275 (comment) for some more explanations.

[dominique-unruh]

There are usually two changes needed when porting a file to the new Subtype:

Instead of

type xxx.
clone Subtype ... with type sT = xxx, pred P = ...

use

clone Subtype ... with op P = ...
type xxx = Subtype.sT

Depending on the situation, this varies a little. In DDH_hybrid, I had to remove some extra cloning because a type was duplicated. In Poly, I had to change a pred to an op because now the parameter P cannot be a pred anymore.

[strub]

I think that I am now convinced that we should allow some tag to forbid the instantiation of abstract types / operators / axioms. This would make this PR much more robust.

I am ok to merge this PR as-is anyway and to change it once the aforementioned mechanism is implemented.

[chdoc]

This PR is clearly progress with regards to the existing subType theory. However, I think it needs a cleanup pass before it can be merged. While we don't enforce 80 char lines, 160 (code) and 190 (comment) is a bit much. Similarly, the proofs should be cleaned up.

As it comes to the incompatibilities, the clone subType with type sT <- ... has always looked suspicious to me. Forcing clients to use the "defined" type sT seems preferable (and would be necessary for other fixes to #275 as well).

@dominique-unruh Did you allow maintainers to push to the PR branch? If so, I volunteer to make a pass.

[strub]

@chdoc Yes, the PR needs a cleanup and thank you for proposing yourself!

[dominique-unruh]

@chdoc Yes, I allowed maintainer edits. And I'd be happy if you could do a pass. (I'll have a look at the changes to get a feeling for the style.)

[chdoc]

@chdoc Yes, I allowed maintainer edits. And I'd be happy if you could do a pass. (I'll have a look at the changes to get a feeling for the style.)

Okay, I will make a pass. Can't promise that I will get to that today, will try though.

[oskgo]

First of all, thank you for adding some momentum to this.

This solution doesn't interact well with instantiations. I'm surprised that there are no failures in the stdlib from this. The following code fails with type `Pointed.PtSub.sT` incompatible type declaration;

abstract theory Pointed.

type T.
op point: T.
type F = T -> T.

op hits_point (f: F): bool = exists t: T, f t = point.

clone import Subtype as PtSub with 
  type T <- F,
  op P <- hits_point.

end Pointed.

abstract theory NeedsPointed.

clone import Pointed.

end NeedsPointed.

theory UsesNeedsPointed.

clone import Pointed with
  type T <= bool,
  op point <= true
  proof * by exists predT.

clone NeedsPointed with
  theory Pointed <- Pointed.

While this case can be easily worked around by instantiating NeedsPointed and its inner Pointed theory at the same time instead of instantiating it outside, this strategy does not work in the presence of multiple theories needing Pointed.

I could see this being fixed by unifying the sT and do_not_use_this_type_or_you_get_unsoundness_admit types in the two clones, but allowing this without leaving soundness holes would be a challenge.

[chdoc]

I made a pass. I called the partial inverse pinv and moved it to Logic.ec.

@oskgo This looks like an opacity/conversion issue. After all, the theory NeedsPointed.Pointed is completely unconstrained. However, from the logical point of view, NeedsPointed should probably require types/ops with certain properties rather than a specific construction.

[oskgo]

Perhaps a more realistic example:

require ZModP.

theory OtherFiles.

abstract theory ZModRingMatrices.
  clone ZModP.ZModRing as Scalars.
  (* lemmas about matrices over Z_p *)
end ZModRingMatrices.

abstract theory ZModRingCircuits.
  clone ZModP.ZModRing as Arith.
  (* lemmas about arithemtic circuits over Z_p *)
end ZModRingCircuits.

end OtherFiles.

theory FHE.

op p = 65537.

clone OtherFiles.ZModRingMatrices with 
  op Scalars.p <= p
  proof * by done.

clone OtherFiles.ZModRingCircuits with 
  theory Arith <- ZModRingMatrices.Scalars.

@chdoc Yes, there's also something weird going on here, but I don't think it makes much of a difference. If we can unify the sT from different clones, then we can likely prove false. If we can't then there is no way to have theories with subtypes with a diamond dependency.

Of course there is always the alternative to not use subtypes until the top level, and just axiomatize everything instead (or come up with some other heuristic that prevents diamond dependencies with subtypes), but this isn't ideal either. Does this mean that ZModPRing can't use subtypes?

EDIT: By the way, I think it's totally fair to say that diamond dependencies just have to deal with it for now and do some hack instead, possibly involving the do_not_use_this_type_or_you_get_unsoundness_admit type or using multiple isomorphic types with simplify hints for converting between them.

[dominique-unruh]

@oskgo
I agree that diamond structures might become hard.
I think this might be a more general problem of the cloning mechanism, not just for the Subtype.
(Think of a theory that defines a module. Different clones of it will be different, even if they are cloned in the same way, as far as I can tell.)

That being said, maybe the following approach could help in situations as the one you describe.

We keep the Subtype from this patch, but we add another theory, say SubtypeInterface which is basically the old Subtype. Then if you want diamond structures, you can do something like:

abstract theory NeedsPointed.
  clone SubtypeInterface as Sub
     with type T = int, op P = ...
     (* No proof *, OK since we are in an abstract theory *)
end NeedPointed.

theory UsePointed.
  clone Subtype as Sub 
     with type T = int, op P = ... 
  proof *. realize inhabited. ... qed.
  clone NeedsPointed with
    theory Sub <- Sub
  proof *. (* No proof obligations occur! *)
end UsePointed.

I'd be happy add this but we should agree what the names should be. (Subtype and SubtypeInterface, or something else, or maybe both inside one file.) @chdoc @strub ?

[oskgo]

@dominique-unruh It is a general problem of the cloning mechanism, but as far as I can tell it only applies to inductive type definitions right now. EasyCrypt lets you instantiate theories with equal code with each other except if they define an inductively defined type. This is part of why your subtype theory works. Only issue is that many abstract theories don't define inductive types, even if they use subtypes, and this change is a regression for those.

Keeping the old subtype theory around and using that for abstract theories sounds good.

[dominique-unruh]

@oskgo

EasyCrypt lets you instantiate theories with equal code with each other except if they define an inductively defined type. This is part of why your subtype theory works. Only issue is that many abstract theories don't define inductive types, even if they use subtypes, and this change is a regression for those.

I admit I don't fully understand this, but are you saying there would be less compatibility problems if the new Subtype would have something like

type sT = do_not_use_this_type_or_you_get_unsoundness_admit.

instead of

type sT = [Wrap of do_not_use_this_type_or_you_get_unsoundness_admit].

?

Because I don't think the inductive type here isn't really necessary, I think. (I put it in so that one cannot accidentally use sT instead of do_not_use_... and vice versa, but since one isn't supposed to use any of the ops involving do_not_use_... anyway, I guess it doesn't really matter...)

[fdupress]

Alternatively, we could classify the fact that theory instantiation doesn't allow merging identical inductive type definitions as a bug, and fix that first. (Or independently.)

@chdoc can i leave you to lead discussions here and make sure that any blockers (or even just sources of unnecessary complexity) that can be construed as EC bugs are raised and discussed in the Dev meeting?

[oskgo]

@dominique-unruh The following code might help with understanding:

require import List.

abstract theory Inner.
  type T1 = bool * bool.
  type T2 = T1 list.
  (* type T3 = [S of T3 | O]. *) (* Adding this line breaks the code *)
  op nul: int = 0.
end Inner.

abstract theory First.
  clone Inner.
end First.

abstract theory Second.
  clone Inner.
end Second.

clone First as Onest.

clone Second as Twost with
  theory Inner <- Onest.Inner.

Making sT non-inductive would fix it, yes. I thought that doing this would make things unsound but after tinkering around for a while it seems that I was wrong. I thought I could do something like the following:

abstract theory Sub.
  op x: bool.
  (* do not use *)
  op bad: bool.

  (* you can use *)
  op y: bool = bad.

  lemma eq: x = y by admit.
  lemma equi: x <=> y by smt(eq).
end Sub.

abstract theory First.
  clone Sub with
    op x <- true
    proof *.
end First.

abstract theory Second.
  clone Sub with
    op x <- false
    proof *.
end Second.

clone First as Onest.

clone Second as Twost with
  theory Sub <- Onest.Sub.

[chdoc]

I admit I don't fully understand this, but are you saying there would be less compatibility problems if the new Subtype would have something like

type sT = do_not_use_this_type_or_you_get_unsoundness_admit.

instead of

type sT = [Wrap of do_not_use_this_type_or_you_get_unsoundness_admit].

?

I can confirm that making this change makes the example from @oskgo check without problem. (@oskgo beat me to it, because I was tinkering with other cloning variants)

Alternatively, we could classify the fact that theory instantiation doesn't allow merging identical inductive type definitions as a bug, and fix that first. (Or independently.)

A-priori I see nothing wrong with this, but we should be careful. From memory, I thought that constructor names - unlike modules/procedures - had to be globally unique. However, this seems to (no longer?) be the case:

theory A.
type wrap_int = [Wrap of int].
end A.
import A.
type wrap_bool = [Wrap of bool].

@strub Was there a (recent) change concerning this?

@chdoc can i leave you to lead discussions here and make sure that any blockers (or even just sources of unnecessary complexity) that can be construed as EC bugs are raised and discussed in the Dev meeting?

I will try.

[chdoc]

Here is one way that might work (and maintain a separation between sT and do_not...admit):

Logic.ec:

type 'a wrapped = [Wrap of 'a].
op unwrap (w : 'a wrapped) = with w = Wrap x => x.

Subtype.eca:

type sT = do_not_use_this_type_or_you_get_unsoundness_admit wrapped.

Side note: one way people find lemmas is by printing theories. And printing (instances of) the new SubType theory - which does not show any of the comments - looks suspicious to say the least

[dominique-unruh]

@chdoc If you think that adding a wrapper type to the stdlib isn't too much "pollution" of the stdlib, I'd be happy to use that solution.

Side note: one way people find lemmas is by printing theories. And printing (instances of) the new SubType theory - which does not show any of the comments - looks suspicious to say the least

Maybe we rename the naughty type into do_not_use_this_type_outside_standard_library?

[chdoc]

Maybe we rename the naughty type into do_not_use_this_type_outside_standard_library?

How about do_not_instantiate_this_type. After all, type instantiation is what would cause unsoundness. Using the type isn't a problem. Since sT is just a wrapper, it is - by some definition - supposed to be used.

Anyway, this is really just a temporary stopgap measure until we get something along the lines of:

type [abstract] sT.

that excludes types from instantiation.

[oskgo]

I liked the idea of having admit in there somewhere to make it easier to find when searching for soundness issues.

[dominique-unruh]

I liked the idea of having admit in there somewhere to make it easier to find when searching for soundness issues.

I agree but for the following reasons I would keep it in the less scary form:

• It's temporary anyway until there is some abstract type support.
• The "search for admit" approach does not work with subtype uses anyway – we can skip the proof * and be unsound.
• It probably leads to less confusion, and it's clear enough for the writer.

On the long run, I'd like to: get rid of this type anyway (via [abstract]), and enforce proof * outside of abstract theories.

[oskgo]

Anyway, this is really just a temporary stopgap measure until we get something along the lines of:

type [abstract] sT.

that excludes types from instantiation.

Note that for this to work [abstract] would still have to permit being part of a theory ... <- ... instantiation, or my example breaks again.

[dominique-unruh]

As I see, @chdoc already renamed the type. So from my side, all is set? Should I do anything else or is this ready for merge?

Note that for this to work [abstract] would still have to permit being part of a theory ... <- ... instantiation, or my example breaks again.

Probably, so that will be something to keep an eye on when the [abstract] thing starts getting implemented.

[chdoc]

Note that for this to work [abstract] would still have to permit being part of a theory ... <- ... instantiation, or my example breaks again.

True, and this actually worries me a bit. If we had a proper typedef, these types (and the accompanying val and insub) would be one "package" and one could check that they arise from the same base type and predicate. Without this connection, one would possibly need to allow replacing abstract types by abstract types and I'm not sure there is a way to do this in a sound manner.

[chdoc]

@fdupress How worried are you about the impact of this change on other projects that are not (yet) in our CI?

[oskgo]

Note that for this to work [abstract] would still have to permit being part of a theory ... <- ... instantiation, or my example breaks again.

True, and this actually worries me a bit. If we had a proper typedef, these types (and the accompanying val and insub) would be one "package" and one could check that they arise from the same base type and predicate. Without this connection, one would possibly need to allow replacing abstract types by abstract types and I'm not sure there is a way to do this in a sound manner.

It's going to be a problem for any use of [abstract] inside a theory intended to be cloned though, not just in Subtype. I think that banning op ... <- .../type ... <- ... while allowing theory ... <- ... would enable building sound abstractions. There would have to be some care taken by the user such that the operator/type occurs in axioms or lemmas (this prevents instantiation that does not use the same operator/type) but that should be it.

It's just something to keep in mind for the [abstract] implementation. I just wanted to mention this while I remember. This shouldn't be a blocker for this PR in my opinion.

Glad we could get diamond cloning working. I have been wanting movement towards proof * by default for a while. I've ran out of objections.

[chdoc]

Yes, the (potential) issues with [abstract] are of no concern to this PR.

It's just a data point that maybe, rather than having cloning restrictions for abstract theories, we just want a (primitive) typedef, similar to what is done in other HOL-based theorem provers.

Waiting for @alleystoughton and @fdupress to respond, but this looks good to me.

[fdupress]

@fdupress How worried are you about the impact of this change on other projects that are not (yet) in our CI?

Not worried about the ones I have sight of: very little exotic (as in, not also done in stdlib or examples) use of subtypes.

Kyber and Dilithium most likely to go wonky: I'll give them a check tomorrow and perhaps pull them and the rest into the external CI. (Kyber and Dilithium are checked with expected cost, so I'll still need to run a manual check.)

[alleystoughton]

Seems fine to me!

[chdoc]

Looking at Dilithium, I'm not too worried. there are only two uses of Subtype, one of them will require the "default fix".

In fact, Kyber and Dilithium both use quotients, which - for similar reasons as for subtypes - come with an unprovable axiom. So maybe this should receive a similar treatment or be implemented using subtypes+choice.

[strub]

Alternatively, we could classify the fact that theory instantiation doesn't allow merging identical inductive type definitions as a bug, and fix that first. (Or independently.)

Yes. That's a defect of the cloning mechanism for types. We should allow merging identical induction type. Let's fix that and we can merge this PR as is.

[strub]

Note only that I started implementing a proper native "subtype" mechanism -- with value dependency. So I expect the Subtype theory to be pruned at some point.