Using a Reveal expression within an Assert doesn't allow verification of an Opaque function.
@Pure
@Opaque
def pure_opaque_func() -> int:
return 3
# Can be proven
x = Reveal(pure_opaque_func())
Assert(x == 3)
# Cannot be proven
Assert(Reveal(pure_opaque_func()) == 3)
Using a Reveal expression within an Assert doesn't allow verification of an Opaque function.