Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Clustering (--comparefuns for equivalence checking) #931

Open
wants to merge 7 commits into
base: scala-2
Choose a base branch
from

Conversation

drganam
Copy link
Collaborator

@drganam drganam commented Mar 11, 2021

Introduces two command line options: --comparefuns and --models, for equivalence checking of specified functions

@CLAassistant
Copy link

CLAassistant commented Mar 11, 2021

CLA assistant check
All committers have signed the CLA.

@drganam drganam marked this pull request as draft March 11, 2021 17:43
@drganam drganam marked this pull request as ready for review March 11, 2021 17:45
@vkuncak vkuncak changed the title Clustering Clustering (--comparefuns for equivalence checking of specified functions) Mar 12, 2021
@vkuncak vkuncak changed the title Clustering (--comparefuns for equivalence checking of specified functions) Clustering (--comparefuns for equivalence checking) Mar 12, 2021
val postcondition = function.postcondition

val precondition = exprOps.preconditionOf(function.fullBody) //function.precondition
val postcondition = exprOps.postconditionOf(function.fullBody) //function.postcondition
val bodyPre = exprOps.withPrecondition(body, precondition)
val bodyPost = exprOps.withPostcondition(bodyPre,postcondition)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Could you try to manipulate specifications (getting pre/postconditions, and changing them), using the new BodyWithSpecs API?

@vkuncak
Copy link
Collaborator

vkuncak commented Mar 31, 2021

@drganam : I just realized that @traceInduct uses .holds pattern for specifying these statements.
We have moved away from it to make it easier to not inline proofs and only keep lemma statements.
So, in the running example, it would be better to have

@opaque
def zero_check(arg: BigInt): Boolean = {
  if (arg > 0) zero_check(arg - 1)
  else true
} ensuring (res =>   zero1(arg) == zero2(arg))


case Some(paths) =>
// Support wildcard `_` as specified in the documentation.
// A leading wildcard is always assumes.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Small typo: assumed


case Some(paths) =>
// Support wildcard `_` as specified in the documentation.
// A leading wildcard is always assumes.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Same here for "assumes", perhaps you could factor this code into a common function

Induction and @traceInduct annotation
-------------------------------------

We introduce the @traceInduct annotation for automating proofs using induction. Stainless will transform the annotated lemma by generating the inductive proof, based on the structure of one of the functions that appear in the lemma. This approach is useful for functions that have simple inductive form and are easily mapped into inductive proofs.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You can surround @traceInduct (and other code) with backquotes like this ``@traceInduct``.

@drganam
Copy link
Collaborator Author

drganam commented May 14, 2021

@jad-hamza @vkuncak the latest implementation (with ensurings and the new BodyWithSpecs API) is here: #1052

@vkuncak vkuncak added the old Work that is substantially behind master label May 20, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
old Work that is substantially behind master
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants