Add opaque keyword to Laurel grammar

[keyboardDrummer]

Summary

Adds an explicit opaque keyword to the Laurel grammar. Previously, a procedure was implicitly opaque when it had ensures clauses, which sometimes meant one had to add ensures true just to make something opaque. Now the opaque keyword must be explicitly specified.

Syntax

The opaque keyword is placed between requires/invokeOn and ensures clauses:

procedure foo()
  opaque
{
    assert true;
    assert false
};

procedure opaqueBody(x: int) returns (r: int)
  requires x > 0
  opaque
  ensures r > 0
  modifies c
{
  ...
};

procedure bodiless() returns (r: int)
  opaque
  ensures r > 0
;

Changes

Grammar (LaurelGrammar.st)

• Added OpaqueClause category with opaqueClause op
• Added optional opaque parameter to both procedure and function ops, positioned between invokeOn and ensures

Parser (ConcreteToAbstractTreeTranslator.lean)

• Updated parseProcedure to accept 10 arguments (was 9) including the new opaqueArg
• Body determination now uses the explicit opaque flag instead of inferring from postconditions

Formatter (LaurelFormat.lean)

• formatBody now outputs opaque for Body.Opaque variants
• Reordered output to put ensures before modifies (matching grammar order)

Test updates

• All Laurel test procedures with ensures clauses now include opaque
• Procedures that only had ensures true now use just opaque (the ensures true is removed)
• Removed comments about considering more explicit opaque syntax
• Updated PythonRuntimeLaurelPart.lean Laurel source strings
• Updated expected outputs in LiftHolesTest, ConstrainedTypeElimTest, PreludeVerifyTest, and T8c_BodilessInlining

Testing

All tests pass except the pre-existing StrataTest.DDM.Integration.Java.TestGen failure (missing jar file, unrelated to this change).

[keyboardDrummer]

@keyboardDrummer-bot please resolve the conflicts

[fabiomadge]

I think #668 supersedes this. Both add opaque to address the implicit "has ensures ⇒ opaque" rule, but #668's approach is stronger:

• Prefix syntax (opaque function f()) matches Lean/Dafny conventions vs. postfix placement here.
• Function-only scope — opaque on procedures is a no-op since they're always modular at the Core level.
• Transparent-with-postconditions — ensures without opaque becomes a useful new combination (body visible + postcondition checked), rather than requiring opaque for any ensures.
• No silent postcondition loss — in this PR, writing ensures without opaque silently drops the postconditions (no error). On main they were honored. feat: support postconditions on Laurel functions #668 avoids this since ensures without opaque has well-defined semantics.

[keyboardDrummer]

I think #668 supersedes this. Both add opaque to address the implicit "has ensures ⇒ opaque" rule, but #668's approach is stronger:

• Prefix syntax (opaque function f()) matches Lean/Dafny conventions vs. postfix placement here.

Could you explain why that is stronger?

• Function-only scope — opaque on procedures is a no-op since they're always modular at the Core level.

Does it matter whether Core procedures are modular or not? This is about Laurel procedures.

• Transparent-with-postconditions — ensures without opaque becomes a useful new combination (body visible + postcondition checked), rather than requiring opaque for any ensures.

It's disallowed by design to reduce VC size. Why would you allow this?

• No silent postcondition loss — in this PR, writing ensures without opaque silently drops the postconditions (no error). On main they were honored. feat: support postconditions on Laurel functions #668 avoids this since ensures without opaque has well-defined semantics.

Are you sure? Should be a syntax error in this PR

[fabiomadge]

Could you explain why that is stronger?

Aesthetic preference — opaque function f() reads more naturally and is consistent with Lean and Dafny.

Does it matter whether Core procedures are modular or not? This is about Laurel procedures.

opaque on a procedure has no semantic difference — verification results are identical with or without it. Adding a keyword with no semantic difference is confusing for users.

It's disallowed by design to reduce VC size. Why would you allow this?

Even when the body is visible, the postcondition axiom can help the solver. If the body is complex (recursive, many branches), deriving the postcondition from the body alone may be hard. The axiom acts as a proof hint — logically redundant but practically useful.

Are you sure? Should be a syntax error in this PR

I tested on a clean build of this branch. procedure foo() returns (r: int) ensures r > 100 { r := 1 } without opaque parses successfully — the DDM grammar accepts it. The postcondition is silently dropped: the body is inlined (transparent), and the postcondition violation is never caught. No error or warning is emitted.

[keyboardDrummer]

opaque on a procedure has no semantic difference — verification results are identical with or without it. Adding a keyword with no semantic difference is confusing for users.

Procedures will support both being opaque or transparent. In the upcoming #927 we will support them being transparent if the body is an expression. I'll also add an error for statement bodies marked as transparent.

Aesthetic preference — opaque function f() reads more naturally and is consistent with Lean and Dafny.

I thought of having it there first, but it relates to ensures clauses and the body, so seems better to locate it there. It doesn't seem important enough to be the first thing that is mentioned when reading the procedure definition. Do you have a strong opinion about this?

It's disallowed by design to reduce VC size. Why would you allow this?

Even when the body is visible, the postcondition axiom can help the solver. If the body is complex (recursive, many branches), deriving the postcondition from the body alone may be hard. The axiom acts as a proof hint — logically redundant but practically useful.

That's right. I think that separate lemmas are better for this use-case since then you don't always get the postcondition. We can offer ways to automatically invoke lemmas, like Verus' broadcast mechanism, so you don't have the boilerplate of having to manually call them.

We can also still decide to allow postconditions and a transparent body, but it's much easier to start than to stop allowing it, so I'd rather stick with not allowing it unless we're absolutely sure we do want to allow it.

I tested on a clean build of this branch. procedure foo() returns (r: int) ensures r > 100 { r := 1 } without opaque parses successfully — the DDM grammar accepts it. The postcondition is silently dropped: the body is inlined (transparent), and the postcondition violation is never caught. No error or warning is emitted.

You're right, updated the PR, thanks.

[keyboardDrummer]

@keyboardDrummer-bot can you resolve the build issues?

[keyboardDrummer]

There should be clear upside to taking something away from users.

I wouldn't call it taking something away because it's never been there.

I don't see what the restriction buys us.

What part of the explanation I gave does not make sense to you? Here it is again:

I think the purpose of a postcondition is to enable encapsulating the body, so it doesn't make sense to have a postcondition and a transparent body. If you want to use the postcondition not for encapsulation but to prove additional properties, then I think it's better to use a different construct, like a lemma.

requires, ensures, modifies all take arguments. opaque alone in that position looks incomplete.

If you would use opaque as a prefix, it would also not take any arguments. What's the difference?

What do you think of the arguments I gave in favor of putting it where this PR puts it?

It also creates visual ambiguity with multiple ensures clauses — is it opaque ensures r > 0 ensures r < 100 or three separate clauses? Prefix avoids this entirely.

Why would someone think that it needs to be repeated?

[robin-aws]

FWIW, here are my opinions on this, in the hopes of tie-breaking:

1. Since Laurel programs are almost exclusively produced from other sources and not written directly, I don't think the syntax matters nearly as much as it does in Lean or Dafny. I also think opaqueness is less fundamental when verification is not the only possible backend. I'm fine with printing it as an argument-less clause as it's just plain easier to implement.
2. I do think it's useful to make opaqueness orthogonal to the specification. I agree with @keyboardDrummer that in many cases you're better off using a lemma instead, but I don't think we're in a position to be so strongly opinionated about it that we don't even support adding an ensures clause without changing opacity.

It also creates visual ambiguity with multiple ensures clauses — is it opaque ensures r > 0 ensures r < 100 or three separate clauses? Prefix avoids this entirely.

If this is about the awkward readability when you put multiple clauses on one line, again I think it's less of a concern since the vast majority of the time we're only going to be printing out source code from translated ASTs, so we'll always have the newlines.

[keyboardDrummer]

FWIW, here are my opinions on this, in the hopes of tie-breaking:

1. Since Laurel programs are almost exclusively produced from other sources and not written directly, I don't think the syntax matters nearly as much as it does in Lean or Dafny. I also think opaqueness is less fundamental when verification is not the only possible backend. I'm fine with printing it as an argument-less clause as it's just plain easier to implement.
2. I do think it's useful to make opaqueness orthogonal to the specification. I agree with @keyboardDrummer that in many cases you're better off using a lemma instead, but I don't think we're in a position to be so strongly opinionated about it that we don't even support adding an ensures clause without changing opacity.

Okay, well (2) is not in scope of this PR. Can you provide your preference for the opaque keyword location? My suggestion would be that if it is not tied to ensures clauses, put it after the ensures clauses, right before the body, and otherwise put it right before the ensures clauses.

[robin-aws]

I don't have a strong preference for the ordering really. Can we support parsing it in either location?

In Dafny I always liked ordering things as:

    requires
    reads
    modifies
    ensures
    decreases

Mainly I liked thinking of requires as "happening before the body", the reads and modifies as "happening during the body", and the ensures as "happening after the body". In retrospect having decreases before the ensures might make more sense as it's also about the ordering of calls made within the body.

With that in mind, I suppose I weakly prefer having it before the ensures.

[fabiomadge]

If you would use opaque as a prefix, it would also not take any arguments. What's the difference?

As a prefix it's a modifier like public or abstract. Argumentless is expected there. Among requires X, ensures X, modifies X, it's the odd one out.

What do you think of the arguments I gave in favor of putting it where this PR puts it?

I understand them. I think the arguments against outweigh them.

Why would someone think that it needs to be repeated?

opaque without an argument among the clauses is ambiguous about its scope. Prefix makes it clear it applies to the whole declaration.

it's just plain easier to implement

By a few lines of parser code.

On ordering: ideally the clause order wouldn't be enforced. If it is, I'd put opaque last, right before the body, since that's what it affects:

procedure foo(x: int) returns (r: int)
  requires x > 0
  ensures r > 0
  modifies c
  opaque
{ r := x };

I still prefer prefix, but this seems like the best postfix option to me.

[keyboardDrummer]

As a prefix it's a modifier like public or abstract. Argumentless is expected there. Among requires X, ensures X, modifies X, it's the odd one out.

I see. I think you're saying that in Java (and other languages?) the modifier keywords are all at the front. That's fair. It makes sense to base syntax on existing languages. In Laurel that precedent had already been violated though, abstract and external are currently also not prefixes. They replace the body.

opaque without an argument among the clauses is ambiguous about its scope. Prefix makes it clear it applies to the whole declaration.

What do you mean with applying to a whole declaration? I wouldn't say it does that since the signature is unaffected. If we put it before ensures/modifies/body, then it's right before the things that it affects.

On ordering: ideally the clause order wouldn't be enforced. If it is, I'd put opaque last, right before the body, since that's what it affects:

If it wouldn't affect the ensures and modifies clause, then I agree, but right now it does affect those. A transparent procedure can not have ensures or modifies clause (unrelated to this PR).

@robin-aws @fabiomadge I'm not feeling any strong objections to this PR from either of you. Can you approve it?

Future looking discussion on disconnected opaque and ensures+modifies

A question I have for both @robin-aws and @fabiomadge is whether you think a modifies clause should be possible on a transparent procedure. For a transparent procedure you will never have to add it, since the heap is not havoc'ed when calling such a procedure: the state of the heap can be inferred from the body. Adding a modifies clause just provides a separate way of learning something about the heap, as a sort of heuristic.

[fabiomadge]

whether you think a modifies clause should be possible on a transparent procedure

Yes. It serves as checked documentation of heap access and catches accidental writes to things the procedure shouldn't touch.

[keyboardDrummer]

whether you think a modifies clause should be possible on a transparent procedure

Yes. It serves as checked documentation of heap access and catches accidental writes to things the procedure shouldn't touch.

Okay, I'm open to discussing the opaque vs ensures+modifies.