Potential unsoundness in clones
Hi!
While investigating a fix to an unsoundness in Creusot, I stumbled on what seems like an unsoundness in Why3's handling of clones:
module C222_A_Mktrue_Interface
type self
function mktrue (_ : ()) : bool
end
module C222_A_Mktrue
type self
function mktrue (_ : ()) : bool = true
end
module C222_A_IsTrue_Interface
type self
clone C222_A_Mktrue_Interface as Mktrue0 with type self = self
val function is_true (_ : ()) : ()
ensures { Mktrue0.mktrue () = true }
end
module C222_Impl0_Mktrue
function mktrue (_ : ()) : bool = false
end
module C222_Impl0
clone C222_Impl0_Mktrue as Mktrue0
clone C222_A_IsTrue_Interface as IsTrue0 with type self = (), function Mktrue0.mktrue = Mktrue0.mktrue
end
module Boom
clone C222_Impl0
goal x : false
end
At the very least I am proving false
and I don't think I've intentionally introduced axioms.