search

EasyCrypt / easycrypt

EasyCrypt: Computer-Aided Cryptographic Proofs
MIT License
320 stars 49 forks source link

Failure to instantiate abstract ADT together with its constituent in abstract theory #567

Open oskgo opened 5 months ago

oskgo commented 5 months ago

Usually we can instantiate an ADT with another that is defined the same way. This can fail when the definition includes a type that is also part of the abstract theory and thus also has to be instantiated.

The following example prints unknown symbol: Top.T.t:

abstract theory T.
  type t.
  type t' = [wrap of t].
  op usewrap: bool = predT wrap.
end T.

clone T as T1.

clone T as T2 with
type t <- T1.t,
type t' <- T1.t'.

Also instantiating usewrap fixes the issue, but this scales with the number of uses of wrap. Another workaround is to do the final clone in two steps:

clone T as Ttemp with
type t <- T1.t.

clone Ttemp as T2 with
type t' <- T1.t'.