assert ... by ... #970
assert ... by ... #970
Conversation
There was a problem hiding this comment.
In general, I am happy to introduce more high-level proof "strategies" in Gobra to make proofs clearer. However, I think we should perhaps consider how such a feature may evolve and think of a syntax that is consistent with those ideas.
First, we are introducing a new keyword "derive", which may be undesirable, and it is not clear to me why that is the case (couldn't we have an assert ... by ... like in Dafny or Verus?). Maybe a reason for that is that this is not a "full assert", in that we cannot assert impure assertions, but I don't think that is a good enough reason to introduce an entirely new concept ("deriving"). Maybe, it would be enough to produce an error message like "Proofs by contradiction cannot be used to prove impure assertions".
Second, nothing in the syntax suggests that this proof is done by contradiction, and I would imagine that this may confuse some people. I think we could, instead, provide syntactic hints that indicate which proof strategy we want to use, like assert P by contra { ... }. If no strategy is selected, than by default we could do the same transformation as Dafny's "assert by". This syntax is also extensible in case we want to introduce additional strategies (possible ideas for these strategies can be found in section 30 of the Verus docs: https://verus-lang.github.io/verus/guide/reference-assert-by.html)
|
|
jcp19
left a comment
jcp19
left a comment
There was a problem hiding this comment.
LGTM, but I do have a few minor comments
| case PUnfold(acc) => wellDefFoldable(acc) | ||
| case n: PAssertBy => | ||
| isExpr(n.exp).out ++ | ||
| isPureExpr(n.exp) ++ |
There was a problem hiding this comment.
Checking the condition is pure makes total sense for proofs by contradiction, but I wonder if this is too strict for regular assert-by. At any rate, the current design is already usable and I am happy with keeping it and extending it later if needed.
| val (pos, info, errT) = n.vprMeta | ||
| val src = n.info | ||
| val nonDetChoice = in.LocalVar(ctx.freshNames.next(), in.BoolT(Addressability.exclusiveVariable))(src) | ||
| val errInfo = n.vprMeta._2.asInstanceOf[Source.Verifier.Info] |
There was a problem hiding this comment.
| val errInfo = n.vprMeta._2.asInstanceOf[Source.Verifier.Info] | |
| val errInfo = info.asInstanceOf[Source.Verifier.Info] |
There was a problem hiding this comment.
the cast might not be necessary, I guess, in which case we can just drop that var
| // if (!P) { L; assert false } | ||
| val (pos, info, errT) = n.vprMeta | ||
| val assertFalse = vpr.Assert(vpr.FalseLit()(pos, info, errT))(pos, info, errT) | ||
| val errInfo = n.vprMeta._2.asInstanceOf[Source.Verifier.Info] |
| reason match { | ||
| case reason: reasons.AssertionFalse => | ||
| reporting.AssertByError(errInfo) | ||
| .dueTo(reporting.AssertByContraBodyError(reason.offendingNode.info.asInstanceOf[Source.Verifier.Info])) |
| reason match { | ||
| case reason: reasons.AssertionFalse => | ||
| reporting.AssertByError(errInfo) | ||
| .dueTo(reporting.AssertByProofBodyError(reason.offendingNode.info.asInstanceOf[Source.Verifier.Info])) |
There was a problem hiding this comment.
I wonder if the cast here is necessary
| thenBranch = vu.seqn(Vector(proof, assertFalse))(pos, info, errT) | ||
| elseBranch = vu.nop(pos, info, errT) | ||
| _ <- cl.errorT({ | ||
| case e@errors.AssertFailed(_, reason, _) if e causedBy assertFalse => |
There was a problem hiding this comment.
To be clear, this assertion applies to all asserts in the proof too, no? It might be confusing to get an "contradiction might not be derivable" error when a regular, user provided assertion fails
2 participants
This PR introduces two styles to derive an assertion:
assert P by { L }andassert P by contra { L }The former proves
Pusing the proofLand then throws away the proof context, similar to how Dafny does it. More specifically, the former is encoded asif(*) { L; assert P; assume false }; assume P.The latter performs a proof by contradiction and is encoded as
if (!P) { L; assert false }.Outdated description
Introduces a new statement
derive <cond> by <block>to derivecondby performing a proof by contradiction. This is particularly useful in connection with opaque functions as their body is revealed withinblockwithout spilling to the rest of the method as the branch evaluatingblockresults in a contradiction and is, thus, killed.Closes #969